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 111622eb503..1ff6d4ec3ad 100644 --- a/src/v4/compiler/01_tokenize.dag +++ b/src/v4/compiler/01_tokenize.dag @@ -9,18 +9,36 @@ // 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` (`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** +// shapes ratified with the LanguageModel carrier; the walker grows by +// `match` on those shapes, not by hardcoding `.dag` surface spellings. +// // 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 finite `Node` tree +// - tokenize: (String, file: Symbol, LexRules) -> Outcome // // Consumes: -// - std/text.dag: Char, String -// - std/diagnostic.dag: Diagnostic -// - std/witness.dag: Witness +// - 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 +// - std/diagnostic.dag: Diagnostic, Outcome, Locus, Textual, WholeFile, +// Correction, ExternalContractUnknown, UserInputBoundary +// - extdeps/languages/dag.dag: language-#1 model binds E0 instances (see +// `dag_wave1_e0_void_lex`); this file stays encoding-generic. // -// Status: scaffold — fill per TASKS.md T-6 +// 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). @@ -28,3 +46,130 @@ module v4.compiler.tokenize + +import v4.std.collection { List } +import v4.std.diagnostic { + Correction, + Diagnostic, + ExternalContractUnknown, + Locus, + Outcome, + Textual, + UserInputBoundary, + WholeFile, +} +import v4.std.node { + ComputationNode, + Conj, + Node, + NodeKind, + Symbol, + TypeNode, + node_well_formed, +} +import v4.std.text { Char, String, string_is_empty } + + +// ───────────────────────────────────────────────────────────────────── +// LexRules — declarative lexical specification as a finite `Node` tree +// (B2-OMNI grammar-as-data). +type LexRules = Node + + +// ───────────────────────────────────────────────────────────────────── +// Token — one classified lexeme in source order. +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 + +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 { + 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 } + } +} + + +fn tokenize_lex_e0_source_not_exhausted_diagnostic(at: Locus) -> Diagnostic { + Diagnostic { + reason: tokenize_lex_e0_source_not_exhausted, + at: at, + correction: Unavailable { reason: UserInputBoundary } + } +} + + +// ───────────────────────────────────────────────────────────────────── +// 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). +// +// 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) { + Rejected { + 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_lexical_walk_not_realized_diagnostic(at: at) + } + } +} diff --git a/src/v4/compiler/02_parse.dag b/src/v4/compiler/02_parse.dag index cd8bdd7aa33..4a6bf7958b5 100644 --- a/src/v4/compiler/02_parse.dag +++ b/src/v4/compiler/02_parse.dag @@ -3,50 +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: -// - ParseTree type -// - parse: (TokenStream, Grammar) -> Result -// (Grammar is declarative data from the LanguageModel, not code here) -// - grammar productions as Node trees +// - Grammar, ParseTree (= Node), parse: (TokenStream, Grammar) -> Outcome // // Consumes: -// - std/node.dag, std/diagnostic.dag, std/witness.dag +// - std/node.dag: Node, NodeKind, TypeNode, ComputationNode, Conj, +// Symbol, node_well_formed +// - std/diagnostic.dag: Diagnostic, Outcome, Locus, PortLocus, Correction, +// ExternalContractUnknown, UserInputBoundary // - compiler/01_tokenize.dag: TokenStream // -// Status: scaffold — fill per TASKS.md T-7 +// 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). @@ -54,3 +40,105 @@ module v4.compiler.parse + +import v4.compiler.tokenize { TokenStream } +import v4.std.diagnostic { + Correction, + Diagnostic, + ExternalContractUnknown, + Locus, + Outcome, + PortLocus, + UserInputBoundary, +} +import v4.std.node { + ComputationNode, + Conj, + Node, + NodeKind, + Symbol, + TypeNode, + node_well_formed, +} + + +type Grammar = Node + + +type ParseTree = Node + + +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 { + 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 } + } +} + + +fn parse_g0_tokens_remain_diagnostic(at: Locus) -> Diagnostic { + Diagnostic { + reason: parse_g0_tokens_remain, + at: at, + correction: Unavailable { reason: UserInputBoundary } + } +} + + +// ───────────────────────────────────────────────────────────────────── +// 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). +fn parse(tokens: TokenStream, grammar: Grammar) -> Outcome { + let at = PortLocus { + port: parse_stage_locus_port + } + 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 { + Rejected { + diagnostic: parse_walk_not_realized_diagnostic(at: at) + } + } +} diff --git a/src/v4/extdeps/languages/dag.dag b/src/v4/extdeps/languages/dag.dag new file mode 100644 index 00000000000..c60e55534cb --- /dev/null +++ b/src/v4/extdeps/languages/dag.dag @@ -0,0 +1,103 @@ +// 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 { Conj, Node, NodeKind, TypeNode } + + +// ───────────────────────────────────────────────────────────────────── +// 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 +} + + +// ───────────────────────────────────────────────────────────────────── +// 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() + } +} 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 6deb9599353..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 } @@ -111,3 +111,14 @@ 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 +// std/algebra.dag's `free_monoid_is_empty` on that carrier — not a +// per-consumer spine walk. +fn string_is_empty(s: String) -> Bool { + free_monoid_is_empty(xs: s) +}