packages feed

compdata-dags 0.1 → 0.2

raw patch · 12 files changed

+495/−26 lines, 12 filesdep −projectiondep ~QuickCheckdep ~compdatadep ~test-framework-quickcheck2setup-changed

Dependencies removed: projection

Dependency ranges changed: QuickCheck, compdata, test-framework-quickcheck2

Files

Setup.hs view
compdata-dags.cabal view
@@ -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/-  (<http://www.diku.dk/~paba/pubs/entries/bahr15popl.html>).+  (<http://dx.doi.org/10.1145/2678015.2682539>).   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
+ examples/Examples/RepminPAG.hs view
@@ -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)+
examples/Examples/Types.hs view
@@ -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 
src/Data/Comp/AG.hs view
@@ -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   
src/Data/Comp/AG/Internal.hs view
@@ -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
src/Data/Comp/Dag/AG.hs view
@@ -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
+ src/Data/Comp/Dag/PAG.hs view
@@ -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 <paba@di.ku.dk>+-- 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'}
+ src/Data/Comp/PAG.hs view
@@ -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 <paba@di.ku.dk>+-- 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'
+ src/Data/Comp/PAG/Internal.hs view
@@ -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 <paba@di.ku.dk>+-- 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
tests/Test/Examples.hs view
@@ -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) 
tests/Test/Utils.hs view
@@ -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