| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
Data.Equality.Graph
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 analysis language
- emptyEGraph :: Language l => EGraph a l
- represent :: forall a l. (Analysis a l, Language l) => Fix l -> EGraph a l -> (ClassId, EGraph a l)
- add :: forall a l. (Analysis a l, Language l) => ENode l -> EGraph a l -> (ClassId, EGraph a l)
- merge :: forall a l. (Analysis a l, Language l) => ClassId -> ClassId -> EGraph a l -> (ClassId, EGraph a l)
- rebuild :: (Analysis a l, Language l) => EGraph a l -> EGraph a l
- find :: ClassId -> EGraph a l -> ClassId
- canonicalize :: Functor l => ENode l -> EGraph a l -> ENode l
- module Data.Equality.Graph.Classes
- module Data.Equality.Graph.Nodes
- module Data.Equality.Language
Definition of e-graph
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.
Functions on e-graphs
emptyEGraph :: Language l => EGraph a l Source #
The empty e-graph. Nothing is represented in it yet.
Transformations
represent :: forall a l. (Analysis a l, Language l) => Fix l -> EGraph a l -> (ClassId, EGraph a l) Source #
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. (Analysis a l, Language l) => ENode l -> EGraph a l -> (ClassId, EGraph a 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 a l. (Analysis a l, Language l) => ClassId -> ClassId -> EGraph a l -> (ClassId, EGraph a l) Source #
Merge 2 e-classes by id
rebuild :: (Analysis a l, Language l) => EGraph a l -> EGraph a 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 a 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 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 𝑐),...)
Re-exports
module Data.Equality.Graph.Classes
module Data.Equality.Graph.Nodes
module Data.Equality.Language