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 Monad
( liftM2
, liftM3
, liftM4
, liftM5
)
import List
( intersperse
, transpose
)
import Data.IORef
import System.IO.Unsafe
newtype Gen a
= Gen (Tree Int -> a)
instance Functor Gen where
fmap f (Gen m) = Gen (\t -> f (m t))
instance Monad Gen where
return a =
Gen (\t -> a)
Gen m >>= k =
Gen (\(Fork _ t1 t2) -> let a = m t1 ; Gen m2 = k a in m2 t2)
generate :: Gen a -> IO a
generate (Gen m) =
do t <- newTree
return (m t)
data Tree a
= Fork a (Tree a) (Tree a)
newTree :: IO (Tree Int)
newTree =
do var <- newIORef 0
tree var
where
tree var = unsafeInterleaveIO $
do n <- new var
t1 <- tree var
t2 <- tree var
return (Fork n t1 t2)
new var = unsafeInterleaveIO $
do n <- readIORef var
let n' = n+1
n' `seq` writeIORef var n'
return n
class Fresh a where
fresh :: Gen a
instance Fresh () where
fresh = return ()
instance ConstructiveSig a => Fresh (Signal a) where
fresh = Gen (\(Fork n _ _) -> varSig ("i" ++ show n))
instance (Fresh a, Fresh b) => Fresh (a,b) where
fresh = liftM2 (,) fresh fresh
instance (Fresh a, Fresh b, Fresh c) => Fresh (a,b,c) where
fresh = liftM3 (,,) fresh fresh fresh
instance (Fresh a, Fresh b, Fresh c, Fresh d) => Fresh (a,b,c,d) where
fresh = liftM4 (,,,) fresh fresh fresh fresh
instance (Fresh a, Fresh b, Fresh c, Fresh d, Fresh e) => Fresh (a,b,c,d,e) where
fresh = liftM5 (,,,,) fresh fresh fresh fresh fresh
instance (Fresh a, Fresh b, Fresh c, Fresh d, Fresh e, Fresh f) => Fresh (a,b,c,d,e,f) where
fresh = liftM6 (,,,,,) fresh fresh fresh fresh fresh 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 = liftM7 (,,,,,,) fresh fresh fresh fresh fresh fresh 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 = ifThenElse
instance CoFresh () where
cofresh gen =
do b <- gen
return (\_ -> b)
instance ChoiceWithSig a => CoFresh (Signal a) where
cofresh gen =
do b1 <- gen
b2 <- gen
return (\a -> ifThenElseWithSig a (b1, b2))
instance (CoFresh a, CoFresh b) => CoFresh (a, b) where
cofresh gen =
do f <- cofresh (cofresh gen)
return (\(a, b) -> f a b)
instance (CoFresh a, CoFresh b, CoFresh c) => CoFresh (a, b, c) where
cofresh gen =
do f <- cofresh (cofresh (cofresh gen))
return (\(a, b, c) -> f a b c)
instance (CoFresh a, CoFresh b, CoFresh c, CoFresh d) => CoFresh (a, b, c, d) where
cofresh gen =
do f <- cofresh (cofresh (cofresh (cofresh gen)))
return (\(a, b, c, d) -> f a b c d)
instance (CoFresh a, CoFresh b, CoFresh c, CoFresh d, CoFresh e) => CoFresh (a, b, c, d, e) where
cofresh gen =
do f <- cofresh (cofresh (cofresh (cofresh (cofresh gen))))
return (\(a, b, c, d, e) -> f a b c d e)
instance (CoFresh a, CoFresh b, CoFresh c, CoFresh d, CoFresh e, CoFresh f) => CoFresh (a, b, c, d, e, f) where
cofresh gen =
do f <- cofresh (cofresh (cofresh (cofresh (cofresh (cofresh gen)))))
return (\(a, b, c, d, e, g) -> f a b c d e 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 =
do f <- cofresh (cofresh (cofresh (cofresh (cofresh (cofresh (cofresh gen))))))
return (\(a, b, c, d, e, g, h) -> f a b c d e g h)
instance (CoFresh a, Choice b, Fresh b) => Fresh (a -> b) where
fresh = cofresh fresh
instance CoFresh a => CoFresh [a] where
cofresh gen =
do fs <- sequence [ cofreshList i gen | i <- [0..] ]
return (\as -> (fs !! length as) as)
instance (Finite a, CoFresh b) => CoFresh (a -> b) where
cofresh gen =
do f <- cofresh gen
return (\g -> f (map g domain))
cofreshList :: (CoFresh a, Choice b, Fresh b) => Int -> Gen b -> Gen ([a] -> b)
cofreshList 0 gen =
do x <- gen
return (\[] -> x)
cofreshList k gen =
do f <- cofreshList (k1) (cofresh gen)
return (\(a:as) -> f as a)
double :: Gen a -> Gen (a,a)
double gen = liftM2 (,) gen gen
triple :: Gen a -> Gen (a,a,a)
triple gen = liftM3 (,,) gen gen gen
list :: Fresh a => Int -> Gen [a]
list n = sequence [ fresh | i <- [1..n] ]
listOf :: Int -> Gen a -> Gen [a]
listOf n gen = sequence [ gen | i <- [1..n] ]
results :: Int -> Gen (a -> b) -> Gen (a -> [b])
results n gen =
do fs <- sequence [ gen | i <- [1..n] ]
return (\a -> map ($ a) fs)
sequential :: (CoFresh a, Fresh b, Choice b) => Int -> Gen (a -> b)
sequential n =
do fb <- fresh
fstate <- results n fresh
let circ inp = (fb inp, fstate inp)
return (loop circ)
where
loop circ a = b
where
(b, state) = circ (a, delay (zeroList n) (state :: [Signal Bool]))
newtype Property
= P (Gen ([Signal Bool], Model -> [[String]]))
class Checkable a where
property :: a -> Property
instance Checkable Property where
property p = p
instance Checkable Bool where
property b = property (bool b)
instance Checkable a => Checkable (Signal a) where
property (Signal s) = P (return ([Signal s], \_ -> []))
instance Checkable a => Checkable [a] where
property as = P $
do sms <- sequence [ gen | (P gen) <- map property as ]
return (concat (map fst sms), \model -> concat (map (($ model) . snd) sms))
instance Checkable a => Checkable (Gen a) where
property m = P (do a <- m ; let P m' = property a in m')
instance (Fresh a, ShowModel a, Checkable b) => Checkable (a -> b) where
property f = forAll fresh f
type Model
= [(String, [String])]
name :: Signal a -> String
name (Signal s) =
case unsymbol s of
VarBool v -> v
VarInt v -> v
_ -> error "no name"
class ShowModel a where
showModel :: Model -> a -> [String]
instance ShowModel (Signal a) where
showModel model sig =
case lookup (name sig) model of
Just xs -> xs
Nothing -> []
instance ShowModel () where
showModel model () =
["()"]
instance (ShowModel a, ShowModel b) => ShowModel (a, b) where
showModel model (a, b) =
zipWith' (\x y -> "(" ++ x ++ "," ++ y ++ ")")
(showModel model a) (showModel model b)
instance (ShowModel a, ShowModel b, ShowModel c) => ShowModel (a, b, c) where
showModel model (a, b, c) =
zipWith3' (\x y z -> "(" ++ x ++ "," ++ y ++ "," ++ z ++ ")")
(showModel model a) (showModel model b) (showModel model c)
instance (ShowModel a, ShowModel b, ShowModel c, ShowModel d) => ShowModel (a, b, c, d) where
showModel model (a, b, c, d) =
zipWith4' (\x y z v -> "(" ++ x ++ "," ++ y ++ "," ++ z ++ "," ++ v ++ ")")
(showModel model a) (showModel model b) (showModel model c) (showModel model 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) =
zipWith5' (\x y z v w -> "(" ++ x ++ "," ++ y ++ "," ++ z ++ "," ++ v ++ "," ++ w ++ ")")
(showModel model a) (showModel model b) (showModel model c) (showModel model d) (showModel model 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) =
zipWith6' (\x y z v w p -> "(" ++ x ++ "," ++ y ++ "," ++ z ++ "," ++ v ++ "," ++ w ++ "," ++ p ++ ")")
(showModel model a) (showModel model b) (showModel model c) (showModel model d) (showModel model e) (showModel model 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) =
zipWith7' (\x y z v w p q -> "(" ++ x ++ "," ++ y ++ "," ++ z ++ "," ++ v ++ "," ++ w ++ "," ++ p ++ "," ++ q ++ ")")
(showModel model a) (showModel model b) (showModel model c) (showModel model d) (showModel model e) (showModel model f) (showModel model g)
instance ShowModel a => ShowModel [a] where
showModel model as =
map (\xs -> "[" ++ concat (intersperse "," xs)
++ "]")
(transpose (map (showModel model) as))
instance ShowModel (a -> b) where
showModel model sig = []
zipWith' f [] [] = []
zipWith' f [] ys = zipWith' f ["?"] ys
zipWith' f xs [] = zipWith' f xs ["?"]
zipWith' f (x:xs) (y:ys) = f x y : zipWith' f xs ys
zipWith3' f [] [] [] = []
zipWith3' f [] ys zs = zipWith3' f ["?"] ys zs
zipWith3' f xs [] zs = zipWith3' f xs ["?"] zs
zipWith3' f xs ys [] = zipWith3' f xs ys ["?"]
zipWith3' f (x:xs) (y:ys) (z:zs) = f x y z : zipWith3' f xs ys zs
zipWith4' f [] [] [] [] = []
zipWith4' f [] ys zs vs = zipWith4' f ["?"] ys zs vs
zipWith4' f xs [] zs vs = zipWith4' f xs ["?"] zs vs
zipWith4' f xs ys [] vs = zipWith4' f xs ys ["?"] vs
zipWith4' f xs ys zs [] = zipWith4' f xs ys zs ["?"]
zipWith4' f (x:xs) (y:ys) (z:zs) (v:vs) = f x y z v : zipWith4' f xs ys zs vs
zipWith5' f [] [] [] [] [] = []
zipWith5' f [] ys zs vs ws = zipWith5' f ["?"] ys zs vs ws
zipWith5' f xs [] zs vs ws = zipWith5' f xs ["?"] zs vs ws
zipWith5' f xs ys [] vs ws = zipWith5' f xs ys ["?"] vs ws
zipWith5' f xs ys zs [] ws = zipWith5' f xs ys zs ["?"] ws
zipWith5' f xs ys zs vs [] = zipWith5' f xs ys zs vs ["?"]
zipWith5' f (x:xs) (y:ys) (z:zs) (v:vs) (w:ws) = f x y z v w : zipWith5' f xs ys zs vs ws
zipWith6' f [] [] [] [] [] [] = []
zipWith6' f [] ys zs vs ws ps = zipWith6' f ["?"] ys zs vs ws ps
zipWith6' f xs [] zs vs ws ps = zipWith6' f xs ["?"] zs vs ws ps
zipWith6' f xs ys [] vs ws ps = zipWith6' f xs ys ["?"] vs ws ps
zipWith6' f xs ys zs [] ws ps = zipWith6' f xs ys zs ["?"] ws ps
zipWith6' f xs ys zs vs [] ps = zipWith6' f xs ys zs vs ["?"] ps
zipWith6' f xs ys zs vs ws [] = zipWith6' f xs ys zs vs ws ["?"]
zipWith6' f (x:xs) (y:ys) (z:zs) (v:vs) (w:ws) (p:ps) = f x y z v w p : zipWith6' f xs ys zs vs ws ps
zipWith7' f [] [] [] [] [] [] [] = []
zipWith7' f [] ys zs vs ws ps qs = zipWith7' f ["?"] ys zs vs ws ps qs
zipWith7' f xs [] zs vs ws ps qs = zipWith7' f xs ["?"] zs vs ws ps qs
zipWith7' f xs ys [] vs ws ps qs = zipWith7' f xs ys ["?"] vs ws ps qs
zipWith7' f xs ys zs [] ws ps qs = zipWith7' f xs ys zs ["?"] ws ps qs
zipWith7' f xs ys zs vs [] ps qs = zipWith7' f xs ys zs vs ["?"] ps qs
zipWith7' f xs ys zs vs ws [] qs = zipWith7' f xs ys zs vs ws ["?"] qs
zipWith7' f xs ys zs vs ws ps [] = zipWith7' f xs ys zs vs ws ps ["?"]
zipWith7' f (x:xs) (y:ys) (z:zs) (v:vs) (w:ws) (p:ps) (q:qs) = f x y z v w p q : zipWith7' f xs ys zs vs ws ps qs
forAll :: (ShowModel a, Checkable b) => Gen a -> (a -> b) -> Property
forAll gen body = P $
do a <- gen
let P m = property (body a)
(sigs, mod) <- m
return (sigs, \model -> showModel model a : mod model)
properties :: Checkable a => a -> IO ([Signal Bool], Model -> [[String]])
properties a = generate gen
where
(P gen) = property a
liftM6 f g1 g2 g3 g4 g5 g6 =
do a1 <- g1
a2 <- g2
a3 <- g3
a4 <- g4
a5 <- g5
a6 <- g6
return (f a1 a2 a3 a4 a5 a6)
liftM7 f g1 g2 g3 g4 g5 g6 g7 =
do a1 <- g1
a2 <- g2
a3 <- g3
a4 <- g4
a5 <- g5
a6 <- g6
a7 <- g7
return (f a1 a2 a3 a4 a5 a6 a7)