1---------------------------------------------------------------------
2-- SmallCheck: another lightweight testing library.
3-- Colin Runciman, August 2006
4-- Version 0.2 (November 2006)
5--
6-- After QuickCheck, by Koen Claessen and John Hughes (2000-2004).
7---------------------------------------------------------------------
8
9module SmallCheck (
10  smallCheck, depthCheck,
11  Property, Testable,
12  forAll, forAllElem,
13  exists, existsDeeperBy, thereExists, thereExistsElem,
14  (==>),
15  Series, Serial(..),
16  (\/), (><), two, three, four,
17  cons0, cons1, cons2, cons3, cons4,
18  alts0, alts1, alts2, alts3, alts4,
19  N(..), Nat, Natural,
20  depth, inc, dec
21  ) where
22
23import Data.List (intersperse)
24import Control.Monad (when)
25import System.IO (stdout, hFlush)
26
27------------------ <Series of depth-bounded values> -----------------
28
29-- Series arguments should be interpreted as a depth bound (>=0)
30-- Series results should have finite length
31
32type Series a = Int -> [a]
33
34-- sum
35infixr 7 \/
36(\/) :: Series a -> Series a -> Series a
37s1 \/ s2 = \d -> s1 d ++ s2 d
38
39-- product
40infixr 8 ><
41(><) :: Series a -> Series b -> Series (a,b)
42s1 >< s2 = \d -> [(x,y) | x <- s1 d, y <- s2 d]
43
44------------------- <methods for type enumeration> ------------------
45
46-- enumerated data values should be finite and fully defined
47-- enumerated functional values should be total and strict
48
49-- bounds:
50-- for data values, the depth of nested constructor applications
51-- for functional values, both the depth of nested case analysis
52-- and the depth of results
53
54class Serial a where
55  series   :: Series a
56  coseries :: Serial b => Series (a->b)
57
58instance Serial () where
59  series   _ = [()]
60  coseries d = [ \() -> b
61               | b <- series d ]
62
63instance Serial Int where
64  series   d = [(-d)..d]
65  coseries d = [ \i -> if i > 0 then f (N (i - 1))
66                       else if i < 0 then g (N (abs i - 1))
67                       else z
68               | z <- alts0 d, f <- alts1 d, g <- alts1 d ]
69
70instance Serial Integer where
71  series   d = [ toInteger (i :: Int)
72               | i <- series d ]
73  coseries d = [ f . (fromInteger :: Integer->Int)
74               | f <- series d ]
75
76newtype N a = N a
77
78instance Show a => Show (N a) where
79  show (N i) = show i
80
81instance (Integral a, Serial a) => Serial (N a) where
82  series   d = map N [0..d']
83               where
84               d' = fromInteger (toInteger d)
85  coseries d = [ \(N i) -> if i > 0 then f (N (i - 1))
86                           else z
87               | z <- alts0 d, f <- alts1 d ]
88
89type Nat = N Int
90type Natural = N Integer
91
92instance Serial Float where
93  series d   = [ encodeFloat sig exp
94               | (sig,exp) <- series d,
95                 odd sig || sig==0 && exp==0 ]
96  coseries d = [ f . decodeFloat
97               | f <- series d ]
98
99instance Serial Double where
100  series   d = [ frac (x :: Float)
101               | x <- series d ]
102  coseries d = [ f . (frac :: Double->Float)
103               | f <- series d ]
104
105frac :: (Real a, Fractional a, Real b, Fractional b) => a -> b
106frac = fromRational . toRational
107
108instance Serial Char where
109  series d   = take (d+1) ['a'..'z']
110  coseries d = [ \c -> f (N (fromEnum c - fromEnum 'a'))
111               | f <- series d ]
112
113instance (Serial a, Serial b) =>
114         Serial (a,b) where
115  series   = series >< series
116  coseries = map uncurry . coseries
117
118instance (Serial a, Serial b, Serial c) =>
119         Serial (a,b,c) where
120  series   = \d -> [(a,b,c) | (a,(b,c)) <- series d]
121  coseries = map uncurry3 . coseries
122
123instance (Serial a, Serial b, Serial c, Serial d) =>
124         Serial (a,b,c,d) where
125  series   = \d -> [(a,b,c,d) | (a,(b,(c,d))) <- series d]
126  coseries = map uncurry4 . coseries
127
128uncurry3 :: (a->b->c->d) -> ((a,b,c)->d)
129uncurry3 f (x,y,z) = f x y z
130
131uncurry4 :: (a->b->c->d->e) -> ((a,b,c,d)->e)
132uncurry4 f (w,x,y,z) = f w x y z
133
134two   :: Series a -> Series (a,a)
135two   s = s >< s
136
137three :: Series a -> Series (a,a,a)
138three s = \d -> [(x,y,z) | (x,(y,z)) <- (s >< s >< s) d]
139
140four  :: Series a -> Series (a,a,a,a)
141four  s = \d -> [(w,x,y,z) | (w,(x,(y,z))) <- (s >< s >< s >< s) d]
142
143cons0 ::
144         a -> Series a
145cons0 c _ = [c]
146
147cons1 :: Serial a =>
148         (a->b) -> Series b
149cons1 c d = [c z | d > 0, z <- series (d-1)]
150
151cons2 :: (Serial a, Serial b) =>
152         (a->b->c) -> Series c
153cons2 c d = [c y z | d > 0, (y,z) <- series (d-1)]
154
155cons3 :: (Serial a, Serial b, Serial c) =>
156         (a->b->c->d) -> Series d
157cons3 c d = [c x y z | d > 0, (x,y,z) <- series (d-1)]
158
159cons4 :: (Serial a, Serial b, Serial c, Serial d) =>
160         (a->b->c->d->e) -> Series e
161cons4 c d = [c w x y z | d > 0, (w,x,y,z) <- series (d-1)]
162
163alts0 ::  Serial a =>
164            Series a
165alts0 d = series d
166
167alts1 ::  (Serial a, Serial b) =>
168            Series (a->b)
169alts1 d = if d > 0 then series (dec d)
170          else [\_ -> x | x <- series d]
171
172alts2 ::  (Serial a, Serial b, Serial c) =>
173            Series (a->b->c)
174alts2 d = if d > 0 then series (dec d)
175          else [\_ _ -> x | x <- series d]
176
177alts3 ::  (Serial a, Serial b, Serial c, Serial d) =>
178            Series (a->b->c->d)
179alts3 d = if d > 0 then series (dec d)
180          else [\_ _ _ -> x | x <- series d]
181
182alts4 ::  (Serial a, Serial b, Serial c, Serial d, Serial e) =>
183            Series (a->b->c->d->e)
184alts4 d = if d > 0 then series (dec d)
185          else [\_ _ _ _ -> x | x <- series d]
186
187instance Serial Bool where
188  series     = cons0 True \/ cons0 False
189  coseries d = [ \x -> if x then b1 else b2
190               | (b1,b2) <- series d ]
191
192instance Serial a => Serial (Maybe a) where
193  series     = cons0 Nothing \/ cons1 Just
194  coseries d = [ \m -> case m of
195                       Nothing -> z
196                       Just x  -> f x
197               |  z <- alts0 d ,
198                  f <- alts1 d ]
199
200instance (Serial a, Serial b) => Serial (Either a b) where
201  series     = cons1 Left \/ cons1 Right
202  coseries d = [ \e -> case e of
203                       Left x  -> f x
204                       Right y -> g y
205               |  f <- alts1 d ,
206                  g <- alts1 d ]
207
208instance Serial a => Serial [a] where
209  series     = cons0 [] \/ cons2 (:)
210  coseries d = [ \xs -> case xs of
211                        []      -> y
212                        (x:xs') -> f x xs'
213               |   y <- alts0 d ,
214                   f <- alts2 d ]
215
216-- Warning: the coseries instance here may generate duplicates.
217instance (Serial a, Serial b) => Serial (a->b) where
218  series = coseries
219  coseries d = [ \f -> g [f x | x <- series d]
220               | g <- series d ]
221
222-- For customising the depth measure.  Use with care!
223
224depth :: Int -> Int -> Int
225depth d d' | d >= 0    = d'+1-d
226           | otherwise = error "SmallCheck.depth: argument < 0"
227
228dec :: Int -> Int
229dec d | d > 0     = d-1
230      | otherwise = error "SmallCheck.dec: argument <= 0"
231
232inc :: Int -> Int
233inc d = d+1
234
235-- show the extension of a function (in part, bounded both by
236-- the number and depth of arguments)
237instance (Serial a, Show a, Show b) => Show (a->b) where
238  show f =
239    if maxarheight == 1
240    && sumarwidth + length ars * length "->;" < widthLimit then
241      "{"++(
242      concat $ intersperse ";" $ [a++"->"++r | (a,r) <- ars]
243      )++"}"
244    else
245      concat $ [a++"->\n"++indent r | (a,r) <- ars]
246    where
247    ars = take lengthLimit [ (show x, show (f x))
248                           | x <- series depthLimit ]
249    maxarheight = maximum  [ max (height a) (height r)
250                           | (a,r) <- ars ]
251    sumarwidth = sum       [ length a + length r
252                           | (a,r) <- ars]
253    indent = unlines . map ("  "++) . lines
254    height = length . lines
255    (widthLimit,lengthLimit,depthLimit) = (80,20,3)::(Int,Int,Int)
256
257---------------- <properties and their evaluation> ------------------
258
259-- adapted from QuickCheck originals: here results come in lists,
260-- properties have depth arguments, stamps (for classifying random
261-- tests) are omitted, existentials are introduced
262
263newtype PR = Prop [Result]
264
265data Result = Result {ok :: Maybe Bool, arguments :: [String]}
266
267nothing :: Result
268nothing = Result {ok = Nothing, arguments = []}
269
270result :: Result -> PR
271result res = Prop [res]
272
273newtype Property = Property (Int -> PR)
274
275class Testable a where
276  property :: a -> Int -> PR
277
278instance Testable Bool where
279  property b _ = Prop [Result (Just b) []]
280
281instance Testable PR where
282  property prop _ = prop
283
284instance (Serial a, Show a, Testable b) => Testable (a->b) where
285  property f = f' where Property f' = forAll series f
286
287instance Testable Property where
288  property (Property f) d = f d
289
290evaluate :: Testable a => a -> Series Result
291evaluate x d = rs where Prop rs = property x d
292
293forAll :: (Show a, Testable b) => Series a -> (a->b) -> Property
294forAll xs f = Property $ \d -> Prop $
295  [ r{arguments = show x : arguments r}
296  | x <- xs d, r <- evaluate (f x) d ]
297
298forAllElem :: (Show a, Testable b) => [a] -> (a->b) -> Property
299forAllElem xs = forAll (const xs)
300
301thereExists :: Testable b => Series a -> (a->b) -> Property
302thereExists xs f = Property $ \d -> Prop $
303  [ Result
304      ( Just $ or [ all pass (evaluate (f x) d)
305                  | x <- xs d ] )
306      [] ]
307  where
308  pass (Result Nothing _)  = True
309  pass (Result (Just b) _) = b
310
311thereExistsElem :: Testable b => [a] -> (a->b) -> Property
312thereExistsElem xs = thereExists (const xs)
313
314exists :: (Serial a, Testable b) =>
315            (a->b) -> Property
316exists = thereExists series
317
318existsDeeperBy :: (Serial a, Testable b) =>
319                    (Int->Int) -> (a->b) -> Property
320existsDeeperBy f = thereExists (series . f)
321
322infixr 0 ==>
323
324(==>) :: Testable a => Bool -> a -> Property
325True ==>  x = Property (property x)
326False ==> x = Property (const (result nothing))
327
328--------------------- <top-level test drivers> ----------------------
329
330-- similar in spirit to QuickCheck but with iterative deepening
331
332-- test for values of depths 0..d stopping when a property
333-- fails or when it has been checked for all these values
334smallCheck :: Testable a => Int -> a -> IO String
335smallCheck d = iterCheck 0 (Just d)
336
337depthCheck :: Testable a => Int -> a -> IO String
338depthCheck d = iterCheck d (Just d)
339
340iterCheck :: Testable a => Int -> Maybe Int -> a -> IO String
341iterCheck dFrom mdTo t = iter dFrom
342  where
343  iter :: Int -> IO String
344  iter d = do
345    let Prop results = property t d
346    (ok,s) <- check (mdTo==Nothing) 0 0 True results
347    maybe (iter (d+1))
348          (\dTo -> if ok && d < dTo
349                        then iter (d+1)
350                        else return s)
351          mdTo
352
353check :: Bool -> Int -> Int -> Bool -> [Result] -> IO (Bool, String)
354check i n x ok rs | null rs = do
355  let s = "  Completed "++show n++" test(s)"
356      y = if i then "." else " without failure."
357      z | x > 0     = "  But "++show x++" did not meet ==> condition."
358        | otherwise = ""
359  return (ok, s ++ y ++ z)
360
361check i n x ok (Result Nothing _ : rs) = do
362  progressReport i n x
363  check i (n+1) (x+1) ok rs
364
365check i n x f (Result (Just True) _ : rs) = do
366  progressReport i n x
367  check i (n+1) x f rs
368
369check i n x f (Result (Just False) args : rs) = do
370  let s = "  Failed test no. "++show (n+1)++". Test values follow."
371      s' = s ++ ": " ++ concat (intersperse ", " args)
372  if i then
373      check i (n+1) x False rs
374    else
375      return (False, s')
376
377progressReport :: Bool -> Int -> Int -> IO ()
378progressReport _ _ _ = return ()
379