diff --git a/LICENSE b/LICENSE new file mode 100644 --- /dev/null +++ b/LICENSE @@ -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. diff --git a/Setup.hs b/Setup.hs new file mode 100644 --- /dev/null +++ b/Setup.hs @@ -0,0 +1,2 @@ +import Distribution.Simple +main = defaultMain diff --git a/compdata-dags.cabal b/compdata-dags.cabal new file mode 100644 --- /dev/null +++ b/compdata-dags.cabal @@ -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/ + (). + + +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 + diff --git a/examples/Examples/Circuit.hs b/examples/Examples/Circuit.hs new file mode 100644 --- /dev/null +++ b/examples/Examples/Circuit.hs @@ -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 diff --git a/examples/Examples/LeavesBelow.hs b/examples/Examples/LeavesBelow.hs new file mode 100644 --- /dev/null +++ b/examples/Examples/LeavesBelow.hs @@ -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) diff --git a/examples/Examples/Repmin.hs b/examples/Examples/Repmin.hs new file mode 100644 --- /dev/null +++ b/examples/Examples/Repmin.hs @@ -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 diff --git a/examples/Examples/TypeInference.hs b/examples/Examples/TypeInference.hs new file mode 100644 --- /dev/null +++ b/examples/Examples/TypeInference.hs @@ -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) + + diff --git a/examples/Examples/Types.hs b/examples/Examples/Types.hs new file mode 100644 --- /dev/null +++ b/examples/Examples/Types.hs @@ -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) +-- ] + diff --git a/src/Data/Comp/AG.hs b/src/Data/Comp/AG.hs new file mode 100644 --- /dev/null +++ b/src/Data/Comp/AG.hs @@ -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 +-- 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' diff --git a/src/Data/Comp/AG/Internal.hs b/src/Data/Comp/AG/Internal.hs new file mode 100644 --- /dev/null +++ b/src/Data/Comp/AG/Internal.hs @@ -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 +-- 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 diff --git a/src/Data/Comp/Dag.hs b/src/Data/Comp/Dag.hs new file mode 100644 --- /dev/null +++ b/src/Data/Comp/Dag.hs @@ -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 +-- 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 diff --git a/src/Data/Comp/Dag/AG.hs b/src/Data/Comp/Dag/AG.hs new file mode 100644 --- /dev/null +++ b/src/Data/Comp/Dag/AG.hs @@ -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 +-- 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'} diff --git a/src/Data/Comp/Dag/Internal.hs b/src/Data/Comp/Dag/Internal.hs new file mode 100644 --- /dev/null +++ b/src/Data/Comp/Dag/Internal.hs @@ -0,0 +1,36 @@ +-------------------------------------------------------------------------------- +-- | +-- Module : Data.Comp.Dag.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 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 + } diff --git a/tests/RunTests.hs b/tests/RunTests.hs new file mode 100644 --- /dev/null +++ b/tests/RunTests.hs @@ -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 + ] diff --git a/tests/Test/Dag.hs b/tests/Test/Dag.hs new file mode 100644 --- /dev/null +++ b/tests/Test/Dag.hs @@ -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) diff --git a/tests/Test/Examples.hs b/tests/Test/Examples.hs new file mode 100644 --- /dev/null +++ b/tests/Test/Examples.hs @@ -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) diff --git a/tests/Test/Utils.hs b/tests/Test/Utils.hs new file mode 100644 --- /dev/null +++ b/tests/Test/Utils.hs @@ -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)