From 0e82e788891b9c2361fae4fed57e89ebaf379197 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Thu, 11 Jun 2026 00:57:03 +0000 Subject: [PATCH 1/2] =?UTF-8?q?WIP:=20M-F=20stage-adoption=20Level-1c=20?= =?UTF-8?q?=E2=80=94=20de-anemize=20the=20next=20pipeline-stage=20hand-ma?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- src/v4/compiler/02_parse.dag | 65 ++++++++------ .../test/claim/parse/parse_table_claims.dag | 84 ++++++++++++++++++- 2 files changed, 122 insertions(+), 27 deletions(-) diff --git a/src/v4/compiler/02_parse.dag b/src/v4/compiler/02_parse.dag index f1a99cc3330..4ddee31b8e5 100644 --- a/src/v4/compiler/02_parse.dag +++ b/src/v4/compiler/02_parse.dag @@ -24,11 +24,9 @@ import v4.std.diagnostic { Some, Unavailable, UserInputBoundary, - diagnostics_merge, diagnostics_singleton, outcome_accepted, - port_locus, - rejected_with_pending + port_locus } import v4.std.node { Atom, @@ -42,7 +40,7 @@ import v4.std.node { Unanchored, well_formed } -import v4.std.provenance { make_node_span_anchored, merge_node_spans } +import v4.std.provenance { fold_node_tree_span, make_node_span_anchored } import v4.std.collection { List, Map, Set, empty_map, map_insert } import v4.std.algebra { Cons, Empty, TailAbsent, TailFound, contains, fold_list, fold_list_right, is_empty, length, list_append, list_snoc_item, list_tail } import v4.std.logic { Bool } @@ -296,32 +294,47 @@ fn parse_node_span_from_token(tok: Token) -> Outcome { make_node_span_anchored(file: tok.file, start: tok.start, end: tok.end) } -fn parse_merge_captured_spans(left: Node, right: Node) -> Outcome { - merge_node_spans(left: left.span, right: right.span) -} - fn parse_non_empty_diagnostics_to_list(ned: NonEmptyDiagnostics) -> List { list_append(left: [ned.head], right: ned.tail) } -fn parse_fold_node_span_step(acc: Outcome, n: Node) -> Outcome { - match acc { - Rejected { diagnostics: r } => Rejected { diagnostics: r } - Accepted { value: current, diagnostics: pending } => - match merge_node_spans(left: current, right: n.span) { - Rejected { diagnostics: r } => - Rejected { diagnostics: rejected_with_pending(pending: pending, rejected: r) } - Accepted { value: merged, diagnostics: d } => - Accepted { - value: merged, - diagnostics: diagnostics_merge(outer: pending, inner: d) - } - } - } +// 🟢 substrate catamorphism consumer — feature: T-8 captured-node tree span merge — +// bind node://adhoc-2145db6b-69a — first consumer of v4.std.provenance.fold_node_tree_span: +// Conj-wrapped capture children merge via the substrate NodeFold rather than hand-written +// flat span folds (parse_merge_captured_spans / parse_fold_node_spans). +fn parse_conj_captured_tree_span(children: List) -> Outcome { + fold_node_tree_span( + n: Node { + kind: TypeNode { connective: Conj }, + children: children, + span: Unanchored + } + ) } -fn parse_fold_node_spans(nodes: List, acc: NodeSpan) -> Outcome { - fold_list(xs: nodes, empty: outcome_accepted(value: acc), cons: parse_fold_node_span_step) +fn parse_sequence_captured_span(cap1: Node, cap2: Node) -> Outcome { + parse_conj_captured_tree_span(children: [ + grammar_named_edge(name: ^grammar_sequence_left_node_projection, target: cap1), + grammar_named_edge(name: ^grammar_sequence_right_node_projection, target: cap2) + ]) +} + +fn parse_repeat_captured_span(acc_nodes: List) -> Outcome { + parse_conj_captured_tree_span( + children: fold_list( + xs: acc_nodes, + empty: Empty, + cons: fn(acc, n) { + list_snoc_item( + xs: acc, + item: Edge { + label: Named { name: ^grammar_repeat_element_node_projection }, + target: n + } + ) + } + ) + ) } fn parse_wrap_production_captured(production: GrammarProduction, captured: Node) -> Node { @@ -827,7 +840,7 @@ fn parse_expr_run_walk( ParseExprRejected { diagnostics: diags2 } => ParseExprRejected { diagnostics: list_append(left: diags1, right: diags2) } ParseExprAccepted { remaining: rest2, captured: cap2, diagnostics: diags2 } => - match parse_merge_captured_spans(left: cap1, right: cap2) { + match parse_sequence_captured_span(cap1: cap1, cap2: cap2) { Rejected { diagnostics: r } => ParseExprRejected { diagnostics: list_append( @@ -931,7 +944,7 @@ fn parse_expr_run_walk( } } ) - match parse_fold_node_spans(nodes: result.acc_nodes, acc: Unanchored) { + match parse_repeat_captured_span(acc_nodes: result.acc_nodes) { Rejected { diagnostics: r } => ParseExprRejected { diagnostics: list_append( diff --git a/src/v4/test/claim/parse/parse_table_claims.dag b/src/v4/test/claim/parse/parse_table_claims.dag index 1837f60c4b8..5f332008e4c 100644 --- a/src/v4/test/claim/parse/parse_table_claims.dag +++ b/src/v4/test/claim/parse/parse_table_claims.dag @@ -21,7 +21,16 @@ import v4.std.logic { Bool } import v4.std.collection { List, Set } import v4.std.algebra { Cons, Empty, length } import v4.std.lexing { Token } -import v4.std.node { Symbol } +import v4.std.diagnostic { Accepted, Rejected, Unanchored } +import v4.std.node { + Anchored, + Atom, + Node, + NodeSpan, + SourceSpan, + Symbol, + TypeNode +} import v4.std.grammar { Choice, GrammarExpr, @@ -42,6 +51,8 @@ import v4.compiler.parse { expr_direct_left_corner_list, expr_has_undefined_nonterminal, expr_is_nullable_given_set, + parse_repeat_captured_span, + parse_sequence_captured_span, token_position_indices } @@ -347,3 +358,74 @@ data unified_claim_parse_table_undefined_nonterminal_morphism: UnifiedTestClaim function: parse_table_undefined_nonterminal_morphism_holds } } + + +fn parse_table_span_fixture_node(class: Symbol, file: Symbol, start: Int, end: Int) -> Node { + Node { + kind: TypeNode { connective: Atom { identity: class } }, + children: [], + span: Anchored { span: SourceSpan { file: file, start: start, end: end } } + } +} + + +fn parse_table_node_span_is_anchored_extent(span: NodeSpan, file: Symbol, start: Int, end: Int) -> Bool { + match span { + Unanchored => false + Anchored { span: s } => (s.file == file) && (s.start == start) && (s.end == end) + } +} + + +// Receipt F (parse_sequence_captured_span / parse_repeat_captured_span are correct +// fold_node_tree_span consumers): EXECUTES the substrate tree-span catamorphism over Conj-wrapped +// capture fixtures and discriminates: +// - Sequence same-file: merged byte extent [0, 10) +// - Sequence cross-file: fail-closed Rejected +// - Repeat two same-file nodes: merged [2, 12) +// - Repeat empty: Unanchored +// Mutating fold_node_tree_span's merge algebra flips at least one conjunct → red. +fn parse_table_captured_tree_span_morphism_holds() -> Bool { + let file_a = ^pt_span_fixture_file_a + let file_b = ^pt_span_fixture_file_b + let cap1 = parse_table_span_fixture_node(class: ^pt_span_tok_a, file: file_a, start: 0, end: 5) + let cap2 = parse_table_span_fixture_node(class: ^pt_span_tok_b, file: file_a, start: 5, end: 10) + let cap3 = parse_table_span_fixture_node(class: ^pt_span_tok_c, file: file_b, start: 0, end: 5) + let rep0 = parse_table_span_fixture_node(class: ^pt_span_tok_d, file: file_a, start: 2, end: 7) + let rep1 = parse_table_span_fixture_node(class: ^pt_span_tok_e, file: file_a, start: 7, end: 12) + ( + match parse_sequence_captured_span(cap1: cap1, cap2: cap2) { + Accepted { value: span, diagnostics: _ } => + parse_table_node_span_is_anchored_extent(span: span, file: file_a, start: 0, end: 10) + Rejected { diagnostics: _ } => false + } + ) + && ( + match parse_sequence_captured_span(cap1: cap1, cap2: cap3) { + Rejected { diagnostics: _ } => true + Accepted { value: _, diagnostics: _ } => false + } + ) + && ( + match parse_repeat_captured_span(acc_nodes: Cons { head: rep0, tail: Cons { head: rep1, tail: Empty } }) { + Accepted { value: span, diagnostics: _ } => + parse_table_node_span_is_anchored_extent(span: span, file: file_a, start: 2, end: 12) + Rejected { diagnostics: _ } => false + } + ) + && ( + match parse_repeat_captured_span(acc_nodes: Empty) { + Accepted { value: span, diagnostics: _ } => span == Unanchored + Rejected { diagnostics: _ } => false + } + ) +} + + +// Co-located BoolWitnessClaim for fold_node_tree_span capture-span migration (Level-1c). +data unified_claim_parse_table_captured_tree_span_morphism: UnifiedTestClaim = BoolWitnessClaim { + witness: BoolWitness { + entry: "src/v4/test/claim/parse/parse_table_claims.dag", + function: parse_table_captured_tree_span_morphism_holds + } +} From 318307b752577e6dcc8dcc46b7265ad04560f0f3 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Thu, 11 Jun 2026 01:01:34 +0000 Subject: [PATCH 2/2] fix(parse claims): import Unanchored from v4.std.node for Level-1c span witness Co-authored-by: Cursor --- src/v4/test/claim/parse/parse_table_claims.dag | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/src/v4/test/claim/parse/parse_table_claims.dag b/src/v4/test/claim/parse/parse_table_claims.dag index 5f332008e4c..b0fb2d9954e 100644 --- a/src/v4/test/claim/parse/parse_table_claims.dag +++ b/src/v4/test/claim/parse/parse_table_claims.dag @@ -21,7 +21,7 @@ import v4.std.logic { Bool } import v4.std.collection { List, Set } import v4.std.algebra { Cons, Empty, length } import v4.std.lexing { Token } -import v4.std.diagnostic { Accepted, Rejected, Unanchored } +import v4.std.diagnostic { Accepted, Rejected } import v4.std.node { Anchored, Atom, @@ -29,7 +29,8 @@ import v4.std.node { NodeSpan, SourceSpan, Symbol, - TypeNode + TypeNode, + Unanchored } import v4.std.grammar { Choice,