hegg-0.3.0.0: Fast equality saturation in Haskell
Safe HaskellSafe-Inferred
LanguageHaskell2010

Data.Equality.Graph.Monad

Description

Monadic interface to e-graph stateful computations

Synopsis

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

type EGraphM a l = State (EGraph a l) Source #

E-graph stateful computation

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.

Instances

Instances details
(Show a, Show1 l) => 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.