Convert DDM files to Lean 4 modules and fix mkScopedIdent for module support

Strata/DDM/Integration/Lean.lean

@@ -5,5 +5,11 @@
 -/
 module
 
+public import Strata.DDM.Format  -- FormatOptions used by test files
 public import Strata.DDM.Integration.Lean.Gen
 public import Strata.DDM.Integration.Lean.HashCommands
+
+/-!
+Umbrella module that re-exports all imports needed to work with
+the Lean integration.
+-/

Strata/DDM/Integration/Lean/Gen.lean

@@ -7,11 +7,16 @@ module
 
 public meta import Lean.Elab.Command
 public meta import Strata.DDM.AST
+-- `public import` provides object-level access for generated code at call sites.
+-- `public meta import` provides meta-level access for #strata_gen elaboration.
+public import      Strata.DDM.BuiltinDialects.Init  -- Generated code uses Init types
+public import      Strata.DDM.HNF  -- Generated ofAst uses ExprF.hnf
 public meta import Strata.DDM.BuiltinDialects.Init
 meta import        Strata.DDM.BuiltinDialects.StrataDDL
 public meta import Strata.DDM.Integration.Categories
 public meta import Strata.DDM.Integration.Lean.Env
-import             Strata.DDM.Integration.Lean.GenTrace
+public meta import Strata.DDM.Integration.Lean.GenTrace  -- trace option
+public import      Strata.DDM.Integration.Lean.OfAstM  -- Generated ofAst combinators
 public meta import Strata.DDM.Integration.Lean.OfAstM
 public meta import Strata.DDM.Util.Graph.Tarjan
 meta import        Strata.Util.DecideProp
@@ -25,7 +30,7 @@ category used by the dialect.
 open Lean (Command Name Ident Term TSyntax getEnv logError profileitM quote
   withTraceNode mkIdentFrom)
 open Lean.Elab (throwUnsupportedSyntax)
-open Lean.Elab.Command (CommandElab CommandElabM elabCommand)
+open Lean.Elab.Command (CommandElab CommandElabM elabCommand getScope)
 open Lean.MonadOptions (getOptions)
 open Lean.MonadResolveName (getCurrNamespace)
 open Lean.Parser.Command (ctor)
@@ -40,22 +45,25 @@ namespace Lean
 
 /--
 Prepend the current namespace to the Lean name and convert to an identifier.
+When in a module file and not in a `public section`, uses `mkPrivateName` to
+resolve the `.decl` pre-resolution hint to the private-mangled name.
 -/
-def mkScopedIdent (scope : Name) (subName : Lean.Name) : Ident :=
-  let fullName := scope ++ subName
-  let nameStr := toString subName
-  .mk (.ident .none nameStr.toRawSubstring subName [.decl fullName []])
-
-/--
-Prepend the current namespace to the Lean name and convert to an identifier.
--/
-def currScopedIdent {m} [Monad m] [Lean.MonadResolveName m]
-    (subName : Lean.Name) : m Ident := do
-  (mkScopedIdent · subName) <$> getCurrNamespace
+def mkScopedIdent (subName : Lean.Name) : CommandElabM Ident := do
+  let env ← getEnv
+  let scope ← getScope
+  let fullName := scope.currNamespace ++ subName
+  let resolvedName :=
+    if !env.header.isModule || scope.isPublic then
+      fullName
+    else
+      Lean.mkPrivateName env fullName
+  let rawStr := (toString subName).toRawSubstring
+  let preresolution := [.decl resolvedName []]
+  return .mk (.ident .none rawStr subName preresolution)
 
 end Lean
 
-open Lean (currScopedIdent)
+open Lean (mkScopedIdent)
 
 def arrayLit [Monad m] [Lean.MonadQuotation m] (as : Array Term) : m Term := do
   ``( (#[ $as:term,* ] : Array _) )
@@ -649,21 +657,6 @@ def mkCategoryIdent (scope : Name) (name : Name) : Ident :=
         aux p' (.str .anonymous v :: r)
   aux name []
 
-/--
-Prepend the current namespace to the Lean name and convert to an identifier.
--/
-def scopedIdent (scope subName : Lean.Name) : Ident :=
-  let name := scope ++ subName
-  let nameStr := toString subName
-  .mk (.ident .none nameStr.toRawSubstring subName [.decl name []])
-
-/--
-Prepend the current namespace to the Lean name and convert to an identifier.
--/
-def mkScopedIdent {m} [Monad m] [Lean.MonadResolveName m]
-    (subName : Lean.Name) : m Ident :=
-  (scopedIdent · subName) <$> getCurrNamespace
-
 /--
 Returns the Lean name for a category, looking it up in the context's
 category name map which handles naming conflicts.
@@ -682,7 +675,7 @@ or a generated category name.
 def getCategoryIdent (cat : QualifiedIdent) : GenM Ident := do
   if let some nm := declaredCategories[cat]? then
     return mkRootIdent nm
-  currScopedIdent (← getCategoryScopedName cat)
+  mkScopedIdent (← getCategoryScopedName cat)
 
 /-- Returns a Lean term for a category type applied to the annotation type. -/
 def getCategoryTerm (cat : QualifiedIdent) (annType : Ident) : GenM Term := do
@@ -691,7 +684,7 @@ def getCategoryTerm (cat : QualifiedIdent) (annType : Ident) : GenM Term := do
 
 /-- Returns a scoped identifier for a constructor in a category. -/
 def getCategoryOpIdent (cat : QualifiedIdent) (name : Name) : GenM Ident := do
-  currScopedIdent <| (← getCategoryScopedName cat) ++ name
+  mkScopedIdent <| (← getCategoryScopedName cat) ++ name
 
 /--
 Generates a Lean type term for a `SyntaxCat`, recursing into parameterized
@@ -828,11 +821,11 @@ def categoryToAstTypeIdent (cat : QualifiedIdent) (annType : Term) : Term :=
 
 /-- Returns the identifier for a category's toAst function. -/
 def toAstIdentM (cat : QualifiedIdent) : GenM Ident := do
-  currScopedIdent <| (← getCategoryScopedName cat) ++ `toAst
+  getCategoryOpIdent cat `toAst
 
 /-- Returns the identifier for a category's ofAst function. -/
 def ofAstIdentM (cat : QualifiedIdent) : GenM Ident := do
-  currScopedIdent <| (← getCategoryScopedName cat) ++ `ofAst
+  getCategoryOpIdent cat `ofAst
 
 /-- Wraps a value with an `Ann`-extracted annotation into an AST argument. -/
 def mkAnnWithTerm (argCtor : Name) (annTerm v : Term) : Term :=
@@ -1322,7 +1315,7 @@ def createNameIndexMap (cat : QualifiedIdent) (ops : Array DefaultCtor)
     | none => map  -- Skip operators without a name
     | some name => map.insert name map.size  -- Assign the next available index
   let ofAstNameMap ←
-    currScopedIdent <| (← getCategoryScopedName cat) ++ `ofAst.nameIndexMap
+    getCategoryOpIdent cat `ofAst.nameIndexMap
   let cmd ← `(def $ofAstNameMap : Std.HashMap Strata.QualifiedIdent Nat :=
     Std.HashMap.ofList $(quote nameIndexMap.toList))
   pure (nameIndexMap, ofAstNameMap, cmd)

Strata/DDM/Integration/Lean/OfAstM.lean

@@ -5,8 +5,6 @@
 -/
 module
 public import Strata.DDM.AST
-public import Strata.DDM.HNF
-import all Strata.DDM.Util.Array
 
 /-!
 Runtime support for converting AST representations back to generated types.
@@ -241,48 +239,6 @@ def ofSeqM {α β} [Repr α] [SizeOf α]
       throwExpected sep.toString arg
   | _ => throwExpected sep.toString arg
 
-/--
-Get the expression at index `lvl` in the arguments.
-
-Note that in conversion, we will
--/
-def atArg {Ann α β} [SizeOf α] {e : α} (as : SizeBounded (Array (ArgF Ann)) e 1) (lvl : Nat)
-        (act : (s : SizeBounded (ArgF Ann) e (-1)) → OfAstM β)
-        (lvlP : lvl < as.val.size := by get_elem_tactic) :
-        OfAstM β :=
-  have lvlP : lvl < as.val.size := by omega
-  have p : sizeOf as.val[lvl] ≤ sizeOf e + (-1 : Int) := by
-      have asP := as.property
-      have inP : as.val[lvl] ∈ as.val := by simp
-      have eltSizeOfP := Array.sizeOf_lt_of_mem_strict inP;
-      omega
-  act ⟨as.val[lvl], p⟩
-
-/--
-Get the expression at index `lvl` in the arguments.
-
-Note that in conversion, we will
--/
-def exprEtaArg {Ann α T} [Repr Ann] [HasEta α T]
-    {e : Expr} {n : Nat}
-    (as : SizeBounded (Array (ArgF Ann)) e 1)
-    (_ : as.val.size ≤ n) (lvl : Nat)
-    (act : (s : ExprF Ann) → sizeOf s < sizeOf e → OfAstM α)
-    : OfAstM α :=
-  if lvlP : lvl < as.val.size then
-    let i := as.val.size - 1 - lvl
-    have iP : i < as.val.size := by omega
-    match arg_eq : as.val[i] with
-    | .expr a1 => act a1 (by
-        have asP := as.property
-        have idxP := Array.sizeOf_getElem as.val i iP;
-        simp +arith [arg_eq] at idxP;
-        omega)
-    | _ => .throwExpectedExpr as.val[i]
-  else
-    let i := n - 1 - lvl
-    return HasEta.bvar i
-
 /--
 Distinguishes between a type parameter (category reference) and a type
 expression in Init.TypeP, applying the appropriate handler.

Strata/DDM/Util/Lean.lean

@@ -58,21 +58,6 @@ instance : Quote Int where
   | Int.ofNat n => Syntax.mkCApp ``Int.ofNat #[quote n]
   | Int.negSucc n => Syntax.mkCApp ``Int.negSucc #[quote n]
 
-/--
-Prepend the current namespace to the Lean name and convert to an identifier.
--/
-def scopedIdent (scope subName : Lean.Name) : Ident :=
-  let name := scope ++ subName
-  let nameStr := toString subName
-  .mk (.ident .none nameStr.toRawSubstring subName [.decl name []])
-
-/--
-Prepend the current namespace to the Lean name and convert to an identifier.
--/
-def currScopedIdent {m} [Monad m] [Lean.MonadResolveName m]
-                    (subName : Lean.Name) : m Ident := do
-  (scopedIdent · subName) <$> getCurrNamespace
-
 /- Returns an identifier from a string. -/
 def localIdent (name : String) : Ident :=
   let dName := .anonymous |>.str name
@@ -89,12 +74,6 @@ def mkRootIdent (name : Name) : Ident :=
   let rootName := `_root_ ++ name
   .mk (.ident .none name.toString.toRawSubstring rootName [.decl name []])
 
-/--
-Create an array literal from an array of term.
--/
-def arrayLit {m} [Monad m] [Lean.MonadQuotation m] (as : Array Term) : m Term := do
-  ``( (#[ $as:term,* ] : Array _) )
-
 end Lean
 
 public section

Strata/Languages/Core/DDMTransform/Parse.lean

@@ -3,13 +3,14 @@
 
   SPDX-License-Identifier: Apache-2.0 OR MIT
 -/
+module
 
+public import Strata.DDM.AST
 import Strata.DDM.Integration.Lean
-import Strata.DDM.Util.Format
-import Strata.Languages.Core.Core
+public import Strata.DDM.Integration.Lean.OfAstM
 
 ---------------------------------------------------------------------
-
+public section
 namespace Strata
 
 ---------------------------------------------------------------------
@@ -368,3 +369,4 @@ end CoreDDM
 ---------------------------------------------------------------------
 
 end Strata
+end

Strata/Languages/Core/DDMTransform/Translate.lean

@@ -5,6 +5,7 @@
 -/
 
 import Strata.DDM.AST
+import Strata.Languages.Core.Core
 import Strata.Languages.Core.DDMTransform.Parse
 import Strata.Languages.Core.CoreGen
 import Strata.DDM.Util.DecimalRat

StrataTest/DDM/ASTTests.lean

@@ -3,8 +3,9 @@
 
   SPDX-License-Identifier: Apache-2.0 OR MIT
 -/
+module
 
-import Strata.DDM.AST
+meta import Strata.DDM.AST
 
 namespace Strata.AST.Tests
 

StrataTest/DDM/Bool.lean

@@ -3,6 +3,7 @@
 
   SPDX-License-Identifier: Apache-2.0 OR MIT
 -/
+module
 
 import Strata.DDM.Integration.Lean
 

StrataTest/DDM/ByteArray.lean

@@ -3,6 +3,8 @@
 
   SPDX-License-Identifier: Apache-2.0 OR MIT
 -/
+module
+
 import Strata.DDM.Integration.Lean
 
 -- Minimal dialect to test dialects can be declared.
@@ -27,7 +29,7 @@ eval b"ab\x12\r\\";
 #eval IO.print bvExample
 
 #guard
-  match Command.ofAst bvExample.commands[0] with
+  match Command.ofAst bvExample.commands[0]! with
   | .ok (Command.eval _ bv) => bv.val == .mk ("ab\x12\r\\".toList.toArray.map Char.toUInt8)
   | _ => false
 

StrataTest/DDM/Comment.lean

@@ -3,11 +3,13 @@
 
   SPDX-License-Identifier: Apache-2.0 OR MIT
 -/
+module
+
+import Strata.DDM.Integration.Lean
 
 /-
 This is a small example showing syntax overriding a comment.
 -/
-import Strata.DDM.Integration.Lean
 
 #dialect
 dialect Comment;

StrataTest/DDM/DeclareFn.lean

@@ -3,8 +3,11 @@
 
   SPDX-License-Identifier: Apache-2.0 OR MIT
 -/
+module
 
-import Strata.DDM.Integration.Lean
+public import Strata.DDM.Integration.Lean
+
+public section
 
 -- Declare dialect for testing declareFn
 #dialect
@@ -107,3 +110,5 @@ check a : F Int;
 -/
 #guard_msgs in
 #eval IO.println testDeclareTypePgm
+
+end

StrataTest/DDM/DeclareTypeVars.lean

@@ -3,6 +3,7 @@
 
   SPDX-License-Identifier: Apache-2.0 OR MIT
 -/
+module
 
 import Strata.DDM.Integration.Lean
 

StrataTest/DDM/Elab.lean

@@ -3,8 +3,11 @@
 
   SPDX-License-Identifier: Apache-2.0 OR MIT
 -/
+module
 
-import Strata.DDM.Integration.Lean
+public import Strata.DDM.Integration.Lean
+
+public section
 
 -- Minimal dialect to test dialects can be declared.
 #guard_msgs in
@@ -124,3 +127,5 @@ program Test;
 str "\r\u20ac\u2022\x9d\n\t";
 str "\\n\"";
 #end
+
+end

StrataTest/DDM/Import.lean

@@ -3,6 +3,7 @@
 
   SPDX-License-Identifier: Apache-2.0 OR MIT
 -/
+module
 
 import StrataTest.DDM.Elab
 -- This tests that we can import a module and see dialects declared there.

StrataTest/DDM/Integration/Java/TestGen.lean

@@ -3,17 +3,21 @@
 
   SPDX-License-Identifier: Apache-2.0 OR MIT
 -/
-
-import Strata.DDM.Integration.Java
-import Strata.DDM.Integration.Lean.Env  -- For dialectExt
-import Strata.DDM.Integration.Lean.HashCommands  -- For #load_dialect
+module
+
+public import Lean.Elab.Command
+public meta import Strata.DDM.BuiltinDialects.Init
+public meta import Strata.DDM.Integration.Java
+public meta import Strata.DDM.Integration.Lean.Env
+meta import Strata.DDM.Integration.Lean.HashCommands  -- For #load_dialect
+public meta import Strata.DDM.Ion
 import Strata.Languages.Core.DDMTransform.Parse  -- Loads Strata Core dialect into env
 
 namespace Strata.Java.Test
 
 open Strata.Java
 
-def check (s sub : String) : Bool := (s.splitOn sub).length > 1
+meta def check (s sub : String) : Bool := (s.splitOn sub).length > 1
 
 -- Test 1: Basic dialect with 2 operators
 #eval do