Fix all tests with type checking changes

6 files changed, 123 insertions, 112 deletions

diff --git a/src/ast_util.ml b/src/ast_util.ml
index 46afe599..8544700b 100644
--- a/src/ast_util.ml
+++ b/src/ast_util.ml
@@ -818,8 +818,9 @@ and string_of_pat (P_aux (pat, l)) =
   | P_vector_concat pats -> string_of_list " @ " string_of_pat pats
   | P_vector pats -> "[" ^ string_of_list ", " string_of_pat pats ^ "]"
   | P_as (pat, id) -> "(" ^ string_of_pat pat ^ " as " ^ string_of_id id ^ ")"
+  | P_string_append [] -> "\"\""
   | P_string_append pats -> string_of_list " ^ " string_of_pat pats
-  | _ -> "PAT"
+  | P_record _ -> "PAT"
 
 and string_of_mpat (MP_aux (pat, l)) =
   match pat with
diff --git a/src/bytecode_util.ml b/src/bytecode_util.ml
index c7fdc62d..3ced48b6 100644
--- a/src/bytecode_util.ml
+++ b/src/bytecode_util.ml
@@ -67,6 +67,9 @@ let instr_number () =
 let idecl ?loc:(l=Parse_ast.Unknown) ctyp id =
   I_aux (I_decl (ctyp, id), (instr_number (), l))
 
+let ireset ?loc:(l=Parse_ast.Unknown) ctyp id =
+  I_aux (I_reset (ctyp, id), (instr_number (), l))
+
 let iinit ?loc:(l=Parse_ast.Unknown) ctyp id cval =
   I_aux (I_init (ctyp, id, cval), (instr_number (), l))
 
diff --git a/src/c_backend.ml b/src/c_backend.ml
index 95ab51df..43fa3719 100644
--- a/src/c_backend.ml
+++ b/src/c_backend.ml
@@ -2576,26 +2576,13 @@ let rec codegen_instr fid ctx (I_aux (instr, (_, l))) =
   | I_clear (ctyp, id) ->
      string (Printf.sprintf "  KILL(%s)(&%s);" (sgen_ctyp_name ctyp) (sgen_id id))
 
-  | I_init (ctyp, id, cval) when is_stack_ctyp ctyp ->
-     if ctyp_equal ctyp (cval_ctyp cval) then
-       ksprintf string "  %s %s = %s;" (sgen_ctyp ctyp) (sgen_id id) (sgen_cval cval)
-     else
-       ksprintf string "  %s %s = CREATE_OF(%s, %s)(%s);"
-                (sgen_ctyp ctyp) (sgen_id id) (sgen_ctyp_name ctyp) (sgen_ctyp_name (cval_ctyp cval)) (sgen_cval_param cval)
   | I_init (ctyp, id, cval) ->
-     ksprintf string "  %s %s;" (sgen_ctyp ctyp) (sgen_id id) ^^ hardline
-     ^^ ksprintf string "  CREATE_OF(%s, %s)(&%s, %s);"
-                 (sgen_ctyp_name ctyp) (sgen_ctyp_name (cval_ctyp cval)) (sgen_id id) (sgen_cval_param cval)
+     codegen_instr fid ctx (idecl ctyp id) ^^ hardline
+     ^^ codegen_conversion Parse_ast.Unknown (CL_id (id, ctyp)) cval
 
-  | I_reinit (ctyp, id, cval) when is_stack_ctyp ctyp ->
-     if ctyp_equal ctyp (cval_ctyp cval) then
-       ksprintf string "  %s %s = %s;" (sgen_ctyp ctyp) (sgen_id id) (sgen_cval cval)
-     else
-       ksprintf string "  %s %s = CREATE_OF(%s, %s)(%s);"
-                (sgen_ctyp ctyp) (sgen_id id) (sgen_ctyp_name ctyp) (sgen_ctyp_name (cval_ctyp cval)) (sgen_cval cval)
   | I_reinit (ctyp, id, cval) ->
-     ksprintf string "  RECREATE_OF(%s, %s)(&%s, %s);"
-              (sgen_ctyp_name ctyp) (sgen_ctyp_name (cval_ctyp cval)) (sgen_id id) (sgen_cval_param cval)
+     codegen_instr fid ctx (ireset ctyp id) ^^ hardline
+     ^^ codegen_conversion Parse_ast.Unknown (CL_id (id, ctyp)) cval
 
   | I_reset (ctyp, id) when is_stack_ctyp ctyp ->
      string (Printf.sprintf "  %s %s;" (sgen_ctyp ctyp) (sgen_id id))
diff --git a/src/constraint.ml b/src/constraint.ml
index f512eb8a..a16b8c73 100644
--- a/src/constraint.ml
+++ b/src/constraint.ml
@@ -63,63 +63,79 @@ let rec pp_sexpr : sexpr -> string = function
   | List xs -> "(" ^ string_of_list " " pp_sexpr xs ^ ")"
   | Atom x -> x
 
-let zencode_kid kid = Util.zencode_string (string_of_kid kid)
-
 (** Each non-Type/Order kind in Sail mapes to a type in the SMT solver *)
 let smt_type l = function
   | K_int -> Atom "Int"
   | K_bool -> Atom "Bool"
   | _ -> raise (Reporting.err_unreachable l __POS__ "Tried to pass Type or Order kinded variable to SMT solver")
 
-let smt_var v = Atom ("v" ^ zencode_kid v)
-
-(** var_decs outputs the list of variables to be used by the SMT
-   solver in SMTLIB v2.0 format. It takes a kind_aux KBindings, as
-   returned by Type_check.get_typ_vars *)
-let var_decs l (vars : kind_aux KBindings.t) : string = vars
-  |> KBindings.bindings
-  |> List.map (fun (v, k) -> sfun "declare-const" [smt_var v; smt_type l k])
-  |> string_of_list "\n" pp_sexpr
-
-let rec smt_nexp (Nexp_aux (aux, l) : nexp) : sexpr =
-  match aux with
-  | Nexp_id id -> Atom (Util.zencode_string (string_of_id id))
-  | Nexp_var v -> smt_var v
-  | Nexp_constant c -> Atom (Big_int.to_string c)
-  | Nexp_app (id, nexps) -> sfun (string_of_id id) (List.map smt_nexp nexps)
-  | Nexp_times (nexp1, nexp2) -> sfun "*" [smt_nexp nexp1; smt_nexp nexp2]
-  | Nexp_sum (nexp1, nexp2) -> sfun "+" [smt_nexp nexp1; smt_nexp nexp2]
-  | Nexp_minus (nexp1, nexp2) -> sfun "-" [smt_nexp nexp1; smt_nexp nexp2]
-  | Nexp_exp nexp -> sfun "^" [Atom "2"; smt_nexp nexp]
-  | Nexp_neg nexp -> sfun "-" [smt_nexp nexp]
-
-let rec smt_constraint (NC_aux (aux, l) : n_constraint) : sexpr =
-  match aux with
-  | NC_equal (nexp1, nexp2) -> sfun "=" [smt_nexp nexp1; smt_nexp nexp2]
-  | NC_bounded_le (nexp1, nexp2) -> sfun "<=" [smt_nexp nexp1; smt_nexp nexp2]
-  | NC_bounded_ge (nexp1, nexp2) -> sfun ">=" [smt_nexp nexp1; smt_nexp nexp2]
-  | NC_not_equal (nexp1, nexp2) -> sfun "not" [sfun "=" [smt_nexp nexp1; smt_nexp nexp2]]
-  | NC_set (v, ints) ->
-     sfun "or" (List.map (fun i -> sfun "=" [smt_var v; Atom (Big_int.to_string i)]) ints)
-  | NC_or (nc1, nc2) -> sfun "or" [smt_constraint nc1; smt_constraint nc2]
-  | NC_and (nc1, nc2) -> sfun "and" [smt_constraint nc1; smt_constraint nc2]
-  | NC_app (id, args) ->
-     sfun (string_of_id id) (List.map smt_typ_arg args)
-  | NC_true -> Atom "true"
-  | NC_false -> Atom "false"
-  | NC_var v -> smt_var v
-
-and smt_typ_arg (A_aux (aux, l) : typ_arg) : sexpr =
-  match aux with
-  | A_nexp nexp -> smt_nexp nexp
-  | A_bool nc -> smt_constraint nc
-  | _ ->
-     raise (Reporting.err_unreachable l __POS__ "Tried to pass Type or Order kind to SMT function")
+let to_smt l vars constr =
+  (* Numbering all SMT variables v0, ... vn, rather than generating
+     names based on their Sail names (e.g. using zencode) ensures that
+     alpha-equivalent constraints generate the same SMT problem, which
+     is important for the SMT memoisation to work properly. *)
+  let var_map = ref KBindings.empty in
+  let vnum = ref (-1) in
+  let smt_var v =
+    match KBindings.find_opt v !var_map with
+    | Some n -> Atom ("v" ^ string_of_int n)
+    | None ->
+       let n = !vnum + 1 in
+       var_map := KBindings.add v n !var_map;
+       vnum := n;
+       Atom ("v" ^ string_of_int n)
+  in
+
+  (* var_decs outputs the list of variables to be used by the SMT
+     solver in SMTLIB v2.0 format. It takes a kind_aux KBindings, as
+     returned by Type_check.get_typ_vars *)
+  let var_decs l (vars : kind_aux KBindings.t) : string =
+    vars
+    |> KBindings.bindings
+    |> List.map (fun (v, k) -> sfun "declare-const" [smt_var v; smt_type l k])
+    |> string_of_list "\n" pp_sexpr
+  in
+  let rec smt_nexp (Nexp_aux (aux, l) : nexp) : sexpr =
+    match aux with
+    | Nexp_id id -> Atom (Util.zencode_string (string_of_id id))
+    | Nexp_var v -> smt_var v
+    | Nexp_constant c -> Atom (Big_int.to_string c)
+    | Nexp_app (id, nexps) -> sfun (string_of_id id) (List.map smt_nexp nexps)
+    | Nexp_times (nexp1, nexp2) -> sfun "*" [smt_nexp nexp1; smt_nexp nexp2]
+    | Nexp_sum (nexp1, nexp2) -> sfun "+" [smt_nexp nexp1; smt_nexp nexp2]
+    | Nexp_minus (nexp1, nexp2) -> sfun "-" [smt_nexp nexp1; smt_nexp nexp2]
+    | Nexp_exp nexp -> sfun "^" [Atom "2"; smt_nexp nexp]
+    | Nexp_neg nexp -> sfun "-" [smt_nexp nexp]
+  in
+  let rec smt_constraint (NC_aux (aux, l) : n_constraint) : sexpr =
+    match aux with
+    | NC_equal (nexp1, nexp2) -> sfun "=" [smt_nexp nexp1; smt_nexp nexp2]
+    | NC_bounded_le (nexp1, nexp2) -> sfun "<=" [smt_nexp nexp1; smt_nexp nexp2]
+    | NC_bounded_ge (nexp1, nexp2) -> sfun ">=" [smt_nexp nexp1; smt_nexp nexp2]
+    | NC_not_equal (nexp1, nexp2) -> sfun "not" [sfun "=" [smt_nexp nexp1; smt_nexp nexp2]]
+    | NC_set (v, ints) ->
+       sfun "or" (List.map (fun i -> sfun "=" [smt_var v; Atom (Big_int.to_string i)]) ints)
+    | NC_or (nc1, nc2) -> sfun "or" [smt_constraint nc1; smt_constraint nc2]
+    | NC_and (nc1, nc2) -> sfun "and" [smt_constraint nc1; smt_constraint nc2]
+    | NC_app (id, args) ->
+       sfun (string_of_id id) (List.map smt_typ_arg args)
+    | NC_true -> Atom "true"
+    | NC_false -> Atom "false"
+    | NC_var v -> smt_var v
+  and smt_typ_arg (A_aux (aux, l) : typ_arg) : sexpr =
+    match aux with
+    | A_nexp nexp -> smt_nexp nexp
+    | A_bool nc -> smt_constraint nc
+    | _ ->
+       raise (Reporting.err_unreachable l __POS__ "Tried to pass Type or Order kind to SMT function")
+  in
+  var_decs l vars, smt_constraint constr
 
 let smtlib_of_constraints ?get_model:(get_model=false) l vars constr : string =
+  let variables, problem = to_smt l vars constr in
   "(push)\n"
-  ^ var_decs l vars ^ "\n"
-  ^ pp_sexpr (sfun "define-fun" [Atom "constraint"; List []; Atom "Bool"; smt_constraint constr])
+  ^ variables ^ "\n"
+  ^ pp_sexpr (sfun "define-fun" [Atom "constraint"; List []; Atom "Bool"; problem])
   ^ "\n(assert constraint)\n(check-sat)"
   ^ (if get_model then "\n(get-model)" else "")
   ^ "\n(pop)"
diff --git a/src/pretty_print_sail.ml b/src/pretty_print_sail.ml
index bae1b893..94bcd54b 100644
--- a/src/pretty_print_sail.ml
+++ b/src/pretty_print_sail.ml
@@ -279,7 +279,7 @@ let doc_lit (L_aux(l,_)) =
   | L_undef -> "undefined"
   | L_string s -> "\"" ^ String.escaped s ^ "\"")
 
-let rec doc_pat (P_aux (p_aux, _) as pat) =
+let rec doc_pat (P_aux (p_aux, (l, _)) as pat) =
   match p_aux with
   | P_id id -> doc_id id
   | P_or (pat1, pat2) -> parens (doc_pat pat1 ^^ string " | " ^^ doc_pat pat2)
@@ -297,7 +297,11 @@ let rec doc_pat (P_aux (p_aux, _) as pat) =
   | P_as (pat, id) -> parens (separate space [doc_pat pat; string "as"; doc_id id])
   | P_app (id, pats) -> doc_id id ^^ parens (separate_map (comma ^^ space) doc_pat pats)
   | P_list pats -> string "[|" ^^ separate_map (comma ^^ space) doc_pat pats ^^ string "|]"
-  | _ -> string (string_of_pat pat)
+  | P_cons (hd_pat, tl_pat) -> separate space [doc_pat hd_pat; string "::"; doc_pat tl_pat]
+  | P_string_append [] -> string "\"\""
+  | P_string_append pats ->
+     parens (separate_map (string " ^ ") doc_pat pats)
+  | P_record _ -> raise (Reporting.err_unreachable l __POS__ "P_record passed to doc_pat")
 
 (* if_block_x is true if x should be printed like a block, i.e. with
    newlines. Blocks are automatically printed as blocks, so this
diff --git a/src/type_check.ml b/src/type_check.ml
index 459fe8d7..51625d4a 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -722,7 +722,16 @@ end = struct
     with
     | Not_found -> typ_error (id_loc id) ("No val spec found for " ^ string_of_id id)
 
-  let ex_counter = ref 0
+  let add_union_id id bind env =
+    typ_print (lazy (adding ^ "union identifier " ^ string_of_id id ^ " : " ^ string_of_bind bind));
+    { env with union_ids = Bindings.add id bind env.union_ids }
+
+  let get_union_id id env =
+    try
+      let bind = Bindings.find id env.union_ids in
+      List.fold_left (fun bind (kid, _) -> freshen_kid env kid bind) bind (KBindings.bindings env.typ_vars)
+    with
+    | Not_found -> typ_error (id_loc id) ("No union constructor found for " ^ string_of_id id)
 
   let rec update_val_spec id (typq, typ) env =
     begin match expand_synonyms env typ with
@@ -757,6 +766,8 @@ end = struct
     if not (Bindings.mem id env.top_val_specs)
     then update_val_spec id (bind_typq, bind_typ) env
     else
+      env
+        (*
       let (existing_typq, existing_typ) = Bindings.find id env.top_val_specs in
       let existing_cmp = (strip_typq existing_typq, strip_typ existing_typ) in
       let bind_cmp = (strip_typq bind_typq, strip_typ bind_typ) in
@@ -764,36 +775,34 @@ end = struct
         typ_error (id_loc id) ("Identifier " ^ string_of_id id ^ " is already bound as " ^ string_of_bind (existing_typq, existing_typ) ^ ", cannot rebind as " ^ string_of_bind (bind_typq, bind_typ))
       else
         env
+         *)
 
   and add_mapping id (typq, typ1, typ2) env =
-    begin
-      typ_print (lazy (adding ^ "mapping " ^ string_of_id id));
-      let forwards_id = mk_id (string_of_id id ^ "_forwards") in
-      let forwards_matches_id = mk_id (string_of_id id ^ "_forwards_matches") in
-      let backwards_id = mk_id (string_of_id id ^ "_backwards") in
-      let backwards_matches_id = mk_id (string_of_id id ^ "_backwards_matches") in
-      let forwards_typ = Typ_aux (Typ_fn ([typ1], typ2, no_effect), Parse_ast.Unknown) in
-      let forwards_matches_typ = Typ_aux (Typ_fn ([typ1], bool_typ, no_effect), Parse_ast.Unknown) in
-      let backwards_typ = Typ_aux (Typ_fn ([typ2], typ1, no_effect), Parse_ast.Unknown) in
-      let backwards_matches_typ = Typ_aux (Typ_fn ([typ2], bool_typ, no_effect), Parse_ast.Unknown) in
-      let env =
-        { env with mappings = Bindings.add id (typq, typ1, typ2) env.mappings }
-        |> add_val_spec forwards_id (typq, forwards_typ)
-        |> add_val_spec backwards_id (typq, backwards_typ)
-        |> add_val_spec forwards_matches_id (typq, forwards_matches_typ)
-        |> add_val_spec backwards_matches_id (typq, backwards_matches_typ)
-      in
-      let prefix_id = mk_id (string_of_id id ^ "_matches_prefix") in
-      begin if strip_typ typ1 = string_typ then
-              let forwards_prefix_typ = Typ_aux (Typ_fn ([typ1], app_typ (mk_id "option") [A_aux (A_typ (tuple_typ [typ2; nat_typ]), Parse_ast.Unknown)], no_effect), Parse_ast.Unknown) in
-              add_val_spec prefix_id (typq, forwards_prefix_typ) env
-            else if strip_typ typ2 = string_typ then
-              let backwards_prefix_typ = Typ_aux (Typ_fn ([typ2], app_typ (mk_id "option") [A_aux (A_typ (tuple_typ [typ1; nat_typ]), Parse_ast.Unknown)], no_effect), Parse_ast.Unknown) in
-              add_val_spec prefix_id (typq, backwards_prefix_typ) env
-            else
-              env
-      end
-    end
+    typ_print (lazy (adding ^ "mapping " ^ string_of_id id));
+    let forwards_id = mk_id (string_of_id id ^ "_forwards") in
+    let forwards_matches_id = mk_id (string_of_id id ^ "_forwards_matches") in
+    let backwards_id = mk_id (string_of_id id ^ "_backwards") in
+    let backwards_matches_id = mk_id (string_of_id id ^ "_backwards_matches") in
+    let forwards_typ = Typ_aux (Typ_fn ([typ1], typ2, no_effect), Parse_ast.Unknown) in
+    let forwards_matches_typ = Typ_aux (Typ_fn ([typ1], bool_typ, no_effect), Parse_ast.Unknown) in
+    let backwards_typ = Typ_aux (Typ_fn ([typ2], typ1, no_effect), Parse_ast.Unknown) in
+    let backwards_matches_typ = Typ_aux (Typ_fn ([typ2], bool_typ, no_effect), Parse_ast.Unknown) in
+    let env =
+      { env with mappings = Bindings.add id (typq, typ1, typ2) env.mappings }
+      |> add_val_spec forwards_id (typq, forwards_typ)
+      |> add_val_spec backwards_id (typq, backwards_typ)
+      |> add_val_spec forwards_matches_id (typq, forwards_matches_typ)
+      |> add_val_spec backwards_matches_id (typq, backwards_matches_typ)
+    in
+    let prefix_id = mk_id (string_of_id id ^ "_matches_prefix") in
+    if strip_typ typ1 = string_typ then
+      let forwards_prefix_typ = Typ_aux (Typ_fn ([typ1], app_typ (mk_id "option") [A_aux (A_typ (tuple_typ [typ2; nat_typ]), Parse_ast.Unknown)], no_effect), Parse_ast.Unknown) in
+      add_val_spec prefix_id (typq, forwards_prefix_typ) env
+    else if strip_typ typ2 = string_typ then
+      let backwards_prefix_typ = Typ_aux (Typ_fn ([typ2], app_typ (mk_id "option") [A_aux (A_typ (tuple_typ [typ1; nat_typ]), Parse_ast.Unknown)], no_effect), Parse_ast.Unknown) in
+      add_val_spec prefix_id (typq, backwards_prefix_typ) env
+    else
+      env
 
   let define_val_spec id env =
     if IdSet.mem id env.defined_val_specs
@@ -921,18 +930,6 @@ end = struct
     match Bindings.find_opt id env.variants with
     | Some (typq, tus) -> typq, tus
     | None -> typ_error (id_loc id) ("union " ^ string_of_id id ^ " not found")
-
-  let add_union_id id bind env =
-    typ_print (lazy (adding ^ "union identifier " ^ string_of_id id ^ " : " ^ string_of_bind bind));
-    { env with union_ids = Bindings.add id bind env.union_ids }
-
-  let get_union_id id env =
-    try
-      let bind = Bindings.find id env.union_ids in
-      List.fold_left (fun bind (kid, _) -> freshen_kid env kid bind) bind (KBindings.bindings env.typ_vars)
-    with
-    | Not_found -> typ_error (id_loc id) ("No union constructor found for " ^ string_of_id id)
-
   let get_flow id env =
     try Bindings.find id env.flow with
     | Not_found -> fun typ -> typ
@@ -1730,6 +1727,8 @@ let rec subtyp l env typ1 typ2 =
      else typ_raise l (Err_subtype (typ1, typ2, Env.get_constraints env, Env.get_typ_var_locs env))
   | None, None ->
   match typ_aux1, typ_aux2 with
+  | _, Typ_internal_unknown when Env.allow_unknowns env -> ()
+
   | Typ_tup typs1, Typ_tup typs2 when List.length typs1 = List.length typs2 ->
      List.iter2 (subtyp l env) typs1 typs2
 
@@ -2598,7 +2597,7 @@ and bind_pat env (P_aux (pat_aux, (l, ())) as pat) (Typ_aux (typ_aux, _) as typ)
 
   | P_app (f, pats) when Env.is_mapping f env ->
      begin
-       let (typq, mapping_typ) = Env.get_union_id f env in
+       let (typq, mapping_typ) = Env.get_val_spec f env in
        let quants = quant_items typq in
        let untuple (Typ_aux (typ_aux, _) as typ) = match typ_aux with
          | Typ_tup typs -> typs
@@ -3317,14 +3316,15 @@ and infer_funapp' l env f (typq, f_typ) xs expected_ret_typ =
   typ_debug (lazy ("Existentials: " ^ string_of_list ", " string_of_kid existentials));
   typ_debug (lazy ("Existential constraints: " ^ string_of_list ", " string_of_n_constraint ex_constraints));
 
+  let universals = KBindings.bindings universals |> List.map fst |> KidSet.of_list in
   let typ_ret =
-    if KidSet.is_empty (KidSet.of_list existentials) || KidSet.is_empty (typ_frees !typ_ret)
+    if KidSet.is_empty (KidSet.of_list existentials) || KidSet.is_empty (KidSet.diff (typ_frees !typ_ret) universals)
     then !typ_ret
     else mk_typ (Typ_exist (existentials, List.fold_left nc_and nc_true ex_constraints, !typ_ret))
   in
   let typ_ret = simp_typ typ_ret in
   let exp = annot_exp (E_app (f, xs)) typ_ret eff in
-  typ_debug (lazy ("RETURNING: " ^ string_of_exp exp));
+  typ_debug (lazy ("Returning: " ^ string_of_exp exp));
 
   exp, !all_unifiers