Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
26 commits
Select commit Hold shift + click to select a range
8afdb1e
WIP layout model: TokenStream source, named line-break derivation, Re…
Sep 30, 2026
8371ea0
Layout control: same tokens, different layout, different stream digests
Sep 30, 2026
ef567ab
Layout: derive a per-token line-break index once per stream; a layout…
Sep 30, 2026
22131ce
Layout identity control parses against the warmed dag_prepared_gramma…
Sep 30, 2026
24b7716
Layout identity control: a module that reaches no layout question (+,…
Sep 30, 2026
0f04f7f
Layout: keep only line-break-preceded starts; digest covers layout by…
Sep 30, 2026
dcc31bb
grammar: cite token_stream_line_break_before (stale symbol, review 73…
Sep 30, 2026
a30b62f
lexing: delete token_stream_source, no consumer after the layout rewo…
Sep 30, 2026
e4e899b
StreamLayout: drop the unread source field (the source is read once, …
Sep 30, 2026
39bbbd4
layout test: the digest covers layout, not source (comment)
Sep 30, 2026
66b9ff1
lexing: spell the tokenizer's source as v2.std.text.String (emit-buil…
Sep 30, 2026
f7888e6
StreamLayout: one representation, start -> line of each line-break-pr…
Sep 30, 2026
cf486fd
Merge remote-tracking branch 'origin/main' into session/calm-fox-43-l…
Oct 1, 2026
0cb9c37
v2 parse: refuse a line-break-preceded '-' at the additive continuati…
Oct 1, 2026
8e02e45
Mutation witness: every live refusal arm is the newline refusal (the …
Oct 1, 2026
26ad3f4
Layout digest folded once in the layout walk; the parse table reads i…
Oct 1, 2026
8990a2d
Merge branch 'session/calm-fox-43-layout-model' into session/calm-fox…
Oct 1, 2026
6094f43
lexing: type the layout digest as Fnv1a64Structural, what combine_has…
Oct 1, 2026
f6e4ebd
Merge branch 'session/calm-fox-43-layout-model' into session/calm-fox…
Oct 1, 2026
def354a
Layout recorded in the tokenizer's own walk (no second pass over the …
Oct 1, 2026
7a73163
lexing: lexeme_has_line_feed takes v2.std.text.String (emit)
Oct 1, 2026
7588a30
Merge branch 'session/calm-fox-43-layout-model' into session/calm-fox…
Oct 1, 2026
64b3751
Merge main (#12773 landed) into the newline refusal
Oct 1, 2026
06f42f2
Newline controls: one data declaration each, same-line control parse-…
Oct 1, 2026
f2fd299
Newline mutation: supply the mutant grammar and the arm census as war…
Oct 1, 2026
8958927
Newline claims: one parse per mutant claim; drop the live-grammar dup…
Oct 1, 2026
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
26 changes: 22 additions & 4 deletions src/v2/extdeps/languages/dag.dag
Original file line number Diff line number Diff line change
Expand Up @@ -20,7 +20,7 @@ import v2.std.optional {
optional_absent,
optional_present
}
import v2.std.parse_refusal_reason { DataValueMissingAfterEq, FnExpressionBodyMissingAfterEq, ParseRefusalReason }
import v2.std.parse_refusal_reason { DataValueMissingAfterEq, FnExpressionBodyMissingAfterEq, NewlineBeforeDualRoleOperator, ParseRefusalReason }
import v2.std.grammar {
grammar_formal_terminal,
grammar_formal_terminal_bound,
Expand Down Expand Up @@ -56,7 +56,9 @@ import v2.std.grammar {
grammar_production_to_node,
grammar_relation_tokens_node,
grammar_empty_sync_tokens,
grammar_expr_after_line_break,
grammar_expr_expect,
grammar_expr_refuse_on_match,
derive_grammar_relation_row,
derive_grammar_relation_row_node,
formal_production_for_lhs_exact,
Expand Down Expand Up @@ -1343,13 +1345,29 @@ fn dag_grammar_multiplicative_expr_helper() -> GrammarExpr {
)
}

// A `-` THAT BEGINS A LINE AFTER A COMPLETE OPERAND REFUSES. `-` is both infix (subtraction) and
// prefix (negation), and this grammar carries no statement terminator, so `x` then a line `-1` could
// be `x - 1` or two statements; neither reading is safe to pick silently. The seed refuses it
// (v1.compiler.parse is_ambiguous_prefix_infix_newline_boundary, whose dual-role set is exactly
// `-`), and so does this row: the refusal alternative is tried FIRST at every additive
// continuation, it matches only a `-` preceded by a line break (v2.std.grammar AfterLineBreak, read
// from the stream's layout), and where it matches the parse refuses at the `-` with
// NewlineBeforeDualRoleOperator. A same-line `-` falls through to subtraction. Every expression
// reaches this continuation, so the rule holds for every statement form -- including a block-headed
// statement, which is an operand since block forms are primaries of binary_expr (#12817).
fn dag_grammar_additive_expr_helper() -> GrammarExpr {
dag_grammar_sequence(
left: dag_grammar_multiplicative_expr_helper(),
right: dag_grammar_repeat(
element: dag_grammar_sequence(
left: dag_grammar_additive_op_choice(),
right: dag_grammar_multiplicative_expr_helper()
element: dag_grammar_choice(
left: grammar_expr_refuse_on_match(
element: grammar_expr_after_line_break(element: dag_grammar_terminal(token_class: ^dag_token_minus)),
reason: NewlineBeforeDualRoleOperator
),
right: dag_grammar_sequence(
left: dag_grammar_additive_op_choice(),
right: dag_grammar_multiplicative_expr_helper()
)
)
)
)
Expand Down
7 changes: 7 additions & 0 deletions src/v2/std/parse_refusal_reason.dag
Original file line number Diff line number Diff line change
Expand Up @@ -14,16 +14,23 @@ import v2.std.node { Symbol }
// AfterLineBreak) was reached on a token stream that carries no
// source, so whether a line break precedes the match has no
// answer; the parse refuses rather than assume one line.
// NewlineBeforeDualRoleOperator -- a `-` (both prefix and infix) begins a line after a complete
// operand. It could continue the expression or start a new one,
// so it refuses, as the seed does (v1.compiler.parse
// is_ambiguous_prefix_infix_newline_boundary): move the operator
// before the newline, or parenthesize the unary expression.
type ParseRefusalReason =
FnExpressionBodyMissingAfterEq
| DataValueMissingAfterEq
| LayoutUnknownWithoutSource
| NewlineBeforeDualRoleOperator

// The diagnostic identity each reason refuses under (`v2.std.diagnostic` `Diagnostic.reason`).
fn parse_refusal_reason_symbol(reason: ParseRefusalReason) -> Symbol {
match reason {
FnExpressionBodyMissingAfterEq => ^parse_fn_expression_body_missing_after_eq
DataValueMissingAfterEq => ^parse_data_value_missing_after_eq
LayoutUnknownWithoutSource => ^parse_layout_unknown_without_source
NewlineBeforeDualRoleOperator => ^parse_newline_before_dual_role_operator
}
}
198 changes: 198 additions & 0 deletions src/v2/test/claim/parse/newline_dual_role_operator_mutation_test.dag
Original file line number Diff line number Diff line change
@@ -0,0 +1,198 @@
module v2.test.parse.newline_dual_role_operator_mutation

import v2.compiler.parse { PreparedGrammar, parse_module_prepared, prepare_grammar }
import v2.std.diagnostic { Outcome }
import v2.compiler.tokenize { tokenize }
import v2.extdeps.languages.dag { dag_grammar, dag_lex }
import v2.std.algebra { fold_list }
import v2.std.grammar {
AfterLineBreak,
Choice,
Expect,
GrammarExpr,
GrammarExprFold,
GrammarProduction,
GrammarRoot,
LiteralTerminal,
ModeledGrammar,
Nonterminal,
Optional,
ParseGrammar,
RefuseOnMatch,
Repeat,
Sequence,
StampClass,
Terminal,
VoidGrammar,
fold_grammar_expr
}
import v2.std.diagnostic { Accepted, Rejected }
import v2.std.parse_refusal_reason {
DataValueMissingAfterEq,
FnExpressionBodyMissingAfterEq,
LayoutUnknownWithoutSource,
NewlineBeforeDualRoleOperator
}
import v2.std.integer { Int }
import v2.std.logic { Bool }
import v2.std.node { Symbol }
import v2.std.text { String }
import v2.test.parse.newline_dual_role_operator_parse {
newline_minus_after_block_source,
newline_minus_after_operand_source,
same_line_minus_source
}

// THE MUTATION THAT REDS THE NEWLINE-`-` REFUSAL (v2.test.parse.newline_dual_role_operator_parse).
// It rebuilds the live dag grammar with every RefuseOnMatch arm replaced by a terminal no token
// carries -- an alternative that can never match -- and asserts that such arms exist and that EVERY
// one of them is the newline refusal (NewlineBeforeDualRoleOperator), so the mutant differs from the
// live grammar in that refusal and nothing else. There is more than one arm because the additive row
// is a helper inlined into each operand position of the comparison and equality rows; it is one
// authored row. Under the mutant the
// next-line sources parse again (the silent merge into one subtraction is back); under the live
// grammar they refuse (the controls in v2.test.parse.newline_dual_role_operator_parse). The
// same-line form parses under both.
//
// THE GRAMMARS ARE SUPPLIED, NOT RE-PREPARED PER CLAIM (DESIGN section 3, a witness discriminates at
// one interface). The mutant is prepared once by the nullary producer nlm_mutant_prepared and the refusal-arm counts are taken once by
// nlm_refusal_arm_census, both enrolled WARM in v2.workflow.floor_pure_producer_share. Each claim pays
// one tokenize and one parse of a one-line declaration.

fn strip_refusals(expr: GrammarExpr) -> GrammarExpr {
fold_grammar_expr(
expr: expr,
algebra: GrammarExprFold {
terminal: fn(token_class, stamp) { Terminal { token_class: token_class, stamp: stamp } },
literal_terminal: fn(token_class, lexeme) { LiteralTerminal { token_class: token_class, lexeme: lexeme } },
nonterminal: fn(production) { Nonterminal { production: production } },
sequence: fn(l, r) { Sequence { left: l, right: r } },
choice: fn(l, r) { Choice { left: l, right: r } },
optional: fn(e) { Optional { element: e } },
repeat: fn(e) { Repeat { element: e } },
expect: fn(e, reason) { Expect { element: e, reason: reason } },
refuse_on_match: fn(_e, _reason) { Terminal { token_class: ^newline_mutation_no_token_carries_this_class, stamp: StampClass } },
after_line_break: fn(e) { AfterLineBreak { element: e } }
}
)
}

fn refusal_arm_count(expr: GrammarExpr) -> Int {
fold_grammar_expr(
expr: expr,
algebra: GrammarExprFold {
terminal: fn(_, _) { 0 },
literal_terminal: fn(_, _) { 0 },
nonterminal: fn(_) { 0 },
sequence: fn(l, r) { l + r },
choice: fn(l, r) { l + r },
optional: fn(e) { e },
repeat: fn(e) { e },
expect: fn(e, _reason) { e },
refuse_on_match: fn(e, _reason) { e + 1 },
after_line_break: fn(e) { e }
}
)
}

fn other_refusal_arm_count(expr: GrammarExpr) -> Int {
fold_grammar_expr(
expr: expr,
algebra: GrammarExprFold {
terminal: fn(_, _) { 0 },
literal_terminal: fn(_, _) { 0 },
nonterminal: fn(_) { 0 },
sequence: fn(l, r) { l + r },
choice: fn(l, r) { l + r },
optional: fn(e) { e },
repeat: fn(e) { e },
expect: fn(e, _reason) { e },
refuse_on_match: fn(e, reason) {
match reason {
NewlineBeforeDualRoleOperator => e
FnExpressionBodyMissingAfterEq => e + 1
DataValueMissingAfterEq => e + 1
LayoutUnknownWithoutSource => e + 1
}
},
after_line_break: fn(e) { e }
}
)
}

fn no_productions() -> List<GrammarProduction> {
[]
}

fn mutant_grammar() -> ParseGrammar {
match dag_grammar() {
ModeledGrammar { root: r } =>
ModeledGrammar {
root: GrammarRoot {
start: r.start,
productions: fold_list(xs: r.productions, empty: no_productions(), cons: fn(acc, prod) {
concat(acc, [GrammarProduction { name: prod.name, expression: strip_refusals(expr: prod.expression), emitted: prod.emitted }])
}),
sync_tokens: r.sync_tokens
}
}
VoidGrammar => VoidGrammar
}
}

type RefusalArmCensus {
total: Int
other: Int
}

// WARM PRODUCER: the refusal arms of the live dag grammar, counted once.
fn nlm_refusal_arm_census() -> RefusalArmCensus {
match dag_grammar() {
ModeledGrammar { root: r } =>
RefusalArmCensus {
total: fold_list(xs: r.productions, empty: 0, cons: fn(acc, prod) { acc + refusal_arm_count(expr: prod.expression) }),
other: fold_list(xs: r.productions, empty: 0, cons: fn(acc, prod) { acc + other_refusal_arm_count(expr: prod.expression) })
}
VoidGrammar => RefusalArmCensus { total: 0, other: 0 }
}
}

// WARM PRODUCER: the mutant grammar, prepared once.
fn nlm_mutant_prepared() -> Outcome<PreparedGrammar> {
prepare_grammar(grammar: mutant_grammar())
}

fn accepts_prepared(text: String, file: Symbol, prepared: Outcome<PreparedGrammar>) -> Bool {
match prepared {
Rejected { diagnostics: _ } => false
Accepted { value: p, diagnostics: residue } =>
match tokenize(text: text, file: file, rules: dag_lex()) {
Rejected { diagnostics: _ } => false
Accepted { value: stream, diagnostics: _ } =>
match parse_module_prepared(tokens: stream, prepared: p, validation_residue: residue) {
Accepted { value: _, diagnostics: _ } => true
Rejected { diagnostics: _ } => false
}
}
}
}

test fn witness_every_live_refusal_arm_is_the_newline_refusal() -> Bool {
let census = nlm_refusal_arm_census()
(census.total > 0) && (census.other == 0)
}

// The live grammar's refusals are the controls in v2.test.parse.newline_dual_role_operator_parse;
// this module asserts only what they cannot: that the refusal arms are what produce them. One claim
// per source, so each pays one tokenize and one parse against the supplied mutant.
test fn witness_without_the_refusal_a_next_line_minus_after_an_operand_merges_RED() -> Bool {
accepts_prepared(text: newline_minus_after_operand_source, file: ^nlm_plain, prepared: nlm_mutant_prepared())
}

test fn witness_without_the_refusal_a_next_line_minus_after_a_block_merges_RED() -> Bool {
accepts_prepared(text: newline_minus_after_block_source, file: ^nlm_block, prepared: nlm_mutant_prepared())
}

test fn witness_without_the_refusal_a_same_line_minus_still_parses() -> Bool {
accepts_prepared(text: same_line_minus_source, file: ^nlm_same, prepared: nlm_mutant_prepared())
}
Loading