Commit 515bb4d9 authored by Gilles Coremans's avatar Gilles Coremans
Browse files

Very basic implementation of QuickCheck-type generator for System F ASTs

parent 771b759b
module SystemFImpl (
isVal,
getTypeFromEnv,
stepEval,
fullEval,
typeOf
) where
import HaskellOutput
isVal :: Term -> Bool
......
import Test.QuickCheck
import Control.Monad
import SystemFImpl
import HaskellOutput
----
-- 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))
----
-- 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))
----
-- 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))
----
-- Instances
----
instance Arbitrary Term where
arbitrary = sized $ genterm 0 0
instance Arbitrary Type where
arbitrary = sized $ gentype 0
----
-- 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 (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
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