Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
18 changes: 14 additions & 4 deletions src/v2/extdeps/languages/dag.dag
Original file line number Diff line number Diff line change
Expand Up @@ -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 {
Expand All @@ -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)
)
)
)
)
}
Expand Down
86 changes: 86 additions & 0 deletions src/v2/test/claim/parse/bare_node_statement_route_test.dag
Original file line number Diff line number Diff line change
@@ -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<Node> {
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
}
4 changes: 4 additions & 0 deletions src/v2/workflow/floor_pure_producer_share.dag
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -914,6 +917,7 @@ data floor_cross_claim_pure_producers_warm: List<String> = [
"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",
Expand Down