Allow unstable-fn to target primitives by saulshanabrook · Pull Request #889 · egraphs-good/egglog

saulshanabrook · 2026-05-18T20:20:16Z

Context

unstable-fn function containers could target table functions, but primitive overloads needed matching typechecking and runtime resolution support.

This remains separate from the primitive-body API work in #881. Keeping the function-container changes isolated makes the dependent experimental PR smaller and avoids coupling (primitive ...) support to the unstable-fn primitive-target behavior.

Changes

Extends unstable-fn type constraints to account for primitive overloads.
Resolves primitive function containers for scheduled rules and merge functions.
Keeps resolver APIs private to this implementation.
Adds tests for primitive-backed function containers and merge-function use.

Validation

cargo fmt --check
cargo test -q --test typed_primitive unstable_app
cargo test -q --test typed_primitive unstable_fn_duplicate_primitive_registration_panics_on_build
cargo test -q --test files --features bin unstable_fn
git diff --check

codspeed-hq · 2026-05-18T22:44:33Z

Merging this PR will improve performance by 25.76%

⚠️

Different runtime environments detected

Some benchmarks with significant performance changes were compared across different runtime environments,
which may affect the accuracy of the results.

Open the report in CodSpeed to investigate

⚡ 2 improved benchmarks
❌ 1 regressed benchmark
✅ 22 untouched benchmarks
🆕 1 new benchmark
⏩ 215 skipped benchmarks¹

Warning

Please fix the performance issues or acknowledge them on CodSpeed.

Performance Changes

	Mode	Benchmark	`BASE`	`HEAD`	Efficiency
🆕	Simulation	`tests[repro-herbie-vanilla]`	N/A	1.4 s	N/A
⚡	Simulation	`rust_rule_fib[rule_run_1000]`	280.7 ms	207.3 ms	+35.41%
❌	Simulation	`tests[python_array_optimize]`	1.5 s	1.7 s	-8.04%
⚡	Simulation	`tests[cykjson]`	440.2 ms	275.6 ms	+59.72%

Tip

Investigate this regression by commenting @codspeedbot fix this regression on this PR, or directly use the CodSpeed MCP with your agent.

_{Comparing saulshanabrook:codex/split-unstable-fn-primitive-targets (62121df) with main (8c1c70b)²}

215 benchmarks were skipped, so the baseline results were used instead. If they were deleted from the codebase, click here and archive them to remove them from the performance reports. ↩
No successful run was found on main (2e1796e) during the generation of this report, so 8c1c70b was used instead as the comparison base. There might be some changes unrelated to this pull request in this report. ↩

codecov-commenter · 2026-05-26T20:06:22Z

Codecov Report

❌ Patch coverage is 85.58559% with 32 lines in your changes missing coverage. Please review.
✅ Project coverage is 87.08%. Comparing base (2e1796e) to head (62121df).

Files with missing lines	Patch %	Lines
src/lib.rs	82.25%	22 Missing ⚠️
src/sort/fn.rs	89.79%	10 Missing ⚠️

Additional details and impacted files

@@            Coverage Diff             @@
##             main     #889      +/-   ##
==========================================
- Coverage   87.12%   87.08%   -0.04%     
==========================================
  Files          88       88              
  Lines       25904    26041     +137     
==========================================
+ Hits        22568    22679     +111     
- Misses       3336     3362      +26

☔ View full report in Codecov by Sentry.
📢 Have feedback on the report? Share it here.

🚀 New features to boost your workflow:

❄️ Test Analytics: Detect flaky tests, report on failures, and find test suite problems.
📦 JS Bundle Analysis: Save yourself from yourself by tracking and limiting bundle sizes in JS merges.

Teach function-container construction to resolve primitive targets as well as ordinary egglog functions. A primitive target is matched against the requested UnstableFn sort plus any explicit partial arguments, and the resulting FunctionContainer stores the runtime primitive ids for each execution context. This keeps the existing application-time dispatch behavior: the context at the unstable-app call site chooses the runtime id, so a function value built in one context is not trapped there. This also handles merge expressions where unstable-fn appears inside a primitive merge function. The merge-function translator now replaces the target name with the same resolved FunctionContainer value used by rule/query lowering, so partially applied primitive targets like `(unstable-fn "+" old)` work as merge functions. Tests now cover primitive targets across nullary, unary, Unit-returning, overloaded, higher-order, container-specific, and merge contexts: - `vec-empty` and `map-empty` as nullary container primitives. - `not` and `<` as unary / Unit-returning primitives. - `+` for both i64 and f64 overloads. - `unstable-vec-map` wrapped through unstable-fn as a higher-order primitive. - a merge function using partially applied `+`. - a fail-typecheck case showing `(unstable-fn "+")` is not enough for an `UnstableFn (i64) i64` merge target without the missing `old` argument. One cleanup is intentionally deferred. Direct duplicate same-signature primitive registrations already panic in `ResolvedCall::from_resolution` after typechecking has concrete sorts but more than one indistinguishable primitive registration remains. This commit keeps primitive unstable-fn targets aligned with that behavior: duplicate exact primitive matches still panic rather than threading a new TypeError/Error path through rule lowering and scheduler rule construction. That deferred work is tracked in egraphs-good#898. The follow-up should make primitive resolution return typed errors for no-match and ambiguous exact-match cases in both direct calls and unstable-fn targets. It should also harden `step_rules_with_scheduler`: that method temporarily takes `self.rulesets` and `self.schedulers`, and the existing fallible `backend.run_rules(...)` paths can return before those fields are restored. A previous version of this patch exposed the same restoration problem through fallible scheduler rule construction, but fixing that scheduler robustness issue is broader than this primitive-target feature and is left for the follow-up. Validation: - cargo fmt --check - cargo test --test typed_primitive - cargo test --test files --features bin typed_primitive_unstable_app - cargo test --test files --features bin unstable_fn_primitive_missing_partial_arg - cargo test --lib scheduler::test - make nits - make test Reviews: - CodeRabbit reported a trivial panic-message issue, fixed here. - Independent sub-agent review reported no remaining blocker, major, or minor findings after the added map-empty / unstable-vec-map coverage.

saulshanabrook · 2026-05-31T13:30:09Z

@coderabbitai full review

coderabbitai · 2026-05-31T13:30:14Z

✅ Actions performed

Full review triggered.

coderabbitai · 2026-05-31T13:36:56Z

📝 Walkthrough

Summary by CodeRabbit

New Features
- unstable-fn function containers now support targeting primitive overloads with automatic overload resolution based on function signatures.

Walkthrough

This PR enables the unstable-fn primitive to resolve both named function containers and primitive overloads. Type constraints are expanded to synthesize arguments for overload checking, a centralized resolution helper is introduced to unify dispatch logic, and both merge-expression translation and runtime compilation are wired to use it.

Changes

unstable-fn Resolution and Primitive Overload Dispatch

Layer / File(s)	Summary
Type constraints and TypeId import for unstable-fn `src/sort/fn.rs`	The `FunctionCTorTypeConstraint` handler now pattern-matches string-literal function names and conditionally builds constraints for both known function types (validating arity and tying arguments to required input/output sorts) and registered primitives (synthesizing "future" arguments and using XOR to resolve among overloads).
Centralized resolution helper function `src/lib.rs`	Introduces `resolve_function_container_target_with_context`, which validates `unstable-fn` output is a function sort, computes partial arc sorts from primitive inputs, and resolves the wrapped target either by named function lookup (with strict sort validation) or by primitive overload selection (via signature acceptance and runtime-context dispatch IDs), returning a `ResolvedFunction`.
Merge-expression and runtime integration `src/lib.rs`	`translate_expr_to_mergefn` validates the first argument is a string literal, resolves the target using the helper, and replaces the raw string with a resolved-function constant. `BackendRule::prim` constructs a context-specific panic ID, delegates to the helper, and injects the resolved function constant into `qe_args[0]`.
Changelog documentation `CHANGELOG.md`	Documents in [Unreleased] that `unstable-fn` function containers can target primitive overloads.

Estimated code review effort

🎯 4 (Complex) | ⏱️ ~60 minutes

Possibly related issues

egraphs-good/egglog#898: Both touch the unstable-fn primitive-resolution code path; this PR centralizes resolution logic while the issue proposes replacing panic-based primitive resolution with typed errors.

Possibly related PRs

egraphs-good/egglog#873: Both PRs address context-aware primitive dispatch and ID resolution; the related PR refactors primitives to be selected via per-Context context_ids, and this PR's unstable-fn resolution uses that runtime-context dispatch machinery.

Suggested labels

status:needs decision

Suggested reviewers

oflatt
FTRobbin

🚥 Pre-merge checks | ✅ 4 | ❌ 1

❌ Failed checks (1 warning)

Check name	Status	Explanation	Resolution
Docstring Coverage	⚠️ Warning	Docstring coverage is 20.00% which is insufficient. The required threshold is 80.00%.	Write docstrings for the functions missing them to satisfy the coverage threshold.

✅ Passed checks (4 passed)

Check name	Status	Explanation
Title check	✅ Passed	The title clearly and concisely summarizes the main change: extending unstable-fn to support primitive overload targeting.
Description check	✅ Passed	The description is well-organized and directly related to the changeset, explaining context, specific changes, and validation steps.
Linked Issues check	✅ Passed	Check skipped because no linked issues were found for this pull request.
Out of Scope Changes check	✅ Passed	Check skipped because no linked issues were found for this pull request.

_{✏️ Tip: You can configure your own custom pre-merge checks in the settings.}

✨ Finishing Touches

🧪 Generate unit tests (beta)

Create PR with unit tests

Thanks for using CodeRabbit! It's free for OSS, and your support helps us grow. If you like it, consider giving us a shout-out.

❤️ Share

_{Comment @coderabbitai help to get the list of available commands and usage tips.}

coderabbitai

Actionable comments posted: 1

🤖 Prompt for all review comments with AI agents

Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.

Inline comments:
In `@src/lib.rs`:
- Around line 1991-1994: The code currently calls
type_info.get_func_type(name).unwrap_or_else(|| panic!("No resolution for
{name:?}")) after functions.get(name) succeeded; replace this blind unwrap with
a defensive check that documents the invariant — e.g., call
type_info.get_func_type(name) and either assert with
debug_assert!(func_type.is_some(), "invariant: func type missing for {name:?}")
then unwrap_unchecked in debug/release as appropriate, or use expect with a more
descriptive message referencing functions.get(name) and name (symbols:
functions.get, type_info.get_func_type, func_type, name) so failures produce a
clear diagnostic.

🪄 Autofix (Beta)

Fix all unresolved CodeRabbit comments on this PR:

Push a commit to this branch (recommended)
Create a new PR with the fixes

ℹ️ Review info

⚙️ Run configuration

Configuration used: Organization UI

Review profile: ASSERTIVE

Plan: Pro

Run ID: 70def3e3-b1e3-42e0-a6c6-facce89551a0

📥 Commits

Reviewing files that changed from the base of the PR and between 2e1796e and 62121df.

⛔ Files ignored due to path filters (4)

tests/fail-typecheck/unstable-fn-primitive-missing-partial-arg.egg is excluded by !**/*.egg
tests/snapshots/files__fail-typecheck__unstable_fn_primitive_missing_partial_arg.snap is excluded by !**/*.snap
tests/snapshots/files__shared_snapshot_typed_primitive_unstable_app.snap is excluded by !**/*.snap
tests/typed_primitive_unstable_app.egg is excluded by !**/*.egg

📒 Files selected for processing (3)

CHANGELOG.md
src/lib.rs
src/sort/fn.rs

📜 Review details

⏰ Context from checks skipped due to timeout of 90000ms. You can increase the timeout in your CodeRabbit configuration to a maximum of 15 minutes (900000ms). (11)

GitHub Check: benchmark (ubuntu-latest, factoring-multisets)
GitHub Check: benchmark (ubuntu-latest, proof_testing_typecheck)
GitHub Check: benchmark (ubuntu-latest, eggcc-2mm)
GitHub Check: benchmark (ubuntu-latest, herbie)
GitHub Check: benchmark (ubuntu-latest, conv1d_128)
GitHub Check: benchmark (ubuntu-latest, math-microbenchmark)
GitHub Check: benchmark (ubuntu-latest, rectangle)
GitHub Check: benchmark (ubuntu-latest, eggcc-extraction)
GitHub Check: benchmark (ubuntu-latest, taylor51)
GitHub Check: test
GitHub Check: coverage

🔇 Additional comments (6)

CHANGELOG.md (1)

10-10: LGTM!

src/sort/fn.rs (2)

12-12: LGTM!

275-405: LGTM!

src/lib.rs (3)

715-743: LGTM!

2181-2190: LGTM!

2038-2045: Verify primitive API compatibility (PrimitiveWithId from type_info.get_prims).
type_info.get_prims(...) returns Option<&[PrimitiveWithId]> (src/typechecking.rs:1018); PrimitiveWithId has context_ids: EnumMap<Context, Option<ExternalFunctionId>> (src/typechecking.rs:164); and PrimitiveWithId is also used with .accept(types, typeinfo) elsewhere (src/core.rs:185), so the .context_ids[runtime_ctx] and .accept(&signature, type_info) accesses are consistent.

After rebasing against origin/main (which had picked up PR egraphs-good#889's unstable-fn dispatch refactor and PR egraphs-good#895's FullState exposure): - Drop the `EGraph::with_full_state` PR egraphs-good#895 added — superseded by our `EGraph::update` from this PR. Our `update` returns `Result<R, Error>` and includes the proof-incompatibility check, so the old `with_full_state` is now redundant. - Pull in `resolve_function_container_target_with_context` from main — main's `unstable-fn` dispatch sites now go through this helper, but `git rebase -X theirs` preferred our older callers without realising the helper was new in main. - Switch the `clear_function` integration test in `tests/integration_test.rs` from the (now `pub(crate)`) `EGraph::lookup_function` to the public `Read::lookup_raw` via `update`. Keeps the legacy private read off the public surface. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>

* api: typed read/write surface on Read/Write traits + EGraph::with_full_state Single source of truth for the typed user API: methods live on the Read and Write traits, the same surface a rust_rule / rust_rule_full callback already sees. Outside a rule, EGraph::with_full_state(|fs| ...) hands out the same FullState handle. // Inside a rule callback (WriteState / FullState): unchanged. ws.set("f", (1_i64,), 42_i64); ws.add_node("Cons", (1_i64, nil)); // Outside a rule: with_full_state batches writes — one flush // happens after the closure returns, so split write/read across // calls for the read to see the write. eg.with_full_state(|mut fs| fs.set("f", (1_i64,), 42_i64)); let v: Option<i64> = eg.with_full_state(|fs| fs.lookup::<_, i64>("f", 1_i64)); // Constructors mint or look up an eclass. The returned Value is // the eclass id; the Rust API does not currently tag Values with // their egglog sort. let nil = eg.with_full_state(|mut fs| fs.add_node("Nil", RawValues(vec![])).unwrap()); // Pattern queries stay on EGraph — they compile a one-shot rule. let rows: Vec<(i64,)> = eg.query_pattern(vars![x: i64], facts![(R x)])?; // Base-value interning stays on EGraph. let v = eg.intern::<i64>(7); let n: i64 = eg.extract(v); Read trait gains lookup<K, V>, eclass_of<K> (returns Option<Value>), contains<K>, plus lookup_raw (untyped escape hatch). Write trait gains a typed remove<K>; its set/add_node already existed. Underpinned by `crate::api`: - IntoRow / IntoColumn for input rows (tuple of base values, single value, or RawValues escape hatch). - FromRow / FromColumn for output rows (symmetric). The Rust API does not currently track egglog sort identity on Values at the Rust type level. A Value returned by one constructor is indistinguishable from one returned by another; callers track sort themselves. Subtype safety: set on a constructor, add_node on a function, lookup on a constructor, eclass_of on a function all PANIC with a message naming the offending table — these are programmer bugs, not runtime input errors. The check is plumbed through a new `egglog_bridge::TableKind` enum on TableAction (Function vs Constructor), derived from the function's default-value kind at table registration time. API audit: no public method anywhere in the egglog crate now takes a TableId, FunctionId, or ExternalFunctionId. The user-facing surface is strings + Value end-to-end. Read::table_name(TableId) (the last leak) is dropped — it had zero callers. Bench evidence (benches/rust_api_benchmarking.rs sweep n_dummy_funcs): 100k inserts in one rule fire, 2000 dummy tables: 7.41 ms vs 7.34 ms at 0 dummy tables — ~1% overhead from the per-call HashMap lookup. Hot-path read bench (50k matches × set + lookup_raw + union) flat across 0/200/2000 dummy funcs. Strings are fast enough; no need to keep a public FunctionId for performance. `with_full_state` mirrors PR #895's helper of the same name; if #895 merges first this commit's body can drop the duplicate. Refs #745, #751, #895. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * api: move table_rows to the Read trait Previously `EGraph::table_rows` was a top-level method; now it's `Read::table_rows`, accessible from `ReadState` / `FullState` — so `add_rust_rule_full` callbacks can iterate tables alongside the other name-indexed methods. Adds `TableAction::for_each` / `for_each_while` in egglog-bridge, mirroring the existing `EGraph::for_each` but reaching the table through an `ExecutionState` (the same pattern as the existing `TableAction::lookup` / `row_count`). `EGraph::table_rows` is kept as a thin convenience wrapper that delegates to `with_full_state`, so top-level callers don't change. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com> * api: clear errors when used with proofs + constant-folding case study The new Rust API surface was silently broken when proofs were enabled: - `rust_rule` / `rust_rule_full` register an auto-generated primitive with `validator: None`, which the proof typechecker doesn't know about. Calling these under `EGraph::new_with_proofs()` previously errored with "Unbound function `@rust_rule_prim_3`" — a leaky internal name with no hint at the real problem. - `EGraph::with_full_state` writes flush directly into the backend, bypassing the proof-encoding pipeline. The proof checker had no record of those updates, so any rule derivation resting on them would have been unverifiable. Both now check `EGraph::are_proofs_enabled()` upfront and return the new `Error::ProofsIncompatibleApi { api, reason }` with a clear explanation. Three tests in `tests/api_proofs.rs` lock in the behavior. `with_full_state`'s signature tightened from `FnOnce(FullState) -> R) -> R` to `FnOnce(FullState) -> Result<R, Error>) -> Result<R, Error>` — collapsing the proofs-check error path with the closure's error path, so callers stay one `?` deep. All 39 existing callsites already returned `Result` from their closure and need no changes. Plus `tests/api_const_fold.rs` — a constant-folding case study that exercises the whole API end-to-end: `with_full_state` to build a `(Add (Num 2) (Add (Num 3) (Num 4)))` expression with `add_node`, a `rust_rule` that pattern-matches `(Add (Num a) (Num b))` and uses `add_node` + `union` to fold, then `table_rows` and `eclass_of` to verify the root collapses to `(Num 9)`. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com> * docs: drop stale 'typed user API' language, refresh changelog After the Id-based dynamic-typing work was reverted (preserved at tag oflatt-dynamic-type-checks), 'typed user API' / 'typed Rust API' / 'typed methods' read as if the API still carries compile-time-typed eclass wrappers. It doesn't — the surface is name-indexed Read / Write methods over plain `Value`s, with column-sort validation as the only runtime type check. Renamed to plain 'API' / 'Read/Write methods' / 'Rust API' throughout. Also: - Drop the stale 'BaseSortName was previously re-exported here' comment in src/lib.rs (intern/extract are long gone). - Drop the stale `table_lookup` reference from the exec_state module doc (the method no longer exists). - CHANGELOG entry for `table_rows` corrected to reflect the `Read::table_rows` primary location with `EGraph::table_rows` as the thin top-level wrapper, plus the new proof-mode-compatibility errors and the constant-folding case study. - 'typed primitive surface' (PurePrim / WritePrim / ReadPrim / FullPrim) kept as-is — that 'typed' refers to the capability-typed primitive contexts (issue #772), not to the eclass typing this PR walked back. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com> * rename with_execution_state -> update Cross-crate rename of the `Database::with_execution_state` / `egglog_bridge::EGraph::with_execution_state` closure-taking method to just `update`. Same behavior; less verbose at the 9 callsites (`db.update(|state| ...)` reads cleaner than `db.with_execution_state(|state| ...)`). The closure can do reads or writes via the `&mut ExecutionState`, but the common use is staging writes that flush on `flush_updates` — the shorter name matches that primary intent. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com> * rename EGraph::with_full_state -> EGraph::update; drop stale comments Cross-PR rename to match the bridge-level `egglog_bridge::EGraph::update` that just landed. The two live in different scopes (`egglog::EGraph` user-facing, `egglog_bridge::EGraph` internal), so the shared name doesn't collide for anyone — and reads more cleanly against the contrast egg sets: - egg: `egraph.add(expr)` / `egraph.union(a, b)` / `egraph.rebuild()` - egglog (now): `egraph.update(|fs| fs.add_node(...))` / `egraph.update(|fs| fs.union(a, b))` — one entry point, all mutations batched and flushed at the end of the closure. Also drop the "earlier revisions" comment in `benches/rust_api_benchmarking.rs` — references to prior iterations of the bench code don't help future readers; they read as a half-written changelog stuck in the source. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com> * rename Write::add_node -> Write::add Symmetric with the just-renamed `EGraph::update`, and closer to egg's `EGraph::add(expr)`: fs.add("Cons", (1_i64, nil)) reads as cleanly as egraph.add(expr) does in egg. The `_node` suffix was redundant — the only thing `Write::add` can add IS a constructor / relation row, by trait signature. (TermDag's internal `add_node` for `Term` is unaffected; that's a separate, lower-level method that does add a term node, not a row.) Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com> * drop per-column sort checking; closes the 1.5x insert regression The sort checking added in the original Stage-1 work was inconsistent with the rest of this PR: it would catch a `String` literal passed where an `i64` was expected (a typo Rust mostly catches at compile time anyway), but it couldn't catch a `Math` eclass passed where a `List` eclass was expected — both are bare `Value`s with no sort metadata to compare. That's the type-confusion this PR's predecessor (the parked dynamic-type-checks tag) was built to catch, and we don't have it here. So the partial sort check was paying a 1.54x cost on `insert_loop` (measured: 77 us baseline -> 119 us with checks) to protect against a narrower class of typos than the API's signature already protects against. Drop it. What's removed: - `ApiError::WrongColumnSort`, `ApiError::WrongOutputSort` - `ColumnSort` enum (was only consumed by the dropped checks) - `IntoColumn::column_sort()` (sort tag no longer needed) - `IntoRow::column_sorts()` replaced by `IntoRow::arity()` — we still want arity validation, that's cheap and catches a different class of typo (passing a 2-tuple to a 3-column table) - `check_input_sorts`, `check_output_sort` collapsed into a single `check_arity` helper - `tests/api_fact_ops::test_wrong_column_sort_errors` and `test_wrong_output_sort_errors` What stays: - `WrongArity`, `WrongSubtype`, `MissingTable` errors and tests - `FunctionConfig.sort_names` plumbing on the bridge side, as a future hook for the parked dynamic-typing work Bench after this change (median, 10 samples): | bench | main | this PR | |--------------------------------|-----------|------------| | insert_loop ops1000_funcs200 | 77.35 us | 82.79 us | 1.07x noise | tableaction_hot_path funcs200 | 5.039 ms | 4.297 ms | 0.85x faster | fib rule_run_1000 | 30.12 ms | 29.79 ms | 0.99x | match_overhead | 2.192 ms | 2.169 ms | 0.99x | match_with_serialize | 44.71 ms | 43.37 ms | 0.97x Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com> * docs: CHANGELOG matches the dropped sort-checking `WrongColumnSort` and `WrongOutputSort` are gone; per-column sort checking is not done. `IntoColumn::column_sort()` is gone; `IntoRow::column_sorts()` became `IntoRow::arity()`. Update the changelog entries to match what's actually in the PR. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com> * docs: trim changelog, drop stale "sort checking" mentions CHANGELOG: removed two entries that were too granular for a public changelog: - proof-mode-incompatibility errors (one error variant + signature tightening — implementation detail of how proofs interact with the new API, not its own feature) - constant-folding case study in tests/ (test coverage isn't a changelog entry) Also folded WrongSubtype / WrongArity / MissingTable, table_rows, and query into the main "name-indexed API" bullet — they belong with the API description, not as separate top-level items. Also picked up three stale references the doc audit caught: - `Read::lookup_raw` doc no longer says "Skips sort checking" — there is no sort checking to skip. - `egglog_bridge::FunctionConfig.sort_names` doc no longer mentions the deleted `ColumnSort::Unchecked` variant or claims runtime validation. It's a hook for future dynamic-typing work. - Two test functions in `api_fact_ops.rs` had `add_node` in their names — renamed to match the actual API method (`add`). Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com> * drop ExecutionState from the public re-export `ExecutionState` was being re-exported from `core_relations` via `pub use core_relations::{BaseValue, ContainerValue, ExecutionState, Value}`, but nothing user-facing actually requires it: every API hands out a `PureState` / `WriteState` / `ReadState` / `FullState` wrapper around it. Make it crate-internal — `core_relations::ExecutionState` is still reachable for anyone who really wants the raw type via the bridge. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com> * EGraph::query returns Vec<HashMap<String, Value>> The R: FromRow generic on query was a complexity-for-not-much: the caller had to remember positional column order to match the vars they declared. Switch to a named-binding return: one HashMap<String, Value> per match, keyed by the variable name from vars. // before let rows: Vec<(i64, i64)> = eg.query::<(i64, i64)>(vars![x: i64, y: i64], facts![...])?; // after let rows: Vec<_> = eg.query(vars![x: i64, y: i64], facts![...])?; for m in rows { let x = eg.value_to_base::<i64>(m["x"]); let y = eg.value_to_base::<i64>(m["y"]); } Values stay raw Value — callers do their own base-value conversion via EGraph::value_to_base (or value_to_container, or whatever fits the column's sort). Generic-over-FromRow path is gone for this method; query is no longer generic. Zero-var queries still return one empty HashMap per match, so .len() reports the number of matches. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com> * drop prelude::query and QueryResult; EGraph::query is the only one The free function `prelude::query` returned a `QueryResult` struct (flat untyped Vec<Value> + per-row chunk iteration) and `EGraph::query` was a thin wrapper that just converted those rows into named HashMaps. With the wrapper in place, nothing benefits from the intermediate type — `EGraph::query` now does the rust_rule + ruleset dance directly and builds the HashMaps from the rust_rule callback. What's deleted: - `prelude::query` free function - `prelude::QueryResult` struct (and its `iter()` / `any_matches()`) - `tests/api_query::legacy_query_still_works` — the test was the only remaining external user - prelude module doc "Legacy" section that pointed at it Doctests on `rule`, `rust_rule`, and the cfg(test) module's own tests are rewritten to use `egraph.query(...)` directly. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com> * fix: read-only table_rows + tighter query under proofs + real arity Four related correctness fixes from the doc audit: 1. `EGraph::table_rows` used to call `self.update(|fs| ...)`, which refuses under proofs. But table_rows is read-only — it should succeed. Now goes directly through the backend's read path without the write-flush dance. 2. `EGraph::query` previously surfaced its proof-mode failure through the inner `rust_rule` call, so the error mentioned the wrong API ("rust_rule" instead of "EGraph::query"). Now checks proofs upfront. 3. `EGraph::query` leaked its temporary ruleset + rule on the error path (any failure between `add_ruleset` and the final cleanup). Now teardown happens unconditionally via a closure. 4. `check_arity` was gated on `input_sort_names().is_empty()` — if a table was registered without sort metadata, arity checking silently skipped. Replaced with `TableAction::input_arity()` which derives input count from `table_math.func_cols - 1` (always known). Also added the missing arity check to `Read::lookup_raw`, which was the one method that didn't have it. Tests in `tests/api_proofs.rs`: - `query_with_proofs_enabled_errors_with_query_api_name` — regression for #2, asserts the error names `EGraph::query`. - `table_rows_works_under_proofs` — regression for #1. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com> * docs: stale comments around the new API surface Fixes the doc-audit findings that were just wrong rather than stale: - `tests/api_query.rs` comments on tests 2 and 3 still described the old `query::<R>` generic signature (returning `Vec<(i64,)>` and `Vec<()>`). Updated to describe the `Vec<HashMap<String, Value>>` shape and the `.len()`-is-match-count behaviour for zero-var. - `tests/api_query.rs:138` had `let _: Value = row[2];` as a "verify we get back a Value" — a no-op binding. Replaced with a comment. - `tests/api_const_fold.rs` module doc claimed to exercise `rust_rule_full`, `Read::lookup_raw`, and `Read::contains` — none of which the test actually uses. It also referenced a "`:cost` table" that never existed. Both fixed. - `egglog-bridge`'s `update` doc still talked about "typed state wrappers"; renamed to "the egglog crate's `Read`/`Write` capability wrappers" to match the post-Id-revert reality. - The `Read` trait summary said "Returns `None` if the row is absent — never inserts," which only applies to the single-row reads. `table_rows` / `table_size` / `table_sizes` walk current contents. Split the summary. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com> * tests + minor cleanups from the doc audit Tests added: - `test_wrong_arity_on_add_errors` — arity validation on Write::add, paralleling the existing set check. - `test_wrong_arity_on_lookup_raw_errors` — locks in the new arity check on `lookup_raw` from the previous commit. - `test_union_same_value_is_noop` — union(x, x) should not error. - `test_table_rows_on_empty_constructor` — verifies the empty-table edge case. Renamed `query_missing_table_errors` (in api_query.rs) to `table_rows_missing_table_errors` — the test exercises `table_rows`, not `query`, so the previous name was misleading. Cleanups: - `Read::table_rows` pre-sizes the output `Vec` with the table's row count to avoid Vec growth on large tables. - Stray trailing blank line inside `ApiError` enum. - Stray blank line before the `impl EGraph` block's closing brace. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com> * rebase fixups against latest main After rebasing against origin/main (which had picked up PR #889's unstable-fn dispatch refactor and PR #895's FullState exposure): - Drop the `EGraph::with_full_state` PR #895 added — superseded by our `EGraph::update` from this PR. Our `update` returns `Result<R, Error>` and includes the proof-incompatibility check, so the old `with_full_state` is now redundant. - Pull in `resolve_function_container_target_with_context` from main — main's `unstable-fn` dispatch sites now go through this helper, but `git rebase -X theirs` preferred our older callers without realising the helper was new in main. - Switch the `clear_function` integration test in `tests/integration_test.rs` from the (now `pub(crate)`) `EGraph::lookup_function` to the public `Read::lookup_raw` via `update`. Keeps the legacy private read off the public surface. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com> * drop V: BaseValue from Read::lookup; return Option<Value> Two problems with the old shape: 1. `Read::lookup<K, V: BaseValue>` could only return base values, so you couldn't lookup a function whose output is an eclass or a container — you had to fall back to `lookup_raw`. 2. It was the only Read method with a typed extraction. `eclass_of`, `contains`, `lookup_raw`, `table_rows`, `query` all return raw `Value`s and let the caller convert. The asymmetry was a holdover from an earlier draft. Both fixed: `Read::lookup<K: IntoRow>(name, key) -> Result<Option<Value>, Error>`. Callers that want an `i64` (or other base) do `.map(|v| fs.value_to_base::<i64>(v))` themselves — same pattern as `lookup_raw`, `eclass_of`, and the `query` HashMap accessors. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com> * drop IntoRow::arity; check row.len() after into_values The arity method existed only to support a "fail fast on wrong column count before converting" pattern. The wasted-on-mismatch work is small (a handful of base-value internings for typo cases), so the convert-then-check ordering is fine. This removes: - `IntoRow::arity(&self)` method from the trait - The arity impls on `RawValues`, the single-column blanket, and the tuple macro - The `[$(stringify!($name)),+].len()` arity-counting trick in the tuple macro — only used by the removed method The Read/Write methods now compute arity as `row.len()` after calling `into_values`, swapping the order with the existing `check_arity` call. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com> * CHANGELOG: collapse PR #901's entry to a single bullet The previous entry sprawled across 15 sub-bullets enumerating every method. The actual user-visible delta is "you can now drive the e-graph by name from primitive bodies and rust_rule callbacks (and from outside a rule via update)" — one paragraph fits. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com> * constructor/function split + rename row traits to *Values Two changes in one: 1. Constructor / function split in the iteration API. `table_rows` was polymorphic over subtype — you'd write `table_rows::<(i64, i64)>("f")` for a function and `table_rows::<(i64, Value)>("Cons")` for a constructor and the row-shape difference was implicit. Replace with two subtype-checked methods that make the distinction structural: fn constructor_enodes(&self, name) -> Result<Vec<(Vec<Value>, Value)>, Error> fn function_entries (&self, name) -> Result<Vec<(Vec<Value>, Value)>, Error> `constructor_enodes` errors with WrongSubtype on a function and vice versa. Each returns `(inputs, output)` per row: for constructors `output` is the eclass id; for functions it's the stored value. Inputs are raw `Value`s — caller does `value_to_base::<T>` or `value_to_container::<T>` per column. Top-level `EGraph::constructor_enodes` / `EGraph::function_entries` are read-only wrappers (work under proofs). 2. Rename the row-encoding traits to remove "Column" and "Row" terminology: IntoColumn → IntoValue // open trait, users can impl FromColumn → FromValue // open trait, users can impl IntoRow → IntoValues // sealed FromRow → FromValues // sealed The IntoValue / FromValue traits used to be sealed for no good reason — they're now open, so users implementing custom sorts can add impls for their own Rust types and have those types flow through `set` / `add` / `function_entries` / `query` naturally. The Values traits stay sealed (row shape is fixed: tuples up to arity 8, plus `RawValues` / `Vec<Value>` / `()` escape hatches). Tests in `tests/api_query.rs` rewritten around the new methods; `tests/api_const_fold.rs`, `tests/api_fact_ops.rs`, `tests/api_proofs.rs` updated to match. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com> * remove Read::lookup_raw from the public surface It was the one remaining method that didn't fit the subtype split: generic over function/constructor, returning a `Value` whose meaning depends on the table. Useful only for primitive bodies that receive raw `&[Value]` from the matcher and want to do an ad-hoc lookup. Callers go through the new pattern instead: `RawValues(args.to_vec())` wrapped around the raw slice plus the subtype-appropriate method — `lookup` for functions, `eclass_of` for constructors. Callers updated: - `tests/typed_primitive.rs`: ReadLookup primitive's apply body - `tests/integration_test.rs`: clear_function test — switched to `eclass_of` since `Num` is a constructor - `tests/api_fact_ops::test_wrong_arity_on_lookup_raw_errors`: dropped - `benches/rust_api_benchmarking.rs`: stale comment Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com> * trim unnecessary bridge changes Two bridge changes that reverted to pre-PR shapes: 1. Bridge's `EGraph::update` / `Database::update` renamed back to `with_execution_state`. The shorter name shadowed the user-facing `egglog::EGraph::update` and confused readers (both took different closure shapes — FullState vs ExecutionState). Now the bridge uses `with_execution_state` (the original name pre-rename) and only the user-facing `egglog::EGraph::update` is called `update`. 2. Drop `FunctionConfig.sort_names` / `FunctionInfo.sort_names` / `TableAction.sort_names` / `input_sort_names()` / `output_sort_name()` from the bridge entirely. These were a hook for the parked dynamic-typing work and nothing reads them at runtime now. The arity check uses `TableAction::input_arity()` (derived from `table_math.func_cols`) which doesn't depend on sort names being populated. `TableKind` stays — it's used by every subtype check in `Read` / `Write` methods and is the clean abstraction for what the bridge already tracks via `default_val`. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com> * docs: flesh out the prelude module doc; brief pointer in lib.rs Reworked the prelude module doc as the main place to read about using egglog from Rust: - Intro: most workflows are an egglog program parsed via `parse_and_run_program`; Rust escapes are for driving the DB directly or for rust_rule callbacks. - Worked example: `eg.update(|fs| fs.set(...))` + read in a separate closure (writes don't flush inside the same closure). - Per-category bullets with links: adding/reading facts (Read/Write), iterating (function_entries / constructor_enodes), querying (EGraph::query), rules (rule / rust_rule / rust_rule_full), and extending egglog (custom sorts, custom primitives). - Caveat section spelling out the type-unsafety at the column level (`Value`s for different sorts are indistinguishable; union / set / add do not check column-sort matching; arity + subtype are checked). `src/lib.rs`'s "Using egglog from Rust" section is now a one-paragraph pointer at the prelude. The details that used to be duplicated between the two live in the prelude only. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com> * docs: restore lib.rs Rust intro; emphasize parse_and_run_program Restore the original "We encourage using the egglog language as much as possible, even from Rust" framing and finish the trailing "....". Calls out the recommended path explicitly: - Default: write your program as egglog text, run via parse_and_run_program. - Reach for EGraph::update only when reads/writes from Rust are really necessary. - rust_rule / rust_rule_full are the rule-RHS escape hatch. Details still live in the prelude module doc. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com> * docs: mention custom primitives in lib.rs intro The previous version covered the "rules whose RHS needs Rust logic" escape hatch (rust_rule) but not the parallel one for adding new functions callable from egglog expressions — implementing a custom Primitive and registering with add_*_primitive (or the add_primitive! macro for the common case). Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com> * docs: cover extraction in the Rust-API intro Two pointers to extraction added: - lib.rs intro: brief mention that `EGraph::extract_value` (and `_with_cost_model` for custom costs) is the way back out, with a link to the `extract` module. - prelude.rs: new "Extracting terms" section listing the three EGraph helpers (`extract_value`, `extract_value_with_cost_model`, `extract_value_to_string`) and pointing at the `extract` module for the full API surface. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com> * docs: spell out the current eval_expr + extract_value pattern Adds the working today pattern for "let-bind a global, extract the term" to both layers of docs: - lib.rs intro: one-line update — let-bind, resolve with eval_expr, then extract_value. - prelude.rs Extracting section: a runnable example using exprs::var("$root") + eval_expr + extract_value. Also reflects this in the PR description follow-up: extract_global is still parked as a future convenience method, but the docs no longer imply there's no way to do it today. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com> * docs: move lib.rs module doc into src/lib.md Markdown lives better in `.md`. The crate-level intro (egglog blurb, Rust-API overview, tutorial links) is now a single `#![doc = include_str!("lib.md")]` in `src/lib.rs`, with the content in the adjacent `src/lib.md`. Behavior is the same — `cargo doc` picks up `lib.md` as the crate's front page; intra-doc links resolve against the egglog crate as they did before. The runnable Rust-API doctest (let-bind + eval_expr + extract_value) stays in `src/prelude.rs` where it can rely on the more permissive markdown-block environment. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com> * docs: tutorial up, Command pointer, prelude case 3, drop intern_container src/lib.md: - Moved the Tutorial section above "Using egglog from Rust" — that's where most newcomers should go first. - New "Language reference" section pointing at the [`Command`] enum (alias for [`ast::GenericCommand`]) and explaining the convention: one variant per top-level egglog command, each with its own doc-commented syntax/semantics. The docs live on `GenericCommand`; the alias just delegates. src/prelude.rs: - Bumped "Two cases" to "Three cases", adding custom primitives alongside `update` and `rust_rule` as a distinct Rust-interop path. Already detailed below in "Extending egglog" — the intro now flags it. src/lib.rs: - Drop `EGraph::intern_container`. It was a pure alias of `container_to_value` with zero callers in src/, tests/, or benches/. Also a quick check while I was poking around: `EGraph::lookup_function` (pub(crate)) is still used by `src/proofs/proof_extraction.rs:83`, so we can't remove it without porting that callsite. Worth a follow-up. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com> * port the proof-extraction lookup off lookup_function; drop the helper The proof system has one read of an internal proof table. Going through `EGraph::update` doesn't work because update refuses under proofs (by design — closures could stage writes that bypass the proof pipeline) and the proof system itself runs under proofs. Refactor: extract the body of `EGraph::update` into a `pub(crate) fn update_unchecked`. `update` is now a thin wrapper that does the proofs check and delegates. Internal callers that need the same machinery without the check (`constructor_enodes`, `function_entries`, `proof_extraction`) call `update_unchecked` directly. Same flush-at-end behavior as `update`; the flush is a no-op on read-only closures. Proof_extraction now reads via: let proof_value = self.egraph.update_unchecked(|fs| { fs.lookup(&proof_function_name, RawValues(vec![witness_value])) })?.unwrap_or_else(|| panic!(...)); `EGraph::lookup_function` had only this one caller and is now gone. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com> * port vec/multiset union primitives off new_union_action The `vec-union` and `multiset-union-values` primitives each held their own `UnionAction` and called it via the privileged `raw_exec_state()` seam — but they already see a `WriteState` and the public `Write::union(x, y)` method does the same thing. // before let action = self.action; let es = state.raw_exec_state(); for (l, r) in zip(left, right) { action.union(es, l, r); } // after for (l, r) in zip(left, right) { state.union(l, r).ok()?; } Drops: - `Union::action: UnionAction` field on vec.rs - `UnionValues::action: UnionAction` field on multiset.rs - `EGraph::new_union_action()` (pub(crate)) — no longer has callers - the `use egglog_bridge::UnionAction` imports vec.rs no longer needs the `Internal` trait either (it was only there for `raw_exec_state`); multiset.rs still uses it elsewhere. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com> * drop EGraph::function_entries / constructor_enodes; go through Read Both methods were thin top-level wrappers over the `Read` trait versions. Now that every other "read the e-graph" operation goes through the wrappers (`eg.update(|fs| fs.lookup(...))` etc.), keeping a separate top-level path for iteration was inconsistent — and it relied on `update_unchecked` to skip the proofs check, which let proofs-mode callers iterate via the top-level method but not via `update`. Asymmetric. Drop both. Callers now use `eg.update(|fs| fs.function_entries(...))` / `eg.update(|fs| fs.constructor_enodes(...))` like everything else. Proofs-mode users can't iterate tables this way — `update` refuses under proofs — and that's now visible at the API. Also: - Switch the `query` method's `std::collections::HashMap` paths to imported `HashMap` (matches the rest of the codebase, which uses `crate::util::HashMap` via the blanket `use util::*;`). - Collapse a nested `if let Some(ruleset_obj) = ... { if let Ruleset::Rules(rules) = ... { ... } }` into a single pattern. - Drop the `tests/api_proofs::read_only_iteration_works_under_proofs` test — exercised the special-case top-level path; that path is gone. - Drop a stale "Top-level convenience versions live on EGraph" line from the prelude module doc. cargo clippy is now clean. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com> * drop EGraph::function_for_each; port callers to Read::constructor_enodes Also clean up small nits surfaced by clippy: - nil.clone() on Copy Value -> bare nil - redundant closure || fib_setup() -> bare fn pointer - stale doc reference on update_unchecked * make fixnits: rustfmt + clippy-fix sweep * resolve copilot review nits - src/lib.rs: stranded `Run a closure with full read-write access` doc comment was sitting on `set_report_level` after the `with_full_state` removal; replace with a doc that actually describes the method. - src/api/mod.rs: `FromValues` tuple impl was silently dropping trailing columns; assert the iterator is exhausted after decoding so a row that's longer than the tuple panics with a clear message instead of looking like a valid result. * Apply suggestions from code review Co-authored-by: Yihong Zhang <yz489@cs.washington.edu> * cosntructor_enodes much faster * change to iter and smallvec * Apply suggestions from code review Co-authored-by: Yihong Zhang <yz489@cs.washington.edu> * respond to review: TableRows rename, uniform top-level scan API, tidy-diff-docs skill - Rename the public table-snapshot type `Rows` to `TableRows` to avoid colliding with `core-relations::Rows`. - Expose `EGraph::function_entries` / `EGraph::constructor_enodes` as top-level table scans mirroring the `Read` trait (thin `update_unchecked` wrappers, read-only so cheap and proof-safe). These replace the callback-based `function_for_each`; `lookup_function` stays deleted. - Add `TableRows::iter_with_subsumption` so the row snapshot can report subsumption — the one piece of info the old callback exposed that the `(inputs, output)` scan dropped. - Add the repo-level `tidy-diff-docs` skill that trims implementation details and duplicate text from doc/code comments in a diff, and reference it from CLAUDE.md. Co-authored-by: Yihong Zhang <yz489@cs.washington.edu> Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> * api: stream constructor_enodes/function_entries via callbacks; &self top-level reads Replace the TableRows snapshot (which materialized the whole table into one buffer via scan_all) with a streaming callback API, addressing the eager-copy concern. Rows now stream in 32-row batches through the bridge's for_each_while. - New purpose-built row types: `Enode { children, eclass, subsumed }` for constructor_enodes and `FunctionEntry { inputs, output, subsumed }` for function_entries, replacing the raw split-it-yourself row. - Add `*_while` early-exit variants (closure returns bool) on both the `Read` trait and `EGraph` — a new capability the old function_for_each lacked. - Make the top-level `EGraph::{constructor_enodes,function_entries}` (and the `_while` forms) take `&self` instead of `&mut self`, backed by a new `EGraph::read(|rs| ...)` read-only mirror of `update`. A pure read never flushes, so the callback may call other `&self` methods like `value_to_base` directly. - Rename bridge `FunctionRow` -> `ScanEntry` (still pub for extract.rs; no longer re-exported from egglog so `egglog::FunctionEntry` is unambiguous). Drop the now-unused `RowScan` / `TableAction::scan_all`. - Update call sites (tests, bench), prelude docs, and the tidy-diff-docs skill. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> * extract api fix --------- Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com> Co-authored-by: Yihong Zhang <yz489@cs.washington.edu>

* Add `:unsafe-seminaive` rule option for arbitrary RHS reads `:naive` lets a rule's RHS read the database (read-primitives) by widening its primitive contexts from `Pure`/`Write` to `Read`/`Full`, but it pays for that by giving up seminaive (delta) evaluation — the body is matched against the whole database every iteration. `:unsafe-seminaive` decouples the two: the rule is still evaluated seminaive-ly, but its query/action are compiled with the permissive `Read`/`Full` contexts and the "no function lookups in actions" typecheck is skipped. So the RHS can perform arbitrary database reads — read-primitives *and* function-table lookups — with seminaive performance. Mechanics: - `GenericRule` gains an `unsafe_seminaive` flag (the `:unsafe-seminaive` rule option; round-trips through Display/parser). - `typecheck_rule` and `add_rule` compute `context_seminaive = seminaive && !rule.unsafe_seminaive` and use that for primitive-context selection, while evaluation still uses `seminaive`. `check_lookup_actions` is gated on `!unsafe_seminaive`. It is **unsafe**: a read on a seminaive rule's RHS observes the database mid-iteration (non-monotonic), so results can depend on evaluation order — the caller takes responsibility. The term/proof encoding can't represent such rules, so `command_supports_proof_encoding` rejects them (`UnsafeSeminaive`). Includes `tests/unsafe-seminaive.egg` (a function lookup in the RHS, accepted on the default backend, rejected under term-encoding/proofs). * proofs: fetch eq-sort var term_proofs via action lookups, tag :unsafe-seminaive The proof encoder injected a body fact `(= p (term_proof var))` for every eq-sort variable in every instrumented rule, only to bind that variable's proof for assembling the rule proof. Every eq-sort term has its term_proof set at constructor-creation time, so the proof is always present when the rule fires — the join never filters; it's one extra join per eq-sort body variable, per rule. Move those fetches into the rule's actions as `(let p (term_proof var))` and tag the generated rule `:unsafe-seminaive` (keeps delta evaluation, permits the RHS lookup). This is the motivating use of the new option. instrument_facts returns the action-side lookups separately; query-only callers (run :until, check) keep the body form. Also reword the unsafe doc to: a seminaive RHS read observes the database mid-iteration, so it won't be re-evaluated if the data changes. Proof + proof_testing variants pass (naturals/combinators/integer_math/ fibonacci_demand/eqsat). * test: read-primitive (FullPrim) in an :unsafe-seminaive RHS Adds tests/unsafe-seminaive-read-prim.egg using the FullPrim `unstable-multiset-fill-index` in a rule's RHS. It needs the Full primitive context, which the default seminaive action context (Write) doesn't admit — without :unsafe-seminaive the call doesn't even resolve. Covers the context-widening arm (the existing test covers the function-lookup arm). * Fix CI: collapse clippy nested-if; add new tests to proof_unsupported snapshot - proof_encoding_helpers: collapse `if let … { if … }` into a let-chain (clippy::collapsible_if, -D warnings on rust 1.91). - Update the proof_unsupported_files snapshot to include unsafe-seminaive{,-read-prim}.egg (they're :unsafe-seminaive, so not proof-supported). * Drop lookups_to_action: query-only callers don't build proofs instrument_facts always emits eq-sort term_proof fetches as action-side lookups now. The only callers that previously passed false (run :until, check) discard both the lookups and the proof, and the term_proof body-joins they emitted were no-ops anyway (every eq-sort term always has a proof, so the join never filters). Removing the flag deletes those dead joins from those queries too. * Rename BackendRule.seminaive -> context_seminaive (Copilot review) The field selects the primitive context (Pure/Write vs Read/Full), not the evaluation strategy. add_rule now passes context_seminaive (which is false for :unsafe-seminaive rules even though they evaluate seminaive-ly), so the old name was misleading. Rename + clarify the doc. * :unsafe-seminaive/:naive: collapse to one RuleEvalMode field, error on conflict Address review feedback (Saul): replace the `naive` / `unsafe_seminaive` booleans on `GenericRule` with a single `RuleEvalMode { Seminaive | Naive | UnsafeSeminaive }`. The parser now stores at most one mode and errors if both `:naive` and `:unsafe-seminaive` are given. Context selection (Read/Full iff `!seminaive || uses_read_contexts()`) is preserved exactly. Adds a fail-typecheck test asserting the mutual-exclusivity parse error. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> * proofs: preserve user :naive through encoding; test against :unsafe-seminaive The proof encoder reads each eq-sort body variable's term_proof from the RHS via an :unsafe-seminaive action-side lookup, which observes the database mid-iteration. - Fix: instrument_rule now preserves a user rule's `:naive`. Previously it chose the eval option purely from whether the rule had RHS reads, so a user `:naive` rule silently became seminaive (no reads) or was downgraded to `:unsafe-seminaive` (with reads). Test: proof_encoding_preserves_naive. - Gate the "no function lookups in actions" check on `!uses_read_contexts()` instead of `!= UnsafeSeminaive`, so `:naive` (which also widens the action context to Full) permits RHS function-table lookups too — `:naive` and `:unsafe-seminaive` then differ only in evaluation strategy. Positive test: tests/naive-action-lookup.egg. - Address Yihong's concern: unsafe_seminaive_matches_naive runs a hardcoded handful of eq-sort files through the encoder twice (default vs a test-only `force_proof_naive` knob that annotates RHS-reading rules :naive) and asserts identical databases. - Lift files.rs's snapshot filter into CommandOutput::snapshot_stable_under_proof_encoding, shared by the new test and the shared-snapshot harness. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> * typecheck: gate action-lookup check on effective context, not eval_mode CodeRabbit review: when the EGraph is non-seminaive (`global_seminaive == false`), every rule is compiled with `Context::Full`, so function lookups in actions are sound — but the check gated on `eval_mode.uses_read_contexts()` still rejected them for default-mode rules. Gate on `read_contexts` instead, matching the backend's context selection. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> * review: clarify naming/logic around read contexts (Saul) Addressing Saul's review comments: - Inline the trivial `uses_read_contexts` helper at its two call sites as a direct `matches!(eval_mode, Naive | UnsafeSeminaive)`, and remove the method (he asked to express it directly). Kept `is_naive` (clearly named). - Simplify `typecheck_rule`'s context selection, dropping the intermediate `seminaive` local: `!global_seminaive || matches!(eval_mode, ...)`. - Rename `check_lookup_actions` -> `check_no_function_lookups_in_actions`. - Invert `BackendRule`'s `context_seminaive` field to `requires_read_context` (true = widen to Read/Full), removing the confusing double negative. Flipped all six call sites and the two context-selection branches to match. - Trim the verbose `RuleEvalMode` and `if !read_contexts` docs. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> * review: condense changelog and fix stale Full-context comment (CodeRabbit) - Condense the `:naive` / `:unsafe-seminaive` changelog bullets into one. - `prelude.rs`: `:unsafe-seminaive` also selects `Context::Full`, so the "only available in :naive" comment was stale; note this helper deliberately keeps the safe whole-database `:naive` path. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> * Avoid redundant proof merge rows * Update proof encoding snapshot * Handle proof-mode primitive and macro regressions * Support eq-sort primitive fact proofs * Avoid cloning type info for proof macros * Handle eq-container fact proof lookups * Name-indexed read/write API on Read/Write traits + EGraph::update (egraphs-good#901) * api: typed read/write surface on Read/Write traits + EGraph::with_full_state Single source of truth for the typed user API: methods live on the Read and Write traits, the same surface a rust_rule / rust_rule_full callback already sees. Outside a rule, EGraph::with_full_state(|fs| ...) hands out the same FullState handle. // Inside a rule callback (WriteState / FullState): unchanged. ws.set("f", (1_i64,), 42_i64); ws.add_node("Cons", (1_i64, nil)); // Outside a rule: with_full_state batches writes — one flush // happens after the closure returns, so split write/read across // calls for the read to see the write. eg.with_full_state(|mut fs| fs.set("f", (1_i64,), 42_i64)); let v: Option<i64> = eg.with_full_state(|fs| fs.lookup::<_, i64>("f", 1_i64)); // Constructors mint or look up an eclass. The returned Value is // the eclass id; the Rust API does not currently tag Values with // their egglog sort. let nil = eg.with_full_state(|mut fs| fs.add_node("Nil", RawValues(vec![])).unwrap()); // Pattern queries stay on EGraph — they compile a one-shot rule. let rows: Vec<(i64,)> = eg.query_pattern(vars![x: i64], facts![(R x)])?; // Base-value interning stays on EGraph. let v = eg.intern::<i64>(7); let n: i64 = eg.extract(v); Read trait gains lookup<K, V>, eclass_of<K> (returns Option<Value>), contains<K>, plus lookup_raw (untyped escape hatch). Write trait gains a typed remove<K>; its set/add_node already existed. Underpinned by `crate::api`: - IntoRow / IntoColumn for input rows (tuple of base values, single value, or RawValues escape hatch). - FromRow / FromColumn for output rows (symmetric). The Rust API does not currently track egglog sort identity on Values at the Rust type level. A Value returned by one constructor is indistinguishable from one returned by another; callers track sort themselves. Subtype safety: set on a constructor, add_node on a function, lookup on a constructor, eclass_of on a function all PANIC with a message naming the offending table — these are programmer bugs, not runtime input errors. The check is plumbed through a new `egglog_bridge::TableKind` enum on TableAction (Function vs Constructor), derived from the function's default-value kind at table registration time. API audit: no public method anywhere in the egglog crate now takes a TableId, FunctionId, or ExternalFunctionId. The user-facing surface is strings + Value end-to-end. Read::table_name(TableId) (the last leak) is dropped — it had zero callers. Bench evidence (benches/rust_api_benchmarking.rs sweep n_dummy_funcs): 100k inserts in one rule fire, 2000 dummy tables: 7.41 ms vs 7.34 ms at 0 dummy tables — ~1% overhead from the per-call HashMap lookup. Hot-path read bench (50k matches × set + lookup_raw + union) flat across 0/200/2000 dummy funcs. Strings are fast enough; no need to keep a public FunctionId for performance. `with_full_state` mirrors PR egraphs-good#895's helper of the same name; if egraphs-good#895 merges first this commit's body can drop the duplicate. Refs egraphs-good#745, egraphs-good#751, egraphs-good#895. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * api: move table_rows to the Read trait Previously `EGraph::table_rows` was a top-level method; now it's `Read::table_rows`, accessible from `ReadState` / `FullState` — so `add_rust_rule_full` callbacks can iterate tables alongside the other name-indexed methods. Adds `TableAction::for_each` / `for_each_while` in egglog-bridge, mirroring the existing `EGraph::for_each` but reaching the table through an `ExecutionState` (the same pattern as the existing `TableAction::lookup` / `row_count`). `EGraph::table_rows` is kept as a thin convenience wrapper that delegates to `with_full_state`, so top-level callers don't change. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com> * api: clear errors when used with proofs + constant-folding case study The new Rust API surface was silently broken when proofs were enabled: - `rust_rule` / `rust_rule_full` register an auto-generated primitive with `validator: None`, which the proof typechecker doesn't know about. Calling these under `EGraph::new_with_proofs()` previously errored with "Unbound function `@rust_rule_prim_3`" — a leaky internal name with no hint at the real problem. - `EGraph::with_full_state` writes flush directly into the backend, bypassing the proof-encoding pipeline. The proof checker had no record of those updates, so any rule derivation resting on them would have been unverifiable. Both now check `EGraph::are_proofs_enabled()` upfront and return the new `Error::ProofsIncompatibleApi { api, reason }` with a clear explanation. Three tests in `tests/api_proofs.rs` lock in the behavior. `with_full_state`'s signature tightened from `FnOnce(FullState) -> R) -> R` to `FnOnce(FullState) -> Result<R, Error>) -> Result<R, Error>` — collapsing the proofs-check error path with the closure's error path, so callers stay one `?` deep. All 39 existing callsites already returned `Result` from their closure and need no changes. Plus `tests/api_const_fold.rs` — a constant-folding case study that exercises the whole API end-to-end: `with_full_state` to build a `(Add (Num 2) (Add (Num 3) (Num 4)))` expression with `add_node`, a `rust_rule` that pattern-matches `(Add (Num a) (Num b))` and uses `add_node` + `union` to fold, then `table_rows` and `eclass_of` to verify the root collapses to `(Num 9)`. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com> * docs: drop stale 'typed user API' language, refresh changelog After the Id-based dynamic-typing work was reverted (preserved at tag oflatt-dynamic-type-checks), 'typed user API' / 'typed Rust API' / 'typed methods' read as if the API still carries compile-time-typed eclass wrappers. It doesn't — the surface is name-indexed Read / Write methods over plain `Value`s, with column-sort validation as the only runtime type check. Renamed to plain 'API' / 'Read/Write methods' / 'Rust API' throughout. Also: - Drop the stale 'BaseSortName was previously re-exported here' comment in src/lib.rs (intern/extract are long gone). - Drop the stale `table_lookup` reference from the exec_state module doc (the method no longer exists). - CHANGELOG entry for `table_rows` corrected to reflect the `Read::table_rows` primary location with `EGraph::table_rows` as the thin top-level wrapper, plus the new proof-mode-compatibility errors and the constant-folding case study. - 'typed primitive surface' (PurePrim / WritePrim / ReadPrim / FullPrim) kept as-is — that 'typed' refers to the capability-typed primitive contexts (issue egraphs-good#772), not to the eclass typing this PR walked back. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com> * rename with_execution_state -> update Cross-crate rename of the `Database::with_execution_state` / `egglog_bridge::EGraph::with_execution_state` closure-taking method to just `update`. Same behavior; less verbose at the 9 callsites (`db.update(|state| ...)` reads cleaner than `db.with_execution_state(|state| ...)`). The closure can do reads or writes via the `&mut ExecutionState`, but the common use is staging writes that flush on `flush_updates` — the shorter name matches that primary intent. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com> * rename EGraph::with_full_state -> EGraph::update; drop stale comments Cross-PR rename to match the bridge-level `egglog_bridge::EGraph::update` that just landed. The two live in different scopes (`egglog::EGraph` user-facing, `egglog_bridge::EGraph` internal), so the shared name doesn't collide for anyone — and reads more cleanly against the contrast egg sets: - egg: `egraph.add(expr)` / `egraph.union(a, b)` / `egraph.rebuild()` - egglog (now): `egraph.update(|fs| fs.add_node(...))` / `egraph.update(|fs| fs.union(a, b))` — one entry point, all mutations batched and flushed at the end of the closure. Also drop the "earlier revisions" comment in `benches/rust_api_benchmarking.rs` — references to prior iterations of the bench code don't help future readers; they read as a half-written changelog stuck in the source. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com> * rename Write::add_node -> Write::add Symmetric with the just-renamed `EGraph::update`, and closer to egg's `EGraph::add(expr)`: fs.add("Cons", (1_i64, nil)) reads as cleanly as egraph.add(expr) does in egg. The `_node` suffix was redundant — the only thing `Write::add` can add IS a constructor / relation row, by trait signature. (TermDag's internal `add_node` for `Term` is unaffected; that's a separate, lower-level method that does add a term node, not a row.) Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com> * drop per-column sort checking; closes the 1.5x insert regression The sort checking added in the original Stage-1 work was inconsistent with the rest of this PR: it would catch a `String` literal passed where an `i64` was expected (a typo Rust mostly catches at compile time anyway), but it couldn't catch a `Math` eclass passed where a `List` eclass was expected — both are bare `Value`s with no sort metadata to compare. That's the type-confusion this PR's predecessor (the parked dynamic-type-checks tag) was built to catch, and we don't have it here. So the partial sort check was paying a 1.54x cost on `insert_loop` (measured: 77 us baseline -> 119 us with checks) to protect against a narrower class of typos than the API's signature already protects against. Drop it. What's removed: - `ApiError::WrongColumnSort`, `ApiError::WrongOutputSort` - `ColumnSort` enum (was only consumed by the dropped checks) - `IntoColumn::column_sort()` (sort tag no longer needed) - `IntoRow::column_sorts()` replaced by `IntoRow::arity()` — we still want arity validation, that's cheap and catches a different class of typo (passing a 2-tuple to a 3-column table) - `check_input_sorts`, `check_output_sort` collapsed into a single `check_arity` helper - `tests/api_fact_ops::test_wrong_column_sort_errors` and `test_wrong_output_sort_errors` What stays: - `WrongArity`, `WrongSubtype`, `MissingTable` errors and tests - `FunctionConfig.sort_names` plumbing on the bridge side, as a future hook for the parked dynamic-typing work Bench after this change (median, 10 samples): | bench | main | this PR | |--------------------------------|-----------|------------| | insert_loop ops1000_funcs200 | 77.35 us | 82.79 us | 1.07x noise | tableaction_hot_path funcs200 | 5.039 ms | 4.297 ms | 0.85x faster | fib rule_run_1000 | 30.12 ms | 29.79 ms | 0.99x | match_overhead | 2.192 ms | 2.169 ms | 0.99x | match_with_serialize | 44.71 ms | 43.37 ms | 0.97x Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com> * docs: CHANGELOG matches the dropped sort-checking `WrongColumnSort` and `WrongOutputSort` are gone; per-column sort checking is not done. `IntoColumn::column_sort()` is gone; `IntoRow::column_sorts()` became `IntoRow::arity()`. Update the changelog entries to match what's actually in the PR. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com> * docs: trim changelog, drop stale "sort checking" mentions CHANGELOG: removed two entries that were too granular for a public changelog: - proof-mode-incompatibility errors (one error variant + signature tightening — implementation detail of how proofs interact with the new API, not its own feature) - constant-folding case study in tests/ (test coverage isn't a changelog entry) Also folded WrongSubtype / WrongArity / MissingTable, table_rows, and query into the main "name-indexed API" bullet — they belong with the API description, not as separate top-level items. Also picked up three stale references the doc audit caught: - `Read::lookup_raw` doc no longer says "Skips sort checking" — there is no sort checking to skip. - `egglog_bridge::FunctionConfig.sort_names` doc no longer mentions the deleted `ColumnSort::Unchecked` variant or claims runtime validation. It's a hook for future dynamic-typing work. - Two test functions in `api_fact_ops.rs` had `add_node` in their names — renamed to match the actual API method (`add`). Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com> * drop ExecutionState from the public re-export `ExecutionState` was being re-exported from `core_relations` via `pub use core_relations::{BaseValue, ContainerValue, ExecutionState, Value}`, but nothing user-facing actually requires it: every API hands out a `PureState` / `WriteState` / `ReadState` / `FullState` wrapper around it. Make it crate-internal — `core_relations::ExecutionState` is still reachable for anyone who really wants the raw type via the bridge. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com> * EGraph::query returns Vec<HashMap<String, Value>> The R: FromRow generic on query was a complexity-for-not-much: the caller had to remember positional column order to match the vars they declared. Switch to a named-binding return: one HashMap<String, Value> per match, keyed by the variable name from vars. // before let rows: Vec<(i64, i64)> = eg.query::<(i64, i64)>(vars![x: i64, y: i64], facts![...])?; // after let rows: Vec<_> = eg.query(vars![x: i64, y: i64], facts![...])?; for m in rows { let x = eg.value_to_base::<i64>(m["x"]); let y = eg.value_to_base::<i64>(m["y"]); } Values stay raw Value — callers do their own base-value conversion via EGraph::value_to_base (or value_to_container, or whatever fits the column's sort). Generic-over-FromRow path is gone for this method; query is no longer generic. Zero-var queries still return one empty HashMap per match, so .len() reports the number of matches. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com> * drop prelude::query and QueryResult; EGraph::query is the only one The free function `prelude::query` returned a `QueryResult` struct (flat untyped Vec<Value> + per-row chunk iteration) and `EGraph::query` was a thin wrapper that just converted those rows into named HashMaps. With the wrapper in place, nothing benefits from the intermediate type — `EGraph::query` now does the rust_rule + ruleset dance directly and builds the HashMaps from the rust_rule callback. What's deleted: - `prelude::query` free function - `prelude::QueryResult` struct (and its `iter()` / `any_matches()`) - `tests/api_query::legacy_query_still_works` — the test was the only remaining external user - prelude module doc "Legacy" section that pointed at it Doctests on `rule`, `rust_rule`, and the cfg(test) module's own tests are rewritten to use `egraph.query(...)` directly. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com> * fix: read-only table_rows + tighter query under proofs + real arity Four related correctness fixes from the doc audit: 1. `EGraph::table_rows` used to call `self.update(|fs| ...)`, which refuses under proofs. But table_rows is read-only — it should succeed. Now goes directly through the backend's read path without the write-flush dance. 2. `EGraph::query` previously surfaced its proof-mode failure through the inner `rust_rule` call, so the error mentioned the wrong API ("rust_rule" instead of "EGraph::query"). Now checks proofs upfront. 3. `EGraph::query` leaked its temporary ruleset + rule on the error path (any failure between `add_ruleset` and the final cleanup). Now teardown happens unconditionally via a closure. 4. `check_arity` was gated on `input_sort_names().is_empty()` — if a table was registered without sort metadata, arity checking silently skipped. Replaced with `TableAction::input_arity()` which derives input count from `table_math.func_cols - 1` (always known). Also added the missing arity check to `Read::lookup_raw`, which was the one method that didn't have it. Tests in `tests/api_proofs.rs`: - `query_with_proofs_enabled_errors_with_query_api_name` — regression for #2, asserts the error names `EGraph::query`. - `table_rows_works_under_proofs` — regression for #1. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com> * docs: stale comments around the new API surface Fixes the doc-audit findings that were just wrong rather than stale: - `tests/api_query.rs` comments on tests 2 and 3 still described the old `query::<R>` generic signature (returning `Vec<(i64,)>` and `Vec<()>`). Updated to describe the `Vec<HashMap<String, Value>>` shape and the `.len()`-is-match-count behaviour for zero-var. - `tests/api_query.rs:138` had `let _: Value = row[2];` as a "verify we get back a Value" — a no-op binding. Replaced with a comment. - `tests/api_const_fold.rs` module doc claimed to exercise `rust_rule_full`, `Read::lookup_raw`, and `Read::contains` — none of which the test actually uses. It also referenced a "`:cost` table" that never existed. Both fixed. - `egglog-bridge`'s `update` doc still talked about "typed state wrappers"; renamed to "the egglog crate's `Read`/`Write` capability wrappers" to match the post-Id-revert reality. - The `Read` trait summary said "Returns `None` if the row is absent — never inserts," which only applies to the single-row reads. `table_rows` / `table_size` / `table_sizes` walk current contents. Split the summary. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com> * tests + minor cleanups from the doc audit Tests added: - `test_wrong_arity_on_add_errors` — arity validation on Write::add, paralleling the existing set check. - `test_wrong_arity_on_lookup_raw_errors` — locks in the new arity check on `lookup_raw` from the previous commit. - `test_union_same_value_is_noop` — union(x, x) should not error. - `test_table_rows_on_empty_constructor` — verifies the empty-table edge case. Renamed `query_missing_table_errors` (in api_query.rs) to `table_rows_missing_table_errors` — the test exercises `table_rows`, not `query`, so the previous name was misleading. Cleanups: - `Read::table_rows` pre-sizes the output `Vec` with the table's row count to avoid Vec growth on large tables. - Stray trailing blank line inside `ApiError` enum. - Stray blank line before the `impl EGraph` block's closing brace. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com> * rebase fixups against latest main After rebasing against origin/main (which had picked up PR egraphs-good#889's unstable-fn dispatch refactor and PR egraphs-good#895's FullState exposure): - Drop the `EGraph::with_full_state` PR egraphs-good#895 added — superseded by our `EGraph::update` from this PR. Our `update` returns `Result<R, Error>` and includes the proof-incompatibility check, so the old `with_full_state` is now redundant. - Pull in `resolve_function_container_target_with_context` from main — main's `unstable-fn` dispatch sites now go through this helper, but `git rebase -X theirs` preferred our older callers without realising the helper was new in main. - Switch the `clear_function` integration test in `tests/integration_test.rs` from the (now `pub(crate)`) `EGraph::lookup_function` to the public `Read::lookup_raw` via `update`. Keeps the legacy private read off the public surface. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com> * drop V: BaseValue from Read::lookup; return Option<Value> Two problems with the old shape: 1. `Read::lookup<K, V: BaseValue>` could only return base values, so you couldn't lookup a function whose output is an eclass or a container — you had to fall back to `lookup_raw`. 2. It was the only Read method with a typed extraction. `eclass_of`, `contains`, `lookup_raw`, `table_rows`, `query` all return raw `Value`s and let the caller convert. The asymmetry was a holdover from an earlier draft. Both fixed: `Read::lookup<K: IntoRow>(name, key) -> Result<Option<Value>, Error>`. Callers that want an `i64` (or other base) do `.map(|v| fs.value_to_base::<i64>(v))` themselves — same pattern as `lookup_raw`, `eclass_of`, and the `query` HashMap accessors. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com> * drop IntoRow::arity; check row.len() after into_values The arity method existed only to support a "fail fast on wrong column count before converting" pattern. The wasted-on-mismatch work is small (a handful of base-value internings for typo cases), so the convert-then-check ordering is fine. This removes: - `IntoRow::arity(&self)` method from the trait - The arity impls on `RawValues`, the single-column blanket, and the tuple macro - The `[$(stringify!($name)),+].len()` arity-counting trick in the tuple macro — only used by the removed method The Read/Write methods now compute arity as `row.len()` after calling `into_values`, swapping the order with the existing `check_arity` call. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com> * CHANGELOG: collapse PR egraphs-good#901's entry to a single bullet The previous entry sprawled across 15 sub-bullets enumerating every method. The actual user-visible delta is "you can now drive the e-graph by name from primitive bodies and rust_rule callbacks (and from outside a rule via update)" — one paragraph fits. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com> * constructor/function split + rename row traits to *Values Two changes in one: 1. Constructor / function split in the iteration API. `table_rows` was polymorphic over subtype — you'd write `table_rows::<(i64, i64)>("f")` for a function and `table_rows::<(i64, Value)>("Cons")` for a constructor and the row-shape difference was implicit. Replace with two subtype-checked methods that make the distinction structural: fn constructor_enodes(&self, name) -> Result<Vec<(Vec<Value>, Value)>, Error> fn function_entries (&self, name) -> Result<Vec<(Vec<Value>, Value)>, Error> `constructor_enodes` errors with WrongSubtype on a function and vice versa. Each returns `(inputs, output)` per row: for constructors `output` is the eclass id; for functions it's the stored value. Inputs are raw `Value`s — caller does `value_to_base::<T>` or `value_to_container::<T>` per column. Top-level `EGraph::constructor_enodes` / `EGraph::function_entries` are read-only wrappers (work under proofs). 2. Rename the row-encoding traits to remove "Column" and "Row" terminology: IntoColumn → IntoValue // open trait, users can impl FromColumn → FromValue // open trait, users can impl IntoRow → IntoValues // sealed FromRow → FromValues // sealed The IntoValue / FromValue traits used to be sealed for no good reason — they're now open, so users implementing custom sorts can add impls for their own Rust types and have those types flow through `set` / `add` / `function_entries` / `query` naturally. The Values traits stay sealed (row shape is fixed: tuples up to arity 8, plus `RawValues` / `Vec<Value>` / `()` escape hatches). Tests in `tests/api_query.rs` rewritten around the new methods; `tests/api_const_fold.rs`, `tests/api_fact_ops.rs`, `tests/api_proofs.rs` updated to match. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com> * remove Read::lookup_raw from the public surface It was the one remaining method that didn't fit the subtype split: generic over function/constructor, returning a `Value` whose meaning depends on the table. Useful only for primitive bodies that receive raw `&[Value]` from the matcher and want to do an ad-hoc lookup. Callers go through the new pattern instead: `RawValues(args.to_vec())` wrapped around the raw slice plus the subtype-appropriate method — `lookup` for functions, `eclass_of` for constructors. Callers updated: - `tests/typed_primitive.rs`: ReadLookup primitive's apply body - `tests/integration_test.rs`: clear_function test — switched to `eclass_of` since `Num` is a constructor - `tests/api_fact_ops::test_wrong_arity_on_lookup_raw_errors`: dropped - `benches/rust_api_benchmarking.rs`: stale comment Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com> * trim unnecessary bridge changes Two bridge changes that reverted to pre-PR shapes: 1. Bridge's `EGraph::update` / `Database::update` renamed back to `with_execution_state`. The shorter name shadowed the user-facing `egglog::EGraph::update` and confused readers (both took different closure shapes — FullState vs ExecutionState). Now the bridge uses `with_execution_state` (the original name pre-rename) and only the user-facing `egglog::EGraph::update` is called `update`. 2. Drop `FunctionConfig.sort_names` / `FunctionInfo.sort_names` / `TableAction.sort_names` / `input_sort_names()` / `output_sort_name()` from the bridge entirely. These were a hook for the parked dynamic-typing work and nothing reads them at runtime now. The arity check uses `TableAction::input_arity()` (derived from `table_math.func_cols`) which doesn't depend on sort names being populated. `TableKind` stays — it's used by every subtype check in `Read` / `Write` methods and is the clean abstraction for what the bridge already tracks via `default_val`. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com> * docs: flesh out the prelude module doc; brief pointer in lib.rs Reworked the prelude module doc as the main place to read about using egglog from Rust: - Intro: most workflows are an egglog program parsed via `parse_and_run_program`; Rust escapes are for driving the DB directly or for rust_rule callbacks. - Worked example: `eg.update(|fs| fs.set(...))` + read in a separate closure (writes don't flush inside the same closure). - Per-category bullets with links: adding/reading facts (Read/Write), iterating (function_entries / constructor_enodes), querying (EGraph::query), rules (rule / rust_rule / rust_rule_full), and extending egglog (custom sorts, custom primitives). - Caveat section spelling out the type-unsafety at the column level (`Value`s for different sorts are indistinguishable; union / set / add do not check column-sort matching; arity + subtype are checked). `src/lib.rs`'s "Using egglog from Rust" section is now a one-paragraph pointer at the prelude. The details that used to be duplicated between the two live in the prelude only. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com> * docs: restore lib.rs Rust intro; emphasize parse_and_run_program Restore the original "We encourage using the egglog language as much as possible, even from Rust" framing and finish the trailing "....". Calls out the recommended path explicitly: - Default: write your program as egglog text, run via parse_and_run_program. - Reach for EGraph::update only when reads/writes from Rust are really necessary. - rust_rule / rust_rule_full are the rule-RHS escape hatch. Details still live in the prelude module doc. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com> * docs: mention custom primitives in lib.rs intro The previous version covered the "rules whose RHS needs Rust logic" escape hatch (rust_rule) but not the parallel one for adding new functions callable from egglog expressions — implementing a custom Primitive and registering with add_*_primitive (or the add_primitive! macro for the common case). Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com> * docs: cover extraction in the Rust-API intro Two pointers to extraction added: - lib.rs intro: brief mention that `EGraph::extract_value` (and `_with_cost_model` for custom costs) is the way back out, with a link to the `extract` module. - prelude.rs: new "Extracting terms" section listing the three EGraph helpers (`extract_value`, `extract_value_with_cost_model`, `extract_value_to_string`) and pointing at the `extract` module for the full API surface. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com> * docs: spell out the current eval_expr + extract_value pattern Adds the working today pattern for "let-bind a global, extract the term" to both layers of docs: - lib.rs intro: one-line update — let-bind, resolve with eval_expr, then extract_value. - prelude.rs Extracting section: a runnable example using exprs::var("$root") + eval_expr + extract_value. Also reflects this in the PR description follow-up: extract_global is still parked as a future convenience method, but the docs no longer imply there's no way to do it today. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com> * docs: move lib.rs module doc into src/lib.md Markdown lives better in `.md`. The crate-level intro (egglog blurb, Rust-API overview, tutorial links) is now a single `#![doc = include_str!("lib.md")]` in `src/lib.rs`, with the content in the adjacent `src/lib.md`. Behavior is the same — `cargo doc` picks up `lib.md` as the crate's front page; intra-doc links resolve against the egglog crate as they did before. The runnable Rust-API doctest (let-bind + eval_expr + extract_value) stays in `src/prelude.rs` where it can rely on the more permissive markdown-block environment. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com> * docs: tutorial up, Command pointer, prelude case 3, drop intern_container src/lib.md: - Moved the Tutorial section above "Using egglog from Rust" — that's where most newcomers should go first. - New "Language reference" section pointing at the [`Command`] enum (alias for [`ast::GenericCommand`]) and explaining the convention: one variant per top-level egglog command, each with its own doc-commented syntax/semantics. The docs live on `GenericCommand`; the alias just delegates. src/prelude.rs: - Bumped "Two cases" to "Three cases", adding custom primitives alongside `update` and `rust_rule` as a distinct Rust-interop path. Already detailed below in "Extending egglog" — the intro now flags it. src/lib.rs: - Drop `EGraph::intern_container`. It was a pure alias of `container_to_value` with zero callers in src/, tests/, or benches/. Also a quick check while I was poking around: `EGraph::lookup_function` (pub(crate)) is still used by `src/proofs/proof_extraction.rs:83`, so we can't remove it without porting that callsite. Worth a follow-up. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com> * port the proof-extraction lookup off lookup_function; drop the helper The proof system has one read of an internal proof table. Going through `EGraph::update` doesn't work because update refuses under proofs (by design — closures could stage writes that bypass the proof pipeline) and the proof system itself runs under proofs. Refactor: extract the body of `EGraph::update` into a `pub(crate) fn update_unchecked`. `update` is now a thin wrapper that does the proofs check and delegates. Internal callers that need the same machinery without the check (`constructor_enodes`, `function_entries`, `proof_extraction`) call `update_unchecked` directly. Same flush-at-end behavior as `update`; the flush is a no-op on read-only closures. Proof_extraction now reads via: let proof_value = self.egraph.update_unchecked(|fs| { fs.lookup(&proof_function_name, RawValues(vec![witness_value])) })?.unwrap_or_else(|| panic!(...)); `EGraph::lookup_function` had only this one caller and is now gone. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com> * port vec/multiset union primitives off new_union_action The `vec-union` and `multiset-union-values` primitives each held their own `UnionAction` and called it via the privileged `raw_exec_state()` seam — but they already see a `WriteState` and the public `Write::union(x, y)` method does the same thing. // before let action = self.action; let es = state.raw_exec_state(); for (l, r) in zip(left, right) { action.union(es, l, r); } // after for (l, r) in zip(left, right) { state.union(l, r).ok()?; } Drops: - `Union::action: UnionAction` field on vec.rs - `UnionValues::action: UnionAction` field on multiset.rs - `EGraph::new_union_action()` (pub(crate)) — no longer has callers - the `use egglog_bridge::UnionAction` imports vec.rs no longer needs the `Internal` trait either (it was only there for `raw_exec_state`); multiset.rs still uses it elsewhere. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com> * drop EGraph::function_entries / constructor_enodes; go through Read Both methods were thin top-level wrappers over the `Read` trait versions. Now that every other "read the e-graph" operation goes through the wrappers (`eg.update(|fs| fs.lookup(...))` etc.), keeping a separate top-level path for iteration was inconsistent — and it relied on `update_unchecked` to skip the proofs check, which let proofs-mode callers iterate via the top-level method but not via `update`. Asymmetric. Drop both. Callers now use `eg.update(|fs| fs.function_entries(...))` / `eg.update(|fs| fs.constructor_enodes(...))` like everything else. Proofs-mode users can't iterate tables this way — `update` refuses under proofs — and that's now visible at the API. Also: - Switch the `query` method's `std::collections::HashMap` paths to imported `HashMap` (matches the rest of the codebase, which uses `crate::util::HashMap` via the blanket `use util::*;`). - Collapse a nested `if let Some(ruleset_obj) = ... { if let Ruleset::Rules(rules) = ... { ... } }` into a single pattern. - Drop the `tests/api_proofs::read_only_iteration_works_under_proofs` test — exercised the special-case top-level path; that path is gone. - Drop a stale "Top-level convenience versions live on EGraph" line from the prelude module doc. cargo clippy is now clean. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com> * drop EGraph::function_for_each; port callers to Read::constructor_enodes Also clean up small nits surfaced by clippy: - nil.clone() on Copy Value -> bare nil - redundant closure || fib_setup() -> bare fn pointer - stale doc reference on update_unchecked * make fixnits: rustfmt + clippy-fix sweep * resolve copilot review nits - src/lib.rs: stranded `Run a closure with full read-write access` doc comment was sitting on `set_report_level` after the `with_full_state` removal; replace with a doc that actually describes the method. - src/api/mod.rs: `FromValues` tuple impl was silently dropping trailing columns; assert the iterator is exhausted after decoding so a row that's longer than the tuple panics with a clear message instead of looking like a valid result. * Apply suggestions from code review Co-authored-by: Yihong Zhang <yz489@cs.washington.edu> * cosntructor_enodes much faster * change to iter and smallvec * Apply suggestions from code review Co-authored-by: Yihong Zhang <yz489@cs.washington.edu> * respond to review: TableRows rename, uniform top-level scan API, tidy-diff-docs skill - Rename the public table-snapshot type `Rows` to `TableRows` to avoid colliding with `core-relations::Rows`. - Expose `EGraph::function_entries` / `EGraph::constructor_enodes` as top-level table scans mirroring the `Read` trait (thin `update_unchecked` wrappers, read-only so cheap and proof-safe). These replace the callback-based `function_for_each`; `lookup_function` stays deleted. - Add `TableRows::iter_with_subsumption` so the row snapshot can report subsumption — the one piece of info the old callback exposed that the `(inputs, output)` scan dropped. - Add the repo-level `tidy-diff-docs` skill that trims implementation details and duplicate text from doc/code comments in a diff, and reference it from CLAUDE.md. Co-authored-by: Yihong Zhang <yz489@cs.washington.edu> Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> * api: stream constructor_enodes/function_entries via callbacks; &self top-level reads Replace the TableRows snapshot (which materialized the whole table into one buffer via scan_all) with a streaming callback API, addressing the eager-copy concern. Rows now stream in 32-row batches through the bridge's for_each_while. - New purpose-built row types: `Enode { children, eclass, subsumed }` for constructor_enodes and `FunctionEntry { inputs, output, subsumed }` for function_entries, replacing the raw split-it-yourself row. - Add `*_while` early-exit variants (closure returns bool) on both the `Read` trait and `EGraph` — a new capability the old function_for_each lacked. - Make the top-level `EGraph::{constructor_enodes,function_entries}` (and the `_while` forms) take `&self` instead of `&mut self`, backed by a new `EGraph::read(|rs| ...)` read-only mirror of `update`. A pure read never flushes, so the callback may call other `&self` methods like `value_to_base` directly. - Rename bridge `FunctionRow` -> `ScanEntry` (still pub for extract.rs; no longer re-exported from egglog so `egglog::FunctionEntry` is unambiguous). Drop the now-unused `RowScan` / `TableAction::scan_all`. - Update call sites (tests, bench), prelude docs, and the tidy-diff-docs skill. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> * extract api fix --------- Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com> Co-authored-by: Yihong Zhang <yz489@cs.washington.edu> * Reject naive eq-sort primitive proof facts * Move proof primitive tests out of lib * Add a test pinning the new-container-in-fact proof gap A rule body that produces a newly-created container via a primitive and then needs its proof in the same iteration currently fails: a container's reflexive `<CSort>Proof` is anchored only during rebuild, not at creation, so the action lookup of its term proof finds no row. Pin the current (failing) behavior so the gap is visible and CI flags when it gets fixed. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> --------- Co-authored-by: oflatt <oflatt@gmail.com> Co-authored-by: Claude Opus 4.8 (1M context) <noreply@anthropic.com> Co-authored-by: Saul Shanabrook <s.shanabrook@gmail.com> Co-authored-by: Yihong Zhang <yz489@cs.washington.edu>

saulshanabrook force-pushed the codex/split-unstable-fn-primitive-targets branch from 5eecf36 to a821985 Compare May 18, 2026 20:38

saulshanabrook force-pushed the codex/split-unstable-fn-primitive-targets branch from a821985 to 671b2b5 Compare May 20, 2026 18:59

saulshanabrook added this to Saul Shanabrook May 26, 2026

saulshanabrook moved this to This Week in Saul Shanabrook May 26, 2026

saulshanabrook moved this from This Week to In Progress in Saul Shanabrook May 26, 2026

saulshanabrook force-pushed the codex/split-unstable-fn-primitive-targets branch from 8c41fd4 to 3ce691c Compare May 26, 2026 19:55