Skip to content

02_parse Level-1d: migrate grammar validity scans, production lookup, and token head-peek onto std/ catamorphisms - #4658

Merged
briansrls merged 4 commits into
mainfrom
session/sleek-wren-682
Jun 11, 2026
Merged

briansrls merged 4 commits into
mainfrom
session/sleek-wren-682

Conversation

@briansrls

@briansrls briansrls commented Jun 11, 2026 •

Copy link
Copy Markdown
Contributor

02_parse Level-1d: migrate grammar validity scans, production lookup, and token head-peek onto std/ catamorphisms

Continues the stage-adoption lane (#4639 Level-1b GrammarExpr folds, #4651 Level-1c capture spans → fold_node_tree_span). Per MODELING M9 the std/ DFS came first: every replacement below consumes an operation that already exists in v4.std.algebra / v4.std.collection — no new substrate was added.

Hand-match queries dissolved

hand-written (deleted) std/ catamorphism consumed
grammar_dup_check_step + GrammarDupCheckResult accumulator coproduct (🟡) v4.std.algebra.unique over production names
grammar_has_left_recursion_step or-fold v4.std.algebra.any
grammar_has_undefined_nonterminals_step or-fold v4.std.algebra.any
grammar_lookup_production_step first-match Witness fold v4.std.algebra.filter + v4.std.collection.list_at_optional head projection
TokenPeek per-use carrier coproduct (🟡) + hand fold_list_right peek v4.std.collection.list_at_optional (Optional<Token> head projection — the mark's exact dissolve-on-arrival condition)

Net: two 🟡 carrier types and four hand step-folds deleted; grammar_has_duplicate_productions's 🟡 upgraded to 🟢 substrate-consumer (the marked scan morphism arrived as unique). The left-recursion / undefined-nonterminal 🟡 marks stay (their full reachability/scan morphisms have not arrived; only the or-fold plumbing migrated). parse_token_first survives as a one-line typed bridge pinning T = Token for the bootstrap compiler's monomorphic field-access inference (direct inline match failed to infer tok.class).

Equivalence notes:

  • filter is order-preserving, so head-of-filtered == old first-match fold; first match == unique match post-validation since duplicate names are rejected pre-parse.
  • unique (pairwise name eq) == old set-membership scan.

Claims (src/v4/test/claim/parse/grammar_validation.dag)

  • claim_distinct_productions_not_duplicate — negative dup-scan case; guards the polarity of the unique migration (existing claim only covered the duplicate→true direction).
  • claim_lookup_production_present_holds — Holds payload is the production with the requested name (second production in the fixture, so a head-only/wrong-filter lookup goes red).
  • claim_lookup_production_absent_violates — fail-closed Violates for a missing name.

Verification

  • gunbc run --claim-run green on both new lookup witnesses (true, exit 0).
  • Scratch combined witness (not committed) executed all six migrated behaviors against the existing fixtures — dup true/false, undefined-start, dangling-ref, left-recursive true, right-recursive false — plus the full right-recursive parse_production path (exercises the Terminal-arm head projection and table lookup): all green.
  • M1 full-tree emit probe (.github/ci-floor/v4-m1-rust-emit-probe.sh): compiled: 442 files emitted, 0 diagnostics.

🤖 Generated with Claude Code

@briansrls briansrls changed the title M-F stage-adoption Level-1d — continue de-anemizing 02_parse hand-match queries onto the std/ catamorphisms, carrying forward the #4639 (Level-1b GrammarExpr) and #4651 (Level-1c capture-span -> fold_node_tree_span) pattern now on main. TASK: DFS std/ first (MODELING M9) to find the existing fold/wi 02_parse Level-1d: migrate grammar validity scans, production lookup, and token head-peek onto std/ catamorphisms Jun 11, 2026
@briansrls
briansrls marked this pull request as ready for review June 11, 2026 02:59
@briansrls

Copy link
Copy Markdown
Contributor Author

Re the non-blocking note on match unique(...) { true => false, false => true }: no not primitive exists in v4.std.logic (or elsewhere in std/) today, and the match-negation is the established idiom — v4.std.algebra.non_empty negates is_empty the same way (src/v4/std/algebra.dag:681). Adding a not to std/logic would be new substrate (model-first lane), out of scope for this migration PR and not worth staling the two approvals on the resolved head; happy to fold it into a future std/logic PR if the lane wants it. — sent from sleek-wren-682

@briansrls
briansrls merged commit 60be7fa into main Jun 11, 2026
11 checks passed
@briansrls
briansrls deleted the session/sleek-wren-682 branch June 11, 2026 10:13
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