Crate egglog_bridge 

An implementation of egglog-style queries on top of core-relations.

This module translates a well-typed egglog-esque query into the abstractions from the core-relations crate. The main higher-level functionality that it implements are seminaive evaluation, default values, and merge functions.

This crate is essentially involved in desugaring: it elaborates the encoding of core egglog functionality, but it does not implement algorithms for joins, union-finds, etc.

Re-exports

pub use proof_format::EqProofId;

pub use proof_format::ProofStore;

pub use proof_format::TermProofId;

Modules

macros

proof_format

A proof format for egglog programs, based on the Rocq format and checker from Tia Vu, Ryan Doegens, and Oliver Flatt.

Macros

add_expressions

define_rule

Structs

EGraph

The state associated with an egglog program.

FunctionConfig

Properties of a function added to an EGraph.

FunctionId

An id representing an egglog function

FunctionRow

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

IterationReport

Running rules produces a report of the results. This includes rough timing information and whether the database was changed.

RuleBuilder

RuleId

An egglog-style rule

RuleReport

SourceSyntax

A data-structure representing an egglog query. Essentially, multiple SourceExprs, one per line, along with a backing store accounting for subterms indexed by [`SyntaxId].

TableAction

This is an intern-able struct that holds all the data needed to do table operations with an ExecutionState, assuming that the FunctionId for the table is known ahead of time.

UnionAction

A variant of TableAction for the union-find.

Enums

ColumnTy

DefaultVal

How defaults are computed for the given function.

Function

MergeFn

How to resolve FD conflicts for a table.

QueryEntry

SourceExpr

Representative source syntax for one line of an egglog query, namely, the left-hand-side of an egglog rule.

TopLevelLhsExpr

Type Aliases

Result

SideChannel

A useful type definition for external functions that need to pass data to outside code, such as Panic.