API Documentation

A Theory is either a vector of Rule or a compiled, callable function.

Construct 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) -> Main.Metatheory.Rule

Methods

Rule(e; mod)

When 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)

Generates a tuple containing the list of formal parameters (Symbols) and the RuntimeGeneratedFunction corresponding to the right hand side of a :dynamicRule.

Signatures

genrhsfun(left::Any, right::Any, mod::Module) -> Tuple{Array{Symbol,1},RuntimeGeneratedFunctions.RuntimeGeneratedFunction{_A,_B,_C,_D} where _D where _C where _B where _A}

Methods

genrhsfun(left, right, mod)

This module contains classical rewriting functions and utilities

Imports

• Base
• Base.Meta
• Core
• Main.Metatheory.Util
• MatchCore

Compile 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 🔥

This 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!).

Compile a theory at runtime to a closure that does the pattern matching job

abstract type AbstractAnalysis

Abstract type representing an EGraph analysis, attaching values from a join semi-lattice domain to an EGraph

Fields

mutable struct EGraph

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

Fields

• U::DataStructures.IntDisjointSets

  stores the equality relations over e-class ids

• M::Dict{Int64,Main.Metatheory.EGraphs.EClassData}

  map from eclass id to eclasses

• H::Dict{Main.Metatheory.EGraphs.ENode,Int64}

• dirty::Array{Int64,1}

  worklist for ammortized upwards merging

• root::Int64

• analyses::Array{Main.Metatheory.EGraphs.AbstractAnalysis,1}

  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.

struct ExtractionAnalysis <: Main.Metatheory.EGraphs.AbstractAnalysis

An AbstractAnalysis that computes the cost of expression nodes and chooses the node with the smallest cost for each E-Class.

Fields

• egraph::Main.Metatheory.EGraphs.EGraph

• costfun::Function

• data::Dict{Int64,Tuple{Main.Metatheory.EGraphs.ENode,Number}}

Given an EGraph and two e-class ids, set the two e-classes as equal.

Signatures

merge!(G::Main.Metatheory.EGraphs.EGraph, a::Int64, b::Int64) -> Int64

Methods

merge!(G, a, b)

Inserts an e-node in an EGraph

Signatures

add!(G::Main.Metatheory.EGraphs.EGraph, n::Main.Metatheory.EGraphs.ENode) -> Main.Metatheory.EGraphs.EClass

Methods

add!(G, n)

Adds an AbstractAnalysis to an EGraph. An EGraph can only contain one analysis of type AnType.

Signatures

addanalysis!(g::Main.Metatheory.EGraphs.EGraph, AnType::Type{var"#s303"} where var"#s303"<:Main.Metatheory.EGraphs.AbstractAnalysis, args::Vararg{Any,N} where N; lazy) -> Any

Methods

addanalysis!(g, AnType, args; lazy)

Recursively traverse an Expr and insert terms into an EGraph. If e is not an Expr, then directly insert the literal into the EGraph.

Signatures

addexpr_rec!(G::Main.Metatheory.EGraphs.EGraph, e::Any) -> Main.Metatheory.EGraphs.EClass

Methods

addexpr_rec!(G, e)

Exactly like addexpr!, but instantiate pattern variables from a substitution, resulting from a pattern matcher run.

Signatures

addexprinst_rec!(G::Main.Metatheory.EGraphs.EGraph, pat::Any, sub::Base.ImmutableDict{Any,Tuple{Main.Metatheory.EGraphs.EClass,Any}}, side::Symbol) -> Main.Metatheory.EGraphs.EClass

Methods

addexprinst_rec!(G, pat, sub, side)

WARNING. This function is unstable.

Signatures

analyze!(g::Main.Metatheory.EGraphs.EGraph, analysis::Main.Metatheory.EGraphs.AbstractAnalysis, ids::Array{Int64,1}) -> Main.Metatheory.EGraphs.AbstractAnalysis

Methods

analyze!(g, analysis, ids)

A basic cost function, where the computed cost is the size (number of children) of the current expression.

Signatures

astsize(n::Main.Metatheory.EGraphs.ENode, an::Main.Metatheory.EGraphs.AbstractAnalysis) -> Any

Methods

astsize(n, an)

A 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::Main.Metatheory.EGraphs.ENode, an::Main.Metatheory.EGraphs.AbstractAnalysis) -> Any

Methods

astsize_inv(n, an)

Construct 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)

From 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::Main.Metatheory.EGraphs.EGraph, t::AbstractArray{Any,1}, v::AbstractArray{Int64,1}, sub::Base.ImmutableDict{Any,Tuple{Main.Metatheory.EGraphs.EClass,Any}}; buf) -> Array{Base.ImmutableDict{Any,Tuple{Main.Metatheory.EGraphs.EClass,Any}},1}

Methods

ematchlist(e, t, v, sub; buf)

Core algorithm of the library: the equality saturation step.

Signatures

eqsat_step!(egraph::Main.Metatheory.EGraphs.EGraph, theory::Array{Main.Metatheory.Rule,1}; scheduler, mod, match_hist, sizeout, stopwhen, matchlimit) -> Tuple{Main.Metatheory.EGraphs.Report,Main.Metatheory.EGraphs.EGraph}

Methods

eqsat_step!(egraph, theory; scheduler, mod, match_hist, sizeout, stopwhen, matchlimit)

Given an ExtractionAnalysis, extract the expression with the smallest computed cost from an EGraph

Signatures

extract!(G::Main.Metatheory.EGraphs.EGraph, extran::Main.Metatheory.EGraphs.ExtractionAnalysis) -> Any

Methods

extract!(G, extran)

Returns the canonical e-class id for a given e-class.

Signatures

find(G::Main.Metatheory.EGraphs.EGraph, a::Int64) -> Int64

Methods

find(G, a)

Recursive function that traverses an EGraph and returns a vector of all reachable e-classes from a given e-class id.

Signatures

reachable(g::Main.Metatheory.EGraphs.EGraph, id::Int64) -> Array{Int64,1}

Methods

reachable(g, id)

This function restores invariants and executes upwards merging in an EGraph. See the egg paper for more details.

Signatures

rebuild!(egraph::Main.Metatheory.EGraphs.EGraph) -> Union{Nothing, Int64}

Methods

rebuild!(egraph)

Given an EGraph and a collection of rewrite rules, execute the equality saturation algorithm.

Signatures

saturate!(egraph::Main.Metatheory.EGraphs.EGraph, theory::Array{Main.Metatheory.Rule,1}; mod, timeout, stopwhen, sizeout, matchlimit, scheduler, schedulerparams) -> Main.Metatheory.EGraphs.Report

Methods

saturate!(egraph, theory; mod, timeout, stopwhen, sizeout, matchlimit, scheduler, schedulerparams)

abstract type AbstractScheduler

Represents a rule scheduler for the equality saturation process

Fields

struct BackoffScheduler <: Main.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{Main.Metatheory.Rule,Main.Metatheory.EGraphs.Schedulers.BackoffSchedulerEntry}

• G::Main.Metatheory.EGraphs.EGraph

• theory::Array{Main.Metatheory.Rule,1}

struct ScoredScheduler <: Main.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{Main.Metatheory.Rule,Main.Metatheory.EGraphs.Schedulers.ScoredSchedulerEntry}

• G::Main.Metatheory.EGraphs.EGraph

• theory::Array{Main.Metatheory.Rule,1}

struct SimpleScheduler <: Main.Metatheory.EGraphs.Schedulers.AbstractScheduler

A simple Rewrite Scheduler that applies every rule every time

Fields

Should return true if the e-graph can be said to be saturated

Signatures

cansaturate(s::Main.Metatheory.EGraphs.Schedulers.AbstractScheduler) -> Bool

Methods

cansaturate(s)

cansaturate(s)

cansaturate(s)

cansaturate(s)

This function is called before pattern matching on the e-graph

Signatures

readstep!(s::Main.Metatheory.EGraphs.Schedulers.AbstractScheduler)

Methods

readstep!(s)

readstep!(s)

readstep!(s)

readstep!(s)

Should return true if the rule r should be skipped

Signatures

shouldskip(s::Main.Metatheory.EGraphs.Schedulers.AbstractScheduler, r::Main.Metatheory.Rule) -> Bool

Methods

shouldskip(s, r)

shouldskip(s, r)

shouldskip(s, r)

shouldskip(s, r)

This function is called after pattern matching on the e-graph

Signatures

writestep!(s::Main.Metatheory.EGraphs.Schedulers.AbstractScheduler, r::Main.Metatheory.Rule) -> Union{Nothing, Int64}

Methods

writestep!(s, r)

writestep!(s, rule)

writestep!(s, rule)

writestep!(s, r)

Definitions of various utility functions for metaprogramming

Imports

• Base
• Base.Meta
• Core
• DocStringExtensions

Add a & expression

Signatures

amp(v::Any) -> Expr

Methods

amp(v)

Breadth 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)

Breadth 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)

HARD FIX of n-arity of operators in Expr trees

Signatures

binarize!(e::Any, ops::Array{Symbol,1}) -> Any

Methods

binarize!(e, ops)

Make a block expression from an array of exprs

Signatures

block(vs::Vararg{Any,N} where N) -> Any

Methods

block(vs)

Binarize n-ary operators (+ and *) and call rmlines

Signatures

cleanast(ex::Any) -> Any

Methods

cleanast(ex)

Depth 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)

Depth 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)

Add a dollar expression

Signatures

dollar(v::Any) -> Expr

Methods

dollar(v)

Iterates 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)

Like 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)

Remove LineNumberNode from quoted blocks of code

Signatures

rmlines(e::Expr) -> Any

Methods

rmlines(e)