Module Ego.Generic
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 StringMap.key = string
module Query : sig ... end
The module
Query
encodes generic patterns (for both matching and transformation) over expressions and is part ofEgo.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.
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.
EGraph Constructors
module MakePrinter : functor (L : LANGUAGE) -> functor (A : ANALYSIS) -> sig ... end
This functor
MakePrinter
allows users to construct EGraph printing utilities for a givenLANGUAGE
andANALYSIS
.
module MakeExtractor : functor (L : LANGUAGE) -> functor (E : COST with type node := Id.t L.shape) -> sig ... end
This functor
MakeExtractor
allows users to construct an EGraph extraction procedure for a givenLANGUAGE
andCOST
system.
module Make : functor (L : LANGUAGE) -> functor (A : ANALYSIS) -> functor (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 aLANGUAGE
, anANALYSIS
and it'sANALYSIS_OPS
.