pub type Command = GenericCommand<Symbol, Symbol>;
Aliased Type§
enum Command {
Show 25 variants
SetOption {
name: GlobalSymbol,
value: GenericExpr<GlobalSymbol, GlobalSymbol>,
},
Datatype {
span: Span,
name: GlobalSymbol,
variants: Vec<Variant>,
},
Datatypes {
span: Span,
datatypes: Vec<(Span, GlobalSymbol, Subdatatypes)>,
},
Sort(Span, GlobalSymbol, Option<(GlobalSymbol, Vec<GenericExpr<GlobalSymbol, GlobalSymbol>>)>),
Function(GenericFunctionDecl<GlobalSymbol, GlobalSymbol>),
Relation {
span: Span,
constructor: GlobalSymbol,
inputs: Vec<GlobalSymbol>,
},
AddRuleset(GlobalSymbol),
UnstableCombinedRuleset(GlobalSymbol, Vec<GlobalSymbol>),
Rule {
name: GlobalSymbol,
ruleset: GlobalSymbol,
rule: GenericRule<GlobalSymbol, GlobalSymbol>,
},
Rewrite(GlobalSymbol, GenericRewrite<GlobalSymbol, GlobalSymbol>, bool),
BiRewrite(GlobalSymbol, GenericRewrite<GlobalSymbol, GlobalSymbol>),
Action(GenericAction<GlobalSymbol, GlobalSymbol>),
RunSchedule(GenericSchedule<GlobalSymbol, GlobalSymbol>),
PrintOverallStatistics,
Simplify {
span: Span,
expr: GenericExpr<GlobalSymbol, GlobalSymbol>,
schedule: GenericSchedule<GlobalSymbol, GlobalSymbol>,
},
QueryExtract {
span: Span,
variants: usize,
expr: GenericExpr<GlobalSymbol, GlobalSymbol>,
},
Check(Span, Vec<GenericFact<GlobalSymbol, GlobalSymbol>>),
PrintFunction(Span, GlobalSymbol, usize),
PrintSize(Span, Option<GlobalSymbol>),
Input {
span: Span,
name: GlobalSymbol,
file: String,
},
Output {
span: Span,
file: String,
exprs: Vec<GenericExpr<GlobalSymbol, GlobalSymbol>>,
},
Push(usize),
Pop(Span, usize),
Fail(Span, Box<GenericCommand<GlobalSymbol, GlobalSymbol>>),
Include(Span, String),
}
Variants§
SetOption
Egglog supports several experimental options
that can be set using the set-option
command.
Options supported include:
- “interactive_mode” (default: false): when enabled, egglog prints “(done)” after each command, allowing an external tool to know when each command has finished running.
Datatype
Declare a user-defined datatype.
Datatypes can be unioned with Action::Union
either
at the top level or in the actions of a rule.
This makes them equal in the implicit, global equality relation.
Example:
(datatype Math
(Num i64)
(Var String)
(Add Math Math)
(Mul Math Math))
defines a simple Math
datatype with variants for numbers, named variables, addition and multiplication.
Datatypes desugar directly to a Command::Sort
and a Command::Function
for each constructor.
The code above becomes:
(sort Math)
(function Num (i64) Math)
(function Var (String) Math)
(function Add (Math Math) Math)
(function Mul (Math Math) Math)
Datatypes are also known as algebraic data types, tagged unions and sum types.
Datatypes
Sort(Span, GlobalSymbol, Option<(GlobalSymbol, Vec<GenericExpr<GlobalSymbol, GlobalSymbol>>)>)
Create a new user-defined sort, which can then
be used in new Command::Function
declarations.
The Command::Datatype
command desugars directly to this command, with one Command::Function
per constructor.
The main use of this command (as opposed to using Command::Datatype
) is for forward-declaring a sort for mutually-recursive datatypes.
It can also be used to create
a container sort.
For example, here’s how to make a sort for vectors
of some user-defined sort Math
:
(sort MathVec (Vec Math))
Now MathVec
can be used as an input or output sort.
Function(GenericFunctionDecl<GlobalSymbol, GlobalSymbol>)
Declare an egglog function, which is a database table with a a functional dependency (also called a primary key) on its inputs to one output.
(function <name:Ident> <schema:Schema> <cost:Cost>
(:on_merge <List<Action>>)?
(:merge <Expr>)?
(:default <Expr>)?)
A function can have a cost
for extraction.
It can also have a default
value, which is used when calling the function.
Finally, it can have a merge
and on_merge
, which are triggered when
the function dependency is violated.
In this case, the merge expression determines which of the two outputs
for the same input is used.
The on_merge
actions are run after the merge expression is evaluated.
Note that the :merge
expression must be monotonic
for the behavior of the egglog program to be consistent and defined.
In other words, the merge function must define a lattice on the output of the function.
If values are merged in different orders, they should still result in the same output.
If the merge expression is not monotonic, the behavior can vary as
actions may be applied more than once with different results.
The function is a datatype when:
- The output is not a primitive
- No merge function is provided
- No default is provided
For example, the following is a datatype:
(function Add (i64 i64) Math)
However, this function is not:
(function LowerBound (Math) i64 :merge (max old new))
A datatype can be unioned with Action::Union
with another datatype of the same sort
.
Functions that are not a datatype can be set
with Action::Set
.
Relation
The relation
is syntactic sugar for a named function which returns the Unit
type.
Example:
(relation path (i64 i64))
(relation edge (i64 i64))
Desugars to:
(function path (i64 i64) Unit :default ())
(function edge (i64 i64) Unit :default ())
AddRuleset(GlobalSymbol)
Using the ruleset
command, defines a new
ruleset that can be added to in Command::Rule
s.
Rulesets are used to group rules together
so that they can be run together in a Schedule
.
Example: Ruleset allows users to define a ruleset- a set of rules
(ruleset myrules)
(rule ((edge x y))
((path x y))
:ruleset myrules)
(run myrules 2)
UnstableCombinedRuleset(GlobalSymbol, Vec<GlobalSymbol>)
Using the combined-ruleset
command, construct another ruleset
which runs all the rules in the given rulesets.
This is useful for running multiple rulesets together.
The combined ruleset also inherits any rules added to the individual rulesets
after the combined ruleset is declared.
Example:
(ruleset myrules1)
(rule ((edge x y))
((path x y))
:ruleset myrules1)
(ruleset myrules2)
(rule ((path x y) (edge y z))
((path x z))
:ruleset myrules2)
(combined-ruleset myrules-combined myrules1 myrules2)
Rule
(rule <body:List<Fact>> <head:List<Action>>)
defines an egglog rule. The rule matches a list of facts with respect to the global database, and runs the list of actions for each match. The matches are done modulo equality, meaning equal datatypes in the database are considered equal. Example:
(rule ((edge x y))
((path x y)))
(rule ((path x y) (edge y z))
((path x z)))
Rewrite(GlobalSymbol, GenericRewrite<GlobalSymbol, GlobalSymbol>, bool)
rewrite
is syntactic sugar for a specific form of rule
which simply unions the left and right hand sides.
Example:
(rewrite (Add a b)
(Add b a))
Desugars to:
(rule ((= lhs (Add a b)))
((union lhs (Add b a))))
Additionally, additional facts can be specified
using a :when
clause.
For example, the same rule can be run only
when a
is zero:
(rewrite (Add a b)
(Add b a)
:when ((= a (Num 0)))
Add the :subsume
flag to cause the left hand side to be subsumed after matching, which means it can
no longer be matched in a rule, but can still be checked against (See Change
for more details.)
(rewrite (Mul a 2) (bitshift-left a 1) :subsume)
Desugars to:
(rule ((= lhs (Mul a 2)))
((union lhs (bitshift-left a 1))
(subsume (Mul a 2))))
BiRewrite(GlobalSymbol, GenericRewrite<GlobalSymbol, GlobalSymbol>)
Similar to Command::Rewrite
, but
generates two rules, one for each direction.
Example:
(bi-rewrite (Mul (Var x) (Num 0))
(Var x))
Becomes:
(rule ((= lhs (Mul (Var x) (Num 0))))
((union lhs (Var x))))
(rule ((= lhs (Var x)))
((union lhs (Mul (Var x) (Num 0)))))
Action(GenericAction<GlobalSymbol, GlobalSymbol>)
Perform an Action
on the global database
(see documentation for Action
for more details).
Example:
(let xplusone (Add (Var "x") (Num 1)))
RunSchedule(GenericSchedule<GlobalSymbol, GlobalSymbol>)
Runs a Schedule
, which specifies
rulesets and the number of times to run them.
Example:
(run-schedule
(saturate my-ruleset-1)
(run my-ruleset-2 4))
Runs my-ruleset-1
until saturation,
then runs my-ruleset-2
four times.
See Schedule
for more details.
PrintOverallStatistics
Print runtime statistics about rules and rulesets so far.
Simplify
Fields
expr: GenericExpr<GlobalSymbol, GlobalSymbol>
schedule: GenericSchedule<GlobalSymbol, GlobalSymbol>
QueryExtract
The query-extract
command runs a query,
extracting the result for each match that it finds.
For a simpler extraction command, use Action::Extract
instead.
Example:
(query-extract (Add a b))
Extracts every Add
term in the database, once
for each class of equivalent a
and b
.
The resulting datatype is chosen from the egraph
as the smallest term by size (taking into account
the :cost
annotations for each constructor).
This cost does not take into account common sub-expressions.
For example, the following term has cost 5:
(Add
(Num 1)
(Num 1))
Under the hood, this command is implemented with the EGraph::extract
function.
Check(Span, Vec<GenericFact<GlobalSymbol, GlobalSymbol>>)
The check
command checks that the given facts
match at least once in the current database.
The list of facts is matched in the same way a Command::Rule
is matched.
Example:
(check (= (+ 1 2) 3))
(check (<= 0 3) (>= 3 0))
(fail (check (= 1 2)))
prints
[INFO ] Checked.
[INFO ] Checked.
[ERROR] Check failed
[INFO ] Command failed as expected.
PrintFunction(Span, GlobalSymbol, usize)
Print out rows a given function, extracting each of the elements of the function. Example:
(print-function Add 20)
prints the first 20 rows of the Add
function.
PrintSize(Span, Option<GlobalSymbol>)
Print out the number of rows in a function or all functions.
Input
Input a CSV file directly into a function.
Output
Extract and output a set of expressions to a file.
Push(usize)
push
the current egraph n
times so that it is saved.
Later, the current database and rules can be restored using pop
.
Pop(Span, usize)
pop
the current egraph, restoring the previous one.
The argument specifies how many egraphs to pop.
Fail(Span, Box<GenericCommand<GlobalSymbol, GlobalSymbol>>)
Assert that a command fails with an error.
Include(Span, String)
Include another egglog file directly as text and run it.