Edit on GitHub

API Documentation

Syntax

Metatheory.Syntax.rewrite_rhs — Method
rewrite_rhs(expr::Expr)

Rewrite the expr by dealing with :where if necessary. The :where is rewritten from, for example, ~x where f(~x) to f(~x) ? ~x : nothing.

source
Metatheory.Syntax.@capture — Macro
@capture ex pattern

Uses a Rule object to capture an expression if it matches the pattern. Returns true and injects slot variable match results into the calling scope when the pattern matches, otherwise returns false. The rule language for specifying the pattern is the same in @capture as it is in @rule. Contextual matching is not yet supported

julia> @syms a; ex = a^a;
julia> if @capture ex (~x)^(~x)
           @show x
       elseif @capture ex 2(~y)
           @show y
       end;
x = a

See also: @rule

source
Metatheory.Syntax.@rule — Macro
@rule [SLOTS...] LHS operator RHS

Creates an AbstractRule object. A rule object is callable, and takes an expression and rewrites it if it matches the LHS pattern to the RHS pattern, returns nothing otherwise. The rule language is described below.

LHS can be any possibly nested function call expression where any of the arugments can optionally be a Slot (~x) or a Segment (~x...) (described below).

SLOTS is an optional list of symbols to be interpeted as slots or segments directly (without using ~). To declare slots for several rules at once, see the @slots macro.

If an expression matches LHS entirely, then it is rewritten to the pattern in the RHS , whose local scope includes the slot matches as variables. Segment (~x) and slot variables (~~x) on the RHS will substitute the result of the matches found for these variables in the LHS.

Rule operators:

  • LHS => RHS: create a DynamicRule. The RHS is evaluated on rewrite.
  • LHS --> RHS: create a RewriteRule. The RHS is not evaluated but symbolically substituted on rewrite.
  • LHS == RHS: create a EqualityRule. In e-graph rewriting, this rule behaves like RewriteRule but can go in both directions. Doesn't work in classical rewriting
  • LHS ≠ RHS: create a UnequalRule. Can only be used in e-graphs, and is used to eagerly stop the process of rewriting if LHS is found to be equal to RHS.

Slot:

A Slot variable is written as ~x and matches a single expression. x is the name of the variable. If a slot appears more than once in an LHS expression then expression matched at every such location must be equal (as shown by isequal).

Example:

Simple rule to turn any sin into cos:

julia> r = @rule sin(~x) --> cos(~x)
sin(~x) --> cos(~x)

julia> r(:(sin(1+a)))
:(cos((1 + a)))

A rule with 2 segment variables

julia> r = @rule sin(~x + ~y) --> sin(~x)*cos(~y) + cos(~x)*sin(~y)
sin(~x + ~y) --> sin(~x) * cos(~y) + cos(~x) * sin(~y)

julia> r(:(sin(a + b)))
:(cos(a)*sin(b) + sin(a)*cos(b))

A rule that matches two of the same expressions:

julia> r = @rule sin(~x)^2 + cos(~x)^2 --> 1
sin(~x) ^ 2 + cos(~x) ^ 2 --> 1

julia> r(:(sin(2a)^2 + cos(2a)^2))
1

julia> r(:(sin(2a)^2 + cos(a)^2))
# nothing

A rule without ~

julia> r = @slots x y z @rule x(y + z) --> x*y + x*z
x(y + z) --> x*y + x*z

Segment: A Segment variable matches zero or more expressions in the function call. Segments may be written by splatting slot variables (~x...).

Example:

julia> r = @rule f(~xs...) --> g(~xs...);
julia> r(:(f(1, 2, 3)))
:(g(1,2,3))

Predicates:

There are two kinds of predicates, namely over slot variables and over the whole rule. For the former, predicates can be used on both ~x and ~~x by using the ~x::f or ~~x::f. Here f can be any julia function. In the case of a slot the function gets a single matched subexpression, in the case of segment, it gets an array of matched expressions.

The predicate should return true if the current match is acceptable, and false otherwise.

julia> two_πs(x::Number) = abs(round(x/(2π)) - x/(2π)) < 10^-9
two_πs (generic function with 1 method)

julia> two_πs(x) = false
two_πs (generic function with 2 methods)

julia> r = @rule sin(~~x + ~y::two_πs + ~~z) => :(sin($(Expr(:call, :+, ~~x..., ~~z...))))
sin(~(~x) + ~(y::two_πs) + ~(~z)) --> sin(+(~(~x)..., ~(~z)...))

julia> r(:(sin(a+$(3π))))

julia> r(:(sin(a+$(6π))))
:(sin(+a))

julia> r(sin(a+6π+c))
:(sin(a + c))

Predicate function gets an array of values if attached to a segment variable (~x...).

For the predicate over the whole rule, use @rule <LHS> => <RHS> where <predicate>:

julia> predicate(x) = x === a;

julia> r = @rule ~x => ~x where f(~x);

julia> r(a)
a

julia> r(b) === nothing
true

Note that this is syntactic sugar and that it is the same as @rule ~x => f(~x) ? ~x : nothing.

Compatibility: Segment variables may still be written as (~~x), and slot (~x) and segment (~x... or ~~x) syntaxes on the RHS will still substitute the result of the matches. See also: @capture, @slots

source
Metatheory.Syntax.@slots — Macro
@slots [SLOTS...] ex

Declare SLOTS as slot variables for all @rule or @capture invocations in the expression ex. Example:

julia> @slots x y z a b c Chain([
    (@rule x^2 + 2x*y + y^2 => (x + y)^2),
    (@rule x^a * y^b => (x*y)^a * y^(b-a)),
    (@rule +(x...) => sum(x)),
])

See also: @rule, @capture

source
Metatheory.Syntax.@theory — Macro
@theory [SLOTS...] begin (LHS operator RHS)... end

Syntax sugar to define a vector of rules in a nice and readable way. Can use @slots or have the slots as the first arguments:

julia> t = @theory x y z begin 
    x * (y + z) --> (x * y) + (x * z)
    x + y       ==  (y + x)
    #...
end;

Is the same thing as writing

julia> v = [
    @rule x y z  x * (y + z) --> (x * y) + (x * z)
    @rule x y x + y == (y + x)
    #...
];
source

Patterns

Metatheory.Patterns.PatSegment — Type

If you want to match a variable number of subexpressions at once, you will need a segment pattern. A segment pattern represents a vector of subexpressions matched. You can attach a predicate g to a segment variable. In the case of segment variables g gets a vector of 0 or more expressions and must return a boolean value.

source
Metatheory.Patterns.PatTerm — Type

Term patterns will match on terms of the same arity and with the same function symbol operation and expression head exprhead.

source
Metatheory.Patterns.PatVar — Type
PatVar{P}(name, debrujin_index, predicate::P)

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

Matcher pattern may contain pattern variables with attached predicates, where predicate is a function that takes a matched expression and returns a boolean value. Such a slot will be considered a match only if f returns true.

predicate can also be a Type{<:t}, this predicate is called a type assertion. Type assertions on a PatVar, will match if and only if the type of the matched term for the pattern variable is a subtype of T.

source

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
source
Metatheory.Rules.EqualityRule — Type

An EqualityRule can is a symbolic substitution rule that can be rewritten bidirectional. Therefore, it should only be used with the EGraphs backend.

@rule ~a * ~b == ~b * ~a
source
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
source
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. 

!a ≠ a
source

Rules

Rewriters

Metatheory.Rewriters — Module

A rewriter is any function which takes an expression and returns an expression or nothing. If nothing is returned that means there was no changes applicable to the input expression.

The Rewriters module contains some types which create and transform rewriters.

  • Empty() is a rewriter which always returns nothing
  • Chain(itr) chain an iterator of rewriters into a single rewriter which applies each chained rewriter in the given order. If a rewriter returns nothing this is treated as a no-change.
  • RestartedChain(itr) like Chain(itr) but restarts from the first rewriter once on the first successful application of one of the chained rewriters.
  • IfElse(cond, rw1, rw2) runs the cond function on the input, applies rw1 if cond returns true, rw2 if it retuns false
  • If(cond, rw) is the same as IfElse(cond, rw, Empty())
  • Prewalk(rw; threaded=false, thread_cutoff=100) returns a rewriter which does a pre-order traversal of a given expression and applies the rewriter rw. Note that if rw returns nothing when a match is not found, then Prewalk(rw) will also return nothing unless a match is found at every level of the walk. threaded=true will use multi threading for traversal. thread_cutoff is the minimum number of nodes in a subtree which should be walked in a threaded spawn.
  • Postwalk(rw; threaded=false, thread_cutoff=100) similarly does post-order traversal.
  • Fixpoint(rw) returns a rewriter which applies rw repeatedly until there are no changes to be made.
  • FixpointNoCycle behaves like Fixpoint but instead it applies rw repeatedly only while it is returning new results.
  • PassThrough(rw) returns a rewriter which if rw(x) returns nothing will instead return x otherwise will return rw(x).

Imports

  • Base
  • Base.Threads
  • Core
  • TermInterface
source
Metatheory.Rewriters.FixpointNoCycle — Type
FixpointNoCycle(rw)

FixpointNoCycle behaves like Fixpoint, but returns a rewriter which applies rw repeatedly until it produces a result that was already produced before, for example, if the repeated application of rw produces results a, b, c, d, b in order, FixpointNoCycle stops because b has been already produced.

source

EGraphs

Metatheory.EGraphs.EGraph — Type
mutable struct EGraph

A concrete type representing an [EGraph]. See the egg paper for implementation details.

Fields

  • uf::IntDisjointSet

    stores the equality relations over e-class ids

  • classes::Dict{Int64, EClass}

    map from eclass id to eclasses

  • memo::Dict{AbstractENode, Int64}

    hashcons

  • dirty::Vector{Int64}

    worklist for ammortized upwards merging

  • root::Int64

  • analyses::Dict{Union{Function, Symbol}, Union{Function, Symbol}}

    A vector of analyses associated to the EGraph

  • symcache::Dict{Any, Vector{Int64}}

    a cache mapping function symbols to e-classes that contain e-nodes with that function symbol.

  • default_termtype::Type

  • termtypes::Dict{Tuple{Any, Int64}, Type}

  • numclasses::Int64

  • numnodes::Int64

  • needslock::Bool

    If we use global buffers we may need to lock. Defaults to true.

  • buffer::Vector{Base.ImmutableDict{Int64, Tuple{Int64, Int64}}}

    Buffer for e-matching which defaults to a global. Use a local buffer for generated functions.

  • merges_buffer::Vector{Tuple{Int64, Int64}}

    Buffer for rule application which defaults to a global. Use a local buffer for generated functions.

  • lock::ReentrantLock

source
Metatheory.EGraphs.EqualityGoal — Type
struct EqualityGoal <: SaturationGoal

This goal is reached when the exprs list of expressions are in the same equivalence class.

Fields

  • exprs::Vector{Any}

  • ids::Vector{Int64}

source
Metatheory.EGraphs.SaturationParams — Type
mutable struct SaturationParams

Configurable Parameters for the equality saturation process.

Fields

  • timeout::Int64

  • timelimit::UInt64

    Timeout in nanoseconds

  • eclasslimit::Int64

    Maximum number of eclasses allowed

  • enodelimit::Int64

  • goal::Union{Nothing, Function, SaturationGoal}

  • stopwhen::Function

  • scheduler::Type{<:Metatheory.EGraphs.Schedulers.AbstractScheduler}

  • schedulerparams::Tuple

  • threaded::Bool

  • timer::Bool

source
Metatheory.EGraphs.analyze! — Method
analyze!(egraph, analysis_name, [ECLASS_IDS])

Given an EGraph and an analysis identified by name analysis_name, do an automated bottom up trasversal of the EGraph, associating a value from the domain of analysis to each ENode in the egraph by the make function. Then, for each EClass, compute the join of the children ENodes analyses values. After analyze! is called, an analysis value will be associated to each EClass in the EGraph. One can inspect and retrieve analysis values by using hasdata and getdata.

Signatures

analyze!(g::EGraph, analysis_ref, ids::Vector{Int64}) -> Bool

Methods

analyze!(g, analysis_ref, ids)

defined at /home/runner/work/Metatheory.jl/Metatheory.jl/src/EGraphs/analysis.jl:61.

source
Metatheory.EGraphs.egraph_reconstruct_expression — Method

When extracting symbolic expressions from an e-graph, we need to instruct the e-graph how to rebuild expressions of a certain type. This function must be extended by the user to add new types of expressions that can be manipulated by e-graphs.

Signatures

egraph_reconstruct_expression(T::Type{Expr}, op, args) -> Any

Methods

egraph_reconstruct_expression(T, op, args)

defined at /home/runner/work/Metatheory.jl/Metatheory.jl/src/EGraphs/egraph.jl:534.

source
Metatheory.EGraphs.islazy — Method
islazy(::Val{analysis_name})

Should return true if the EGraph Analysis an is lazy and false otherwise. A lazy EGraph Analysis is computed only when analyze! is called. Non-lazy analyses are instead computed on-the-fly every time ENodes are added to the EGraph or EClasses are merged.

Signatures

islazy(analysis_name::Val{analysis_name}) -> Bool

Methods

islazy(_)

defined at /home/runner/work/Metatheory.jl/Metatheory.jl/src/EGraphs/analysis.jl:14.

islazy(analysis_name)

defined at /home/runner/work/Metatheory.jl/Metatheory.jl/src/EGraphs/analysis.jl:15.

islazy(_)

defined at /home/runner/work/Metatheory.jl/Metatheory.jl/src/EGraphs/analysis.jl:135.

source

EGraph Schedulers

Metatheory.EGraphs.Schedulers.BackoffScheduler — Type
mutable struct BackoffScheduler <: Metatheory.EGraphs.Schedulers.AbstractScheduler

A Rewrite Scheduler that implements exponential rule backoff. For each rewrite, there exists a configurable initial match limit. If a rewrite search yield more than this limit, then we ban this rule for number of iterations, double its limit, and double the time it will be banned next time.

This seems effective at preventing explosive rules like associativity from taking an unfair amount of resources.

Fields

  • data::IdDict{AbstractRule, Metatheory.EGraphs.Schedulers.BackoffSchedulerEntry}

  • G::EGraph

  • theory::Vector{<:AbstractRule}

  • curr_iter::Int64

source
Metatheory.EGraphs.Schedulers.ScoredScheduler — Type
mutable struct ScoredScheduler <: Metatheory.EGraphs.Schedulers.AbstractScheduler

A Rewrite Scheduler that implements exponential rule backoff. For each rewrite, there exists a configurable initial match limit. If a rewrite search yield more than this limit, then we ban this rule for number of iterations, double its limit, and double the time it will be banned next time.

This seems effective at preventing explosive rules like associativity from taking an unfair amount of resources.

Fields

  • data::IdDict{AbstractRule, Metatheory.EGraphs.Schedulers.ScoredSchedulerEntry}

  • G::EGraph

  • theory::Vector{<:AbstractRule}

  • curr_iter::Int64

source
Metatheory.EGraphs.Schedulers.inform! — Function

This function is called after pattern matching on the e-graph, informs the scheduler about the yielded matches. Returns false if the matches should not be yielded and ignored. 

inform!(s::AbstractScheduler, r::AbstractRule, n_matches)

Signatures

Methods

inform!(s, r, n_matches)

defined at /home/runner/work/Metatheory.jl/Metatheory.jl/src/EGraphs/Schedulers.jl:68.

inform!(s, rule, n_matches)

defined at /home/runner/work/Metatheory.jl/Metatheory.jl/src/EGraphs/Schedulers.jl:123.

inform!(s, rule, n_matches)

defined at /home/runner/work/Metatheory.jl/Metatheory.jl/src/EGraphs/Schedulers.jl:234.

source