API Documentation
Metatheory
Metatheory.Theory
— TypeA Theory is either a vector of Rule
or a compiled, callable function.
Metatheory.Rule
— MethodConstruct a Rule
from a quoted expression. You can also use the [@rule
] macro to create a Rule
.
Symbolic Rules
Rules defined as left_hand => right_hand
are called symbolic
rules. Application of a symbolic
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.
Dynamic Rules
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
Type Assertions
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.
Examples
Symbolic rule
Rule(:(a * b => b * a))
Equational rule
Rule(:(a * b == b * a))
Dynamic rule
Rule(:(a::Number * b::Number |> a*b))
Signatures
Rule(e::Expr; mod) -> Rule
Methods
Rule(e; mod)
Metatheory.eval_types_in_assertions
— MethodWhen creating a theory, type assertions in the left hand contain symbols. We want to replace the type symbols with the real type values, to fully support the subtyping mechanism during pattern matching.
Signatures
eval_types_in_assertions(x::Any, mod::Module) -> Any
Methods
eval_types_in_assertions(x, mod)
Metatheory.genrhsfun
— MethodGenerates the RuntimeGeneratedFunction
corresponding to the right hand side of a :dynamic
Rule
.
Signatures
genrhsfun(r::Rule, mod::Module) -> RuntimeGeneratedFunctions.RuntimeGeneratedFunction{_A,_B,_C,_D} where _D where _C where _B where _A
Methods
genrhsfun(r, mod)
Metatheory.Classic
Metatheory.Classic
— ModuleThis module contains classical rewriting functions and utilities
Imports
Base
Base.Meta
Core
MatchCore
Metatheory.Util
Metatheory.Classic.compile_theory
— MethodCompile a theory to a closure that does the pattern matching job Returns a RuntimeGeneratedFunction, which does not use eval and is as fast as a regular Julia anonymous function 🔥
Metatheory.Classic.rewrite
— MethodThis function executes a classical rewriting algorithm on a Julia expression ex
. Classical rewriting applies rule in order with a fixed point iteration:
This algorithm heavily relies on RuntimeGeneratedFunctions.jl and the MatchCore pattern matcher. NOTE: this does not involve the use of EGraphs.EGraph
or equality saturation (EGraphs.saturate!
). When using rewrite
, be aware of infinite loops: Since rules are matched in order in every iteration, it is possible that commonly used symbolic rules such as commutativity or associativity of operators may cause this algorithm to have a cycling computation instantly. This algorithm detects cycling computation by keeping an history of hashes, and instantly returns when a cycle is detected.
This algorithm is suitable for simple, deterministic symbolic rewrites. For more advanced use cases, where it is needed to apply multiple rewrites at the same time, or it is known that rules are causing loops, please use EGraphs.EGraph
and equality saturation (EGraphs.saturate!
).
Metatheory.Classic.@compile_theory
— MacroCompile a theory at runtime to a closure that does the pattern matching job
Metatheory.EGraphs
Metatheory.EGraphs.ClassMem
— TypeAbstract type representing an EGraph
analysis, attaching values from a join semi-lattice domain to an EGraph
Metatheory.EGraphs.EGraph
— Typemutable struct EGraph
A concrete type representing an [EGraph
]. See the egg paper for implementation details
Fields
uf::DataStructures.IntDisjointSets
stores the equality relations over e-class ids
emap::Dict{Int64,Metatheory.EGraphs.EClass}
map from eclass id to eclasses
hashcons::Dict{Metatheory.EGraphs.ENode,Int64}
dirty::Array{Int64,1}
worklist for ammortized upwards merging
root::Int64
analyses::Set{Type{var"#s309"} where var"#s309"<:Metatheory.EGraphs.AbstractAnalysis}
A vector of analyses associated to the EGraph
symcache::Dict{Any,Array{Int64,1}}
a cache mapping function symbols to e-classes that contain e-nodes with that function symbol.
Metatheory.EGraphs.ExtractionAnalysis
— TypeAn AbstractAnalysis
that computes the cost of expression nodes and chooses the node with the smallest cost for each E-Class. This abstract type is parametrised by a function F. This is useful for the analysis storage in EClass
Metatheory.EGraphs.SaturationParams
— Typemutable struct SaturationParams
Configurable Parameters for the equality saturation process.
Fields
timeout::Int64
Default: 7
sizeout::Int64
Default: 2 ^ 14
matchlimit::Int64
Default: 5000
eclasslimit::Int64
Default: 5000
stopwhen::Function
Default: ()->begin #= /juliateam/.julia/packages/Metatheory/j9P5S/src/EGraphs/saturation_params.jl:12 =# false end
scheduler::Type{var"#s309"} where var"#s309"<:Metatheory.EGraphs.Schedulers.AbstractScheduler
Default: BackoffScheduler
schedulerparams::Tuple
Default: ()
Base.merge!
— MethodGiven an EGraph
and two e-class ids, set the two e-classes as equal.
Signatures
merge!(g::Metatheory.EGraphs.EGraph, a::Int64, b::Int64) -> Int64
Methods
merge!(g, a, b)
Metatheory.EGraphs.add!
— MethodInserts an e-node in an EGraph
Signatures
add!(g::Metatheory.EGraphs.EGraph, n::Metatheory.EGraphs.ENode) -> Metatheory.EGraphs.EClass
Methods
add!(g, n)
Metatheory.EGraphs.addexpr_rec!
— MethodMetatheory.EGraphs.addexprinst_rec!
— MethodExactly like addexpr!
, but instantiate pattern variables from a substitution, resulting from a pattern matcher run.
Signatures
addexprinst_rec!(G::Metatheory.EGraphs.EGraph, pat::Any, sub::Base.ImmutableDict{Any,Tuple{Metatheory.EGraphs.EClass,Any}}, side::Symbol, r::Rule) -> Metatheory.EGraphs.EClass
Methods
addexprinst_rec!(G, pat, sub, side, r)
Metatheory.EGraphs.analyze!
— MethodWARNING. This function is unstable. An EGraph
can only contain one analysis of type an
.
Signatures
analyze!(g::Metatheory.EGraphs.EGraph, an::Type{var"#s305"} where var"#s305"<:Metatheory.EGraphs.AbstractAnalysis, ids::Array{Int64,1}) -> Bool
Methods
analyze!(g, an, ids)
Metatheory.EGraphs.astsize
— MethodA basic cost function, where the computed cost is the size (number of children) of the current expression.
Signatures
astsize(n::Metatheory.EGraphs.ENode, g::Metatheory.EGraphs.EGraph, an::Type{var"#s307"} where var"#s307"<:Metatheory.EGraphs.AbstractAnalysis) -> Any
Methods
astsize(n, g, an)
Metatheory.EGraphs.astsize_inv
— MethodA basic cost function, where the computed cost is the size (number of children) of the current expression, times -1. Strives to get the largest expression
Signatures
astsize_inv(n::Metatheory.EGraphs.ENode, g::Metatheory.EGraphs.EGraph, an::Type{var"#s308"} where var"#s308"<:Metatheory.EGraphs.AbstractAnalysis) -> Any
Methods
astsize_inv(n, g, an)
Metatheory.EGraphs.clean_enode!
— MethodCanonicalize an ENode
and reset it from the hashcons.
Signatures
clean_enode!(g::Metatheory.EGraphs.EGraph, t::Metatheory.EGraphs.ENode, to::Int64) -> Metatheory.EGraphs.ENode
Methods
clean_enode!(g, t, to)
Metatheory.EGraphs.discard_value
— MethodConstruct a TimeData
from a NamedTuple
returned by @timed
Signatures
discard_value(stats::NamedTuple) -> NamedTuple{(:time, :bytes, :gctime),_A} where _A<:Tuple
Methods
discard_value(stats)
Metatheory.EGraphs.ematchlist
— MethodFrom https://www.hpl.hp.com/techreports/2003/HPL-2003-148.pdf The iterator ematchlist
matches a list of terms t
to a list of E-nodes by first finding all substitutions that match the first term to the first E-node, and then extending each such substitution in all possible ways that match the remaining terms to the remaining E-nodes. The base case of this recursion is the empty list, which requires no extension to the substitution; the other case relies on Match to find the substitutions that match the first term to the first E-node.
Signatures
ematchlist(e::Metatheory.EGraphs.EGraph, t::AbstractArray{Any,1}, v::AbstractArray{Int64,1}, sub::Base.ImmutableDict{Any,Tuple{Metatheory.EGraphs.EClass,Any}}; buf) -> Array{Base.ImmutableDict{Any,Tuple{Metatheory.EGraphs.EClass,Any}},1}
Methods
ematchlist(e, t, v, sub; buf)
Metatheory.EGraphs.eqsat_step!
— MethodCore algorithm of the library: the equality saturation step.
Signatures
eqsat_step!(egraph::Metatheory.EGraphs.EGraph, theory::Array{Rule,1}, mod::Module, scheduler::Metatheory.EGraphs.Schedulers.AbstractScheduler, match_hist::OrderedCollections.OrderedSet{Tuple{Rule,Base.ImmutableDict{Any,Tuple{Metatheory.EGraphs.EClass,Any}},Int64,Bool}}, params::Metatheory.EGraphs.SaturationParams) -> Tuple{Metatheory.EGraphs.Report,Metatheory.EGraphs.EGraph}
Methods
eqsat_step!(egraph, theory, mod, scheduler, match_hist, params)
Metatheory.EGraphs.extract!
— MethodGiven a cost function, extract the expression with the smallest computed cost from an EGraph
Signatures
extract!(g::Metatheory.EGraphs.EGraph, costfun::Function; root) -> Any
Methods
extract!(g, costfun; root)
Metatheory.EGraphs.extract!
— MethodGiven an ExtractionAnalysis
, extract the expression with the smallest computed cost from an EGraph
Signatures
extract!(g::Metatheory.EGraphs.EGraph, a::Type{Metatheory.EGraphs.ExtractionAnalysis{F}} where F; root) -> Any
Methods
extract!(g, a; root)
Metatheory.EGraphs.find
— MethodReturns the canonical e-class id for a given e-class.
Signatures
find(g::Metatheory.EGraphs.EGraph, a::Int64) -> Int64
Methods
find(g, a)
Metatheory.EGraphs.reachable
— MethodRecursive function that traverses an EGraph
and returns a vector of all reachable e-classes from a given e-class id.
Signatures
reachable(g::Metatheory.EGraphs.EGraph, id::Int64) -> Array{Int64,1}
Methods
reachable(g, id)
Metatheory.EGraphs.rebuild!
— MethodMetatheory.EGraphs.saturate!
— MethodGiven an EGraph
and a collection of rewrite rules, execute the equality saturation algorithm.
Signatures
saturate!(egraph::Metatheory.EGraphs.EGraph, theory::Array{Rule,1}; mod) -> Metatheory.EGraphs.Report
Methods
saturate!(egraph, theory; mod)
Metatheory.EGraphs.Schedulers
Metatheory.EGraphs.Schedulers.AbstractScheduler
— Typeabstract type AbstractScheduler
Represents a rule scheduler for the equality saturation process
Fields
Metatheory.EGraphs.Schedulers.BackoffScheduler
— Typestruct 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::Dict{Rule,Metatheory.EGraphs.Schedulers.BackoffSchedulerEntry}
G::Metatheory.EGraphs.EGraph
theory::Array{Rule,1}
Metatheory.EGraphs.Schedulers.ScoredScheduler
— Typestruct 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::Dict{Rule,Metatheory.EGraphs.Schedulers.ScoredSchedulerEntry}
G::Metatheory.EGraphs.EGraph
theory::Array{Rule,1}
Metatheory.EGraphs.Schedulers.SimpleScheduler
— Typestruct SimpleScheduler <: Metatheory.EGraphs.Schedulers.AbstractScheduler
A simple Rewrite Scheduler that applies every rule every time
Fields
Metatheory.EGraphs.Schedulers.cansaturate
— MethodShould return true if the e-graph can be said to be saturated
Signatures
cansaturate(s::Metatheory.EGraphs.Schedulers.AbstractScheduler) -> Bool
Methods
cansaturate(s)
cansaturate(s)
cansaturate(s)
cansaturate(s)
Metatheory.EGraphs.Schedulers.readstep!
— MethodThis function is called before pattern matching on the e-graph
Signatures
readstep!(s::Metatheory.EGraphs.Schedulers.AbstractScheduler)
Methods
readstep!(s)
readstep!(s)
readstep!(s)
readstep!(s)
Metatheory.EGraphs.Schedulers.shouldskip
— MethodShould return true if the rule r
should be skipped
Signatures
shouldskip(s::Metatheory.EGraphs.Schedulers.AbstractScheduler, r::Rule) -> Bool
Methods
shouldskip(s, r)
shouldskip(s, r)
shouldskip(s, r)
shouldskip(s, r)
Metatheory.EGraphs.Schedulers.writestep!
— MethodThis function is called after pattern matching on the e-graph
Signatures
writestep!(s::Metatheory.EGraphs.Schedulers.AbstractScheduler, r::Rule) -> Union{Nothing, Int64}
Methods
writestep!(s, r)
writestep!(s, rule)
writestep!(s, rule)
writestep!(s, r)
Metatheory.Util
Metatheory.Util
— ModuleDefinitions of various utility functions for metaprogramming
Imports
Base
Base.Meta
Core
DocStringExtensions
Metatheory.Util.amp
— MethodAdd a & expression
Signatures
amp(v::Any) -> Expr
Methods
amp(v)
Metatheory.Util.bf_walk!
— MethodBreadth First Walk (Tree Prewalk) on expressions mutates expression in-place.
Signatures
bf_walk!(f::Any, e::Any, f_args::Vararg{Any,N} where N; skip, skip_call) -> Any
Methods
bf_walk!(f, e, f_args; skip, skip_call)
Metatheory.Util.bf_walk
— MethodBreadth First Walk (Tree Prewalk) on expressions. Does not mutate expressions.
Signatures
bf_walk(f::Any, e::Any, f_args::Vararg{Any,N} where N; skip, skip_call) -> Any
Methods
bf_walk(f, e, f_args; skip, skip_call)
Metatheory.Util.binarize!
— MethodHARD FIX of n-arity of operators in Expr
trees.
Signatures
binarize!(e::Any, ops::Array{Symbol,1}) -> Any
Methods
binarize!(e, ops)
Metatheory.Util.block
— MethodMake a block expression from an array of exprs
Signatures
block(vs::Vararg{Any,N} where N) -> Any
Methods
block(vs)
Metatheory.Util.cleanast
— MethodBinarize n-ary operators (+
and *
) and call rmlines
Signatures
cleanast(ex::Any) -> Any
Methods
cleanast(ex)
Metatheory.Util.df_walk!
— MethodDepth First Walk (Tree Postwalk) on expressions, mutates expression in-place.
Signatures
df_walk!(f::Any, e::Any, f_args::Vararg{Any,N} where N; skip, skip_call) -> Any
Methods
df_walk!(f, e, f_args; skip, skip_call)
Metatheory.Util.df_walk
— MethodDepth First Walk (Tree Postwalk) on expressions. Does not mutate expressions.
Signatures
df_walk(f::Any, e::Any, f_args::Vararg{Any,N} where N; skip, skip_call) -> Any
Methods
df_walk(f, e, f_args; skip, skip_call)
Metatheory.Util.dollar
— MethodAdd a dollar expression
Signatures
dollar(v::Any) -> Expr
Methods
dollar(v)
Metatheory.Util.normalize
— MethodIterates a function f
on datum
until a fixed point is reached where f(x) == x
Signatures
normalize(f::Any, datum::Any, fargs::Vararg{Any,N} where N; callback) -> Any
Methods
normalize(f, datum, fargs; callback)
Metatheory.Util.normalize_nocycle
— MethodLike normalize
but keeps a vector of hashes to detect cycles, returns the current datum when a cycle is detected
Signatures
normalize_nocycle(f::Any, datum::Any, fargs::Vararg{Any,N} where N; callback) -> Any
Methods
normalize_nocycle(f, datum, fargs; callback)
Metatheory.Util.rmlines
— MethodRemove LineNumberNode from quoted blocks of code
Signatures
rmlines(e::Expr) -> Any
Methods
rmlines(e)