Data.Equality.Graph.Monad

Monadic interface to e-graph stateful computations

Documentation

egraph :: Language l => EGraphM l a -> (a, EGraph l)

Run EGraph computation on an empty e-graph

Example

egraph $ do
 id1 <- represent t1
 id2 <- represent t2
 merge id1 id2

represent :: Language l => Fix l -> EGraphM l ClassId

Represent an expression (Fix l) in an e-graph by recursively representing sub expressions

add :: Language l => ENode l -> EGraphM l ClassId

Add an e-node to the e-graph

merge :: Language l => ClassId -> ClassId -> EGraphM l ClassId

Merge two e-classes by id

E-graph invariants may be broken by merging, and rebuild should be used eventually to restore them

rebuild :: Language l => EGraphM l ()

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 l -> ENode l

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 l -> ClassId

Find the canonical representation of an e-class id in the e-graph Invariant: The e-class id always exists.

emptyEGraph :: Language l => EGraph l

The empty e-graph. Nothing is represented in it yet.

E-graph stateful computations

type EGraphM s = State (EGraph s)

E-graph stateful computation

runEGraphM :: EGraph l -> EGraphM l a -> (a, EGraph l)

Run EGraphM computation on a given e-graph

E-graph definition re-export

data EGraph l

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

(Show (Domain l), Show1 l) => Show (EGraph l)

Defined in Data.Equality.Graph.Internal

Methods

showsPrec :: Int -> EGraph l -> ShowS

show :: EGraph l -> String

showList :: [EGraph 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.

• modify f = get >>= (put . f)

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.

• gets f = liftM f get