-- | For documentation, see the paper "SmallCheck and Lazy SmallCheck:
-- automatic exhaustive testing for small values" available at
-- <http://www.cs.york.ac.uk/fp/smallcheck/>.  Several examples are
-- also included in the package.

module Test.LazySmallCheck
  ( Serial(series) -- :: class
  , Series         -- :: type Series a = Int -> Cons a
  , Cons           -- :: *
  , cons           -- :: a -> Series a
  , (><)           -- :: Series (a -> b) -> Series a -> Series b
  , empty          -- :: Series a
  , (\/)           -- :: Series a -> Series a -> Series a
  , drawnFrom      -- :: [a] -> Cons a
  , cons0          -- :: a -> Series a
  , cons1          -- :: Serial a => (a -> b) -> Series b
  , cons2          -- :: (Serial a, Serial b) => (a -> b -> c) -> Series c
  , cons3          -- :: ...
  , cons4          -- :: ...
  , cons5          -- :: ...
  , Testable       -- :: class
  , depthCheck     -- :: Testable a => Int -> a -> IO ()
  , smallCheck     -- :: Testable a => Int -> a -> IO ()
  , test           -- :: Testable a => a -> IO ()
  , (==>)          -- :: Bool -> Bool -> Bool
  , Property       -- :: *
  , lift           -- :: Bool -> Property
  , neg            -- :: Property -> Property
  , (*&*)          -- :: Property -> Property -> Property
  , (*|*)          -- :: Property -> Property -> Property
  , (*=>*)         -- :: Property -> Property -> Property
  , (*=*)          -- :: Property -> Property -> Property
  )
  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

-- Series constructors

cons :: a -> Series a
cons :: a -> Series a
cons a
a Int
d = Type -> [[Term] -> a] -> Cons a
forall a. Type -> [[Term] -> a] -> Cons a
C ([[Type]] -> Type
SumOfProd [[]]) [a -> [Term] -> a
forall a b. a -> b -> a
const a
a]

empty :: Series a
empty :: Series a
empty Int
d = Type -> [[Term] -> a] -> Cons a
forall a. Type -> [[Term] -> a] -> Cons a
C ([[Type]] -> Type
SumOfProd []) []

(><) :: Series (a -> b) -> Series a -> Series b
(Series (a -> b)
f >< :: Series (a -> b) -> Series a -> Series b
>< Series a
a) Int
d = Type -> [[Term] -> b] -> Cons b
forall a. Type -> [[Term] -> a] -> Cons a
C ([[Type]] -> Type
SumOfProd [Type
taType -> [Type] -> [Type]
forall 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
dInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1)
    cs :: [[Term] -> b]
cs = [\(Term
x:[Term]
xs) -> [Term] -> a -> b
cf [Term]
xs ([[Term] -> a] -> Term -> a
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 Int -> Int -> Bool
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 ([[Type]] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [[Type]]
ps)

(\/) :: Series a -> Series a -> Series a
(Series a
a \/ :: Series a -> Series a -> Series a
\/ Series a
b) Int
d = Type -> [[Term] -> a] -> Cons a
forall a. Type -> [[Term] -> a] -> Cons a
C ([[Type]] -> Type
SumOfProd ([[Type]]
ssa [[Type]] -> [[Type]] -> [[Type]]
forall a. [a] -> [a] -> [a]
++ [[Type]]
ssb)) ([[Term] -> a]
ca [[Term] -> a] -> [[Term] -> a] -> [[Term] -> a]
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 :: [[Term] -> a] -> Term -> a
conv [[Term] -> a]
cs (Var Pos
p Type
_) = [Char] -> a
forall a. HasCallStack => [Char] -> a
error (Char
'\0'Char -> [Char] -> [Char]
forall a. a -> [a] -> [a]
:(Int -> Char) -> Pos -> [Char]
forall a b. (a -> b) -> [a] -> [b]
map Int -> Char
forall a. Enum a => Int -> a
toEnum Pos
p)
conv [[Term] -> a]
cs (Ctr Int
i [Term]
xs) = ([[Term] -> a]
cs [[Term] -> a] -> Int -> [Term] -> a
forall a. [a] -> Int -> a
!! Int
i) [Term]
xs

drawnFrom :: [a] -> Cons a
drawnFrom :: [a] -> Cons a
drawnFrom [a]
xs = Type -> [[Term] -> a] -> Cons a
forall a. Type -> [[Term] -> a] -> Cons a
C ([[Type]] -> Type
SumOfProd ((a -> [Type]) -> [a] -> [[Type]]
forall a b. (a -> b) -> [a] -> [b]
map ([Type] -> a -> [Type]
forall a b. a -> b -> a
const []) [a]
xs)) ((a -> [Term] -> a) -> [a] -> [[Term] -> a]
forall a b. (a -> b) -> [a] -> [b]
map a -> [Term] -> a
forall a b. a -> b -> a
const [a]
xs)

-- Helpers, a la SmallCheck

cons0 :: a -> Series a
cons0 :: a -> Series a
cons0 a
f = a -> Series a
forall a. a -> Series a
cons a
f

cons1 :: Serial a => (a -> b) -> Series b
cons1 :: (a -> b) -> Series b
cons1 a -> b
f = (a -> b) -> Series (a -> b)
forall a. a -> Series a
cons a -> b
f Series (a -> b) -> Series a -> Series b
forall a b. Series (a -> b) -> Series a -> Series b
>< Series a
forall a. Serial a => Series a
series

cons2 :: (Serial a, Serial b) => (a -> b -> c) -> Series c
cons2 :: (a -> b -> c) -> Series c
cons2 a -> b -> c
f = (a -> b -> c) -> Series (a -> b -> c)
forall a. a -> Series a
cons a -> b -> c
f Series (a -> b -> c) -> Series a -> Series (b -> c)
forall a b. Series (a -> b) -> Series a -> Series b
>< Series a
forall a. Serial a => Series a
series Series (b -> c) -> Series b -> Series c
forall a b. Series (a -> b) -> Series a -> Series b
>< Series b
forall a. Serial a => Series a
series

cons3 :: (Serial a, Serial b, Serial c) => (a -> b -> c -> d) -> Series d
cons3 :: (a -> b -> c -> d) -> Series d
cons3 a -> b -> c -> d
f = (a -> b -> c -> d) -> Series (a -> b -> c -> d)
forall a. a -> Series a
cons a -> b -> c -> d
f Series (a -> b -> c -> d) -> Series a -> Series (b -> c -> d)
forall a b. Series (a -> b) -> Series a -> Series b
>< Series a
forall a. Serial a => Series a
series Series (b -> c -> d) -> Series b -> Series (c -> d)
forall a b. Series (a -> b) -> Series a -> Series b
>< Series b
forall a. Serial a => Series a
series Series (c -> d) -> Series c -> Series d
forall a b. Series (a -> b) -> Series a -> Series b
>< Series c
forall a. Serial a => Series a
series

cons4 :: (Serial a, Serial b, Serial c, Serial d) =>
  (a -> b -> c -> d -> e) -> Series e
cons4 :: (a -> b -> c -> d -> e) -> Series e
cons4 a -> b -> c -> d -> e
f = (a -> b -> c -> d -> e) -> Series (a -> b -> c -> d -> e)
forall a. a -> Series a
cons a -> b -> c -> d -> e
f Series (a -> b -> c -> d -> e)
-> Series a -> Series (b -> c -> d -> e)
forall a b. Series (a -> b) -> Series a -> Series b
>< Series a
forall a. Serial a => Series a
series Series (b -> c -> d -> e) -> Series b -> Series (c -> d -> e)
forall a b. Series (a -> b) -> Series a -> Series b
>< Series b
forall a. Serial a => Series a
series Series (c -> d -> e) -> Series c -> Series (d -> e)
forall a b. Series (a -> b) -> Series a -> Series b
>< Series c
forall a. Serial a => Series a
series Series (d -> e) -> Series d -> Series e
forall a b. Series (a -> b) -> Series a -> Series b
>< Series d
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 :: (a -> b -> c -> d -> e -> f) -> Series f
cons5 a -> b -> c -> d -> e -> f
f = (a -> b -> c -> d -> e -> f) -> Series (a -> b -> c -> d -> e -> f)
forall a. a -> Series a
cons a -> b -> c -> d -> e -> f
f Series (a -> b -> c -> d -> e -> f)
-> Series a -> Series (b -> c -> d -> e -> f)
forall a b. Series (a -> b) -> Series a -> Series b
>< Series a
forall a. Serial a => Series a
series Series (b -> c -> d -> e -> f)
-> Series b -> Series (c -> d -> e -> f)
forall a b. Series (a -> b) -> Series a -> Series b
>< Series b
forall a. Serial a => Series a
series Series (c -> d -> e -> f) -> Series c -> Series (d -> e -> f)
forall a b. Series (a -> b) -> Series a -> Series b
>< Series c
forall a. Serial a => Series a
series Series (d -> e -> f) -> Series d -> Series (e -> f)
forall a b. Series (a -> b) -> Series a -> Series b
>< Series d
forall a. Serial a => Series a
series Series (e -> f) -> Series e -> Series f
forall a b. Series (a -> b) -> Series a -> Series b
>< Series e
forall a. Serial a => Series a
series

-- Standard instances

instance Serial () where
  series :: Series ()
series = () -> Series ()
forall a. a -> Series a
cons0 ()

instance Serial Bool where
  series :: Series Bool
series = Bool -> Series Bool
forall a. a -> Series a
cons0 Bool
False Series Bool -> Series Bool -> Series Bool
forall a. Series a -> Series a -> Series a
\/ Bool -> Series Bool
forall a. a -> Series a
cons0 Bool
True

instance Serial a => Serial (Maybe a) where
  series :: Series (Maybe a)
series = Maybe a -> Series (Maybe a)
forall a. a -> Series a
cons0 Maybe a
forall a. Maybe a
Nothing Series (Maybe a) -> Series (Maybe a) -> Series (Maybe a)
forall a. Series a -> Series a -> Series a
\/ (a -> Maybe a) -> Series (Maybe a)
forall a b. Serial a => (a -> b) -> Series b
cons1 a -> Maybe a
forall a. a -> Maybe a
Just

instance (Serial a, Serial b) => Serial (Either a b) where
  series :: Series (Either a b)
series = (a -> Either a b) -> Series (Either a b)
forall a b. Serial a => (a -> b) -> Series b
cons1 a -> Either a b
forall a b. a -> Either a b
Left Series (Either a b) -> Series (Either a b) -> Series (Either a b)
forall a. Series a -> Series a -> Series a
\/ (b -> Either a b) -> Series (Either a b)
forall a b. Serial a => (a -> b) -> Series b
cons1 b -> Either a b
forall a b. b -> Either a b
Right

instance Serial a => Serial [a] where
  series :: Series [a]
series = [a] -> Series [a]
forall a. a -> Series a
cons0 [] Series [a] -> Series [a] -> Series [a]
forall a. Series a -> Series a -> Series a
\/ (a -> [a] -> [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 = (a -> b -> (a, b)) -> Series (a, b)
forall a b c. (Serial a, Serial b) => (a -> b -> c) -> Series c
cons2 (,) Series (a, b) -> (Int -> Int) -> Series (a, b)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Int -> Int -> Int
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 = (a -> b -> c -> (a, b, c)) -> Series (a, b, c)
forall a b c d.
(Serial a, Serial b, Serial c) =>
(a -> b -> c -> d) -> Series d
cons3 (,,) Series (a, b, c) -> (Int -> Int) -> Series (a, b, c)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Int -> Int -> Int
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 = (a -> b -> c -> d -> (a, b, c, d)) -> Series (a, b, c, d)
forall a b c d e.
(Serial a, Serial b, Serial c, Serial d) =>
(a -> b -> c -> d -> e) -> Series e
cons4 (,,,) Series (a, b, c, d) -> (Int -> Int) -> Series (a, b, c, d)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Int -> Int -> Int
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 = (a -> b -> c -> d -> e -> (a, b, c, d, e))
-> Series (a, b, c, d, e)
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 (,,,,) Series (a, b, c, d, e) -> (Int -> Int) -> Series (a, b, c, d, e)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Int -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1)

instance Serial Int where
  series :: Series Int
series Int
d = Pos -> Cons Int
forall a. [a] -> Cons a
drawnFrom [-Int
d..Int
d]

instance Serial Integer where
  series :: Series Integer
series Int
d = [Integer] -> Cons Integer
forall a. [a] -> Cons a
drawnFrom ((Int -> Integer) -> Pos -> [Integer]
forall a b. (a -> b) -> [a] -> [b]
map Int -> Integer
forall a. Integral a => a -> Integer
toInteger [-Int
d..Int
d])

instance Serial Char where
  series :: Series Char
series Int
d = [Char] -> Cons Char
forall a. [a] -> Cons a
drawnFrom (Int -> [Char] -> [Char]
forall a. Int -> [a] -> [a]
take (Int
dInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) [Char
'a'..])

instance Serial Float where
  series :: Series Float
series Int
d = [Float] -> Cons Float
forall a. [a] -> Cons a
drawnFrom (Int -> [Float]
forall a. RealFloat a => Int -> [a]
floats Int
d)

instance Serial Double where
  series :: Series Double
series Int
d = [Double] -> Cons Double
forall a. [a] -> Cons a
drawnFrom (Int -> [Double]
forall a. RealFloat a => Int -> [a]
floats Int
d)

floats :: RealFloat a => Int -> [a]
floats :: Int -> [a]
floats Int
d = [ Integer -> Int -> a
forall a. RealFloat a => Integer -> Int -> a
encodeFloat Integer
sig Int
exp
           | Integer
sig <- (Int -> Integer) -> Pos -> [Integer]
forall a b. (a -> b) -> [a] -> [b]
map Int -> Integer
forall a. Integral a => a -> Integer
toInteger [-Int
d..Int
d]
           , Int
exp <- [-Int
d..Int
d]
           , Integer -> Bool
forall a. Integral a => a -> Bool
odd Integer
sig Bool -> Bool -> Bool
|| Integer
sig Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
0 Bool -> Bool -> Bool
&& Int
exp Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0
           ]

-- Term refinement

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 = ([Term] -> Term) -> [[Term]] -> [Term]
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 [Term] -> [Term] -> [Term]
forall a. [a] -> [a] -> [a]
++ Term
yTerm -> [Term] -> [Term]
forall a. a -> [a] -> [a]
:[Term]
rs | Term
y <- Term -> Pos -> [Term]
refine Term
x Pos
is]
  where ([Term]
ls, Term
x:[Term]
rs) = Int -> [Term] -> ([Term], [Term])
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 ((Int -> Type -> Term) -> Pos -> [Type] -> [Term]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\Int
i Type
t -> Pos -> Type -> Term
Var (Pos
pPos -> Pos -> Pos
forall a. [a] -> [a] -> [a]
++[Int
i]) Type
t) [Int
0..] [Type]
ts)
           | (Int
c, [Type]
ts) <- Pos -> [[Type]] -> [(Int, [Type])]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int
0..] [[Type]]
ps ]

-- Find total instantiations of a partial value

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 <- (Term -> [Term]) -> [Term] -> [[Term]]
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]

-- Answers

answer :: a -> (a -> IO b) -> (Pos -> IO b) -> IO b
answer :: 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 <- IO a -> IO (Either ErrorCall a)
forall e a. Exception e => IO a -> IO (Either e a)
try (a -> IO a
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 ((Char -> Int) -> [Char] -> Pos
forall a b. (a -> b) -> [a] -> [b]
map Char -> Int
forall a. Enum a => a -> Int
fromEnum [Char]
p)
       Left ErrorCall
e -> ErrorCall -> IO b
forall a e. Exception e => e -> a
throw ErrorCall
e

-- Refute

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 = Property -> (Bool -> IO Int) -> (Pos -> IO Int) -> IO Int
forall a. Property -> (Bool -> IO a) -> (Pos -> IO a) -> IO a
eval (Result -> [Term] -> Property
apply Result
r [Term]
xs) Bool -> IO Int
forall a. Num a => Bool -> IO a
known Pos -> IO Int
unknown
      where
        known :: Bool -> IO a
known Bool
True = a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return a
1
        known Bool
False = IO a
forall b. IO b
report
        unknown :: Pos -> IO Int
unknown Pos
p = ([Term] -> IO Int) -> Int -> [[Term]] -> IO Int
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:"
             ([Char] -> IO ()) -> [[Char]] -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ [Char] -> IO ()
putStrLn ([[Char]] -> IO ()) -> [[Char]] -> IO ()
forall a b. (a -> b) -> a -> b
$ ((Term -> [Char]) -> Term -> [Char])
-> [Term -> [Char]] -> [Term] -> [[Char]]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (Term -> [Char]) -> Term -> [Char]
forall a b. (a -> b) -> a -> b
($) (Result -> [Term -> [Char]]
showArgs Result
r)
                            ([Term] -> [[Char]]) -> [Term] -> [[Char]]
forall a b. (a -> b) -> a -> b
$ [[Term]] -> [Term]
forall a. [a] -> a
head [[Term]
ys | [Term]
ys <- (Term -> [Term]) -> [Term] -> [[Term]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Term -> [Term]
total [Term]
xs]
             ExitCode -> IO b
forall a. ExitCode -> IO a
exitWith ExitCode
ExitSuccess

sumMapM :: (a -> IO Int) -> Int -> [a] -> IO Int
sumMapM :: (a -> IO Int) -> Int -> [a] -> IO Int
sumMapM a -> IO Int
f Int
n [] = Int -> IO Int
forall (m :: * -> *) a. Monad m => a -> m a
return Int
n
sumMapM a -> IO Int
f Int
n (a
a:[a]
as) = Int -> IO Int -> IO Int
seq Int
n (do Int
m <- a -> IO Int
f a
a ; (a -> IO Int) -> Int -> [a] -> IO Int
forall a. (a -> IO Int) -> Int -> [a] -> IO Int
sumMapM a -> IO Int
f (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
m) [a]
as)

-- Properties with parallel conjunction (Lindblad TFP'07)

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 :: Property -> (Bool -> IO a) -> (Pos -> IO a) -> IO a
eval Property
p Bool -> IO a
k Pos -> IO a
u = Property -> (Property -> IO a) -> (Pos -> IO a) -> IO a
forall a b. a -> (a -> IO b) -> (Pos -> IO b) -> IO b
answer Property
p (\Property
p -> Property -> (Bool -> IO a) -> (Pos -> IO a) -> IO a
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 a) -> (Pos -> IO a) -> IO a
eval' (Bool Bool
b) Bool -> IO a
k Pos -> IO a
u = Bool -> (Bool -> IO a) -> (Pos -> IO a) -> IO a
forall a b. a -> (a -> IO b) -> (Pos -> IO b) -> IO b
answer Bool
b Bool -> IO a
k Pos -> IO a
u
eval' (Neg Property
p) Bool -> IO a
k Pos -> IO a
u = Property -> (Bool -> IO a) -> (Pos -> IO a) -> IO a
forall a. Property -> (Bool -> IO a) -> (Pos -> IO a) -> IO a
eval Property
p (Bool -> IO a
k (Bool -> IO a) -> (Bool -> Bool) -> Bool -> IO a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> Bool
not) Pos -> IO a
u
eval' (And Property
p Property
q) Bool -> IO a
k Pos -> IO a
u = Property -> (Bool -> IO a) -> (Pos -> IO a) -> IO a
forall a. Property -> (Bool -> IO a) -> (Pos -> IO a) -> IO a
eval Property
p (\Bool
b-> if Bool
b then Property -> (Bool -> IO a) -> (Pos -> IO a) -> IO a
forall a. Property -> (Bool -> IO a) -> (Pos -> IO a) -> IO a
eval Property
q Bool -> IO a
k Pos -> IO a
u else Bool -> IO a
k Bool
b) Pos -> IO a
u
eval' (Eq Property
p Property
q) Bool -> IO a
k Pos -> IO a
u = Property -> (Bool -> IO a) -> (Pos -> IO a) -> IO a
forall a. Property -> (Bool -> IO a) -> (Pos -> IO a) -> IO a
eval Property
p (\Bool
b-> if Bool
b then Property -> (Bool -> IO a) -> (Pos -> IO a) -> IO a
forall a. Property -> (Bool -> IO a) -> (Pos -> IO a) -> IO a
eval Property
q Bool -> IO a
k Pos -> IO a
u else Property -> (Bool -> IO a) -> (Pos -> IO a) -> IO a
forall a. Property -> (Bool -> IO a) -> (Pos -> IO a) -> IO a
eval (Property -> Property
Neg Property
q) Bool -> IO a
k Pos -> IO a
u) Pos -> IO a
u
eval' (ParAnd Property
p Property
q) Bool -> IO a
k Pos -> IO a
u = Property -> (Bool -> IO a) -> (Pos -> IO a) -> IO a
forall a. Property -> (Bool -> IO a) -> (Pos -> IO a) -> IO a
eval Property
p (\Bool
b-> if Bool
b then Property -> (Bool -> IO a) -> (Pos -> IO a) -> IO a
forall a. Property -> (Bool -> IO a) -> (Pos -> IO a) -> IO a
eval Property
q Bool -> IO a
k Pos -> IO a
u else Bool -> IO a
k Bool
b) Pos -> IO a
unknown
  where
    unknown :: Pos -> IO a
unknown Pos
pos = Property -> (Bool -> IO a) -> (Pos -> IO a) -> IO a
forall a. Property -> (Bool -> IO a) -> (Pos -> IO a) -> IO a
eval Property
q (\Bool
b-> if Bool
b then Pos -> IO a
u Pos
pos else Bool -> IO a
k Bool
b) (\Pos
_-> Pos -> IO a
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

-- Boolean implication

(==>) :: Bool -> Bool -> Bool
Bool
False ==> :: Bool -> Bool -> Bool
==> Bool
_ = Bool
True
Bool
True ==> Bool
x = Bool
x

-- Testable

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 :: ([Term] -> a) -> Int -> Int -> Result
run [Term] -> a
a = Int -> Int -> Result
f where P Int -> Int -> Result
f = ([Term] -> a) -> P
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 ((Int -> Int -> Result) -> P) -> (Int -> Int -> Result) -> P
forall a b. (a -> b) -> a -> b
$ \Int
n Int
d -> [Term] -> [Term -> [Char]] -> ([Term] -> Property) -> Result
Result [] [] (Bool -> Property
Bool (Bool -> Property) -> ([Term] -> Bool) -> [Term] -> Property
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Term] -> Bool
apply ([Term] -> Bool) -> ([Term] -> [Term]) -> [Term] -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Term] -> [Term]
forall a. [a] -> [a]
reverse)

instance Testable Property where
  property :: ([Term] -> Property) -> P
property [Term] -> Property
apply = (Int -> Int -> Result) -> P
P ((Int -> Int -> Result) -> P) -> (Int -> Int -> Result) -> P
forall a b. (a -> b) -> a -> b
$ \Int
n Int
d -> [Term] -> [Term -> [Char]] -> ([Term] -> Property) -> Result
Result [] [] ([Term] -> Property
apply ([Term] -> Property) -> ([Term] -> [Term]) -> [Term] -> Property
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Term] -> [Term]
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 ((Int -> Int -> Result) -> P) -> (Int -> Int -> Result) -> P
forall a b. (a -> b) -> a -> b
$ \Int
n Int
d ->
    let C Type
t [[Term] -> a]
c = Series a
forall a. Serial a => Series a
series Int
d
        c' :: Term -> a
c' = [[Term] -> a] -> Term -> a
forall a. [[Term] -> a] -> Term -> a
conv [[Term] -> a]
c
        r :: Result
r = ([Term] -> b) -> Int -> Int -> Result
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
nInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) Int
d
    in  Result
r { args :: [Term]
args = Pos -> Type -> Term
Var [Int
n] Type
t Term -> [Term] -> [Term]
forall a. a -> [a] -> [a]
: Result -> [Term]
args Result
r, showArgs :: [Term -> [Char]]
showArgs = (a -> [Char]
forall a. Show a => a -> [Char]
show (a -> [Char]) -> (Term -> a) -> Term -> [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> a
c') (Term -> [Char]) -> [Term -> [Char]] -> [Term -> [Char]]
forall a. a -> [a] -> [a]
: Result -> [Term -> [Char]]
showArgs Result
r }

-- Top-level interface

depthCheck :: Testable a => Int -> a -> IO ()
depthCheck :: Int -> a -> IO ()
depthCheck Int
d a
p =
  do Int
n <- Result -> IO Int
refute (Result -> IO Int) -> Result -> IO Int
forall a b. (a -> b) -> a -> b
$ ([Term] -> a) -> Int -> Int -> Result
forall a. Testable a => ([Term] -> a) -> Int -> Int -> Result
run (a -> [Term] -> a
forall a b. a -> b -> a
const a
p) Int
0 Int
d
     [Char] -> IO ()
putStrLn ([Char] -> IO ()) -> [Char] -> IO ()
forall a b. (a -> b) -> a -> b
$ [Char]
"OK, required " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Int -> [Char]
forall a. Show a => a -> [Char]
show Int
n [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" tests at depth " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Int -> [Char]
forall a. Show a => a -> [Char]
show Int
d

smallCheck :: Testable a => Int -> a -> IO ()
smallCheck :: Int -> a -> IO ()
smallCheck Int
d a
p = (Int -> IO ()) -> Pos -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (Int -> a -> IO ()
forall a. Testable a => Int -> a -> IO ()
`depthCheck` a
p) [Int
0..Int
d]

test :: Testable a => a -> IO ()
test :: a -> IO ()
test a
p = (Int -> IO ()) -> Pos -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (Int -> a -> IO ()
forall a. Testable a => Int -> a -> IO ()
`depthCheck` a
p) [Int
0..]