Store a function's signature once, and expose it to primitives

[oflatt-claude]

Three additions to what a primitive body can see. None are specific to any one
extension: together they are what an out-of-tree primitive needs to walk the
term structure under an e-class and build a modified copy of it.

The motivating consumer is an unstable-subst substitution primitive in
egraphs-good/egglog-experimental#60, which lives there rather
than here because substitution is a language experiment, not core e-graph
machinery. This PR is only the introspection; it is worth reviewing on its own
terms.

Read::enodes_for_eclass(name, eclass, f)

Walks a constructor's rows by output e-class through the backend's lazy column
index, instead of scanning the table and filtering. Cherry-picked from #934,
along with the core-relations ExecutionState::for_each_matching_col and
egglog-bridge TableAction::for_each_output_value it rests on — credit to
that PR; this takes only the traversal hunks and none of the extraction work.

Read::constructor_schema(name), Read::function_schema(name), Read::table_subtype(name)

A table's declared signature, and whether it is a constructor or a function.
EGraph::functions_iter already exposes this from &EGraph, but a primitive
body only ever sees a state wrapper, and those carried no sort information at
all — so a primitive could read rows without being able to tell an e-class
column from a base value, or a constructor's eclass column from a function's
output.

The schema accessor is split by subtype and errors with WrongSubtype on a
mismatch, matching how the rest of Read and Write already work
(lookup/eclass_of, constructor_enodes/function_entries, set/add).
That split is not just cosmetic: a constructor's last column is an e-class and
a function's is an output. table_subtype is the error-free predicate for code
that accepts either.

Breaking: a signature is now stored once

The first cut of this branch added a FunctionSchemas registry to back those
accessors. That was a third copy of data egglog already kept twice —
TypeInfo::func_types holds a FuncType {name, subtype, input, output}, and
Function held the same content again as a ResolvedSchema plus
decl.subtype (and a third time, unresolved, in decl.schema). What was
missing was never the data, only a way to reach it from a state wrapper.

So TypeInfo::func_types became the single store and the shared cell, and the
new registry is gone:

• TypeInfo::get_func_type returns Option<Arc<FuncType>>, not
  Option<&FuncType>.
• Function points at the same Arc<FuncType>;
  Function::schema() -> &ResolvedSchema becomes
  Function::func_type() -> &FuncType.
• ResolvedSchema is removed; its get_by_pos moves to FuncType.
• declare_function reuses the signature typechecking already resolved instead
  of resolving the sorts a second time. It still resolves and records the
  functions desugaring generates (global bindings, proof tables), which never
  go through typechecking — so func_types now covers every declared table.
• GenericFunctionDecl::resolved_schema is gone, along with the placeholder
  String::new() an unresolved decl carried in it and its
  ResolvedCall::view_types reader. Its only consumer was proof encoding, which
  runs over decls desugaring generates after typechecking (the functions
  global bindings lower to) and so cannot look those up by name — but it never
  needed a FuncType, only the column sorts, and those resolve by name from
  TypeInfo like any other sort. (Recording the generated signatures into
  TypeInfo instead does not work: the desugared program is typechecked again
  afterwards, so recording early trips the already-bound check.)
• ResolvedCall::Func holds an Arc<FuncType>, so a resolved call site shares
  the signature rather than cloning it — and there is one of those per call in
  every rule. Patterns that matched
  ResolvedCall::Func(FuncType { subtype: Custom, .. }) cannot look through an
  Arc, so they match the variant and test the subtype in a guard via a new
  ResolvedCall::is_custom_func.

Two subtleties worth a reviewer's eye. TypeInfo::clone deep-copies the map: a
clone is an independent e-graph — a pushed copy, or the parallel typechecking
the proof checker keeps in original_typechecking — and declaring a function in
one must not make it resolve in the other. And pop restores the pushed
contents into the live cell the registered primitives already hold, rather than
swapping in a cell they have no handle to.

No lock: the signature reaches a primitive as a borrow

The obvious way to back those accessors is to hand the primitive an
Arc<RwLock<_>>, and the first cut of this branch did. That lock would never
have been guarding a race — declaring anything needs &mut EGraph, run_rules
already holds that borrow for the whole execution, and nothing on
Core/Read/Write can declare. It was there only because external functions
are stored as Box<dyn ExternalFunction + 'static>, so a wrapper cannot hold a
borrow of the e-graph.

So this changes the route instead of the synchronization. ExecutionState
carries an ExternalContext — a borrowed value the caller of an operation
makes visible to the external functions it reaches — and egglog passes
&TypeInfo into run_rules and with_execution_state*. The state wrappers
read it back, so constructor_schema hands out a &FuncType borrowed from the
e-graph itself.

The invariant is then enforced by the borrow checker rather than stood in for
by a lock: that &TypeInfo is live for exactly the operation that supplied it,
so the e-graph cannot be mutably borrowed to declare a function while a rule is
running. TypeInfo::func_types stays a plain owned map, get_func_type keeps
its Option<&FuncType> signature and costs a map lookup, TypeInfo::clone
stays derived, and push/pop restore it like every other field.

Rebuild paths pass None: they run generated rebuild rules whose actions
evaluate in the Write context, which has no schema accessors.

This does not touch the pre-existing ActionRegistry read lock in
RegistryPrimWrapper::invoke, which every registry primitive still pays per
invocation — the same seam would remove it, as a follow-up.

table_subtype also retires an existing workaround in egglog-experimental,
which determines a table's subtype by starting a constructor scan and reading
the error off the subtype check — removed in the companion PR.

Core::rebuild_container(type_id, value, remap)

Remaps a container value's contents and interns the result, over the existing
ContainerValues::rebuild_val_with. Out-of-tree code cannot reach this through
Core::register_container, which requires naming the container's Rust type —
impossible for an arbitrary container sort.

Notes

• No behaviour change to existing programs; this is additive.
• FunctionSchemas costs one HashMap entry per declared table.
• Adds one rule to the repo's tidy-diff-docs skill: prefer an import over an
  inline full path for a type.
• Verified: full workspace test suite passes (including the 799-program files
  harness), cargo clippy --tests --workspace clean, cargo fmt --check clean,
  and cargo doc adds no new warnings.

🤖 Generated with Claude Code

[codspeed-hq]

Merging this PR will improve performance by 5.88%

⚠️ 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

⚡ 1 improved benchmark
✅ 36 untouched benchmarks
⏩ 227 skipped benchmarks¹

Performance Changes

	Mode	Benchmark	BASE	HEAD	Efficiency
⚡	Simulation	tests[stresstest_large_expr]	1.6 s	1.5 s	+5.88%

Tip

Curious why this is faster? Comment @codspeedbot explain why this is faster on this PR, or directly use the CodSpeed MCP with your agent.

---

_{Comparing oflatt-claude:subst-egraph-introspection (53f4fe5) with main (95f539c)}

Footnotes

1. 227 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. ↩

[saulshanabrook]

This seems a bit awkward, having a global like this

[codecov-commenter]

Codecov Report

❌ Patch coverage is 92.83820% with 27 lines in your changes missing coverage. Please review.
✅ Project coverage is 86.76%. Comparing base (716c320) to head (53f4fe5).
⚠️ Report is 7 commits behind head on main.

Files with missing lines	Patch %	Lines
src/lib.rs	85.93%	9 Missing ⚠️
egglog-bridge/src/lib.rs	88.13%	7 Missing ⚠️
core-relations/src/action/mod.rs	85.71%	5 Missing ⚠️
src/exec_state.rs	94.80%	4 Missing ⚠️
core-relations/src/hash_index/bench_support.rs	0.00%	1 Missing ⚠️
src/proofs/proof_normal_form.rs	85.71%	1 Missing ⚠️

Additional details and impacted files

@@            Coverage Diff             @@
##             main     #986      +/-   ##
==========================================
+ Coverage   86.59%   86.76%   +0.17%     
==========================================
  Files          95       95              
  Lines       29676    29871     +195     
==========================================
+ Hits        25698    25918     +220     
+ Misses       3978     3953      -25     

☔ View full report in Codecov by Harness.
📢 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.

[yihozhang]

Great work! Mostly just low-level nits.

[yihozhang]

Great! I see it also fixes some other places that use non_stale() while an iter suffices, which is nice.