Commit 487e2451 authored by Gilles Coremans's avatar Gilles Coremans
Browse files

New implementation using type-based generation and the Alternative

typeclass
parent ddbdf385
import Test.QuickCheck
import Control.Monad
import Control.Applicative
import qualified Data.Array as Arr
import SystemFImpl
import HaskellOutput
import Comble
data Abs = Term | Type
----
-- Terms
----
genterm :: [Abs] -> Int -> Gen Term
genterm [] 0 = return $ TmAbs (TmVar Z) (TyBase)
genterm var 0 = liftM TmVar $ gentermvar var
genterm [] n = nonvarterm [] n
genterm var n = frequency [(n^3 - n^2, nonvarterm var n),
(n^2, liftM TmVar $ gentermvar var)]
nonvarterm :: [Abs] -> Int -> Gen Term
nonvarterm var n = oneof [liftM2 TmAbs (genterm (Term:var) (2*(n `div` 3))) nextTy,
liftM2 TmApp nextTe nextTe,
liftM2 TmTApp nextTe nextTy,
liftM TmTAbs (genterm (Type:var) (2*(n `div` 3)))]
where
nextTe = genterm var (2*(n `div` 3))
nextTy = gentype var (2*(n `div` 3))
----
-- Types
----
gentype :: [Abs] -> Int -> Gen Type
gentype var 0 = oneof [return TyBase,
liftM TyVar $ gentypevar var]
gentype var n =
frequency [(n^3 - n^2,
oneof [ liftM2 TyArr nextTy nextTy,
liftM TyAll nextTy
]),
(n^2,
gentype var 0)]
where
nextTy = gentype var (2*(n `div` 3))
----
-- Variables
----
gentermvar :: [Abs] -> Gen HNat
gentermvar [] = gentermvar' []
gentermvar (Term:as) = gentermvar' $ reverse as -- First abstraction is a Term => skip it
gentermvar (Type:as) = gentermvar' $ reverse (Type:as)
gentermvar' :: [Abs] -> Gen HNat
gentermvar' [] = return $ mkvar []
gentermvar' (Type:as) = gentermvar' as -- Last abstraction needs to be a Term
gentermvar' (Term:as) = frequency [(prob, return $ mkvar $ reverse $ Term:as),
(1000-prob, gentermvar' as)]
where
prob = 1000 `div` (length (Term:as))
gentypevar :: [Abs] -> Gen HNat
gentypevar [] = gentypevar' []
gentypevar (Type:as) = gentypevar' $ reverse as -- First abstraction is a Type => skip it
gentypevar (Term:as) = gentypevar' $ reverse (Type:as)
gentypevar' :: [Abs] -> Gen HNat
gentypevar' [] = return $ mkvar []
gentypevar' (Term:as) = gentypevar' as
gentypevar' (Type:as) = frequency [(prob, return $ mkvar $ reverse $ Term:as),
(1000-prob, gentypevar' as)]
where
prob = 1000 `div` (length (Type:as))
gentermoftype :: Alternative alt => Type -> Env -> Int -> alt Term
gentermoftype (TyBase) env 0 = asum [pure (TmNum n) | n <- [1..10]] -- Size zero constants: constants or variables
<|> asum (varsmatching TyBase env)
gentermoftype t env 0 = asum (varsmatching t env) -- Size zero for other types: a matching variable if one exists
gentermoftype (TyBase) env n = -- Constants
asum [TmApp <$> gentermoftype (TyArr t TyBase) env n1 <*> gentermoftype t env n2 | t <- typesofsize n, (n1,n2) <- split2 (n-1)]
<|> asum (varsmatching TyBase env)
<|> asum [pure (TmNum i) | i <- [1..10]]
gentermoftype (TyAll t) env n = -- Type abstraction
asum [TmApp <$> gentermoftype (TyArr t2 (TyAll t)) env n1 <*> gentermoftype t2 env n2 | t2 <- typesofsize n, (n1,n2) <- split2 (n-1)]
<|> asum (varsmatching (TyAll t) env)
<|> (TmTAbs <$> gentermoftype t (ETypeVar env) (n-1))
gentermoftype (TyArr l r) env n = -- Function types
asum [TmApp <$> gentermoftype (TyArr t (TyArr l r)) env n1 <*> gentermoftype t env n2 | t <- typesofsize n, (n1,n2) <- split2 (n-1)]
<|> asum (varsmatching (TyArr l r) env)
<|> (TmAbs <$> gentermoftype r (ETermVar l env) (n-1) <*> pure l)
gentermoftype (TyVar h) env n = -- Type variables
asum [TmApp <$> gentermoftype (TyArr t (TyVar h)) env n1 <*> gentermoftype t env n2 | t <- typesofsize n, (n1,n2) <- split2 (n-1)]
<|> asum (varsmatching (TyVar h) env)
varsmatching :: (Alternative alt) => Type -> Env -> [alt Term]
varsmatching a b = undefined
typesofsize :: Int -> [Type]
typesofsize n = undefined
mkvar :: [Abs] -> HNat
mkvar [] = Z
mkvar (Term:as) = STermVar (mkvar as)
mkvar (Type:as) = STypeVar (mkvar as)
----
-- Instances
----
instance Arbitrary Term where
arbitrary = sized $ genterm []
instance Arbitrary Type where
arbitrary = sized $ gentype []
----
-- Properties
----
notLeft :: Either a b -> Bool
notLeft (Right _) = True
notLeft (Left _) = False
prop_checks :: Term -> Bool
prop_checks t = notLeft $ typeOf t Nil
maybeTrue :: Maybe Bool -> Bool
maybeTrue (Just b) = b
maybeTrue Nothing = False
prop_checksinvariant t = notLeft (typeOf t Nil) ==> maybeTrue $ fmap notLeft $ fmap ((flip typeOf) Nil) (stepEval t)
prop_dummy :: Term -> Property
prop_dummy t = collect (termSize t) $
collect (typeOf t Nil) $
True
termSize :: Term -> Int
termSize (TmVar _) = 1
termSize (TmAbs t _) = 1 + termSize t
termSize (TmApp t1 t2) = 1 + (termSize t1) + (termSize t2)
termSize (TmTApp t _) = 1 + termSize t
termSize (TmTAbs t) = 1 + termSize t
......@@ -35,6 +35,7 @@ data Term
| TmTApp Term
Type
| TmTAbs Term
| TmNum Int
deriving (Show, Eq)
data HNat
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment