From 524a842ef74685025a2a4cc2dcc1e0d224668b09 Mon Sep 17 00:00:00 2001 From: Andrew Wells Date: Wed, 4 Mar 2026 02:24:46 +0000 Subject: [PATCH 1/2] Ignore pycache --- StrataTest/Languages/Python/.gitignore | 1 + 1 file changed, 1 insertion(+) diff --git a/StrataTest/Languages/Python/.gitignore b/StrataTest/Languages/Python/.gitignore index f7df56a3c..ba6cf4577 100644 --- a/StrataTest/Languages/Python/.gitignore +++ b/StrataTest/Languages/Python/.gitignore @@ -1,2 +1,3 @@ *.python.st.ion *.sarif +__pycache__ From f785214ee77c3f71318ea5d85566eb7240490f78 Mon Sep 17 00:00:00 2001 From: Andrew Wells Date: Wed, 4 Mar 2026 02:25:29 +0000 Subject: [PATCH 2/2] Simple handling for Any type --- .../Laurel/LaurelToCoreTranslator.lean | 38 +++++++-- Strata/Languages/Python/CorePrelude.lean | 34 +++++++- Strata/Languages/Python/PythonToLaurel.lean | 78 +++++++++++++++++-- 3 files changed, 136 insertions(+), 14 deletions(-) diff --git a/Strata/Languages/Laurel/LaurelToCoreTranslator.lean b/Strata/Languages/Laurel/LaurelToCoreTranslator.lean index ab8521161..5e86c42e6 100644 --- a/Strata/Languages/Laurel/LaurelToCoreTranslator.lean +++ b/Strata/Languages/Laurel/LaurelToCoreTranslator.lean @@ -72,6 +72,8 @@ def isCoreFunction (funcNames : FunctionNames) (name : Identifier) : Bool := name == "select" || name == "update" || name == "const" || -- Type hierarchy functions generated by typeHierarchyTransform name == "ancestorsPerType" || name.startsWith "ancestorsFor" || name.endsWith "_TypeTag" || + -- PyAnyType coercion functions (pyAny_to_*, pyAny_from_*) + name.startsWith "pyAny_" || funcNames.contains name /-- State threaded through expression and statement translation -/ @@ -82,6 +84,9 @@ structure TranslateState where fieldNames : List String := [] /-- Names of procedures that are translated as Core functions -/ funcNames : FunctionNames := [] + /-- Output parameter info for each procedure, used to generate discard variables + when a procedure call's return value is ignored. -/ + procOutputs : List (String × List Parameter) := [] /-- The translation monad: state over Id -/ abbrev TranslateM := StateT TranslateState Id @@ -244,7 +249,7 @@ def getNameFromMd (md : Imperative.MetaData Core.Expression): String := let fileRange := (Imperative.getFileRange md).getD (panic "getNameFromMd bug") s!"({fileRange.range.start})" -def defaultExprForType (ty : HighTypeMd) : Core.Expression.Expr := +def defaultExprForType (ty : HighTypeMd) (idx : Nat := 0) : Core.Expression.Expr := match ty.val with | .TInt => .const () (.intConst 0) | .TBool => .const () (.boolConst false) @@ -253,8 +258,10 @@ def defaultExprForType (ty : HighTypeMd) : Core.Expression.Expr := -- For types without a natural default (arrays, composites, etc.), -- use a fresh free variable. This is only used when the value is -- immediately overwritten by a procedure call. + -- Each call site must use a unique idx to avoid name collisions + -- that cause type-checking failures. let coreTy := translateType ty - .fvar () (⟨"$default", ()⟩) (some coreTy) + .fvar () (⟨s!"$default_{idx}", ()⟩) (some coreTy) /-- Translate Laurel StmtExpr to Core Statements using the `TranslateM` monad. @@ -293,7 +300,7 @@ def translateStmt (env : TypeEnv) (outputParams : List Parameter) (stmt : StmtEx else -- Translate as: var name; call name := callee(args) let coreArgs ← args.mapM (fun a => translateExpr env a) - let defaultExpr := defaultExprForType ty + let defaultExpr := defaultExprForType ty env'.length let initStmt := Core.Statement.init ident boogieType (some defaultExpr) md let callStmt := Core.Statement.call [ident] callee coreArgs md return (env', [initStmt, callStmt]) @@ -301,7 +308,7 @@ def translateStmt (env : TypeEnv) (outputParams : List Parameter) (stmt : StmtEx let coreExpr ← translateExpr env initExpr return (env', [Core.Statement.init ident boogieType (some coreExpr) md]) | none => - let defaultExpr := defaultExprForType ty + let defaultExpr := defaultExprForType ty env'.length return (env', [Core.Statement.init ident boogieType (some defaultExpr) md]) | .Assign targets value => match targets with @@ -348,7 +355,24 @@ def translateStmt (env : TypeEnv) (outputParams : List Parameter) (stmt : StmtEx return (env, []) else let coreArgs ← args.mapM (fun a => translateExpr env a) - return (env, [Core.Statement.call [] name coreArgs md]) + -- If the procedure has outputs but the call discards them, generate + -- temporary variables to capture the return values (Core requires arity match). + let outputs := s.procOutputs.lookup name |>.getD [] + if outputs.isEmpty then + return (env, [Core.Statement.call [] name coreArgs md]) + else + let discardVars : List (Core.Expression.Ident × LTy) := + outputs.mapIdx fun i p => + let ident : Core.Expression.Ident := ⟨s!"$discard_{env.length}_{i}", ()⟩ + let ty := translateType p.type + (ident, LTy.forAll [] ty) + let initStmts : List Core.Statement := + discardVars.map fun (ident, bty) => + Core.Statement.init ident bty none md + let lhsIdents : List Core.Expression.Ident := + discardVars.map fun (ident, _) => ident + let callStmt := Core.Statement.call lhsIdents name coreArgs md + return (env, initStmts ++ [callStmt]) | .Return valueOpt => match valueOpt, outputParams.head? with | some value, some outParam => @@ -576,7 +600,9 @@ def translate (program : Program) : Except (Array DiagnosticModel) (Core.Program let (markedPure, procProcs) := program.staticProcedures.partition (·.isFunctional) -- Build the shared initial state with constants and function names let funcNames : FunctionNames := markedPure.map (·.name) - let initState : TranslateState := { fieldNames := fieldNames, funcNames } + -- Build a map from procedure name to output parameters for arity-correct call translation. + let procOutputs := procProcs.map (fun p => (p.name, p.outputs)) + let initState : TranslateState := { fieldNames := fieldNames, funcNames, procOutputs } -- Try to translate each isFunctional procedure to a Core function, collecting errors for failures let (pureErrors, pureFuncDecls) := markedPure.foldl (fun (errs, decls) p => match tryTranslatePureToFunction p initState with diff --git a/Strata/Languages/Python/CorePrelude.lean b/Strata/Languages/Python/CorePrelude.lean index 60fd5adc5..0a2e70222 100644 --- a/Strata/Languages/Python/CorePrelude.lean +++ b/Strata/Languages/Python/CorePrelude.lean @@ -331,9 +331,37 @@ spec { assume [assume_maybe_except_none]: (ExceptOrNone..isExceptOrNone_mk_none(maybe_except)); }; -datatype PyAnyType () { - PyAnyType_Inhabitant() -}; +// PyAnyType: opaque type for Python's `Any` / unannotated values. +// Coercion functions let the translator bridge PyAnyType and concrete sorts. +type PyAnyType; + +// --- coercions: PyAnyType → concrete type --- +function pyAny_to_int(x : PyAnyType) : int; +function pyAny_to_bool(x : PyAnyType) : bool; +function pyAny_to_string(x : PyAnyType) : string; +function pyAny_to_ExceptOrNone(x : PyAnyType) : ExceptOrNone; +function pyAny_to_StrOrNone(x : PyAnyType) : StrOrNone; +function pyAny_to_IntOrNone(x : PyAnyType) : IntOrNone; +function pyAny_to_BoolOrNone(x : PyAnyType) : BoolOrNone; +function pyAny_to_AnyOrNone(x : PyAnyType) : AnyOrNone; +function pyAny_to_DictStrAny(x : PyAnyType) : DictStrAny; +function pyAny_to_ListStr(x : PyAnyType) : ListStr; +function pyAny_to_Datetime(x : PyAnyType) : Datetime; +function pyAny_to_None(x : PyAnyType) : None; +function pyAny_to_Object(x : PyAnyType) : Object; + +// --- coercions: concrete type → PyAnyType --- +function pyAny_from_int(x : int) : PyAnyType; +function pyAny_from_bool(x : bool) : PyAnyType; +function pyAny_from_string(x : string) : PyAnyType; +function pyAny_from_ExceptOrNone(x : ExceptOrNone) : PyAnyType; +function pyAny_from_StrOrNone(x : StrOrNone) : PyAnyType; +function pyAny_from_IntOrNone(x : IntOrNone) : PyAnyType; +function pyAny_from_DictStrAny(x : DictStrAny) : PyAnyType; +function pyAny_from_ListStr(x : ListStr) : PyAnyType; +function pyAny_from_Datetime(x : Datetime) : PyAnyType; +function pyAny_from_None(x : None) : PyAnyType; +function pyAny_from_Object(x : Object) : PyAnyType; #end diff --git a/Strata/Languages/Python/PythonToLaurel.lean b/Strata/Languages/Python/PythonToLaurel.lean index a81884705..66a15b29d 100644 --- a/Strata/Languages/Python/PythonToLaurel.lean +++ b/Strata/Languages/Python/PythonToLaurel.lean @@ -151,6 +151,11 @@ def pythonTypeToCoreType (typeStr : String) : Option String := match typeStr with | "Dict[str, Any]" => some "DictStrAny" | "List[str]" => some "ListStr" + -- Optional[T] → TOrNone + | "Optional[str]" => some "StrOrNone" + | "Optional[int]" => some "IntOrNone" + | "Optional[bool]" => some "BoolOrNone" + | "Optional[Any]" => some "AnyOrNone" | _ => none /-- Translate Python type annotation to Laurel HighType -/ @@ -207,6 +212,24 @@ def resolveDispatch (ctx : TranslationContext) /-! ## Expression Translation -/ +/-- Get the Core type name of a translated expression, if it can be determined + from the translation context (variable types) or from the expression shape. -/ +def getExprTypeName (ctx : TranslationContext) (expr : StmtExprMd) : Option String := + match expr.val with + | .Identifier name => + match ctx.variableTypes.lookup name with + | some ty => match ty.val with + | .TCore s => some s + | .TInt => some "int" + | .TBool => some "bool" + | .TString => some "string" + | _ => none + | none => none + | .LiteralInt _ => some "int" + | .LiteralBool _ => some "bool" + | .LiteralString _ => some "string" + | _ => none + /-- Check if a function has a model (is in prelude or user-defined) -/ def hasModel (ctx : TranslationContext) (funcName : String) : Bool := ctx.preludeProcedures.any (·.1 == funcName) || ctx.userFunctions.contains funcName @@ -438,6 +461,23 @@ partial def translateCall (ctx : TranslationContext) (f : Python.expr SourceRang let paramType := sig.inputs[i]! translatedArgs := translatedArgs ++ [mkNoneForType paramType] + -- Coerce PyAnyType arguments to expected parameter types + let mut coercedArgs : List StmtExprMd := [] + for i in [:translatedArgs.length] do + let arg := translatedArgs[i]! + if h : i < sig.inputs.length then + let expectedType := sig.inputs[i] + match getExprTypeName ctx arg with + | some "PyAnyType" => + if expectedType != "PyAnyType" then + coercedArgs := coercedArgs ++ [mkStmtExprMd (.StaticCall s!"pyAny_to_{expectedType}" [arg])] + else + coercedArgs := coercedArgs ++ [arg] + | _ => coercedArgs := coercedArgs ++ [arg] + else + coercedArgs := coercedArgs ++ [arg] + translatedArgs := coercedArgs + -- Check if function returns maybe_except (by convention, last output if present) if sig.outputs.length > 0 && sig.outputs.getLast! == "ExceptOrNone" then let call := mkStmtExprMd (StmtExpr.StaticCall funcName translatedArgs) @@ -475,9 +515,17 @@ partial def translateStmt (ctx : TranslationContext) (s : Python.stmt SourceRang -- Simple variable assignment: x = expr let target := name.val let valueExpr ← translateExpr ctx value - let targetExpr := mkStmtExprMd (StmtExpr.Identifier target) - let assignStmt := mkStmtExprMd (StmtExpr.Assign [targetExpr] valueExpr) - return (ctx, assignStmt) + -- Check if translateExpr returned a prelude procedure call (Assign with ExceptOrNone) + -- If so, replace the synthetic result0 target with the actual variable name + match valueExpr.val with + | .Assign targets call => + let newTargets := [mkStmtExprMd (.Identifier target)] ++ targets.drop 1 + let assignStmt := mkStmtExprMd (.Assign newTargets call) + return (ctx, assignStmt) + | _ => + let targetExpr := mkStmtExprMd (StmtExpr.Identifier target) + let assignStmt := mkStmtExprMd (StmtExpr.Assign [targetExpr] valueExpr) + return (ctx, assignStmt) | .Attribute _ obj attr _ => -- Field assignment: obj.field = expr or self.field = expr let valueExpr ← translateExpr ctx value @@ -547,8 +595,28 @@ partial def translateStmt (ctx : TranslationContext) (s : Python.stmt SourceRang else -- Regular call, not a constructor let initVal ← translateCall ctx f args.val.toList - let declStmt := mkStmtExprMd (StmtExpr.LocalVariable varName varType (some initVal)) - return (newCtx, declStmt) + -- Check if translateCall returned a prelude procedure call (Assign with ExceptOrNone) + -- If so, emit Block [var declaration; (varName, maybe_except) := call] instead of + -- embedding the Assign as a LocalVariable initializer + match initVal.val with + | .Assign targets call => + -- Use the procedure's actual first output type for the variable + let callFuncName := match call.val with + | .StaticCall name _ => some name + | _ => none + let actualType := match callFuncName.bind (fun n => List.lookup n ctx.preludeProcedures) with + | some (sig : CoreProcedureSignature) => + if sig.outputs.length > 1 then mkCoreType sig.outputs[0]! else varType + | none => varType + let newCtx' := { ctx with variableTypes := ctx.variableTypes ++ [(varName, actualType)] } + let newTargets := [mkStmtExprMd (.Identifier varName)] ++ targets.drop 1 + let declStmt := mkStmtExprMd (StmtExpr.LocalVariable varName actualType none) + let assignStmt := mkStmtExprMd (.Assign newTargets call) + let blockStmt := mkStmtExprMd (StmtExpr.Block [declStmt, assignStmt] none) + return (newCtx', blockStmt) + | _ => + let declStmt := mkStmtExprMd (StmtExpr.LocalVariable varName varType (some initVal)) + return (newCtx, declStmt) | some initExpr => do -- Regular annotated assignment with initializer let initVal ← translateExpr newCtx initExpr