|
Packit |
1d8052 |
{-# LANGUAGE ScopedTypeVariables, TemplateHaskell #-}
|
|
Packit |
1d8052 |
module Main where
|
|
Packit |
1d8052 |
|
|
Packit |
1d8052 |
--------------------------------------------------------------------------
|
|
Packit |
1d8052 |
-- imports
|
|
Packit |
1d8052 |
|
|
Packit |
1d8052 |
import Test.QuickCheck
|
|
Packit |
1d8052 |
|
|
Packit |
1d8052 |
import Control.Monad
|
|
Packit |
1d8052 |
( liftM
|
|
Packit |
1d8052 |
, liftM2
|
|
Packit |
1d8052 |
)
|
|
Packit |
1d8052 |
|
|
Packit |
1d8052 |
import Data.Char
|
|
Packit |
1d8052 |
( toUpper
|
|
Packit |
1d8052 |
)
|
|
Packit |
1d8052 |
|
|
Packit |
1d8052 |
import Data.Set (Set)
|
|
Packit |
1d8052 |
import qualified Data.Set as Set
|
|
Packit |
1d8052 |
|
|
Packit |
1d8052 |
--------------------------------------------------------------------------
|
|
Packit |
1d8052 |
-- types for lambda expressions
|
|
Packit |
1d8052 |
|
|
Packit |
1d8052 |
-- variables
|
|
Packit |
1d8052 |
|
|
Packit |
1d8052 |
newtype Var = MkVar String
|
|
Packit |
1d8052 |
deriving ( Eq, Ord )
|
|
Packit |
1d8052 |
|
|
Packit |
1d8052 |
instance Show Var where
|
|
Packit |
1d8052 |
show (MkVar s) = s
|
|
Packit |
1d8052 |
|
|
Packit |
1d8052 |
varList :: [Var]
|
|
Packit |
1d8052 |
varList = [ MkVar s
|
|
Packit |
1d8052 |
| let vs = [ c:v | v <- "" : vs, c <- ['a'..'z'] ]
|
|
Packit |
1d8052 |
, s <- vs
|
|
Packit |
1d8052 |
]
|
|
Packit |
1d8052 |
|
|
Packit |
1d8052 |
instance Arbitrary Var where
|
|
Packit |
1d8052 |
arbitrary = growingElements [ MkVar [c] | c <- ['a'..'z'] ]
|
|
Packit |
1d8052 |
|
|
Packit |
1d8052 |
-- constants
|
|
Packit |
1d8052 |
|
|
Packit |
1d8052 |
newtype Con = MkCon String
|
|
Packit |
1d8052 |
deriving ( Eq, Ord )
|
|
Packit |
1d8052 |
|
|
Packit |
1d8052 |
instance Show Con where
|
|
Packit |
1d8052 |
show (MkCon s) = s
|
|
Packit |
1d8052 |
|
|
Packit |
1d8052 |
instance Arbitrary Con where
|
|
Packit |
1d8052 |
arbitrary = growingElements [ MkCon [c] | c <- ['A'..'Z'] ]
|
|
Packit |
1d8052 |
|
|
Packit |
1d8052 |
-- expressions
|
|
Packit |
1d8052 |
|
|
Packit |
1d8052 |
data Exp
|
|
Packit |
1d8052 |
= Lam Var Exp
|
|
Packit |
1d8052 |
| App Exp Exp
|
|
Packit |
1d8052 |
| Var Var
|
|
Packit |
1d8052 |
| Con Con
|
|
Packit |
1d8052 |
deriving ( Eq, Ord )
|
|
Packit |
1d8052 |
|
|
Packit |
1d8052 |
instance Show Exp where
|
|
Packit |
1d8052 |
showsPrec n (Lam x t) = showParen (n>0) (showString "\\" . shows x . showString "." . shows t)
|
|
Packit |
1d8052 |
showsPrec n (App s t) = showParen (n>1) (showsPrec 1 s . showString " " . showsPrec 2 t)
|
|
Packit |
1d8052 |
showsPrec _ (Var x) = shows x
|
|
Packit |
1d8052 |
showsPrec _ (Con c) = shows c
|
|
Packit |
1d8052 |
|
|
Packit |
1d8052 |
instance Arbitrary Exp where
|
|
Packit |
1d8052 |
arbitrary = sized arbExp
|
|
Packit |
1d8052 |
where
|
|
Packit |
1d8052 |
arbExp n =
|
|
Packit |
1d8052 |
frequency $
|
|
Packit |
1d8052 |
[ (2, liftM Var arbitrary)
|
|
Packit |
1d8052 |
, (1, liftM Con arbitrary)
|
|
Packit |
1d8052 |
] ++
|
|
Packit |
1d8052 |
concat
|
|
Packit |
1d8052 |
[ [ (5, liftM2 Lam arbitrary arbExp1)
|
|
Packit |
1d8052 |
, (5, liftM2 App arbExp2 arbExp2)
|
|
Packit |
1d8052 |
]
|
|
Packit |
1d8052 |
| n > 0
|
|
Packit |
1d8052 |
]
|
|
Packit |
1d8052 |
where
|
|
Packit |
1d8052 |
arbExp1 = arbExp (n-1)
|
|
Packit |
1d8052 |
arbExp2 = arbExp (n `div` 2)
|
|
Packit |
1d8052 |
|
|
Packit |
1d8052 |
shrink (Lam x a) = [ a ]
|
|
Packit |
1d8052 |
++ [ Lam x a' | a' <- shrink a ]
|
|
Packit |
1d8052 |
shrink (App a b) = [ a, b ]
|
|
Packit |
1d8052 |
++ [ ab
|
|
Packit |
1d8052 |
| Lam x a' <- [a]
|
|
Packit |
1d8052 |
, let ab = subst x b a'
|
|
Packit |
1d8052 |
, length (show ab) < length (show (App a b))
|
|
Packit |
1d8052 |
]
|
|
Packit |
1d8052 |
++ [ App a' b | a' <- shrink a ]
|
|
Packit |
1d8052 |
++ [ App a b' | b' <- shrink b ]
|
|
Packit |
1d8052 |
shrink (Var x) = [Con (MkCon (map toUpper (show x)))]
|
|
Packit |
1d8052 |
shrink _ = []
|
|
Packit |
1d8052 |
|
|
Packit |
1d8052 |
--------------------------------------------------------------------------
|
|
Packit |
1d8052 |
-- functions for lambda expressions
|
|
Packit |
1d8052 |
|
|
Packit |
1d8052 |
free :: Exp -> Set Var
|
|
Packit |
1d8052 |
free (Lam x a) = Set.delete x (free a)
|
|
Packit |
1d8052 |
free (App a b) = free a `Set.union` free b
|
|
Packit |
1d8052 |
free (Var x) = Set.singleton x
|
|
Packit |
1d8052 |
free (Con _) = Set.empty
|
|
Packit |
1d8052 |
|
|
Packit |
1d8052 |
subst :: Var -> Exp -> Exp -> Exp
|
|
Packit |
1d8052 |
subst x c (Var y) | x == y = c
|
|
Packit |
1d8052 |
subst x b (Lam y a) | x /= y = Lam y (subst x b a)
|
|
Packit |
1d8052 |
subst x c (App a b) = App (subst x c a) (subst x c b)
|
|
Packit |
1d8052 |
subst x c a = a
|
|
Packit |
1d8052 |
|
|
Packit |
1d8052 |
fresh :: Var -> Set Var -> Var
|
|
Packit |
1d8052 |
fresh x ys = head (filter (`Set.notMember` ys) (x:varList))
|
|
Packit |
1d8052 |
|
|
Packit |
1d8052 |
rename :: Var -> Var -> Exp -> Exp
|
|
Packit |
1d8052 |
rename x y a | x == y = a
|
|
Packit |
1d8052 |
| otherwise = subst x (Var y) a
|
|
Packit |
1d8052 |
|
|
Packit |
1d8052 |
-- different bugs:
|
|
Packit |
1d8052 |
--subst x b (Lam y a) | x /= y = Lam y (subst x b a) -- bug 1
|
|
Packit |
1d8052 |
--subst x b (Lam y a) | x /= y = Lam y' (subst x b (rename y y' a)) where y':_ = (y:varList) \\ free b -- bug 2
|
|
Packit |
1d8052 |
--subst x b (Lam y a) | x /= y = Lam y' (subst x b (rename y y' a)) where y' = (y:varList) \\ (x:free b) -- bug 3
|
|
Packit |
1d8052 |
--subst x b (Lam y a) | x /= y = Lam y' (subst x b (rename y y' a)) where y' = fresh y (x:free b) -- bug 4
|
|
Packit |
1d8052 |
--subst x c (Lam y a) | x /= y = Lam y' (subst x c (rename y y' a)) where y' = fresh y (x `insert` delete y (free a) `union` free c)
|
|
Packit |
1d8052 |
|
|
Packit |
1d8052 |
--------------------------------------------------------------------------
|
|
Packit |
1d8052 |
-- properties for substitutions
|
|
Packit |
1d8052 |
|
|
Packit |
1d8052 |
showResult :: (Show a, Testable prop) => a -> (a -> prop) -> Property
|
|
Packit |
1d8052 |
showResult x f =
|
|
Packit |
1d8052 |
whenFail (putStrLn ("Result: " ++ show x)) $
|
|
Packit |
1d8052 |
f x
|
|
Packit |
1d8052 |
|
|
Packit |
1d8052 |
prop_SubstFreeNoVarCapture a x b =
|
|
Packit |
1d8052 |
showResult (subst x b a) $ \subst_x_b_a ->
|
|
Packit |
1d8052 |
x `Set.member` free_a ==>
|
|
Packit |
1d8052 |
free subst_x_b_a == (Set.delete x free_a `Set.union` free b)
|
|
Packit |
1d8052 |
where
|
|
Packit |
1d8052 |
free_a = free a
|
|
Packit |
1d8052 |
|
|
Packit |
1d8052 |
prop_SubstNotFreeSame a x b =
|
|
Packit |
1d8052 |
showResult (subst x b a) $ \subst_x_b_a ->
|
|
Packit |
1d8052 |
x `Set.notMember` free a ==>
|
|
Packit |
1d8052 |
subst_x_b_a == a
|
|
Packit |
1d8052 |
|
|
Packit |
1d8052 |
prop_SubstNotFreeSameVars a x b =
|
|
Packit |
1d8052 |
showResult (subst x b a) $ \subst_x_b_a ->
|
|
Packit |
1d8052 |
x `Set.notMember` free a ==>
|
|
Packit |
1d8052 |
free subst_x_b_a == free a
|
|
Packit |
1d8052 |
|
|
Packit |
1d8052 |
main1 =
|
|
Packit |
1d8052 |
do quickCheck prop_SubstFreeNoVarCapture
|
|
Packit |
1d8052 |
quickCheck prop_SubstNotFreeSame
|
|
Packit |
1d8052 |
quickCheck prop_SubstNotFreeSameVars
|
|
Packit |
1d8052 |
|
|
Packit |
1d8052 |
--expectFailure $
|
|
Packit |
1d8052 |
|
|
Packit |
1d8052 |
|
|
Packit |
1d8052 |
|
|
Packit |
1d8052 |
|
|
Packit |
1d8052 |
|
|
Packit |
1d8052 |
|
|
Packit |
1d8052 |
|
|
Packit |
1d8052 |
|
|
Packit |
1d8052 |
--------------------------------------------------------------------------
|
|
Packit |
1d8052 |
-- eval
|
|
Packit |
1d8052 |
|
|
Packit |
1d8052 |
eval :: Exp -> Exp
|
|
Packit |
1d8052 |
eval (Var x) = error "eval: free variable"
|
|
Packit |
1d8052 |
eval (App a b) =
|
|
Packit |
1d8052 |
case eval a of
|
|
Packit |
1d8052 |
Lam x a' -> eval (subst x b a')
|
|
Packit |
1d8052 |
a' -> App a' (eval b)
|
|
Packit |
1d8052 |
eval a = a
|
|
Packit |
1d8052 |
|
|
Packit |
1d8052 |
--------------------------------------------------------------------------
|
|
Packit |
1d8052 |
-- closed lambda expressions
|
|
Packit |
1d8052 |
|
|
Packit |
1d8052 |
newtype ClosedExp = Closed Exp deriving ( Show )
|
|
Packit |
1d8052 |
|
|
Packit |
1d8052 |
instance Arbitrary ClosedExp where
|
|
Packit |
1d8052 |
arbitrary = Closed `fmap` sized (arbExp [])
|
|
Packit |
1d8052 |
where
|
|
Packit |
1d8052 |
arbExp xs n =
|
|
Packit |
1d8052 |
frequency $
|
|
Packit |
1d8052 |
[ (8, liftM Var (elements xs))
|
|
Packit |
1d8052 |
| not (null xs)
|
|
Packit |
1d8052 |
] ++
|
|
Packit |
1d8052 |
[ (2, liftM Con arbitrary)
|
|
Packit |
1d8052 |
] ++
|
|
Packit |
1d8052 |
[ (20, do x <- arbitrary
|
|
Packit |
1d8052 |
t <- arbExp (x:xs) n'
|
|
Packit |
1d8052 |
return (Lam x t))
|
|
Packit |
1d8052 |
| n > 0 || null xs
|
|
Packit |
1d8052 |
] ++
|
|
Packit |
1d8052 |
[ (20, liftM2 App (arbExp xs n2) (arbExp xs n2))
|
|
Packit |
1d8052 |
| n > 0
|
|
Packit |
1d8052 |
]
|
|
Packit |
1d8052 |
where
|
|
Packit |
1d8052 |
n' = n-1
|
|
Packit |
1d8052 |
n2 = n `div` 2
|
|
Packit |
1d8052 |
|
|
Packit |
1d8052 |
shrink (Closed a) =
|
|
Packit |
1d8052 |
[ Closed a' | a' <- shrink a, Set.null (free a') ]
|
|
Packit |
1d8052 |
|
|
Packit |
1d8052 |
--------------------------------------------------------------------------
|
|
Packit |
1d8052 |
-- properties for closed lambda expressions
|
|
Packit |
1d8052 |
|
|
Packit |
1d8052 |
isValue :: Exp -> Bool
|
|
Packit |
1d8052 |
isValue (Var _) = False
|
|
Packit |
1d8052 |
isValue (App (Lam _ _) _) = False
|
|
Packit |
1d8052 |
isValue (App a b) = isValue a && isValue b
|
|
Packit |
1d8052 |
isValue _ = True
|
|
Packit |
1d8052 |
|
|
Packit |
1d8052 |
prop_ClosedExpIsClosed (Closed a) =
|
|
Packit |
1d8052 |
Set.null (free a)
|
|
Packit |
1d8052 |
|
|
Packit |
1d8052 |
prop_EvalProducesValue (Closed a) =
|
|
Packit |
1d8052 |
within 1000 $
|
|
Packit |
1d8052 |
isValue (eval a)
|
|
Packit |
1d8052 |
|
|
Packit |
1d8052 |
main2 =
|
|
Packit |
1d8052 |
do quickCheck prop_ClosedExpIsClosed
|
|
Packit |
1d8052 |
quickCheck prop_EvalProducesValue
|
|
Packit |
1d8052 |
|
|
Packit |
1d8052 |
-- expectFailure $
|
|
Packit |
1d8052 |
|
|
Packit |
1d8052 |
--------------------------------------------------------------------------
|
|
Packit |
1d8052 |
-- main
|
|
Packit |
1d8052 |
|
|
Packit |
1d8052 |
main =
|
|
Packit |
1d8052 |
do main1
|
|
Packit |
1d8052 |
main2
|
|
Packit |
1d8052 |
|
|
Packit |
1d8052 |
--------------------------------------------------------------------------
|
|
Packit |
1d8052 |
-- the end.
|
|
Packit |
1d8052 |
|
|
Packit |
1d8052 |
{-
|
|
Packit |
1d8052 |
instance Arbitrary Exp where
|
|
Packit |
1d8052 |
arbitrary = sized (arbExp [])
|
|
Packit |
1d8052 |
where
|
|
Packit |
1d8052 |
|
|
Packit |
1d8052 |
arbitrary = repair [] `fmap` sized arbExp
|
|
Packit |
1d8052 |
where
|
|
Packit |
1d8052 |
arbExp n =
|
|
Packit |
1d8052 |
frequency $
|
|
Packit |
1d8052 |
[ (1, liftM Var arbitrary)
|
|
Packit |
1d8052 |
] ++ concat
|
|
Packit |
1d8052 |
[ [ (3, liftM2 Lam arbitrary (arbExp n'))
|
|
Packit |
1d8052 |
, (4, liftM2 App (arbExp n2) (arbExp n2))
|
|
Packit |
1d8052 |
]
|
|
Packit |
1d8052 |
| n > 0
|
|
Packit |
1d8052 |
]
|
|
Packit |
1d8052 |
where
|
|
Packit |
1d8052 |
n' = n-1
|
|
Packit |
1d8052 |
n2 = n `div` 2
|
|
Packit |
1d8052 |
|
|
Packit |
1d8052 |
repair xs (Var x)
|
|
Packit |
1d8052 |
| x `elem` xs = Var x
|
|
Packit |
1d8052 |
| null xs = Lam x (Var x)
|
|
Packit |
1d8052 |
| otherwise = Var (xs !! (ord (last (show x)) `mod` length xs))
|
|
Packit |
1d8052 |
repair xs (App a b) = App (repair xs a) (repair xs b)
|
|
Packit |
1d8052 |
repair xs (Lam x a) = Lam x (repair (x:xs) a)
|
|
Packit |
1d8052 |
|
|
Packit |
1d8052 |
-- lots of clever shrinking added
|
|
Packit |
1d8052 |
shrinkRec (Lam x a) = [ a | x `notElem` free a ]
|
|
Packit |
1d8052 |
shrinkRec (App a b) = [ a, b ]
|
|
Packit |
1d8052 |
++ [ red
|
|
Packit |
1d8052 |
| Lam x a' <- [a]
|
|
Packit |
1d8052 |
, let red = subst x b a'
|
|
Packit |
1d8052 |
, length (show red) < length (show (App a b))
|
|
Packit |
1d8052 |
]
|
|
Packit |
1d8052 |
shrinkRec (Var x) = [Con (MkCon (map toUpper (show x)))]
|
|
Packit |
1d8052 |
shrinkRec _ = []
|
|
Packit |
1d8052 |
|
|
Packit |
1d8052 |
-- types
|
|
Packit |
1d8052 |
|
|
Packit |
1d8052 |
data Type
|
|
Packit |
1d8052 |
= Base Con
|
|
Packit |
1d8052 |
| Type :-> Type
|
|
Packit |
1d8052 |
deriving ( Eq, Show )
|
|
Packit |
1d8052 |
|
|
Packit |
1d8052 |
instance Arbitrary Type where
|
|
Packit |
1d8052 |
arbitrary = sized arbType
|
|
Packit |
1d8052 |
where
|
|
Packit |
1d8052 |
arbType n =
|
|
Packit |
1d8052 |
frequency $
|
|
Packit |
1d8052 |
[ (1, liftM Base arbitrary)
|
|
Packit |
1d8052 |
] ++
|
|
Packit |
1d8052 |
[ (4, liftM2 (:->) arbType2 arbType2)
|
|
Packit |
1d8052 |
| n > 0
|
|
Packit |
1d8052 |
]
|
|
Packit |
1d8052 |
where
|
|
Packit |
1d8052 |
arbType2 = arbType (n `div` 2)
|
|
Packit |
1d8052 |
|
|
Packit |
1d8052 |
newtype WellTypedExp = WellTyped Exp
|
|
Packit |
1d8052 |
deriving ( Eq, Show )
|
|
Packit |
1d8052 |
|
|
Packit |
1d8052 |
arbExpWithType n env t =
|
|
Packit |
1d8052 |
frequency $
|
|
Packit |
1d8052 |
[ (2, liftM Var (elements xs))
|
|
Packit |
1d8052 |
| let xs = [ x | (x,t') <- env, t == t' ]
|
|
Packit |
1d8052 |
, not (null xs)
|
|
Packit |
1d8052 |
] ++
|
|
Packit |
1d8052 |
[ (1, return (Con b))
|
|
Packit |
1d8052 |
| Base b <- [t]
|
|
Packit |
1d8052 |
] ++
|
|
Packit |
1d8052 |
[ (if n > 0 then 5 else 1
|
|
Packit |
1d8052 |
, do x <- arbitrary
|
|
Packit |
1d8052 |
b <- arbExpWithType n1 ((x,ta):[ xt | xt <- env, fst xt /= x ]) tb
|
|
Packit |
1d8052 |
return (Lam x b))
|
|
Packit |
1d8052 |
| ta :-> tb <- [t]
|
|
Packit |
1d8052 |
] ++
|
|
Packit |
1d8052 |
[ (5, do tb <- arbitrary
|
|
Packit |
1d8052 |
a <- arbExpWithType n2 env (tb :-> t)
|
|
Packit |
1d8052 |
b <- arbExpWithType n2 env tb
|
|
Packit |
1d8052 |
return (App a b))
|
|
Packit |
1d8052 |
| n > 0
|
|
Packit |
1d8052 |
]
|
|
Packit |
1d8052 |
where
|
|
Packit |
1d8052 |
n1 = n-1
|
|
Packit |
1d8052 |
n2 = n `div` 2
|
|
Packit |
1d8052 |
|
|
Packit |
1d8052 |
instance Arbitrary WellTypedExp where
|
|
Packit |
1d8052 |
arbitrary =
|
|
Packit |
1d8052 |
do t <- arbitrary
|
|
Packit |
1d8052 |
e <- sized (\n -> arbExpWithType n [] t)
|
|
Packit |
1d8052 |
return (WellTyped e)
|
|
Packit |
1d8052 |
|
|
Packit |
1d8052 |
shrink _ = []
|
|
Packit |
1d8052 |
|
|
Packit |
1d8052 |
newtype OpenExp = Open Exp
|
|
Packit |
1d8052 |
deriving ( Eq, Show )
|
|
Packit |
1d8052 |
|
|
Packit |
1d8052 |
instance Arbitrary OpenExp where
|
|
Packit |
1d8052 |
arbitrary = Open `fmap` sized arbExp
|
|
Packit |
1d8052 |
where
|
|
Packit |
1d8052 |
arbExp n =
|
|
Packit |
1d8052 |
frequency $
|
|
Packit |
1d8052 |
[ (2, liftM Var arbitrary)
|
|
Packit |
1d8052 |
, (1, liftM Con arbitrary)
|
|
Packit |
1d8052 |
] ++
|
|
Packit |
1d8052 |
concat
|
|
Packit |
1d8052 |
[ [ (5, liftM2 Lam arbitrary arbExp1)
|
|
Packit |
1d8052 |
, (5, liftM2 App arbExp2 arbExp2)
|
|
Packit |
1d8052 |
]
|
|
Packit |
1d8052 |
| n > 0
|
|
Packit |
1d8052 |
]
|
|
Packit |
1d8052 |
where
|
|
Packit |
1d8052 |
arbExp1 = arbExp (n-1)
|
|
Packit |
1d8052 |
arbExp2 = arbExp (n `div` 2)
|
|
Packit |
1d8052 |
|
|
Packit |
1d8052 |
shrink (Open a) = map Open (shrink a)
|
|
Packit |
1d8052 |
|
|
Packit |
1d8052 |
prop_EvalProducesValueWT (WellTyped a) =
|
|
Packit |
1d8052 |
isValue (eval a)
|
|
Packit |
1d8052 |
|
|
Packit |
1d8052 |
-}
|
|
Packit |
1d8052 |
|
|
Packit |
1d8052 |
x = MkVar "x"
|
|
Packit |
1d8052 |
y = MkVar "y"
|
|
Packit |
1d8052 |
|