Copyright | (c) 2014 Patrick Bahr, Emil Axelsson |
---|---|
License | BSD3 |
Maintainer | Patrick Bahr <paba@di.ku.dk> |
Stability | experimental |
Portability | non-portable (GHC Extensions) |
Safe Haskell | None |
Language | Haskell98 |
This module implements a representation of directed acyclic graphs
(DAGs) as compact representations of trees (or Term
s).
- data Dag f
- termTree :: Functor f => Term f -> Dag f
- reifyDag :: Traversable f => Term f -> IO (Dag f)
- unravel :: forall f. Functor f => Dag f -> Term f
- bisim :: forall f. (EqF f, Functor f, Foldable f) => Dag f -> Dag f -> Bool
- iso :: (Traversable f, Foldable f, EqF f) => Dag f -> Dag f -> Bool
- strongIso :: (Functor f, Foldable f, EqF f) => Dag f -> Dag f -> Bool
Documentation
The type of directed acyclic graphs (DAGs). Dag
s are used as a
compact representation of Term
s.
reifyDag :: Traversable f => Term f -> IO (Dag f) Source
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.
unravel :: forall f. Functor f => Dag f -> Term f Source
This function unravels a given graph to the term it represents.
bisim :: forall f. (EqF f, Functor f, Foldable f) => Dag f -> Dag f -> Bool Source
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.