Safe Haskell	Safe-Inferred
Language	Haskell2010

Data.Equality.Graph

Contents

Definition of e-graph
Functions on e-graphs
- Transformations
- Querying
Re-exports

Description

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.

Synopsis

data EGraph l = EGraph {
- unionFind :: !ReprUnionFind
- classes :: !(ClassIdMap (EClass l))
- memo :: !(Memo l)
- worklist :: !(Worklist l)
- analysisWorklist :: !(Worklist l)
}
type Memo l = NodeMap l ClassId
type Worklist l = NodeMap l ClassId
emptyEGraph :: Language l => EGraph l
add :: forall l. Language l => ENode l -> EGraph l -> (ClassId, EGraph l)
merge :: forall l. Language l => ClassId -> ClassId -> EGraph l -> (ClassId, EGraph l)
rebuild :: Language l => EGraph l -> EGraph l
find :: ClassId -> EGraph l -> ClassId
canonicalize :: Functor l => ENode l -> EGraph l -> ENode l
module Data.Equality.Graph.Classes
module Data.Equality.Graph.Nodes
module Data.Equality.Language

Definition of e-graph

data EGraph l 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.

Constructors

EGraph

Fields

unionFind :: !ReprUnionFind
Union find like structure to find canonical representation of an e-class id
classes :: !(ClassIdMap (EClass l))
Map canonical e-class ids to their e-classes
memo :: !(Memo l)
Hashcons maps all canonical e-nodes to their e-class ids
worklist :: !(Worklist l)
Worklist of e-class ids that need to be upward merged
analysisWorklist :: !(Worklist l)
Like worklist but for analysis repairing

Instances

Instances details

(Show (Domain l), Show1 l) => Show (EGraph l) Source #
Instance details Defined in Data.Equality.Graph Methods showsPrec :: Int -> EGraph l -> ShowS # show :: EGraph l -> String # showList :: [EGraph l] -> ShowS #

type Memo l = NodeMap l ClassId Source #

The hashcons 𝐻 is a map from e-nodes to e-class ids

type Worklist l = NodeMap l ClassId Source #

Maintained worklist of e-class ids that need to be “upward merged”

Functions on e-graphs

emptyEGraph :: Language l => EGraph l Source #

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

Transformations

add :: forall l. Language l => ENode l -> EGraph l -> (ClassId, EGraph l) Source #

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 l. Language l => ClassId -> ClassId -> EGraph l -> (ClassId, EGraph l) Source #

Merge 2 e-classes by id

rebuild :: Language l => EGraph l -> EGraph l Source #

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 :: ClassId -> EGraph l -> ClassId Source #

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

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

Re-exports

module Data.Equality.Graph.Classes

module Data.Equality.Graph.Nodes

module Data.Equality.Language