package ego

  1. Overview
  2. Docs

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

type t

Represents rewrite rules over the language of the EGraph.

type query

Represents a pattern over the language of the EGraph - it can either be used to match and bind a particular subpattern in an expression, or can be used to express the output schema for a rewrite.

type 'p egraph

Represents an EGraph with read/write permissions 'p.

val make_constant : from:query -> into:query -> t

make_constant ~from ~into creates a rewrite rule from a pattern from into a schema into that applies a purely syntactic transformation.

val make_conditional : from:query -> into:query -> cond:(rw egraph -> Id.t -> Id.t StringMap.t -> bool) -> t

make_conditional ~from ~into ~cond creates a syntactic rewrite rule from from to into that is conditionally applied based on some property cond of the EGraph, the root eclass of the sub-expression being transformed and the eclasses of all bound variables.

val make_dynamic : from:query -> generator:(rw egraph -> Id.t -> Id.t StringMap.t -> query option) -> t

make_dynamic ~from ~generator creates a dynamic rewrite rule from a pattern from into a schema that is conditionally generated based on properties of the EGraph, the root eclass of the sub-expression being transformed and the eclasses of all bound variables