From bbb3c3b668cac615c551308ed9af99c89c335c32 Mon Sep 17 00:00:00 2001 From: Joe Hendrix Date: Thu, 5 Mar 2026 19:56:47 -0800 Subject: [PATCH] Add --skip flag, failed import fallback, and overload body handling MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Improves the robustness of the pySpecs command so it reports failures gracefully — including regex usage — instead of aborting, and extracts the core logic into a reusable API with CLI flags for skipping definitions, controlling verbosity, and selecting log events. - Graceful failure handling: when a Python import cannot be resolved, the translator now registers the imported names as opaque extern types and continues, rather than aborting. Overload stubs with unexpected bodies produce a warning instead of failing. - Regex support: `from re import compile` is recognized via the built-in prelude, so Python files that use regex no longer trigger unknown-identifier errors. - Reusable API: the translation logic that was inline in the CLI callback is extracted into a self-contained entry point in SimpleAPI, returning structured errors instead of calling exitFailure. - CLI flags: --skip omits named top-level definitions (overloads kept), --quiet suppresses logging and warnings, --log enables event types. - Warning pipeline: warnings are collected during translation and returned as data; a three-level verbosity setting controls reporting. - Composable assertion expressions: the expression tree is refactored from fused nodes into orthogonal building blocks, making serialization a direct structural recursion with no special cases. - Readable DDM output: ensure(pred, msg) format, infix comparisons, indented class member blocks. - Event logging cleanup: global mutable reference replaced by a context- threaded event set. --- Strata/Languages/Python/Specs.lean | 131 +++++++++++++++------ Strata/Languages/Python/Specs/DDM.lean | 92 +++++++++------ Strata/Languages/Python/Specs/Decls.lean | 16 +-- Strata/SimpleAPI.lean | 85 +++++++++++++ StrataMain.lean | 51 ++++---- StrataTest/Languages/Python/Specs/main.py | 1 + StrataTest/Languages/Python/SpecsTest.lean | 8 +- 7 files changed, 274 insertions(+), 110 deletions(-) diff --git a/Strata/Languages/Python/Specs.lean b/Strata/Languages/Python/Specs.lean index 9184e3d48..0aba12c7a 100644 --- a/Strata/Languages/Python/Specs.lean +++ b/Strata/Languages/Python/Specs.lean @@ -25,17 +25,11 @@ public abbrev EventType := String def importEvent : EventType := "import" /-- -Set of event types to log to stderr. Test code can modify this to -enable/disable logging. --/ -initialize stdoutEventsRef : IO.Ref (Std.HashSet EventType) ← IO.mkRef {} - -/-- -Log message for event type if enabled in `stdoutEventsRef`. +Log message for event type if enabled in the given event set. Output format: `[event]: message` -/ -def logEvent (event : EventType) (message : String) : BaseIO Unit := do - let events ← stdoutEventsRef.get +def baseLogEvent (events : Std.HashSet EventType) + (event : EventType) (message : String) : BaseIO Unit := do if event ∈ events then let _ ← IO.eprintln s!"[{event}]: {message}" |>.toBaseIO pure () @@ -148,6 +142,7 @@ inductive SpecValue | typingRequired | typingNotRequired | typingUnpack +| reCompile | requiredType (type : SpecType) | notRequiredType (type : SpecType) | typeValue (type : SpecType) @@ -206,6 +201,7 @@ def preludeSig := .mk .typingRequired .typingRequired, .mk .typingNotRequired .typingNotRequired, .mk .typingUnpack .typingUnpack, + .mk .reCompile .reCompile, ] inductive ClassRef where @@ -216,6 +212,10 @@ inductive ClassRef where abbrev ModuleReader := ModuleName → EIO String System.FilePath structure PySpecContext where + /-- Events to log -/ + eventSet : Std.HashSet String + /-- Top-level definitions to skip. -/ + skipNames : Std.HashSet PythonIdent := {} /-- Command to run for Python -/ pythonCmd : String /-- Path to Python dialect. -/ @@ -256,6 +256,23 @@ structure PySpecState where abbrev PySpecM := ReaderT PySpecContext (StateT PySpecState BaseIO) +def logEvent (event : EventType) (message : String) : PySpecM Unit := do + baseLogEvent (←read).eventSet event message + +/-- Check whether a decorator list contains `@overload`. -/ +private def hasOverloadDecorator + (decorators : Array (Strata.Python.expr Strata.SourceRange)) : Bool := + decorators.any fun d => + match d with + | .Name _ ⟨_, "overload"⟩ _ => true + | _ => false + +/-- Should we skip the given top-level name? -/ +def shouldSkip (name : String) : PySpecM Bool := do + let ctx ← read + let mod := ctx.pythonFile.fileStem.getD "" + return ctx.skipNames.contains { pythonModule := mod, name } + def specErrorAt (file : System.FilePath) (loc : SourceRange) (message : String) : PySpecM Unit := do let e : SpecError := { file, loc, message } modify fun s => { s with errors := s.errors.push e } @@ -448,7 +465,8 @@ def translateConstant (value : constant SourceRange) : PySpecM SpecValue := do specError value.ann s!"Could not interpret constant {value}" return default -def translateSubscript (paramLoc : SourceRange) (paramType : String) (sargs : SpecValue) : PySpecM SpecValue := do +def translateSubscript (paramLoc : SourceRange) (paramType : String) + (sargs : SpecValue) : PySpecM SpecValue := do match ← getNameValue? paramType with | none => specError paramLoc s!"Unknown parameterized type {paramType}." @@ -757,12 +775,12 @@ def transAssertExpr (e : expr SourceRange) | .GtE _ => match comparators.val[0] with | .Constant _ (.ConPos _ n) _ => - return .lenGe subj n.val + return .intGe (.len subj) (.intLit n.val) | _ => pure () | .LtE _ => match comparators.val[0] with | .Constant _ (.ConPos _ n) _ => - return .lenLe subj n.val + return .intLe (.len subj) (.intLit n.val) | _ => pure () | _ => pure () | none => pure () @@ -778,16 +796,16 @@ def transAssertExpr (e : expr SourceRange) | .GtE _ => match comparators.val[0] with | .Constant _ (.ConPos _ n) _ => - return .valueGe subj (Int.ofNat n.val) + return .intGe subj (.intLit (Int.ofNat n.val)) | .Constant _ (.ConNeg _ n) _ => - return .valueGe subj (Int.negOfNat n.val) + return .intGe subj (.intLit (Int.negOfNat n.val)) | _ => pure () | .LtE _ => match comparators.val[0] with | .Constant _ (.ConPos _ n) _ => - return .valueLe subj (Int.ofNat n.val) + return .intLe subj (.intLit (Int.ofNat n.val)) | .Constant _ (.ConNeg _ n) _ => - return .valueLe subj (Int.negOfNat n.val) + return .intLe subj (.intLit (Int.negOfNat n.val)) | _ => pure () | _ => pure () | none => pure () @@ -945,7 +963,14 @@ def pySpecFunctionArgs (fnLoc : SourceRange) match returns with | none => pure <| .ident fnLoc .typingAny | some tp => pySpecType tp - let as ← collectAssertions argDecls returnType <| body.forM blockStmt + let as ← collectAssertions argDecls returnType <| + if overload then + -- Overload stubs should have `...` as their only body statement. + unless body.size = 1 && + body[0]! matches .Expr _ (.Constant _ (.ConEllipsis _) _) do + specWarning fnLoc "overload body is not `...`" + else + body.forM blockStmt return { loc := fnLoc @@ -1039,7 +1064,8 @@ def checkLevel (loc : SourceRange) (level : Option (int SourceRange)) : PySpecM | none => specError loc s!"Missing import level." -def translateImportFrom (mod : String) (types : Std.HashMap String SpecValue) (names : Array (alias SourceRange)) : PySpecM Unit := do +def translateImportFrom (mod : String) (types : Std.HashMap String SpecValue) + (names : Array (alias SourceRange)) : PySpecM Unit := do -- Check if module is a builtin (in prelude) - if so, don't generate extern declarations let isBuiltinModule := preludeSig.rank.contains mod for a in names do @@ -1126,15 +1152,14 @@ partial def resolveModule (loc : SourceRange) (modName : String) : | .error _ => false -- If Strata is newer use it. if useStrata then - logEvent importEvent s!"Importing {modName} from PySpec file" match ← readDDM strataFile |>.toBaseIO with | .ok sigs => + logEvent importEvent s!"Imported {modName} from PySpec file" return signatureValueMap modName sigs | .error msg => specError loc s!"Could not load Strata file: {msg}" return default - logEvent importEvent s!"Importing {modName} from Python" let pythonCmd := (←read).pythonCmd let dialectFile := (←read).dialectFile let commands ← @@ -1144,13 +1169,18 @@ partial def resolveModule (loc : SourceRange) (modName : String) : specError loc msg return default let errors := (←get).errors + let warnings := (←get).warnings let errorCount := errors.size - modify fun s => { s with errors := #[] } + modify fun s => { s with errors := #[], warnings := #[] } let ctx := { (←read) with pythonFile := pythonFile } - let (sigs, t) ← translateModuleAux commands |>.run ctx |>.run { errors := errors } - modify fun s => { s with errors := t.errors } + let initState : PySpecState := { errors, warnings } + let (sigs, t) ← translateModuleAux commands |>.run ctx |>.run initState + let newWarnings := t.warnings.size - warnings.size + modify fun s => { s with errors := t.errors, warnings := t.warnings } if t.errors.size > errorCount then return default + let warnMsg := if newWarnings > 0 then s!" ({newWarnings} warning(s))" else "" + logEvent importEvent s!"Imported {modName}{warnMsg}" if let .error msg ← IO.FS.createDirAll strataDir |>.toBaseIO then specError loc s!"Could not create directory {strataDir}: {msg}" @@ -1173,7 +1203,7 @@ partial def resolveModuleCached (loc : SourceRange) (modName : String) modify fun s => { s with typeSigs := s.typeSigs.insert modName r } return r -partial def translate (body : Array (Strata.Python.stmt Strata.SourceRange)) : PySpecM Unit := do +partial def translate (body : Array (stmt Strata.SourceRange)) : PySpecM Unit := do for stmt in body do match stmt with | .Assign loc ⟨_, targets⟩ value _typeAnn => @@ -1208,6 +1238,9 @@ partial def translate (body : Array (Strata.Python.stmt Strata.SourceRange)) : P ⟨_returnsLoc, returns⟩ ⟨_typeCommentLoc, typeComment⟩ ⟨_typeParamsLoc, typeParams⟩ => + if hasOverloadDecorator decorators = false ∧ (←shouldSkip funName) then + logEvent "skip" s!"Skipping function {funName}" + continue assert! _bodyLoc.isNone -- Flag indicating this is an overload assert! _decoratorsLoc.isNone @@ -1228,7 +1261,21 @@ partial def translate (body : Array (Strata.Python.stmt Strata.SourceRange)) : P | specError loc s!"Local imports not supported"; continue if let some types ← resolveModuleCached loc mod then translateImportFrom mod types names + else + -- Module resolution failed; register imported names as opaque extern + -- types so that downstream references don't produce unknown-identifier + -- errors. + for a in names do + let name := a.name + let asname := a.asname.getD name + let source : PythonIdent := { pythonModule := mod, name := name } + let tpv : SpecValue := .typeValue (.ident loc source) + setNameValue asname tpv + pushSignature (.externTypeDecl asname source) | .ClassDef loc ⟨_classNameLoc, className⟩ bases keywords stmts decorators typeParams => + if ←shouldSkip className then + logEvent "skip" s!"Skipping class {className}" + continue assert! _classNameLoc.isNone assert! keywords.val.size = 0 assert! decorators.val.size = 0 @@ -1275,29 +1322,37 @@ end /-- Maps file paths to their FileMap for error location reporting. -/ public abbrev FileMaps := Std.HashMap System.FilePath Lean.FileMap -def FileMaps.ppSourceRange (fmm : Strata.Python.Specs.FileMaps) (path : System.FilePath) (loc : SourceRange) : String := +namespace FileMaps + +def ppSourceRange (fmm : FileMaps) (path : System.FilePath) (loc : SourceRange) : String := match fmm[path]? with | none => panic! "Invalid path {file}" | some fm => loc.format path fm +end FileMaps + /-- Translates Python AST statements to PySpec signatures with dependency resolution. -/ def translateModule (dialectFile searchPath strataDir pythonFile : System.FilePath) (fileMap : Lean.FileMap) (body : Array (Strata.Python.stmt Strata.SourceRange)) - (pythonCmd : String := "python") : - BaseIO (FileMaps × Array Signature × Array SpecError) := do + (pythonCmd : String := "python") + (events : Std.HashSet EventType := {}) + (skipNames : Std.HashSet PythonIdent := {}) : + BaseIO (FileMaps × Array Signature × Array SpecError × Array SpecError) := do let fmm : FileMaps := {} let fmm := fmm.insert pythonFile fileMap let fileMapsRef : IO.Ref FileMaps ← IO.mkRef fmm let ctx : PySpecContext := { + eventSet := events + skipNames := skipNames pythonCmd := pythonCmd dialectFile := dialectFile.toString moduleReader := fun (mod : ModuleName) => do let pythonPath ← mod.findInPath searchPath - logEvent "findFile" s!"Found {mod} as {pythonPath} in {searchPath}" + baseLogEvent events "findFile" s!"Found {mod} as {pythonPath} in {searchPath}" match ← IO.FS.readFile pythonPath |>.toBaseIO with | .ok contents => let fm := Lean.FileMap.ofString contents @@ -1310,16 +1365,16 @@ def translateModule } let (res, s) ← translateModuleAux body |>.run ctx |>.run {} let fmm ← fileMapsRef.get - for w in s.warnings do - let _ ← IO.eprintln s!"warning: {fmm.ppSourceRange w.file w.loc}: {w.message}" |>.toBaseIO - pure (fmm, res, s.errors) + pure (fmm, res, s.errors, s.warnings) /-- Translates a Python source file to PySpec signatures. Main entry point for translation. -/ public def translateFile (dialectFile strataDir pythonFile : System.FilePath) (pythonCmd : String := "python") - (searchPath : Option System.FilePath := none) : - EIO String (Array Signature) := do + (searchPath : Option System.FilePath := none) + (events : Std.HashSet EventType := {}) + (skipNames : Std.HashSet PythonIdent := {}) : + EIO String (Array Signature × Array String) := do let searchPath ← match searchPath with | some p => pure p @@ -1340,9 +1395,11 @@ public def translateFile match ← pythonToStrata (pythonCmd := pythonCmd) dialectFile pythonFile |>.toBaseIO with | .ok r => pure r | .error msg => throw msg - let (fmm, sigs, errors) ← - Strata.Python.Specs.translateModule + let (fmm, sigs, errors, warnings) ← + translateModule (pythonCmd := pythonCmd) + (events := events) + (skipNames := skipNames) (dialectFile := dialectFile) (searchPath := searchPath) (strataDir := strataDir) @@ -1354,6 +1411,8 @@ public def translateFile let msg := errors.foldl (init := msg) fun msg e => s!"{msg}{fmm.ppSourceRange pythonFile e.loc}: {e.message}\n" throw msg - pure sigs + let warningMsgs := warnings.map fun w => + s!"{fmm.ppSourceRange w.file w.loc}: {w.message}" + pure (sigs, warningMsgs) end Strata.Python.Specs diff --git a/Strata/Languages/Python/Specs/DDM.lean b/Strata/Languages/Python/Specs/DDM.lean index 6495764b2..5dca2aa35 100644 --- a/Strata/Languages/Python/Specs/DDM.lean +++ b/Strata/Languages/Python/Specs/DDM.lean @@ -30,14 +30,17 @@ category SpecType; category DictFieldDecl; op typeIdentNoArgs (x : Str) : SpecType => "ident" "(" x ")"; -op typeIdent (x : Str, y : CommaSepBy SpecType) : SpecType => "ident" "(" x ", " y ")"; +op typeIdent (x : Str, y : CommaSepBy SpecType) : SpecType => + "ident" "(" x ", " y ")"; op typeClassNoArgs (x : Ident) : SpecType => "class" "(" x ")"; -op typeClass (x : Ident, y : CommaSepBy SpecType) : SpecType => "class" "(" x ", " y ")"; +op typeClass (x : Ident, y : CommaSepBy SpecType) : SpecType => + "class" "(" x ", " y ")"; op typeIntLiteral (x : Int) : SpecType => x; op typeStringLiteral (x : Str) : SpecType => x; -op typeUnion (args : CommaSepBy SpecType) : SpecType => "union" "(" args ")"; -op typeTypedDict (fields : CommaSepBy DictFieldDecl): SpecType => - "dict" "(" fields ")"; +op typeUnion (args : CommaSepBy SpecType) : SpecType => + "union" "(" args ")"; +op typeTypedDict (fields : NewlineSepBy DictFieldDecl): SpecType => + "dict" "(\n" indent(2, fields) ")"; op mkDictFieldDecl(name : Ident, fieldType : SpecType, isRequired : Bool) : DictFieldDecl => name " : " fieldType " [required=" isRequired "]"; @@ -59,28 +62,29 @@ op mkKwargsDecl(name : Ident, kwargsType : SpecType) : KwargsDecl => "kwargs" ": " name " : " kwargsType "\n"; category SpecExprDecl; -op placeholderExpr() : SpecExprDecl => - "placeholder" "\n"; -op varExpr(name : Ident) : SpecExprDecl => - name "\n"; +op placeholderExpr() : SpecExprDecl => "placeholder"; +op varExpr(name : Ident) : SpecExprDecl => name; op getIndexExpr(subject : SpecExprDecl, field : Ident) : SpecExprDecl => - subject "[" field "]" "\n"; + subject "[" field "]"; op isInstanceOfExpr(subject : SpecExprDecl, typeName : Str) : SpecExprDecl => - "isinstance(" subject ", " typeName ")" "\n"; -op lenGeExpr(subject : SpecExprDecl, bound : Num) : SpecExprDecl => - "len_ge(" subject ", " bound ")" "\n"; -op lenLeExpr(subject : SpecExprDecl, bound : Num) : SpecExprDecl => - "len_le(" subject ", " bound ")" "\n"; -op valueGeExpr(subject : SpecExprDecl, bound : Int) : SpecExprDecl => - "value_ge(" subject ", " bound ")" "\n"; -op valueLeExpr(subject : SpecExprDecl, bound : Int) : SpecExprDecl => - "value_le(" subject ", " bound ")" "\n"; + "isinstance(" subject ", " typeName ")"; +op lenExpr(subject : SpecExprDecl) : SpecExprDecl => + "len(" subject ")"; +op intExpr(value : Int) : SpecExprDecl => value; +op intGeExpr(subject : SpecExprDecl, bound : SpecExprDecl) : SpecExprDecl => + subject " >= " bound; +op intLeExpr(subject : SpecExprDecl, bound : SpecExprDecl) : SpecExprDecl => + subject " <= " bound; op enumMemberExpr(subject : SpecExprDecl, values : Seq Str) : SpecExprDecl => - "enum(" subject ", [" values "])" "\n"; + "enum(" subject ", [" values "])"; category Assertion; op mkAssertion(formula : SpecExprDecl, message : Str) : Assertion => - formula " " message "\n"; + "ensure(" formula ", " message ")\n"; + +category PostconditionEntry; +op mkPostconditionEntry(expr : SpecExprDecl) : PostconditionEntry => + expr "\n"; category FunDecl; op mkFunDecl (name : Str, @@ -90,7 +94,8 @@ op mkFunDecl (name : Str, returnType : SpecType, isOverload : Bool, preconditions : Seq Assertion, - postconditions : Seq SpecExprDecl) : FunDecl => + postconditions : Seq PostconditionEntry) + : FunDecl => "function " name "{\n" indent(2, "args" ": " "[\n" @@ -111,15 +116,23 @@ op mkFunDecl (name : Str, "}\n"; category ClassDecl; -op mkClassDecl(name : Str, bases : Seq Str, fields : Seq ClassFieldDecl, - classVars : Seq ClassVarDecl, subclasses : Seq ClassDecl, - methods : Seq FunDecl) : ClassDecl => +op mkClassDecl(name : Str, bases : Seq Str, + fields : Seq ClassFieldDecl, + classVars : Seq ClassVarDecl, + subclasses : Seq ClassDecl, + methods : Seq FunDecl) : ClassDecl => "class " name " {\n" indent(2, "bases" ": " "[" bases "]\n" - "fields" ": " "[" fields "]\n" - "classVars" ": " "[" classVars "]\n" - "subclasses" ": " "[" subclasses "]\n" + "fields" ": " "[\n" + indent(2, fields) + "]\n" + "classVars" ": " "[\n" + indent(2, classVars) + "]\n" + "subclasses" ": " "[\n" + indent(2, subclasses) + "]\n" methods) "}\n"; @@ -199,10 +212,10 @@ private def SpecExpr.toDDM (e : SpecExpr) : DDM.SpecExprDecl SourceRange := | .var name => .varExpr .none ⟨.none, name⟩ | .getIndex subj field => .getIndexExpr .none subj.toDDM ⟨.none, field⟩ | .isInstanceOf subj tn => .isInstanceOfExpr .none subj.toDDM ⟨.none, tn⟩ - | .lenGe subj bound => .lenGeExpr .none subj.toDDM ⟨.none, bound⟩ - | .lenLe subj bound => .lenLeExpr .none subj.toDDM ⟨.none, bound⟩ - | .valueGe subj bound => .valueGeExpr .none subj.toDDM (toDDMInt .none bound) - | .valueLe subj bound => .valueLeExpr .none subj.toDDM (toDDMInt .none bound) + | .len subj => .lenExpr .none subj.toDDM + | .intLit v => .intExpr .none (toDDMInt .none v) + | .intGe subj bound => .intGeExpr .none subj.toDDM bound.toDDM + | .intLe subj bound => .intLeExpr .none subj.toDDM bound.toDDM | .enumMember subj values => .enumMemberExpr .none subj.toDDM ⟨.none, values.map (⟨.none, ·⟩)⟩ @@ -223,7 +236,9 @@ private def FunctionDecl.toDDM (d : FunctionDecl) : DDM.FunDecl SourceRange := (returnType := d.returnType.toDDM) (isOverload := ⟨.none, d.isOverload⟩) (preconditions := ⟨.none, d.preconditions.map (·.toDDM)⟩) - (postconditions := ⟨.none, d.postconditions.map (·.toDDM)⟩) + (postconditions := ⟨.none, + d.postconditions.map fun e => + .mkPostconditionEntry .none e.toDDM⟩) private def ClassVariable.toDDM (cv : ClassVariable) : DDM.ClassVarDecl SourceRange := .mkClassVarDecl .none ⟨.none, cv.name⟩ ⟨.none, cv.value⟩ @@ -304,10 +319,10 @@ private def DDM.SpecExprDecl.fromDDM (d : DDM.SpecExprDecl SourceRange) : Specs. | .varExpr _ ⟨_, name⟩ => .var name | .getIndexExpr _ subj ⟨_, field⟩ => .getIndex subj.fromDDM field | .isInstanceOfExpr _ subj ⟨_, tn⟩ => .isInstanceOf subj.fromDDM tn - | .lenGeExpr _ subj ⟨_, bound⟩ => .lenGe subj.fromDDM bound - | .lenLeExpr _ subj ⟨_, bound⟩ => .lenLe subj.fromDDM bound - | .valueGeExpr _ subj bound => .valueGe subj.fromDDM bound.ofDDM - | .valueLeExpr _ subj bound => .valueLe subj.fromDDM bound.ofDDM + | .lenExpr _ subj => .len subj.fromDDM + | .intExpr _ i => .intLit i.ofDDM + | .intGeExpr _ subj bound => .intGe subj.fromDDM bound.fromDDM + | .intLeExpr _ subj bound => .intLe subj.fromDDM bound.fromDDM | .enumMemberExpr _ subj ⟨_, values⟩ => .enumMember subj.fromDDM (values.map (·.2)) private def DDM.Assertion.fromDDM (d : DDM.Assertion SourceRange) : Specs.Assertion := @@ -334,7 +349,8 @@ private def DDM.FunDecl.fromDDM (d : DDM.FunDecl SourceRange) : Specs.FunctionDe returnType := returnType.fromDDM isOverload := isOverload preconditions := preconditions.map (·.fromDDM) - postconditions := postconditions.map (·.fromDDM) + postconditions := postconditions.map fun + | .mkPostconditionEntry _ e => e.fromDDM } private def DDM.ClassDecl.fromDDM (d : DDM.ClassDecl SourceRange) : Specs.ClassDef := diff --git a/Strata/Languages/Python/Specs/Decls.lean b/Strata/Languages/Python/Specs/Decls.lean index 30306a8a3..b555cfd60 100644 --- a/Strata/Languages/Python/Specs/Decls.lean +++ b/Strata/Languages/Python/Specs/Decls.lean @@ -57,6 +57,7 @@ def typingUnion := mk "typing" "Union" def typingRequired := mk "typing" "Required" def typingNotRequired := mk "typing" "NotRequired" def typingUnpack := mk "typing" "Unpack" +def reCompile := mk "re" "compile" end PythonIdent @@ -317,9 +318,10 @@ def count (ad : ArgDecls) := ad.args.size + ad.kwonly.size end ArgDecls /-- -A specification expression with `free` free variables (arguments + return value -for postconditions). Supports value and predicate expressions for assert -statements in function bodies. +A composable expression tree for translating Python `assert` statements into +structured preconditions and postconditions. Leaf nodes are `var`, `intLit`, +and `placeholder`; interior nodes represent operations like `len`, `getIndex`, +`intGe`/`intLe`, `isInstanceOf`, and `enumMember`. -/ inductive SpecExpr where /-- Stands in for an assert pattern not yet supported by the translator. @@ -328,10 +330,10 @@ inductive SpecExpr where | var (name : String) | getIndex (subject : SpecExpr) (field : String) | isInstanceOf (subject : SpecExpr) (typeName : String) -| lenGe (subject : SpecExpr) (bound : Nat) -- Nat: len() is non-negative -| lenLe (subject : SpecExpr) (bound : Nat) -| valueGe (subject : SpecExpr) (bound : Int) -- Int: values may be negative -| valueLe (subject : SpecExpr) (bound : Int) +| len (subject : SpecExpr) +| intLit (value : Int) +| intGe (subject : SpecExpr) (bound : SpecExpr) +| intLe (subject : SpecExpr) (bound : SpecExpr) | enumMember (subject : SpecExpr) (values : Array String) deriving Inhabited diff --git a/Strata/SimpleAPI.lean b/Strata/SimpleAPI.lean index af478e8c8..42a9c1d1e 100644 --- a/Strata/SimpleAPI.lean +++ b/Strata/SimpleAPI.lean @@ -20,6 +20,7 @@ import Strata.Languages.Laurel.Grammar.ConcreteToAbstractTreeTranslator import Strata.Languages.Laurel.LaurelToCoreTranslator import Strata.Languages.Python.Python +import Strata.Languages.Python.Specs /-! ## Simple Strata API @@ -184,3 +185,87 @@ Do deductive verification of a Core program, including any external solver invocation that is necessary. -/ noncomputable opaque Core.verify : Core.Program → Core.VerifyOptions → IO Core.VCResults + +/-- Controls how translation warnings are reported. -/ +inductive WarningOutput where + /-- Suppress all warning output. -/ + | none + /-- Print only a count summary (e.g., "3 warning(s)"). -/ + | summary + /-- Print each warning followed by a count summary. -/ + | detail +deriving Inhabited, BEq + +/-- +Translate a Python source file into PySpec signatures and write the result as a +DDM Ion file under `strataDir`. The output filename is derived from the Python +module name (e.g., `foo.bar` → `foo.bar.pyspec.st.ion`). + +The `dialectFile` path points to a serialized Python dialect used during +translation. Optional `events` controls logging (e.g., `"import"` for +import progress). + +Each entry in `skipNames` is either a qualified `"module.name"` string +(split on the last dot) or an unqualified `"name"` string (the module is +inferred from the Python file stem). Matching top-level definitions are +omitted from the output, except overloaded variants which are always kept. + +The `warningOutput` parameter controls how translation warnings are reported +to stderr: `.none` suppresses them, `.summary` prints only a count, and +`.detail` prints each warning followed by a count. +-/ +def pySpecs (pythonFile strataDir dialectFile : System.FilePath) + (events : Std.HashSet String := {}) + (skipNames : Array String := #[]) + (warningOutput : WarningOutput := .detail) + : EIO String Unit := do + -- Validate source file + match ← pythonFile.metadata |>.toBaseIO with + | .ok md => + if md.type != .file then + throw s!"Expected {pythonFile} to be a regular file" + | .error e => throw s!"Cannot access {pythonFile}: {e}" + + -- Parse skip names into PythonIdents + let some fileStem := pythonFile.fileStem + | throw s!"No file stem for {pythonFile}" + let stem := fileStem + + let mod ← match Strata.Python.Specs.ModuleName.ofString fileStem with + | .ok m => pure m + | .error e => throw s!"Invalid module name '{fileStem}': {e}" + + let skipIdents := skipNames.foldl (init := {}) fun acc s => + match Strata.Python.Specs.PythonIdent.ofString s with + | some id => acc.insert id + | none => acc.insert { pythonModule := stem, name := s } + + -- Create directory if it doesn't exist + match ← strataDir.metadata |>.toBaseIO with + | .ok md => + if md.type != .dir then + throw s!"Expected {strataDir} to be a directory" + | .error _ => + match ← IO.FS.createDirAll strataDir |>.toBaseIO with + | .ok () => pure () + | .error e => throw s!"Could not create {strataDir}: {e}" + + let (sigs, warnings) ← Strata.Python.Specs.translateFile + dialectFile strataDir pythonFile + (events := events) (skipNames := skipIdents) + + let strataFile := strataDir / mod.strataFileName + match ← Strata.Python.Specs.writeDDM strataFile sigs |>.toBaseIO with + | .ok () => pure () + | .error e => throw s!"Could not write {strataFile}: {e}" + + -- Report warnings + if warnings.size > 0 then + match warningOutput with + | .none => pure () + | .summary => + let _ ← IO.eprintln s!"{warnings.size} warning(s)" |>.toBaseIO + | .detail => + for w in warnings do + let _ ← IO.eprintln s!"warning: {w}" |>.toBaseIO + let _ ← IO.eprintln s!"{warnings.size} warning(s)" |>.toBaseIO diff --git a/StrataMain.lean b/StrataMain.lean index 434314257..a433650c8 100644 --- a/StrataMain.lean +++ b/StrataMain.lean @@ -167,36 +167,35 @@ def readPythonStrata (strataPath : String) : IO Strata.Program := do def pySpecsCommand : Command where name := "pySpecs" args := [ "python_path", "strata_path" ] + flags := [ + { name := "quiet", help := "Suppress default logging." }, + { name := "log", help := "Enable logging for an event type.", + takesArg := .repeat "event" }, + { name := "skip", + help := "Skip a top-level definition (module.name). Overloads are kept.", + takesArg := .repeat "name" } + ] help := "Translate a Python specification (.py) file into Strata DDM Ion format. Creates the output directory if needed. (Experimental)" - callback := fun v _ => do + callback := fun v pflags => do + let quiet := pflags.getBool "quiet" + let mut events : Std.HashSet String := {} + if !quiet then + events := events.insert "import" + for e in pflags.getRepeated "log" do + events := events.insert e + let skipNames := pflags.getRepeated "skip" + let warningOutput : Strata.WarningOutput := + if quiet then .none else .detail -- Serialize embedded dialect for Python subprocess IO.FS.withTempFile fun _handle dialectFile => do IO.FS.writeBinFile dialectFile Strata.Python.Python.toIon - let pythonFile : System.FilePath := v[0] - let strataDir : System.FilePath := v[1] - if (←pythonFile.metadata).type != .file then - exitFailure s!"Expected Python to be a regular file." - match ←strataDir.metadata |>.toBaseIO with - | .ok md => - if md.type != .dir then - exitFailure s!"Expected Strata to be a directory." - | .error _ => - IO.FS.createDir strataDir - let r ← Strata.Python.Specs.translateFile - (dialectFile := dialectFile) - (strataDir := strataDir) - (pythonFile := pythonFile) |>.toBaseIO - - let sigs ← - match r with - | .ok t => pure t - | .error msg => exitFailure msg - let some mod := pythonFile.fileStem - | exitFailure s!"No stem {pythonFile}" - let .ok mod := Strata.Python.Specs.ModuleName.ofString mod - | exitFailure s!"Invalid module {mod}" - let strataFile := strataDir / mod.strataFileName - Strata.Python.Specs.writeDDM strataFile sigs + let r ← Strata.pySpecs (events := events) + (skipNames := skipNames) + (warningOutput := warningOutput) + v[0] v[1] dialectFile |>.toBaseIO + match r with + | .ok () => pure () + | .error msg => exitFailure msg def pyTranslateCommand : Command where name := "pyTranslate" diff --git a/StrataTest/Languages/Python/Specs/main.py b/StrataTest/Languages/Python/Specs/main.py index 6fef3e5d3..b1635ce87 100644 --- a/StrataTest/Languages/Python/Specs/main.py +++ b/StrataTest/Languages/Python/Specs/main.py @@ -1,3 +1,4 @@ +from re import compile from basetypes import BaseClass from typing import Any, Dict, List, Sequence diff --git a/StrataTest/Languages/Python/SpecsTest.lean b/StrataTest/Languages/Python/SpecsTest.lean index 5588516a0..e909e7ed8 100644 --- a/StrataTest/Languages/Python/SpecsTest.lean +++ b/StrataTest/Languages/Python/SpecsTest.lean @@ -108,8 +108,8 @@ function "kwargs_function"{ return: ident("typing.Any") overload: false preconditions: [ - isinstance(kw[name], "str") "Expected name to be str" - value_ge(kw[count], 1) "Expected count >= 1" + ensure(isinstance(kw[name], "str"), "Expected name to be str") + ensure(kw[count] >= 1, "Expected count >= 1") ] postconditions: [ ] @@ -149,11 +149,13 @@ def testCase : IO Unit := do (pythonFile := pythonFile) |>.toBaseIO match r with - | .ok sigs => + | .ok (sigs, warnings) => let pgm := toDDMProgram sigs let pgmCommands := pgm.commands.map (·.mapAnn (fun _ => ())) let expCommands := expectedPySpec.commands.map (·.mapAnn (fun _ => ())) assert! pgmCommands == expCommands + -- from re import compile resolves via prelude without warnings + assert! warnings.isEmpty | .error e => throw <| IO.userError e