v2.5: phase-typed stage interface kit (Tier 1)

src/v2.5/std/diagnostic.dag

@@ -0,0 +1,42 @@
+// src/v2.5/std/diagnostic.dag
+// Scope: fail-closed diagnostic schema for v2.5.
+// Owns: Diagnostic, Outcome, Locus, Extent, Correction, NoCorrectionReason.
+// Consumes: v2_5.std.node.
+// Status: v2.5 Tier 0 draft.
+
+module v2_5.std.diagnostic
+
+import v2_5.std.node { Symbol, Nat, Node, Path }
+
+// 🟡 coproduct dissolution — feature:byte-range-ordering-witness
+type Extent
+  = WholeFile
+  | ByteRange { start: Nat, end: Nat }
+
+// 🟢 coproduct dissolution
+type Locus
+  = Textual { file: Symbol, extent: Extent }
+  | NodeLocus { node: Node }
+  | PortLocus { path: Path }
+
+// 🟢 coproduct dissolution
+type NoCorrectionReason
+  = UserInputBoundary
+  | AmbiguousIntent
+  | ExternalContractUnknown
+
+// 🟢 coproduct dissolution
+type Correction
+  = Suggested { node: Node }
+  | Unavailable { reason: NoCorrectionReason }
+
+type Diagnostic {
+  reason: Symbol
+  at: Locus
+  correction: Correction
+}
+
+// 🟢 coproduct dissolution
+type Outcome<T>
+  = Produced { value: T }
+  | Rejected { diagnostic: Diagnostic }

src/v2.5/std/identity.dag

@@ -0,0 +1,27 @@
+// v2.5 identity and provenance — shared across all pipeline phases.
+// Parse phases use AuthoredName; post-resolve phases use Symbol (from node).
+// Shape-reference: dsl/std/types.dag SourceSpan/FilePath (transcribed; no cross-tree import).
+
+module v2_5.std.identity
+
+import v2_5.std.node { Symbol }
+
+// Shape-ref: std.types FilePath (non_empty refinement deferred in fork).
+type FilePath = String
+
+// Shape-ref: std.types SourceSpan
+type SourceSpan {
+  file: FilePath
+  start: Int
+  end: Int
+}
+
+type AuthoredName {
+  text: String
+  span: SourceSpan
+}
+
+type BoundName {
+  symbol: Symbol
+  span: SourceSpan
+}

src/v2.5/std/node.dag

@@ -0,0 +1,157 @@
+// src/v2.5/std/node.dag
+// Scope: v2.5 substrate root — type kernel for the forked tree.
+// Owns: Symbol, Hash, Nat, Connective, Behavior, NodeKind, EdgeLabel, Edge, Node, NodeFold, fold_node, EdgeDiscipline, connective_edge_discipline, all_edges_named, all_edges_positional, name_occurrences, all_names_distinct, edges_conform, node_locally_well_formed, node_well_formed, PathStep, Path, Edit, Diff.
+// Consumes: none.
+// Status: v2.5 Tier 0 draft.
+
+module v2_5.std.node
+
+type Symbol
+type Hash
+type Nat
+
+// 🟢 coproduct dissolution
+type Connective
+  = Atom { identity: Symbol }
+  | Conj
+  | Disj
+  | Arrow
+  | Cardinality
+  | Instantiation
+
+// 🟢 coproduct dissolution
+type Behavior
+  = Value
+  | Transform
+  | Branch
+  | Loop
+  | Bind
+
+// 🟢 coproduct dissolution
+type NodeKind
+  = TypeForm { connective: Connective }
+  | Computation { behavior: Behavior }
+
+// 🟢 coproduct dissolution
+type EdgeLabel
+  = Named { name: Symbol }
+  | Positional
+
+type Edge {
+  label: EdgeLabel
+  target: Node
+}
+
+type Node {
+  kind: NodeKind
+  children: List<Edge>
+}
+
+type NodeFold<R> {
+  init: fn(Node) -> R
+  step: fn(R, Edge, R) -> R
+}
+
+fn fold_node<R>(n: Node, algebra: NodeFold<R>) -> R {
+  fold(n.children, init: algebra.init(n), f: (acc, e) =>
+    algebra.step(acc, e, fold_node(n: e.target, algebra: algebra))
+  )
+}
+
+// 🟢 coproduct dissolution
+type EdgeDiscipline
+  = NoEdges
+  | LabeledEdges
+  | PositionalEdges
+
+fn connective_edge_discipline(c: Connective) -> EdgeDiscipline {
+  match c {
+    Atom { identity: _ } => NoEdges
+    Conj => LabeledEdges
+    Disj => LabeledEdges
+    Arrow => PositionalEdges
+    Cardinality => PositionalEdges
+    Instantiation => PositionalEdges
+  }
+}
+
+fn behavior_edge_discipline(b: Behavior) -> EdgeDiscipline {
+  match b {
+    Value => NoEdges
+    Transform => PositionalEdges
+    Branch => LabeledEdges
+    Loop => PositionalEdges
+    Bind => PositionalEdges
+  }
+}
+
+fn all_edges_named(children: List<Edge>) -> Bool {
+  fold(children, init: true, f: (acc, e) => match e.label {
+    Named { name: _ } => acc
+    Positional => false
+  })
+}
+
+fn all_edges_positional(children: List<Edge>) -> Bool {
+  fold(children, init: true, f: (acc, e) => match e.label {
+    Named { name: _ } => false
+    Positional => acc
+  })
+}
+
+fn name_occurrences(name: Symbol, children: List<Edge>) -> Int {
+  fold(children, init: 0, f: (acc, e) => match e.label {
+    Named { name: n } => if n == name { acc + 1 } else { acc }
+    Positional => acc
+  })
+}
+
+fn all_names_distinct(children: List<Edge>) -> Bool {
+  fold(children, init: true, f: (acc, e) => match e.label {
+    Named { name: n } => acc && (name_occurrences(name: n, children: children) == 1)
+    Positional => acc
+  })
+}
+
+fn edges_conform(children: List<Edge>, d: EdgeDiscipline) -> Bool {
+  match d {
+    NoEdges => count(children) == 0
+    LabeledEdges =>
+      all_edges_named(children: children) && all_names_distinct(children: children)
+    PositionalEdges => all_edges_positional(children: children)
+  }
+}
+
+fn node_locally_well_formed(n: Node) -> Bool {
+  match n.kind {
+    TypeForm { connective: c } =>
+      edges_conform(children: n.children, d: connective_edge_discipline(c: c))
+    Computation { behavior: b } =>
+      edges_conform(children: n.children, d: behavior_edge_discipline(b: b))
+  }
+}
+
+fn node_well_formed(n: Node) -> Bool {
+  fold_node(n: n, algebra: NodeFold {
+    init: n0 => node_locally_well_formed(n: n0),
+    step: (acc, edge, child_ok) => acc && child_ok
+  })
+}
+
+// 🟢 coproduct dissolution
+type PathStep
+  = NamedStep { name: Symbol }
+  | PositionalStep { index: Nat }
+
+type Path {
+  steps: List<PathStep>
+}
+
+type Edit {
+  at: Path
+  replacement: Node
+}
+
+type Diff {
+  edits: List<Edit>
+}