Add pySpec generator (#355)

This PR introduces a PySpec generator prototype along with several
supporting improvements and bug fixes.
Main Feature: PySpec Generator
Adds a new strata pySpecs subcommand that translates Python
specification files into binary PySpec files. Python specification
files capture method signatures and their pre/post-conditions as
idiomatic Python source code, facilitating LLM-assisted generation.
The binary PySpec format enables efficient loading when validating
source code that uses these imports.
New files:
- Strata/Languages/Python/Specs.lean - Core specification
translation logic
- Strata/Languages/Python/Specs/DDM.lean - DDM types for PySpec
- Strata/Languages/Python/Specs/Decls.lean - Declaration handling
- Strata/Languages/Python/ReadPython.lean - Python file reading
utilities
- Test files: StrataTest/Languages/Python/Specs/{basetypes.py, main.py}
and SpecsTest.lean
- StrataTest/Util/Python.lean - Python testing utilities
Refactoring and Code Organization
Source range improvements:
- Migrated source mapping types from Strata/DDM/AST.lean to
dedicated modules:
- Strata/DDM/Util/SourceRange.lean - SourceRange definition
- Strata/Util/FileRange.lean - FileRange, Uri, DiagnosticModel
types and formatting
- Added Strata/Util/DecideProp.lean for decidability utilities
- Reduces unnecessary code in DDM and improves modularity
Import organization:
- Pruned unnecessary imports in StrataMain.lean
- Filter builtin module imports from Python signatures
Bug Fixes
1. DDM Ion parsing: Fixed bug in parsing DDM Ident types in Ion
files (changed .asString to .asSymbolString in
Strata/DDM/Ion.lean)
2. DDM formatting:
- Fixed precedence calculation in Strata/DDM/Format.lean
(changed maxPrec to maxPrec + 1 in atom definition)
- This fixes C_Simp formatting issues where output had missing
spaces (e.g., (bool)proceduretrivial() → bool procedure trivial())
- Made FormatState.empty public to enable external
instantiation
3. Python tooling:
- Added recursion limit (2500) in Tools/Python/strata/gen.py
- Improved parse error handling with dedicated exit code (100) for
parse failures
- Cleaned up handling of deprecated AST operations
Testing
- Updated C_Simp example test expectations to reflect formatting
fixes
- Added comprehensive PySpec test cases
---
By submitting this pull request, I confirm that you can use, modify,
copy, and redistribute this contribution, under the terms of your
choice.

---------

Co-authored-by: Claude Sonnet 4.5 <noreply@anthropic.com>

Author: joehendrix

.github/workflows/ci.yml

@@ -157,6 +157,8 @@ jobs:
         auto-config: false
         build: true
         build-args: "strata:exe"
+    - name: Run PySpec test that may be skipped without Python
+      run: PYTHON=python PYTHON_TEST=1 lake build StrataTest.Languages.Python.SpecsTest
     - name: Run test script
       run: FAIL_FAST=1 ./scripts/run_cpython_tests.sh ${{ matrix.python_version }}
       working-directory: Tools/Python

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
@@ -158,6 +158,28 @@ protected def instTypeM {m α} [Monad m] (d : TypeExprF α) (bindings : α → N
   | .arrow n a b => .arrow n <$> a.instTypeM bindings <*> b.instTypeM bindings
 termination_by d
 
+/-- Monadic map over all annotations in a type expression. -/
+@[specialize]
+def mapAnnM {α β} {m} [Monad m] (t : TypeExprF α) (f : α → m β)
+    : m (TypeExprF β) := do
+  match t with
+  | .ident ann name args =>
+    return .ident (← f ann) name
+      (← args.attach.mapM fun ⟨e, _⟩ => e.mapAnnM f)
+  | .bvar ann index => return .bvar (← f ann) index
+  | .tvar ann name => return .tvar (← f ann) name
+  | .fvar ann fv args =>
+    return .fvar (← f ann) fv
+      (← args.attach.mapM fun ⟨e, _⟩ => e.mapAnnM f)
+  | .arrow ann arg res =>
+    return .arrow (← f ann) (← arg.mapAnnM f) (← res.mapAnnM f)
+termination_by t
+
+/-- Map over all annotations in a type expression. -/
+@[specialize]
+def mapAnn {α β} (t : TypeExprF α) (f : α → β) : TypeExprF β :=
+  t.mapAnnM (m := Id) f
+
 end TypeExprF
 
 /-- Separator format for sequence formatting -/
@@ -267,128 +289,104 @@ end OperationF
 
 namespace ExprF
 
+/--
+Flattens a curried application expression into its head and list of arguments.
+For example, `((f a) b) c` becomes `(f, [a, b, c])`.
+-/
 public def flatten {α} (e : ExprF α) (prev : List (ArgF α) := []) : ExprF α × List (ArgF α) :=
   match e with
   | .app _ f e => f.flatten (e :: prev)
   | _ => (e, prev)
 
 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 }
+/-- Monadic map over all annotations in a syntax category. -/
+@[specialize]
+def SyntaxCatF.mapAnnM {α β} {m} [Monad m] (c : SyntaxCatF α)
+    (f : α → m β) : m (SyntaxCatF β) := do
+  return {
+    ann := ← f c.ann
+    name := c.name
+    args := ← c.args.attach.mapM fun ⟨e, _⟩ => e.mapAnnM f
+  }
+termination_by sizeOf c
+decreasing_by
+  cases c
+  case mk ann name args =>
+    decreasing_tactic
 
-/-- 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 }
+/-- Map over all annotations in a syntax category. -/
+@[specialize]
+def SyntaxCatF.mapAnn {α β} (c : SyntaxCatF α) (f : α → β) : SyntaxCatF β :=
+  c.mapAnnM (m := Id) f
 
-/-- Create a DiagnosticModel with source location. -/
-def DiagnosticModel.withRange (fr : FileRange) (msg : Format) : DiagnosticModel :=
-  { fileRange := fr, message := toString msg }
+mutual
 
-/-- 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})"
+/-- Monadic map over all annotations in an expression. -/
+@[specialize]
+def ExprF.mapAnnM {α β} {m} [Monad m] (e : ExprF α) (f : α → m β)
+    : m (ExprF β) := do
+  match e with
+  | .bvar ann idx => return .bvar (← f ann) idx
+  | .fvar ann idx => return .fvar (← f ann) idx
+  | .fn ann ident => return .fn (← f ann) ident
+  | .app ann e a =>
+    return .app (← f ann) (← e.mapAnnM f) (← a.mapAnnM f)
+termination_by sizeOf e
+
+/-- Monadic map over all annotations in an argument. -/
+@[specialize]
+def ArgF.mapAnnM {α β} {m} [Monad m] (a : ArgF α) (f : α → m β)
+    : m (ArgF β) := do
+  match a with
+  | .op o => return .op (← o.mapAnnM f)
+  | .cat c => return .cat (← c.mapAnnM f)
+  | .expr e => return .expr (← e.mapAnnM f)
+  | .type t => return .type (← t.mapAnnM f)
+  | .ident ann i => return .ident (← f ann) i
+  | .num ann v => return .num (← f ann) v
+  | .decimal ann v => return .decimal (← f ann) v
+  | .strlit ann i => return .strlit (← f ann) i
+  | .bytes ann b => return .bytes (← f ann) b
+  | .option ann none => return .option (← f ann) none
+  | .option ann (some a) =>
+    return .option (← f ann) (some (← a.mapAnnM f))
+  | .seq ann sep l =>
+    return .seq (← f ann) sep
+      (← l.attach.mapM fun ⟨e, _⟩ => e.mapAnnM f)
+termination_by sizeOf a
+
+/-- Map a monadic function over all annotations in an operation. -/
+@[specialize]
+def OperationF.mapAnnM {α β} {m} [Monad m] (op : OperationF α)
+    (f : α → m β) : m (OperationF β) := do
+  return {
+    ann := ← f op.ann
+    name := op.name
+    args := ← op.args.attach.mapM fun ⟨e, _⟩ => e.mapAnnM f
+  }
+termination_by sizeOf op
+decreasing_by
+  cases op
+  case mk ann name args =>
+    decreasing_tactic
 
-/-- 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}"
+end
 
-/-- 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?
+/-- Map a pure function over all annotations in an expression. -/
+@[specialize]
+def ExprF.mapAnn {α β} (e : ExprF α) (f : α → β) : ExprF β :=
+  e.mapAnnM (m := Id) f
 
-/-- 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
+/-- Map a pure function over all annotations in an argument. -/
+@[specialize]
+def ArgF.mapAnn {α β} (a : ArgF α) (f : α → β) : ArgF β :=
+  a.mapAnnM (m := Id) f
 
-instance : ToString DiagnosticModel where
-  toString dm := dm.format none |> toString
+/-- Map a pure function over all annotations in an operation. -/
+@[specialize]
+def OperationF.mapAnn {α β} (op : OperationF α) (f : α → β) : OperationF β :=
+  op.mapAnnM (m := Id) f
 
 abbrev Arg := ArgF SourceRange
 abbrev Expr := ExprF SourceRange
@@ -612,6 +610,10 @@ end Metadata
 
 abbrev Var := String
 
+/--
+Converts a deBruijn index to a level (counting from the start rather than
+the end). Used internally for metadata argument processing.
+-/
 private def catbvarLevel (varCount : Nat) : MetadataArg → Nat
 | .catbvar idx =>
   if idx < varCount then
@@ -1068,6 +1070,7 @@ def nameIndex {argDecls} : BindingSpec argDecls → DebruijnIndex argDecls.size
 
 end BindingSpec
 
+/-- Monad for parsing new binding specifications, accumulating error messages. -/
 private abbrev NewBindingM := StateM (Array String)
 
 private def newBindingErr (msg : String) : NewBindingM Unit :=
@@ -1713,7 +1716,9 @@ end DialectMap
 mutual
 
 /--
-Invoke a function `f` over each of the declaration specifications for an arg.
+Recursively folds over all binding specifications declared within an argument.
+Used to collect type bindings, value bindings, and other declarations that
+appear nested within operation arguments.
 -/
 partial def foldOverArgBindingSpecs {α β}
     (m : DialectMap)
@@ -1750,7 +1755,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

@@ -73,7 +73,7 @@ deriving Inhabited
 
 namespace PrecFormat
 
-private def atom (format : Format) : PrecFormat := { format, prec := maxPrec }
+private def atom (format : Format) : PrecFormat := { format, prec := maxPrec + 1 }
 
 private def ofFormat {α} [Std.ToFormat α] (x : α) (prec : Nat := maxPrec) : PrecFormat := { format := Std.format x, prec }
 
@@ -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

@@ -82,7 +82,10 @@ end Ion.Ion
 
 namespace Strata
 
-
+/--
+Represents an Ion value that is either a symbol/string or a non-empty
+s-expression. The size proof ensures termination in recursive deserialization.
+-/
 private inductive StringOrSexp (v : Ion SymbolId) where
 | string (s : String)
 | sexp (a : Array (Ion SymbolId)) (p : a.size > 0 ∧ sizeOf a < sizeOf v)
@@ -92,6 +95,11 @@ private inductive Required where
 | opt
 deriving DecidableEq
 
+/--
+Maps struct field names to their position indices, tracking which fields are
+required. Used during Ion deserialization to validate that all required fields
+are present.
+-/
 private structure StructArgMap (size : Nat) where
   map : Std.HashMap String (Fin size) := {}
   required : Array (String × Fin size)
@@ -259,6 +267,11 @@ private def sizeOfArrayLowerBound [h : SizeOf α] (a : Array α) : sizeOf a ≥
     have p := sizeOfListLowerBound l
     decreasing_tactic
 
+/--
+Maps an array of Ion struct fields to a fixed-size vector according to the
+StructArgMap, validating that all required fields are present and no fields are
+duplicated.
+-/
 private def mapFields {size} (args : Array (SymbolId × Ion SymbolId)) (m : StructArgMap size) :
   FromIonM (Vector (Ion SymbolId) size) := do
   -- We use an assigned vector below to check
@@ -598,7 +611,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]
@@ -1452,7 +1465,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 =>