package ego

You can search for identifiers within the package.

in-package search v0.2.0

On This Page

Parameters
Signature

ego
- Ego
  - Basic
    
    EGraph
    
    Query
    
    Rule
    
    Symbol
  - Generic
    
    ANALYSIS
    
    ANALYSIS_OPS
    
    COST
    
    GRAPH_API
    
    LANGUAGE
    
    Make
    
    A
    
    BuildRunner
    
    S
    
    L
    
    MakeAnalysisOps
    
    S
    
    Rule
    
    MakeExtractor
    
    E
    
    L
    
    MakePrinter
    
    A
    
    L
    
    Query
    
    RULE
    
    SCHEDULER
    
    Scheduler
    
    Backoff
    
    Simple
  - Id

Legend:
Library
Module
Module type
Parameter
Class
Class type

Parameters

module 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

Signature

type 'p t = (Id.t L.shape, A.t, A.data, 'p) egraph

Represents the EGraph over which the analysis operates.

val make : ro t -> Id.t L.shape -> A.data

make graph node returns the analysis data for node.

This function is called whenever a new node is added and should generate a new abstract value for the node, usually using the abstract values of its children.

Note: In terms of abstract interpretation, this function can be thought of the "abstraction" function, mapping concrete terms to their corresponding values in the abstract domain.

val merge : A.t -> A.data -> A.data -> A.data * (bool * bool)

merge st d1 d2 returns the analysis data that represents the combination of d1 and d2 and a tuple indicating whether the result differs from d1 and or d2.

This function is called whenever two equivalance classes are merged and should produce a new abstract value that represents the merge of their corresponding abstract values.

Note: In terms of abstract interpretation, this function can be thought of the least upper bound (lub), exposing the semi-lattice structure of the abstract domain.

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

modify graph class is used to introduce new children of an equivalence class whenever new information about its elements is found by the analysis.

This function is called whenever the children or abstract values of an eclass are modified and may use the abstract value of its to modify the egraph.

Note: In terms of abstract interpretation, this function can be thought of the "abstraction" function, mapping concrete terms to their corresponding values in the abstract domain.