Skip to content

v2 parse: grammar Expect label; fn '=' with no expression refuses at the '=' with a typed reason - #12686

Merged
gunbai-bot[bot] merged 7 commits into
mainfrom
session/calm-fox-43
Sep 30, 2026
Merged

gunbai-bot[bot] merged 7 commits into
mainfrom
session/calm-fox-43

Conversation

@gunbai-bot

@gunbai-bot gunbai-bot Bot commented Sep 29, 2026 •

Copy link
Copy Markdown
Contributor

Work item: node://adhoc-9e531074-9d1 (native-seven empty_eq_fn_decl_refuses). Design A, approved by quiet-gull-780 / neat-boar-16.

Root cause (DESIGN §6b)

For fn f(a: Int) -> Int = the parse already refused with a location: parse_g0_tokens_remain at the furthest failure (end of file). The overlap residue at the front is advisory text left over from grammar preparation, not the cause. The real gap is that std.grammar GrammarExpr gave a grammar row no way to name what it expects, so every such failure collapsed into "tokens remain". The claim asserted only "not Accepted", so any refusal made it pass.

Change

  • std.grammar: adds Expect { element, reason }. It is a label, not a cut: it matches and captures exactly what element does, so ordered choice and backtracking are unchanged. Adds a matching field to GrammarExprFold. reason is typed by the new closed v2.std.parse_refusal_reason ParseRefusalReason (the parse stage's refusal-reason vocabulary: FnExpressionBodyMissingAfterEq, DataValueMissingAfterEq), so an unknown reason does not typecheck. The node projection now carries the Expect.
  • 02_parse:
    • A new PreparedExpect arm.
    • ParseFurthestFailure positions can carry one expectation. The join still decides by position. When two records tie at the same position, the expectation recorded first in parse order wins, and the memo-miss join is now ordered caller first.
    • When the fatal leftover-tokens refusal has an expectation, it becomes that reason, located at the token the missing element was to follow.
    • Every GrammarExpr and PreparedGrammarExpr match now names every arm; the wildcards that could have silently absorbed the new arm are gone.
  • The other GrammarExprFold algebras (nullable, FIRST, corner, demand, undefined-nonterminal, occurrence_role, namespace_graft, body_lowering) pass Expect through as its element.
  • Emit and coercion read formal productions and relation rows, not GrammarExpr, so they see no Expect at all.
  • dag grammar: the fn_decl row's '=' expr arm wraps expr in Expect { reason: FnExpressionBodyMissingAfterEq }, and the data_decl row's '=' expr in Expect { reason: DataValueMissingAfterEq }. No other grammar changes.

Claims

  • v2.test.parse.expression_bodied_fn_decl_parse empty_eq_fn_decl_refuses_holds now asserts the fatal reason is ^parse_fn_expression_body_missing_after_eq, located on the parse-stage port at the = span 43..44. Under the old behaviour (residue in front, parse_g0_tokens_remain as the fatal reason) it is red.
  • empty_eq_data_decl_refuses_holds: data x: Int = refuses with DataValueMissingAfterEq at the = span 37..38.
  • The positive controls (expression-bodied, literal-bodied and braced declarations still parse and survive normalize) are unchanged.
  • New v2.test.parse.grammar_expect:
    • expect_tie_first_ordered_alternative_wins_holds and expect_tie_swapped_alternatives_swap_the_label_holds: the tie goes to the first alternative in ordered choice, and swapping the alternatives swaps the label.
    • expect_wrapping_every_row_changes_no_accepted_tree_holds: wrapping every subexpression of a grammar in Expect gives the same accepted tree (compared by content_hash).

Evidence

  • Green at 528f64b (run 36644179879): floor, generated and witnesses. The claims in this PR's changed modules held, including empty_eq_fn_decl_refuses_holds, empty_eq_data_decl_refuses_holds, the positive controls, the three grammar_expect claims, and the emit round-trip modules (emit_ingest_grammar_relation_round_trip, dag_add_emit_round_trip).
  • Discriminating red (DO-NOT-MERGE DO NOT MERGE: discriminating red for #12686 #12717, run 36648553184): the same head with only the fn_decl Expect wrapper removed. required-floor: FAIL v2.test.parse.expression_bodied_fn_decl_parse.empty_eq_fn_decl_refuses_holds returned Bool(false) was the only red, while empty_eq_data_decl_refuses_holds (wrapper intact) passed. So the claim fails under any cause other than the located expectation.

Only the dag grammar's digest changes: its two Expect nodes are part of its identity.

🤖 Generated with Claude Code

…h a located typed reason

std.grammar gains Expect { element, reason }: a label, never a cut. It matches and captures
exactly what its element does in every direction; when the element fails at the furthest
position the parse reached, the refusal names the reason at the token the element was to
follow. Ties at one position go to the expectation recorded first in parse order. Reasons
come from a declared GrammarRoot.expectations roster; preparation refuses undeclared and
unconsumed reasons.

The dag fn_decl row wraps the expression after '=' with
^parse_fn_expression_body_missing_after_eq, and empty_eq_fn_decl_refuses now asserts that
exact fatal reason at the '=' span (43..44).

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
@gunbai-bot
gunbai-bot Bot marked this pull request as ready for review September 29, 2026 19:57
gunbai-bot Bot pushed a commit that referenced this pull request Sep 29, 2026
gunbc-ci-auto-heal and others added 5 commits September 29, 2026 20:32
…portedBareProvider)

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…Fixed

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…mis-added arg; declared text unfold in dag_arrow_lambda witness

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…d-kept roster

Review 72912: GrammarRoot.expectations was a hand copy of the reasons the Expect nodes already
carry, checked against them after the fact (DESIGN §5). It is deleted with both comparison
checks, and every grammar root is back to its main shape. The reason field is now typed by
v2.std.parse_refusal_reason ParseRefusalReason, the parse stage's closed refusal-reason
coproduct, so a misspelled reason fails to typecheck. Members: FnExpressionBodyMissingAfterEq
and DataValueMissingAfterEq; the data_decl '= expr' row carries the second, and its own claim
asserts the reason and the '=' span.

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
@gunbai-bot

gunbai-bot Bot commented Sep 29, 2026

Copy link
Copy Markdown
Contributor Author

Re review 72912: agreed. The roster was validation standing where construction was available (DESIGN §5). Fixed in 528f64b:

  • GrammarRoot.expectations, grammar_empty_expectations, dag_grammar_expectations and both preparation checks (parse_grammar_undeclared_expectation / parse_grammar_unconsumed_expectation) are deleted. Every other grammar's root is back to its main shape, so the PR now touches 9 files.
  • The parse stage had no closed carrier for refusal reasons (Diagnostic.reason is a bare Symbol), and a bare-Symbol fallback lets a misspelled reason silently become a new reason. So Expect.reason is now typed by a new closed coproduct, v2.std.parse_refusal_reason ParseRefusalReason. An unknown reason cannot be written, and the type itself is the roster. It is scoped as the parse stage's refusal-reason vocabulary, not as an Expect-only type, so later parse reasons join it as variants. parse_refusal_reason_symbol gives each variant's diagnostic identity.
  • The vocabulary has two real members: FnExpressionBodyMissingAfterEq (the fn ... = row) and DataValueMissingAfterEq, which the data name: T = expr row now carries. empty_eq_data_decl_refuses_holds asserts that reason at the = span.
  • The tie claims use the two real variants as their labels.

— sent from calm-fox-43

@briansrls briansrls left a comment

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Verdict: APPROVE 528f64b

Expect is modeled as a typed grammar label, not a cut. On acceptance it returns the element's captured tree and diagnostics unchanged; nullable, FIRST, corner, demand, undefined-nonterminal, occurrence-role, namespace-graft and body-lowering analyses all project through to the element. The parse failure carrier still orders by furthest position, with only equal-position labels resolved by first parse order; the memo-miss join preserves that order instead of making cache warmth decide the reason.

The refusal vocabulary is closed, the fn/data grammar rows name distinct variants, and the final diagnostic is located at the token the missing expression was to follow. The controls cover accepted-tree transparency, both ordered-choice tie directions, the exact fn/data reasons and loci, and the positive declaration forms. The reported mutation removing only the fn wrapper makes only the exact fn claim red, so the target claim is no longer green on an arbitrary refusal.

Exact-head witnesses run 36644179879 is green. Source review; no independent local rerun and no merge action.

@briansrls
briansrls added this pull request to the merge queue Sep 30, 2026
@github-merge-queue
github-merge-queue Bot removed this pull request from the merge queue due to a conflict with the base branch Sep 30, 2026
gunbai-bot Bot pushed a commit that referenced this pull request Sep 30, 2026
…ated matches)

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
gunbai-bot Bot pushed a commit that referenced this pull request Sep 30, 2026
@gunbai-bot
gunbai-bot Bot added this pull request to the merge queue Sep 30, 2026
Merged via the queue into main with commit 75f99ab Sep 30, 2026
5 checks passed
@gunbai-bot
gunbai-bot Bot deleted the session/calm-fox-43 branch September 30, 2026 10:23
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant