Egglog AST macros with unquote and unquote splice - #947
Conversation
9848a4d to
e11bc66
Compare
Token-tree quasiquotes that route egglog written as Rust tokens through the parser: `expr!`, `fact!`, `facts!`, `action!`, `actions!`, `command!`, `egglog!`, `rule!`, `sexp!`, `sexps!`. Adds: - the `egglog-quote` proc-macro crate, - `parse.rs` helpers: `atom_to_sexp`, `keyword_to_sexp`, the `ToSexp` trait (+ impls for Sexp/&str/String/i64/Expr), `expr_to_sexp`, and an iterative `Display for Sexp` (heap work-stack, so deep list chains can't overflow), - re-exports from the crate root and `prelude`. The proc-macros replace the old infallible `macro_rules!` `expr!`/`fact!`/ `facts!`/`action!`/`actions!`: they now go through the parser (so `?x`, `:field`, `...`, `#`-splices, and every registered parser macro work) and return `Result`. Ported the call sites in tests/benches accordingly. Upstream's `query`/`rule`/`rust_rule` API is kept; `rule!` is reachable as `egglog::rule!` but not re-exported into `prelude` (it would collide with the `rule()` helper fn). `#(expr)` splices unwrap the parens so the generated `to_sexp(expr, ..)` is `unused_parens`-clean under `-D warnings`. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
- Add a "Writing egglog inline from Rust" section (with a runnable, tested example) to the crate-root docs (lib.md). - Fix pre-existing broken intra-doc links in proofs::proof_format: the private `RawProof`/`RawProof::Rule` links become code spans, `Fact` points at `crate::ast::Fact`, and the `Propostion` typo is fixed. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Codecov Report❌ Patch coverage is
Additional details and impacted files@@ Coverage Diff @@
## main #947 +/- ##
==========================================
- Coverage 86.42% 86.00% -0.42%
==========================================
Files 94 98 +4
Lines 29102 30014 +912
==========================================
+ Hits 25151 25815 +664
- Misses 3951 4199 +248 ☔ View full report in Codecov by Harness. 🚀 New features to boost your workflow:
|
e11bc66 to
fda2a26
Compare
Merging this PR will improve performance by 14.55%
Performance Changes
Tip Curious why this is faster? Comment Comparing Footnotes
|
Give every parsing quasiquote three flavors: - `x!` — parse only (optional parser) -> unresolved AST - `resolve_x!(eg, …)` — typecheck against the e-graph -> Resolved… (no run) - `run_x!(eg, …)` — resolve + execute -> execution result Covers expression / query / action(s) / command / program (egglog) / rule. Returns: `run_egglog!`/`run_command!`/`run_rule!`/`run_action(s)!` -> `Vec<CommandOutput>`; `run_expr!` -> `(ArcSort, Value)`; `run_query!` -> `Vec<HashMap<String, Value>>` (matches, with vars derived from the facts so no explicit `vars` needed). `resolve_*` return the matching `Resolved…` AST. Naming: since each variant has a distinct name, no parser-vs-e-graph type dispatch is needed. `run_` returns the *execution result*, not the resolved AST, so `run` and `resolve` stay distinct. Hard-renamed `facts!` -> `query!` (and dropped the singular `fact!`): "running facts" is a query, so `run_query!` returning matches is the natural fit. Supporting e-graph methods (thin wrappers over existing internals): `resolve_commands`, `resolve_expr`, `resolve_facts`, `query_all`. Also derived `Clone` for `Sexp` (needed to build `(rule …)` from spliced parts). Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
- Drop the "no quotes" / "real parser" framing (it implied an alternative the
reader has no context for); describe the macros in their own terms.
- Trim the lib.md section to a short intro + a small runnable example, and
point to the `egglog_quote` crate for the full reference.
- Soften jargon ("round-trip" / "splices as identity") in the parse.rs and
sexp! docs.
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
`rule(egraph, ruleset, facts, actions)` is subsumed by `run_egglog!(egraph, (rule (<facts>) (<actions>) :ruleset r))` (and `run_rule!` for the default ruleset) now that the run macros exist — it had no library callers, only tests/doctests. Removing it also frees the name: `rule!` is now re-exported into `prelude` alongside `resolve_rule!`/`run_rule!` (it was held out only to avoid colliding with the fn), so the rule triple is complete and consistent with the other categories. Migrated the test/doc call sites to `run_egglog!((rule … :ruleset …))`. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
- Remove `add_sort` / `add_function` / `add_constructor` / `add_relation`: 0 callers, and each is just `run_egglog!(eg, (sort …))` / `(function …)` / `(constructor …)` / `(relation …)` with a `Schema` struct instead of egglog syntax. (Two were only ever used by the removed `datatype!`.) - `add_base_sort` / `add_container_sort` register a Rust sort *type* (no egglog text equivalent), so they stay — but drop their redundant explicit `span: Span` parameter (every caller passed `span!()`) and use `span!()` internally, matching how the rest of the API hides spans. The remaining Rust-side helpers already fit the new API: `rust_rule` / `rust_rule_full` / `EGraph::query` take `Facts` (what `query!` produces); `add_ruleset` / `run_ruleset` are thin typed conveniences used internally by `query`/`rust_rule`; `exprs` / `sort!` / `vars!` are the low-level builders that back `rust_rule`. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Put the full, user-facing macro guide — the parse / resolve_* / run_* table,
the splice forms, and an example — in `egglog::prelude`, alongside the rest of
the Rust API (custom rules, primitives, sorts). It leads the module now, since
writing egglog inline is the primary way to use egglog from Rust.
- `egglog-quote`'s module doc shrinks to a one-line pointer (it's an
implementation crate; users read `egglog::prelude`).
- `lib.md` keeps a short intro + example and points at [`prelude`].
- Per-macro docs point to `egglog::prelude` instead of "the module docs".
- Dropped implementation framing ("token-tree", "routes through the parser",
`ToSexp`/`Sexp` internals) in favor of what the macros let you do.
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
egglog_header! now also generates `pub fn <name>_schema() -> Result<Vec<Command>, egglog::Error>` returning the header's declarations as commands. A schema can then be declared once (the header) and used for BOTH compile-time checking (the generated macro) and runtime emission (the fn), instead of being restated. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
The compile-time macros are named for what they do — check egglog at build time — so `egglog_checked!` / `run_egglog_checked!` read better than the `_static` names, and the crate name matches. - crate egglog-static → egglog-checked (dir static-macro → checked-macro) - egglog_static! → egglog_checked!, run_egglog_static! → run_egglog_checked! - egglog_header! unchanged; the internal @egglog_checked marker already matched Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
- CHANGELOG: summarize the new runtime quasiquotes (egglog-quote, re-exported through egglog::prelude) and the compile-time egglog-checked crate. - lib.md + prelude: point to egglog-checked (egglog_checked! / run_egglog_checked! / egglog_header!) alongside the runtime quasiquotes, so the full macro system is discoverable from the crate root and the prelude guide. - Correctness: the runtime quasiquotes surface parse errors as runtime `Result`s (spanned to your Rust source), not build errors "at the call site" — that phrasing described egglog-checked's compile-time behavior, not these. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
There was a problem hiding this comment.
Pull request overview
This PR introduces token-tree “quasiquote” macros for writing egglog programs inline in Rust, including # unquote, #.. splice, and :# runtime keyword splicing. It also adds compile-time-checked egglog macros and improves error/span plumbing so macro expansion errors can be mapped back to source locations.
Changes:
- Add
egglog-quoteproc-macro crate (expr!,query!,egglog!,run_egglog!, andresolve_*/run_*variants) plus supporting AST utilities (ToSexp, atom rendering). - Add
egglog-checkedproc-macro crate for compile-time parsing/typechecking of embedded egglog programs and reusable schema headers. - Update Rust API tests/benches/docs to use the new
query!/run_egglog!forms, and addError::span/TypeError::spanhelpers.
Reviewed changes
Copilot reviewed 21 out of 22 changed files in this pull request and generated 4 comments.
Show a summary per file
| File | Description |
|---|---|
| tests/extraction_proof_mode.rs | Switch rule construction to run_egglog! inline commands. |
| tests/api_query.rs | Update query examples/tests to use query! instead of facts!. |
| tests/api_proofs.rs | Update proofs-related API tests to use query!. |
| tests/api_const_fold.rs | Update const-fold rule setup to use query!. |
| src/typechecking.rs | Add TypeError::span() and a unit test validating span extraction. |
| src/proofs/proof_format.rs | Adjust rustdoc links/text in Justification docs. |
| src/prelude.rs | Add inline-egglog guide and re-export new quasiquote macro surface. |
| src/lib.rs | Re-export quasiquote macros; add resolve_facts, query_all, resolve_expr, resolve_commands, and Error::span. |
| src/lib.md | Add brief “writing egglog inline” documentation and example. |
| src/ast/parse.rs | Add Sexp: Clone, Display, atom classification helpers, and ToSexp for splicing. |
| quote-macro/src/lib.rs | Implement egglog-quote proc macros and splice parsing (#, #.., :#). |
| quote-macro/Cargo.toml | Add egglog-quote proc-macro crate manifest. |
| egglog-ast/src/tokens.rs | Add shared token-to-egglog-atom rendering (atom_run). |
| egglog-ast/src/lib.rs | Gate tokens module behind a feature flag. |
| egglog-ast/Cargo.toml | Add optional proc-macro2 dep + tokens feature. |
| checked-macro/tests/basic.rs | Add integration tests covering checked macros and header composition. |
| checked-macro/src/lib.rs | Implement compile-time parse/typecheck macros and schema header composition. |
| checked-macro/Cargo.toml | Add egglog-checked proc-macro crate manifest. |
| Cargo.toml | Add new workspace members + dependencies (proc-macro2, egglog-quote). |
| Cargo.lock | Lockfile updates for new crates/deps. |
| benches/rust_api_benchmarking.rs | Update benchmark rule/query setup to use query!. |
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
| /// Render an `Sexp` back to egglog source text (the inverse of parsing an | ||
| /// atom/list; literals use [`Literal`]'s own `Display`, so it round-trips). | ||
| /// | ||
| /// Deliberately **iterative** with an explicit work stack rather than | ||
| /// recursive: a built term can be a very deep left-nested chain (e.g. | ||
| /// `(ICons a (ICons b (ICons c …)))` for a long list), and per-level | ||
| /// recursion would risk a stack overflow. The work stack lives on the heap | ||
| /// and grows with the term's size instead. |
| Method::Sexp => quote! {{ | ||
| let __span = ::egglog::span!(); | ||
| let __sexps: ::std::vec::Vec<::egglog::ast::Sexp> = #items; | ||
| assert_eq!(__sexps.len(), 1, "sexp! expects exactly one form (use sexps! for many)"); |
| quote! {{ | ||
| let mut __egraph = ::egglog::EGraph::default(); | ||
| ::egglog::EGraph::parse_and_run_program( | ||
| &mut __egraph, | ||
| ::core::option::Option::None, | ||
| #src, |
| /// Proves a grounded equality `t1 = t2` which appears | ||
| /// in the body of a rule given a substitution given proofs | ||
| /// for each premise ([`Fact`]) of the rule. | ||
| /// If the [`Propostion`] proven is a term like `t = t`, | ||
| /// for each premise ([`Fact`](crate::ast::Fact)) of the rule. | ||
| /// If the [`Proposition`] proven is a term like `t = t`, | ||
| /// t may be a subexpression of the body of the rule under the substitution. |
In the crate-root overview, mention the compile-time `egglog-checked` crate as a short clause up front alongside the runtime quasiquotes, instead of a longer paragraph tacked on at the end. (prelude keeps its end-of-guide pointer, which fits there.) Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
There was a problem hiding this comment.
Just a few thoughts and comments. I have not done a full review of the code
- The lsp seems to be confused currently
- This PR is nice in that it reuses and parametrizes over the parser (so supports egglog macros), and it does not touch most of the existing code (so less pressure for code review).
- We need to have test in experimental making sure the parser also works there.
- I think the team needs to discuss if this is the interface we will commit to (since it seems this will replace prelude). My worry is this is not as general as the rust function-based apis, even though we have unquote. (edit: this looks very general)
- I was originally thinking this could be in experimental or its own repo, but it seems if this is replacing prelude then it should be in this repo?
- quote-macro is currently not tested?
- Do we want both quote-macro and checked-macro? It seems both are useful, but I'm worried that this will confuse users.
| /// ```ignore | ||
| /// let kind = "MyOp"; | ||
| /// let fields = vec!["?a", "?b"]; | ||
| /// let frag = sexp!((#kind #..fields)); // Sexp `(MyOp ?a ?b)` |
There was a problem hiding this comment.
Why is one sexp! while another is expr!?
There was a problem hiding this comment.
An Expr can't have special custom syntax if you have your own parser macros, so we provide it in case you are using it.
Luminal might use this so they can use experimental named arguments with these macros
See the changelog for this PR!