diff --git a/Setup.hs b/Setup.hs --- a/Setup.hs +++ b/Setup.hs diff --git a/compdata-dags.cabal b/compdata-dags.cabal --- a/compdata-dags.cabal +++ b/compdata-dags.cabal @@ -1,11 +1,11 @@ Name: compdata-dags -Version: 0.1 +Version: 0.2 Synopsis: Compositional Data Types on DAGs Description: This library implements recursion schemes on directed acyclic graphs. The recursion schemes are explained in detail in the paper /Generalising Tree Traversals to DAGs/ - (). + (). Category: Generics @@ -27,11 +27,14 @@ library Exposed-Modules: Data.Comp.AG + Data.Comp.PAG Data.Comp.Dag Data.Comp.Dag.AG + Data.Comp.Dag.PAG Other-Modules: Data.Comp.Dag.Internal Data.Comp.AG.Internal - Build-Depends: base >= 4.7, base < 5, compdata == 0.9.*, projection, unordered-containers, + Data.Comp.PAG.Internal + Build-Depends: base >= 4.7, base < 5, compdata == 0.10.*, unordered-containers, mtl, containers, vector hs-source-dirs: src ghc-options: -W @@ -41,9 +44,9 @@ Type: exitcode-stdio-1.0 Main-is: RunTests.hs hs-source-dirs: tests examples src - Build-Depends: base >= 4.7, base < 5, compdata == 0.9.*, projection, unordered-containers, - mtl, containers, vector, test-framework-hunit, HUnit, test-framework, QuickCheck, - test-framework-quickcheck2 + Build-Depends: base >= 4.7, base < 5, compdata == 0.10.*, unordered-containers, + mtl, containers, vector, test-framework-hunit, HUnit, test-framework, + QuickCheck >= 2 && < 2.8, test-framework-quickcheck2 >= 0.3 source-repository head diff --git a/examples/Examples/RepminPAG.hs b/examples/Examples/RepminPAG.hs new file mode 100644 --- /dev/null +++ b/examples/Examples/RepminPAG.hs @@ -0,0 +1,52 @@ +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE ImplicitParams #-} +{-# LANGUAGE DeriveFunctor #-} +{-# LANGUAGE DeriveFoldable #-} +{-# LANGUAGE DeriveTraversable #-} + +-- This is an implementation of repmin as a PAG. The use of a PAG +-- allows us to implement repmin such that the result of repmin is a +-- DAG with only one leaf node, which is shared throughout the +-- DAG. This is achieved as follows: instead of only collecting the +-- minimum synthesised attribute and then turning it into an inherited +-- attribute, which propagates the minimum to the leaves of the graph, +-- we construct a single leaf node with the minimum labelling and +-- propagate it downwards as an inherited attribute. + +module Examples.RepminPAG where + +import Data.Comp.PAG +import Data.Comp.Dag +import qualified Data.Comp.Dag.PAG as Dag +import Data.Comp.Term +import Examples.Types +import Data.Comp.Multi.HFunctor + +import Data.Foldable + + +newtype MinS a = MinS {unMinS :: Int} deriving (Eq,Ord,Functor, Foldable, Traversable) +newtype MinI a = MinI a deriving (Functor, Foldable, Traversable) + + +minS :: Syn IntTreeF atts MinS f +minS (Leaf i) = MinS i +minS (Node a b) = MinS $ min (unMinS $ below a) (unMinS $ below b) + +minI :: Inh IntTreeF atts MinI f +minI _ = empty + +rep :: (MinI :< atts) => Syn IntTreeF atts I IntTreeF +rep (Leaf _) = let MinI n = above in I (Hole n) +rep (Node a b) = I $ iNode (Hole $ unI $ below a) (Hole $ unI $ below b) + + +repminG :: Dag IntTreeF -> Dag IntTreeF +repminG = unI . fsnd . Dag.runPAG const (minS |*| rep) minI init + where init (MinS i :*: _) = MinI (iLeaf i) + + +repmin :: Term IntTreeF -> Term IntTreeF +repmin = unI . fsnd . runPAG (minS |*| rep) minI init + where init (MinS i :*: _) = MinI (iLeaf i) + diff --git a/examples/Examples/Types.hs b/examples/Examples/Types.hs --- a/examples/Examples/Types.hs +++ b/examples/Examples/Types.hs @@ -1,7 +1,8 @@ -{-# LANGUAGE DeriveFoldable #-} -{-# LANGUAGE DeriveFunctor #-} -{-# LANGUAGE DeriveTraversable #-} -{-# LANGUAGE TemplateHaskell #-} +{-# LANGUAGE DeriveFoldable #-} +{-# LANGUAGE DeriveFunctor #-} +{-# LANGUAGE DeriveTraversable #-} +{-# LANGUAGE TemplateHaskell #-} +{-# LANGUAGE FlexibleContexts #-} module Examples.Types where diff --git a/src/Data/Comp/AG.hs b/src/Data/Comp/AG.hs --- a/src/Data/Comp/AG.hs +++ b/src/Data/Comp/AG.hs @@ -29,7 +29,7 @@ import Data.Comp.Algebra import Data.Comp.Mapping as I import Data.Comp.Term -import Data.Projection as I +import Data.Comp.Projection as I diff --git a/src/Data/Comp/AG/Internal.hs b/src/Data/Comp/AG/Internal.hs --- a/src/Data/Comp/AG/Internal.hs +++ b/src/Data/Comp/AG/Internal.hs @@ -22,7 +22,7 @@ import Data.Comp.Mapping import Data.Comp.Term -import Data.Projection +import Data.Comp.Projection -- | This function provides access to attributes of the immediate diff --git a/src/Data/Comp/Dag/AG.hs b/src/Data/Comp/Dag/AG.hs --- a/src/Data/Comp/Dag/AG.hs +++ b/src/Data/Comp/Dag/AG.hs @@ -37,7 +37,7 @@ import Data.Comp.Dag import Data.Comp.Dag.Internal import Data.Comp.Mapping as I -import Data.Projection as I +import Data.Comp.Projection as I import Data.Comp.Term import qualified Data.IntMap as IntMap import Data.Maybe diff --git a/src/Data/Comp/Dag/PAG.hs b/src/Data/Comp/Dag/PAG.hs new file mode 100644 --- /dev/null +++ b/src/Data/Comp/Dag/PAG.hs @@ -0,0 +1,204 @@ +{-# LANGUAGE IncoherentInstances #-} +{-# LANGUAGE UndecidableInstances #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE NamedFieldPuns #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE RecursiveDo #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE FlexibleInstances #-} + + +-------------------------------------------------------------------------------- +-- | +-- Module : Data.Comp.Dag.PAG +-- Copyright : (c) 2014 Patrick Bahr, Emil Axelsson +-- License : BSD3 +-- Maintainer : Patrick Bahr +-- Stability : experimental +-- Portability : non-portable (GHC Extensions) +-- +-- This module implements the recursion schemes from module +-- "Data.Comp.PAG" on 'Dag's. In order to deal with the sharing present +-- in 'Dag's, the recursion schemes additionally take an argument of +-- type @d -> d -> d@ that resolves clashing inherited attribute +-- values. +-- +-------------------------------------------------------------------------------- + + +module Data.Comp.Dag.PAG + ( runPAG + , module I + ) where + +import Control.Monad.ST + +import Data.Comp.Dag +import Data.Comp.Dag.Internal +import Data.Comp.Mapping as I +import Data.Comp.Multi.Projection as I +import Data.Comp.PAG.Internal +import qualified Data.Comp.PAG.Internal as I hiding (explicit) +import Data.Comp.Term + +import qualified Data.IntMap as IntMap +import Data.IntMap (IntMap) + +import Data.Vector (MVector) + + +import Data.Maybe +import Data.STRef +import qualified Data.Traversable as Traversable + + +import qualified Data.Vector as Vec +import qualified Data.Vector.Generic.Mutable as MVec + +import Control.Monad.State + + +-- | This function runs an attribute grammar on a dag. The result is +-- the (combined) synthesised attribute at the root of the dag. + +runPAG :: forall f d u g . (Traversable f, Traversable d, Traversable g, Traversable u) + => (forall a . d a -> d a -> d a) -- ^ resolution function for inherited attributes + -> Syn' f (u :*: d) u g -- ^ semantic function of synthesised attributes + -> Inh' f (u :*: d) d g -- ^ semantic function of inherited attributes + -> (forall a . u a -> d (Context g a)) -- ^ initialisation of inherited attributes + -> Dag f -- ^ input term + -> u (Dag g) +runPAG res syn inh dinit Dag {edges,root,nodeCount} = result where + (uFin, result) = runST runM + runM :: forall s . ST s (u Node, u (Dag g)) + runM = mdo + -- construct empty mapping from nodes to inherited attribute values + dmap <- MVec.new nodeCount + MVec.set dmap Nothing + -- allocate mapping from nodes to synthesised attribute values + umap <- MVec.new nodeCount + -- allocate counter for numbering child nodes + count <- newSTRef 0 + -- allocate references represent edges of the target DAG + nextNode <- newSTRef 0 + newEdges <- newSTRef (IntMap.empty :: IntMap (g (Context g Node))) + let -- This function is applied to each edge + iter (node,s) = do + let d = fromJust $ dmapFin Vec.! node + u <- run d s + MVec.unsafeWrite umap node u + -- Runs the AG on an edge with the given input inherited + -- attribute value and produces the output synthesised + -- attribute value along with the rewritten subtree. + run :: d Node -> f (Context f Node) -> ST s (u Node) + run d t = mdo + e <- readSTRef newEdges + n <- readSTRef nextNode + -- apply the semantic functions + let mkFresh = liftM2 (,) (Traversable.mapM freshNode $ explicit syn (u :*: d) unNumbered result) + (Traversable.mapM (Traversable.mapM freshNode) $ explicit inh (u :*: d) unNumbered result) + ((u,m),(Fresh n' e')) = runState mkFresh (Fresh n e) + writeSTRef newEdges e' + writeSTRef nextNode n' + -- recurses into the child nodes and numbers them + let run' :: Context f Node -> ST s (Numbered ((u :*: d) Node)) + run' s = do i <- readSTRef count + writeSTRef count $! (i+1) + let d' = case lookupNumMap' i m of + Nothing -> d + Just d' -> d' + u' <- runF d' s + return (Numbered i (u' :*: d')) + writeSTRef count 0 + result <- Traversable.mapM run' t + return u + -- recurses through the tree structure + runF d (Term t) = run d t + runF d (Hole x) = do + -- we found a node: update the mapping for inherited + -- attribute values + old <- MVec.unsafeRead dmap x + let new = case old of + Just o -> res o d + _ -> d + MVec.unsafeWrite dmap x (Just new) + return (umapFin Vec.! x) + e <- readSTRef newEdges + n <- readSTRef nextNode + let (dFin,Fresh n' e') = runState (Traversable.mapM freshNode $ dinit uFin) (Fresh n e) + writeSTRef newEdges e' + writeSTRef nextNode n' + -- first apply to the root + u <- run dFin root + -- then apply to the edges + mapM_ iter $ IntMap.toList edges + -- finalise the mappings for attribute values and target DAG + dmapFin <- Vec.unsafeFreeze dmap + umapFin <- Vec.unsafeFreeze umap + newEdgesFin <- readSTRef newEdges + newEdgesCount <- readSTRef nextNode + let relabel n = relabelNodes n newEdgesFin newEdgesCount + return (u, fmap relabel u) + + +-- | The state space for the function 'freshNode'. + +data Fresh f = Fresh {nextFreshNode :: Int, freshEdges :: IntMap (f (Context f Node))} + +-- | Allocates a fresh node for the given context. A new edge is store +-- in the state monad that maps the fresh node to the context that was +-- passed to the function. If the context is just a single node, that +-- node is returned. + +freshNode :: Context g Node -> State (Fresh g) Node +freshNode (Hole n) = return n +freshNode (Term t) = do + s <- get + let n = nextFreshNode s + e = freshEdges s + put (s {freshEdges= IntMap.insert n t e, nextFreshNode = n+1 }) + return n + + +-- | This function relabels the nodes of the given dag. Parts that are +-- unreachable from the root are discarded. +relabelNodes :: forall f . Traversable f + => Node + -> IntMap (f (Context f Node)) + -> Int + -> Dag f +relabelNodes root edges nodeCount = runST run where + run :: ST s (Dag f) + run = do + -- allocate counter for generating nodes + curNode <- newSTRef 0 + newEdges <- newSTRef IntMap.empty -- the new graph + -- construct empty mapping for mapping old nodes to new nodes + newNodes :: MVector s (Maybe Int) <- MVec.new nodeCount + MVec.set newNodes Nothing + let -- Replaces node in the old graph with a node in the new + -- graph. This function is applied to all nodes reachable + -- from the given node as well. + build :: Node -> ST s Node + build node = do + -- check whether we have already constructed a new node + -- for the given node + mnewNode <- MVec.unsafeRead newNodes node + case mnewNode of + Just newNode -> return newNode + Nothing -> do + -- Create a new node and call build recursively + newNode <- readSTRef curNode + writeSTRef curNode $! (newNode+1) + MVec.unsafeWrite newNodes node (Just newNode) + f' <- Traversable.mapM (Traversable.mapM build) (edges IntMap.! node) + modifySTRef newEdges (IntMap.insert newNode f') + return newNode + -- start relabelling from the root + root' <- Traversable.mapM (Traversable.mapM build) (edges IntMap.! root) + -- collect the final edges mapping and node count + edges' <- readSTRef newEdges + nodeCount' <- readSTRef curNode + return Dag {edges = edges', root = root', nodeCount = nodeCount'} diff --git a/src/Data/Comp/PAG.hs b/src/Data/Comp/PAG.hs new file mode 100644 --- /dev/null +++ b/src/Data/Comp/PAG.hs @@ -0,0 +1,59 @@ +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeOperators #-} + + +-------------------------------------------------------------------------------- +-- | +-- Module : Data.Comp.PAG +-- Copyright : (c) 2014 Patrick Bahr, Emil Axelsson +-- License : BSD3 +-- Maintainer : Patrick Bahr +-- Stability : experimental +-- Portability : non-portable (GHC Extensions) +-- +-- This module implements recursion schemes derived from attribute +-- grammars. The variant implemented in this module, called parametric +-- attribute grammars, generalises both attribute grammars and +-- attribute grammars with rewrite function (as implemented in +-- "Data.Comp.AG"). +-- +-------------------------------------------------------------------------------- + +module Data.Comp.PAG + ( runPAG + , module I + ) where + +import Data.Comp.PAG.Internal +import qualified Data.Comp.PAG.Internal as I hiding (explicit) +import Data.Comp.Algebra +import Data.Comp.Mapping as I +import Data.Comp.Term +import Data.Comp.Multi.Projection as I + + + + +-- | This function runs a parametric attribute grammar on a term. The +-- result is the (combined) synthesised attribute at the root of the +-- term. + +runPAG :: forall f u d g . (Traversable f, Functor g, Functor d, Functor u) + => Syn' f (u :*: d) u g -- ^ semantic function of synthesised attributes + -> Inh' f (u :*: d) d g -- ^ semantic function of inherited attributes + -> (forall a . u a -> d (Context g a)) -- ^ initialisation of inherited attributes + -> Term f -- ^ input term + -> u (Term g) +runPAG up down dinit t = uFin where + uFin = run dFin t + dFin = fmap appCxt $ dinit uFin + run :: d (Term g) -> Term f -> u (Term g) + run d (Term t) = u where + t' = fmap bel $ number t + bel (Numbered i s) = + let d' = lookupNumMap d i m + in Numbered i (run d' s :*: d') + m = fmap (fmap appCxt) $ explicit down (u :*: d) unNumbered t' + u = fmap appCxt $ explicit up (u :*: d) unNumbered t' diff --git a/src/Data/Comp/PAG/Internal.hs b/src/Data/Comp/PAG/Internal.hs new file mode 100644 --- /dev/null +++ b/src/Data/Comp/PAG/Internal.hs @@ -0,0 +1,98 @@ +{-# LANGUAGE ImplicitParams #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE Rank2Types #-} +{-# LANGUAGE TypeOperators #-} + +-------------------------------------------------------------------------------- +-- | +-- Module : Data.Comp.PAG.Internal +-- Copyright : (c) 2014 Patrick Bahr, Emil Axelsson +-- License : BSD3 +-- Maintainer : Patrick Bahr +-- Stability : experimental +-- Portability : non-portable (GHC Extensions) +-- +-- This module defines the types for parametric attribute grammars +-- along with some utility functions. +-- +-------------------------------------------------------------------------------- + +module Data.Comp.PAG.Internal + ( module Data.Comp.PAG.Internal + , module I + ) where + + +import Data.Comp.Mapping +import Data.Comp.Term +import Data.Comp.Multi.Projection +import Data.Comp.AG.Internal as I (explicit) + +-- | This function provides access to attributes of the immediate +-- children of the current node. + +below :: (?below :: child -> q a, p :< q) => child -> p a +below = pr . ?below + +-- | This function provides access to attributes of the current node + +above :: (?above :: q a, p :< q) => p a +above = pr ?above + + +-- | The type of semantic functions for synthesised attributes. For +-- defining semantic functions use the type 'Syn', which includes the +-- synthesised attribute that is defined by the semantic function into +-- the available attributes. + +type Syn' f p q g = forall child a . (?below :: child -> p a, ?above :: p a) => f child -> q (Context g a) + +-- | The type of semantic functions for synthesised attributes. +type Syn f p q g = (q :< p) => Syn' f p q g + +-- | Combines the semantic functions for two synthesised attributes to +-- form a semantic function for the compound attribute consisting of +-- the two original attributes. + +prodSyn :: (p :< c, q :< c) => Syn f c p g -> Syn f c q g -> Syn f c (p :*: q) g +prodSyn sp sq t = (sp t :*: sq t) + + +-- | Combines the semantic functions for two synthesised attributes to +-- form a semantic function for the compound attribute consisting of +-- the two original attributes. + +(|*|) :: (p :< c, q :< c) + => Syn f c p g -> Syn f c q g -> Syn f c (p :*: q) g +(|*|) = prodSyn + + + + +-- | The type of semantic functions for inherited attributes. For +-- defining semantic functions use the type 'Inh', which includes the +-- inherited attribute that is defined by the semantic function into +-- the available attributes. + +type Inh' f p q g = forall m i a . (Mapping m i, ?below :: i -> p a, ?above :: p a) + => f i -> m (q (Context g a)) + +-- | The type of semantic functions for inherited attributes. + +type Inh f p q g = (q :< p) => Inh' f p q g + +-- | Combines the semantic functions for two inherited attributes to +-- form a semantic function for the compound attribute consisting of +-- the two original attributes. + +prodInh :: (p :< c, q :< c, Functor p, Functor q) => Inh f c p g -> Inh f c q g -> Inh f c (p :*: q) g +prodInh sp sq t = prodMapWith (:*:) (fmap Hole above) (fmap Hole above) (sp t) (sq t) + + +-- | Combines the semantic functions for two inherited attributes to +-- form a semantic function for the compound attribute consisting of +-- the two original attributes. + +(>*<) :: (p :< c, q :< c, Functor p, Functor q) + => Inh f c p g -> Inh f c q g -> Inh f c (p:*:q) g +(>*<) = prodInh diff --git a/tests/Test/Examples.hs b/tests/Test/Examples.hs --- a/tests/Test/Examples.hs +++ b/tests/Test/Examples.hs @@ -1,3 +1,5 @@ +{-# LANGUAGE GADTs #-} + module Test.Examples where import Examples.Types @@ -5,39 +7,65 @@ import Examples.TypeInference import Examples.LeavesBelow import Test.QuickCheck +import Test.HUnit import Test.Framework import Test.Framework.Providers.QuickCheck2 import Test.Framework.Providers.HUnit import Test.Utils +import Test.Dag import Data.Comp.Term import Data.Comp.Dag import qualified Data.Map as Map +import qualified Examples.RepminPAG as PAG +import Data.Comp.Dag.Internal +import qualified Data.IntMap as IntMap tests = [ testGroup "Repmin" [ testCase "AG" case_repminAG , testCase "Rewrite" case_repminRewrite + , testCase "TreePAG" case_repminTreePAG + , testCase "PAG bisim" case_repminPAG + , testCase "PAG single leaf" case_repminPAG_singleLeaf + , testCase "PAG iso" case_repminPAG_iso ] , testProperty "LeavesBelow" prop_leavesBelow , testCase "TypeInference" case_typeInf ] - - -intTrees :: [Term IntTreeF] -intTrees = [it1,it2,it3,it4] where - it1 = iNode (iNode x (iLeaf 10)) x - where x = iNode y y - y = iLeaf 20 - it2 = iNode x (iNode (iLeaf 5) x) - where x = iNode (iNode (iLeaf 24) (iLeaf 3)) (iLeaf 4) - it3 = iLeaf 5 - it4 = iNode x x - where x = iLeaf 0 - case_repminAG = testAllEq' intTrees repmin repminG case_repminRewrite = testAllEq' intTrees repmin (unravel . repminG') + +-- Result of rewrite version and version are not iso but at least +-- bisimilar. +case_repminPAG = testAllDagBisim' intTrees repminG' PAG.repminG + +-- The PAG version produces a result with only one leaf node. +case_repminPAG_singleLeaf = testAllDag' hasSingleLeaf message intTrees PAG.repminG + where message g = show g ++ " has more than one leaf node" + +-- The PAG version produces a result with only one leaf node. +case_repminPAG_iso = testAllDag2' p message intTrees repminG' PAG.repminG + where p g1 g2 = g1 `iso` g2 || (not (hasSingleLeaf g1) && hasSingleLeaf g2) + message g1 g2 = show g1 ++ " and " ++ show g2 ++ " should coincide since the former has only one leaf node" + + +-- | Checks whether the given dag has only one leaf node. +hasSingleLeaf :: Dag IntTreeF -> Bool +hasSingleLeaf Dag {root = r, edges = e} = IntMap.foldr (\t c -> countLeaves t + c) (countLeaves r) e == 1 + +-- | Counts the leaf nodes in the given context. +countLeaves :: IntTreeF (Context IntTreeF a) -> Int +countLeaves (Leaf _) = 1 +countLeaves (Node x y) = countLeaves' x + countLeaves' y + where + countLeaves' (Term t) = countLeaves t + countLeaves' (Hole _) = 0 + + +case_repminTreePAG = mapM_ run intTrees + where run t = repmin t @=? PAG.repmin t prop_leavesBelow d = testAllEq intTrees (leavesBelow d) (leavesBelowG d) diff --git a/tests/Test/Utils.hs b/tests/Test/Utils.hs --- a/tests/Test/Utils.hs +++ b/tests/Test/Utils.hs @@ -4,12 +4,36 @@ 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