ego 0.0.6 (latest) · OCaml Package

This module implements a generic EGraph-based equality saturation engine that operates over arbitrary user-defined languages and provides support for extensible custom user-defined EClass analyses.

The main interface to EGraph is provided by the functor Make which constructs an EGraph given a LANGUAGE and ANALYSIS, ANALYSIS_OPS.

You may want to check out the quick start guide.

type ('node, 'analysis, 'data, 'permission) egraph

A generic representation of an EGraph, parameterised over the language term types 'node, analysis state 'analysis and data 'data and read permissions 'permission.

module StringMap : Stdlib.Map.S with type key = string

module Query : sig ... end

The module Query encodes generic patterns (for both matching and transformation) over expressions and is part of Ego.Generic's API for expressing rewrites.

module Scheduler : sig ... end

The module Scheduler provides implementations of some generic schedulers for Ego's equality saturation engine.

Read/Write permissions

For convenience, the operations over the EGraph are split into those which read and write to the graph rw t and those that are read-only ro t. When defining the analysis operations, certain operations assume that the graph is not modified, so these anotations will help users to avoid violating the internal invariants of the data structure.

type rw

Encodes a read/write permission for a graph.

type ro

Encodes a read-only permission for a graph.

Interfaces

module type LANGUAGE = sig ... end

The LANGUAGE module type represents the definition of an arbitrary language for use with an EGraph.

module type ANALYSIS = sig ... end

The module type ANALYSIS encodes the data-types for an abstract EClass analysis over EGraphs.

module type ANALYSIS_OPS = sig ... end

The module type ANALYSIS_OPS defines the main operations for an EClass analysis over an EGraph.

module type COST = sig ... end

The module type COST represents the definition of some arbitrary cost system for ranking expressions over some language.

module type SCHEDULER = sig ... end

The module type SCHEDULER represents the definition of some scheduling system for ranking rule applications during equality saturation.

module type GRAPH_API = sig ... end

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

module type RULE = sig ... end

This module type RULE defines the rewrite interface for an EGraph, allowing users to express relatively complex transformations of expressions over some language.

EGraph Constructors

module MakePrinter (L : LANGUAGE) (A : ANALYSIS) : sig ... end

This functor MakePrinter allows users to construct EGraph printing utilities for a given LANGUAGE and ANALYSIS.

module MakeExtractor
  (L : LANGUAGE)
  (E : COST with type node := Id.t L.shape) : 
  sig ... end

This functor MakeExtractor allows users to construct an EGraph extraction procedure for a given LANGUAGE and COST system.

module Make
  (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) : 
  sig ... end

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.

package ego

Read/Write permissions

Interfaces

EGraph Constructors