module Lava.Property
  ( Gen
  , generate
  , ChoiceWithSig
  , Fresh(..)
  , CoFresh(..)
  , double
  , triple
  , list
  , listOf
  , results
  , sequential
  , forAll
  , Property(..)
  , Checkable(..)
  , ShowModel(..)
  , Model
  , properties
  )
 where

import Lava.Signal
import Lava.Generic

import Control.Applicative (Applicative (..))

import Control.Monad
  ( ap
  , liftM2
  , liftM3
  , liftM4
  , liftM5
  )

import Data.List
  ( intersperse
  , transpose
  )

import Data.IORef
import System.IO.Unsafe

----------------------------------------------------------------
-- Gen Monad

newtype Gen a
  = Gen (Tree Int -> a)

instance Functor Gen where
  fmap :: (a -> b) -> Gen a -> Gen b
fmap f :: a -> b
f (Gen m :: Tree Int -> a
m) = (Tree Int -> b) -> Gen b
forall a. (Tree Int -> a) -> Gen a
Gen (\t :: Tree Int
t -> a -> b
f (Tree Int -> a
m Tree Int
t))

instance Applicative Gen where
  pure :: a -> Gen a
pure  = a -> Gen a
forall (m :: * -> *) a. Monad m => a -> m a
return
  <*> :: Gen (a -> b) -> Gen a -> Gen b
(<*>) = Gen (a -> b) -> Gen a -> Gen b
forall (m :: * -> *) a b. Monad m => m (a -> b) -> m a -> m b
ap

instance Monad Gen where
  return :: a -> Gen a
return a :: a
a =
    (Tree Int -> a) -> Gen a
forall a. (Tree Int -> a) -> Gen a
Gen (\t :: Tree Int
t -> a
a)

  Gen m :: Tree Int -> a
m >>= :: Gen a -> (a -> Gen b) -> Gen b
>>= k :: a -> Gen b
k =
    (Tree Int -> b) -> Gen b
forall a. (Tree Int -> a) -> Gen a
Gen (\(Fork _ t1 :: Tree Int
t1 t2 :: Tree Int
t2) -> let a :: a
a = Tree Int -> a
m Tree Int
t1 ; Gen m2 :: Tree Int -> b
m2 = a -> Gen b
k a
a in Tree Int -> b
m2 Tree Int
t2)

generate :: Gen a -> IO a
generate :: Gen a -> IO a
generate (Gen m :: Tree Int -> a
m) =
  do Tree Int
t <- IO (Tree Int)
newTree
     a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Tree Int -> a
m Tree Int
t)

-- Gen Tree

data Tree a
  = Fork a (Tree a) (Tree a)

newTree :: IO (Tree Int)
newTree :: IO (Tree Int)
newTree =
  do IORef Int
var <- Int -> IO (IORef Int)
forall a. a -> IO (IORef a)
newIORef 0
     IORef Int -> IO (Tree Int)
forall a. Num a => IORef a -> IO (Tree a)
tree IORef Int
var
 where
  tree :: IORef a -> IO (Tree a)
tree var :: IORef a
var = IO (Tree a) -> IO (Tree a)
forall a. IO a -> IO a
unsafeInterleaveIO (IO (Tree a) -> IO (Tree a)) -> IO (Tree a) -> IO (Tree a)
forall a b. (a -> b) -> a -> b
$
    do a
n  <- IORef a -> IO a
forall a. Num a => IORef a -> IO a
new IORef a
var
       Tree a
t1 <- IORef a -> IO (Tree a)
tree IORef a
var
       Tree a
t2 <- IORef a -> IO (Tree a)
tree IORef a
var
       Tree a -> IO (Tree a)
forall (m :: * -> *) a. Monad m => a -> m a
return (a -> Tree a -> Tree a -> Tree a
forall a. a -> Tree a -> Tree a -> Tree a
Fork a
n Tree a
t1 Tree a
t2)

  new :: IORef a -> IO a
new var :: IORef a
var = IO a -> IO a
forall a. IO a -> IO a
unsafeInterleaveIO (IO a -> IO a) -> IO a -> IO a
forall a b. (a -> b) -> a -> b
$
    do a
n <- IORef a -> IO a
forall a. IORef a -> IO a
readIORef IORef a
var
       let n' :: a
n' = a
na -> a -> a
forall a. Num a => a -> a -> a
+1
       a
n' a -> IO () -> IO ()
forall a b. a -> b -> b
`seq` IORef a -> a -> IO ()
forall a. IORef a -> a -> IO ()
writeIORef IORef a
var a
n'
       a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return a
n

----------------------------------------------------------------
-- Fresh

class Fresh a where
  fresh :: Gen a

instance Fresh () where
  fresh :: Gen ()
fresh = () -> Gen ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()

instance ConstructiveSig a => Fresh (Signal a) where
  fresh :: Gen (Signal a)
fresh = (Tree Int -> Signal a) -> Gen (Signal a)
forall a. (Tree Int -> a) -> Gen a
Gen (\(Fork n :: Int
n _ _) -> String -> Signal a
forall a. ConstructiveSig a => String -> Signal a
varSig ("i" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
n))

instance (Fresh a, Fresh b) => Fresh (a,b) where
  fresh :: Gen (a, b)
fresh = (a -> b -> (a, b)) -> Gen a -> Gen b -> Gen (a, b)
forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 (,) Gen a
forall a. Fresh a => Gen a
fresh Gen b
forall a. Fresh a => Gen a
fresh

instance (Fresh a, Fresh b, Fresh c) => Fresh (a,b,c) where
  fresh :: Gen (a, b, c)
fresh = (a -> b -> c -> (a, b, c))
-> Gen a -> Gen b -> Gen c -> Gen (a, b, c)
forall (m :: * -> *) a1 a2 a3 r.
Monad m =>
(a1 -> a2 -> a3 -> r) -> m a1 -> m a2 -> m a3 -> m r
liftM3 (,,) Gen a
forall a. Fresh a => Gen a
fresh Gen b
forall a. Fresh a => Gen a
fresh Gen c
forall a. Fresh a => Gen a
fresh

instance (Fresh a, Fresh b, Fresh c, Fresh d) => Fresh (a,b,c,d) where
  fresh :: Gen (a, b, c, d)
fresh = (a -> b -> c -> d -> (a, b, c, d))
-> Gen a -> Gen b -> Gen c -> Gen d -> Gen (a, b, c, d)
forall (m :: * -> *) a1 a2 a3 a4 r.
Monad m =>
(a1 -> a2 -> a3 -> a4 -> r) -> m a1 -> m a2 -> m a3 -> m a4 -> m r
liftM4 (,,,) Gen a
forall a. Fresh a => Gen a
fresh Gen b
forall a. Fresh a => Gen a
fresh Gen c
forall a. Fresh a => Gen a
fresh Gen d
forall a. Fresh a => Gen a
fresh

instance (Fresh a, Fresh b, Fresh c, Fresh d, Fresh e) => Fresh (a,b,c,d,e) where
  fresh :: Gen (a, b, c, d, e)
fresh = (a -> b -> c -> d -> e -> (a, b, c, d, e))
-> Gen a -> Gen b -> Gen c -> Gen d -> Gen e -> Gen (a, b, c, d, e)
forall (m :: * -> *) a1 a2 a3 a4 a5 r.
Monad m =>
(a1 -> a2 -> a3 -> a4 -> a5 -> r)
-> m a1 -> m a2 -> m a3 -> m a4 -> m a5 -> m r
liftM5 (,,,,) Gen a
forall a. Fresh a => Gen a
fresh Gen b
forall a. Fresh a => Gen a
fresh Gen c
forall a. Fresh a => Gen a
fresh Gen d
forall a. Fresh a => Gen a
fresh Gen e
forall a. Fresh a => Gen a
fresh

instance (Fresh a, Fresh b, Fresh c, Fresh d, Fresh e, Fresh f) => Fresh (a,b,c,d,e,f) where
  fresh :: Gen (a, b, c, d, e, f)
fresh = (a -> b -> c -> d -> e -> f -> (a, b, c, d, e, f))
-> Gen a
-> Gen b
-> Gen c
-> Gen d
-> Gen e
-> Gen f
-> Gen (a, b, c, d, e, f)
forall (m :: * -> *) t t t t t t b.
Monad m =>
(t -> t -> t -> t -> t -> t -> b)
-> m t -> m t -> m t -> m t -> m t -> m t -> m b
liftM6 (,,,,,) Gen a
forall a. Fresh a => Gen a
fresh Gen b
forall a. Fresh a => Gen a
fresh Gen c
forall a. Fresh a => Gen a
fresh Gen d
forall a. Fresh a => Gen a
fresh Gen e
forall a. Fresh a => Gen a
fresh Gen f
forall a. Fresh a => Gen a
fresh

instance (Fresh a, Fresh b, Fresh c, Fresh d, Fresh e, Fresh f, Fresh g) => Fresh (a,b,c,d,e,f,g) where
  fresh :: Gen (a, b, c, d, e, f, g)
fresh = (a -> b -> c -> d -> e -> f -> g -> (a, b, c, d, e, f, g))
-> Gen a
-> Gen b
-> Gen c
-> Gen d
-> Gen e
-> Gen f
-> Gen g
-> Gen (a, b, c, d, e, f, g)
forall (m :: * -> *) t t t t t t t b.
Monad m =>
(t -> t -> t -> t -> t -> t -> t -> b)
-> m t -> m t -> m t -> m t -> m t -> m t -> m t -> m b
liftM7 (,,,,,,) Gen a
forall a. Fresh a => Gen a
fresh Gen b
forall a. Fresh a => Gen a
fresh Gen c
forall a. Fresh a => Gen a
fresh Gen d
forall a. Fresh a => Gen a
fresh Gen e
forall a. Fresh a => Gen a
fresh Gen f
forall a. Fresh a => Gen a
fresh Gen g
forall a. Fresh a => Gen a
fresh

-- CoFresh

class ChoiceWithSig a where
  ifThenElseWithSig :: Choice b => Signal a -> (b, b) -> b

class CoFresh a where
  cofresh :: (Choice b, Fresh b) => Gen b -> Gen (a -> b)

instance ChoiceWithSig Bool where
  ifThenElseWithSig :: Signal Bool -> (b, b) -> b
ifThenElseWithSig = Signal Bool -> (b, b) -> b
forall b. Choice b => Signal Bool -> (b, b) -> b
ifThenElse

instance CoFresh () where
  cofresh :: Gen b -> Gen (() -> b)
cofresh gen :: Gen b
gen =
    do b
b <- Gen b
gen
       (() -> b) -> Gen (() -> b)
forall (m :: * -> *) a. Monad m => a -> m a
return (\_ -> b
b)

instance ChoiceWithSig a => CoFresh (Signal a) where
  cofresh :: Gen b -> Gen (Signal a -> b)
cofresh gen :: Gen b
gen =
    do b
b1 <- Gen b
gen
       b
b2 <- Gen b
gen
       (Signal a -> b) -> Gen (Signal a -> b)
forall (m :: * -> *) a. Monad m => a -> m a
return (\a :: Signal a
a -> Signal a -> (b, b) -> b
forall a b. (ChoiceWithSig a, Choice b) => Signal a -> (b, b) -> b
ifThenElseWithSig Signal a
a (b
b1, b
b2))

instance (CoFresh a, CoFresh b) => CoFresh (a, b) where
  cofresh :: Gen b -> Gen ((a, b) -> b)
cofresh gen :: Gen b
gen =
    do a -> b -> b
f <- Gen (b -> b) -> Gen (a -> b -> b)
forall a b. (CoFresh a, Choice b, Fresh b) => Gen b -> Gen (a -> b)
cofresh (Gen b -> Gen (b -> b)
forall a b. (CoFresh a, Choice b, Fresh b) => Gen b -> Gen (a -> b)
cofresh Gen b
gen)
       ((a, b) -> b) -> Gen ((a, b) -> b)
forall (m :: * -> *) a. Monad m => a -> m a
return (\(a :: a
a, b :: b
b) -> a -> b -> b
f a
a b
b)

instance (CoFresh a, CoFresh b, CoFresh c) => CoFresh (a, b, c) where
  cofresh :: Gen b -> Gen ((a, b, c) -> b)
cofresh gen :: Gen b
gen =
    do a -> b -> c -> b
f <- Gen (b -> c -> b) -> Gen (a -> b -> c -> b)
forall a b. (CoFresh a, Choice b, Fresh b) => Gen b -> Gen (a -> b)
cofresh (Gen (c -> b) -> Gen (b -> c -> b)
forall a b. (CoFresh a, Choice b, Fresh b) => Gen b -> Gen (a -> b)
cofresh (Gen b -> Gen (c -> b)
forall a b. (CoFresh a, Choice b, Fresh b) => Gen b -> Gen (a -> b)
cofresh Gen b
gen))
       ((a, b, c) -> b) -> Gen ((a, b, c) -> b)
forall (m :: * -> *) a. Monad m => a -> m a
return (\(a :: a
a, b :: b
b, c :: c
c) -> a -> b -> c -> b
f a
a b
b c
c)

instance (CoFresh a, CoFresh b, CoFresh c, CoFresh d) => CoFresh (a, b, c, d) where
  cofresh :: Gen b -> Gen ((a, b, c, d) -> b)
cofresh gen :: Gen b
gen =
    do a -> b -> c -> d -> b
f <- Gen (b -> c -> d -> b) -> Gen (a -> b -> c -> d -> b)
forall a b. (CoFresh a, Choice b, Fresh b) => Gen b -> Gen (a -> b)
cofresh (Gen (c -> d -> b) -> Gen (b -> c -> d -> b)
forall a b. (CoFresh a, Choice b, Fresh b) => Gen b -> Gen (a -> b)
cofresh (Gen (d -> b) -> Gen (c -> d -> b)
forall a b. (CoFresh a, Choice b, Fresh b) => Gen b -> Gen (a -> b)
cofresh (Gen b -> Gen (d -> b)
forall a b. (CoFresh a, Choice b, Fresh b) => Gen b -> Gen (a -> b)
cofresh Gen b
gen)))
       ((a, b, c, d) -> b) -> Gen ((a, b, c, d) -> b)
forall (m :: * -> *) a. Monad m => a -> m a
return (\(a :: a
a, b :: b
b, c :: c
c, d :: d
d) -> a -> b -> c -> d -> b
f a
a b
b c
c d
d)

instance (CoFresh a, CoFresh b, CoFresh c, CoFresh d, CoFresh e) => CoFresh (a, b, c, d, e) where
  cofresh :: Gen b -> Gen ((a, b, c, d, e) -> b)
cofresh gen :: Gen b
gen =
    do a -> b -> c -> d -> e -> b
f <- Gen (b -> c -> d -> e -> b) -> Gen (a -> b -> c -> d -> e -> b)
forall a b. (CoFresh a, Choice b, Fresh b) => Gen b -> Gen (a -> b)
cofresh (Gen (c -> d -> e -> b) -> Gen (b -> c -> d -> e -> b)
forall a b. (CoFresh a, Choice b, Fresh b) => Gen b -> Gen (a -> b)
cofresh (Gen (d -> e -> b) -> Gen (c -> d -> e -> b)
forall a b. (CoFresh a, Choice b, Fresh b) => Gen b -> Gen (a -> b)
cofresh (Gen (e -> b) -> Gen (d -> e -> b)
forall a b. (CoFresh a, Choice b, Fresh b) => Gen b -> Gen (a -> b)
cofresh (Gen b -> Gen (e -> b)
forall a b. (CoFresh a, Choice b, Fresh b) => Gen b -> Gen (a -> b)
cofresh Gen b
gen))))
       ((a, b, c, d, e) -> b) -> Gen ((a, b, c, d, e) -> b)
forall (m :: * -> *) a. Monad m => a -> m a
return (\(a :: a
a, b :: b
b, c :: c
c, d :: d
d, e :: e
e) -> a -> b -> c -> d -> e -> b
f a
a b
b c
c d
d e
e)

instance (CoFresh a, CoFresh b, CoFresh c, CoFresh d, CoFresh e, CoFresh f) => CoFresh (a, b, c, d, e, f) where
  cofresh :: Gen b -> Gen ((a, b, c, d, e, f) -> b)
cofresh gen :: Gen b
gen =
    do a -> b -> c -> d -> e -> f -> b
f <- Gen (b -> c -> d -> e -> f -> b)
-> Gen (a -> b -> c -> d -> e -> f -> b)
forall a b. (CoFresh a, Choice b, Fresh b) => Gen b -> Gen (a -> b)
cofresh (Gen (c -> d -> e -> f -> b) -> Gen (b -> c -> d -> e -> f -> b)
forall a b. (CoFresh a, Choice b, Fresh b) => Gen b -> Gen (a -> b)
cofresh (Gen (d -> e -> f -> b) -> Gen (c -> d -> e -> f -> b)
forall a b. (CoFresh a, Choice b, Fresh b) => Gen b -> Gen (a -> b)
cofresh (Gen (e -> f -> b) -> Gen (d -> e -> f -> b)
forall a b. (CoFresh a, Choice b, Fresh b) => Gen b -> Gen (a -> b)
cofresh (Gen (f -> b) -> Gen (e -> f -> b)
forall a b. (CoFresh a, Choice b, Fresh b) => Gen b -> Gen (a -> b)
cofresh (Gen b -> Gen (f -> b)
forall a b. (CoFresh a, Choice b, Fresh b) => Gen b -> Gen (a -> b)
cofresh Gen b
gen)))))
       ((a, b, c, d, e, f) -> b) -> Gen ((a, b, c, d, e, f) -> b)
forall (m :: * -> *) a. Monad m => a -> m a
return (\(a :: a
a, b :: b
b, c :: c
c, d :: d
d, e :: e
e, g :: f
g) -> a -> b -> c -> d -> e -> f -> b
f a
a b
b c
c d
d e
e f
g)

instance (CoFresh a, CoFresh b, CoFresh c, CoFresh d, CoFresh e, CoFresh f, CoFresh g) => CoFresh (a, b, c, d, e, f, g) where
  cofresh :: Gen b -> Gen ((a, b, c, d, e, f, g) -> b)
cofresh gen :: Gen b
gen =
    do a -> b -> c -> d -> e -> f -> g -> b
f <- Gen (b -> c -> d -> e -> f -> g -> b)
-> Gen (a -> b -> c -> d -> e -> f -> g -> b)
forall a b. (CoFresh a, Choice b, Fresh b) => Gen b -> Gen (a -> b)
cofresh (Gen (c -> d -> e -> f -> g -> b)
-> Gen (b -> c -> d -> e -> f -> g -> b)
forall a b. (CoFresh a, Choice b, Fresh b) => Gen b -> Gen (a -> b)
cofresh (Gen (d -> e -> f -> g -> b) -> Gen (c -> d -> e -> f -> g -> b)
forall a b. (CoFresh a, Choice b, Fresh b) => Gen b -> Gen (a -> b)
cofresh (Gen (e -> f -> g -> b) -> Gen (d -> e -> f -> g -> b)
forall a b. (CoFresh a, Choice b, Fresh b) => Gen b -> Gen (a -> b)
cofresh (Gen (f -> g -> b) -> Gen (e -> f -> g -> b)
forall a b. (CoFresh a, Choice b, Fresh b) => Gen b -> Gen (a -> b)
cofresh (Gen (g -> b) -> Gen (f -> g -> b)
forall a b. (CoFresh a, Choice b, Fresh b) => Gen b -> Gen (a -> b)
cofresh (Gen b -> Gen (g -> b)
forall a b. (CoFresh a, Choice b, Fresh b) => Gen b -> Gen (a -> b)
cofresh Gen b
gen))))))
       ((a, b, c, d, e, f, g) -> b) -> Gen ((a, b, c, d, e, f, g) -> b)
forall (m :: * -> *) a. Monad m => a -> m a
return (\(a :: a
a, b :: b
b, c :: c
c, d :: d
d, e :: e
e, g :: f
g, h :: g
h) -> a -> b -> c -> d -> e -> f -> g -> b
f a
a b
b c
c d
d e
e f
g g
h)

instance (CoFresh a, Choice b, Fresh b) => Fresh (a -> b) where
  fresh :: Gen (a -> b)
fresh = Gen b -> Gen (a -> b)
forall a b. (CoFresh a, Choice b, Fresh b) => Gen b -> Gen (a -> b)
cofresh Gen b
forall a. Fresh a => Gen a
fresh

instance CoFresh a => CoFresh [a] where
  cofresh :: Gen b -> Gen ([a] -> b)
cofresh gen :: Gen b
gen =
    do [[a] -> b]
fs <- [Gen ([a] -> b)] -> Gen [[a] -> b]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence [ Int -> Gen b -> Gen ([a] -> b)
forall a b.
(CoFresh a, Choice b, Fresh b) =>
Int -> Gen b -> Gen ([a] -> b)
cofreshList Int
i Gen b
gen | Int
i <- [0..] ]
       ([a] -> b) -> Gen ([a] -> b)
forall (m :: * -> *) a. Monad m => a -> m a
return (\as :: [a]
as -> ([[a] -> b]
fs [[a] -> b] -> Int -> [a] -> b
forall a. [a] -> Int -> a
!! [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [a]
as) [a]
as)

instance (Finite a, CoFresh b) => CoFresh (a -> b) where
  cofresh :: Gen b -> Gen ((a -> b) -> b)
cofresh gen :: Gen b
gen =
    do [b] -> b
f <- Gen b -> Gen ([b] -> b)
forall a b. (CoFresh a, Choice b, Fresh b) => Gen b -> Gen (a -> b)
cofresh Gen b
gen
       ((a -> b) -> b) -> Gen ((a -> b) -> b)
forall (m :: * -> *) a. Monad m => a -> m a
return (\g :: a -> b
g -> [b] -> b
f ((a -> b) -> [a] -> [b]
forall a b. (a -> b) -> [a] -> [b]
map a -> b
g [a]
forall a. Finite a => [a]
domain))

cofreshList :: (CoFresh a, Choice b, Fresh b) => Int -> Gen b -> Gen ([a] -> b)
cofreshList :: Int -> Gen b -> Gen ([a] -> b)
cofreshList 0 gen :: Gen b
gen =
  do b
x <- Gen b
gen
     ([a] -> b) -> Gen ([a] -> b)
forall (m :: * -> *) a. Monad m => a -> m a
return (\[] -> b
x)

cofreshList k :: Int
k gen :: Gen b
gen =
  do [a] -> a -> b
f <- Int -> Gen (a -> b) -> Gen ([a] -> a -> b)
forall a b.
(CoFresh a, Choice b, Fresh b) =>
Int -> Gen b -> Gen ([a] -> b)
cofreshList (Int
kInt -> Int -> Int
forall a. Num a => a -> a -> a
-1) (Gen b -> Gen (a -> b)
forall a b. (CoFresh a, Choice b, Fresh b) => Gen b -> Gen (a -> b)
cofresh Gen b
gen)
     ([a] -> b) -> Gen ([a] -> b)
forall (m :: * -> *) a. Monad m => a -> m a
return (\(a :: a
a:as :: [a]
as) -> [a] -> a -> b
f [a]
as a
a)

----------------------------------------------------------------
-- some combinators

double :: Gen a -> Gen (a,a)
double :: Gen a -> Gen (a, a)
double gen :: Gen a
gen = (a -> a -> (a, a)) -> Gen a -> Gen a -> Gen (a, a)
forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 (,) Gen a
gen Gen a
gen

triple :: Gen a -> Gen (a,a,a)
triple :: Gen a -> Gen (a, a, a)
triple gen :: Gen a
gen = (a -> a -> a -> (a, a, a))
-> Gen a -> Gen a -> Gen a -> Gen (a, a, a)
forall (m :: * -> *) a1 a2 a3 r.
Monad m =>
(a1 -> a2 -> a3 -> r) -> m a1 -> m a2 -> m a3 -> m r
liftM3 (,,) Gen a
gen Gen a
gen Gen a
gen

list :: Fresh a => Int -> Gen [a]
list :: Int -> Gen [a]
list n :: Int
n = [Gen a] -> Gen [a]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence [ Gen a
forall a. Fresh a => Gen a
fresh | Int
i <- [1..Int
n] ]

listOf :: Int -> Gen a -> Gen [a]
listOf :: Int -> Gen a -> Gen [a]
listOf n :: Int
n gen :: Gen a
gen = [Gen a] -> Gen [a]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence [ Gen a
gen | Int
i <- [1..Int
n] ]

----------------------------------------------------------------
-- combinators for circuits

results :: Int -> Gen (a -> b) -> Gen (a -> [b])
results :: Int -> Gen (a -> b) -> Gen (a -> [b])
results n :: Int
n gen :: Gen (a -> b)
gen =
  do [a -> b]
fs <- [Gen (a -> b)] -> Gen [a -> b]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence [ Gen (a -> b)
gen | Int
i <- [1..Int
n] ]
     (a -> [b]) -> Gen (a -> [b])
forall (m :: * -> *) a. Monad m => a -> m a
return (\a :: a
a -> ((a -> b) -> b) -> [a -> b] -> [b]
forall a b. (a -> b) -> [a] -> [b]
map ((a -> b) -> a -> b
forall a b. (a -> b) -> a -> b
$ a
a) [a -> b]
fs)

sequential :: (CoFresh a, Fresh b, Choice b) => Int -> Gen (a -> b)
sequential :: Int -> Gen (a -> b)
sequential n :: Int
n =
  do (a, [Signal Bool]) -> b
fb     <- Gen ((a, [Signal Bool]) -> b)
forall a. Fresh a => Gen a
fresh
     (a, [Signal Bool]) -> [Signal Bool]
fstate <- Int
-> Gen ((a, [Signal Bool]) -> Signal Bool)
-> Gen ((a, [Signal Bool]) -> [Signal Bool])
forall a b. Int -> Gen (a -> b) -> Gen (a -> [b])
results Int
n Gen ((a, [Signal Bool]) -> Signal Bool)
forall a. Fresh a => Gen a
fresh
     let circ :: (a, [Signal Bool]) -> (b, [Signal Bool])
circ inp :: (a, [Signal Bool])
inp = ((a, [Signal Bool]) -> b
fb (a, [Signal Bool])
inp, (a, [Signal Bool]) -> [Signal Bool]
fstate (a, [Signal Bool])
inp)
     (a -> b) -> Gen (a -> b)
forall (m :: * -> *) a. Monad m => a -> m a
return (((a, [Signal Bool]) -> (b, [Signal Bool])) -> a -> b
forall a a. ((a, [Signal Bool]) -> (a, [Signal Bool])) -> a -> a
loop (a, [Signal Bool]) -> (b, [Signal Bool])
circ)
 where
  loop :: ((a, [Signal Bool]) -> (a, [Signal Bool])) -> a -> a
loop circ :: (a, [Signal Bool]) -> (a, [Signal Bool])
circ a :: a
a = a
b
    where
      (b :: a
b, state :: [Signal Bool]
state) = (a, [Signal Bool]) -> (a, [Signal Bool])
circ (a
a, [Signal Bool] -> [Signal Bool] -> [Signal Bool]
forall a. Generic a => a -> a -> a
delay (Int -> [Signal Bool]
forall a. Constructive a => Int -> [a]
zeroList Int
n) ([Signal Bool]
state :: [Signal Bool]))

----------------------------------------------------------------
-- checkable

newtype Property
  = P (Gen ([Signal Bool], Model -> [[String]]))

class Checkable a where
  property :: a -> Property

instance Checkable Property where
  property :: Property -> Property
property p :: Property
p = Property
p

instance Checkable Bool where
  property :: Bool -> Property
property b :: Bool
b = Signal Bool -> Property
forall a. Checkable a => a -> Property
property (Bool -> Signal Bool
bool Bool
b)

instance Checkable a => Checkable (Signal a) where
  property :: Signal a -> Property
property (Signal s :: Symbol
s) = Gen ([Signal Bool], Model -> [[String]]) -> Property
P (([Signal Bool], Model -> [[String]])
-> Gen ([Signal Bool], Model -> [[String]])
forall (m :: * -> *) a. Monad m => a -> m a
return ([Symbol -> Signal Bool
forall a. Symbol -> Signal a
Signal Symbol
s], \_ -> []))

instance Checkable a => Checkable [a] where
  property :: [a] -> Property
property as :: [a]
as = Gen ([Signal Bool], Model -> [[String]]) -> Property
P (Gen ([Signal Bool], Model -> [[String]]) -> Property)
-> Gen ([Signal Bool], Model -> [[String]]) -> Property
forall a b. (a -> b) -> a -> b
$
    do [([Signal Bool], Model -> [[String]])]
sms <- [Gen ([Signal Bool], Model -> [[String]])]
-> Gen [([Signal Bool], Model -> [[String]])]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence [ Gen ([Signal Bool], Model -> [[String]])
gen | (P gen :: Gen ([Signal Bool], Model -> [[String]])
gen) <- (a -> Property) -> [a] -> [Property]
forall a b. (a -> b) -> [a] -> [b]
map a -> Property
forall a. Checkable a => a -> Property
property [a]
as ]
       ([Signal Bool], Model -> [[String]])
-> Gen ([Signal Bool], Model -> [[String]])
forall (m :: * -> *) a. Monad m => a -> m a
return ([[Signal Bool]] -> [Signal Bool]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ((([Signal Bool], Model -> [[String]]) -> [Signal Bool])
-> [([Signal Bool], Model -> [[String]])] -> [[Signal Bool]]
forall a b. (a -> b) -> [a] -> [b]
map ([Signal Bool], Model -> [[String]]) -> [Signal Bool]
forall a b. (a, b) -> a
fst [([Signal Bool], Model -> [[String]])]
sms), \model :: Model
model -> [[[String]]] -> [[String]]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ((([Signal Bool], Model -> [[String]]) -> [[String]])
-> [([Signal Bool], Model -> [[String]])] -> [[[String]]]
forall a b. (a -> b) -> [a] -> [b]
map (((Model -> [[String]]) -> Model -> [[String]]
forall a b. (a -> b) -> a -> b
$ Model
model) ((Model -> [[String]]) -> [[String]])
-> (([Signal Bool], Model -> [[String]]) -> Model -> [[String]])
-> ([Signal Bool], Model -> [[String]])
-> [[String]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([Signal Bool], Model -> [[String]]) -> Model -> [[String]]
forall a b. (a, b) -> b
snd) [([Signal Bool], Model -> [[String]])]
sms))

instance Checkable a => Checkable (Gen a) where
  property :: Gen a -> Property
property m :: Gen a
m = Gen ([Signal Bool], Model -> [[String]]) -> Property
P (do a
a <- Gen a
m ; let P m' :: Gen ([Signal Bool], Model -> [[String]])
m' = a -> Property
forall a. Checkable a => a -> Property
property a
a in Gen ([Signal Bool], Model -> [[String]])
m')

instance (Fresh a, ShowModel a, Checkable b) => Checkable (a -> b) where
  property :: (a -> b) -> Property
property f :: a -> b
f = Gen a -> (a -> b) -> Property
forall a b.
(ShowModel a, Checkable b) =>
Gen a -> (a -> b) -> Property
forAll Gen a
forall a. Fresh a => Gen a
fresh a -> b
f

----------------------------------------------------------------
-- quantify

type Model
  = [(String, [String])]

name :: Signal a -> String
name :: Signal a -> String
name (Signal s :: Symbol
s) =
  case Symbol -> S Symbol
unsymbol Symbol
s of
    VarBool v :: String
v -> String
v
    VarInt v :: String
v  -> String
v
    _         -> String -> String
forall a. HasCallStack => String -> a
error "no name"

class ShowModel a where
  showModel :: Model -> a -> [String]

instance ShowModel (Signal a) where
  showModel :: Model -> Signal a -> [String]
showModel model :: Model
model sig :: Signal a
sig =
    case String -> Model -> Maybe [String]
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup (Signal a -> String
forall a. Signal a -> String
name Signal a
sig) Model
model of
      Just xs :: [String]
xs -> [String]
xs
      Nothing -> []

instance ShowModel () where
  showModel :: Model -> () -> [String]
showModel model :: Model
model () =
    ["()"]

instance (ShowModel a, ShowModel b) => ShowModel (a, b) where
  showModel :: Model -> (a, b) -> [String]
showModel model :: Model
model (a :: a
a, b :: b
b) =
    (String -> String -> String) -> [String] -> [String] -> [String]
forall a. (String -> String -> a) -> [String] -> [String] -> [a]
zipWith' (\x :: String
x y :: String
y -> "(" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
x String -> String -> String
forall a. [a] -> [a] -> [a]
++ "," String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
y String -> String -> String
forall a. [a] -> [a] -> [a]
++ ")")
      (Model -> a -> [String]
forall a. ShowModel a => Model -> a -> [String]
showModel Model
model a
a) (Model -> b -> [String]
forall a. ShowModel a => Model -> a -> [String]
showModel Model
model b
b)

instance (ShowModel a, ShowModel b, ShowModel c) => ShowModel (a, b, c) where
  showModel :: Model -> (a, b, c) -> [String]
showModel model :: Model
model (a :: a
a, b :: b
b, c :: c
c) =
    (String -> String -> String -> String)
-> [String] -> [String] -> [String] -> [String]
forall a.
(String -> String -> String -> a)
-> [String] -> [String] -> [String] -> [a]
zipWith3' (\x :: String
x y :: String
y z :: String
z -> "(" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
x String -> String -> String
forall a. [a] -> [a] -> [a]
++ "," String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
y String -> String -> String
forall a. [a] -> [a] -> [a]
++ "," String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
z String -> String -> String
forall a. [a] -> [a] -> [a]
++ ")")
      (Model -> a -> [String]
forall a. ShowModel a => Model -> a -> [String]
showModel Model
model a
a) (Model -> b -> [String]
forall a. ShowModel a => Model -> a -> [String]
showModel Model
model b
b) (Model -> c -> [String]
forall a. ShowModel a => Model -> a -> [String]
showModel Model
model c
c)

instance (ShowModel a, ShowModel b, ShowModel c, ShowModel d) => ShowModel (a, b, c, d) where
  showModel :: Model -> (a, b, c, d) -> [String]
showModel model :: Model
model (a :: a
a, b :: b
b, c :: c
c, d :: d
d) =
    (String -> String -> String -> String -> String)
-> [String] -> [String] -> [String] -> [String] -> [String]
forall a.
(String -> String -> String -> String -> a)
-> [String] -> [String] -> [String] -> [String] -> [a]
zipWith4' (\x :: String
x y :: String
y z :: String
z v :: String
v -> "(" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
x String -> String -> String
forall a. [a] -> [a] -> [a]
++ "," String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
y String -> String -> String
forall a. [a] -> [a] -> [a]
++ "," String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
z String -> String -> String
forall a. [a] -> [a] -> [a]
++ "," String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
v String -> String -> String
forall a. [a] -> [a] -> [a]
++ ")")
      (Model -> a -> [String]
forall a. ShowModel a => Model -> a -> [String]
showModel Model
model a
a) (Model -> b -> [String]
forall a. ShowModel a => Model -> a -> [String]
showModel Model
model b
b) (Model -> c -> [String]
forall a. ShowModel a => Model -> a -> [String]
showModel Model
model c
c) (Model -> d -> [String]
forall a. ShowModel a => Model -> a -> [String]
showModel Model
model d
d)

instance (ShowModel a, ShowModel b, ShowModel c, ShowModel d, ShowModel e) => ShowModel (a, b, c, d, e) where
  showModel :: Model -> (a, b, c, d, e) -> [String]
showModel model :: Model
model (a :: a
a, b :: b
b, c :: c
c, d :: d
d, e :: e
e) =
    (String -> String -> String -> String -> String -> String)
-> [String]
-> [String]
-> [String]
-> [String]
-> [String]
-> [String]
forall a.
(String -> String -> String -> String -> String -> a)
-> [String] -> [String] -> [String] -> [String] -> [String] -> [a]
zipWith5' (\x :: String
x y :: String
y z :: String
z v :: String
v w :: String
w -> "(" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
x String -> String -> String
forall a. [a] -> [a] -> [a]
++ "," String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
y String -> String -> String
forall a. [a] -> [a] -> [a]
++ "," String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
z String -> String -> String
forall a. [a] -> [a] -> [a]
++ "," String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
v String -> String -> String
forall a. [a] -> [a] -> [a]
++ "," String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
w String -> String -> String
forall a. [a] -> [a] -> [a]
++ ")")
      (Model -> a -> [String]
forall a. ShowModel a => Model -> a -> [String]
showModel Model
model a
a) (Model -> b -> [String]
forall a. ShowModel a => Model -> a -> [String]
showModel Model
model b
b) (Model -> c -> [String]
forall a. ShowModel a => Model -> a -> [String]
showModel Model
model c
c) (Model -> d -> [String]
forall a. ShowModel a => Model -> a -> [String]
showModel Model
model d
d) (Model -> e -> [String]
forall a. ShowModel a => Model -> a -> [String]
showModel Model
model e
e)

instance (ShowModel a, ShowModel b, ShowModel c, ShowModel d, ShowModel e, ShowModel f) => ShowModel (a, b, c, d, e, f) where
  showModel :: Model -> (a, b, c, d, e, f) -> [String]
showModel model :: Model
model (a :: a
a, b :: b
b, c :: c
c, d :: d
d, e :: e
e, f :: f
f) =
    (String
 -> String -> String -> String -> String -> String -> String)
-> [String]
-> [String]
-> [String]
-> [String]
-> [String]
-> [String]
-> [String]
forall a.
(String -> String -> String -> String -> String -> String -> a)
-> [String]
-> [String]
-> [String]
-> [String]
-> [String]
-> [String]
-> [a]
zipWith6' (\x :: String
x y :: String
y z :: String
z v :: String
v w :: String
w p :: String
p -> "(" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
x String -> String -> String
forall a. [a] -> [a] -> [a]
++ "," String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
y String -> String -> String
forall a. [a] -> [a] -> [a]
++ "," String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
z String -> String -> String
forall a. [a] -> [a] -> [a]
++ "," String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
v String -> String -> String
forall a. [a] -> [a] -> [a]
++ "," String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
w String -> String -> String
forall a. [a] -> [a] -> [a]
++ "," String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
p String -> String -> String
forall a. [a] -> [a] -> [a]
++ ")")
      (Model -> a -> [String]
forall a. ShowModel a => Model -> a -> [String]
showModel Model
model a
a) (Model -> b -> [String]
forall a. ShowModel a => Model -> a -> [String]
showModel Model
model b
b) (Model -> c -> [String]
forall a. ShowModel a => Model -> a -> [String]
showModel Model
model c
c) (Model -> d -> [String]
forall a. ShowModel a => Model -> a -> [String]
showModel Model
model d
d) (Model -> e -> [String]
forall a. ShowModel a => Model -> a -> [String]
showModel Model
model e
e) (Model -> f -> [String]
forall a. ShowModel a => Model -> a -> [String]
showModel Model
model f
f)

instance (ShowModel a, ShowModel b, ShowModel c, ShowModel d, ShowModel e, ShowModel f, ShowModel g) => ShowModel (a, b, c, d, e, f, g) where
  showModel :: Model -> (a, b, c, d, e, f, g) -> [String]
showModel model :: Model
model (a :: a
a, b :: b
b, c :: c
c, d :: d
d, e :: e
e, f :: f
f, g :: g
g) =
    (String
 -> String
 -> String
 -> String
 -> String
 -> String
 -> String
 -> String)
-> [String]
-> [String]
-> [String]
-> [String]
-> [String]
-> [String]
-> [String]
-> [String]
forall a.
(String
 -> String -> String -> String -> String -> String -> String -> a)
-> [String]
-> [String]
-> [String]
-> [String]
-> [String]
-> [String]
-> [String]
-> [a]
zipWith7' (\x :: String
x y :: String
y z :: String
z v :: String
v w :: String
w p :: String
p q :: String
q -> "(" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
x String -> String -> String
forall a. [a] -> [a] -> [a]
++ "," String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
y String -> String -> String
forall a. [a] -> [a] -> [a]
++ "," String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
z String -> String -> String
forall a. [a] -> [a] -> [a]
++ "," String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
v String -> String -> String
forall a. [a] -> [a] -> [a]
++ "," String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
w String -> String -> String
forall a. [a] -> [a] -> [a]
++ "," String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
p String -> String -> String
forall a. [a] -> [a] -> [a]
++ "," String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
q String -> String -> String
forall a. [a] -> [a] -> [a]
++ ")")
      (Model -> a -> [String]
forall a. ShowModel a => Model -> a -> [String]
showModel Model
model a
a) (Model -> b -> [String]
forall a. ShowModel a => Model -> a -> [String]
showModel Model
model b
b) (Model -> c -> [String]
forall a. ShowModel a => Model -> a -> [String]
showModel Model
model c
c) (Model -> d -> [String]
forall a. ShowModel a => Model -> a -> [String]
showModel Model
model d
d) (Model -> e -> [String]
forall a. ShowModel a => Model -> a -> [String]
showModel Model
model e
e) (Model -> f -> [String]
forall a. ShowModel a => Model -> a -> [String]
showModel Model
model f
f) (Model -> g -> [String]
forall a. ShowModel a => Model -> a -> [String]
showModel Model
model g
g)

instance ShowModel a => ShowModel [a] where
  showModel :: Model -> [a] -> [String]
showModel model :: Model
model as :: [a]
as =
    ([String] -> String) -> [[String]] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (\xs :: [String]
xs -> "[" String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat (String -> [String] -> [String]
forall a. a -> [a] -> [a]
intersperse "," [String]
xs)
                    String -> String -> String
forall a. [a] -> [a] -> [a]
++ "]")
      ([[String]] -> [[String]]
forall a. [[a]] -> [[a]]
transpose ((a -> [String]) -> [a] -> [[String]]
forall a b. (a -> b) -> [a] -> [b]
map (Model -> a -> [String]
forall a. ShowModel a => Model -> a -> [String]
showModel Model
model) [a]
as))

instance ShowModel (a -> b) where
  showModel :: Model -> (a -> b) -> [String]
showModel model :: Model
model sig :: a -> b
sig = []

zipWith' :: (String -> String -> a) -> [String] -> [String] -> [a]
zipWith' f :: String -> String -> a
f []     []     = []
zipWith' f :: String -> String -> a
f []     ys :: [String]
ys     = (String -> String -> a) -> [String] -> [String] -> [a]
zipWith' String -> String -> a
f ["?"] [String]
ys
zipWith' f :: String -> String -> a
f xs :: [String]
xs     []     = (String -> String -> a) -> [String] -> [String] -> [a]
zipWith' String -> String -> a
f [String]
xs ["?"]
zipWith' f :: String -> String -> a
f (x :: String
x:xs :: [String]
xs) (y :: String
y:ys :: [String]
ys) = String -> String -> a
f String
x String
y a -> [a] -> [a]
forall a. a -> [a] -> [a]
: (String -> String -> a) -> [String] -> [String] -> [a]
zipWith' String -> String -> a
f [String]
xs [String]
ys

zipWith3' :: (String -> String -> String -> a)
-> [String] -> [String] -> [String] -> [a]
zipWith3' f :: String -> String -> String -> a
f []     []     []     = []
zipWith3' f :: String -> String -> String -> a
f []     ys :: [String]
ys     zs :: [String]
zs     = (String -> String -> String -> a)
-> [String] -> [String] -> [String] -> [a]
zipWith3' String -> String -> String -> a
f ["?"] [String]
ys [String]
zs
zipWith3' f :: String -> String -> String -> a
f xs :: [String]
xs     []     zs :: [String]
zs     = (String -> String -> String -> a)
-> [String] -> [String] -> [String] -> [a]
zipWith3' String -> String -> String -> a
f [String]
xs ["?"] [String]
zs
zipWith3' f :: String -> String -> String -> a
f xs :: [String]
xs     ys :: [String]
ys     []     = (String -> String -> String -> a)
-> [String] -> [String] -> [String] -> [a]
zipWith3' String -> String -> String -> a
f [String]
xs [String]
ys ["?"]
zipWith3' f :: String -> String -> String -> a
f (x :: String
x:xs :: [String]
xs) (y :: String
y:ys :: [String]
ys) (z :: String
z:zs :: [String]
zs) = String -> String -> String -> a
f String
x String
y String
z a -> [a] -> [a]
forall a. a -> [a] -> [a]
: (String -> String -> String -> a)
-> [String] -> [String] -> [String] -> [a]
zipWith3' String -> String -> String -> a
f [String]
xs [String]
ys [String]
zs

zipWith4' :: (String -> String -> String -> String -> a)
-> [String] -> [String] -> [String] -> [String] -> [a]
zipWith4' f :: String -> String -> String -> String -> a
f []     []     []     []     = []
zipWith4' f :: String -> String -> String -> String -> a
f []     ys :: [String]
ys     zs :: [String]
zs     vs :: [String]
vs     = (String -> String -> String -> String -> a)
-> [String] -> [String] -> [String] -> [String] -> [a]
zipWith4' String -> String -> String -> String -> a
f ["?"] [String]
ys [String]
zs [String]
vs
zipWith4' f :: String -> String -> String -> String -> a
f xs :: [String]
xs     []     zs :: [String]
zs     vs :: [String]
vs     = (String -> String -> String -> String -> a)
-> [String] -> [String] -> [String] -> [String] -> [a]
zipWith4' String -> String -> String -> String -> a
f [String]
xs ["?"] [String]
zs [String]
vs
zipWith4' f :: String -> String -> String -> String -> a
f xs :: [String]
xs     ys :: [String]
ys     []     vs :: [String]
vs     = (String -> String -> String -> String -> a)
-> [String] -> [String] -> [String] -> [String] -> [a]
zipWith4' String -> String -> String -> String -> a
f [String]
xs [String]
ys ["?"] [String]
vs
zipWith4' f :: String -> String -> String -> String -> a
f xs :: [String]
xs     ys :: [String]
ys     zs :: [String]
zs     []     = (String -> String -> String -> String -> a)
-> [String] -> [String] -> [String] -> [String] -> [a]
zipWith4' String -> String -> String -> String -> a
f [String]
xs [String]
ys [String]
zs ["?"]
zipWith4' f :: String -> String -> String -> String -> a
f (x :: String
x:xs :: [String]
xs) (y :: String
y:ys :: [String]
ys) (z :: String
z:zs :: [String]
zs) (v :: String
v:vs :: [String]
vs) = String -> String -> String -> String -> a
f String
x String
y String
z String
v a -> [a] -> [a]
forall a. a -> [a] -> [a]
: (String -> String -> String -> String -> a)
-> [String] -> [String] -> [String] -> [String] -> [a]
zipWith4' String -> String -> String -> String -> a
f [String]
xs [String]
ys [String]
zs [String]
vs

zipWith5' :: (String -> String -> String -> String -> String -> a)
-> [String] -> [String] -> [String] -> [String] -> [String] -> [a]
zipWith5' f :: String -> String -> String -> String -> String -> a
f []     []     []     []     []     = []
zipWith5' f :: String -> String -> String -> String -> String -> a
f []     ys :: [String]
ys     zs :: [String]
zs     vs :: [String]
vs     ws :: [String]
ws     = (String -> String -> String -> String -> String -> a)
-> [String] -> [String] -> [String] -> [String] -> [String] -> [a]
zipWith5' String -> String -> String -> String -> String -> a
f ["?"] [String]
ys [String]
zs [String]
vs [String]
ws
zipWith5' f :: String -> String -> String -> String -> String -> a
f xs :: [String]
xs     []     zs :: [String]
zs     vs :: [String]
vs     ws :: [String]
ws     = (String -> String -> String -> String -> String -> a)
-> [String] -> [String] -> [String] -> [String] -> [String] -> [a]
zipWith5' String -> String -> String -> String -> String -> a
f [String]
xs ["?"] [String]
zs [String]
vs [String]
ws
zipWith5' f :: String -> String -> String -> String -> String -> a
f xs :: [String]
xs     ys :: [String]
ys     []     vs :: [String]
vs     ws :: [String]
ws     = (String -> String -> String -> String -> String -> a)
-> [String] -> [String] -> [String] -> [String] -> [String] -> [a]
zipWith5' String -> String -> String -> String -> String -> a
f [String]
xs [String]
ys ["?"] [String]
vs [String]
ws
zipWith5' f :: String -> String -> String -> String -> String -> a
f xs :: [String]
xs     ys :: [String]
ys     zs :: [String]
zs     []     ws :: [String]
ws     = (String -> String -> String -> String -> String -> a)
-> [String] -> [String] -> [String] -> [String] -> [String] -> [a]
zipWith5' String -> String -> String -> String -> String -> a
f [String]
xs [String]
ys [String]
zs ["?"] [String]
ws
zipWith5' f :: String -> String -> String -> String -> String -> a
f xs :: [String]
xs     ys :: [String]
ys     zs :: [String]
zs     vs :: [String]
vs     []     = (String -> String -> String -> String -> String -> a)
-> [String] -> [String] -> [String] -> [String] -> [String] -> [a]
zipWith5' String -> String -> String -> String -> String -> a
f [String]
xs [String]
ys [String]
zs [String]
vs ["?"]
zipWith5' f :: String -> String -> String -> String -> String -> a
f (x :: String
x:xs :: [String]
xs) (y :: String
y:ys :: [String]
ys) (z :: String
z:zs :: [String]
zs) (v :: String
v:vs :: [String]
vs) (w :: String
w:ws :: [String]
ws) = String -> String -> String -> String -> String -> a
f String
x String
y String
z String
v String
w a -> [a] -> [a]
forall a. a -> [a] -> [a]
: (String -> String -> String -> String -> String -> a)
-> [String] -> [String] -> [String] -> [String] -> [String] -> [a]
zipWith5' String -> String -> String -> String -> String -> a
f [String]
xs [String]
ys [String]
zs [String]
vs [String]
ws

zipWith6' :: (String -> String -> String -> String -> String -> String -> a)
-> [String]
-> [String]
-> [String]
-> [String]
-> [String]
-> [String]
-> [a]
zipWith6' f :: String -> String -> String -> String -> String -> String -> a
f []     []     []     []     []     []     = []
zipWith6' f :: String -> String -> String -> String -> String -> String -> a
f []     ys :: [String]
ys     zs :: [String]
zs     vs :: [String]
vs     ws :: [String]
ws     ps :: [String]
ps     = (String -> String -> String -> String -> String -> String -> a)
-> [String]
-> [String]
-> [String]
-> [String]
-> [String]
-> [String]
-> [a]
zipWith6' String -> String -> String -> String -> String -> String -> a
f ["?"] [String]
ys [String]
zs [String]
vs [String]
ws [String]
ps
zipWith6' f :: String -> String -> String -> String -> String -> String -> a
f xs :: [String]
xs     []     zs :: [String]
zs     vs :: [String]
vs     ws :: [String]
ws     ps :: [String]
ps     = (String -> String -> String -> String -> String -> String -> a)
-> [String]
-> [String]
-> [String]
-> [String]
-> [String]
-> [String]
-> [a]
zipWith6' String -> String -> String -> String -> String -> String -> a
f [String]
xs ["?"] [String]
zs [String]
vs [String]
ws [String]
ps
zipWith6' f :: String -> String -> String -> String -> String -> String -> a
f xs :: [String]
xs     ys :: [String]
ys     []     vs :: [String]
vs     ws :: [String]
ws     ps :: [String]
ps     = (String -> String -> String -> String -> String -> String -> a)
-> [String]
-> [String]
-> [String]
-> [String]
-> [String]
-> [String]
-> [a]
zipWith6' String -> String -> String -> String -> String -> String -> a
f [String]
xs [String]
ys ["?"] [String]
vs [String]
ws [String]
ps
zipWith6' f :: String -> String -> String -> String -> String -> String -> a
f xs :: [String]
xs     ys :: [String]
ys     zs :: [String]
zs     []     ws :: [String]
ws     ps :: [String]
ps     = (String -> String -> String -> String -> String -> String -> a)
-> [String]
-> [String]
-> [String]
-> [String]
-> [String]
-> [String]
-> [a]
zipWith6' String -> String -> String -> String -> String -> String -> a
f [String]
xs [String]
ys [String]
zs ["?"] [String]
ws [String]
ps
zipWith6' f :: String -> String -> String -> String -> String -> String -> a
f xs :: [String]
xs     ys :: [String]
ys     zs :: [String]
zs     vs :: [String]
vs     []     ps :: [String]
ps     = (String -> String -> String -> String -> String -> String -> a)
-> [String]
-> [String]
-> [String]
-> [String]
-> [String]
-> [String]
-> [a]
zipWith6' String -> String -> String -> String -> String -> String -> a
f [String]
xs [String]
ys [String]
zs [String]
vs ["?"] [String]
ps
zipWith6' f :: String -> String -> String -> String -> String -> String -> a
f xs :: [String]
xs     ys :: [String]
ys     zs :: [String]
zs     vs :: [String]
vs     ws :: [String]
ws     []     = (String -> String -> String -> String -> String -> String -> a)
-> [String]
-> [String]
-> [String]
-> [String]
-> [String]
-> [String]
-> [a]
zipWith6' String -> String -> String -> String -> String -> String -> a
f [String]
xs [String]
ys [String]
zs [String]
vs [String]
ws ["?"]
zipWith6' f :: String -> String -> String -> String -> String -> String -> a
f (x :: String
x:xs :: [String]
xs) (y :: String
y:ys :: [String]
ys) (z :: String
z:zs :: [String]
zs) (v :: String
v:vs :: [String]
vs) (w :: String
w:ws :: [String]
ws) (p :: String
p:ps :: [String]
ps) = String -> String -> String -> String -> String -> String -> a
f String
x String
y String
z String
v String
w String
p a -> [a] -> [a]
forall a. a -> [a] -> [a]
: (String -> String -> String -> String -> String -> String -> a)
-> [String]
-> [String]
-> [String]
-> [String]
-> [String]
-> [String]
-> [a]
zipWith6' String -> String -> String -> String -> String -> String -> a
f [String]
xs [String]
ys [String]
zs [String]
vs [String]
ws [String]
ps

zipWith7' :: (String
 -> String -> String -> String -> String -> String -> String -> a)
-> [String]
-> [String]
-> [String]
-> [String]
-> [String]
-> [String]
-> [String]
-> [a]
zipWith7' f :: String
-> String -> String -> String -> String -> String -> String -> a
f []     []     []     []     []     []     []     = []
zipWith7' f :: String
-> String -> String -> String -> String -> String -> String -> a
f []     ys :: [String]
ys     zs :: [String]
zs     vs :: [String]
vs     ws :: [String]
ws     ps :: [String]
ps     qs :: [String]
qs     = (String
 -> String -> String -> String -> String -> String -> String -> a)
-> [String]
-> [String]
-> [String]
-> [String]
-> [String]
-> [String]
-> [String]
-> [a]
zipWith7' String
-> String -> String -> String -> String -> String -> String -> a
f ["?"] [String]
ys [String]
zs [String]
vs [String]
ws [String]
ps [String]
qs
zipWith7' f :: String
-> String -> String -> String -> String -> String -> String -> a
f xs :: [String]
xs     []     zs :: [String]
zs     vs :: [String]
vs     ws :: [String]
ws     ps :: [String]
ps     qs :: [String]
qs     = (String
 -> String -> String -> String -> String -> String -> String -> a)
-> [String]
-> [String]
-> [String]
-> [String]
-> [String]
-> [String]
-> [String]
-> [a]
zipWith7' String
-> String -> String -> String -> String -> String -> String -> a
f [String]
xs ["?"] [String]
zs [String]
vs [String]
ws [String]
ps [String]
qs
zipWith7' f :: String
-> String -> String -> String -> String -> String -> String -> a
f xs :: [String]
xs     ys :: [String]
ys     []     vs :: [String]
vs     ws :: [String]
ws     ps :: [String]
ps     qs :: [String]
qs     = (String
 -> String -> String -> String -> String -> String -> String -> a)
-> [String]
-> [String]
-> [String]
-> [String]
-> [String]
-> [String]
-> [String]
-> [a]
zipWith7' String
-> String -> String -> String -> String -> String -> String -> a
f [String]
xs [String]
ys ["?"] [String]
vs [String]
ws [String]
ps [String]
qs
zipWith7' f :: String
-> String -> String -> String -> String -> String -> String -> a
f xs :: [String]
xs     ys :: [String]
ys     zs :: [String]
zs     []     ws :: [String]
ws     ps :: [String]
ps     qs :: [String]
qs     = (String
 -> String -> String -> String -> String -> String -> String -> a)
-> [String]
-> [String]
-> [String]
-> [String]
-> [String]
-> [String]
-> [String]
-> [a]
zipWith7' String
-> String -> String -> String -> String -> String -> String -> a
f [String]
xs [String]
ys [String]
zs ["?"] [String]
ws [String]
ps [String]
qs
zipWith7' f :: String
-> String -> String -> String -> String -> String -> String -> a
f xs :: [String]
xs     ys :: [String]
ys     zs :: [String]
zs     vs :: [String]
vs     []     ps :: [String]
ps     qs :: [String]
qs     = (String
 -> String -> String -> String -> String -> String -> String -> a)
-> [String]
-> [String]
-> [String]
-> [String]
-> [String]
-> [String]
-> [String]
-> [a]
zipWith7' String
-> String -> String -> String -> String -> String -> String -> a
f [String]
xs [String]
ys [String]
zs [String]
vs ["?"] [String]
ps [String]
qs
zipWith7' f :: String
-> String -> String -> String -> String -> String -> String -> a
f xs :: [String]
xs     ys :: [String]
ys     zs :: [String]
zs     vs :: [String]
vs     ws :: [String]
ws     []     qs :: [String]
qs     = (String
 -> String -> String -> String -> String -> String -> String -> a)
-> [String]
-> [String]
-> [String]
-> [String]
-> [String]
-> [String]
-> [String]
-> [a]
zipWith7' String
-> String -> String -> String -> String -> String -> String -> a
f [String]
xs [String]
ys [String]
zs [String]
vs [String]
ws ["?"] [String]
qs
zipWith7' f :: String
-> String -> String -> String -> String -> String -> String -> a
f xs :: [String]
xs     ys :: [String]
ys     zs :: [String]
zs     vs :: [String]
vs     ws :: [String]
ws     ps :: [String]
ps     []     = (String
 -> String -> String -> String -> String -> String -> String -> a)
-> [String]
-> [String]
-> [String]
-> [String]
-> [String]
-> [String]
-> [String]
-> [a]
zipWith7' String
-> String -> String -> String -> String -> String -> String -> a
f [String]
xs [String]
ys [String]
zs [String]
vs [String]
ws [String]
ps ["?"]
zipWith7' f :: String
-> String -> String -> String -> String -> String -> String -> a
f (x :: String
x:xs :: [String]
xs) (y :: String
y:ys :: [String]
ys) (z :: String
z:zs :: [String]
zs) (v :: String
v:vs :: [String]
vs) (w :: String
w:ws :: [String]
ws) (p :: String
p:ps :: [String]
ps) (q :: String
q:qs :: [String]
qs) = String
-> String -> String -> String -> String -> String -> String -> a
f String
x String
y String
z String
v String
w String
p String
q a -> [a] -> [a]
forall a. a -> [a] -> [a]
: (String
 -> String -> String -> String -> String -> String -> String -> a)
-> [String]
-> [String]
-> [String]
-> [String]
-> [String]
-> [String]
-> [String]
-> [a]
zipWith7' String
-> String -> String -> String -> String -> String -> String -> a
f [String]
xs [String]
ys [String]
zs [String]
vs [String]
ws [String]
ps [String]
qs

forAll :: (ShowModel a, Checkable b) => Gen a -> (a -> b) -> Property
forAll :: Gen a -> (a -> b) -> Property
forAll gen :: Gen a
gen body :: a -> b
body = Gen ([Signal Bool], Model -> [[String]]) -> Property
P (Gen ([Signal Bool], Model -> [[String]]) -> Property)
-> Gen ([Signal Bool], Model -> [[String]]) -> Property
forall a b. (a -> b) -> a -> b
$
  do a
a <- Gen a
gen
     let P m :: Gen ([Signal Bool], Model -> [[String]])
m = b -> Property
forall a. Checkable a => a -> Property
property (a -> b
body a
a)
     (sigs :: [Signal Bool]
sigs, mod :: Model -> [[String]]
mod) <- Gen ([Signal Bool], Model -> [[String]])
m
     ([Signal Bool], Model -> [[String]])
-> Gen ([Signal Bool], Model -> [[String]])
forall (m :: * -> *) a. Monad m => a -> m a
return ([Signal Bool]
sigs, \model :: Model
model -> Model -> a -> [String]
forall a. ShowModel a => Model -> a -> [String]
showModel Model
model a
a [String] -> [[String]] -> [[String]]
forall a. a -> [a] -> [a]
: Model -> [[String]]
mod Model
model)

----------------------------------------------------------------
-- evaluate

properties :: Checkable a => a -> IO ([Signal Bool], Model -> [[String]])
properties :: a -> IO ([Signal Bool], Model -> [[String]])
properties a :: a
a = Gen ([Signal Bool], Model -> [[String]])
-> IO ([Signal Bool], Model -> [[String]])
forall a. Gen a -> IO a
generate Gen ([Signal Bool], Model -> [[String]])
gen
 where
  (P gen :: Gen ([Signal Bool], Model -> [[String]])
gen) = a -> Property
forall a. Checkable a => a -> Property
property a
a

----------------------------------------------------------------
-- bweeuh

liftM6 :: (t -> t -> t -> t -> t -> t -> b)
-> m t -> m t -> m t -> m t -> m t -> m t -> m b
liftM6 f :: t -> t -> t -> t -> t -> t -> b
f g1 :: m t
g1 g2 :: m t
g2 g3 :: m t
g3 g4 :: m t
g4 g5 :: m t
g5 g6 :: m t
g6 =
  do t
a1 <- m t
g1
     t
a2 <- m t
g2
     t
a3 <- m t
g3
     t
a4 <- m t
g4
     t
a5 <- m t
g5
     t
a6 <- m t
g6
     b -> m b
forall (m :: * -> *) a. Monad m => a -> m a
return (t -> t -> t -> t -> t -> t -> b
f t
a1 t
a2 t
a3 t
a4 t
a5 t
a6)

liftM7 :: (t -> t -> t -> t -> t -> t -> t -> b)
-> m t -> m t -> m t -> m t -> m t -> m t -> m t -> m b
liftM7 f :: t -> t -> t -> t -> t -> t -> t -> b
f g1 :: m t
g1 g2 :: m t
g2 g3 :: m t
g3 g4 :: m t
g4 g5 :: m t
g5 g6 :: m t
g6 g7 :: m t
g7 =
  do t
a1 <- m t
g1
     t
a2 <- m t
g2
     t
a3 <- m t
g3
     t
a4 <- m t
g4
     t
a5 <- m t
g5
     t
a6 <- m t
g6
     t
a7 <- m t
g7
     b -> m b
forall (m :: * -> *) a. Monad m => a -> m a
return (t -> t -> t -> t -> t -> t -> t -> b
f t
a1 t
a2 t
a3 t
a4 t
a5 t
a6 t
a7)

----------------------------------------------------------------
-- the end.