package ego

  1. Overview
  2. Docs

This module GRAPH_API represents the interface through which EClass analyses can interact with an EGraph.

type 'p t

Represents an EGraph with read permissions 'p.

type data

Represents the additional analysis information that we will be attached to each EClass.

type analysis

Represents the persistent state of the analysis.

type 'a shape

Represents the shape of expressions in the language.

type node

Represents concrete terms of expressions in the language

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 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 iter_children : ro t -> Id.t -> Id.t shape Iter.t

iter_children graph cls returns an iterator over the children of the current EClass.

val set_data : rw t -> Id.t -> data -> unit

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

val get_data : ro t -> Id.t -> data

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

val get_analysis : rw t -> analysis

get_analysis graph returns the persistent analysis sate for an EGraph.

val add_node : rw t -> node -> 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.