diff --git a/Strata/Languages/Python/PythonLaurelCorePrelude.lean b/Strata/Languages/Python/PythonLaurelCorePrelude.lean index 654ad1d68..8dc63bae9 100644 --- a/Strata/Languages/Python/PythonLaurelCorePrelude.lean +++ b/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 } diff --git a/Strata/Languages/Python/PythonToLaurel.lean b/Strata/Languages/Python/PythonToLaurel.lean index 1a5103b67..500fc6e41 100644 --- a/Strata/Languages/Python/PythonToLaurel.lean +++ b/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))) diff --git a/StrataTest/Languages/Python/AnalyzeLaurelTest.lean b/StrataTest/Languages/Python/AnalyzeLaurelTest.lean index a070383d9..d11bffda0 100644 --- a/StrataTest/Languages/Python/AnalyzeLaurelTest.lean +++ b/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]", diff --git a/StrataTest/Languages/Python/Specs/dispatch_test/test_augassign.py b/StrataTest/Languages/Python/Specs/dispatch_test/test_augassign.py new file mode 100644 index 000000000..388b95760 --- /dev/null +++ b/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 diff --git a/StrataTest/Languages/Python/Specs/dispatch_test/test_except_var_usage.py b/StrataTest/Languages/Python/Specs/dispatch_test/test_except_var_usage.py new file mode 100644 index 000000000..43760ecf7 --- /dev/null +++ b/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 diff --git a/StrataTest/Languages/Python/Specs/dispatch_test/test_fstring.py b/StrataTest/Languages/Python/Specs/dispatch_test/test_fstring.py new file mode 100644 index 000000000..3c2a0c9a0 --- /dev/null +++ b/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 diff --git a/StrataTest/Languages/Python/Specs/dispatch_test/test_pow_operator.py b/StrataTest/Languages/Python/Specs/dispatch_test/test_pow_operator.py new file mode 100644 index 000000000..8938e5298 --- /dev/null +++ b/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 diff --git a/StrataTest/Languages/Python/Specs/dispatch_test/test_slice.py b/StrataTest/Languages/Python/Specs/dispatch_test/test_slice.py new file mode 100644 index 000000000..db6a82d0f --- /dev/null +++ b/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 diff --git a/StrataTest/Languages/Python/Specs/dispatch_test/test_ternary.py b/StrataTest/Languages/Python/Specs/dispatch_test/test_ternary.py new file mode 100644 index 000000000..4e0e98605 --- /dev/null +++ b/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