Data.Equality.Graph

An e-graph efficiently represents a congruence relation over many expressions.

Based on "egg: Fast and Extensible Equality Saturation" https://arxiv.org/abs/2004.03082.

Definition of e-graph

data EGraph analysis (language :: Type -> Type)

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 a, Show (l ClassId)) => Show (EGraph a l)

Defined in Data.Equality.Graph.Internal

Methods

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

show :: EGraph a l -> String

showList :: [EGraph a l] -> ShowS

E-graph transformations

represent :: forall a (l :: Type -> Type). (Analysis a l, Language l) => Fix l -> EGraph a l -> (ClassId, EGraph a l)

Represent an expression (in it's fixed point form) in an e-graph. Returns the updated e-graph and the id from the e-class in which it was represented.

add :: forall a (l :: Type -> Type). (Analysis a l, Language l) => ENode l -> EGraph a l -> (ClassId, EGraph a l)

Add an e-node to the e-graph

If the e-node is already represented in this e-graph, the class-id of the class it's already represented in will be returned.

merge :: forall a (l :: Type -> Type). (Analysis a l, Language l) => ClassId -> ClassId -> EGraph a l -> (ClassId, EGraph a l)

Merge 2 e-classes by id

rebuild :: forall a (l :: Type -> Type). (Analysis a l, Language l) => EGraph a l -> EGraph a l

The rebuild operation processes the e-graph's current worklist, restoring the invariants of deduplication and congruence. Rebuilding is similar to other approaches in how it restores congruence; but it uniquely allows the client to choose when to restore invariants in the context of a larger algorithm like equality saturation.

Querying

find :: forall a (l :: Type -> Type). ClassId -> EGraph a l -> ClassId

Find the canonical representation of an e-class id in the e-graph

Invariant: The e-class id always exists.

canonicalize :: forall (l :: Type -> Type) a. Functor l => ENode l -> EGraph a 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 𝑐),...)

Functions on e-graphs

emptyEGraph :: forall (l :: Type -> Type) a. Language l => EGraph a l

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

newEClass :: forall (l :: Type -> Type) a. Language l => a -> EGraph a l -> (ClassId, EGraph a l)

Creates an empty e-class in an e-graph, with the explicitly given domain analysis data. (That is, an e-class with no e-nodes)

E-graph transformations for monadic analysis

These are the same operations over e-graphs as above but over a monad in which the analysis is defined. It is common to only have a valid Analysis under a monadic context. In that case, these are the functions to use -- they are just like the non-monadic ones, but have require an Analysis defined in a monadic context (AnalysisM).

representM :: forall a (l :: Type -> Type) m. (AnalysisM m a l, Language l) => Fix l -> EGraph a l -> m (ClassId, EGraph a l)

Like represent, but for a monadic analysis

addM :: forall a (l :: Type -> Type) m. (AnalysisM m a l, Language l) => ENode l -> EGraph a l -> m (ClassId, EGraph a l)

Like add, but for a monadic analysis

mergeM :: forall a (l :: Type -> Type) m. (AnalysisM m a l, Language l) => ClassId -> ClassId -> EGraph a l -> m (ClassId, EGraph a l)

Like merge, but for a monadic analysis

rebuildM :: forall a (l :: Type -> Type) m. (AnalysisM m a l, Language l) => EGraph a l -> m (EGraph a l)

Like rebuild, but for a monadic analysis

Re-exports

module Data.Equality.Graph.Classes

module Data.Equality.Graph.Nodes

module Data.Equality.Language