| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Data.Equality.Graph.Monad
Description
Monadic interface to e-graph stateful computations
Synopsis
- egraph :: forall (l :: Type -> Type) anl a. Language l => EGraphM anl l a -> (a, EGraph anl l)
- represent :: forall anl (l :: Type -> Type). (Analysis anl l, Language l) => Fix l -> EGraphM anl l ClassId
- add :: forall anl (l :: Type -> Type). (Analysis anl l, Language l) => ENode l -> EGraphM anl l ClassId
- merge :: forall anl (l :: Type -> Type). (Analysis anl l, Language l) => ClassId -> ClassId -> EGraphM anl l ClassId
- rebuild :: forall anl (l :: Type -> Type). (Analysis anl l, Language l) => EGraphM anl l ()
- canonicalize :: forall (l :: Type -> Type) a. Functor l => ENode l -> EGraph a l -> ENode l
- find :: forall a (l :: Type -> Type). ClassId -> EGraph a l -> ClassId
- emptyEGraph :: forall (l :: Type -> Type) a. Language l => EGraph a l
- representM :: forall (m :: Type -> Type) anl (l :: Type -> Type). (AnalysisM m anl l, Language l) => Fix l -> EGraphMT anl l m ClassId
- addM :: forall (m :: Type -> Type) anl (l :: Type -> Type). (AnalysisM m anl l, Language l) => ENode l -> EGraphMT anl l m ClassId
- mergeM :: forall (m :: Type -> Type) anl (l :: Type -> Type). (AnalysisM m anl l, Language l) => ClassId -> ClassId -> EGraphMT anl l m ClassId
- rebuildM :: forall (m :: Type -> Type) anl (l :: Type -> Type). (AnalysisM m anl l, Language l) => EGraphMT anl l m ()
- type EGraphM a (l :: Type -> Type) = State (EGraph a l)
- type EGraphMT a (l :: Type -> Type) = StateT (EGraph a l)
- runEGraphM :: forall anl (l :: Type -> Type) a. EGraph anl l -> EGraphM anl l a -> (a, EGraph anl l)
- runEGraphMT :: forall anl (l :: Type -> Type) m a. EGraph anl l -> EGraphMT anl l m a -> m (a, EGraph anl l)
- data EGraph analysis (language :: Type -> Type)
- 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
Threading e-graphs in a stateful computation
These are the same operations over e-graphs as in Graph,
but defined in the context of a State monad threading around the e-graph.
egraph :: forall (l :: Type -> Type) anl a. 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 :: forall anl (l :: Type -> Type). (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 :: forall anl (l :: Type -> Type). (Analysis anl l, Language l) => ENode l -> EGraphM anl l ClassId Source #
Add an e-node to the e-graph
merge :: forall anl (l :: Type -> Type). (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 :: forall anl (l :: Type -> Type). (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 :: forall (l :: Type -> Type) a. 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 :: forall a (l :: Type -> Type). 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 :: forall (l :: Type -> Type) a. Language l => EGraph a l Source #
The empty e-graph. Nothing is represented in it yet.
E-graph transformations for monadic analysis
The same e-graph operations in a stateful computation threading around
the e-graph, but for Analysis defined monadically (AnalysisM).
representM :: forall (m :: Type -> Type) anl (l :: Type -> Type). (AnalysisM m anl l, Language l) => Fix l -> EGraphMT anl l m ClassId Source #
Like represent, but for a monadic analysis
addM :: forall (m :: Type -> Type) anl (l :: Type -> Type). (AnalysisM m anl l, Language l) => ENode l -> EGraphMT anl l m ClassId Source #
Like add, but for a monadic analysis
mergeM :: forall (m :: Type -> Type) anl (l :: Type -> Type). (AnalysisM m anl l, Language l) => ClassId -> ClassId -> EGraphMT anl l m ClassId Source #
Like merge, but for a monadic analysis
rebuildM :: forall (m :: Type -> Type) anl (l :: Type -> Type). (AnalysisM m anl l, Language l) => EGraphMT anl l m () Source #
Like rebuild, but for a monadic analysis
E-graph stateful computations
type EGraphMT a (l :: Type -> Type) = StateT (EGraph a l) Source #
E-graph stateful computation over an arbitrary monad
runEGraphM :: forall anl (l :: Type -> Type) a. EGraph anl l -> EGraphM anl l a -> (a, EGraph anl l) Source #
Run EGraphM computation on a given e-graph
runEGraphMT :: forall anl (l :: Type -> Type) m a. EGraph anl l -> EGraphMT anl l m a -> m (a, EGraph anl l) Source #
Run EGraphM computation on a given e-graph over a monadic analysis
E-graph definition re-export
data EGraph analysis (language :: Type -> Type) 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.