Work in progress pyanalyze error handling

Strata/DDM/Ion.lean

@@ -1299,4 +1299,19 @@ def fromIonFragment (f : Ion.Fragment) (dialects : DialectMap) (dialect : Dialec
     commands := commands
   }
 
+def fromIon (dialects : DialectMap) (dialect : DialectName) (bytes : ByteArray) : Except String Strata.Program := do
+  let (hdr, frag) ←
+    match Strata.Ion.Header.parse bytes with
+    | .error msg =>
+      throw msg
+    | .ok p =>
+      pure p
+  match hdr with
+  | .dialect _ =>
+    throw "Expected a Strata program instead of a dialect."
+  | .program name => do
+    if name != dialect then
+      throw s!"{name} program found when {dialect} expected."
+    fromIonFragment frag dialects dialect
+
 end Program

Strata/Languages/Python/BoogiePrelude.lean

@@ -88,6 +88,7 @@ function AnyOrNone_none_val(v : AnyOrNone) : (None);
 function AnyOrNone_mk_str(s : string) : (AnyOrNone);
 function AnyOrNone_mk_none(v : None) : (AnyOrNone);
 function IntOrNone_mk_none(v : None) : (IntOrNone);
+function IntOrNone_mk_int(i : int) : (IntOrNone);
 function BytesOrStrOrNone_mk_none(v : None) : (BytesOrStrOrNone);
 function BytesOrStrOrNone_mk_str(s : string) : (BytesOrStrOrNone);
 function MappingStrStrOrNone_mk_none(v : None) : (MappingStrStrOrNone);
@@ -104,6 +105,7 @@ function BoolOrStrOrNone_mk_bool(b : bool) : (BoolOrStrOrNone);
 function BoolOrStrOrNone_mk_str(s : string) : (BoolOrStrOrNone);
 function BoolOrStrOrNone_mk_none(v : None) : (BoolOrStrOrNone);
 function Client_tag(v : Client) : (ClientTag);
+function DictStrAny_mk(s : string) : (DictStrAny);
 
 // Unique const axioms
 axiom [unique_ExceptOrNoneTag]: EN_STR_TAG != EN_NONE_TAG;
@@ -142,11 +144,33 @@ procedure importFrom(module : string, names : ListStr, level : int) returns ()
 procedure import(names : ListStr) returns ()
 ;
 
-procedure print(msg : string) returns ()
+procedure print(msg : string, opt : StrOrNone) returns ()
+;
+
+procedure json_dumps(msg : DictStrAny, opt_indent : IntOrNone) returns (s: string, maybe_except: ExceptOrNone)
+;
+
+procedure json_loads(msg : string) returns (d: DictStrAny, maybe_except: ExceptOrNone)
+;
+
+procedure input(msg : string) returns (result: string, maybe_except: ExceptOrNone)
+;
+
+procedure random_choice(l : ListStr) returns (result: string, maybe_except: ExceptOrNone)
 ;
 
 function str_len(s : string) : int;
 
+function str_in_list_str(s : string, l: ListStr) : bool;
+
+function str_in_dict_str_any(s : string, l: DictStrAny) : bool;
+
+function list_str_get(l : ListStr, i: int) : string;
+
+function dict_str_any_get(d : DictStrAny, k: string) : DictStrAny;
+
+function dict_str_any_length(d : DictStrAny) : int;
+
 procedure test_helper_procedure(req_name : string, opt_name : StrOrNone) returns (maybe_except: ExceptOrNone)
 spec {
   requires [req_name_is_foo]: req_name == "foo";

Strata/Languages/Python/FunctionSignatures.lean

@@ -9,21 +9,40 @@ import Strata.Languages.Boogie.Boogie
 namespace Strata
 namespace Python
 
--- We should extract the function signatures from the prelude:
-def getFuncSigOrder (fname: String) : List String :=
-  match fname with
-  | "test_helper_procedure" => ["req_name", "opt_name"]
-  | _ => panic! s!"Missing function signature : {fname}"
-
--- We should extract the function signatures from the prelude:
-def getFuncSigType (fname: String) (arg: String) : String :=
-  match fname with
-  | "test_helper_procedure" =>
-    match arg with
-    | "req_name" => "string"
-    | "opt_name" => "StrOrNone"
-    | _ => panic! s!"Unrecognized arg : {arg}"
-  | _ => panic! s!"Missing function signature : {fname}"
+inductive PyType where
+| AnyOrNone
+| BoolOrNone
+| BoolOrStrOrNone
+| BytesOrStrOrNone
+| DictStrAny
+| IntOrNone
+| ListStr
+| MappingStrStrOrNone
+| StrOrNone
+| Str
+deriving Inhabited
+
+namespace PyType
+
+def toString (atp : PyType) : String :=
+  match atp with
+  | AnyOrNone => "AnyOrNone"
+  | BoolOrNone => "BoolOrNone"
+  | BoolOrStrOrNone => "BoolOrStrOrNone"
+  | BytesOrStrOrNone => "BytesOrStrOrNone"
+  | DictStrAny => "DictStrAny"
+  | IntOrNone => "IntOrNone"
+  | ListStr => "ListStr"
+  | MappingStrStrOrNone => "MappingStrStrOrNone"
+  | StrOrNone => "StrOrNone"
+  | Str => "string"
+
+def allowNone (atp : PyType) : Bool :=
+  match atp with
+  | Str => False
+  | _ => True
+
+end PyType
 
 def TypeStrToBoogieExpr (ty: String) : Boogie.Expression.Expr :=
   if !ty.endsWith "OrNone" then
@@ -39,5 +58,67 @@ def TypeStrToBoogieExpr (ty: String) : Boogie.Expression.Expr :=
     | "MappingStrStrOrNone" => .app () (.op () "MappingStrStrOrNone_mk_none" none) (.op () "None_none" none)
     | _ => panic! s!"unsupported type: {ty}"
 
+
+structure FuncSignature where
+  args : Array (String × PyType)
+  required_arg_count : Nat := args.size
+  indexMap : Std.HashMap String Nat
+deriving Inhabited
+
+namespace FuncSignature
+
+def ofArray (args : Array (String × PyType)) : FuncSignature where
+  args := args
+  indexMap := args.foldl (init := {}) fun m (name, _) => m.insert name m.size
+
+end FuncSignature
+
+/--
+Global database of function signatures
+-/
+structure FuncSigDB where
+  -- TODO: Migrate from a map from String to a map that incorporates Python module
+  -- information.
+  map : Std.HashMap String FuncSignature := {}
+deriving Inhabited
+
+namespace FuncSigDB
+
+instance : GetElem? FuncSigDB String FuncSignature (fun db name => name ∈ db.map) where
+  getElem db nm p := db.map[nm]'p
+  getElem? db nm := db.map[nm]?
+  getElem! db nm := db.map[nm]!
+
+def add! (db : FuncSigDB) (name : String) (args : List (String × PyType)) :=
+    assert! name ∉ db.map
+    { db with map := db.map.insert name (.ofArray args.toArray) }
+
+end FuncSigDB
+
+def funcSigs (db : FuncSigDB := {}) : FuncSigDB := Prod.snd <| Id.run <| StateT.run (s := db) do
+  let arg (name : String) (tp : PyType) : String × PyType := (name, tp)
+  let add name args := modify (·.add! name args)
+  add "input" [
+    arg "msg" .Str,
+  ]
+  add "json_dumps" [
+    arg "msg" .DictStrAny,
+    arg "opt_indent" .IntOrNone,
+  ]
+  add "json_loads" [
+    arg "msg" .Str
+  ]
+  add "print" [
+    arg "msg" .Str,
+    arg "opt" .StrOrNone,
+  ]
+  add "random_choice" [
+    arg "l" .ListStr
+  ]
+  add "test_helper_procedure" [
+    arg "req_name" .Str,
+    arg "opt_name" .StrOrNone,
+  ]
+
 end Python
 end Strata

Strata/Languages/Python/PythonDialect.lean

@@ -16,6 +16,15 @@ namespace Strata
 namespace Python
 #load_dialect "../../../Tools/Python/test_results/dialects/Python.dialect.st.ion"
 #strata_gen Python
+
+/--
+Return the annotation associated with an expression
+
+FIXME. #strata_gen should eventually generate a more optimized version of this automatically.
+-/
+def expr.ann {α} [Inhabited α] (expr : Python.expr α) : α := expr.toAst |>.ann
+
+
 end Python