Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
26 changes: 11 additions & 15 deletions docs/audit/dissolution-inventory.md
Original file line number Diff line number Diff line change
Expand Up @@ -332,19 +332,15 @@ follow-up.** The two functions surfaced as #3225's un-cleared codex
REQUEST_CHANGES findings (threads `3255338394` / `3255338395`) are
captured here as the audit anchor for the rest:

- `merge_binding_self` (94) — 🟡 **walker** (the "sym↦sym module harvest"
codex finding). The leaf helper is `map_insert(m, sym, sym)`, but it
is the symbolic-merge primitive used inside three named-harvest
walkers (`add_module_named_exports` at 99, `add_arrow_domain_named_params`
at 113, `add_bind_atom_binder` at 140) — all three are `fold` over
`Node.children` doing constructor-discriminated recursion.
**Substrate dependency satisfied (PR #3297):** `fold_node` exists in
`std/node.dag`. These four sites are the **P5 cascade** — they still
need a scoped binding-harvest `NodeFold<Map<Symbol, Symbol>>` (or
equivalent) that preserves resolver scope semantics; not a repeat
T-1 substrate-extension PR. Dissolves to `fold_node(root, ⟨algebra⟩)`
over that algebra; eliminates the three harvest walkers plus the
implicit recursion in `merge_binding_self`'s callers.
- `merge_binding_self` (94) — 🟢 **DISSOLVED 2026-05-19.** The "sym↦sym"
leaf helper is gone. The three binding-harvest sites
(`add_module_named_exports`, `add_arrow_domain_named_params`,
`add_bind_atom_binder`) now consume scoped `NodeFold<Map<Symbol, Symbol>>`
algebras (`direct_named_edge_binding_fold`, `direct_atom_binding_fold`)
through `fold_node`. The algebras ignore child fold results where the
resolver contract requires direct children only, preserving module,
arrow-domain, and arity-3 `Bind` scope semantics while deleting the
local `Node.children` folds.

- The other 22 fns in 03_resolve.dag (`empty_namespace`,
`empty_canonical_symbol_set`, `build_program_namespace`,
Expand Down Expand Up @@ -777,7 +773,7 @@ work, not C1's** — C1 marks and flags.

| class | 🔴 dissolve-now | 🟡 gated (named feature: / consumer:) | 🟢 terminal |
|---|---|---|---|
| walker | — | 2 (`std/algebra.dag free_monoid_length` → `fold FreeMonoid`; `std/float.dag nat_compare` → `fold Nat`) + **P5 cascade** (`compiler/03_resolve.dag` binding-harvest sites → scoped `fold_node` algebra; substrate **#3297**) | rest |
| walker | — | 2 (`std/algebra.dag free_monoid_length` → `fold FreeMonoid`; `std/float.dag nat_compare` → `fold Nat`) | rest; **P5 cascade closed** (`compiler/03_resolve.dag` binding-harvest sites consume scoped `fold_node` algebra; substrate **#3297**) |
| traverse | — | 4 (`std/node.dag` × 4: → `forall` / `count_where` / `unique` over `FreeMonoid<T>` in `std/collection.dag` Wave-A2) | rest |
| predicate | empty-`Conj` R1 predicate **landed** PR #3284 (`std/node.dag` `is_empty_conj_root`, `DECISIONS.md` §CP-1b item 12); LLVM R2 predicate **landed** PR #3245 (`terminator_is_catchswitch` deleted; `block_well_formed` consumes `CatchSwitch` directly) | 3 (`std/node.dag connective_edge_discipline` → per-`Connective` discipline fact; `std/float.dag float_finite_magnitude_zero` → `nat_is_zero`; `extdeps/languages/llvm_ir.dag feature_disposition` → per-feature disposition fact (T-4 fact-bundle)); `llvm_instruction_cost` **landed** under `lens/cost.dag`. | rest |
| carrier | — | — | lane-wide |
Expand All @@ -788,7 +784,7 @@ work, not C1's** — C1 marks and flags.
dissolve-on-arrival rule):

1. ~~`fold_node` — `Node` catamorphism in `std/node.dag` (substrate-extension
under T-1).~~ **LANDED PR #3297** (`NodeFold<R>`, `fold_node`; `node_well_formed` is a consumer). **P5 cascade** (binding-harvest in `03_resolve.dag`) remains open under a scoped algebra, not absent substrate.
under T-1).~~ **LANDED PR #3297** (`NodeFold<R>`, `fold_node`; `node_well_formed` is a consumer). **P5 cascade closed 2026-05-19:** binding-harvest in `03_resolve.dag` consumes scoped `NodeFold<Map<Symbol, Symbol>>` algebras.
2. `fold` / `cata` over `FreeMonoid<T>` and `Nat` in `std/algebra.dag` /
`std/nat.dag` (Wave-A2).
3. `forall`, `count_where`, `unique` over `FreeMonoid<T>` in
Expand Down
8 changes: 5 additions & 3 deletions src/v4/DECISIONS.md
Original file line number Diff line number Diff line change
Expand Up @@ -200,9 +200,9 @@ consumes that derived fact.

4. **`SurfaceSugarKind` (`compiler/03_normalize.dag`):** **Classification — 🟡 YELLOW (scaffold):** T-8 normalize seam; not a terminal substrate primitive while the stage is scaffold. **Dissolution pattern — enumerated axis (closed N=4):** names the four C3 surface-sugar connectives aligned with the `data dag_c3_surface_sugar_*` identities in `extdeps/languages/dag.dag` (THESIS/C3; not a foreign-label consumer coproduct). **Named triggers:** `classify_sugar`; feeds `normalize_node` / `malformed_sugar_diagnostic`.

5. **`SugarClassification` (`compiler/03_normalize.dag`):** **Classification — 🟡 YELLOW (scaffold).** **Dissolution pattern — partition:** `Sugar` vs `NotSugar` splits the normalize walk between C3-shaped sugar and pass-through `Node` kinds. **Named triggers:** `classify_sugar`; `normalize_node`; `normalize_edge`.
5. **`SugarClassification` (`compiler/03_normalize.dag`):** **DISSOLVED 2026-05-19.** The local `Sugar | NotSugar` carrier was replaced by the existing optional carrier: `classify_sugar(n) -> SurfaceSugarKind?`. The remaining `SurfaceSugarKind` axis is item 4; absence is now the canonical `None` branch, not a second stage-local coproduct.

6. **`NormalizeChildrenResult` (`compiler/03_normalize.dag`):** **Classification — 🟡 YELLOW (scaffold).** **Dissolution pattern — success-or-Diagnostic carrier:** `NormalizedChildren` vs `NormalizeChildrenRejected` threads child recursion fail-closed without a second authority. **Named triggers:** `normalize_children`; `normalize_edge` / `normalize_node` folds.
6. **`NormalizeChildrenResult` (`compiler/03_normalize.dag`):** **DISSOLVED 2026-05-19.** The local success-or-diagnostic carrier was replaced by the canonical `Outcome<List<Edge>>` from `std/diagnostic.dag`; `normalize_children`, `normalize_edge`, and `normalize_node` now share the same fail-closed carrier.

7. **`Scope` (`compiler/03_resolve.dag`):** **Classification — 🟡 YELLOW (scaffold).** **Dissolution pattern — structured lexical environment:** `ScopeRoot` (module `Namespace`) vs `ScopeFrame` (locals + outer) for K-1 use→def binding (B-4; Part 1 **B-4** row). **Named triggers:** `resolve_node`; `resolve_atom`; `resolve_bind_*` family.

Expand All @@ -214,7 +214,9 @@ consumes that derived fact.

11. **`compiler/01_tokenize.dag` — `LexRules` / wave-1 E0 (T-6 / B2-OMNI; PR #3284 → T-8 spine update #3311):** lexical authority is the typed coproduct `LexRules = VoidLexRules | ModeledLexRules { root: LexRuleSet }`, with rule rows carried by `LexRule` payloads rather than ad-hoc `Node` variant tags. Each `TokenRule.pattern` is a bounded `LexPattern` regular-language carrier (`EmptyPattern`, literal/char/class atoms, sequence, choice, optional, repeat), not a raw `Node` bridge. Wave-1 E0 void lex is `VoidLexRules`. `ModeledLexRules` fail-closes with `tokenize_lexical_walk_not_realized` until the P3 lexical walk primitive lands; no hand-rolled walker is introduced. Rationale lives here per Practice 9; `01_tokenize.dag` carries no in-file rationale beyond the mandated terse header (path + Scope/Owns/Consumes/Status + optional `Anchor:`) and the one-line tags on the tokenize coproducts.

12. **`std/node.dag` — `is_empty_conj_root` (P5 / INVARIANTS §Progress Is Dissolution; codex PR #3284):** **Not a net-new `is_*` verifier** — this is the **landed R1 receipt** from `docs/audit/dissolution-inventory.md` §1.0: one structural query replaces three literal duplicate predicates (`compiler/01_tokenize.dag`, `compiler/02_parse.dag`, `extdeps/languages/dag.dag`). **Interim steady-state:** shared empty-`Conj`-root shape leg for wave-1 void LM / E0–G0 stubs until T-6/T-7 generic walks consume grammar-as-data without re-deriving this `match`. **Forward dissolution (named triggers):** (a) `fold_node` / `NodeFold` in `std/node.dag` is **landed** (dissolution-inventory **P5** substrate — PR #3297; `node_well_formed` is already a consumer). Optional follow-up: fold this discriminant into that catamorphism / shared query surface if a ratified consumer wants to shed the dedicated `match`. Remaining **P5** debt is the **`compiler/03_resolve.dag` binding-harvest cascade** (inventory §2.3), not absent substrate. (b) `feature: compiler pipeline-stage lex-walk + parse-walk substrate` (inventory **P3**, TASKS T-6/T-7) — grammar-as-data carries void-book as constructor-shaped facts so consumers discriminate on `NodeKind` / carriers instead of calling `is_empty_conj_root`. **Audit anchor:** inventory §1.0 row **R1** (status = landed PR #3284). **Api-review receipt (PR #3274):** duplicate-collapse / modeling-discipline Practice 5 single authority — not a parallel verification predicate. **INVARIANTS.md §P5 — Dispatch-Discipline Mechanisms (b)** SG-0 `EXPECTED_HAND_AUTHORED_*` census gates **new** `src/v3/compiler/tests/**` hand-Rust paths; they do **not** apply to this v4-only substrate `fn`. **Exhaustiveness:** `NodeKind` is the closed `TypeNode | ComputationNode` pair today; a third top-level variant would require updating every `match n.kind` in `std/node.dag`, including this helper, in the same substrate edit that extends `NodeKind`.
12. **`std/node.dag` — `is_empty_conj_root` (P5 / INVARIANTS §Progress Is Dissolution; codex PR #3284):** **Not a net-new `is_*` verifier** — this is the **landed R1 receipt** from `docs/audit/dissolution-inventory.md` §1.0: one structural query replaces three literal duplicate predicates (`compiler/01_tokenize.dag`, `compiler/02_parse.dag`, `extdeps/languages/dag.dag`). **Interim steady-state:** shared empty-`Conj`-root shape leg for wave-1 void LM / E0–G0 stubs until T-6/T-7 generic walks consume grammar-as-data without re-deriving this `match`. **Forward dissolution (named triggers):** (a) `fold_node` / `NodeFold` in `std/node.dag` is **landed** (dissolution-inventory **P5** substrate — PR #3297; `node_well_formed` is already a consumer). Optional follow-up: fold this discriminant into that catamorphism / shared query surface if a ratified consumer wants to shed the dedicated `match`; the separate `compiler/03_resolve.dag` binding-harvest cascade that depended on the same substrate is closed in item 12a. (b) `feature: compiler pipeline-stage lex-walk + parse-walk substrate` (inventory **P3**, TASKS T-6/T-7) — grammar-as-data carries void-book as constructor-shaped facts so consumers discriminate on `NodeKind` / carriers instead of calling `is_empty_conj_root`. **Audit anchor:** inventory §1.0 row **R1** (status = landed PR #3284). **Api-review receipt (PR #3274):** duplicate-collapse / modeling-discipline Practice 5 single authority — not a parallel verification predicate. **INVARIANTS.md §P5 — Dispatch-Discipline Mechanisms (b)** SG-0 `EXPECTED_HAND_AUTHORED_*` census gates **new** `src/v3/compiler/tests/**` hand-Rust paths; they do **not** apply to this v4-only substrate `fn`. **Exhaustiveness:** `NodeKind` is the closed `TypeNode | ComputationNode` pair today; a third top-level variant would require updating every `match n.kind` in `std/node.dag`, including this helper, in the same substrate edit that extends `NodeKind`.

12a. **`compiler/03_resolve.dag` — binding-harvest cascade (P5):** **DISSOLVED 2026-05-19.** The local `merge_binding_self` leaf plus three direct child walkers (`add_module_named_exports`, `add_arrow_domain_named_params`, `add_bind_atom_binder`) now route through scoped `NodeFold<Map<Symbol, Symbol>>` algebras: `direct_named_edge_binding_fold` for direct `Conj` named-edge harvest and `direct_atom_binding_fold` for the arity-3 `Bind` binder slot. The algebras intentionally ignore child fold results where resolver scope semantics require direct children only; the recursion surface is the canonical `fold_node` substrate primitive, not hand recursion over `Node.children`.

13a. **`LexCharClass` (`compiler/01_tokenize.dag`):** **Classification — 🟡 YELLOW (P3-gated declarative seam).** **Dissolution pattern — closed character-class vocabulary:** variants name the lexical character classes the future T-6 walk consumes. **Named triggers:** `feature:T-6`; consumed by `LexPattern.CharClassPattern`.

Expand Down
61 changes: 32 additions & 29 deletions src/v4/compiler/03_normalize.dag
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
// src/v4/compiler/03_normalize.dag
//
// Scope: Stage 3a — ParseTree→NormalizedTree; C3 sugar to Node.
// Owns: NormalizedTree; SurfaceSugarKind; SugarClassification; normalize; stage Symbol reasons.
// Owns: NormalizedTree; SurfaceSugarKind; normalize; stage Symbol reasons.
// Consumes: std/node.dag, std/diagnostic.dag, compiler/02_parse.dag, extdeps/languages/dag.dag.
// Status: scaffold — TASKS T-8.
// Anchor: https://en.wikipedia.org/wiki/Abstract_syntax_tree
Expand Down Expand Up @@ -48,34 +48,38 @@ type SurfaceSugarKind
| OperationSugar


// 🟡 coproduct dissolution — DECISIONS.md CP-1b item 5 (SugarClassification)
type SugarClassification
= Sugar { kind: SurfaceSugarKind }
| NotSugar
fn some_surface_sugar_kind(kind: SurfaceSugarKind) -> SurfaceSugarKind? {
Some { value: kind }
}


fn no_surface_sugar_kind() -> SurfaceSugarKind? {
None
}


fn classify_sugar(n: Node) -> SugarClassification {
fn classify_sugar(n: Node) -> SurfaceSugarKind? {
match n.kind {
TypeNode { connective: Atom { identity: id } } =>
if id == dag_c3_surface_sugar_service {
Sugar { kind: ServiceSugar }
some_surface_sugar_kind(kind: ServiceSugar)
} else {
if id == dag_c3_surface_sugar_fn {
Sugar { kind: FnSugar }
some_surface_sugar_kind(kind: FnSugar)
} else {
if id == dag_c3_surface_sugar_type {
Sugar { kind: TypeSugar }
some_surface_sugar_kind(kind: TypeSugar)
} else {
if id == dag_c3_surface_sugar_operation {
Sugar { kind: OperationSugar }
some_surface_sugar_kind(kind: OperationSugar)
} else {
NotSugar
no_surface_sugar_kind()
}
}
}
}
TypeNode { connective: _ } => NotSugar
ComputationNode { behavior: _ } => NotSugar
TypeNode { connective: _ } => no_surface_sugar_kind()
ComputationNode { behavior: _ } => no_surface_sugar_kind()
}
}

Expand Down Expand Up @@ -117,25 +121,24 @@ fn normalize_edge(e: Edge) -> Outcome<Edge> {
}


// 🟡 coproduct dissolution — DECISIONS.md CP-1b item 6 (NormalizeChildrenResult)
type NormalizeChildrenResult
= NormalizedChildren { children: List<Edge> }
| NormalizeChildrenRejected { diagnostic: Diagnostic }
fn empty_normalized_children() -> Outcome<List<Edge>> {
Produced { value: Empty }
}


fn normalize_children(children: List<Edge>) -> NormalizeChildrenResult {
fold(children, init: NormalizedChildren { children: [] }, f: fn(acc, e) {
fn normalize_children(children: List<Edge>) -> Outcome<List<Edge>> {
fold(children, init: empty_normalized_children(), f: fn(acc, e) {
match acc {
NormalizeChildrenRejected { diagnostic: d } =>
NormalizeChildrenRejected { diagnostic: d }
NormalizedChildren { children: done } =>
Rejected { diagnostic: d } =>
Rejected { diagnostic: d }
Produced { value: done } =>
match normalize_edge(e: e) {
Produced { value: normalized_edge } =>
NormalizedChildren {
children: list_push(done, normalized_edge)
Produced {
value: list_push(done, normalized_edge)
}
Rejected { diagnostic: d } =>
NormalizeChildrenRejected { diagnostic: d }
Rejected { diagnostic: d }
}
}
})
Expand Down Expand Up @@ -205,12 +208,12 @@ fn normalize_sugar(kind: SurfaceSugarKind, n: Node, children: List<Edge>) -> Out

fn normalize_node(n: Node) -> Outcome<Node> {
match normalize_children(children: n.children) {
NormalizeChildrenRejected { diagnostic: d } => Rejected { diagnostic: d }
NormalizedChildren { children: normalized_children } =>
Rejected { diagnostic: d } => Rejected { diagnostic: d }
Produced { value: normalized_children } =>
match classify_sugar(n: n) {
Sugar { kind: kind } =>
Some { value: kind } =>
normalize_sugar(kind: kind, n: n, children: normalized_children)
NotSugar =>
None =>
Produced {
value: Node {
kind: n.kind,
Expand Down
75 changes: 50 additions & 25 deletions src/v4/compiler/03_resolve.dag
Original file line number Diff line number Diff line change
Expand Up @@ -29,8 +29,10 @@ import v4.std.node {
Conj,
Edge,
Node,
NodeFold,
Symbol,
TypeNode,
fold_node,
node_well_formed
}

Expand Down Expand Up @@ -91,42 +93,69 @@ fn empty_canonical_symbol_set() -> Set<Symbol> {
}


fn merge_binding_self(m: Map<Symbol, Symbol>, sym: Symbol) -> Map<Symbol, Symbol> {
map_insert(m, sym, sym)
fn direct_named_edge_binding_fold(base: Map<Symbol, Symbol>) -> NodeFold<Map<Symbol, Symbol>> {
NodeFold {
init: fn(_) {
base
},
step: fn(acc, e, _) {
match e.label {
Named { name: sym } => map_insert(acc, sym, sym)
Positional => acc
}
}
}
}


fn add_module_named_exports(root: Node, acc: Map<Symbol, Symbol>) -> Map<Symbol, Symbol> {
fn direct_atom_binding_fold(base: Map<Symbol, Symbol>) -> NodeFold<Map<Symbol, Symbol>> {
NodeFold {
init: fn(n0) {
match n0.kind {
TypeNode { connective: Atom { identity: sym } } =>
map_insert(base, sym, sym)
_ => base
}
},
step: fn(acc, _, _) {
acc
}
}
}


fn harvest_conj_named_bindings(root: Node, acc: Map<Symbol, Symbol>) -> Map<Symbol, Symbol> {
match root.kind {
TypeNode { connective: Conj } =>
fold(root.children, init: acc, f: fn(acc2, e) {
match e.label {
Named { name: decl } => merge_binding_self(m: acc2, sym: decl)
Positional => acc2
}
})
fold_node(
n: root,
algebra: direct_named_edge_binding_fold(base: acc)
)
_ => acc
}
}


fn harvest_direct_atom_binding(root: Node, acc: Map<Symbol, Symbol>) -> Map<Symbol, Symbol> {
fold_node(
n: root,
algebra: direct_atom_binding_fold(base: acc)
)
}


fn add_module_named_exports(root: Node, acc: Map<Symbol, Symbol>) -> Map<Symbol, Symbol> {
harvest_conj_named_bindings(root: root, acc: acc)
}


fn add_arrow_domain_named_params(n: Node, acc: Map<Symbol, Symbol>) -> Map<Symbol, Symbol> {
match n.kind {
TypeNode { connective: Arrow } =>
if count(n.children) >= 1 {
match first(n.children) {
Some { value: e0 } =>
match e0.target.kind {
TypeNode { connective: Conj } =>
fold(e0.target.children, init: acc, f: fn(acc2, pe) {
match pe.label {
Named { name: param } =>
merge_binding_self(m: acc2, sym: param)
Positional => acc2
}
})
_ => acc
}
harvest_conj_named_bindings(root: e0.target, acc: acc)
None => acc
}
} else {
Expand All @@ -143,11 +172,7 @@ fn add_bind_atom_binder(n: Node, acc: Map<Symbol, Symbol>) -> Map<Symbol, Symbol
if count(n.children) == 3 {
match first(n.children) {
Some { value: e0 } =>
match e0.target.kind {
TypeNode { connective: Atom { identity: b } } =>
merge_binding_self(m: acc, sym: b)
_ => acc
}
harvest_direct_atom_binding(root: e0.target, acc: acc)
None => acc
}
} else {
Expand Down
Loading