Module Generic.Make
This functor Make
serves as the main interface to Ego's generic EGraphs, and constructs an EGraph given a LANGUAGE
, an ANALYSIS
and it's ANALYSIS_OPS
.
Parameters
L : LANGUAGE
A : ANALYSIS
MakeAnalysisOps : functor (S : GRAPH_API with type 'p t = (Id.t L.shape, A.t, A.data, 'p) egraph and type analysis := A.t and type data := A.data and type 'a shape := 'a L.shape and type node := L.t) -> ANALYSIS_OPS with type 'p t = (Id.t L.shape, A.t, A.data, 'p) egraph and type analysis := A.t and type data := A.data and type node := Id.t L.shape
Signature
type 'p t
= (Id.t L.shape, A.t, A.data, 'p) egraph
This type represents an EGraph parameterised over a particular language
L
and analysisA
.
module Rule : RULE with type query := L.op Query.t and type 'a egraph := (Id.t L.shape, A.t, A.data, 'a) egraph
This module
Rule
defines the rewrite interface for the EGraph, allowing users to express relatively complex transformations of expressions of the LanguageL
.
val freeze : rw t -> ro t
freeze graph
returns a read-only reference to the EGraph.Note: it is safe to modify
graph
after passing it to freeze, this method is mainly intended to allow using the read-only APIs of the EGraph when you have a RW instance of the EGraph.
val init : A.t -> 'p t
init analysis
creates a new EGraph with an initial persistent analysis state ofanalysis
.
val class_equal : ro t -> Id.t -> Id.t -> bool
class_equal graph cls1 cls2
returns true if and only ifcls1
andcls2
are congruent in the EGraphgraph
.
val set_data : rw t -> Id.t -> A.data -> unit
set_data graph cls data
sets the analysis data for EClasscls
in EGraphgraph
to bedata
.
val get_data : _ t -> Id.t -> A.data
get_data graph cls
returns the analysis data for EClasscls
in EGraphgraph
.
val get_analysis : rw t -> A.t
get_analysis graph
returns the persistent analysis sate for an EGraph.
val iter_children : ro t -> Id.t -> Id.t L.shape Iter.t
iter_children graph cls
returns an iterator over the elements of an eclasscls
.
val to_dot : (Id.t L.shape, A.t, A.data, _) egraph -> Odot.graph
to_dot graph
converts an EGraph into a Graphviz representation for debugging.
val add_node : rw t -> L.t -> Id.t
add_node graph term
adds the termterm
into the EGraphgraph
and returns the corresponding equivalence class.
val merge : rw t -> Id.t -> Id.t -> unit
merge graph cls1 cls2
merges the two equivalence classescls1
andcls2
.
val rebuild : rw t -> unit
rebuild graph
restores the internal invariants of the graph.Note: If you call
merge
manually (i.e outside of analysis functions), you must callrebuild
before running any queries or extraction.
val find_matches : ro t -> L.op Query.t -> (Id.t * Id.t StringMap.t) Iter.t
find_matches graph query
returns an iterator over each match of the queryquery
in the EGraph.
val apply_rules : (Id.t L.shape, A.t, A.data, rw) egraph -> Rule.t list -> unit
apply_rules graph rules
runs each of the rewrites inrules
exactly once over the egraphgraph
and then returns.
val run_until_saturation : ?scheduler:Scheduler.Backoff.t -> ?node_limit:[ `Bounded of int | `Unbounded ] -> ?fuel:[ `Bounded of int | `Unbounded ] -> ?until:((Id.t L.shape, A.t, A.data, rw) egraph -> bool) -> (Id.t L.shape, A.t, A.data, rw) egraph -> Rule.t list -> bool
run_until_saturation ?scheduler ?node_limit ?fuel ?until graph rules
repeatedly each one of the rewrites inrules
according to the schedulerscheduler
until no further changes occur (i.e equality saturation), or until it runs out offuel
(defaults to 30) or reaches anode_limit
if supplied (defaults to 10_000) or some predicateuntil
is satisfied.It returns a boolean indicating whether it reached equality saturation or had to terminate early.
module BuildRunner : functor (S : SCHEDULER with type 'a egraph := (Id.t L.shape, A.t, A.data, rw) egraph and type rule := Rule.t) -> sig ... end
The module
BuildRunner
allows users to supply their own custom domain-specific scheduling strategies for equality saturation by supplying a corresponding Scheduling module satisfyingSCHEDULER