package ego

  1. Overview
  2. Docs

Module Generic.MakeSource

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

module L : LANGUAGE
module A : ANALYSIS
module MakeAnalysisOps (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

Sourcetype 'p t = (Id.t L.shape, A.t, A.data, 'p) egraph

This type represents an EGraph parameterised over a particular language L and analysis A.

Sourcemodule 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 Language L.

Sourceval 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.

Sourceval init : A.t -> 'p t

init analysis creates a new EGraph with an initial persistent analysis state of analysis.

Sourceval class_equal : ro t -> Id.t -> Id.t -> bool

class_equal graph cls1 cls2 returns true if and only if cls1 and cls2 are congruent in the EGraph graph.

Sourceval set_data : rw t -> Id.t -> A.data -> unit

set_data graph cls data sets the analysis data for EClass cls in EGraph graph to be data.

Sourceval get_data : _ t -> Id.t -> A.data

get_data graph cls returns the analysis data for EClass cls in EGraph graph.

Sourceval get_analysis : rw t -> A.t

get_analysis graph returns the persistent analysis sate for an EGraph.

Sourceval iter_children : ro t -> Id.t -> Id.t L.shape Iter.t

iter_children graph cls returns an iterator over the elements of an eclass cls.

Sourceval 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.

Sourceval add_node : rw t -> L.t -> Id.t

add_node graph term adds the term term into the EGraph graph and returns the corresponding equivalence class.

Sourceval merge : rw t -> Id.t -> Id.t -> unit

merge graph cls1 cls2 merges the two equivalence classes cls1 and cls2.

Sourceval 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 call rebuild before running any queries or extraction.

Sourceval 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 query query in the EGraph.

Sourceval 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 in rules exactly once over the egraph graph and then returns.

Sourceval 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 in rules according to the scheduler scheduler until no further changes occur (i.e equality saturation), or until it runs out of fuel (defaults to 30) or reaches a node_limit if supplied (defaults to 10_000) or some predicate until is satisfied.

It returns a boolean indicating whether it reached equality saturation or had to terminate early.

Sourcemodule BuildRunner (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 satisfying SCHEDULER

OCaml

Innovation. Community. Security.