Add pySpec generator

Strata/DDM/AST.lean

@@ -6,10 +6,10 @@
 module
 
 public import Std.Data.HashMap.Basic
+public import Strata.DDM.AST.Datatype
 public import Strata.DDM.Util.ByteArray
 public import Strata.DDM.Util.Decimal
-public import Lean.Data.Position
-public import Strata.DDM.AST.Datatype
+public import Strata.DDM.Util.SourceRange
 
 import Std.Data.HashMap
 import all Strata.DDM.Util.Array
@@ -263,122 +263,6 @@ public def flatten {α} (e : ExprF α) (prev : List (ArgF α) := []) : ExprF α
 
 end ExprF
 
-/--
-Source location information in the DDM is defined
-by a range of bytes in a UTF-8 string with the input
-Line/column information can be construced from a
-`Lean.FileMap`
-
-As an example, in the string `"123abc\ndef"`, the string
-`"abc"` has the position `{start := 3, stop := 6 }` while
-`"def"` has the position `{start := 7, stop := 10 }`.
--/
-structure SourceRange where
-  /-- The starting offset of the source range. -/
-  start : String.Pos.Raw
-  /-- One past the end of the range. -/
-  stop : String.Pos.Raw
-deriving DecidableEq, Inhabited, Repr
-
-namespace SourceRange
-
-def none : SourceRange := { start := 0, stop := 0 }
-
-def isNone (loc : SourceRange) : Bool := loc.start = 0 ∧ loc.stop = 0
-
-instance : ToFormat SourceRange where
- format fr := f!"{fr.start}-{fr.stop}"
-
-end SourceRange
-
-inductive Uri where
-  | file (path: String)
-  deriving DecidableEq, Repr, Inhabited
-
-instance : ToFormat Uri where
- format fr := match fr with | .file path => path
-
-structure FileRange where
-  file: Uri
-  range: Strata.SourceRange
-  deriving DecidableEq, Repr, Inhabited
-
-instance : ToFormat FileRange where
- format fr := f!"{fr.file}:{fr.range}"
-
-/-- A default file range for errors without source location.
-This should only be used for generated nodes that are guaranteed to be correct. -/
-def FileRange.unknown : FileRange :=
-  { file := .file "<unknown>", range := SourceRange.none }
-
-/-- A diagnostic model that holds a file range and a message.
-    This can be converted to a formatted string using a FileMap. -/
-structure DiagnosticModel where
-  fileRange : FileRange
-  message : String
-  deriving Repr, BEq, Inhabited
-
-instance : Inhabited DiagnosticModel where
-  default := { fileRange := FileRange.unknown, message := "" }
-
-/-- Create a DiagnosticModel from just a message (using default location).
-This should not be called, it only exists temporarily to enabling incrementally migrating code without error locations -/
-def DiagnosticModel.fromMessage (msg : String) : DiagnosticModel :=
-  { fileRange := FileRange.unknown, message := msg }
-
-/-- Create a DiagnosticModel from a Format (using default location).
-This should not be called, it only exists temporarily to enabling incrementally migrating code without error locations -/
-def DiagnosticModel.fromFormat (fmt : Std.Format) : DiagnosticModel :=
-  { fileRange := FileRange.unknown, message := toString fmt }
-
-/-- Create a DiagnosticModel with source location. -/
-def DiagnosticModel.withRange (fr : FileRange) (msg : Format) : DiagnosticModel :=
-  { fileRange := fr, message := toString msg }
-
-/-- Format a file range using a FileMap to convert byte offsets to line/column positions. -/
-def FileRange.format (fr : FileRange) (fileMap : Option Lean.FileMap) (includeEnd? : Bool := true) : Std.Format :=
-  let baseName := match fr.file with
-                  | .file path => (path.splitToList (· == '/')).getLast!
-  match fileMap with
-  | some fm =>
-    let startPos := fm.toPosition fr.range.start
-    let endPos := fm.toPosition fr.range.stop
-    if includeEnd? then
-      if startPos.line == endPos.line then
-        f!"{baseName}({startPos.line},({startPos.column}-{endPos.column}))"
-      else
-        f!"{baseName}(({startPos.line},{startPos.column})-({endPos.line},{endPos.column}))"
-    else
-      f!"{baseName}({startPos.line}, {startPos.column})"
-  | none =>
-    if fr.range.isNone then
-      f!""
-    else
-      f!"{baseName}({fr.range.start}-{fr.range.stop})"
-
-/-- Format a DiagnosticModel using a FileMap to convert byte offsets to line/column positions. -/
-def DiagnosticModel.format (dm : DiagnosticModel) (fileMap : Option Lean.FileMap) (includeEnd? : Bool := true) : Std.Format :=
-  let rangeStr := dm.fileRange.format fileMap includeEnd?
-  if dm.fileRange.range.isNone then
-    f!"{dm.message}"
-  else
-    f!"{rangeStr} {dm.message}"
-
-/-- Format just the file range portion of a DiagnosticModel. -/
-def DiagnosticModel.formatRange (dm : DiagnosticModel) (fileMap : Option Lean.FileMap) (includeEnd? : Bool := true) : Std.Format :=
-  dm.fileRange.format fileMap includeEnd?
-
-/-- Update the file range of a DiagnosticModel if it's currently unknown.
-This should not be called, it only exists temporarily to enabling incrementally migrating code without error locations -/
-def DiagnosticModel.withRangeIfUnknown (dm : DiagnosticModel) (fr : FileRange) : DiagnosticModel :=
-  if dm.fileRange.range.isNone then
-    { dm with fileRange := fr }
-  else
-    dm
-
-instance : ToString DiagnosticModel where
-  toString dm := dm.format none |> toString
-
 abbrev Arg := ArgF SourceRange
 abbrev Expr := ExprF SourceRange
 abbrev Operation := OperationF SourceRange
@@ -1739,7 +1623,7 @@ private partial def OperationF.foldBindingSpecs {α β}
         | some lvl => foldOverArgAtLevel m f init argDecls argsV lvl
       decl.newBindings.foldl (init := init) fun a b => f a op.ann b argsV
     else
-      @panic _ ⟨init⟩ "Expected arguments to match bindings"
+      @panic _ ⟨init⟩ s!"{op.name} expects {argDecls.size} arguments when {args.size} provided."
   | _ => @panic _ ⟨init⟩ s!"Unknown operation {op.name}"
 
 /--

Strata/DDM/Format.lean

@@ -133,10 +133,10 @@ structure FormatState where
 namespace FormatState
 
 /-- A format context that uses no syntactic sugar. -/
-private def empty : FormatState where
+def empty : FormatState where
   openDialects := {}
 
-private instance : Inhabited FormatState where
+instance : Inhabited FormatState where
   default := .empty
 
 def pushBinding (s : FormatState) (ident : String) : FormatState :=

Strata/DDM/Ion.lean

@@ -603,7 +603,7 @@ private protected def ArgF.fromIon {α} [FromIon α] (v : Ion SymbolId) : FromIo
   | "ident" =>
     let ⟨p⟩ ← .checkArgCount "ident" sexp 3
     .ident <$> fromIon sexp[1]
-           <*> .asString "Identifier value" sexp[2]
+           <*> .asSymbolString "Identifier value" sexp[2]
   | "num" =>
     let ⟨p⟩ ← .checkArgCount "num" sexp 3
     let ann ← fromIon sexp[1]
@@ -1457,7 +1457,10 @@ def fromIonFragment (f : Ion.Fragment)
     commands := ← fromIonFragmentCommands f
   }
 
-def fileFromIon (dialects : DialectMap) (dialect : DialectName) (bytes : ByteArray) : Except String Strata.Program := do
+/--
+Decodes bytes in the Ion format into a single Strata program.
+-/
+def fromIon (dialects : DialectMap) (dialect : DialectName) (bytes : ByteArray) : Except String Strata.Program := do
   let (hdr, frag) ←
     match Strata.Ion.Header.parse bytes with
     | .error msg =>

Strata/DDM/Util/Fin.lean

@@ -35,3 +35,10 @@ end Range
 def range (n : Nat) : Range n := .mk
 
 end Fin
+
+public section
+namespace Strata.Fin
+export _root_.Fin(Range range)
+end Strata.Fin
+
+end

Strata/DDM/Util/SourceRange.lean

@@ -0,0 +1,38 @@
+/-
+  Copyright Strata Contributors
+
+  SPDX-License-Identifier: Apache-2.0 OR MIT
+-/
+module
+
+public section
+namespace Strata
+
+/--
+Source location information in the DDM is defined
+by a range of bytes in a UTF-8 string with the input
+Line/column information can be construced from a
+`Lean.FileMap`
+
+As an example, in the string `"123abc\ndef"`, the string
+`"abc"` has the position `{start := 3, stop := 6 }` while
+`"def"` has the position `{start := 7, stop := 10 }`.
+-/
+structure SourceRange where
+  /-- The starting offset of the source range. -/
+  start : String.Pos.Raw
+  /-- One past the end of the range. -/
+  stop : String.Pos.Raw
+deriving DecidableEq, Inhabited, Repr
+
+namespace SourceRange
+
+def none : SourceRange := { start := 0, stop := 0 }
+
+def isNone (loc : SourceRange) : Bool := loc.start = 0 ∧ loc.stop = 0
+
+instance : Std.ToFormat SourceRange where
+ format fr := f!"{fr.start}-{fr.stop}"
+
+end Strata.SourceRange
+end

Strata/DL/Imperative/MetaData.lean

@@ -6,8 +6,7 @@
 
 import Strata.DL.Imperative.PureExpr
 import Strata.DL.Util.DecidableEq
-import Strata.DDM.AST
-import Lean.Data.Position
+import Strata.Util.FileRange
 
 namespace Imperative
 open Strata (DiagnosticModel FileRange)

Strata/DL/Lambda/Identifiers.lean

@@ -4,11 +4,9 @@
   SPDX-License-Identifier: Apache-2.0 OR MIT
 -/
 
-
-
 import Strata.DL.Lambda.LTy
 import Strata.DL.Util.Map
-import Strata.DDM.AST
+import Strata.Util.FileRange
 
 ---------------------------------------------------------------------
 

Strata/Languages/Python/PythonDialect.lean

@@ -7,5 +7,130 @@ import Strata.DDM.Integration.Lean
 
 namespace Strata.Python
 #load_dialect "../../../Tools/Python/dialects/Python.dialect.st.ion"
+
 #strata_gen Python
+
+instance {α} [Inhabited α] : ToString (Strata.Python.constant α) where
+  toString s := toString (eformat s.toAst)
+
+deriving instance DecidableEq for operator
+
+def alias.ann {α} : alias α → α
+| .mk_alias ann _ _ => ann
+
+def alias.name {α} : alias α → String
+| .mk_alias _ name _ => name.val
+
+def alias.asname {α} : alias α → Option String
+| .mk_alias _ _ asname => asname.val.map (·.val)
+
+def constant.ann {α} : constant α → α
+| ConTrue ann .. => ann
+| ConFalse ann .. => ann
+| ConPos ann .. => ann
+| ConNeg ann .. => ann
+| ConString ann .. => ann
+| ConFloat ann .. => ann
+| ConComplex ann .. => ann
+| ConNone ann .. => ann
+| ConEllipsis ann .. => ann
+| ConBytes ann .. => ann
+
+def keyword.ann {α} : keyword α → α
+| .mk_keyword ann _ _ => ann
+
+def keyword.arg {α} : keyword α → Ann (Option (Ann String α)) α
+| .mk_keyword _ arg _ => arg
+
+def keyword.value {α} : keyword α → expr α
+| .mk_keyword _ _ value => value
+
+namespace int
+
+def value {α} (i : int α) : Int :=
+  match i with
+  | IntPos _ n => n.val
+  | IntNeg _ n => - (n.val : Int)
+
+end int
+
+
+namespace expr
+
+def ann {α} : expr α → α
+| BoolOp a .. => a
+| NamedExpr a .. => a
+| BinOp a .. => a
+| UnaryOp a .. => a
+| Lambda a .. => a
+| IfExp a .. => a
+| Dict a .. => a
+| Set a .. => a
+| ListComp a .. => a
+| SetComp a .. => a
+| DictComp a .. => a
+| GeneratorExp a .. => a
+| Await a .. => a
+| Yield a .. => a
+| YieldFrom a .. => a
+| Compare a .. => a
+| Call a .. => a
+| FormattedValue a .. => a
+| Interpolation a .. => a
+| JoinedStr a .. => a
+| TemplateStr a .. => a
+| Constant a .. => a
+| Attribute a .. => a
+| Subscript a .. => a
+| Starred a .. => a
+| Name a .. => a
+| List a .. => a
+| Tuple a .. => a
+| Slice a .. => a
+
+end expr
+
+namespace stmt
+
+def ann {α} : stmt α → α
+| AnnAssign a .. => a
+| Assert a .. => a
+| Assign a .. => a
+| AsyncFor a .. => a
+| AsyncFunctionDef a .. => a
+| AsyncWith a .. => a
+| AugAssign a .. => a
+| Break a .. => a
+| ClassDef a .. => a
+| Continue a .. => a
+| Delete a .. => a
+| Expr a .. => a
+| For a .. => a
+| FunctionDef a .. => a
+| Global a .. => a
+| If a .. => a
+| Import a .. => a
+| ImportFrom a .. => a
+| Match a .. => a
+| Nonlocal a .. => a
+| Pass a .. => a
+| Raise a .. => a
+| Return a .. => a
+| Try a .. => a
+| TryStar a .. => a
+| TypeAlias a .. => a
+| While a .. => a
+| With a .. => a
+
+end stmt
+
+instance {α} [Inhabited α] : ToString (Strata.Python.expr α) where
+  toString s := toString (eformat s.toAst)
+
+def stmt.format {α} [Inhabited α] : ToString (Strata.Python.stmt α) where
+  toString s := toString (mformat s.toAst (.ofDialects Python_map) .empty |>.format)
+
+instance {α} [Inhabited α] : ToString (Strata.Python.stmt α) where
+  toString s := toString (mformat s.toAst (.ofDialects Python_map) .empty |>.format)
+
 end Strata.Python