Type Alias egglog::ast::Command

source ·
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.

Fields

§span: Span
§variants: Vec<Variant>
§

Datatypes

Fields

§span: Span
§

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

Fields

§span: Span
§constructor: GlobalSymbol
§

AddRuleset(GlobalSymbol)

Using the ruleset command, defines a new ruleset that can be added to in Command::Rules. 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

§

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.

Fields

§span: Span
§file: String
§

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.