module Test.Utils where
import Test.HUnit
import Test.QuickCheck
import Data.Comp.Term
import Data.Comp.Dag
import Data.Comp.Equality
import Data.Comp.Show
import Data.Traversable
testAllEq' :: (Traversable f, Show a, Eq a) => [Term f] -> (Term f -> a) -> (Dag f -> a) -> Assertion
testAllEq' trees f1 f2 = mapM_ run trees
where run t = do d <- reifyDag t
f1 t @=? f2 d
testAllDagEq' :: (Traversable f, EqF g, ShowF g, Traversable g) => [Term f] -> (Dag f -> Dag g) -> (Dag f -> Dag g) -> Assertion
testAllDagEq' trees f1 f2 = mapM_ run trees
where run t = do d <- reifyDag t
assertBool (show (f1 d) ++ " =iso= " ++ show (f2 d)) (f1 d `iso` f2 d)
testAllDagBisim' :: (Traversable f, EqF g, ShowF g, Traversable g) => [Term f] -> (Dag f -> Dag g) -> (Dag f -> Dag g) -> Assertion
testAllDagBisim' trees f1 f2 = mapM_ run trees
where run t = do d <- reifyDag t
assertBool (show (f1 d) ++ " =bisim= " ++ show (f2 d)) (f1 d `bisim` f2 d)
testAllDag' :: (Traversable f, Traversable g) => (Dag g -> Bool) -> (Dag g -> String) -> [Term f] -> (Dag f -> Dag g) -> Assertion
testAllDag' p message trees f1 = mapM_ run trees
where run t = do d <- reifyDag t
assertBool (message (f1 d)) (p (f1 d))
testAllDag2' :: (Traversable f, Traversable g) => (Dag g -> Dag g -> Bool) -> (Dag g -> Dag g -> String) -> [Term f] -> (Dag f -> Dag g) -> (Dag f -> Dag g) -> Assertion
testAllDag2' p message trees f1 f2 = mapM_ run trees
where run t = do d <- reifyDag t
assertBool (message (f1 d) (f2 d)) (p (f1 d) (f2 d))
testAllEq :: (Traversable f, Show a, Eq a) => [Term f] -> (Term f -> a) -> (Dag f -> a) -> Property
testAllEq trees f1 f2 = conjoin $ map run trees
where run t = ioProperty $ do
d <- reifyDag t
return (f1 t === f2 d)