hegg-0.5.0.0: Fast equality saturation in Haskell
Safe HaskellNone
LanguageHaskell2010

Data.Equality.Graph.Monad

Description

Monadic interface to e-graph stateful computations

Synopsis

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 EGraphM a (l :: Type -> Type) = State (EGraph a l) Source #

E-graph stateful computation

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.

Instances

Instances details
(Show a, Show (l ClassId)) => Show (EGraph a l) Source # 
Instance details

Defined in Data.Equality.Graph.Internal

Methods

showsPrec :: Int -> EGraph a l -> ShowS #

show :: EGraph a l -> String #

showList :: [EGraph a l] -> ShowS #

State monad re-exports

modify :: forall (m :: Type -> Type) s. Monad m => (s -> s) -> StateT s m () #

modify f is an action that updates the state to the result of applying f to the current state.

get :: forall (m :: Type -> Type) s. Monad m => StateT s m s #

Fetch the current value of the state within the monad.

gets :: forall (m :: Type -> Type) s a. Monad m => (s -> a) -> StateT s m a #

Get a specific component of the state, using a projection function supplied.