Merge branch 'main' into josh/adt-alias

Author: joscoh

Strata/Languages/Python/PythonToCore.lean

@@ -209,18 +209,14 @@ def PyExprToMonoTy (e : Python.expr SourceRange) : Lambda.LMonoTy :=
   match e with
   | .Name _ n _ =>
     match n.val with
-    | "bool" => .tcons "bool" []
-    | "int" => .tcons "int" []
     | "str" => .tcons "string" []
     | "float" => .tcons "string" []
     | "Dict[str Any]" => .tcons "DictStrAny" []
     | "List[str]" => .tcons "ListStr" []
     | "datetime" => .tcons "Datetime" []
     | "date" => .tcons "Date" []
     | "timedelta" => .tcons "Timedelta" []
-    | "Client" => .tcons "Client" []
-    | "LatencyAnalyzer" => .tcons "LatencyAnalyzer" []
-    | _ => panic! s!"Unhandled name: {repr e}"
+    | _ => .tcons n.val []
   | .Subscript _ val _slice _ =>
     match val with
     | .Name _ n _ =>
@@ -775,17 +771,20 @@ def pythonToCore (signatures : Python.Signatures) (pgm: Strata.Program): Core.Pr
     let new_acc := update acc info
     let (ys, acc'') := helper f update new_acc xs
     (y ++ ys, acc'')
-  let func_info : TranslationContext := { signatures }
 
-  let func_defs_and_infos := helper PyFuncDefToCore (fun acc info => {acc with func_infos := info :: acc.func_infos}) func_info func_defs.toList
-  let func_defs := func_defs_and_infos.fst
-  let func_infos := func_defs_and_infos.snd
+  -- TODO: in Python, declarations can be circular
+  let base_ctx : TranslationContext := { signatures }
 
-  let class_defs_and_infos := helper PyClassDefToCore (fun acc info => {acc with class_infos := info :: acc.class_infos}) func_infos class_defs.toList
+  let class_defs_and_infos := helper PyClassDefToCore (fun acc info => {acc with class_infos := info :: acc.class_infos}) base_ctx class_defs.toList
   let class_defs := class_defs_and_infos.fst
   let class_infos := class_defs_and_infos.snd
-  let class_ty_decls := [(.type (.con {name := "LatencyAnalyzer", numargs := 0})) ]
 
-  {decls := globals ++ class_ty_decls ++ func_defs ++ class_defs ++ [.proc (pythonFuncToCore "__main__" [] non_func_blocks none default class_infos)]}
+  let class_ty_decls := class_infos.class_infos.map (λ info => .type (.con {name := info.name, numargs := 0}))
+
+  let func_defs_and_infos := helper PyFuncDefToCore (fun acc info => {acc with func_infos := info :: acc.func_infos}) class_infos func_defs.toList
+  let func_defs := func_defs_and_infos.fst
+  let func_infos := func_defs_and_infos.snd
+
+  {decls := globals ++ class_ty_decls ++ func_defs ++ class_defs ++ [.proc (pythonFuncToCore "__main__" [] non_func_blocks none default func_infos)]}
 
 end Strata

StrataTest/Languages/Python/expected/test_class_decl.expected

@@ -0,0 +1,14 @@
+
+datetime_now_ensures_0: ✅ pass
+
+datetime_utcnow_ensures_0: ✅ pass
+
+ensures_str_strp_reverse: ✅ pass
+
+assert_name_is_foo: ✅ pass
+
+assert_opt_name_none_or_str: ✅ pass
+
+assert_opt_name_none_or_bar: ✅ pass
+
+ensures_maybe_except_none: ✅ pass

StrataTest/Languages/Python/run_py_analyze.sh

@@ -17,6 +17,8 @@ for test_file in tests/test_*.py; do
                 echo "ERROR: Analysis output for $base_name does not match expected result"
                 echo "$output" | diff "$expected_file" -
                 failed=1
+            else
+                echo "Test passed: " $base_name
             fi
         fi
     fi

StrataTest/Languages/Python/tests/test_class_decl.py

@@ -0,0 +1,14 @@
+import test_helper
+from typing import List
+
+class CircularBuffer:
+    def __init__(self, n: int):
+        print("Hi")
+
+def main():
+    my_buf: CircularBuffer = CircularBuffer(5)
+
+    print("Bye")
+
+if __name__ == "__main__":
+    main()