{-# 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"