From 7281901562a0ff5a738bc8b87a53595057db01cd Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Fri, 2 Oct 2026 22:20:39 +0000 Subject: [PATCH 01/33] body_lowering_fold: an if's arms are read at their slots of the if_expr row MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit body_lower_if_else_capture_optional searched the if's capture and, at any left element that was not `else`, recursed LEFT before right. For `if b { if c { X } else { Y } } else { Z }` it entered the then-arm and answered the nested if's `else { Y }` as the outer else: Z was dropped, Y lowered twice, and normalize ACCEPTED the module (silent wrongness, DESIGN §5). It was loud only when Y held a function value, whose binder occurrence then appeared twice: dag/std/materialization_ladder.dag value_materialization refused as normalize_reason_minted_occurrence_duplicated, one of the native seven's file refusals. body_lower_if_then_arm_optional searched the same way. Both arm readers are now projections of body_lower_if_row_arms_optional, which reads the two if_expr grammar rows by position (block: if cond fn_body else (if_expr | fn_body); then-form: if cond then expr else expr) and answers Absent for any other capture. The dead searching helper body_lower_if_fn_body_capture_optional is deleted. The arm contract is unchanged: an `else if` is answered as its if_expr shell, any other arm as its production's captured child. Claims: v2.test.claim.body_lowering.if_arm_position (an atom count over the normalized tree, plus the function-value forms). Row: the capture side is filed on gunbc.recurring_failure_mode else_arm_lowered_as_an_if_nested_inside_it. Co-Authored-By: Claude Opus 5.5 (1M context) --- ..._arm_lowered_as_an_if_nested_inside_it.dag | 7 +- src/v2/compiler/body_lowering_fold.dag | 207 ++++++++---------- .../body_lowering/if_arm_position_test.dag | 111 ++++++++++ 3 files changed, 203 insertions(+), 122 deletions(-) create mode 100644 src/v2/test/claim/body_lowering/if_arm_position_test.dag diff --git a/dag/gunbc/recurring_failure_mode/else_arm_lowered_as_an_if_nested_inside_it.dag b/dag/gunbc/recurring_failure_mode/else_arm_lowered_as_an_if_nested_inside_it.dag index e033a4d37a8..9876174b963 100644 --- a/dag/gunbc/recurring_failure_mode/else_arm_lowered_as_an_if_nested_inside_it.dag +++ b/dag/gunbc/recurring_failure_mode/else_arm_lowered_as_an_if_nested_inside_it.dag @@ -10,7 +10,8 @@ data else_arm_lowered_as_an_if_nested_inside_it: RecurringFailureMode = Recurrin receipts: [ "INVALID STATE: an `else` arm lowered to an `if` nested INSIDE it, as though the arm were `else if`. `v2.compiler.body_lowering_fold` `body_lower_if_else_capture_optional` answered what follows `else` with the first if_expr found by a DEEP search of the else part (`body_lower_find_production_shell_optional`), so `if u == 0 { .. } else { match k { A => x B { v: w } => if c { w } else { u } } }` lowered its else arm to the nested `if c {..} else {..}` alone: the match's scrutinee, its other arms and its patterns were dropped with no refusal.", "SPECIMEN, MEASURED ON MAIN 5bffaa1e82f (2026-09-30), PRE-EXISTING: `dag/gunbc/machine_intake/boot_image_export_ownership.dag` `export_ownership_standing` -- seven atoms absent (`observed_key`, `Absent`, `ExportOwnershipUnrecognizedAccount`, `observed_name`, `Present`, `value`, `k`). The module was refused on main for an unrelated guard; the structured-tail change (gunbc#12713) admitted it, and that PR's reference-conservation census surfaced the drop. A minimal fixture drops identically under main's fold, so the defect is independent of that change.", - "RUNG FOUND AT: below the floor (silent wrongness, and a correct program refused when a pattern binder the dropped arm bound is read in the kept if). RUNG NOW: structurally guaranteed at this link -- `body_lower_else_part_if_expr_optional` reads the else part's FIRST production shell without descending into any production (`body_lower_first_production_shell_optional`), which the grammar makes either an if_expr (an `else if`) or a fn_body, so an if nested inside the else body cannot be taken for the else part. CEILING: the same.", + "SECOND SITE, THE CAPTURE SIDE, MEASURED ON MAIN 1a013596270 (2026-10-02): the else-PART fix above left the reader that finds the else at all searching. `body_lower_if_else_capture_optional` walked the if's capture and, at any left element that was not the `else` token, recursed LEFT before right -- so for `if b { if c { X } else { Y } } else { Z }` it entered the then-arm and answered the NESTED if's `else { Y }` as the OUTER if's else. Z was dropped, Y lowered twice, and normalize ACCEPTED the module (an atom count over the normalized tree: Z 1, Y 3, against 2 and 2). It was loud only when Y held a function value, whose binder occurrence then appeared twice: `dag/std/materialization_ladder.dag` `value_materialization` refused as normalize_reason_minted_occurrence_duplicated, one of the native seven's file refusals. `body_lower_if_then_arm_optional` searched the same way (the first fn_body anywhere in the capture). Both arms are now projections of `body_lower_if_row_arms_optional`, which reads the two if_expr grammar rows by POSITION and answers Absent for any other capture, so a nested if cannot be taken for either arm.", + "RUNG FOUND AT: below the floor (silent wrongness, and a correct program refused when a pattern binder the dropped arm bound is read in the kept if). RUNG NOW: structurally guaranteed at this link -- `body_lower_else_part_if_expr_optional` reads the else part's FIRST production shell without descending into any production (`body_lower_first_production_shell_optional`), which the grammar makes either an if_expr (an `else if`) or a fn_body, so an if nested inside the else body cannot be taken for the else part. Both sides now hold at the same rung: the else part by its first production shell, and the arms by their slots in the if_expr row. CEILING: the same.", ], evidence: [ @@ -19,5 +20,9 @@ data else_arm_lowered_as_an_if_nested_inside_it: RecurringFailureMode = Recurrin DeclarationRef { module_path: "v2.test.claim.namespace_xl0.else_arm_nested_if", decl_name: "the_if_nested_in_the_match_arm_is_still_read", field: WholeDeclaration }, DeclarationRef { module_path: "v2.test.claim.namespace_xl0.else_arm_nested_if", decl_name: "a_real_else_if_chain_still_reads_its_nested_else", field: WholeDeclaration }, DeclarationRef { module_path: "v2.test.claim.namespace_xl0.else_arm_nested_if", decl_name: "the_declared_shape_resolves", field: WholeDeclaration }, + DeclarationRef { module_path: "v2.compiler.body_lowering_fold", decl_name: "body_lower_if_row_arms_optional", field: WholeDeclaration }, + DeclarationRef { module_path: "v2.test.claim.body_lowering.if_arm_position", decl_name: "an_if_nested_in_the_then_arm_keeps_the_outer_else_holds", field: WholeDeclaration }, + DeclarationRef { module_path: "v2.test.claim.body_lowering.if_arm_position", decl_name: "a_function_value_in_a_nested_else_lowers_once_holds", field: WholeDeclaration }, + DeclarationRef { module_path: "v2.test.claim.body_lowering.if_arm_position", decl_name: "an_else_if_chain_keeps_every_arm_control_holds", field: WholeDeclaration }, ], } diff --git a/src/v2/compiler/body_lowering_fold.dag b/src/v2/compiler/body_lowering_fold.dag index 1eb52cb08d6..acb37b7f224 100644 --- a/src/v2/compiler/body_lowering_fold.dag +++ b/src/v2/compiler/body_lowering_fold.dag @@ -7049,50 +7049,91 @@ fn body_lower_if_expr_capture_optional(spine: Node) -> Optional { } } -fn body_lower_if_fn_body_capture_optional(spine: Node) -> Optional { - match body_lower_find_captured(root: spine, emitted: ^dag_surface_fn_body) { - ParseSubtreeFound { captured: body } => Present { value: body } - ParseSubtreeAbsent => - if is_empty_conj_root(n: spine) { - Absent - } else { - match body_lower_match_spine_left(spine: spine) { - Present { value: left } => - match body_lower_match_spine_right(spine: spine) { - Present { value: right } => - match node_atom_identity_optional(node: body_lower_deep_unwrap_optional(node: left)) { - Present { value: id } => - match id == ^dag_token_kw_else { - true => body_lower_if_fn_body_capture_optional(spine: right) - false => - match body_lower_if_fn_body_capture_optional(spine: left) { - Present { value: found } => Present { value: found } - Absent => body_lower_if_fn_body_capture_optional(spine: right) - } - } - Absent => - match body_lower_if_fn_body_capture_optional(spine: left) { - Present { value: found } => Present { value: found } - Absent => body_lower_if_fn_body_capture_optional(spine: right) - } - } - Absent => Absent - } - Absent => Absent - } +// THE if_expr ROW IS READ BY POSITION, NEVER SEARCHED. v2.extdeps.languages.dag declares exactly +// two rows: dag_grammar_if_block_expr seq(`if`, seq(cond, seq(fn_body, seq(`else`, if_expr | fn_body)))) +// and dag_grammar_if_then_expr seq(`if`, seq(cond, seq(`then`, seq(expr, seq(`else`, expr))))). Each +// arm is the element at its own slot. The readers this replaces SEARCHED the capture -- the else +// reader recursed into the LEFT subtree before the right whenever the token there was not `else`, so +// for `if b { if c { X } else { Y } } else { Z }` it entered the then-arm and answered the NESTED if's +// else `{ Y }` as the OUTER if's else: Z was dropped, Y lowered twice, and the module was ACCEPTED +// (gunbc.recurring_failure_mode else_arm_lowered_as_an_if_nested_inside_it, capture side). A capture +// that is neither row is Absent, and every caller refuses it as navigation, never guesses. +type IfRowArms { + then_arm: Node, + else_part: Node, +} + +fn body_lower_if_row_arms_optional(captured: Node) -> Optional { + let spine = body_lower_unwrap_surface_shell(node: captured) + match body_lower_if_row_slot_after_token(seq: spine, token: ^dag_token_kw_if) { + Absent => optional_absent() + Present { value: after_if } => + match body_lower_match_spine_right(spine: after_if) { + Absent => optional_absent() + Present { value: after_cond } => + match body_lower_if_row_slot_after_token(seq: after_cond, token: ^dag_token_kw_then) { + Present { value: after_then } => + match body_lower_match_spine_left(spine: after_then) { + Absent => optional_absent() + Present { value: then_expr } => + match body_lower_match_spine_right(spine: after_then) { + Absent => optional_absent() + Present { value: else_seq } => + body_lower_if_row_with_else(then_arm: body_lower_if_row_captured(node: then_expr), else_seq: else_seq) + } + } + Absent => + match body_lower_match_spine_left(spine: after_cond) { + Absent => optional_absent() + Present { value: then_body } => + match body_lower_match_spine_right(spine: after_cond) { + Absent => optional_absent() + Present { value: else_seq } => + body_lower_if_row_with_else(then_arm: body_lower_if_row_captured(node: then_body), else_seq: else_seq) + } + } + } } } } -fn body_lower_if_then_fn_body_optional(captured: Node) -> Optional { - let spine = body_lower_unwrap_surface_shell(node: captured) - match body_lower_if_fn_body_capture_optional(spine: spine) { - Present { value: first } => - match body_lower_find_captured(root: captured, emitted: ^dag_surface_fn_body) { - ParseSubtreeFound { captured: only } => Present { value: only } - ParseSubtreeAbsent => Present { value: first } +// seq(`else`, else_part): the else part, read as the arm readers have always answered it. +fn body_lower_if_row_with_else(then_arm: Node, else_seq: Node) -> Optional { + match body_lower_if_row_slot_after_token(seq: else_seq, token: ^dag_token_kw_else) { + Absent => optional_absent() + Present { value: else_part } => + optional_present(value: IfRowArms { then_arm: then_arm, else_part: body_lower_if_row_else_arm(else_part: else_part) }) + } +} + +// seq(, rest) -> rest, when the left element is exactly that keyword token. +fn body_lower_if_row_slot_after_token(seq: Node, token: Symbol) -> Optional { + match body_lower_match_spine_left(spine: seq) { + Absent => optional_absent() + Present { value: left } => + match node_atom_identity_optional(node: body_lower_deep_unwrap_optional(node: left)) { + Present { value: id } => + if id == token { body_lower_match_spine_right(spine: seq) } else { optional_absent() } + Absent => optional_absent() } - Absent => Absent + } +} + +// An arm slot holds one production (fn_body or expr); the arm readers answer its captured child. +fn body_lower_if_row_captured(node: Node) -> Node { + let shell = body_lower_deep_unwrap_optional(node: node) + match parse_production_captured_child_optional(node: shell) { + Present { value: captured } => captured + Absent => shell + } +} + +// An `else if` arm is answered as its if_expr SHELL, so body_lower_if_arm_lowered sees an if and +// lowers it whole; any other else part is its production's captured child. +fn body_lower_if_row_else_arm(else_part: Node) -> Node { + match body_lower_else_part_if_expr_optional(else_part: else_part) { + Present { value: nested } => nested + Absent => body_lower_if_row_captured(node: else_part) } } @@ -7127,57 +7168,10 @@ fn body_lower_first_production_shell_optional(root: Node) -> Optional { } } -// AN `else if` ARM IS ANSWERED AS ITS if_expr SHELL, so body_lower_if_arm_lowered can see it is an -// if and lower it whole. Answering the shell's captured content instead hid the if_expr identity, and -// the arm's statement-sequence search found the nested then-arm: `if a { b } else if c { d } else { u }` -// lowered to Branch(a, b, d), and both the nested condition and its else reached no reference site. fn body_lower_if_else_capture_optional(captured: Node) -> Optional { - let spine = body_lower_unwrap_surface_shell(node: captured) - match is_empty_conj_root(n: spine) { - true => Absent - false => - match body_lower_match_spine_left(spine: spine) { - Present { value: left } => - match body_lower_match_spine_right(spine: spine) { - Present { value: right } => - match node_atom_identity_optional(node: body_lower_deep_unwrap_optional(node: left)) { - Present { value: id } => - match id == ^dag_token_kw_else { - true => - match body_lower_else_part_if_expr_optional(else_part: right) { - Present { value: nested } => Present { value: nested } - Absent => - match body_lower_if_fn_body_capture_optional(spine: right) { - Present { value: body } => Present { value: body } - Absent => - match body_lower_if_expr_capture_optional(spine: right) { - Present { value: expr } => Present { value: expr } - Absent => Absent - } - } - } - false => - match body_lower_if_else_capture_optional(captured: left) { - Present { value: found } => Present { value: found } - Absent => body_lower_if_else_capture_optional(captured: right) - } - } - Absent => - match body_lower_if_else_capture_optional(captured: left) { - Present { value: found } => Present { value: found } - Absent => body_lower_if_else_capture_optional(captured: right) - } - } - Absent => Absent - } - Absent => - fold(spine.children, init: Absent, f: fn(acc, e) { - match acc { - Present { value: _ } => acc - Absent => body_lower_if_else_capture_optional(captured: e.target) - } - }) - } + match body_lower_if_row_arms_optional(captured: captured) { + Present { value: arms } => optional_present(value: arms.else_part) + Absent => optional_absent() } } @@ -7218,38 +7212,9 @@ fn body_lower_if_condition_optional(captured: Node) -> Optional { } fn body_lower_if_then_arm_optional(captured: Node) -> Optional { - let spine = body_lower_unwrap_surface_shell(node: captured) - match body_lower_find_captured(root: spine, emitted: ^dag_surface_fn_body) { - ParseSubtreeFound { captured: body } => Present { value: body } - ParseSubtreeAbsent => - match body_lower_if_then_fn_body_optional(captured: captured) { - Present { value: body } => Present { value: body } - Absent => - match body_lower_match_spine_left(spine: spine) { - Present { value: left } => - match body_lower_match_spine_right(spine: spine) { - Present { value: right } => - match node_atom_identity_optional(node: body_lower_deep_unwrap_optional(node: left)) { - Present { value: id } => - match id == ^dag_token_kw_then { - true => body_lower_if_expr_capture_optional(spine: right) - false => - match body_lower_if_then_arm_optional(captured: left) { - Present { value: found } => Present { value: found } - Absent => body_lower_if_then_arm_optional(captured: right) - } - } - Absent => - match body_lower_if_then_arm_optional(captured: left) { - Present { value: found } => Present { value: found } - Absent => body_lower_if_then_arm_optional(captured: right) - } - } - Absent => Absent - } - Absent => Absent - } - } + match body_lower_if_row_arms_optional(captured: captured) { + Present { value: arms } => optional_present(value: arms.then_arm) + Absent => optional_absent() } } diff --git a/src/v2/test/claim/body_lowering/if_arm_position_test.dag b/src/v2/test/claim/body_lowering/if_arm_position_test.dag new file mode 100644 index 00000000000..f71c38cf274 --- /dev/null +++ b/src/v2/test/claim/body_lowering/if_arm_position_test.dag @@ -0,0 +1,111 @@ +module v2.test.claim.body_lowering.if_arm_position + +import v2.compiler.normalize { normalize } +import v2.compiler.parse { parse_module } +import v2.compiler.tokenize { tokenize } +import v2.extdeps.languages.dag { dag_language_model } +import v2.std.algebra { fold_list } +import v2.std.diagnostic { Accepted, Rejected, diagnostics_fatal_reason } +import v2.std.grammar { node_atom_identity_optional } +import v2.std.integer { Int } +import v2.std.language_model { LanguageModel } +import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly } +import v2.std.logic { Bool } +import v2.std.node { Node, node_subtree_nodes, symbol_lexeme } +import v2.std.optional { Absent, Optional, Present } +import v2.std.text { String } + +data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly + +// AN if's ARMS ARE READ AT THEIR OWN SLOTS OF THE if_expr ROW. The subject is +// v2.compiler.body_lowering_fold body_lower_if_row_arms_optional, the one reader both arm readers +// project from. The else reader it replaced searched the if's capture and recursed into the left +// subtree first, so for an if nested in the THEN arm it answered the nested if's else as the outer +// if's else: the outer else was dropped, the nested else lowered twice, and normalize ACCEPTED the +// module (gunbc.recurring_failure_mode else_arm_lowered_as_an_if_nested_inside_it, capture side). +// +// THE MEASURE IS AN ATOM COUNT OVER THE NORMALIZED TREE, because the defect is silent: each marker is a +// parameter (one atom in the domain) plus one atom per use, so a marker used once counts 2 when its arm +// was kept exactly once. THE REDS under the searching reader: the outer else's marker counts 1 (dropped) +// and the nested else's counts 3 (lowered twice); and a function value in that nested else refused as +// normalize_reason_minted_occurrence_duplicated, the only form in which the defect was ever loud. +// CONTROLS, TRUE UNDER BOTH: a flat if and a real else-if chain keep every arm once. +// +// The stages are the native route's own, tokenize -> parse -> normalize, and nothing above them. +data iap_cached_lm: LanguageModel = dag_language_model() + +fn iap_normalized_root(src: String) -> Optional { + let lm = iap_cached_lm + match tokenize(text: src, file: ^if_arm_position_subject, rules: lm.lex) { + Rejected { diagnostics: _ } => Absent + Accepted { value: ts, diagnostics: _ } => + match parse_module(tokens: ts, grammar: lm.grammar) { + Rejected { diagnostics: _ } => Absent + Accepted { value: a, diagnostics: _ } => + match normalize(parse_tree: a.tree) { + Rejected { diagnostics: _ } => Absent + Accepted { value: tree, diagnostics: _ } => Present { value: tree.root } + } + } + } +} + +fn iap_normalize_outcome(src: String) -> String { + let lm = iap_cached_lm + match tokenize(text: src, file: ^if_arm_position_subject, rules: lm.lex) { + Rejected { diagnostics: d } => symbol_lexeme(sym: diagnostics_fatal_reason(d: d)) + Accepted { value: ts, diagnostics: _ } => + match parse_module(tokens: ts, grammar: lm.grammar) { + Rejected { diagnostics: d } => symbol_lexeme(sym: diagnostics_fatal_reason(d: d)) + Accepted { value: a, diagnostics: _ } => + match normalize(parse_tree: a.tree) { + Rejected { diagnostics: d } => symbol_lexeme(sym: diagnostics_fatal_reason(d: d)) + Accepted { value: _, diagnostics: _ } => "ACCEPTED" + } + } + } +} + +fn iap_count(root: Node, name: String) -> Int { + fold_list(xs: node_subtree_nodes(root: root), empty: 0, cons: fn(acc, n) { + match node_atom_identity_optional(node: n) { + Present { value: id } => if symbol_lexeme(sym: id) == name { acc + 1 } else { acc } + Absent => acc + } + }) +} + +// Every marker kept exactly once: its parameter atom plus its one use. +fn iap_each_arm_kept_once(src: String) -> Bool { + match iap_normalized_root(src: src) { + Absent => false + Present { value: root } => + (iap_count(root: root, name: "zzz_then") == 2) + && (iap_count(root: root, name: "zzz_inner_else") == 2) + && (iap_count(root: root, name: "zzz_outer_else") == 2) + } +} + +data src_nested_in_then: String = "module m.t\nfn t(b: Bool, c: Bool, zzz_then: Int, zzz_inner_else: Int, zzz_outer_else: Int) -> Int {\n if b {\n if c {\n zzz_then\n } else {\n zzz_inner_else\n }\n } else {\n zzz_outer_else\n }\n}\n" + +data src_flat_and_else_if: String = "module m.t\nfn t(b: Bool, c: Bool, zzz_then: Int, zzz_inner_else: Int, zzz_outer_else: Int) -> Int {\n if b {\n zzz_then\n } else if c {\n zzz_inner_else\n } else {\n zzz_outer_else\n }\n}\n" + +data src_lambda_in_nested_else: String = "module m.t\nfn g(p: Int) -> Bool {\n p > 3\n}\nfn h(w: fn(Int) -> Bool) -> Int {\n 0\n}\nfn t(b: Bool, c: Bool) -> Int {\n if b {\n if c {\n 2\n } else {\n h(w: p => g(p: p))\n }\n } else {\n 0\n }\n}\n" + +data src_fn_literal_in_nested_else: String = "module m.t\nfn g(p: Int) -> Bool {\n p > 3\n}\nfn h(w: fn(Int) -> Bool) -> Int {\n 0\n}\nfn t(b: Bool, c: Bool) -> Int {\n if b {\n if c {\n 2\n } else {\n h(w: fn(p) { g(p: p) })\n }\n } else {\n 0\n }\n}\n" + +test fn an_if_nested_in_the_then_arm_keeps_the_outer_else_holds() -> Bool { + iap_each_arm_kept_once(src: src_nested_in_then) +} + +test fn a_function_value_in_a_nested_else_lowers_once_holds() -> Bool { + iap_normalize_outcome(src: src_lambda_in_nested_else) == "ACCEPTED" +} + +test fn a_fn_literal_in_a_nested_else_lowers_once_holds() -> Bool { + iap_normalize_outcome(src: src_fn_literal_in_nested_else) == "ACCEPTED" +} + +test fn an_else_if_chain_keeps_every_arm_control_holds() -> Bool { + iap_each_arm_kept_once(src: src_flat_and_else_if) +} From 8351814bc0d11ce5ae710e0c6862dcc1cc396939 Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Fri, 2 Oct 2026 23:28:58 +0000 Subject: [PATCH 02/33] if_arm_position: one warm producer for the four claims The first floor run (37073686904) refused all four claims over the new-witness enrolment margin (353k-687k eval steps against 72300): each claim frame paid its own tokenize -> parse -> normalize. iap_verdicts computes the four verdicts once into four Bools (portable: no Node, no closure), each claim reads its field, and the producer is enrolled WARM in v2.workflow.floor_pure_producer_share beside eam_outcomes, the same ground. Co-Authored-By: Claude Opus 5.5 (1M context) --- .../body_lowering/if_arm_position_test.dag | 27 ++++++++++++++++--- src/v2/workflow/floor_pure_producer_share.dag | 4 +++ 2 files changed, 27 insertions(+), 4 deletions(-) diff --git a/src/v2/test/claim/body_lowering/if_arm_position_test.dag b/src/v2/test/claim/body_lowering/if_arm_position_test.dag index f71c38cf274..923f73cd13c 100644 --- a/src/v2/test/claim/body_lowering/if_arm_position_test.dag +++ b/src/v2/test/claim/body_lowering/if_arm_position_test.dag @@ -94,18 +94,37 @@ data src_lambda_in_nested_else: String = "module m.t\nfn g(p: Int) -> Bool {\n data src_fn_literal_in_nested_else: String = "module m.t\nfn g(p: Int) -> Bool {\n p > 3\n}\nfn h(w: fn(Int) -> Bool) -> Int {\n 0\n}\nfn t(b: Bool, c: Bool) -> Int {\n if b {\n if c {\n 2\n } else {\n h(w: fn(p) { g(p: p) })\n }\n } else {\n 0\n }\n}\n" +// ONE PRODUCER FOR EVERY CLAIM, enrolled WARM in v2.workflow.floor_pure_producer_share. Each verdict +// pays a full tokenize -> parse -> normalize of its own source, and the four claims would otherwise +// pay all four per claim frame; the stored value is four Bools (no Node, no closure), so it is portable. +type IapVerdicts { + nested_in_then_keeps_outer_else: Bool, + function_value_in_nested_else_lowers: Bool, + fn_literal_in_nested_else_lowers: Bool, + else_if_chain_keeps_every_arm: Bool, +} + +fn iap_verdicts() -> IapVerdicts { + IapVerdicts { + nested_in_then_keeps_outer_else: iap_each_arm_kept_once(src: src_nested_in_then), + function_value_in_nested_else_lowers: iap_normalize_outcome(src: src_lambda_in_nested_else) == "ACCEPTED", + fn_literal_in_nested_else_lowers: iap_normalize_outcome(src: src_fn_literal_in_nested_else) == "ACCEPTED", + else_if_chain_keeps_every_arm: iap_each_arm_kept_once(src: src_flat_and_else_if), + } +} + test fn an_if_nested_in_the_then_arm_keeps_the_outer_else_holds() -> Bool { - iap_each_arm_kept_once(src: src_nested_in_then) + iap_verdicts().nested_in_then_keeps_outer_else } test fn a_function_value_in_a_nested_else_lowers_once_holds() -> Bool { - iap_normalize_outcome(src: src_lambda_in_nested_else) == "ACCEPTED" + iap_verdicts().function_value_in_nested_else_lowers } test fn a_fn_literal_in_a_nested_else_lowers_once_holds() -> Bool { - iap_normalize_outcome(src: src_fn_literal_in_nested_else) == "ACCEPTED" + iap_verdicts().fn_literal_in_nested_else_lowers } test fn an_else_if_chain_keeps_every_arm_control_holds() -> Bool { - iap_each_arm_kept_once(src: src_flat_and_else_if) + iap_verdicts().else_if_chain_keeps_every_arm } diff --git a/src/v2/workflow/floor_pure_producer_share.dag b/src/v2/workflow/floor_pure_producer_share.dag index 6c9461b1448..72e16e87760 100644 --- a/src/v2/workflow/floor_pure_producer_share.dag +++ b/src/v2/workflow/floor_pure_producer_share.dag @@ -651,6 +651,9 @@ import v2.std.collection { List } // five claims over the enrolment margin at ~590ms each, every one of them paying the same ingest. // THE XL-2 ELSE-ARM ROW IS THE SAME GROUND AT FIVE SPECIMENS: v2.test.claim.namespace_xl0.else_arm_nested_if // eam_outcomes drives one front end over five inline modules and stores one verdict arm per module. +// THE IF-ARM-POSITION ROW IS THE SAME GROUND AT FOUR SPECIMENS: v2.test.claim.body_lowering.if_arm_position +// iap_verdicts tokenizes, parses and normalizes four inline modules and stores four Bools. Its first floor +// run (37073686904) refused all four claims over the enrolment margin, at 353k-687k eval steps each. // THE XL-2 REIFY-OPERAND ROW: v2.test.claim.body_lowering.reify_operand_refusal ror_verdicts tokenizes // and parses two inline modules and reifies two supplied bodies over each; the stored value is four // verdicts (no Node, no closure), portable for the same reason cav_outcomes is. @@ -827,6 +830,7 @@ data floor_cross_claim_pure_producers_warm: List = [ "v2.test.claim.body_lowering.match_position_structure.mps_normalized", "v2.test.claim.namespace_xl0.wildcard_arm_resolve.wc_outcomes", "v2.test.claim.namespace_xl0.else_arm_nested_if.eam_outcomes", + "v2.test.claim.body_lowering.if_arm_position.iap_verdicts", "v2.test.cli.v2_native_cli.cli_probe_trailing_outcome", "v2.test.emit.closure_emit_arrow_body_refusal.arrow_body_probe_verdict", "v2.test.emit.closure_emit_arrow_body_refusal.arrow_body_mixed_probe_verdict", From 4a1a9bd45f2c51bb38cfe27b68c61e9a59ce00cd Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Sat, 3 Oct 2026 00:12:03 +0000 Subject: [PATCH 03/33] nested_if_else_eval: the evaluated form of the nested-if else arm `if false { if true {1} else {2} } else {3}` is 3. The searching else reader took the nested `else { 2 }` as the outer else, so a body lowered through it answers 2. The mirror (`if true { if false {1} else {2} } else {3}` is 2) holds under either reader and is the control. The module is import-free: the floor evaluates it through the seed, and the native lane through the emitted compiler's own body lowering, where it is the discriminating red. It is not yet merge-blocking evidence for the v2 reader, since the native lane is not a required lane. Co-Authored-By: Claude Opus 5.5 (1M context) --- .../nested_if_else_eval_test.dag | 43 +++++++++++++++++++ 1 file changed, 43 insertions(+) create mode 100644 src/v2/test/claim/body_lowering/nested_if_else_eval_test.dag diff --git a/src/v2/test/claim/body_lowering/nested_if_else_eval_test.dag b/src/v2/test/claim/body_lowering/nested_if_else_eval_test.dag new file mode 100644 index 00000000000..5f23e05fa23 --- /dev/null +++ b/src/v2/test/claim/body_lowering/nested_if_else_eval_test.dag @@ -0,0 +1,43 @@ +module v2.test.claim.body_lowering.nested_if_else_eval + +// THE EVALUATED FORM OF THE NESTED-IF ELSE ARM (gunbc.recurring_failure_mode +// else_arm_lowered_as_an_if_nested_inside_it, capture side). The outer condition is false, so the +// program's value is the OUTER else, 3. The searching else reader took the nested if's `else { 2 }` as +// the outer if's else, so a body lowered through it answers 2: the dropped arm changes the evaluated +// result, not only the atom count v2.test.claim.body_lowering.if_arm_position measures. Import-free on +// purpose, so the native route prepares it cheaply: the floor evaluates it through the seed, and the +// native lane evaluates it through the emitted compiler's own body lowering, where it is the +// discriminating red for the arm readers. +fn nested_if_else_value() -> Int { + if false { + if true { + 1 + } else { + 2 + } + } else { + 3 + } +} + +// THE MIRROR: the outer condition is true, so the value is the nested if's own else, 2. It holds under +// either reader, so it is the control that the subject's red is the dropped OUTER else and nothing else. +fn nested_if_then_value() -> Int { + if true { + if false { + 1 + } else { + 2 + } + } else { + 3 + } +} + +test fn the_outer_else_of_an_if_nested_in_the_then_arm_is_the_value_holds() -> Bool { + nested_if_else_value() == 3 +} + +test fn the_nested_else_inside_the_then_arm_is_the_value_control_holds() -> Bool { + nested_if_then_value() == 2 +} From 020dcee503b63a51d3477f8704b82e43c52e555a Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Sat, 3 Oct 2026 00:17:56 +0000 Subject: [PATCH 04/33] v2 parse: choice-overlap proof reads k=2 lookahead and proves not-predicate guards A FIRST-overlap row is now removed only when the declared lookahead (k=2) proves the alternatives disjoint. A leading not-predicate subtracts the prefixes it is proved to cover, and only when the guard is plain (a finite token-string set whose PEG success is membership). A guard naming one word of a class narrows that position to class-less-word (the k=1 op_requires shape). Every undecidable arm keeps the row. Roster 51 -> 48: stmt return-vs-bare-assignment, let_expr let-vs-bare, let_sugar node-vs-bare are disjoint at k=2. Co-Authored-By: Claude Opus 5.5 (1M context) --- src/v2/compiler/02_parse.dag | 693 +++++++++++++++++- .../parse/choice_lookahead_guard_test.dag | 154 ++++ src/v2/test/claim/parse/choice_plan_test.dag | 3 + 3 files changed, 836 insertions(+), 14 deletions(-) create mode 100644 src/v2/test/claim/parse/choice_lookahead_guard_test.dag diff --git a/src/v2/compiler/02_parse.dag b/src/v2/compiler/02_parse.dag index 5b1a8ee7ce4..b22176b5f6b 100644 --- a/src/v2/compiler/02_parse.dag +++ b/src/v2/compiler/02_parse.dag @@ -2332,6 +2332,615 @@ fn expr_first_fold_from_prepared( } } +// THE CHOICE-OVERLAP PROOF READS A DECLARED k TOKENS OF LOOKAHEAD, AND A GUARD COUNTS ONLY WHERE IT +// IS PROVED TO COVER. (operator zero_ambiguity_ruling 2026-10-02, stern-bear-500 ruling A.) A +// single-token FIRST overlap is the candidate row; the row is removed only when the k-prefix sets of +// the alternative and of every alternative after it are disjoint. A leading not-predicate `!G X` +// subtracts from X's prefixes exactly the prefixes every string of which begins with a string of G, +// and only when G is a PLAIN guard (lookahead_guard_strings): a finite set of token strings whose PEG +// success is membership. Where one position of a prefix is a whole token class and G names one word +// of it, the class is narrowed to the class less that word -- the k=1 shape +// `!('none' | 'opaque') type_list`. Every undecidable arm -- a cycle without consumption, a missing +// production, a guard that is not plain, a guard string longer than the prefix it would cover -- +// answers by subtracting nothing or by LookaheadUnknown, and Unknown keeps the row. So the proof +// removes rows and never widens: a guard that misses one prefix is the near miss that keeps its row. +fn grammar_choice_lookahead_depth() -> Int { 2 } + +type LookaheadContext { + productions: Map + nullable_set: List + first_rows: Map> +} + +// One position of a prefix: the FirstKey it reads, less the exact words of its class a proved +// guard removed. `excluded` is empty unless `key` is FirstAnyOfClass. +type LookaheadKey { + key: FirstKey + excluded: List +} + +// `complete`: the alternative can END after `keys`, so a following sequence element extends it. +type LookaheadPrefix { + keys: List + complete: Bool +} + +type LookaheadPrefixes + = LookaheadKnown { prefixes: List } + | LookaheadUnknown + +type GuardCoverage + = GuardCoversAll + | GuardCoversButOneWord { keys: List } + | GuardMisses + +fn lookahead_prefix_keys(p: LookaheadPrefix) -> List { p.keys } +fn lookahead_prefix_complete(p: LookaheadPrefix) -> Bool { p.complete } +fn lookahead_production_expression(p: GrammarProduction) -> GrammarExpr { p.expression } + +fn lookahead_none() -> LookaheadPrefixes { LookaheadKnown { prefixes: std.algebra.Empty } } + +fn lookahead_empty_only() -> LookaheadPrefixes { + LookaheadKnown { + prefixes: Cons { head: LookaheadPrefix { keys: std.algebra.Empty, complete: true }, tail: std.algebra.Empty } + } +} + +fn lookahead_union(left: LookaheadPrefixes, right: LookaheadPrefixes) -> LookaheadPrefixes { + match left { + LookaheadUnknown => LookaheadUnknown + LookaheadKnown { prefixes: l } => + match right { + LookaheadUnknown => LookaheadUnknown + LookaheadKnown { prefixes: r } => LookaheadKnown { prefixes: list_append(left: l, right: r) } + } + } +} + +fn lookahead_head_admits(head_keys: Optional>, key: FirstKey) -> Bool { + match head_keys { + Absent => true + Present { value: keys } => any(xs: keys, predicate: fn(k) { first_key_overlaps(left: k, right: key) }) + } +} + +fn lookahead_token(key: FirstKey, head_keys: Optional>) -> LookaheadPrefixes { + if lookahead_head_admits(head_keys: head_keys, key: key) { + LookaheadKnown { + prefixes: Cons { + head: LookaheadPrefix { + keys: Cons { head: LookaheadKey { key: key, excluded: std.algebra.Empty }, tail: std.algebra.Empty }, + complete: true + }, + tail: std.algebra.Empty + } + } + } else { + lookahead_none() + } +} + +// One token left and no head restriction: the production's FIRST row already answers it. +fn lookahead_from_first(first: List, nullable: Bool) -> LookaheadPrefixes { + let singles = fold_list( + xs: first, + empty: std.algebra.Empty, + cons: fn(acc, k) { + list_snoc_item( + xs: acc, + item: LookaheadPrefix { + keys: Cons { head: LookaheadKey { key: k, excluded: std.algebra.Empty }, tail: std.algebra.Empty }, + complete: false + } + ) + } + ) + let known = LookaheadKnown { prefixes: singles } + if nullable { lookahead_union(left: known, right: lookahead_empty_only()) } else { known } +} + +fn lookahead_prefixes( + expr: GrammarExpr, + depth: Int, + head_keys: Optional>, + visiting: List, + ctx: LookaheadContext +) -> LookaheadPrefixes { + match expr { + Terminal { token_class: c, stamp: _ } => lookahead_token(key: FirstAnyOfClass { token_class: c }, head_keys: head_keys) + LiteralTerminal { token_class: c, lexeme: w } => + lookahead_token(key: FirstExactWord { token_class: c, lexeme: w }, head_keys: head_keys) + Nonterminal { production: name } => + lookahead_nonterminal(name: name, depth: depth, head_keys: head_keys, visiting: visiting, ctx: ctx) + Sequence { left: left, right: right } => + lookahead_sequence(left: left, right: right, depth: depth, head_keys: head_keys, visiting: visiting, ctx: ctx) + Choice { left: left, right: right } => + lookahead_union( + left: lookahead_prefixes(expr: left, depth: depth, head_keys: head_keys, visiting: visiting, ctx: ctx), + right: lookahead_prefixes(expr: right, depth: depth, head_keys: head_keys, visiting: visiting, ctx: ctx) + ) + Optional { element: element } => + lookahead_union( + left: lookahead_prefixes(expr: element, depth: depth, head_keys: head_keys, visiting: visiting, ctx: ctx), + right: lookahead_empty_only() + ) + Repeat { element: element } => + lookahead_repeat(element: element, depth: depth, head_keys: head_keys, visiting: visiting, ctx: ctx) + Expect { element: element, reason: _ } => + lookahead_prefixes(expr: element, depth: depth, head_keys: head_keys, visiting: visiting, ctx: ctx) + RefuseOnMatch { element: element, reason: _ } => + lookahead_prefixes(expr: element, depth: depth, head_keys: head_keys, visiting: visiting, ctx: ctx) + AfterLineBreak { element: element } => + lookahead_prefixes(expr: element, depth: depth, head_keys: head_keys, visiting: visiting, ctx: ctx) + NotPredicate { element: _ } => lookahead_empty_only() + } +} + +// A production re-entered before any token is consumed is a cycle the bounded walk cannot decide. +fn lookahead_nonterminal( + name: Symbol, + depth: Int, + head_keys: Optional>, + visiting: List, + ctx: LookaheadContext +) -> LookaheadPrefixes { + let nullable = symbol_list_contains(xs: ctx.nullable_set, item: name) + let first = production_first_row_lookup(rows: ctx.first_rows, name: name) + match head_keys { + Present { value: keys } => + if !nullable && is_empty(xs: first_list_intersect(left: first, right: keys)) { + lookahead_none() + } else { + lookahead_nonterminal_expand(name: name, depth: depth, head_keys: head_keys, visiting: visiting, ctx: ctx) + } + Absent => + if depth == 1 { + lookahead_from_first(first: first, nullable: nullable) + } else { + lookahead_nonterminal_expand(name: name, depth: depth, head_keys: head_keys, visiting: visiting, ctx: ctx) + } + } +} + +fn lookahead_nonterminal_expand( + name: Symbol, + depth: Int, + head_keys: Optional>, + visiting: List, + ctx: LookaheadContext +) -> LookaheadPrefixes { + if symbol_list_contains(xs: visiting, item: name) { + LookaheadUnknown + } else { + match map_lookup(m: ctx.productions, key: name) { + Present { value: p } => + lookahead_prefixes( + expr: lookahead_production_expression(p: p), + depth: depth, + head_keys: head_keys, + visiting: Cons { head: name, tail: visiting }, + ctx: ctx + ) + Absent => LookaheadUnknown + } + } +} + +fn lookahead_sequence( + left: GrammarExpr, + right: GrammarExpr, + depth: Int, + head_keys: Optional>, + visiting: List, + ctx: LookaheadContext +) -> LookaheadPrefixes { + match left { + NotPredicate { element: guard } => + lookahead_subtract_guard( + prefixes: lookahead_prefixes(expr: right, depth: depth, head_keys: head_keys, visiting: visiting, ctx: ctx), + guard: guard, + ctx: ctx + ) + _ => + lookahead_extend( + prefixes: lookahead_prefixes(expr: left, depth: depth, head_keys: head_keys, visiting: visiting, ctx: ctx), + right: right, + depth: depth, + head_keys: head_keys, + visiting: visiting, + ctx: ctx + ) + } +} + +fn lookahead_prepend(keys: List, prefixes: LookaheadPrefixes) -> LookaheadPrefixes { + match prefixes { + LookaheadUnknown => LookaheadUnknown + LookaheadKnown { prefixes: ps } => + LookaheadKnown { + prefixes: fold_list( + xs: ps, + empty: std.algebra.Empty, + cons: fn(acc, q) { + list_snoc_item( + xs: acc, + item: LookaheadPrefix { + keys: list_append(left: keys, right: lookahead_prefix_keys(p: q)), + complete: lookahead_prefix_complete(p: q) + } + ) + } + ) + } + } +} + +fn lookahead_truncated(keys: List) -> LookaheadPrefixes { + LookaheadKnown { prefixes: Cons { head: LookaheadPrefix { keys: keys, complete: false }, tail: std.algebra.Empty } } +} + +// Extend each prefix that ended early by the prefixes of what follows. The head restriction and the +// cycle set hold only while nothing has been consumed. +fn lookahead_extend_one( + prefix: LookaheadPrefix, + right: GrammarExpr, + depth: Int, + head_keys: Optional>, + visiting: List, + ctx: LookaheadContext +) -> LookaheadPrefixes { + let used = length(xs: prefix.keys) + if prefix.complete && used < depth { + if used == 0 { + lookahead_prefixes(expr: right, depth: depth, head_keys: head_keys, visiting: visiting, ctx: ctx) + } else { + lookahead_prepend( + keys: prefix.keys, + prefixes: lookahead_prefixes(expr: right, depth: depth - used, head_keys: Absent, visiting: std.algebra.Empty, ctx: ctx) + ) + } + } else { + lookahead_truncated(keys: prefix.keys) + } +} + +fn lookahead_extend( + prefixes: LookaheadPrefixes, + right: GrammarExpr, + depth: Int, + head_keys: Optional>, + visiting: List, + ctx: LookaheadContext +) -> LookaheadPrefixes { + match prefixes { + LookaheadUnknown => LookaheadUnknown + LookaheadKnown { prefixes: ps } => + fold_list( + xs: ps, + empty: lookahead_none(), + cons: fn(acc, p) { + lookahead_union( + left: acc, + right: lookahead_extend_one(prefix: p, right: right, depth: depth, head_keys: head_keys, visiting: visiting, ctx: ctx) + ) + } + ) + } +} + +// Zero or more: the empty prefix, and each consuming iteration extended by the repeat again. An +// iteration that consumed nothing adds nothing the empty prefix does not already say. +fn lookahead_repeat( + element: GrammarExpr, + depth: Int, + head_keys: Optional>, + visiting: List, + ctx: LookaheadContext +) -> LookaheadPrefixes { + match lookahead_prefixes(expr: element, depth: depth, head_keys: head_keys, visiting: visiting, ctx: ctx) { + LookaheadUnknown => LookaheadUnknown + LookaheadKnown { prefixes: ps } => + fold_list( + xs: ps, + empty: lookahead_empty_only(), + cons: fn(acc, p) { + lookahead_union(left: acc, right: lookahead_repeat_one(prefix: p, element: element, depth: depth, ctx: ctx)) + } + ) + } +} + +fn lookahead_repeat_one(prefix: LookaheadPrefix, element: GrammarExpr, depth: Int, ctx: LookaheadContext) -> LookaheadPrefixes { + let used = length(xs: prefix.keys) + if used == 0 { + lookahead_none() + } else { + if prefix.complete && used < depth { + lookahead_prepend( + keys: prefix.keys, + prefixes: lookahead_repeat(element: element, depth: depth - used, head_keys: Absent, visiting: std.algebra.Empty, ctx: ctx) + ) + } else { + lookahead_truncated(keys: prefix.keys) + } + } +} + +// A PLAIN GUARD'S STRINGS. A guard is plain when its PEG success is exactly "the input begins with one +// of these token strings": a token, a choice of plain guards, or a single-token set followed by a +// plain guard. A choice that is not last in a sequence is not plain -- `(x / x y) z` fails on +// `x y z` under ordered choice -- so it answers Absent and the guard subtracts nothing. +fn lookahead_guard_strings(expr: GrammarExpr, visiting: List, ctx: LookaheadContext) -> Optional>> { + match expr { + Terminal { token_class: c, stamp: _ } => + Present { value: Cons { head: Cons { head: FirstAnyOfClass { token_class: c }, tail: std.algebra.Empty }, tail: std.algebra.Empty } } + LiteralTerminal { token_class: c, lexeme: w } => + Present { value: Cons { head: Cons { head: FirstExactWord { token_class: c, lexeme: w }, tail: std.algebra.Empty }, tail: std.algebra.Empty } } + Choice { left: left, right: right } => + match lookahead_guard_strings(expr: left, visiting: visiting, ctx: ctx) { + Absent => Absent + Present { value: l } => + match lookahead_guard_strings(expr: right, visiting: visiting, ctx: ctx) { + Absent => Absent + Present { value: r } => Present { value: list_append(left: l, right: r) } + } + } + Sequence { left: left, right: right } => + match lookahead_guard_token_set(expr: left, visiting: visiting, ctx: ctx) { + Absent => Absent + Present { value: heads } => + match lookahead_guard_strings(expr: right, visiting: std.algebra.Empty, ctx: ctx) { + Absent => Absent + Present { value: tails } => + Present { + value: fold_list( + xs: heads, + empty: std.algebra.Empty, + cons: fn(acc, h) { + list_append( + left: acc, + right: fold_list( + xs: tails, + empty: std.algebra.Empty, + cons: fn(inner, t) { list_snoc_item(xs: inner, item: Cons { head: h, tail: t }) } + ) + ) + } + ) + } + } + } + Nonterminal { production: name } => + if symbol_list_contains(xs: visiting, item: name) { + Absent + } else { + match map_lookup(m: ctx.productions, key: name) { + Present { value: p } => + lookahead_guard_strings(expr: lookahead_production_expression(p: p), visiting: Cons { head: name, tail: visiting }, ctx: ctx) + Absent => Absent + } + } + _ => Absent + } +} + +// A set of single tokens, each alternative consuming exactly one token. +fn lookahead_guard_token_set(expr: GrammarExpr, visiting: List, ctx: LookaheadContext) -> Optional> { + match expr { + Terminal { token_class: c, stamp: _ } => Present { value: Cons { head: FirstAnyOfClass { token_class: c }, tail: std.algebra.Empty } } + LiteralTerminal { token_class: c, lexeme: w } => + Present { value: Cons { head: FirstExactWord { token_class: c, lexeme: w }, tail: std.algebra.Empty } } + Choice { left: left, right: right } => + match lookahead_guard_token_set(expr: left, visiting: visiting, ctx: ctx) { + Absent => Absent + Present { value: l } => + match lookahead_guard_token_set(expr: right, visiting: visiting, ctx: ctx) { + Absent => Absent + Present { value: r } => Present { value: list_append(left: l, right: r) } + } + } + Nonterminal { production: name } => + if symbol_list_contains(xs: visiting, item: name) { + Absent + } else { + match map_lookup(m: ctx.productions, key: name) { + Present { value: p } => + lookahead_guard_token_set(expr: lookahead_production_expression(p: p), visiting: Cons { head: name, tail: visiting }, ctx: ctx) + Absent => Absent + } + } + _ => Absent + } +} + +fn lookahead_subtract_guard(prefixes: LookaheadPrefixes, guard: GrammarExpr, ctx: LookaheadContext) -> LookaheadPrefixes { + match prefixes { + LookaheadUnknown => LookaheadUnknown + LookaheadKnown { prefixes: ps } => + match lookahead_guard_strings(expr: guard, visiting: std.algebra.Empty, ctx: ctx) { + Absent => LookaheadKnown { prefixes: ps } + Present { value: strings } => + LookaheadKnown { + prefixes: fold_list( + xs: strings, + empty: ps, + cons: fn(acc, g) { lookahead_subtract_string(prefixes: acc, guard: g) } + ) + } + } + } +} + +fn lookahead_subtract_string(prefixes: List, guard: List) -> List { + fold_list( + xs: prefixes, + empty: std.algebra.Empty, + cons: fn(acc, p) { + match lookahead_guard_coverage(keys: lookahead_prefix_keys(p: p), guard: guard) { + GuardCoversAll => acc + GuardCoversButOneWord { keys: narrowed } => + list_snoc_item(xs: acc, item: LookaheadPrefix { keys: narrowed, complete: lookahead_prefix_complete(p: p) }) + GuardMisses => list_snoc_item(xs: acc, item: p) + } + } + ) +} + +// Every string the prefix denotes begins with the guard string (GuardCoversAll), or does so exactly +// when one class position holds one named word (GuardCoversButOneWord, that word excluded). A guard +// string longer than the prefix covers nothing the bounded walk can see. +fn lookahead_guard_coverage(keys: List, guard: List) -> GuardCoverage { + match list_head(xs: guard) { + HeadAbsent => GuardCoversAll + HeadFound { value: g } => + match list_head(xs: keys) { + HeadAbsent => GuardMisses + HeadFound { value: k } => + lookahead_guard_coverage_at( + key: k, + guard_key: g, + rest: lookahead_guard_coverage(keys: lookahead_list_rest(xs: keys), guard: lookahead_list_rest(xs: guard)), + keys_rest: lookahead_list_rest(xs: keys) + ) + } + } +} + +fn lookahead_list_rest(xs: List) -> List { + match list_tail(xs: xs) { + TailFound { tail: rest } => rest + TailAbsent => std.algebra.Empty + } +} + +fn lookahead_guard_coverage_at(key: LookaheadKey, guard_key: FirstKey, rest: GuardCoverage, keys_rest: List) -> GuardCoverage { + if lookahead_guard_key_covers(guard_key: guard_key, key: key.key) { + match rest { + GuardCoversAll => GuardCoversAll + GuardCoversButOneWord { keys: narrowed } => GuardCoversButOneWord { keys: Cons { head: key, tail: narrowed } } + GuardMisses => GuardMisses + } + } else { + match lookahead_guard_word_of_class(guard_key: guard_key, key: key.key) { + Absent => GuardMisses + Present { value: word } => + match rest { + GuardCoversAll => + GuardCoversButOneWord { + keys: Cons { + head: LookaheadKey { key: key.key, excluded: set_symbol_insert(s: key.excluded, item: word) }, + tail: keys_rest + } + } + GuardCoversButOneWord { keys: _ } => GuardMisses + GuardMisses => GuardMisses + } + } + } +} + +// The guard key matches every token the prefix key admits. +fn lookahead_guard_key_covers(guard_key: FirstKey, key: FirstKey) -> Bool { + match guard_key { + FirstAnyOfClass { token_class: gc } => first_key_class(key: key) == gc + FirstExactWord { token_class: _, lexeme: _ } => first_key_eq(left: guard_key, right: key) + } +} + +// The guard names one word of a class the prefix admits whole. +fn lookahead_guard_word_of_class(guard_key: FirstKey, key: FirstKey) -> Optional { + match guard_key { + FirstAnyOfClass { token_class: _ } => Absent + FirstExactWord { token_class: gc, lexeme: w } => + match key { + FirstAnyOfClass { token_class: kc } => lookahead_word_if_same_class(word: w, guard_class: gc, key_class: kc) + FirstExactWord { token_class: _, lexeme: _ } => Absent + } + } +} + +fn lookahead_word_if_same_class(word: Symbol, guard_class: Symbol, key_class: Symbol) -> Optional { + if guard_class == key_class { lookahead_word_present(word: word) } else { lookahead_word_absent() } +} + +fn lookahead_word_present(word: Symbol) -> Optional { Present { value: word } } +fn lookahead_word_absent() -> Optional { Absent } + +fn lookahead_key_excludes(key: LookaheadKey, other: FirstKey) -> Bool { + match other { + FirstExactWord { token_class: _, lexeme: w } => symbol_list_contains(xs: key.excluded, item: w) + FirstAnyOfClass { token_class: _ } => false + } +} + +fn lookahead_key_overlaps(left: LookaheadKey, right: LookaheadKey) -> Bool { + first_key_overlaps(left: left.key, right: right.key) + && !lookahead_key_excludes(key: left, other: right.key) + && !lookahead_key_excludes(key: right, other: left.key) +} + +// Two prefixes overlap when every position both read could be one token. A shorter prefix overlaps +// any longer one it agrees with, so a short alternative is never proved disjoint by its brevity. +fn lookahead_prefix_keys_overlap(left: List, right: List) -> Bool { + match list_head(xs: left) { + HeadAbsent => true + HeadFound { value: l } => + match list_head(xs: right) { + HeadAbsent => true + HeadFound { value: r } => + lookahead_key_overlaps(left: l, right: r) + && lookahead_prefix_keys_overlap(left: lookahead_list_rest(xs: left), right: lookahead_list_rest(xs: right)) + } + } +} + +// The empty prefix (a nullable alternative) is the both-nullable row's question, not this one's, so +// it is not compared here -- exactly as the single-token FIRST check never counted it. +fn lookahead_prefix_sets_overlap(left: List, right: List) -> Bool { + any( + xs: left, + predicate: fn(l) { + !is_empty(xs: lookahead_prefix_keys(p: l)) + && any( + xs: right, + predicate: fn(r) { + !is_empty(xs: lookahead_prefix_keys(p: r)) + && lookahead_prefix_keys_overlap(left: lookahead_prefix_keys(p: l), right: lookahead_prefix_keys(p: r)) + } + ) + } + ) +} + +fn lookahead_alternatives_overlap( + left: GrammarExpr, + rest: List, + head_keys: List, + ctx: LookaheadContext +) -> Bool { + let depth = grammar_choice_lookahead_depth() + let restrict = Present { value: head_keys } + let left_prefixes = lookahead_prefixes(expr: left, depth: depth, head_keys: restrict, visiting: std.algebra.Empty, ctx: ctx) + let right_prefixes = fold_list( + xs: rest, + empty: lookahead_none(), + cons: fn(acc, alt) { + lookahead_union( + left: acc, + right: lookahead_prefixes(expr: alt, depth: depth, head_keys: restrict, visiting: std.algebra.Empty, ctx: ctx) + ) + } + ) + match left_prefixes { + LookaheadUnknown => true + LookaheadKnown { prefixes: l } => + match right_prefixes { + LookaheadUnknown => true + LookaheadKnown { prefixes: r } => lookahead_prefix_sets_overlap(left: l, right: r) + } + } +} + fn ordered_backtrack_row( production: Symbol, alts: List @@ -2358,7 +2967,17 @@ fn ordered_backtrack_emit(alts: List) -> PreparedChoicePlan { ChoiceOrderedBacktrack { alternatives: choice_alt_trees(alts: alts) } } -fn authored_choice_site_residue(alts: List, production: Symbol) -> List { +// A ROW STANDS UNLESS THE DECLARED LOOKAHEAD PROVES THE ALTERNATIVES DISJOINT. The single-token +// overlap is the candidate; a candidate is dropped only when the k-prefix sets of the alternative +// and of the alternatives after it share no prefix (lookahead_alternatives_overlap). Every arm of +// that proof that cannot decide answers "overlap", so the proof can remove a row and never adds +// a route: a guard that does not cover keeps its row, and an ordering never stands for a proof. +fn authored_choice_site_residue( + alts: List, + raw_alts: List, + production: Symbol, + ctx: LookaheadContext +) -> List { match list_tail(xs: alts) { TailAbsent => std.algebra.Empty TailFound { tail: rest } => @@ -2366,19 +2985,54 @@ fn authored_choice_site_residue(alts: List, production: Symbol std.algebra.Empty } else { let row = ordered_backtrack_row(production: production, alts: alts) - let here = if !is_empty(xs: row.overlap_terminals) || row.both_nullable { + let raw_rest = match list_tail(xs: raw_alts) { + TailFound { tail: r } => r + TailAbsent => std.algebra.Empty + } + let stands = row.both_nullable || ( + !is_empty(xs: row.overlap_terminals) + && lookahead_site_overlaps(alts: alts, raw_alts: raw_alts, raw_rest: raw_rest, ctx: ctx) + ) + let here = if stands { Cons { head: row, tail: std.algebra.Empty } } else { std.algebra.Empty } list_append( left: here, - right: authored_choice_site_residue(alts: rest, production: production) + right: authored_choice_site_residue(alts: rest, raw_alts: raw_rest, production: production, ctx: ctx) ) } } } +fn lookahead_site_overlaps( + alts: List, + raw_alts: List, + raw_rest: List, + ctx: LookaheadContext +) -> Bool { + let empty_first = GrammarExprFirstFold { terminals: grammar_empty_terminal_list(), nullable: false } + let left_first = match list_head(xs: alts) { + HeadFound { value: alt } => prepared_expr_fold_first(alt: alt) + HeadAbsent => empty_first + } + let right_first = match list_tail(xs: alts) { + TailFound { tail: rest } => choice_alts_union_first_from(alts: rest, acc: empty_first) + TailAbsent => empty_first + } + match list_head(xs: raw_alts) { + HeadAbsent => true + HeadFound { value: left } => + lookahead_alternatives_overlap( + left: left, + rest: raw_rest, + head_keys: first_list_intersect(left: left_first.terminals, right: right_first.terminals), + ctx: ctx + ) + } +} + fn compile_choice_alts( alts: List, nullable_set: List, @@ -2546,6 +3200,7 @@ fn prepare_grammar_expr( expr: GrammarExpr, nullable_set: List, first_rows: Map>, + productions: Map, production: Symbol, token_dispatch: Bool ) -> PreparedExprFold { @@ -2569,8 +3224,8 @@ fn prepare_grammar_expr( residue: std.algebra.Empty } Sequence { left: left, right: right } => - let left_prepared = prepare_grammar_expr(expr: left, nullable_set: nullable_set, first_rows: first_rows, production: production, token_dispatch: token_dispatch) - let right_prepared = prepare_grammar_expr(expr: right, nullable_set: nullable_set, first_rows: first_rows, production: production, token_dispatch: token_dispatch) + let left_prepared = prepare_grammar_expr(expr: left, nullable_set: nullable_set, first_rows: first_rows, productions: productions, production: production, token_dispatch: token_dispatch) + let right_prepared = prepare_grammar_expr(expr: right, nullable_set: nullable_set, first_rows: first_rows, productions: productions, production: production, token_dispatch: token_dispatch) PreparedExprFold { tree: PreparedSequence { left: left_prepared.tree, right: right_prepared.tree }, first: expr_first_fold_sequence(left: left_prepared.first, right: right_prepared.first), @@ -2584,7 +3239,7 @@ fn prepare_grammar_expr( cons: fn(acc, alt) { list_snoc_item( xs: acc, - item: prepare_grammar_expr(expr: alt, nullable_set: nullable_set, first_rows: first_rows, production: production, token_dispatch: token_dispatch) + item: prepare_grammar_expr(expr: alt, nullable_set: nullable_set, first_rows: first_rows, productions: productions, production: production, token_dispatch: token_dispatch) ) } ) @@ -2603,46 +3258,51 @@ fn prepare_grammar_expr( first: union_first, residue: list_append( left: concat_prepared_alt_residue(alts: prepared_alts), - right: authored_choice_site_residue(alts: prepared_alts, production: production) + right: authored_choice_site_residue( + alts: prepared_alts, + raw_alts: alts, + production: production, + ctx: LookaheadContext { productions: productions, nullable_set: nullable_set, first_rows: first_rows } + ) ) } Optional { element: element } => - let element_prepared = prepare_grammar_expr(expr: element, nullable_set: nullable_set, first_rows: first_rows, production: production, token_dispatch: token_dispatch) + let element_prepared = prepare_grammar_expr(expr: element, nullable_set: nullable_set, first_rows: first_rows, productions: productions, production: production, token_dispatch: token_dispatch) PreparedExprFold { tree: PreparedOptional { element: element_prepared.tree }, first: expr_first_fold_optional(element: element_prepared.first), residue: element_prepared.residue } Repeat { element: element } => - let element_prepared = prepare_grammar_expr(expr: element, nullable_set: nullable_set, first_rows: first_rows, production: production, token_dispatch: token_dispatch) + let element_prepared = prepare_grammar_expr(expr: element, nullable_set: nullable_set, first_rows: first_rows, productions: productions, production: production, token_dispatch: token_dispatch) PreparedExprFold { tree: PreparedRepeat { element: element_prepared.tree }, first: expr_first_fold_repeat(element: element_prepared.first), residue: element_prepared.residue } Expect { element: element, reason: reason } => - let element_prepared = prepare_grammar_expr(expr: element, nullable_set: nullable_set, first_rows: first_rows, production: production, token_dispatch: token_dispatch) + let element_prepared = prepare_grammar_expr(expr: element, nullable_set: nullable_set, first_rows: first_rows, productions: productions, production: production, token_dispatch: token_dispatch) PreparedExprFold { tree: PreparedExpect { element: element_prepared.tree, reason: reason }, first: element_prepared.first, residue: element_prepared.residue } RefuseOnMatch { element: element, reason: reason } => - let element_prepared = prepare_grammar_expr(expr: element, nullable_set: nullable_set, first_rows: first_rows, production: production, token_dispatch: token_dispatch) + let element_prepared = prepare_grammar_expr(expr: element, nullable_set: nullable_set, first_rows: first_rows, productions: productions, production: production, token_dispatch: token_dispatch) PreparedExprFold { tree: PreparedRefuseOnMatch { element: element_prepared.tree, reason: reason }, first: element_prepared.first, residue: element_prepared.residue } AfterLineBreak { element: element } => - let element_prepared = prepare_grammar_expr(expr: element, nullable_set: nullable_set, first_rows: first_rows, production: production, token_dispatch: token_dispatch) + let element_prepared = prepare_grammar_expr(expr: element, nullable_set: nullable_set, first_rows: first_rows, productions: productions, production: production, token_dispatch: token_dispatch) PreparedExprFold { tree: PreparedAfterLineBreak { element: element_prepared.tree }, first: element_prepared.first, residue: element_prepared.residue } NotPredicate { element: element } => - let element_prepared = prepare_grammar_expr(expr: element, nullable_set: nullable_set, first_rows: first_rows, production: production, token_dispatch: token_dispatch) + let element_prepared = prepare_grammar_expr(expr: element, nullable_set: nullable_set, first_rows: first_rows, productions: productions, production: production, token_dispatch: token_dispatch) PreparedExprFold { tree: PreparedNotPredicate { element: element_prepared.tree, first: element_prepared.first }, first: expr_first_fold_predicate(), @@ -2673,6 +3333,7 @@ fn parse_table_prepared_expr(table: ParseTable, production: GrammarProduction) - expr: production.expression, nullable_set: table.nullable_set, first_rows: table.first_rows, + productions: empty_map(), production: production.name, token_dispatch: parse_table_token_dispatch(table: table, production: production.name) ).tree @@ -2681,6 +3342,7 @@ fn parse_table_prepared_expr(table: ParseTable, production: GrammarProduction) - expr: production.expression, nullable_set: table.nullable_set, first_rows: table.first_rows, + productions: empty_map(), production: production.name, token_dispatch: parse_table_token_dispatch(table: table, production: production.name) ).tree @@ -2697,6 +3359,7 @@ fn compute_grammar_first_analysis_given( nullable_set: List ) -> GrammarFirstAnalysis { let first_rows = compute_production_first_rows(root: root, nullable_set: nullable_set) + let productions = grammar_production_index(productions: root.productions) let prep = fold_list( xs: root.productions, empty: AnalysisPrepAcc { prepared_exprs: empty_map(), residue: std.algebra.Empty }, @@ -2705,6 +3368,7 @@ fn compute_grammar_first_analysis_given( expr: p.expression, nullable_set: nullable_set, first_rows: first_rows, + productions: productions, production: p.name, token_dispatch: true ) @@ -2719,7 +3383,7 @@ fn compute_grammar_first_analysis_given( first_rows: first_rows, prepared_exprs: prep.prepared_exprs, grammar_digest: parse_grammar_digest(validated: ValidatedGrammarRoot { root: root }), - productions_by_name: grammar_production_index(productions: root.productions), + productions_by_name: productions, choice_residue: prep.residue, memo_recurrence: parse_memo_recurrence_census(root: root, nullable_set: nullable_set) } @@ -4122,6 +4786,7 @@ fn parse_expr( expr: expr, nullable_set: table.nullable_set, first_rows: table.first_rows, + productions: empty_map(), production: root.start, token_dispatch: parse_table_token_dispatch(table: table, production: root.start) ).tree, diff --git a/src/v2/test/claim/parse/choice_lookahead_guard_test.dag b/src/v2/test/claim/parse/choice_lookahead_guard_test.dag new file mode 100644 index 00000000000..cb84abe938d --- /dev/null +++ b/src/v2/test/claim/parse/choice_lookahead_guard_test.dag @@ -0,0 +1,154 @@ +module v2.test.parse.choice_lookahead_guard_test + +import std.algebra { Cons, Empty } +import v2.std.grammar { + Choice, + GrammarExpr, + GrammarProduction, + GrammarRoot, + LiteralTerminal, + NotPredicate, + Optional, + Sequence, + StampClass, + Terminal, + grammar_atom, + grammar_empty_sync_tokens, + node_atom_identity_optional +} +import v2.compiler.parse { grammar_choice_ambiguity_count, parse_module_prepared } +import v2.compiler.program_assembly { dag_prepared_grammar } +import v2.compiler.tokenize { tokenize } +import v2.extdeps.languages.dag { dag_lex } +import v2.std.diagnostic { Accepted, Outcome, Rejected, bind_outcome } +import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly } +import v2.std.logic { Bool } +import v2.std.node { Node, Symbol } +import v2.std.optional { Absent, Optional, Present } + +data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly + +// THE CHOICE-OVERLAP PROOF REMOVES A ROW ONLY WHERE THE DECLARED LOOKAHEAD PROVES THE ALTERNATIVES +// DISJOINT (v2.compiler.parse lookahead_alternatives_overlap). Each grammar here is supplied, so a +// claim's cost is one analysis of a two-production root. The pairs are the ruling's controls: a guard +// that covers the shared prefix removes the row, the same guard missing that prefix keeps it, and +// the unguarded alternative keeps it -- so the removal is the guard's, not the lookahead's alone. +fn clg_tok(c: Symbol) -> GrammarExpr { Terminal { token_class: c, stamp: StampClass } } + +fn clg_word(w: Symbol) -> GrammarExpr { LiteralTerminal { token_class: ^clg_ident, lexeme: w } } + +fn clg_seq(left: GrammarExpr, right: GrammarExpr) -> GrammarExpr { Sequence { left: left, right: right } } + +fn clg_root(choice: GrammarExpr) -> GrammarRoot { + GrammarRoot { + start: ^clg_start, + productions: Cons { + head: GrammarProduction { name: ^clg_start, expression: choice, emitted: grammar_atom(identity: ^clg_start) }, + tail: Empty + }, + sync_tokens: grammar_empty_sync_tokens() + } +} + +// `a :` | X, where X = `a (: | b)`: both alternatives can begin `a :`. +fn clg_named() -> GrammarExpr { clg_seq(left: clg_tok(c: ^clg_a), right: clg_tok(c: ^clg_colon)) } + +fn clg_positional() -> GrammarExpr { + clg_seq(left: clg_tok(c: ^clg_a), right: Choice { left: clg_tok(c: ^clg_colon), right: clg_tok(c: ^clg_b) }) +} + +fn clg_rows(guard: GrammarExpr) -> Int { + grammar_choice_ambiguity_count( + root: clg_root(choice: Choice { left: clg_named(), right: clg_seq(left: NotPredicate { element: guard }, right: clg_positional()) }) + ) +} + +test fn covering_two_token_guard_removes_the_row() -> Bool { + clg_rows(guard: clg_named()) == 0 +} + +test fn near_miss_two_token_guard_keeps_the_row() -> Bool { + clg_rows(guard: clg_seq(left: clg_tok(c: ^clg_a), right: clg_tok(c: ^clg_b))) == 1 +} + +test fn unguarded_shared_two_token_prefix_keeps_the_row() -> Bool { + grammar_choice_ambiguity_count(root: clg_root(choice: Choice { left: clg_named(), right: clg_positional() })) == 1 +} + +// A guard whose strings would cover but whose form is not plain proves nothing: `a? :` admits `a :`, +// but an Optional is not a token-string set, so it subtracts nothing and the row stands. +test fn non_plain_guard_keeps_the_row() -> Bool { + clg_rows(guard: clg_seq(left: Optional { element: clg_tok(c: ^clg_a) }, right: clg_tok(c: ^clg_colon))) == 1 +} + +// The k=1 word shape (op_requires): 'none' | 'opaque' | !('none' | 'opaque') ident. +fn clg_words_guarded(guard: GrammarExpr) -> Int { + grammar_choice_ambiguity_count( + root: clg_root( + choice: Choice { + left: clg_word(w: ^clg_none), + right: Choice { + left: clg_word(w: ^clg_opaque), + right: clg_seq(left: NotPredicate { element: guard }, right: clg_tok(c: ^clg_ident)) + } + } + ) + ) +} + +test fn excluded_words_guard_removes_both_word_rows() -> Bool { + clg_words_guarded(guard: Choice { left: clg_word(w: ^clg_none), right: clg_word(w: ^clg_opaque) }) == 0 +} + +test fn guard_missing_one_word_keeps_that_row() -> Bool { + clg_words_guarded(guard: clg_word(w: ^clg_none)) == 1 +} + +// THE ROUTE ON REAL INPUT, for a row the k=2 proof removed with no guard: `stmt`'s `return` head +// against let_sugar's bare `name = e`, whose name admits the keyword. `=` begins no expression, so +// `return 1` and `return = 1` start alike only for one token. Each must take its own alternative: +// the return statement carries no let_expr, the bare assignment is one. +fn clg_parse(text: String, file: Symbol) -> Outcome { + match dag_prepared_grammar() { + Rejected { diagnostics: d } => Rejected { diagnostics: d } + Accepted { value: prepared, diagnostics: residue } => + bind_outcome( + o: tokenize(text: text, file: file, rules: dag_lex()), + f: fn(token_stream) { + match parse_module_prepared(tokens: token_stream, prepared: prepared, validation_residue: residue) { + Rejected { diagnostics: r } => Rejected { diagnostics: r } + Accepted { value: artifact, diagnostics: d } => Accepted { value: artifact.tree, diagnostics: d } + } + } + ) + } +} + +fn clg_tree_has_identity(root: Node, identity: Symbol) -> Bool { + let here = match node_atom_identity_optional(node: root) { + Present { value: id } => id == identity + Absent => false + } + here || fold(root.children, init: false, f: fn(found, e) { found || clg_tree_has_identity(root: e.target, identity: identity) }) +} + +fn clg_parsed_has_let(text: String, file: Symbol) -> Optional { + match clg_parse(text: text, file: file) { + Accepted { value: tree, diagnostics: _ } => Present { value: clg_tree_has_identity(root: tree, identity: ^dag_surface_let_expr) } + Rejected { diagnostics: _ } => Absent + } +} + +test fn return_statement_takes_the_return_route() -> Bool { + match clg_parsed_has_let(text: "module probe.clg_return\nfn f() -> Int { return 1 }\n", file: ^clg_return) { + Present { value: has_let } => !has_let + Absent => false + } +} + +test fn keyword_named_bare_assignment_takes_the_let_route() -> Bool { + match clg_parsed_has_let(text: "module probe.clg_assign\nfn f() -> Int {\n return = 1\n 1\n}\n", file: ^clg_assign) { + Present { value: has_let } => has_let + Absent => false + } +} diff --git a/src/v2/test/claim/parse/choice_plan_test.dag b/src/v2/test/claim/parse/choice_plan_test.dag index ed79645cd08..46668568e8d 100644 --- a/src/v2/test/claim/parse/choice_plan_test.dag +++ b/src/v2/test/claim/parse/choice_plan_test.dag @@ -167,6 +167,7 @@ fn pcp_choice_plan(expr: GrammarExpr) -> PreparedChoicePlan { expr: expr, nullable_set: Empty, first_rows: empty_map(), + productions: empty_map(), production: ^pcp_start, token_dispatch: true ).tree { @@ -349,6 +350,7 @@ test fn compile_choice_alts_stamp_split_is_choice_token_prefix() -> Bool { expr: stamp_split_left, nullable_set: Empty, first_rows: empty_map(), + productions: empty_map(), production: ^pcp_start, token_dispatch: true ) @@ -356,6 +358,7 @@ test fn compile_choice_alts_stamp_split_is_choice_token_prefix() -> Bool { expr: stamp_split_right, nullable_set: Empty, first_rows: empty_map(), + productions: empty_map(), production: ^pcp_start, token_dispatch: true ) From f45e4e58afd3bcc7a34594ed92ce5ec88f75df20 Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Sat, 3 Oct 2026 00:28:55 +0000 Subject: [PATCH 05/33] choice_plan_test: import LiveTreeDisposition and SubstrateInputsOnly; retire its debt row Touching the file put its bare references under the unimported-provider gate. Both names are now imported, so the SubstrateInputsOnly row moves ActiveDebt -> Retired { ImportsFixed }. Co-Authored-By: Claude Opus 5.5 (1M context) --- src/v2/test/claim/parse/choice_plan_test.dag | 1 + src/v2/workflow/floor_unimported_bare_provider_debt_roster.dag | 2 +- 2 files changed, 2 insertions(+), 1 deletion(-) diff --git a/src/v2/test/claim/parse/choice_plan_test.dag b/src/v2/test/claim/parse/choice_plan_test.dag index 46668568e8d..b00a72ef122 100644 --- a/src/v2/test/claim/parse/choice_plan_test.dag +++ b/src/v2/test/claim/parse/choice_plan_test.dag @@ -40,6 +40,7 @@ import v2.compiler.parse { parse_table_for_production, prepare_grammar_expr } +import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly } import v2.std.optional { Absent, Present } import v2.std.algebra { fold_list, length } import v2.std.diagnostic { Accepted, Diagnostic, NonEmptyDiagnostics, None, Rejected, Some, invariant_port_locus } diff --git a/src/v2/workflow/floor_unimported_bare_provider_debt_roster.dag b/src/v2/workflow/floor_unimported_bare_provider_debt_roster.dag index cfce9b90e91..ab8733918e9 100644 --- a/src/v2/workflow/floor_unimported_bare_provider_debt_roster.dag +++ b/src/v2/workflow/floor_unimported_bare_provider_debt_roster.dag @@ -2059,7 +2059,7 @@ data unimported_bare_provider_dispositions: List Date: Sat, 3 Oct 2026 00:56:09 +0000 Subject: [PATCH 06/33] v2 parse lookahead: a guard also refuses the other side's covered prefix; no wildcard arms The ruling's direction: a pair of prefixes is disjoint when one side's prefix is covered by the other side's proved-plain guard, whatever length the guarded side's own prefix has (name: e | !(name :) e, whose positional side can be one token). Guards ride the prefixes they head and survive extension. The three GrammarExpr matches are written out arm by arm (NonFoldResidueRosterDiverged). Two controls added for the short-side case. Co-Authored-By: Claude Opus 5.5 (1M context) --- src/v2/compiler/02_parse.dag | 136 ++++++++++++++---- .../parse/choice_lookahead_guard_test.dag | 25 ++++ 2 files changed, 133 insertions(+), 28 deletions(-) diff --git a/src/v2/compiler/02_parse.dag b/src/v2/compiler/02_parse.dag index b22176b5f6b..e267f3b807b 100644 --- a/src/v2/compiler/02_parse.dag +++ b/src/v2/compiler/02_parse.dag @@ -2340,7 +2340,10 @@ fn expr_first_fold_from_prepared( // and only when G is a PLAIN guard (lookahead_guard_strings): a finite set of token strings whose PEG // success is membership. Where one position of a prefix is a whole token class and G names one word // of it, the class is narrowed to the class less that word -- the k=1 shape -// `!('none' | 'opaque') type_list`. Every undecidable arm -- a cycle without consumption, a missing +// `!('none' | 'opaque') type_list`. The guard is also carried on the prefixes it heads, and a pair of +// prefixes is disjoint when one alternative's prefix is covered by the other's guard: the guarded +// alternative then fails on every input that prefix denotes, however short its own prefix is (the +// `name: e | !(name :) e` shape, whose positional side can be one token). Every undecidable arm -- a cycle without consumption, a missing // production, a guard that is not plain, a guard string longer than the prefix it would cover -- // answers by subtracting nothing or by LookaheadUnknown, and Unknown keeps the row. So the proof // removes rows and never widens: a guard that misses one prefix is the near miss that keeps its row. @@ -2360,9 +2363,12 @@ type LookaheadKey { } // `complete`: the alternative can END after `keys`, so a following sequence element extends it. +// `guards`: the strings of the proved-plain not-predicates standing at the prefix's first token. An +// input that begins with one of them is refused by this alternative, whatever follows. type LookaheadPrefix { keys: List complete: Bool + guards: List> } type LookaheadPrefixes @@ -2376,13 +2382,14 @@ type GuardCoverage fn lookahead_prefix_keys(p: LookaheadPrefix) -> List { p.keys } fn lookahead_prefix_complete(p: LookaheadPrefix) -> Bool { p.complete } +fn lookahead_prefix_guards(p: LookaheadPrefix) -> List> { p.guards } fn lookahead_production_expression(p: GrammarProduction) -> GrammarExpr { p.expression } fn lookahead_none() -> LookaheadPrefixes { LookaheadKnown { prefixes: std.algebra.Empty } } fn lookahead_empty_only() -> LookaheadPrefixes { LookaheadKnown { - prefixes: Cons { head: LookaheadPrefix { keys: std.algebra.Empty, complete: true }, tail: std.algebra.Empty } + prefixes: Cons { head: LookaheadPrefix { keys: std.algebra.Empty, complete: true, guards: std.algebra.Empty }, tail: std.algebra.Empty } } } @@ -2410,7 +2417,8 @@ fn lookahead_token(key: FirstKey, head_keys: Optional>) -> Lookah prefixes: Cons { head: LookaheadPrefix { keys: Cons { head: LookaheadKey { key: key, excluded: std.algebra.Empty }, tail: std.algebra.Empty }, - complete: true + complete: true, + guards: std.algebra.Empty }, tail: std.algebra.Empty } @@ -2430,7 +2438,8 @@ fn lookahead_from_first(first: List, nullable: Bool) -> LookaheadPrefi xs: acc, item: LookaheadPrefix { keys: Cons { head: LookaheadKey { key: k, excluded: std.algebra.Empty }, tail: std.algebra.Empty }, - complete: false + complete: false, + guards: std.algebra.Empty } ) } @@ -2526,6 +2535,22 @@ fn lookahead_nonterminal_expand( } } +fn lookahead_leading_guard(expr: GrammarExpr) -> Optional { + match expr { + NotPredicate { element: guard } => Present { value: guard } + Terminal { token_class: _, stamp: _ } => Absent + LiteralTerminal { token_class: _, lexeme: _ } => Absent + Nonterminal { production: _ } => Absent + Sequence { left: _, right: _ } => Absent + Choice { left: _, right: _ } => Absent + Optional { element: _ } => Absent + Repeat { element: _ } => Absent + Expect { element: _, reason: _ } => Absent + RefuseOnMatch { element: _, reason: _ } => Absent + AfterLineBreak { element: _ } => Absent + } +} + fn lookahead_sequence( left: GrammarExpr, right: GrammarExpr, @@ -2534,14 +2559,14 @@ fn lookahead_sequence( visiting: List, ctx: LookaheadContext ) -> LookaheadPrefixes { - match left { - NotPredicate { element: guard } => + match lookahead_leading_guard(expr: left) { + Present { value: guard } => lookahead_subtract_guard( prefixes: lookahead_prefixes(expr: right, depth: depth, head_keys: head_keys, visiting: visiting, ctx: ctx), guard: guard, ctx: ctx ) - _ => + Absent => lookahead_extend( prefixes: lookahead_prefixes(expr: left, depth: depth, head_keys: head_keys, visiting: visiting, ctx: ctx), right: right, @@ -2553,7 +2578,7 @@ fn lookahead_sequence( } } -fn lookahead_prepend(keys: List, prefixes: LookaheadPrefixes) -> LookaheadPrefixes { +fn lookahead_prepend(keys: List, guards: List>, prefixes: LookaheadPrefixes) -> LookaheadPrefixes { match prefixes { LookaheadUnknown => LookaheadUnknown LookaheadKnown { prefixes: ps } => @@ -2566,7 +2591,8 @@ fn lookahead_prepend(keys: List, prefixes: LookaheadPrefixes) -> L xs: acc, item: LookaheadPrefix { keys: list_append(left: keys, right: lookahead_prefix_keys(p: q)), - complete: lookahead_prefix_complete(p: q) + complete: lookahead_prefix_complete(p: q), + guards: guards } ) } @@ -2575,8 +2601,10 @@ fn lookahead_prepend(keys: List, prefixes: LookaheadPrefixes) -> L } } -fn lookahead_truncated(keys: List) -> LookaheadPrefixes { - LookaheadKnown { prefixes: Cons { head: LookaheadPrefix { keys: keys, complete: false }, tail: std.algebra.Empty } } +fn lookahead_truncated(prefix: LookaheadPrefix) -> LookaheadPrefixes { + LookaheadKnown { + prefixes: Cons { head: LookaheadPrefix { keys: prefix.keys, complete: false, guards: prefix.guards }, tail: std.algebra.Empty } + } } // Extend each prefix that ended early by the prefixes of what follows. The head restriction and the @@ -2596,11 +2624,12 @@ fn lookahead_extend_one( } else { lookahead_prepend( keys: prefix.keys, + guards: prefix.guards, prefixes: lookahead_prefixes(expr: right, depth: depth - used, head_keys: Absent, visiting: std.algebra.Empty, ctx: ctx) ) } } else { - lookahead_truncated(keys: prefix.keys) + lookahead_truncated(prefix: prefix) } } @@ -2658,10 +2687,11 @@ fn lookahead_repeat_one(prefix: LookaheadPrefix, element: GrammarExpr, depth: In if prefix.complete && used < depth { lookahead_prepend( keys: prefix.keys, + guards: prefix.guards, prefixes: lookahead_repeat(element: element, depth: depth - used, head_keys: Absent, visiting: std.algebra.Empty, ctx: ctx) ) } else { - lookahead_truncated(keys: prefix.keys) + lookahead_truncated(prefix: prefix) } } } @@ -2720,7 +2750,12 @@ fn lookahead_guard_strings(expr: GrammarExpr, visiting: List, ctx: Looka Absent => Absent } } - _ => Absent + Optional { element: _ } => Absent + Repeat { element: _ } => Absent + Expect { element: _, reason: _ } => Absent + RefuseOnMatch { element: _, reason: _ } => Absent + AfterLineBreak { element: _ } => Absent + NotPredicate { element: _ } => Absent } } @@ -2749,7 +2784,13 @@ fn lookahead_guard_token_set(expr: GrammarExpr, visiting: List, ctx: Loo Absent => Absent } } - _ => Absent + Sequence { left: _, right: _ } => Absent + Optional { element: _ } => Absent + Repeat { element: _ } => Absent + Expect { element: _, reason: _ } => Absent + RefuseOnMatch { element: _, reason: _ } => Absent + AfterLineBreak { element: _ } => Absent + NotPredicate { element: _ } => Absent } } @@ -2760,14 +2801,34 @@ fn lookahead_subtract_guard(prefixes: LookaheadPrefixes, guard: GrammarExpr, ctx match lookahead_guard_strings(expr: guard, visiting: std.algebra.Empty, ctx: ctx) { Absent => LookaheadKnown { prefixes: ps } Present { value: strings } => - LookaheadKnown { + lookahead_attach_guards( prefixes: fold_list( xs: strings, empty: ps, cons: fn(acc, g) { lookahead_subtract_string(prefixes: acc, guard: g) } - ) + ), + strings: strings + ) + } + } +} + +fn lookahead_attach_guards(prefixes: List, strings: List>) -> LookaheadPrefixes { + LookaheadKnown { + prefixes: fold_list( + xs: prefixes, + empty: std.algebra.Empty, + cons: fn(acc, p) { + list_snoc_item( + xs: acc, + item: LookaheadPrefix { + keys: lookahead_prefix_keys(p: p), + complete: lookahead_prefix_complete(p: p), + guards: list_append(left: lookahead_prefix_guards(p: p), right: strings) } + ) } + ) } } @@ -2779,7 +2840,10 @@ fn lookahead_subtract_string(prefixes: List, guard: List acc GuardCoversButOneWord { keys: narrowed } => - list_snoc_item(xs: acc, item: LookaheadPrefix { keys: narrowed, complete: lookahead_prefix_complete(p: p) }) + list_snoc_item( + xs: acc, + item: LookaheadPrefix { keys: narrowed, complete: lookahead_prefix_complete(p: p), guards: lookahead_prefix_guards(p: p) } + ) GuardMisses => list_snoc_item(xs: acc, item: p) } } @@ -2894,21 +2958,37 @@ fn lookahead_prefix_keys_overlap(left: List, right: List>) -> Bool { + any( + xs: guards, + predicate: fn(g) { + match lookahead_guard_coverage(keys: lookahead_prefix_keys(p: prefix), guard: g) { + GuardCoversAll => true + GuardCoversButOneWord { keys: _ } => false + GuardMisses => false + } + } + ) +} + +fn lookahead_prefix_pair_overlaps(left: LookaheadPrefix, right: LookaheadPrefix) -> Bool { + !is_empty(xs: lookahead_prefix_keys(p: left)) + && !is_empty(xs: lookahead_prefix_keys(p: right)) + && lookahead_prefix_keys_overlap(left: lookahead_prefix_keys(p: left), right: lookahead_prefix_keys(p: right)) + && !lookahead_prefix_refused_by(prefix: left, guards: lookahead_prefix_guards(p: right)) + && !lookahead_prefix_refused_by(prefix: right, guards: lookahead_prefix_guards(p: left)) +} + // The empty prefix (a nullable alternative) is the both-nullable row's question, not this one's, so // it is not compared here -- exactly as the single-token FIRST check never counted it. fn lookahead_prefix_sets_overlap(left: List, right: List) -> Bool { any( xs: left, - predicate: fn(l) { - !is_empty(xs: lookahead_prefix_keys(p: l)) - && any( - xs: right, - predicate: fn(r) { - !is_empty(xs: lookahead_prefix_keys(p: r)) - && lookahead_prefix_keys_overlap(left: lookahead_prefix_keys(p: l), right: lookahead_prefix_keys(p: r)) - } - ) - } + predicate: fn(l) { any(xs: right, predicate: fn(r) { lookahead_prefix_pair_overlaps(left: l, right: r) }) } ) } diff --git a/src/v2/test/claim/parse/choice_lookahead_guard_test.dag b/src/v2/test/claim/parse/choice_lookahead_guard_test.dag index cb84abe938d..82937f05dd4 100644 --- a/src/v2/test/claim/parse/choice_lookahead_guard_test.dag +++ b/src/v2/test/claim/parse/choice_lookahead_guard_test.dag @@ -81,6 +81,31 @@ test fn non_plain_guard_keeps_the_row() -> Bool { clg_rows(guard: clg_seq(left: Optional { element: clg_tok(c: ^clg_a) }, right: clg_tok(c: ^clg_colon))) == 1 } +// `a : x | !(a :) a b?`: the guarded side can be the one token `a`, shorter than the guard, so +// no subtraction from its own prefixes can clear the row. The guard covers the OTHER side's `a :`, +// and that is the proof; the near miss `!(a x)` covers nothing and keeps the row. +fn clg_short_rows(guard: GrammarExpr) -> Int { + grammar_choice_ambiguity_count( + root: clg_root( + choice: Choice { + left: clg_seq(left: clg_named(), right: clg_tok(c: ^clg_x)), + right: clg_seq( + left: NotPredicate { element: guard }, + right: clg_seq(left: clg_tok(c: ^clg_a), right: Optional { element: clg_tok(c: ^clg_b) }) + ) + } + ) + ) +} + +test fn guard_covering_the_other_side_clears_a_short_guarded_side() -> Bool { + clg_short_rows(guard: clg_named()) == 0 +} + +test fn guard_covering_neither_side_keeps_the_short_row() -> Bool { + clg_short_rows(guard: clg_seq(left: clg_tok(c: ^clg_a), right: clg_tok(c: ^clg_x))) == 1 +} + // The k=1 word shape (op_requires): 'none' | 'opaque' | !('none' | 'opaque') ident. fn clg_words_guarded(guard: GrammarExpr) -> Int { grammar_choice_ambiguity_count( From 8793156f5783dbe8af7e5f5a1e39e2098265995b Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Sat, 3 Oct 2026 01:02:28 +0000 Subject: [PATCH 07/33] dag grammar: guard arg, stmt and the lambda name head with proved-plain not-predicates arg: positional is !(name :) expr. stmt: the expression alternative is !(name = | 'node' name) expr. expr: binary_expr is !(name =>) binary. Each guard captures nothing, so trees are unchanged; the overlap proof clears dag_production_arg and stmt's ident-led row. Co-Authored-By: Claude Opus 5.5 (1M context) --- src/v2/extdeps/languages/dag.dag | 56 ++++++++++++++++++++++++++++++-- 1 file changed, 53 insertions(+), 3 deletions(-) diff --git a/src/v2/extdeps/languages/dag.dag b/src/v2/extdeps/languages/dag.dag index a6dcdab3a1e..659270a9840 100644 --- a/src/v2/extdeps/languages/dag.dag +++ b/src/v2/extdeps/languages/dag.dag @@ -1225,6 +1225,24 @@ fn dag_grammar_else_less_if_stmt_expr() -> GrammarExpr { ) } +// AN EXPRESSION STATEMENT NEVER BEGINS WITH A LET SPELLING. `name =` and `node name` head the two +// let_sugar forms (dag_grammar_let_sugar_expr) and begin no expression, so the expression +// alternative is guarded by exactly those heads: the two alternatives are disjoint by construction +// and the choice-overlap proof reads the guard. The guard captures nothing; the statement's tree is +// the expression's. +fn dag_grammar_let_sugar_head_expr() -> GrammarExpr { + dag_grammar_choice( + left: dag_grammar_sequence( + left: dag_grammar_binding_name_terminal(), + right: dag_grammar_terminal(token_class: ^dag_token_eq) + ), + right: dag_grammar_sequence( + left: dag_grammar_literal_terminal(token_class: ^dag_token_ident, lexeme: symbol_intern_lexeme(lexeme: "node")), + right: dag_grammar_binding_name_terminal() + ) + ) +} + fn dag_grammar_stmt_expr() -> GrammarExpr { dag_grammar_choice( left: dag_grammar_sequence( @@ -1234,7 +1252,10 @@ fn dag_grammar_stmt_expr() -> GrammarExpr { right: dag_grammar_choice( left: dag_grammar_nonterminal(production: ^dag_production_let_expr), right: dag_grammar_choice( - left: dag_grammar_nonterminal(production: ^dag_production_expr), + left: dag_grammar_sequence( + left: grammar_expr_not_predicate(element: dag_grammar_let_sugar_head_expr()), + right: dag_grammar_nonterminal(production: ^dag_production_expr) + ), right: dag_grammar_nonterminal(production: ^dag_production_else_less_if_stmt) ) ) @@ -1347,6 +1368,17 @@ fn dag_grammar_let_sugar_expr() -> GrammarExpr { // Evidence: `v2.test.parse.block_expr_as_binary_operand_parse` -- two arms red before this reorder // (a `match` and an `if` heading a binary chain), three controls green on both sides (each block // form standing alone, and an operand that was never block-shaped). +// A BINARY EXPRESSION NEVER BEGINS `name =>`: that head is the one-parameter arrow lambda's, and +// the guard says so where the two alternatives meet, so they are disjoint on a name by +// construction. The parenthesised lambda head is not separable at bounded lookahead from a grouped +// expression; it is restructured with dag_grammar_arrow_lambda_expr, not guarded here. +fn dag_grammar_arrow_lambda_name_head_expr() -> GrammarExpr { + dag_grammar_sequence( + left: dag_grammar_ident_or_type_decl_modifier_name(), + right: dag_grammar_terminal(token_class: ^dag_token_fat_arrow) + ) +} + fn dag_grammar_expr_expr() -> GrammarExpr { dag_grammar_choice( left: dag_grammar_nonterminal(production: ^dag_production_fn_literal), @@ -1354,7 +1386,10 @@ fn dag_grammar_expr_expr() -> GrammarExpr { left: dag_grammar_nonterminal(production: ^dag_production_block_expr), right: dag_grammar_choice( left: dag_grammar_nonterminal(production: ^dag_production_arrow_lambda), - right: dag_grammar_nonterminal(production: ^dag_production_binary_expr) + right: dag_grammar_sequence( + left: grammar_expr_not_predicate(element: dag_grammar_arrow_lambda_name_head_expr()), + right: dag_grammar_nonterminal(production: ^dag_production_binary_expr) + ) ) ) ) @@ -1725,6 +1760,18 @@ fn dag_grammar_block_expr_expr() -> GrammarExpr { dag_grammar_nonterminal(production: ^dag_production_fn_body) } +// A NAMED ARGUMENT AND A POSITIONAL ONE ARE DISJOINT BY CONSTRUCTION. Both can begin with a name; +// only the named one continues `name :`. The positional alternative is guarded by the not-predicate +// over exactly that head, so it refuses every input the named one denotes, and the choice-overlap +// proof (v2.compiler.parse lookahead_alternatives_overlap) reads the guard and clears the row. The +// guard captures nothing, so the positional argument's tree is the expression's, as before. +fn dag_grammar_arg_named_head_expr() -> GrammarExpr { + dag_grammar_sequence( + left: dag_grammar_binding_name_terminal(), + right: dag_grammar_terminal(token_class: ^dag_token_colon) + ) +} + fn dag_grammar_arg_expr() -> GrammarExpr { dag_grammar_choice( left: dag_grammar_sequence( @@ -1734,7 +1781,10 @@ fn dag_grammar_arg_expr() -> GrammarExpr { right: dag_grammar_nonterminal(production: ^dag_production_expr) ) ), - right: dag_grammar_nonterminal(production: ^dag_production_expr) + right: dag_grammar_sequence( + left: grammar_expr_not_predicate(element: dag_grammar_arg_named_head_expr()), + right: dag_grammar_nonterminal(production: ^dag_production_expr) + ) ) } From 4ae94b44bbed19f1cdbdede2ed7f1a22d0cac34b Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Sat, 3 Oct 2026 01:12:17 +0000 Subject: [PATCH 08/33] dag grammar: a match arm body is one production, the statement sequence The expression body was a second alternative sharing every expression-led input with the statement body. It is the one-statement case; body_lower_match_arm_body_lowered already lowers a statement body through body_lower_stmt_spine, whose last statement is the value. Co-Authored-By: Claude Opus 5.5 (1M context) --- src/v2/extdeps/languages/dag.dag | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) diff --git a/src/v2/extdeps/languages/dag.dag b/src/v2/extdeps/languages/dag.dag index 659270a9840..03d5e79498d 100644 --- a/src/v2/extdeps/languages/dag.dag +++ b/src/v2/extdeps/languages/dag.dag @@ -1862,15 +1862,17 @@ fn dag_grammar_match_arm_stmt_body_expr() -> GrammarExpr { ) } +// AN ARM BODY IS ONE PRODUCTION: a statement sequence of one or more statements. An expression +// body is the one-statement case, so it is not a second alternative: offered beside the statement +// body, the two shared every expression-led input and the choice picked the expression. The arm +// body lowers through body_lower_stmt_spine (v2.compiler.body_lowering_fold +// body_lower_match_arm_body_lowered), whose last statement is the value, exactly as a fn body's. fn dag_grammar_match_arm_expr() -> GrammarExpr { dag_grammar_sequence( left: dag_grammar_nonterminal(production: ^dag_production_pattern), right: dag_grammar_sequence( left: dag_grammar_terminal(token_class: ^dag_token_fat_arrow), - right: dag_grammar_choice( - left: dag_grammar_nonterminal(production: ^dag_production_expr), - right: dag_grammar_nonterminal(production: ^dag_production_match_arm_stmt_body) - ) + right: dag_grammar_nonterminal(production: ^dag_production_match_arm_stmt_body) ) ) } From 1f4fdd95caf26bfa97ba1a90973ee9c00a53f657 Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Sat, 3 Oct 2026 01:15:54 +0000 Subject: [PATCH 09/33] dag grammar: one if, head read once, block form's else optional (operator ruling 2026-10-03, this case only) if_expr := if expr ( then expr else expr | block (else (if|block))? ). The else_less_if_stmt production is deleted; stmt no longer offers it. With-else trees are unchanged (a present optional and a choice pass through). Lowering reads an else-less if through one positional reader, body_lower_else_less_if_parts_optional: at statement position a block ending in return is the admitted guard; the exit walk and the if value reader refuse every other else-less if as else_less_if_unlowered, at it. Controls (v2.test.parse.else_less_if_value_category): the guard is accepted; the value position refuses at the if; both parse to the one else-less if_expr route. Co-Authored-By: Claude Opus 5.5 (1M context) --- src/v2/compiler/body_lowering_fold.dag | 120 +++++++++++++----- src/v2/extdeps/languages/dag.dag | 97 ++++++-------- .../parse/closure_parse_batch_two_test.dag | 2 +- .../else_less_if_value_category_test.dag | 98 ++++++++++++++ 4 files changed, 228 insertions(+), 89 deletions(-) create mode 100644 src/v2/test/claim/parse/else_less_if_value_category_test.dag diff --git a/src/v2/compiler/body_lowering_fold.dag b/src/v2/compiler/body_lowering_fold.dag index 1c84bf6758b..208a0f120b9 100644 --- a/src/v2/compiler/body_lowering_fold.dag +++ b/src/v2/compiler/body_lowering_fold.dag @@ -8264,6 +8264,13 @@ fn body_lower_try_if_from_captured(captured: Node) -> Outcome> { } fn body_lower_if_expr(shell: Node) -> Outcome { + match body_lower_else_less_if_parts_optional(if_shell: shell) { + Present { value: _ } => body_lower_else_less_if_reject(shell: shell) + Absent => body_lower_if_expr_valued(shell: shell) + } +} + +fn body_lower_if_expr_valued(shell: Node) -> Outcome { match body_lower_unwrap_captured(shell: shell) { Absent => outcome_rejected( @@ -10690,40 +10697,88 @@ fn body_lower_return_statement_expr_optional(stmt: Node) -> Optional { } } -// A GUARD'S PARTS, read positionally: dag_grammar_else_less_if_stmt_expr is -// seq(`if`, seq(expr, fn_body)). It is admitted only when its arm's last statement is a return, so -// the guard exits exactly when it is taken; an arm that falls through (`if c { log() }`) is not a -// guard and keeps refusing else_less_if_unlowered. +// AN ELSE-LESS `if`'S PARTS, read positionally: dag_grammar_if_expr_expr's block form without its +// optional else captures seq(`if`, seq(condition, seq(fn_body, ))). The expression form and a +// block form with an else do not have that shape, so this reader answers exactly the `if` that has +// no value (operator ruling 2026-10-03). At statement position it is a guard when its arm's last +// statement is a return (body_lower_admitted_guard_optional), so the guard exits exactly when it is +// taken; an arm that falls through (`if c { log() }`) is not a guard and refuses else_less_if_unlowered, +// as does every else-less `if` where a value is owed. type BodyLowerGuard { shell: Node condition: Node arm: Node } -fn body_lower_guard_optional(stmt: Node) -> Optional { - let inner = match parse_production_captured_child_optional(node: stmt) { - Present { value: c } => c - Absent => stmt +fn body_lower_else_less_if_parts_optional(if_shell: Node) -> Optional { + match body_lower_unwrap_captured(shell: if_shell) { + Absent => optional_absent() + Present { value: captured } => + match sugar_sequence_pair_optional(node: body_lower_unwrap_surface_shell(node: captured)) { + Absent => optional_absent() + Present { value: if_rest } => + match sugar_sequence_pair_optional(node: body_lower_unwrap_surface_shell(node: if_rest.right)) { + Absent => optional_absent() + Present { value: cond_tail } => + match sugar_sequence_pair_optional(node: body_lower_unwrap_surface_shell(node: cond_tail.right)) { + Absent => optional_absent() + Present { value: arm_else } => + if body_lower_is_fn_body_shell(node: arm_else.left) + && is_empty_conj_root(n: body_lower_deep_unwrap_optional(node: arm_else.right)) { + optional_present(value: BodyLowerGuard { shell: if_shell, condition: cond_tail.left, arm: arm_else.left }) + } else { + optional_absent() + } + } + } + } + } +} + +fn body_lower_is_fn_body_shell(node: Node) -> Bool { + match parse_production_emitted_identity_optional(node: node) { + Present { value: id } => id == ^dag_surface_fn_body + Absent => false } - match parse_production_emitted_identity_optional(node: inner) { +} + +// The `if` a statement IS, when the whole statement is one `if`: the statement's production shells +// and the operator spines whose tail is empty are passed through, as body_lower_exit_walk passes +// them; anything else -- an `if` that is an operand, a call, a literal -- is not one. +fn body_lower_statement_sole_if_optional(node: Node) -> Optional { + match parse_production_emitted_identity_optional(node: node) { Present { value: id } => - if id == ^dag_surface_else_less_if_stmt { - match body_lower_unwrap_captured(shell: inner) { + if id == ^dag_surface_if_expr { + optional_present(value: node) + } else if body_lower_is_pass_through_emitted(emitted: id) || (id == ^dag_surface_primary_expr) { + match parse_production_captured_child_optional(node: node) { + Present { value: captured } => body_lower_statement_sole_if_optional(node: captured) Absent => optional_absent() - Present { value: captured } => - match sugar_sequence_pair_optional(node: body_lower_unwrap_surface_shell(node: captured)) { - Absent => optional_absent() - Present { value: if_rest } => - match sugar_sequence_pair_optional(node: body_lower_unwrap_surface_shell(node: if_rest.right)) { - Absent => optional_absent() - Present { value: cond_arm } => - optional_present(value: BodyLowerGuard { shell: inner, condition: cond_arm.left, arm: cond_arm.right }) - } - } } } else { optional_absent() } + Absent => + let peeled = body_lower_deep_unwrap_optional(node: node) + if peeled != node { + body_lower_statement_sole_if_optional(node: peeled) + } else { + match sugar_sequence_pair_optional(node: node) { + Present { value: pair } => + if is_empty_conj_root(n: body_lower_deep_unwrap_optional(node: pair.right)) { + body_lower_statement_sole_if_optional(node: pair.left) + } else { + optional_absent() + } + Absent => optional_absent() + } + } + } +} + +fn body_lower_guard_optional(stmt: Node) -> Optional { + match body_lower_statement_sole_if_optional(node: stmt) { + Present { value: if_shell } => body_lower_else_less_if_parts_optional(if_shell: if_shell) Absent => optional_absent() } } @@ -10824,8 +10879,6 @@ fn body_lower_exit_walk(node: Node, tail: Bool, arm_tail: Bool) -> Optional body_lower_exit_walk_children(node: node, tail: tail, arm_tail: false) } - } else if id == ^dag_surface_else_less_if_stmt { - body_lower_exit_refused(reason: ^body_lowering_reason_else_less_if_unlowered, at: node) } else if id == ^dag_surface_stmt_seq { match body_lower_unwrap_captured(shell: node) { Present { value: spine } => body_lower_exit_walk_spine(spine: spine, tail: tail) @@ -10884,6 +10937,13 @@ fn body_lower_match_arm_stripped(arm: Node) -> Node { // An `if`: its condition is not a tail; each arm is the if's own tail. The three reads cover the // whole if -- the rest of it is keywords -- and an if they cannot read is walked with no tail. fn body_lower_exit_walk_if(shell: Node, tail: Bool) -> Optional> { + match body_lower_else_less_if_parts_optional(if_shell: shell) { + Present { value: _ } => body_lower_exit_refused(reason: ^body_lowering_reason_else_less_if_unlowered, at: shell) + Absent => body_lower_exit_walk_if_valued(shell: shell, tail: tail) + } +} + +fn body_lower_exit_walk_if_valued(shell: Node, tail: Bool) -> Optional> { match body_lower_unwrap_captured(shell: shell) { Absent => body_lower_exit_walk_children(node: shell, tail: false, arm_tail: false) Present { value: captured } => @@ -10969,15 +11029,11 @@ fn body_lower_after_children(folded: Node, fn_body_pass_through: Bool) -> Outcom match parse_production_emitted_identity_optional(node: folded) { Absent => body_lowering_lowered(o: outcome_accepted(value: folded)) Present { value: emitted } => - if emitted == ^dag_surface_else_less_if_stmt { - body_lowering_lowered(o: body_lower_else_less_if_reject(shell: folded)) - } else { - body_lower_production_emitted( - shell: folded, - emitted: emitted, - fn_body_pass_through: fn_body_pass_through - ) - } + body_lower_production_emitted( + shell: folded, + emitted: emitted, + fn_body_pass_through: fn_body_pass_through + ) } } } diff --git a/src/v2/extdeps/languages/dag.dag b/src/v2/extdeps/languages/dag.dag index 03d5e79498d..3d285691aa2 100644 --- a/src/v2/extdeps/languages/dag.dag +++ b/src/v2/extdeps/languages/dag.dag @@ -1208,23 +1208,6 @@ fn dag_grammar_stmt_seq_expr() -> GrammarExpr { dag_grammar_repeat(element: dag_grammar_nonterminal(production: ^dag_production_stmt)) } -// An `if` with no `else` is a STATEMENT, never a value: `if count(parts) != 2 { return Malformed {..} }` -// (extdeps.uri_path), the guard form v1.compiler.parse admits. Its meaning is an early exit -- the -// branch leaves the function, otherwise execution falls through to the rest of the block -- which -// the v2 core has no lowering for, so body_lower_after_children refuses this production with the -// typed, located, counted body_lowering_reason_else_less_if_unlowered rather than dropping or -// rewriting it. It is tried AFTER expr, so an `if` that has an `else` is the ordinary if-expression -// and never reaches this row. -fn dag_grammar_else_less_if_stmt_expr() -> GrammarExpr { - dag_grammar_sequence( - left: dag_grammar_terminal(token_class: ^dag_token_kw_if), - right: dag_grammar_sequence( - left: dag_grammar_nonterminal(production: ^dag_production_expr), - right: dag_grammar_nonterminal(production: ^dag_production_fn_body) - ) - ) -} - // AN EXPRESSION STATEMENT NEVER BEGINS WITH A LET SPELLING. `name =` and `node name` head the two // let_sugar forms (dag_grammar_let_sugar_expr) and begin no expression, so the expression // alternative is guarded by exactly those heads: the two alternatives are disjoint by construction @@ -1251,12 +1234,9 @@ fn dag_grammar_stmt_expr() -> GrammarExpr { ), right: dag_grammar_choice( left: dag_grammar_nonterminal(production: ^dag_production_let_expr), - right: dag_grammar_choice( - left: dag_grammar_sequence( - left: grammar_expr_not_predicate(element: dag_grammar_let_sugar_head_expr()), - right: dag_grammar_nonterminal(production: ^dag_production_expr) - ), - right: dag_grammar_nonterminal(production: ^dag_production_else_less_if_stmt) + right: dag_grammar_sequence( + left: grammar_expr_not_predicate(element: dag_grammar_let_sugar_head_expr()), + right: dag_grammar_nonterminal(production: ^dag_production_expr) ) ) ) @@ -1937,39 +1917,44 @@ fn dag_grammar_field_pattern_expr() -> GrammarExpr { ) } -fn dag_grammar_if_block_expr() -> GrammarExpr { +// ONE `if`, ITS HEAD READ ONCE. `if cond` is shared by the two forms, so it is the production's +// prefix and the forms are the choice after it: `then` begins the expression form, a block the +// block form, so the next token decides (they were two alternatives repeating the head, an overlap +// no bounded lookahead decides). +// +// THE BLOCK FORM'S `else` IS OPTIONAL, and an `if` without one has no value. That is a fact about +// the value category, not an ambiguity deferred past the parser: the parse is unique either way +// (operator ruling 2026-10-03, for this case only). At statement position, where no value is owed, +// an else-less `if` whose block ends in a return is the early-return guard +// (v2.compiler.body_lowering_fold body_lower_admitted_guard_optional); wherever a value is required +// it refuses at lowering, typed and located, as body_lowering_reason_else_less_if_unlowered. A tree +// with an else is the one the two-form grammar built: a present optional and a choice each pass +// their element through. +fn dag_grammar_if_else_tail_expr() -> GrammarExpr { dag_grammar_sequence( - left: dag_grammar_terminal(token_class: ^dag_token_kw_if), - right: dag_grammar_sequence( - left: dag_grammar_nonterminal(production: ^dag_production_expr), - right: dag_grammar_sequence( - left: dag_grammar_nonterminal(production: ^dag_production_fn_body), - right: dag_grammar_sequence( - left: dag_grammar_terminal(token_class: ^dag_token_kw_else), - right: dag_grammar_choice( - left: dag_grammar_nonterminal(production: ^dag_production_if_expr), - right: dag_grammar_nonterminal(production: ^dag_production_fn_body) - ) - ) - ) + left: dag_grammar_terminal(token_class: ^dag_token_kw_else), + right: dag_grammar_choice( + left: dag_grammar_nonterminal(production: ^dag_production_if_expr), + right: dag_grammar_nonterminal(production: ^dag_production_fn_body) ) ) } -fn dag_grammar_if_then_expr() -> GrammarExpr { +fn dag_grammar_if_block_form_expr() -> GrammarExpr { dag_grammar_sequence( - left: dag_grammar_terminal(token_class: ^dag_token_kw_if), + left: dag_grammar_nonterminal(production: ^dag_production_fn_body), + right: dag_grammar_optional(element: dag_grammar_if_else_tail_expr()) + ) +} + +fn dag_grammar_if_then_form_expr() -> GrammarExpr { + dag_grammar_sequence( + left: dag_grammar_terminal(token_class: ^dag_token_kw_then), right: dag_grammar_sequence( left: dag_grammar_nonterminal(production: ^dag_production_expr), right: dag_grammar_sequence( - left: dag_grammar_terminal(token_class: ^dag_token_kw_then), - right: dag_grammar_sequence( - left: dag_grammar_nonterminal(production: ^dag_production_expr), - right: dag_grammar_sequence( - left: dag_grammar_terminal(token_class: ^dag_token_kw_else), - right: dag_grammar_nonterminal(production: ^dag_production_expr) - ) - ) + left: dag_grammar_terminal(token_class: ^dag_token_kw_else), + right: dag_grammar_nonterminal(production: ^dag_production_expr) ) ) ) @@ -1983,9 +1968,15 @@ fn dag_grammar_loop_expr_expr() -> GrammarExpr { } fn dag_grammar_if_expr_expr() -> GrammarExpr { - dag_grammar_choice( - left: dag_grammar_if_then_expr(), - right: dag_grammar_if_block_expr() + dag_grammar_sequence( + left: dag_grammar_terminal(token_class: ^dag_token_kw_if), + right: dag_grammar_sequence( + left: dag_grammar_nonterminal(production: ^dag_production_expr), + right: dag_grammar_choice( + left: dag_grammar_if_then_form_expr(), + right: dag_grammar_if_block_form_expr() + ) + ) ) } @@ -3296,11 +3287,6 @@ fn dag_grammar_root() -> GrammarRoot { expression: dag_grammar_field_decl_block_expr(), emitted: ^dag_surface_field_decl_block ) - let else_less_if_stmt = dag_grammar_production( - name: ^dag_production_else_less_if_stmt, - expression: dag_grammar_else_less_if_stmt_expr(), - emitted: ^dag_surface_else_less_if_stmt - ) let default_value = dag_grammar_production( name: ^dag_production_default_value, expression: dag_grammar_default_value_expr(), @@ -3495,7 +3481,6 @@ fn dag_grammar_root() -> GrammarRoot { uses_clause, uses_entry, admit_callers_clause, - else_less_if_stmt, fn_body, stmt_seq, stmt, diff --git a/src/v2/test/claim/parse/closure_parse_batch_two_test.dag b/src/v2/test/claim/parse/closure_parse_batch_two_test.dag index 40d891a8db0..afb22ba1cec 100644 --- a/src/v2/test/claim/parse/closure_parse_batch_two_test.dag +++ b/src/v2/test/claim/parse/closure_parse_batch_two_test.dag @@ -86,7 +86,7 @@ test fn empty_admit_callers_refuses_as_in_v1_holds() -> Bool { } } -// A -- dag_grammar_else_less_if_stmt_expr (extdeps.uri_path guards): an early-return guard +// A -- an else-less if_expr at statement position (dag_grammar_if_expr_expr; extdeps.uri_path guards): an early-return guard // followed by a statement parses and lowers, to Branch(c, arm, rest of the spine) // (v2.compiler.body_lowering_fold body_lower_guard_branch). It refused // body_lowering_reason_else_less_if_unlowered until the guard had a lowered form; a guard that falls diff --git a/src/v2/test/claim/parse/else_less_if_value_category_test.dag b/src/v2/test/claim/parse/else_less_if_value_category_test.dag new file mode 100644 index 00000000000..8ceea6ac358 --- /dev/null +++ b/src/v2/test/claim/parse/else_less_if_value_category_test.dag @@ -0,0 +1,98 @@ +module v2.test.parse.else_less_if_value_category + +import v2.compiler.body_lowering_fold { body_lower_else_less_if_parts_optional } +import v2.compiler.normalized_tree { NormalizedTree } +import v2.compiler.parse { parse_module_prepared } +import v2.compiler.program_assembly { dag_prepared_grammar } +import v2.compiler.tokenize { tokenize } +import v2.extdeps.languages.dag { dag_lex, parse_production_emitted_identity_optional } +import v2.std.diagnostic { Accepted, DeclarationLocus, InvariantPortLocus, Locus, NodeLocus, Outcome, Rejected, SourcePortLocus, Textual, bind_outcome, diagnostics_fatal } +import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly } +import v2.std.logic { Bool } +import v2.std.node { Node, Symbol } +import v2.std.optional { Absent, Present } +import v2.test.parse.supplied_token_stream_support { supplied_parsed_normalize } + +data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly + +// AN ELSE-LESS `if` PARSES ONE WAY AND HAS NO VALUE (operator ruling 2026-10-03, for this case +// only; v2.extdeps.languages.dag dag_grammar_if_expr_expr). The three controls the ruling names: +// the statement-position guard is accepted; the same `if` where a value is owed refuses as +// body_lowering_reason_else_less_if_unlowered, located at that `if`; and both inputs parse to the +// one if_expr route with its else slot empty -- the route, not only the verdict. +data elif_guard_source: String = "module probe.elif_guard\nfn f(x: Int) -> Int {\n if x == 0 { return 1 }\n x\n}\n" +data elif_value_source: String = "module probe.elif_value\nfn f(x: Int) -> Int {\n let y = if x == 0 { 1 }\n y\n}\n" + +fn elif_parse(text: String, file: Symbol) -> Outcome { + match dag_prepared_grammar() { + Rejected { diagnostics: d } => Rejected { diagnostics: d } + Accepted { value: prepared, diagnostics: residue } => + bind_outcome( + o: tokenize(text: text, file: file, rules: dag_lex()), + f: fn(token_stream) { + match parse_module_prepared(tokens: token_stream, prepared: prepared, validation_residue: residue) { + Rejected { diagnostics: r } => Rejected { diagnostics: r } + Accepted { value: artifact, diagnostics: d } => Accepted { value: artifact.tree, diagnostics: d } + } + } + ) + } +} + +fn elif_is_else_less_if(node: Node) -> Bool { + match parse_production_emitted_identity_optional(node: node) { + Present { value: id } => + if id == ^dag_surface_if_expr { + match body_lower_else_less_if_parts_optional(if_shell: node) { + Present { value: _ } => true + Absent => false + } + } else { + false + } + Absent => false + } +} + +fn elif_count_else_less_ifs(root: Node) -> Int { + let here = if elif_is_else_less_if(node: root) { 1 } else { 0 } + fold(root.children, init: here, f: fn(acc, e) { acc + elif_count_else_less_ifs(root: e.target) }) +} + +fn elif_parses_to_one_else_less_if(text: String, file: Symbol) -> Bool { + match elif_parse(text: text, file: file) { + Accepted { value: tree, diagnostics: _ } => elif_count_else_less_ifs(root: tree) == 1 + Rejected { diagnostics: _ } => false + } +} + +test fn statement_guard_and_value_if_each_parse_to_one_else_less_if_route() -> Bool { + elif_parses_to_one_else_less_if(text: elif_guard_source, file: ^elif_guard) + && elif_parses_to_one_else_less_if(text: elif_value_source, file: ^elif_value) +} + +test fn statement_position_guard_is_accepted() -> Bool { + match supplied_parsed_normalize(parsed: elif_parse(text: elif_guard_source, file: ^elif_guard)) { + Accepted { value: _, diagnostics: _ } => true + Rejected { diagnostics: _ } => false + } +} + +fn elif_locus_is_the_if(at: Locus) -> Bool { + match at { + NodeLocus { anchor: anchor } => elif_is_else_less_if(node: anchor.at) + SourcePortLocus { anchor: _, file: _, extent: _ } => false + Textual { file: _, extent: _ } => false + InvariantPortLocus { anchor: _, invariant: _ } => false + DeclarationLocus { declaration: _ } => false + } +} + +test fn value_position_else_less_if_refuses_at_the_if() -> Bool { + match supplied_parsed_normalize(parsed: elif_parse(text: elif_value_source, file: ^elif_value)) { + Accepted { value: _, diagnostics: _ } => false + Rejected { diagnostics: d } => + let fatal = diagnostics_fatal(d: d) + fatal.reason == ^body_lowering_reason_else_less_if_unlowered && elif_locus_is_the_if(at: fatal.at) + } +} From 915f2f6cb6acebd09166ff27c3f6568b70a7e505 Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Sat, 3 Oct 2026 01:20:01 +0000 Subject: [PATCH 10/33] dag grammar: statement let only; let x = e in body refuses at the in (LetInExpressionDropped) Per the 2026-10-02 zero-ambiguity decisions (statement let only, let-in dropped). The in-form alternative shared 'let name = value' with the statement form. A statement let's value followed by 'in' now refuses by name at the 'in' (a not-predicate over refuse_on_match, so a statement let's tree is unchanged). The six in-form lowering readers are deleted; no non-test source used the form. Test sources that used it are moved to the statement form or dropped where the statement form was already covered; let_in_form_refuses_at_the_in_holds is the refusal control. Co-Authored-By: Claude Opus 5.5 (1M context) --- src/v2/compiler/body_lowering_fold.dag | 211 ++---------------- src/v2/extdeps/languages/dag.dag | 35 ++- src/v2/std/parse_refusal_reason.dag | 7 + src/v2/test/claim/body_cast_node_test.dag | 18 -- .../caret_symbol_value_lowering_test.dag | 9 - .../body_lowering/statement_let_bind_test.dag | 49 ++-- ...wline_dual_role_operator_mutation_test.dag | 1 + src/v2/workflow/floor_pure_producer_share.dag | 4 - 8 files changed, 76 insertions(+), 258 deletions(-) diff --git a/src/v2/compiler/body_lowering_fold.dag b/src/v2/compiler/body_lowering_fold.dag index 208a0f120b9..8c98be2d244 100644 --- a/src/v2/compiler/body_lowering_fold.dag +++ b/src/v2/compiler/body_lowering_fold.dag @@ -3203,16 +3203,6 @@ fn body_lower_try_body_lowered(node: Node) -> Outcome> { Present { value: lowered } => outcome_with_diagnostics(value: optional_present(value: lowered), diagnostics: fd) Absent => - match body_lower_try_let_in_from_node(node: node) { - Rejected { diagnostics: r } => Rejected { diagnostics: r } - Accepted { value: let_found, diagnostics: ld } => - match let_found { - Present { value: lowered } => - outcome_with_diagnostics( - value: optional_present(value: lowered), - diagnostics: ld - ) - Absent => match body_lower_try_loop_expr_from_node(node: node) { Rejected { diagnostics: r } => Rejected { diagnostics: r } Accepted { value: loop_found, diagnostics: lcd } => @@ -3256,8 +3246,6 @@ fn body_lower_try_body_lowered(node: Node) -> Outcome> { } } } - } - } } } } @@ -3679,7 +3667,7 @@ fn body_lower_body_subtree_lower_control_forms(captured: Node) -> Outcome