diff --git a/dev/api/index.html b/dev/api/index.html index 2a896497..6849aea0 100644 --- a/dev/api/index.html +++ b/dev/api/index.html @@ -1,11 +1,11 @@ -API Documentation · Metatheory.jl
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;
+API Documentation · Metatheory.jl
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)
+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)))
@@ -46,11 +46,11 @@
 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([
+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 
+])
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)
     #...
@@ -58,25 +58,25 @@
     @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.FunctionGoal — Type
struct FunctionGoal <: SaturationGoal
Boolean valued function as an arbitrary saturation goal. User supplied function must take an EGraph as the only parameter.
Fields
  • fun::Function
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, 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) -> Expr
-
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
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
Metatheory.EGraphs.saturate! — Function
Given an EGraph and a collection of rewrite rules, execute the equality saturation algorithm.
Signatures
saturate!(g::EGraph, theory::Vector{<:AbstractRule}) -> Metatheory.EGraphs.SaturationReport
+];
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.FunctionGoal — Type
struct FunctionGoal <: SaturationGoal
Boolean valued function as an arbitrary saturation goal. User supplied function must take an EGraph as the only parameter.
Fields
  • fun::Function
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, 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) -> Expr
+
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
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

+saturate!(g, theory, params)

defined at /home/runner/work/Metatheory.jl/Metatheory.jl/src/EGraphs/saturation.jl:286.

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
diff --git a/dev/egraphs/index.html b/dev/egraphs/index.html index c3cf5ee8..49e1a9f7 100644 --- a/dev/egraphs/index.html +++ b/dev/egraphs/index.html @@ -134,4 +134,4 @@ custom_analysis(:(2*a)) # :even custom_analysis(:(3*3)) # :odd custom_analysis(:(3*(2+a)*2)) # :even -custom_analysis(:(3y * (2x*y))) # :even +custom_analysis(:(3y * (2x*y))) # :even diff --git a/dev/index.html b/dev/index.html index f64576d1..1638fcc9 100644 --- a/dev/index.html +++ b/dev/index.html @@ -5,4 +5,4 @@ -

+

diff --git a/dev/rewrite/index.html b/dev/rewrite/index.html index aa3f2960..12043232 100644 --- a/dev/rewrite/index.html +++ b/dev/rewrite/index.html @@ -34,4 +34,4 @@ distrib = @theory a b c begin a * (b + c) => (a * b) + (a * c) end -t = comm_monoid ∪ comm_group ∪ distrib

Composing rewriters

Rules may be chained together into more sophisticated rewriters to avoid manual application of the rules. A rewriter is any callable object 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 Rules we created above are rewriters.

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

Chaining rewriters

Several rules may be chained to give chain of rules. Chain is an array of rules which are subsequently applied to the expression. Important feature of Chain is that it returns the expression instead of nothing if it doesn't change the expression It is important to notice, that chain is ordered, so if rules are in different order it wouldn't work the same as in earlier example

One way to circumvent the problem of order of applying rules in chain is to use RestartedChain, it restarts the chain after each successful application of a rule, so after a rule is hit it (re)starts again and it can apply all the other rules to the resulting expression. You can also use Fixpoint to apply the rules until there are no changes.

+t = comm_monoid ∪ comm_group ∪ distrib

Composing rewriters

Rules may be chained together into more sophisticated rewriters to avoid manual application of the rules. A rewriter is any callable object 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 Rules we created above are rewriters.

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

Chaining rewriters

Several rules may be chained to give chain of rules. Chain is an array of rules which are subsequently applied to the expression. Important feature of Chain is that it returns the expression instead of nothing if it doesn't change the expression It is important to notice, that chain is ordered, so if rules are in different order it wouldn't work the same as in earlier example

One way to circumvent the problem of order of applying rules in chain is to use RestartedChain, it restarts the chain after each successful application of a rule, so after a rule is hit it (re)starts again and it can apply all the other rules to the resulting expression. You can also use Fixpoint to apply the rules until there are no changes.

diff --git a/dev/search/index.html b/dev/search/index.html index 10ac593e..77169264 100644 --- a/dev/search/index.html +++ b/dev/search/index.html @@ -1,2 +1,2 @@ -Search · Metatheory.jl

Loading search...

    +Search · Metatheory.jl

    Loading search...

      diff --git a/dev/search_index.js b/dev/search_index.js index 6b5cc358..c68034b4 100644 --- a/dev/search_index.js +++ b/dev/search_index.js @@ -1,3 +1,3 @@ var documenterSearchIndex = {"docs": -[{"location":"tutorials/while_interpreter/","page":"Write a very tiny Turing Complete language in Julia.","title":"Write a very tiny Turing Complete language in Julia.","text":"EditURL = \"https://github.com/JuliaSymbolics/Metatheory.jl/blob/master/test/tutorials/while_interpreter.jl\"","category":"page"},{"location":"tutorials/while_interpreter/#Write-a-very-tiny-Turing-Complete-language-in-Julia.","page":"Write a very tiny Turing Complete language in Julia.","title":"Write a very tiny Turing Complete language in Julia.","text":"","category":"section"},{"location":"tutorials/while_interpreter/","page":"Write a very tiny Turing Complete language in Julia.","title":"Write a very tiny Turing Complete language in Julia.","text":"WHILE is a very tiny Turing Complete Programming Language defined by denotational semantics. Semantics come from the excellent course notes in \"Elements of computability and complexity\" by prof. Pierpaolo Degano.","category":"page"},{"location":"tutorials/while_interpreter/","page":"Write a very tiny Turing Complete language in Julia.","title":"Write a very tiny Turing Complete language in Julia.","text":"It is a toy C-like language used to explain the core concepts of computability and Turing-completeness. The name WHILE, comes from the fact that the most complicated construct in the language is a WHILE loop. The language supports:","category":"page"},{"location":"tutorials/while_interpreter/","page":"Write a very tiny Turing Complete language in Julia.","title":"Write a very tiny Turing Complete language in Julia.","text":"A variable-value memory that can be pre-defined for program input.\nInteger arithmetics.\nBoolean logic.\nConditional if-then-else statement called cond.\nRunning a command after another with seq(c1,c2).\nRepeatedly applying a command c while a condition g holds with loop(g,c).","category":"page"},{"location":"tutorials/while_interpreter/","page":"Write a very tiny Turing Complete language in Julia.","title":"Write a very tiny Turing Complete language in Julia.","text":"This is enough to be Turing-complete!","category":"page"},{"location":"tutorials/while_interpreter/","page":"Write a very tiny Turing Complete language in Julia.","title":"Write a very tiny Turing Complete language in Julia.","text":"We are going to implement this tiny imperative language with classical rewriting rules in Metatheory.jl. WHILE is implemented in around 55 readable lines of code, and reaches around 80 lines with tests.","category":"page"},{"location":"tutorials/while_interpreter/","page":"Write a very tiny Turing Complete language in Julia.","title":"Write a very tiny Turing Complete language in Julia.","text":"The goal of this tutorial is to show an implementation of a programming language interpreter that is very, very very close to the simple theory used to describe it in a textbook. Each denotational semantics rule in the course notes is a Metatheory.jl rewrite rule, with a few extras and minor naming changes. The idea, is that Julia is a really valid didactical programming language!","category":"page"},{"location":"tutorials/while_interpreter/","page":"Write a very tiny Turing Complete language in Julia.","title":"Write a very tiny Turing Complete language in Julia.","text":"Let's load the Metatheory and Test packages.","category":"page"},{"location":"tutorials/while_interpreter/","page":"Write a very tiny Turing Complete language in Julia.","title":"Write a very tiny Turing Complete language in Julia.","text":"using Test, Metatheory","category":"page"},{"location":"tutorials/while_interpreter/#Memory","page":"Write a very tiny Turing Complete language in Julia.","title":"Memory","text":"","category":"section"},{"location":"tutorials/while_interpreter/","page":"Write a very tiny Turing Complete language in Julia.","title":"Write a very tiny Turing Complete language in Julia.","text":"The first thing that our programming language needs, is a model of the computer memory, that is going to hold the state of the programs. We define the type of WHILE's memory as a map from variables (Julia Symbols) to actual values. We want to keep things simple so in our toy programming language we are just going to use boolean or integer values. Surprisingly, we can still achieve turing completeness without having to introduce strings or any other complex data type. We are going to use the letter σ (sigma) to denote an actual value of type Mem, in simple words the state of a program in a given moment. For example, if a σ::Mem holds the value σ[:a] = 2, this means that at that given moment, in our program the variable a holds the value 2.","category":"page"},{"location":"tutorials/while_interpreter/","page":"Write a very tiny Turing Complete language in Julia.","title":"Write a very tiny Turing Complete language in Julia.","text":"Mem = Dict{Symbol,Union{Bool,Int}}","category":"page"},{"location":"tutorials/while_interpreter/","page":"Write a very tiny Turing Complete language in Julia.","title":"Write a very tiny Turing Complete language in Julia.","text":"We are now ready to define our first rewrite rule. In WHILE, un-evaluated expressions are represented by a tuple of (program, state). This simple rule tells us that, if at a given memory state σ we want to know the value of a variable v, we can simply read it from the memory and return the value.","category":"page"},{"location":"tutorials/while_interpreter/","page":"Write a very tiny Turing Complete language in Julia.","title":"Write a very tiny Turing Complete language in Julia.","text":"read_mem = @theory v σ begin\n (v::Symbol, σ::Mem) => σ[v]\nend","category":"page"},{"location":"tutorials/while_interpreter/","page":"Write a very tiny Turing Complete language in Julia.","title":"Write a very tiny Turing Complete language in Julia.","text":"Let's test this behavior. We first create a Mem, holding the variable x with value 2.","category":"page"},{"location":"tutorials/while_interpreter/","page":"Write a very tiny Turing Complete language in Julia.","title":"Write a very tiny Turing Complete language in Julia.","text":"σ₁ = Mem(:x => 2)","category":"page"},{"location":"tutorials/while_interpreter/","page":"Write a very tiny Turing Complete language in Julia.","title":"Write a very tiny Turing Complete language in Julia.","text":"Then, we define a program. Julia helps us avoid unneeded complications. Generally, to create an interpreted programming language, one would have to design a syntax for it, and then engineer components such as a lexer or a parser in order to turn the input string into a manipulable, structured program. The Julia developers were really smart. We can directly re-use the whole Julia syntax, because Julia allows us to treat programs as values. You can try this by prefixing any expression you type in the REPL inside of :( ... ) or quote ... end. If you type this in the Julia REPL:","category":"page"},{"location":"tutorials/while_interpreter/","page":"Write a very tiny Turing Complete language in Julia.","title":"Write a very tiny Turing Complete language in Julia.","text":"2 + 2","category":"page"},{"location":"tutorials/while_interpreter/","page":"Write a very tiny Turing Complete language in Julia.","title":"Write a very tiny Turing Complete language in Julia.","text":"You get the obvious result out, but if you wrap it in quote or :(...), you can see that the program will not be executed, but instead stored as an Expr.","category":"page"},{"location":"tutorials/while_interpreter/","page":"Write a very tiny Turing Complete language in Julia.","title":"Write a very tiny Turing Complete language in Julia.","text":"some_expr = :(2 + 2)","category":"page"},{"location":"tutorials/while_interpreter/","page":"Write a very tiny Turing Complete language in Julia.","title":"Write a very tiny Turing Complete language in Julia.","text":"We can use the $ unary operator to interpolate and insert values inside of quoted code.","category":"page"},{"location":"tutorials/while_interpreter/","page":"Write a very tiny Turing Complete language in Julia.","title":"Write a very tiny Turing Complete language in Julia.","text":":(2 + $(1 + 1))","category":"page"},{"location":"tutorials/while_interpreter/","page":"Write a very tiny Turing Complete language in Julia.","title":"Write a very tiny Turing Complete language in Julia.","text":"These code-manipulation utilities can be very useful, because we can completely skip the burden of having to write a new syntax for our educational programming language, and just re-use Julia's syntax. It hints us that Julia is very powerful, because you can define new semantics and customize the language's behaviour without having to leave the comfort of the Julia terminal. This is also how julia @macros work. The practice of manipulating programs in the language itself is called Metaprogramming, and you can read more about metaprogramming in Julia in the official docs.","category":"page"},{"location":"tutorials/while_interpreter/","page":"Write a very tiny Turing Complete language in Julia.","title":"Write a very tiny Turing Complete language in Julia.","text":"Let's test that our first, simple rule is working.","category":"page"},{"location":"tutorials/while_interpreter/","page":"Write a very tiny Turing Complete language in Julia.","title":"Write a very tiny Turing Complete language in Julia.","text":"program = :(x, $σ₁)\n@test rewrite(program, read_mem) == 2","category":"page"},{"location":"tutorials/while_interpreter/#Arithmetics","page":"Write a very tiny Turing Complete language in Julia.","title":"Arithmetics","text":"","category":"section"},{"location":"tutorials/while_interpreter/","page":"Write a very tiny Turing Complete language in Julia.","title":"Write a very tiny Turing Complete language in Julia.","text":"How can our programming language be turing complete if we do not include basic arithmetics? If we have an integer and a memory state, we can just keep the integer The following rules are the first cases of recursion. Given two expressions a,b, to know what's a + b in state σ, we need to know first what a and b are in state σ The last dynamic rules let us directly evaluate arithmetic operations.","category":"page"},{"location":"tutorials/while_interpreter/","page":"Write a very tiny Turing Complete language in Julia.","title":"Write a very tiny Turing Complete language in Julia.","text":"arithm_rules = @theory a b n σ begin\n (n::Int, σ::Mem) --> n\n (a + b, σ::Mem) --> (a, σ) + (b, σ)\n (a * b, σ::Mem) --> (a, σ) * (b, σ)\n (a - b, σ::Mem) --> (a, σ) - (b, σ)\n (a::Int + b::Int) => a + b\n (a::Int * b::Int) => a * b\n (a::Int - b::Int) => a - b\nend","category":"page"},{"location":"tutorials/while_interpreter/#Evaluation-strategy","page":"Write a very tiny Turing Complete language in Julia.","title":"Evaluation strategy","text":"","category":"section"},{"location":"tutorials/while_interpreter/","page":"Write a very tiny Turing Complete language in Julia.","title":"Write a very tiny Turing Complete language in Julia.","text":"We now have some nice denotational semantic rules for arithmetics, but in what order should we apply them? Metatheory.jl provides a flexible rewriter combinator library. You can read more in the Rewriters module docs.","category":"page"},{"location":"tutorials/while_interpreter/","page":"Write a very tiny Turing Complete language in Julia.","title":"Write a very tiny Turing Complete language in Julia.","text":"Given a set of rules, we can define a rewriter strategy by functionally composing rewriters. First, we want to use Chain to combine together the many rules in the theory, and to try to apply them one-by-one on our expressions.","category":"page"},{"location":"tutorials/while_interpreter/","page":"Write a very tiny Turing Complete language in Julia.","title":"Write a very tiny Turing Complete language in Julia.","text":"But should we first evaluate the outermost operations in the expression, or the innermost? Intuitively, if we have the program (1 + 2) - 3, it can hint us that we do want to first evaluate the innermost expressions. To do so, we then pass the result to the Postwalk rewriter, which recursively walks the input expression tree, and applies the rewriter first on the inner expressions, and then, on the outer, rewritten expression. (Hence the name Post-walk. Can you guess what Prewalk does?).","category":"page"},{"location":"tutorials/while_interpreter/","page":"Write a very tiny Turing Complete language in Julia.","title":"Write a very tiny Turing Complete language in Julia.","text":"The last component of our strategy is the Fixpoint combinator. This combinator repeatedly applies the rewriter on the input expression, and it does stop looping only when the output expression is the unchanged input expression.","category":"page"},{"location":"tutorials/while_interpreter/","page":"Write a very tiny Turing Complete language in Julia.","title":"Write a very tiny Turing Complete language in Julia.","text":"using Metatheory.Rewriters\nstrategy = (Fixpoint ∘ Postwalk ∘ Chain)","category":"page"},{"location":"tutorials/while_interpreter/","page":"Write a very tiny Turing Complete language in Julia.","title":"Write a very tiny Turing Complete language in Julia.","text":"In Metatheory.jl, rewrite theories are just vectors of Rules. It means we can compose them by concatenating the vectors, or elegantly using the built-in set operations provided by the Julia language.","category":"page"},{"location":"tutorials/while_interpreter/","page":"Write a very tiny Turing Complete language in Julia.","title":"Write a very tiny Turing Complete language in Julia.","text":"arithm_lang = read_mem ∪ arithm_rules","category":"page"},{"location":"tutorials/while_interpreter/","page":"Write a very tiny Turing Complete language in Julia.","title":"Write a very tiny Turing Complete language in Julia.","text":"We can define a convenience function that takes an expression, a memory state and calls our strategy.","category":"page"},{"location":"tutorials/while_interpreter/","page":"Write a very tiny Turing Complete language in Julia.","title":"Write a very tiny Turing Complete language in Julia.","text":"eval_arithm(ex, mem) = strategy(arithm_lang)(:($ex, $mem))","category":"page"},{"location":"tutorials/while_interpreter/","page":"Write a very tiny Turing Complete language in Julia.","title":"Write a very tiny Turing Complete language in Julia.","text":"Does it work?","category":"page"},{"location":"tutorials/while_interpreter/","page":"Write a very tiny Turing Complete language in Julia.","title":"Write a very tiny Turing Complete language in Julia.","text":"@test eval_arithm(:(2 + 3), Mem()) == 5","category":"page"},{"location":"tutorials/while_interpreter/","page":"Write a very tiny Turing Complete language in Julia.","title":"Write a very tiny Turing Complete language in Julia.","text":"Yay! Let's say that before the program started, the computer memory already held a variable x with value 2.","category":"page"},{"location":"tutorials/while_interpreter/","page":"Write a very tiny Turing Complete language in Julia.","title":"Write a very tiny Turing Complete language in Julia.","text":"@test eval_arithm(:(2 + x), Mem(:x => 2)) == 4","category":"page"},{"location":"tutorials/while_interpreter/#Boolean-Logic","page":"Write a very tiny Turing Complete language in Julia.","title":"Boolean Logic","text":"","category":"section"},{"location":"tutorials/while_interpreter/","page":"Write a very tiny Turing Complete language in Julia.","title":"Write a very tiny Turing Complete language in Julia.","text":"To be Turing-complete, our tiny WHILE language requires boolean logic support. There's nothing special or different from other programming languages. These rules define boolean operations to work just as you would expect, and in the same way we defined arithmetic rules for integers.","category":"page"},{"location":"tutorials/while_interpreter/","page":"Write a very tiny Turing Complete language in Julia.","title":"Write a very tiny Turing Complete language in Julia.","text":"We need to bridge together the world of integer arithmetics and boolean logic to achieve something useful. The last two rules in the theory.","category":"page"},{"location":"tutorials/while_interpreter/","page":"Write a very tiny Turing Complete language in Julia.","title":"Write a very tiny Turing Complete language in Julia.","text":"bool_rules = @theory a b σ begin\n (a::Bool || b::Bool) => (a || b)\n (a::Bool && b::Bool) => (a && b)\n !a::Bool => !a\n (a::Bool, σ::Mem) => a\n (!b, σ::Mem) => !eval_bool(b, σ)\n (a || b, σ::Mem) --> (a, σ) || (b, σ)\n (a && b, σ::Mem) --> (a, σ) && (b, σ)\n (a < b, σ::Mem) => (eval_arithm(a, σ) < eval_arithm(b, σ)) # This rule bridges together ints and bools\n (a::Int < b::Int) => (a < b)\nend\n\neval_bool(ex, mem) = strategy(bool_rules)(:($ex, $mem))","category":"page"},{"location":"tutorials/while_interpreter/","page":"Write a very tiny Turing Complete language in Julia.","title":"Write a very tiny Turing Complete language in Julia.","text":"Let's run a few tests.","category":"page"},{"location":"tutorials/while_interpreter/","page":"Write a very tiny Turing Complete language in Julia.","title":"Write a very tiny Turing Complete language in Julia.","text":"@test all(\n [\n eval_bool(:(false || false), Mem()) == false\n eval_bool(:((false || false) || !(false || false)), Mem(:x => 2)) == true\n eval_bool(:((2 < 3) && (3 < 4)), Mem(:x => 2)) == true\n eval_bool(:((2 < x) || !(3 < 4)), Mem(:x => 2)) == false\n eval_bool(:((2 < x) || !(3 < 4)), Mem(:x => 4)) == true\n ],\n)","category":"page"},{"location":"tutorials/while_interpreter/#Conditionals:-If-then-else","page":"Write a very tiny Turing Complete language in Julia.","title":"Conditionals: If-then-else","text":"","category":"section"},{"location":"tutorials/while_interpreter/","page":"Write a very tiny Turing Complete language in Julia.","title":"Write a very tiny Turing Complete language in Julia.","text":"Conditional expressions in our language take the form of cond(guard, thenbranch) or cond(guard, branch, elsebranch) It means that our program at this point will:","category":"page"},{"location":"tutorials/while_interpreter/","page":"Write a very tiny Turing Complete language in Julia.","title":"Write a very tiny Turing Complete language in Julia.","text":"Evaluate the guard expressions\nIf guard evaluates to true, then evaluate thenbranch\nIf guard evaluates to false, then evaluate elsebranch","category":"page"},{"location":"tutorials/while_interpreter/","page":"Write a very tiny Turing Complete language in Julia.","title":"Write a very tiny Turing Complete language in Julia.","text":"The first rule here is simple. If there's no elsebranch in the cond statement, we add an empty one with the skip command. Otherwise, we piggyback on the existing Julia if-then-else ternary operator. To do so, we need to evaluate the boolean expression in the guard by using the eval_bool function we defined above.","category":"page"},{"location":"tutorials/while_interpreter/","page":"Write a very tiny Turing Complete language in Julia.","title":"Write a very tiny Turing Complete language in Julia.","text":"if_rules = @theory guard t f σ begin\n (cond(guard, t), σ::Mem) --> (cond(guard, t, :skip), σ)\n (cond(guard, t, f), σ::Mem) => (eval_bool(guard, σ) ? :($t, $σ) : :($f, $σ))\nend\n\neval_if(ex, mem::Mem) = strategy(read_mem ∪ arithm_rules ∪ if_rules)(:($ex, $mem))","category":"page"},{"location":"tutorials/while_interpreter/","page":"Write a very tiny Turing Complete language in Julia.","title":"Write a very tiny Turing Complete language in Julia.","text":"And here is our working conditional","category":"page"},{"location":"tutorials/while_interpreter/","page":"Write a very tiny Turing Complete language in Julia.","title":"Write a very tiny Turing Complete language in Julia.","text":"@testset \"If Semantics\" begin\n @test 2 == eval_if(:(cond(true, x, 0)), Mem(:x => 2))\n @test 0 == eval_if(:(cond(false, x, 0)), Mem(:x => 2))\n @test 2 == eval_if(:(cond(!(false), x, 0)), Mem(:x => 2))\n @test 0 == eval_if(:(cond(!(2 < x), x, 0)), Mem(:x => 3))\nend","category":"page"},{"location":"tutorials/while_interpreter/#Writing-memory","page":"Write a very tiny Turing Complete language in Julia.","title":"Writing memory","text":"","category":"section"},{"location":"tutorials/while_interpreter/","page":"Write a very tiny Turing Complete language in Julia.","title":"Write a very tiny Turing Complete language in Julia.","text":"Our language then needs a mechanism to write in memory. We define the behavior of the store construct, which behaves like the = assignment operator in other programming languages. store(a, 5) will store the value 5 in the a variable inside the program's memory.","category":"page"},{"location":"tutorials/while_interpreter/","page":"Write a very tiny Turing Complete language in Julia.","title":"Write a very tiny Turing Complete language in Julia.","text":"write_mem = @theory sym val σ begin\n (store(sym::Symbol, val), σ) => (σ[sym] = eval_if(val, σ);\n σ)\nend","category":"page"},{"location":"tutorials/while_interpreter/#While-loops-and-sequential-computation.","page":"Write a very tiny Turing Complete language in Julia.","title":"While loops and sequential computation.","text":"","category":"section"},{"location":"tutorials/while_interpreter/","page":"Write a very tiny Turing Complete language in Julia.","title":"Write a very tiny Turing Complete language in Julia.","text":"while_rules = @theory guard a b σ begin\n (:skip, σ::Mem) --> σ\n ((:skip; b), σ::Mem) --> (b, σ)\n (seq(a, b), σ::Mem) --> (b, merge((a, σ), σ))\n merge(a::Mem, σ::Mem) => merge(σ, a)\n merge(a::Union{Bool,Int}, σ::Mem) --> σ\n (loop(guard, a), σ::Mem) --> (cond(guard, seq(a, loop(guard, a)), :skip), σ)\nend","category":"page"},{"location":"tutorials/while_interpreter/#Completing-the-language.","page":"Write a very tiny Turing Complete language in Julia.","title":"Completing the language.","text":"","category":"section"},{"location":"tutorials/while_interpreter/","page":"Write a very tiny Turing Complete language in Julia.","title":"Write a very tiny Turing Complete language in Julia.","text":"while_language = write_mem ∪ read_mem ∪ arithm_rules ∪ if_rules ∪ while_rules;\n\nusing Metatheory.Syntax: rmlines\neval_while(ex, mem) = strategy(while_language)(:($(rmlines(ex)), $mem))","category":"page"},{"location":"tutorials/while_interpreter/","page":"Write a very tiny Turing Complete language in Julia.","title":"Write a very tiny Turing Complete language in Julia.","text":"Final steps","category":"page"},{"location":"tutorials/while_interpreter/","page":"Write a very tiny Turing Complete language in Julia.","title":"Write a very tiny Turing Complete language in Julia.","text":"@testset \"While Semantics\" begin\n @test Mem(:x => 3) == eval_while(:((store(x, 3))), Mem(:x => 2))\n @test Mem(:x => 5) == eval_while(:(seq(store(x, 4), store(x, x + 1))), Mem(:x => 3))\n @test Mem(:x => 4) == eval_while(:(cond(x < 10, store(x, x + 1))), Mem(:x => 3))\n @test 10 == eval_while(:(seq(loop(x < 10, store(x, x + 1)), x)), Mem(:x => 3))\n @test 50 == eval_while(:(seq(loop(x < y, seq(store(x, x + 1), store(y, y - 1))), x)), Mem(:x => 0, :y => 100))\nend","category":"page"},{"location":"tutorials/while_interpreter/","page":"Write a very tiny Turing Complete language in Julia.","title":"Write a very tiny Turing Complete language in Julia.","text":"","category":"page"},{"location":"tutorials/while_interpreter/","page":"Write a very tiny Turing Complete language in Julia.","title":"Write a very tiny Turing Complete language in Julia.","text":"This page was generated using Literate.jl.","category":"page"},{"location":"api/#API-Documentation","page":"API Documentation","title":"API Documentation","text":"","category":"section"},{"location":"api/#Syntax","page":"API Documentation","title":"Syntax","text":"","category":"section"},{"location":"api/","page":"API Documentation","title":"API Documentation","text":"Modules = [Metatheory.Syntax]","category":"page"},{"location":"api/#Metatheory.Syntax.rewrite_rhs-Tuple{Expr}","page":"API Documentation","title":"Metatheory.Syntax.rewrite_rhs","text":"rewrite_rhs(expr::Expr)\n\nRewrite the expr by dealing with :where if necessary. The :where is rewritten from, for example, ~x where f(~x) to f(~x) ? ~x : nothing.\n\n\n\n\n\n","category":"method"},{"location":"api/#Metatheory.Syntax.rmlines-Tuple{Expr}","page":"API Documentation","title":"Metatheory.Syntax.rmlines","text":"Remove LineNumberNode from quoted blocks of code\n\n\n\n\n\n","category":"method"},{"location":"api/#Metatheory.Syntax.@capture-Tuple","page":"API Documentation","title":"Metatheory.Syntax.@capture","text":"@capture ex pattern\n\nUses 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\n\njulia> @syms a; ex = a^a;\njulia> if @capture ex (~x)^(~x)\n @show x\n elseif @capture ex 2(~y)\n @show y\n end;\nx = a\n\nSee also: @rule\n\n\n\n\n\n","category":"macro"},{"location":"api/#Metatheory.Syntax.@rule-Tuple","page":"API Documentation","title":"Metatheory.Syntax.@rule","text":"@rule [SLOTS...] LHS operator RHS\n\nCreates 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.\n\nLHS 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).\n\nSLOTS 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.\n\nIf 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.\n\nRule operators:\n\nLHS => RHS: create a DynamicRule. The RHS is evaluated on rewrite.\nLHS --> RHS: create a RewriteRule. The RHS is not evaluated but symbolically substituted on rewrite.\nLHS == 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\nLHS ≠ 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.\n\nSlot:\n\nA 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).\n\nExample:\n\nSimple rule to turn any sin into cos:\n\njulia> r = @rule sin(~x) --> cos(~x)\nsin(~x) --> cos(~x)\n\njulia> r(:(sin(1+a)))\n:(cos((1 + a)))\n\nA rule with 2 segment variables\n\njulia> r = @rule sin(~x + ~y) --> sin(~x)*cos(~y) + cos(~x)*sin(~y)\nsin(~x + ~y) --> sin(~x) * cos(~y) + cos(~x) * sin(~y)\n\njulia> r(:(sin(a + b)))\n:(cos(a)*sin(b) + sin(a)*cos(b))\n\nA rule that matches two of the same expressions:\n\njulia> r = @rule sin(~x)^2 + cos(~x)^2 --> 1\nsin(~x) ^ 2 + cos(~x) ^ 2 --> 1\n\njulia> r(:(sin(2a)^2 + cos(2a)^2))\n1\n\njulia> r(:(sin(2a)^2 + cos(a)^2))\n# nothing\n\nA rule without ~\n\njulia> r = @slots x y z @rule x(y + z) --> x*y + x*z\nx(y + z) --> x*y + x*z\n\nSegment: A Segment variable matches zero or more expressions in the function call. Segments may be written by splatting slot variables (~x...).\n\nExample:\n\njulia> r = @rule f(~xs...) --> g(~xs...);\njulia> r(:(f(1, 2, 3)))\n:(g(1,2,3))\n\nPredicates:\n\nThere 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.\n\nThe predicate should return true if the current match is acceptable, and false otherwise.\n\njulia> two_πs(x::Number) = abs(round(x/(2π)) - x/(2π)) < 10^-9\ntwo_πs (generic function with 1 method)\n\njulia> two_πs(x) = false\ntwo_πs (generic function with 2 methods)\n\njulia> r = @rule sin(~~x + ~y::two_πs + ~~z) => :(sin($(Expr(:call, :+, ~~x..., ~~z...))))\nsin(~(~x) + ~(y::two_πs) + ~(~z)) --> sin(+(~(~x)..., ~(~z)...))\n\njulia> r(:(sin(a+$(3π))))\n\njulia> r(:(sin(a+$(6π))))\n:(sin(+a))\n\njulia> r(sin(a+6π+c))\n:(sin(a + c))\n\nPredicate function gets an array of values if attached to a segment variable (~x...).\n\nFor the predicate over the whole rule, use @rule => where :\n\njulia> predicate(x) = x === a;\n\njulia> r = @rule ~x => ~x where f(~x);\n\njulia> r(a)\na\n\njulia> r(b) === nothing\ntrue\n\nNote that this is syntactic sugar and that it is the same as @rule ~x => f(~x) ? ~x : nothing.\n\nCompatibility: 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\n\n\n\n\n\n","category":"macro"},{"location":"api/#Metatheory.Syntax.@slots-Tuple","page":"API Documentation","title":"Metatheory.Syntax.@slots","text":"@slots [SLOTS...] ex\n\nDeclare SLOTS as slot variables for all @rule or @capture invocations in the expression ex. Example:\n\njulia> @slots x y z a b c Chain([\n (@rule x^2 + 2x*y + y^2 => (x + y)^2),\n (@rule x^a * y^b => (x*y)^a * y^(b-a)),\n (@rule +(x...) => sum(x)),\n])\n\nSee also: @rule, @capture\n\n\n\n\n\n","category":"macro"},{"location":"api/#Metatheory.Syntax.@theory-Tuple","page":"API Documentation","title":"Metatheory.Syntax.@theory","text":"@theory [SLOTS...] begin (LHS operator RHS)... end\n\nSyntax sugar to define a vector of rules in a nice and readable way. Can use @slots or have the slots as the first arguments:\n\njulia> t = @theory x y z begin \n x * (y + z) --> (x * y) + (x * z)\n x + y == (y + x)\n #...\nend;\n\nIs the same thing as writing\n\njulia> v = [\n @rule x y z x * (y + z) --> (x * y) + (x * z)\n @rule x y x + y == (y + x)\n #...\n];\n\n\n\n\n\n","category":"macro"},{"location":"api/","page":"API Documentation","title":"API Documentation","text":"","category":"page"},{"location":"api/#Patterns","page":"API Documentation","title":"Patterns","text":"","category":"section"},{"location":"api/","page":"API Documentation","title":"API Documentation","text":"Modules = [Metatheory.Patterns]","category":"page"},{"location":"api/#Metatheory.Patterns.AbstractPat","page":"API Documentation","title":"Metatheory.Patterns.AbstractPat","text":"Abstract type representing a pattern used in all the various pattern matching backends. \n\n\n\n\n\n","category":"type"},{"location":"api/#Metatheory.Patterns.PatSegment","page":"API Documentation","title":"Metatheory.Patterns.PatSegment","text":"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. \n\n\n\n\n\n","category":"type"},{"location":"api/#Metatheory.Patterns.PatTerm","page":"API Documentation","title":"Metatheory.Patterns.PatTerm","text":"Term patterns will match on terms of the same arity and with the same function symbol operation and expression head exprhead.\n\n\n\n\n\n","category":"type"},{"location":"api/#Metatheory.Patterns.PatVar","page":"API Documentation","title":"Metatheory.Patterns.PatVar","text":"PatVar{P}(name, debrujin_index, predicate::P)\n\nPattern variables will first match on one subterm and instantiate the substitution to that subterm.\n\nMatcher 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.\n\npredicate 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. \n\n\n\n\n\n","category":"type"},{"location":"api/#Metatheory.Patterns.isground-Tuple{AbstractPat}","page":"API Documentation","title":"Metatheory.Patterns.isground","text":"A ground pattern contains no pattern variables and only literal values to match.\n\n\n\n\n\n","category":"method"},{"location":"api/#Metatheory.Patterns.patvars-Tuple{PatVar, Any}","page":"API Documentation","title":"Metatheory.Patterns.patvars","text":"Collects pattern variables appearing in a pattern into a vector of symbols\n\n\n\n\n\n","category":"method"},{"location":"api/","page":"API Documentation","title":"API Documentation","text":"","category":"page"},{"location":"api/#Rules","page":"API Documentation","title":"Rules","text":"","category":"section"},{"location":"api/","page":"API Documentation","title":"API Documentation","text":"Modules = [Metatheory.Rules]","category":"page"},{"location":"api/#Metatheory.Rules.DynamicRule","page":"API Documentation","title":"Metatheory.Rules.DynamicRule","text":"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.\n\nDynamic rule\n\n@rule ~a::Number * ~b::Number => ~a*~b\n\n\n\n\n\n","category":"type"},{"location":"api/#Metatheory.Rules.EqualityRule","page":"API Documentation","title":"Metatheory.Rules.EqualityRule","text":"An EqualityRule can is a symbolic substitution rule that can be rewritten bidirectional. Therefore, it should only be used with the EGraphs backend.\n\n@rule ~a * ~b == ~b * ~a\n\n\n\n\n\n","category":"type"},{"location":"api/#Metatheory.Rules.RewriteRule","page":"API Documentation","title":"Metatheory.Rules.RewriteRule","text":"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.\n\n@rule ~a * ~b --> ~b * ~a\n\n\n\n\n\n","category":"type"},{"location":"api/#Metatheory.Rules.UnequalRule","page":"API Documentation","title":"Metatheory.Rules.UnequalRule","text":"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. \n\n!a ≠ a\n\n\n\n\n\n","category":"type"},{"location":"api/","page":"API Documentation","title":"API Documentation","text":"","category":"page"},{"location":"api/#Rules-2","page":"API Documentation","title":"Rules","text":"","category":"section"},{"location":"api/","page":"API Documentation","title":"API Documentation","text":"Modules = [Metatheory.Rules]","category":"page"},{"location":"api/","page":"API Documentation","title":"API Documentation","text":"","category":"page"},{"location":"api/#Rewriters","page":"API Documentation","title":"Rewriters","text":"","category":"section"},{"location":"api/","page":"API Documentation","title":"API Documentation","text":"Modules = [Metatheory.Rewriters]","category":"page"},{"location":"api/#Metatheory.Rewriters","page":"API Documentation","title":"Metatheory.Rewriters","text":"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.\n\nThe Rewriters module contains some types which create and transform rewriters.\n\nEmpty() is a rewriter which always returns nothing\nChain(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.\nRestartedChain(itr) like Chain(itr) but restarts from the first rewriter once on the first successful application of one of the chained rewriters.\nIfElse(cond, rw1, rw2) runs the cond function on the input, applies rw1 if cond returns true, rw2 if it retuns false\nIf(cond, rw) is the same as IfElse(cond, rw, Empty())\nPrewalk(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.\nPostwalk(rw; threaded=false, thread_cutoff=100) similarly does post-order traversal.\nFixpoint(rw) returns a rewriter which applies rw repeatedly until there are no changes to be made.\nFixpointNoCycle behaves like Fixpoint but instead it applies rw repeatedly only while it is returning new results.\nPassThrough(rw) returns a rewriter which if rw(x) returns nothing will instead return x otherwise will return rw(x).\n\n\n\nImports\n\nBase\nBase.Threads\nCore\nTermInterface\n\n\n\n\n\n","category":"module"},{"location":"api/#Metatheory.Rewriters.FixpointNoCycle","page":"API Documentation","title":"Metatheory.Rewriters.FixpointNoCycle","text":"FixpointNoCycle(rw)\n\nFixpointNoCycle 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. \n\n\n\n\n\n","category":"type"},{"location":"api/","page":"API Documentation","title":"API Documentation","text":"","category":"page"},{"location":"api/#EGraphs","page":"API Documentation","title":"EGraphs","text":"","category":"section"},{"location":"api/","page":"API Documentation","title":"API Documentation","text":"Modules = [Metatheory.EGraphs]","category":"page"},{"location":"api/#Metatheory.EGraphs.EGraph","page":"API Documentation","title":"Metatheory.EGraphs.EGraph","text":"mutable struct EGraph\n\nA concrete type representing an [EGraph]. See the egg paper for implementation details.\n\n\n\nFields\n\nuf::IntDisjointSet\nstores the equality relations over e-class ids\nclasses::Dict{Int64, EClass}\nmap from eclass id to eclasses\nmemo::Dict{AbstractENode, Int64}\nhashcons\ndirty::Vector{Int64}\nworklist for ammortized upwards merging\nroot::Int64\nanalyses::Dict{Union{Function, Symbol}, Union{Function, Symbol}}\nA vector of analyses associated to the EGraph\nsymcache::Dict{Any, Vector{Int64}}\na cache mapping function symbols to e-classes that contain e-nodes with that function symbol.\ndefault_termtype::Type\ntermtypes::Dict{Tuple{Any, Int64}, Type}\nnumclasses::Int64\nnumnodes::Int64\nneedslock::Bool\nIf we use global buffers we may need to lock. Defaults to true.\nbuffer::Vector{Base.ImmutableDict{Int64, Tuple{Int64, Int64}}}\nBuffer for e-matching which defaults to a global. Use a local buffer for generated functions.\nmerges_buffer::Vector{Tuple{Int64, Int64}}\nBuffer for rule application which defaults to a global. Use a local buffer for generated functions.\nlock::ReentrantLock\n\n\n\n\n\n","category":"type"},{"location":"api/#Metatheory.EGraphs.EGraph-Tuple{}","page":"API Documentation","title":"Metatheory.EGraphs.EGraph","text":"EGraph(expr)\n\nConstruct an EGraph from a starting symbolic expression expr.\n\n\n\nSignatures\n\nEGraph() -> EGraph\n\n\n\n\nMethods\n\nEGraph()\n\ndefined at /home/runner/work/Metatheory.jl/Metatheory.jl/src/EGraphs/egraph.jl:212.\n\n\n\n\n\n","category":"method"},{"location":"api/#Metatheory.EGraphs.EqualityGoal","page":"API Documentation","title":"Metatheory.EGraphs.EqualityGoal","text":"struct EqualityGoal <: SaturationGoal\n\nThis goal is reached when the exprs list of expressions are in the same equivalence class.\n\n\n\nFields\n\nexprs::Vector{Any}\nids::Vector{Int64}\n\n\n\n\n\n","category":"type"},{"location":"api/#Metatheory.EGraphs.FunctionGoal","page":"API Documentation","title":"Metatheory.EGraphs.FunctionGoal","text":"struct FunctionGoal <: SaturationGoal\n\nBoolean valued function as an arbitrary saturation goal. User supplied function must take an EGraph as the only parameter.\n\n\n\nFields\n\nfun::Function\n\n\n\n\n\n","category":"type"},{"location":"api/#Metatheory.EGraphs.SaturationParams","page":"API Documentation","title":"Metatheory.EGraphs.SaturationParams","text":"mutable struct SaturationParams\n\nConfigurable Parameters for the equality saturation process.\n\n\n\nFields\n\ntimeout::Int64\ntimelimit::UInt64\nTimeout in nanoseconds\neclasslimit::Int64\nMaximum number of eclasses allowed\nenodelimit::Int64\ngoal::Union{Nothing, SaturationGoal}\nstopwhen::Function\nscheduler::Type{<:Metatheory.EGraphs.Schedulers.AbstractScheduler}\nschedulerparams::Tuple\nthreaded::Bool\ntimer::Bool\n\n\n\n\n\n","category":"type"},{"location":"api/#Base.merge!-Tuple{EGraph, Int64, Int64}","page":"API Documentation","title":"Base.merge!","text":"Given an EGraph and two e-class ids, set the two e-classes as equal.\n\n\n\nSignatures\n\nmerge!(g::EGraph, a::Int64, b::Int64) -> Int64\n\n\n\n\nMethods\n\nmerge!(g, a, b)\n\ndefined at /home/runner/work/Metatheory.jl/Metatheory.jl/src/EGraphs/egraph.jl:391.\n\n\n\n\n\n","category":"method"},{"location":"api/#Metatheory.EGraphs.add!-Tuple{EGraph, AbstractENode}","page":"API Documentation","title":"Metatheory.EGraphs.add!","text":"Inserts an e-node in an EGraph\n\n\n\nSignatures\n\nadd!(g::EGraph, n::AbstractENode) -> Int64\n\n\n\n\nMethods\n\nadd!(g, n)\n\ndefined at /home/runner/work/Metatheory.jl/Metatheory.jl/src/EGraphs/egraph.jl:315.\n\n\n\n\n\n","category":"method"},{"location":"api/#Metatheory.EGraphs.addexpr!-Tuple{EGraph, Any}","page":"API Documentation","title":"Metatheory.EGraphs.addexpr!","text":"Recursively traverse an type satisfying the TermInterface and insert terms into an EGraph. If e has no children (has an arity of 0) then directly insert the literal into the EGraph.\n\n\n\nSignatures\n\naddexpr!(g::EGraph, se) -> Int64\n\n\n\n\nMethods\n\naddexpr!(g, se)\n\ndefined at /home/runner/work/Metatheory.jl/Metatheory.jl/src/EGraphs/egraph.jl:365.\n\naddexpr!(g, ec)\n\ndefined at /home/runner/work/Metatheory.jl/Metatheory.jl/src/EGraphs/egraph.jl:382.\n\n\n\n\n\n","category":"method"},{"location":"api/#Metatheory.EGraphs.analyze!-Tuple{EGraph, Any, Vector{Int64}}","page":"API Documentation","title":"Metatheory.EGraphs.analyze!","text":"analyze!(egraph, analysis_name, [ECLASS_IDS])\n\nGiven 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.\n\n\n\nSignatures\n\nanalyze!(g::EGraph, analysis_ref, ids::Vector{Int64}) -> Bool\n\n\n\n\nMethods\n\nanalyze!(g, analysis_ref, ids)\n\ndefined at /home/runner/work/Metatheory.jl/Metatheory.jl/src/EGraphs/analysis.jl:61.\n\n\n\n\n\n","category":"method"},{"location":"api/#Metatheory.EGraphs.astsize-Tuple{ENodeTerm, EGraph}","page":"API Documentation","title":"Metatheory.EGraphs.astsize","text":"A basic cost function, where the computed cost is the size (number of children) of the current expression.\n\n\n\nSignatures\n\nastsize(n::ENodeTerm, g::EGraph) -> Any\n\n\n\n\nMethods\n\nastsize(n, g)\n\ndefined at /home/runner/work/Metatheory.jl/Metatheory.jl/src/EGraphs/analysis.jl:98.\n\n\n\n\n\n","category":"method"},{"location":"api/#Metatheory.EGraphs.astsize_inv-Tuple{ENodeTerm, EGraph}","page":"API Documentation","title":"Metatheory.EGraphs.astsize_inv","text":"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\n\n\n\nSignatures\n\nastsize_inv(n::ENodeTerm, g::EGraph) -> Any\n\n\n\n\nMethods\n\nastsize_inv(n, g)\n\ndefined at /home/runner/work/Metatheory.jl/Metatheory.jl/src/EGraphs/analysis.jl:115.\n\n\n\n\n\n","category":"method"},{"location":"api/#Metatheory.EGraphs.egraph_reconstruct_expression-Tuple{Type{Expr}, Any, Any}","page":"API Documentation","title":"Metatheory.EGraphs.egraph_reconstruct_expression","text":"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.\n\n\n\nSignatures\n\negraph_reconstruct_expression(T::Type{Expr}, op, args) -> Expr\n\n\n\n\nMethods\n\negraph_reconstruct_expression(T, op, args)\n\ndefined at /home/runner/work/Metatheory.jl/Metatheory.jl/src/EGraphs/egraph.jl:534.\n\n\n\n\n\n","category":"method"},{"location":"api/#Metatheory.EGraphs.eqsat_search!-Tuple{EGraph, Vector{<:AbstractRule}, Metatheory.EGraphs.Schedulers.AbstractScheduler, Metatheory.EGraphs.SaturationReport}","page":"API Documentation","title":"Metatheory.EGraphs.eqsat_search!","text":"Returns an iterator of Matches.\n\n\n\nSignatures\n\neqsat_search!(g::EGraph, theory::Vector{<:AbstractRule}, scheduler::Metatheory.EGraphs.Schedulers.AbstractScheduler, report::Metatheory.EGraphs.SaturationReport) -> Int64\n\n\n\n\nMethods\n\neqsat_search!(g, theory, scheduler, report)\n\ndefined at /home/runner/work/Metatheory.jl/Metatheory.jl/src/EGraphs/saturation.jl:114.\n\n\n\n\n\n","category":"method"},{"location":"api/#Metatheory.EGraphs.eqsat_step!-Tuple{EGraph, Vector{<:AbstractRule}, Any, Metatheory.EGraphs.Schedulers.AbstractScheduler, SaturationParams, Any}","page":"API Documentation","title":"Metatheory.EGraphs.eqsat_step!","text":"Core algorithm of the library: the equality saturation step.\n\n\n\nSignatures\n\neqsat_step!(g::EGraph, theory::Vector{<:AbstractRule}, curr_iter, scheduler::Metatheory.EGraphs.Schedulers.AbstractScheduler, params::SaturationParams, report) -> Any\n\n\n\n\nMethods\n\neqsat_step!(g, theory, curr_iter, scheduler, params, report)\n\ndefined at /home/runner/work/Metatheory.jl/Metatheory.jl/src/EGraphs/saturation.jl:257.\n\n\n\n\n\n","category":"method"},{"location":"api/#Metatheory.EGraphs.extract!-Tuple{EGraph, Function}","page":"API Documentation","title":"Metatheory.EGraphs.extract!","text":"Given a cost function, extract the expression with the smallest computed cost from an EGraph\n\n\n\nSignatures\n\nextract!(g::EGraph, costfun::Function) -> Any\n\n\n\n\nMethods\n\nextract!(g, costfun)\n\ndefined at /home/runner/work/Metatheory.jl/Metatheory.jl/src/EGraphs/analysis.jl:163.\n\n\n\n\n\n","category":"method"},{"location":"api/#Metatheory.EGraphs.find-Tuple{EGraph, Int64}","page":"API Documentation","title":"Metatheory.EGraphs.find","text":"Returns the canonical e-class id for a given e-class.\n\n\n\nSignatures\n\nfind(g::EGraph, a::Int64) -> Int64\n\n\n\n\nMethods\n\nfind(g, a)\n\ndefined at /home/runner/work/Metatheory.jl/Metatheory.jl/src/EGraphs/egraph.jl:272.\n\n\n\n\n\n","category":"method"},{"location":"api/#Metatheory.EGraphs.instantiate_actual_param!-Tuple{Base.ImmutableDict{Int64, Tuple{Int64, Int64}}, EGraph, Any}","page":"API Documentation","title":"Metatheory.EGraphs.instantiate_actual_param!","text":"Instantiate argument for dynamic rule application in e-graph\n\n\n\nSignatures\n\ninstantiate_actual_param!(bindings::Base.ImmutableDict{Int64, Tuple{Int64, Int64}}, g::EGraph, i) -> Any\n\n\n\n\nMethods\n\ninstantiate_actual_param!(bindings, g, i)\n\ndefined at /home/runner/work/Metatheory.jl/Metatheory.jl/src/EGraphs/saturation.jl:194.\n\n\n\n\n\n","category":"method"},{"location":"api/#Metatheory.EGraphs.islazy-Union{Tuple{Val{analysis_name}}, Tuple{analysis_name}} where analysis_name","page":"API Documentation","title":"Metatheory.EGraphs.islazy","text":"islazy(::Val{analysis_name})\n\nShould 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. \n\n\n\nSignatures\n\n\n\nMethods\n\nislazy(_)\n\ndefined at /home/runner/work/Metatheory.jl/Metatheory.jl/src/EGraphs/analysis.jl:14.\n\nislazy(analysis_name)\n\ndefined at /home/runner/work/Metatheory.jl/Metatheory.jl/src/EGraphs/analysis.jl:15.\n\nislazy(_)\n\ndefined at /home/runner/work/Metatheory.jl/Metatheory.jl/src/EGraphs/analysis.jl:135.\n\n\n\n\n\n","category":"method"},{"location":"api/#Metatheory.EGraphs.join-Union{Tuple{analysis_name}, Tuple{Val{analysis_name}, Any, Any}} where analysis_name","page":"API Documentation","title":"Metatheory.EGraphs.join","text":"join(::Val{analysis_name}, a, b)\n\nJoins two analyses values into a single one, used by analyze! when two eclasses are being merged or the analysis is being constructed.\n\n\n\nSignatures\n\n\n\nMethods\n\njoin(analysis, a, b)\n\ndefined at /home/runner/work/Metatheory.jl/Metatheory.jl/src/EGraphs/analysis.jl:35.\n\n\n\n\n\n","category":"method"},{"location":"api/#Metatheory.EGraphs.make-Tuple{Function, EGraph, AbstractENode}","page":"API Documentation","title":"Metatheory.EGraphs.make","text":"When passing a function to analysis functions it is considered as a cost function\n\n\n\nSignatures\n\nmake(f::Function, g::EGraph, n::AbstractENode) -> Tuple{AbstractENode, Any}\n\n\n\n\nMethods\n\nmake(f, g, n)\n\ndefined at /home/runner/work/Metatheory.jl/Metatheory.jl/src/EGraphs/analysis.jl:131.\n\n\n\n\n\n","category":"method"},{"location":"api/#Metatheory.EGraphs.make-Union{Tuple{analysis_name}, Tuple{Val{analysis_name}, Any, Any}} where analysis_name","page":"API Documentation","title":"Metatheory.EGraphs.make","text":"make(::Val{analysis_name}, g, n)\n\nGiven an ENode n, make should return the corresponding analysis value. \n\n\n\nSignatures\n\nmake(_::Val{analysis_name}, g, n)\n\n\n\n\nMethods\n\nmake(_, g, n)\n\ndefined at /home/runner/work/Metatheory.jl/Metatheory.jl/src/EGraphs/analysis.jl:44.\n\n\n\n\n\n","category":"method"},{"location":"api/#Metatheory.EGraphs.modify!-Union{Tuple{analysis_name}, Tuple{Val{analysis_name}, Any, Any}} where analysis_name","page":"API Documentation","title":"Metatheory.EGraphs.modify!","text":"modify!(::Val{analysis_name}, g, id)\n\nThe modify! function for EGraph Analysis can optionally modify the eclass g[id] after it has been analyzed, typically by adding an ENode. It should be idempotent if no other changes occur to the EClass. (See the egg paper).\n\n\n\nSignatures\n\n\n\nMethods\n\nmodify!(_, g, id)\n\ndefined at /home/runner/work/Metatheory.jl/Metatheory.jl/src/EGraphs/analysis.jl:25.\n\n\n\n\n\n","category":"method"},{"location":"api/#Metatheory.EGraphs.preprocess-Tuple{Expr}","page":"API Documentation","title":"Metatheory.EGraphs.preprocess","text":"Extend this function on your types to do preliminary preprocessing of a symbolic term before adding it to an EGraph. Most common preprocessing techniques are binarization of n-ary terms and metadata stripping.\n\n\n\nSignatures\n\npreprocess(e::Expr) -> Any\n\n\n\n\nMethods\n\npreprocess(e)\n\ndefined at /home/runner/work/Metatheory.jl/Metatheory.jl/src/EGraphs/egraph.jl:355.\n\n\n\n\n\n","category":"method"},{"location":"api/#Metatheory.EGraphs.reachable-Tuple{EGraph, Int64}","page":"API Documentation","title":"Metatheory.EGraphs.reachable","text":"Recursive function that traverses an EGraph and returns a vector of all reachable e-classes from a given e-class id.\n\n\n\nSignatures\n\nreachable(g::EGraph, id::Int64) -> Vector{Int64}\n\n\n\n\nMethods\n\nreachable(g, id)\n\ndefined at /home/runner/work/Metatheory.jl/Metatheory.jl/src/EGraphs/egraph.jl:501.\n\n\n\n\n\n","category":"method"},{"location":"api/#Metatheory.EGraphs.rebuild!-Tuple{EGraph}","page":"API Documentation","title":"Metatheory.EGraphs.rebuild!","text":"This function restores invariants and executes upwards merging in an EGraph. See the egg paper for more details.\n\n\n\nSignatures\n\nrebuild!(g::EGraph) -> Bool\n\n\n\n\nMethods\n\nrebuild!(g)\n\ndefined at /home/runner/work/Metatheory.jl/Metatheory.jl/src/EGraphs/egraph.jl:426.\n\n\n\n\n\n","category":"method"},{"location":"api/#Metatheory.EGraphs.saturate!","page":"API Documentation","title":"Metatheory.EGraphs.saturate!","text":"Given an EGraph and a collection of rewrite rules, execute the equality saturation algorithm.\n\n\n\nSignatures\n\nsaturate!(g::EGraph, theory::Vector{<:AbstractRule}) -> Metatheory.EGraphs.SaturationReport\nsaturate!(g::EGraph, theory::Vector{<:AbstractRule}, params) -> Metatheory.EGraphs.SaturationReport\n\n\n\n\nMethods\n\nsaturate!(g, theory)\nsaturate!(g, theory, params)\n\ndefined at /home/runner/work/Metatheory.jl/Metatheory.jl/src/EGraphs/saturation.jl:286.\n\n\n\n\n\n","category":"function"},{"location":"api/","page":"API Documentation","title":"API Documentation","text":"","category":"page"},{"location":"api/#EGraph-Schedulers","page":"API Documentation","title":"EGraph Schedulers","text":"","category":"section"},{"location":"api/","page":"API Documentation","title":"API Documentation","text":"Modules = [Metatheory.EGraphs.Schedulers]","category":"page"},{"location":"api/#Metatheory.EGraphs.Schedulers.AbstractScheduler","page":"API Documentation","title":"Metatheory.EGraphs.Schedulers.AbstractScheduler","text":"abstract type AbstractScheduler\n\nRepresents a rule scheduler for the equality saturation process\n\n\n\nFields\n\n\n\n\n\n","category":"type"},{"location":"api/#Metatheory.EGraphs.Schedulers.BackoffScheduler","page":"API Documentation","title":"Metatheory.EGraphs.Schedulers.BackoffScheduler","text":"mutable struct BackoffScheduler <: Metatheory.EGraphs.Schedulers.AbstractScheduler\n\nA 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.\n\nThis seems effective at preventing explosive rules like associativity from taking an unfair amount of resources.\n\n\n\nFields\n\ndata::IdDict{AbstractRule, Metatheory.EGraphs.Schedulers.BackoffSchedulerEntry}\nG::EGraph\ntheory::Vector{<:AbstractRule}\ncurr_iter::Int64\n\n\n\n\n\n","category":"type"},{"location":"api/#Metatheory.EGraphs.Schedulers.ScoredScheduler","page":"API Documentation","title":"Metatheory.EGraphs.Schedulers.ScoredScheduler","text":"mutable struct ScoredScheduler <: Metatheory.EGraphs.Schedulers.AbstractScheduler\n\nA 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.\n\nThis seems effective at preventing explosive rules like associativity from taking an unfair amount of resources.\n\n\n\nFields\n\ndata::IdDict{AbstractRule, Metatheory.EGraphs.Schedulers.ScoredSchedulerEntry}\nG::EGraph\ntheory::Vector{<:AbstractRule}\ncurr_iter::Int64\n\n\n\n\n\n","category":"type"},{"location":"api/#Metatheory.EGraphs.Schedulers.SimpleScheduler","page":"API Documentation","title":"Metatheory.EGraphs.Schedulers.SimpleScheduler","text":"struct SimpleScheduler <: Metatheory.EGraphs.Schedulers.AbstractScheduler\n\nA simple Rewrite Scheduler that applies every rule every time\n\n\n\nFields\n\n\n\n\n\n","category":"type"},{"location":"api/#Metatheory.EGraphs.Schedulers.cansaturate","page":"API Documentation","title":"Metatheory.EGraphs.Schedulers.cansaturate","text":"Should return true if the e-graph can be said to be saturated\n\ncansaturate(s::AbstractScheduler)\n\n\n\nSignatures\n\n\n\nMethods\n\ncansaturate(s)\n\ndefined at /home/runner/work/Metatheory.jl/Metatheory.jl/src/EGraphs/Schedulers.jl:63.\n\ncansaturate(s)\n\ndefined at /home/runner/work/Metatheory.jl/Metatheory.jl/src/EGraphs/Schedulers.jl:120.\n\ncansaturate(s)\n\ndefined at /home/runner/work/Metatheory.jl/Metatheory.jl/src/EGraphs/Schedulers.jl:231.\n\n\n\n\n\n","category":"function"},{"location":"api/#Metatheory.EGraphs.Schedulers.cansearch","page":"API Documentation","title":"Metatheory.EGraphs.Schedulers.cansearch","text":"Should return false if the rule r should be skipped\n\ncansearch(s::AbstractScheduler, r::Rule)\n\n\n\nSignatures\n\n\n\nMethods\n\ncansearch(s, r)\n\ndefined at /home/runner/work/Metatheory.jl/Metatheory.jl/src/EGraphs/Schedulers.jl:64.\n\ncansearch(s, r)\n\ndefined at /home/runner/work/Metatheory.jl/Metatheory.jl/src/EGraphs/Schedulers.jl:100.\n\ncansearch(s, r)\n\ndefined at /home/runner/work/Metatheory.jl/Metatheory.jl/src/EGraphs/Schedulers.jl:169.\n\n\n\n\n\n","category":"function"},{"location":"api/#Metatheory.EGraphs.Schedulers.inform!","page":"API Documentation","title":"Metatheory.EGraphs.Schedulers.inform!","text":"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. \n\ninform!(s::AbstractScheduler, r::AbstractRule, n_matches)\n\n\n\nSignatures\n\n\n\nMethods\n\ninform!(s, r, n_matches)\n\ndefined at /home/runner/work/Metatheory.jl/Metatheory.jl/src/EGraphs/Schedulers.jl:68.\n\ninform!(s, rule, n_matches)\n\ndefined at /home/runner/work/Metatheory.jl/Metatheory.jl/src/EGraphs/Schedulers.jl:123.\n\ninform!(s, rule, n_matches)\n\ndefined at /home/runner/work/Metatheory.jl/Metatheory.jl/src/EGraphs/Schedulers.jl:234.\n\n\n\n\n\n","category":"function"},{"location":"rewrite/#Classical-Term-Rewriting","page":"Classical Term Rewriting","title":"Classical Term Rewriting","text":"","category":"section"},{"location":"rewrite/#Rule-based-rewriting","page":"Classical Term Rewriting","title":"Rule-based rewriting","text":"","category":"section"},{"location":"rewrite/","page":"Classical Term Rewriting","title":"Classical Term Rewriting","text":"Rewrite rules match and transform an expression. A rule is written using either the @rule or @theory macros. It creates a callable Rule object.","category":"page"},{"location":"rewrite/#Basics-of-rule-based-term-rewriting-in-Metatheory.jl","page":"Classical Term Rewriting","title":"Basics of rule-based term rewriting in Metatheory.jl","text":"","category":"section"},{"location":"rewrite/","page":"Classical Term Rewriting","title":"Classical Term Rewriting","text":"NOTE: for a real world use case using mathematical constructs, please refer to SymbolicUtils.jl. SU provides optimized types for mathematical expressions, code generation and a polished set of rules for simplification.","category":"page"},{"location":"rewrite/","page":"Classical Term Rewriting","title":"Classical Term Rewriting","text":"Here is a simple symbolic rewrite rule, that uses formula for the double angle of the sine function:","category":"page"},{"location":"rewrite/","page":"Classical Term Rewriting","title":"Classical Term Rewriting","text":"using Metatheory\n\nr1 = @rule sin(2(~x)) --> 2sin(~x)*cos(~x)\n\nexpr = :(sin(2z))\nr1(expr)","category":"page"},{"location":"rewrite/","page":"Classical Term Rewriting","title":"Classical Term Rewriting","text":"The @rule macro takes a pair of patterns – the matcher and the consequent (@rule matcher OPERATOR consequent). If an expression matches the matcher pattern, it is rewritten to the consequent pattern. @rule returns a callable object that applies the rule to an expression. There are different kinds of rule in Metatheory.jl:","category":"page"},{"location":"rewrite/","page":"Classical Term Rewriting","title":"Classical Term Rewriting","text":"Rule operators:","category":"page"},{"location":"rewrite/","page":"Classical Term Rewriting","title":"Classical Term Rewriting","text":"LHS => RHS: create a DynamicRule. The RHS is evaluated on rewrite.\nLHS --> RHS: create a RewriteRule. The RHS is not evaluated but symbolically substituted on rewrite.\nLHS == 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.\nLHS ≠ 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.","category":"page"},{"location":"rewrite/","page":"Classical Term Rewriting","title":"Classical Term Rewriting","text":"You can use dynamic rules, defined with the => operator, to dynamically compute values in the right hand of expressions. This is the default behaviour of rules in SymbolicUtils.jl 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.","category":"page"},{"location":"rewrite/","page":"Classical Term Rewriting","title":"Classical Term Rewriting","text":"~x in the example is what is a slot variable (or pattern variable) named x. In a matcher pattern, slot variables are placeholders that match exactly one expression. When used on the consequent side, they stand in for the matched expression. If a slot variable appears twice in a matcher pattern, in classical rewriting all corresponding matches must be equal (as tested by Base.isequal function). Hence this rule says: if you see something added to itself, make it twice of that thing, and works as such.","category":"page"},{"location":"rewrite/","page":"Classical Term Rewriting","title":"Classical Term Rewriting","text":"If you try to apply this rule to an expression with triple angle, it will return nothing – this is the way a rule signifies failure to match.","category":"page"},{"location":"rewrite/","page":"Classical Term Rewriting","title":"Classical Term Rewriting","text":"r1(:(sin(3z))) === nothing","category":"page"},{"location":"rewrite/","page":"Classical Term Rewriting","title":"Classical Term Rewriting","text":"Slot variable (matcher) is not necessary a single variable","category":"page"},{"location":"rewrite/","page":"Classical Term Rewriting","title":"Classical Term Rewriting","text":"r1(:(sin(2*(w-z))))","category":"page"},{"location":"rewrite/","page":"Classical Term Rewriting","title":"Classical Term Rewriting","text":"but it must be a single expression","category":"page"},{"location":"rewrite/","page":"Classical Term Rewriting","title":"Classical Term Rewriting","text":"r1(:(sin(2*(w+z)*(α+β)))) === nothing","category":"page"},{"location":"rewrite/","page":"Classical Term Rewriting","title":"Classical Term Rewriting","text":"Rules are of course not limited to single slot variable","category":"page"},{"location":"rewrite/","page":"Classical Term Rewriting","title":"Classical Term Rewriting","text":"r2 = @rule sin(~x + ~y) --> sin(~x)*cos(~y) + cos(~x)*sin(~y);\n\nr2(:(sin(α+β)))","category":"page"},{"location":"rewrite/","page":"Classical Term Rewriting","title":"Classical Term Rewriting","text":"If you want to match a variable number of subexpressions at once, you will need a segment variable. ~xs... in the following example is a segment variable:","category":"page"},{"location":"rewrite/","page":"Classical Term Rewriting","title":"Classical Term Rewriting","text":"@rule(+(~xs...) => xs)(:(x + y + z))","category":"page"},{"location":"rewrite/","page":"Classical Term Rewriting","title":"Classical Term Rewriting","text":"~xs is a vector of subexpressions matched. You can use it to construct something more useful:","category":"page"},{"location":"rewrite/","page":"Classical Term Rewriting","title":"Classical Term Rewriting","text":"r3 = @rule *(~ys...)^~x => :((*)($(map(y-> :($y^$x), ys)...)));\n\nr3(:((w*w*α*β)^2))","category":"page"},{"location":"rewrite/#Predicates-for-matching","page":"Classical Term Rewriting","title":"Predicates for matching","text":"","category":"section"},{"location":"rewrite/","page":"Classical Term Rewriting","title":"Classical Term Rewriting","text":"Matcher pattern may contain slot variables with attached predicates, written as ~x::p where p is either","category":"page"},{"location":"rewrite/","page":"Classical Term Rewriting","title":"Classical Term Rewriting","text":"A function that takes a matched expression and returns a boolean value. Such a slot will be considered a match only if p returns true.\nA Julia type. Will be considered a match if and only if the value matching against x has a type that is a subtype of p (typeof(x) <: p)","category":"page"},{"location":"rewrite/","page":"Classical Term Rewriting","title":"Classical Term Rewriting","text":"Similarly ~x::g... is a way of attaching 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. If the same slot or segment variable appears twice in the matcher pattern, then at most one of the occurrence should have a predicate.","category":"page"},{"location":"rewrite/","page":"Classical Term Rewriting","title":"Classical Term Rewriting","text":"For example,","category":"page"},{"location":"rewrite/","page":"Classical Term Rewriting","title":"Classical Term Rewriting","text":"r = @rule +(~x, ~y::(ys->iseven(length(ys)))...) => \"odd terms\";\n\n@show r(:(a + b + c + d))\n@show r(:(b + c + d))\n@show r(:(b + c + b))\n@show r(:(a + b))","category":"page"},{"location":"rewrite/#Declaring-Slots","page":"Classical Term Rewriting","title":"Declaring Slots","text":"","category":"section"},{"location":"rewrite/","page":"Classical Term Rewriting","title":"Classical Term Rewriting","text":"Slot variables can be declared without the ~ using the @slots macro","category":"page"},{"location":"rewrite/","page":"Classical Term Rewriting","title":"Classical Term Rewriting","text":"@slots x y @rule sin(x + y) => sin(x)*cos(y) + cos(x)*sin(y);","category":"page"},{"location":"rewrite/","page":"Classical Term Rewriting","title":"Classical Term Rewriting","text":"This works for segments as well:","category":"page"},{"location":"rewrite/","page":"Classical Term Rewriting","title":"Classical Term Rewriting","text":"@slots xs @rule(+(~xs...) => xs);","category":"page"},{"location":"rewrite/","page":"Classical Term Rewriting","title":"Classical Term Rewriting","text":"The @slots macro is superfluous for the @rule, @capture and @theory macros. Slot variables may be declared directly as the first arguments to those macros:","category":"page"},{"location":"rewrite/","page":"Classical Term Rewriting","title":"Classical Term Rewriting","text":"@rule x y sin(x + y) => sin(x)*cos(y) + cos(x)*sin(y);","category":"page"},{"location":"rewrite/#Theories","page":"Classical Term Rewriting","title":"Theories","text":"","category":"section"},{"location":"rewrite/","page":"Classical Term Rewriting","title":"Classical Term Rewriting","text":"In almost all use cases, it is practical to define many rules grouped together. A set of rewrite rules and equalities is called a theory, and can be defined with the @theory macro. This macro is just syntax sugar to define vectors of rules in a nice and readable way. ","category":"page"},{"location":"rewrite/","page":"Classical Term Rewriting","title":"Classical Term Rewriting","text":"t = @theory x y z begin \n x * (y + z) --> (x * y) + (x * z)\n x + y == (y + x)\n #...\nend;","category":"page"},{"location":"rewrite/","page":"Classical Term Rewriting","title":"Classical Term Rewriting","text":"Is the same thing as writing","category":"page"},{"location":"rewrite/","page":"Classical Term Rewriting","title":"Classical Term Rewriting","text":"v = [\n @rule x y z x * (y + z) --> (x * y) + (x * z)\n @rule x y x + y == (y + x)\n #...\n];","category":"page"},{"location":"rewrite/","page":"Classical Term Rewriting","title":"Classical Term Rewriting","text":"Theories are just collections 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.","category":"page"},{"location":"rewrite/","page":"Classical Term Rewriting","title":"Classical Term Rewriting","text":"using Metatheory\nusing Metatheory.Library\n\ncomm_monoid = @commutative_monoid (*) 1\ncomm_group = @theory a b c begin\n a + 0 --> a\n a + b --> b + a\n a + inv(a) --> 0 # inverse\n a + (b + c) --> (a + b) + c\nend\ndistrib = @theory a b c begin\n a * (b + c) => (a * b) + (a * c)\nend\nt = comm_monoid ∪ comm_group ∪ distrib","category":"page"},{"location":"rewrite/#Composing-rewriters","page":"Classical Term Rewriting","title":"Composing rewriters","text":"","category":"section"},{"location":"rewrite/","page":"Classical Term Rewriting","title":"Classical Term Rewriting","text":"Rules may be chained together into more sophisticated rewriters to avoid manual application of the rules. A rewriter is any callable object 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 Rules we created above are rewriters.","category":"page"},{"location":"rewrite/","page":"Classical Term Rewriting","title":"Classical Term Rewriting","text":"The Metatheory.Rewriters module contains some types which create and transform rewriters.","category":"page"},{"location":"rewrite/","page":"Classical Term Rewriting","title":"Classical Term Rewriting","text":"Empty() is a rewriter which always returns nothing\nChain(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.\nRestartedChain(itr) like Chain(itr) but restarts from the first rewriter once on the first successful application of one of the chained rewriters.\nIfElse(cond, rw1, rw2) runs the cond function on the input, applies rw1 if cond returns true, rw2 if it returns false\nIf(cond, rw) is the same as IfElse(cond, rw, Empty())\nPrewalk(rw; threaded=false, thread_cutoff=100) returns a rewriter which does a pre-order (from top to bottom and from left to right) traversal of a given expression and applies the rewriter rw. threaded=true will use multi threading for traversal. 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. If you are applying multiple rules, then Chain already has the appropriate passthrough behavior. If you only want to apply one rule, then consider using PassThrough. thread_cutoff is the minimum number of nodes in a subtree which should be walked in a threaded spawn.\nPostwalk(rw; threaded=false, thread_cutoff=100) similarly does post-order (from left to right and from bottom to top) traversal.\nFixpoint(rw) returns a rewriter which applies rw repeatedly until there are no changes to be made.\nFixpointNoCycle behaves like Fixpoint but instead it applies rw repeatedly only while it is returning new results.\nPassThrough(rw) returns a rewriter which if rw(x) returns nothing will instead return x otherwise will return rw(x).","category":"page"},{"location":"rewrite/#Chaining-rewriters","page":"Classical Term Rewriting","title":"Chaining rewriters","text":"","category":"section"},{"location":"rewrite/","page":"Classical Term Rewriting","title":"Classical Term Rewriting","text":"Several rules may be chained to give chain of rules. Chain is an array of rules which are subsequently applied to the expression. Important feature of Chain is that it returns the expression instead of nothing if it doesn't change the expression It is important to notice, that chain is ordered, so if rules are in different order it wouldn't work the same as in earlier example","category":"page"},{"location":"rewrite/","page":"Classical Term Rewriting","title":"Classical Term Rewriting","text":"One way to circumvent the problem of order of applying rules in chain is to use RestartedChain, it restarts the chain after each successful application of a rule, so after a rule is hit it (re)starts again and it can apply all the other rules to the resulting expression. You can also use Fixpoint to apply the rules until there are no changes.","category":"page"},{"location":"tutorials/fibonacci/","page":"Benchmarking Fibonacci. E-Graphs memoize computation.","title":"Benchmarking Fibonacci. E-Graphs memoize computation.","text":"EditURL = \"https://github.com/JuliaSymbolics/Metatheory.jl/blob/master/test/tutorials/fibonacci.jl\"","category":"page"},{"location":"tutorials/fibonacci/#Benchmarking-Fibonacci.-E-Graphs-memoize-computation.","page":"Benchmarking Fibonacci. E-Graphs memoize computation.","title":"Benchmarking Fibonacci. E-Graphs memoize computation.","text":"","category":"section"},{"location":"tutorials/fibonacci/","page":"Benchmarking Fibonacci. E-Graphs memoize computation.","title":"Benchmarking Fibonacci. E-Graphs memoize computation.","text":"using Metatheory\nusing Test\n\nfunction fib end\n\nfibo = @theory x y n begin\n x::Int + y::Int => x + y\n fib(n::Int) => (n < 2 ? n : :(fib($(n - 1)) + fib($(n - 2))))\nend\n\nparams = SaturationParams(timeout = 60)","category":"page"},{"location":"tutorials/fibonacci/","page":"Benchmarking Fibonacci. E-Graphs memoize computation.","title":"Benchmarking Fibonacci. E-Graphs memoize computation.","text":"We run the saturation twice to see a result that does not include compilation time.","category":"page"},{"location":"tutorials/fibonacci/","page":"Benchmarking Fibonacci. E-Graphs memoize computation.","title":"Benchmarking Fibonacci. E-Graphs memoize computation.","text":"g = EGraph(:(fib(10)))\nsaturate!(g, fibo, params)","category":"page"},{"location":"tutorials/fibonacci/","page":"Benchmarking Fibonacci. E-Graphs memoize computation.","title":"Benchmarking Fibonacci. E-Graphs memoize computation.","text":"That's fast!","category":"page"},{"location":"tutorials/fibonacci/","page":"Benchmarking Fibonacci. E-Graphs memoize computation.","title":"Benchmarking Fibonacci. E-Graphs memoize computation.","text":"z = EGraph(:(fib(10)))\nsaturate!(z, fibo, params)","category":"page"},{"location":"tutorials/fibonacci/","page":"Benchmarking Fibonacci. E-Graphs memoize computation.","title":"Benchmarking Fibonacci. E-Graphs memoize computation.","text":"We can test that the result is correct.","category":"page"},{"location":"tutorials/fibonacci/","page":"Benchmarking Fibonacci. E-Graphs memoize computation.","title":"Benchmarking Fibonacci. E-Graphs memoize computation.","text":"@testset \"Fibonacci\" begin\n @test 55 == extract!(g, astsize)\nend","category":"page"},{"location":"tutorials/fibonacci/","page":"Benchmarking Fibonacci. E-Graphs memoize computation.","title":"Benchmarking Fibonacci. E-Graphs memoize computation.","text":"","category":"page"},{"location":"tutorials/fibonacci/","page":"Benchmarking Fibonacci. E-Graphs memoize computation.","title":"Benchmarking Fibonacci. E-Graphs memoize computation.","text":"This page was generated using Literate.jl.","category":"page"},{"location":"egraphs/#EGraphs-and-Equality-Saturation","page":"EGraphs and Equality Saturation","title":"EGraphs and Equality Saturation","text":"","category":"section"},{"location":"egraphs/","page":"EGraphs and Equality Saturation","title":"EGraphs and Equality Saturation","text":"An EGraph is an efficient data structure for representing congruence relations. EGraphs are data structures originating from theorem provers. Several projects have very recently repurposed EGraphs to implement state-of-the-art, rewrite-driven compiler optimizations and program synthesizers using a technique known as equality saturation. Metatheory.jl provides a general purpose, customizable implementation of EGraphs and equality saturation, inspired from the egg library for Rust. You can read more about the design of the EGraph data structure and equality saturation algorithm in the egg paper.","category":"page"},{"location":"egraphs/","page":"EGraphs and Equality Saturation","title":"EGraphs and Equality Saturation","text":"Let's load Metatheory and the rule library","category":"page"},{"location":"egraphs/","page":"EGraphs and Equality Saturation","title":"EGraphs and Equality Saturation","text":"using Metatheory\nusing Metatheory.Library","category":"page"},{"location":"egraphs/","page":"EGraphs and Equality Saturation","title":"EGraphs and Equality Saturation","text":"DocTestSetup = quote \n using Metatheory\n using Metatheory.Library\nend","category":"page"},{"location":"egraphs/#What-can-I-do-with-EGraphs-in-Metatheory.jl?","page":"EGraphs and Equality Saturation","title":"What can I do with EGraphs in Metatheory.jl?","text":"","category":"section"},{"location":"egraphs/","page":"EGraphs and Equality Saturation","title":"EGraphs and Equality Saturation","text":"In classical term rewriting, rewrites are typically destructive and forget the matched left-hand side. Therefore, rules are applied in an arbitrary or controlled order - this often results in local minima and looping. For decades, programmers and scientists using term rewriting systems have spent their time trying to find confluent and terminating systems of rules. This requires a lot of effort and time. When studying any computational, mathematical or scientific system governed by equational rules, about non obviously oriented equations, such as (a + b) + c = a + (b + c )?","category":"page"},{"location":"egraphs/","page":"EGraphs and Equality Saturation","title":"EGraphs and Equality Saturation","text":"E-Graphs come to our help. EGraphs are bipartite graphs of ENodes and EClasses: a data structure for efficiently represent and rewrite on many equivalent expressions at the same time. A sort of fast data structure for sets of trees. Subtrees and parents are shared if possible. This makes EGraphs similar to DAGs. Most importantly, with EGraph rewriting you can use bidirectional rewrite rules, such as equalities without worrying about the ordering and confluence of your rewrite system! Therefore, rule application in EGraphs is non-destructive - everything is copied! This allows users to run non-deterministic rewrite systems. Many rules can match at the same time and the previous state of expressions will not be lost.","category":"page"},{"location":"egraphs/","page":"EGraphs and Equality Saturation","title":"EGraphs and Equality Saturation","text":"The EGraph backend for Metatheory.jl allows you to create an EGraph from a starting expression, to add more expressions to the EGraph with addexpr!, and then to effectively fill the EGraph with all possible equivalent expressions resulting from applying rewrite rules from a theory, by using the saturate! function. You can then easily extract expressions from an e-graph by calling extract! with a cost function.","category":"page"},{"location":"egraphs/","page":"EGraphs and Equality Saturation","title":"EGraphs and Equality Saturation","text":"A killer feature of egg and Metatheory.jl are EGraph Analyses. They allow you to annotate expressions and equivalence classes in an EGraph with values from a semilattice domain, and then to:","category":"page"},{"location":"egraphs/","page":"EGraphs and Equality Saturation","title":"EGraphs and Equality Saturation","text":"Automatically extract optimal expressions from an EGraph deciding from analysis data.\nHave conditional rules that are executed if some criteria is met on analysis data\nHave dynamic rules that compute the right hand side based on analysis data.","category":"page"},{"location":"egraphs/#Library","page":"EGraphs and Equality Saturation","title":"Library","text":"","category":"section"},{"location":"egraphs/","page":"EGraphs and Equality Saturation","title":"EGraphs and Equality Saturation","text":"The Metatheory.Library module contains utility functions and macros for creating rules and theories from commonly used algebraic structures and properties, to be used with the e-graph backend.","category":"page"},{"location":"egraphs/","page":"EGraphs and Equality Saturation","title":"EGraphs and Equality Saturation","text":"comm_monoid = @commutative_monoid (*) 1\n\n# output\n\n4-element Vector{RewriteRule}:\n ~a * ~b --> ~b * ~a\n (~a * ~b) * ~c --> ~a * (~b * ~c)\n ~a * (~b * ~c) --> (~a * ~b) * ~c\n 1 * ~a --> ~a\n","category":"page"},{"location":"egraphs/#Theories-and-Algebraic-Structures","page":"EGraphs and Equality Saturation","title":"Theories and Algebraic Structures","text":"","category":"section"},{"location":"egraphs/","page":"EGraphs and Equality Saturation","title":"EGraphs and Equality Saturation","text":"The e-graphs backend can directly handle associativity, equalities commutativity and distributivity, rules that are otherwise known of causing loops and require extensive user reasoning in classical rewriting.","category":"page"},{"location":"egraphs/","page":"EGraphs and Equality Saturation","title":"EGraphs and Equality Saturation","text":"t = @theory a b c begin\n a * b == b * a\n a * 1 == a\n a * (b * c) == (a * b) * c\nend\n\n# output\n\n3-element Vector{EqualityRule}:\n ~a * ~b == ~b * ~a\n ~a * 1 == ~a\n ~a * (~b * ~c) == (~a * ~b) * ~c\n","category":"page"},{"location":"egraphs/#Equality-Saturation","page":"EGraphs and Equality Saturation","title":"Equality Saturation","text":"","category":"section"},{"location":"egraphs/","page":"EGraphs and Equality Saturation","title":"EGraphs and Equality Saturation","text":"We can programmatically build and saturate an EGraph. The function saturate! takes an EGraph and a theory, and executes equality saturation. Returns a report of the equality saturation process. saturate! is configurable, customizable parameters include a timeout on the number of iterations, a eclasslimit on the number of e-classes in the EGraph, a stopwhen functions that stops saturation when it evaluates to true.","category":"page"},{"location":"egraphs/","page":"EGraphs and Equality Saturation","title":"EGraphs and Equality Saturation","text":"g = EGraph(:((a * b) * (1 * (b + c))));\nreport = saturate!(g, t);","category":"page"},{"location":"egraphs/","page":"EGraphs and Equality Saturation","title":"EGraphs and Equality Saturation","text":"With the EGraph equality saturation backend, Metatheory.jl can prove simple equalities very efficiently. The @areequal macro takes a theory and some expressions and returns true iff the expressions are equal according to the theory. The following example may return true with an appropriate example theory. ","category":"page"},{"location":"egraphs/","page":"EGraphs and Equality Saturation","title":"EGraphs and Equality Saturation","text":"julia> @areequal some_theory (x+y)*(a+b) ((a*(x+y))+b*(x+y)) ((x*(a+b))+y*(a+b)) ","category":"page"},{"location":"egraphs/#Configurable-Parameters","page":"EGraphs and Equality Saturation","title":"Configurable Parameters","text":"","category":"section"},{"location":"egraphs/","page":"EGraphs and Equality Saturation","title":"EGraphs and Equality Saturation","text":"EGraphs.saturate! can accept an additional parameter of type EGraphs.SaturationParams to configure the equality saturation algorithm. Extensive documentation for the configurable parameters is available in the EGraphs.SaturationParams API docstring.","category":"page"},{"location":"egraphs/","page":"EGraphs and Equality Saturation","title":"EGraphs and Equality Saturation","text":"# create the saturation params\nparams = SaturationParams(timeout=10, eclasslimit=4000)\nsaturate!(egraph, theory, params)","category":"page"},{"location":"egraphs/","page":"EGraphs and Equality Saturation","title":"EGraphs and Equality Saturation","text":"CurrentModule = Base","category":"page"},{"location":"egraphs/#Outline-of-the-Equality-Saturation-Algorithm","page":"EGraphs and Equality Saturation","title":"Outline of the Equality Saturation Algorithm","text":"","category":"section"},{"location":"egraphs/","page":"EGraphs and Equality Saturation","title":"EGraphs and Equality Saturation","text":"The saturate! function behaves as following. Given a starting e-graph g, a set of rewrite rules t and some parameters p (including an iteration limit n):","category":"page"},{"location":"egraphs/","page":"EGraphs and Equality Saturation","title":"EGraphs and Equality Saturation","text":"For each rule in t, search through the e-graph for l.h.s.\nFor each match produced, apply the rewrite\nDo a bottom-up traversal of the e-graph to rebuild the congruence closure\nIf the e-graph hasn’t changed from last iteration, it has saturated. If so, halt saturation.\nLoop at most n times.","category":"page"},{"location":"egraphs/","page":"EGraphs and Equality Saturation","title":"EGraphs and Equality Saturation","text":"Note that knowing if an expression with a set of rules saturates an e-graph or never terminates is still an open research problem","category":"page"},{"location":"egraphs/#Extracting-from-an-EGraph","page":"EGraphs and Equality Saturation","title":"Extracting from an EGraph","text":"","category":"section"},{"location":"egraphs/","page":"EGraphs and Equality Saturation","title":"EGraphs and Equality Saturation","text":"Since e-graphs non-deterministically represent many equivalent symbolic terms, extracting an expression from an EGraph is the process of selecting and extracting a single symbolic expression from the set of all the possible expressions contained in the EGraph. Extraction is done through the extract! function, and the theoretical background behind this procedure is an EGraph Analysis; A cost function is provided as a parameter to the extract! function. This cost function will examine mostly every e-node in the e-graph and will determine which e-nodes will be chosen from each e-class through an automated, recursive algorithm.","category":"page"},{"location":"egraphs/","page":"EGraphs and Equality Saturation","title":"EGraphs and Equality Saturation","text":"Metatheory.jl already provides some simple cost functions, such as astsize, which expresses preference for the smallest expressions contained in equivalence classes.","category":"page"},{"location":"egraphs/","page":"EGraphs and Equality Saturation","title":"EGraphs and Equality Saturation","text":"Here's an example Given the theory:","category":"page"},{"location":"egraphs/","page":"EGraphs and Equality Saturation","title":"EGraphs and Equality Saturation","text":"using Metatheory\nusing Metatheory.Library\n\ncomm_monoid = @commutative_monoid (*) 1;\nt = @theory a b c begin\n a + 0 --> a\n a + b --> b + a\n a + inv(a) --> 0 # inverse\n a + (b + c) --> (a + b) + c\n\ta * (b + c) --> (a * b) + (a * c)\n\t(a * b) + (a * c) --> a * (b + c)\n\ta * a --> a^2\n\ta --> a^1\n\ta^b * a^c --> a^(b+c)\n\tlog(a^b) --> b * log(a)\n\tlog(a * b) --> log(a) + log(b)\n\tlog(1) --> 0\n\tlog(:e) --> 1\n\t:e^(log(a)) --> a\n\ta::Number + b::Number => a + b\n\ta::Number * b::Number => a * b\nend\nt = comm_monoid ∪ t ;\nnothing # hide","category":"page"},{"location":"egraphs/","page":"EGraphs and Equality Saturation","title":"EGraphs and Equality Saturation","text":"We can extract an expression by using","category":"page"},{"location":"egraphs/","page":"EGraphs and Equality Saturation","title":"EGraphs and Equality Saturation","text":"\nexpr = :((log(e) * log(e)) * (log(a^3 * a^2)))\ng = EGraph(expr)\nsaturate!(g, t)\nex = extract!(g, astsize)","category":"page"},{"location":"egraphs/","page":"EGraphs and Equality Saturation","title":"EGraphs and Equality Saturation","text":"The second argument to extract! is a cost function. astsize is a cost function provided by default, which computes the size of expressions.","category":"page"},{"location":"egraphs/#Defining-custom-cost-functions-for-extraction.","page":"EGraphs and Equality Saturation","title":"Defining custom cost functions for extraction.","text":"","category":"section"},{"location":"egraphs/","page":"EGraphs and Equality Saturation","title":"EGraphs and Equality Saturation","text":"A cost function for EGraph extraction is a function used to determine which e-node will be extracted from an e-class. ","category":"page"},{"location":"egraphs/","page":"EGraphs and Equality Saturation","title":"EGraphs and Equality Saturation","text":"It must return a positive, non-complex number value and, must accept 3 arguments.","category":"page"},{"location":"egraphs/","page":"EGraphs and Equality Saturation","title":"EGraphs and Equality Saturation","text":"The current ENode n that is being inspected. \nThe current EGraph g.\nThe current analysis name an::Symbol.","category":"page"},{"location":"egraphs/","page":"EGraphs and Equality Saturation","title":"EGraphs and Equality Saturation","text":"From those 3 parameters, one can access all the data needed to compute the cost of an e-node recursively.","category":"page"},{"location":"egraphs/","page":"EGraphs and Equality Saturation","title":"EGraphs and Equality Saturation","text":"One can use TermInterface.jl methods to access the operation and child arguments of an e-node: operation(n), arity(n) and arguments(n)\nSince e-node children always point to e-classes in the same e-graph, one can retrieve the EClass object for each child of the currently visited enode with g[id] for id in arguments(n)\nOne can inspect the analysis data for a given eclass and a given analysis name an, by using hasdata and getdata.\nExtraction analyses always associate a tuple of 2 values to a single e-class: which e-node is the one that minimizes the cost","category":"page"},{"location":"egraphs/","page":"EGraphs and Equality Saturation","title":"EGraphs and Equality Saturation","text":"and its cost. More details can be found in the egg paper in the Analyses section. ","category":"page"},{"location":"egraphs/","page":"EGraphs and Equality Saturation","title":"EGraphs and Equality Saturation","text":"Here's an example:","category":"page"},{"location":"egraphs/","page":"EGraphs and Equality Saturation","title":"EGraphs and Equality Saturation","text":"# This is a cost function that behaves like `astsize` but increments the cost \n# of nodes containing the `^` operation. This results in a tendency to avoid \n# extraction of expressions containing '^'.\nfunction cost_function(n::ENodeTerm, g::EGraph)\n cost = 1 + arity(n)\n\n operation(n) == :^ && (cost += 2)\n\n for id in arguments(n)\n eclass = g[id]\n # if the child e-class has not yet been analyzed, return +Inf\n !hasdata(eclass, cost_function) && (cost += Inf; break)\n cost += last(getdata(eclass, cost_function))\n end\n return cost\nend\n\n# All literal expressions (e.g `a`, 123, 0.42, \"hello\") have cost 1\ncost_function(n::ENodeLiteral, g::EGraph) = 1","category":"page"},{"location":"egraphs/#EGraph-Analyses","page":"EGraphs and Equality Saturation","title":"EGraph Analyses","text":"","category":"section"},{"location":"egraphs/","page":"EGraphs and Equality Saturation","title":"EGraphs and Equality Saturation","text":"An EGraph Analysis is an efficient and automated way of analyzing all the possible terms contained in an e-graph. Metatheory.jl provides a toolkit to ease and automate the process of EGraph Analysis. ","category":"page"},{"location":"egraphs/","page":"EGraphs and Equality Saturation","title":"EGraphs and Equality Saturation","text":"An EGraph Analysis defines a domain of values and associates a value from the domain to each EClass in the graph. Theoretically, the domain should form a join semilattice. Rewrites can cooperate with e-class analyses by depending on analysis facts and adding equivalences that in turn establish additional facts. ","category":"page"},{"location":"egraphs/","page":"EGraphs and Equality Saturation","title":"EGraphs and Equality Saturation","text":"In Metatheory.jl, EGraph Analyses are uniquely identified by either","category":"page"},{"location":"egraphs/","page":"EGraphs and Equality Saturation","title":"EGraphs and Equality Saturation","text":"An unique name of type Symbol. \nA function object f, used for cost function analysis. This will use built-in definitions of make and join.","category":"page"},{"location":"egraphs/","page":"EGraphs and Equality Saturation","title":"EGraphs and Equality Saturation","text":"If you are specifying a custom analysis by its Symbol name, the following functions define an interface for analyses based on multiple dispatch on Val{analysis_name::Symbol}: ","category":"page"},{"location":"egraphs/","page":"EGraphs and Equality Saturation","title":"EGraphs and Equality Saturation","text":"islazy(an) should return true if the analysis name an should NOT be computed on-the-fly during egraphs operation, but only when inspected. \nmake(an, egraph, n) should take an ENode n and return a value from the analysis domain.\njoin(an, x,y) should return the semilattice join of x and y in the analysis domain (e.g. given two analyses value from ENodes in the same EClass, which one should I choose?). If an is a Function, it is treated as a cost function analysis, it is automatically defined to be the minimum analysis value between x and y. Typically, the domain value of cost functions are real numbers, but if you really do want to have your own cost type, make sure that Base.isless is defined.\nmodify!(an, egraph, eclassid) Can be optionally implemented. This can be used modify an EClass egraph[eclassid] on-the-fly during an e-graph saturation iteration, given its analysis value.","category":"page"},{"location":"egraphs/#Defining-a-custom-analysis","page":"EGraphs and Equality Saturation","title":"Defining a custom analysis","text":"","category":"section"},{"location":"egraphs/","page":"EGraphs and Equality Saturation","title":"EGraphs and Equality Saturation","text":"In this example, we will provide a custom analysis that tags each EClass in an EGraph with :even if it contains an even number or with :odd if it represents an odd number, or nothing if it does not contain a number at all. Let's suppose that the language of the symbolic expressions that we are considering will contain only integer numbers, variable symbols and the `and+` operations.*","category":"page"},{"location":"egraphs/","page":"EGraphs and Equality Saturation","title":"EGraphs and Equality Saturation","text":"Since we are in a symbolic computation context, we are not interested in the the actual numeric result of the expressions in the EGraph, but we only care to analyze and identify the symbolic expressions that will result in an even or an odd number.","category":"page"},{"location":"egraphs/","page":"EGraphs and Equality Saturation","title":"EGraphs and Equality Saturation","text":"Defining an EGraph Analysis is similar to the process Mathematical Induction. To define a custom EGraph Analysis, one should start by defining a name of type Symbol that will be used to identify this specific analysis and to dispatch against the required methods.","category":"page"},{"location":"egraphs/","page":"EGraphs and Equality Saturation","title":"EGraphs and Equality Saturation","text":"using Metatheory\nusing Metatheory.EGraphs","category":"page"},{"location":"egraphs/","page":"EGraphs and Equality Saturation","title":"EGraphs and Equality Saturation","text":"The next step, the base case of induction, is to define a method for make dispatching against our OddEvenAnalysis. First, we want to associate an analysis value only to the literals contained in the EGraph. To do this we take advantage of multiple dispatch against ENodeLiteral.","category":"page"},{"location":"egraphs/","page":"EGraphs and Equality Saturation","title":"EGraphs and Equality Saturation","text":"function EGraphs.make(::Val{:OddEvenAnalysis}, g::EGraph, n::ENodeLiteral)\n if n.value isa Integer\n return iseven(n.value) ? :even : :odd\n else \n return nothing\n end\nend","category":"page"},{"location":"egraphs/","page":"EGraphs and Equality Saturation","title":"EGraphs and Equality Saturation","text":"Now we have to consider the induction step. Knowing that our language contains only * and + operations, and knowing that:","category":"page"},{"location":"egraphs/","page":"EGraphs and Equality Saturation","title":"EGraphs and Equality Saturation","text":"odd * odd = odd\nodd * even = even\neven * even = even","category":"page"},{"location":"egraphs/","page":"EGraphs and Equality Saturation","title":"EGraphs and Equality Saturation","text":"And we know that ","category":"page"},{"location":"egraphs/","page":"EGraphs and Equality Saturation","title":"EGraphs and Equality Saturation","text":"odd + odd = even \nodd + even = odd \neven + even = even","category":"page"},{"location":"egraphs/","page":"EGraphs and Equality Saturation","title":"EGraphs and Equality Saturation","text":"We can now define a method for make dispatching against OddEvenAnalysis and ENodeTerms to compute the analysis value for nested symbolic terms. We take advantage of the methods in TermInterface to inspect the content of an ENodeTerm. From the definition of an ENode, we know that children of ENodes are always IDs pointing to EClasses in the EGraph.","category":"page"},{"location":"egraphs/","page":"EGraphs and Equality Saturation","title":"EGraphs and Equality Saturation","text":"function EGraphs.make(::Val{:OddEvenAnalysis}, g::EGraph, n::ENodeTerm)\n # Let's consider only binary function call terms.\n if exprhead(n) == :call && arity(n) == 2\n op = operation(n)\n # Get the left and right child eclasses\n child_eclasses = arguments(n)\n l = g[child_eclasses[1]]\n r = g[child_eclasses[2]]\n\n # Get the corresponding OddEvenAnalysis value of the children\n # defaulting to nothing \n ldata = getdata(l, :OddEvenAnalysis, nothing)\n rdata = getdata(r, :OddEvenAnalysis, nothing)\n\n if ldata isa Symbol && rdata isa Symbol\n if op == :*\n if ldata == rdata\n ldata\n elseif (ldata == :even || rdata == :even) \n :even\n else\n nothing \n end\n elseif op == :+\n (ldata == rdata) ? :even : :odd\n end\n elseif isnothing(ldata) && rdata isa Symbol && op == :*\n rdata\n elseif ldata isa Symbol && isnothing(rdata) && op == :*\n ldata\n end\n end\n\n return nothing\nend","category":"page"},{"location":"egraphs/","page":"EGraphs and Equality Saturation","title":"EGraphs and Equality Saturation","text":"We have now defined a way of tagging each ENode in the EGraph with :odd or :even, reasoning inductively on the analyses values. The analyze! function will do the dirty job of doing a recursive walk over the EGraph. The missing piece, is now telling Metatheory.jl how to merge together analysis values. Since EClasses represent many equal ENodes, we have to inform the automated analysis how to extract a single value out of the many analyses values contained in an EGraph. We do this by defining a method for join.","category":"page"},{"location":"egraphs/","page":"EGraphs and Equality Saturation","title":"EGraphs and Equality Saturation","text":"function EGraphs.join(::Val{:OddEvenAnalysis}, a, b)\n if a == b \n return a \n else\n # an expression cannot be odd and even at the same time!\n # this is contradictory, so we ignore the analysis value\n return nothing \n end\nend","category":"page"},{"location":"egraphs/","page":"EGraphs and Equality Saturation","title":"EGraphs and Equality Saturation","text":"We do not care to modify the content of EClasses in consequence of our analysis. Therefore, we can skip the definition of modify!. We are now ready to test our analysis.","category":"page"},{"location":"egraphs/","page":"EGraphs and Equality Saturation","title":"EGraphs and Equality Saturation","text":"t = @theory a b c begin \n a * (b * c) == (a * b) * c\n a + (b + c) == (a + b) + c\n a * b == b * a\n a + b == b + a\n a * (b + c) == (a * b) + (a * c)\nend\n\nfunction custom_analysis(expr)\n g = EGraph(expr)\n saturate!(g, t)\n analyze!(g, OddEvenAnalysis)\n return getdata(g[g.root], OddEvenAnalysis)\nend\n\ncustom_analysis(:(2*a)) # :even\ncustom_analysis(:(3*3)) # :odd\ncustom_analysis(:(3*(2+a)*2)) # :even\ncustom_analysis(:(3y * (2x*y))) # :even","category":"page"},{"location":"tutorials/mu/","page":"The MU Puzzle","title":"The MU Puzzle","text":"EditURL = \"https://github.com/JuliaSymbolics/Metatheory.jl/blob/master/test/tutorials/mu.jl\"","category":"page"},{"location":"tutorials/mu/#The-MU-Puzzle","page":"The MU Puzzle","title":"The MU Puzzle","text":"","category":"section"},{"location":"tutorials/mu/","page":"The MU Puzzle","title":"The MU Puzzle","text":"The puzzle cannot be solved: it is impossible to change the string MI into MU by repeatedly applying the given rules. In other words, MU is not a theorem of the MIU formal system. To prove this, one must step \"outside\" the formal system itself. Wikipedia","category":"page"},{"location":"tutorials/mu/","page":"The MU Puzzle","title":"The MU Puzzle","text":"using Metatheory, Test","category":"page"},{"location":"tutorials/mu/","page":"The MU Puzzle","title":"The MU Puzzle","text":"Here are the axioms of MU:","category":"page"},{"location":"tutorials/mu/","page":"The MU Puzzle","title":"The MU Puzzle","text":"Composition of the string monoid is associative\nAdd a uf to the end of any string ending in I\nDouble the string after the M\nReplace any III with a U\nRemove any UU","category":"page"},{"location":"tutorials/mu/","page":"The MU Puzzle","title":"The MU Puzzle","text":"function ⋅ end\nmiu = @theory x y z begin\n x ⋅ (y ⋅ z) --> (x ⋅ y) ⋅ z\n x ⋅ :I ⋅ :END --> x ⋅ :I ⋅ :U ⋅ :END\n :M ⋅ x ⋅ :END --> :M ⋅ x ⋅ x ⋅ :END\n :I ⋅ :I ⋅ :I --> :U\n x ⋅ :U ⋅ :U ⋅ y --> x ⋅ y\nend","category":"page"},{"location":"tutorials/mu/","page":"The MU Puzzle","title":"The MU Puzzle","text":"No matter the timeout we set here, MU is not a theorem of the MIU system","category":"page"},{"location":"tutorials/mu/","page":"The MU Puzzle","title":"The MU Puzzle","text":"params = SaturationParams(timeout = 12, eclasslimit = 8000)\nstart = :(M ⋅ I ⋅ END)\ng = EGraph(start)\nsaturate!(g, miu)\n@test false == areequal(g, miu, start, :(M ⋅ U ⋅ END); params = params)","category":"page"},{"location":"tutorials/mu/","page":"The MU Puzzle","title":"The MU Puzzle","text":"","category":"page"},{"location":"tutorials/mu/","page":"The MU Puzzle","title":"The MU Puzzle","text":"This page was generated using Literate.jl.","category":"page"},{"location":"#Metatheory.jl-2.0","page":"Metatheory.jl 2.0","title":"Metatheory.jl 2.0","text":"","category":"section"},{"location":"","page":"Metatheory.jl 2.0","title":"Metatheory.jl 2.0","text":"

      \n\n

      ","category":"page"},{"location":"","page":"Metatheory.jl 2.0","title":"Metatheory.jl 2.0","text":"(Image: Docs) (Image: Docs) (Image: CI) (Image: codecov) (Image: arXiv) (Image: status) (Image: Zulip)","category":"page"},{"location":"","page":"Metatheory.jl 2.0","title":"Metatheory.jl 2.0","text":"Metatheory.jl is a general purpose term rewriting, metaprogramming and algebraic computation library for the Julia programming language, designed to take advantage of the powerful reflection capabilities to bridge the gap between symbolic mathematics, abstract interpretation, equational reasoning, optimization, composable compiler transforms, and advanced homoiconic pattern matching features. The core features of Metatheory.jl are a powerful rewrite rule definition language, a vast library of functional combinators for classical term rewriting and an e-graph rewriting, a fresh approach to term rewriting achieved through an equality saturation algorithm. Metatheory.jl can manipulate any kind of Julia symbolic expression type, as long as it satisfies the TermInterface.jl.","category":"page"},{"location":"","page":"Metatheory.jl 2.0","title":"Metatheory.jl 2.0","text":"Metatheory.jl provides:","category":"page"},{"location":"","page":"Metatheory.jl 2.0","title":"Metatheory.jl 2.0","text":"An eDSL (domain specific language) to define different kinds of symbolic rewrite rules.\nA classical rewriting backend, derived from the SymbolicUtils.jl pattern matcher, supporting associative-commutative rules. It is based on the pattern matcher in the SICM book.\nA flexible library of rewriter combinators.\nAn e-graph rewriting (equality saturation) backend and pattern matcher, based on the egg library, supporting backtracking and non-deterministic term rewriting by using a data structure called e-graph, efficiently incorporating the notion of equivalence in order to reduce the amount of user effort required to achieve optimization tasks and equational reasoning.\n@capture macro for flexible metaprogramming.","category":"page"},{"location":"","page":"Metatheory.jl 2.0","title":"Metatheory.jl 2.0","text":"Intuitively, Metatheory.jl transforms Julia expressions in other Julia expressions and can achieve such at both compile and run time. This allows Metatheory.jl users to perform customized and composable compiler optimizations specifically tailored to single, arbitrary Julia packages. Our library provides a simple, algebraically composable interface to help scientists in implementing and reasoning about semantics and all kinds of formal systems, by defining concise rewriting rules in pure, syntactically valid Julia on a high level of abstraction. Our implementation of equality saturation on e-graphs is based on the excellent, state-of-the-art technique implemented in the egg library, reimplemented in pure Julia.","category":"page"},{"location":"#.0-is-out!","page":"Metatheory.jl 2.0","title":"2.0 is out!","text":"","category":"section"},{"location":"","page":"Metatheory.jl 2.0","title":"Metatheory.jl 2.0","text":"Second stable version is out:","category":"page"},{"location":"","page":"Metatheory.jl 2.0","title":"Metatheory.jl 2.0","text":"New e-graph pattern matching system, relies on functional programming and closures, and is much more extensible than 1.0's virtual machine.\nNo longer dispatch against types, but instead dispatch against objects.\nFaster E-Graph Analysis\nBetter library macros \nUpdated TermInterface to 0.3.3\nNew interface for e-graph extraction using EGraphs.egraph_reconstruct_expression\nSimplify E-Graph Analysis Interface. Use Symbols or functions for identifying Analyses. \nRemove duplicates in E-Graph analyses data.","category":"page"},{"location":"","page":"Metatheory.jl 2.0","title":"Metatheory.jl 2.0","text":"Many features have been ported from SymbolicUtils.jl. Metatheory.jl can be used in place of SymbolicUtils.jl when you have no need of manipulating mathematical expressions. The introduction of TermInterface.jl has allowed for large potential in generalization of term rewriting and symbolic analysis and manipulation features. Integration between Metatheory.jl with Symbolics.jl, as it has been shown in the \"High-performance symbolic-numerics via multiple dispatch\" paper.","category":"page"},{"location":"#Recommended-Readings-Selected-Publications","page":"Metatheory.jl 2.0","title":"Recommended Readings - Selected Publications","text":"","category":"section"},{"location":"","page":"Metatheory.jl 2.0","title":"Metatheory.jl 2.0","text":"The Metatheory.jl manual \nThe Metatheory.jl introductory paper gives a brief high level overview on the library and its functionalities.\nThe Julia Manual metaprogramming section is fundamental to understand what homoiconic expression manipulation is and how it happens in Julia.\nAn introductory blog post on SIGPLAN about egg and e-graphs rewriting.\negg: Fast and Extensible Equality Saturation contains the definition of E-Graphs on which Metatheory.jl's equality saturation rewriting backend is based. This is a strongly recommended reading.\nHigh-performance symbolic-numerics via multiple dispatch: a paper about how we used Metatheory.jl to optimize code generation in Symbolics.jl","category":"page"},{"location":"#Contributing","page":"Metatheory.jl 2.0","title":"Contributing","text":"","category":"section"},{"location":"","page":"Metatheory.jl 2.0","title":"Metatheory.jl 2.0","text":"If you'd like to give us a hand and contribute to this repository you can:","category":"page"},{"location":"","page":"Metatheory.jl 2.0","title":"Metatheory.jl 2.0","text":"Find a high level description of the project architecture in ARCHITECTURE.md\nRead the contribution guidelines in CONTRIBUTING.md","category":"page"},{"location":"","page":"Metatheory.jl 2.0","title":"Metatheory.jl 2.0","text":"If you enjoyed Metatheory.jl and would like to help, please also consider a tiny donation 💕!","category":"page"},{"location":"#Installation","page":"Metatheory.jl 2.0","title":"Installation","text":"","category":"section"},{"location":"","page":"Metatheory.jl 2.0","title":"Metatheory.jl 2.0","text":"You can install the stable version:","category":"page"},{"location":"","page":"Metatheory.jl 2.0","title":"Metatheory.jl 2.0","text":"julia> using Pkg; Pkg.add(\"Metatheory\")","category":"page"},{"location":"","page":"Metatheory.jl 2.0","title":"Metatheory.jl 2.0","text":"Or you can install the developer version (recommended by now for latest bugfixes)","category":"page"},{"location":"","page":"Metatheory.jl 2.0","title":"Metatheory.jl 2.0","text":"julia> using Pkg; Pkg.add(url=\"https://github.com/JuliaSymbolics/Metatheory.jl\")","category":"page"},{"location":"#Documentation","page":"Metatheory.jl 2.0","title":"Documentation","text":"","category":"section"},{"location":"","page":"Metatheory.jl 2.0","title":"Metatheory.jl 2.0","text":"Extensive Metatheory.jl is available here","category":"page"},{"location":"#Citing","page":"Metatheory.jl 2.0","title":"Citing","text":"","category":"section"},{"location":"","page":"Metatheory.jl 2.0","title":"Metatheory.jl 2.0","text":"If you use Metatheory.jl in your research, please cite our works.","category":"page"},{"location":"","page":"Metatheory.jl 2.0","title":"Metatheory.jl 2.0","text":"","category":"page"},{"location":"","page":"Metatheory.jl 2.0","title":"Metatheory.jl 2.0","text":"

      \n \n \n\n

      ","category":"page"},{"location":"visualizing/#Visualizing-E-Graphs","page":"Visualizing E-Graphs","title":"Visualizing E-Graphs","text":"","category":"section"},{"location":"visualizing/","page":"Visualizing E-Graphs","title":"Visualizing E-Graphs","text":"You can visualize e-graphs in VSCode by using GraphViz.jl","category":"page"},{"location":"visualizing/","page":"Visualizing E-Graphs","title":"Visualizing E-Graphs","text":"All you need to do is to install GraphViz.jl and to evaluate an e-graph after including the extra script:","category":"page"},{"location":"visualizing/","page":"Visualizing E-Graphs","title":"Visualizing E-Graphs","text":"using GraphViz\n\ninclude(dirname(pathof(Metatheory)) * \"/extras/graphviz.jl\")\n\nalgebra_rules = @theory a b c begin\n a * (b * c) == (a * b) * c\n a + (b + c) == (a + b) + c\n\n a + b == b + a\n a * (b + c) == (a * b) + (a * c)\n (a + b) * c == (a * c) + (b * c)\n\n -a == -1 * a\n a - b == a + -b\n 1 * a == a\n\n 0 * a --> 0\n a + 0 --> a\n\n a::Number * b == b * a::Number\n a::Number * b::Number => a * b\n a::Number + b::Number => a + b\nend;\n\nex = :(a - a)\ng = EGraph(ex)\nparams = SaturationParams(; timeout = 2)\nsaturate!(g, algebra_rules, params)\ng","category":"page"},{"location":"visualizing/","page":"Visualizing E-Graphs","title":"Visualizing E-Graphs","text":"And you will see a nice e-graph drawing in the Julia Plots VSCode panel:","category":"page"},{"location":"visualizing/","page":"Visualizing E-Graphs","title":"Visualizing E-Graphs","text":"(Image: E-Graph Drawing)","category":"page"},{"location":"tutorials/custom_types/","page":"Interfacing with Metatheory.jl","title":"Interfacing with Metatheory.jl","text":"EditURL = \"https://github.com/JuliaSymbolics/Metatheory.jl/blob/master/test/tutorials/custom_types.jl\"","category":"page"},{"location":"tutorials/custom_types/#Interfacing-with-Metatheory.jl","page":"Interfacing with Metatheory.jl","title":"Interfacing with Metatheory.jl","text":"","category":"section"},{"location":"tutorials/custom_types/","page":"Interfacing with Metatheory.jl","title":"Interfacing with Metatheory.jl","text":"This section is for Julia package developers who may want to use the rule rewriting systems on their own expression types.","category":"page"},{"location":"tutorials/custom_types/#Defining-the-interface","page":"Interfacing with Metatheory.jl","title":"Defining the interface","text":"","category":"section"},{"location":"tutorials/custom_types/","page":"Interfacing with Metatheory.jl","title":"Interfacing with Metatheory.jl","text":"Metatheory.jl matchers can match any Julia object that implements an interface to traverse it as a tree. The interface in question, is defined in the TermInterface.jl package. Its purpose is to provide a shared interface between various symbolic programming Julia packages. In particular, you should define methods from TermInterface.jl for an expression tree type T with symbol types S to work with SymbolicUtils.jl You can read the documentation of TermInterface.jl on the Github repository.","category":"page"},{"location":"tutorials/custom_types/#Concrete-example","page":"Interfacing with Metatheory.jl","title":"Concrete example","text":"","category":"section"},{"location":"tutorials/custom_types/","page":"Interfacing with Metatheory.jl","title":"Interfacing with Metatheory.jl","text":"using Metatheory, TermInterface, Test\nusing Metatheory.EGraphs","category":"page"},{"location":"tutorials/custom_types/","page":"Interfacing with Metatheory.jl","title":"Interfacing with Metatheory.jl","text":"We first define our custom expression type in MyExpr: It behaves like Expr, but it adds some extra fields.","category":"page"},{"location":"tutorials/custom_types/","page":"Interfacing with Metatheory.jl","title":"Interfacing with Metatheory.jl","text":"struct MyExpr\n head::Any\n args::Vector{Any}\n foo::String # additional metadata\nend\nMyExpr(head, args) = MyExpr(head, args, \"\")\nMyExpr(head) = MyExpr(head, [])","category":"page"},{"location":"tutorials/custom_types/","page":"Interfacing with Metatheory.jl","title":"Interfacing with Metatheory.jl","text":"We also need to define equality for our expression.","category":"page"},{"location":"tutorials/custom_types/","page":"Interfacing with Metatheory.jl","title":"Interfacing with Metatheory.jl","text":"function Base.:(==)(a::MyExpr, b::MyExpr)\n a.head == b.head && a.args == b.args && a.foo == b.foo\nend","category":"page"},{"location":"tutorials/custom_types/#Overriding-TermInterface-methods","page":"Interfacing with Metatheory.jl","title":"Overriding TermInterface` methods","text":"","category":"section"},{"location":"tutorials/custom_types/","page":"Interfacing with Metatheory.jl","title":"Interfacing with Metatheory.jl","text":"First, we need to discern when an expression is a leaf or a tree node. We can do it by overriding istree.","category":"page"},{"location":"tutorials/custom_types/","page":"Interfacing with Metatheory.jl","title":"Interfacing with Metatheory.jl","text":"TermInterface.istree(::MyExpr) = true","category":"page"},{"location":"tutorials/custom_types/","page":"Interfacing with Metatheory.jl","title":"Interfacing with Metatheory.jl","text":"The operation function tells us what's the node's represented operation.","category":"page"},{"location":"tutorials/custom_types/","page":"Interfacing with Metatheory.jl","title":"Interfacing with Metatheory.jl","text":"TermInterface.operation(e::MyExpr) = e.head","category":"page"},{"location":"tutorials/custom_types/","page":"Interfacing with Metatheory.jl","title":"Interfacing with Metatheory.jl","text":"arguments tells the system how to extract the children nodes.","category":"page"},{"location":"tutorials/custom_types/","page":"Interfacing with Metatheory.jl","title":"Interfacing with Metatheory.jl","text":"TermInterface.arguments(e::MyExpr) = e.args","category":"page"},{"location":"tutorials/custom_types/","page":"Interfacing with Metatheory.jl","title":"Interfacing with Metatheory.jl","text":"A particular function is exprhead. It is used to bridge our custom MyExpr type, together with the Expr functionality that is used in Metatheory rule syntax. In this example we say that all expressions of type MyExpr, can be represented (and matched against) by a pattern that is represented by a :call Expr.","category":"page"},{"location":"tutorials/custom_types/","page":"Interfacing with Metatheory.jl","title":"Interfacing with Metatheory.jl","text":"TermInterface.exprhead(::MyExpr) = :call","category":"page"},{"location":"tutorials/custom_types/","page":"Interfacing with Metatheory.jl","title":"Interfacing with Metatheory.jl","text":"While for common usage you will always define exprhead it to be :call, there are some cases where you would like to match your expression types against more complex patterns, for example, to match an expression x against an a[b] kind of pattern, you would need to inform the system that exprhead(x) is :ref, because","category":"page"},{"location":"tutorials/custom_types/","page":"Interfacing with Metatheory.jl","title":"Interfacing with Metatheory.jl","text":"ex = :(a[b])\n(ex.head, ex.args)","category":"page"},{"location":"tutorials/custom_types/","page":"Interfacing with Metatheory.jl","title":"Interfacing with Metatheory.jl","text":"metadata should return the extra metadata. If you have many fields, i suggest using a NamedTuple.","category":"page"},{"location":"tutorials/custom_types/","page":"Interfacing with Metatheory.jl","title":"Interfacing with Metatheory.jl","text":"TermInterface.metadata(e::MyExpr) = e.foo","category":"page"},{"location":"tutorials/custom_types/","page":"Interfacing with Metatheory.jl","title":"Interfacing with Metatheory.jl","text":"Additionally, you can override EGraphs.preprocess on your custom expression to pre-process any expression before insertion in the E-Graph. In this example, we always uppercase the foo::String field of MyExpr.","category":"page"},{"location":"tutorials/custom_types/","page":"Interfacing with Metatheory.jl","title":"Interfacing with Metatheory.jl","text":"EGraphs.preprocess(e::MyExpr) = MyExpr(e.head, e.args, uppercase(e.foo))","category":"page"},{"location":"tutorials/custom_types/","page":"Interfacing with Metatheory.jl","title":"Interfacing with Metatheory.jl","text":"TermInterface provides a very important function called similarterm. It is used to create a term that is in the same closure of types of x. Given an existing term x, it is used to instruct Metatheory how to recompose a similar expression, given a head (the result of operation), some children (given by arguments) and additionally, metadata and exprehead, in case you are recomposing an Expr.","category":"page"},{"location":"tutorials/custom_types/","page":"Interfacing with Metatheory.jl","title":"Interfacing with Metatheory.jl","text":"function TermInterface.similarterm(x::MyExpr, head, args; metadata = nothing, exprhead = :call)\n MyExpr(head, args, isnothing(metadata) ? \"\" : metadata)\nend","category":"page"},{"location":"tutorials/custom_types/","page":"Interfacing with Metatheory.jl","title":"Interfacing with Metatheory.jl","text":"Since similarterm works by making a new term similar to an existing term x, in the e-graphs system, there won't be enough information such as a 'reference' object. Only the type of the object is known. This extra function adds a bit of verbosity, due to compatibility with SymbolicUtils.jl","category":"page"},{"location":"tutorials/custom_types/","page":"Interfacing with Metatheory.jl","title":"Interfacing with Metatheory.jl","text":"function EGraphs.egraph_reconstruct_expression(::Type{MyExpr}, op, args; metadata = nothing, exprhead = nothing)\n MyExpr(op, args, (isnothing(metadata) ? () : metadata))\nend","category":"page"},{"location":"tutorials/custom_types/#Theory-Example","page":"Interfacing with Metatheory.jl","title":"Theory Example","text":"","category":"section"},{"location":"tutorials/custom_types/","page":"Interfacing with Metatheory.jl","title":"Interfacing with Metatheory.jl","text":"Note that terms in the RHS will inherit the type of terms in the LHS.","category":"page"},{"location":"tutorials/custom_types/","page":"Interfacing with Metatheory.jl","title":"Interfacing with Metatheory.jl","text":"t = @theory a begin\n f(z(2), a) --> f(a)\nend","category":"page"},{"location":"tutorials/custom_types/","page":"Interfacing with Metatheory.jl","title":"Interfacing with Metatheory.jl","text":"Let's create an example expression and e-graph","category":"page"},{"location":"tutorials/custom_types/","page":"Interfacing with Metatheory.jl","title":"Interfacing with Metatheory.jl","text":"hcall = MyExpr(:h, [4], \"hello\")\nex = MyExpr(:f, [MyExpr(:z, [2]), hcall])\ng = EGraph(ex; keepmeta = true)","category":"page"},{"location":"tutorials/custom_types/","page":"Interfacing with Metatheory.jl","title":"Interfacing with Metatheory.jl","text":"We use settermtype! on an existing e-graph to inform the system about the default type of expressions that we want newly added expressions to have.","category":"page"},{"location":"tutorials/custom_types/","page":"Interfacing with Metatheory.jl","title":"Interfacing with Metatheory.jl","text":"settermtype!(g, MyExpr)","category":"page"},{"location":"tutorials/custom_types/","page":"Interfacing with Metatheory.jl","title":"Interfacing with Metatheory.jl","text":"Now let's test that it works.","category":"page"},{"location":"tutorials/custom_types/","page":"Interfacing with Metatheory.jl","title":"Interfacing with Metatheory.jl","text":"saturate!(g, t)\nexpected = MyExpr(:f, [MyExpr(:h, [4], \"HELLO\")], \"\")\nextracted = extract!(g, astsize)\n@test expected == extracted","category":"page"},{"location":"tutorials/custom_types/","page":"Interfacing with Metatheory.jl","title":"Interfacing with Metatheory.jl","text":"","category":"page"},{"location":"tutorials/custom_types/","page":"Interfacing with Metatheory.jl","title":"Interfacing with Metatheory.jl","text":"This page was generated using Literate.jl.","category":"page"}] +[{"location":"tutorials/while_interpreter/","page":"Write a very tiny Turing Complete language in Julia.","title":"Write a very tiny Turing Complete language in Julia.","text":"EditURL = \"https://github.com/JuliaSymbolics/Metatheory.jl/blob/master/test/tutorials/while_interpreter.jl\"","category":"page"},{"location":"tutorials/while_interpreter/#Write-a-very-tiny-Turing-Complete-language-in-Julia.","page":"Write a very tiny Turing Complete language in Julia.","title":"Write a very tiny Turing Complete language in Julia.","text":"","category":"section"},{"location":"tutorials/while_interpreter/","page":"Write a very tiny Turing Complete language in Julia.","title":"Write a very tiny Turing Complete language in Julia.","text":"WHILE is a very tiny Turing Complete Programming Language defined by denotational semantics. Semantics come from the excellent course notes in \"Elements of computability and complexity\" by prof. Pierpaolo Degano.","category":"page"},{"location":"tutorials/while_interpreter/","page":"Write a very tiny Turing Complete language in Julia.","title":"Write a very tiny Turing Complete language in Julia.","text":"It is a toy C-like language used to explain the core concepts of computability and Turing-completeness. The name WHILE, comes from the fact that the most complicated construct in the language is a WHILE loop. The language supports:","category":"page"},{"location":"tutorials/while_interpreter/","page":"Write a very tiny Turing Complete language in Julia.","title":"Write a very tiny Turing Complete language in Julia.","text":"A variable-value memory that can be pre-defined for program input.\nInteger arithmetics.\nBoolean logic.\nConditional if-then-else statement called cond.\nRunning a command after another with seq(c1,c2).\nRepeatedly applying a command c while a condition g holds with loop(g,c).","category":"page"},{"location":"tutorials/while_interpreter/","page":"Write a very tiny Turing Complete language in Julia.","title":"Write a very tiny Turing Complete language in Julia.","text":"This is enough to be Turing-complete!","category":"page"},{"location":"tutorials/while_interpreter/","page":"Write a very tiny Turing Complete language in Julia.","title":"Write a very tiny Turing Complete language in Julia.","text":"We are going to implement this tiny imperative language with classical rewriting rules in Metatheory.jl. WHILE is implemented in around 55 readable lines of code, and reaches around 80 lines with tests.","category":"page"},{"location":"tutorials/while_interpreter/","page":"Write a very tiny Turing Complete language in Julia.","title":"Write a very tiny Turing Complete language in Julia.","text":"The goal of this tutorial is to show an implementation of a programming language interpreter that is very, very very close to the simple theory used to describe it in a textbook. Each denotational semantics rule in the course notes is a Metatheory.jl rewrite rule, with a few extras and minor naming changes. The idea, is that Julia is a really valid didactical programming language!","category":"page"},{"location":"tutorials/while_interpreter/","page":"Write a very tiny Turing Complete language in Julia.","title":"Write a very tiny Turing Complete language in Julia.","text":"Let's load the Metatheory and Test packages.","category":"page"},{"location":"tutorials/while_interpreter/","page":"Write a very tiny Turing Complete language in Julia.","title":"Write a very tiny Turing Complete language in Julia.","text":"using Test, Metatheory","category":"page"},{"location":"tutorials/while_interpreter/#Memory","page":"Write a very tiny Turing Complete language in Julia.","title":"Memory","text":"","category":"section"},{"location":"tutorials/while_interpreter/","page":"Write a very tiny Turing Complete language in Julia.","title":"Write a very tiny Turing Complete language in Julia.","text":"The first thing that our programming language needs, is a model of the computer memory, that is going to hold the state of the programs. We define the type of WHILE's memory as a map from variables (Julia Symbols) to actual values. We want to keep things simple so in our toy programming language we are just going to use boolean or integer values. Surprisingly, we can still achieve turing completeness without having to introduce strings or any other complex data type. We are going to use the letter σ (sigma) to denote an actual value of type Mem, in simple words the state of a program in a given moment. For example, if a σ::Mem holds the value σ[:a] = 2, this means that at that given moment, in our program the variable a holds the value 2.","category":"page"},{"location":"tutorials/while_interpreter/","page":"Write a very tiny Turing Complete language in Julia.","title":"Write a very tiny Turing Complete language in Julia.","text":"Mem = Dict{Symbol,Union{Bool,Int}}","category":"page"},{"location":"tutorials/while_interpreter/","page":"Write a very tiny Turing Complete language in Julia.","title":"Write a very tiny Turing Complete language in Julia.","text":"We are now ready to define our first rewrite rule. In WHILE, un-evaluated expressions are represented by a tuple of (program, state). This simple rule tells us that, if at a given memory state σ we want to know the value of a variable v, we can simply read it from the memory and return the value.","category":"page"},{"location":"tutorials/while_interpreter/","page":"Write a very tiny Turing Complete language in Julia.","title":"Write a very tiny Turing Complete language in Julia.","text":"read_mem = @theory v σ begin\n (v::Symbol, σ::Mem) => σ[v]\nend","category":"page"},{"location":"tutorials/while_interpreter/","page":"Write a very tiny Turing Complete language in Julia.","title":"Write a very tiny Turing Complete language in Julia.","text":"Let's test this behavior. We first create a Mem, holding the variable x with value 2.","category":"page"},{"location":"tutorials/while_interpreter/","page":"Write a very tiny Turing Complete language in Julia.","title":"Write a very tiny Turing Complete language in Julia.","text":"σ₁ = Mem(:x => 2)","category":"page"},{"location":"tutorials/while_interpreter/","page":"Write a very tiny Turing Complete language in Julia.","title":"Write a very tiny Turing Complete language in Julia.","text":"Then, we define a program. Julia helps us avoid unneeded complications. Generally, to create an interpreted programming language, one would have to design a syntax for it, and then engineer components such as a lexer or a parser in order to turn the input string into a manipulable, structured program. The Julia developers were really smart. We can directly re-use the whole Julia syntax, because Julia allows us to treat programs as values. You can try this by prefixing any expression you type in the REPL inside of :( ... ) or quote ... end. If you type this in the Julia REPL:","category":"page"},{"location":"tutorials/while_interpreter/","page":"Write a very tiny Turing Complete language in Julia.","title":"Write a very tiny Turing Complete language in Julia.","text":"2 + 2","category":"page"},{"location":"tutorials/while_interpreter/","page":"Write a very tiny Turing Complete language in Julia.","title":"Write a very tiny Turing Complete language in Julia.","text":"You get the obvious result out, but if you wrap it in quote or :(...), you can see that the program will not be executed, but instead stored as an Expr.","category":"page"},{"location":"tutorials/while_interpreter/","page":"Write a very tiny Turing Complete language in Julia.","title":"Write a very tiny Turing Complete language in Julia.","text":"some_expr = :(2 + 2)","category":"page"},{"location":"tutorials/while_interpreter/","page":"Write a very tiny Turing Complete language in Julia.","title":"Write a very tiny Turing Complete language in Julia.","text":"We can use the $ unary operator to interpolate and insert values inside of quoted code.","category":"page"},{"location":"tutorials/while_interpreter/","page":"Write a very tiny Turing Complete language in Julia.","title":"Write a very tiny Turing Complete language in Julia.","text":":(2 + $(1 + 1))","category":"page"},{"location":"tutorials/while_interpreter/","page":"Write a very tiny Turing Complete language in Julia.","title":"Write a very tiny Turing Complete language in Julia.","text":"These code-manipulation utilities can be very useful, because we can completely skip the burden of having to write a new syntax for our educational programming language, and just re-use Julia's syntax. It hints us that Julia is very powerful, because you can define new semantics and customize the language's behaviour without having to leave the comfort of the Julia terminal. This is also how julia @macros work. The practice of manipulating programs in the language itself is called Metaprogramming, and you can read more about metaprogramming in Julia in the official docs.","category":"page"},{"location":"tutorials/while_interpreter/","page":"Write a very tiny Turing Complete language in Julia.","title":"Write a very tiny Turing Complete language in Julia.","text":"Let's test that our first, simple rule is working.","category":"page"},{"location":"tutorials/while_interpreter/","page":"Write a very tiny Turing Complete language in Julia.","title":"Write a very tiny Turing Complete language in Julia.","text":"program = :(x, $σ₁)\n@test rewrite(program, read_mem) == 2","category":"page"},{"location":"tutorials/while_interpreter/#Arithmetics","page":"Write a very tiny Turing Complete language in Julia.","title":"Arithmetics","text":"","category":"section"},{"location":"tutorials/while_interpreter/","page":"Write a very tiny Turing Complete language in Julia.","title":"Write a very tiny Turing Complete language in Julia.","text":"How can our programming language be turing complete if we do not include basic arithmetics? If we have an integer and a memory state, we can just keep the integer The following rules are the first cases of recursion. Given two expressions a,b, to know what's a + b in state σ, we need to know first what a and b are in state σ The last dynamic rules let us directly evaluate arithmetic operations.","category":"page"},{"location":"tutorials/while_interpreter/","page":"Write a very tiny Turing Complete language in Julia.","title":"Write a very tiny Turing Complete language in Julia.","text":"arithm_rules = @theory a b n σ begin\n (n::Int, σ::Mem) --> n\n (a + b, σ::Mem) --> (a, σ) + (b, σ)\n (a * b, σ::Mem) --> (a, σ) * (b, σ)\n (a - b, σ::Mem) --> (a, σ) - (b, σ)\n (a::Int + b::Int) => a + b\n (a::Int * b::Int) => a * b\n (a::Int - b::Int) => a - b\nend","category":"page"},{"location":"tutorials/while_interpreter/#Evaluation-strategy","page":"Write a very tiny Turing Complete language in Julia.","title":"Evaluation strategy","text":"","category":"section"},{"location":"tutorials/while_interpreter/","page":"Write a very tiny Turing Complete language in Julia.","title":"Write a very tiny Turing Complete language in Julia.","text":"We now have some nice denotational semantic rules for arithmetics, but in what order should we apply them? Metatheory.jl provides a flexible rewriter combinator library. You can read more in the Rewriters module docs.","category":"page"},{"location":"tutorials/while_interpreter/","page":"Write a very tiny Turing Complete language in Julia.","title":"Write a very tiny Turing Complete language in Julia.","text":"Given a set of rules, we can define a rewriter strategy by functionally composing rewriters. First, we want to use Chain to combine together the many rules in the theory, and to try to apply them one-by-one on our expressions.","category":"page"},{"location":"tutorials/while_interpreter/","page":"Write a very tiny Turing Complete language in Julia.","title":"Write a very tiny Turing Complete language in Julia.","text":"But should we first evaluate the outermost operations in the expression, or the innermost? Intuitively, if we have the program (1 + 2) - 3, it can hint us that we do want to first evaluate the innermost expressions. To do so, we then pass the result to the Postwalk rewriter, which recursively walks the input expression tree, and applies the rewriter first on the inner expressions, and then, on the outer, rewritten expression. (Hence the name Post-walk. Can you guess what Prewalk does?).","category":"page"},{"location":"tutorials/while_interpreter/","page":"Write a very tiny Turing Complete language in Julia.","title":"Write a very tiny Turing Complete language in Julia.","text":"The last component of our strategy is the Fixpoint combinator. This combinator repeatedly applies the rewriter on the input expression, and it does stop looping only when the output expression is the unchanged input expression.","category":"page"},{"location":"tutorials/while_interpreter/","page":"Write a very tiny Turing Complete language in Julia.","title":"Write a very tiny Turing Complete language in Julia.","text":"using Metatheory.Rewriters\nstrategy = (Fixpoint ∘ Postwalk ∘ Chain)","category":"page"},{"location":"tutorials/while_interpreter/","page":"Write a very tiny Turing Complete language in Julia.","title":"Write a very tiny Turing Complete language in Julia.","text":"In Metatheory.jl, rewrite theories are just vectors of Rules. It means we can compose them by concatenating the vectors, or elegantly using the built-in set operations provided by the Julia language.","category":"page"},{"location":"tutorials/while_interpreter/","page":"Write a very tiny Turing Complete language in Julia.","title":"Write a very tiny Turing Complete language in Julia.","text":"arithm_lang = read_mem ∪ arithm_rules","category":"page"},{"location":"tutorials/while_interpreter/","page":"Write a very tiny Turing Complete language in Julia.","title":"Write a very tiny Turing Complete language in Julia.","text":"We can define a convenience function that takes an expression, a memory state and calls our strategy.","category":"page"},{"location":"tutorials/while_interpreter/","page":"Write a very tiny Turing Complete language in Julia.","title":"Write a very tiny Turing Complete language in Julia.","text":"eval_arithm(ex, mem) = strategy(arithm_lang)(:($ex, $mem))","category":"page"},{"location":"tutorials/while_interpreter/","page":"Write a very tiny Turing Complete language in Julia.","title":"Write a very tiny Turing Complete language in Julia.","text":"Does it work?","category":"page"},{"location":"tutorials/while_interpreter/","page":"Write a very tiny Turing Complete language in Julia.","title":"Write a very tiny Turing Complete language in Julia.","text":"@test eval_arithm(:(2 + 3), Mem()) == 5","category":"page"},{"location":"tutorials/while_interpreter/","page":"Write a very tiny Turing Complete language in Julia.","title":"Write a very tiny Turing Complete language in Julia.","text":"Yay! Let's say that before the program started, the computer memory already held a variable x with value 2.","category":"page"},{"location":"tutorials/while_interpreter/","page":"Write a very tiny Turing Complete language in Julia.","title":"Write a very tiny Turing Complete language in Julia.","text":"@test eval_arithm(:(2 + x), Mem(:x => 2)) == 4","category":"page"},{"location":"tutorials/while_interpreter/#Boolean-Logic","page":"Write a very tiny Turing Complete language in Julia.","title":"Boolean Logic","text":"","category":"section"},{"location":"tutorials/while_interpreter/","page":"Write a very tiny Turing Complete language in Julia.","title":"Write a very tiny Turing Complete language in Julia.","text":"To be Turing-complete, our tiny WHILE language requires boolean logic support. There's nothing special or different from other programming languages. These rules define boolean operations to work just as you would expect, and in the same way we defined arithmetic rules for integers.","category":"page"},{"location":"tutorials/while_interpreter/","page":"Write a very tiny Turing Complete language in Julia.","title":"Write a very tiny Turing Complete language in Julia.","text":"We need to bridge together the world of integer arithmetics and boolean logic to achieve something useful. The last two rules in the theory.","category":"page"},{"location":"tutorials/while_interpreter/","page":"Write a very tiny Turing Complete language in Julia.","title":"Write a very tiny Turing Complete language in Julia.","text":"bool_rules = @theory a b σ begin\n (a::Bool || b::Bool) => (a || b)\n (a::Bool && b::Bool) => (a && b)\n !a::Bool => !a\n (a::Bool, σ::Mem) => a\n (!b, σ::Mem) => !eval_bool(b, σ)\n (a || b, σ::Mem) --> (a, σ) || (b, σ)\n (a && b, σ::Mem) --> (a, σ) && (b, σ)\n (a < b, σ::Mem) => (eval_arithm(a, σ) < eval_arithm(b, σ)) # This rule bridges together ints and bools\n (a::Int < b::Int) => (a < b)\nend\n\neval_bool(ex, mem) = strategy(bool_rules)(:($ex, $mem))","category":"page"},{"location":"tutorials/while_interpreter/","page":"Write a very tiny Turing Complete language in Julia.","title":"Write a very tiny Turing Complete language in Julia.","text":"Let's run a few tests.","category":"page"},{"location":"tutorials/while_interpreter/","page":"Write a very tiny Turing Complete language in Julia.","title":"Write a very tiny Turing Complete language in Julia.","text":"@test all(\n [\n eval_bool(:(false || false), Mem()) == false\n eval_bool(:((false || false) || !(false || false)), Mem(:x => 2)) == true\n eval_bool(:((2 < 3) && (3 < 4)), Mem(:x => 2)) == true\n eval_bool(:((2 < x) || !(3 < 4)), Mem(:x => 2)) == false\n eval_bool(:((2 < x) || !(3 < 4)), Mem(:x => 4)) == true\n ],\n)","category":"page"},{"location":"tutorials/while_interpreter/#Conditionals:-If-then-else","page":"Write a very tiny Turing Complete language in Julia.","title":"Conditionals: If-then-else","text":"","category":"section"},{"location":"tutorials/while_interpreter/","page":"Write a very tiny Turing Complete language in Julia.","title":"Write a very tiny Turing Complete language in Julia.","text":"Conditional expressions in our language take the form of cond(guard, thenbranch) or cond(guard, branch, elsebranch) It means that our program at this point will:","category":"page"},{"location":"tutorials/while_interpreter/","page":"Write a very tiny Turing Complete language in Julia.","title":"Write a very tiny Turing Complete language in Julia.","text":"Evaluate the guard expressions\nIf guard evaluates to true, then evaluate thenbranch\nIf guard evaluates to false, then evaluate elsebranch","category":"page"},{"location":"tutorials/while_interpreter/","page":"Write a very tiny Turing Complete language in Julia.","title":"Write a very tiny Turing Complete language in Julia.","text":"The first rule here is simple. If there's no elsebranch in the cond statement, we add an empty one with the skip command. Otherwise, we piggyback on the existing Julia if-then-else ternary operator. To do so, we need to evaluate the boolean expression in the guard by using the eval_bool function we defined above.","category":"page"},{"location":"tutorials/while_interpreter/","page":"Write a very tiny Turing Complete language in Julia.","title":"Write a very tiny Turing Complete language in Julia.","text":"if_rules = @theory guard t f σ begin\n (cond(guard, t), σ::Mem) --> (cond(guard, t, :skip), σ)\n (cond(guard, t, f), σ::Mem) => (eval_bool(guard, σ) ? :($t, $σ) : :($f, $σ))\nend\n\neval_if(ex, mem::Mem) = strategy(read_mem ∪ arithm_rules ∪ if_rules)(:($ex, $mem))","category":"page"},{"location":"tutorials/while_interpreter/","page":"Write a very tiny Turing Complete language in Julia.","title":"Write a very tiny Turing Complete language in Julia.","text":"And here is our working conditional","category":"page"},{"location":"tutorials/while_interpreter/","page":"Write a very tiny Turing Complete language in Julia.","title":"Write a very tiny Turing Complete language in Julia.","text":"@testset \"If Semantics\" begin\n @test 2 == eval_if(:(cond(true, x, 0)), Mem(:x => 2))\n @test 0 == eval_if(:(cond(false, x, 0)), Mem(:x => 2))\n @test 2 == eval_if(:(cond(!(false), x, 0)), Mem(:x => 2))\n @test 0 == eval_if(:(cond(!(2 < x), x, 0)), Mem(:x => 3))\nend","category":"page"},{"location":"tutorials/while_interpreter/#Writing-memory","page":"Write a very tiny Turing Complete language in Julia.","title":"Writing memory","text":"","category":"section"},{"location":"tutorials/while_interpreter/","page":"Write a very tiny Turing Complete language in Julia.","title":"Write a very tiny Turing Complete language in Julia.","text":"Our language then needs a mechanism to write in memory. We define the behavior of the store construct, which behaves like the = assignment operator in other programming languages. store(a, 5) will store the value 5 in the a variable inside the program's memory.","category":"page"},{"location":"tutorials/while_interpreter/","page":"Write a very tiny Turing Complete language in Julia.","title":"Write a very tiny Turing Complete language in Julia.","text":"write_mem = @theory sym val σ begin\n (store(sym::Symbol, val), σ) => (σ[sym] = eval_if(val, σ);\n σ)\nend","category":"page"},{"location":"tutorials/while_interpreter/#While-loops-and-sequential-computation.","page":"Write a very tiny Turing Complete language in Julia.","title":"While loops and sequential computation.","text":"","category":"section"},{"location":"tutorials/while_interpreter/","page":"Write a very tiny Turing Complete language in Julia.","title":"Write a very tiny Turing Complete language in Julia.","text":"while_rules = @theory guard a b σ begin\n (:skip, σ::Mem) --> σ\n ((:skip; b), σ::Mem) --> (b, σ)\n (seq(a, b), σ::Mem) --> (b, merge((a, σ), σ))\n merge(a::Mem, σ::Mem) => merge(σ, a)\n merge(a::Union{Bool,Int}, σ::Mem) --> σ\n (loop(guard, a), σ::Mem) --> (cond(guard, seq(a, loop(guard, a)), :skip), σ)\nend","category":"page"},{"location":"tutorials/while_interpreter/#Completing-the-language.","page":"Write a very tiny Turing Complete language in Julia.","title":"Completing the language.","text":"","category":"section"},{"location":"tutorials/while_interpreter/","page":"Write a very tiny Turing Complete language in Julia.","title":"Write a very tiny Turing Complete language in Julia.","text":"while_language = write_mem ∪ read_mem ∪ arithm_rules ∪ if_rules ∪ while_rules;\n\nusing Metatheory.Syntax: rmlines\neval_while(ex, mem) = strategy(while_language)(:($(rmlines(ex)), $mem))","category":"page"},{"location":"tutorials/while_interpreter/","page":"Write a very tiny Turing Complete language in Julia.","title":"Write a very tiny Turing Complete language in Julia.","text":"Final steps","category":"page"},{"location":"tutorials/while_interpreter/","page":"Write a very tiny Turing Complete language in Julia.","title":"Write a very tiny Turing Complete language in Julia.","text":"@testset \"While Semantics\" begin\n @test Mem(:x => 3) == eval_while(:((store(x, 3))), Mem(:x => 2))\n @test Mem(:x => 5) == eval_while(:(seq(store(x, 4), store(x, x + 1))), Mem(:x => 3))\n @test Mem(:x => 4) == eval_while(:(cond(x < 10, store(x, x + 1))), Mem(:x => 3))\n @test 10 == eval_while(:(seq(loop(x < 10, store(x, x + 1)), x)), Mem(:x => 3))\n @test 50 == eval_while(:(seq(loop(x < y, seq(store(x, x + 1), store(y, y - 1))), x)), Mem(:x => 0, :y => 100))\nend","category":"page"},{"location":"tutorials/while_interpreter/","page":"Write a very tiny Turing Complete language in Julia.","title":"Write a very tiny Turing Complete language in Julia.","text":"","category":"page"},{"location":"tutorials/while_interpreter/","page":"Write a very tiny Turing Complete language in Julia.","title":"Write a very tiny Turing Complete language in Julia.","text":"This page was generated using Literate.jl.","category":"page"},{"location":"api/#API-Documentation","page":"API Documentation","title":"API Documentation","text":"","category":"section"},{"location":"api/#Syntax","page":"API Documentation","title":"Syntax","text":"","category":"section"},{"location":"api/","page":"API Documentation","title":"API Documentation","text":"Modules = [Metatheory.Syntax]","category":"page"},{"location":"api/#Metatheory.Syntax.rewrite_rhs-Tuple{Expr}","page":"API Documentation","title":"Metatheory.Syntax.rewrite_rhs","text":"rewrite_rhs(expr::Expr)\n\nRewrite the expr by dealing with :where if necessary. The :where is rewritten from, for example, ~x where f(~x) to f(~x) ? ~x : nothing.\n\n\n\n\n\n","category":"method"},{"location":"api/#Metatheory.Syntax.rmlines-Tuple{Expr}","page":"API Documentation","title":"Metatheory.Syntax.rmlines","text":"Remove LineNumberNode from quoted blocks of code\n\n\n\n\n\n","category":"method"},{"location":"api/#Metatheory.Syntax.@capture-Tuple","page":"API Documentation","title":"Metatheory.Syntax.@capture","text":"@capture ex pattern\n\nUses 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\n\njulia> @syms a; ex = a^a;\njulia> if @capture ex (~x)^(~x)\n @show x\n elseif @capture ex 2(~y)\n @show y\n end;\nx = a\n\nSee also: @rule\n\n\n\n\n\n","category":"macro"},{"location":"api/#Metatheory.Syntax.@rule-Tuple","page":"API Documentation","title":"Metatheory.Syntax.@rule","text":"@rule [SLOTS...] LHS operator RHS\n\nCreates 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.\n\nLHS 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).\n\nSLOTS 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.\n\nIf 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.\n\nRule operators:\n\nLHS => RHS: create a DynamicRule. The RHS is evaluated on rewrite.\nLHS --> RHS: create a RewriteRule. The RHS is not evaluated but symbolically substituted on rewrite.\nLHS == 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\nLHS ≠ 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.\n\nSlot:\n\nA 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).\n\nExample:\n\nSimple rule to turn any sin into cos:\n\njulia> r = @rule sin(~x) --> cos(~x)\nsin(~x) --> cos(~x)\n\njulia> r(:(sin(1+a)))\n:(cos((1 + a)))\n\nA rule with 2 segment variables\n\njulia> r = @rule sin(~x + ~y) --> sin(~x)*cos(~y) + cos(~x)*sin(~y)\nsin(~x + ~y) --> sin(~x) * cos(~y) + cos(~x) * sin(~y)\n\njulia> r(:(sin(a + b)))\n:(cos(a)*sin(b) + sin(a)*cos(b))\n\nA rule that matches two of the same expressions:\n\njulia> r = @rule sin(~x)^2 + cos(~x)^2 --> 1\nsin(~x) ^ 2 + cos(~x) ^ 2 --> 1\n\njulia> r(:(sin(2a)^2 + cos(2a)^2))\n1\n\njulia> r(:(sin(2a)^2 + cos(a)^2))\n# nothing\n\nA rule without ~\n\njulia> r = @slots x y z @rule x(y + z) --> x*y + x*z\nx(y + z) --> x*y + x*z\n\nSegment: A Segment variable matches zero or more expressions in the function call. Segments may be written by splatting slot variables (~x...).\n\nExample:\n\njulia> r = @rule f(~xs...) --> g(~xs...);\njulia> r(:(f(1, 2, 3)))\n:(g(1,2,3))\n\nPredicates:\n\nThere 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.\n\nThe predicate should return true if the current match is acceptable, and false otherwise.\n\njulia> two_πs(x::Number) = abs(round(x/(2π)) - x/(2π)) < 10^-9\ntwo_πs (generic function with 1 method)\n\njulia> two_πs(x) = false\ntwo_πs (generic function with 2 methods)\n\njulia> r = @rule sin(~~x + ~y::two_πs + ~~z) => :(sin($(Expr(:call, :+, ~~x..., ~~z...))))\nsin(~(~x) + ~(y::two_πs) + ~(~z)) --> sin(+(~(~x)..., ~(~z)...))\n\njulia> r(:(sin(a+$(3π))))\n\njulia> r(:(sin(a+$(6π))))\n:(sin(+a))\n\njulia> r(sin(a+6π+c))\n:(sin(a + c))\n\nPredicate function gets an array of values if attached to a segment variable (~x...).\n\nFor the predicate over the whole rule, use @rule => where :\n\njulia> predicate(x) = x === a;\n\njulia> r = @rule ~x => ~x where f(~x);\n\njulia> r(a)\na\n\njulia> r(b) === nothing\ntrue\n\nNote that this is syntactic sugar and that it is the same as @rule ~x => f(~x) ? ~x : nothing.\n\nCompatibility: 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\n\n\n\n\n\n","category":"macro"},{"location":"api/#Metatheory.Syntax.@slots-Tuple","page":"API Documentation","title":"Metatheory.Syntax.@slots","text":"@slots [SLOTS...] ex\n\nDeclare SLOTS as slot variables for all @rule or @capture invocations in the expression ex. Example:\n\njulia> @slots x y z a b c Chain([\n (@rule x^2 + 2x*y + y^2 => (x + y)^2),\n (@rule x^a * y^b => (x*y)^a * y^(b-a)),\n (@rule +(x...) => sum(x)),\n])\n\nSee also: @rule, @capture\n\n\n\n\n\n","category":"macro"},{"location":"api/#Metatheory.Syntax.@theory-Tuple","page":"API Documentation","title":"Metatheory.Syntax.@theory","text":"@theory [SLOTS...] begin (LHS operator RHS)... end\n\nSyntax sugar to define a vector of rules in a nice and readable way. Can use @slots or have the slots as the first arguments:\n\njulia> t = @theory x y z begin \n x * (y + z) --> (x * y) + (x * z)\n x + y == (y + x)\n #...\nend;\n\nIs the same thing as writing\n\njulia> v = [\n @rule x y z x * (y + z) --> (x * y) + (x * z)\n @rule x y x + y == (y + x)\n #...\n];\n\n\n\n\n\n","category":"macro"},{"location":"api/","page":"API Documentation","title":"API Documentation","text":"","category":"page"},{"location":"api/#Patterns","page":"API Documentation","title":"Patterns","text":"","category":"section"},{"location":"api/","page":"API Documentation","title":"API Documentation","text":"Modules = [Metatheory.Patterns]","category":"page"},{"location":"api/#Metatheory.Patterns.AbstractPat","page":"API Documentation","title":"Metatheory.Patterns.AbstractPat","text":"Abstract type representing a pattern used in all the various pattern matching backends. \n\n\n\n\n\n","category":"type"},{"location":"api/#Metatheory.Patterns.PatSegment","page":"API Documentation","title":"Metatheory.Patterns.PatSegment","text":"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. \n\n\n\n\n\n","category":"type"},{"location":"api/#Metatheory.Patterns.PatTerm","page":"API Documentation","title":"Metatheory.Patterns.PatTerm","text":"Term patterns will match on terms of the same arity and with the same function symbol operation and expression head exprhead.\n\n\n\n\n\n","category":"type"},{"location":"api/#Metatheory.Patterns.PatVar","page":"API Documentation","title":"Metatheory.Patterns.PatVar","text":"PatVar{P}(name, debrujin_index, predicate::P)\n\nPattern variables will first match on one subterm and instantiate the substitution to that subterm.\n\nMatcher 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.\n\npredicate 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. \n\n\n\n\n\n","category":"type"},{"location":"api/#Metatheory.Patterns.isground-Tuple{AbstractPat}","page":"API Documentation","title":"Metatheory.Patterns.isground","text":"A ground pattern contains no pattern variables and only literal values to match.\n\n\n\n\n\n","category":"method"},{"location":"api/#Metatheory.Patterns.patvars-Tuple{PatVar, Any}","page":"API Documentation","title":"Metatheory.Patterns.patvars","text":"Collects pattern variables appearing in a pattern into a vector of symbols\n\n\n\n\n\n","category":"method"},{"location":"api/","page":"API Documentation","title":"API Documentation","text":"","category":"page"},{"location":"api/#Rules","page":"API Documentation","title":"Rules","text":"","category":"section"},{"location":"api/","page":"API Documentation","title":"API Documentation","text":"Modules = [Metatheory.Rules]","category":"page"},{"location":"api/#Metatheory.Rules.DynamicRule","page":"API Documentation","title":"Metatheory.Rules.DynamicRule","text":"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.\n\nDynamic rule\n\n@rule ~a::Number * ~b::Number => ~a*~b\n\n\n\n\n\n","category":"type"},{"location":"api/#Metatheory.Rules.EqualityRule","page":"API Documentation","title":"Metatheory.Rules.EqualityRule","text":"An EqualityRule can is a symbolic substitution rule that can be rewritten bidirectional. Therefore, it should only be used with the EGraphs backend.\n\n@rule ~a * ~b == ~b * ~a\n\n\n\n\n\n","category":"type"},{"location":"api/#Metatheory.Rules.RewriteRule","page":"API Documentation","title":"Metatheory.Rules.RewriteRule","text":"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.\n\n@rule ~a * ~b --> ~b * ~a\n\n\n\n\n\n","category":"type"},{"location":"api/#Metatheory.Rules.UnequalRule","page":"API Documentation","title":"Metatheory.Rules.UnequalRule","text":"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. \n\n!a ≠ a\n\n\n\n\n\n","category":"type"},{"location":"api/","page":"API Documentation","title":"API Documentation","text":"","category":"page"},{"location":"api/#Rules-2","page":"API Documentation","title":"Rules","text":"","category":"section"},{"location":"api/","page":"API Documentation","title":"API Documentation","text":"Modules = [Metatheory.Rules]","category":"page"},{"location":"api/","page":"API Documentation","title":"API Documentation","text":"","category":"page"},{"location":"api/#Rewriters","page":"API Documentation","title":"Rewriters","text":"","category":"section"},{"location":"api/","page":"API Documentation","title":"API Documentation","text":"Modules = [Metatheory.Rewriters]","category":"page"},{"location":"api/#Metatheory.Rewriters","page":"API Documentation","title":"Metatheory.Rewriters","text":"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.\n\nThe Rewriters module contains some types which create and transform rewriters.\n\nEmpty() is a rewriter which always returns nothing\nChain(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.\nRestartedChain(itr) like Chain(itr) but restarts from the first rewriter once on the first successful application of one of the chained rewriters.\nIfElse(cond, rw1, rw2) runs the cond function on the input, applies rw1 if cond returns true, rw2 if it retuns false\nIf(cond, rw) is the same as IfElse(cond, rw, Empty())\nPrewalk(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.\nPostwalk(rw; threaded=false, thread_cutoff=100) similarly does post-order traversal.\nFixpoint(rw) returns a rewriter which applies rw repeatedly until there are no changes to be made.\nFixpointNoCycle behaves like Fixpoint but instead it applies rw repeatedly only while it is returning new results.\nPassThrough(rw) returns a rewriter which if rw(x) returns nothing will instead return x otherwise will return rw(x).\n\n\n\nImports\n\nBase\nBase.Threads\nCore\nTermInterface\n\n\n\n\n\n","category":"module"},{"location":"api/#Metatheory.Rewriters.FixpointNoCycle","page":"API Documentation","title":"Metatheory.Rewriters.FixpointNoCycle","text":"FixpointNoCycle(rw)\n\nFixpointNoCycle 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. \n\n\n\n\n\n","category":"type"},{"location":"api/","page":"API Documentation","title":"API Documentation","text":"","category":"page"},{"location":"api/#EGraphs","page":"API Documentation","title":"EGraphs","text":"","category":"section"},{"location":"api/","page":"API Documentation","title":"API Documentation","text":"Modules = [Metatheory.EGraphs]","category":"page"},{"location":"api/#Metatheory.EGraphs.EGraph","page":"API Documentation","title":"Metatheory.EGraphs.EGraph","text":"mutable struct EGraph\n\nA concrete type representing an [EGraph]. See the egg paper for implementation details.\n\n\n\nFields\n\nuf::IntDisjointSet\nstores the equality relations over e-class ids\nclasses::Dict{Int64, EClass}\nmap from eclass id to eclasses\nmemo::Dict{AbstractENode, Int64}\nhashcons\ndirty::Vector{Int64}\nworklist for ammortized upwards merging\nroot::Int64\nanalyses::Dict{Union{Function, Symbol}, Union{Function, Symbol}}\nA vector of analyses associated to the EGraph\nsymcache::Dict{Any, Vector{Int64}}\na cache mapping function symbols to e-classes that contain e-nodes with that function symbol.\ndefault_termtype::Type\ntermtypes::Dict{Tuple{Any, Int64}, Type}\nnumclasses::Int64\nnumnodes::Int64\nneedslock::Bool\nIf we use global buffers we may need to lock. Defaults to true.\nbuffer::Vector{Base.ImmutableDict{Int64, Tuple{Int64, Int64}}}\nBuffer for e-matching which defaults to a global. Use a local buffer for generated functions.\nmerges_buffer::Vector{Tuple{Int64, Int64}}\nBuffer for rule application which defaults to a global. Use a local buffer for generated functions.\nlock::ReentrantLock\n\n\n\n\n\n","category":"type"},{"location":"api/#Metatheory.EGraphs.EGraph-Tuple{}","page":"API Documentation","title":"Metatheory.EGraphs.EGraph","text":"EGraph(expr)\n\nConstruct an EGraph from a starting symbolic expression expr.\n\n\n\nSignatures\n\nEGraph() -> EGraph\n\n\n\n\nMethods\n\nEGraph()\n\ndefined at /home/runner/work/Metatheory.jl/Metatheory.jl/src/EGraphs/egraph.jl:212.\n\n\n\n\n\n","category":"method"},{"location":"api/#Metatheory.EGraphs.EqualityGoal","page":"API Documentation","title":"Metatheory.EGraphs.EqualityGoal","text":"struct EqualityGoal <: SaturationGoal\n\nThis goal is reached when the exprs list of expressions are in the same equivalence class.\n\n\n\nFields\n\nexprs::Vector{Any}\nids::Vector{Int64}\n\n\n\n\n\n","category":"type"},{"location":"api/#Metatheory.EGraphs.FunctionGoal","page":"API Documentation","title":"Metatheory.EGraphs.FunctionGoal","text":"struct FunctionGoal <: SaturationGoal\n\nBoolean valued function as an arbitrary saturation goal. User supplied function must take an EGraph as the only parameter.\n\n\n\nFields\n\nfun::Function\n\n\n\n\n\n","category":"type"},{"location":"api/#Metatheory.EGraphs.SaturationParams","page":"API Documentation","title":"Metatheory.EGraphs.SaturationParams","text":"mutable struct SaturationParams\n\nConfigurable Parameters for the equality saturation process.\n\n\n\nFields\n\ntimeout::Int64\ntimelimit::UInt64\nTimeout in nanoseconds\neclasslimit::Int64\nMaximum number of eclasses allowed\nenodelimit::Int64\ngoal::Union{Nothing, SaturationGoal}\nstopwhen::Function\nscheduler::Type{<:Metatheory.EGraphs.Schedulers.AbstractScheduler}\nschedulerparams::Tuple\nthreaded::Bool\ntimer::Bool\n\n\n\n\n\n","category":"type"},{"location":"api/#Base.merge!-Tuple{EGraph, Int64, Int64}","page":"API Documentation","title":"Base.merge!","text":"Given an EGraph and two e-class ids, set the two e-classes as equal.\n\n\n\nSignatures\n\nmerge!(g::EGraph, a::Int64, b::Int64) -> Int64\n\n\n\n\nMethods\n\nmerge!(g, a, b)\n\ndefined at /home/runner/work/Metatheory.jl/Metatheory.jl/src/EGraphs/egraph.jl:391.\n\n\n\n\n\n","category":"method"},{"location":"api/#Metatheory.EGraphs.add!-Tuple{EGraph, AbstractENode}","page":"API Documentation","title":"Metatheory.EGraphs.add!","text":"Inserts an e-node in an EGraph\n\n\n\nSignatures\n\nadd!(g::EGraph, n::AbstractENode) -> Int64\n\n\n\n\nMethods\n\nadd!(g, n)\n\ndefined at /home/runner/work/Metatheory.jl/Metatheory.jl/src/EGraphs/egraph.jl:315.\n\n\n\n\n\n","category":"method"},{"location":"api/#Metatheory.EGraphs.addexpr!-Tuple{EGraph, Any}","page":"API Documentation","title":"Metatheory.EGraphs.addexpr!","text":"Recursively traverse an type satisfying the TermInterface and insert terms into an EGraph. If e has no children (has an arity of 0) then directly insert the literal into the EGraph.\n\n\n\nSignatures\n\naddexpr!(g::EGraph, se) -> Int64\n\n\n\n\nMethods\n\naddexpr!(g, se)\n\ndefined at /home/runner/work/Metatheory.jl/Metatheory.jl/src/EGraphs/egraph.jl:365.\n\naddexpr!(g, ec)\n\ndefined at /home/runner/work/Metatheory.jl/Metatheory.jl/src/EGraphs/egraph.jl:382.\n\n\n\n\n\n","category":"method"},{"location":"api/#Metatheory.EGraphs.analyze!-Tuple{EGraph, Any, Vector{Int64}}","page":"API Documentation","title":"Metatheory.EGraphs.analyze!","text":"analyze!(egraph, analysis_name, [ECLASS_IDS])\n\nGiven 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.\n\n\n\nSignatures\n\nanalyze!(g::EGraph, analysis_ref, ids::Vector{Int64}) -> Bool\n\n\n\n\nMethods\n\nanalyze!(g, analysis_ref, ids)\n\ndefined at /home/runner/work/Metatheory.jl/Metatheory.jl/src/EGraphs/analysis.jl:61.\n\n\n\n\n\n","category":"method"},{"location":"api/#Metatheory.EGraphs.astsize-Tuple{ENodeTerm, EGraph}","page":"API Documentation","title":"Metatheory.EGraphs.astsize","text":"A basic cost function, where the computed cost is the size (number of children) of the current expression.\n\n\n\nSignatures\n\nastsize(n::ENodeTerm, g::EGraph) -> Any\n\n\n\n\nMethods\n\nastsize(n, g)\n\ndefined at /home/runner/work/Metatheory.jl/Metatheory.jl/src/EGraphs/analysis.jl:98.\n\n\n\n\n\n","category":"method"},{"location":"api/#Metatheory.EGraphs.astsize_inv-Tuple{ENodeTerm, EGraph}","page":"API Documentation","title":"Metatheory.EGraphs.astsize_inv","text":"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\n\n\n\nSignatures\n\nastsize_inv(n::ENodeTerm, g::EGraph) -> Any\n\n\n\n\nMethods\n\nastsize_inv(n, g)\n\ndefined at /home/runner/work/Metatheory.jl/Metatheory.jl/src/EGraphs/analysis.jl:115.\n\n\n\n\n\n","category":"method"},{"location":"api/#Metatheory.EGraphs.egraph_reconstruct_expression-Tuple{Type{Expr}, Any, Any}","page":"API Documentation","title":"Metatheory.EGraphs.egraph_reconstruct_expression","text":"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.\n\n\n\nSignatures\n\negraph_reconstruct_expression(T::Type{Expr}, op, args) -> Expr\n\n\n\n\nMethods\n\negraph_reconstruct_expression(T, op, args)\n\ndefined at /home/runner/work/Metatheory.jl/Metatheory.jl/src/EGraphs/egraph.jl:534.\n\n\n\n\n\n","category":"method"},{"location":"api/#Metatheory.EGraphs.eqsat_search!-Tuple{EGraph, Vector{<:AbstractRule}, Metatheory.EGraphs.Schedulers.AbstractScheduler, Metatheory.EGraphs.SaturationReport}","page":"API Documentation","title":"Metatheory.EGraphs.eqsat_search!","text":"Returns an iterator of Matches.\n\n\n\nSignatures\n\neqsat_search!(g::EGraph, theory::Vector{<:AbstractRule}, scheduler::Metatheory.EGraphs.Schedulers.AbstractScheduler, report::Metatheory.EGraphs.SaturationReport) -> Int64\n\n\n\n\nMethods\n\neqsat_search!(g, theory, scheduler, report)\n\ndefined at /home/runner/work/Metatheory.jl/Metatheory.jl/src/EGraphs/saturation.jl:114.\n\n\n\n\n\n","category":"method"},{"location":"api/#Metatheory.EGraphs.eqsat_step!-Tuple{EGraph, Vector{<:AbstractRule}, Any, Metatheory.EGraphs.Schedulers.AbstractScheduler, SaturationParams, Any}","page":"API Documentation","title":"Metatheory.EGraphs.eqsat_step!","text":"Core algorithm of the library: the equality saturation step.\n\n\n\nSignatures\n\neqsat_step!(g::EGraph, theory::Vector{<:AbstractRule}, curr_iter, scheduler::Metatheory.EGraphs.Schedulers.AbstractScheduler, params::SaturationParams, report) -> Any\n\n\n\n\nMethods\n\neqsat_step!(g, theory, curr_iter, scheduler, params, report)\n\ndefined at /home/runner/work/Metatheory.jl/Metatheory.jl/src/EGraphs/saturation.jl:257.\n\n\n\n\n\n","category":"method"},{"location":"api/#Metatheory.EGraphs.extract!-Tuple{EGraph, Function}","page":"API Documentation","title":"Metatheory.EGraphs.extract!","text":"Given a cost function, extract the expression with the smallest computed cost from an EGraph\n\n\n\nSignatures\n\nextract!(g::EGraph, costfun::Function) -> Any\n\n\n\n\nMethods\n\nextract!(g, costfun)\n\ndefined at /home/runner/work/Metatheory.jl/Metatheory.jl/src/EGraphs/analysis.jl:163.\n\n\n\n\n\n","category":"method"},{"location":"api/#Metatheory.EGraphs.find-Tuple{EGraph, Int64}","page":"API Documentation","title":"Metatheory.EGraphs.find","text":"Returns the canonical e-class id for a given e-class.\n\n\n\nSignatures\n\nfind(g::EGraph, a::Int64) -> Int64\n\n\n\n\nMethods\n\nfind(g, a)\n\ndefined at /home/runner/work/Metatheory.jl/Metatheory.jl/src/EGraphs/egraph.jl:272.\n\n\n\n\n\n","category":"method"},{"location":"api/#Metatheory.EGraphs.instantiate_actual_param!-Tuple{Base.ImmutableDict{Int64, Tuple{Int64, Int64}}, EGraph, Any}","page":"API Documentation","title":"Metatheory.EGraphs.instantiate_actual_param!","text":"Instantiate argument for dynamic rule application in e-graph\n\n\n\nSignatures\n\ninstantiate_actual_param!(bindings::Base.ImmutableDict{Int64, Tuple{Int64, Int64}}, g::EGraph, i) -> Any\n\n\n\n\nMethods\n\ninstantiate_actual_param!(bindings, g, i)\n\ndefined at /home/runner/work/Metatheory.jl/Metatheory.jl/src/EGraphs/saturation.jl:194.\n\n\n\n\n\n","category":"method"},{"location":"api/#Metatheory.EGraphs.islazy-Union{Tuple{Val{analysis_name}}, Tuple{analysis_name}} where analysis_name","page":"API Documentation","title":"Metatheory.EGraphs.islazy","text":"islazy(::Val{analysis_name})\n\nShould 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. \n\n\n\nSignatures\n\n\n\nMethods\n\nislazy(_)\n\ndefined at /home/runner/work/Metatheory.jl/Metatheory.jl/src/EGraphs/analysis.jl:14.\n\nislazy(analysis_name)\n\ndefined at /home/runner/work/Metatheory.jl/Metatheory.jl/src/EGraphs/analysis.jl:15.\n\nislazy(_)\n\ndefined at /home/runner/work/Metatheory.jl/Metatheory.jl/src/EGraphs/analysis.jl:135.\n\n\n\n\n\n","category":"method"},{"location":"api/#Metatheory.EGraphs.join-Union{Tuple{analysis_name}, Tuple{Val{analysis_name}, Any, Any}} where analysis_name","page":"API Documentation","title":"Metatheory.EGraphs.join","text":"join(::Val{analysis_name}, a, b)\n\nJoins two analyses values into a single one, used by analyze! when two eclasses are being merged or the analysis is being constructed.\n\n\n\nSignatures\n\n\n\nMethods\n\njoin(analysis, a, b)\n\ndefined at /home/runner/work/Metatheory.jl/Metatheory.jl/src/EGraphs/analysis.jl:35.\n\n\n\n\n\n","category":"method"},{"location":"api/#Metatheory.EGraphs.make-Tuple{Function, EGraph, AbstractENode}","page":"API Documentation","title":"Metatheory.EGraphs.make","text":"When passing a function to analysis functions it is considered as a cost function\n\n\n\nSignatures\n\nmake(f::Function, g::EGraph, n::AbstractENode) -> Tuple{AbstractENode, Any}\n\n\n\n\nMethods\n\nmake(f, g, n)\n\ndefined at /home/runner/work/Metatheory.jl/Metatheory.jl/src/EGraphs/analysis.jl:131.\n\n\n\n\n\n","category":"method"},{"location":"api/#Metatheory.EGraphs.make-Union{Tuple{analysis_name}, Tuple{Val{analysis_name}, Any, Any}} where analysis_name","page":"API Documentation","title":"Metatheory.EGraphs.make","text":"make(::Val{analysis_name}, g, n)\n\nGiven an ENode n, make should return the corresponding analysis value. \n\n\n\nSignatures\n\n\n\nMethods\n\nmake(_, g, n)\n\ndefined at /home/runner/work/Metatheory.jl/Metatheory.jl/src/EGraphs/analysis.jl:44.\n\n\n\n\n\n","category":"method"},{"location":"api/#Metatheory.EGraphs.modify!-Union{Tuple{analysis_name}, Tuple{Val{analysis_name}, Any, Any}} where analysis_name","page":"API Documentation","title":"Metatheory.EGraphs.modify!","text":"modify!(::Val{analysis_name}, g, id)\n\nThe modify! function for EGraph Analysis can optionally modify the eclass g[id] after it has been analyzed, typically by adding an ENode. It should be idempotent if no other changes occur to the EClass. (See the egg paper).\n\n\n\nSignatures\n\nmodify!(_::Val{analysis_name}, g, id)\n\n\n\n\nMethods\n\nmodify!(_, g, id)\n\ndefined at /home/runner/work/Metatheory.jl/Metatheory.jl/src/EGraphs/analysis.jl:25.\n\n\n\n\n\n","category":"method"},{"location":"api/#Metatheory.EGraphs.preprocess-Tuple{Expr}","page":"API Documentation","title":"Metatheory.EGraphs.preprocess","text":"Extend this function on your types to do preliminary preprocessing of a symbolic term before adding it to an EGraph. Most common preprocessing techniques are binarization of n-ary terms and metadata stripping.\n\n\n\nSignatures\n\npreprocess(e::Expr) -> Any\n\n\n\n\nMethods\n\npreprocess(e)\n\ndefined at /home/runner/work/Metatheory.jl/Metatheory.jl/src/EGraphs/egraph.jl:355.\n\n\n\n\n\n","category":"method"},{"location":"api/#Metatheory.EGraphs.reachable-Tuple{EGraph, Int64}","page":"API Documentation","title":"Metatheory.EGraphs.reachable","text":"Recursive function that traverses an EGraph and returns a vector of all reachable e-classes from a given e-class id.\n\n\n\nSignatures\n\nreachable(g::EGraph, id::Int64) -> Vector{Int64}\n\n\n\n\nMethods\n\nreachable(g, id)\n\ndefined at /home/runner/work/Metatheory.jl/Metatheory.jl/src/EGraphs/egraph.jl:501.\n\n\n\n\n\n","category":"method"},{"location":"api/#Metatheory.EGraphs.rebuild!-Tuple{EGraph}","page":"API Documentation","title":"Metatheory.EGraphs.rebuild!","text":"This function restores invariants and executes upwards merging in an EGraph. See the egg paper for more details.\n\n\n\nSignatures\n\nrebuild!(g::EGraph) -> Bool\n\n\n\n\nMethods\n\nrebuild!(g)\n\ndefined at /home/runner/work/Metatheory.jl/Metatheory.jl/src/EGraphs/egraph.jl:426.\n\n\n\n\n\n","category":"method"},{"location":"api/#Metatheory.EGraphs.saturate!","page":"API Documentation","title":"Metatheory.EGraphs.saturate!","text":"Given an EGraph and a collection of rewrite rules, execute the equality saturation algorithm.\n\n\n\nSignatures\n\nsaturate!(g::EGraph, theory::Vector{<:AbstractRule}) -> Metatheory.EGraphs.SaturationReport\nsaturate!(g::EGraph, theory::Vector{<:AbstractRule}, params) -> Metatheory.EGraphs.SaturationReport\n\n\n\n\nMethods\n\nsaturate!(g, theory)\nsaturate!(g, theory, params)\n\ndefined at /home/runner/work/Metatheory.jl/Metatheory.jl/src/EGraphs/saturation.jl:286.\n\n\n\n\n\n","category":"function"},{"location":"api/","page":"API Documentation","title":"API Documentation","text":"","category":"page"},{"location":"api/#EGraph-Schedulers","page":"API Documentation","title":"EGraph Schedulers","text":"","category":"section"},{"location":"api/","page":"API Documentation","title":"API Documentation","text":"Modules = [Metatheory.EGraphs.Schedulers]","category":"page"},{"location":"api/#Metatheory.EGraphs.Schedulers.AbstractScheduler","page":"API Documentation","title":"Metatheory.EGraphs.Schedulers.AbstractScheduler","text":"abstract type AbstractScheduler\n\nRepresents a rule scheduler for the equality saturation process\n\n\n\nFields\n\n\n\n\n\n","category":"type"},{"location":"api/#Metatheory.EGraphs.Schedulers.BackoffScheduler","page":"API Documentation","title":"Metatheory.EGraphs.Schedulers.BackoffScheduler","text":"mutable struct BackoffScheduler <: Metatheory.EGraphs.Schedulers.AbstractScheduler\n\nA 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.\n\nThis seems effective at preventing explosive rules like associativity from taking an unfair amount of resources.\n\n\n\nFields\n\ndata::IdDict{AbstractRule, Metatheory.EGraphs.Schedulers.BackoffSchedulerEntry}\nG::EGraph\ntheory::Vector{<:AbstractRule}\ncurr_iter::Int64\n\n\n\n\n\n","category":"type"},{"location":"api/#Metatheory.EGraphs.Schedulers.ScoredScheduler","page":"API Documentation","title":"Metatheory.EGraphs.Schedulers.ScoredScheduler","text":"mutable struct ScoredScheduler <: Metatheory.EGraphs.Schedulers.AbstractScheduler\n\nA 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.\n\nThis seems effective at preventing explosive rules like associativity from taking an unfair amount of resources.\n\n\n\nFields\n\ndata::IdDict{AbstractRule, Metatheory.EGraphs.Schedulers.ScoredSchedulerEntry}\nG::EGraph\ntheory::Vector{<:AbstractRule}\ncurr_iter::Int64\n\n\n\n\n\n","category":"type"},{"location":"api/#Metatheory.EGraphs.Schedulers.SimpleScheduler","page":"API Documentation","title":"Metatheory.EGraphs.Schedulers.SimpleScheduler","text":"struct SimpleScheduler <: Metatheory.EGraphs.Schedulers.AbstractScheduler\n\nA simple Rewrite Scheduler that applies every rule every time\n\n\n\nFields\n\n\n\n\n\n","category":"type"},{"location":"api/#Metatheory.EGraphs.Schedulers.cansaturate","page":"API Documentation","title":"Metatheory.EGraphs.Schedulers.cansaturate","text":"Should return true if the e-graph can be said to be saturated\n\ncansaturate(s::AbstractScheduler)\n\n\n\nSignatures\n\n\n\nMethods\n\ncansaturate(s)\n\ndefined at /home/runner/work/Metatheory.jl/Metatheory.jl/src/EGraphs/Schedulers.jl:63.\n\ncansaturate(s)\n\ndefined at /home/runner/work/Metatheory.jl/Metatheory.jl/src/EGraphs/Schedulers.jl:120.\n\ncansaturate(s)\n\ndefined at /home/runner/work/Metatheory.jl/Metatheory.jl/src/EGraphs/Schedulers.jl:231.\n\n\n\n\n\n","category":"function"},{"location":"api/#Metatheory.EGraphs.Schedulers.cansearch","page":"API Documentation","title":"Metatheory.EGraphs.Schedulers.cansearch","text":"Should return false if the rule r should be skipped\n\ncansearch(s::AbstractScheduler, r::Rule)\n\n\n\nSignatures\n\n\n\nMethods\n\ncansearch(s, r)\n\ndefined at /home/runner/work/Metatheory.jl/Metatheory.jl/src/EGraphs/Schedulers.jl:64.\n\ncansearch(s, r)\n\ndefined at /home/runner/work/Metatheory.jl/Metatheory.jl/src/EGraphs/Schedulers.jl:100.\n\ncansearch(s, r)\n\ndefined at /home/runner/work/Metatheory.jl/Metatheory.jl/src/EGraphs/Schedulers.jl:169.\n\n\n\n\n\n","category":"function"},{"location":"api/#Metatheory.EGraphs.Schedulers.inform!","page":"API Documentation","title":"Metatheory.EGraphs.Schedulers.inform!","text":"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. \n\ninform!(s::AbstractScheduler, r::AbstractRule, n_matches)\n\n\n\nSignatures\n\n\n\nMethods\n\ninform!(s, r, n_matches)\n\ndefined at /home/runner/work/Metatheory.jl/Metatheory.jl/src/EGraphs/Schedulers.jl:68.\n\ninform!(s, rule, n_matches)\n\ndefined at /home/runner/work/Metatheory.jl/Metatheory.jl/src/EGraphs/Schedulers.jl:123.\n\ninform!(s, rule, n_matches)\n\ndefined at /home/runner/work/Metatheory.jl/Metatheory.jl/src/EGraphs/Schedulers.jl:234.\n\n\n\n\n\n","category":"function"},{"location":"rewrite/#Classical-Term-Rewriting","page":"Classical Term Rewriting","title":"Classical Term Rewriting","text":"","category":"section"},{"location":"rewrite/#Rule-based-rewriting","page":"Classical Term Rewriting","title":"Rule-based rewriting","text":"","category":"section"},{"location":"rewrite/","page":"Classical Term Rewriting","title":"Classical Term Rewriting","text":"Rewrite rules match and transform an expression. A rule is written using either the @rule or @theory macros. It creates a callable Rule object.","category":"page"},{"location":"rewrite/#Basics-of-rule-based-term-rewriting-in-Metatheory.jl","page":"Classical Term Rewriting","title":"Basics of rule-based term rewriting in Metatheory.jl","text":"","category":"section"},{"location":"rewrite/","page":"Classical Term Rewriting","title":"Classical Term Rewriting","text":"NOTE: for a real world use case using mathematical constructs, please refer to SymbolicUtils.jl. SU provides optimized types for mathematical expressions, code generation and a polished set of rules for simplification.","category":"page"},{"location":"rewrite/","page":"Classical Term Rewriting","title":"Classical Term Rewriting","text":"Here is a simple symbolic rewrite rule, that uses formula for the double angle of the sine function:","category":"page"},{"location":"rewrite/","page":"Classical Term Rewriting","title":"Classical Term Rewriting","text":"using Metatheory\n\nr1 = @rule sin(2(~x)) --> 2sin(~x)*cos(~x)\n\nexpr = :(sin(2z))\nr1(expr)","category":"page"},{"location":"rewrite/","page":"Classical Term Rewriting","title":"Classical Term Rewriting","text":"The @rule macro takes a pair of patterns – the matcher and the consequent (@rule matcher OPERATOR consequent). If an expression matches the matcher pattern, it is rewritten to the consequent pattern. @rule returns a callable object that applies the rule to an expression. There are different kinds of rule in Metatheory.jl:","category":"page"},{"location":"rewrite/","page":"Classical Term Rewriting","title":"Classical Term Rewriting","text":"Rule operators:","category":"page"},{"location":"rewrite/","page":"Classical Term Rewriting","title":"Classical Term Rewriting","text":"LHS => RHS: create a DynamicRule. The RHS is evaluated on rewrite.\nLHS --> RHS: create a RewriteRule. The RHS is not evaluated but symbolically substituted on rewrite.\nLHS == 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.\nLHS ≠ 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.","category":"page"},{"location":"rewrite/","page":"Classical Term Rewriting","title":"Classical Term Rewriting","text":"You can use dynamic rules, defined with the => operator, to dynamically compute values in the right hand of expressions. This is the default behaviour of rules in SymbolicUtils.jl 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.","category":"page"},{"location":"rewrite/","page":"Classical Term Rewriting","title":"Classical Term Rewriting","text":"~x in the example is what is a slot variable (or pattern variable) named x. In a matcher pattern, slot variables are placeholders that match exactly one expression. When used on the consequent side, they stand in for the matched expression. If a slot variable appears twice in a matcher pattern, in classical rewriting all corresponding matches must be equal (as tested by Base.isequal function). Hence this rule says: if you see something added to itself, make it twice of that thing, and works as such.","category":"page"},{"location":"rewrite/","page":"Classical Term Rewriting","title":"Classical Term Rewriting","text":"If you try to apply this rule to an expression with triple angle, it will return nothing – this is the way a rule signifies failure to match.","category":"page"},{"location":"rewrite/","page":"Classical Term Rewriting","title":"Classical Term Rewriting","text":"r1(:(sin(3z))) === nothing","category":"page"},{"location":"rewrite/","page":"Classical Term Rewriting","title":"Classical Term Rewriting","text":"Slot variable (matcher) is not necessary a single variable","category":"page"},{"location":"rewrite/","page":"Classical Term Rewriting","title":"Classical Term Rewriting","text":"r1(:(sin(2*(w-z))))","category":"page"},{"location":"rewrite/","page":"Classical Term Rewriting","title":"Classical Term Rewriting","text":"but it must be a single expression","category":"page"},{"location":"rewrite/","page":"Classical Term Rewriting","title":"Classical Term Rewriting","text":"r1(:(sin(2*(w+z)*(α+β)))) === nothing","category":"page"},{"location":"rewrite/","page":"Classical Term Rewriting","title":"Classical Term Rewriting","text":"Rules are of course not limited to single slot variable","category":"page"},{"location":"rewrite/","page":"Classical Term Rewriting","title":"Classical Term Rewriting","text":"r2 = @rule sin(~x + ~y) --> sin(~x)*cos(~y) + cos(~x)*sin(~y);\n\nr2(:(sin(α+β)))","category":"page"},{"location":"rewrite/","page":"Classical Term Rewriting","title":"Classical Term Rewriting","text":"If you want to match a variable number of subexpressions at once, you will need a segment variable. ~xs... in the following example is a segment variable:","category":"page"},{"location":"rewrite/","page":"Classical Term Rewriting","title":"Classical Term Rewriting","text":"@rule(+(~xs...) => xs)(:(x + y + z))","category":"page"},{"location":"rewrite/","page":"Classical Term Rewriting","title":"Classical Term Rewriting","text":"~xs is a vector of subexpressions matched. You can use it to construct something more useful:","category":"page"},{"location":"rewrite/","page":"Classical Term Rewriting","title":"Classical Term Rewriting","text":"r3 = @rule *(~ys...)^~x => :((*)($(map(y-> :($y^$x), ys)...)));\n\nr3(:((w*w*α*β)^2))","category":"page"},{"location":"rewrite/#Predicates-for-matching","page":"Classical Term Rewriting","title":"Predicates for matching","text":"","category":"section"},{"location":"rewrite/","page":"Classical Term Rewriting","title":"Classical Term Rewriting","text":"Matcher pattern may contain slot variables with attached predicates, written as ~x::p where p is either","category":"page"},{"location":"rewrite/","page":"Classical Term Rewriting","title":"Classical Term Rewriting","text":"A function that takes a matched expression and returns a boolean value. Such a slot will be considered a match only if p returns true.\nA Julia type. Will be considered a match if and only if the value matching against x has a type that is a subtype of p (typeof(x) <: p)","category":"page"},{"location":"rewrite/","page":"Classical Term Rewriting","title":"Classical Term Rewriting","text":"Similarly ~x::g... is a way of attaching 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. If the same slot or segment variable appears twice in the matcher pattern, then at most one of the occurrence should have a predicate.","category":"page"},{"location":"rewrite/","page":"Classical Term Rewriting","title":"Classical Term Rewriting","text":"For example,","category":"page"},{"location":"rewrite/","page":"Classical Term Rewriting","title":"Classical Term Rewriting","text":"r = @rule +(~x, ~y::(ys->iseven(length(ys)))...) => \"odd terms\";\n\n@show r(:(a + b + c + d))\n@show r(:(b + c + d))\n@show r(:(b + c + b))\n@show r(:(a + b))","category":"page"},{"location":"rewrite/#Declaring-Slots","page":"Classical Term Rewriting","title":"Declaring Slots","text":"","category":"section"},{"location":"rewrite/","page":"Classical Term Rewriting","title":"Classical Term Rewriting","text":"Slot variables can be declared without the ~ using the @slots macro","category":"page"},{"location":"rewrite/","page":"Classical Term Rewriting","title":"Classical Term Rewriting","text":"@slots x y @rule sin(x + y) => sin(x)*cos(y) + cos(x)*sin(y);","category":"page"},{"location":"rewrite/","page":"Classical Term Rewriting","title":"Classical Term Rewriting","text":"This works for segments as well:","category":"page"},{"location":"rewrite/","page":"Classical Term Rewriting","title":"Classical Term Rewriting","text":"@slots xs @rule(+(~xs...) => xs);","category":"page"},{"location":"rewrite/","page":"Classical Term Rewriting","title":"Classical Term Rewriting","text":"The @slots macro is superfluous for the @rule, @capture and @theory macros. Slot variables may be declared directly as the first arguments to those macros:","category":"page"},{"location":"rewrite/","page":"Classical Term Rewriting","title":"Classical Term Rewriting","text":"@rule x y sin(x + y) => sin(x)*cos(y) + cos(x)*sin(y);","category":"page"},{"location":"rewrite/#Theories","page":"Classical Term Rewriting","title":"Theories","text":"","category":"section"},{"location":"rewrite/","page":"Classical Term Rewriting","title":"Classical Term Rewriting","text":"In almost all use cases, it is practical to define many rules grouped together. A set of rewrite rules and equalities is called a theory, and can be defined with the @theory macro. This macro is just syntax sugar to define vectors of rules in a nice and readable way. ","category":"page"},{"location":"rewrite/","page":"Classical Term Rewriting","title":"Classical Term Rewriting","text":"t = @theory x y z begin \n x * (y + z) --> (x * y) + (x * z)\n x + y == (y + x)\n #...\nend;","category":"page"},{"location":"rewrite/","page":"Classical Term Rewriting","title":"Classical Term Rewriting","text":"Is the same thing as writing","category":"page"},{"location":"rewrite/","page":"Classical Term Rewriting","title":"Classical Term Rewriting","text":"v = [\n @rule x y z x * (y + z) --> (x * y) + (x * z)\n @rule x y x + y == (y + x)\n #...\n];","category":"page"},{"location":"rewrite/","page":"Classical Term Rewriting","title":"Classical Term Rewriting","text":"Theories are just collections 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.","category":"page"},{"location":"rewrite/","page":"Classical Term Rewriting","title":"Classical Term Rewriting","text":"using Metatheory\nusing Metatheory.Library\n\ncomm_monoid = @commutative_monoid (*) 1\ncomm_group = @theory a b c begin\n a + 0 --> a\n a + b --> b + a\n a + inv(a) --> 0 # inverse\n a + (b + c) --> (a + b) + c\nend\ndistrib = @theory a b c begin\n a * (b + c) => (a * b) + (a * c)\nend\nt = comm_monoid ∪ comm_group ∪ distrib","category":"page"},{"location":"rewrite/#Composing-rewriters","page":"Classical Term Rewriting","title":"Composing rewriters","text":"","category":"section"},{"location":"rewrite/","page":"Classical Term Rewriting","title":"Classical Term Rewriting","text":"Rules may be chained together into more sophisticated rewriters to avoid manual application of the rules. A rewriter is any callable object 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 Rules we created above are rewriters.","category":"page"},{"location":"rewrite/","page":"Classical Term Rewriting","title":"Classical Term Rewriting","text":"The Metatheory.Rewriters module contains some types which create and transform rewriters.","category":"page"},{"location":"rewrite/","page":"Classical Term Rewriting","title":"Classical Term Rewriting","text":"Empty() is a rewriter which always returns nothing\nChain(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.\nRestartedChain(itr) like Chain(itr) but restarts from the first rewriter once on the first successful application of one of the chained rewriters.\nIfElse(cond, rw1, rw2) runs the cond function on the input, applies rw1 if cond returns true, rw2 if it returns false\nIf(cond, rw) is the same as IfElse(cond, rw, Empty())\nPrewalk(rw; threaded=false, thread_cutoff=100) returns a rewriter which does a pre-order (from top to bottom and from left to right) traversal of a given expression and applies the rewriter rw. threaded=true will use multi threading for traversal. 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. If you are applying multiple rules, then Chain already has the appropriate passthrough behavior. If you only want to apply one rule, then consider using PassThrough. thread_cutoff is the minimum number of nodes in a subtree which should be walked in a threaded spawn.\nPostwalk(rw; threaded=false, thread_cutoff=100) similarly does post-order (from left to right and from bottom to top) traversal.\nFixpoint(rw) returns a rewriter which applies rw repeatedly until there are no changes to be made.\nFixpointNoCycle behaves like Fixpoint but instead it applies rw repeatedly only while it is returning new results.\nPassThrough(rw) returns a rewriter which if rw(x) returns nothing will instead return x otherwise will return rw(x).","category":"page"},{"location":"rewrite/#Chaining-rewriters","page":"Classical Term Rewriting","title":"Chaining rewriters","text":"","category":"section"},{"location":"rewrite/","page":"Classical Term Rewriting","title":"Classical Term Rewriting","text":"Several rules may be chained to give chain of rules. Chain is an array of rules which are subsequently applied to the expression. Important feature of Chain is that it returns the expression instead of nothing if it doesn't change the expression It is important to notice, that chain is ordered, so if rules are in different order it wouldn't work the same as in earlier example","category":"page"},{"location":"rewrite/","page":"Classical Term Rewriting","title":"Classical Term Rewriting","text":"One way to circumvent the problem of order of applying rules in chain is to use RestartedChain, it restarts the chain after each successful application of a rule, so after a rule is hit it (re)starts again and it can apply all the other rules to the resulting expression. You can also use Fixpoint to apply the rules until there are no changes.","category":"page"},{"location":"tutorials/fibonacci/","page":"Benchmarking Fibonacci. E-Graphs memoize computation.","title":"Benchmarking Fibonacci. E-Graphs memoize computation.","text":"EditURL = \"https://github.com/JuliaSymbolics/Metatheory.jl/blob/master/test/tutorials/fibonacci.jl\"","category":"page"},{"location":"tutorials/fibonacci/#Benchmarking-Fibonacci.-E-Graphs-memoize-computation.","page":"Benchmarking Fibonacci. E-Graphs memoize computation.","title":"Benchmarking Fibonacci. E-Graphs memoize computation.","text":"","category":"section"},{"location":"tutorials/fibonacci/","page":"Benchmarking Fibonacci. E-Graphs memoize computation.","title":"Benchmarking Fibonacci. E-Graphs memoize computation.","text":"using Metatheory\nusing Test\n\nfunction fib end\n\nfibo = @theory x y n begin\n x::Int + y::Int => x + y\n fib(n::Int) => (n < 2 ? n : :(fib($(n - 1)) + fib($(n - 2))))\nend\n\nparams = SaturationParams(timeout = 60)","category":"page"},{"location":"tutorials/fibonacci/","page":"Benchmarking Fibonacci. E-Graphs memoize computation.","title":"Benchmarking Fibonacci. E-Graphs memoize computation.","text":"We run the saturation twice to see a result that does not include compilation time.","category":"page"},{"location":"tutorials/fibonacci/","page":"Benchmarking Fibonacci. E-Graphs memoize computation.","title":"Benchmarking Fibonacci. E-Graphs memoize computation.","text":"g = EGraph(:(fib(10)))\nsaturate!(g, fibo, params)","category":"page"},{"location":"tutorials/fibonacci/","page":"Benchmarking Fibonacci. E-Graphs memoize computation.","title":"Benchmarking Fibonacci. E-Graphs memoize computation.","text":"That's fast!","category":"page"},{"location":"tutorials/fibonacci/","page":"Benchmarking Fibonacci. E-Graphs memoize computation.","title":"Benchmarking Fibonacci. E-Graphs memoize computation.","text":"z = EGraph(:(fib(10)))\nsaturate!(z, fibo, params)","category":"page"},{"location":"tutorials/fibonacci/","page":"Benchmarking Fibonacci. E-Graphs memoize computation.","title":"Benchmarking Fibonacci. E-Graphs memoize computation.","text":"We can test that the result is correct.","category":"page"},{"location":"tutorials/fibonacci/","page":"Benchmarking Fibonacci. E-Graphs memoize computation.","title":"Benchmarking Fibonacci. E-Graphs memoize computation.","text":"@testset \"Fibonacci\" begin\n @test 55 == extract!(g, astsize)\nend","category":"page"},{"location":"tutorials/fibonacci/","page":"Benchmarking Fibonacci. E-Graphs memoize computation.","title":"Benchmarking Fibonacci. E-Graphs memoize computation.","text":"","category":"page"},{"location":"tutorials/fibonacci/","page":"Benchmarking Fibonacci. E-Graphs memoize computation.","title":"Benchmarking Fibonacci. E-Graphs memoize computation.","text":"This page was generated using Literate.jl.","category":"page"},{"location":"egraphs/#EGraphs-and-Equality-Saturation","page":"EGraphs and Equality Saturation","title":"EGraphs and Equality Saturation","text":"","category":"section"},{"location":"egraphs/","page":"EGraphs and Equality Saturation","title":"EGraphs and Equality Saturation","text":"An EGraph is an efficient data structure for representing congruence relations. EGraphs are data structures originating from theorem provers. Several projects have very recently repurposed EGraphs to implement state-of-the-art, rewrite-driven compiler optimizations and program synthesizers using a technique known as equality saturation. Metatheory.jl provides a general purpose, customizable implementation of EGraphs and equality saturation, inspired from the egg library for Rust. You can read more about the design of the EGraph data structure and equality saturation algorithm in the egg paper.","category":"page"},{"location":"egraphs/","page":"EGraphs and Equality Saturation","title":"EGraphs and Equality Saturation","text":"Let's load Metatheory and the rule library","category":"page"},{"location":"egraphs/","page":"EGraphs and Equality Saturation","title":"EGraphs and Equality Saturation","text":"using Metatheory\nusing Metatheory.Library","category":"page"},{"location":"egraphs/","page":"EGraphs and Equality Saturation","title":"EGraphs and Equality Saturation","text":"DocTestSetup = quote \n using Metatheory\n using Metatheory.Library\nend","category":"page"},{"location":"egraphs/#What-can-I-do-with-EGraphs-in-Metatheory.jl?","page":"EGraphs and Equality Saturation","title":"What can I do with EGraphs in Metatheory.jl?","text":"","category":"section"},{"location":"egraphs/","page":"EGraphs and Equality Saturation","title":"EGraphs and Equality Saturation","text":"In classical term rewriting, rewrites are typically destructive and forget the matched left-hand side. Therefore, rules are applied in an arbitrary or controlled order - this often results in local minima and looping. For decades, programmers and scientists using term rewriting systems have spent their time trying to find confluent and terminating systems of rules. This requires a lot of effort and time. When studying any computational, mathematical or scientific system governed by equational rules, about non obviously oriented equations, such as (a + b) + c = a + (b + c )?","category":"page"},{"location":"egraphs/","page":"EGraphs and Equality Saturation","title":"EGraphs and Equality Saturation","text":"E-Graphs come to our help. EGraphs are bipartite graphs of ENodes and EClasses: a data structure for efficiently represent and rewrite on many equivalent expressions at the same time. A sort of fast data structure for sets of trees. Subtrees and parents are shared if possible. This makes EGraphs similar to DAGs. Most importantly, with EGraph rewriting you can use bidirectional rewrite rules, such as equalities without worrying about the ordering and confluence of your rewrite system! Therefore, rule application in EGraphs is non-destructive - everything is copied! This allows users to run non-deterministic rewrite systems. Many rules can match at the same time and the previous state of expressions will not be lost.","category":"page"},{"location":"egraphs/","page":"EGraphs and Equality Saturation","title":"EGraphs and Equality Saturation","text":"The EGraph backend for Metatheory.jl allows you to create an EGraph from a starting expression, to add more expressions to the EGraph with addexpr!, and then to effectively fill the EGraph with all possible equivalent expressions resulting from applying rewrite rules from a theory, by using the saturate! function. You can then easily extract expressions from an e-graph by calling extract! with a cost function.","category":"page"},{"location":"egraphs/","page":"EGraphs and Equality Saturation","title":"EGraphs and Equality Saturation","text":"A killer feature of egg and Metatheory.jl are EGraph Analyses. They allow you to annotate expressions and equivalence classes in an EGraph with values from a semilattice domain, and then to:","category":"page"},{"location":"egraphs/","page":"EGraphs and Equality Saturation","title":"EGraphs and Equality Saturation","text":"Automatically extract optimal expressions from an EGraph deciding from analysis data.\nHave conditional rules that are executed if some criteria is met on analysis data\nHave dynamic rules that compute the right hand side based on analysis data.","category":"page"},{"location":"egraphs/#Library","page":"EGraphs and Equality Saturation","title":"Library","text":"","category":"section"},{"location":"egraphs/","page":"EGraphs and Equality Saturation","title":"EGraphs and Equality Saturation","text":"The Metatheory.Library module contains utility functions and macros for creating rules and theories from commonly used algebraic structures and properties, to be used with the e-graph backend.","category":"page"},{"location":"egraphs/","page":"EGraphs and Equality Saturation","title":"EGraphs and Equality Saturation","text":"comm_monoid = @commutative_monoid (*) 1\n\n# output\n\n4-element Vector{RewriteRule}:\n ~a * ~b --> ~b * ~a\n (~a * ~b) * ~c --> ~a * (~b * ~c)\n ~a * (~b * ~c) --> (~a * ~b) * ~c\n 1 * ~a --> ~a\n","category":"page"},{"location":"egraphs/#Theories-and-Algebraic-Structures","page":"EGraphs and Equality Saturation","title":"Theories and Algebraic Structures","text":"","category":"section"},{"location":"egraphs/","page":"EGraphs and Equality Saturation","title":"EGraphs and Equality Saturation","text":"The e-graphs backend can directly handle associativity, equalities commutativity and distributivity, rules that are otherwise known of causing loops and require extensive user reasoning in classical rewriting.","category":"page"},{"location":"egraphs/","page":"EGraphs and Equality Saturation","title":"EGraphs and Equality Saturation","text":"t = @theory a b c begin\n a * b == b * a\n a * 1 == a\n a * (b * c) == (a * b) * c\nend\n\n# output\n\n3-element Vector{EqualityRule}:\n ~a * ~b == ~b * ~a\n ~a * 1 == ~a\n ~a * (~b * ~c) == (~a * ~b) * ~c\n","category":"page"},{"location":"egraphs/#Equality-Saturation","page":"EGraphs and Equality Saturation","title":"Equality Saturation","text":"","category":"section"},{"location":"egraphs/","page":"EGraphs and Equality Saturation","title":"EGraphs and Equality Saturation","text":"We can programmatically build and saturate an EGraph. The function saturate! takes an EGraph and a theory, and executes equality saturation. Returns a report of the equality saturation process. saturate! is configurable, customizable parameters include a timeout on the number of iterations, a eclasslimit on the number of e-classes in the EGraph, a stopwhen functions that stops saturation when it evaluates to true.","category":"page"},{"location":"egraphs/","page":"EGraphs and Equality Saturation","title":"EGraphs and Equality Saturation","text":"g = EGraph(:((a * b) * (1 * (b + c))));\nreport = saturate!(g, t);","category":"page"},{"location":"egraphs/","page":"EGraphs and Equality Saturation","title":"EGraphs and Equality Saturation","text":"With the EGraph equality saturation backend, Metatheory.jl can prove simple equalities very efficiently. The @areequal macro takes a theory and some expressions and returns true iff the expressions are equal according to the theory. The following example may return true with an appropriate example theory. ","category":"page"},{"location":"egraphs/","page":"EGraphs and Equality Saturation","title":"EGraphs and Equality Saturation","text":"julia> @areequal some_theory (x+y)*(a+b) ((a*(x+y))+b*(x+y)) ((x*(a+b))+y*(a+b)) ","category":"page"},{"location":"egraphs/#Configurable-Parameters","page":"EGraphs and Equality Saturation","title":"Configurable Parameters","text":"","category":"section"},{"location":"egraphs/","page":"EGraphs and Equality Saturation","title":"EGraphs and Equality Saturation","text":"EGraphs.saturate! can accept an additional parameter of type EGraphs.SaturationParams to configure the equality saturation algorithm. Extensive documentation for the configurable parameters is available in the EGraphs.SaturationParams API docstring.","category":"page"},{"location":"egraphs/","page":"EGraphs and Equality Saturation","title":"EGraphs and Equality Saturation","text":"# create the saturation params\nparams = SaturationParams(timeout=10, eclasslimit=4000)\nsaturate!(egraph, theory, params)","category":"page"},{"location":"egraphs/","page":"EGraphs and Equality Saturation","title":"EGraphs and Equality Saturation","text":"CurrentModule = Base","category":"page"},{"location":"egraphs/#Outline-of-the-Equality-Saturation-Algorithm","page":"EGraphs and Equality Saturation","title":"Outline of the Equality Saturation Algorithm","text":"","category":"section"},{"location":"egraphs/","page":"EGraphs and Equality Saturation","title":"EGraphs and Equality Saturation","text":"The saturate! function behaves as following. Given a starting e-graph g, a set of rewrite rules t and some parameters p (including an iteration limit n):","category":"page"},{"location":"egraphs/","page":"EGraphs and Equality Saturation","title":"EGraphs and Equality Saturation","text":"For each rule in t, search through the e-graph for l.h.s.\nFor each match produced, apply the rewrite\nDo a bottom-up traversal of the e-graph to rebuild the congruence closure\nIf the e-graph hasn’t changed from last iteration, it has saturated. If so, halt saturation.\nLoop at most n times.","category":"page"},{"location":"egraphs/","page":"EGraphs and Equality Saturation","title":"EGraphs and Equality Saturation","text":"Note that knowing if an expression with a set of rules saturates an e-graph or never terminates is still an open research problem","category":"page"},{"location":"egraphs/#Extracting-from-an-EGraph","page":"EGraphs and Equality Saturation","title":"Extracting from an EGraph","text":"","category":"section"},{"location":"egraphs/","page":"EGraphs and Equality Saturation","title":"EGraphs and Equality Saturation","text":"Since e-graphs non-deterministically represent many equivalent symbolic terms, extracting an expression from an EGraph is the process of selecting and extracting a single symbolic expression from the set of all the possible expressions contained in the EGraph. Extraction is done through the extract! function, and the theoretical background behind this procedure is an EGraph Analysis; A cost function is provided as a parameter to the extract! function. This cost function will examine mostly every e-node in the e-graph and will determine which e-nodes will be chosen from each e-class through an automated, recursive algorithm.","category":"page"},{"location":"egraphs/","page":"EGraphs and Equality Saturation","title":"EGraphs and Equality Saturation","text":"Metatheory.jl already provides some simple cost functions, such as astsize, which expresses preference for the smallest expressions contained in equivalence classes.","category":"page"},{"location":"egraphs/","page":"EGraphs and Equality Saturation","title":"EGraphs and Equality Saturation","text":"Here's an example Given the theory:","category":"page"},{"location":"egraphs/","page":"EGraphs and Equality Saturation","title":"EGraphs and Equality Saturation","text":"using Metatheory\nusing Metatheory.Library\n\ncomm_monoid = @commutative_monoid (*) 1;\nt = @theory a b c begin\n a + 0 --> a\n a + b --> b + a\n a + inv(a) --> 0 # inverse\n a + (b + c) --> (a + b) + c\n\ta * (b + c) --> (a * b) + (a * c)\n\t(a * b) + (a * c) --> a * (b + c)\n\ta * a --> a^2\n\ta --> a^1\n\ta^b * a^c --> a^(b+c)\n\tlog(a^b) --> b * log(a)\n\tlog(a * b) --> log(a) + log(b)\n\tlog(1) --> 0\n\tlog(:e) --> 1\n\t:e^(log(a)) --> a\n\ta::Number + b::Number => a + b\n\ta::Number * b::Number => a * b\nend\nt = comm_monoid ∪ t ;\nnothing # hide","category":"page"},{"location":"egraphs/","page":"EGraphs and Equality Saturation","title":"EGraphs and Equality Saturation","text":"We can extract an expression by using","category":"page"},{"location":"egraphs/","page":"EGraphs and Equality Saturation","title":"EGraphs and Equality Saturation","text":"\nexpr = :((log(e) * log(e)) * (log(a^3 * a^2)))\ng = EGraph(expr)\nsaturate!(g, t)\nex = extract!(g, astsize)","category":"page"},{"location":"egraphs/","page":"EGraphs and Equality Saturation","title":"EGraphs and Equality Saturation","text":"The second argument to extract! is a cost function. astsize is a cost function provided by default, which computes the size of expressions.","category":"page"},{"location":"egraphs/#Defining-custom-cost-functions-for-extraction.","page":"EGraphs and Equality Saturation","title":"Defining custom cost functions for extraction.","text":"","category":"section"},{"location":"egraphs/","page":"EGraphs and Equality Saturation","title":"EGraphs and Equality Saturation","text":"A cost function for EGraph extraction is a function used to determine which e-node will be extracted from an e-class. ","category":"page"},{"location":"egraphs/","page":"EGraphs and Equality Saturation","title":"EGraphs and Equality Saturation","text":"It must return a positive, non-complex number value and, must accept 3 arguments.","category":"page"},{"location":"egraphs/","page":"EGraphs and Equality Saturation","title":"EGraphs and Equality Saturation","text":"The current ENode n that is being inspected. \nThe current EGraph g.\nThe current analysis name an::Symbol.","category":"page"},{"location":"egraphs/","page":"EGraphs and Equality Saturation","title":"EGraphs and Equality Saturation","text":"From those 3 parameters, one can access all the data needed to compute the cost of an e-node recursively.","category":"page"},{"location":"egraphs/","page":"EGraphs and Equality Saturation","title":"EGraphs and Equality Saturation","text":"One can use TermInterface.jl methods to access the operation and child arguments of an e-node: operation(n), arity(n) and arguments(n)\nSince e-node children always point to e-classes in the same e-graph, one can retrieve the EClass object for each child of the currently visited enode with g[id] for id in arguments(n)\nOne can inspect the analysis data for a given eclass and a given analysis name an, by using hasdata and getdata.\nExtraction analyses always associate a tuple of 2 values to a single e-class: which e-node is the one that minimizes the cost","category":"page"},{"location":"egraphs/","page":"EGraphs and Equality Saturation","title":"EGraphs and Equality Saturation","text":"and its cost. More details can be found in the egg paper in the Analyses section. ","category":"page"},{"location":"egraphs/","page":"EGraphs and Equality Saturation","title":"EGraphs and Equality Saturation","text":"Here's an example:","category":"page"},{"location":"egraphs/","page":"EGraphs and Equality Saturation","title":"EGraphs and Equality Saturation","text":"# This is a cost function that behaves like `astsize` but increments the cost \n# of nodes containing the `^` operation. This results in a tendency to avoid \n# extraction of expressions containing '^'.\nfunction cost_function(n::ENodeTerm, g::EGraph)\n cost = 1 + arity(n)\n\n operation(n) == :^ && (cost += 2)\n\n for id in arguments(n)\n eclass = g[id]\n # if the child e-class has not yet been analyzed, return +Inf\n !hasdata(eclass, cost_function) && (cost += Inf; break)\n cost += last(getdata(eclass, cost_function))\n end\n return cost\nend\n\n# All literal expressions (e.g `a`, 123, 0.42, \"hello\") have cost 1\ncost_function(n::ENodeLiteral, g::EGraph) = 1","category":"page"},{"location":"egraphs/#EGraph-Analyses","page":"EGraphs and Equality Saturation","title":"EGraph Analyses","text":"","category":"section"},{"location":"egraphs/","page":"EGraphs and Equality Saturation","title":"EGraphs and Equality Saturation","text":"An EGraph Analysis is an efficient and automated way of analyzing all the possible terms contained in an e-graph. Metatheory.jl provides a toolkit to ease and automate the process of EGraph Analysis. ","category":"page"},{"location":"egraphs/","page":"EGraphs and Equality Saturation","title":"EGraphs and Equality Saturation","text":"An EGraph Analysis defines a domain of values and associates a value from the domain to each EClass in the graph. Theoretically, the domain should form a join semilattice. Rewrites can cooperate with e-class analyses by depending on analysis facts and adding equivalences that in turn establish additional facts. ","category":"page"},{"location":"egraphs/","page":"EGraphs and Equality Saturation","title":"EGraphs and Equality Saturation","text":"In Metatheory.jl, EGraph Analyses are uniquely identified by either","category":"page"},{"location":"egraphs/","page":"EGraphs and Equality Saturation","title":"EGraphs and Equality Saturation","text":"An unique name of type Symbol. \nA function object f, used for cost function analysis. This will use built-in definitions of make and join.","category":"page"},{"location":"egraphs/","page":"EGraphs and Equality Saturation","title":"EGraphs and Equality Saturation","text":"If you are specifying a custom analysis by its Symbol name, the following functions define an interface for analyses based on multiple dispatch on Val{analysis_name::Symbol}: ","category":"page"},{"location":"egraphs/","page":"EGraphs and Equality Saturation","title":"EGraphs and Equality Saturation","text":"islazy(an) should return true if the analysis name an should NOT be computed on-the-fly during egraphs operation, but only when inspected. \nmake(an, egraph, n) should take an ENode n and return a value from the analysis domain.\njoin(an, x,y) should return the semilattice join of x and y in the analysis domain (e.g. given two analyses value from ENodes in the same EClass, which one should I choose?). If an is a Function, it is treated as a cost function analysis, it is automatically defined to be the minimum analysis value between x and y. Typically, the domain value of cost functions are real numbers, but if you really do want to have your own cost type, make sure that Base.isless is defined.\nmodify!(an, egraph, eclassid) Can be optionally implemented. This can be used modify an EClass egraph[eclassid] on-the-fly during an e-graph saturation iteration, given its analysis value.","category":"page"},{"location":"egraphs/#Defining-a-custom-analysis","page":"EGraphs and Equality Saturation","title":"Defining a custom analysis","text":"","category":"section"},{"location":"egraphs/","page":"EGraphs and Equality Saturation","title":"EGraphs and Equality Saturation","text":"In this example, we will provide a custom analysis that tags each EClass in an EGraph with :even if it contains an even number or with :odd if it represents an odd number, or nothing if it does not contain a number at all. Let's suppose that the language of the symbolic expressions that we are considering will contain only integer numbers, variable symbols and the `and+` operations.*","category":"page"},{"location":"egraphs/","page":"EGraphs and Equality Saturation","title":"EGraphs and Equality Saturation","text":"Since we are in a symbolic computation context, we are not interested in the the actual numeric result of the expressions in the EGraph, but we only care to analyze and identify the symbolic expressions that will result in an even or an odd number.","category":"page"},{"location":"egraphs/","page":"EGraphs and Equality Saturation","title":"EGraphs and Equality Saturation","text":"Defining an EGraph Analysis is similar to the process Mathematical Induction. To define a custom EGraph Analysis, one should start by defining a name of type Symbol that will be used to identify this specific analysis and to dispatch against the required methods.","category":"page"},{"location":"egraphs/","page":"EGraphs and Equality Saturation","title":"EGraphs and Equality Saturation","text":"using Metatheory\nusing Metatheory.EGraphs","category":"page"},{"location":"egraphs/","page":"EGraphs and Equality Saturation","title":"EGraphs and Equality Saturation","text":"The next step, the base case of induction, is to define a method for make dispatching against our OddEvenAnalysis. First, we want to associate an analysis value only to the literals contained in the EGraph. To do this we take advantage of multiple dispatch against ENodeLiteral.","category":"page"},{"location":"egraphs/","page":"EGraphs and Equality Saturation","title":"EGraphs and Equality Saturation","text":"function EGraphs.make(::Val{:OddEvenAnalysis}, g::EGraph, n::ENodeLiteral)\n if n.value isa Integer\n return iseven(n.value) ? :even : :odd\n else \n return nothing\n end\nend","category":"page"},{"location":"egraphs/","page":"EGraphs and Equality Saturation","title":"EGraphs and Equality Saturation","text":"Now we have to consider the induction step. Knowing that our language contains only * and + operations, and knowing that:","category":"page"},{"location":"egraphs/","page":"EGraphs and Equality Saturation","title":"EGraphs and Equality Saturation","text":"odd * odd = odd\nodd * even = even\neven * even = even","category":"page"},{"location":"egraphs/","page":"EGraphs and Equality Saturation","title":"EGraphs and Equality Saturation","text":"And we know that ","category":"page"},{"location":"egraphs/","page":"EGraphs and Equality Saturation","title":"EGraphs and Equality Saturation","text":"odd + odd = even \nodd + even = odd \neven + even = even","category":"page"},{"location":"egraphs/","page":"EGraphs and Equality Saturation","title":"EGraphs and Equality Saturation","text":"We can now define a method for make dispatching against OddEvenAnalysis and ENodeTerms to compute the analysis value for nested symbolic terms. We take advantage of the methods in TermInterface to inspect the content of an ENodeTerm. From the definition of an ENode, we know that children of ENodes are always IDs pointing to EClasses in the EGraph.","category":"page"},{"location":"egraphs/","page":"EGraphs and Equality Saturation","title":"EGraphs and Equality Saturation","text":"function EGraphs.make(::Val{:OddEvenAnalysis}, g::EGraph, n::ENodeTerm)\n # Let's consider only binary function call terms.\n if exprhead(n) == :call && arity(n) == 2\n op = operation(n)\n # Get the left and right child eclasses\n child_eclasses = arguments(n)\n l = g[child_eclasses[1]]\n r = g[child_eclasses[2]]\n\n # Get the corresponding OddEvenAnalysis value of the children\n # defaulting to nothing \n ldata = getdata(l, :OddEvenAnalysis, nothing)\n rdata = getdata(r, :OddEvenAnalysis, nothing)\n\n if ldata isa Symbol && rdata isa Symbol\n if op == :*\n if ldata == rdata\n ldata\n elseif (ldata == :even || rdata == :even) \n :even\n else\n nothing \n end\n elseif op == :+\n (ldata == rdata) ? :even : :odd\n end\n elseif isnothing(ldata) && rdata isa Symbol && op == :*\n rdata\n elseif ldata isa Symbol && isnothing(rdata) && op == :*\n ldata\n end\n end\n\n return nothing\nend","category":"page"},{"location":"egraphs/","page":"EGraphs and Equality Saturation","title":"EGraphs and Equality Saturation","text":"We have now defined a way of tagging each ENode in the EGraph with :odd or :even, reasoning inductively on the analyses values. The analyze! function will do the dirty job of doing a recursive walk over the EGraph. The missing piece, is now telling Metatheory.jl how to merge together analysis values. Since EClasses represent many equal ENodes, we have to inform the automated analysis how to extract a single value out of the many analyses values contained in an EGraph. We do this by defining a method for join.","category":"page"},{"location":"egraphs/","page":"EGraphs and Equality Saturation","title":"EGraphs and Equality Saturation","text":"function EGraphs.join(::Val{:OddEvenAnalysis}, a, b)\n if a == b \n return a \n else\n # an expression cannot be odd and even at the same time!\n # this is contradictory, so we ignore the analysis value\n return nothing \n end\nend","category":"page"},{"location":"egraphs/","page":"EGraphs and Equality Saturation","title":"EGraphs and Equality Saturation","text":"We do not care to modify the content of EClasses in consequence of our analysis. Therefore, we can skip the definition of modify!. We are now ready to test our analysis.","category":"page"},{"location":"egraphs/","page":"EGraphs and Equality Saturation","title":"EGraphs and Equality Saturation","text":"t = @theory a b c begin \n a * (b * c) == (a * b) * c\n a + (b + c) == (a + b) + c\n a * b == b * a\n a + b == b + a\n a * (b + c) == (a * b) + (a * c)\nend\n\nfunction custom_analysis(expr)\n g = EGraph(expr)\n saturate!(g, t)\n analyze!(g, OddEvenAnalysis)\n return getdata(g[g.root], OddEvenAnalysis)\nend\n\ncustom_analysis(:(2*a)) # :even\ncustom_analysis(:(3*3)) # :odd\ncustom_analysis(:(3*(2+a)*2)) # :even\ncustom_analysis(:(3y * (2x*y))) # :even","category":"page"},{"location":"tutorials/mu/","page":"The MU Puzzle","title":"The MU Puzzle","text":"EditURL = \"https://github.com/JuliaSymbolics/Metatheory.jl/blob/master/test/tutorials/mu.jl\"","category":"page"},{"location":"tutorials/mu/#The-MU-Puzzle","page":"The MU Puzzle","title":"The MU Puzzle","text":"","category":"section"},{"location":"tutorials/mu/","page":"The MU Puzzle","title":"The MU Puzzle","text":"The puzzle cannot be solved: it is impossible to change the string MI into MU by repeatedly applying the given rules. In other words, MU is not a theorem of the MIU formal system. To prove this, one must step \"outside\" the formal system itself. Wikipedia","category":"page"},{"location":"tutorials/mu/","page":"The MU Puzzle","title":"The MU Puzzle","text":"using Metatheory, Test","category":"page"},{"location":"tutorials/mu/","page":"The MU Puzzle","title":"The MU Puzzle","text":"Here are the axioms of MU:","category":"page"},{"location":"tutorials/mu/","page":"The MU Puzzle","title":"The MU Puzzle","text":"Composition of the string monoid is associative\nAdd a uf to the end of any string ending in I\nDouble the string after the M\nReplace any III with a U\nRemove any UU","category":"page"},{"location":"tutorials/mu/","page":"The MU Puzzle","title":"The MU Puzzle","text":"function ⋅ end\nmiu = @theory x y z begin\n x ⋅ (y ⋅ z) --> (x ⋅ y) ⋅ z\n x ⋅ :I ⋅ :END --> x ⋅ :I ⋅ :U ⋅ :END\n :M ⋅ x ⋅ :END --> :M ⋅ x ⋅ x ⋅ :END\n :I ⋅ :I ⋅ :I --> :U\n x ⋅ :U ⋅ :U ⋅ y --> x ⋅ y\nend","category":"page"},{"location":"tutorials/mu/","page":"The MU Puzzle","title":"The MU Puzzle","text":"No matter the timeout we set here, MU is not a theorem of the MIU system","category":"page"},{"location":"tutorials/mu/","page":"The MU Puzzle","title":"The MU Puzzle","text":"params = SaturationParams(timeout = 12, eclasslimit = 8000)\nstart = :(M ⋅ I ⋅ END)\ng = EGraph(start)\nsaturate!(g, miu)\n@test false == areequal(g, miu, start, :(M ⋅ U ⋅ END); params = params)","category":"page"},{"location":"tutorials/mu/","page":"The MU Puzzle","title":"The MU Puzzle","text":"","category":"page"},{"location":"tutorials/mu/","page":"The MU Puzzle","title":"The MU Puzzle","text":"This page was generated using Literate.jl.","category":"page"},{"location":"#Metatheory.jl-2.0","page":"Metatheory.jl 2.0","title":"Metatheory.jl 2.0","text":"","category":"section"},{"location":"","page":"Metatheory.jl 2.0","title":"Metatheory.jl 2.0","text":"

      \n\n

      ","category":"page"},{"location":"","page":"Metatheory.jl 2.0","title":"Metatheory.jl 2.0","text":"(Image: Docs) (Image: Docs) (Image: CI) (Image: codecov) (Image: arXiv) (Image: status) (Image: Zulip)","category":"page"},{"location":"","page":"Metatheory.jl 2.0","title":"Metatheory.jl 2.0","text":"Metatheory.jl is a general purpose term rewriting, metaprogramming and algebraic computation library for the Julia programming language, designed to take advantage of the powerful reflection capabilities to bridge the gap between symbolic mathematics, abstract interpretation, equational reasoning, optimization, composable compiler transforms, and advanced homoiconic pattern matching features. The core features of Metatheory.jl are a powerful rewrite rule definition language, a vast library of functional combinators for classical term rewriting and an e-graph rewriting, a fresh approach to term rewriting achieved through an equality saturation algorithm. Metatheory.jl can manipulate any kind of Julia symbolic expression type, as long as it satisfies the TermInterface.jl.","category":"page"},{"location":"","page":"Metatheory.jl 2.0","title":"Metatheory.jl 2.0","text":"Metatheory.jl provides:","category":"page"},{"location":"","page":"Metatheory.jl 2.0","title":"Metatheory.jl 2.0","text":"An eDSL (domain specific language) to define different kinds of symbolic rewrite rules.\nA classical rewriting backend, derived from the SymbolicUtils.jl pattern matcher, supporting associative-commutative rules. It is based on the pattern matcher in the SICM book.\nA flexible library of rewriter combinators.\nAn e-graph rewriting (equality saturation) backend and pattern matcher, based on the egg library, supporting backtracking and non-deterministic term rewriting by using a data structure called e-graph, efficiently incorporating the notion of equivalence in order to reduce the amount of user effort required to achieve optimization tasks and equational reasoning.\n@capture macro for flexible metaprogramming.","category":"page"},{"location":"","page":"Metatheory.jl 2.0","title":"Metatheory.jl 2.0","text":"Intuitively, Metatheory.jl transforms Julia expressions in other Julia expressions and can achieve such at both compile and run time. This allows Metatheory.jl users to perform customized and composable compiler optimizations specifically tailored to single, arbitrary Julia packages. Our library provides a simple, algebraically composable interface to help scientists in implementing and reasoning about semantics and all kinds of formal systems, by defining concise rewriting rules in pure, syntactically valid Julia on a high level of abstraction. Our implementation of equality saturation on e-graphs is based on the excellent, state-of-the-art technique implemented in the egg library, reimplemented in pure Julia.","category":"page"},{"location":"#.0-is-out!","page":"Metatheory.jl 2.0","title":"2.0 is out!","text":"","category":"section"},{"location":"","page":"Metatheory.jl 2.0","title":"Metatheory.jl 2.0","text":"Second stable version is out:","category":"page"},{"location":"","page":"Metatheory.jl 2.0","title":"Metatheory.jl 2.0","text":"New e-graph pattern matching system, relies on functional programming and closures, and is much more extensible than 1.0's virtual machine.\nNo longer dispatch against types, but instead dispatch against objects.\nFaster E-Graph Analysis\nBetter library macros \nUpdated TermInterface to 0.3.3\nNew interface for e-graph extraction using EGraphs.egraph_reconstruct_expression\nSimplify E-Graph Analysis Interface. Use Symbols or functions for identifying Analyses. \nRemove duplicates in E-Graph analyses data.","category":"page"},{"location":"","page":"Metatheory.jl 2.0","title":"Metatheory.jl 2.0","text":"Many features have been ported from SymbolicUtils.jl. Metatheory.jl can be used in place of SymbolicUtils.jl when you have no need of manipulating mathematical expressions. The introduction of TermInterface.jl has allowed for large potential in generalization of term rewriting and symbolic analysis and manipulation features. Integration between Metatheory.jl with Symbolics.jl, as it has been shown in the \"High-performance symbolic-numerics via multiple dispatch\" paper.","category":"page"},{"location":"#Recommended-Readings-Selected-Publications","page":"Metatheory.jl 2.0","title":"Recommended Readings - Selected Publications","text":"","category":"section"},{"location":"","page":"Metatheory.jl 2.0","title":"Metatheory.jl 2.0","text":"The Metatheory.jl manual \nThe Metatheory.jl introductory paper gives a brief high level overview on the library and its functionalities.\nThe Julia Manual metaprogramming section is fundamental to understand what homoiconic expression manipulation is and how it happens in Julia.\nAn introductory blog post on SIGPLAN about egg and e-graphs rewriting.\negg: Fast and Extensible Equality Saturation contains the definition of E-Graphs on which Metatheory.jl's equality saturation rewriting backend is based. This is a strongly recommended reading.\nHigh-performance symbolic-numerics via multiple dispatch: a paper about how we used Metatheory.jl to optimize code generation in Symbolics.jl","category":"page"},{"location":"#Contributing","page":"Metatheory.jl 2.0","title":"Contributing","text":"","category":"section"},{"location":"","page":"Metatheory.jl 2.0","title":"Metatheory.jl 2.0","text":"If you'd like to give us a hand and contribute to this repository you can:","category":"page"},{"location":"","page":"Metatheory.jl 2.0","title":"Metatheory.jl 2.0","text":"Find a high level description of the project architecture in ARCHITECTURE.md\nRead the contribution guidelines in CONTRIBUTING.md","category":"page"},{"location":"","page":"Metatheory.jl 2.0","title":"Metatheory.jl 2.0","text":"If you enjoyed Metatheory.jl and would like to help, please also consider a tiny donation 💕!","category":"page"},{"location":"#Installation","page":"Metatheory.jl 2.0","title":"Installation","text":"","category":"section"},{"location":"","page":"Metatheory.jl 2.0","title":"Metatheory.jl 2.0","text":"You can install the stable version:","category":"page"},{"location":"","page":"Metatheory.jl 2.0","title":"Metatheory.jl 2.0","text":"julia> using Pkg; Pkg.add(\"Metatheory\")","category":"page"},{"location":"","page":"Metatheory.jl 2.0","title":"Metatheory.jl 2.0","text":"Or you can install the developer version (recommended by now for latest bugfixes)","category":"page"},{"location":"","page":"Metatheory.jl 2.0","title":"Metatheory.jl 2.0","text":"julia> using Pkg; Pkg.add(url=\"https://github.com/JuliaSymbolics/Metatheory.jl\")","category":"page"},{"location":"#Documentation","page":"Metatheory.jl 2.0","title":"Documentation","text":"","category":"section"},{"location":"","page":"Metatheory.jl 2.0","title":"Metatheory.jl 2.0","text":"Extensive Metatheory.jl is available here","category":"page"},{"location":"#Citing","page":"Metatheory.jl 2.0","title":"Citing","text":"","category":"section"},{"location":"","page":"Metatheory.jl 2.0","title":"Metatheory.jl 2.0","text":"If you use Metatheory.jl in your research, please cite our works.","category":"page"},{"location":"","page":"Metatheory.jl 2.0","title":"Metatheory.jl 2.0","text":"","category":"page"},{"location":"","page":"Metatheory.jl 2.0","title":"Metatheory.jl 2.0","text":"

      \n \n \n\n

      ","category":"page"},{"location":"visualizing/#Visualizing-E-Graphs","page":"Visualizing E-Graphs","title":"Visualizing E-Graphs","text":"","category":"section"},{"location":"visualizing/","page":"Visualizing E-Graphs","title":"Visualizing E-Graphs","text":"You can visualize e-graphs in VSCode by using GraphViz.jl","category":"page"},{"location":"visualizing/","page":"Visualizing E-Graphs","title":"Visualizing E-Graphs","text":"All you need to do is to install GraphViz.jl and to evaluate an e-graph after including the extra script:","category":"page"},{"location":"visualizing/","page":"Visualizing E-Graphs","title":"Visualizing E-Graphs","text":"using GraphViz\n\ninclude(dirname(pathof(Metatheory)) * \"/extras/graphviz.jl\")\n\nalgebra_rules = @theory a b c begin\n a * (b * c) == (a * b) * c\n a + (b + c) == (a + b) + c\n\n a + b == b + a\n a * (b + c) == (a * b) + (a * c)\n (a + b) * c == (a * c) + (b * c)\n\n -a == -1 * a\n a - b == a + -b\n 1 * a == a\n\n 0 * a --> 0\n a + 0 --> a\n\n a::Number * b == b * a::Number\n a::Number * b::Number => a * b\n a::Number + b::Number => a + b\nend;\n\nex = :(a - a)\ng = EGraph(ex)\nparams = SaturationParams(; timeout = 2)\nsaturate!(g, algebra_rules, params)\ng","category":"page"},{"location":"visualizing/","page":"Visualizing E-Graphs","title":"Visualizing E-Graphs","text":"And you will see a nice e-graph drawing in the Julia Plots VSCode panel:","category":"page"},{"location":"visualizing/","page":"Visualizing E-Graphs","title":"Visualizing E-Graphs","text":"(Image: E-Graph Drawing)","category":"page"},{"location":"tutorials/custom_types/","page":"Interfacing with Metatheory.jl","title":"Interfacing with Metatheory.jl","text":"EditURL = \"https://github.com/JuliaSymbolics/Metatheory.jl/blob/master/test/tutorials/custom_types.jl\"","category":"page"},{"location":"tutorials/custom_types/#Interfacing-with-Metatheory.jl","page":"Interfacing with Metatheory.jl","title":"Interfacing with Metatheory.jl","text":"","category":"section"},{"location":"tutorials/custom_types/","page":"Interfacing with Metatheory.jl","title":"Interfacing with Metatheory.jl","text":"This section is for Julia package developers who may want to use the rule rewriting systems on their own expression types.","category":"page"},{"location":"tutorials/custom_types/#Defining-the-interface","page":"Interfacing with Metatheory.jl","title":"Defining the interface","text":"","category":"section"},{"location":"tutorials/custom_types/","page":"Interfacing with Metatheory.jl","title":"Interfacing with Metatheory.jl","text":"Metatheory.jl matchers can match any Julia object that implements an interface to traverse it as a tree. The interface in question, is defined in the TermInterface.jl package. Its purpose is to provide a shared interface between various symbolic programming Julia packages. In particular, you should define methods from TermInterface.jl for an expression tree type T with symbol types S to work with SymbolicUtils.jl You can read the documentation of TermInterface.jl on the Github repository.","category":"page"},{"location":"tutorials/custom_types/#Concrete-example","page":"Interfacing with Metatheory.jl","title":"Concrete example","text":"","category":"section"},{"location":"tutorials/custom_types/","page":"Interfacing with Metatheory.jl","title":"Interfacing with Metatheory.jl","text":"using Metatheory, TermInterface, Test\nusing Metatheory.EGraphs","category":"page"},{"location":"tutorials/custom_types/","page":"Interfacing with Metatheory.jl","title":"Interfacing with Metatheory.jl","text":"We first define our custom expression type in MyExpr: It behaves like Expr, but it adds some extra fields.","category":"page"},{"location":"tutorials/custom_types/","page":"Interfacing with Metatheory.jl","title":"Interfacing with Metatheory.jl","text":"struct MyExpr\n head::Any\n args::Vector{Any}\n foo::String # additional metadata\nend\nMyExpr(head, args) = MyExpr(head, args, \"\")\nMyExpr(head) = MyExpr(head, [])","category":"page"},{"location":"tutorials/custom_types/","page":"Interfacing with Metatheory.jl","title":"Interfacing with Metatheory.jl","text":"We also need to define equality for our expression.","category":"page"},{"location":"tutorials/custom_types/","page":"Interfacing with Metatheory.jl","title":"Interfacing with Metatheory.jl","text":"function Base.:(==)(a::MyExpr, b::MyExpr)\n a.head == b.head && a.args == b.args && a.foo == b.foo\nend","category":"page"},{"location":"tutorials/custom_types/#Overriding-TermInterface-methods","page":"Interfacing with Metatheory.jl","title":"Overriding TermInterface` methods","text":"","category":"section"},{"location":"tutorials/custom_types/","page":"Interfacing with Metatheory.jl","title":"Interfacing with Metatheory.jl","text":"First, we need to discern when an expression is a leaf or a tree node. We can do it by overriding istree.","category":"page"},{"location":"tutorials/custom_types/","page":"Interfacing with Metatheory.jl","title":"Interfacing with Metatheory.jl","text":"TermInterface.istree(::MyExpr) = true","category":"page"},{"location":"tutorials/custom_types/","page":"Interfacing with Metatheory.jl","title":"Interfacing with Metatheory.jl","text":"The operation function tells us what's the node's represented operation.","category":"page"},{"location":"tutorials/custom_types/","page":"Interfacing with Metatheory.jl","title":"Interfacing with Metatheory.jl","text":"TermInterface.operation(e::MyExpr) = e.head","category":"page"},{"location":"tutorials/custom_types/","page":"Interfacing with Metatheory.jl","title":"Interfacing with Metatheory.jl","text":"arguments tells the system how to extract the children nodes.","category":"page"},{"location":"tutorials/custom_types/","page":"Interfacing with Metatheory.jl","title":"Interfacing with Metatheory.jl","text":"TermInterface.arguments(e::MyExpr) = e.args","category":"page"},{"location":"tutorials/custom_types/","page":"Interfacing with Metatheory.jl","title":"Interfacing with Metatheory.jl","text":"A particular function is exprhead. It is used to bridge our custom MyExpr type, together with the Expr functionality that is used in Metatheory rule syntax. In this example we say that all expressions of type MyExpr, can be represented (and matched against) by a pattern that is represented by a :call Expr.","category":"page"},{"location":"tutorials/custom_types/","page":"Interfacing with Metatheory.jl","title":"Interfacing with Metatheory.jl","text":"TermInterface.exprhead(::MyExpr) = :call","category":"page"},{"location":"tutorials/custom_types/","page":"Interfacing with Metatheory.jl","title":"Interfacing with Metatheory.jl","text":"While for common usage you will always define exprhead it to be :call, there are some cases where you would like to match your expression types against more complex patterns, for example, to match an expression x against an a[b] kind of pattern, you would need to inform the system that exprhead(x) is :ref, because","category":"page"},{"location":"tutorials/custom_types/","page":"Interfacing with Metatheory.jl","title":"Interfacing with Metatheory.jl","text":"ex = :(a[b])\n(ex.head, ex.args)","category":"page"},{"location":"tutorials/custom_types/","page":"Interfacing with Metatheory.jl","title":"Interfacing with Metatheory.jl","text":"metadata should return the extra metadata. If you have many fields, i suggest using a NamedTuple.","category":"page"},{"location":"tutorials/custom_types/","page":"Interfacing with Metatheory.jl","title":"Interfacing with Metatheory.jl","text":"TermInterface.metadata(e::MyExpr) = e.foo","category":"page"},{"location":"tutorials/custom_types/","page":"Interfacing with Metatheory.jl","title":"Interfacing with Metatheory.jl","text":"Additionally, you can override EGraphs.preprocess on your custom expression to pre-process any expression before insertion in the E-Graph. In this example, we always uppercase the foo::String field of MyExpr.","category":"page"},{"location":"tutorials/custom_types/","page":"Interfacing with Metatheory.jl","title":"Interfacing with Metatheory.jl","text":"EGraphs.preprocess(e::MyExpr) = MyExpr(e.head, e.args, uppercase(e.foo))","category":"page"},{"location":"tutorials/custom_types/","page":"Interfacing with Metatheory.jl","title":"Interfacing with Metatheory.jl","text":"TermInterface provides a very important function called similarterm. It is used to create a term that is in the same closure of types of x. Given an existing term x, it is used to instruct Metatheory how to recompose a similar expression, given a head (the result of operation), some children (given by arguments) and additionally, metadata and exprehead, in case you are recomposing an Expr.","category":"page"},{"location":"tutorials/custom_types/","page":"Interfacing with Metatheory.jl","title":"Interfacing with Metatheory.jl","text":"function TermInterface.similarterm(x::MyExpr, head, args; metadata = nothing, exprhead = :call)\n MyExpr(head, args, isnothing(metadata) ? \"\" : metadata)\nend","category":"page"},{"location":"tutorials/custom_types/","page":"Interfacing with Metatheory.jl","title":"Interfacing with Metatheory.jl","text":"Since similarterm works by making a new term similar to an existing term x, in the e-graphs system, there won't be enough information such as a 'reference' object. Only the type of the object is known. This extra function adds a bit of verbosity, due to compatibility with SymbolicUtils.jl","category":"page"},{"location":"tutorials/custom_types/","page":"Interfacing with Metatheory.jl","title":"Interfacing with Metatheory.jl","text":"function EGraphs.egraph_reconstruct_expression(::Type{MyExpr}, op, args; metadata = nothing, exprhead = nothing)\n MyExpr(op, args, (isnothing(metadata) ? () : metadata))\nend","category":"page"},{"location":"tutorials/custom_types/#Theory-Example","page":"Interfacing with Metatheory.jl","title":"Theory Example","text":"","category":"section"},{"location":"tutorials/custom_types/","page":"Interfacing with Metatheory.jl","title":"Interfacing with Metatheory.jl","text":"Note that terms in the RHS will inherit the type of terms in the LHS.","category":"page"},{"location":"tutorials/custom_types/","page":"Interfacing with Metatheory.jl","title":"Interfacing with Metatheory.jl","text":"t = @theory a begin\n f(z(2), a) --> f(a)\nend","category":"page"},{"location":"tutorials/custom_types/","page":"Interfacing with Metatheory.jl","title":"Interfacing with Metatheory.jl","text":"Let's create an example expression and e-graph","category":"page"},{"location":"tutorials/custom_types/","page":"Interfacing with Metatheory.jl","title":"Interfacing with Metatheory.jl","text":"hcall = MyExpr(:h, [4], \"hello\")\nex = MyExpr(:f, [MyExpr(:z, [2]), hcall])\ng = EGraph(ex; keepmeta = true)","category":"page"},{"location":"tutorials/custom_types/","page":"Interfacing with Metatheory.jl","title":"Interfacing with Metatheory.jl","text":"We use settermtype! on an existing e-graph to inform the system about the default type of expressions that we want newly added expressions to have.","category":"page"},{"location":"tutorials/custom_types/","page":"Interfacing with Metatheory.jl","title":"Interfacing with Metatheory.jl","text":"settermtype!(g, MyExpr)","category":"page"},{"location":"tutorials/custom_types/","page":"Interfacing with Metatheory.jl","title":"Interfacing with Metatheory.jl","text":"Now let's test that it works.","category":"page"},{"location":"tutorials/custom_types/","page":"Interfacing with Metatheory.jl","title":"Interfacing with Metatheory.jl","text":"saturate!(g, t)\nexpected = MyExpr(:f, [MyExpr(:h, [4], \"HELLO\")], \"\")\nextracted = extract!(g, astsize)\n@test expected == extracted","category":"page"},{"location":"tutorials/custom_types/","page":"Interfacing with Metatheory.jl","title":"Interfacing with Metatheory.jl","text":"","category":"page"},{"location":"tutorials/custom_types/","page":"Interfacing with Metatheory.jl","title":"Interfacing with Metatheory.jl","text":"This page was generated using Literate.jl.","category":"page"}] } diff --git a/dev/tutorials/custom_types/index.html b/dev/tutorials/custom_types/index.html index 35d4fb01..1446444b 100644 --- a/dev/tutorials/custom_types/index.html +++ b/dev/tutorials/custom_types/index.html @@ -18,7 +18,7 @@ end
      1-element Vector{RewriteRule}:
  f(z(2), ~a) --> f(~a)

      Let's create an example expression and e-graph

      hcall = MyExpr(:h, [4], "hello")
 ex = MyExpr(:f, [MyExpr(:z, [2]), hcall])
-g = EGraph(ex; keepmeta = true)
      EGraph(IntDisjointSet([-1, -1, -1, -1, -1], Base.RefValue{Bool}(true)), Dict{Int64, EClass}(5 => EClass 5 ([ENode(call, f, Main.var"ex-custom_types".MyExpr, [2, 4])], (metadata_analysis = Base.RefValue{Any}(""),)), 4 => EClass 4 ([ENode(call, h, Main.var"ex-custom_types".MyExpr, [3])], (metadata_analysis = Base.RefValue{Any}("HELLO"),)), 2 => EClass 2 ([ENode(call, z, Main.var"ex-custom_types".MyExpr, [1])], (metadata_analysis = Base.RefValue{Any}(""),)), 3 => EClass 3 ([4], NamedTuple()), 1 => EClass 1 ([2], NamedTuple())), Dict{AbstractENode, Int64}(4 => 3, 2 => 1, ENode(call, f, Main.var"ex-custom_types".MyExpr, [2, 4]) => 5, ENode(call, z, Main.var"ex-custom_types".MyExpr, [1]) => 2, ENode(call, h, Main.var"ex-custom_types".MyExpr, [3]) => 4), Int64[], 5, Dict{Union{Function, Symbol}, Union{Function, Symbol}}(:metadata_analysis => :metadata_analysis), Dict{Any, Vector{Int64}}(:f => [5], 4 => [3], 2 => [1], :h => [4], :z => [2]), Expr, Dict{Tuple{Any, Int64}, Type}(), 5, 0, false, Base.ImmutableDict{Int64, Tuple{Int64, Int64}}[], Tuple{Int64, Int64}[], ReentrantLock(nothing, 0x00000000, 0x00, Base.GenericCondition{Base.Threads.SpinLock}(Base.IntrusiveLinkedList{Task}(nothing, nothing), Base.Threads.SpinLock(0)), (1, 140564982919552, 0)))

      We use settermtype! on an existing e-graph to inform the system about the default type of expressions that we want newly added expressions to have.

      settermtype!(g, MyExpr)
      Main.var"ex-custom_types".MyExpr

      Now let's test that it works.

      saturate!(g, t)
+g = EGraph(ex; keepmeta = true)
      EGraph(IntDisjointSet([-1, -1, -1, -1, -1], Base.RefValue{Bool}(true)), Dict{Int64, EClass}(5 => EClass 5 ([ENode(call, f, Main.var"ex-custom_types".MyExpr, [2, 4])], (metadata_analysis = Base.RefValue{Any}(""),)), 4 => EClass 4 ([ENode(call, h, Main.var"ex-custom_types".MyExpr, [3])], (metadata_analysis = Base.RefValue{Any}("HELLO"),)), 2 => EClass 2 ([ENode(call, z, Main.var"ex-custom_types".MyExpr, [1])], (metadata_analysis = Base.RefValue{Any}(""),)), 3 => EClass 3 ([4], NamedTuple()), 1 => EClass 1 ([2], NamedTuple())), Dict{AbstractENode, Int64}(4 => 3, 2 => 1, ENode(call, f, Main.var"ex-custom_types".MyExpr, [2, 4]) => 5, ENode(call, z, Main.var"ex-custom_types".MyExpr, [1]) => 2, ENode(call, h, Main.var"ex-custom_types".MyExpr, [3]) => 4), Int64[], 5, Dict{Union{Function, Symbol}, Union{Function, Symbol}}(:metadata_analysis => :metadata_analysis), Dict{Any, Vector{Int64}}(:f => [5], 4 => [3], 2 => [1], :h => [4], :z => [2]), Expr, Dict{Tuple{Any, Int64}, Type}(), 5, 0, false, Base.ImmutableDict{Int64, Tuple{Int64, Int64}}[], Tuple{Int64, Int64}[], ReentrantLock(nothing, 0x00000000, 0x00, Base.GenericCondition{Base.Threads.SpinLock}(Base.IntrusiveLinkedList{Task}(nothing, nothing), Base.Threads.SpinLock(0)), (0, 140347632022704, 141733920768)))

      We use settermtype! on an existing e-graph to inform the system about the default type of expressions that we want newly added expressions to have.

      settermtype!(g, MyExpr)
      Main.var"ex-custom_types".MyExpr

      Now let's test that it works.

      saturate!(g, t)
 expected = MyExpr(:f, [MyExpr(:h, [4], "HELLO")], "")
 extracted = extract!(g, astsize)
-@test expected == extracted
      Test Passed

      This page was generated using Literate.jl.

      +@test expected == extracted
      Test Passed

      This page was generated using Literate.jl.

      diff --git a/dev/tutorials/fibonacci/index.html b/dev/tutorials/fibonacci/index.html index 074460b5..291365fe 100644 --- a/dev/tutorials/fibonacci/index.html +++ b/dev/tutorials/fibonacci/index.html @@ -18,15 +18,15 @@ ──────────────────────────────────────────────────────────────────── Time Allocations ─────────────────────── ──────────────────────── - Tot / % measured: 379ms / 12.2% 24.5MiB / 7.9% + Tot / % measured: 465ms / 12.6% 24.5MiB / 7.9% Section ncalls time %tot avg alloc %tot avg ──────────────────────────────────────────────────────────────────── - Search 16 30.0ms 64.9% 1.88ms 1.32MiB 68.4% 84.3KiB - 2 16 29.9ms 64.5% 1.87ms 1.27MiB 66.0% 81.3KiB - 1 16 125μs 0.3% 7.84μs 43.2KiB 2.2% 2.70KiB - Apply 16 16.0ms 34.6% 1.00ms 553KiB 28.1% 34.6KiB - Rebuild 16 238μs 0.5% 14.9μs 69.4KiB 3.5% 4.34KiB + Search 16 38.0ms 64.8% 2.38ms 1.32MiB 68.4% 84.3KiB + 2 16 37.8ms 64.4% 2.36ms 1.27MiB 66.0% 81.3KiB + 1 16 166μs 0.3% 10.4μs 43.2KiB 2.2% 2.70KiB + Apply 16 20.4ms 34.7% 1.27ms 553KiB 28.1% 34.6KiB + Rebuild 16 295μs 0.5% 18.4μs 69.4KiB 3.5% 4.34KiB ────────────────────────────────────────────────────────────────────

      That's fast!

      z = EGraph(:(fib(10)))
 saturate!(z, fibo, params)
      SaturationReport
@@ -37,16 +37,16 @@
  ────────────────────────────────────────────────────────────────────
                             Time                    Allocations      
                    ───────────────────────   ────────────────────────
- Tot / % measured:     1.37ms /  84.0%            575KiB /  87.3%    
+ Tot / % measured:     1.85ms /  81.8%            575KiB /  87.3%    
 
  Section   ncalls     time    %tot     avg     alloc    %tot      avg
  ────────────────────────────────────────────────────────────────────
- Apply         16    768μs   66.6%  48.0μs    332KiB   66.2%  20.7KiB
- Rebuild       16    193μs   16.7%  12.1μs   69.4KiB   13.8%  4.34KiB
- Search        16    193μs   16.7%  12.0μs    100KiB   20.0%  6.27KiB
-   1           16   89.7μs    7.8%  5.60μs   43.2KiB    8.6%  2.70KiB
-   2           16   89.1μs    7.7%  5.57μs   53.0KiB   10.6%  3.31KiB
+ Apply         16   1.01ms   67.1%  63.3μs    332KiB   66.2%  20.7KiB
+ Search        16    255μs   16.9%  15.9μs    100KiB   20.0%  6.27KiB
+   1           16    121μs    8.0%  7.55μs   43.2KiB    8.6%  2.70KiB
+   2           16    113μs    7.5%  7.08μs   53.0KiB   10.6%  3.31KiB
+ Rebuild       16    242μs   16.0%  15.1μs   69.4KiB   13.8%  4.34KiB
  ────────────────────────────────────────────────────────────────────

      We can test that the result is correct.

      @testset "Fibonacci" begin
   @test 55 == extract!(g, astsize)
-end
      Test.DefaultTestSet("Fibonacci", Any[], 1, false, false, true, 1.699265322367369e9, 1.699265322399251e9, false)

      This page was generated using Literate.jl.

      +end
      Test.DefaultTestSet("Fibonacci", Any[], 1, false, false, true, 1.699626131807928e9, 1.69962613186598e9, false)

      This page was generated using Literate.jl.

      diff --git a/dev/tutorials/mu/index.html b/dev/tutorials/mu/index.html index 1592b11c..75876c0a 100644 --- a/dev/tutorials/mu/index.html +++ b/dev/tutorials/mu/index.html @@ -15,4 +15,4 @@ start = :(M ⋅ I ⋅ END) g = EGraph(start) saturate!(g, miu) -@test false == areequal(g, miu, start, :(M ⋅ U ⋅ END); params = params)
      Test Passed

      This page was generated using Literate.jl.

      +@test false == areequal(g, miu, start, :(M ⋅ U ⋅ END); params = params)
      Test Passed

      This page was generated using Literate.jl.

      diff --git a/dev/tutorials/while_interpreter/index.html b/dev/tutorials/while_interpreter/index.html index 22ee03a3..e43d9d19 100644 --- a/dev/tutorials/while_interpreter/index.html +++ b/dev/tutorials/while_interpreter/index.html @@ -58,7 +58,7 @@ @test 0 == eval_if(:(cond(false, x, 0)), Mem(:x => 2)) @test 2 == eval_if(:(cond(!(false), x, 0)), Mem(:x => 2)) @test 0 == eval_if(:(cond(!(2 < x), x, 0)), Mem(:x => 3)) -end
      Test.DefaultTestSet("If Semantics", Any[], 4, false, false, true, 1.699265328546345e9, 1.699265328963836e9, false)

      Writing memory

      Our language then needs a mechanism to write in memory. We define the behavior of the store construct, which behaves like the = assignment operator in other programming languages. store(a, 5) will store the value 5 in the a variable inside the program's memory.

      write_mem = @theory sym val σ begin
+end
      Test.DefaultTestSet("If Semantics", Any[], 4, false, false, true, 1.699626139662027e9, 1.699626140181648e9, false)

      Writing memory

      Our language then needs a mechanism to write in memory. We define the behavior of the store construct, which behaves like the = assignment operator in other programming languages. store(a, 5) will store the value 5 in the a variable inside the program's memory.

      write_mem = @theory sym val σ begin
   (store(sym::Symbol, val), σ) => (σ[sym] = eval_if(val, σ);
   σ)
 end
      1-element Vector{DynamicRule}:
@@ -90,4 +90,4 @@
   @test Mem(:x => 4) == eval_while(:(cond(x < 10, store(x, x + 1))), Mem(:x => 3))
   @test 10 == eval_while(:(seq(loop(x < 10, store(x, x + 1)), x)), Mem(:x => 3))
   @test 50 == eval_while(:(seq(loop(x < y, seq(store(x, x + 1), store(y, y - 1))), x)), Mem(:x => 0, :y => 100))
-end
      Test.DefaultTestSet("While Semantics", Any[], 5, false, false, true, 1.699265330288707e9, 1.699265331226944e9, false)

      This page was generated using Literate.jl.

      +end
      Test.DefaultTestSet("While Semantics", Any[], 5, false, false, true, 1.699626141894854e9, 1.699626143056729e9, false)

      This page was generated using Literate.jl.

      diff --git a/dev/visualizing/index.html b/dev/visualizing/index.html index b8adea6e..081f3c14 100644 --- a/dev/visualizing/index.html +++ b/dev/visualizing/index.html @@ -27,4 +27,4 @@ g = EGraph(ex) params = SaturationParams(; timeout = 2) saturate!(g, algebra_rules, params) -g

      And you will see a nice e-graph drawing in the Julia Plots VSCode panel:

      E-Graph Drawing

      +g

      And you will see a nice e-graph drawing in the Julia Plots VSCode panel:

      E-Graph Drawing