diff --git a/src/v2/extdeps/languages/dag.dag b/src/v2/extdeps/languages/dag.dag index 24d62c1b2b1..ef46fc7c9b7 100644 --- a/src/v2/extdeps/languages/dag.dag +++ b/src/v2/extdeps/languages/dag.dag @@ -1219,9 +1219,13 @@ fn dag_grammar_stmt_seq_expr() -> GrammarExpr { dag_grammar_repeat(element: dag_grammar_nonterminal(production: ^dag_production_stmt)) } -// 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 +// AN EXPRESSION STATEMENT NEVER BEGINS WITH A LET SPELLING. `name =` and `node name :` / `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 node head is all three tokens: +// a bare `node` statement followed on the next line by a statement that begins with a name (the +// next match arm, an `if`) begins `node name` too, and it is an expression; a two-token guard +// refused it while the sugar, lacking its `:` / `=`, refused it as well. So the guard is read at +// depth three: 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 { @@ -1232,7 +1236,13 @@ fn dag_grammar_let_sugar_head_expr() -> GrammarExpr { ), 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() + right: dag_grammar_sequence( + left: dag_grammar_binding_name_terminal(), + right: dag_grammar_choice( + left: dag_grammar_terminal(token_class: ^dag_token_colon), + right: dag_grammar_terminal(token_class: ^dag_token_eq) + ) + ) ) ) } diff --git a/src/v2/test/claim/parse/bare_node_statement_route_test.dag b/src/v2/test/claim/parse/bare_node_statement_route_test.dag new file mode 100644 index 00000000000..59b41df596c --- /dev/null +++ b/src/v2/test/claim/parse/bare_node_statement_route_test.dag @@ -0,0 +1,86 @@ +module v2.test.parse.bare_node_statement_route + +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, 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, Present } + +data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly + +// A BARE `node` STATEMENT IS AN EXPRESSION, EVEN WHEN THE NEXT LINE BEGINS WITH A NAME +// (v2.extdeps.languages.dag dag_grammar_let_sugar_head_expr). The node let-sugar head is +// `node name :` / `node name =`; a two-token guard `node name` also excluded a bare `node` value +// followed by the next match arm or an `if`, and five corpus files refused (among them +// src/v2/std/node.dag). The shapes are the regression's own: an arm `=> node` before the next arm, +// and `node` before an `if`. Each takes the expression route (no let_expr); the sugar `node y = 1` +// still takes the let route (one let_expr). The first two sources are the regression's fixtures +// verbatim (a1, a3). Each claim pays ONE parse of the smallest module that +// reaches its route. +data bns_arm_source: String = "module a1\ntype O = S { node: Int } | L { x: Int }\nfn f(o: O) -> Int {\n match o {\n S { node: node } => node\n L { x: x } => x\n }\n}\n" +data bns_if_source: String = "module a3\nfn f(node: Int, c: Bool) -> Int {\n node\n if c {\n 1\n } else {\n 0\n }\n}\n" +data bns_sugar_source: String = "module p\nfn f() -> I {\n node y = 1\n y\n}\n" + +fn bns_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 bns_lets(root: Node) -> Int { + let here = match parse_production_emitted_identity_optional(node: root) { + Present { value: id } => if id == ^dag_surface_let_expr { 1 } else { 0 } + Absent => 0 + } + fold(root.children, init: here, f: fn(acc, e) { acc + bns_lets(root: e.target) }) +} + +// Accepted, holding exactly `lets` let_expr nodes. +fn bns_route(text: String, file: Symbol, lets: Int) -> Bool { + match bns_parse(text: text, file: file) { + Accepted { value: tree, diagnostics: _ } => bns_lets(root: tree) == lets + Rejected { diagnostics: _ } => false + } +} + +// THE THREE ROUTES, FROM ONE PARSE OF EACH SOURCE. Nullary and pure, enrolled WARM in +// v2.workflow.floor_pure_producer_share: each claim reads its stored Bool. +type BnsVerdicts { + arm_before_arm: Bool + node_before_if: Bool + sugar: Bool +} + +fn bns_verdicts() -> BnsVerdicts { + BnsVerdicts { + arm_before_arm: bns_route(text: bns_arm_source, file: ^bns_arm, lets: 0), + node_before_if: bns_route(text: bns_if_source, file: ^bns_if, lets: 0), + sugar: bns_route(text: bns_sugar_source, file: ^bns_sugar, lets: 1) + } +} + +test fn bare_node_arm_body_before_the_next_arm_takes_the_expression_route() -> Bool { + bns_verdicts().arm_before_arm +} + +test fn bare_node_statement_before_an_if_takes_the_expression_route() -> Bool { + bns_verdicts().node_before_if +} + +test fn node_let_sugar_still_takes_the_let_route() -> Bool { + bns_verdicts().sugar +} diff --git a/src/v2/workflow/floor_pure_producer_share.dag b/src/v2/workflow/floor_pure_producer_share.dag index e6ba567c078..2f49018b5cb 100644 --- a/src/v2/workflow/floor_pure_producer_share.dag +++ b/src/v2/workflow/floor_pure_producer_share.dag @@ -637,6 +637,9 @@ import v2.std.collection { List } // stores four. Each claim that paid its own parse measured at the new-witness budget's edge on the // floor runs of #13056 (eval steps 66-72k, enrolment margin refused on cpu). Portable because each // holds only Bools. +// THE BARE node STATEMENT ROW: v2.test.parse.bare_node_statement_route bns_verdicts parses three +// one-function modules once each and stores three Bool verdicts, on the same ground. Portable because it +// holds only Bools. // 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 @@ -914,6 +917,7 @@ data floor_cross_claim_pure_producers_warm: List = [ "v2.test.claim.body_lowering.caret_symbol_value_lowering.csv_verdicts", "v2.test.parse.else_less_if_value_category.elif_verdicts", "v2.test.parse.brace_and_lambda_head_route.bhr_verdicts", + "v2.test.parse.bare_node_statement_route.bns_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",