Py simple any type

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,15 +300,15 @@ 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])
       | some initExpr =>
           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

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
 

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

StrataTest/Languages/Python/.gitignore

@@ -1,2 +1,3 @@
 *.python.st.ion
 *.sarif
+__pycache__