Add PySpec to StrataCore translation pipeline

Strata/DDM/Integration/Lean/Gen.lean

@@ -25,7 +25,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 +40,24 @@ 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
+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 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
+  return .mk (.ident .none nameStr.toRawSubstring subName [.decl resolvedName []])
 
 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 +651,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 +669,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 +678,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 +815,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
+  mkScopedIdent <| (← getCategoryScopedName cat) ++ `toAst
 
 /-- Returns the identifier for a category's ofAst function. -/
 def ofAstIdentM (cat : QualifiedIdent) : GenM Ident := do
-  currScopedIdent <| (← getCategoryScopedName cat) ++ `ofAst
+  mkScopedIdent <| (← getCategoryScopedName cat) ++ `ofAst
 
 /-- Wraps a value with an `Ann`-extracted annotation into an AST argument. -/
 def mkAnnWithTerm (argCtor : Name) (annTerm v : Term) : Term :=
@@ -1322,7 +1309,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
+    mkScopedIdent <| (← getCategoryScopedName cat) ++ `ofAst.nameIndexMap
   let cmd ← `(def $ofAstNameMap : Std.HashMap Strata.QualifiedIdent Nat :=
     Std.HashMap.ofList $(quote nameIndexMap.toList))
   pure (nameIndexMap, ofAstNameMap, cmd)

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/DDM/Util/SourceRange.lean

@@ -5,6 +5,8 @@
 -/
 module
 
+public import Lean.Data.Position
+
 public section
 namespace Strata
 
@@ -34,5 +36,16 @@ def isNone (loc : SourceRange) : Bool := loc.start = 0 ∧ loc.stop = 0
 instance : Std.ToFormat SourceRange where
  format fr := f!"{fr.start}-{fr.stop}"
 
+/-- Format a SourceRange as a string using a FileMap for line:column conversion.
+    Renders location information in a format VSCode understands.
+    Returns "path:line:col-col" if on same line, otherwise "path:line:col". -/
+def format (loc : SourceRange) (path : System.FilePath) (fm : Lean.FileMap) : String :=
+  let spos := fm.toPosition loc.start
+  let epos := fm.toPosition loc.stop
+  if spos.line == epos.line then
+    s!"{path}:{spos.line}:{spos.column+1}-{epos.column+1}"
+  else
+    s!"{path}:{spos.line}:{spos.column+1}"
+
 end Strata.SourceRange
 end

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
 
 ---------------------------------------------------------------------
@@ -361,10 +362,11 @@ op command_mutual (commands : SpacePrefixSepBy Command) : Command =>
 
 namespace CoreDDM
 
---#strata_gen Boogie
+#strata_gen Core
 
 end CoreDDM
 
 ---------------------------------------------------------------------
 
 end Strata
+end

Strata/Languages/Core/DDMTransform/Translate.lean

@@ -4,12 +4,10 @@
   SPDX-License-Identifier: Apache-2.0 OR MIT
 -/
 
-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
 
-
 ---------------------------------------------------------------------
 namespace Strata
 
@@ -1762,6 +1760,11 @@ def translateProgram (p : Program) : TransM Core.Program := do
   let decls ← translateCoreDecls p {}
   return { decls := decls }
 
+def Core.getProgram
+  (p : Strata.Program)
+  (ictx : InputContext := Inhabited.default) : Core.Program × Array String :=
+  TransM.run ictx (translateProgram p)
+
 ---------------------------------------------------------------------
 
 end Strata

Strata/Languages/Core/Verifier.lean

@@ -483,11 +483,6 @@ def typeCheck (ictx : InputContext) (env : Program) (options : Options := Option
   else
     .error <| DiagnosticModel.fromFormat s!"DDM Transform Error: {repr errors}"
 
-def Core.getProgram
-  (p : Strata.Program)
-  (ictx : InputContext := Inhabited.default) : Core.Program × Array String :=
-  TransM.run ictx (translateProgram p)
-
 def verify
     (env : Program)
     (ictx : InputContext := Inhabited.default)

Strata/Languages/Python/CorePrelude.lean

@@ -4,10 +4,7 @@
   SPDX-License-Identifier: Apache-2.0 OR MIT
 -/
 
-import Strata.DDM.Elab
-import Strata.DDM.AST
-import Strata.Languages.Core.DDMTransform.Parse
-import Strata.Languages.Core.Verifier
+import Strata.Languages.Core.DDMTransform.Translate
 
 namespace Strata
 namespace Python