lazysmallcheck 0.2 → 0.3
raw patch · 4 files changed
+61/−27 lines, 4 files
Files
- Test/LazySmallCheck.hs +43/−25
- examples/Mate.hs +1/−1
- examples/test/make.sh +15/−0
- lazysmallcheck.cabal +2/−1
Test/LazySmallCheck.hs view
@@ -7,6 +7,7 @@ , Cons -- :: * , cons -- :: a -> Series a , (><) -- :: Series (a -> b) -> Series a -> Series b+ , empty -- :: Series a , (\/) -- :: Series a -> Series a -> Series a , drawnFrom -- :: [a] -> Cons a , cons0 -- :: a -> Series a@@ -17,14 +18,16 @@ , cons5 -- :: ... , Testable -- :: class , depthCheck -- :: Testable a => Int -> a -> IO ()+ , smallCheck -- :: 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+ , Property -- :: *+ , lift -- :: Bool -> Property+ , neg -- :: Property -> Property+ , (*&*) -- :: Property -> Property -> Property+ , (*|*) -- :: Property -> Property -> Property+ , (*=>*) -- :: Property -> Property -> Property+ , (*=*) -- :: Property -> Property -> Property ) where @@ -54,13 +57,20 @@ cons :: a -> Series a cons a d = C (SumOfProd [[]]) [const a] +empty :: Series a+empty d = C (SumOfProd []) []+ (><) :: Series (a -> b) -> Series a -> Series b-(f >< a) d = C (SumOfProd [ta:p | d > 0, p <- ps]) cs+(f >< a) d = C (SumOfProd [ta:p | shallow, 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]+ cs = [\(x:xs) -> cf xs (conv cas x) | shallow, cf <- cfs]+ shallow = d > 0 && nonEmpty ta +nonEmpty :: Type -> Bool+nonEmpty (SumOfProd ps) = not (null ps)+ (\/) :: Series a -> Series a -> Series a (a \/ b) d = C (SumOfProd (ssa ++ ssb)) (ca ++ cb) where@@ -193,11 +203,9 @@ 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+ do putStrLn "Counter example found:"+ mapM_ putStrLn $ zipWith ($) (showArgs r)+ $ head [ys | ys <- mapM total xs] exitWith ExitSuccess sumMapM :: (a -> IO Int) -> Int -> [a] -> IO Int@@ -206,28 +214,35 @@ -- Properties with parallel conjunction (Lindblad TFP'07) -data Prop = Bool Bool | Neg Prop | And Prop Prop | ParAnd Prop Prop+data Property =+ Bool Bool+ | Neg Property+ | And Property Property+ | ParAnd Property Property+ | Eq Property Property -eval :: Prop -> (Bool -> IO a) -> (Pos -> IO a) -> IO a+eval :: Property -> (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+eval' (And p q) k u = eval p (\b-> if b then eval q k u else k b) u+eval' (Eq p q) k u = eval p (\b-> if b then eval q k u else eval (Neg q) k u) 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)+ unknown pos = eval q (\b-> if b then u pos else k b) (\_-> u pos) -lift :: Bool -> Prop+lift :: Bool -> Property lift b = Bool b -neg :: Prop -> Prop+neg :: Property -> Property neg p = Neg p -(*&*), (*|*), (*=>*) :: Prop -> Prop -> Prop+(*&*), (*|*), (*=>*) :: Property -> Property -> Property p *&* q = ParAnd p q p *|* q = neg (neg p *&* neg q) p *=>* q = neg (p *&* neg q)+p *=* q = Eq p q -- Boolean implication @@ -240,21 +255,21 @@ data Result = Result { args :: [Term] , showArgs :: [Term -> String]- , apply :: [Term] -> Prop+ , apply :: [Term] -> Property } -data Property = P (Int -> Int -> Result)+data P = 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+ property :: ([Term] -> a) -> P instance Testable Bool where property apply = P $ \n d -> Result [] [] (Bool . apply . reverse) -instance Testable Prop where+instance Testable Property where property apply = P $ \n d -> Result [] [] (apply . reverse) instance (Show a, Serial a, Testable b) => Testable (a -> b) where@@ -270,6 +285,9 @@ depthCheck d p = do n <- refute $ run (const p) 0 d putStrLn $ "OK, required " ++ show n ++ " tests at depth " ++ show d++smallCheck :: Testable a => Int -> a -> IO ()+smallCheck d p = mapM_ (`depthCheck` p) [0..d] test :: Testable a => a -> IO () test p = mapM_ (`depthCheck` p) [0..]
examples/Mate.hs view
@@ -1,6 +1,6 @@ module Mate where -import LazySmallCheck+import Test.LazySmallCheck import List data Kind = King | Queen | Rook | Bishop | Knight | Pawn
+ examples/test/make.sh view
@@ -0,0 +1,15 @@+ghc --make -O2 -i../ -i../../ TestCatch.hs+ghc --make -O2 -i../ -i../../ TestCountdown1.hs+ghc --make -O2 -i../ -i../../ TestCountdown2.hs+ghc --make -O2 -i../ -i../../ TestHuffman1.hs+ghc --make -O2 -i../ -i../../ TestHuffman2.hs+ghc --make -O2 -i../ -i../../ TestListSet1.hs+ghc --make -O2 -i../ -i../../ TestMate.hs+ghc --make -O2 -i../ -i../../ TestMux1.hs+ghc --make -O2 -i../ -i../../ TestMux2.hs+ghc --make -O2 -i../ -i../../ TestMux3.hs+ghc --make -O2 -i../ -i../../ TestRedBlack.hs+ghc --make -O2 -i../ -i../../ TestRegExp.hs+ghc --make -O2 -i../ -i../../ TestSad.hs+ghc --make -O2 -i../ -i../../ TestSumPuz.hs+ghc --make -O2 -i../ -i../../ TestTurner.hs
lazysmallcheck.cabal view
@@ -1,5 +1,5 @@ Name: lazysmallcheck-Version: 0.2+Version: 0.3 Maintainer: Matthew Naylor <mfn@cs.york.ac.uk> Homepage: http://www.cs.york.ac.uk/~mfn/lazysmallcheck/ Build-Depends: base, haskell98@@ -45,6 +45,7 @@ examples/test/TestMate.hs examples/test/TestTurner.hs examples/test/TestMux1.hs+ examples/test/make.sh Exposed-modules: Test.LazySmallCheck