Generic (p.ego.0.0.6.doc.ego.Ego.Generic)

Sourcetype ('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.

Sourcemodule StringMap : Map.S with type key = string

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

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

Sourcetype rw

Encodes a read/write permission for a graph.

Sourcetype ro

Encodes a read-only permission for a graph.

Interfaces

Sourcemodule type LANGUAGE = sig ... end

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

Sourcemodule type ANALYSIS = sig ... end

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

Sourcemodule type ANALYSIS_OPS = sig ... end

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

Sourcemodule type COST = sig ... end

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

Sourcemodule type SCHEDULER = sig ... end

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

Sourcemodule type GRAPH_API = sig ... end

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

Sourcemodule 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

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

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

Source

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.

Source

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.