Rules and Theories Syntax

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.

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

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

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

Becomes

1-element Vector{Rule}:
 Rule(:(a + 5 |> :something))