Repository navigation
D4: single-arm match, field named match, data-initializer lambdas - #10967
Conversation
|
review 63228 is right: The tail walk now skips only before extract, and only for empty Conj, a comma atom, Optional whose element skips, or a sequence whose both sides skip. A navigate-emitted production with no captured child (and any other unknown shape) is not a skip; extract's Head is now 3a52a25. PR stays draft for the srv2 closure receipt on this sha. — sent from gentle-pike-522 |
|
Closure before/after for #10967 at head 68 → 60. Zero regressions: no previously accepted module refuses; no file outside the attributed set changed cause; nothing moved to an earlier stage. Per mechanism, using the carrier's attribution:
Terminal-cause histogram after: parse 26, graft 25, lexer 8, post-normalize-not-well-formed 1. The match-arm and wrapper-retention causes no longer occur anywhere in the closure. This satisfies the cause-relative bar for D, F and R at population grain. Still owed before un-draft (per the review requirement relayed separately): three cause-level commits with three red/green control pairs so each mechanism's evidence stands on its own; this receipt already attributes the closure delta per mechanism, so the split needs only the commit and fixture structure. |
e6171ce to
ab1267b
Compare
ab1267b to
0443d4e
Compare
|
Refreshed closure receipt for #10967 at head Identical to the This receipt binds to |
|
review 63356 — addressed on 3ce7f15.
|
|
review 63375 — agreed; not pushed (frozen head 3ce7f15).
Proposed fix on parent go: delete — sent from gentle-pike-522 |
|
review 63375 — roster class corrected on 2d2fe70. PROVEN was the wrong class: there is no measured fill-netted marginal over 500ms. A local claim_batch PASS is recorded as an observation, not as the roster's fact. Cause R data-record discriminators, zero-arm, and the F sniff stay off the roster: they produced verdicts. |
|
Closure before/after for #10967 at head 68 → 60. Zero regressions. Cause-relative outcome for the 8 D rows: 7 RefusalCleared ( Identical outcome to the receipt at |
…er as a malformed match. A one-arm match was refused because the empty comma-list Repeat tail was navigated as a missing arm; a field named match was sniffed as a match expression because kw_match headed an identity-absent sequence after a dot. Empty-arm match still refuses. Arrow-lambda and fn-literal shells in data initializers are preserved after the child fold so they stop emitting wrapper-retention. Co-authored-by: Cursor <cursoragent@cursor.com>
Skip only empty Conj, comma, Optional-of-skip, or a sequence of those, and do it before extract. An unknown or navigate-emitted node keeps its match-arm navigation refusal instead of lowering a silently shorter match. Co-authored-by: Cursor <cursoragent@cursor.com>
Two-arm and three-arm remain green so the discriminator is arm count, not parity or pattern form. Co-authored-by: Cursor <cursoragent@cursor.com>
… keyword controls. Infix a.match == b.match is the same field-access sniff, not a bare-access special case. Co-authored-by: Cursor <cursoragent@cursor.com>
…ral in an fn body already did. Arrow-lambda and fn-literal spellings both sit in the data initializer; the fn-body record is the control that never wrapper-retained. Co-authored-by: Cursor <cursoragent@cursor.com>
…eir own pair. Co-authored-by: Cursor <cursoragent@cursor.com>
The annotation still said five identities after the list grew; the count is not the authority. Co-authored-by: Cursor <cursoragent@cursor.com>
The tokenize/parse/normalize control strings were BUDGET-REFUSED or, for the zero-arm source, completed false against a reason string; the floor's discriminators are now the skip/sniff/structure classifiers themselves. Co-authored-by: Cursor <cursoragent@cursor.com>
The negative control was PARSE_REFUSED because the empty brace was taken as a
record on t. match (t) { } is the empty arm list, and still refuses
body_lowering_reason_match_arm_navigation_refused.
Co-authored-by: Cursor <cursoragent@cursor.com>
…ows.
The skip/sniff/structure stand-ins are not evidence about tokenize/parse/normalize.
Thirteen claims that BUDGET-REFUSED on job 103096598642 stay enrolled via
floor_cost_debt censored (D3's mechanism). Zero-arm and the F sniff stay on the
floor: they completed. Zero-arm fixture remains match (t) { }.
Co-authored-by: Cursor <cursoragent@cursor.com>
review 63356: drop the censored enrolment that treated a 501ms interrupt as a cost, extract the shared normalize helper, and leave both data-record classifier witnesses off the debt roster. Co-authored-by: Cursor <cursoragent@cursor.com>
review 63375: PROVEN needs a fill-netted marginal over the ceiling, which these rows do not have. The floor of record interrupted them before a verdict; that is the censored class, keyed to the CI observation, with restoration a measured marginal under 500ms. Co-authored-by: Cursor <cursoragent@cursor.com>
2d2fe70 to
49dff28
Compare
|
review 63396 — already resolved on 49dff28; no new commit. That review was filed against the pre-rebase head (DIRTY / CONFLICTING). This head is rebased onto main 267d69b (
The where-rehome helpers ( Because the rebase touched — sent from gentle-pike-522 |
required-floor job 103155806208 refused: 13 interrupted before verdict (D4 R/zero-arm plus the D1 where family) and braced_fn_decl_survives_normalize completed at 503ms. Censored vs proven split matches what that job observed. Co-authored-by: Cursor <cursoragent@cursor.com>
|
Verified against 5000c1d for review 63588. Both findings are real. No commit on this head: D4 is frozen until the post-#11029 (then D2/D3) remerge. Finding 1 (zero_arm + two R data-record claims on chunk_04 vs stale “stay off floor_cost_debt” comments). The enrolment is true: those three identities are in Parent ruling for the remerge (not this SHA): those three stay on D4’s censored list because they interrupted on the floor of record (job 103155806208 / run 34556768895). They are D4’s own changed-witness interrupts, not hitchhikers. The 503 ms Finding 2 (ten D1/G identities + proven_21 on a D4 chunk). Agreed, and already the remerge recipe: keep main’s Stale comments will be corrected in that same motion so they no longer claim the three stay on the ordinary floor. — sent from gentle-pike-522 |
1 participant
Summary
Three independently evidenced roots in body_lowering_fold.
Freeze head: 49dff28 (rebased onto main 267d69b). The merge conflict was
body_lowering_fold.dag(D1 where-refinements vs Cause R structure-preserve). Resolution kept both: where_refinement_clause / where_predicate and arrow_lambda / fn_literal. That is closure source, so the aaaad15 srv2 receipt does not carry to this head; retake after G at the landing head. Land last: #10988 -> D2 -> D3 -> D1 -> G -> D4. P0a.1 is not a prerequisite. The required-v2-native CI job is deleted (#11003). Required CI is build + floor. The srv2 167-member closure receipt bound to the landing head is the required native semantic evidence; retake it after G lands. That receipt establishes the compiler closure and this PR's cause-relative delta, not whole-v2.test.* native admission.body_lower_match_arm_repeat_elem_is_separator— empty comma-list Repeat tail is skipped before extract. Pipeline-path control: zero-armmatch (t) { }still refusesbody_lowering_reason_match_arm_navigation_refused; one-arm wildcard/constructor/shorthand accept (two-arm and three-arm stay green). Closure 7/7 RefusalCleared (prior receipt):src/v2/compiler/05_eval.dag,src/v2/extdeps/runtimes/v2_effect_io_pure.dag,src/v2/lens/machine_shape.dag,src/v2/lens/undecidable_verdict_collapse.dag,src/v2/std/cardinality.dag,src/v2/std/integer.dag,src/v2/std/model_core.dag.body_lower_match_spine_has_lbrace— identity-absentkw_matchsniff requires a following lbrace. Pipeline-path:r.matchanda.match == b.matchaccept;r.other,r.loop,r.typealready accepted. Closure:src/v2/std/runtime.dagAdvancedToNewCausenormalize_reason_post_normalize_not_well_formed(cause 19, not this PR).body_lower_is_structure_preserved_emitted—dag_surface_arrow_lambdaanddag_surface_fn_literalpreserved after the child fold. Pipeline-path: data-field(a, b) => aandfn(a, b) { a }accept; the same literal in an fn body already accepted. Closure:src/v2/std/logic.dagRefusalCleared.Restored pipeline-path claims and floor_cost_debt
Skip/sniff/structure replacements are deleted. Witnesses are again tokenize/parse/normalize (plus the F sniff that already completed). After review 63375:
proven_chunk_21is deleted. Eleven identities interrupted_before_verdict on the floor of record (job 103096598642 / run 34534985281, 501-520ms) are onfloor_cost_debt_censored_chunk_03. That asserts they did not finish inside the ceiling on the charged clock; own-work cost is unmeasured. Restoration is a measured fill-netted marginal under 500ms on that floor. A local claim_batch PASS is an observation, not the roster's fact. Left off because they produced verdicts: zero-arm refusal, F sniff, and both Cause R data-record discriminators.single_arm_wildcard_match_normalizes_holdstwo_arm_match_still_accepts_holdsthree_arm_match_is_not_parity_holdsone_arm_constructor_pattern_normalizes_holdsone_arm_shorthand_field_pattern_normalizes_holdszero_arm_match_still_refuses_holdsmatch (t) { }field_named_match_normalizes_holdsinfix_field_named_match_normalizes_holdsfield_renamed_other_control_holdsfield_named_loop_control_holdsfield_named_type_control_holdsmatch_keyword_after_dot_is_not_a_match_expr_sniff_holdsbody_lowering_match_field_name_spine_does_not_sniff_holds(was already on e268ca2, not a 092689f replacement)data_record_arrow_lambda_field_is_not_retained_holdsdata_record_fn_literal_field_is_not_retained_holdslambda_in_fn_body_control_holdsObservation (not this PR)
match t { }is parsed as a record literal on the ident scrutineet, so an empty match-arm list is not a parse of that spelling. Reproducer: modulem.t,type T = A | B,fn f(t: T) -> Int { match t { } }—normalize_outcomeisPARSE_REFUSED. Control:match t { _ => 1 }in the same module ACCEPTED. Discriminator:match (t) { }reaches body-lowering and refusesbody_lowering_reason_match_arm_navigation_refused. Candidate row for a later parse/grammar lane (D1 ownsdag.dag); not part of #10967.Test plan
match (t) { }enrolled on the floor.