lazysmallcheck 0.1 → 0.2
raw patch · 39 files changed
+1741/−994 lines, 39 filesdep −randomnew-uploader
Dependencies removed: random
Files
- Test/LazySmallCheck.hs +275/−0
- Test/LazySmallCheck/Generic.hs +143/−0
- benchmarks/Benchmark.hs +0/−35
- benchmarks/Countdown.hs +0/−187
- benchmarks/List.hs +0/−20
- benchmarks/Mux.hs +0/−33
- benchmarks/RegExp.hs +0/−124
- benchmarks/Sad.hs +0/−92
- benchmarks/SumPuz.hs +0/−68
- benchmarks/clean.sh +0/−5
- examples/Catch.hs +112/−0
- examples/Countdown.hs +195/−0
- examples/Huffman.hs +86/−0
- examples/ListSet.hs +34/−0
- examples/Mate.hs +256/−0
- examples/Mux.hs +64/−0
- examples/RedBlack.hs +80/−0
- examples/RegExp.hs +91/−0
- examples/Sad.hs +96/−0
- examples/SumPuz.hs +76/−0
- examples/Turner.hs +59/−0
- examples/test/TestCatch.hs +17/−0
- examples/test/TestCountdown1.hs +5/−0
- examples/test/TestCountdown2.hs +5/−0
- examples/test/TestHuffman1.hs +8/−0
- examples/test/TestHuffman2.hs +8/−0
- examples/test/TestListSet1.hs +5/−0
- examples/test/TestMate.hs +19/−0
- examples/test/TestMux1.hs +5/−0
- examples/test/TestMux2.hs +5/−0
- examples/test/TestMux3.hs +5/−0
- examples/test/TestRedBlack.hs +11/−0
- examples/test/TestRegExp.hs +19/−0
- examples/test/TestSad.hs +5/−0
- examples/test/TestSumPuz.hs +5/−0
- examples/test/TestTurner.hs +11/−0
- lazysmallcheck.cabal +41/−24
- source/LazySmallCheck.hs +0/−262
- source/LazySmallCheck/Generic.hs +0/−144
+ Test/LazySmallCheck.hs view
@@ -0,0 +1,275 @@+-- Lazy SmallCheck (type-class variant, largely a SmallCheck subset)+-- Lindblad, Naylor and Runciman++module Test.LazySmallCheck+ ( Serial(series) -- :: class+ , Series -- :: type Series a = Int -> Cons a+ , Cons -- :: *+ , cons -- :: a -> Series a+ , (><) -- :: Series (a -> b) -> Series a -> Series b+ , (\/) -- :: Series a -> Series a -> Series a+ , drawnFrom -- :: [a] -> Cons a+ , cons0 -- :: a -> Series a+ , cons1 -- :: Serial a => (a -> b) -> Series b+ , cons2 -- :: (Serial a, Serial b) => (a -> b -> c) -> Series c+ , cons3 -- :: ...+ , cons4 -- :: ...+ , cons5 -- :: ...+ , Testable -- :: class+ , depthCheck -- :: Testable a => Int -> a -> IO ()+ , test -- :: Testable a => a -> IO ()+ , (==>) -- :: Bool -> Bool -> Bool+ , Prop -- :: *+ , lift -- :: Bool -> Prop+ , neg -- :: Prop -> Prop+ , (*&*) -- :: Prop -> Prop -> Prop+ , (*|*) -- :: Prop -> Prop -> Prop+ , (*=>*) -- :: Prop -> Prop -> Prop+ )+ where++import Monad+import Control.Exception+import System.Exit++infixr 0 ==>, *=>*+infixr 3 \/, *|*+infixl 4 ><, *&*++type Pos = [Int]++data Term = Var Pos Type | Ctr Int [Term]++data Type = SumOfProd [[Type]]++type Series a = Int -> Cons a++data Cons a = C Type ([[Term] -> a])++class Serial a where+ series :: Series a++-- Series constructors++cons :: a -> Series a+cons a d = C (SumOfProd [[]]) [const a]++(><) :: Series (a -> b) -> Series a -> Series b+(f >< a) d = C (SumOfProd [ta:p | d > 0, p <- ps]) cs+ where+ C (SumOfProd ps) cfs = f d+ C ta cas = a (d-1)+ cs = [\(x:xs) -> cf xs (conv cas x) | d > 0, cf <- cfs]++(\/) :: Series a -> Series a -> Series a+(a \/ b) d = C (SumOfProd (ssa ++ ssb)) (ca ++ cb)+ where+ C (SumOfProd ssa) ca = a d+ C (SumOfProd ssb) cb = b d++conv :: [[Term] -> a] -> Term -> a+conv cs (Var p _) = error ('\0':map toEnum p)+conv cs (Ctr i xs) = (cs !! i) xs++drawnFrom :: [a] -> Cons a+drawnFrom xs = C (SumOfProd (map (const []) xs)) (map const xs)++-- Helpers, a la SmallCheck++cons0 :: a -> Series a+cons0 f = cons f++cons1 :: Serial a => (a -> b) -> Series b+cons1 f = cons f >< series++cons2 :: (Serial a, Serial b) => (a -> b -> c) -> Series c+cons2 f = cons f >< series >< series++cons3 :: (Serial a, Serial b, Serial c) => (a -> b -> c -> d) -> Series d+cons3 f = cons f >< series >< series >< series++cons4 :: (Serial a, Serial b, Serial c, Serial d) =>+ (a -> b -> c -> d -> e) -> Series e+cons4 f = cons f >< series >< series >< series >< series++cons5 :: (Serial a, Serial b, Serial c, Serial d, Serial e) =>+ (a -> b -> c -> d -> e -> f) -> Series f+cons5 f = cons f >< series >< series >< series >< series >< series++-- Standard instances++instance Serial () where+ series = cons0 ()++instance Serial Bool where+ series = cons0 False \/ cons0 True++instance Serial a => Serial (Maybe a) where+ series = cons0 Nothing \/ cons1 Just++instance (Serial a, Serial b) => Serial (Either a b) where+ series = cons1 Left \/ cons1 Right++instance Serial a => Serial [a] where+ series = cons0 [] \/ cons2 (:)++instance (Serial a, Serial b) => Serial (a, b) where+ series = cons2 (,) . (+1)++instance (Serial a, Serial b, Serial c) => Serial (a, b, c) where+ series = cons3 (,,) . (+1)++instance (Serial a, Serial b, Serial c, Serial d) =>+ Serial (a, b, c, d) where+ series = cons4 (,,,) . (+1)++instance (Serial a, Serial b, Serial c, Serial d, Serial e) =>+ Serial (a, b, c, d, e) where+ series = cons5 (,,,,) . (+1)++instance Serial Int where+ series d = drawnFrom [-d..d]++instance Serial Integer where+ series d = drawnFrom (map toInteger [-d..d])++instance Serial Char where+ series d = drawnFrom (take (d+1) ['a'..])++instance Serial Float where+ series d = drawnFrom (floats d)++instance Serial Double where+ series d = drawnFrom (floats d)++floats :: RealFloat a => Int -> [a]+floats d = [ encodeFloat sig exp+ | sig <- map toInteger [-d..d]+ , exp <- [-d..d]+ , odd sig || sig == 0 && exp == 0+ ]++-- Term refinement++refine :: Term -> Pos -> [Term]+refine (Var p (SumOfProd ss)) [] = new p ss+refine (Ctr c xs) p = map (Ctr c) (refineList xs p)++refineList :: [Term] -> Pos -> [[Term]]+refineList xs (i:is) = [ls ++ y:rs | y <- refine x is]+ where (ls, x:rs) = splitAt i xs++new :: Pos -> [[Type]] -> [Term]+new p ps = [ Ctr c (zipWith (\i t -> Var (p++[i]) t) [0..] ts)+ | (c, ts) <- zip [0..] ps ]++-- Find total instantiations of a partial value++total :: Term -> [Term] +total val = tot val+ where+ tot (Ctr c xs) = [Ctr c ys | ys <- mapM tot xs] + tot (Var p (SumOfProd ss)) = [y | x <- new p ss, y <- tot x]++-- Answers++answer :: a -> (a -> IO b) -> (Pos -> IO b) -> IO b+answer a known unknown =+ do res <- try (evaluate a)+ case res of+ Right b -> known b+ Left (ErrorCall ('\0':p)) -> unknown (map fromEnum p)+ Left e -> throw e++-- Refute++refute :: Result -> IO Int+refute r = ref (args r)+ where+ ref xs = eval (apply r xs) known unknown+ where+ known True = return 1+ known False = report+ unknown p = sumMapM ref 1 (refineList xs p)++ report =+ do putStr "Counter example found"+ case [ys | ys <- mapM total xs] of+ [] -> putStrLn ", but too deep to fully instantiate"+ as:_ -> do putStrLn ":"+ mapM_ putStrLn $ zipWith ($) (showArgs r) as+ exitWith ExitSuccess++sumMapM :: (a -> IO Int) -> Int -> [a] -> IO Int+sumMapM f n [] = return n+sumMapM f n (a:as) = seq n (do m <- f a ; sumMapM f (n+m) as)++-- Properties with parallel conjunction (Lindblad TFP'07)++data Prop = Bool Bool | Neg Prop | And Prop Prop | ParAnd Prop Prop++eval :: Prop -> (Bool -> IO a) -> (Pos -> IO a) -> IO a+eval p k u = answer p (\p -> eval' p k u) u++eval' (Bool b) k u = answer b k u+eval' (Neg p) k u = eval p (k . not) u+eval' (And p q) k u = eval p (\b -> if b then eval q k u else k b) u+eval' (ParAnd p q) k u = eval p (\b -> if b then eval q k u else k b) unknown+ where+ unknown pos = eval q (\b -> if b then u pos else k b) (\_ -> u pos)++lift :: Bool -> Prop+lift b = Bool b++neg :: Prop -> Prop+neg p = Neg p++(*&*), (*|*), (*=>*) :: Prop -> Prop -> Prop+p *&* q = ParAnd p q+p *|* q = neg (neg p *&* neg q)+p *=>* q = neg (p *&* neg q)++-- Boolean implication++(==>) :: Bool -> Bool -> Bool+False ==> _ = True+True ==> x = x++-- Testable++data Result =+ Result { args :: [Term]+ , showArgs :: [Term -> String]+ , apply :: [Term] -> Prop+ }++data Property = P (Int -> Int -> Result)++run :: Testable a => ([Term] -> a) -> Int -> Int -> Result+run a = f where P f = property a++class Testable a where+ property :: ([Term] -> a) -> Property++instance Testable Bool where+ property apply = P $ \n d -> Result [] [] (Bool . apply . reverse)++instance Testable Prop where+ property apply = P $ \n d -> Result [] [] (apply . reverse)++instance (Show a, Serial a, Testable b) => Testable (a -> b) where+ property f = P $ \n d ->+ let C t c = series d+ c' = conv c+ r = run (\(x:xs) -> f xs (c' x)) (n+1) d+ in r { args = Var [n] t : args r, showArgs = (show . c') : showArgs r }++-- Top-level interface++depthCheck :: Testable a => Int -> a -> IO ()+depthCheck d p =+ do n <- refute $ run (const p) 0 d+ putStrLn $ "OK, required " ++ show n ++ " tests at depth " ++ show d++test :: Testable a => a -> IO ()+test p = mapM_ (`depthCheck` p) [0..]
+ Test/LazySmallCheck/Generic.hs view
@@ -0,0 +1,143 @@+{-# OPTIONS -fglasgow-exts #-} + +module Test.LazySmallCheck.Generic + ( depthCheck -- :: (Data a, Show a) => Int -> (a -> Bool) -> IO [a] + , (==>) -- :: Bool -> Bool -> Bool + ) where + +import Data.Maybe +import Data.Generics +import Control.Exception +import Control.Monad +import System.Exit + +uniquePrefix = "UP:" + +lenUniquePrefix = length uniquePrefix + +type Position = String + +initPData :: a +initPData = error uniquePrefix + +data HLP a = HLP Int (Either a [a]) + +refinePData :: Data a => String -> Int -> Position -> a -> [a] +refinePData s d = r + where + depleft = d - (length s - lenUniquePrefix) + r :: Data a => Position -> a -> [a] + r [] x = + let dt = dataTypeOf x + in case dataTypeRep dt of + AlgRep cons -> + let cons = dataTypeConstrs dt + z x = (0, x) + k (i, g) = (i + 1, g (error $ s ++ [toEnum i])) + xs' = map (gunfold k z) cons + in if depleft > 0 + then map snd xs' + else mapMaybe (\(ncon, x') -> + if ncon == 0 + then Just x' + else Nothing) xs' + IntRep -> mkPrim dt (mkIntConstr dt . toInteger) + [-depleft .. depleft] + StringRep -> mkPrim dt (mkStringConstr dt . (:[])) + (take (depleft+1) ['a' .. 'z']) + _ -> error $ "LazySmallCheck.Generic: Can't generate type " + ++ dataTypeName dt + r (c:ps) x = + let p = fromEnum c + z y = HLP 0 (Left y) + k (HLP i (Left xs)) y | i == p = HLP (i + 1) (Right $ map xs (r ps y)) + k (HLP i (Left xs)) y = HLP (i + 1) (Left $ xs y) + k (HLP i (Right xss)) y = HLP (i + 1) (Right $ map (\xs -> xs y) xss) + HLP _ (Right x') = gfoldl k z x + in x' + +mkPrim dt mk vs = map (\i -> fromJust $ gunfold undefined Just $ mk i) vs + +-- + +mapVars :: Data a => (forall b . Data b => b -> IO b) -> a -> IO a +mapVars f = gmapM (\x -> Control.Exception.catch + (mapVars f x) + (\exc -> case exc of + ErrorCall s | take (length uniquePrefix) s == uniquePrefix -> + f x + _ -> throw exc + ) + ) + +-- Taken from Ralf Laemmel, SYB website +-- Generate all terms of a given depth +enumerate :: Data a => Int -> [a] +enumerate 0 = [] +enumerate d = result + where + -- Getting hold of the result (type) + result = concat (map recurse cons') + + -- Find all terms headed by a specific Constr + recurse :: Data a => Constr -> [a] + recurse con = gmapM (\_ -> enumerate (d-1)) + (fromConstr con) + + -- We could also deal with primitive types easily. + -- Then we had to use cons' instead of cons. + -- + cons' :: [Constr] + cons' = case dataTypeRep ty of + AlgRep cons -> cons + IntRep -> map (mkIntConstr ty . toInteger) [-d .. d] + StringRep -> map (mkStringConstr ty . (:[])) (take d ['a'..'z']) + --FloatRep -> + where + ty = dataTypeOf (head result) + +smallValue :: Data a => a +smallValue = f 1 + where + f d = case enumerate d of + [] -> f (d + 1) + (x:_) -> x + +smallInstance :: Data a => a -> IO a +smallInstance = mapVars (\_ -> return smallValue) + +-- + +refute :: (Show a, Data a) => Int -> (a -> Bool) -> IO Int +refute d p = r initPData + where + r x = do res <- try (evaluate (p x)) + case res of + Right True -> return 1 + Right False -> stop x "Counter example found:" + Left (ErrorCall s) + | take (lenUniquePrefix) s == uniquePrefix -> + let pos = drop lenUniquePrefix s + in do ns <- mapM r (refinePData s d pos x) + return (1 + sum ns) + Left e -> stop x "Property crashed on input:" + + stop x s = do putStrLn s + x' <- smallInstance x + putStrLn (show x') + exitWith ExitSuccess + +-- + +depthCheck :: (Show a, Data a) => Int -> (a -> Bool) -> IO () +depthCheck d f = do count <- refute d f + putStrLn $ "Completed " ++ show count + ++ " tests without finding a counter example." + +-- + +infixr 0 ==> + +(==>) :: Bool -> Bool -> Bool +False ==> a = True +True ==> a = a
− benchmarks/Benchmark.hs
@@ -1,35 +0,0 @@-import System-import Data.List--main :: IO ()-main = do args <- getArgs- case args of- [checker, file] -> benchmark checker file- _ -> error usage--usage = "Usage: runhugs Benchmark.hs "- ++ "[SmallCheck|LazySmallCheck|LazySmallCheck.Generic] FILE"--benchmark checker file =- do extra <-- case checker of- "SmallCheck" -> return ""- "LazySmallCheck" -> return ""- "LazySmallCheck.Generic" -> return "import Data.Generics\n"- _ -> error usage- if '.' `elem` file then error "Filename should not contain '.'"- else return ()- contents <- readFile (file ++ ".hs")- let props = nub $ filter ("prop_" `isPrefixOf`) (words contents)- writeFile (file ++ "2.hs") $ extra- ++ "import System\n"- ++ "import " ++ checker ++ "\n\n"- ++ contents ++ "\n\n"- ++ "main = do { [p, d] <- getArgs"- ++ " ; case p of { "- ++ concatMap propAlt props- ++ "_ -> error \"Unknown property\"}}"- system $ "ghc -fglasgow-exts -O2 --make " ++ file ++ "2.hs -o " ++ file- return ()--propAlt p = "\"" ++ p ++ "\" -> " ++ "depthCheck (read d) " ++ p ++ ";"
− benchmarks/Countdown.hs
@@ -1,187 +0,0 @@------------------------------------------------------------------------------------ The Countdown Problem------ Graham Hutton--- University of Nottingham------ November 2001------------------------------------------------------------------------------------------------------------------------------------------------------------------- Formally specifying the problem--------------------------------------------------------------------------------data Op = Add | Sub | Mul | Div- deriving Eq--valid :: Op -> Int -> Int -> Bool-valid Add _ _ = True-valid Sub x y = x > y-valid Mul _ _ = True-valid Div x y = x `mod` y == 0- -apply :: Op -> Int -> Int -> Int-apply Add x y = x + y-apply Sub x y = x - y-apply Mul x y = x * y-apply Div x y = x `div` y--data Expr = Val Int | App Op Expr Expr- deriving Eq--values :: Expr -> [Int]-values (Val n) = [n]-values (App _ l r) = values l ++ values r--eval :: Expr -> [Int]-eval (Val n) = [n | n > 0]-eval (App o l r) = [apply o x y | x <- eval l, y <- eval r, valid o x y]--subbags :: [a] -> [[a]]-subbags xs = [zs | ys <- subs xs, zs <- perms ys]--subs :: [a] -> [[a]]-subs [] = [[]]-subs (x:xs) = ys ++ map (x:) ys- where- ys = subs xs--perms :: [a] -> [[a]]-perms [] = [[]]-perms (x:xs) = concat (map (interleave x) (perms xs))--interleave :: a -> [a] -> [[a]]-interleave x [] = [[x]]-interleave x (y:ys) = (x:y:ys) : map (y:) (interleave x ys)--solution :: Expr -> [Int] -> Int -> Bool-solution e ns n = elem (values e) (subbags ns) && eval e == [n]---------------------------------------------------------------------------------- Brute force implementation--------------------------------------------------------------------------------split :: [a] -> [([a],[a])]-split [] = [([],[])]-split (x:xs) = ([],x:xs) : [(x:ls,rs) | (ls,rs) <- split xs]--nesplit :: [a] -> [([a],[a])]-nesplit = filter ne . split--ne :: ([a],[b]) -> Bool-ne (xs,ys) = not (null xs || null ys)--exprs :: [Int] -> [Expr]-exprs [] = []-exprs [n] = [Val n]-exprs ns = [e | (ls,rs) <- nesplit ns- , l <- exprs ls- , r <- exprs rs- , e <- combine l r]--combine :: Expr -> Expr -> [Expr]-combine l r = [App o l r | o <- ops]- -ops :: [Op]-ops = [Add,Sub,Mul,Div]--solutions :: [Int] -> Int -> [Expr]-solutions ns n = [e | ns' <- subbags ns, e <- exprs ns', eval e == [n]]---------------------------------------------------------------------------------- Fusing generation and evaluation--------------------------------------------------------------------------------type Result = (Expr,Int)--results :: [Int] -> [Result]-results [] = []-results [n] = [(Val n,n) | n > 0]-results ns = [res | (ls,rs) <- nesplit ns- , lx <- results ls- , ry <- results rs- , res <- combine' lx ry]--combine' :: Result -> Result -> [Result]-combine' (l,x) (r,y) = [(App o l r, apply o x y) | o <- ops, valid o x y]--solutions' :: [Int] -> Int -> [Expr]-solutions' ns n = [e | ns' <- subbags ns, (e,m) <- results ns', m == n]---------------------------------------------------------------------------------- Exploiting arithmetic properties--------------------------------------------------------------------------------valid' :: Op -> Int -> Int -> Bool-valid' Add x y = x <= y-valid' Sub x y = x > y-valid' Mul x y = x /= 1 && y /= 1 && x <= y-valid' Div x y = y /= 1 && x `mod` y == 0--eval' :: Expr -> [Int]-eval' (Val n) = [n | n > 0]-eval' (App o l r) = [apply o x y | x <- eval' l, y <- eval' r, valid' o x y]--solution' :: Expr -> [Int] -> Int -> Bool-solution' e ns n = elem (values e) (subbags ns) && eval' e == [n]--results' :: [Int] -> [Result]-results' [] = []-results' [n] = [(Val n,n) | n > 0]-results' ns = [res | (ls,rs) <- nesplit ns- , lx <- results' ls- , ry <- results' rs- , res <- combine'' lx ry]--combine'' :: Result -> Result -> [Result]-combine'' (l,x) (r,y) = [(App o l r, apply o x y) | o <- ops, valid' o x y]--solutions'' :: [Int] -> Int -> [Expr]-solutions'' ns n = [e | ns' <- subbags ns, (e,m) <- results' ns', m == n]---------------------------------------------------------------------------------- Interactive version for testing--------------------------------------------------------------------------------instance Show Op where- show Add = "+"- show Sub = "-"- show Mul = "*"- show Div = "/"--instance Show Expr where- show (Val n) = show n- show (App o l r) = bracket l ++ show o ++ bracket r- where- bracket (Val n) = show n- bracket e = "(" ++ show e ++ ")"--display :: [Expr] -> IO ()-display [] = putStr "\nThere are no solutions.\n\n"-display (e:es) = do putStr "\nOne possible solution is "- putStr (show e)- putStr ".\n\nPress return to continue searching..."- getLine- putStr "\n"- if null es then- putStr "There are no more solutions.\n\n"- else- do sequence [print e | e <- es]- putStr "\nThere were "- putStr (show (length (e:es)))- putStr " solutions in total.\n\n"--prop_lemma1 :: ([Int], [Int], [Int]) -> Bool-prop_lemma1 (xs, ys, zs) = ((xs,ys) `elem` split zs) == (xs ++ ys == zs)--prop_lemma3 :: ([Int], [Int], [Int]) -> Bool-prop_lemma3 (xs, ys, zs) = ((xs, ys) `elem` nesplit zs)- == (xs ++ ys == zs && ne (xs, ys))--prop_lemma4 :: ([Int], [Int], [Int]) -> Bool-prop_lemma4 (xs, ys, zs) = ((xs, ys) `elem` nesplit zs) ==>- (length xs < length zs && length ys < length zs)--prop_solutions (ns, m) = solutions ns m == solutions' ns m
− benchmarks/List.hs
@@ -1,20 +0,0 @@-ord [] = True-ord [x] = True-ord (x:y:ys) = x <= y && ord (y:ys)--insert x [] = [x]-insert x (y:ys)- | x <= y = x:y:ys- | otherwise = y:insert x ys--merge [] ys = ys-merge xs [] = xs-merge (x:xs) (y:ys)- | x <= y = x : merge xs (y:ys)- | otherwise = y : merge (x:xs) ys--prop_ordInsert :: (Char, [Char]) -> Bool-prop_ordInsert (x, xs) = ord xs ==> ord (insert x xs)--prop_ordMerge :: ([Char], [Char]) -> Bool-prop_ordMerge (xs, ys) = ord xs && ord ys ==> ord (merge xs ys)
− benchmarks/Mux.hs
@@ -1,33 +0,0 @@-import Data.List---- Binary multiplexor--tree :: (a -> a -> a) -> [a] -> a-tree f [x] = x-tree f (x:y:ys) = tree f (ys ++ [f x y])--unaryMux :: [Bool] -> [[Bool]] -> [Bool]-unaryMux sel xs = map (tree (||))- $ transpose- $ zipWith (\s x -> map (s &&) x) sel xs--decode [] = [True]-decode [x] = [not x,x]-decode (x:xs) = concatMap (\y -> [not x && y,x && y]) rest- where- rest = decode xs--binaryMux :: [Bool] -> [[Bool]] -> [Bool]-binaryMux sel xs = unaryMux (decode sel) xs--num :: [Bool] -> Int-num [] = 0-num (a:as) = (if a then 1 else 0) + 2 * num as---- Property--prop_binMux :: ([Bool], [[Bool]]) -> Bool-prop_binMux (sel, xs) =- ((length xs == 2 ^ length sel)- && all ((== length (head xs)) . length) xs)- ==> (binaryMux sel xs == xs !! num sel)
− benchmarks/RegExp.hs
@@ -1,124 +0,0 @@-(<==>) :: Bool -> Bool -> Bool -a <==> b = (a ==> b) && (b ==> a) - --- --------------------- - -data Nat = Zer - | Suc Nat - deriving Show--- deriving (Show,Data, Typeable)- --instance Serial Nat where- series = cons0 Zer \/ cons1 Suc--sub :: Nat -> Nat -> Nat -sub x y = - case y of - Zer -> x - Suc y' -> case x of - Zer -> Zer - Suc x' -> sub x' y' - -data Sym = N0 - | N1 Sym - deriving (Eq, Show) --- deriving (Eq, Show, Data, Typeable) --instance Serial Sym where- series = cons0 N0 \/ cons1 N1---- deriving Eq - -data RE = Sym Sym - | Or RE RE - | Seq RE RE - | And RE RE - | Star RE - | Empty - deriving Show--- deriving (Data, Typeable, Show)--{--instance Serial RE where- series = cons0 Empty- \/ cons1 Star- \/ cons2 And- \/ cons2 Seq- \/ cons2 Or- \/ cons1 Sym--}--instance Serial RE where- series = cons1 Sym- \/ cons2 Or- \/ cons2 Seq- \/ cons2 And- \/ cons1 Star- \/ cons0 Empty--- -accepts :: RE -> [Sym] -> Bool -accepts re ss = - case re of - Sym n -> case ss of - [] -> False - (n':ss') -> n == n' && null ss' - Or re1 re2 -> accepts re1 ss || accepts re2 ss - Seq re1 re2 -> seqSplit re1 re2 [] ss - And re1 re2 -> accepts re1 ss && accepts re2 ss - Star re' -> case ss of - [] -> True - (s:ss') -> seqSplit re' re (s:[]) ss' - -- accepts Empty ss || accepts (Seq re' re) ss - Empty -> null ss - -seqSplit :: RE -> RE -> [Sym] -> [Sym] -> Bool -seqSplit re1 re2 ss2 ss = - seqSplit'' re1 re2 ss2 ss || seqSplit' re1 re2 ss2 ss - -seqSplit'' :: RE -> RE -> [Sym] -> [Sym] -> Bool -seqSplit'' re1 re2 ss2 ss = accepts re1 ss2 && accepts re2 ss - -seqSplit' :: RE -> RE -> [Sym] -> [Sym] -> Bool -seqSplit' re1 re2 ss2 ss = - case ss of - [] -> False - (n:ss') -> - seqSplit re1 re2 (ss2 ++ [n]) ss' - -rep :: Nat -> RE -> RE -rep n re = - case n of - Zer -> Empty - Suc n' -> Seq re (rep n' re) - -repMax :: Nat -> RE -> RE -repMax n re = - case n of - Zer -> Empty - Suc n' -> Or (rep n re) (repMax n' re) - -repInt' :: Nat -> Nat -> RE -> RE -repInt' n k re = - case k of - Zer -> rep n re - Suc k' -> Or (rep n re) (repInt' (Suc n) k' re) - -repInt :: Nat -> Nat -> RE -> RE -repInt n k re = repInt' n (sub k n) re - --- --------------------- - - --- main_1-prop_regex :: (Nat, Nat, RE, RE, [Sym]) -> Bool -prop_regex (n, k, p, q, s) = r -- if r then True else True- where- r = (accepts (repInt n k (And p q)) s)- <==> (accepts (And (repInt n k p) (repInt n k q)) s)---(accepts (And (repInt n k p) (repInt n k q)) s) <==> (accepts (repInt n k (And p q)) s) - -a_sol = (Zer, Suc (Suc Zer), Sym N0, Seq (Sym N0) (Sym N0), [N0, N0]) -
− benchmarks/Sad.hs
@@ -1,92 +0,0 @@--- We take the following specification for the sum of absolute--- differences, and develop a program that generates circuits that--- have the same behaviour--sad :: [Int] -> [Int] -> Int-sad xs ys = sum (map abs (zipWith (-) xs ys))--type Bit = Bool--low :: Bit-low = False--high :: Bit-high = True--inv :: Bit -> Bit-inv a = not a--and2 :: Bit -> Bit -> Bit-and2 a b = a && b-or2 a b = a || b-xor2 a b = a /= b-xnor2 a b = a == b--mux2 :: Bit -> Bit -> Bit -> Bit-mux2 sel a b = (sel && b) || (not sel && a)--bitAdd :: Bit -> [Bit] -> [Bit]-bitAdd x [] = [x]-bitAdd x (y:ys) = let (sum,carry) = halfAdd x y- in sum:bitAdd carry ys--halfAdd x y = (xor2 x y,and2 x y)--binAdd :: [Bit] -> [Bit] -> [Bit]-binAdd xs ys = binAdd' low xs ys--binAdd' cin [] [] = [cin]-binAdd' cin (x:xs) [] = bitAdd cin (x:xs)-binAdd' cin [] (y:ys) = bitAdd cin (y:ys)-binAdd' cin (x:xs) (y:ys) = let (sum,cout) = fullAdd cin x y- in sum:binAdd' cout xs ys--fullAdd cin a b = let (s0,c0) = halfAdd a b- (s1,c1) = halfAdd cin s0- in (s1,xor2 c0 c1)--binGte :: [Bit] -> [Bit] -> Bit-binGte xs ys = binGte' high xs ys--binGte' gin [] [] = gin-binGte' gin (x:xs) [] = orl (gin:x:xs)-binGte' gin [] (y:ys) = and2 gin (orl (y:ys))-binGte' gin (x:xs) (y:ys) = let gout = gteCell gin x y- in binGte' gout xs ys--gteCell gin x y = mux2 (xnor2 x y) x gin--orl :: [Bit] -> Bit-orl xs = tree or2 low xs--binDiff :: [Bit] -> [Bit] -> [Bit]-binDiff xs ys = let xs' = pad (length ys) xs- ys' = pad (length xs) ys- gte = binGte xs' ys'- xs'' = map (xor2 (inv gte)) xs'- ys'' = map (xor2 gte) ys'- in init (binAdd' high xs'' ys'')- -pad :: Int -> [Bit] -> [Bit]-pad n xs | m > n = xs- | otherwise = xs ++ replicate (n-m) False- where- m = length xs--tree :: (a -> a -> a) -> a -> [a] -> a-tree f z [] = z-tree f z [x] = x-tree f z (x:y:ys) = tree f z (ys ++ [f x y])--binSum :: [[Bit]] -> [Bit]-binSum xs = tree binAdd [] xs--binSad :: [[Bit]] -> [[Bit]] -> [Bit]-binSad xs ys = binSum (zipWith binDiff xs ys)--num :: [Bit] -> Int-num [] = 0-num (a:as) = fromEnum a + 2 * num as--prop_binSad (xs, ys) = sad (map num xs) (map num ys)- == num (binSad xs ys)
− benchmarks/SumPuz.hs
@@ -1,68 +0,0 @@-import Data.List((\\))-import Char(isAlpha, chr, ord)-import Maybe(fromJust)--type Soln = [(Char, Int)]--solve :: String -> String-solve p =- display p (solutions xs ys zs 0 [])- where- [xs,ys,zs] = map reverse (words (filter (`notElem` "+=") p))--display :: String -> [Soln] -> String-display p [] = "No solution!"-display p (s:_) =- map soln p- where- soln c = if isAlpha c then chr (ord '0' + img s c) else c--rng :: Soln -> [Int]-rng = map snd--img :: Soln -> Char -> Int-img lds l = fromJust (lookup l lds)--bindings :: Char -> [Int] -> Soln -> [Soln]-bindings l ds lds =- case lookup l lds of- Nothing -> map (:lds) (zip (repeat l) (ds \\ rng lds))- Just d -> if d `elem` ds then [lds] else []--solutions :: String -> String -> String -> Int -> Soln -> [Soln]-solutions [] [] [] c lds = if c==0 then [lds] else []-solutions [] [] [z] c lds = if c==1 then bindings z [1] lds else []-solutions (x:xs) (y:ys) (z:zs) c lds =- solns `ofAll`- bindings y [(if null ys then 1 else 0)..9] `ofAll`- bindings x [(if null xs then 1 else 0)..9] lds- where - solns s = - solutions xs ys zs (xy `div` 10) `ofAll` bindings z [xy `mod` 10] s- where - xy = img s x + img s y + c--infixr 5 `ofAll`-ofAll :: (a -> [b]) -> [a] -> [b]-ofAll = concatMap---- Property--find :: String -> String -> String -> [Soln]-find xs ys zs = solutions (reverse xs) (reverse ys) (reverse zs) 0 []--val :: Soln -> String -> Int-val s "" = 0-val s xs = read (concatMap (show . img s) xs)--prop_Sound :: (String, String, String) -> Bool-prop_Sound (xs, ys, zs) =- length xs == length ys- && (diff == 0 || diff == 1)- && not (null sols)- ==> and [ val s xs + val s ys == val s zs- | s <- sols- ]- where- sols = find xs ys zs- diff = length zs - length xs
− benchmarks/clean.sh
@@ -1,5 +0,0 @@-#!/bin/sh--rm -f *.hi *.o List Countdown *2.hs RegExp Mux SumPuz Sad-cd LazySmallCheck-rm -f *.hi *.o
+ examples/Catch.hs view
@@ -0,0 +1,112 @@+module Catch where++-- A property of Catch by Neil Mitchell++import Data.List+import Data.Maybe+++-- Property++data Prop a = Or [Prop a] | And [Prop a] | Lit a++andP = And+orP = Or+lit = Lit+true = And []+++-- Constraints++data Sat a = Sat a Constraint++substP :: Eq alpha => [(alpha,beta)] -> Prop (Sat alpha) -> Prop (Sat beta)+substP xs (Lit (Sat i k)) = Lit $ Sat (fromJust $ lookup i xs) k+substP xs (And p) = And $ map (substP xs) p+substP xs (Or p) = Or $ map (substP xs) p+++-- MP constraints++type Constraint = [Val]+data Val = [Pattern] :* [Pattern] | Any deriving (Show,Eq)+data Pattern = Pattern CtorName [Val] deriving (Show,Eq)+++(<|) :: CtorName -> Constraint -> Prop (Sat Int)+c <| vs = orP (map f vs)+ where+ (rec,non) = partition (isRec . (,) c) [0..arity c-1]++ f Any = true+ f (ms_1 :* ms_2) = orP [ andP $ map lit $ g vs_1+ | Pattern c_1 vs_1 <- ms_1, c_1 == c]+ where g vs = zipWith Sat non (map (:[]) vs) +++ map (`Sat` [ms_2 :* ms_2]) rec++mergeVal :: Val -> Val -> Val+(a_1 :* b_1) `mergeVal` (a_2 :* b_2) = merge a_1 a_2 :* merge b_1 b_2+x `mergeVal` y = if x == Any then y else x++merge :: [Pattern] -> [Pattern] -> [Pattern]+merge ms_1 ms_2 = [Pattern c_1 (zipWith mergeVal vs_1 vs_2) |+ Pattern c_1 vs_1 <- ms_1, Pattern c_2 vs_2 <- ms_2, c_1 == c_2]++validConstraint = all validVal+validVal Any = True+validVal (ms1 :* ms2) = validPatterns ms1 && validPatterns ms2+validPatterns = all validPattern+validPattern (Pattern c xs) = (fields c == length xs) && all validVal xs+++-- Evaluator++data Value = Value CtorName [Value]+ | Bottom+ deriving (Eq,Show)++sat :: Sat Value -> Bool+sat (Sat Bottom k) = True+sat (Sat (Value c xs) k) = sat' $ substP (zip [0..] xs) (c <| k)++sat' :: Prop (Sat Value) -> Bool+sat' (And xs) = all sat' xs+sat' (Or xs) = any sat' xs+sat' (Lit x) = sat x+++-- Core language++data CtorName = Ctor | CtorN | CtorR | CtorNR+ deriving (Show,Eq)++arity Ctor = 0+arity CtorN = 1+arity CtorR = 1+arity CtorNR = 2++fields Ctor = 0+fields CtorN = 1+fields CtorR = 0+fields CtorNR = 1++isRec (CtorR, 0) = True+isRec (CtorNR, 1) = True+isRec _ = False++validValue :: Value -> Bool+validValue Bottom = True+validValue (Value c xs) = (arity c == length xs) && all validValue xs+++-- Properties++infixr 0 -->+False --> _ = True+True --> x = x++prop :: (Value, [Pattern], [Pattern]) -> Bool+prop (v,ms1,ms2) = (validValue v && validPatterns ms1 && validPatterns ms2 &&+ sat (Sat v [ms :* ms])) --> sat (Sat v [ms1 :* ms2])+ where+ ms = merge ms1 ms2
+ examples/Countdown.hs view
@@ -0,0 +1,195 @@+module Countdown where++-----------------------------------------------------------------------------+--+-- The Countdown Problem+--+-- Graham Hutton+-- University of Nottingham+--+-- November 2001+--+-----------------------------------------------------------------------------++-----------------------------------------------------------------------------+-- Formally specifying the problem+-----------------------------------------------------------------------------++data Op = Add | Sub | Mul | Div+ deriving Eq++valid :: Op -> Int -> Int -> Bool+valid Add _ _ = True+valid Sub x y = x > y+valid Mul _ _ = True+valid Div x y = x `mod` y == 0++apply :: Op -> Int -> Int -> Int+apply Add x y = x + y+apply Sub x y = x - y+apply Mul x y = x * y+apply Div x y = x `div` y++data Expr = Val Int | App Op Expr Expr+ deriving Eq++values :: Expr -> [Int]+values (Val n) = [n]+values (App _ l r) = values l ++ values r++eval :: Expr -> [Int]+eval (Val n) = [n | n > 0]+eval (App o l r) = [apply o x y | x <- eval l, y <- eval r, valid o x y]++subbags :: [a] -> [[a]]+subbags xs = [zs | ys <- subs xs, zs <- perms ys]++subs :: [a] -> [[a]]+subs [] = [[]]+subs (x:xs) = ys ++ map (x:) ys+ where+ ys = subs xs++perms :: [a] -> [[a]]+perms [] = [[]]+perms (x:xs) = concat (map (interleave x) (perms xs))++interleave :: a -> [a] -> [[a]]+interleave x [] = [[x]]+interleave x (y:ys) = (x:y:ys) : map (y:) (interleave x ys)++solution :: Expr -> [Int] -> Int -> Bool+solution e ns n = elem (values e) (subbags ns) && eval e == [n]++-----------------------------------------------------------------------------+-- Brute force implementation+-----------------------------------------------------------------------------++split :: [a] -> [([a],[a])]+split [] = [([],[])]+split (x:xs) = ([],x:xs) : [(x:ls,rs) | (ls,rs) <- split xs]++nesplit :: [a] -> [([a],[a])]+nesplit = filter ne . split++ne :: ([a],[b]) -> Bool+ne (xs,ys) = not (null xs || null ys)++exprs :: [Int] -> [Expr]+exprs [] = []+exprs [n] = [Val n]+exprs ns = [e | (ls,rs) <- nesplit ns+ , l <- exprs ls+ , r <- exprs rs+ , e <- combine l r]++combine :: Expr -> Expr -> [Expr]+combine l r = [App o l r | o <- ops]++ops :: [Op]+ops = [Add,Sub,Mul,Div]++solutions :: [Int] -> Int -> [Expr]+solutions ns n = [e | ns' <- subbags ns, e <- exprs ns', eval e == [n]]++-----------------------------------------------------------------------------+-- Fusing generation and evaluation+-----------------------------------------------------------------------------++type Result = (Expr,Int)++results :: [Int] -> [Result]+results [] = []+results [n] = [(Val n,n) | n > 0]+results ns = [res | (ls,rs) <- nesplit ns+ , lx <- results ls+ , ry <- results rs+ , res <- combine' lx ry]++combine' :: Result -> Result -> [Result]+combine' (l,x) (r,y) = [(App o l r, apply o x y) | o <- ops, valid o x y]++solutions' :: [Int] -> Int -> [Expr]+solutions' ns n = [e | ns' <- subbags ns, (e,m) <- results ns', m == n]++-----------------------------------------------------------------------------+-- Exploiting arithmetic properties+-----------------------------------------------------------------------------++valid' :: Op -> Int -> Int -> Bool+valid' Add x y = x <= y+valid' Sub x y = x > y+valid' Mul x y = x /= 1 && y /= 1 && x <= y+valid' Div x y = y /= 1 && x `mod` y == 0++eval' :: Expr -> [Int]+eval' (Val n) = [n | n > 0]+eval' (App o l r) = [apply o x y | x <- eval' l, y <- eval' r, valid' o x y]++solution' :: Expr -> [Int] -> Int -> Bool+solution' e ns n = elem (values e) (subbags ns) && eval' e == [n]++results' :: [Int] -> [Result]+results' [] = []+results' [n] = [(Val n,n) | n > 0]+results' ns = [res | (ls,rs) <- nesplit ns+ , lx <- results' ls+ , ry <- results' rs+ , res <- combine'' lx ry]++combine'' :: Result -> Result -> [Result]+combine'' (l,x) (r,y) = [(App o l r, apply o x y) | o <- ops, valid' o x y]++solutions'' :: [Int] -> Int -> [Expr]+solutions'' ns n = [e | ns' <- subbags ns, (e,m) <- results' ns', m == n]++-----------------------------------------------------------------------------+-- Interactive version for testing+-----------------------------------------------------------------------------++instance Show Op where+ show Add = "+"+ show Sub = "-"+ show Mul = "*"+ show Div = "/"++instance Show Expr where+ show (Val n) = show n+ show (App o l r) = bracket l ++ show o ++ bracket r+ where+ bracket (Val n) = show n+ bracket e = "(" ++ show e ++ ")"++display :: [Expr] -> IO ()+display [] = putStr "\nThere are no solutions.\n\n"+display (e:es) = do putStr "\nOne possible solution is "+ putStr (show e)+ putStr ".\n\nPress return to continue searching..."+ getLine+ putStr "\n"+ if null es then+ putStr "There are no more solutions.\n\n"+ else+ do sequence [print e | e <- es]+ putStr "\nThere were "+ putStr (show (length (e:es)))+ putStr " solutions in total.\n\n"++-- Properties++infixr 0 -->+False --> _ = True+True --> x = x++prop_lemma1 :: ([Int], [Int], [Int]) -> Bool+prop_lemma1 (xs, ys, zs) = ((xs,ys) `elem` split zs) == (xs ++ ys == zs)++prop_lemma3 :: ([Int], [Int], [Int]) -> Bool+prop_lemma3 (xs, ys, zs) = ((xs, ys) `elem` nesplit zs)+ == (xs ++ ys == zs && ne (xs, ys))++prop_lemma4 :: ([Int], [Int], [Int]) -> Bool+prop_lemma4 (xs, ys, zs) = ((xs, ys) `elem` nesplit zs) -->+ (length xs < length zs && length ys < length zs)++prop_solutions (ns, m) = solutions ns m == solutions' ns m
+ examples/Huffman.hs view
@@ -0,0 +1,86 @@+module Huffman where++-- A Huffman codec, slightly adapted from Bird+-- (with properties added)++data BTree a = Leaf a | Fork (BTree a) (BTree a)+ deriving Show++decode t bs = if null bs then [] else dec t t bs++dec (Leaf x) t bs = x : decode t bs+dec (Fork xt yt) t (b:bs) = dec (if b then yt else xt) t bs++encode t cs = enc (codetable t) cs++enc table [] = []+enc table (c:cs) = (table ! c) ++ enc table cs++((x, bs) : xbs) ! y = if x == y then bs else xbs ! y++codetable t = tab [] t++tab p (Leaf x) = [(x,p)]+tab p (Fork xt yt) = tab (p++[False]) xt ++ tab (p++[True]) yt++collate [] = []+collate (c:cs) = insert (1+n, Leaf c) (collate ds)+ where (n, ds) = count c cs++count x [] = (0, [])+count x (y:ys) = if x == y then (1+n, zs) else (n, y:zs)+ where (n, zs) = count x ys++insert (w, x) [] = [(w, x)]+insert (w0, x) ((w1, y):wys)+ | w0 <= w1 = (w0, x) : (w1, y) : wys+ | otherwise = (w1, y) : insert (w0, x) wys++hufftree cs = mkHuff (collate cs)++mkHuff [(w, t)] = t+mkHuff ((w0, t0):(w1, t1):wts) =+ mkHuff (insert (w0+w1, Fork t0 t1) wts)++-- Properties++infixr 0 -->+False --> _ = True+True --> x = x++prop_decEnc cs = length h > 1 --> (decode t (encode t cs) == cs)+ where+ h = collate cs+ t = mkHuff h+ types = cs :: String++prop_optimal (cs, t) =+ t `treeOf` h --> cost h t >= cost h (mkHuff h)+ where+ h = collate cs+ types = cs :: String++-- Cost++cost h t = cost' h (codetable t)++cost' h [] = 0+cost' h ((c, bs):cbs) = (n * length bs) + cost' h cbs+ where+ n = head [n | (n, Leaf sym) <- h, sym == c]++leaves (Leaf c) = [c]+leaves (Fork xt yt) = leaves xt ++ leaves yt++treeOf t h = leaves t === [c | (_, Leaf c) <- h]++[] === [] = True+(x:xs) === ys = case del x ys of+ Nothing -> False+ Just zs -> xs === zs+_ === _ = False++del x [] = Nothing+del x (y:ys) = if x == y then Just ys else case del x ys of+ Nothing -> Nothing+ Just zs -> Just (y:zs)
+ examples/ListSet.hs view
@@ -0,0 +1,34 @@+module ListSet where++type Set a = [a]++empty :: Set a+empty = []++insert :: Ord a => a -> Set a -> Set a+insert a [] = [a]+insert a (x:xs)+ | a < x = a:x:xs+ | a > x = x:insert a xs+ | a == x = x:xs++set :: Ord a => [a] -> Set a+set = foldr insert empty++ordered [] = True+ordered [x] = True+ordered (x:y:zs) = x <= y && ordered (y:zs)++allDiff [] = True+allDiff (x:xs) = x `notElem` xs && allDiff xs++isSet s = ordered s && allDiff s++-- Properties++infixr 0 -->+False --> _ = True+True --> x = x++prop_insertSet :: (Char, Set Char) -> Bool+prop_insertSet (c, s) = ordered s --> ordered (insert c s)
+ examples/Mate.hs view
@@ -0,0 +1,256 @@+module Mate where++import LazySmallCheck+import List++data Kind = King | Queen | Rook | Bishop | Knight | Pawn+ deriving (Eq, Show)++data Colour = Black | White+ deriving (Eq, Show)++type Piece = (Colour,Kind)+type Square = (Int,Int)++data Board = Board+ [(Kind,Square)] -- white+ [(Kind,Square)] -- black+ deriving Show++pieceAt :: Board -> Square -> Maybe Piece+pieceAt (Board wkss bkss) sq =+ pieceAtWith White (pieceAtWith Black Nothing bkss) wkss+ where+ pieceAtWith c n [] = n+ pieceAtWith c n ((k,s):xs) = if s==sq then Just (c,k) else pieceAtWith c n xs++emptyAtAll :: Board -> (Square->Bool) -> Bool+emptyAtAll (Board wkss bkss) e =+ emptyAtAllAnd (emptyAtAllAnd True bkss) wkss+ where+ emptyAtAllAnd b [] = b+ emptyAtAllAnd b ((_,s):xs) = not (e s) && emptyAtAllAnd b xs++rmPieceAt White sq (Board wkss bkss) = Board (rPa sq wkss) bkss+rmPieceAt Black sq (Board wkss bkss) = Board wkss (rPa sq bkss)++rPa sq (ks@(k,s):kss) = if s==sq then kss else ks : rPa sq kss++putPieceAt sq (White,k) (Board wkss bkss) = Board ((k,sq):wkss) bkss+putPieceAt sq (Black,k) (Board wkss bkss) = Board wkss ((k,sq):bkss)++kingSquare :: Colour -> Board -> Square+kingSquare White (Board kss _) = kSq kss+kingSquare Black (Board _ kss) = kSq kss++kSq ((King,s):_) = s+kSq ( _:kss) = kSq kss ++opponent Black = White+opponent White = Black++colourOf :: Piece -> Colour+colourOf (c,_) = c++kindOf :: Piece -> Kind+kindOf (_,k) = k++onboard :: Square -> Bool+onboard (p,q) = 1<=p && p<=8 && 1<=q && q<=8++forcesColoured White (Board kss _) = kss+forcesColoured Black (Board _ kss) = kss++emptyBoard = Board [] []++data Move = Move + Square -- to here+ (Maybe Piece) -- capturing this+ (Maybe Piece) -- gaining promotion to this+ +data MoveInFull = MoveInFull Piece Square Move++tryMove :: Colour -> (Kind,Square) -> Move -> Board -> Maybe (MoveInFull,Board)+tryMove c ksq@(k,sq) m@(Move sq' mcp mpp) bd =+ if not (kingincheck c bd2) then Just (MoveInFull p sq m, bd2)+ else Nothing + where+ p = (c,k)+ bd1 = rmPieceAt c sq bd+ p' = maybe p id mpp+ bd2 = maybe (putPieceAt sq' p' bd1)+ (const (putPieceAt sq' p' (rmPieceAt (opponent c) sq' bd1)))+ mcp++moveDetailsFor :: Colour -> Board -> [(MoveInFull,Board)]+moveDetailsFor c bd =+ foldr ( \ksq ms ->+ foldr (\rm ms' -> maybe id (:) (tryMove c ksq rm bd) ms')+ ms+ (rawmoves c ksq bd) )+ []+ (forcesColoured c bd)+++-- NB raw move = might illegally leave the king in check.+rawmoves :: Colour -> (Kind,Square) -> Board -> [Move]+rawmoves c (k,sq) bd = m c sq bd+ where+ m = case k of+ King -> kingmoves+ Queen -> queenmoves+ Rook -> rookmoves+ Bishop -> bishopmoves+ Knight -> knightmoves+ Pawn -> pawnmoves++bishopmoves :: Colour -> Square -> Board -> [Move]+bishopmoves c sq bd =+ ( moveLine bd c sq (\(x,y) -> (x-1,y+1)) $+ moveLine bd c sq (\(x,y) -> (x+1,y+1)) $+ moveLine bd c sq (\(x,y) -> (x-1,y-1)) $+ moveLine bd c sq (\(x,y) -> (x+1,y-1)) id+ ) []++rookmoves :: Colour -> Square -> Board -> [Move]+rookmoves c sq bd =+ ( moveLine bd c sq (\(x,y) -> (x-1,y)) $+ moveLine bd c sq (\(x,y) -> (x+1,y)) $+ moveLine bd c sq (\(x,y) -> (x,y-1)) $+ moveLine bd c sq (\(x,y) -> (x,y+1)) id+ ) []++moveLine :: Board -> Colour -> Square -> (Square->Square) -> ([Move]->a) -> [Move] -> a+moveLine bd c sq inc cont = ml sq+ where+ ml sq ms =+ let sq' = inc sq in+ if onboard sq' then+ case pieceAt bd sq' of+ Nothing -> ml sq' (Move sq' Nothing Nothing : ms)+ Just p' -> if colourOf p' /= c then+ cont (Move sq' (Just p') Nothing : ms)+ else cont ms+ else cont ms++kingmoves :: Colour -> Square -> Board -> [Move]+kingmoves c (p,q) bd =+ sift c bd [] [(p-1,q+1), (p,q+1), (p+1,q+1),+ (p-1,q), (p+1,q),+ (p-1,q-1), (p,q-1), (p+1,q-1)]++knightmoves :: Colour -> Square -> Board -> [Move]+knightmoves c (p,q) bd =+ sift c bd [] [ (p-1,q+2),(p+1,q+2),+ (p-2,q+1), (p+2,q+1),+ (p-2,q-1), (p+2,q-1),+ (p-1,q-2),(p+1,q-2) ]++sift :: Colour -> Board -> [Move] -> [Square] -> [Move]+sift _ _ ms [] = ms+sift c bd ms (sq:sqs) =+ if onboard sq then+ case pieceAt bd sq of+ Nothing -> sift c bd (Move sq Nothing Nothing : ms) sqs+ Just p' -> if colourOf p' == c then sift c bd ms sqs+ else sift c bd (Move sq (Just p') Nothing : ms) sqs+ else sift c bd ms sqs++pawnmoves :: Colour -> Square -> Board -> [Move]+pawnmoves c (p,q) bd = movs ++ caps+ where+ movs = let on1 = (p,q+fwd)+ on2 = (p,q+2*fwd) in+ if pieceAt bd on1 == Nothing then+ promote on1 Nothing +++ if (q==2 && c==White || q==7 && c==Black) &&+ pieceAt bd on2 == Nothing then [Move on2 Nothing Nothing] + else []+ else []+ caps = concat [ promote sq mcp+ | sq <- [(p+1,q+fwd), (p-1,q+fwd)],+ mcp@(Just p') <- [pieceAt bd sq], colourOf p'/=c ]+ fwd = case c of+ White -> 1+ Black -> -1+ promote sq@(x,y) mcp = + if (c==Black && y==1 || c==White && y==8) then+ map (Move sq mcp . Just)+ [(c,Queen), (c,Rook), (c,Bishop), (c,Knight)]+ else [Move sq mcp Nothing]++queenmoves :: Colour -> Square -> Board -> [Move]+queenmoves c sq bd = bishopmoves c sq bd ++ rookmoves c sq bd++kingincheck :: Colour -> Board -> Bool+kingincheck c bd =+ any givesCheck (forcesColoured (opponent c) bd)+ where+ givesCheck (k,(x,y)) = kthreat k+ where+ kthreat King =+ abs (x-xk) <= 1 && abs (y-yk) <= 1+ kthreat Queen =+ kthreat Rook || kthreat Bishop+ kthreat Rook =+ x==xk &&+ emptyAtAll bd (\(xe,ye) -> xe==xk && min y yk < ye && ye < max y yk) ||+ y==yk &&+ emptyAtAll bd (\(xe,ye) -> ye==yk && min x xk < xe && xe < max x xk)+ kthreat Bishop =+ x+y==xk+yk &&+ emptyAtAll bd (\(xe,ye) -> xe+ye==xk+yk && min x xk < xe && xe < max x xk) ||+ x-y==xk-yk &&+ emptyAtAll bd (\(xe,ye) -> xe-ye==xk-yk && min x xk < xe && xe < max x xk)+ kthreat Knight =+ abs (x-xk) == 2 && abs (y-yk) == 1 ||+ abs (x-xk) == 1 && abs (y-yk) == 2+ kthreat Pawn =+ abs (x-xk) == 1 &&+ case c of+ Black -> yk == y+1+ White -> yk == y-1+ (xk,yk) = kingSquare c bd++checkmate :: Colour -> Board -> Bool+checkmate col b = null (moveDetailsFor col b) && kingincheck col b++-- Board generator++allDiff [] = True+allDiff (x:xs) = x `notElem` xs && allDiff xs++onBoard (p, q) = 1 <= p && p <= 8 && 1 <= q && q <= 8++one p [] = False+one p (x:xs) = if p x then all (not . p) xs else one p xs++kingsDontTouch ws bs =+ (bx > succ wx || wx > succ bx || by > succ wy || wy > succ by)+ where+ (wx, wy) = kSq ws+ (bx, by) = kSq bs++validBoard (Board ws bs) =+ one ((== King) . fst) ws+ && one ((== King) . fst) bs+ && all onBoard sqs+ && kingsDontTouch ws bs+ && allDiff sqs+ where+ sqs = map snd (ws ++ bs)++-- Property++infixr 0 -->+False --> _ = True+True --> x = x++prop_checkmate b = + ( length ws == 2+ && Pawn `elem` (map fst ws)+ && validBoard b+ )+ ==> not (checkmate Black b)+ where+ ws = forcesColoured White b
+ examples/Mux.hs view
@@ -0,0 +1,64 @@+module Mux where++import Data.List++type Bit = Bool+ +mux :: [Bit] -> [[Bit]] -> [Bit]+mux sel xs = map (tree (||))+ $ transpose+ $ zipWith (\s x -> map (s &&) x) sel xs++tree :: (a -> a -> a) -> [a] -> a+tree f [x] = x+tree f (x:y:ys) = tree f (ys ++ [f x y])++decode :: [Bit] -> [Bit]+decode [] = [True] +decode [x] = [not x,x]+decode (x:xs) = concatMap (\y -> [not x && y,x && y]) rest+ where+ rest = decode xs+ +binaryMux :: [Bit] -> [[Bit]] -> [Bit]+binaryMux sel xs = mux (decode sel) xs++num :: [Bool] -> Int+num [] = 0+num (a:as) = (if a then 1 else 0) + 2 * num as++encode as = enc (as ++ replicate n False)+ where+ n = 2 ^ ulog2 (length as) - length as++enc [_] = []+enc as = zipWith (||) (enc ls) (enc rs) ++ [tree (||) rs]+ where+ (ls, rs) = splitAt (length as `div` 2) as++oneHot [] = False+oneHot (a:as) = if a then not (or as) else oneHot as++log2 n = if n == 1 then 0 else 1 + log2 (n `div` 2)++ulog2 n = log2 (2*n - 1)++-- Properties++infixr 0 -->+False --> _ = True+True --> x = x++prop_encode as = oneHot as --> (num (encode as) == n)+ where+ n = length (takeWhile not as)++prop_mux (sel, xs) =+ oneHot sel+ && length sel == length xs+ && all ((== length (head xs)) . length) xs+ --> mux sel xs == xs !! n+ where+ n = length (takeWhile not sel)++prop_encDec as = encode (decode as) == as
+ examples/RedBlack.hs view
@@ -0,0 +1,80 @@+module RedBlack where++-- Red-Black trees in a functional setting, by Okasaki.+-- (With invariants coded, and a fault injected.)++data Colour = R | B+ deriving Show++data Tree a = E | T Colour (Tree a) a (Tree a)+ deriving Show++-- Methods++member x E = False+member x (T _ a y b)+ | x < y = member x a+ | x > y = member x b+ | otherwise = True++makeBlack (T _ a y b) = T B a y b++insert x s = makeBlack (ins x s)++ins x E = T R E x E+ins x (T col a y b)+ | x < y = balance col (ins x a) y b+ | x > y = balance col a y (ins x b)+ | otherwise = T col a y b++-- Mistake on 4th line, 3rd line is correct+balance B (T R (T R a x b) y c) z d = T R (T B a x b) y (T B c z d)+balance B (T R a x (T R b y c)) z d = T R (T B a x b) y (T B c z d)+--balance B a x (T R (T R b y c) z d) = T R (T B a x b) y (T B c z d)+balance B a x (T R (T R c y b) z d) = T R (T B a x b) y (T B c z d)+balance B a x (T R b y (T R c z d)) = T R (T B a x b) y (T B c z d)+balance col a x b = T col a x b++-- Helpers++isRed R = True+isRed B = False++blackRoot E = True+blackRoot (T col a x b) = not (isRed col)++-- INVARIANT 1. No red node has a red parent.++red E = True+red (T col a x b) =+ (if isRed col then blackRoot a && blackRoot b else True) && red a && red b++-- INVARIANT 2. Every path from the root to an empty node contains the+-- same number of black nodes.++black t = fst (black' t)++black' E = (True, 1)+black' (T col a x b) = (b0 && b1 && n == m, n + if isRed col then 0 else 1)+ where (b0, n) = black' a+ (b1, m) = black' b++-- INVARIANT 3. Trees are ordered.++every p E = True+every p (T _ a x b) = p x && every p a && every p b++ord E = True+ord (T _ a x b) = every (<= x) a && every (>= x) b && ord a && ord b++-- Properties++infixr 0 -->+False --> _ = True+True --> x = x++redBlack t = red t && black t && ord t++prop_insertRB (x, t) = redBlack t --> redBlack (insert x t)+ where+ types = x :: Int
+ examples/RegExp.hs view
@@ -0,0 +1,91 @@+module RegExp where++(<==>) :: Bool -> Bool -> Bool+a <==> b = a == b++-- ---------------------++data Nat = Zer+ | Suc Nat+ deriving (Eq, Show)++sub :: Nat -> Nat -> Nat+sub x y =+ case y of+ Zer -> x+ Suc y' -> case x of+ Zer -> Zer+ Suc x' -> sub x' y'++data Sym = N0+ | N1 Sym+ deriving (Eq, Show)++data RE = Sym Sym+ | Or RE RE+ | Seq RE RE+ | And RE RE+ | Star RE+ | Empty+ deriving (Eq, Show)++accepts :: RE -> [Sym] -> Bool+accepts re ss =+ case re of+ Sym n -> case ss of+ [] -> False+ (n':ss') -> n == n' && null ss'+ Or re1 re2 -> accepts re1 ss || accepts re2 ss+ Seq re1 re2 -> seqSplit re1 re2 [] ss+ And re1 re2 -> accepts re1 ss && accepts re2 ss+ Star re' -> case ss of+ [] -> True+ (s:ss') -> seqSplit re' re (s:[]) ss'+ -- accepts Empty ss || accepts (Seq re' re) ss+ Empty -> null ss++seqSplit :: RE -> RE -> [Sym] -> [Sym] -> Bool+seqSplit re1 re2 ss2 ss =+ seqSplit'' re1 re2 ss2 ss || seqSplit' re1 re2 ss2 ss++seqSplit'' :: RE -> RE -> [Sym] -> [Sym] -> Bool+seqSplit'' re1 re2 ss2 ss = accepts re1 ss2 && accepts re2 ss++seqSplit' :: RE -> RE -> [Sym] -> [Sym] -> Bool+seqSplit' re1 re2 ss2 ss =+ case ss of+ [] -> False+ (n:ss') ->+ seqSplit re1 re2 (ss2 ++ [n]) ss'++rep :: Nat -> RE -> RE+rep n re =+ case n of+ Zer -> Empty+ Suc n' -> Seq re (rep n' re)++repMax :: Nat -> RE -> RE+repMax n re =+ case n of+ Zer -> Empty+ Suc n' -> Or (rep n re) (repMax n' re)++repInt' :: Nat -> Nat -> RE -> RE+repInt' n k re =+ case k of+ Zer -> rep n re+ Suc k' -> Or (rep n re) (repInt' (Suc n) k' re)++repInt :: Nat -> Nat -> RE -> RE+repInt n k re = repInt' n (sub k n) re++-- Properties++prop_regex :: (Nat, Nat, RE, RE, [Sym]) -> Bool+prop_regex (n, k, p, q, s) = r+ where+ r = (accepts (repInt n k (And p q)) s)+ <==> (accepts (And (repInt n k p) (repInt n k q)) s)+ --(accepts (And (repInt n k p) (repInt n k q)) s) <==> (accepts (repInt n k (And p q)) s)^M++a_sol = (Zer, Suc (Suc Zer), Sym N0, Seq (Sym N0) (Sym N0), [N0, N0])
+ examples/Sad.hs view
@@ -0,0 +1,96 @@+module Sad where++-- We take the following specification for the sum of absolute+-- differences, and develop a program that generates circuits that+-- have the same behaviour++sad :: [Int] -> [Int] -> Int+sad xs ys = sum (map abs (zipWith (-) xs ys))++type Bit = Bool++low :: Bit+low = False++high :: Bit+high = True++inv :: Bit -> Bit+inv a = not a++and2 :: Bit -> Bit -> Bit+and2 a b = a && b+or2 a b = a || b+xor2 a b = a /= b+xnor2 a b = a == b++mux2 :: Bit -> Bit -> Bit -> Bit+mux2 sel a b = (sel && b) || (not sel && a)++bitAdd :: Bit -> [Bit] -> [Bit]+bitAdd x [] = [x]+bitAdd x (y:ys) = let (sum,carry) = halfAdd x y+ in sum:bitAdd carry ys++halfAdd x y = (xor2 x y,and2 x y)++binAdd :: [Bit] -> [Bit] -> [Bit]+binAdd xs ys = binAdd' low xs ys++binAdd' cin [] [] = [cin]+binAdd' cin (x:xs) [] = bitAdd cin (x:xs)+binAdd' cin [] (y:ys) = bitAdd cin (y:ys)+binAdd' cin (x:xs) (y:ys) = let (sum,cout) = fullAdd cin x y+ in sum:binAdd' cout xs ys++fullAdd cin a b = let (s0,c0) = halfAdd a b+ (s1,c1) = halfAdd cin s0+ in (s1,xor2 c0 c1)++binGte :: [Bit] -> [Bit] -> Bit+binGte xs ys = binGte' high xs ys++binGte' gin [] [] = gin+binGte' gin (x:xs) [] = orl (gin:x:xs)+binGte' gin [] (y:ys) = and2 gin (orl (y:ys))+binGte' gin (x:xs) (y:ys) = let gout = gteCell gin x y+ in binGte' gout xs ys++gteCell gin x y = mux2 (xnor2 x y) x gin++orl :: [Bit] -> Bit+orl xs = tree or2 low xs++binDiff :: [Bit] -> [Bit] -> [Bit]+binDiff xs ys = let xs' = pad (length ys) xs+ ys' = pad (length xs) ys+ gte = binGte xs' ys'+ xs'' = map (xor2 (inv gte)) xs'+ ys'' = map (xor2 gte) ys'+ in init (binAdd' high xs'' ys'')++pad :: Int -> [Bit] -> [Bit]+pad n xs | m > n = xs+ | otherwise = xs ++ replicate (n-m) False+ where+ m = length xs++tree :: (a -> a -> a) -> a -> [a] -> a+tree f z [] = z+tree f z [x] = x+tree f z (x:y:ys) = tree f z (ys ++ [f x y])++binSum :: [[Bit]] -> [Bit]+binSum xs = tree binAdd [] xs++binSad :: [[Bit]] -> [[Bit]] -> [Bit]+binSad xs ys = binSum (zipWith binDiff xs ys)++num :: [Bit] -> Int+num [] = 0+num (a:as) = fromEnum a + 2 * num as++-- Properties++prop_binSad (xs, ys) = sad (map num xs) (map num ys)+ == num (binSad xs ys)
+ examples/SumPuz.hs view
@@ -0,0 +1,76 @@+module SumPuz where++-- Cryptarithmetic solver from AFP 2003++import Data.List((\\))+import Char(isAlpha, chr, ord)+import Maybe(fromJust)++type Soln = [(Char, Int)]++solve :: String -> String+solve p =+ display p (solutions xs ys zs 0 [])+ where+ [xs,ys,zs] = map reverse (words (filter (`notElem` "+=") p))++display :: String -> [Soln] -> String+display p [] = "No solution!"+display p (s:_) =+ map soln p+ where+ soln c = if isAlpha c then chr (ord '0' + img s c) else c++rng :: Soln -> [Int]+rng = map snd++img :: Soln -> Char -> Int+img lds l = fromJust (lookup l lds)++bindings :: Char -> [Int] -> Soln -> [Soln]+bindings l ds lds =+ case lookup l lds of+ Nothing -> map (:lds) (zip (repeat l) (ds \\ rng lds))+ Just d -> if d `elem` ds then [lds] else []++solutions :: String -> String -> String -> Int -> Soln -> [Soln]+solutions [] [] [] c lds = if c==0 then [lds] else []+solutions [] [] [z] c lds = if c==1 then bindings z [1] lds else []+solutions (x:xs) (y:ys) (z:zs) c lds =+ solns `ofAll`+ bindings y [(if null ys then 1 else 0)..9] `ofAll`+ bindings x [(if null xs then 1 else 0)..9] lds+ where + solns s = + solutions xs ys zs (xy `div` 10) `ofAll` bindings z [xy `mod` 10] s+ where + xy = img s x + img s y + c++infixr 5 `ofAll`+ofAll :: (a -> [b]) -> [a] -> [b]+ofAll = concatMap++-- Properties++infixr 0 -->+False --> _ = True+True --> x = x++find :: String -> String -> String -> [Soln]+find xs ys zs = solutions (reverse xs) (reverse ys) (reverse zs) 0 []++val :: Soln -> String -> Int+val s "" = 0+val s xs = read (concatMap (show . img s) xs)++prop_Sound :: (String, String, String) -> Bool+prop_Sound (xs, ys, zs) =+ length xs == length ys+ && (diff == 0 || diff == 1)+ && not (null sols)+ --> and [ val s xs + val s ys == val s zs+ | s <- sols+ ]+ where+ sols = find xs ys zs+ diff = length zs - length xs
+ examples/Turner.hs view
@@ -0,0 +1,59 @@+module Turner where++-- Turner's abstraction algorithm as defined by Simon PJ+-- (with properties added)++infixl 9 :@++data Var = V0 | V1+ deriving (Show, Eq)++data Exp = Exp :@ Exp | L Var Exp | V Var | F Comb+ deriving (Show, Eq)++data Comb = I | K | B | C | S | C' | B' | S'+ deriving (Show, Eq)++compile (f :@ x) = compile f :@ compile x+compile (L v e) = abstr v (compile e)+compile e = e++abstr v (f :@ x) = opt (F S :@ abstr v f :@ abstr v x)+abstr v (V w) | v == w = F I+abstr v e = F K :@ e++opt (F S :@ (F K :@ p) :@ (F K :@ q)) = F K :@ (p :@ q)+opt (F S :@ (F K :@ p) :@ F I) = p+opt (F S :@ (F K :@ p) :@ (F B :@ q :@ r)) = F B' :@ p :@ q :@ r+opt (F S :@ (F K :@ p) :@ q) = F B :@ p :@ q+opt (F S :@ (F B :@ p :@ q) :@ (F K :@ r)) = F C' :@ p :@ q :@ r+opt (F S :@ p :@ (F K :@ q)) = F C :@ p :@ q+opt (F S :@ (F B :@ p :@ q) :@ r) = F S' :@ p :@ q :@ r+opt e = e++-- Combinator reduction++simp (F I :@ a) = Just a+simp (F K :@ a :@ b) = Just a+simp (F S :@ f :@ g :@ x) = Just $ f :@ x :@ (g :@ x)+simp (F B :@ f :@ g :@ x) = Just $ f :@ (g :@ x)+simp (F C :@ f :@ g :@ x) = Just $ f :@ x :@ g+simp (F B' :@ k :@ f :@ g :@ x) = Just $ k :@ (f :@ (g :@ x))+simp (F C' :@ k :@ f :@ g :@ x) = Just $ k :@ (f :@ x) :@ g+simp (F S' :@ k :@ f :@ g :@ x) = Just $ k :@ (f :@ x) :@ (g :@ x)+simp e = Nothing++simplify e =+ case simp e of+ Nothing -> case e of+ f :@ g -> simplify f :@ simplify g+ _ -> e+ Just e' -> simplify e'++-- Properties++infixr 0 -->+False --> _ = True+True --> x = x++prop_abstr (v, e) = simplify (abstr v e :@ V v) == e
+ examples/test/TestCatch.hs view
@@ -0,0 +1,17 @@+import Test.LazySmallCheck+import Catch+import System++instance Serial Value where+ series = cons0 Bottom \/ cons2 Value++instance Serial CtorName where+ series = cons0 Ctor \/ cons0 CtorN \/ cons0 CtorR \/ cons0 CtorNR++instance Serial Val where+ series = cons2 (:*) \/ cons0 Any++instance Serial Pattern where+ series = cons2 Pattern++main = do [d] <- getArgs ; depthCheck (read d) prop
+ examples/test/TestCountdown1.hs view
@@ -0,0 +1,5 @@+import Test.LazySmallCheck+import Countdown+import System++main = do [d] <- getArgs ; depthCheck (read d) prop_lemma3
+ examples/test/TestCountdown2.hs view
@@ -0,0 +1,5 @@+import Test.LazySmallCheck+import Countdown+import System++main = do [d] <- getArgs ; depthCheck (read d) prop_solutions
+ examples/test/TestHuffman1.hs view
@@ -0,0 +1,8 @@+import Test.LazySmallCheck+import Huffman+import System++instance Serial a => Serial (BTree a) where+ series = cons1 Leaf \/ cons2 Fork++main = do [d] <- getArgs ; depthCheck (read d) prop_decEnc
+ examples/test/TestHuffman2.hs view
@@ -0,0 +1,8 @@+import Test.LazySmallCheck+import Huffman+import System++instance Serial a => Serial (BTree a) where+ series = cons1 Leaf \/ cons2 Fork++main = do [d] <- getArgs ; depthCheck (read d) prop_optimal
+ examples/test/TestListSet1.hs view
@@ -0,0 +1,5 @@+import Test.LazySmallCheck+import ListSet+import System++main = do [d] <- getArgs ; depthCheck (read d) prop_insertSet
+ examples/test/TestMate.hs view
@@ -0,0 +1,19 @@+import Test.LazySmallCheck+import Mate+import System++instance Serial Kind where+ series = cons0 King+ \/ cons0 Queen+ \/ cons0 Rook+ \/ cons0 Bishop+ \/ cons0 Knight+ \/ cons0 Pawn++instance Serial Colour where+ series = cons0 Black \/ cons0 White++instance Serial Board where+ series = cons2 Board++main = do [d] <- getArgs ; depthCheck (read d) prop_checkmate
+ examples/test/TestMux1.hs view
@@ -0,0 +1,5 @@+import Test.LazySmallCheck+import Mux+import System++main = do [d] <- getArgs ; depthCheck (read d) prop_mux
+ examples/test/TestMux2.hs view
@@ -0,0 +1,5 @@+import Test.LazySmallCheck+import Mux+import System++main = do [d] <- getArgs ; depthCheck (read d) prop_encode
+ examples/test/TestMux3.hs view
@@ -0,0 +1,5 @@+import Test.LazySmallCheck+import Mux+import System++main = do [d] <- getArgs ; depthCheck (read d) prop_encDec
+ examples/test/TestRedBlack.hs view
@@ -0,0 +1,11 @@+import Test.LazySmallCheck+import RedBlack+import System++instance Serial Colour where+ series = cons0 R \/ cons0 B++instance Serial a => Serial (Tree a) where+ series = cons0 E \/ cons4 T++main = do [d] <- getArgs ; depthCheck (read d) prop_insertRB
+ examples/test/TestRegExp.hs view
@@ -0,0 +1,19 @@+import Test.LazySmallCheck+import RegExp+import System++instance Serial Nat where+ series = cons0 Zer \/ cons1 Suc++instance Serial Sym where+ series = cons0 N0 \/ cons1 N1++instance Serial RE where+ series = cons1 Sym+ \/ cons2 Or+ \/ cons2 Seq+ \/ cons2 And+ \/ cons1 Star+ \/ cons0 Empty++main = do [d] <- getArgs ; depthCheck (read d) prop_regex
+ examples/test/TestSad.hs view
@@ -0,0 +1,5 @@+import Test.LazySmallCheck+import Sad+import System++main = do [d] <- getArgs ; depthCheck (read d) prop_binSad
+ examples/test/TestSumPuz.hs view
@@ -0,0 +1,5 @@+import Test.LazySmallCheck+import SumPuz+import System++main = do [d] <- getArgs ; depthCheck (read d) prop_Sound
+ examples/test/TestTurner.hs view
@@ -0,0 +1,11 @@+import Test.LazySmallCheck+import Turner+import System++instance Serial Var where+ series = cons0 V0 \/ cons0 V1++instance Serial Exp where+ series = cons2 (:@) \/ cons2 L \/ (cons1 V . (+1))++main = do [d] <- getArgs ; depthCheck (read d) prop_abstr
lazysmallcheck.cabal view
@@ -1,34 +1,51 @@ Name: lazysmallcheck-Version: 0.1-Copyright: 2007, Matthew Naylor-Maintainer: mfn@cs.york.ac.uk+Version: 0.2+Maintainer: Matthew Naylor <mfn@cs.york.ac.uk> Homepage: http://www.cs.york.ac.uk/~mfn/lazysmallcheck/-Build-Depends: base, haskell98, random-Build-Type: Simple+Build-Depends: base, haskell98 License: BSD3 License-File: LICENSE Author: Matthew Naylor and Fredrik Lindblad Synopsis: A library for demand-driven testing of Haskell programs Description:- Lazy SmallCheck is a library for exhaustive, demand-driven testing of- Haskell programs. It is based on the idea that if a property holds- for a partially-defined input then it must also hold for all- fully-defined instantiations of the that input. Compared to ``eager''- input generation as in SmallCheck, Lazy SmallCheck may require- significantly fewer test-cases to verify a property for all inputs up- to a given depth.+ Lazy SmallCheck is a library for exhaustive, demand-driven testing of+ Haskell programs. It is based on the idea that if a property holds+ for a partially-defined input then it must also hold for all+ fully-defined refinements of the that input. Compared to ``eager'' + input generation as in SmallCheck, Lazy SmallCheck may require+ significantly fewer test-cases to verify a property for all inputs up + to a given depth. Category: Testing-Hs-Source-dirs:- source+Build-Depends: base, haskell98+Build-Type: Simple Extra-Source-Files:- benchmarks/Benchmark.hs- benchmarks/Countdown.hs- benchmarks/List.hs- benchmarks/Mux.hs- benchmarks/RegExp.hs- benchmarks/Sad.hs- benchmarks/SumPuz.hs- benchmarks/clean.sh+ examples/Catch.hs+ examples/Mate.hs+ examples/Sad.hs+ examples/Countdown.hs+ examples/Mux.hs+ examples/SumPuz.hs+ examples/Huffman.hs+ examples/RedBlack.hs+ examples/Turner.hs+ examples/ListSet.hs+ examples/RegExp.hs+ examples/test/TestCatch.hs+ examples/test/TestMux2.hs+ examples/test/TestCountdown1.hs+ examples/test/TestMux3.hs+ examples/test/TestCountdown2.hs+ examples/test/TestRedBlack.hs+ examples/test/TestHuffman1.hs+ examples/test/TestRegExp.hs+ examples/test/TestHuffman2.hs+ examples/test/TestSad.hs+ examples/test/TestListSet1.hs+ examples/test/TestSumPuz.hs+ examples/test/TestMate.hs+ examples/test/TestTurner.hs+ examples/test/TestMux1.hs+ Exposed-modules:- LazySmallCheck- LazySmallCheck.Generic+ Test.LazySmallCheck+ Test.LazySmallCheck.Generic
− source/LazySmallCheck.hs
@@ -1,262 +0,0 @@-module LazySmallCheck- ( Serial(series) -- class Serial- , (\/) -- :: Series a -> Series a -> Series a- , cons0 -- :: a -> Series a- , cons1 -- :: Serial a => (a -> b) -> Series b- , cons2 -- :: (Serial a, Serial b) =>- -- (a -> b -> c) -> Series c- , cons3 -- :: (Serial a, Serial b, Serial c) =>- -- (a -> b -> c -> d) -> Series d- , cons4 -- :: (Serial a, Serial b, Serial c, Serial d) =>- -- (a -> b -> c -> d -> e) -> Series e- , cons5 -- :: (Serial a, Serial b, Serial c, Serial d, Serial e) =>- -- (a -> b -> c -> d -> e -> f) -> Series f- , Testable -- class Testable- , depthCheck -- :: Testable a => Int -> a -> IO ()- , (==>) -- :: Bool -> Bool -> Bool- ) where--import Control.Monad-import Control.Exception-import System.Exit--infixr 3 \/-infixr 0 ==>---- Type class and instance helpers--data Family = Algebraic [(Int, [Family])] | Builtin (Int -> [Value])--data Value = Var Family Int String | Ctr Int [Value] | Prim Prim--data Prim = Char Char | Int Int | Integer Integer--type Series a = Int -> (Family, [[Value] -> a])--class Serial a where- series :: Series a--genSeries :: Serial a => (Family, [[Value] -> a])-genSeries = series 0--convert :: [[Value] -> a] -> Value -> a-convert alts (Var _ _ v) = error v-convert alts (Prim p) = head alts [Prim p]-convert alts (Ctr n as) = (alts !! n) as--(\/) :: Series a -> Series a -> Series a-(c0 \/ c1) n = (Algebraic (cs0 ++ cs1), alts0 ++ alts1)- where- (Algebraic cs0, alts0) = c0 n- (Algebraic cs1, alts1) = c1 (n + 1)--cons0 :: a -> Series a-cons0 c n = (Algebraic [(n, [])], alts)- where- alts = [\_ -> c]--cons1 :: Serial a => (a -> b) -> Series b-cons1 c n = (Algebraic [(n, [fam0])], alts)- where- alts = [\(a0:_) -> c (convert alts0 a0)]- (fam0, alts0) = genSeries--cons2 :: (Serial a, Serial b) => (a -> b -> c) -> Series c-cons2 c n = (Algebraic [(n, [fam0, fam1])], alts)- where- alts = [\(a0:a1:_) -> c (convert alts0 a0) (convert alts1 a1)]- (fam0, alts0) = genSeries- (fam1, alts1) = genSeries--cons3 :: (Serial a, Serial b, Serial c) => (a -> b -> c -> d) -> Series d-cons3 c n = (Algebraic [(n, [fam0, fam1, fam2])], alts)- where- alts = [\(a0:a1:a2:_) -> c (convert alts0 a0)- (convert alts1 a1)- (convert alts2 a2)]- (fam0, alts0) = genSeries- (fam1, alts1) = genSeries- (fam2, alts2) = genSeries--cons4 :: (Serial a, Serial b, Serial c, Serial d) =>- (a -> b -> c -> d -> e) -> Series e-cons4 c n = (Algebraic [(n, [fam0, fam1, fam2, fam3])], alts)- where- alts = [\(a0:a1:a2:a3:_) -> c (convert alts0 a0)- (convert alts1 a1)- (convert alts2 a2)- (convert alts3 a3)]- (fam0, alts0) = genSeries- (fam1, alts1) = genSeries- (fam2, alts2) = genSeries- (fam3, alts3) = genSeries---cons5 :: (Serial a, Serial b, Serial c, Serial d, Serial e) =>- (a -> b -> c -> d -> e -> f) -> Series f-cons5 c n = (Algebraic [(n, [fam0, fam1, fam2, fam3, fam4])], alts)- where- alts = [\(a0:a1:a2:a3:a4:_) -> c (convert alts0 a0)- (convert alts1 a1)- (convert alts2 a2)- (convert alts3 a3)- (convert alts4 a4)]- (fam0, alts0) = genSeries- (fam1, alts1) = genSeries- (fam2, alts2) = genSeries- (fam3, alts3) = genSeries- (fam4, alts4) = genSeries----- Useful Serial instances--instance Serial Bool where- series = cons0 False \/ cons0 True--instance Serial a => Serial (Maybe a) where- series = cons0 Nothing \/ cons1 Just--instance (Serial a, Serial b) => Serial (Either a b) where- series = cons1 Left \/ cons1 Right--instance Serial a => Serial [a] where- series = cons0 [] \/ cons2 (:)--instance (Serial a, Serial b) => Serial (a, b) where- series = cons2 (,)--instance (Serial a, Serial b, Serial c) => Serial (a, b, c) where- series = cons3 (,,)--instance (Serial a, Serial b, Serial c, Serial d) => Serial (a, b, c, d) where- series = cons4 (,,,)--instance (Serial a, Serial b, Serial c, Serial d, Serial e) =>- Serial (a, b, c, d, e) where- series = cons5 (,,,,)---- Primitive Serial instances--instance Serial Int where- series _ = (fam, alts)- where- fam = Builtin (\d -> map (Prim . Int) [-d .. d])- alts = [\(Prim (Int i):_) -> i]--instance Serial Integer where- series _ = (fam, alts)- where- fam = Builtin (\d -> map (Prim . Integer . toInteger) [-d .. d])- alts = [\(Prim (Integer i):_) -> i]--instance Serial Char where- series _ = (fam, alts)- where- fam = Builtin (\d -> map (Prim . Char) (take (d+1) ['a'..'z']))- alts = [\(Prim (Char c):_) -> c]---- Refinement of partial values--uniquePrefix = "UP:"--lenUniquePrefix = length uniquePrefix--type Position = String--inst :: Int -> String -> (Int, [Family]) -> Value-inst d s (n, fs) = Ctr n (zipWith mkVar fs ['\NUL'..])- where- mkVar fam c = Var fam d (s++[c])--refine :: Position -> Value -> [Value]-refine [] (Var (Algebraic cs) d s) = map (inst (d-1) s) cs'- where- cs' = if d == 0 then filter (null . snd) cs else cs-refine [] (Var (Builtin f) d s) = f d-refine (p:ps) (Ctr n as) = map (Ctr n) (refineMany p ps as)--refineMany :: Char -> Position -> [Value] -> [[Value]]-refineMany p ps as = [(xs ++ a':ys) | a' <- refine ps a]- where- (xs, a:ys) = splitAt (fromEnum p) as---- Find total instantiations of a partial value, by iterative deepening--total :: Int -> Value -> [Value]-total d val = tot d val ++ total (d-1) val--tot :: Int -> Value -> [Value]-tot lim (Prim p) = [Prim p]-tot lim (Ctr n as) = [Ctr n as' | as' <- mapM (tot lim) as]-tot lim (Var fam d s)- | d < lim = []- | otherwise = case fam of- Builtin f -> f (d - lim)- Algebraic cs -> concatMap (tot lim . inst (d-1) s) cs---- General--False ==> _ = True-True ==> a = a---- Testable class machinery--data Info = Info { arguments :: [Value]- , showFuncs :: [Value -> String]- , apply :: ([Value] -> Bool)- }--newtype Property = Prop (Int -> Int -> Info)--eval :: Testable a => ([Value] -> a) -> Int -> Int -> Info-eval a = gen where Prop gen = property a--class Testable a where- property :: ([Value] -> a) -> Property--instance Testable Bool where- property apply = Prop $ \depth n -> Info [] [] (apply . reverse)--instance (Show a, Serial a, Testable b) => Testable (a -> b) where- property f =- Prop $ \depth n ->- let (fam, alts) = genSeries- initial = Var fam depth (uniquePrefix ++ [toEnum n])- val = convert alts initial- g (x:xs) = f xs (convert alts x)- info = eval g depth (n+1)- in info { arguments = initial : arguments info- , showFuncs = (show . convert alts) : showFuncs info- }---- Refute--refute :: Info -> IO Int-refute info = r (arguments info)- where- r args = do res <- try (evaluate (prop args))- case res of- Right True -> return 1- Right False -> stop args "Counter example found:"- Left (ErrorCall s)- | take (lenUniquePrefix) s == uniquePrefix ->- let (c:pos) = drop lenUniquePrefix s- in do ns <- mapM r (refineMany c pos args)- return (1 + sum ns)- Left e -> stop args $ "Property crashed on input:"-- prop = apply info- disp as = zipWith ($) (showFuncs info) as- stop args s = do putStrLn s- let args' = head [as | as <- mapM (total 0) args]- mapM putStrLn (disp args')- exitWith ExitSuccess--depthCheck :: Testable a => Int -> a -> IO ()-depthCheck d p =- do count <- refute info- putStrLn $ "Completed " ++ show count- ++ " tests without finding a counter example."- where- Prop f = property (const p)- info = f d 0
− source/LazySmallCheck/Generic.hs
@@ -1,144 +0,0 @@-{-# OPTIONS -fglasgow-exts #-} - -module LazySmallCheck.Generic - ( depthCheck -- :: (Data a, Show a) => Int -> (a -> Bool) -> IO [a] - , (==>) -- :: Bool -> Bool -> Bool - ) where - -import Data.Maybe -import Data.Generics -import Control.Exception -import Control.Monad -import System.Random -import System.Exit - -uniquePrefix = "UP:" - -lenUniquePrefix = length uniquePrefix - -type Position = String - -initPData :: a -initPData = error uniquePrefix - -data HLP a = HLP Int (Either a [a]) - -refinePData :: Data a => String -> Int -> Position -> a -> [a] -refinePData s d = r - where - depleft = d - (length s - lenUniquePrefix) - r :: Data a => Position -> a -> [a] - r [] x = - let dt = dataTypeOf x - in case dataTypeRep dt of - AlgRep cons -> - let cons = dataTypeConstrs dt - z x = (0, x) - k (i, g) = (i + 1, g (error $ s ++ [toEnum i])) - xs' = map (gunfold k z) cons - in if depleft > 0 - then map snd xs' - else mapMaybe (\(ncon, x') -> - if ncon == 0 - then Just x' - else Nothing) xs' - IntRep -> mkPrim dt (mkIntConstr dt . toInteger) - [-depleft .. depleft] - StringRep -> mkPrim dt (mkStringConstr dt . (:[])) - (take (depleft+1) ['a' .. 'z']) - _ -> error $ "LazySmallCheck.Generic: Can't generate type " - ++ dataTypeName dt - r (c:ps) x = - let p = fromEnum c - z y = HLP 0 (Left y) - k (HLP i (Left xs)) y | i == p = HLP (i + 1) (Right $ map xs (r ps y)) - k (HLP i (Left xs)) y = HLP (i + 1) (Left $ xs y) - k (HLP i (Right xss)) y = HLP (i + 1) (Right $ map (\xs -> xs y) xss) - HLP _ (Right x') = gfoldl k z x - in x' - -mkPrim dt mk vs = map (\i -> fromJust $ gunfold undefined Just $ mk i) vs - --- - -mapVars :: Data a => (forall b . Data b => b -> IO b) -> a -> IO a -mapVars f = gmapM (\x -> Control.Exception.catch - (mapVars f x) - (\exc -> case exc of - ErrorCall s | take (length uniquePrefix) s == uniquePrefix -> - f x - _ -> throw exc - ) - ) - --- Taken from Ralf Laemmel, SYB website --- Generate all terms of a given depth -enumerate :: Data a => Int -> [a] -enumerate 0 = [] -enumerate d = result - where - -- Getting hold of the result (type) - result = concat (map recurse cons') - - -- Find all terms headed by a specific Constr - recurse :: Data a => Constr -> [a] - recurse con = gmapM (\_ -> enumerate (d-1)) - (fromConstr con) - - -- We could also deal with primitive types easily. - -- Then we had to use cons' instead of cons. - -- - cons' :: [Constr] - cons' = case dataTypeRep ty of - AlgRep cons -> cons - IntRep -> map (mkIntConstr ty . toInteger) [-d .. d] - StringRep -> map (mkStringConstr ty . (:[])) (take d ['a'..'z']) - --FloatRep -> - where - ty = dataTypeOf (head result) - -smallValue :: Data a => a -smallValue = f 1 - where - f d = case enumerate d of - [] -> f (d + 1) - (x:_) -> x - -smallInstance :: Data a => a -> IO a -smallInstance = mapVars (\_ -> return smallValue) - --- - -refute :: (Show a, Data a) => Int -> (a -> Bool) -> IO Int -refute d p = r initPData - where - r x = do res <- try (evaluate (p x)) - case res of - Right True -> return 1 - Right False -> stop x "Counter example found:" - Left (ErrorCall s) - | take (lenUniquePrefix) s == uniquePrefix -> - let pos = drop lenUniquePrefix s - in do ns <- mapM r (refinePData s d pos x) - return (1 + sum ns) - Left e -> stop x "Property crashed on input:" - - stop x s = do putStrLn s - x' <- smallInstance x - putStrLn (show x') - exitWith ExitSuccess - --- - -depthCheck :: (Show a, Data a) => Int -> (a -> Bool) -> IO () -depthCheck d f = do count <- refute d f - putStrLn $ "Completed " ++ show count - ++ " tests without finding a counter example." - --- - -infixr 0 ==> - -(==>) :: Bool -> Bool -> Bool -False ==> a = True -True ==> a = a