diff --git a/dag/gunbc/recurring_failure_mode/round_trip_claim_passes_on_emitted_text_reread_as_another_construct.dag b/dag/gunbc/recurring_failure_mode/round_trip_claim_passes_on_emitted_text_reread_as_another_construct.dag new file mode 100644 index 00000000000..f4302823e0d --- /dev/null +++ b/dag/gunbc/recurring_failure_mode/round_trip_claim_passes_on_emitted_text_reread_as_another_construct.dag @@ -0,0 +1,25 @@ +module gunbc.recurring_failure_mode.round_trip_claim_passes_on_emitted_text_reread_as_another_construct + +import std.types { NonEmptyStr } +import std.decl_ref { DeclarationRef, WholeDeclaration } +import gunbc.recurring_failure_mode { RecurringFailureMode } + +data round_trip_claim_passes_on_emitted_text_reread_as_another_construct: RecurringFailureMode = RecurringFailureMode { + identity: "round_trip_claim_passes_on_emitted_text_reread_as_another_construct" as NonEmptyStr, + + receipts: [ + "**a round-trip claim passes because malformed emitted text is re-read as a DIFFERENT valid construct** (INVALID STATE: an emit -> text -> ingest claim whose assertion is satisfied by a tree the emitter did not write.) The emitted text is wrong, the reader ACCEPTS it as something else, and the claim asks only a property both trees have: that the text parses, that a count is at least one, that no refusal fired. HARM: the claim is green, its assertion is true, and it establishes nothing about the round trip (DESIGN 3: the designed fixture reaching the same verdict through a different mechanism). Every later claim built on the same renderer inherits the pass.", + "RECEIPT, found by eager-crab-610 building gunbc#13099. The dag target declared no separation between tokens: its lex is `v2.extdeps.languages.dag` `dag_lex` and `dag_target_model` carried `token_class_emit_transforms` empty, and the flat token fold `v2.std.compilers.target_model` `bound_tokens_source_text` never read that map at all. A Bind rendered with `let` and `x` run together as `letx=(a)` inside its braces; `letx` lexes as one identifier, and the text was read as a bare assignment. A text-based version of that PR's Bind claims passed on it. EXECUTED on main a0a5c62161 (swift-lark-785, a scratch probe run by `gunbc run --function`, not landed): the six tokens `if true then 1 else x` render as `iftruethen1elsex`, which the dag grammar's `expr` production ACCEPTS as one identifier with no conditional in it; spaced, the same tokens read as one `if_expr`. EXECUTED on this change's tree: the unseparated nested Bind (each `let x` written `letx`) parses to TWO nested `let_expr` nodes, the same count the separated text gives, because `letx = (..)` reads as a bare-assignment binding. A claim counting lets cannot tell the two texts apart; the first draft of this change's own red asserted that count and was wrong.", + "DISTINGUISHING FACTS. (1) The reader is total enough to accept the damage: whitespace is the only thing separating a keyword from a name, so its loss yields a valid token, not a lex error. (2) The claim's oracle is weaker than identity: it inspects a property of the re-read tree rather than joining it to what was emitted. (3) The red is authorable and cheap: render the same tokens through the suspect renderer and compare the TOKEN CLASS SEQUENCE read back to the sequence emitted. That join needs no parse and fails on any merge or split of tokens.", + "RECOGNITION RULE. A round-trip claim must join what was read back to what was emitted at identity grain (the token class sequence, then the production stamps of the tree), never only ask that the text parses. A claim that would still pass if the emitted text were replaced by ANY valid expression is not a round-trip claim. Where the emitter's product is a token sequence, parsing those tokens directly (as `v2.test.emit.dag_bind_let_block_scoped` does) is a sound claim about the EMITTER and is silent about the TEXT; the text owes its own claim.", + "RUNG FOUND AT: silent wrongness on the text path (outside the ladder, DESIGN 4b): malformed text was Accepted as another construct. NOW: mechanically preventable. The dag target's separation is declared as rows on its token classes (`dag_token_class_emit_transforms`, one row per class the lex rule set declares) and both text folds read them; `v2.test.emit.dag_target_text_round_trip` holds the join and keeps the red enrolled (`mixed_expression_text_without_separation_is_one_identifier`, `nested_bind_text_without_separation_reads_back_as_other_tokens`). The state stays writable: a target may still declare no rows. CEILING: structurally guaranteed, because whether two adjacent spellings lex back as the two classes emitted is decidable from the lex rule set. NEXT-RUNG TRIGGER, NAMING THE CAPABILITY: the serializer derives or checks separation from the target's own lex rules for every adjacent pair it writes and refuses, located, a pair that would not lex back as itself, for every target rather than by rows authored per target. Sufficient for: no Accepted emission whose text lexes to a different token sequence.", + ], + + evidence: [ + DeclarationRef { module_path: "v2.extdeps.languages.dag", decl_name: "dag_token_class_emit_transforms", field: WholeDeclaration }, + DeclarationRef { module_path: "v2.std.compilers.target_model", decl_name: "bound_tokens_source_text_with_transforms", field: WholeDeclaration }, + DeclarationRef { module_path: "v2.test.emit.dag_target_text_round_trip", decl_name: "mixed_expression_text_without_separation_is_one_identifier", field: WholeDeclaration }, + DeclarationRef { module_path: "v2.test.emit.dag_target_text_round_trip", decl_name: "trt_bind_text_round_trips", field: WholeDeclaration }, + DeclarationRef { module_path: "v2.test.emit.dag_target_text_round_trip", decl_name: "the_dag_target_model_serializes_a_bind_with_its_tokens_separated", field: WholeDeclaration }, + ], +} diff --git a/src/v2/compiler/target_serialize.dag b/src/v2/compiler/target_serialize.dag index 6a9f35a85e6..9251ea85280 100644 --- a/src/v2/compiler/target_serialize.dag +++ b/src/v2/compiler/target_serialize.dag @@ -97,7 +97,7 @@ import v2.std.compilers.target_model { target_type_expr_emitted_kind, type_expression_projection_from_target, lex_rules_literal, - bound_tokens_source_text, + bound_tokens_source_text_with_transforms, TargetText, text_atom, target_text_seq, @@ -624,10 +624,11 @@ fn serialize_concrete_syntax_tokens_to_source_string( target: TargetModel, tokens: List ) -> Outcome { - bound_tokens_source_text( + bound_tokens_source_text_with_transforms( tokens: tokens, lex: target.lex, - binding_spellings: target.binding_spellings + binding_spellings: target.binding_spellings, + transforms: target.token_class_emit_transforms ) } diff --git a/src/v2/extdeps/languages/dag.dag b/src/v2/extdeps/languages/dag.dag index 75ae87c566c..86d3894182b 100644 --- a/src/v2/extdeps/languages/dag.dag +++ b/src/v2/extdeps/languages/dag.dag @@ -97,6 +97,8 @@ import v2.std.compilers.lexing { TriviaRule, WhitespaceChar, lex_rule_set_insert_token_classes, + lex_rule_set_matching_rules, + lex_rule_token_class_optional, lex_rule_set_token_class_map, lex_rule_set_keyword_class_member, lex_rule_set_token_class_member, @@ -179,7 +181,7 @@ import v2.std.compilers.target_model { TargetValueExpressionProjection, grammar_relation_row_attach_bodied_scaffold, target_operator_realizations_catalog_node, - value_expr_projection_bundle_node, target_model_emit_transforms_empty, + value_expr_projection_bundle_node, EmitSpellingWrap, TokenClassEmitTransform, Prepend, BlockEvaluationMode, ValueProducing, @@ -681,6 +683,25 @@ fn dag_lex() -> LexRules { ModeledLexRules { root: dag_lex_rules() } } +// EVERY dag TOKEN CLASS IS WRITTEN WITH ONE SPACE AFTER IT. Whitespace is trivia in dag_lex_rules, so +// a space after a token cannot change the tree read back; its absence can. Two adjacent word tokens +// lex as one identifier ("let" "x" -> "letx"), and two adjacent punctuation tokens can spell a third +// (">" "=" -> ">=", "/" "/" opens an annotation), so no token class is exempt. The rows are derived +// from the lex rule set, the one authority for which token classes exist, in the shape the other +// targets declare their separation in (v2.extdeps.languages.verilog verilog_emit_layout_transforms). +fn dag_token_class_emit_transforms() -> Map { + fold_list( + xs: lex_rule_set_matching_rules(rules: dag_lex_rules()), + empty: empty_map(), + cons: fn(acc, rule) { + match lex_rule_token_class_optional(rule: rule) { + Present { value: c } => map_insert(m: acc, key: c, value: EmitSpellingWrap { prefix: "", suffix: " " }) + Absent => acc + } + } + ) +} + fn dag_grammar_atom(id: Symbol) -> Node { Node { kind: TypeNode { @@ -3901,7 +3922,7 @@ fn dag_target_model_with_fidelity_quotient(quotient: Node) -> TargetModel { bundle: dag_target_model_bundle_with_fidelity_quotient(quotient: quotient), lex: dag_lex(), binding_spellings: dag_binding_spellings(), - token_class_emit_transforms: target_model_emit_transforms_empty, + token_class_emit_transforms: dag_token_class_emit_transforms(), authority_source_text: dag_source_text, runtime_row: target_emit_host_runtime_row_unconfigured } @@ -6005,7 +6026,7 @@ fn dag_bodied_fn_target_model( bundle: dag_bodied_fn_target_model_bundle_node(spec: spec), lex: dag_lex(), binding_spellings: dag_binding_spellings(), - token_class_emit_transforms: target_model_emit_transforms_empty, + token_class_emit_transforms: dag_token_class_emit_transforms(), authority_source_text: spec.authority_source_text, runtime_row: row } @@ -6015,7 +6036,7 @@ fn dag_bodied_fn_target_model( bundle: dag_bodied_fn_target_model_bundle_node(spec: spec), lex: dag_lex(), binding_spellings: dag_binding_spellings(), - token_class_emit_transforms: target_model_emit_transforms_empty, + token_class_emit_transforms: dag_token_class_emit_transforms(), authority_source_text: spec.authority_source_text, runtime_row: target_emit_host_runtime_row_unconfigured } @@ -6346,7 +6367,7 @@ fn dag_target_model() -> TargetModel { bundle: dag_target_model_node(), lex: dag_lex(), binding_spellings: dag_binding_spellings(), - token_class_emit_transforms: target_model_emit_transforms_empty, + token_class_emit_transforms: dag_token_class_emit_transforms(), authority_source_text: dag_source_text, runtime_row: target_emit_host_runtime_row_unconfigured } diff --git a/src/v2/extdeps/languages/rust_emit_small_fixtures.dag b/src/v2/extdeps/languages/rust_emit_small_fixtures.dag index f0c008a08d2..9321075f3ce 100644 --- a/src/v2/extdeps/languages/rust_emit_small_fixtures.dag +++ b/src/v2/extdeps/languages/rust_emit_small_fixtures.dag @@ -46,8 +46,8 @@ fn rust_emit_small_translation_claim() -> TranslationClaim { } } -// serialize_concrete_syntax_tokens_to_source_string reads only lex and -// binding_spellings. No bundle lookup, host execution or produced declaration +// serialize_concrete_syntax_tokens_to_source_string reads only lex, +// binding_spellings and token_class_emit_transforms. No bundle lookup, host execution or produced declaration // occurs on this path. fn rust_emit_small_serialization_target( lex: LexRules, diff --git a/src/v2/std/compilers/target_model.dag b/src/v2/std/compilers/target_model.dag index f91c8137d55..151ec709a4f 100644 --- a/src/v2/std/compilers/target_model.dag +++ b/src/v2/std/compilers/target_model.dag @@ -1371,10 +1371,16 @@ fn target_text_is_empty(t: TargetText) -> Bool { t.empty } -fn bound_tokens_source_text( +// THE FLAT TOKEN FOLD CONSULTS THE SAME EMIT-TRANSFORM MAP AS THE RELATION-ROW ROUTE. It read only +// the lexer and the binding spellings, so a target whose separation is declared on its token classes +// (token_class_emit_transforms) lost it on this route and its tokens ran together: the dag target +// wrote a Bind as "letx=ainx", one identifier. A transform is a fact about how a TOKEN CLASS +// renders, whichever fold spells the token, so both folds reach layout_or_atom_in. +fn bound_tokens_source_text_with_transforms( tokens: List, lex: LexRules, - binding_spellings: Map + binding_spellings: Map, + transforms: Map ) -> Outcome { fold_list( xs: tokens, @@ -1388,14 +1394,20 @@ fn bound_tokens_source_text( bind_outcome( o: lex_rules_literal_for_class(rules: lex, token_class: tc), f: fn(spelling) { - Accepted { value: target_text_seq(acc: partial, next: text_atom(lexeme: spelling)), diagnostics: ad } + bind_outcome( + o: layout_or_atom_in(transforms: transforms, token_class: tc, spelling: spelling), + f: fn(text) { Accepted { value: target_text_seq(acc: partial, next: text), diagnostics: ad } } + ) } ) - BoundToken { token_class: _, binding: b } => + BoundToken { token_class: tc, binding: b } => bind_outcome( o: bound_spelling_from_map(binding_spellings: binding_spellings, binding: b), f: fn(spelling) { - Accepted { value: target_text_seq(acc: partial, next: text_atom(lexeme: spelling)), diagnostics: ad } + bind_outcome( + o: layout_or_atom_in(transforms: transforms, token_class: tc, spelling: spelling), + f: fn(text) { Accepted { value: target_text_seq(acc: partial, next: text), diagnostics: ad } } + ) } ) } @@ -1404,6 +1416,19 @@ fn bound_tokens_source_text( ) } +fn bound_tokens_source_text( + tokens: List, + lex: LexRules, + binding_spellings: Map +) -> Outcome { + bound_tokens_source_text_with_transforms( + tokens: tokens, + lex: lex, + binding_spellings: binding_spellings, + transforms: target_model_emit_transforms_empty + ) +} + fn target_binding_spelling_lookup( target: TargetModel, binding: Symbol @@ -1524,8 +1549,8 @@ fn bound_token_spelling_from_model( ) } -fn layout_or_atom(target: TargetModel, token_class: Symbol, spelling: String) -> Outcome { - match map_get(target.token_class_emit_transforms, token_class) { +fn layout_or_atom_in(transforms: Map, token_class: Symbol, spelling: String) -> Outcome { + match map_get(transforms, token_class) { Accepted { value: Present { value: transform }, diagnostics: d } => match transform { EmitLineBreaks { before: b, after: a } => @@ -1542,6 +1567,10 @@ fn layout_or_atom(target: TargetModel, token_class: Symbol, spelling: String) -> } } +fn layout_or_atom(target: TargetModel, token_class: Symbol, spelling: String) -> Outcome { + layout_or_atom_in(transforms: target.token_class_emit_transforms, token_class: token_class, spelling: spelling) +} + // THE CARRIER-NATIVE TOKEN SPELLING: the lexeme (fixed: the lex literal; bound: the binding's // spelling) under the token class's emit transform, as TargetText, so an EmitLineBreaks class keeps // its line breaks. It takes the token already decoded: the serializer decodes each token node once to diff --git a/src/v2/test/claim/emit/dag_target_text_round_trip_test.dag b/src/v2/test/claim/emit/dag_target_text_round_trip_test.dag new file mode 100644 index 00000000000..df3c6de4f7f --- /dev/null +++ b/src/v2/test/claim/emit/dag_target_text_round_trip_test.dag @@ -0,0 +1,298 @@ +module v2.test.emit.dag_target_text_round_trip + +import v2.compiler.parse { PreparedModeled, PreparedVoidGrammar, parse_production_prepared } +import v2.compiler.program_assembly { dag_prepared_grammar } +import v2.compiler.target_serialize { serialize_concrete_syntax_tokens_to_source_string } +import v2.compiler.tokenize { tokenize } +import v2.extdeps.languages.dag { + dag_lex, + dag_target_model, + dag_token_class_emit_transforms, + dag_value_expression_projection, + parse_production_emitted_identity_optional +} +import v2.std.compilers.lexing { Token } +import v2.std.compilers.target_model { + BoundToken, + FixedToken, + ConcreteSyntaxToken, + TokenClassEmitTransform, + bind_let_value_producing_tokens, + bound_tokens_source_text_with_transforms, + render_target_text, + target_model_emit_transforms_empty +} +import std.algebra { list_append } +import v2.std.algebra { list_map } +import v2.std.collection { Map, empty_map, map_insert } +import v2.std.diagnostic { Accepted, Rejected } +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 TEXT THE dag TARGET WRITES IS TEXT THE dag GRAMMAR READS BACK AS THE SAME TREE. The dag target +// declared no separation between tokens, so a Bind rendered as "{letx=(a){x}}" and a conditional as +// "iftruethen1elsex": the first reads back with no binding in it and the second as one identifier, +// both ACCEPTED. Each claim here renders an emitted token sequence to text, lexes that text with the +// dag lex rules and (where a tree is owed) parses it once at the `expr` production. The inputs are +// supplied at the rendering interface (the lex rules, the spellings, the transform rows); the last +// claim is the inhabitance one, on the real route with the dag target model. +fn trt_ident(binding: Symbol) -> List { + [BoundToken { token_class: ^dag_token_ident, binding: binding }] +} + +fn trt_spellings() -> Map { + map_insert( + m: map_insert(m: map_insert(m: empty_map(), key: ^dag_binding_bind_x, value: "x"), key: ^dag_binding_pick_lit_one, value: "a"), + key: ^trt_binding_one, + value: "1" + ) +} + +fn trt_bind(value: List) -> List { + bind_let_value_producing_tokens( + projection: dag_value_expression_projection(), + key_tokens: trt_ident(binding: ^dag_binding_bind_x), + value_tokens: value, + body_tokens: trt_ident(binding: ^dag_binding_bind_x) + ) +} + +// A Bind as the VALUE of a Bind, from the real emitter. +fn trt_nested_bind() -> List { + trt_bind(value: trt_bind(value: trt_ident(binding: ^dag_binding_pick_lit_one))) +} + +// `if true then 1 else x`: keywords, a literal and an identifier, every one adjacent to another word. +fn trt_mixed() -> List { + [ + FixedToken { token_class: ^dag_token_kw_if }, + FixedToken { token_class: ^dag_token_kw_true }, + FixedToken { token_class: ^dag_token_kw_then }, + BoundToken { token_class: ^dag_token_int_literal, binding: ^trt_binding_one }, + FixedToken { token_class: ^dag_token_kw_else }, + BoundToken { token_class: ^dag_token_ident, binding: ^dag_binding_bind_x } + ] +} + +fn trt_text(tokens: List, transforms: Map) -> String { + match bound_tokens_source_text_with_transforms( + tokens: tokens, + lex: dag_lex(), + binding_spellings: trt_spellings(), + transforms: transforms + ) { + Accepted { value: t, diagnostics: _ } => render_target_text(t: t) + Rejected { diagnostics: _ } => "" + } +} + +fn trt_lex(text: String) -> List { + match tokenize(text: text, file: ^trt_probe, rules: dag_lex()) { + Accepted { value: stream, diagnostics: _ } => stream.all + Rejected { diagnostics: _ } => [] + } +} + +fn trt_emitted_classes(tokens: List) -> List { + list_map(xs: tokens, f: fn(t) { + match t { + FixedToken { token_class: c } => c + BoundToken { token_class: c, binding: _ } => c + } + }) +} + +// The token classes the text lexes to, in order: the emitted sequence, or it was not round-tripped. +fn trt_read_classes(text: String) -> List { + trt_token_classes(tokens: trt_lex(text: text)) +} + +fn trt_token_classes(tokens: List) -> List { + list_map(xs: tokens, f: fn(t) { t.class }) +} + +fn trt_parse(tokens: List) -> Optional { + match dag_prepared_grammar() { + Rejected { diagnostics: _ } => Absent + Accepted { value: prepared, diagnostics: _ } => + match prepared { + PreparedVoidGrammar => Absent + PreparedModeled { modeled: modeled, materialization: m } => + match parse_production_prepared( + tokens: tokens, + validated: modeled.validated, + analysis: modeled.analysis, + production_name: ^dag_production_expr, + materialization: m + ) { + Rejected { diagnostics: _ } => Absent + Accepted { value: artifact, diagnostics: _ } => trt_present(node: artifact.tree) + } + } + } +} + +fn trt_present(node: Node) -> Optional { Present { value: node } } + +fn trt_is(node: Node, production: Symbol) -> Bool { + match parse_production_emitted_identity_optional(node: node) { + Present { value: id } => id == production + Absent => false + } +} + +fn trt_count(root: Node, production: Symbol) -> Int { + let here = if trt_is(node: root, production: production) { 1 } else { 0 } + fold(root.children, init: here, f: fn(acc, e) { acc + trt_count(root: e.target, production: production) }) +} + +fn trt_count_below(root: Node, production: Symbol) -> Int { + fold(root.children, init: 0, f: fn(acc, e) { acc + trt_count(root: e.target, production: production) }) +} + +// A let with exactly one let under it. +fn trt_has_nested_let(root: Node) -> Bool { + if trt_is(node: root, production: ^dag_surface_let_expr) && trt_count_below(root: root, production: ^dag_surface_let_expr) == 1 { + true + } else { + fold(root.children, init: false, f: fn(found, e) { found || trt_has_nested_let(root: e.target) }) + } +} + +fn trt_fixed(classes: List) -> List { + list_map(xs: classes, f: fn(c) { trt_fixed_one(token_class: c) }) +} + +fn trt_fixed_one(token_class: Symbol) -> ConcreteSyntaxToken { FixedToken { token_class: token_class } } + +// One Bind `{ let x = (a) { body } }` from the real emitter, with the given body. +fn trt_bind_with_body(body: List) -> List { + bind_let_value_producing_tokens( + projection: dag_value_expression_projection(), + key_tokens: trt_ident(binding: ^dag_binding_bind_x), + value_tokens: trt_ident(binding: ^dag_binding_pick_lit_one), + body_tokens: body + ) +} + +// THE TEXT-GRAIN ROUND TRIP OF ONE EMITTED TOKEN SEQUENCE: rendered with the dag target's rows, the +// text lexes back to the emitted token classes in order (the join: any merge or split of tokens +// fails here), and those lexed tokens parse at `expr` to ONE tree holding exactly `lets` bindings. +// `let_under_let` is the tree's shape: a Bind in the VALUE group sits under the outer let node, a +// Bind in the BODY block does not (the block follows the let as its own statement). The let count is +// asked only AFTER the join, never instead of it: the unseparated text has the same count. +fn trt_bind_text_round_trips(tokens: List, lets: Int, let_under_let: Bool) -> Bool { + let read = trt_lex(text: trt_text(tokens: tokens, transforms: dag_token_class_emit_transforms())) + trt_token_classes(tokens: read) == trt_emitted_classes(tokens: tokens) + && match trt_parse(tokens: read) { + Present { value: tree } => + trt_count(root: tree, production: ^dag_surface_let_expr) == lets && trt_has_nested_let(root: tree) == let_under_let + Absent => false + } +} + +fn trt_mixed_text_round_trips() -> Bool { + let read = trt_lex(text: trt_text(tokens: trt_mixed(), transforms: dag_token_class_emit_transforms())) + trt_token_classes(tokens: read) == trt_emitted_classes(tokens: trt_mixed()) + && match trt_parse(tokens: read) { + Present { value: tree } => trt_count(root: tree, production: ^dag_surface_if_expr) == 1 + Absent => false + } +} + +// THE SIX TEXT ROUND TRIPS, ONE RENDER, ONE LEX AND ONE PARSE EACH. Nullary and pure, enrolled WARM +// in v2.workflow.floor_pure_producer_share: one expression parse is at or past a new witness's +// eval-step budget (this PR's first floor run: 67k for the conditional, 122k for the nested Bind, +// against 72.3k), so each text is round-tripped once at preparation and every claim reads its Bool. +type TrtVerdicts { + bare_body: Bool + empty_literal_body: Bool + minus_body: Bool + bind_body: Bool + bind_value: Bool + mixed: Bool +} + +fn trt_verdicts() -> TrtVerdicts { + TrtVerdicts { + bare_body: trt_bind_text_round_trips(tokens: trt_bind_with_body(body: trt_ident(binding: ^dag_binding_bind_x)), lets: 1, let_under_let: false), + empty_literal_body: trt_bind_text_round_trips(tokens: trt_bind_with_body(body: trt_fixed(classes: [^dag_token_lbrace, ^dag_token_rbrace])), lets: 1, let_under_let: false), + minus_body: trt_bind_text_round_trips( + tokens: trt_bind_with_body(body: list_append(left: trt_fixed(classes: [^dag_token_minus]), right: trt_ident(binding: ^dag_binding_bind_x))), + lets: 1, + let_under_let: false + ), + bind_body: trt_bind_text_round_trips(tokens: trt_bind_with_body(body: trt_bind(value: trt_ident(binding: ^dag_binding_pick_lit_one))), lets: 2, let_under_let: false), + bind_value: trt_bind_text_round_trips(tokens: trt_nested_bind(), lets: 2, let_under_let: true), + mixed: trt_mixed_text_round_trips() + } +} + +// THE BLOCK-SCOPED BIND `{ let k = (v) { b } }`, AT TEXT GRAIN, for each body the emitter may be +// handed: a bare name, an empty brace literal, a `-`-led expression, and a Bind. +test fn a_bind_with_a_bare_name_body_round_trips_as_text() -> Bool { + trt_verdicts().bare_body +} + +test fn a_bind_with_an_empty_brace_literal_body_round_trips_as_text() -> Bool { + trt_verdicts().empty_literal_body +} + +test fn a_bind_with_a_minus_led_body_round_trips_as_text() -> Bool { + trt_verdicts().minus_body +} + +test fn a_bind_with_a_bind_body_round_trips_as_text() -> Bool { + trt_verdicts().bind_body +} + +test fn a_bind_with_a_bind_value_round_trips_as_text() -> Bool { + trt_verdicts().bind_value +} + +// THE RED, KEPT: the same tokens with no transform rows are the rendering the dag target had, and +// they do not read back as the tokens emitted (`let` `x` is the one identifier `letx`). That text +// still PARSES, and to two nested lets (`letx = (..)` reads as a bare-assignment binding), so a +// claim that counted lets passed on it; the token join is what refuses it. +test fn nested_bind_text_without_separation_reads_back_as_other_tokens() -> Bool { + trt_read_classes(text: trt_text(tokens: trt_nested_bind(), transforms: target_model_emit_transforms_empty)) + != trt_emitted_classes(tokens: trt_nested_bind()) +} + +test fn mixed_expression_text_round_trips() -> Bool { + trt_verdicts().mixed +} + +// THE CLASS, at its cheapest specimen: unseparated, the six tokens are ONE identifier, which is a +// valid expression. A claim that only asked "does the emitted text parse" passes on it. +test fn mixed_expression_text_without_separation_is_one_identifier() -> Bool { + trt_read_classes(text: trt_text(tokens: trt_mixed(), transforms: target_model_emit_transforms_empty)) == [^dag_token_ident] +} + +// Punctuation is not exempt: `>` then `=` unseparated is the one token `>=`. +test fn adjacent_punctuation_reads_back_as_two_tokens() -> Bool { + let pair = [FixedToken { token_class: ^dag_token_gt }, FixedToken { token_class: ^dag_token_eq }] + trt_read_classes(text: trt_text(tokens: pair, transforms: dag_token_class_emit_transforms())) == [^dag_token_gt, ^dag_token_eq] + && trt_read_classes(text: trt_text(tokens: pair, transforms: target_model_emit_transforms_empty)) == [^dag_token_gte] +} + +// INHABITANCE, ON THE REAL ROUTE: the dag target model carries the rows, and the serializer the +// emitter calls (v2.compiler.target_serialize) reads them. Dropping the rows from dag_target_model, +// or the map from that serializer, runs the tokens together and fails this. The value is the name +// `x`: the model spells its other bindings as digits, which lex as literals, not as the identifier +// class these tokens carry. +fn trt_model_bind() -> List { + trt_bind(value: trt_ident(binding: ^dag_binding_bind_x)) +} + +test fn the_dag_target_model_serializes_a_bind_with_its_tokens_separated() -> Bool { + match serialize_concrete_syntax_tokens_to_source_string(target: dag_target_model(), tokens: trt_model_bind()) { + Accepted { value: t, diagnostics: _ } => + trt_read_classes(text: render_target_text(t: t)) == trt_emitted_classes(tokens: trt_model_bind()) + Rejected { diagnostics: _ } => false + } +} diff --git a/src/v2/test/claim/emit/target_text_layout_test.dag b/src/v2/test/claim/emit/target_text_layout_test.dag index 8afa801430b..b848362803a 100644 --- a/src/v2/test/claim/emit/target_text_layout_test.dag +++ b/src/v2/test/claim/emit/target_text_layout_test.dag @@ -7,6 +7,7 @@ import v2.std.grammar { Holds, Violates } import v2.std.compilers.target_model { TargetModel, TargetText, + FixedToken, target_text_line_breaks, text_atom, target_text_seq, @@ -16,7 +17,7 @@ import v2.std.compilers.target_model { render_target_text, fixed_token_spelling_from_model } -import v2.compiler.target_serialize { target_serialize_relation_row_from_model_bounded } +import v2.compiler.target_serialize { serialize_concrete_syntax_tokens_to_source_string, target_serialize_relation_row_from_model_bounded } import v2.extdeps.languages.verilog { verilog_interlock_emitted, verilog_relation_row_for, @@ -73,6 +74,29 @@ test fn a_layout_token_class_refuses_the_flat_spelling() -> Bool { } } +// THE FLAT TOKEN ROUTE SPELLS A TOKEN CLASS AS THE RELATION-ROW ROUTE DOES. The flat fold +// (v2.compiler.target_serialize serialize_concrete_syntax_tokens_to_source_string) read no +// transform rows, so the same class rendered two ways depending on which fold spelled it. Here the +// consuming target's own rows apply: `assign` keeps its trailing space, `=` its two, and `;` its +// line break instead of refusing or dropping it. +test fn the_flat_token_route_applies_the_targets_transform_rows() -> Bool { + match verilog_relation_row_for(lhs: ^verilog_production_ansi_module_decl, emitted: verilog_interlock_emitted()) { + Holds { value: row } => + match serialize_concrete_syntax_tokens_to_source_string( + target: verilog_target_model_with_single_row(row: row), + tokens: [ + FixedToken { token_class: ^verilog_token_kw_assign }, + FixedToken { token_class: ^verilog_token_equals }, + FixedToken { token_class: ^verilog_token_semicolon } + ] + ) { + Accepted { value: t, diagnostics: _ } => render_target_text(t: t) == "assign = ;\n" + Rejected { diagnostics: _ } => false + } + Violates { diagnostic: _ } => false + } +} + // A nested occurrence whose unit the target does not spell refuses rather than indenting by the // symbol's own name; the same module with the unit spelled emits. test fn an_unspelled_nest_unit_refuses_and_a_spelled_one_emits() -> Bool { diff --git a/src/v2/workflow/floor_pure_producer_share.dag b/src/v2/workflow/floor_pure_producer_share.dag index 298d2528144..65f8c290e4b 100644 --- a/src/v2/workflow/floor_pure_producer_share.dag +++ b/src/v2/workflow/floor_pure_producer_share.dag @@ -638,6 +638,10 @@ import v2.std.collection { List } // 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 dag TARGET TEXT ROUND-TRIP ROW: v2.test.emit.dag_target_text_round_trip trt_verdicts renders six +// emitted token sequences to text, lexes each and parses each once, and stores six Bool verdicts. The +// floor of #13113 measured one such claim at 67k and one at 122k eval steps when each paid its own +// parse. 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. @@ -902,6 +906,7 @@ data floor_cross_claim_pure_producers_warm: List = [ "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.emit.dag_target_text_round_trip.trt_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",