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
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)
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
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
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)
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] ]
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]))
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
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)
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
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)