lazysmallcheck (empty) → 0.1
raw patch · 13 files changed
+1036/−0 lines, 13 filesdep +basedep +haskell98dep +randomsetup-changed
Dependencies added: base, haskell98, random
Files
- LICENSE +30/−0
- Setup.hs +2/−0
- benchmarks/Benchmark.hs +35/−0
- benchmarks/Countdown.hs +187/−0
- benchmarks/List.hs +20/−0
- benchmarks/Mux.hs +33/−0
- benchmarks/RegExp.hs +124/−0
- benchmarks/Sad.hs +92/−0
- benchmarks/SumPuz.hs +68/−0
- benchmarks/clean.sh +5/−0
- lazysmallcheck.cabal +34/−0
- source/LazySmallCheck.hs +262/−0
- source/LazySmallCheck/Generic.hs +144/−0
+ LICENSE view
@@ -0,0 +1,30 @@+Copyright Matthew Naylor 2006-2007.+All rights reserved.++Redistribution and use in source and binary forms, with or without+modification, are permitted provided that the following conditions are+met:++ * Redistributions of source code must retain the above copyright+ notice, this list of conditions and the following disclaimer.++ * Redistributions in binary form must reproduce the above+ copyright notice, this list of conditions and the following+ disclaimer in the documentation and/or other materials provided+ with the distribution.++ * Neither the name of Neil Mitchell nor the names of other+ contributors may be used to endorse or promote products derived+ from this software without specific prior written permission.++THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT+OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+ Setup.hs view
@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain
+ benchmarks/Benchmark.hs view
@@ -0,0 +1,35 @@+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 view
@@ -0,0 +1,187 @@+-----------------------------------------------------------------------------+--+-- 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 view
@@ -0,0 +1,20 @@+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 view
@@ -0,0 +1,33 @@+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 view
@@ -0,0 +1,124 @@+(<==>) :: 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 view
@@ -0,0 +1,92 @@+-- 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 view
@@ -0,0 +1,68 @@+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 view
@@ -0,0 +1,5 @@+#!/bin/sh++rm -f *.hi *.o List Countdown *2.hs RegExp Mux SumPuz Sad+cd LazySmallCheck+rm -f *.hi *.o
+ lazysmallcheck.cabal view
@@ -0,0 +1,34 @@+Name: lazysmallcheck+Version: 0.1+Copyright: 2007, Matthew Naylor+Maintainer: mfn@cs.york.ac.uk+Homepage: http://www.cs.york.ac.uk/~mfn/lazysmallcheck/+Build-Depends: base, haskell98, random+Build-Type: Simple+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.+Category: Testing+Hs-Source-dirs:+ source+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+Exposed-modules:+ LazySmallCheck+ LazySmallCheck.Generic
+ source/LazySmallCheck.hs view
@@ -0,0 +1,262 @@+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 view
@@ -0,0 +1,144 @@+{-# 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