unstable-subst: substitution over a reachable sub-e-graph

[oflatt-claude]

Blocked on egraphs-good/egglog#986 — draft until that merges, since the
Cargo.toml here points at its branch. Review that one first; this is the
consumer that motivated it.

(unstable-subst root map) : (R, Map<K, K>) -> R

root is an e-class of any eq-sort; map is a Map whose key and value sorts
are the same eq-sort. It walks the constructor rows reachable from root,
copies the part of that sub-e-graph the substitution actually touches with each
key e-class replaced by its mapped value, and returns the copied root.
E-classes the substitution does not affect are shared with the original rather
than copied, so substituting an empty map returns root itself and writes
nothing. Container children are walked into and rebuilt around their
substituted contents. Also available from Rust as egglog_experimental::subst.

SUBST_DESIGN.md has the full semantics; the three things worth knowing before
relying on it:

The region's equations are substituted along with its terms. Copying an
e-class copies every one of its e-nodes, so t1 = t2 in the original becomes
σ(t1) = σ(t2) in the copy — and an e-node with no substituted children copies
to itself, merging the copy back into the original class. That is correct for
equations a rewrite rule derived, which hold for every value of the substituted
class: with (rewrite (Mul a (Num 0)) (Num 0)), substituting x := 5 into
(Mul x (Num 0)) merges back into the class of 0, and 5 * 0 really is 0.
It is wrong for a ground union pinning a substituted class down. So only
substitute classes that behave like universally quantified variables. Both
directions are pinned by tests.

No e-class id is ever invented. Every copied e-node goes in through
lookup_or_insert, the same way (Add a b) in an action does. A cyclic
e-class is therefore copied only when one of its e-nodes has all its children
outside the cycle to name the copy first — x = {Var "x", Add x (Num 0)}
qualifies and works. A cycle with no such e-node is reported rather than
half-copied.

It reads live tables, so it is a Context::Full primitive: top-level
actions and :naive rule heads. A term the enclosing action has only just
staged is not yet in the tables and comes back unsubstituted; terms from
earlier commands and earlier rule iterations are fine, which is what the
:naive beta-reduction shape needs.

Implementation

Three passes: collect the reachable e-nodes and container contents; mark the
e-classes the substitution changes by worklist from the map keys; then copy in
postorder, sweeping until no further progress, which is what lets a grounded
cycle close. E-class walks use an explicit stack, so term depth is bounded by
the heap (there is a 20k-deep test).

Built entirely on egglog's public API: Read::enodes_for_eclass to walk a
constructor's rows by output e-class, Read::constructor_schema to classify
each column, and Core::rebuild_container for container children. Also swaps
table_rows::is_constructor off its subtype probe and onto
Read::table_subtype. 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.

Notes

• 23 tests in tests/subst.rs. Full suite passes; cargo clippy --tests and
  cargo fmt --check clean.
• A failing substitution reaches an egglog program as the generic
  "primitive panicked", with the reason in the log: registering a custom panic
  message needs egglog_bridge::EGraph::new_panic, and egglog exposes no
  accessor for its backend. A Write::panic_with(message) upstream would fix
  it.
• Proof mode is unsupported — the copied rows carry no justification. The
  primitive is registered without a validator, so program_supports_proofs
  already excludes programs using it from proof-checking runs.

🤖 Generated with Claude Code