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
9-element Vector{Rule}: a * b == b * a a * b * c => a * b * c a * b * c => a * b * c 1 * a => a a + 0 => a a + b => b + a a + inv(a) => 0 a + b + c => a + b + c a * b + c => a * b + a * c
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 Vector{Rule}: a + 5 |> :something
Patterns
Metatheory.Rules.PatAllTerm
— TypeThis 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
— TypeThis 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
— TypeA 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
— TypeTerm patterns will match on terms of the same arity
and with the same function symbol (head
).
Metatheory.Rules.PatTypeAssertion
— TypeType 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
. Type assertions are supported in the left hand of rules to match and access literal values both when using classic rewriting and EGraph based rewriting. To use a type assertion pattern, add ::T
after a pattern variable in the left_hand
of a rule.
Metatheory.Rules.PatVar
— TypePattern variables will first match on any subterm and instantiate the substitution to that subterm.
Metatheory.Rules.Pattern
— TypeAbstract 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
.
Metatheory.Rules.patvars
— MethodCollects pattern variables appearing in a pattern into a vector of symbols
Rules
Metatheory.Rules.DynamicRule
— TypeRules 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
— TypeRule(:(a * b == b * a))
Metatheory.Rules.RewriteRule
— TypeRules 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
— TypeThis 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
— TypeA Theory is either a vector of Rule
or a compiled, callable function.
Metatheory.Rules.Rule
— TypeConstruct a Rule
from a quoted expression. You can also use the [@rule
] macro to create a Rule
.