lazy-smallcheck-2012: 28ba7719fb98595f32a6e59526456e3cd870264a
1: {-# OPTIONS_GHC -XMultiParamTypeClasses #-}
2:
3: -- Lazy SmallCheck (type-class variant, largely a SmallCheck subset)
4: -- Lindblad, Naylor and Runciman
5:
6: module LazySmallCheck
7: ( Serial(series) -- :: class
8: , Series -- :: type Series a = Int -> Cons a
9: , Cons -- :: *
10: , cons -- :: a -> Series a
11: , (><) -- :: Series (a -> b) -> Series a -> Series b
12: , empty -- :: Series a
13: , (\/) -- :: Series a -> Series a -> Series a
14: , drawnFrom -- :: [a] -> Cons a
15: , cons0 -- :: a -> Series a
16: , cons1 -- :: Serial a => (a -> b) -> Series b
17: , cons2 -- :: (Serial a, Serial b) => (a -> b -> c) -> Series c
18: , cons3 -- :: ...
19: , cons4 -- :: ...
20: , cons5 -- :: ...
21: , Testable -- :: class
22: , depthCheck -- :: Testable a => Int -> a -> IO ()
23: , sat -- :: Testable a => Int -> a -> IO ()
24: , smallCheck -- :: Testable a => Int -> a -> IO ()
25: , test -- :: Testable a => a -> IO ()
26: , (==>) -- :: Bool -> Bool -> Bool
27: , Property -- :: *
28: , lift -- :: Bool -> Property
29: , true -- :: Property
30: , false -- :: Property
31: , neg -- :: Property -> Property
32: , Logical(..) -- :: class
33: , Seq(..) -- :: data Seq a = Seq [a]
34: , Seq1(..) -- :: data Seq1 a = Seq1 [a]
35: , Nat(..) -- :: data Nat = N Int
36: )
37: where
38:
39: import Control.Monad hiding ((>=>))
40: import Control.Exception
41: import System.Exit
42:
43: infixr 0 ==>, >=>
44: infixr 3 \/, <|>
45: infixl 4 ><, <&>, |&|
46:
47: type Pos = [Int]
48:
49: data Term = Var Pos Type | Ctr Int [Term]
50:
51: data Type = SumOfProd [[Type]]
52:
53: type Series a = Int -> Cons a
54:
55: data Cons a = C Type ([[Term] -> a])
56:
57: class Serial a where
58: series :: Series a
59:
60: -- Series constructors
61:
62: cons :: a -> Series a
63: cons a d = C (SumOfProd [[]]) [const a]
64:
65: empty :: Series a
66: empty d = C (SumOfProd []) []
67:
68: (><) :: Series (a -> b) -> Series a -> Series b
69: (f >< a) d = C (SumOfProd [ta:p | shallow, p <- ps]) cs
70: where
71: C (SumOfProd ps) cfs = f d
72: C ta cas = a (d-1)
73: cs = [\(x:xs) -> cf xs (conv cas x) | shallow, cf <- cfs]
74: shallow = d > 0 && nonEmpty ta
75:
76: nonEmpty :: Type -> Bool
77: nonEmpty (SumOfProd ps) = not (null ps)
78:
79: (\/) :: Series a -> Series a -> Series a
80: (a \/ b) d = C (SumOfProd (ssa ++ ssb)) (ca ++ cb)
81: where
82: C (SumOfProd ssa) ca = a d
83: C (SumOfProd ssb) cb = b d
84:
85: conv :: [[Term] -> a] -> Term -> a
86: conv cs (Var p _) = error ('\0':map toEnum p)
87: conv cs (Ctr i xs) = (cs !! i) xs
88:
89: drawnFrom :: [a] -> Cons a
90: drawnFrom xs = C (SumOfProd (map (const []) xs)) (map const xs)
91:
92: -- Helpers, a la SmallCheck
93:
94: cons0 :: a -> Series a
95: cons0 f = cons f
96:
97: cons1 :: Serial a => (a -> b) -> Series b
98: cons1 f = cons f >< series
99:
100: cons2 :: (Serial a, Serial b) => (a -> b -> c) -> Series c
101: cons2 f = cons f >< series >< series
102:
103: cons3 :: (Serial a, Serial b, Serial c) => (a -> b -> c -> d) -> Series d
104: cons3 f = cons f >< series >< series >< series
105:
106: cons4 :: (Serial a, Serial b, Serial c, Serial d) =>
107: (a -> b -> c -> d -> e) -> Series e
108: cons4 f = cons f >< series >< series >< series >< series
109:
110: cons5 :: (Serial a, Serial b, Serial c, Serial d, Serial e) =>
111: (a -> b -> c -> d -> e -> f) -> Series f
112: cons5 f = cons f >< series >< series >< series >< series >< series
113:
114: -- Standard instances
115:
116: instance Serial () where
117: series = cons0 ()
118:
119: instance Serial Bool where
120: series = cons0 False \/ cons0 True
121:
122: instance Serial a => Serial (Maybe a) where
123: series = cons0 Nothing \/ cons1 Just
124:
125: instance (Serial a, Serial b) => Serial (Either a b) where
126: series = cons1 Left \/ cons1 Right
127:
128: instance Serial a => Serial [a] where
129: series = cons0 [] \/ cons2 (:)
130:
131: instance (Serial a, Serial b) => Serial (a, b) where
132: series = cons2 (,) . (+1)
133:
134: instance (Serial a, Serial b, Serial c) => Serial (a, b, c) where
135: series = cons3 (,,) . (+1)
136:
137: instance (Serial a, Serial b, Serial c, Serial d) =>
138: Serial (a, b, c, d) where
139: series = cons4 (,,,) . (+1)
140:
141: instance (Serial a, Serial b, Serial c, Serial d, Serial e) =>
142: Serial (a, b, c, d, e) where
143: series = cons5 (,,,,) . (+1)
144:
145: instance Serial Int where
146: series d = drawnFrom [-d..d]
147:
148: instance Serial Integer where
149: series d = drawnFrom (map toInteger [-d..d])
150:
151: instance Serial Char where
152: series d = drawnFrom (take (d+1) ['a'..])
153:
154: instance Serial Float where
155: series d = drawnFrom (floats d)
156:
157: instance Serial Double where
158: series d = drawnFrom (floats d)
159:
160: floats :: RealFloat a => Int -> [a]
161: floats d = [ encodeFloat sig exp
162: | sig <- map toInteger [-d..d]
163: , exp <- [-d..d]
164: , odd sig || sig == 0 && exp == 0
165: ]
166:
167: newtype Nat = N Int
168:
169: instance Serial Nat where
170: series d = drawnFrom $ map N [0..d]
171:
172: instance Show Nat where
173: show (N n) = show n
174:
175: -- Sequences (each list element is generated at same depth)
176:
177: newtype Seq a = Seq [a] deriving (Ord,Eq)
178:
179: instance Show a => Show (Seq a) where
180: show (Seq xs) = show xs
181:
182: instance Serial a => Serial (Seq a) where
183: series = (cons Seq >< children) . (+1)
184:
185: children d = list d
186: where
187: list = cons []
188: \/ cons (:) >< const (series (d-1)) >< list
189:
190: newtype Seq1 a = Seq1 [a] deriving (Ord,Eq)
191:
192: instance Show a => Show (Seq1 a) where
193: show (Seq1 xs) = show xs
194:
195: instance Serial a => Serial (Seq1 a) where
196: series = (cons Seq1 >< children1) . (+1)
197:
198: children1 d = (cons (:) >< elem >< list) d
199: where
200: elem = const (series (d-1))
201: list = cons []
202: \/ cons (:) >< elem >< list
203:
204: -- Term refinement
205:
206: refine :: Term -> Pos -> [Term]
207: refine (Var p (SumOfProd ss)) [] = new p ss
208: refine (Ctr c xs) p = map (Ctr c) (refineList xs p)
209:
210: refineList :: [Term] -> Pos -> [[Term]]
211: refineList xs (i:is) = [ls ++ y:rs | y <- refine x is]
212: where (ls, x:rs) = splitAt i xs
213:
214: new :: Pos -> [[Type]] -> [Term]
215: new p ps = [ Ctr c (zipWith (\i t -> Var (p++[i]) t) [0..] ts)
216: | (c, ts) <- zip [0..] ps ]
217:
218: -- Find total instantiations of a partial value
219:
220: total :: Term -> [Term]
221: total val = tot val
222: where
223: tot (Ctr c xs) = [Ctr c ys | ys <- mapM tot xs]
224: tot (Var p (SumOfProd ss)) = [y | x <- new p ss, y <- tot x]
225:
226: -- Answers
227:
228: answer :: a -> (a -> IO b) -> (Pos -> IO b) -> IO b
229: answer a known unknown =
230: do res <- try (evaluate a)
231: case res of
232: Right b -> known b
233: Left (ErrorCall ('\0':p)) -> unknown (map fromEnum p)
234: Left e -> throw e
235:
236: -- Refute
237:
238: refute :: Bool -> Result -> IO Int
239: refute sat r = ref (args r)
240: where
241: ref xs = eval (apply r xs) known unknown
242: where
243: known True = if sat then display >> return 1 else return 1
244: known False
245: | sat = return 0
246: | otherwise =
247: do putStrLn "Counter example found:"
248: display
249: exitWith ExitSuccess
250:
251: unknown p = sumMapM ref (if sat then 0 else 1) (refineList xs p)
252:
253: display =
254: mapM_ putStrLn $ zipWith ($) (showArgs r)
255: $ head [ys | ys <- mapM total xs]
256:
257: sumMapM :: (a -> IO Int) -> Int -> [a] -> IO Int
258: sumMapM f n [] = return n
259: sumMapM f n (a:as) = seq n (do m <- f a ; sumMapM f (n+m) as)
260:
261: -- Properties with parallel conjunction (Lindblad TFP'07)
262:
263: data Property =
264: Bool Bool
265: | Neg Property
266: | And Property Property
267: | Or Property Property
268: | Implies Property Property
269: | ParAnd Property Property
270:
271: eval :: Property -> (Bool -> IO a) -> (Pos -> IO a) -> IO a
272: eval p k u = answer p (\p -> eval' p k u) u
273:
274: eval' (Bool b) k u = answer b k u
275: eval' (Neg p) k u = eval p (k . not) u
276: eval' (And p q) k u = eval p (\b -> if b then eval q k u else k b) u
277: eval' (Or p q) k u = eval p (\b -> if b then k b else eval q k u) u
278: eval' (Implies p q) k u = eval p (\b -> if b then eval q k u else k True) u
279: eval' (ParAnd p q) k u = eval p (\b -> if b then eval q k u else k b) unknown
280: where unknown pos = eval q (\b-> if b then u pos else k b) (\_-> u pos)
281:
282: lift :: Bool -> Property
283: lift b = Bool b
284:
285: true :: Property
286: true = lift True
287:
288: false :: Property
289: false = lift False
290:
291: neg :: Property -> Property
292: neg p = Neg p
293:
294: class Logical a b where
295: (|&|) :: a -> b -> Property -- Parallel and
296: (<&>) :: a -> b -> Property -- Sequential and
297: (<|>) :: a -> b -> Property -- Sequential or
298: (>=>) :: a -> b -> Property -- Sequential implies
299:
300: instance Logical Bool Bool where
301: p |&| q = ParAnd (lift p) (lift q)
302: p <&> q = And (lift p) (lift q)
303: p <|> q = Or (lift p) (lift q)
304: p >=> q = Implies (lift p) (lift q)
305:
306: instance Logical Bool Property where
307: p |&| q = ParAnd (lift p) q
308: p <&> q = And (lift p) q
309: p <|> q = Or (lift p) q
310: p >=> q = Implies (lift p) q
311:
312: instance Logical Property Bool where
313: p |&| q = ParAnd p (lift q)
314: p <&> q = And p (lift q)
315: p <|> q = Or p (lift q)
316: p >=> q = Implies p (lift q)
317:
318: instance Logical Property Property where
319: p |&| q = ParAnd p q
320: p <&> q = And p q
321: p <|> q = Or p q
322: p >=> q = Implies p q
323:
324: -- Boolean implication
325:
326: (==>) :: Bool -> Bool -> Bool
327: False ==> _ = True
328: True ==> x = x
329:
330: -- Testable
331:
332: data Result =
333: Result { args :: [Term]
334: , showArgs :: [Term -> String]
335: , apply :: [Term] -> Property
336: }
337:
338: data P = P (Int -> Int -> Result)
339:
340: run :: Testable a => ([Term] -> a) -> Int -> Int -> Result
341: run a = f where P f = property a
342:
343: class Testable a where
344: property :: ([Term] -> a) -> P
345:
346: instance Testable Bool where
347: property apply = P $ \n d -> Result [] [] (Bool . apply . reverse)
348:
349: instance Testable Property where
350: property apply = P $ \n d -> Result [] [] (apply . reverse)
351:
352: instance (Show a, Serial a, Testable b) => Testable (a -> b) where
353: property f = P $ \n d ->
354: let C t c = series d
355: c' = conv c
356: r = run (\(x:xs) -> f xs (c' x)) (n+1) d
357: in r { args = Var [n] t : args r, showArgs = (show . c') : showArgs r }
358:
359: -- Top-level interface
360:
361: depthCheck :: Testable a => Int -> a -> IO ()
362: depthCheck d p =
363: do n <- refute False $ run (const p) 0 d
364: putStrLn $ "OK, required " ++ show n ++ " tests at depth " ++ show d
365:
366: sat :: Testable a => Int -> a -> IO ()
367: sat d p =
368: do n <- refute True $ run (const p) 0 d
369: putStrLn $ "Generated " ++ show n ++ " inputs at depth " ++ show d
370:
371: smallCheck :: Testable a => Int -> a -> IO ()
372: smallCheck d p = mapM_ (`depthCheck` p) [0..d]
373:
374: test :: Testable a => a -> IO ()
375: test p = mapM_ (`depthCheck` p) [0..]
Generated by git2html.