Rename Any_to_bool to python_is_truthy and add construct support

Strata/Languages/Python/PythonLaurelCorePrelude.lean

@@ -271,12 +271,11 @@ inline function isError (e: Error) : bool {
 }
 
 // /////////////////////////////////////////////////////////////////////////////////////
-//The following function convert Any type to bool
-//based on the Python definition of truthiness for basic types
+//The following function implements Python truthiness for basic types
 // https://docs.python.org/3/library/stdtypes.html
 // /////////////////////////////////////////////////////////////////////////////////////
 
-inline function Any_to_bool (v: Any) : bool
+inline function python_is_truthy (v: Any) : bool
   requires (Any..isfrom_bool(v) || Any..isfrom_none(v) || Any..isfrom_string(v) || Any..isfrom_int(v));
 {
   if (Any..isfrom_bool(v)) then Any..as_bool!(v) else
@@ -825,13 +824,13 @@ inline function PNEq (v: Any, v': Any) : Any {
 inline function PAnd (v1: Any, v2: Any) : Any
   requires (Any..isfrom_bool(v1) || Any..isfrom_none(v1) || Any..isfrom_string(v1) || Any..isfrom_int(v1));
 {
-  if ! Any_to_bool (v1) then v1 else v2
+  if ! python_is_truthy (v1) then v1 else v2
 }
 
 inline function POr (v1: Any, v2: Any) : Any
   requires (Any..isfrom_bool(v1) || Any..isfrom_none(v1) || Any..isfrom_string(v1) || Any..isfrom_int(v1));
 {
-  if Any_to_bool (v1) then v1 else v2
+  if python_is_truthy (v1) then v1 else v2
 }
 
 

Strata/Languages/Python/PythonToLaurel.lean

@@ -251,7 +251,7 @@ def strToAny (s: String) := mkStmtExprMd (.StaticCall "from_string" [mkStmtExprM
 def intToAny (i: Int) := mkStmtExprMd (.StaticCall "from_int" [mkStmtExprMd (StmtExpr.LiteralInt i)])
 def boolToAny (b: Bool) := mkStmtExprMd (.StaticCall "from_bool" [mkStmtExprMd (StmtExpr.LiteralBool b)])
 def AnyNone := mkStmtExprMd (.StaticCall "from_none" [])
-def Any_to_bool (b: StmtExprMd) := mkStmtExprMd (.StaticCall "Any_to_bool" [b])
+def python_is_truthy (b: StmtExprMd) := mkStmtExprMd (.StaticCall "python_is_truthy" [b])
 
 /-- Wrap a field access expression in the appropriate Any constructor based on HighType.
     After heap parameterization, field reads return concrete types (int, bool, etc.)
@@ -436,6 +436,7 @@ partial def translateExpr (ctx : TranslationContext) (e : Python.expr SourceRang
       | .Div _ => return mkStmtExprMd .Hole -- Floating-point are not supported yet
       | .FloorDiv _ => .ok "PFloorDiv"  -- Python // maps to Laurel Div
       | .Mod _ => .ok "PMod"
+      | .Pow _ => .ok "PPow"
       | .BitAnd _ => return mkStmtExprMd .Hole --TODO: Adding BitVector subtype in Any type, then the related operations
       | .BitOr _ => return mkStmtExprMd .Hole
       | .BitXor _ => return mkStmtExprMd .Hole
@@ -502,7 +503,11 @@ partial def translateExpr (ctx : TranslationContext) (e : Python.expr SourceRang
     let condExpr ← translateExpr ctx cond
     let thenExpr ← translateExpr ctx thenb
     let elseExpr ← translateExpr ctx elseb
-    return mkStmtExprMd (StmtExpr.IfThenElse (Any_to_bool condExpr) thenExpr elseExpr)
+    return mkStmtExprMd (StmtExpr.IfThenElse (python_is_truthy condExpr) thenExpr elseExpr)
+
+  -- FormattedValue (f-string interpolation) - translate the inner expression
+  | .FormattedValue _ value _ _ =>
+    translateExpr ctx value
 
   | .Call _ f args kwargs => translateCall ctx f args.val.toList kwargs.val.toList
 
@@ -577,6 +582,9 @@ partial def translateExpr (ctx : TranslationContext) (e : Python.expr SourceRang
   -- Generator expression: (x for x in items)
   | .GeneratorExp .. => return mkStmtExprMd .Hole
 
+  -- Slice expression: items[start:stop:step]
+  | .Slice .. => return mkStmtExprMd .Hole
+
   | _ => throw (.unsupportedConstruct "Expression type not yet supported" (toString (repr e)))
 
 
@@ -1026,7 +1034,7 @@ partial def translateStmt (ctx : TranslationContext) (s : Python.stmt SourceRang
     else do
       let (_, elseStmts) ← translateStmtList bodyCtx orelse.val.toList
       .ok (some (mkStmtExprMd (StmtExpr.Block elseStmts none)))
-    let ifStmt := mkStmtExprMdWithLoc (StmtExpr.IfThenElse (Any_to_bool condExpr) bodyBlock elseBlock) md
+    let ifStmt := mkStmtExprMdWithLoc (StmtExpr.IfThenElse (python_is_truthy condExpr) bodyBlock elseBlock) md
 
     return (bodyCtx, varDecls ++ [ifStmt])
 
@@ -1041,7 +1049,7 @@ partial def translateStmt (ctx : TranslationContext) (s : Python.stmt SourceRang
     let loopCtx := { ctx with loopBreakLabel := some breakLabel, loopContinueLabel := some continueLabel }
     let (_, bodyStmts) ← translateStmtList loopCtx body.val.toList
     let bodyBlock := mkStmtExprMd (StmtExpr.Block bodyStmts (some continueLabel))
-    let whileStmt := mkStmtExprMd (StmtExpr.While (Any_to_bool condExpr) [] none bodyBlock)
+    let whileStmt := mkStmtExprMd (StmtExpr.While (python_is_truthy condExpr) [] none bodyBlock)
     let whileWrapped := mkStmtExprMdWithLoc (StmtExpr.Block [whileStmt] (some breakLabel)) md
     return (loopCtx, varDecls ++ [whileWrapped])
 
@@ -1058,7 +1066,7 @@ partial def translateStmt (ctx : TranslationContext) (s : Python.stmt SourceRang
   -- Assert statement
   | .Assert _ test _msg => do
     let condExpr ← translateExpr ctx test
-    let assertStmt := mkStmtExprMdWithLoc (StmtExpr.Assert (Any_to_bool condExpr)) md
+    let assertStmt := mkStmtExprMdWithLoc (StmtExpr.Assert (python_is_truthy condExpr)) md
     return (ctx, [assertStmt])
 
   --Ignore comments in source code
@@ -1094,13 +1102,13 @@ partial def translateStmt (ctx : TranslationContext) (s : Python.stmt SourceRang
     -- in try/except are visible after the block).
     let bodyDecls := collectDeclaredNamesAndTypes body.val.toList
 
-    let errorVarDecls: List (String × String) := (handlers.val.toList.filterMap (λ h => match h with
-          | .ExceptHandler _ _ errname _ => errname.val)).map (λ h => (h.val, "PythonError"))
+    let errorVarPairs: List (String × String) := (handlers.val.toList.filterMap (λ h => match h with
+          | .ExceptHandler _ _ errname _ => errname.val)).map (λ h => (h.val, "Any"))
 
     let handlerDecls := handlers.val.toList.flatMap fun h => match h with
       | .ExceptHandler _ _ _ hBody => collectDeclaredNamesAndTypes hBody.val.toList
 
-    let allNewDecls := (bodyDecls ++ errorVarDecls ++ handlerDecls)
+    let allNewDecls := (bodyDecls ++ errorVarPairs ++ handlerDecls)
     let (hoistedDecls, hoistedCtx) := createVarDeclStmtsAndCtx ctx allNewDecls
 
     -- Translate try body (with hoisted context so inner decls become assigns)
@@ -1209,19 +1217,20 @@ partial def translateStmt (ctx : TranslationContext) (s : Python.stmt SourceRang
     | some lbl => return (ctx, [mkStmtExprMdWithLoc (StmtExpr.Exit lbl) md])
     | none => return (ctx, [mkStmtExprMdWithLoc (StmtExpr.Assert (mkStmtExprMd .Hole)) md])
 
-  -- Augmented assignment: x += expr  →  x = x op expr
+  -- Augmented assignment: x += y  →  x = x + y
   | .AugAssign _ target op value => do
-    let targetExpr ← translateExpr ctx target
-    let valueExpr ← translateExpr ctx value
-    let rhs := match op with
-      | .Add _      => mkStmtExprMd (StmtExpr.StaticCall "PAdd"      [targetExpr, valueExpr])
-      | .Sub _      => mkStmtExprMd (StmtExpr.StaticCall "PSub"      [targetExpr, valueExpr])
-      | .Mult _     => mkStmtExprMd (StmtExpr.StaticCall "PMul"      [targetExpr, valueExpr])
-      | .FloorDiv _ => mkStmtExprMd (StmtExpr.StaticCall "PFloorDiv" [targetExpr, valueExpr])
-      | .Mod _      => mkStmtExprMd (StmtExpr.StaticCall "PMod"      [targetExpr, valueExpr])
-      | _           => mkStmtExprMd .Hole
-    let assignStmt := mkStmtExprMdWithLoc (StmtExpr.Assign [targetExpr] rhs) md
-    return (ctx, [assignStmt])
+    let lhsExpr ← translateExpr ctx target
+    let rhsExpr ← translateExpr ctx value
+    let opName ← match op with
+      | .Add _ => .ok "PAdd"
+      | .Sub _ => .ok "PSub"
+      | .Mult _ => .ok "PMul"
+      | .FloorDiv _ => .ok "PFloorDiv"
+      | .Mod _ => .ok "PMod"
+      | _ => throw (.unsupportedConstruct s!"Augmented assignment operator not yet supported: {repr op}" (toString (repr s)))
+    let combined := mkStmtExprMd (StmtExpr.StaticCall opName [lhsExpr, rhsExpr])
+    let assign := mkStmtExprMd (StmtExpr.Assign [lhsExpr] combined)
+    return (ctx, [assign])
 
   | _ => throw (.unsupportedConstruct "Statement type not yet supported" (toString (repr s)))
 

StrataTest/Languages/Python/AnalyzeLaurelTest.lean

@@ -161,6 +161,12 @@ private meta def testCases : List (String × Expected) := [
   .mk "test_list_str.py" .success,
   .mk "test_nested_try.py" .success,
   .mk "test_try_scope.py" .success,
+  .mk "test_ternary.py" .success,
+  .mk "test_pow_operator.py" .success,
+  .mk "test_except_var_usage.py" .success,
+  .mk "test_fstring.py" .success,
+  .mk "test_slice.py" .success,
+  .mk "test_augassign.py" .success,
   -- Negative tests
   .mk "test_invalid_service.py" $
     .fail "User code error: 'connect' called with unknown string \"invalid\"; known services: #[messaging, storage]",

StrataTest/Languages/Python/Specs/dispatch_test/test_augassign.py

@@ -0,0 +1,8 @@
+import servicelib
+
+def use_augassign() -> bool:
+    client: Storage = servicelib.connect("storage")
+    count: int = 0
+    items: list = client.list_items(Bucket="mybucket")
+    count += 1
+    return True

StrataTest/Languages/Python/Specs/dispatch_test/test_except_var_usage.py

@@ -0,0 +1,10 @@
+import servicelib
+
+def except_var_usage() -> bool:
+    client: Storage = servicelib.connect("storage")
+    try:
+        client.put_item(Bucket="b", Key="k", Data="v")
+    except Exception as e:
+        msg: str = str(e)
+        return False
+    return True

StrataTest/Languages/Python/Specs/dispatch_test/test_fstring.py

@@ -0,0 +1,8 @@
+import servicelib
+
+def use_fstring() -> bool:
+    client: Storage = servicelib.connect("storage")
+    name: str = "backup"
+    bucket: str = f"{name}_bucket"
+    client.put_item(Bucket=bucket, Key="k", Data="v")
+    return True

StrataTest/Languages/Python/Specs/dispatch_test/test_pow_operator.py

@@ -0,0 +1,7 @@
+import servicelib
+
+def use_pow() -> bool:
+    base: int = 2
+    exp: int = 10
+    result: int = base ** exp
+    return True

StrataTest/Languages/Python/Specs/dispatch_test/test_slice.py

@@ -0,0 +1,7 @@
+import servicelib
+
+def use_slice() -> bool:
+    client: Storage = servicelib.connect("storage")
+    items: list = client.list_items(Bucket="mybucket")
+    subset: list = items[1:]
+    return True

StrataTest/Languages/Python/Specs/dispatch_test/test_ternary.py

@@ -0,0 +1,8 @@
+import servicelib
+
+def use_ternary() -> bool:
+    client: Storage = servicelib.connect("storage")
+    flag: bool = True
+    bucket: str = "a" if flag else "b"
+    client.put_item(Bucket=bucket, Key="k", Data="v")
+    return True