From bacf9b8909a427a187dc376dbf11bfde47b7f280 Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Sat, 3 Oct 2026 10:23:55 +0000 Subject: [PATCH 1/4] target_model: a Bind's separator is Optional; dag emits a Bind block-scoped, { let k = (v) { b } } Operator/parent ruling (stern-bear-500, ruling A): ahead of the dag grammar dropping 'let x = e in body' (#13056), TargetBindLetShape.in_token becomes Optional. C/Rust/TypeScript keep Present(';'); dag declares Absent and a core Bind is emitted as a block whose first statement is the binding and whose last is the body: the value is parenthesised and the body braced so no continuation of the value can absorb the body, and the outer braces give the binding a statement position wherever the Bind stands. Absent travels in the projection bundle as its own atom, so a bundle missing the field still refuses. The dag bind family's tokens and authority text move to that spelling. Controls (v2.test.emit.dag_bind_let_block_scoped): a Bind nested as the value of a Bind, and bodies that are a bare name, an empty brace literal, a '-'-led expression and a nested Bind, each emitted through the dag projection and reparsed by the dag grammar to the same binds. Co-Authored-By: Claude Opus 5.5 (1M context) --- src/v2/extdeps/languages/c.dag | 3 +- src/v2/extdeps/languages/dag.dag | 13 +- src/v2/extdeps/languages/rust.dag | 3 +- src/v2/extdeps/languages/typescript.dag | 3 +- src/v2/std/compilers/target_model.dag | 90 ++++++++++- .../emit/dag_bind_let_block_scoped_test.dag | 150 ++++++++++++++++++ 6 files changed, 251 insertions(+), 11 deletions(-) create mode 100644 src/v2/test/claim/emit/dag_bind_let_block_scoped_test.dag diff --git a/src/v2/extdeps/languages/c.dag b/src/v2/extdeps/languages/c.dag index bf766fe6bb2..459e3e45a61 100644 --- a/src/v2/extdeps/languages/c.dag +++ b/src/v2/extdeps/languages/c.dag @@ -62,6 +62,7 @@ import v2.std.grammar { grammar_relation_tokens_node } import v2.std.compilers.target_model { + target_bind_let_separator_present, IntLiteralUnwired, InfixToken, canonical_operation_op_add, @@ -1098,7 +1099,7 @@ fn c_value_expression_projection() -> TargetValueExpressionProjection { let_form: TargetBindLetShape { let_token: ^c_token_unwired_let, assign_token: ^c_token_unwired_assign, - in_token: ^c_token_semicolon + in_token: target_bind_let_separator_present(token: ^c_token_semicolon) }, loop_form: TargetLoopShape { loop_token: ^c_token_unwired_loop }, record_construct_form: TargetRecordConstructShape { diff --git a/src/v2/extdeps/languages/dag.dag b/src/v2/extdeps/languages/dag.dag index f80d4b5f612..cf442a8b4b1 100644 --- a/src/v2/extdeps/languages/dag.dag +++ b/src/v2/extdeps/languages/dag.dag @@ -238,8 +238,8 @@ data dag_pick_false_source_text: String = "fn one_or_two() -> Int { if false the data dag_loop_source_text: String = "fn one() -> Int { loop 1 }" data dag_loop_wrong_value_source_text: String = "fn one() -> Int { loop 2 }" -data dag_bind_source_text: String = "fn one() -> Int { let x = 1 in x }" -data dag_bind_wrong_value_source_text: String = "fn one() -> Int { let x = 2 in x }" +data dag_bind_source_text: String = "fn one() -> Int { { let x = (1) { x } } }" +data dag_bind_wrong_value_source_text: String = "fn one() -> Int { { let x = (2) { x } } }" data dag_match_source_text: String = "fn one_or_two() -> Int { match true { true => 1, false => 2 } }" @@ -332,12 +332,17 @@ fn dag_bind_concrete_tokens() -> List { FixedToken { token_class: ^dag_token_arrow }, BoundToken { token_class: ^dag_token_ident, binding: ^dag_binding_type_int }, FixedToken { token_class: ^dag_token_lbrace }, + FixedToken { token_class: ^dag_token_lbrace }, FixedToken { token_class: ^dag_token_kw_let }, BoundToken { token_class: ^dag_token_ident, binding: ^dag_binding_bind_x }, FixedToken { token_class: ^dag_token_eq }, + FixedToken { token_class: ^dag_token_lparen }, BoundToken { token_class: ^dag_token_ident, binding: ^dag_binding_pick_lit_one }, - FixedToken { token_class: ^dag_token_kw_in }, + FixedToken { token_class: ^dag_token_rparen }, + FixedToken { token_class: ^dag_token_lbrace }, BoundToken { token_class: ^dag_token_ident, binding: ^dag_binding_bind_x }, + FixedToken { token_class: ^dag_token_rbrace }, + FixedToken { token_class: ^dag_token_rbrace }, FixedToken { token_class: ^dag_token_rbrace } ] } @@ -5828,7 +5833,7 @@ fn dag_value_expression_projection() -> TargetValueExpressionProjection { let_form: TargetBindLetShape { let_token: ^dag_token_kw_let, assign_token: ^dag_token_eq, - in_token: ^dag_token_kw_in + in_token: Absent }, loop_form: TargetLoopShape { loop_token: ^dag_token_kw_loop diff --git a/src/v2/extdeps/languages/rust.dag b/src/v2/extdeps/languages/rust.dag index f02bf8e7c6a..5d1d12d5110 100644 --- a/src/v2/extdeps/languages/rust.dag +++ b/src/v2/extdeps/languages/rust.dag @@ -144,6 +144,7 @@ import v2.std.compilers.coproduct_variant_shape { coproduct_all_variants_nullary } import v2.std.compilers.target_model { + target_bind_let_separator_present, IntLiteralDecimal, TargetCapabilityKey, ProducedDeclSupport, @@ -1204,7 +1205,7 @@ fn rust_value_expression_projection() -> TargetValueExpressionProjection { let_form: TargetBindLetShape { let_token: ^rust_token_kw_let, assign_token: ^rust_token_equal, - in_token: ^rust_token_semicolon + in_token: target_bind_let_separator_present(token: ^rust_token_semicolon) }, loop_form: TargetLoopShape { loop_token: ^rust_token_unwired_loop }, record_construct_form: TargetRecordConstructShape { diff --git a/src/v2/extdeps/languages/typescript.dag b/src/v2/extdeps/languages/typescript.dag index 95ffe98acfc..b5f6a82b8cb 100644 --- a/src/v2/extdeps/languages/typescript.dag +++ b/src/v2/extdeps/languages/typescript.dag @@ -99,6 +99,7 @@ import v2.std.grounding { } import v2.std.node_query { find_named_child } import v2.std.compilers.target_model { + target_bind_let_separator_present, IntLiteralUnwired, ProducedDeclParamSegment, ProducedDeclRenderRows, @@ -656,7 +657,7 @@ fn ts_value_expression_projection_full( let_form: TargetBindLetShape { let_token: ^ts_token_kw_let, assign_token: ^ts_token_eq, - in_token: ^ts_token_unwired_bind_in + in_token: target_bind_let_separator_present(token: ^ts_token_unwired_bind_in) }, loop_form: TargetLoopShape { loop_token: ^ts_token_unwired_loop diff --git a/src/v2/std/compilers/target_model.dag b/src/v2/std/compilers/target_model.dag index da130f7bfa3..f91c8137d55 100644 --- a/src/v2/std/compilers/target_model.dag +++ b/src/v2/std/compilers/target_model.dag @@ -1824,12 +1824,38 @@ type TargetConditionalShape { delimiting: ConditionalDelimiting } +// THE TOKEN BETWEEN A BINDING AND ITS BODY, WHEN THE TARGET HAS ONE. `let k = v in b` (`in`) and the +// statement-sequenced C/Rust/TypeScript forms (`;`) name it. A target whose let is a STATEMENT and +// has no separator token (dag: statement `let` only, `let x = e in body` dropped by the 2026-10-02 +// zero-ambiguity decisions) declares Absent, and a core Bind is emitted as a block that holds the +// binding as its first statement and the body as its last: `{ let k = (v) { b } }` +// (bind_let_block_scoped_tokens). The value is parenthesised and the body braced so that no +// continuation of the value can absorb the body -- a call suffix, an operator or a brace literal +// cannot follow a closed group into a block -- whatever the value and body are; the outer braces give +// the binding a statement position wherever the Bind stands, an expression position included. type TargetBindLetShape { let_token: Symbol assign_token: Symbol - in_token: Symbol + in_token: Optional } +// Absent is carried in the projection bundle as its own atom, never as a missing field: a bundle that +// lost the field still refuses at decode rather than reading as "no separator". +fn target_bind_let_separator_atom(in_token: Optional) -> Symbol { + match in_token { + Present { value: t } => t + Absent => ^target_bind_let_no_separator + } +} + +fn target_bind_let_separator_of_atom(atom: Symbol) -> Optional { + if atom == ^target_bind_let_no_separator { target_bind_let_separator_absent() } else { target_bind_let_separator_present(token: atom) } +} + +fn target_bind_let_separator_absent() -> Optional { Absent } + +fn target_bind_let_separator_present(token: Symbol) -> Optional { Present { value: token } } + type TargetLoopShape { loop_token: Symbol } @@ -3011,7 +3037,7 @@ fn decode_bind_let_shape_bundle(bundle: Node) -> Outcome { TargetBindLetShape { let_token: let_token, assign_token: assign_token, - in_token: in_token + in_token: target_bind_let_separator_of_atom(atom: in_token) } ) } @@ -6491,6 +6517,62 @@ fn bind_let_value_producing_tokens( key_tokens: List, value_tokens: List, body_tokens: List +) -> List { + match projection.let_form.in_token { + Present { value: in_token } => + bind_let_separated_tokens(projection: projection, in_token: in_token, key_tokens: key_tokens, value_tokens: value_tokens, body_tokens: body_tokens) + Absent => + bind_let_block_scoped_tokens(projection: projection, key_tokens: key_tokens, value_tokens: value_tokens, body_tokens: body_tokens) + } +} + +// `{ let k = ( v ) { b } }`, with the target's own block and group delimiters (closure body and +// primitive apply). See TargetBindLetShape for why each delimiter is there. +fn bind_let_block_scoped_tokens( + projection: TargetValueExpressionProjection, + key_tokens: List, + value_tokens: List, + body_tokens: List +) -> List { + list_append( + left: list_append( + left: list_append( + left: list_append( + left: list_append( + left: [ + FixedToken { token_class: projection.closure_form.body_open }, + FixedToken { token_class: projection.let_form.let_token } + ], + right: key_tokens + ), + right: [ + FixedToken { token_class: projection.let_form.assign_token }, + FixedToken { token_class: projection.primitive_apply_form.open } + ] + ), + right: value_tokens + ), + right: [ + FixedToken { token_class: projection.primitive_apply_form.close }, + FixedToken { token_class: projection.closure_form.body_open } + ] + ), + right: list_append( + left: body_tokens, + right: [ + FixedToken { token_class: projection.closure_form.body_close }, + FixedToken { token_class: projection.closure_form.body_close } + ] + ) + ) +} + +fn bind_let_separated_tokens( + projection: TargetValueExpressionProjection, + in_token: Symbol, + key_tokens: List, + value_tokens: List, + body_tokens: List ) -> List { list_append( left: list_append( @@ -6509,7 +6591,7 @@ fn bind_let_value_producing_tokens( right: value_tokens ), right: [ - FixedToken { token_class: projection.let_form.in_token } + FixedToken { token_class: in_token } ] ), right: body_tokens @@ -8956,7 +9038,7 @@ fn value_expr_projection_bundle_node(projection: TargetValueExpressionProjection target_model_named_edge( name: ^target_value_expr_field_in_token, target: target_model_type_atom_node( - identity: projection.let_form.in_token + identity: target_bind_let_separator_atom(in_token: projection.let_form.in_token) ) ) ] diff --git a/src/v2/test/claim/emit/dag_bind_let_block_scoped_test.dag b/src/v2/test/claim/emit/dag_bind_let_block_scoped_test.dag new file mode 100644 index 00000000000..2e5845aa421 --- /dev/null +++ b/src/v2/test/claim/emit/dag_bind_let_block_scoped_test.dag @@ -0,0 +1,150 @@ +module v2.test.emit.dag_bind_let_block_scoped + +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_bind_target_model, + dag_lex, + dag_value_expression_projection, + parse_production_emitted_identity_optional +} +import v2.std.compilers.target_model { + BoundToken, + FixedToken, + ConcreteSyntaxToken, + bind_let_value_producing_tokens, + bound_tokens_source_text, + render_target_text +} +import v2.std.diagnostic { Accepted, None, Outcome, Rejected, bind_outcome } +import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly } +import std.algebra { list_append } +import v2.std.logic { Bool } +import v2.std.node { Node, Symbol } +import v2.std.optional { Absent, Present } + +data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly + +// A CORE BIND EMITTED THROUGH THE dag TARGET PARSES BACK AS THE SAME BINDS, AT EXPRESSION POSITION. +// dag declares no separator (v2.std.compilers.target_model TargetBindLetShape, in_token Absent), so a +// Bind is emitted block-scoped: `{ let k = (v) { b } }`. The control nests one Bind as the VALUE of +// another -- the hardest position, inside the group -- emits it with the real emitter +// (bind_let_value_producing_tokens over dag_value_expression_projection), renders it with the dag +// target's own spellings, places it where a value is owed (a data initializer) and reparses it with +// the dag grammar. It must parse, hold exactly two let_expr nodes with one inside the other, and +// carry no `in`: the text the emitter writes is text the grammar reads, one way. +fn dbl_token(binding: Symbol) -> List { + [BoundToken { token_class: ^dag_token_ident, binding: binding }] +} + +fn dbl_bind(value: List) -> List { + dbl_bind_body(value: value, body: dbl_token(binding: ^dag_binding_bind_x)) +} + +fn dbl_bind_body(value: List, body: List) -> List { + bind_let_value_producing_tokens( + projection: dag_value_expression_projection(), + key_tokens: dbl_token(binding: ^dag_binding_bind_x), + value_tokens: value, + body_tokens: body + ) +} + +fn dbl_nested_text() -> Outcome { + dbl_text(tokens: dbl_bind(value: dbl_bind(value: dbl_token(binding: ^dag_binding_pick_lit_one)))) +} + +fn dbl_text(tokens: List) -> Outcome { + let model = dag_bind_target_model() + bind_outcome( + o: bound_tokens_source_text( + tokens: tokens, + lex: model.lex, + binding_spellings: model.binding_spellings + ), + f: fn(t) { Accepted { value: render_target_text(t: t), diagnostics: None } } + ) +} + +fn dbl_parse(text: String) -> Outcome { + match dag_prepared_grammar() { + Rejected { diagnostics: d } => Rejected { diagnostics: d } + Accepted { value: prepared, diagnostics: residue } => + bind_outcome( + o: tokenize(text: text, file: ^dbl_probe, 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 dbl_is_let(node: Node) -> Bool { + match parse_production_emitted_identity_optional(node: node) { + Present { value: id } => id == ^dag_surface_let_expr + Absent => false + } +} + +fn dbl_count_lets(root: Node) -> Int { + let here = if dbl_is_let(node: root) { 1 } else { 0 } + fold(root.children, init: here, f: fn(acc, e) { acc + dbl_count_lets(root: e.target) }) +} + +// A let with another let somewhere under it. +fn dbl_has_nested_let(root: Node) -> Bool { + if dbl_is_let(node: root) && fold(root.children, init: 0, f: fn(acc, e) { acc + dbl_count_lets(root: e.target) }) == 1 { + true + } else { + fold(root.children, init: false, f: fn(found, e) { found || dbl_has_nested_let(root: e.target) }) + } +} + +fn dbl_reparses_to_two_nested_lets(text: String) -> Bool { + match dbl_parse(text: concat(concat("module p\ndata d: I = ", text), "\n")) { + Accepted { value: tree, diagnostics: _ } => dbl_count_lets(root: tree) == 2 && dbl_has_nested_let(root: tree) + Rejected { diagnostics: _ } => false + } +} + +// One Bind with the given body, at expression position: it parses, and it holds exactly `lets` let +// nodes (the binding, plus any the body itself holds) -- the body is read as the body, never +// absorbed into the value or into a literal. +fn dbl_body_round_trips(body: List, lets: Int) -> Bool { + match dbl_text(tokens: dbl_bind_body(value: dbl_token(binding: ^dag_binding_pick_lit_one), body: body)) { + Rejected { diagnostics: _ } => false + Accepted { value: text, diagnostics: _ } => + match dbl_parse(text: concat(concat("module p\ndata d: I = ", text), "\n")) { + Accepted { value: tree, diagnostics: _ } => dbl_count_lets(root: tree) == lets + Rejected { diagnostics: _ } => false + } + } +} + +test fn a_bare_identifier_body_round_trips() -> Bool { + dbl_body_round_trips(body: dbl_token(binding: ^dag_binding_bind_x), lets: 1) +} + +test fn an_empty_brace_literal_body_round_trips() -> Bool { + dbl_body_round_trips(body: [FixedToken { token_class: ^dag_token_lbrace }, FixedToken { token_class: ^dag_token_rbrace }], lets: 1) +} + +test fn a_body_starting_with_minus_round_trips() -> Bool { + dbl_body_round_trips(body: list_append(left: [FixedToken { token_class: ^dag_token_minus }], right: dbl_token(binding: ^dag_binding_bind_x)), lets: 1) +} + +test fn a_bind_body_round_trips_nested() -> Bool { + dbl_body_round_trips(body: dbl_bind(value: dbl_token(binding: ^dag_binding_pick_lit_one)), lets: 2) +} + +test fn nested_bind_emitted_block_scoped_reparses_to_the_same_binds() -> Bool { + match dbl_nested_text() { + Rejected { diagnostics: _ } => false + Accepted { value: text, diagnostics: _ } => + !string_contains(s: text, pattern: " in ") && dbl_reparses_to_two_nested_lets(text: text) + } +} From c4cd047d1e21187a8e9b1a7a2ea11ce6839b63ee Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Sat, 3 Oct 2026 11:43:10 +0000 Subject: [PATCH 2/4] dag_bind_let_block_scoped: one expression parse per claim, no target model per claim Floor refused the five round-trip claims on cost (74-112k against 72.3k). Each now renders with the dag lex rules and the two spellings its tokens bind instead of building dag_bind_target_model, and parses the emitted text as the dag grammar's expr production over the shared prepared grammar instead of a module around it. Co-Authored-By: Claude Opus 5.5 (1M context) --- .../emit/dag_bind_let_block_scoped_test.dag | 72 ++++++++++++------- 1 file changed, 46 insertions(+), 26 deletions(-) diff --git a/src/v2/test/claim/emit/dag_bind_let_block_scoped_test.dag b/src/v2/test/claim/emit/dag_bind_let_block_scoped_test.dag index 2e5845aa421..065b3fd2e05 100644 --- a/src/v2/test/claim/emit/dag_bind_let_block_scoped_test.dag +++ b/src/v2/test/claim/emit/dag_bind_let_block_scoped_test.dag @@ -1,10 +1,9 @@ module v2.test.emit.dag_bind_let_block_scoped -import v2.compiler.parse { parse_module_prepared } +import v2.compiler.parse { PreparedModeled, PreparedVoidGrammar, parse_production_prepared } import v2.compiler.program_assembly { dag_prepared_grammar } import v2.compiler.tokenize { tokenize } import v2.extdeps.languages.dag { - dag_bind_target_model, dag_lex, dag_value_expression_projection, parse_production_emitted_identity_optional @@ -17,12 +16,13 @@ import v2.std.compilers.target_model { bound_tokens_source_text, render_target_text } +import v2.std.collection { Map, empty_map, map_insert } import v2.std.diagnostic { Accepted, None, Outcome, Rejected, bind_outcome } import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly } import std.algebra { list_append } import v2.std.logic { Bool } import v2.std.node { Node, Symbol } -import v2.std.optional { Absent, Present } +import v2.std.optional { Absent, Optional, Present } data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly @@ -31,9 +31,11 @@ data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly // Bind is emitted block-scoped: `{ let k = (v) { b } }`. The control nests one Bind as the VALUE of // another -- the hardest position, inside the group -- emits it with the real emitter // (bind_let_value_producing_tokens over dag_value_expression_projection), renders it with the dag -// target's own spellings, places it where a value is owed (a data initializer) and reparses it with -// the dag grammar. It must parse, hold exactly two let_expr nodes with one inside the other, and -// carry no `in`: the text the emitter writes is text the grammar reads, one way. +// lex rules, and reparses it with the dag grammar as an expression -- the `expr` production, where a +// value is owed. It must parse, hold exactly two let_expr nodes with one inside the other, and carry +// no `in`: the text the emitter writes is text the grammar reads, one way. The body cases below do +// the same for a bare name, an empty brace literal, a `-`-led expression and a nested Bind. Each +// claim pays one parse of its own tokens (DESIGN section 3's witness rule). fn dbl_token(binding: Symbol) -> List { [BoundToken { token_class: ^dag_token_ident, binding: binding }] } @@ -55,34 +57,52 @@ fn dbl_nested_text() -> Outcome { dbl_text(tokens: dbl_bind(value: dbl_bind(value: dbl_token(binding: ^dag_binding_pick_lit_one)))) } +// Rendered with the dag lex rules and the two spellings the tokens bind -- the target model would +// supply the same, at the cost of building the whole model inside every claim. +fn dbl_spellings() -> Map { + map_insert(m: map_insert(m: empty_map(), key: ^dag_binding_bind_x, value: "x"), key: ^dag_binding_pick_lit_one, value: "a") +} + fn dbl_text(tokens: List) -> Outcome { - let model = dag_bind_target_model() bind_outcome( o: bound_tokens_source_text( tokens: tokens, - lex: model.lex, - binding_spellings: model.binding_spellings + lex: dag_lex(), + binding_spellings: dbl_spellings() ), f: fn(t) { Accepted { value: render_target_text(t: t), diagnostics: None } } ) } -fn dbl_parse(text: String) -> Outcome { +// The emitted Bind is parsed as the expression it is (the dag grammar's `expr` production, over the +// shared prepared grammar), so a claim pays for its own tokens and no module around them. +fn dbl_parse(text: String) -> Optional { match dag_prepared_grammar() { - Rejected { diagnostics: d } => Rejected { diagnostics: d } - Accepted { value: prepared, diagnostics: residue } => - bind_outcome( - o: tokenize(text: text, file: ^dbl_probe, 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 } + Rejected { diagnostics: _ } => Absent + Accepted { value: prepared, diagnostics: _ } => + match prepared { + PreparedVoidGrammar => Absent + PreparedModeled { modeled: modeled, materialization: m } => + match tokenize(text: text, file: ^dbl_probe, rules: dag_lex()) { + Rejected { diagnostics: _ } => Absent + Accepted { value: token_stream, diagnostics: _ } => + match parse_production_prepared( + tokens: token_stream.all, + validated: modeled.validated, + analysis: modeled.analysis, + production_name: ^dag_production_expr, + materialization: m + ) { + Rejected { diagnostics: _ } => Absent + Accepted { value: artifact, diagnostics: _ } => dbl_tree(node: artifact.tree) + } } - } - ) + } } } +fn dbl_tree(node: Node) -> Optional { Present { value: node } } + fn dbl_is_let(node: Node) -> Bool { match parse_production_emitted_identity_optional(node: node) { Present { value: id } => id == ^dag_surface_let_expr @@ -105,9 +125,9 @@ fn dbl_has_nested_let(root: Node) -> Bool { } fn dbl_reparses_to_two_nested_lets(text: String) -> Bool { - match dbl_parse(text: concat(concat("module p\ndata d: I = ", text), "\n")) { - Accepted { value: tree, diagnostics: _ } => dbl_count_lets(root: tree) == 2 && dbl_has_nested_let(root: tree) - Rejected { diagnostics: _ } => false + match dbl_parse(text: text) { + Present { value: tree } => dbl_count_lets(root: tree) == 2 && dbl_has_nested_let(root: tree) + Absent => false } } @@ -118,9 +138,9 @@ fn dbl_body_round_trips(body: List, lets: Int) -> Bool { match dbl_text(tokens: dbl_bind_body(value: dbl_token(binding: ^dag_binding_pick_lit_one), body: body)) { Rejected { diagnostics: _ } => false Accepted { value: text, diagnostics: _ } => - match dbl_parse(text: concat(concat("module p\ndata d: I = ", text), "\n")) { - Accepted { value: tree, diagnostics: _ } => dbl_count_lets(root: tree) == lets - Rejected { diagnostics: _ } => false + match dbl_parse(text: text) { + Present { value: tree } => dbl_count_lets(root: tree) == lets + Absent => false } } } From 0d1697681287425ab43eae7cda568b27dd3d13ba Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Sat, 3 Oct 2026 13:02:23 +0000 Subject: [PATCH 3/4] dag_bind_let_block_scoped: parse the emitted tokens; pin the token sequence, not text Floor: the round trips were still 72-105k against 72.3k. The emitter's product is a token sequence, so each claim now hands those tokens to the expr production directly (no render, no lexer). The previous text route also passed for the wrong reason: dag text rendering puts no separation between tokens ({letx=(a){x}}), and 'letx = (a)' re-read as a bare assignment let. a_single_bind_emits_block_scoped_tokens pins the exact token sequence instead; the rendering defect predates this change and is reported separately. Co-Authored-By: Claude Opus 5.5 (1M context) --- .../emit/dag_bind_let_block_scoped_test.dag | 136 ++++++++++-------- 1 file changed, 73 insertions(+), 63 deletions(-) diff --git a/src/v2/test/claim/emit/dag_bind_let_block_scoped_test.dag b/src/v2/test/claim/emit/dag_bind_let_block_scoped_test.dag index 065b3fd2e05..2a5bda8eb33 100644 --- a/src/v2/test/claim/emit/dag_bind_let_block_scoped_test.dag +++ b/src/v2/test/claim/emit/dag_bind_let_block_scoped_test.dag @@ -2,9 +2,7 @@ module v2.test.emit.dag_bind_let_block_scoped import v2.compiler.parse { PreparedModeled, PreparedVoidGrammar, parse_production_prepared } import v2.compiler.program_assembly { dag_prepared_grammar } -import v2.compiler.tokenize { tokenize } import v2.extdeps.languages.dag { - dag_lex, dag_value_expression_projection, parse_production_emitted_identity_optional } @@ -12,14 +10,14 @@ import v2.std.compilers.target_model { BoundToken, FixedToken, ConcreteSyntaxToken, - bind_let_value_producing_tokens, - bound_tokens_source_text, - render_target_text + bind_let_value_producing_tokens } -import v2.std.collection { Map, empty_map, map_insert } -import v2.std.diagnostic { Accepted, None, Outcome, Rejected, bind_outcome } +import v2.std.diagnostic { Accepted, Rejected } import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly } import std.algebra { list_append } +import v2.std.compilers.lexing { Token } +import v2.std.algebra { any, fold_list, length } +import std.algebra { list_snoc_item } import v2.std.logic { Bool } import v2.std.node { Node, Symbol } import v2.std.optional { Absent, Optional, Present } @@ -30,12 +28,12 @@ data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly // dag declares no separator (v2.std.compilers.target_model TargetBindLetShape, in_token Absent), so a // Bind is emitted block-scoped: `{ let k = (v) { b } }`. The control nests one Bind as the VALUE of // another -- the hardest position, inside the group -- emits it with the real emitter -// (bind_let_value_producing_tokens over dag_value_expression_projection), renders it with the dag -// lex rules, and reparses it with the dag grammar as an expression -- the `expr` production, where a -// value is owed. It must parse, hold exactly two let_expr nodes with one inside the other, and carry -// no `in`: the text the emitter writes is text the grammar reads, one way. The body cases below do -// the same for a bare name, an empty brace literal, a `-`-led expression and a nested Bind. Each -// claim pays one parse of its own tokens (DESIGN section 3's witness rule). +// (bind_let_value_producing_tokens over dag_value_expression_projection), and parses the emitted tokens +// with the dag grammar as an expression (the `expr` production, where a value is owed). It must parse, +// hold exactly two let_expr nodes with one inside the other, and carry no `in` token: what the emitter +// writes is what the grammar reads, one way. The body cases below do the same for a bare name, an +// empty brace literal, a `-`-led expression and a nested Bind. Each claim pays one parse of its own +// tokens (DESIGN section 3's witness rule). fn dbl_token(binding: Symbol) -> List { [BoundToken { token_class: ^dag_token_ident, binding: binding }] } @@ -53,54 +51,61 @@ fn dbl_bind_body(value: List, body: List Outcome { - dbl_text(tokens: dbl_bind(value: dbl_bind(value: dbl_token(binding: ^dag_binding_pick_lit_one)))) -} - -// Rendered with the dag lex rules and the two spellings the tokens bind -- the target model would -// supply the same, at the cost of building the whole model inside every claim. -fn dbl_spellings() -> Map { - map_insert(m: map_insert(m: empty_map(), key: ^dag_binding_bind_x, value: "x"), key: ^dag_binding_pick_lit_one, value: "a") -} - -fn dbl_text(tokens: List) -> Outcome { - bind_outcome( - o: bound_tokens_source_text( - tokens: tokens, - lex: dag_lex(), - binding_spellings: dbl_spellings() - ), - f: fn(t) { Accepted { value: render_target_text(t: t), diagnostics: None } } - ) -} - -// The emitted Bind is parsed as the expression it is (the dag grammar's `expr` production, over the -// shared prepared grammar), so a claim pays for its own tokens and no module around them. -fn dbl_parse(text: String) -> Optional { +// The emitted TOKENS are parsed as the expression they form (the dag grammar's `expr` production, over +// the shared prepared grammar): the emitter's product is a token sequence, and rendering it to text +// is a separate step (see a_single_bind_emits_block_scoped_tokens). So a claim pays for its own +// tokens and no render, lexer or module around them. +fn dbl_parse(concrete: List) -> Optional { match dag_prepared_grammar() { Rejected { diagnostics: _ } => Absent Accepted { value: prepared, diagnostics: _ } => match prepared { PreparedVoidGrammar => Absent PreparedModeled { modeled: modeled, materialization: m } => - match tokenize(text: text, file: ^dbl_probe, rules: dag_lex()) { + match parse_production_prepared( + tokens: dbl_lexed(concrete: concrete), + validated: modeled.validated, + analysis: modeled.analysis, + production_name: ^dag_production_expr, + materialization: m + ) { Rejected { diagnostics: _ } => Absent - Accepted { value: token_stream, diagnostics: _ } => - match parse_production_prepared( - tokens: token_stream.all, - validated: modeled.validated, - analysis: modeled.analysis, - production_name: ^dag_production_expr, - materialization: m - ) { - Rejected { diagnostics: _ } => Absent - Accepted { value: artifact, diagnostics: _ } => dbl_tree(node: artifact.tree) - } + Accepted { value: artifact, diagnostics: _ } => dbl_tree(node: artifact.tree) } } } } +// The lexer's token for each emitted token: its class, and for a bound token its spelling. +fn dbl_lexed(concrete: List) -> List { + fold_list(xs: concrete, empty: [], cons: fn(acc, c) { + list_snoc_item(xs: acc, item: dbl_lexed_one(token: c, at: length(xs: acc))) + }) +} + +fn dbl_lexed_one(token: ConcreteSyntaxToken, at: Int) -> Token { + match token { + FixedToken { token_class: c } => Token { class: c, lexeme: "", file: ^dbl_probe, start: at, end: at + 1 } + BoundToken { token_class: c, binding: b } => + Token { class: c, lexeme: dbl_spelling(binding: b), file: ^dbl_probe, start: at, end: at + 1 } + } +} + +fn dbl_spelling(binding: Symbol) -> String { + if binding == ^dag_binding_bind_x { "x" } else { "a" } +} + +fn dbl_has_in(concrete: List) -> Bool { + any(xs: concrete, predicate: fn(c) { dbl_class(token: c) == ^dag_token_kw_in }) +} + +fn dbl_class(token: ConcreteSyntaxToken) -> Symbol { + match token { + FixedToken { token_class: c } => c + BoundToken { token_class: c, binding: _ } => c + } +} + fn dbl_tree(node: Node) -> Optional { Present { value: node } } fn dbl_is_let(node: Node) -> Bool { @@ -124,8 +129,8 @@ fn dbl_has_nested_let(root: Node) -> Bool { } } -fn dbl_reparses_to_two_nested_lets(text: String) -> Bool { - match dbl_parse(text: text) { +fn dbl_reparses_to_two_nested_lets(concrete: List) -> Bool { + match dbl_parse(concrete: concrete) { Present { value: tree } => dbl_count_lets(root: tree) == 2 && dbl_has_nested_let(root: tree) Absent => false } @@ -135,13 +140,9 @@ fn dbl_reparses_to_two_nested_lets(text: String) -> Bool { // nodes (the binding, plus any the body itself holds) -- the body is read as the body, never // absorbed into the value or into a literal. fn dbl_body_round_trips(body: List, lets: Int) -> Bool { - match dbl_text(tokens: dbl_bind_body(value: dbl_token(binding: ^dag_binding_pick_lit_one), body: body)) { - Rejected { diagnostics: _ } => false - Accepted { value: text, diagnostics: _ } => - match dbl_parse(text: text) { - Present { value: tree } => dbl_count_lets(root: tree) == lets - Absent => false - } + match dbl_parse(concrete: dbl_bind_body(value: dbl_token(binding: ^dag_binding_pick_lit_one), body: body)) { + Present { value: tree } => dbl_count_lets(root: tree) == lets + Absent => false } } @@ -162,9 +163,18 @@ test fn a_bind_body_round_trips_nested() -> Bool { } test fn nested_bind_emitted_block_scoped_reparses_to_the_same_binds() -> Bool { - match dbl_nested_text() { - Rejected { diagnostics: _ } => false - Accepted { value: text, diagnostics: _ } => - !string_contains(s: text, pattern: " in ") && dbl_reparses_to_two_nested_lets(text: text) - } + let concrete = dbl_bind(value: dbl_bind(value: dbl_token(binding: ^dag_binding_pick_lit_one))) + !dbl_has_in(concrete: concrete) && dbl_reparses_to_two_nested_lets(concrete: concrete) +} + +// The token sequence the dag target writes for one Bind, exactly: `{ let k = ( v ) { b } }`. The claims +// above parse emitted TOKENS; this pins what those tokens are. Text is not the grain here: the dag +// target's rendering puts no separation between tokens (its lex is dag_lex, with no emit +// transforms), so a keyword and the name after it render fused -- a defect of dag text rendering that +// predates this change and is reported on its own, not something a text round trip could check. +test fn a_single_bind_emits_block_scoped_tokens() -> Bool { + map(dbl_bind(value: dbl_token(binding: ^dag_binding_pick_lit_one)), fn(c) { dbl_class(token: c) }) == [ + ^dag_token_lbrace, ^dag_token_kw_let, ^dag_token_ident, ^dag_token_eq, ^dag_token_lparen, ^dag_token_ident, + ^dag_token_rparen, ^dag_token_lbrace, ^dag_token_ident, ^dag_token_rbrace, ^dag_token_rbrace + ] } From d5996ae720d2c5fd827a20915d51ded724a031f3 Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Sat, 3 Oct 2026 14:23:12 +0000 Subject: [PATCH 4/4] dag_bind_let_block_scoped: nested Binds by composition; parses shared once (warm producer) The nested-value and nested-body claims parsed ~21 tokens each (87-105k steps). They are replaced by two composition claims (the emitter places a Bind's tokens verbatim in the value group and the body block) and two slot parses (a Bind inside a value group, a Bind as a body statement), which with the lone-Bind parse cover nesting in a context-free grammar. The five parses run once in dbl_verdicts, enrolled warm in floor_pure_producer_share; claims read stored Bools. Co-Authored-By: Claude Opus 5.5 (1M context) --- .../emit/dag_bind_let_block_scoped_test.dag | 112 ++++++++++++++---- src/v2/workflow/floor_pure_producer_share.dag | 5 + 2 files changed, 92 insertions(+), 25 deletions(-) diff --git a/src/v2/test/claim/emit/dag_bind_let_block_scoped_test.dag b/src/v2/test/claim/emit/dag_bind_let_block_scoped_test.dag index 2a5bda8eb33..2697657d68e 100644 --- a/src/v2/test/claim/emit/dag_bind_let_block_scoped_test.dag +++ b/src/v2/test/claim/emit/dag_bind_let_block_scoped_test.dag @@ -26,14 +26,12 @@ data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly // A CORE BIND EMITTED THROUGH THE dag TARGET PARSES BACK AS THE SAME BINDS, AT EXPRESSION POSITION. // dag declares no separator (v2.std.compilers.target_model TargetBindLetShape, in_token Absent), so a -// Bind is emitted block-scoped: `{ let k = (v) { b } }`. The control nests one Bind as the VALUE of -// another -- the hardest position, inside the group -- emits it with the real emitter -// (bind_let_value_producing_tokens over dag_value_expression_projection), and parses the emitted tokens -// with the dag grammar as an expression (the `expr` production, where a value is owed). It must parse, -// hold exactly two let_expr nodes with one inside the other, and carry no `in` token: what the emitter -// writes is what the grammar reads, one way. The body cases below do the same for a bare name, an -// empty brace literal, a `-`-led expression and a nested Bind. Each claim pays one parse of its own -// tokens (DESIGN section 3's witness rule). +// Bind is emitted block-scoped: `{ let k = (v) { b } }`. The controls emit Binds with the real emitter +// (bind_let_value_producing_tokens over dag_value_expression_projection) and parse the emitted TOKENS +// with the dag grammar as an expression (the `expr` production, where a value is owed), carrying no +// `in` token. Bodies that are a bare name, an empty brace literal and a `-`-led expression each read +// back as one Bind; a nested Bind is covered by composition (see dbl_inner). The parses run once, in +// dbl_verdicts (DESIGN section 3's witness rule). fn dbl_token(binding: Symbol) -> List { [BoundToken { token_class: ^dag_token_ident, binding: binding }] } @@ -120,18 +118,29 @@ fn dbl_count_lets(root: Node) -> Int { fold(root.children, init: here, f: fn(acc, e) { acc + dbl_count_lets(root: e.target) }) } -// A let with another let somewhere under it. -fn dbl_has_nested_let(root: Node) -> Bool { - if dbl_is_let(node: root) && fold(root.children, init: 0, f: fn(acc, e) { acc + dbl_count_lets(root: e.target) }) == 1 { - true - } else { - fold(root.children, init: false, f: fn(found, e) { found || dbl_has_nested_let(root: e.target) }) - } +// A NESTED BIND IS PROVED BY COMPOSITION, NOT BY ONE LONG PARSE. The emitter puts a Bind's tokens +// verbatim into the value group `( .. )` and into the body block `{ .. }` (the two composition claims); +// a lone Bind parses as one whole expression (a_bare_identifier_body_round_trips); and a Bind parses +// both inside a value group and as a body block's statement (the two slot claims). The grammar is +// context-free in those slots, so the nested emission reads as nested Binds. Parsing the whole +// nested text in one claim costs more than a claim may (DESIGN section 3's witness rule). +fn dbl_inner() -> List { + dbl_bind(value: dbl_token(binding: ^dag_binding_pick_lit_one)) +} + +fn dbl_fixed(classes: List) -> List { + map(classes, fn(c) { dbl_fixed_one(token_class: c) }) +} + +fn dbl_fixed_one(token_class: Symbol) -> ConcreteSyntaxToken { FixedToken { token_class: token_class } } + +fn dbl_wrapped(open: List, inner: List, close: List) -> List { + list_append(left: list_append(left: open, right: inner), right: close) } -fn dbl_reparses_to_two_nested_lets(concrete: List) -> Bool { +fn dbl_parses_to_one_let(concrete: List) -> Bool { match dbl_parse(concrete: concrete) { - Present { value: tree } => dbl_count_lets(root: tree) == 2 && dbl_has_nested_let(root: tree) + Present { value: tree } => dbl_count_lets(root: tree) == 1 Absent => false } } @@ -146,25 +155,78 @@ fn dbl_body_round_trips(body: List, lets: Int) -> Bool { } } +// THE FIVE PARSE VERDICTS, ONE PARSE EACH. Nullary and pure, enrolled WARM in +// v2.workflow.floor_pure_producer_share: each emitted token sequence is parsed once at preparation and +// every claim reads its stored Bool, so no claim pays a parse. +type DblVerdicts { + bare_body: Bool + empty_literal_body: Bool + minus_body: Bool + in_value_group: Bool + as_body_statement: Bool +} + +fn dbl_verdicts() -> DblVerdicts { + DblVerdicts { + bare_body: dbl_body_round_trips(body: dbl_token(binding: ^dag_binding_bind_x), lets: 1), + empty_literal_body: dbl_body_round_trips(body: dbl_fixed(classes: [^dag_token_lbrace, ^dag_token_rbrace]), lets: 1), + minus_body: dbl_body_round_trips(body: list_append(left: dbl_fixed(classes: [^dag_token_minus]), right: dbl_token(binding: ^dag_binding_bind_x)), lets: 1), + in_value_group: dbl_parses_to_one_let(concrete: dbl_wrapped(open: dbl_fixed(classes: [^dag_token_lparen]), inner: dbl_inner(), close: dbl_fixed(classes: [^dag_token_rparen]))), + as_body_statement: dbl_parses_to_one_let(concrete: dbl_wrapped(open: dbl_fixed(classes: [^dag_token_lbrace]), inner: dbl_inner(), close: dbl_fixed(classes: [^dag_token_rbrace]))) + } +} + test fn a_bare_identifier_body_round_trips() -> Bool { - dbl_body_round_trips(body: dbl_token(binding: ^dag_binding_bind_x), lets: 1) + dbl_verdicts().bare_body } test fn an_empty_brace_literal_body_round_trips() -> Bool { - dbl_body_round_trips(body: [FixedToken { token_class: ^dag_token_lbrace }, FixedToken { token_class: ^dag_token_rbrace }], lets: 1) + dbl_verdicts().empty_literal_body } test fn a_body_starting_with_minus_round_trips() -> Bool { - dbl_body_round_trips(body: list_append(left: [FixedToken { token_class: ^dag_token_minus }], right: dbl_token(binding: ^dag_binding_bind_x)), lets: 1) + dbl_verdicts().minus_body +} + +test fn a_bind_as_the_value_is_placed_verbatim_in_the_value_group() -> Bool { + let nested = dbl_bind(value: dbl_inner()) + !dbl_has_in(concrete: nested) + && nested == dbl_wrapped( + open: list_append( + left: dbl_fixed(classes: [^dag_token_lbrace, ^dag_token_kw_let]), + right: list_append(left: dbl_token(binding: ^dag_binding_bind_x), right: dbl_fixed(classes: [^dag_token_eq, ^dag_token_lparen])) + ), + inner: dbl_inner(), + close: list_append( + left: dbl_fixed(classes: [^dag_token_rparen, ^dag_token_lbrace]), + right: list_append(left: dbl_token(binding: ^dag_binding_bind_x), right: dbl_fixed(classes: [^dag_token_rbrace, ^dag_token_rbrace])) + ) + ) +} + +test fn a_bind_as_the_body_is_placed_verbatim_in_the_body_block() -> Bool { + dbl_bind_body(value: dbl_token(binding: ^dag_binding_pick_lit_one), body: dbl_inner()) == dbl_wrapped( + open: list_append( + left: dbl_fixed(classes: [^dag_token_lbrace, ^dag_token_kw_let]), + right: list_append( + left: dbl_token(binding: ^dag_binding_bind_x), + right: list_append( + left: dbl_fixed(classes: [^dag_token_eq, ^dag_token_lparen]), + right: list_append(left: dbl_token(binding: ^dag_binding_pick_lit_one), right: dbl_fixed(classes: [^dag_token_rparen, ^dag_token_lbrace])) + ) + ) + ), + inner: dbl_inner(), + close: dbl_fixed(classes: [^dag_token_rbrace, ^dag_token_rbrace]) + ) } -test fn a_bind_body_round_trips_nested() -> Bool { - dbl_body_round_trips(body: dbl_bind(value: dbl_token(binding: ^dag_binding_pick_lit_one)), lets: 2) +test fn a_bind_parses_inside_a_value_group() -> Bool { + dbl_verdicts().in_value_group } -test fn nested_bind_emitted_block_scoped_reparses_to_the_same_binds() -> Bool { - let concrete = dbl_bind(value: dbl_bind(value: dbl_token(binding: ^dag_binding_pick_lit_one))) - !dbl_has_in(concrete: concrete) && dbl_reparses_to_two_nested_lets(concrete: concrete) +test fn a_bind_parses_as_a_body_block_statement() -> Bool { + dbl_verdicts().as_body_statement } // The token sequence the dag target writes for one Bind, exactly: `{ let k = ( v ) { b } }`. The claims diff --git a/src/v2/workflow/floor_pure_producer_share.dag b/src/v2/workflow/floor_pure_producer_share.dag index 58bae12f992..50cb77cd67d 100644 --- a/src/v2/workflow/floor_pure_producer_share.dag +++ b/src/v2/workflow/floor_pure_producer_share.dag @@ -634,6 +634,10 @@ import v2.std.collection { List } // THE XL-2 LET-IN CAST ROW: v2.test.claim.body_cast_node bcn_let_in_value_cast_verdict assembles one // inline module through the production route and stores one Bool (the lowered body carries exactly // one cast node with its target), portable because it holds no Node and no closure. +// THE dag BIND BLOCK-SCOPED ROW: v2.test.emit.dag_bind_let_block_scoped dbl_verdicts parses five emitted +// token sequences once each and stores five Bool verdicts; each claim that paid its own parse measured +// over the new-witness budget on the floor runs of #13099 (eval steps 72-105k). Portable because it +// holds only Bools. // THE XL-2 IF-ARM AND STATEMENT-SPINE ROW IS THE SAME GROUND AT THIRTEEN SPECIMENS: // v2.test.claim.namespace_xl0.if_arm_and_statement_lowering_refusal iasl_outcomes drives one front // end over thirteen inline modules and stores one verdict arm per module, portable for the same reason. @@ -885,6 +889,7 @@ data floor_cross_claim_pure_producers_warm: List = [ "v2.test.claim.namespace_xl0.call_argument_value_resolve_refusal.cav_outcomes", "v2.test.claim.normalize.authored_marker_spelling.ams_verdicts", "v2.test.claim.body_lowering.caret_symbol_value_lowering.csv_verdicts", + "v2.test.emit.dag_bind_let_block_scoped.dbl_verdicts", "v2.test.parse.type_decl_modifier_g0_parse_probe.caret_tree_atom_identities", "v2.test.claim.body_lowering.string_literal_value_lowering.slv_verdicts", "v2.test.claim.body_cast_node.bcn_let_in_value_cast_verdict",