Store a function's signature once, and expose it to primitives - #986
Open
oflatt-claude wants to merge 4 commits into
Open
Store a function's signature once, and expose it to primitives#986oflatt-claude wants to merge 4 commits into
oflatt-claude wants to merge 4 commits into
Conversation
Three additions to what a primitive body can see, none of them 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. 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 egraphs-good#934 along with the core-relations ExecutionState::for_each_matching_col and egglog-bridge TableAction::for_each_output_value it rests on. Read::table_schema(name) and Read::table_subtype(name) report a table's declared column sorts and its subtype. 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. Backed by a FunctionSchemas map the e-graph shares with the wrappers exactly as it already shares ActionRegistry, and snapshot/restored across push/pop so a popped table stops resolving. table_subtype also replaces probing a subtype by starting a scan and reading the error, which egglog-experimental does today. Core::rebuild_container(type_id, value, remap) remaps a container value's contents and interns the result. Out-of-tree code cannot go through Core::register_container, which requires naming the container's Rust type. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
oflatt-claude
requested review from
saulshanabrook
and removed request for
a team
August 6, 2026 19:45
table_schema returned a schema for either subtype, which reads past the fact that a constructor's last column is an e-class and a function's is an output. Splitting it matches how the rest of Read and Write already work - lookup / eclass_of, constructor_enodes / function_entries, set / add - so it is now constructor_schema and function_schema, each erroring with WrongSubtype on a mismatch. table_subtype stays as the error-free predicate to dispatch on when either subtype is acceptable, which is what retires the subtype probe in egglog-experimental. Also applies the tidy-diff-docs skill to the comments this branch adds, and records a new rule in that skill: import a type rather than naming it by an inline full path, which is what FunctionSchemas was doing with crate::util::HashMap. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
The first cut of this branch added a FunctionSchemas registry so a primitive
body could see column sorts. That was a third copy of data egglog already kept
twice: TypeInfo::func_types holds a FuncType {name, subtype, input, output},
and Function holds the same content again as a ResolvedSchema plus decl.subtype
(and a third time, unresolved, in decl.schema). What was actually missing was
not the data but a way to reach it from a state wrapper.
So there is now one store. TypeInfo::func_types becomes the shared cell -
Arc<RwLock<HashMap<String, Arc<FuncType>>>> - and the state wrappers hold a
handle to it, which is what backs constructor_schema / function_schema /
table_subtype. FunctionSchemas is gone. Function points at the same Arc<FuncType>
rather than storing its own copy, so Function::schema() -> &ResolvedSchema
becomes Function::func_type() -> &FuncType and ResolvedSchema is removed, its
get_by_pos moving 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.
Two things this had to get right. TypeInfo::clone deep-copies the map: a clone
is an independent e-graph - a pushed copy, or the parallel typechecking the
proof checker keeps - 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.
Also drops the second RwLock acquisition per primitive invocation the first cut
introduced: the wrapper holds the unlocked handle and the schema accessors lock
only when called, so a primitive that never asks pays nothing.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
The additions belong with the name-indexed e-graph access entry they extend, not as a standalone block longer than anything else on the list. The signature consolidation keeps a one-line breaking bullet next to the other breaking ones. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Merging this PR will not alter performance
Comparing Footnotes
|
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.
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-substsubstitution primitive inegraphs-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-relationsExecutionState::for_each_matching_colandegglog-bridgeTableAction::for_each_output_valueit rests on — credit tothat 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_iteralready exposes this from&EGraph, but a primitivebody 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
WrongSubtypeon amismatch, matching how the rest of
ReadandWritealready 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_subtypeis the error-free predicate for codethat accepts either.
Breaking: a signature is now stored once
The first cut of this branch added a
FunctionSchemasregistry to back thoseaccessors. That was a third copy of data egglog already kept twice —
TypeInfo::func_typesholds aFuncType {name, subtype, input, output}, andFunctionheld the same content again as aResolvedSchemaplusdecl.subtype(and a third time, unresolved, indecl.schema). What wasmissing was never the data, only a way to reach it from a state wrapper.
So
TypeInfo::func_typesbecame the single store and the shared cell, and thenew registry is gone:
TypeInfo::get_func_typereturnsOption<Arc<FuncType>>, notOption<&FuncType>.Functionpoints at the sameArc<FuncType>;Function::schema() -> &ResolvedSchemabecomesFunction::func_type() -> &FuncType.ResolvedSchemais removed; itsget_by_posmoves toFuncType.declare_functionreuses the signature typechecking already resolved insteadof 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_typesnow covers every declared table.Two subtleties worth a reviewer's eye.
TypeInfo::clonedeep-copies the map: aclone is an independent e-graph — a
pushed copy, or the parallel typecheckingthe proof checker keeps in
original_typechecking— and declaring a function inone must not make it resolve in the other. And
poprestores the pushedcontents into the live cell the registered primitives already hold, rather than
swapping in a cell they have no handle to.
Primitive invocation cost is unchanged: the wrapper holds the unlocked handle
and the schema accessors lock only when called, so a primitive that never asks
pays nothing.
table_subtypealso retires an existing workaround inegglog-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 throughCore::register_container, which requires naming the container's Rust type —impossible for an arbitrary container sort.
Notes
FunctionSchemascosts oneHashMapentry per declared table.tidy-diff-docsskill: prefer an import over aninline full path for a type.
filesharness),
cargo clippy --tests --workspaceclean,cargo fmt --checkclean,and
cargo docadds no new warnings.🤖 Generated with Claude Code