Commit 57de48e8 authored by Gilles Coremans's avatar Gilles Coremans
Browse files

Improvements on the variable generator that don't seem to actually

improve anything
parent 515bb4d9
......@@ -4,75 +4,86 @@ import Control.Monad
import SystemFImpl
import HaskellOutput
data Abs = Term | Type
----
-- Terms
----
genterm :: Int -> Int -> Int -> Gen Term
genterm ted _ 0 = liftM TmVar $ gentermvar ted
genterm ted tyd n =
frequency [(n^3 - n^2,
oneof [ liftM2 TmAbs (genterm (ted+1) tyd (2*(n `div` 3))) nextTy,
liftM2 TmApp nextTe nextTe,
liftM2 TmTApp nextTe nextTy,
liftM TmTAbs (genterm ted (tyd+1) (2*(n `div` 3)))
]),
(n^2,
liftM TmVar $ gentermvar ted)]
where
nextTe = genterm ted tyd (2*(n `div` 3))
nextTy = gentype tyd (2*(n `div` 3))
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 :: Int -> Int -> Gen Type
gentype tyd 0 = oneof [return TyBase,
liftM TyVar $ gentypevar tyd]
gentype tyd n =
frequency [(n^3 - n^2,
oneof [ liftM2 TyArr nextTy nextTy,
liftM TyAll $ gentype (tyd+1) (2*(n `div` 3))
]),
(n^2,
gentype tyd 0)]
where
nextTy = gentype tyd (2*(n `div` 3))
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 :: Int -> Gen HNat
gentermvar 0 = return $ termvar 1
gentermvar 1 = gentermvar 0
gentermvar d = frequency [(prob, return $ termvar (d-1)),
(1000-prob, gentermvar (d-1))]
where
prob = 1000 `div` d
termvar :: Int -> HNat
termvar 0 = Z
termvar d = STermVar (termvar (d-1))
gentypevar :: Int -> Gen HNat
gentypevar 0 = return $ typevar 1
gentypevar 1 = gentypevar 0
gentypevar d = frequency [(prob, return $ typevar (d-1)),
(1000-prob, gentypevar (d-1))]
where
prob = 1000 `div` d
typevar :: Int -> HNat
typevar 0 = Z
typevar d = STypeVar (typevar (d-1))
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))
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 0 0
arbitrary = sized $ genterm []
instance Arbitrary Type where
arbitrary = sized $ gentype 0
arbitrary = sized $ gentype []
----
-- Properties
......@@ -91,13 +102,13 @@ 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 (termNodes t) $
collect (typeOf t Nil) $
True
termNodes :: Term -> Int
termNodes (TmVar _) = 1
termNodes (TmAbs t _) = 1 + termNodes t
termNodes (TmApp t1 t2) = 1 + (termNodes t1) + (termNodes t2)
termNodes (TmTApp t _) = 1 + termNodes t
termNodes (TmTAbs t) = 1 + termNodes t
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
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