Crate egglog 

egglog

egglog is a language specialized for writing equality saturation applications. It is the successor to the rust library egg. egglog is faster and more general than egg.

Documentation

Documentation for the egglog language can be found here: Command.

Tutorial

We have a text tutorial on egglog and how to use it. We also have a slightly outdated video tutorial.

Re-exports

pub use ast::ResolvedExpr;

pub use ast::ResolvedFact;

pub use ast::ResolvedVar;

Modules

ast

constraint

extract

prelude

This module makes it easier to use egglog from Rust.

proof

Read-only proof reconstruction API.

scheduler

sort

util

Macros

action

actions

add_literal_prim

This macro lets the user declare literal primitives with automatic validator generation. It automatically generates validators by converting between Rust values and Literal types.

add_primitive

This macro lets the user declare custom egglog primitives. It supports a few special features:

add_primitive_with_validator

This macro lets the user declare custom egglog primitives with explicit validators. It combines primitive registration with a custom validator function.

call

datatype

Adds sorts and constructor tables to the database.

expr

fact

facts

lit

match_term_app

sort

span

var

vars

Structs

CommandMacroRegistry

A registry of command macros

EGraph

ExecutionState

A handle on a database that may be in the process of running a rule.

FullState

Wrapper for Context::Full. Implements Core + Read + Write.

Function

A function in the e-graph.

FunctionRow

A struct representing the content of a row in a function table

NotFoundError

PureState

Wrapper for Context::Pure. Implements Core only.

ReadState

Wrapper for Context::Read. Implements Core + Read.

ResolvedSchema

SerializeConfig

SerializeOutput

Output of serializing an e-graph, including values that were omitted if any.

SpecializedPrimitive

TermDag

A hashconsing arena for Terms.

TypeInfo

Stores resolved typechecking information.

Value

A generic identifier representing an egglog value

WriteState

Wrapper for Context::Write. Implements Core + Write.

Enums

CommandOutput

Output from a command.

Context

The four contexts a primitive may run in, named after the capability profile they grant. Each variant maps 1:1 to one of the state wrappers below: Pure ↔ PureState, Write ↔ WriteState, Read ↔ ReadState, Full ↔ FullState. The egglog typechecker filters primitive definitions by whether they carry a runtime id for the surrounding Context at each call site.

Error

ResolvedCall

RunMode

SerializedNode

A node in the serialized egraph.

Term

Like Exprs but with sharing and deduplication.

TypeError

Constants

GLOBAL_NAME_PREFIX

Traits

BaseValue

A simple data type that can be interned in a database.

CommandMacro

A command macro that can transform commands during desugaring

ContainerValue

A trait implemented by container types.

Core

Core methods available on every state wrapper: base values, counters, container interning, value/base/container conversion sugar. Always seminaive-safe.

FullPrim

A primitive whose body sees a FullState. Register via EGraph::add_full_primitive.

Primitive

Methods shared by every kind-specific primitive trait.

PurePrim

A primitive whose body sees a PureState. Register via EGraph::add_pure_primitive.

Read

Read-side methods — name-indexed table lookup. Implemented for ReadState and FullState; not for PureState or WriteState (a Write context body must not depend on live DB state). Returns None if the row is absent — never inserts.

ReadPrim

A primitive whose body sees a ReadState. Register via EGraph::add_read_primitive.

UserDefinedCommand

A user-defined command allows users to inject custom command that can be called in an egglog program.

UserDefinedCommandOutput

A user-defined command output trait.

Write

Action-side write methods — name-indexed inserts/removes/subsumes plus union and panic. Implemented for WriteState and FullState; not for PureState or ReadState.

WritePrim

A primitive whose body sees a WriteState. Register via EGraph::add_write_primitive.

Functions

cli

Start a command-line interface for the E-graph.

file_supports_proofs

Reads a file and checks that its commands support the proof encoding.

program_supports_proofs

Checks whether a desugared program supports proof encoding.

Type Aliases

ArcSort

Atom

AtomTerm

PrimitiveValidator

Validators take a termdag and arguments (as TermIds) and return a newly computed TermId if the primitive application is valid, or None if it is invalid.

TermId