stream-fusion-0.1: tests/Test/SmallCheck/Partial.hs
{-# OPTIONS_GHC -fallow-incoherent-instances -fallow-undecidable-instances #-}
---------------------------------------------------------------------
-- SmallCheck: another lightweight testing library.
-- Colin Runciman, August 2006
-- Version 0.2 (November 2006)
--
-- After QuickCheck, by Koen Claessen and John Hughes (2000-2004).
---------------------------------------------------------------------
module Test.SmallCheck.Partial (
smallCheck, smallCheckI, depthCheck, test,
Property, Testable,
forAll, forAllElem,
exists, existsDeeperBy, thereExists, thereExistsElem,
(==>),
Series, Serial(..),
(\/), (><), two, three, four,
cons0, cons1, cons2, cons3, cons4,
alts0, alts1, alts2, alts3, alts4,
PositiveIntegral(..), Nat, Natural,
depth, inc, dec,
run, runTests, TestOptions(..)
) where
import List (intersperse)
import Monad (when)
import IO (stdout, hFlush)
import Foreign (unsafePerformIO) -- used only for Testable (IO a)
import qualified Test.ChasingBottoms as Bottoms
------------------ <Series of depth-bounded values> -----------------
-- Series arguments should be interpreted as a depth bound (>=0)
-- Series results should have finite length
type Series a = Int -> [a]
-- sum
infixr 7 \/
(\/) :: Series a -> Series a -> Series a
(s1 \/ s2) 0 = bottom : []
(s1 \/ s2) d = bottom : s1 (d-1) ++ s2 (d-1)
-- product
infixr 8 ><
(><) :: Series a -> Series b -> Series (a,b)
(s1 >< s2) 0 = bottom : []
(s1 >< s2) d = bottom : [(x,y) | x <- s1 (d-1), y <- s2 (d-1)]
------------------- <methods for type enumeration> ------------------
-- enumerated data values should be finite and fully defined
-- enumerated functional values should be total and strict
bottom :: a
bottom = error "_|_"
-- bounds:
-- for data values, the depth of nested constructor applications
-- for functional values, both the depth of nested case analysis
-- and the depth of results
class Serial a where
series :: Series a
coseries :: Serial b => Series (a->b)
instance Serial () where
series d = take (d+1) [bottom, ()]
coseries d = [ \() -> b
| b <- series d ]
instance Serial Int where
series d = seq 0
where seq n | n > d = []
seq n@0 = bottom : seq (n+1)
seq n@1 = 0 : seq (n+1)
seq n = -(n-1) : (n-1) : seq (n+1)
coseries d = [ \i -> if i > 0 then f (N (i - 1))
else if i < 0 then g (N (abs i - 1))
else z
| z <- alts0 d, f <- alts1 d, g <- alts1 d ]
instance Serial Integer where
series d = [ toInteger (i :: Int)
| i <- series d ]
coseries d = [ f . (fromInteger :: Integer->Int)
| f <- series d ]
newtype PositiveIntegral a = N a
instance Show a => Show (PositiveIntegral a) where
show (N i) = show i
instance (Integral a, Serial a) => Serial (PositiveIntegral a) where
series d = map N [0..d']
where
d' = fromInteger (toInteger d)
coseries d = [ \(N i) -> if i > 0 then f (N (i - 1))
else z
| z <- alts0 d, f <- alts1 d ]
type Nat = PositiveIntegral Int
type Natural = PositiveIntegral Integer
instance Serial Float where
series d = [ encodeFloat sig exp
| (sig,exp) <- series d,
odd sig || sig==0 && exp==0 ]
coseries d = [ f . decodeFloat
| f <- series d ]
instance Serial Double where
series d = [ frac (x :: Float)
| x <- series d ]
coseries d = [ f . (frac :: Double->Float)
| f <- series d ]
frac :: (Real a, Fractional a, Real b, Fractional b) => a -> b
frac = fromRational . toRational
instance Serial Char where
series d = take (d+1) " \nab\0cd,ef"
coseries d = [ \c -> f (N (fromEnum c - fromEnum 'a'))
| f <- series d ]
instance (Serial a, Serial b) =>
Serial (a,b) where
series = series >< series
coseries = map uncurry . coseries
instance (Serial a, Serial b, Serial c) =>
Serial (a,b,c) where
series = \d -> bottom
: [ (x,y,z)
| x <- series (d-1)
, y <- series (d-1)
, z <- series (d-1)]
coseries = map uncurry3 . coseries
instance (Serial a, Serial b, Serial c, Serial d) =>
Serial (a,b,c,d) where
series = \d -> bottom
: [ (x,y,z,a)
| x <- series (d-1)
, y <- series (d-1)
, z <- series (d-1)
, a <- series (d-1)]
coseries = map uncurry4 . coseries
uncurry3 :: (a->b->c->d) -> ((a,b,c)->d)
uncurry3 f (x,y,z) = f x y z
uncurry4 :: (a->b->c->d->e) -> ((a,b,c,d)->e)
uncurry4 f (w,x,y,z) = f w x y z
two :: Series a -> Series (a,a)
two s = s >< s
three :: Series a -> Series (a,a,a)
three s = \d -> [(x,y,z) | (x,(y,z)) <- (s >< s >< s) d]
four :: Series a -> Series (a,a,a,a)
four s = \d -> [(w,x,y,z) | (w,(x,(y,z))) <- (s >< s >< s >< s) d]
cons0 ::
a -> Series a
cons0 c _ = [c]
cons1 :: Serial a =>
(a->b) -> Series b
cons1 c d = [c z | d > 0, z <- series (d-1)]
cons2 :: (Serial a, Serial b) =>
(a->b->c) -> Series c
cons2 c d = [c y z | d > 0, y <- series (d-1), z <- series (d-1)]
cons3 :: (Serial a, Serial b, Serial c) =>
(a->b->c->d) -> Series d
cons3 c d = [c x y z | d > 0, (x,y,z) <- series (d-1)]
cons4 :: (Serial a, Serial b, Serial c, Serial d) =>
(a->b->c->d->e) -> Series e
cons4 c d = [c w x y z | d > 0, (w,x,y,z) <- series (d-1)]
alts0 :: Serial a =>
Series a
alts0 d = series d
alts1 :: (Serial a, Serial b) =>
Series (a->b)
alts1 d = if d > 0 then series (dec d)
else [\_ -> x | x <- series d]
alts2 :: (Serial a, Serial b, Serial c) =>
Series (a->b->c)
alts2 d = if d > 0 then series (dec d)
else [\_ _ -> x | x <- series d]
alts3 :: (Serial a, Serial b, Serial c, Serial d) =>
Series (a->b->c->d)
alts3 d = if d > 0 then series (dec d)
else [\_ _ _ -> x | x <- series d]
alts4 :: (Serial a, Serial b, Serial c, Serial d, Serial e) =>
Series (a->b->c->d->e)
alts4 d = if d > 0 then series (dec d)
else [\_ _ _ _ -> x | x <- series d]
instance Serial Bool where
series = cons0 False \/ cons0 True
coseries d = [ \x -> if x then b1 else b2
| b1 <- series d, b2 <- series d ]
instance Serial Ordering where
series = cons0 EQ \/ cons0 LT \/ cons0 GT
coseries d = [ \m -> case m of
LT -> x
EQ -> y
GT -> z
| x <- alts0 d ,
y <- alts0 d ,
z <- alts0 d ]
instance Serial a => Serial (Maybe a) where
series = cons0 Nothing \/ cons1 Just
coseries d = [ \m -> case m of
Nothing -> z
Just x -> f x
| z <- alts0 d ,
f <- alts1 d ]
instance (Serial a, Serial b) => Serial (Either a b) where
series = cons1 Left \/ cons1 Right
coseries d = [ \e -> case e of
Left x -> f x
Right y -> g y
| f <- alts1 d ,
g <- alts1 d ]
instance Serial a => Serial [a] where
series = cons0 [] \/ cons2 (:)
coseries d = [ \xs -> case xs of
[] -> y
(x:xs') -> f x xs'
| y <- alts0 d ,
f <- alts2 d ]
-- Warning: the coseries instance here may generate duplicates.
instance (Serial a, Serial b) => Serial (a->b) where
series 0 = bottom : []
series (d+1) = bottom : [ \_ -> x | x <- series d ] ++ tail (coseries d)
coseries d = [ \f -> g [f x | x <- series d]
| g <- series d ]
-- For customising the depth measure. Use with care!
depth :: Int -> Int -> Int
depth d d' | d >= 0 = d'+1-d
| otherwise = error "SmallCheck.depth: argument < 0"
dec :: Int -> Int
dec d | d > 0 = d-1
| otherwise = error "SmallCheck.dec: argument <= 0"
inc :: Int -> Int
inc d = d+1
{-
-- show the extension of a function (in part, bounded both by
-- the number and depth of arguments)
instance (Serial a, Show a, Show b) => Show (a->b) where
show f =
if maxarheight == 1
&& sumarwidth + length ars * length "->;" < widthLimit then
"{"++(
concat $ intersperse ";" $ [a++"->"++r | (a,r) <- ars]
)++"}"
else
concat $ [a++"->\n"++indent r | (a,r) <- ars]
where
ars = take lengthLimit [ (show x, show (f x))
| x <- series depthLimit ]
maxarheight = maximum [ max (height a) (height r)
| (a,r) <- ars ]
sumarwidth = sum [ length a + length r
| (a,r) <- ars]
indent = unlines . map (" "++) . lines
height = length . lines
(widthLimit,lengthLimit,depthLimit) = (80,20,3)::(Int,Int,Int)
-}
instance (Serial a, Bottoms.ApproxShow a, Bottoms.ApproxShow b) => Show (a->b) where
show f
| Bottoms.isBottom f = "_|_"
| otherwise =
if maxarheight == 1
&& sumarwidth + length ars * length "->;" < widthLimit then
"{"++(
concat $ intersperse ";" $ [a++"->"++r | (a,r) <- ars]
)++"}"
else
concat $ [a++"->\n"++indent r | (a,r) <- ars]
where
ars = take lengthLimit [ (Bottoms.approxShow 1000 x, Bottoms.approxShow 1000 (f x))
| x <- series depthLimit ]
maxarheight = maximum [ max (height a) (height r)
| (a,r) <- ars ]
sumarwidth = sum [ length a + length r
| (a,r) <- ars]
indent = unlines . map (" "++) . lines
height = length . lines
(widthLimit,lengthLimit,depthLimit) = (80,20,3)::(Int,Int,Int)
---------------- <properties and their evaluation> ------------------
-- adapted from QuickCheck originals: here results come in lists,
-- properties have depth arguments, stamps (for classifying random
-- tests) are omitted, existentials are introduced
newtype PR = Prop [Result]
data Result = Result {ok :: Maybe Bool, arguments :: [String]}
nothing :: Result
nothing = Result {ok = Nothing, arguments = []}
result :: Result -> PR
result res = Prop [res]
newtype Property = Property (Int -> PR)
class Testable a where
property :: a -> Int -> PR
instance Testable Bool where
property b _ = Prop [Result (Just b) []]
instance Testable PR where
property prop _ = prop
instance (Serial a, Bottoms.ApproxShow a, Testable b) => Testable (a->b) where
property f = f' where Property f' = forAll series f
instance Testable Property where
property (Property f) d = f d
-- For testing properties involving IO. Unsafe, so use with care!
instance Testable a => Testable (IO a) where
property = property . unsafePerformIO
evaluate :: Testable a => a -> Series Result
evaluate x d = rs where Prop rs = property x d
forAll :: (Bottoms.ApproxShow a, Testable b) => Series a -> (a->b) -> Property
forAll xs f = Property $ \d -> Prop $
[ r{arguments = Bottoms.approxShow 1000 x : arguments r}
| x <- xs d, r <- evaluate (f x) d ]
forAllElem :: (Bottoms.ApproxShow a, Testable b) => [a] -> (a->b) -> Property
forAllElem xs = forAll (const xs)
thereExists :: Testable b => Series a -> (a->b) -> Property
thereExists xs f = Property $ \d -> Prop $
[ Result
( Just $ or [ all pass (evaluate (f x) d)
| x <- xs d ] )
[] ]
where
pass (Result Nothing _) = True
pass (Result (Just b) _) = b
thereExistsElem :: Testable b => [a] -> (a->b) -> Property
thereExistsElem xs = thereExists (const xs)
exists :: (Serial a, Testable b) =>
(a->b) -> Property
exists = thereExists series
existsDeeperBy :: (Serial a, Testable b) =>
(Int->Int) -> (a->b) -> Property
existsDeeperBy f = thereExists (series . f)
infixr 0 ==>
(==>) :: Testable a => Bool -> a -> Property
True ==> x = Property (property x)
False ==> x = Property (const (result nothing))
--------------------- <top-level test drivers> ----------------------
-- similar in spirit to QuickCheck but with iterative deepening
test :: Testable a => a -> IO ()
test = smallCheckI
-- test for values of depths 0..d stopping when a property
-- fails or when it has been checked for all these values
smallCheck :: Testable a => Int -> a -> IO ()
smallCheck d = iterCheck 0 (Just d)
-- interactive variant, asking the user whether testing should
-- continue/go deeper after a failure/completed iteration
smallCheckI :: Testable a => a -> IO ()
smallCheckI = iterCheck 0 Nothing
depthCheck :: Testable a => Int -> a -> IO ()
depthCheck d = iterCheck d (Just d)
iterCheck :: Testable a => Int -> Maybe Int -> a -> IO ()
iterCheck dFrom mdTo t = iter dFrom
where
iter d = do
putStrLn ("Depth "++show d++":")
let Prop results = property t d
ok <- check (mdTo==Nothing) 0 0 True results
maybe (whenUserWishes " Deeper" () $ iter (d+1))
(\dTo -> when (ok && d < dTo) $ iter (d+1))
mdTo
check :: Bool -> Int -> Int -> Bool -> [Result] -> IO Bool
check i n x ok rs | null rs = do
putStr (" Completed "++show n++" test(s)")
putStrLn (if ok then " without failure." else ".")
when (x > 0) $
putStrLn (" But "++show x++" did not meet ==> condition.")
return ok
check i n x ok (Result Nothing _ : rs) = do
progressReport i n x
check i (n+1) (x+1) ok rs
check i n x f (Result (Just True) _ : rs) = do
progressReport i n x
check i (n+1) x f rs
check i n x f (Result (Just False) args : rs) = do
putStrLn (" Failed test no. "++show (n+1)++". Test values follow.")
mapM_ (putStrLn . (" "++)) args
( if i then
whenUserWishes " Continue" False $ check i (n+1) x False rs
else
return False )
whenUserWishes :: String -> a -> IO a -> IO a
whenUserWishes wish x action = do
putStr (wish++"? ")
hFlush stdout
reply <- getLine
( if (null reply || reply=="y") then action
else return x )
progressReport :: Bool -> Int -> Int -> IO ()
progressReport i n x | n >= x = do
when i $ ( putStr (n' ++ replicate (length n') '\b') >>
hFlush stdout )
where
n' = show n
run :: Testable a => a -> Property
run p = Property (property p)
data TestResult = TestOk Int
| TestExhausted Int
| TestFailed Int [String]
data TestOptions = TestOptions {
testDepth :: Int,
maxTests :: Int
}
runTest :: TestOptions -> Property -> TestResult
runTest TestOptions { testDepth = depth, maxTests = max } p =
let Prop results = property p depth
in check 0 results
where check n _ | n >= max = TestExhausted n
check n [] = TestOk n
check n (Result Nothing _ : rs) = check (n+1) rs
check n (Result (Just True ) _ : rs) = check (n+1) rs
check n (Result (Just False) args : rs) = TestFailed n args
runTests :: String -> TestOptions -> [Property] -> IO ()
runTests name opts props =
do putStr (rjustify 25 name ++ " : ")
failures <- tr 1 props [] 0
mapM fa (reverse failures)
return ()
where
rjustify n s = replicate (max 0 (n - length s)) ' ' ++ s
tr n [] xs c = do
putStr (rjustify (max 0 (35-n)) " (" ++ show c ++ ")\n")
return xs
tr n (prop:props) failures c =
case runTest opts prop of
TestOk m
-> do { putStr "." ;
tr (n+1) props failures (c+m) }
TestExhausted m
-> do { putStr "?" ;
tr (n+1) props failures (c+m) }
TestFailed m args
-> do { putStr "#" ;
tr (n+1) props ((args,n,m):failures) c }
fa :: ([String],Int,Int) -> IO ()
fa (f,n,m) =
do putStr "\n"
putStr (" ** test "
++ show (n :: Int)
++ " of "
++ name
++ " failed (after " ++ show m ++ " steps) with the binding(s)\n")
sequence_ [putStr (" ** " ++ v ++ "\n")
| v <- f ]
putStr "\n"
------------------------------------------------------------------------
--
-- foldl'
-- lines too strict
-- structure of domain, insert bottoms in correct position.
--