ego 0.0.6 (latest) · OCaml Package

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

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 analysis A.

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

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 of analysis.

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

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

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

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

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 eclass cls.

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 term term into the EGraph graph and returns the corresponding equivalence class.

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

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

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 call rebuild 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 query query 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 in rules exactly once over the egraph graph 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 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.

module 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

package ego

Parameters

Signature