Repository navigation
v2 infer gather: thread one facts Map through fold_node; delete the entries scan and concat - #12640
Closed
gunbai-bot[bot] wants to merge 83 commits into
Closed
gunbai-bot[bot] wants to merge 83 commits into
gunbai-bot[bot] wants to merge 83 commits into
Conversation
…st holds the label in an Rc)
…e generic-ident-class flip
…_atom_identities) instead of re-parsing each
…uments (the witness is about carets, not the lambda frontier)
…ypes a bare Cons as FreeMonoid)
…l spelling instead of being captured Body lowering rewrote every type atom spelled Int or Bool to the kernel binding before any scope existed. A module that declared its own `type Int = | Mine` and wrote `let y: Int = 1` therefore had its annotation replaced by the kernel Int, and infer judged the let matched. The spelling table moves to its language authority (v2.extdeps.languages.dag dag_kernel_type_binding_optional), and resolve_atom consults it only after the scope walk and the symbol index. A hit declared in the referencing module binds that declaration. Imported, foreign, ambiguous and unbound kernel spellings keep the kernel binding, unchanged. Claims (v2.test.claim.body_let_annotation, 5c): the module-declared Int and Bool lets refuse at the annotation, and the annotation is asserted not to be the kernel binding. An undeclared Int/Bool still binds the kernel type. Both shadow rows are red on main 9ce0394 and green here. The rfm row records the residual and its trigger. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…l Int Resolve now reads a kernel spelling by the declaration a door selected. v2.extdeps.languages.dag dag_kernel_type_declaration_binding_optional lists the declarations a kernel spelling denotes. A hit on one of them takes the canonical binding, and the module's own declaration shadows it. Any other declaration, reached through an import or another module, refuses with resolve_reason_kernel_type_spelling_names_a_foreign_declaration. Unbound and ambiguous names keep the spelling fallback. Third RED: bla_imported_user_int_refuses_rather_than_binding_the_kernel_int (a two-module fixture, p imports q's `type Int = | Mine`). All three REDs are F on main and T here, and the controls are T on both. The new specimens are enrolled in floor_pure_producer_share. The rfm row now states rung = refused, with the trigger at capability grain: declaration-keyed binding across every door. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…te is a kernel declaration An ambiguous kernel spelling now binds the kernel type only when every candidate is a kernel declaration of it: v2.std.integer Int beside std.integer Int is one kernel type. Otherwise it refuses with the ordinary resolve_reason_ambiguous_symbol instead of defaulting to the kernel. An unbound name keeps the kernel binding, which is the correct answer when no declaration is in scope. New claims: - RED bla_ambiguous_imported_int_refuses_rather_than_defaulting_to_the_kernel (p imports Int from q and r). F on main, T here. - Control bla_ambiguous_kernel_declarations_bind_the_kernel_type. T on both. The multi-module specimens now share one helper, bla_assemble_with_peers. The rfm residual is now only the kernel-declaration path list. Its trigger is a mark on the kernel declarations themselves. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…-ibex-696/symbol-arm # Conflicts: # src/v2/test/claim/body_let_annotation_test.dag # src/v2/workflow/floor_pure_producer_share.dag
…std.node Symbol) Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…hored return-type spelling Three floor blockers on fa8c596. These claims read the positional return clause from body lowering and expected the kernel binding (dag_binding_type_int, bool_node_symbol). Lowering used to produce that binding by rewriting the spelling. That rewrite now happens in v2.compiler.resolve, after the scope walk, so lowering carries `Int` and `Bool` as written, as the generic row already reads `T`. Arm 1 still discriminates: the return type is Bool, not the parameter's Int. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
review 72280: the symbol arm tested dag_node_is_symbol_literal_atom and then recomputed dag_symbol_literal_name_optional. That was the same optional twice, and the recomputation needed an arm the predicate had already ruled out. The decision now matches the optional once. The remaining Absent arm is a name payload with no atom identity, which is reachable. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…teral_name_optional directly (review 72280 on #12549)
…-ibex-696/symbol-arm # Conflicts: # src/v2/compiler/03_resolve.dag
…xeme-stamped terminal; delete the span/source-text route and its prose note row (review 72294 on #12549) Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…-ibex-696/symbol-arm
…ens span route: nothing else consumed them Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…-ibex-696/symbol-arm
…pe as this PR derives it review 72301: the receipt still said the symbol literal's type stays on the GroundingNotDerived frontier. The arm in this PR makes that false. It now names the derivation route (DagCanonicalSymbolLiteral, infer_literal_type_binding, v2.std.node symbol_type_node) and the two body_let_annotation claims that execute it. Census trigger (a) stays open and the receipt says why: it names the source checker v1.compiler.types, which still types LitSymbol as string_type. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…anned per lookup facts_map_from_entries admitted entries into a List and answered every lookup with lookup_inferred_facts_in_entries, a linear scan: each consumer walking the tree paid quadratic. It now enters admitted entries into a Map<Node, InferredFacts> once and answers lookup with map_lookup. A repeated node keeps its FIRST admitted entry, as the scan did. The gather fold's own scans (lookup_inferred_facts_in_entries inside infer_gather_fold_algebra) remain: the catamorphism computes children independently, so removing them needs a state-threading node fold, filed as node adhoc-914690c3-870. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…ions; ownership reads declared_in GitHub review 5342739525 on #12540. The same-module test compared a declaration's path to ctx.namespace.module_qn, but build_program_namespace (the plain normalize -> resolve route) leaves module_qn Empty and records its owner in declared_in. namespace_owns_declaration now reads declared_in, which is the owner on both namespace routes and the field root_binding_origin reads. Measuring that route found the earlier boundary. build_program_namespace harvested only the root's named edges, and a normalized module keeps its declarations under captured -> <module path>, so none of them were bound. `type Myint` refused as unbound, and a module's own `type Int` fell through to the kernel spelling and was silently bound to the kernel Int. The namespace now also harvests the module body, which it finds by declared_in. Controls on that route (v2.test.claim.body_let_annotation, enrolled share points): - bla_single_tree_module_declared_int_and_bool_bind_the_local_declaration: F before, T now. - bla_single_tree_undeclared_int_binds_the_kernel_type: T on both. The foreign-import refusal and both ambiguity dispositions are unchanged and still hold. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
# Conflicts: # src/v2/workflow/floor_pure_producer_share.dag
…y walking names Review 5343957887 (P2 on b55b8a7). namespace_tree_module_body walked the module path's names and restarted at the root on a missing step. Two leaks followed: - `module m.t` with a root-level record `t` missed `m`, restarted, found `t`, and bound the record's field as a module binding. - `module t` with a record `t` selected it at once. The body is now selected by the producer's own mark. v2.compiler.namespace_graft namespace_graft_module_body_optional descends the containment spine (namespace_graft_spine_segment_edge_optional) until a step is not a segment, never restarts, and answers only when that stop is the marked body (namespace_graft_node_is_module_body). Header and flat representations have no grafted body, so they keep root-only harvesting. The admission reader in v2.compiler.name_resolve already descended the same spine with its own copy (admit_named_exports_body_root and _descend_spine). It now calls the one function in namespace_graft (namespace_graft_module_body_root), so the spine has one reader. Controls (v2.test.claim.resolve.single_tree_module_body): supplied emit-shaped roots, because normalize always emits a well-formed graft and source text cannot author these shapes. - a_record_matching_the_path_suffix_is_not_a_module_body_holds: F on b55b8a7, T here. - a_record_named_like_a_flat_module_is_not_its_body_holds: F on b55b8a7, T here. Each asserts `leaked` is not bound and `t` still is. The local Int/Bool and undeclared-kernel controls still hold. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…ation The parse phase refused a // annotation inside the fn body (DESIGN section 4c: only module-item grain is modeled). This is the same text, placed above the declaration. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…-ibex-696/symbol-arm # Conflicts: # src/v2/test/claim/body_let_annotation_test.dag # src/v2/workflow/floor_pure_producer_share.dag
…ection ahead of #12382's renamed named-argument header Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…-ibex-696/symbol-arm
…g insert; literal payloads by family Merge session/eager-newt-412 (#12582). A key already carrying a different fact now fails the gather with infer_facts_key_conflict instead of the first entry answering; the literal payload edge dispatches on #12582's InferLiteralPayload family. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…mbol_value_lowering (the refusal suite stays deleted)
…aret_symbol_value_refusal (carried via #12549), add main's bcn_let_in_value_cast_verdict share row Main's #12615 let-in caret case lived in the retired refusal test; moving it into the lowering test is #12420's (flagged to its owner). Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…sion/neat-eagle-675
…-ibex-696/symbol-arm
…sion/neat-eagle-675
…ipt; caret cause row stays retired; let-in comment matches the lowering)
…sion/neat-eagle-675
…y a run-wide lookup Asked of the threaded map, 'does this node already have an entry' saw a structurally equal node entered elsewhere and skipped the row, dropping that occurrence's frontier diagnostic (DNM #12648 run 36647127349: 046/051/070 differ only in their infer_grounding_not_derived count). The list gather's subtree-scoped check never found the node itself, so the row always ran. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
gunbai-bot Bot
pushed a commit
that referenced
this pull request
Sep 30, 2026
…r-node facts, root) on #12640 with the kind-decided product row Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…first-entry-wins (review 72985) Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
briansrls
marked this pull request as ready for review
September 30, 2026 02:40
Codex Review SummaryThis comment shows the latest Codex review activity on this pull request.
ℹ️ About Codex in GitHubYour team has set up Codex to review pull requests in this repo. Reviews are triggered when you
Codex reacts with 👀 while any review is running, comments if it has suggestions, and reacts with 👍 once all reviews finish with no findings. |
![chatgpt-codex-connector[bot]](https://avatars.githubusercontent.com/in/1144995?s=60&v=4){kind=small}
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: ca5c4d8a4b
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
Comment on lines
+2368
to
+2369
| match inferred_facts_map_enter(facts: state.facts, entry: entry) { | ||
| Rejected { diagnostics: r } => infer_gather_state_failed(state: state, rejected: r) |
There was a problem hiding this comment.
When distinct source occurrences lower to structurally equal synthetic Node keys but derive different facts, the run-wide map treats them as the same subject and this insertion fails immediately with infer_facts_key_conflict. This preempts the actual semantic diagnostic for existing refinement and coproduct inputs; the differential probe records the changed fatal reason for 11 of 98 specimens. Keep facts occurrence-scoped, or defer the threaded global map until keys include occurrence identity.
Useful? React with 👍 / 👎.
| @@ -0,0 +1,3591 @@ | |||
| module v2.compiler.infer | |||
There was a problem hiding this comment.
This adds a 3,591-line frozen copy of the inference implementation solely for the new probe_tmp shell scripts; repo-wide search finds no production or test-discovery consumer. Every subsequent inference change can leave this second implementation stale, while the scripts also copy the repository into /tmp and replace the live module manually, so these throwaway comparison artifacts should remain outside the committed source tree.
Useful? React with 👍 / 👎.
Contributor
Author
|
Closing as superseded by eager-newt-412's site-keyed facts trie, per neat-boar-16's ruling: this PR's hold existed so the facts accumulator wasn't rewritten twice while its key was undecided, and the trie settles that key (ruling B: a site key, injective by construction because the structure mirrors the tree). A Map keyed by structural Node, as here, would still collide on equal synthetic nodes. The trie PR carries this PR's goal as a condition: ONE accumulator threaded through fold_node, with no per-node copies or rebuilds, the entries scan and concat deleted, and the cost shape stated and measured at the native seven's subject. Reusable parts may be taken from this branch, credited. — sent from quiet-gull-780 |
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.
What changed
v2.compiler.infer's gather no longer carries an entries list. It is still onev2.std.nodefold_node, but the carrier is a function over a single threadedInferGatherState, which holds the factsMap<Node, InferredFacts>, the pending diagnostics and a failed flag. Each node'srunruns its children in edge order and then enters its own facts. What a node awaits is still decided at fold time.lookup_inferred_facts_in_entries(the per-lookup list scan) andconcat_inferred_facts_entries(the per-parent join). Every row reads the map throughinfer_known_facts, which is declared atInferredFacts. The seven "derive, admit, or fail" row bodies collapse intoinfer_gather_state_admit.inferred_facts_map_enter. A key already carrying a different fact fails the run withinfer_facts_key_conflict; it no longer lets the first fact answer.v2.test.execution.infer_gather_costinfer_gather_deep_product_spine_derives_its_root_holdsruns a supplied 8-level product spine through the threaded gather to its root. It is an inhabitance claim, not a cost gate. No depth that fits the new-witness budget (v2.workflow.required_floorrequired_floor_new_witness_eval_step_budget) separates old from new, so cost evidence is the floor reading below. Its pairing claim, which runs the real front end, isv2.test.execution.infer_product_introductionproduct_introduction_derives_fully_evidenced_products_holds.Cost (what this PR claims, and what it does not)
Instrument: the required floor's per-claim eval-step reading, from the
[over-cost]/COMPLETED-OVER-COST-REQUIREMENTlines and therequired_floor_claim_cost.tsveval_stepscolumn. It measures the spine claim at depths 24, 48 and 96 on two throwaway branches:dnm/neat-eagle-675-cost-base, v2 infer gather: thread one facts Map through fold_node; delete the entries scan and concat #12640's pre-change base476baf1, run 36621935843.dnm/neat-eagle-675-differentialataf6192e, run 36621886463.Readings from those runs (eval steps):
Node-keyed map insert and lookup hash and compare whole subtrees, and each node pays per-node descent-witness work over its subtree. Next trigger: the occurrence-keyedFactSubjectchange, which keys facts by occurrence identity rather than by structuralNode(blocked on the lowering occurrence fix, MQ PR1 (model): a lowering closes its image; derived nodes mint OccurrenceProjected #12604).Differential (identity grain, old list gather vs threaded gather)
Recipe: DNM #12648, branch
dnm/neat-eagle-675-differential. It carries the old gather as the probe modulev2.test.claim.dnm.infer_old_gather: #12582's ownv2.compiler.infer, verbatim exceptinferrenamed toinfer_old, so the two sides differ only in the gather.v2.test.claim.dnm.infer_gather_differentialassembles each specimen withtpb_assemble, runs both infers, and compares four fields:infer_facts_key_conflictwith the same key and locus. The threaded gather stops at the first conflicting insert and the list gather at map build, so the chain before the fatal may be shorter.facts.lookup(n)for everynode_subtree_nodesnode.The universe is all 98 distinct
"module p\n..."sources insrc/v2/test.Nodekeys collide at different positions, and a run-wide lookup answers from the other position.infer_grounding_not_derivedcount. Cause: the product-row guard read the run-wide map. Fixed in 3cd4135 by deciding the row by kind.infer_facts_key_conflict. 0 of 98 acceptances became refusals.The #12640 floor on 3cd4135 is green: no enrolled claim regresses and none newly refuses with a key conflict.
Why the gather cannot close this by itself. Every variant that threads one run-wide map over a structural
Nodekey meets the synthetic-occurrence collisions somewhere. The pre-3cd4135 guard matched these 11 but silently dropped advisories on 046/051/070; the kind-decided row keeps the advisories but reaches a key conflict first. Subtree-scoped lookups were rejected because they hide the node-key defect. Occurrence keys are the fix.🤖 Generated with Claude Code