Register user primitives on the term-encoding typechecker

[oflatt-claude]

Problem

A primitive registered through the Rust API (EGraph::add_pure_primitive / add_read_primitive / add_write_primitive / add_full_primitive, or the add_primitive! / add_literal_prim! macros) after the e-graph is constructed is only registered on the running e-graph. Under term encoding / proofs (new_with_term_encoding / new_with_proofs), typechecking is done by a separate proof_state.original_typechecking e-graph, which never learns about the primitive — so the encoder reports it as an unbound function:

let mut egraph = EGraph::new_with_term_encoding();
add_literal_prim!(&mut egraph, "tripleit" = |x: i64| -> i64 { x * 3 });
egraph.parse_and_run_program(None, "(function f (i64) i64 :merge (min old new))
(set (f 0) (tripleit 7)) (run 1) (check (= (f 0) 21))")?;
// before: Error — "Unbound function tripleit"

Callers had to work around it by manually re-registering on proof_state.original_typechecking (a proof test did exactly that).

Fix

register_per_context now walks the original_typechecking chain and registers the primitive on each e-graph. A typechecker only typechecks and never evaluates, so the wrapper's runtime state (e.g. an action registry) is irrelevant there; and both e-graphs register the same built-ins at construction, so a primitive added to both gets the same ExternalFunctionId.

A sort's primitives already reach the typechecker through its own add_arcsort when the typechecker typechecks the sort command, so add_arcsort detaches the typechecker while a sort registers — otherwise container/sort primitives would be double-registered and primitive resolution would become ambiguous.

Tests

• New prelude::tests::add_primitive_under_term_encoding regression test.
• Removed the now-unnecessary manual original_typechecking registration from the container proof test.
• Full suite green (cargo test, incl. the proof/term-encoding tests).

🤖 Generated with Claude Code

[codecov-commenter]

Codecov Report

❌ Patch coverage is 96.87500% with 1 line in your changes missing coverage. Please review.
✅ Project coverage is 86.71%. Comparing base (6f0d26e) to head (4ed4acc).

Files with missing lines	Patch %	Lines
src/prelude.rs	91.66%	1 Missing ⚠️

Additional details and impacted files

@@           Coverage Diff           @@
##             main     #945   +/-   ##
=======================================
  Coverage   86.71%   86.71%           
=======================================
  Files          92       92           
  Lines       28609    28641   +32     
=======================================
+ Hits        24807    24837   +30     
- Misses       3802     3804    +2     

☔ 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.

[codspeed-hq]

Merging this PR will not alter performance

✅ 37 untouched benchmarks
⏩ 227 skipped benchmarks¹

---

_{Comparing oflatt-claude:fix-user-primitives-term-encoding (4ed4acc) with main (6f0d26e)}

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