Proof §1.2: extract desugar model (dissolve SurfaceSugarKind)

src/v4/compiler/03_normalize.dag

@@ -1,13 +1,13 @@
 // src/v4/compiler/03_normalize.dag
 //
 // Scope: Stage 3a — ParseTree→NormalizedTree; C3 sugar to Node.
-// Status: T-8 modeled — traversal on normalize_fold init/step; sugar classify/apply inline (model extraction in #4694).
+// Status: T-8 modeled — traversal on normalize_fold init/step; model in std/sugar.dag.
 // Anchor: https://en.wikipedia.org/wiki/Abstract_syntax_tree
 
 module v4.compiler.normalize
 
 import v4.std.algebra { list_snoc_item }
-import v4.std.collection { Absent, Present, optional_absent, optional_present }
+import v4.std.collection { Absent, Present }
 import v4.std.grammar { ParseTree }
 
 import v4.std.diagnostic {
@@ -23,72 +23,21 @@ import v4.std.diagnostic {
   rejected_with_pending
 }
 import v4.std.node {
-  Connective,
   Edge,
   Node,
   Symbol,
-  TypeNode,
-  is_positional,
-  all_edges_named,
-  all_edges_positional,
   node_rebuild,
   well_formed
 }
+import v4.std.sugar {
+  apply_sugar,
+  classify_sugar
+}
 
 type NormalizedTree = Node
 
-data normalize_reason_malformed_sugar: Symbol = normalize_reason_malformed_sugar
 data normalize_reason_post_normalize_not_well_formed: Symbol = normalize_reason_post_normalize_not_well_formed
 
-// 🟡 gated — feature:CP-1b-surface-sugar-language-model — bind TASKS.md T-8 / LanguageModel — dissolve-on: surface-to-kernel sugar mapping owned by language-model substrate facts, not compiler-local Atom identity comparison in classify_sugar; forbidden: persistent local SurfaceSugarKind taxonomy without structural LanguageModel carrier.
-type SurfaceSugarKind
-  = ServiceSugar
-  | FnSugar
-  | TypeSugar
-  | OperationSugar
-
-fn some_surface_sugar_kind(kind: SurfaceSugarKind) -> SurfaceSugarKind? {
-  optional_present(value: kind)
-}
-
-fn no_surface_sugar_kind() -> SurfaceSugarKind? {
-  optional_absent()
-}
-
-// 🟡 gated — feature:CP-1b-surface-sugar-language-model — bind TASKS.md T-8 — dissolve-on: classify_sugar reads modeled LanguageModel sugar facts; forbidden: Atom identity string/symbol comparison as permanent authority.
-fn classify_sugar(n: Node) -> SurfaceSugarKind? {
-  match n.kind {
-    TypeNode { connective: Atom { identity: id } } =>
-      if id == ^dag_c3_surface_sugar_service {
-        some_surface_sugar_kind(kind: ServiceSugar)
-      } else {
-        if id == ^dag_c3_surface_sugar_fn {
-          some_surface_sugar_kind(kind: FnSugar)
-        } else {
-          if id == ^dag_c3_surface_sugar_type {
-            some_surface_sugar_kind(kind: TypeSugar)
-          } else {
-            if id == ^dag_c3_surface_sugar_operation {
-              some_surface_sugar_kind(kind: OperationSugar)
-            } else {
-              no_surface_sugar_kind()
-            }
-          }
-        }
-      }
-    TypeNode { connective: _ } => no_surface_sugar_kind()
-    ComputationNode { behavior: _ } => no_surface_sugar_kind()
-  }
-}
-
-fn malformed_sugar_diagnostic(n: Node) -> Diagnostic {
-  Diagnostic {
-    reason: normalize_reason_malformed_sugar,
-    at: node_locus(node: n),
-    correction: Unavailable { reason: UserInputBoundary }
-  }
-}
-
 fn post_normalize_not_well_formed_diagnostic(n: Node) -> Diagnostic {
   Diagnostic {
     reason: normalize_reason_post_normalize_not_well_formed,
@@ -97,52 +46,6 @@ fn post_normalize_not_well_formed_diagnostic(n: Node) -> Diagnostic {
   }
 }
 
-fn type_node(connective: Connective, children: List<Edge>, n: Node) -> Node {
-  Node {
-    kind: TypeNode { connective: connective },
-    children: children,
-    occurrence_id: n.occurrence_id
-  }
-}
-
-fn normalize_sugar(kind: SurfaceSugarKind, n: Node, children: List<Edge>) -> Outcome<Node> {
-  match kind {
-    ServiceSugar =>
-      if all_edges_named(children: children) {
-        Accepted { value: type_node(connective: Conj, children: children, n: n), diagnostics: None }
-      } else {
-        Rejected { diagnostics: diagnostics_singleton(d: malformed_sugar_diagnostic(n: n)) }
-      }
-    FnSugar =>
-      if all_edges_positional(children: children) {
-        Accepted { value: type_node(connective: Arrow, children: children, n: n), diagnostics: None }
-      } else {
-        Rejected { diagnostics: diagnostics_singleton(d: malformed_sugar_diagnostic(n: n)) }
-      }
-    TypeSugar =>
-      if count(children) == 1 {
-        match children |> first {
-          Present { value: e0 } =>
-            if is_positional(e: e0) {
-              Accepted { value: e0.target, diagnostics: None }
-            } else {
-              Rejected { diagnostics: diagnostics_singleton(d: malformed_sugar_diagnostic(n: n)) }
-            }
-          Absent =>
-            Rejected { diagnostics: diagnostics_singleton(d: malformed_sugar_diagnostic(n: n)) }
-        }
-      } else {
-        Rejected { diagnostics: diagnostics_singleton(d: malformed_sugar_diagnostic(n: n)) }
-      }
-    OperationSugar =>
-      if all_edges_positional(children: children) {
-        Accepted { value: type_node(connective: Arrow, children: children, n: n), diagnostics: None }
-      } else {
-        Rejected { diagnostics: diagnostics_singleton(d: malformed_sugar_diagnostic(n: n)) }
-      }
-  }
-}
-
 fn normalize_fold_init(n: Node) -> Outcome<Node> {
   Accepted { value: node_rebuild(n: n, children: []), diagnostics: None }
 }
@@ -173,8 +76,8 @@ fn normalize_fold_step(acc: Outcome<Node>, edge: Edge, child: Outcome<Node>) ->
 
 fn normalize_sugar_finish(n: Node, folded: Node, cd: Diagnostics) -> Outcome<Node> {
   match classify_sugar(n: n) {
-    Present { value: kind } =>
-      match normalize_sugar(kind: kind, n: n, children: folded.children) {
+    Present { value: rule } =>
+      match apply_sugar(rule: rule, n: n, children: folded.children) {
         Rejected { diagnostics: r } =>
           Rejected {
             diagnostics: rejected_with_pending(pending: cd, rejected: r)

src/v4/std/sugar.dag

@@ -0,0 +1,151 @@
+// src/v4/std/sugar.dag
+// Scope: surface sugar — sugar-rule lowering to kernel connective + edge discipline.
+// M9 concept-DAG home: sibling to node.dag (Connective, EdgeDiscipline, edges_conform).
+// Surface atom IDENTITY (^dag_c3_surface_sugar_* prelude) is language-specific extdep;
+// this module owns the TRANSFORMATION model only, keyed by-reference to those atoms.
+// Status: T-8 modeled — data-table authority for surface_atom → SugarLowering.
+// 🟡 gated — feature:CP-1b-surface-sugar-language-model — dissolve-on: surface_atom identity lookup owned by LanguageModel carrier; forbidden: parallel Atom identity classifier outside this table + LanguageModel projection.
+
+module v4.std.sugar
+
+import v4.std.collection { Absent, Present, optional_absent, optional_present }
+import v4.std.diagnostic {
+  Diagnostic,
+  node_locus,
+  Outcome,
+  UserInputBoundary,
+  Accepted,
+  None,
+  diagnostics_singleton
+}
+import v4.std.node {
+  Arrow,
+  Conj,
+  Connective,
+  Edge,
+  EdgeDiscipline,
+  LabeledEdges,
+  Node,
+  PositionalEdges,
+  Symbol,
+  TypeNode,
+  edges_conform,
+  is_positional
+}
+
+data sugar_reason_malformed: Symbol = sugar_reason_malformed
+
+// 🟢 TERMINAL — sugar lowering kinds: rewrite to kernel connective + edge discipline, or unwrap single positional child (irreducible transformation arms for surface sugar dissolution).
+type SugarLowering
+  = SugarRewriteConnective { connective: Connective, edges: EdgeDiscipline }
+  | SugarUnwrapPositionalChild {}
+
+type SugarRule {
+  surface_atom: Symbol
+  lowering: SugarLowering
+}
+
+data sugar_rule_service: SugarRule = SugarRule {
+  surface_atom: ^dag_c3_surface_sugar_service,
+  lowering: SugarRewriteConnective { connective: Conj, edges: LabeledEdges }
+}
+data sugar_rule_fn: SugarRule = SugarRule {
+  surface_atom: ^dag_c3_surface_sugar_fn,
+  lowering: SugarRewriteConnective { connective: Arrow, edges: PositionalEdges }
+}
+data sugar_rule_type: SugarRule = SugarRule {
+  surface_atom: ^dag_c3_surface_sugar_type,
+  lowering: SugarUnwrapPositionalChild {}
+}
+data sugar_rule_operation: SugarRule = SugarRule {
+  surface_atom: ^dag_c3_surface_sugar_operation,
+  lowering: SugarRewriteConnective { connective: Arrow, edges: PositionalEdges }
+}
+
+fn sugar_rules() -> List<SugarRule> {
+  [
+    sugar_rule_service,
+    sugar_rule_fn,
+    sugar_rule_type,
+    sugar_rule_operation
+  ]
+}
+
+fn no_sugar_rule() -> SugarRule? {
+  optional_absent()
+}
+
+fn sugar_rule_for_atom(id: Symbol, rule: SugarRule) -> SugarRule? {
+  if id == rule.surface_atom {
+    optional_present(value: rule)
+  } else {
+    optional_absent()
+  }
+}
+
+fn classify_sugar(n: Node) -> SugarRule? {
+  match n.kind {
+    TypeNode { connective: Atom { identity: id } } =>
+      fold(sugar_rules(), init: no_sugar_rule(), f: fn(acc, rule) {
+        match acc {
+          Present { value: _ } => acc
+          Absent => sugar_rule_for_atom(id: id, rule: rule)
+        }
+      })
+    TypeNode { connective: _ } => no_sugar_rule()
+    ComputationNode { behavior: _ } => no_sugar_rule()
+  }
+}
+
+fn sugar_malformed_diagnostic(n: Node) -> Diagnostic {
+  Diagnostic {
+    reason: sugar_reason_malformed,
+    at: node_locus(node: n),
+    correction: Unavailable { reason: UserInputBoundary }
+  }
+}
+
+fn sugar_type_node(connective: Connective, children: List<Edge>, n: Node) -> Node {
+  Node {
+    kind: TypeNode { connective: connective },
+    children: children,
+    occurrence_id: n.occurrence_id
+  }
+}
+
+fn sugar_positional_unwrap_child(children: List<Edge>) -> Node? {
+  if count(children) == 1 {
+    match children |> first {
+      Present { value: e0 } =>
+        if is_positional(e: e0) {
+          optional_present(value: e0.target)
+        } else {
+          optional_absent()
+        }
+      Absent => optional_absent()
+    }
+  } else {
+    optional_absent()
+  }
+}
+
+fn apply_sugar(rule: SugarRule, n: Node, children: List<Edge>) -> Outcome<Node> {
+  match rule.lowering {
+    SugarRewriteConnective { connective: connective, edges: discipline } =>
+      if edges_conform(children: children, d: discipline) {
+        Accepted {
+          value: sugar_type_node(connective: connective, children: children, n: n),
+          diagnostics: None
+        }
+      } else {
+        Rejected { diagnostics: diagnostics_singleton(d: sugar_malformed_diagnostic(n: n)) }
+      }
+    SugarUnwrapPositionalChild {} =>
+      match sugar_positional_unwrap_child(children: children) {
+        Present { value: child } =>
+          Accepted { value: child, diagnostics: None }
+        Absent =>
+          Rejected { diagnostics: diagnostics_singleton(d: sugar_malformed_diagnostic(n: n)) }
+      }
+  }
+}