Rules and Theories Syntax
TODO: table of syntax
The Metatheory Library
The Metatheory.Library
module contains utility functions and macros for creating rules and theories from commonly used algebraic structures and properties.
using Metatheory.Library
comm_monoid = commutative_monoid(:(*), 1)
# alternatively
comm_monoid = @commutative_monoid (*) 1
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))