Module Make.Rule
This module Rule
defines the rewrite interface for the EGraph, allowing users to express relatively complex transformations of expressions of the Language L
.
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.
val make_constant : from:query -> into:query -> t
make_constant ~from ~into
creates a rewrite rule from a patternfrom
into a schemainto
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 fromfrom
tointo
that is conditionally applied based on some propertycond
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 patternfrom
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