lazysmallcheck-0.1: source/LazySmallCheck.hs
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