Eliminate need for forward type declarations in recursive datatypes

Strata/DDM/BuiltinDialects/StrataDDL.lean

@@ -164,7 +164,7 @@ def StrataDDL : Dialect := BuiltinM.create! "StrataDDL" #[initDialect] do
   -- Metadata for marking an operation as a constructor list push (list followed by constructor)
   declareMetadata { name := "constructorListPush", args := #[.mk "list" .ident, .mk "constructor" .ident] }
   declareMetadata { name := "declareType", args := #[.mk "name" .ident, .mk "args" (.opt .ident)] }
-  declareMetadata { name := "declareTypeForward", args := #[.mk "name" .ident, .mk "args" (.opt .ident)] }
+  declareMetadata { name := "preRegisterTypes", args := #[.mk "scope" .ident] }
   declareMetadata { name := "aliasType",   args := #[.mk "name" .ident, .mk "args" (.opt .ident), .mk "def" .ident] }
   declareMetadata { name := "declare",     args := #[.mk "name" .ident, .mk "type" .ident] }
   declareMetadata { name := "declareFn",   args := #[.mk "name" .ident, .mk "args" .ident, .mk "type" .ident] }

Strata/DDM/Elab/SyntaxElab.lean

@@ -91,8 +91,24 @@ structure SyntaxElaborator where
   syntaxCount : Nat
   argElaborators : ArgElaboratorArray syntaxCount
   resultScope : Option Nat
+  /-- Index into argElaborators for each argument
+  (indexed by argLevel), None if arg has no syntax. -/
+  argElabIndex : Array (Option Nat) := #[]
+  /-- If set, pre-register type names from children at this arg level before elaboration. -/
+  preRegisterTypesScope : Option Nat := none
 deriving Inhabited, Repr
 
+/-- Build an argElabIndex mapping each argLevel to its
+position in the given elaborator array. -/
+private def buildArgElabIndex (argDecls : ArgDecls)
+    {sc} (elabs : ArgElaboratorArray sc)
+    : Array (Option Nat) :=
+  let init := Array.replicate argDecls.size none
+  let (result, _) := elabs.foldl (init := (init, 0))
+    fun (arr, idx) ⟨ae, _⟩ =>
+      (arr.set! ae.argLevel (some idx), idx + 1)
+  result
+
 /-- Build the syntax elaborator that maps parsed syntax positions to
 argument positions.  For `.passthrough`, this is trivial: one syntax
 position maps directly to argument 0.  For `.mk`, we walk the atoms to
@@ -110,10 +126,13 @@ private def mkSyntaxElab! (argDecls : ArgDecls) (stx : SyntaxDef) (opMd : Metada
       contextLevel := argDecls.argScopeLevel ⟨0, h⟩
       datatypeScope := argDecls.argScopeDatatypeLevel ⟨0, h⟩
     }
+    let elabs := #[⟨ae, Nat.zero_lt_one⟩]
     {
       syntaxCount := 1
-      argElaborators := #[⟨ae, Nat.zero_lt_one⟩]
+      argElaborators := elabs
       resultScope := opMd.resultLevel argDecls.size
+      argElabIndex := buildArgElabIndex argDecls elabs
+      preRegisterTypesScope := opMd.preRegisterTypesLevel argDecls.size
     }
   | .std atoms _ =>
     let init : ArgElaborators := {
@@ -131,6 +150,8 @@ private def mkSyntaxElab! (argDecls : ArgDecls) (stx : SyntaxDef) (opMd : Metada
       syntaxCount := as.syntaxCount
       argElaborators := elabs
       resultScope := opMd.resultLevel argDecls.size
+      argElabIndex := buildArgElabIndex argDecls elabs
+      preRegisterTypesScope := opMd.preRegisterTypesLevel argDecls.size
     }
 
 private def opDeclElaborator! (decl : OpDecl) : SyntaxElaborator :=

Strata/DDM/Integration/Lean/ToExpr.lean

@@ -422,7 +422,6 @@ private def toExpr {argDecls} (bi : BindingSpec argDecls) (argDeclsExpr : Lean.E
   match bi with
   | .value b => astExpr! value argDeclsExpr (b.toExpr argDeclsExpr)
   | .type b => astExpr! type argDeclsExpr (b.toExpr argDeclsExpr)
-  | .typeForward b => astExpr! typeForward argDeclsExpr (b.toExpr argDeclsExpr)
   | .datatype b => astExpr! datatype argDeclsExpr (b.toExpr argDeclsExpr)
   | .tvar b => astExpr! tvar argDeclsExpr (b.toExpr argDeclsExpr)
 

Strata/Languages/Core/DDMTransform/ASTtoCST.lean

@@ -314,23 +314,10 @@ def datatypeToCST {M} [Inhabited M] (datatypes : List (Lambda.LDatatype Visibili
     let cmd ← processDatatype dt
     pure [cmd]
   | _ => do
-    -- Multiple datatypes - generate forward declarations and mutual block.
-    let mut forwardDecls : List (Command M) := []
-    for dt in datatypes.reverse do
-      let name : Ann String M := ⟨default, dt.name⟩
-      let args : Ann (Option (Bindings M)) M :=
-        if dt.typeArgs.isEmpty then
-          ⟨default, none⟩
-        else
-          let bindings := dt.typeArgs.map fun param =>
-            let paramName : Ann String M := ⟨default, param⟩
-            let paramType := TypeP.type default
-            Binding.mkBinding default paramName paramType
-          ⟨default, some (.mkBindings default ⟨default, bindings.toArray⟩)⟩
-      forwardDecls := forwardDecls ++ [.command_forward_typedecl default name args]
+    -- Multiple datatypes - mutual block with pre-registration handles forward references.
     let cmds ← datatypes.mapM processDatatype
     let mutualCmd := Command.command_mutual default ⟨default, cmds.toArray⟩
-    pure (forwardDecls ++ [mutualCmd])
+    pure [mutualCmd]
 
 /-- Convert a type synonym declaration to CST -/
 def typeSynToCST {M} [Inhabited M] (syn : TypeSynonym)
@@ -1081,7 +1068,7 @@ private def recreateGlobalContext (ctx : ToCSTContext M)
     (map.insert name i, i + 1)
   let vars := allFreeVars.map fun name =>
     -- .fvar below is really a dummy value.
-    (name, GlobalKind.expr (.fvar default 0 #[]), DeclState.defined)
+    (name, GlobalKind.expr (.fvar default 0 #[]))
   { nameMap, vars }
 
 -- Extract types not in `Core.KnownTypes`.

Strata/Languages/Core/DDMTransform/Grammar.lean

@@ -274,10 +274,6 @@ op command_procedure (name : Ident,
 op command_typedecl (name : Ident, args : Option Bindings) : Command =>
   "type " name args ";\n";
 
-@[declareTypeForward(name, some args)]
-op command_forward_typedecl (name : Ident, args : Option Bindings) : Command =>
-  "forward type " name args ";\n";
-
 @[aliasType(name, some args, rhs)]
 op command_typesynonym (name : Ident,
                         args : Option Bindings,
@@ -372,8 +368,8 @@ op command_datatype (name : Ident,
       "datatype " name typeParams " {" constructors "\n}" ";\n";
 
 // Mutual block for defining mutually recursive types
-// Types should be forward-declared before the mutual block
-@[scope(commands)]
+// Type names are pre-registered via @[preRegisterTypes] before elaboration
+@[scope(commands), preRegisterTypes(commands)]
 op command_mutual (commands : SpacePrefixSepBy Command) : Command =>
   "mutual\n  " indent(2, commands) "end;\n";
 

Strata/Languages/Core/DDMTransform/Translate.lean

@@ -350,31 +350,6 @@ def translateTypeDecl (bindings : TransBindings) (op : Operation) :
   let decl := Core.Decl.type (.con { name := name, numargs := numargs }) md
   return (decl, { bindings with freeVars := bindings.freeVars.push decl })
 
-/--
-Translate a forward type declaration. This creates a placeholder entry that will
-be replaced when the actual datatype definition is encountered in a mutual block.
--/
-def translateForwardTypeDecl (bindings : TransBindings) (op : Operation) :
-  TransM (Core.Decl × TransBindings) := do
-  let _ ← @checkOp (Core.Decl × TransBindings) op q`Core.command_forward_typedecl 2
-  let name ← translateIdent TyIdentifier op.args[0]!
-  let numargs ←
-    translateOption
-      (fun maybearg =>
-            do match maybearg with
-            | none => pure 0
-            | some arg =>
-              let bargs ← checkOpArg arg q`Core.mkBindings 1
-              let numargs ←
-                  match bargs[0]! with
-                  | .seq _ .comma args => pure args.size
-                  | _ => TransM.error
-                          s!"translateForwardTypeDecl expects a comma separated list: {repr bargs[0]!}")
-                    op.args[1]!
-  let md ← getOpMetaData op
-  let decl := Core.Decl.type (.con { name := name, numargs := numargs }) md
-  return (decl, { bindings with freeVars := bindings.freeVars.push decl })
-
 ---------------------------------------------------------------------
 
 def translateLhs (arg : Arg) : TransM Core.CoreIdent := do
@@ -1491,7 +1466,9 @@ Extract and translate constructor information from a constructor list argument.
 -/
 def translateConstructorList (p : Program) (bindings : TransBindings) (arg : Arg) :
     TransM (Array TransConstructorInfo) := do
-  let constructorInfos := GlobalContext.extractConstructorInfo p.dialects arg
+  let constructorInfos ← match extractConstructorInfo p.dialects arg with
+    | .ok info => pure info
+    | .error e => TransM.error s!"Constructor extraction error: {e}"
   constructorInfos.mapM (translateConstructorInfo bindings)
 
 ---------------------------------------------------------------------
@@ -1634,7 +1611,9 @@ def translateDatatype (p : Program) (bindings : TransBindings) (op : Operation)
 /--
 Translate a mutual block containing mutually recursive datatype definitions.
 This collects all datatypes, creates a single TypeDecl.data with all of them,
-and updates the forward-declared entries in bindings.freeVars.
+and adds placeholder entries for type references during translation.
+The `@[preRegisterTypes]` metadata on the mutual block operation ensures that
+type names are pre-registered in the DDM GlobalContext before processing.
 -/
 def translateMutualBlock (p : Program) (bindings : TransBindings) (op : Operation) :
     TransM (Core.Decl × TransBindings) := do
@@ -1653,29 +1632,34 @@ def translateMutualBlock (p : Program) (bindings : TransBindings) (op : Operatio
   if datatypeOps.size == 0 then
     TransM.error "Mutual block must contain at least one datatype"
   else
-    -- First pass: collect all datatype names, type args, and their indices in freeVars
-    -- Forward declarations MUST already be in bindings.freeVars
+    -- First pass: collect all datatype names and type args, and allocate placeholder
+    -- entries in freeVars for each one (replacing any pre-registered entries if present)
     let mut datatypeInfos : Array (String × List TyIdentifier × Nat) := #[]
     let mut bindingsWithPlaceholders := bindings
 
     for dtOp in datatypeOps do
       let datatypeName ← translateIdent String dtOp.args[0]!
       let (typeArgs, _) ← translateDatatypeTypeArgs bindings dtOp.args[1]! "translateMutualBlock"
 
-      -- Find the index of this datatype in freeVars (from forward declaration)
+      -- Check if this datatype was already pre-registered in freeVars
       let existingIdx := bindings.freeVars.findIdx? fun decl =>
         match decl with
         | .type t _ => t.names.contains datatypeName
         | _ => false
 
+      let placeholderDecl := Core.Decl.type (.data [mkPlaceholderLDatatype datatypeName typeArgs])
       match existingIdx with
       | some i =>
-        let placeholderDecl := Core.Decl.type (.data [mkPlaceholderLDatatype datatypeName typeArgs])
+        -- Replace existing pre-registered entry with placeholder
         datatypeInfos := datatypeInfos.push (datatypeName, typeArgs, i)
         bindingsWithPlaceholders := { bindingsWithPlaceholders with
           freeVars := bindingsWithPlaceholders.freeVars.set! i placeholderDecl }
       | none =>
-        TransM.error s!"Mutual datatype {datatypeName} requires a forward declaration"
+        -- Allocate a new placeholder entry
+        let idx := bindingsWithPlaceholders.freeVars.size
+        datatypeInfos := datatypeInfos.push (datatypeName, typeArgs, idx)
+        bindingsWithPlaceholders := { bindingsWithPlaceholders with
+          freeVars := bindingsWithPlaceholders.freeVars.push placeholderDecl }
 
     -- Second pass: translate all constructors with all placeholders in scope
     let ldatatypes ← (datatypeOps.zip datatypeInfos).toList.mapM fun (dtOp, (datatypeName, typeArgs, _idx)) => do
@@ -1696,8 +1680,7 @@ def translateMutualBlock (p : Program) (bindings : TransBindings) (op : Operatio
     let md ← getOpMetaData op
     let mutualTypeDecl := Core.Decl.type (.data ldatatypes) md
 
-    -- Update bindings.freeVars: replace forward-declared entries with the mutual block
-    -- For each datatype, update its entry to point to the mutual TypeDecl
+    -- Update bindings.freeVars: replace placeholder entries with the mutual block
     let mut finalBindings := bindings
 
     for (_datatypeName, _typeArgs, idx) in datatypeInfos do
@@ -1739,13 +1722,7 @@ partial def translateCoreDecls (p : Program) (bindings : TransBindings) :
   | 0 => return ([], bindings)
   | _ + 1 =>
     let op := ops[count]!
-    let (newDecls, bindings) ←
-      match op.name with
-      | q`Core.command_forward_typedecl =>
-        -- Forward declarations do NOT produce AST nodes - they only update bindings
-        let (_, bindings) ← translateForwardTypeDecl bindings op
-        pure ([], bindings)
-      | _ =>
+    let (newDecls, bindings) ← do
         let (decl, bindings) ←
           match op.name with
           | q`Core.command_datatype =>