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;

pub use syntax::SourceExpr;

pub use syntax::SourceSyntax;

pub use syntax::TopLevelLhsExpr;

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.

syntax

Egglog proofs reference the source syntax of the query, but the syntax in egglog-bridge is a lower-level, “desugared” representation of that syntax.

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

RuleBuilder

RuleId

An egglog-style rule

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

Type Aliases

Result

SideChannel

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