From 2608364e31817e196049ed48214e9e06d0d281e3 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Sat, 16 May 2026 18:12:12 -0400 Subject: [PATCH 1/9] =?UTF-8?q?WIP:=20CP-1a=20=E2=80=94=20v4=20front-end?= =?UTF-8?q?=20tokenize/parse=20+=20declarative=20grammar-as-data?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- src/v4/compiler/01_tokenize.dag | 115 +++++++++++++++++++++++++++++--- src/v4/compiler/02_parse.dag | 93 ++++++++++++++++++++++++-- 2 files changed, 194 insertions(+), 14 deletions(-) diff --git a/src/v4/compiler/01_tokenize.dag b/src/v4/compiler/01_tokenize.dag index 111622eb503..c2bf1caceb7 100644 --- a/src/v4/compiler/01_tokenize.dag +++ b/src/v4/compiler/01_tokenize.dag @@ -10,17 +10,23 @@ // STOP. See 00_compile.dag B2-OMNI for the pivot. // // Owns: -// - TokenStream type (output) -// - tokenize: (FreeMonoid, LexRules) -> Result -// (LexRules is declarative data from the LanguageModel, not code here) -// - character-class predicates (driven by LexRules) +// - Token, TokenStream carriers +// - LexRules — declarative lexical authority as a `Node` tree (B2: +// grammar-as-data; the generic walker reads this substrate, never a +// language-specific hardcoded recognizer) +// - tokenize: (String, file: Symbol, LexRules) -> Outcome +// (DECISIONS.md **I** — fail-closed stage seam beside `Diagnostic`) // // Consumes: -// - std/text.dag: Char, String -// - std/diagnostic.dag: Diagnostic -// - std/witness.dag: Witness +// - std/text.dag: String (= FreeMonoid per text.dag) +// - std/node.dag: Node, Symbol, node_well_formed +// - std/collection.dag: List +// - std/diagnostic.dag: Diagnostic, Outcome, Locus, Correction, +// NoCorrectionReason, Extent // -// Status: scaffold — fill per TASKS.md T-6 +// Status: Wave-1 generic machinery — lexical **walk** not realized on the +// v2 bridge (honest `Rejected`); structural carriers + contracts are +// authoritative for downstream T-6/T-7 consumers. // Brief: see BRIEF_TEMPLATE.md; this file's I/O contract is the immutable // contract for the worker. Splitting this file requires explicit operator // ratification (substrate extension = stop signal). @@ -28,3 +34,96 @@ module v4.compiler.tokenize + +import v4.std.collection { List } +import v4.std.diagnostic { + Correction, + Diagnostic, + Locus, + NoCorrectionReason, + Outcome, +} +import v4.std.node { Node, Symbol, node_well_formed } +import v4.std.text { String } + + +// ───────────────────────────────────────────────────────────────────── +// LexRules — declarative lexical specification as a finite `Node` tree +// (B2-OMNI grammar-as-data). Language #1 binds a concrete instance when +// the ratified LanguageModel carrier path exists; this file stays generic. +type LexRules = Node + + +// ───────────────────────────────────────────────────────────────────── +// Token — one classified lexeme in source order. +// +// `class` is an opaque `Symbol` naming the token class **as declared by +// the LanguageModel's lexical data** — the kernel does not interpret the +// spelling (K-1). `lexeme` is the matched surface text (boundary carrier). +// Offsets are half-open `[start, end)` byte indices into `text` (same +// scaffold honesty as `Extent.ByteRange` in diagnostic.dag — producer +// bounds; refinement substrate is T-3 cardinality work elsewhere). +type Token { + class: Symbol + lexeme: String + file: Symbol + start: Int + end: Int +} + + +// ───────────────────────────────────────────────────────────────────── +// TokenStream — ordered output of stage 1. +type TokenStream { + tokens: List +} + + +// ───────────────────────────────────────────────────────────────────── +// Reason symbols — owned by this dimension (diagnostic.dag owns schema). +data tokenize_lexical_walk_not_realized: Symbol = tokenize_lexical_walk_not_realized + +data tokenize_lex_rules_not_well_formed: Symbol = tokenize_lex_rules_not_well_formed + + +fn tokenize_lexical_walk_not_realized_diagnostic(at: Locus) -> Diagnostic { + Diagnostic { + reason: tokenize_lexical_walk_not_realized, + at: at, + correction: Unavailable { reason: ExternalContractUnknown } + } +} + + +fn tokenize_lex_rules_not_well_formed_diagnostic(at: Locus) -> Diagnostic { + Diagnostic { + reason: tokenize_lex_rules_not_well_formed, + at: at, + correction: Unavailable { reason: ExternalContractUnknown } + } +} + + +// ───────────────────────────────────────────────────────────────────── +// tokenize — GENERIC lexical ingest (B2-OMNI). +// +// `rules` is the only lexical authority; there is no language-keyed +// branch on `file` or `text` spelling here. Bridge-era note: the full +// walk is not executed in the v2 seed — this entry point fail-closes with +// a typed `Diagnostic` until the walker lowers; ill-formed `LexRules` +// trees reject before that staged work. +fn tokenize(text: String, file: Symbol, rules: LexRules) -> Outcome { + let at = Textual { + file: file, + extent: WholeFile + } + if node_well_formed(n: rules) { + Rejected { + diagnostic: tokenize_lexical_walk_not_realized_diagnostic(at: at) + } + } else { + Rejected { + diagnostic: tokenize_lex_rules_not_well_formed_diagnostic(at: at) + } + } +} diff --git a/src/v4/compiler/02_parse.dag b/src/v4/compiler/02_parse.dag index cd8bdd7aa33..eb7ea788266 100644 --- a/src/v4/compiler/02_parse.dag +++ b/src/v4/compiler/02_parse.dag @@ -37,16 +37,22 @@ // production hardcoded in this generic walker. // // Owns: -// - ParseTree type -// - parse: (TokenStream, Grammar) -> Result -// (Grammar is declarative data from the LanguageModel, not code here) -// - grammar productions as Node trees +// - Grammar — declarative syntactic authority as a finite `Node` tree +// - ParseTree — surface syntax tree prior to normalize (carrier = `Node`) +// - parse: (TokenStream, Grammar) -> Outcome +// (DECISIONS.md **I**) // // Consumes: -// - std/node.dag, std/diagnostic.dag, std/witness.dag +// - std/node.dag: Node, Symbol, node_well_formed +// - std/collection.dag: List +// - std/diagnostic.dag: Diagnostic, Outcome, Locus, Correction, +// NoCorrectionReason, Extent // - compiler/01_tokenize.dag: TokenStream // -// Status: scaffold — fill per TASKS.md T-7 +// Status: Wave-1 generic machinery — syntactic **walk** not realized on +// the v2 bridge (honest `Rejected`); PARSE-1 bodiless-fn production is a +// constraint on the ratified LanguageModel grammar **data** (operator- +// pending file home), not encoded in this walker. // Brief: see BRIEF_TEMPLATE.md; this file's I/O contract is the immutable // contract for the worker. Splitting this file requires explicit operator // ratification (substrate extension = stop signal). @@ -54,3 +60,78 @@ module v4.compiler.parse + +import v4.compiler.tokenize { TokenStream } +import v4.std.diagnostic { + Correction, + Diagnostic, + Locus, + NoCorrectionReason, + Outcome, +} +import v4.std.node { Node, Symbol, node_well_formed } + + +// ───────────────────────────────────────────────────────────────────── +// Grammar — declarative syntactic specification as a finite `Node` tree +// (B2-OMNI). Productions (including PARSE-1 bodiless signature rows) are +// DATA in the LanguageModel instance, never special-cased here. +type Grammar = Node + + +// ───────────────────────────────────────────────────────────────────── +// ParseTree — stage-2 output; the syntax tree is a `Node` forest spine +// (A1) until normalize dissolves sugar (T-8). +type ParseTree = Node + + +// ───────────────────────────────────────────────────────────────────── +// Reason symbols — owned by this dimension (diagnostic.dag owns schema). +data parse_stage_locus_port: Symbol = parse_stage_locus_port + +data parse_walk_not_realized: Symbol = parse_walk_not_realized + +data parse_grammar_not_well_formed: Symbol = parse_grammar_not_well_formed + + +fn parse_walk_not_realized_diagnostic(at: Locus) -> Diagnostic { + Diagnostic { + reason: parse_walk_not_realized, + at: at, + correction: Unavailable { reason: ExternalContractUnknown } + } +} + + +fn parse_grammar_not_well_formed_diagnostic(at: Locus) -> Diagnostic { + Diagnostic { + reason: parse_grammar_not_well_formed, + at: at, + correction: Unavailable { reason: ExternalContractUnknown } + } +} + + +// ───────────────────────────────────────────────────────────────────── +// parse — GENERIC syntactic ingest (B2-OMNI). +// +// `grammar` is the only syntactic authority. `tokens` is threaded so the +// entry point composes with stage 1; there is no token-shape hardcoding +// beyond the shared `TokenStream` carrier. Bridge-era note: the full +// walk is not executed in the v2 seed — fail-closed `Rejected` until the +// walker lowers. +fn parse(tokens: TokenStream, grammar: Grammar) -> Outcome { + let at = PortLocus { + port: parse_stage_locus_port + } + let _toks = tokens.tokens + if node_well_formed(n: grammar) { + Rejected { + diagnostic: parse_walk_not_realized_diagnostic(at: at) + } + } else { + Rejected { + diagnostic: parse_grammar_not_well_formed_diagnostic(at: at) + } + } +} From 4500c98097b689a3ca5f6a0b2216f8871d0d005f Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Sat, 16 May 2026 18:13:41 -0400 Subject: [PATCH 2/9] =?UTF-8?q?WIP:=20CP-1a=20=E2=80=94=20v4=20front-end?= =?UTF-8?q?=20tokenize/parse=20+=20declarative=20grammar-as-data?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- src/v4/DECISIONS.md | 1 + src/v4/STRUCTURE.md | 9 +++-- src/v4/compiler/01_tokenize.dag | 4 +- src/v4/compiler/02_parse.dag | 8 ++-- src/v4/extdeps/languages/dag.dag | 68 ++++++++++++++++++++++++++++++++ 5 files changed, 83 insertions(+), 7 deletions(-) create mode 100644 src/v4/extdeps/languages/dag.dag diff --git a/src/v4/DECISIONS.md b/src/v4/DECISIONS.md index 8d6114b3eae..cbc8bcf884e 100644 --- a/src/v4/DECISIONS.md +++ b/src/v4/DECISIONS.md @@ -39,6 +39,7 @@ through — and moves to Part 1. | **L-1** | Verilog/SPICE/English added as **parallel B2-OMNI falsification probes** (T-4.9/4.10/4.11), maximally diverse on purpose. Forks resolved: English = boundary-honesty probe (Shape B emit + fail-closed ingest TestClaim), **not** a language model; SPICE = `extdeps/formats/` (netlist is a data format); Verilog = the IN-B concurrency validation (a needed 6th behavior = C1 escalation, by design caught early) | `TASKS.md` T-4.9/4.10/4.11 + `extdeps/languages/verilog.dag`, `extdeps/formats/spice.dag`, `test/claim/boundary/english_ingest_fail_closed.dag` | | **L-3** | **Down-the-stack** B2-OMNI probes added (operator-ratified 2026-05-15, parallel up front): T-4.12 `extdeps/languages/llvm_ir.dag` (SSA IR — generalize down the stack; F ~all-structural), T-4.13 `extdeps/languages/machine_code.dag` (bottom of stack; no cosmetics; disassembly = the extreme fail-closed/no-engine test), T-4.14 `extdeps/languages/ptx.dag` (CUDA SIMT — IN-B bet vs the 5 behaviors). Validates the model across the **full target spectrum** (source→IR→machine code) — concretizes C5-fidelity ("we don't necessarily output a binary; F is model+intent-relative"). **Forks DISSOLVED (cascade-closure, resolves 3250390911; no PROPOSED residue):** neither was a genuine open fork — each is forced by an already-ratified parent, and the alternative *contradicts* a ratified decision. (1) machine_code = ONE model parameterized by an `Isa` — **forced by B2-OMNI** (parameterize-not-enumerate / O(N+M); per-ISA files ARE the N×M trap B2-OMNI forbids). (2) CUDA = model **PTX** — **forced by L-3's own ratified down-the-stack-IR scope**: PTX is the SIMT *IR* layer (the down-the-stack probe T-4.14 exists to test); CUDA-C++ is just another Shape A *source* language already covered by general modeling, so it would not be a down-the-stack probe at all. Per P5 the fork dissolves into already-ratified coordinates, not a new decision | `TASKS.md` T-4.12/4.13/4.14 + `extdeps/languages/{llvm_ir,machine_code,ptx}.dag` | | **L-4** | **PROOF-1's prover model lands as `extdeps/languages/lean.dag`** (B-2, side-session 2026-05-15 — operator-ratified). PROOF-1 (#3158, merged) was framed "no new file" and explicitly deferred its prover model to "realized when a lean/coq model lands"; this IS that model. B2-OMNI **structurally requires** a declarative `LanguageModel` file to emit to any target, so PROOF-1's "emit to a lean model" needs exactly this file — adding it is the closed-tree extension operator-ratified here (STRUCTURE.md invariant #1). **ONE prover first — Lean** — scoped to the first theorem class **termination** (A2 structural descent ≈ Lean well-founded recursion / `termination_by`). **Coq is the DEFERRED second-prover falsification probe** ("does the model generalize across provers?" — O(1) per B2-OMNI, added only when a theorem class needs it; same probe posture as L-1/L-3; a future operator-ratified extension, never a silent TODO). Per L-2 the Lean *spec* is modeled, not Mathlib. STRUCTURE count 63→64 .dag | `extdeps/languages/lean.dag` (new) + `STRUCTURE.md` languages enumeration/count + `TASKS.md` PROOF-1/T-15 note; cross-ref DECISIONS PROOF-1 / B2-OMNI / L-2 | +| **L-5** | **`extdeps/languages/dag.dag` admitted — gunbc's native `.dag` LanguageModel** (operator **Option A**, C1 closed-tree extension 2026-05-16, relay merry-ibex-337). `.dag` is B2-OMNI **language #1** (never hardcoded into the generic `01_tokenize` / `02_parse` walkers); lexical + syntactic authority is declarative **`Node` grammar-data** here, same `extdeps/languages/*` bundle shape as the other Shape-A models. L-2 **spec-first** without an external URL: anchor is repo-owned **`docs/v3-spec.md`** plus the v4 closed tree (`STRUCTURE.md`, `TASKS.md` T-6/T-7). PARSE-1 bodiless-`fn` is a **grammar production in data**, not walker code. STRUCTURE count **64→65** `.dag`. | `extdeps/languages/dag.dag` (new) + `STRUCTURE.md` languages line + total; cross-ref `compiler/01_tokenize.dag` / `compiler/02_parse.dag` + B2-OMNI + PARSE-1 | | **QRY-1** | **RETRACTED & reframed (operator-corrected 2026-05-15).** "query = user-defined lens" is wrong: user-vs-kernel is PROVENANCE, not a structural distinction (feedback_naming_is_aliasing) — a decorative name distinguished only by who-authored-it must not exist ("a real distinction, or not exist"). There is NO query concept/noun/subsystem. The REAL axis is **scope/parameterization**, already modeled with no new noun: (1) `SectionRef` (DeclarationScope\|NodeScope) — applying a lens AT a scope; (2) parameterized lens signatures — the **affected-set lens (T-21) `(Dag,Diff)->Witness` is the archetype**: "the affected set of THIS change" = `affected_set(dag,diff)`, already first-class. Lenses, read at scopes and/or parameterized. No `query.dag`. The B2-OMNI "one read over the Node pivot, all ingested languages" property holds for ANY lens, not a "query" | `lens/application.dag` header + THESIS §1.5 + `lens/affected_set.dag` (T-21) | | **PAR-1** | Parallelism (T-13) is a THESIS free consequence, a target-AGNOSTIC lens reporting the independence **FACT** (`Witness`); WHETHER/HOW to realize it is target-DEPENDENT — a cost-derived decision (U1/U2 per-target) at emit(T-11)/eval(T-22), NOT the lens. independence = structural-disjointness ∧ effect-independence (consumes `lens/effect.dag`, B3 — Node-disjoint is necessary not sufficient) ∧ fold-combiner associativity-by-inhabitance (consumes `std/algebra.dag` — parallel-reduce is an algebra fact, not a heuristic). fact ≠ spawn-decision; no annotation, no scheduling heuristic. **User-facing contract:** NOT a "parallelize my code" command (forbidden — engine-shaped from the user's seat); a lens the user READS (same UX as complexity/cost); control = structure not a knob; default introspective with the realize-decision derived+inspectable per target (e.g. honestly "no — CPython GIL"); guarantee via `apply_lens(parallelism, Enforce)` (T-23, uniform opt-in-depth). 4 worked examples embedded | `lens/parallelism.dag` header + `TASKS.md` T-13 | | **B1** | One content-addressing scheme: a `std`-level Merkle catamorphism `content_hash : Node -> Hash` over the **canonical-form clause** (a SEPARATE explicit node.dag authority — NOT subsumed by A1, which only covers recursion/axis-closure/generics/termination). `Hash` is an opaque digest (no content accessor, K-1-style). One scheme consumed by T-15/T-20/T-21 + A3 + C5 + structural build/CI artifact caching (a cache key IS `content_hash` of the input subgraph — see `lens/affected_set.dag`). NOT workflow-level | `std/node.dag` — the `Hash` type lands here (re-homed beside `Symbol` by the primitive.dag-decomposition; `Hash` is a content identity, not a scalar); the **B1-CANON block** is the canonical-form clause — operator-DESIGNED & ratified in-header 2026-05-15 (pulled back from worker delegation because every consumer rests on it); the canonical-form clause + `content_hash = merkle_fold ∘ canonical` fold land in `std/node.dag`; T-1 IMPLEMENTS that contract, it does not design it | diff --git a/src/v4/STRUCTURE.md b/src/v4/STRUCTURE.md index 1667f55e091..7d0e8ed7d22 100644 --- a/src/v4/STRUCTURE.md +++ b/src/v4/STRUCTURE.md @@ -32,8 +32,9 @@ src/v4/ verification.dag # TestClaim schema (imported from v3) report.dag # advisory carrier (NOT fail-closed Diagnostic); used by synthesis lens - extdeps/ # external system contracts (20 files) + extdeps/ # external system contracts (21 files) languages/ # language models (direction-agnostic — emit AND ingest) + dag.dag # gunbc `.dag` — B2-OMNI language #1 (C1 extension 2026-05-16; relay merry-ibex-337) rust.dag python.dag go.dag @@ -109,10 +110,12 @@ src/v4/ fixture/ # canonical input programs ``` -**Total: 64 .dag files + 5 docs + 5 .gitkeep = 74 files.** (Per invariant +**Total: 65 .dag files + 5 docs + 5 .gitkeep = 75 files.** (Per invariant #1 the enumeration above — not the count — is authoritative; the count is a checksum, updated on every operator-ratified file addition/removal. -−5 .dag 2026-05-15: work-direction meta-layer cut, operator-ratified.) ++1 .dag 2026-05-16: `extdeps/languages/dag.dag` — operator-ratified C1 closed-tree +extension (Option A, relay merry-ibex-337). −5 .dag 2026-05-15: work-direction +meta-layer cut, operator-ratified.) ## Scalar/numeric concept decomposition diff --git a/src/v4/compiler/01_tokenize.dag b/src/v4/compiler/01_tokenize.dag index c2bf1caceb7..be0a323d4c1 100644 --- a/src/v4/compiler/01_tokenize.dag +++ b/src/v4/compiler/01_tokenize.dag @@ -22,7 +22,9 @@ // - std/node.dag: Node, Symbol, node_well_formed // - std/collection.dag: List // - std/diagnostic.dag: Diagnostic, Outcome, Locus, Correction, -// NoCorrectionReason, Extent +// NoCorrectionReason +// - extdeps/languages/dag.dag: language-#1 `DagLanguageModel.lex` authority +// (B2-OMNI — binds here as `LexRules`/`Node`, never special-cased in-body) // // Status: Wave-1 generic machinery — lexical **walk** not realized on the // v2 bridge (honest `Rejected`); structural carriers + contracts are diff --git a/src/v4/compiler/02_parse.dag b/src/v4/compiler/02_parse.dag index eb7ea788266..a850cfd6edb 100644 --- a/src/v4/compiler/02_parse.dag +++ b/src/v4/compiler/02_parse.dag @@ -46,13 +46,15 @@ // - std/node.dag: Node, Symbol, node_well_formed // - std/collection.dag: List // - std/diagnostic.dag: Diagnostic, Outcome, Locus, Correction, -// NoCorrectionReason, Extent +// NoCorrectionReason // - compiler/01_tokenize.dag: TokenStream +// - extdeps/languages/dag.dag: language-#1 `DagLanguageModel.grammar` +// authority (B2-OMNI + PARSE-1 — data-carried, not walker-special-cased) // // Status: Wave-1 generic machinery — syntactic **walk** not realized on // the v2 bridge (honest `Rejected`); PARSE-1 bodiless-fn production is a -// constraint on the ratified LanguageModel grammar **data** (operator- -// pending file home), not encoded in this walker. +// constraint on `DagLanguageModel.grammar` **data** in `extdeps/languages/dag.dag`, +// not encoded in this generic walker. // Brief: see BRIEF_TEMPLATE.md; this file's I/O contract is the immutable // contract for the worker. Splitting this file requires explicit operator // ratification (substrate extension = stop signal). diff --git a/src/v4/extdeps/languages/dag.dag b/src/v4/extdeps/languages/dag.dag new file mode 100644 index 00000000000..a9c2620a8a4 --- /dev/null +++ b/src/v4/extdeps/languages/dag.dag @@ -0,0 +1,68 @@ +// src/v4/extdeps/languages/dag.dag +// +// Scope: gunbc `.dag` surface — the native **LanguageModel** for language #1 +// (B2-OMNI). Direction-agnostic: the same declarative data authorizes +// ingest (`01_tokenize` ∘ `02_parse` over `lex` + `grammar`) and emit +// (downstream `05_emit` / targets), per THESIS:188 unification. +// Anchor: **Repo-owned specification** (L-2 spec-first without an external +// standards URL): `docs/v3-spec.md` (v3 language surface + arch +// context carried forward as the checkable authority for the +// bridge-era subset) **plus** the v4 closed tree itself (`STRUCTURE.md`, +// `TASKS.md` T-6/T-7, `compiler/01_tokenize.dag` / +// `compiler/02_parse.dag` contracts, `DECISIONS.md` B2-OMNI / +// PARSE-1). Grammar obligations ratified in-repo supersede prose; +// drift = visible C1 edits to those artifacts, never silent extension. +// Unifies: (per THESIS:188) language spec = transport spec = interpreter +// runtime. ONE substrate carrier for all three roles. Different +// lenses read different facts from the same data (emission reads +// syntax; transport reads serialization; interpreter reads execution +// semantics). A worker needing transport or runtime extends this file, +// not a new "transport spec" file. +// +// B2-OMNI (operator-ratified 2026-05-15): `.dag` is **language #1**, never +// hardcoded into the generic tokenizer/parser walkers — those stages consume +// **this** model's `lex` / `grammar` `Node` trees as the only lexical and +// syntactic authority (O(N+M) pivot; same pattern as other `extdeps/languages/*`). +// +// PARSE-1: bodiless `fn` signature declarations are a **first-class grammar +// production** encoded as **data** in `grammar` (v4-self-parse era). The generic +// `02_parse` walker does not special-case them; v2-bridge preflight remains +// safe (frozen v2 never parses bodiless `fn`). See `compiler/02_parse.dag` +// header. +// +// Owns: +// - `DagLanguageModel` — bundles declarative `lex: Node` + `grammar: Node` +// (the `LexRules` / `Grammar` roles named in `compiler/01_tokenize.dag` / +// `compiler/02_parse.dag`; carrier = `Node` per A1) +// - (bundled / Wave follow-on) lexical + syntactic production tables, +// C5-fidelity dispositions, D2 resolver facts — same Owns/ELSEWHERE split +// discipline as `rust.dag` / `go.dag`; this slice lands the **admission + +// bundle head** only +// +// Consumes: +// - std/node.dag: Node (the grammar-as-data substrate) +// - cross-ref: `docs/v3-spec.md`, `STRUCTURE.md`, `TASKS.md` T-4/T-6/T-7, +// `DECISIONS.md` **L-5** + B2-OMNI + PARSE-1 + L-2 +// +// Status: operator-ratified C1 closed-tree extension 2026-05-16 (Option **A**, +// relay merry-ibex-337) — **admitted**; scaffold — fill per TASKS.md T-4 + T-6/T-7. +// Brief: see BRIEF_TEMPLATE.md; this file's I/O contract is the immutable +// contract for the worker. Splitting this file requires explicit operator +// ratification (substrate extension = stop signal). + + +module v4.extdeps.languages.dag + + +import v4.std.node { Node } + + +// ───────────────────────────────────────────────────────────────────── +// DagLanguageModel — gunbc `.dag` as a first-class Shape-A LanguageModel +// (B2-OMNI language #1). `lex` / `grammar` are the lexical and syntactic rule +// forests consumed by the generic pipeline stages; both are finite `Node` +// trees (A1), never procedural recognizers in `compiler/*`. +type DagLanguageModel { + lex: Node + grammar: Node +} From c7282dc7b0101a3aa3af2b758b4d8a36a9a2f387 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Sat, 16 May 2026 22:15:16 +0000 Subject: [PATCH 3/9] fix: align 02_parse.dag header Consumes with actual imports Remove erroneous std/collection.dag line; parse consumes TokenStream via tokenize only. Co-authored-by: Cursor --- src/v4/compiler/02_parse.dag | 1 - 1 file changed, 1 deletion(-) diff --git a/src/v4/compiler/02_parse.dag b/src/v4/compiler/02_parse.dag index a850cfd6edb..2939ad13b4b 100644 --- a/src/v4/compiler/02_parse.dag +++ b/src/v4/compiler/02_parse.dag @@ -44,7 +44,6 @@ // // Consumes: // - std/node.dag: Node, Symbol, node_well_formed -// - std/collection.dag: List // - std/diagnostic.dag: Diagnostic, Outcome, Locus, Correction, // NoCorrectionReason // - compiler/01_tokenize.dag: TokenStream From e8ba78b9f592ba725a02a5c65dc62d9d630c0442 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Sat, 16 May 2026 18:19:48 -0400 Subject: [PATCH 4/9] =?UTF-8?q?WIP:=20CP-1a=20=E2=80=94=20v4=20front-end?= =?UTF-8?q?=20tokenize/parse=20+=20declarative=20grammar-as-data?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- src/v4/compiler/01_tokenize.dag | 124 ++++++++++++++++++++-------- src/v4/compiler/02_parse.dag | 134 +++++++++++++++++-------------- src/v4/extdeps/languages/dag.dag | 37 ++++++++- 3 files changed, 200 insertions(+), 95 deletions(-) diff --git a/src/v4/compiler/01_tokenize.dag b/src/v4/compiler/01_tokenize.dag index be0a323d4c1..6ed27fbe86b 100644 --- a/src/v4/compiler/01_tokenize.dag +++ b/src/v4/compiler/01_tokenize.dag @@ -9,26 +9,35 @@ // A .dag-only character class hardcoded here reintroduces the N×M trap = // STOP. See 00_compile.dag B2-OMNI for the pivot. // +// Wave-1 **encoding contract** (grammar-as-data over `Node`, not prose): +// **E0 — void lexical fragment**: `LexRules` root is a **type** `Node` +// whose connective is **`Conj` with zero children** — exactly zero +// lexical productions. The walker recognizes this shape **structurally** +// (discriminant + `count(children)==0`), never by `Symbol` spelling. +// E0 + empty `String` (`FreeMonoid` spine `Empty`) ⇒ `Produced` empty +// `TokenStream`. E0 + non-empty source ⇒ `Rejected` (source not exhausted +// — fail-closed; no fabricated tokens). +// Further encodings (E1+, keywords, …) land as additional **data** +// shapes ratified with the LanguageModel carrier; the walker grows by +// `match` on those shapes, not by hardcoding `.dag` surface spellings. +// // Owns: // - Token, TokenStream carriers -// - LexRules — declarative lexical authority as a `Node` tree (B2: -// grammar-as-data; the generic walker reads this substrate, never a -// language-specific hardcoded recognizer) +// - LexRules — declarative lexical authority as a finite `Node` tree // - tokenize: (String, file: Symbol, LexRules) -> Outcome -// (DECISIONS.md **I** — fail-closed stage seam beside `Diagnostic`) // // Consumes: -// - std/text.dag: String (= FreeMonoid per text.dag) -// - std/node.dag: Node, Symbol, node_well_formed +// - std/text.dag: String (= FreeMonoid) +// - std/node.dag: Node, NodeKind, TypeNode, ComputationNode, Connective, +// Conj, Symbol, node_well_formed // - std/collection.dag: List -// - std/diagnostic.dag: Diagnostic, Outcome, Locus, Correction, -// NoCorrectionReason -// - extdeps/languages/dag.dag: language-#1 `DagLanguageModel.lex` authority -// (B2-OMNI — binds here as `LexRules`/`Node`, never special-cased in-body) +// - std/diagnostic.dag: Diagnostic, Outcome, Locus, Textual, WholeFile, +// Correction, NoCorrectionReason +// - extdeps/languages/dag.dag: language-#1 model binds E0 instances (see +// `dag_wave1_e0_void_lex`); this file stays encoding-generic. // -// Status: Wave-1 generic machinery — lexical **walk** not realized on the -// v2 bridge (honest `Rejected`); structural carriers + contracts are -// authoritative for downstream T-6/T-7 consumers. +// Status: Wave-1 — E0 void-lex path is **realized** (`Produced`); richer +// encodings ⇒ honest `Rejected { … walk_not_realized }` until ratified. // Brief: see BRIEF_TEMPLATE.md; this file's I/O contract is the immutable // contract for the worker. Splitting this file requires explicit operator // ratification (substrate extension = stop signal). @@ -44,27 +53,30 @@ import v4.std.diagnostic { Locus, NoCorrectionReason, Outcome, + Textual, + WholeFile, +} +import v4.std.algebra { FreeMonoid } +import v4.std.node { + ComputationNode, + Conj, + Node, + NodeKind, + Symbol, + TypeNode, + node_well_formed, } -import v4.std.node { Node, Symbol, node_well_formed } -import v4.std.text { String } +import v4.std.text { Char, String } // ───────────────────────────────────────────────────────────────────── // LexRules — declarative lexical specification as a finite `Node` tree -// (B2-OMNI grammar-as-data). Language #1 binds a concrete instance when -// the ratified LanguageModel carrier path exists; this file stays generic. +// (B2-OMNI grammar-as-data). type LexRules = Node // ───────────────────────────────────────────────────────────────────── // Token — one classified lexeme in source order. -// -// `class` is an opaque `Symbol` naming the token class **as declared by -// the LanguageModel's lexical data** — the kernel does not interpret the -// spelling (K-1). `lexeme` is the matched surface text (boundary carrier). -// Offsets are half-open `[start, end)` byte indices into `text` (same -// scaffold honesty as `Extent.ByteRange` in diagnostic.dag — producer -// bounds; refinement substrate is T-3 cardinality work elsewhere). type Token { class: Symbol lexeme: String @@ -87,6 +99,8 @@ data tokenize_lexical_walk_not_realized: Symbol = tokenize_lexical_walk_not_real data tokenize_lex_rules_not_well_formed: Symbol = tokenize_lex_rules_not_well_formed +data tokenize_lex_e0_source_not_exhausted: Symbol = tokenize_lex_e0_source_not_exhausted + fn tokenize_lexical_walk_not_realized_diagnostic(at: Locus) -> Diagnostic { Diagnostic { @@ -106,26 +120,72 @@ fn tokenize_lex_rules_not_well_formed_diagnostic(at: Locus) -> Diagnostic { } +fn tokenize_lex_e0_source_not_exhausted_diagnostic(at: Locus) -> Diagnostic { + Diagnostic { + reason: tokenize_lex_e0_source_not_exhausted, + at: at, + correction: Unavailable { reason: ExternalContractUnknown } + } +} + + +// ───────────────────────────────────────────────────────────────────── +// free_monoid_char_len — walk the `FreeMonoid` spine (`String` alias). +fn free_monoid_char_len(xs: FreeMonoid) -> Int { + match xs { + Empty => 0 + Cons { head: _, tail: t } => 1 + free_monoid_char_len(xs: t) + } +} + + +// ───────────────────────────────────────────────────────────────────── +// string_is_empty — `String` = `FreeMonoid` (std/text.dag). +fn string_is_empty(s: String) -> Bool { + free_monoid_char_len(xs: s) == 0 +} + + +// ───────────────────────────────────────────────────────────────────── +// lex_rules_node_is_conj_empty_root — structural E0 predicate (Wave-1). +fn lex_rules_node_is_conj_empty_root(rules: Node) -> Bool { + match rules.kind { + TypeNode { connective: Conj } => count(rules.children) == 0 + TypeNode { connective: _ } => false + ComputationNode { behavior: _ } => false + } +} + + // ───────────────────────────────────────────────────────────────────── // tokenize — GENERIC lexical ingest (B2-OMNI). // -// `rules` is the only lexical authority; there is no language-keyed -// branch on `file` or `text` spelling here. Bridge-era note: the full -// walk is not executed in the v2 seed — this entry point fail-closes with -// a typed `Diagnostic` until the walker lowers; ill-formed `LexRules` -// trees reject before that staged work. +// Discriminates on **declared** `LexRules` shape; only E0 is realized in +// Wave-1. No `file` or `text` content branches on language identity. fn tokenize(text: String, file: Symbol, rules: LexRules) -> Outcome { let at = Textual { file: file, extent: WholeFile } - if node_well_formed(n: rules) { + if !node_well_formed(n: rules) { Rejected { - diagnostic: tokenize_lexical_walk_not_realized_diagnostic(at: at) + diagnostic: tokenize_lex_rules_not_well_formed_diagnostic(at: at) + } + } else if lex_rules_node_is_conj_empty_root(rules: rules) { + if string_is_empty(s: text) { + Produced { + value: TokenStream { + tokens: [] + } + } + } else { + Rejected { + diagnostic: tokenize_lex_e0_source_not_exhausted_diagnostic(at: at) + } } } else { Rejected { - diagnostic: tokenize_lex_rules_not_well_formed_diagnostic(at: at) + diagnostic: tokenize_lexical_walk_not_realized_diagnostic(at: at) } } } diff --git a/src/v4/compiler/02_parse.dag b/src/v4/compiler/02_parse.dag index 2939ad13b4b..f5118b7f3d2 100644 --- a/src/v4/compiler/02_parse.dag +++ b/src/v4/compiler/02_parse.dag @@ -3,57 +3,36 @@ // Scope: pipeline stage 2 — TokenStream to ParseTree. Pure function, fail-closed. // Anchor: https://en.wikipedia.org/wiki/Parsing // -// B2-OMNI (operator-ratified 2026-05-15): parse is NOT a .dag parser. It -// is the GENERIC walker over a `LanguageModel`'s declarative grammar -// (B2). Parsing .dag is `parse(tokens, dag_model.grammar)` — `.dag` is -// language #1, never hardcoded/special-cased. The same generic walker -// ingests other **Shape A languages** (Rust/Python/…) via their models. -// Shape B data formats (JSON, SPICE netlists) are NOT LanguageModels and -// do NOT pass through this compiler-language parser — they ingest via -// the formats data-model path (THESIS Shape A / Shape B is a hard -// boundary; conflating them here re-blurs the ingest boundary = STOP). -// This is the load-bearing enabler of the O(N+M) pivot (see -// 00_compile.dag B2-OMNI). A `.dag`-specific production hardcoded here = -// the N×M trap creeping back = STOP. +// B2-OMNI (operator-ratified 2026-05-15): parse is the GENERIC walker over a +// `LanguageModel`'s declarative grammar (`Grammar` as `Node`); `.dag` is +// language #1 at the **data** layer (`extdeps/languages/dag.dag`), never +// special-cased in-body here. // -// PARSE-1 (operator-ratified 2026-05-15): the `.dag` LanguageModel -// grammar MUST admit a BODILESS SIGNATURE declaration as a first-class -// production (an `fn name(args) -> T` with NO body — the -// contract-as-checked-signature surface). This graduates the "immutable -// I/O contract for the worker" (the scaffold-header convention) from -// comment-prose into compiler-enforced structure: a later filled body -// must conform to the frozen signature, divergence = a fail-closed type -// error (structural, per no-annotations). NOT a v2-bridge feature — -// verified: frozen v2's parser REJECTS bodiless `fn` (`expected LBrace`) -// while cleanly parsing the full ratified kernel shape WITH bodies -// (40k-line src/v2 corpus + constructive kernel probe, zero syntax -// errors). So bridge-era substrate contracts stay comment-prose (current -// scaffold form) and the fail-closed parse-class gate is safe (v2 is -// never asked to parse bodiless fn); the bodiless-signature production -// is a v4-self-parser-era surface only. This is the conditional that -// makes the bridge-era deferral acceptable — supportable by construction -// (it is v4's own grammar; nothing external constrains it). Per B2-OMNI -// this is a grammar-DATA production in the `.dag` model, not a -// production hardcoded in this generic walker. +// Wave-1 **encoding contract** (mirrors `01_tokenize.dag` E0): +// **G0 — void syntactic fragment**: `Grammar` root is **type** `Node` with +// connective **`Conj` + zero children**. With an **empty** `TokenStream`, +// the parse result is `Produced { value: grammar }` — the grammar root is +// itself the (degenerate) `ParseTree` spine for the empty sentence (A1: +// `ParseTree = Node`). Non-empty tokens against G0 ⇒ `Rejected` +// (tokens unconsumed). Empty tokens against non-G0 grammar ⇒ not realized +// until additional productions are ratified in data. +// +// PARSE-1 bodiless-`fn` remains a **grammar-data** obligation on the +// LanguageModel file, not a special case in this walker (see header in +// `extdeps/languages/dag.dag`). // // Owns: -// - Grammar — declarative syntactic authority as a finite `Node` tree -// - ParseTree — surface syntax tree prior to normalize (carrier = `Node`) -// - parse: (TokenStream, Grammar) -> Outcome -// (DECISIONS.md **I**) +// - Grammar, ParseTree (= Node), parse: (TokenStream, Grammar) -> Outcome // // Consumes: -// - std/node.dag: Node, Symbol, node_well_formed -// - std/diagnostic.dag: Diagnostic, Outcome, Locus, Correction, +// - std/node.dag: Node, NodeKind, TypeNode, ComputationNode, Connective, +// Conj, Symbol, node_well_formed +// - std/diagnostic.dag: Diagnostic, Outcome, Locus, PortLocus, Correction, // NoCorrectionReason // - compiler/01_tokenize.dag: TokenStream -// - extdeps/languages/dag.dag: language-#1 `DagLanguageModel.grammar` -// authority (B2-OMNI + PARSE-1 — data-carried, not walker-special-cased) // -// Status: Wave-1 generic machinery — syntactic **walk** not realized on -// the v2 bridge (honest `Rejected`); PARSE-1 bodiless-fn production is a -// constraint on `DagLanguageModel.grammar` **data** in `extdeps/languages/dag.dag`, -// not encoded in this generic walker. +// Status: Wave-1 — G0 void-grammar + empty tokens path **realized**; else +// honest `Rejected` per encoding coverage. // Brief: see BRIEF_TEMPLATE.md; this file's I/O contract is the immutable // contract for the worker. Splitting this file requires explicit operator // ratification (substrate extension = stop signal). @@ -69,31 +48,34 @@ import v4.std.diagnostic { Locus, NoCorrectionReason, Outcome, + PortLocus, +} +import v4.std.node { + ComputationNode, + Conj, + Connective, + Node, + NodeKind, + Symbol, + TypeNode, + node_well_formed, } -import v4.std.node { Node, Symbol, node_well_formed } -// ───────────────────────────────────────────────────────────────────── -// Grammar — declarative syntactic specification as a finite `Node` tree -// (B2-OMNI). Productions (including PARSE-1 bodiless signature rows) are -// DATA in the LanguageModel instance, never special-cased here. type Grammar = Node -// ───────────────────────────────────────────────────────────────────── -// ParseTree — stage-2 output; the syntax tree is a `Node` forest spine -// (A1) until normalize dissolves sugar (T-8). type ParseTree = Node -// ───────────────────────────────────────────────────────────────────── -// Reason symbols — owned by this dimension (diagnostic.dag owns schema). data parse_stage_locus_port: Symbol = parse_stage_locus_port data parse_walk_not_realized: Symbol = parse_walk_not_realized data parse_grammar_not_well_formed: Symbol = parse_grammar_not_well_formed +data parse_g0_tokens_remain: Symbol = parse_g0_tokens_remain + fn parse_walk_not_realized_diagnostic(at: Locus) -> Diagnostic { Diagnostic { @@ -113,26 +95,54 @@ fn parse_grammar_not_well_formed_diagnostic(at: Locus) -> Diagnostic { } +fn parse_g0_tokens_remain_diagnostic(at: Locus) -> Diagnostic { + Diagnostic { + reason: parse_g0_tokens_remain, + at: at, + correction: Unavailable { reason: ExternalContractUnknown } + } +} + + +// ───────────────────────────────────────────────────────────────────── +// grammar_node_is_conj_empty_root — structural G0 predicate (Wave-1). +fn grammar_node_is_conj_empty_root(g: Node) -> Bool { + match g.kind { + TypeNode { connective: Conj } => count(g.children) == 0 + TypeNode { connective: _ } => false + ComputationNode { behavior: _ } => false + } +} + + // ───────────────────────────────────────────────────────────────────── // parse — GENERIC syntactic ingest (B2-OMNI). -// -// `grammar` is the only syntactic authority. `tokens` is threaded so the -// entry point composes with stage 1; there is no token-shape hardcoding -// beyond the shared `TokenStream` carrier. Bridge-era note: the full -// walk is not executed in the v2 seed — fail-closed `Rejected` until the -// walker lowers. fn parse(tokens: TokenStream, grammar: Grammar) -> Outcome { let at = PortLocus { port: parse_stage_locus_port } - let _toks = tokens.tokens - if node_well_formed(n: grammar) { + let ntok = count(tokens.tokens) + if !node_well_formed(n: grammar) { + Rejected { + diagnostic: parse_grammar_not_well_formed_diagnostic(at: at) + } + } else if grammar_node_is_conj_empty_root(g: grammar) { + if ntok == 0 { + Produced { + value: grammar + } + } else { + Rejected { + diagnostic: parse_g0_tokens_remain_diagnostic(at: at) + } + } + } else if ntok == 0 { Rejected { diagnostic: parse_walk_not_realized_diagnostic(at: at) } } else { Rejected { - diagnostic: parse_grammar_not_well_formed_diagnostic(at: at) + diagnostic: parse_walk_not_realized_diagnostic(at: at) } } } diff --git a/src/v4/extdeps/languages/dag.dag b/src/v4/extdeps/languages/dag.dag index a9c2620a8a4..c60e55534cb 100644 --- a/src/v4/extdeps/languages/dag.dag +++ b/src/v4/extdeps/languages/dag.dag @@ -54,7 +54,7 @@ module v4.extdeps.languages.dag -import v4.std.node { Node } +import v4.std.node { Conj, Node, NodeKind, TypeNode } // ───────────────────────────────────────────────────────────────────── @@ -66,3 +66,38 @@ type DagLanguageModel { lex: Node grammar: Node } + + +// ───────────────────────────────────────────────────────────────────── +// Wave-1 **E0 / G0** canonical roots — zero-production `Conj` leaves. +// +// These are the **data** instances `compiler/01_tokenize.dag` and +// `compiler/02_parse.dag` recognize structurally (empty `TypeNode{Conj}` +// child list). They are not special-cased in the walkers beyond that +// shared shape; any LanguageModel may reuse E0/G0 for empty fragments. +fn dag_wave1_e0_void_lex() -> Node { + Node { + kind: TypeNode { + connective: Conj + }, + children: [] + } +} + + +fn dag_wave1_g0_void_grammar() -> Node { + Node { + kind: TypeNode { + connective: Conj + }, + children: [] + } +} + + +fn dag_language_model_wave1_void() -> DagLanguageModel { + DagLanguageModel { + lex: dag_wave1_e0_void_lex(), + grammar: dag_wave1_g0_void_grammar() + } +} From 39335bc3a8e5c9732e6d5668c2262d6a0890acaf Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Sat, 16 May 2026 22:20:04 +0000 Subject: [PATCH 5/9] feat(v4): Wave-1 generic tokenize/parse walkers for E0/G0 void rule encodings Implement structural walks over declarative Node-shaped LexRules/Grammar: empty TypeNode{Conj} roots with token/stream and String=FreeMonoid emptiness. Produced paths battle-test the Outcome/TokenStream/ParseTree seam; non-covered encodings fail closed without v2/v3 seed changes. Co-authored-by: Cursor --- src/v4/compiler/01_tokenize.dag | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/v4/compiler/01_tokenize.dag b/src/v4/compiler/01_tokenize.dag index 6ed27fbe86b..154e44845a6 100644 --- a/src/v4/compiler/01_tokenize.dag +++ b/src/v4/compiler/01_tokenize.dag @@ -28,8 +28,8 @@ // // Consumes: // - std/text.dag: String (= FreeMonoid) -// - std/node.dag: Node, NodeKind, TypeNode, ComputationNode, Connective, -// Conj, Symbol, node_well_formed +// - std/node.dag: Node, NodeKind, TypeNode, ComputationNode, Conj, +// Symbol, node_well_formed // - std/collection.dag: List // - std/diagnostic.dag: Diagnostic, Outcome, Locus, Textual, WholeFile, // Correction, NoCorrectionReason From 7bb5595b73813dd4617b8e433200409f98edefb5 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Sat, 16 May 2026 18:21:17 -0400 Subject: [PATCH 6/9] =?UTF-8?q?WIP:=20CP-1a=20=E2=80=94=20v4=20front-end?= =?UTF-8?q?=20tokenize/parse=20+=20declarative=20grammar-as-data?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- src/v4/compiler/02_parse.dag | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/v4/compiler/02_parse.dag b/src/v4/compiler/02_parse.dag index f5118b7f3d2..dadcf246ca9 100644 --- a/src/v4/compiler/02_parse.dag +++ b/src/v4/compiler/02_parse.dag @@ -25,8 +25,8 @@ // - Grammar, ParseTree (= Node), parse: (TokenStream, Grammar) -> Outcome // // Consumes: -// - std/node.dag: Node, NodeKind, TypeNode, ComputationNode, Connective, -// Conj, Symbol, node_well_formed +// - std/node.dag: Node, NodeKind, TypeNode, ComputationNode, Conj, +// Symbol, node_well_formed // - std/diagnostic.dag: Diagnostic, Outcome, Locus, PortLocus, Correction, // NoCorrectionReason // - compiler/01_tokenize.dag: TokenStream From a26be3e01c4a32e53e20f593137178531ffc0f9d Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Sat, 16 May 2026 22:38:36 +0000 Subject: [PATCH 7/9] fix(v4): address claude-opus PR review on tokenize/parse - Collapse duplicate parse branches that both emitted walk_not_realized. - Align 01_tokenize header Consumes with std/algebra FreeMonoid import. - Use UserInputBoundary for E0/G0 model-vs-input mismatch diagnostics; keep ExternalContractUnknown for not-yet-realized walker paths. - Drop unused Connective / NoCorrectionReason imports in 02_parse. Co-authored-by: Cursor --- src/v4/compiler/01_tokenize.dag | 10 ++++++---- src/v4/compiler/02_parse.dag | 12 ++++-------- 2 files changed, 10 insertions(+), 12 deletions(-) diff --git a/src/v4/compiler/01_tokenize.dag b/src/v4/compiler/01_tokenize.dag index 154e44845a6..6fd564cdd77 100644 --- a/src/v4/compiler/01_tokenize.dag +++ b/src/v4/compiler/01_tokenize.dag @@ -27,12 +27,13 @@ // - tokenize: (String, file: Symbol, LexRules) -> Outcome // // Consumes: -// - std/text.dag: String (= FreeMonoid) +// - std/text.dag: String (= FreeMonoid alias; see std/algebra.dag) +// - std/algebra.dag: FreeMonoid (spine walk for `string_is_empty`) // - std/node.dag: Node, NodeKind, TypeNode, ComputationNode, Conj, // Symbol, node_well_formed // - std/collection.dag: List // - std/diagnostic.dag: Diagnostic, Outcome, Locus, Textual, WholeFile, -// Correction, NoCorrectionReason +// Correction, ExternalContractUnknown, UserInputBoundary // - extdeps/languages/dag.dag: language-#1 model binds E0 instances (see // `dag_wave1_e0_void_lex`); this file stays encoding-generic. // @@ -50,10 +51,11 @@ import v4.std.collection { List } import v4.std.diagnostic { Correction, Diagnostic, + ExternalContractUnknown, Locus, - NoCorrectionReason, Outcome, Textual, + UserInputBoundary, WholeFile, } import v4.std.algebra { FreeMonoid } @@ -124,7 +126,7 @@ fn tokenize_lex_e0_source_not_exhausted_diagnostic(at: Locus) -> Diagnostic { Diagnostic { reason: tokenize_lex_e0_source_not_exhausted, at: at, - correction: Unavailable { reason: ExternalContractUnknown } + correction: Unavailable { reason: UserInputBoundary } } } diff --git a/src/v4/compiler/02_parse.dag b/src/v4/compiler/02_parse.dag index dadcf246ca9..4a6bf7958b5 100644 --- a/src/v4/compiler/02_parse.dag +++ b/src/v4/compiler/02_parse.dag @@ -28,7 +28,7 @@ // - std/node.dag: Node, NodeKind, TypeNode, ComputationNode, Conj, // Symbol, node_well_formed // - std/diagnostic.dag: Diagnostic, Outcome, Locus, PortLocus, Correction, -// NoCorrectionReason +// ExternalContractUnknown, UserInputBoundary // - compiler/01_tokenize.dag: TokenStream // // Status: Wave-1 — G0 void-grammar + empty tokens path **realized**; else @@ -45,15 +45,15 @@ import v4.compiler.tokenize { TokenStream } import v4.std.diagnostic { Correction, Diagnostic, + ExternalContractUnknown, Locus, - NoCorrectionReason, Outcome, PortLocus, + UserInputBoundary, } import v4.std.node { ComputationNode, Conj, - Connective, Node, NodeKind, Symbol, @@ -99,7 +99,7 @@ fn parse_g0_tokens_remain_diagnostic(at: Locus) -> Diagnostic { Diagnostic { reason: parse_g0_tokens_remain, at: at, - correction: Unavailable { reason: ExternalContractUnknown } + correction: Unavailable { reason: UserInputBoundary } } } @@ -136,10 +136,6 @@ fn parse(tokens: TokenStream, grammar: Grammar) -> Outcome { diagnostic: parse_g0_tokens_remain_diagnostic(at: at) } } - } else if ntok == 0 { - Rejected { - diagnostic: parse_walk_not_realized_diagnostic(at: at) - } } else { Rejected { diagnostic: parse_walk_not_realized_diagnostic(at: at) From da6d8a18d01bce675bd1f726a5c62c3a9b11c180 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Sat, 16 May 2026 19:07:48 -0400 Subject: [PATCH 8/9] =?UTF-8?q?WIP:=20CP-1a=20=E2=80=94=20v4=20front-end?= =?UTF-8?q?=20tokenize/parse=20+=20declarative=20grammar-as-data?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- src/v4/std/text.dag | 14 ++++++++++++++ 1 file changed, 14 insertions(+) diff --git a/src/v4/std/text.dag b/src/v4/std/text.dag index 6deb9599353..9920292f5c7 100644 --- a/src/v4/std/text.dag +++ b/src/v4/std/text.dag @@ -111,3 +111,17 @@ type Char = Nat // reads of std/algebra.dag's `FreeMonoid` shape, not operations // re-declared in this file. type String = FreeMonoid + + +// ───────────────────────────────────────────────────────────────────── +// string_is_empty — canonical **boundary query** for `String`. +// +// `String` is `FreeMonoid` (alias edge above). Emptiness is the +// structural discriminant on that carrier — a read of std/algebra.dag's +// `Empty | Cons` spine, not a tokenizer-local length re-implementation. +fn string_is_empty(s: String) -> Bool { + match s { + Empty => true + Cons { head: _, tail: _ } => false + } +} From c1313bfbf4c1f66fcb4d3ccbce7f2b347f44ccd4 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Sat, 16 May 2026 23:09:15 +0000 Subject: [PATCH 9/9] fix(v4): expose FreeMonoid boundary queries in std algebra Tokenizer E0 no longer walks Empty|Cons locally; it imports string_is_empty from text.dag, which delegates to algebra free_monoid_is_empty (M9/P2). Co-authored-by: Cursor --- src/v4/compiler/01_tokenize.dag | 26 ++++---------------------- src/v4/std/algebra.dag | 26 +++++++++++++++++++++++++- src/v4/std/text.dag | 13 +++++-------- 3 files changed, 34 insertions(+), 31 deletions(-) diff --git a/src/v4/compiler/01_tokenize.dag b/src/v4/compiler/01_tokenize.dag index 6fd564cdd77..1ff6d4ec3ad 100644 --- a/src/v4/compiler/01_tokenize.dag +++ b/src/v4/compiler/01_tokenize.dag @@ -14,7 +14,7 @@ // whose connective is **`Conj` with zero children** — exactly zero // lexical productions. The walker recognizes this shape **structurally** // (discriminant + `count(children)==0`), never by `Symbol` spelling. -// E0 + empty `String` (`FreeMonoid` spine `Empty`) ⇒ `Produced` empty +// E0 + empty `String` (`std/text.dag` `string_is_empty`) ⇒ `Produced` empty // `TokenStream`. E0 + non-empty source ⇒ `Rejected` (source not exhausted // — fail-closed; no fabricated tokens). // Further encodings (E1+, keywords, …) land as additional **data** @@ -27,8 +27,8 @@ // - tokenize: (String, file: Symbol, LexRules) -> Outcome // // Consumes: -// - std/text.dag: String (= FreeMonoid alias; see std/algebra.dag) -// - std/algebra.dag: FreeMonoid (spine walk for `string_is_empty`) +// - std/text.dag: String, string_is_empty (= FreeMonoid boundary; +// see std/algebra.dag `free_monoid_is_empty`) // - std/node.dag: Node, NodeKind, TypeNode, ComputationNode, Conj, // Symbol, node_well_formed // - std/collection.dag: List @@ -58,7 +58,6 @@ import v4.std.diagnostic { UserInputBoundary, WholeFile, } -import v4.std.algebra { FreeMonoid } import v4.std.node { ComputationNode, Conj, @@ -68,7 +67,7 @@ import v4.std.node { TypeNode, node_well_formed, } -import v4.std.text { Char, String } +import v4.std.text { Char, String, string_is_empty } // ───────────────────────────────────────────────────────────────────── @@ -131,23 +130,6 @@ fn tokenize_lex_e0_source_not_exhausted_diagnostic(at: Locus) -> Diagnostic { } -// ───────────────────────────────────────────────────────────────────── -// free_monoid_char_len — walk the `FreeMonoid` spine (`String` alias). -fn free_monoid_char_len(xs: FreeMonoid) -> Int { - match xs { - Empty => 0 - Cons { head: _, tail: t } => 1 + free_monoid_char_len(xs: t) - } -} - - -// ───────────────────────────────────────────────────────────────────── -// string_is_empty — `String` = `FreeMonoid` (std/text.dag). -fn string_is_empty(s: String) -> Bool { - free_monoid_char_len(xs: s) == 0 -} - - // ───────────────────────────────────────────────────────────────────── // lex_rules_node_is_conj_empty_root — structural E0 predicate (Wave-1). fn lex_rules_node_is_conj_empty_root(rules: Node) -> Bool { diff --git a/src/v4/std/algebra.dag b/src/v4/std/algebra.dag index 2040cf17d1b..e54800eeca9 100644 --- a/src/v4/std/algebra.dag +++ b/src/v4/std/algebra.dag @@ -14,7 +14,9 @@ // associativity/distributivity, so Float is NOT an exact Field; // see std/float.dag + DECISIONS.md C5-fidelity) // * BooleanAlgebra (classical logic) -// * FreeMonoid (free constructions) +// * FreeMonoid (free constructions) + structural boundary +// queries (`free_monoid_is_empty`, `free_monoid_length`) over +// its declared Empty|Cons carrier // * PointwisePower (power-set / characteristic-function carrier // whose BooleanAlgebra structure is inherited pointwise from Bool) // The "roots" (Magma/Monoid/BooleanAlgebra/FreeMonoid) are where the @@ -333,6 +335,28 @@ type FreeMonoid | Cons { head: T, tail: FreeMonoid } +// ───────────────────────────────────────────────────────────────────── +// FreeMonoid boundary queries (M9/P2). +// +// Declared structural reads over the terminal Empty|Cons carrier. Every +// consumer (e.g. std/text.dag for `String = FreeMonoid`) imports +// these instead of re-encoding the spine in a downstream module. +fn free_monoid_is_empty(xs: FreeMonoid) -> Bool { + match xs { + Empty => true + Cons { head: _, tail: _ } => false + } +} + + +fn free_monoid_length(xs: FreeMonoid) -> Int { + match xs { + Empty => 0 + Cons { head: _, tail: t } => 1 + free_monoid_length(xs: t) + } +} + + // ───────────────────────────────────────────────────────────────────── // PointwisePower — the power-set / characteristic-function carrier // over T. A value is a predicate T → Bool; BooleanAlgebra operations are diff --git a/src/v4/std/text.dag b/src/v4/std/text.dag index 9920292f5c7..5eb3871f5c2 100644 --- a/src/v4/std/text.dag +++ b/src/v4/std/text.dag @@ -50,7 +50,7 @@ module v4.std.text -import v4.std.algebra { FreeMonoid } +import v4.std.algebra { FreeMonoid, free_monoid_is_empty } import v4.std.nat { Nat } @@ -116,12 +116,9 @@ type String = FreeMonoid // ───────────────────────────────────────────────────────────────────── // string_is_empty — canonical **boundary query** for `String`. // -// `String` is `FreeMonoid` (alias edge above). Emptiness is the -// structural discriminant on that carrier — a read of std/algebra.dag's -// `Empty | Cons` spine, not a tokenizer-local length re-implementation. +// `String` is `FreeMonoid` (alias edge above). Emptiness is +// std/algebra.dag's `free_monoid_is_empty` on that carrier — not a +// per-consumer spine walk. fn string_is_empty(s: String) -> Bool { - match s { - Empty => true - Cons { head: _, tail: _ } => false - } + free_monoid_is_empty(xs: s) }