Rules and Theories

Rule Syntax for Classical Rewriting

Kind	Supported in Left Hand Side	Operator	Supported in Right Hand Side
Symbolic Rule	`x` (pattern variables) $\\$`:foo` (symbol literals) $\\$`x::Type` (type assertions) $\\$`$(2 + 3)` (unquoting) $\\$`a...` (pattern variable destructuring, matches many subterms as a tuple) $\\$ Other literals are supported.	`=>`	`x` (pattern variables) $\\$`:foo`(symbol literals) $\\$`a...` (pattern variable destructuring) $\\$`$(2 + 3)` (unquoting) $\\$ Other literals are supported.
Dynamic Rule	Same as above	`\|>`	Dynamic rules can execute all valid Julia code. The pattern variables that matched are available (bound) in the r.h.s.. Other global variables in the execution module are bound. An additional variable `_lhs_expr` is bound, referring to the left hand side that matched the rule.
Equational Rule	Unsupported	`==`	Unsupported

Rule Syntax for EGraphs Rewriting

Kind	Supported in Left Hand Side	Operator	Supported in Right Hand Side
Symbolic Rule	`x` (pattern variables) $\\$`:foo` (symbol literals) $\\$`x::Type` (type assertions) $\\$`$(2 + 3)` (unquoting) $\\$ Other literals are supported. Pattern variable destructuring is not supported.	`=>`	`x` (pattern variables) $\\$`:foo`(symbol literals) $\\$`$(2 + 3)` (unquoting) $\\$ Other literals are supported.
Dynamic Rule	Same as above	`\|>`	Dynamic rules execute valid Julia code. The pattern variables that matched are available (bound) in the r.h.s.. Other global variables in the execution module are bound. An additional variable `_lhs_expr` is bound, referring to the left hand side that matched the rule. NOTE: additionally, the `_egraph` variable is bound, referring to the current `EGraph` on which rewriting is happening.
Equational Rule	Same as Symbolic Rules.	`==`	Same as left hand side of symbolic rules.

Theories are Collections and Composable

Theories are just collections, precisely vectors of the Rule object, and can be composed as regular Julia collections. The most useful way of composing theories is unioning them with the '∪' operator. You are not limited to composing theories, you can manipulate and create them at both runtime and compile time as regular vectors.

using Metatheory
using Metatheory.EGraphs
using Metatheory.Library

comm_monoid = commutative_monoid(:(*), 1);
comm_group = @theory begin
    a + 0 => a
    a + b => b + a
    a + inv(a) => 0 # inverse
    a + (b + c) => (a + b) + c
end
distrib = @theory begin
    a * (b + c) => (a * b) + (a * c)
end
t = comm_monoid ∪ comm_group ∪ distrib

8-element Array{Rule,1}:
 EqualityRule((a*b), (b*a))
 EqualityRule((a*(b*c)), ((a*b)*c))
 RewriteRule((1*a), a, false)
 RewriteRule((a+0), a, false)
 RewriteRule((a+b), (b+a), false)
 RewriteRule((a+inv(a)), 0, false)
 RewriteRule((a+(b+c)), ((a+b)+c), false)
 RewriteRule((a*(b+c)), ((a*b)+(a*c)), false)

Type Assertions and Dynamic Rules

You can use type assertions in the left hand of rules to match and access literal values both when using classic rewriting and EGraph based rewriting.

You can also use dynamic rules, defined with the |> operator, to dynamically compute values in the right hand of expressions. Dynamic rules, are similar to anonymous functions. Instead of a symbolic substitution, the right hand of a dynamic |> rule is evaluated during rewriting: the values that produced a match are bound to the pattern variables.

fold_mul = @theory begin
    a::Number * b::Number |> a*b
end
t = comm_monoid ∪ fold_mul
@areequal t (3*4) 12

true

Escaping

You can escape values in the left hand side of rules using $ just as you would do with the regular quoting/unquoting mechanism.

example = @theory begin
    a + $(3+2) |> :something
end

1-element Array{Rule,1}:
 DynamicRule((a+5), :(:something), PatVar[a], false)

Patterns

Metatheory.Rules.PatAllTerm — Type

This pattern type matches on a function application but instead of strictly matching on a head symbol, it has a pattern variable as head. It can be used for example to match arbitrary function calls.

Metatheory.Rules.PatEquiv — Type

This type of pattern will match if and only if the two subpatterns exist in the same equivalence class, in the e-graph on which the matching is performed. Can be used only in the e-graphs backend

Metatheory.Rules.PatLiteral — Type

A pattern literal will match only against an instance of itself. Example:

PatLiteral(2)

Will match only against values that are equal (using Base.(==)) to 2.

PatLiteral(:a)

Will match only against instances of the literal symbol :a.

Metatheory.Rules.PatTerm — Type

Term patterns will match on terms of the same arity and with the same function symbol (head).

Metatheory.Rules.PatTypeAssertion — Type

Type assertions on a PatVar, will match if and only if the type of the matched term for the pattern variable var is a subtype of type.

Metatheory.Rules.PatVar — Type

Pattern variables will first match on any subterm and instantiate the substitution to that subterm.

Metatheory.Rules.Pattern — Type

Abstract type representing a pattern used in all the various pattern matching backends. You can use the Pattern constructor to recursively convert an Expr (or any type satisfying Metatheory.TermInterface) to a Pattern.

Rules

Metatheory.Rules.DynamicRule — Type

Rules defined as left_hand |> right_hand are called dynamic rules. Dynamic rules behave like anonymous functions. Instead of a symbolic substitution, the right hand of a dynamic |> rule is evaluated during rewriting: matched values are bound to pattern variables as in a regular function call. This allows for dynamic computation of right hand sides.

Dynamic rule

Rule(:(a::Number * b::Number |> a*b))

Metatheory.Rules.EqualityRule — Type

Rule(:(a * b == b * a))

Metatheory.Rules.RewriteRule — Type

Rules defined as left_hand => right_hand are called symbolic rewrite rules. Application of a rewrite Rule is a replacement of the left_hand pattern with the right_hand substitution, with the correct instantiation of pattern variables. Function call symbols are not treated as pattern variables, all other identifiers are treated as pattern variables. Literals such as 5, :e, "hello" are not treated as pattern variables.

Rule(:(a * b => b * a))

Metatheory.Rules.UnequalRule — Type

This type of anti-rules is used for checking contradictions in the EGraph backend. If two terms, corresponding to the left and right hand side of an anti-rule are found in an [EGraph], saturation is halted immediately.

Metatheory.Rules.Theory — Type

A Theory is either a vector of Rule or a compiled, callable function.

Metatheory.Rules.Rule — Method

Construct a Rule from a quoted expression. You can also use the [@rule] macro to create a Rule.

Metatheory.Rules.@pruningrule — Macro

Generates a rule with the prune attribute set to true, which deletes all other nodes in an e-class when applied (pruning). Can only be used with the equality saturation e-graphs backend.