Add v2.5 infer stage prototype

src/v2.5/04_infer.dag

@@ -0,0 +1,83 @@
+module v2_5.compiler.infer
+
+import v2_5.std.node { Symbol }
+import v2_5.std.stage_types {
+  NormalizedModule,
+  InferredModule,
+  InferredOtherItem
+}
+
+type ExprDataDissolution
+  = NoExprDataRetired
+  | LiteralCase
+  | ErrorCase
+  | VarCase
+  | FieldAccessCase
+  | CallCase
+  | MethodCallCase
+  | MatchCase
+  | IfCase
+  | LetCase
+  | RecordLitCase
+  | ListLitCase
+  | BinOpCase
+  | UnaryOpCase
+  | LambdaCase
+  | StringInterpCase
+  | BlockCase
+  | CastCase
+  | ForEachCase
+  | IndexCase
+  | SliceCase
+  | ReturnCase
+
+type InferCarrierClosure
+  = ClosedExprDataDissolution
+  | ClosedInferReadiness
+  | ClosedBinderScopeFold
+  | ClosedRecursiveExprFold
+
+type InferReadiness
+  = AwaitingTier1StageTypes { gate: Symbol }
+  | AwaitingRecursiveExprFold { gate: Symbol }
+  | BoundToTier1StageTypes
+
+type BinderScopeFold
+  = AwaitingPreChildScopeHook { gate: Symbol }
+  | HasPreChildScopeHook
+
+data v25_infer_tier1_gate: Symbol = v25_infer_tier1_gate
+data recursive_expr_fold_gate: Symbol = recursive_expr_fold_gate
+data binder_scope_fold_gate: Symbol = binder_scope_fold_gate
+
+data infer_readiness: InferReadiness = AwaitingRecursiveExprFold { gate: recursive_expr_fold_gate }
+data binder_scope_fold_status: BinderScopeFold = AwaitingPreChildScopeHook { gate: binder_scope_fold_gate }
+data infer_carrier_closure: List<InferCarrierClosure> = [
+  ClosedExprDataDissolution,
+  ClosedInferReadiness,
+  ClosedBinderScopeFold,
+  ClosedRecursiveExprFold
+]
+
+fn infer(module: NormalizedModule) -> InferredModule {
+  match infer_readiness {
+    AwaitingTier1StageTypes { gate: _ } =>
+      infer_unavailable(module: module, keyword: "infer-awaiting-tier1-stage-types")
+    AwaitingRecursiveExprFold { gate: _ } =>
+      infer_unavailable(module: module, keyword: "infer-awaiting-recursive-expression-fold")
+    BoundToTier1StageTypes =>
+      infer_unavailable(module: module, keyword: "infer-bound-without-recursive-expression-fold")
+  }
+}
+
+fn infer_unavailable(module: NormalizedModule, keyword: String) -> InferredModule {
+  InferredModule {
+    name: module.name,
+    imports: [],
+    items: [InferredOtherItem {
+      keyword: keyword,
+      raw_span: module.span
+    }],
+    span: module.span
+  }
+}

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,22 @@
+// v2.5 identity and provenance — shared across all pipeline phases.
+// Parse phases use AuthoredName; post-resolve phases use Symbol (from node).
+
+module v2_5.std.identity
+
+import v2_5.std.node { Symbol }
+
+type SourceSpan {
+  start: Int
+  end: Int
+  file: String
+}
+
+type AuthoredName {
+  text: String
+  span: SourceSpan
+}
+
+type BoundName {
+  symbol: Symbol
+  span: SourceSpan
+}

src/v2.5/std/node.dag

@@ -0,0 +1,146 @@
+// 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 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: _ } => true
+  }
+}
+
+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>
+}