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