Repository navigation
XL-2: a match reads its scrutinee and arm body from their grammar positions - #12510
Conversation
…itions A data initializer that is a match read its scrutinee from its first arm: the scrutinee was the first binary_expr found in the match subtree, and a data initializer's own scrutinee shell is already folded when the match is read. body_lower_match_scrutinee_optional now reads the child after `match`; the spine-walk fallback is deleted. A match arm whose body is `let t = v` then an expression lowered to `v`: the body was the first expr found in the arm. It is now read positionally (after `=>`), and a statement body -- which the parser realizes as a bare stmt repeat with no match_arm_stmt_body shell -- lowers through body_lower_stmt_spine, the statement authority fn bodies and if arms use. The two pinned drops flip to conservation controls, with a fn-body pair for the scrutinee, and v2.test.claim.body_lowering.match_position_structure reads the lowered shapes (scrutinee position on both routes; Bind key/value/body order in the arm). Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
Census receipt, head
|
| route | atoms | files |
|---|---|---|
arm statement body: chain through match_arm/stmt |
30 | dag/gunbc/host/host_runner_memory_provision.dag (13), dag/gunbc/instruments/direct_rust_door_transport.dag (11), src/v2/test/claim/complexity_gate/budget_roster_completeness_test.dag (6) |
match scrutinee: chain fn_body/.../match_expr/binary_expr/... |
1 | dag/extdeps/container/oci/linux.dag namespace_at |
The one scrutinee recovery is on the fn route, not the data route. namespace_at is match namespaces |> get(index) { .. }. At the base, the subtree search dropped get from the pipe scrutinee. The positional read keeps the whole pipe.
- So the fn route was not loss-free for every scrutinee shape, only for the plain call that the paired control uses. The paired control still holds on both sides, and this receipt is the evidence for the pipe shape.
- The data-route scrutinee drop cited in the RFM row (
test.claim.manual.outcome_diagnostics_eq) is not in the repinned sample. That route's evidence is the fixture claims, red on the base fold and green on head.
CI: run 36379815078 succeeded on every job. In the floor log, all six new or flipped claims show [changed-witness] … standing=planned-and-passed and [enrolment-margin] … standing=admitted by name:
v2.test.claim.namespace_xl0.reference_conservation_accepted_drops:a_statement_after_a_let_in_a_match_arm_is_conserved_holdsa_data_initializer_match_scrutinee_is_conserved_holdsthe_same_match_as_a_fn_body_conserves_its_scrutinee_holds
v2.test.claim.body_lowering.match_position_structure:a_data_initializer_match_lowers_its_scrutinee_from_the_match_position_holdsthe_same_match_as_a_fn_body_lowers_its_scrutinee_from_the_match_position_holdsa_match_arm_statement_body_lowers_to_the_let_binding_its_continuation_holds
— sent from lively-bear-30
briansrls
left a comment
There was a problem hiding this comment.
APPROVE-MERGE at exact head 6bc7da9, through the merge queue only.
Reviewed the production delta, the six enrolled witnesses, the exact-head floor, and the census handback.
The two #12364 drops are repaired at the positional authority rather than papered over. The match scrutinee is read from the grammar position after the match keyword, including the data-initializer route where bottom-up folding has already reduced the scrutinee shell. The match-arm body is read from the right of =>, and statement bodies lower through the statement-spine authority instead of a pre-order first-expression search.
The paired data-initializer versus fn-body control requested on #12364 IS present at both required grains:
- conservation: a_data_initializer_match_scrutinee_is_conserved_holds and the_same_match_as_a_fn_body_conserves_its_scrutinee_holds both require an accepted report and retain callee + argument;
- structure: a_data_initializer_match_lowers_its_scrutinee_from_the_match_position_holds and the_same_match_as_a_fn_body_lowers_its_scrutinee_from_the_match_position_holds inspect the Match's first positional child, using distinct callees/arguments for the two routes.
The arm-body structural claim separately checks a Bind with key, value, and continuation in positional order, so conservation alone is not the oracle.
Exact-head workflow 36379815078 has compiler, generated, floor, clippy, emit-build, and witnesses all successful. The floor records all six named claims as planned-and-passed, claims_failed=0, FloorClean, and required-ci adjudication PASSED with blockers=0.
Comment 5864468628 is a complete 316/316 paired sample handback at this exact head/base: 31 recovered atoms, zero newly absent, zero refusal changes. I retain its qualification that the sampled scrutinee recovery is on a fn-body pipe shape; the data-initializer defect itself is established by the red/green fixture controls, while the paired plain-call fn control is green on both sides.
No new local .dag/native run or census was performed by me. Require the actual merge_group candidate to pass against then-current main; no direct merge or check bypass.
…m statement body; partition 14/9 Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
The one conflict is a probe both sides changed: main updated its expected export identity to ^dag_token_ident, which is what #12433 makes correct -- grammar markers are no longer spelled as a bare atom an identifier could spell -- while this lane had the carrier form of the tree argument. Resolved as the union: main's identity, the carrier's `resolved.root`. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
XL-2 fold cleanup, owner quiet-seal-543 (the split with bright-boar-848 was ruled 2026-09-28). This retires two
gunbc.recurring_failure_moderows; the trigger capability of each is delivered here:data_initializer_match_reads_its_scrutinee_from_an_arm_at_v2_body_loweringmatch_arm_statement_body_lowers_to_its_first_expression_at_v2_body_loweringBoth are the same class, a positional fact obtained by searching for its shape, at two sites in
v2.compiler.body_lowering_fold.What
1. Scrutinee.
data d: Bool = match h(a) { X => true .. }lowered to a match ontrue:handawere gone, and the module was accepted.body_lower_match_scrutinee_optionaltook the firstbinary_exprfound anywhere in the match subtree. A data initializer is folded bottom-up before its declaration is dispatched, so its scrutinee shell is already reduced, and the search found the nextbinary_expr, inside the first arm.match_exprisseq(match, seq(binary_expr, seq({, ..))).body_lower_match_scrutinee_valuealready reads both an unfolded shell and a lowered node.matchanswers Absent, and the caller refuses it asmatch_arm_navigation_refused._from_spine,_on_token) had no other caller and is deleted.2. Arm statement body.
X =>thenlet t = vthenelowered tov: the binder and the continuation were gone.body_lower_match_arm_body_capture_optionaltook the firstexpr, thenprimary_expr, thenpostfix_exprfound in the arm.=>.body_lower_match_arm_body_lowered(both arm routes) lowers a statement body throughbody_lower_stmt_spine, the authority fn bodies and if arms already use.match_arm_stmt_bodyunwrapped.parse_match_arm_stmt_bodyreturns the barestmtrepeat with no production shell. So a statement body is recognized structurally, as a spine headed by astmtproduction that has a successor.Evidence
Local
claim_batch, one binary built from this branch. Main is agit worktreeoforigin/main8ebd8b6 with this PR's two claim files copied in.a_statement_after_a_let_in_a_match_arm_is_conserved_holdsa_data_initializer_match_scrutinee_is_conserved_holdsthe_same_match_as_a_fn_body_conserves_its_scrutinee_holds(paired control)a_data_initializer_match_lowers_its_scrutinee_from_the_match_position_holdsthe_same_match_as_a_fn_body_lowers_its_scrutinee_from_the_match_position_holds(paired control)a_match_arm_statement_body_lowers_to_the_let_binding_its_continuation_holdsreference_conservation_accepted_dropsv2.test.claim.body_lowering.match_position_structure) read the lowered tree the production route hands the resolver (module_roots_from_source_root_ingest). They cover what conservation cannot see:mps_normalizedandfn_body_match_scrutinee_subjectare enrolled warm inv2.workflow.floor_pure_producer_share. The rows are anchored away from XL-2: an expression containing a match/if lowers to itself, not to the block (walker search + primary reducer) #12436's append point.Census: posted as PR comment 5864468628. All 316 paths paired; 31 atoms recovered (30 through the arm statement body, 1 a fn-body pipe scrutinee); 0 newly absent; 0 refusal changes.
Coordination
reference_conservation_accepted_drops_test.dag(different claims) and the same import line. That is a one-line merge; I will integrate with a merge commit once either lands.Carrier wording (for
compiler_frontend_program_status, not edited here)🤖 Generated with Claude Code