module Test.LazySmallCheck
( Serial(series)
, Series
, Cons
, cons
, (><)
, empty
, (\/)
, drawnFrom
, cons0
, cons1
, cons2
, cons3
, cons4
, cons5
, Testable
, depthCheck
, smallCheck
, test
, (==>)
, Property
, lift
, neg
, (*&*)
, (*|*)
, (*=>*)
, (*=*)
)
where
import Control.Monad
import Control.Exception
import System.Exit
infixr 0 ==>, *=>*
infixr 3 \/, *|*
infixl 4 ><, *&*
type Pos = [Int]
data Term = Var Pos Type | Ctr Int [Term]
data Type = SumOfProd [[Type]]
type Series a = Int -> Cons a
data Cons a = C Type ([[Term] -> a])
class Serial a where
series :: Series a
cons :: a -> Series a
cons :: forall a. a -> Series a
cons a
a Int
d = forall a. Type -> [[Term] -> a] -> Cons a
C ([[Type]] -> Type
SumOfProd [[]]) [forall a b. a -> b -> a
const a
a]
empty :: Series a
empty :: forall a. Series a
empty Int
d = forall a. Type -> [[Term] -> a] -> Cons a
C ([[Type]] -> Type
SumOfProd []) []
(><) :: Series (a -> b) -> Series a -> Series b
(Series (a -> b)
f >< :: forall a b. Series (a -> b) -> Series a -> Series b
>< Series a
a) Int
d = forall a. Type -> [[Term] -> a] -> Cons a
C ([[Type]] -> Type
SumOfProd [Type
taforall a. a -> [a] -> [a]
:[Type]
p | Bool
shallow, [Type]
p <- [[Type]]
ps]) [[Term] -> b]
cs
where
C (SumOfProd [[Type]]
ps) [[Term] -> a -> b]
cfs = Series (a -> b)
f Int
d
C Type
ta [[Term] -> a]
cas = Series a
a (Int
dforall a. Num a => a -> a -> a
-Int
1)
cs :: [[Term] -> b]
cs = [\(Term
x:[Term]
xs) -> [Term] -> a -> b
cf [Term]
xs (forall a. [[Term] -> a] -> Term -> a
conv [[Term] -> a]
cas Term
x) | Bool
shallow, [Term] -> a -> b
cf <- [[Term] -> a -> b]
cfs]
shallow :: Bool
shallow = Int
d forall a. Ord a => a -> a -> Bool
> Int
0 Bool -> Bool -> Bool
&& Type -> Bool
nonEmpty Type
ta
nonEmpty :: Type -> Bool
nonEmpty :: Type -> Bool
nonEmpty (SumOfProd [[Type]]
ps) = Bool -> Bool
not (forall (t :: * -> *) a. Foldable t => t a -> Bool
null [[Type]]
ps)
(\/) :: Series a -> Series a -> Series a
(Series a
a \/ :: forall a. Series a -> Series a -> Series a
\/ Series a
b) Int
d = forall a. Type -> [[Term] -> a] -> Cons a
C ([[Type]] -> Type
SumOfProd ([[Type]]
ssa forall a. [a] -> [a] -> [a]
++ [[Type]]
ssb)) ([[Term] -> a]
ca forall a. [a] -> [a] -> [a]
++ [[Term] -> a]
cb)
where
C (SumOfProd [[Type]]
ssa) [[Term] -> a]
ca = Series a
a Int
d
C (SumOfProd [[Type]]
ssb) [[Term] -> a]
cb = Series a
b Int
d
conv :: [[Term] -> a] -> Term -> a
conv :: forall a. [[Term] -> a] -> Term -> a
conv [[Term] -> a]
cs (Var Pos
p Type
_) = forall a. HasCallStack => [Char] -> a
error (Char
'\0'forall a. a -> [a] -> [a]
:forall a b. (a -> b) -> [a] -> [b]
map forall a. Enum a => Int -> a
toEnum Pos
p)
conv [[Term] -> a]
cs (Ctr Int
i [Term]
xs) = ([[Term] -> a]
cs forall a. [a] -> Int -> a
!! Int
i) [Term]
xs
drawnFrom :: [a] -> Cons a
drawnFrom :: forall a. [a] -> Cons a
drawnFrom [a]
xs = forall a. Type -> [[Term] -> a] -> Cons a
C ([[Type]] -> Type
SumOfProd (forall a b. (a -> b) -> [a] -> [b]
map (forall a b. a -> b -> a
const []) [a]
xs)) (forall a b. (a -> b) -> [a] -> [b]
map forall a b. a -> b -> a
const [a]
xs)
cons0 :: a -> Series a
cons0 :: forall a. a -> Series a
cons0 a
f = forall a. a -> Series a
cons a
f
cons1 :: Serial a => (a -> b) -> Series b
cons1 :: forall a b. Serial a => (a -> b) -> Series b
cons1 a -> b
f = forall a. a -> Series a
cons a -> b
f forall a b. Series (a -> b) -> Series a -> Series b
>< forall a. Serial a => Series a
series
cons2 :: (Serial a, Serial b) => (a -> b -> c) -> Series c
cons2 :: forall a b c. (Serial a, Serial b) => (a -> b -> c) -> Series c
cons2 a -> b -> c
f = forall a. a -> Series a
cons a -> b -> c
f forall a b. Series (a -> b) -> Series a -> Series b
>< forall a. Serial a => Series a
series forall a b. Series (a -> b) -> Series a -> Series b
>< forall a. Serial a => Series a
series
cons3 :: (Serial a, Serial b, Serial c) => (a -> b -> c -> d) -> Series d
cons3 :: forall a b c d.
(Serial a, Serial b, Serial c) =>
(a -> b -> c -> d) -> Series d
cons3 a -> b -> c -> d
f = forall a. a -> Series a
cons a -> b -> c -> d
f forall a b. Series (a -> b) -> Series a -> Series b
>< forall a. Serial a => Series a
series forall a b. Series (a -> b) -> Series a -> Series b
>< forall a. Serial a => Series a
series forall a b. Series (a -> b) -> Series a -> Series b
>< forall a. Serial a => Series a
series
cons4 :: (Serial a, Serial b, Serial c, Serial d) =>
(a -> b -> c -> d -> e) -> Series e
cons4 :: forall a b c d e.
(Serial a, Serial b, Serial c, Serial d) =>
(a -> b -> c -> d -> e) -> Series e
cons4 a -> b -> c -> d -> e
f = forall a. a -> Series a
cons a -> b -> c -> d -> e
f forall a b. Series (a -> b) -> Series a -> Series b
>< forall a. Serial a => Series a
series forall a b. Series (a -> b) -> Series a -> Series b
>< forall a. Serial a => Series a
series forall a b. Series (a -> b) -> Series a -> Series b
>< forall a. Serial a => Series a
series forall a b. Series (a -> b) -> Series a -> Series b
>< forall a. Serial a => Series a
series
cons5 :: (Serial a, Serial b, Serial c, Serial d, Serial e) =>
(a -> b -> c -> d -> e -> f) -> Series f
cons5 :: forall a b c d e f.
(Serial a, Serial b, Serial c, Serial d, Serial e) =>
(a -> b -> c -> d -> e -> f) -> Series f
cons5 a -> b -> c -> d -> e -> f
f = forall a. a -> Series a
cons a -> b -> c -> d -> e -> f
f forall a b. Series (a -> b) -> Series a -> Series b
>< forall a. Serial a => Series a
series forall a b. Series (a -> b) -> Series a -> Series b
>< forall a. Serial a => Series a
series forall a b. Series (a -> b) -> Series a -> Series b
>< forall a. Serial a => Series a
series forall a b. Series (a -> b) -> Series a -> Series b
>< forall a. Serial a => Series a
series forall a b. Series (a -> b) -> Series a -> Series b
>< forall a. Serial a => Series a
series
instance Serial () where
series :: Series ()
series = forall a. a -> Series a
cons0 ()
instance Serial Bool where
series :: Series Bool
series = forall a. a -> Series a
cons0 Bool
False forall a. Series a -> Series a -> Series a
\/ forall a. a -> Series a
cons0 Bool
True
instance Serial a => Serial (Maybe a) where
series :: Series (Maybe a)
series = forall a. a -> Series a
cons0 forall a. Maybe a
Nothing forall a. Series a -> Series a -> Series a
\/ forall a b. Serial a => (a -> b) -> Series b
cons1 forall a. a -> Maybe a
Just
instance (Serial a, Serial b) => Serial (Either a b) where
series :: Series (Either a b)
series = forall a b. Serial a => (a -> b) -> Series b
cons1 forall a b. a -> Either a b
Left forall a. Series a -> Series a -> Series a
\/ forall a b. Serial a => (a -> b) -> Series b
cons1 forall a b. b -> Either a b
Right
instance Serial a => Serial [a] where
series :: Series [a]
series = forall a. a -> Series a
cons0 [] forall a. Series a -> Series a -> Series a
\/ forall a b c. (Serial a, Serial b) => (a -> b -> c) -> Series c
cons2 (:)
instance (Serial a, Serial b) => Serial (a, b) where
series :: Series (a, b)
series = forall a b c. (Serial a, Serial b) => (a -> b -> c) -> Series c
cons2 (,) forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall a. Num a => a -> a -> a
+Int
1)
instance (Serial a, Serial b, Serial c) => Serial (a, b, c) where
series :: Series (a, b, c)
series = forall a b c d.
(Serial a, Serial b, Serial c) =>
(a -> b -> c -> d) -> Series d
cons3 (,,) forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall a. Num a => a -> a -> a
+Int
1)
instance (Serial a, Serial b, Serial c, Serial d) =>
Serial (a, b, c, d) where
series :: Series (a, b, c, d)
series = forall a b c d e.
(Serial a, Serial b, Serial c, Serial d) =>
(a -> b -> c -> d -> e) -> Series e
cons4 (,,,) forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall a. Num a => a -> a -> a
+Int
1)
instance (Serial a, Serial b, Serial c, Serial d, Serial e) =>
Serial (a, b, c, d, e) where
series :: Series (a, b, c, d, e)
series = forall a b c d e f.
(Serial a, Serial b, Serial c, Serial d, Serial e) =>
(a -> b -> c -> d -> e -> f) -> Series f
cons5 (,,,,) forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall a. Num a => a -> a -> a
+Int
1)
instance Serial Int where
series :: Series Int
series Int
d = forall a. [a] -> Cons a
drawnFrom [-Int
d..Int
d]
instance Serial Integer where
series :: Series Integer
series Int
d = forall a. [a] -> Cons a
drawnFrom (forall a b. (a -> b) -> [a] -> [b]
map forall a. Integral a => a -> Integer
toInteger [-Int
d..Int
d])
instance Serial Char where
series :: Series Char
series Int
d = forall a. [a] -> Cons a
drawnFrom (forall a. Int -> [a] -> [a]
take (Int
dforall a. Num a => a -> a -> a
+Int
1) [Char
'a'..])
instance Serial Float where
series :: Series Float
series Int
d = forall a. [a] -> Cons a
drawnFrom (forall a. RealFloat a => Int -> [a]
floats Int
d)
instance Serial Double where
series :: Series Double
series Int
d = forall a. [a] -> Cons a
drawnFrom (forall a. RealFloat a => Int -> [a]
floats Int
d)
floats :: RealFloat a => Int -> [a]
floats :: forall a. RealFloat a => Int -> [a]
floats Int
d = [ forall a. RealFloat a => Integer -> Int -> a
encodeFloat Integer
sig Int
exp
| Integer
sig <- forall a b. (a -> b) -> [a] -> [b]
map forall a. Integral a => a -> Integer
toInteger [-Int
d..Int
d]
, Int
exp <- [-Int
d..Int
d]
, forall a. Integral a => a -> Bool
odd Integer
sig Bool -> Bool -> Bool
|| Integer
sig forall a. Eq a => a -> a -> Bool
== Integer
0 Bool -> Bool -> Bool
&& Int
exp forall a. Eq a => a -> a -> Bool
== Int
0
]
refine :: Term -> Pos -> [Term]
refine :: Term -> Pos -> [Term]
refine (Var Pos
p (SumOfProd [[Type]]
ss)) [] = Pos -> [[Type]] -> [Term]
new Pos
p [[Type]]
ss
refine (Ctr Int
c [Term]
xs) Pos
p = forall a b. (a -> b) -> [a] -> [b]
map (Int -> [Term] -> Term
Ctr Int
c) ([Term] -> Pos -> [[Term]]
refineList [Term]
xs Pos
p)
refineList :: [Term] -> Pos -> [[Term]]
refineList :: [Term] -> Pos -> [[Term]]
refineList [Term]
xs (Int
i:Pos
is) = [[Term]
ls forall a. [a] -> [a] -> [a]
++ Term
yforall a. a -> [a] -> [a]
:[Term]
rs | Term
y <- Term -> Pos -> [Term]
refine Term
x Pos
is]
where ([Term]
ls, Term
x:[Term]
rs) = forall a. Int -> [a] -> ([a], [a])
splitAt Int
i [Term]
xs
new :: Pos -> [[Type]] -> [Term]
new :: Pos -> [[Type]] -> [Term]
new Pos
p [[Type]]
ps = [ Int -> [Term] -> Term
Ctr Int
c (forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\Int
i Type
t -> Pos -> Type -> Term
Var (Pos
pforall a. [a] -> [a] -> [a]
++[Int
i]) Type
t) [Int
0..] [Type]
ts)
| (Int
c, [Type]
ts) <- forall a b. [a] -> [b] -> [(a, b)]
zip [Int
0..] [[Type]]
ps ]
total :: Term -> [Term]
total :: Term -> [Term]
total Term
val = Term -> [Term]
tot Term
val
where
tot :: Term -> [Term]
tot (Ctr Int
c [Term]
xs) = [Int -> [Term] -> Term
Ctr Int
c [Term]
ys | [Term]
ys <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Term -> [Term]
tot [Term]
xs]
tot (Var Pos
p (SumOfProd [[Type]]
ss)) = [Term
y | Term
x <- Pos -> [[Type]] -> [Term]
new Pos
p [[Type]]
ss, Term
y <- Term -> [Term]
tot Term
x]
answer :: a -> (a -> IO b) -> (Pos -> IO b) -> IO b
answer :: forall a b. a -> (a -> IO b) -> (Pos -> IO b) -> IO b
answer a
a a -> IO b
known Pos -> IO b
unknown =
do Either ErrorCall a
res <- forall e a. Exception e => IO a -> IO (Either e a)
try (forall a. a -> IO a
evaluate a
a)
case Either ErrorCall a
res of
Right a
b -> a -> IO b
known a
b
Left (ErrorCall (Char
'\0':[Char]
p)) -> Pos -> IO b
unknown (forall a b. (a -> b) -> [a] -> [b]
map forall a. Enum a => a -> Int
fromEnum [Char]
p)
Left ErrorCall
e -> forall a e. Exception e => e -> a
throw ErrorCall
e
refute :: Result -> IO Int
refute :: Result -> IO Int
refute Result
r = [Term] -> IO Int
ref (Result -> [Term]
args Result
r)
where
ref :: [Term] -> IO Int
ref [Term]
xs = forall a. Property -> (Bool -> IO a) -> (Pos -> IO a) -> IO a
eval (Result -> [Term] -> Property
apply Result
r [Term]
xs) forall {a}. Num a => Bool -> IO a
known Pos -> IO Int
unknown
where
known :: Bool -> IO a
known Bool
True = forall (m :: * -> *) a. Monad m => a -> m a
return a
1
known Bool
False = forall {b}. IO b
report
unknown :: Pos -> IO Int
unknown Pos
p = forall a. (a -> IO Int) -> Int -> [a] -> IO Int
sumMapM [Term] -> IO Int
ref Int
1 ([Term] -> Pos -> [[Term]]
refineList [Term]
xs Pos
p)
report :: IO b
report =
do [Char] -> IO ()
putStrLn [Char]
"Counter example found:"
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ [Char] -> IO ()
putStrLn forall a b. (a -> b) -> a -> b
$ forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith forall a b. (a -> b) -> a -> b
($) (Result -> [Term -> [Char]]
showArgs Result
r)
forall a b. (a -> b) -> a -> b
$ forall a. [a] -> a
head [[Term]
ys | [Term]
ys <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Term -> [Term]
total [Term]
xs]
forall a. ExitCode -> IO a
exitWith ExitCode
ExitSuccess
sumMapM :: (a -> IO Int) -> Int -> [a] -> IO Int
sumMapM :: forall a. (a -> IO Int) -> Int -> [a] -> IO Int
sumMapM a -> IO Int
f Int
n [] = forall (m :: * -> *) a. Monad m => a -> m a
return Int
n
sumMapM a -> IO Int
f Int
n (a
a:[a]
as) = seq :: forall a b. a -> b -> b
seq Int
n (do Int
m <- a -> IO Int
f a
a ; forall a. (a -> IO Int) -> Int -> [a] -> IO Int
sumMapM a -> IO Int
f (Int
nforall a. Num a => a -> a -> a
+Int
m) [a]
as)
data Property =
Bool Bool
| Neg Property
| And Property Property
| ParAnd Property Property
| Eq Property Property
eval :: Property -> (Bool -> IO a) -> (Pos -> IO a) -> IO a
eval :: forall a. Property -> (Bool -> IO a) -> (Pos -> IO a) -> IO a
eval Property
p Bool -> IO a
k Pos -> IO a
u = forall a b. a -> (a -> IO b) -> (Pos -> IO b) -> IO b
answer Property
p (\Property
p -> forall a. Property -> (Bool -> IO a) -> (Pos -> IO a) -> IO a
eval' Property
p Bool -> IO a
k Pos -> IO a
u) Pos -> IO a
u
eval' :: Property -> (Bool -> IO b) -> (Pos -> IO b) -> IO b
eval' (Bool Bool
b) Bool -> IO b
k Pos -> IO b
u = forall a b. a -> (a -> IO b) -> (Pos -> IO b) -> IO b
answer Bool
b Bool -> IO b
k Pos -> IO b
u
eval' (Neg Property
p) Bool -> IO b
k Pos -> IO b
u = forall a. Property -> (Bool -> IO a) -> (Pos -> IO a) -> IO a
eval Property
p (Bool -> IO b
k forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> Bool
not) Pos -> IO b
u
eval' (And Property
p Property
q) Bool -> IO b
k Pos -> IO b
u = forall a. Property -> (Bool -> IO a) -> (Pos -> IO a) -> IO a
eval Property
p (\Bool
b-> if Bool
b then forall a. Property -> (Bool -> IO a) -> (Pos -> IO a) -> IO a
eval Property
q Bool -> IO b
k Pos -> IO b
u else Bool -> IO b
k Bool
b) Pos -> IO b
u
eval' (Eq Property
p Property
q) Bool -> IO b
k Pos -> IO b
u = forall a. Property -> (Bool -> IO a) -> (Pos -> IO a) -> IO a
eval Property
p (\Bool
b-> if Bool
b then forall a. Property -> (Bool -> IO a) -> (Pos -> IO a) -> IO a
eval Property
q Bool -> IO b
k Pos -> IO b
u else forall a. Property -> (Bool -> IO a) -> (Pos -> IO a) -> IO a
eval (Property -> Property
Neg Property
q) Bool -> IO b
k Pos -> IO b
u) Pos -> IO b
u
eval' (ParAnd Property
p Property
q) Bool -> IO b
k Pos -> IO b
u = forall a. Property -> (Bool -> IO a) -> (Pos -> IO a) -> IO a
eval Property
p (\Bool
b-> if Bool
b then forall a. Property -> (Bool -> IO a) -> (Pos -> IO a) -> IO a
eval Property
q Bool -> IO b
k Pos -> IO b
u else Bool -> IO b
k Bool
b) Pos -> IO b
unknown
where
unknown :: Pos -> IO b
unknown Pos
pos = forall a. Property -> (Bool -> IO a) -> (Pos -> IO a) -> IO a
eval Property
q (\Bool
b-> if Bool
b then Pos -> IO b
u Pos
pos else Bool -> IO b
k Bool
b) (\Pos
_-> Pos -> IO b
u Pos
pos)
lift :: Bool -> Property
lift :: Bool -> Property
lift Bool
b = Bool -> Property
Bool Bool
b
neg :: Property -> Property
neg :: Property -> Property
neg Property
p = Property -> Property
Neg Property
p
(*&*), (*|*), (*=>*), (*=*) :: Property -> Property -> Property
Property
p *&* :: Property -> Property -> Property
*&* Property
q = Property -> Property -> Property
ParAnd Property
p Property
q
Property
p *|* :: Property -> Property -> Property
*|* Property
q = Property -> Property
neg (Property -> Property
neg Property
p Property -> Property -> Property
*&* Property -> Property
neg Property
q)
Property
p *=>* :: Property -> Property -> Property
*=>* Property
q = Property -> Property
neg (Property
p Property -> Property -> Property
*&* Property -> Property
neg Property
q)
Property
p *=* :: Property -> Property -> Property
*=* Property
q = Property -> Property -> Property
Eq Property
p Property
q
(==>) :: Bool -> Bool -> Bool
Bool
False ==> :: Bool -> Bool -> Bool
==> Bool
_ = Bool
True
Bool
True ==> Bool
x = Bool
x
data Result =
Result { Result -> [Term]
args :: [Term]
, Result -> [Term -> [Char]]
showArgs :: [Term -> String]
, Result -> [Term] -> Property
apply :: [Term] -> Property
}
data P = P (Int -> Int -> Result)
run :: Testable a => ([Term] -> a) -> Int -> Int -> Result
run :: forall a. Testable a => ([Term] -> a) -> Int -> Int -> Result
run [Term] -> a
a = Int -> Int -> Result
f where P Int -> Int -> Result
f = forall a. Testable a => ([Term] -> a) -> P
property [Term] -> a
a
class Testable a where
property :: ([Term] -> a) -> P
instance Testable Bool where
property :: ([Term] -> Bool) -> P
property [Term] -> Bool
apply = (Int -> Int -> Result) -> P
P forall a b. (a -> b) -> a -> b
$ \Int
n Int
d -> [Term] -> [Term -> [Char]] -> ([Term] -> Property) -> Result
Result [] [] (Bool -> Property
Bool forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Term] -> Bool
apply forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. [a] -> [a]
reverse)
instance Testable Property where
property :: ([Term] -> Property) -> P
property [Term] -> Property
apply = (Int -> Int -> Result) -> P
P forall a b. (a -> b) -> a -> b
$ \Int
n Int
d -> [Term] -> [Term -> [Char]] -> ([Term] -> Property) -> Result
Result [] [] ([Term] -> Property
apply forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. [a] -> [a]
reverse)
instance (Show a, Serial a, Testable b) => Testable (a -> b) where
property :: ([Term] -> a -> b) -> P
property [Term] -> a -> b
f = (Int -> Int -> Result) -> P
P forall a b. (a -> b) -> a -> b
$ \Int
n Int
d ->
let C Type
t [[Term] -> a]
c = forall a. Serial a => Series a
series Int
d
c' :: Term -> a
c' = forall a. [[Term] -> a] -> Term -> a
conv [[Term] -> a]
c
r :: Result
r = forall a. Testable a => ([Term] -> a) -> Int -> Int -> Result
run (\(Term
x:[Term]
xs) -> [Term] -> a -> b
f [Term]
xs (Term -> a
c' Term
x)) (Int
nforall a. Num a => a -> a -> a
+Int
1) Int
d
in Result
r { args :: [Term]
args = Pos -> Type -> Term
Var [Int
n] Type
t forall a. a -> [a] -> [a]
: Result -> [Term]
args Result
r, showArgs :: [Term -> [Char]]
showArgs = (forall a. Show a => a -> [Char]
show forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> a
c') forall a. a -> [a] -> [a]
: Result -> [Term -> [Char]]
showArgs Result
r }
depthCheck :: Testable a => Int -> a -> IO ()
depthCheck :: forall a. Testable a => Int -> a -> IO ()
depthCheck Int
d a
p =
do Int
n <- Result -> IO Int
refute forall a b. (a -> b) -> a -> b
$ forall a. Testable a => ([Term] -> a) -> Int -> Int -> Result
run (forall a b. a -> b -> a
const a
p) Int
0 Int
d
[Char] -> IO ()
putStrLn forall a b. (a -> b) -> a -> b
$ [Char]
"OK, required " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Int
n forall a. [a] -> [a] -> [a]
++ [Char]
" tests at depth " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Int
d
smallCheck :: Testable a => Int -> a -> IO ()
smallCheck :: forall a. Testable a => Int -> a -> IO ()
smallCheck Int
d a
p = forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (forall a. Testable a => Int -> a -> IO ()
`depthCheck` a
p) [Int
0..Int
d]
test :: Testable a => a -> IO ()
test :: forall a. Testable a => a -> IO ()
test a
p = forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (forall a. Testable a => Int -> a -> IO ()
`depthCheck` a
p) [Int
0..]