| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
Data.Equality.Graph.Monad
Description
Monadic interface to e-graph stateful computations
Synopsis
- egraph :: Language l => EGraphM anl l a -> (a, EGraph anl l)
- represent :: (Analysis anl l, Language l) => Fix l -> EGraphM anl l ClassId
- add :: (Analysis anl l, Language l) => ENode l -> EGraphM anl l ClassId
- merge :: (Analysis anl l, Language l) => ClassId -> ClassId -> EGraphM anl l ClassId
- rebuild :: (Analysis anl l, Language l) => EGraphM anl l ()
- canonicalize :: Functor l => ENode l -> EGraph a l -> ENode l
- find :: ClassId -> EGraph a l -> ClassId
- emptyEGraph :: Language l => EGraph a l
- type EGraphM a l = State (EGraph a l)
- runEGraphM :: EGraph anl l -> EGraphM anl l a -> (a, EGraph anl l)
- data EGraph analysis language
- modify :: forall (m :: Type -> Type) s. Monad m => (s -> s) -> StateT s m ()
- get :: forall (m :: Type -> Type) s. Monad m => StateT s m s
- gets :: forall (m :: Type -> Type) s a. Monad m => (s -> a) -> StateT s m a
Documentation
egraph :: Language l => EGraphM anl l a -> (a, EGraph anl l) Source #
Run EGraph computation on an empty e-graph
Example
egraph $ do id1 <- represent t1 id2 <- represent t2 merge id1 id2
represent :: (Analysis anl l, Language l) => Fix l -> EGraphM anl l ClassId Source #
Represent an expression (Fix l) in an e-graph by recursively
representing sub expressions
add :: (Analysis anl l, Language l) => ENode l -> EGraphM anl l ClassId Source #
Add an e-node to the e-graph
merge :: (Analysis anl l, Language l) => ClassId -> ClassId -> EGraphM anl l ClassId Source #
Merge two e-classes by id
E-graph invariants may be broken by merging, and rebuild should be used
eventually to restore them
rebuild :: (Analysis anl l, Language l) => EGraphM anl l () Source #
Rebuild: Restore e-graph invariants
E-graph invariants are traditionally maintained after every merge, but we
allow operations to temporarilly break the invariants (specifically, until we call
rebuild)
The paper describing rebuilding in detail is https://arxiv.org/abs/2004.03082
canonicalize :: Functor l => ENode l -> EGraph a l -> ENode l Source #
Canonicalize an e-node
Two e-nodes are equal when their canonical form is equal. Canonicalization makes the list of e-class ids the e-node holds a list of canonical ids. Meaning two seemingly different e-nodes might be equal when we figure out that their e-class ids are represented by the same e-class canonical ids
canonicalize(𝑓(𝑎,𝑏,𝑐,...)) = 𝑓((find 𝑎), (find 𝑏), (find 𝑐),...)
find :: ClassId -> EGraph a l -> ClassId Source #
Find the canonical representation of an e-class id in the e-graph
Invariant: The e-class id always exists.
emptyEGraph :: Language l => EGraph a l Source #
The empty e-graph. Nothing is represented in it yet.
E-graph stateful computations
runEGraphM :: EGraph anl l -> EGraphM anl l a -> (a, EGraph anl l) Source #
Run EGraphM computation on a given e-graph
E-graph definition re-export
data EGraph analysis language Source #
E-graph representing terms of language l.
Intuitively, an e-graph is a set of equivalence classes (e-classes). Each e-class is a set of e-nodes representing equivalent terms from a given language, and an e-node is a function symbol paired with a list of children e-classes.