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.