Merge main, and address the second review - #73
Merged
oflatt merged 26 commits intoSep 22, 2026
Merged
Conversation
`(unstable-subst root map)` takes an e-class of any eq-sort and a Map from an eq-sort to itself, walks the constructor rows reachable from the root, and copies the part of that sub-e-graph the substitution touches with each key e-class replaced by its mapped value, returning the copied root. E-classes the substitution does not affect are shared rather than copied; container children are rebuilt around their substituted contents. Also available as egglog_experimental::subst. Copies are named by lookup_or_insert like any other action-built term, so no e-class id is invented: a cyclic e-class is copied when one of its e-nodes has all its children outside the cycle, and a cycle with no such e-node is reported instead of half-copied. Reads live tables, so it is a Context::Full primitive - top-level actions and :naive rule heads. Built entirely on egglog's public API: Read::enodes_for_eclass to walk a constructor's rows by output e-class, Read::table_schema / table_subtype to classify each column, and Core::rebuild_container for container children. The type constraint enumerates the declared Map and eq-sorts through TypeInfo::get_arcsorts_by, identifying a Map sort by the Rust type its values intern under since the ContainerSort impl behind an ArcSort is not nameable from out of tree. Cargo.toml points at a local egglog checkout while that API is unmerged. See SUBST_DESIGN.md for the semantics and the sharp edges. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Points the egglog dependencies at egraphs-good/egglog#986, which adds Read::enodes_for_eclass, Read::table_schema / table_subtype, and Core::rebuild_container. Moves back to an egraphs-good rev once that merges. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
egglog now splits its schema accessor by subtype, so resolving the walk's constructors is one call that rejects function tables (and so globals, which lower to function tables) instead of a subtype check plus a schema lookup. is_constructor now asks table_subtype instead of starting a constructor scan and reading the answer off the error, which is what that accessor was for. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
egglog now keeps one FuncType per function, shared between TypeInfo and Function, so the schema accessors hand back an Arc<FuncType> and Function::schema() is Function::func_type(). The walk holds the Arc directly instead of a borrowed slice of input sorts. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
`constructor_schema` now returns a `&FuncType` borrowed from the e-graph rather than an `Arc` cloned out from behind a lock, so the walk holds plain references. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
egraphs-good/egglog#986 merged, so the egglog dependencies point back at an egraphs-good rev rather than the branch they were reviewed on. The staging limit was a bullet among others, phrased as a mechanism ("a term built in the same action is not visible"). It is the one thing a caller can get wrong silently, so it is now a warning up front, phrased as the rule that follows from it: pass a root the query bound, or one from an earlier command. A root the action just built has no rows yet, so the walk finds nothing under it and hands it back unchanged, with no error. Also states the boundary, since it is not obvious: replacements are exempt. A map's values are spliced into the copy without being walked, so those can be built in the same action. `a_replacement_built_in_the_same_action_is_fine` pins that, so the doc is checked rather than asserted. Docs tidy over the diff: the alias `Constructor` and `constructors` said the same thing about per-call resolution, the "globals lower to function tables" fact appeared twice a few lines apart, and a memo field restated the method it memoizes. Also drops a `let _ = &mut eg;` left over in a test. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
…gn doc Review found a silent wrong answer. `kind_of` decided "container with e-classes inside" from `Sort::is_eq_container_sort()`, but `FunctionSort` computes that from `self.inputs` - the arguments still to be applied - while `inner_values` returns the arguments the value actually *captured*. Those are different sets, so a `(sort Thunk (UnstableFn () Math))` holding an e-class reported no eq-sort elements, was classified `Opaque`, and its captured e-classes were never substituted. No error: the root simply came back unchanged. Classifying by `is_container_sort()` and letting `inner_values` say what the value holds cannot miss one. It costs an `inner_values` call on containers that turn out to have no e-classes inside, which is memoized and yields no leaves. `substitutes_inside_a_captured_function_value` is the regression test, and fails against the old classification. Two smaller ones from the same review: the ungrounded-cycle message deduped an unsorted list, so it could name a constructor twice; and the container fallback in `container_image` would turn an internal inconsistency into a silently unsubstituted container, so it now debug-asserts. The design doc had drifted: it named `Error::SubstError`, `Read::table_schema` and `Core::rebuild_container`, none of which exist by those names any more, and claimed a program that enables proofs and calls the primitive is not caught. It is caught - `--proofs` refuses the command with "primitive operation lacks a validator function", which I checked by running it. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
With `{Lit 1, Var "x"}` in one class and `x |-> 2`, the copy holds `2` and
nothing asserts `1 = 2`: a key is spliced in rather than walked into, so the
other e-nodes in its class are never consulted. That is the opposite of an
affected non-key class, where every e-node is copied - worth having both
pinned next to each other.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
…thing From review: the sweep called `state.add`/`union` as it went and only discovered an ungrounded cycle once it reached one. egglog flushes an action's staged writes even when it ends in an error, and the primitive's panic path does not roll them back, so a failed substitution left the copyable part of the region behind - contradicting the documented error-rather-than-partial-copy behaviour. Reproduced with an acyclic affected branch beside an ungrounded cycle: `Add` grew from 3 rows to 4 across a substitution that failed. `plan` now decides the whole question up front, from the snapshot alone: a least fixpoint of "has an e-node whose children all resolve", which yields both whether every e-node in the region is copyable and an order to name the classes in. It writes nothing, so a doomed substitution fails having touched nothing. `build` then follows that order without having to discover blockage, which also answers the review's other point about the sweep: the repeated pass is now a pure in-memory fixpoint, and the writing half is two linear passes - name each class from its first buildable e-node, then add the rest as further ways to say the class they came from. Also from review: - The two `None`s in `FullPrim::apply` that meant "our bug" rather than "egglog failed" now panic: the typechecker fixes the arity and admits only `Map` values, so reaching either is a defect here. Documented when `apply` does return `None`. - `handles_a_deep_spine` drops from 20k to 5k, which still covers far more depth than a program writes by hand (1.20s -> 0.28s for the file). Its comment no longer claims to exceed a native stack, which neither depth reliably does. - `SUBST_DESIGN.md` moves to `docs/unstable-subst.md`, and its fenced block gained a language for markdownlint. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
`tests/unstable-subst.egg` shows the motivating use, beta reduction through a `:naive` rule, so the feature has a readable example rather than only Rust tests. `tests/subst-basics.egg` moves the fourteen semantics cases that were `.egg` strings inside `tests/subst.rs` out to where they read as egglog, one push/pop scope each so the cases stay independent. What `check` cannot see — e-class identity, table sizes, error variants, the `subst` entry point — stays in Rust. Writing them as real .egg files surfaced an egglog bug: walking the tables after a `pop` handed the backend a table id it no longer had. Pinned to the branch that fixes it until egraphs-good/egglog#1003 lands, which also renames `enodes_for_eclass` to `constructor_enodes_for_eclass`. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Main released 3.0.0 and rewrote the crate docs. Five files overlapped: * `src/keep_best.rs`, `src/table_stats.rs` — the same `schema()` -> `func_type()` rename done on both sides; took main's, which also hoists the binding. * `src/lib.rs` — main replaced the bullet list of extensions with sectioned docs, so the `unstable-subst` bullet moves into "Language and values" in that style. Kept the module export beside main's new doc comment on `new_experimental_egraph`. * `Cargo.toml` — kept the fork pin, which carries the `pop` fix this branch needs, and took main's `version = "3.0.0"` field. * `Cargo.lock` — regenerated. Also added the `unstable-subst` entry to the changelog main introduced. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Preserve subsumed rows in unstable-subst
Resolve the conflicts left by main's extraction and scheduler work: - Cargo.toml/Cargo.lock: keep this branch's egglog pin a07403c0, which already contains main's d61ba050 plus the subsumption fix the branch needs; restore main's `.git` remote URL spelling. - keep_best/multi_extract/set_cost/scheduling: take main's versions. This branch only ported these to the newer extraction and scheduler APIs; main did the same port and added greedy-DAG extraction, `:dag` multi-extract, and the scheduler node limit on top. - CHANGELOG: keep both sides' entries. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Resolve conflicts with main: - `src/lib.rs`: register both sides' extensions in `new_experimental_egraph` — main's `Maybe`, `map-fold-kv`, and `f64` primitives plus this branch's `unstable-subst`. - `Cargo.toml`/`Cargo.lock`: pin egglog to upstream `9063586` and drop main's `[patch]` onto the egg-smol fork. That fork rev was pinned for user-defined output downcasting pending egglog#1008, which is now merged upstream; upstream main also carries egglog#1010, the prediction-aware `Write::subsume` this branch needs (the fork's `subsume` does a pure `lookup`, so subsuming a row added in the same action would panic). - `docs/unstable-subst.md`: egglog#1010 has landed upstream, so record the new pin instead of the PR head commit. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…log-pin Pin egglog to upstream subsumption fix
unstable-subst: substitution over a reachable sub-e-graph
`main` gained `unstable-subst` (egraphs-good#60). The only conflict was two doc bullets added at the same place in the crate docs; both are kept. Both sides already pin the same egglog, so the manifest and lockfile merged cleanly. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
oflatt-claude
requested review from
FTRobbin
and removed request for
a team
September 22, 2026 18:23
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Two things: the merge with
mainafter #60 landed, and the three regressions from the second review.Merge
The only conflict was two doc bullets added at the same place in the crate docs —
unstable-substand named arguments — and both are kept. Both sides already pin the same egglog (9063586), so the manifest and lockfile merged cleanly.The three regressions
All three came from moving expansion to the command-macro stage, and the first one is the reason to move back.
[P1] Cloned e-graphs shared field mappings.
CommandMacro::transformreceives only aSymbolGenand aTypeInfo, so the field names had to live in the macro object — whoseArcevery clone of an e-graph shares. There is no per-e-graph storage at that stage, so keying by(name, arity)was never going to be enough, as the review says.The parser turns out to be the right home after all: it is part of the e-graph, so it is cloned with one and snapshotted by
push/pop, and a per-name expression macro only fires for the declaration that registered it. Expansion is back in the parser, and the two things the original parse-time version was missing are fixed directly:(include ...)is read once while parsing, so the declarations inside register their field names before the calls that follow the include are parsed. The command itself is passed through untouched, so egglog still reads and runs the file exactly as before — only the registration moves earlier. The read is best-effort and never reports: a missing or unparsable file is left for egglog to fail on from its own include handling, so this can only add registrations. That is the original [P2].Function already bound R, even inside a(push)), so the only way one name is declared twice is(push)/declare/(pop)/declare — where the later declaration in the source is exactly the one live afterwards. That is the original [P3], and it makes source order match declaration scope without needing the command stage.[P2] Named calls inside extension commands. Gone with the move: parse-time expression macros fire wherever
parse_exprruns, including user-defined command arguments, so(extract (C :x 1))works again.[P3] Positional tables rejecting
:-prefixed variables. Also gone: a macro is only registered for names that were actually declared, so(relation R (i64))/(let :value 1)/(R :value)is never inspected for markers. The speculative "not declared with named fields" error is removed.Tests
Regression tests for all six reported cases, each confirmed to fail on the implementation it was reported against:
tests/named-args-ellipsis-fresh.eggtests/named-args-include.eggtests/named-args-scope.eggtest_named_args_do_not_leak_between_cloned_egraphstests/named-args-extract.eggtests/named-args-positional-vars.eggThe include test covers both halves: the included relation is usable by name, and it is declared exactly once — a second execution of the include would fail with
Function already bound.The earlier succinctness changes are kept:
register_named_argsis the only public item, oneread_named_fieldvalidator is shared between schemas and datatype variants, andregister_named_callis gone. Thedeclare()note from the second review no longer applies — that function belonged to the command-macro version.make testandmake nitspass: 175 nextest tests, doctests,cargo clippy --tests -- -D warnings,cargo fmt --check.🤖 Generated with Claude Code