Module ast

Modules§

check_shadowing
desugar
proof_global_remover: Remove global variables from the program by translating them into constructors, making proof generation easier. Does not support primitive-valued globals.
remove_globals: Remove global variables from the program by translating them into functions with no arguments. This requires type information, so it is done after type checking. Primitives are translated into functions with a primitive output. When a globally-bound primitive value is used in the actions of a rule, we add a new variable to the query bound to the primitive value.

CorrespondingVar
Facts
GenericActions
GenericFunctionDecl: Represents the declaration of a function directly parsed from source syntax.
GenericRewrite
GenericRule
GenericRunConfig
IdentSort
ParseError
Parser
ResolvedVar
RustSpan
Schema
SimpleMacro
Variant

Change: Change a function entry.
FunctionSubtype
GenericAction
GenericCommand: A Command is the top-level construct in egglog. It includes defining rules, declaring functions, adding to tables, and running rules (via a Schedule).
GenericExpr
GenericFact: Facts are the left-hand side of a [Command::Rule]. They represent a part of a database query. Facts can be expressions or equality constraints between expressions.
GenericNCommand: A NCommand is a desugared Command, where syntactic sugars like Command::Datatype and Command::Rewrite are eliminated. Most of the heavy lifting in egglog is done over NCommands.
GenericSchedule
Literal
PrintFunctionMode: The mode of printing a function. The default mode prints the function in a user-friendly way and has an unreliable interface. The CSV mode prints the function in the CSV format.
Sexp
Span
Subdatatypes

get_max_underscores: Computes the maximum number of underscores in any symbol name in the program.
replace_internal_symbol_with: Replaces all identifiers containing the internal symbol prefix with the given replacement string.
sanitize_internal_names: Sanitizes internal names so they do not contain any internal characters. This enables printing desugared egglog in a way that can be re-parsed.

Action
Actions
Command
Expr
Fact
FunctionDecl
NCommand
ResolvedCommand
ResolvedExpr: A generated expression is an expression that is generated by the system and does not have annotations.
ResolvedFact
Rewrite
Rule
RunConfig
Schedule
Subsume