packages feed

compdata-dags (empty) → 0.1

raw patch · 17 files changed

+1342/−0 lines, 17 filesdep +HUnitdep +QuickCheckdep +basesetup-changed

Dependencies added: HUnit, QuickCheck, base, compdata, containers, mtl, projection, test-framework, test-framework-hunit, test-framework-quickcheck2, unordered-containers, vector

Files

+ LICENSE view
@@ -0,0 +1,30 @@+Copyright (c) 2014 Patrick Bahr, Emil Axelsson++All rights reserved.++Redistribution and use in source and binary forms, with or without+modification, are permitted provided that the following conditions+are met:++1. Redistributions of source code must retain the above copyright+   notice, this list of conditions and the following disclaimer.++2. Redistributions in binary form must reproduce the above copyright+   notice, this list of conditions and the following disclaimer in the+   documentation and/or other materials provided with the distribution.++3. Neither the name of the author nor the names of his contributors+   may be used to endorse or promote products derived from this software+   without specific prior written permission.++THIS SOFTWARE IS PROVIDED BY THE AUTHORS ``AS IS'' AND ANY EXPRESS OR+IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED+WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE+DISCLAIMED.  IN NO EVENT SHALL THE AUTHORS OR CONTRIBUTORS BE LIABLE FOR+ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL+DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS+OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION)+HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT,+STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN+ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE+POSSIBILITY OF SUCH DAMAGE.
+ Setup.hs view
@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain
+ compdata-dags.cabal view
@@ -0,0 +1,52 @@+Name:			compdata-dags+Version:		0.1+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>).+++Category:               Generics+License:                BSD3+License-file:           LICENSE+Author:                 Patrick Bahr, Emil Axelsson+Maintainer:             paba@di.ku.dk+Build-Type:             Simple+Cabal-Version:          >=1.9.2+bug-reports:            https://github.com/pa-ba/compdata-dags/issues+++extra-source-files:+  -- test files+  tests/Test/*.hs+  -- example files+  examples/Examples/*.hs+++library+  Exposed-Modules:      Data.Comp.AG+                        Data.Comp.Dag+                        Data.Comp.Dag.AG+  Other-Modules:        Data.Comp.Dag.Internal+                        Data.Comp.AG.Internal+  Build-Depends:	base >= 4.7, base < 5, compdata == 0.9.*, projection, unordered-containers, +                        mtl, containers, vector+  hs-source-dirs:	src+  ghc-options:          -W+++Test-Suite test+  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+++source-repository head+  type:     git+  location: https://github.com/pa-ba/compdata-dags+
+ examples/Examples/Circuit.hs view
@@ -0,0 +1,48 @@+{-# LANGUAGE DeriveFoldable             #-}+{-# LANGUAGE DeriveFunctor              #-}+{-# LANGUAGE DeriveTraversable          #-}+{-# LANGUAGE FlexibleContexts           #-}+{-# LANGUAGE GeneralizedNewtypeDeriving #-}+{-# LANGUAGE ImplicitParams             #-}+{-# LANGUAGE ScopedTypeVariables        #-}+{-# LANGUAGE TemplateHaskell            #-}+{-# LANGUAGE TypeOperators              #-}++module Examples.Circuit where++import Data.Comp.AG+import Data.Comp.Dag+import qualified Data.Comp.Dag.AG as Dag+import Data.Comp.Term+import Data.Comp.Derive++++++data CircuitF a = Input | Nand a a+  deriving (Eq, Show, Functor, Foldable, Traversable)++$(derive [smartConstructors, makeShowF] [''CircuitF])+++type Circuit = Dag CircuitF++newtype Delay  = Delay  Int  deriving (Eq,Ord,Show,Num)+newtype Load   = Load   Int  deriving (Eq,Ord,Show,Num)++gateDelay :: (Load :< atts) => Syn CircuitF atts Delay+gateDelay Input       = 0+gateDelay (Nand a b)  =+  max (below a) (below b) + 10 + Delay l+    where Load l = above++gateLoad :: Inh CircuitF atts Load+gateLoad (Nand a b)  = a |-> 1 & b |-> 1+gateLoad _           = empty++delay :: Circuit -> Load -> Delay+delay g l = Dag.runAG (+) gateDelay gateLoad (const l) g++delayTree :: Term CircuitF -> Load -> Delay+delayTree c l = runAG gateDelay gateLoad (const l) c
+ examples/Examples/LeavesBelow.hs view
@@ -0,0 +1,34 @@+{-# LANGUAGE TypeOperators  #-}+{-# LANGUAGE ImplicitParams #-}+++module Examples.LeavesBelow where++import Data.Comp.AG+import Data.Comp.Dag+import qualified Data.Comp.Dag.AG as Dag+import Data.Comp.Term+import Examples.Types+import Data.Set (Set)+import qualified Data.Set as Set+++leavesBelowI :: Inh IntTreeF atts Int+leavesBelowI (Leaf _)      = empty+leavesBelowI (Node t1 t2)  = t1 |-> d' & t2 |-> d'+            where d' = above - 1++leavesBelowS :: (Int :< atts) => Syn IntTreeF atts (Set Int)+leavesBelowS (Leaf i)+    | (above :: Int) <= 0  =  Set.singleton i+    | otherwise            =  Set.empty+leavesBelowS (Node t1 t2)  =  below t1 `Set.union` below t2+++-- | As AG on terms+leavesBelow :: Int -> Term IntTreeF -> Set Int+leavesBelow d = runAG leavesBelowS leavesBelowI (const d)++-- | As AG on dags+leavesBelowG :: Int -> Dag IntTreeF -> Set Int+leavesBelowG d = Dag.runAG min leavesBelowS leavesBelowI (const d)
+ examples/Examples/Repmin.hs view
@@ -0,0 +1,56 @@+{-# LANGUAGE TypeOperators  #-}+{-# LANGUAGE ImplicitParams #-}+++module Examples.Repmin where++import Data.Comp.AG+import Data.Comp.Dag+import qualified Data.Comp.Dag.AG as Dag+import Data.Comp.Term+import Examples.Types++newtype MinS = MinS Int deriving (Eq,Ord)+newtype MinI = MinI Int++-- | Repmin as an AG on terms.++repmin :: Term IntTreeF -> Term IntTreeF+repmin = snd . runAG (minS |*| rep) minI init+  where init (MinS i,_) = MinI i++-- | Repmin as an AG on dags.++repminG :: Dag IntTreeF -> Term IntTreeF+repminG =  snd . Dag.runAG const (minS |*| rep) minI init+  where init (MinS i,_) = MinI i+++globMin :: (?above :: atts, MinI :< atts) => Int+globMin = let MinI i = above in i++minS ::  Syn IntTreeF atts MinS+minS (Leaf i)    =  MinS i+minS (Node a b)  =  min (below a) (below b)++minI :: Inh IntTreeF atts MinI+minI _ = empty++rep ::  (MinI :< atts) => Syn IntTreeF atts (Term IntTreeF)+rep (Leaf _)    =  iLeaf globMin+rep (Node a b)  =  iNode (below a) (below b)+++-- | Repmin as a rewriting AG on dags.++repminG' :: Dag IntTreeF -> Dag IntTreeF+repminG' = snd . Dag.runRewrite const minS minI rep' init+  where init (MinS i) = MinI i++rep' ::  (MinI :< atts) => Rewrite IntTreeF atts IntTreeF+rep' (Leaf _)    =  iLeaf globMin+rep' (Node a b)  =  iNode (Hole a) (Hole b)++repmin' :: Term IntTreeF -> Term IntTreeF+repmin' = snd . runRewrite minS minI rep' init+  where init (MinS i) = MinI i
+ examples/Examples/TypeInference.hs view
@@ -0,0 +1,147 @@+{-# LANGUAGE PatternGuards #-}+{-# LANGUAGE DeriveFoldable             #-}+{-# LANGUAGE DeriveFunctor              #-}+{-# LANGUAGE DeriveTraversable          #-}+{-# LANGUAGE FlexibleContexts           #-}+{-# LANGUAGE GeneralizedNewtypeDeriving #-}+{-# LANGUAGE ImplicitParams             #-}+{-# LANGUAGE ScopedTypeVariables        #-}+{-# LANGUAGE TemplateHaskell            #-}+{-# LANGUAGE TypeOperators              #-}++module Examples.TypeInference where++import Data.Comp.AG+import Data.Comp.Dag+import qualified Data.Comp.Dag.AG as Dag+import Data.Comp.Term+import Data.Map (Map)+import qualified Data.Map as Map+import Data.Comp.Derive++import System.IO.Unsafe+++intersection :: (Ord k, Eq v) => Map k v -> Map k v -> Map k v+intersection = Map.mergeWithKey (\_ x1 x2 -> if x1 == x2 then Just x1 else Nothing)+                     (const Map.empty) (const Map.empty)+++++type Name = String++data  Type  = BoolType | IntType deriving (Eq, Show)+type  Env   = Map Name Type++insertEnv :: Name -> Maybe Type -> Env -> Env+insertEnv _ Nothing   env  =  env+insertEnv v (Just t)  env  =  Map.insert v t env++lookEnv :: Name -> Env -> Maybe Type+lookEnv = Map.lookup+++data ExpF a  =  LitB Bool   |  LitI Int  |  Var Name+             |  Eq a a      |  Add a a   |  If a a a+             |  Iter Name a a a+  deriving (Eq, Show, Functor, Foldable, Traversable)++$(derive [smartConstructors, makeShowF] [''ExpF])++typeOf ::  (?below :: a -> atts, Maybe Type :< atts) =>+           a -> Maybe Type+typeOf = below++typeInfS :: (Env :< atts) => Syn ExpF atts (Maybe Type)+typeInfS (LitB _)                =  Just BoolType+typeInfS (LitI _)                =  Just IntType+typeInfS (Eq a b)+  |  Just ta        <-  typeOf a+  ,  Just tb        <-  typeOf b+  ,  ta == tb                     =  Just BoolType+typeInfS (Add a b)+  |  Just  IntType  <-  typeOf a+  ,  Just  IntType  <-  typeOf b  =  Just IntType+typeInfS (If c t f)+  |  Just BoolType  <-  typeOf c+  ,  Just tt        <-  typeOf t+  ,  Just tf        <-  typeOf f+  ,  tt == tf                     =  Just tt+typeInfS (Var v)                 =  lookEnv v above+typeInfS (Iter _ n i b)+  |  Just IntType   <-  typeOf n+  ,  Just ti        <-  typeOf i+  ,  Just tb        <-  typeOf b+  ,  ti == tb                     =  Just tb+typeInfS _                        =  Nothing++typeInfI :: (Maybe Type :< atts) => Inh ExpF atts Env+typeInfI (Iter v _ i b)  =  b |-> insertEnv v ti above+                               where ti = typeOf i+typeInfI _                =  empty++typeInf :: Env -> Term ExpF -> Maybe Type+typeInf env = runAG typeInfS typeInfI (const env)++typeInfG :: Env -> Dag ExpF -> Maybe Type+typeInfG env = Dag.runAG intersection typeInfS typeInfI (const env)++gt1 :: Term ExpF+gt1 = iIter "x" x x (iAdd (iIter "y" z z (iAdd z y)) y)+    where x = iLitI 10+          y = iVar "x"+          z = iLitI 5++g1 :: Dag ExpF+g1 = unsafePerformIO $ reifyDag gt1+--     [ (0, Iter "x" 1 1 2)+--     , (1, LitI 10)+--     , (2, Add 3 4)+--     , (3, Iter "y" 5 5 6)+--     , (4, Var "x")+--     , (5, LitI 5)+--     , (6, Add 5 4)+--     ]++typeTestG1 = typeInfG Map.empty g1+typeTestT1 = typeInf Map.empty (unravel g1)++gt2 :: Term ExpF+gt2 = iIter "x" x (iIter "x" x x y) y+    where x = iLitI 0+          y = iVar "x"++g2 :: Dag ExpF+g2 = unsafePerformIO $ reifyDag gt2++--     [ (0, Iter "x" 1 2 3)+--     , (1, LitI 0)+--     , (2, Iter "x" 1 1 3)+--     , (3, Var "x")+--     ]++typeTestG2 = typeInfG Map.empty g2+typeTestT2 = typeInf Map.empty (unravel g2)++gt3 :: Term ExpF+gt3 = iAdd (iIter "x" x x z) (iIter "x" y y z)+    where x = iLitI 10+          y = iLitB False+          z = iVar "x"++g3 :: Dag ExpF+g3 = unsafePerformIO $ reifyDag gt3++--     [ (0, Add 1 3)+--     , (1, Iter "x" 2 2 5)+--     , (2, LitI 10)+--     , (3, Iter "x" 4 4 5)+--     , (4, LitB False)+--     , (5, Var "x")+--     ]++typeTestG3 = typeInfG Map.empty g3+typeTestT3 = typeInf Map.empty (unravel g3)++
+ examples/Examples/Types.hs view
@@ -0,0 +1,56 @@+{-# LANGUAGE DeriveFoldable    #-}+{-# LANGUAGE DeriveFunctor     #-}+{-# LANGUAGE DeriveTraversable #-}+{-# LANGUAGE TemplateHaskell   #-}++module Examples.Types where+++import Data.Comp.Term+import Data.Comp.Dag+import Data.Comp.Derive+import System.IO.Unsafe++++data IntTreeF a = Leaf Int | Node a a+  deriving (Eq, Show, Functor, Foldable, Traversable)++$(derive [smartConstructors, makeShowF, makeEqF] [''IntTreeF])+++-- Example terms and dags++it1 :: Term IntTreeF+it1 = iNode (iNode x (iLeaf 10)) x+    where x = iNode y y+          y = iLeaf 20++i1 :: Dag IntTreeF+i1 = unsafePerformIO $ reifyDag it1++--     [ (0, Node 1 2)+--     , (1, Node 2 3)+--     , (2, Node 4 4)+--     , (3, Leaf 10)+--     , (4, Leaf 20)+--     ]+++it2 :: Term IntTreeF+it2 = iNode x (iNode (iLeaf 5) x)+    where x = iNode (iNode (iLeaf 24) (iLeaf 3)) (iLeaf 4)++i2 :: Dag IntTreeF+i2 = unsafePerformIO $ reifyDag it2++--     [ (0, Node 2 1)+--     , (1, Node 4 2)+--     , (2, Node 3 5)+--     , (3, Node 6 7)+--     , (4, Leaf 5)+--     , (5, Leaf 4)+--     , (6, Leaf 24)+--     , (7, Leaf 3)+--     ]+
+ src/Data/Comp/AG.hs view
@@ -0,0 +1,80 @@+{-# LANGUAGE FlexibleContexts    #-}+{-# LANGUAGE RankNTypes          #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeOperators       #-}+++--------------------------------------------------------------------------------+-- |+-- Module      :  Data.Comp.AG+-- 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.+--+--------------------------------------------------------------------------------++module Data.Comp.AG+    ( runAG+    , runRewrite+    , module I+    )  where++import Data.Comp.AG.Internal+import qualified Data.Comp.AG.Internal as I hiding (explicit)+import Data.Comp.Algebra+import Data.Comp.Mapping as I+import Data.Comp.Term+import Data.Projection as I+++++-- | This function runs an attribute grammar on a term. The result is+-- the (combined) synthesised attribute at the root of the term.++runAG :: forall f u d . Traversable f+      => Syn' f (u,d) u -- ^ semantic function of synthesised attributes+      -> Inh' f (u,d) d -- ^ semantic function of inherited attributes+      -> (u -> d)       -- ^ initialisation of inherited attributes+      -> Term f         -- ^ input term+      -> u+runAG up down dinit t = uFin where+    uFin = run dFin t+    dFin = dinit uFin+    run :: d -> Term f -> u+    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 = explicit down (u,d) unNumbered t'+        u = explicit up (u,d) unNumbered t'++-- | This function runs an attribute grammar with rewrite function on+-- a term. The result is the (combined) synthesised attribute at the+-- root of the term and the rewritten term.++runRewrite :: forall f g u d . (Traversable f, Functor g)+           => Syn' f (u,d) u -> Inh' f (u,d) d -- ^ semantic function of synthesised attributes+           -> Rewrite f (u,d) g                -- ^ semantic function of inherited attributes+           -> (u -> d)                         -- ^ initialisation of inherited attributes+           -> Term f                           -- ^ input term+           -> (u, Term g)+runRewrite up down trans dinit t = res where+    res@(uFin,_) = run dFin t+    dFin = dinit uFin+    run :: d -> Term f -> (u, Term g)+    run d (Term t) = (u,t'') where+        t' = fmap bel $ number t+        bel (Numbered i s) =+            let d' = lookupNumMap d i m+                (u', s') = run d' s+            in Numbered i ((u', d'),s')+        m = explicit down (u,d) (fst . unNumbered) t'+        u = explicit up (u,d) (fst . unNumbered) t'+        t'' = appCxt $ fmap (snd . unNumbered) $ explicit trans (u,d) (fst . unNumbered) t'
+ src/Data/Comp/AG/Internal.hs view
@@ -0,0 +1,107 @@+{-# LANGUAGE ImplicitParams        #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE Rank2Types            #-}+{-# LANGUAGE TypeOperators         #-}++--------------------------------------------------------------------------------+-- |+-- Module      :  Data.Comp.AG.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 attribute grammars along with+-- some utility functions.+--+--------------------------------------------------------------------------------++module Data.Comp.AG.Internal where+++import Data.Comp.Mapping+import Data.Comp.Term+import Data.Projection+++-- | This function provides access to attributes of the immediate+-- children of the current node.++below :: (?below :: child -> q, p :< q) => child -> p+below = pr . ?below++-- | This function provides access to attributes of the current node++above :: (?above :: q, p :< q) => p+above = pr ?above++-- | Turns the explicit parameters @?above@ and @?below@ into explicit+-- ones.++explicit :: ((?above :: q, ?below :: a -> q) => b) -> q -> (a -> q) -> b+explicit x ab be = x where ?above = ab; ?below = be+++-- | A simple rewrite function that may depend on (inherited and/or+-- synthesised) attributes.+type Rewrite f q g = forall a . (?below :: a -> q, ?above :: q) => f a -> Context g a+++-- | 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 = forall a . (?below :: a -> p, ?above :: p) => f a -> q++-- | The type of semantic functions for synthesised attributes.+type Syn  f p q = (q :< p) => Syn' f p q++-- | 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 -> Syn f c q -> Syn f c (p,q)+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 -> Syn f c q -> Syn f c (p,q)+(|*|) = 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 = forall m i . (Mapping m i, ?below :: i -> p, ?above :: p)+                                => f i -> m q++-- | The type of semantic functions for inherited attributes.++type Inh f p q = (q :< p) => Inh' f p q++-- | 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) => Inh f c p -> Inh f c q -> Inh f c (p,q)+prodInh sp sq t = prodMap above 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 f)+         => Inh f c p -> Inh f c q -> Inh f c (p,q)+(>*<) = prodInh
+ src/Data/Comp/Dag.hs view
@@ -0,0 +1,250 @@+{-# LANGUAGE BangPatterns        #-}+{-# LANGUAGE DeriveDataTypeable  #-}+{-# LANGUAGE DoAndIfThenElse     #-}+{-# LANGUAGE GADTs               #-}+{-# LANGUAGE NamedFieldPuns      #-}+{-# LANGUAGE ScopedTypeVariables #-}+++--------------------------------------------------------------------------------+-- |+-- Module      :  Data.Comp.Dag+-- 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 a representation of directed acyclic graphs+-- (DAGs) as compact representations of trees (or 'Term's).+--+--------------------------------------------------------------------------------++module Data.Comp.Dag+    ( Dag+    , termTree+    , reifyDag+    , unravel+    , bisim+    , iso+    , strongIso+    ) where++import Control.Applicative+import Control.Exception.Base+import Control.Monad.State+import Data.Comp.Dag.Internal+import Data.Comp.Equality+import Data.Comp.Term+import Data.Foldable (Foldable)+import qualified Data.HashMap.Lazy as HashMap+import Data.IntMap+import qualified Data.IntMap as IntMap+import Data.IORef+import Data.Traversable (Traversable)+import qualified Data.Traversable as Traversable+import Data.Typeable+import System.Mem.StableName++import Control.Monad.ST+import Data.Comp.Show+import Data.List+import Data.STRef+import qualified Data.Vector as Vec+import qualified Data.Vector.Generic.Mutable as MVec++instance (ShowF f, Functor f) => Show (Dag f)+  where+    show (Dag r es _) = unwords+        [ "mkDag"+        , show  (Term r)+        , showLst ["(" ++ show n ++ "," ++ show (Term f) ++ ")" | (n,f) <- IntMap.toList es ]+        ]+      where+        showLst ss = "[" ++ intercalate "," ss ++ "]"++++-- | Turn a term into a graph without sharing.+termTree :: Functor f => Term f -> Dag f+termTree (Term t) = Dag (fmap toCxt t) IntMap.empty 0++-- | This exception indicates that a 'Term' could not be reified to a+-- 'Dag' (using 'reifyDag') due to its cyclic sharing structure.+data CyclicException = CyclicException+    deriving (Show, Typeable)++instance Exception CyclicException++-- | This function takes a term, and returns a 'Dag' with the implicit+-- sharing of the input data structure made explicit. If the sharing+-- structure of the term is cyclic an exception of type+-- 'CyclicException' is thrown.+reifyDag :: Traversable f => Term f -> IO (Dag f)+reifyDag m = do+  tabRef <- newIORef HashMap.empty+  let findNodes (Term !j) = do+        st <- liftIO $ makeStableName j+        tab <- readIORef tabRef+        case HashMap.lookup st tab of+          Just (single,f) | single -> writeIORef tabRef (HashMap.insert st (False,f) tab)+                                      >> return st+                          | otherwise -> return st+          Nothing -> do res <- Traversable.mapM findNodes j+                        tab <- readIORef tabRef+                        if HashMap.member st tab+                          then throwIO CyclicException+                          else writeIORef tabRef (HashMap.insert st (True,res) tab)+                               >> return st+  st <- findNodes m+  tab <- readIORef tabRef+  counterRef <- newIORef 0+  edgesRef <- newIORef IntMap.empty+  nodesRef <- newIORef HashMap.empty+  let run st = do+        let (single,f) = tab HashMap.! st+        if single then Term <$> Traversable.mapM run f+        else do+          nodes <- readIORef nodesRef+          case HashMap.lookup st nodes of+            Just n -> return (Hole n)+            Nothing -> do+              n <- readIORef counterRef+              writeIORef counterRef $! (n+1)+              writeIORef nodesRef (HashMap.insert st n nodes)+              f' <- Traversable.mapM run f+              modifyIORef edgesRef (IntMap.insert n f')+              return (Hole n)+  Term root <- run st+  edges <- readIORef edgesRef+  count <- readIORef counterRef+  return (Dag root edges count)+++-- | This function unravels a given graph to the term it+-- represents.++unravel :: forall f. Functor f => Dag f -> Term f+unravel Dag {edges, root} = Term $ build <$> root+    where build :: Context f Node -> Term f+          build (Term t) = Term $ build <$> t+          build (Hole n) = Term $ build <$> edges IntMap.! n++-- | Checks whether two dags are bisimilar. In particular, we have+-- the following equality+--+-- @+-- bisim g1 g2 = (unravel g1 == unravel g2)+-- @+--+-- That is, two dags are bisimilar iff they have the same unravelling.++bisim :: forall f . (EqF f, Functor f, Foldable f)  => Dag f -> Dag f -> Bool+bisim Dag {root=r1,edges=e1}  Dag {root=r2,edges=e2} = runF r1 r2+    where run :: (Context f Node, Context f Node) -> Bool+          run (t1, t2) = runF (step e1 t1) (step e2 t2)+          step :: Edges f -> Context f Node -> f (Context f Node)+          step e (Hole n) = e IntMap.! n+          step _ (Term t) = t+          runF :: f (Context f Node) -> f (Context f Node) -> Bool+          runF f1 f2 = case eqMod f1 f2 of+                         Nothing -> False+                         Just l -> all run l+++-- | Checks whether the two given DAGs are isomorphic.++iso :: (Traversable f, Foldable f, EqF f) => Dag f -> Dag f -> Bool+iso g1 g2 = checkIso eqMod (flatten g1) (flatten g2)+++-- | Checks whether the two given DAGs are strongly isomorphic, i.e.+--   their internal representation is the same modulo renaming of+--   nodes.++strongIso :: (Functor f, Foldable f, EqF f) => Dag f -> Dag f -> Bool+strongIso Dag {root=r1,edges=e1,nodeCount=nx1}+          Dag {root=r2,edges=e2,nodeCount=nx2}+              = checkIso checkEq (r1,e1,nx1) (r2,e2,nx2)+    where checkEq t1 t2 = eqMod (Term t1) (Term t2)++++-- | This function flattens the internal representation of a DAG. That+-- is, it turns the nested representation of edges into single layers.++flatten :: forall f . Traversable f => Dag f -> (f Node, IntMap (f Node), Int)+flatten Dag {root,edges,nodeCount} = runST run where+    run :: forall s . ST s (f Node, IntMap (f Node), Int)+    run = do+      count <- newSTRef 0+      nMap :: Vec.MVector s (Maybe Node) <- MVec.new nodeCount+      MVec.set nMap Nothing+      newEdges <- newSTRef IntMap.empty+      let build :: Context f Node -> ST s Node+          build (Hole n) = mkNode n+          build (Term t) = do+            n' <- readSTRef count+            writeSTRef count $! (n'+1)+            t' <- Traversable.mapM build t+            modifySTRef newEdges (IntMap.insert n' t')+            return n'+          mkNode n = do+            mn' <- MVec.unsafeRead nMap n+            case mn' of+              Just n' -> return n'+              Nothing -> do n' <- readSTRef count+                            writeSTRef count $! (n'+1)+                            MVec.unsafeWrite nMap n (Just n')+                            return n'+          buildF (n,t) = do+            n' <- mkNode n+            t' <- Traversable.mapM build t+            modifySTRef newEdges (IntMap.insert n' t')+      root' <- Traversable.mapM build root+      mapM_ buildF $ IntMap.toList edges+      edges' <- readSTRef newEdges+      nodeCount' <- readSTRef count+      return (root', edges', nodeCount')++++-- | Checks whether the two given dag representations are+-- isomorphic. This function is polymorphic in the representation of+-- the edges. The first argument is a function that checks whether two+-- edges have the same labelling and if so, returns the matching pairs+-- of outgoing nodes the two edges point to. Otherwise the function+-- returns 'Nothing'.++checkIso :: (e -> e -> Maybe [(Node,Node)])+         -> (e, IntMap e, Int)+         -> (e, IntMap e, Int) -> Bool+checkIso checkEq (r1,e1,nx1) (r2,e2,nx2) = runST run where+   run :: ST s Bool+   run = do+     -- create empty mapping from nodes in g1 to nodes in g2+     nMap :: Vec.MVector s (Maybe Node) <- MVec.new nx1+     MVec.set nMap Nothing+     -- create empty set of nodes in g2 that are "mapped to" by the+     -- mapping created above+     nSet :: Vec.MVector s Bool <- MVec.new nx2+     MVec.set nSet False+     let checkT t1 t2 = case checkEq t1 t2 of+                          Nothing -> return False+                          Just l -> liftM and $ mapM checkN l+         checkN (n1,n2) = do+           nm' <- MVec.unsafeRead nMap n1+           case nm' of+             Just n' -> return (n2 == n')+             _ -> do+               b <- MVec.unsafeRead nSet n2+               if b+               -- n2 is already mapped to by another node+               then return False+               -- n2 is not mapped to+               else do+                 -- create mapping from n1 to n2+                 MVec.unsafeWrite nMap n1 (Just n2)+                 MVec.unsafeWrite nSet n2 True+                 checkT (e1 IntMap.! n1) (e2 IntMap.! n2)+     checkT r1 r2
+ src/Data/Comp/Dag/AG.hs view
@@ -0,0 +1,247 @@+{-# LANGUAGE FlexibleContexts    #-}+{-# LANGUAGE GADTs               #-}+{-# LANGUAGE NamedFieldPuns      #-}+{-# LANGUAGE RankNTypes          #-}+{-# LANGUAGE RecursiveDo         #-}+{-# LANGUAGE ScopedTypeVariables #-}+++--------------------------------------------------------------------------------+-- |+-- Module      :  Data.Comp.Dag.AG+-- 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.AG" 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.AG+    ( runAG+    , runRewrite+    , module I+    ) where++import Control.Monad.ST+import Control.Monad.State+import Data.Comp.AG.Internal+import qualified Data.Comp.AG.Internal as I hiding (explicit)+import Data.Comp.Dag+import Data.Comp.Dag.Internal+import Data.Comp.Mapping as I+import Data.Projection as I+import Data.Comp.Term+import qualified Data.IntMap as IntMap+import Data.Maybe+import Data.STRef+import qualified Data.Traversable as Traversable+import Data.Vector (Vector,MVector)+import qualified Data.Vector as Vec+import qualified Data.Vector.Generic.Mutable as MVec++-- | This function runs an attribute grammar on a dag. The result is+-- the (combined) synthesised attribute at the root of the dag.++runAG :: forall f d u .Traversable f+    => (d -> d -> d)   -- ^ resolution function for inherited attributes+    -> Syn' f (u,d) u  -- ^ semantic function of synthesised attributes+    -> Inh' f (u,d) d  -- ^ semantic function of inherited attributes+    -> (u -> d)        -- ^ initialisation of inherited attributes+    -> Dag f           -- ^ input dag+    -> u+runAG res syn inh dinit Dag {edges,root,nodeCount} = uFin where+    uFin = runST runM+    dFin = dinit uFin+    runM :: forall s . ST s u+    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+      let -- Runs the AG on an edge with the given input inherited+          -- attribute value and produces the output synthesised+          -- attribute value.+          run :: d -> f (Context f Node) -> ST s u+          run d t = mdo+             -- apply the semantic functions+             let u = explicit syn (u,d) unNumbered result+                 m = explicit inh (u,d) unNumbered result+                 -- recurses into the child nodes and numbers them+                 run' :: Context f Node -> ST s (Numbered (u,d))+                 run' s = do i <- readSTRef count+                             writeSTRef count $! (i+1)+                             let d' = lookupNumMap d i m+                             u' <- runF d' s -- recurse+                             return (Numbered i (u',d'))+             writeSTRef count 0  -- re-initialize counter+             result <- Traversable.mapM run' t+             return u+          -- recurses through the tree structure+          runF :: d -> Context f Node -> ST s u+          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)+          runF d (Term t)  = run d t+          -- This function is applied to each edge+          iter (n, t) = do+            u <- run (fromJust $ dmapFin Vec.! n) t+            MVec.unsafeWrite umap n u+      -- 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+      dmapFin <- Vec.unsafeFreeze dmap+      umapFin <- Vec.unsafeFreeze umap+      return u++++-- | This function runs an attribute grammar with rewrite function on+-- a dag. The result is the (combined) synthesised attribute at the+-- root of the dag and the rewritten dag.++runRewrite :: forall f g d u .(Traversable f, Traversable g)+    => (d -> d -> d)       -- ^ resolution function for inherited attributes+    -> Syn' f (u,d) u      -- ^ semantic function of synthesised attributes+    -> Inh' f (u,d) d      -- ^ semantic function of inherited attributes+    -> Rewrite f (u, d) g  -- ^ initialisation of inherited attributes+    -> (u -> d)            -- ^ input term+    -> Dag f+    -> (u, Dag g)+runRewrite res syn inh rewr dinit Dag {edges,root,nodeCount} = result where+    result@(uFin,_) = runST runM+    dFin = dinit uFin+    runM :: forall s . ST s (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 vector to represent edges of the target DAG+      allEdges <- MVec.new nodeCount+      let -- This function is applied to each edge+          iter (node,s) = do+             let d = fromJust $ dmapFin Vec.! node+             (u,t) <- run d s+             MVec.unsafeWrite umap node u+             MVec.unsafeWrite allEdges node t+          -- 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 -> f (Context f Node) -> ST s (u, Context g Node)+          run d t = mdo+             -- apply the semantic functions+             let u = explicit syn (u,d) (fst . unNumbered) result+                 m = explicit inh (u,d) (fst . unNumbered) result+                 -- recurses into the child nodes and numbers them+                 run' :: Context f Node -> ST s (Numbered ((u,d), Context g Node))+                 run' s = do i <- readSTRef count+                             writeSTRef count $! (i+1)+                             let d' = lookupNumMap d i m+                             (u',t) <- runF d' s+                             return (Numbered i ((u',d'), t))+             writeSTRef count 0+             result <- Traversable.mapM run' t+             let t' = join $ fmap (snd . unNumbered) $ explicit rewr (u,d) (fst . unNumbered) result+             return (u, t')+          -- 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, Hole x)+      -- first apply to the root+      (u,interRoot) <- 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+      allEdgesFin <- Vec.unsafeFreeze allEdges+      return (u, relabelNodes interRoot allEdgesFin nodeCount)+++-- | This function relabels the nodes of the given dag. Parts that are+-- unreachable from the root are discarded. Instead of an 'IntMap',+-- edges are represented by a 'Vector'.+relabelNodes :: forall f . Traversable f +             => Context f Node+             -> Vector (Cxt Hole f Int) +             -> 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 -> +                   case edges Vec.! node of+                     Hole n -> do+                       -- We found an edge that just maps to another+                       -- node. We shortcut this edge.+                       newNode <- build n+                       MVec.unsafeWrite newNodes node (Just newNode)+                       return newNode+                     Term f -> 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) f+                       modifySTRef newEdges (IntMap.insert newNode f')+                       return newNode+          -- This function is only used for the root. If the root is+          -- only a node, we lookup the mapping for that+          -- node. In any case we apply build to all nodes.+          build' :: Context f Node -> ST s (f (Context f Node))+          build' (Hole n) = do+                         n' <- build n+                         e <- readSTRef newEdges+                         return (e IntMap.! n')+          build' (Term f) = Traversable.mapM (Traversable.mapM build) f+      -- start relabelling from the root+      root' <- build' 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/Dag/Internal.hs view
@@ -0,0 +1,36 @@+--------------------------------------------------------------------------------+-- |+-- Module      :  Data.Comp.Dag.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 representing DAGs. However,+-- 'Dag's should only be constructed using the interface provided by+-- "Data.Comp.Dag".+--+--------------------------------------------------------------------------------++module Data.Comp.Dag.Internal where++import Data.Comp.Term+import Data.IntMap (IntMap)++-- | The type of node in a 'Dag'.++type Node = Int++-- | The type of the compact edge representation used in a 'Dag'.++type Edges f = IntMap (f (Context f Node))++-- | The type of directed acyclic graphs (DAGs). 'Dag's are used as a+-- compact representation of 'Term's.++data Dag f = Dag +    { root      :: f (Context f Node) -- ^ the entry point for the DAG+    , edges     :: Edges f            -- ^ the edges of the DAG+    , nodeCount :: Int                -- ^ the total number of nodes in the DAG+    }
+ tests/RunTests.hs view
@@ -0,0 +1,10 @@+import Test.Examples as Ex+import Test.Dag as Dag+import Test.Framework++main = defaultMain allTests++allTests =    +    [ testGroup "Examples" Ex.tests+    , testGroup "Dag" Dag.tests+    ]
+ tests/Test/Dag.hs view
@@ -0,0 +1,113 @@+module Test.Dag where++import Examples.Types+import Examples.Repmin+import Examples.TypeInference+import Examples.LeavesBelow+import Test.HUnit+import Test.Framework+import Test.Framework.Providers.QuickCheck2+import Test.Framework.Providers.HUnit+import Test.Utils+import Data.Comp.Term+import Data.Comp.Dag+import Data.Comp.Dag.Internal+import qualified Data.IntMap as IntMap++tests = +    [ testGroup "reify"+      [ testCase "unravel" case_reifyUnravel+      , testCase "strongIso" case_reifyStrongIso+      , testCase "iso" case_reifyIso+      , testCase "bisim" case_reifyBisim+      ]+    ]+++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_reifyUnravel = testAllEq' intTrees id unravel+++intGraphs :: [Dag IntTreeF]+intGraphs = [it1,it2,it3,it4] where+    it1 = Dag { root = Node (iNode (Hole 0) (iLeaf 10)) (Hole 0)+              , edges = IntMap.fromList +                        [(0, Node (Hole 1) (Hole 1)),+                         (1, Leaf 20)]+              , nodeCount = 2}+    it2 = Dag { root = Node (Hole 0) (iNode (iLeaf 5) (Hole 0))+              , edges = IntMap.fromList [(0, Node (iNode (iLeaf 24) (iLeaf 3)) (iLeaf 4))]+              , nodeCount = 1}+    it3 = Dag { root = Leaf 5, edges = IntMap.empty, nodeCount = 0 }+    it4 = Dag { root = Node (Hole 0) (Hole 0)+              , edges = IntMap.singleton 0 (Leaf 0)+              , nodeCount = 1}+++isoNotStrong :: [(Term IntTreeF,Dag IntTreeF)]+isoNotStrong = [(it1,ig1),(it2,ig2)] where+    it1 = iNode z x+        where x = iNode y y+              y = iLeaf 20+              z = iNode x (iLeaf 10)+    ig1 = Dag { root = Node (Hole 2) (Hole 0)+              , edges = IntMap.fromList +                        [(0, Node (Hole 1) (Hole 1)),+                         (1, Leaf 20),+                         (2, Node (Hole 0) (iLeaf 10))]+              , nodeCount = 3}+    it2 = iNode x z+        where x = iNode (iNode (iLeaf 24) (iLeaf 3)) (iLeaf 4)+              z = iNode (iLeaf 5) x+    ig2 = Dag { root = Node (Hole 0) (Hole 1)+              , edges = IntMap.fromList +                        [ (0, Node (iNode (iLeaf 24) (iLeaf 3)) (iLeaf 4))+                        , (1, Node (iLeaf 5) (Hole 0))]+              , nodeCount = 2}++bisimNotIso :: [(Term IntTreeF,Dag IntTreeF)]+bisimNotIso = [(it1,ig1),(it2,ig2)] where+    it1 = iNode z x+        where x = iNode y y+              y = iLeaf 20+              z = iNode x (iLeaf 10)+    ig1 = Dag { root = Node (iNode (Hole 0) (iLeaf 10)) (Hole 0)+              , edges = IntMap.fromList +                        [(0, Node (iLeaf 20) (iLeaf 20))]+              , nodeCount = 1}++    it2 = iNode x z+        where x = iNode (iNode y y) (iLeaf 4)+              y = iLeaf 3+              z = iNode (iLeaf 5) x+    ig2 = Dag { root = Node (Hole 0) (iNode (iLeaf 5) (Hole 0))+              , edges = IntMap.fromList [(0, Node (iNode (iLeaf 3) (iLeaf 3)) (iLeaf 4))]+              , nodeCount = 1}+++case_reifyStrongIso = sequence_ $ zipWith run intTrees intGraphs+    where run t g = do d <- reifyDag t+                       assertBool ("strongIso\n" ++ show d ++ "\n\n" ++ show g) (strongIso d g)++case_reifyIso = mapM_ run isoNotStrong+    where run (t1, d2) = do d1 <- reifyDag t1+                            assertBool ("not strongIso\n" ++ show d1 ++ "\n\n" ++ show d2) (not (strongIso d1 d2))+                            assertBool ("iso\n" ++ show d1 ++ "\n\n" ++ show d2) (iso d1 d2)+++case_reifyBisim = mapM_ run bisimNotIso+    where run (t1, d2) = do +            d1 <- reifyDag t1+            assertBool ("not iso\n" ++ show d1 ++ "\n\n" ++ show d2) (not (iso d1 d2))+            assertBool ("bisim\n" ++ show d1 ++ "\n\n" ++ show d2) (bisim d1 d2)
+ tests/Test/Examples.hs view
@@ -0,0 +1,56 @@+module Test.Examples where++import Examples.Types+import Examples.Repmin+import Examples.TypeInference+import Examples.LeavesBelow+import Test.QuickCheck+import Test.Framework+import Test.Framework.Providers.QuickCheck2+import Test.Framework.Providers.HUnit+import Test.Utils+import Data.Comp.Term+import Data.Comp.Dag+import qualified Data.Map as Map++tests = +    [ testGroup "Repmin"+      [ testCase "AG" case_repminAG+      , testCase "Rewrite" case_repminRewrite+      ]+    , 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')++prop_leavesBelow d = testAllEq intTrees (leavesBelow d) (leavesBelowG d)+++expTrees :: [Term ExpF]+expTrees = [t1,t2] where+    t1 = iIter "x" x x (iAdd (iIter "y" z z (iAdd z y)) y)+        where x = iLitI 10+              y = iVar "x"+              z = iLitI 5+    t2 = iAdd (iIter "x" x x z) (iIter "y" y y z)+        where x = iLitI 10+              y = iLitB False+              z = iVar "x"++case_typeInf = testAllEq' expTrees (typeInf Map.empty) (typeInfG Map.empty)
+ tests/Test/Utils.hs view
@@ -0,0 +1,18 @@+module Test.Utils where++import Test.HUnit+import Test.QuickCheck+import Data.Comp.Term+import Data.Comp.Dag+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++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)