Refactor type environment

First, split the typing environment into a local and global environment.

Second, move the typing environment to a separate module Type_env which
is re-exported by Type_check as Env. Some common definitions and the
setup for type-errors are moved to Type_internal (which should not be
used outside the type checker, as the name suggests)

src/bin/repl.ml

@@ -450,8 +450,7 @@ let handle_input' istate input =
             let nc = Initial_check.constraint_of_string arg in
             { istate with env = Type_check.Env.add_constraint nc istate.env }
         | ":v" | ":verbose" ->
-            Type_check.opt_tc_debug := (!Type_check.opt_tc_debug + 1) mod 3;
-            print_endline ("Verbosity: " ^ string_of_int !Type_check.opt_tc_debug);
+            Type_check.set_tc_debug (int_of_string arg);
             istate
         | ":clear" ->
             if arg = "on" || arg = "true" then { istate with clear = true }
@@ -664,7 +663,7 @@ let handle_input istate input =
   | Failure str ->
       print_endline ("Error: " ^ str);
       istate
-  | Type_check.Type_error (_, err) ->
+  | Type_error.Type_error (_, err) ->
       print_endline (Type_error.string_of_type_error err);
       istate
   | Reporting.Fatal_error err ->

src/bin/sail.ml

@@ -204,7 +204,7 @@ let rec options =
         "<solver> choose SMT solver. Supported solvers are z3 (default), alt-ergo, cvc4, mathsat, vampire and yices."
       );
       ( "-smt_linearize",
-        Arg.Set Type_check.opt_smt_linearize,
+        Arg.Set Type_env.opt_smt_linearize,
         "(experimental) force linearization for constraints involving exponentials"
       );
       ("-Oconstant_fold", Arg.Set Constant_fold.optimize_constant_fold, " apply constant folding optimizations");
@@ -222,10 +222,7 @@ let rec options =
       );
       ("-ddump_initial_ast", Arg.Set Frontend.opt_ddump_initial_ast, " (debug) dump the initial ast to stdout");
       ("-ddump_tc_ast", Arg.Set Frontend.opt_ddump_tc_ast, " (debug) dump the typechecked ast to stdout");
-      ( "-dtc_verbose",
-        Arg.Int (fun verbosity -> Type_check.opt_tc_debug := verbosity),
-        "<verbosity> (debug) verbose typechecker output: 0 is silent"
-      );
+      ("-dtc_verbose", Arg.Int Type_check.set_tc_debug, "<verbosity> (debug) verbose typechecker output: 0 is silent");
       ("-dsmt_verbose", Arg.Set Constraint.opt_smt_verbose, " (debug) print SMTLIB constraints sent to SMT solver");
       ("-dmagic_hash", Arg.Set Initial_check.opt_magic_hash, " (debug) allow special character # in identifiers");
       ( "-dprofile",

src/lib/ast_util.ml

@@ -819,6 +819,8 @@ and map_loop_measure_annot f = function Loop (loop, exp) -> Loop (loop, map_exp_
 
 let def_loc (DEF_aux (_, annot)) = annot.loc
 
+let deinfix = function Id_aux (Id v, l) -> Id_aux (Operator v, l) | Id_aux (Operator v, l) -> Id_aux (Operator v, l)
+
 let id_of_kid = function Kid_aux (Var v, l) -> Id_aux (Id (String.sub v 1 (String.length v - 1)), l)
 
 let kid_of_id = function Id_aux (Id v, l) -> Kid_aux (Var ("'" ^ v), l) | Id_aux (Operator _, _) -> assert false

src/lib/ast_util.mli

@@ -459,6 +459,8 @@ val id_of_dec_spec : 'a dec_spec -> id
 
 (** {2 Functions for manipulating identifiers} *)
 
+val deinfix : id -> id
+
 val id_of_kid : kid -> id
 val kid_of_id : id -> kid
 

src/lib/constant_fold.ml

@@ -209,7 +209,7 @@ let rw_exp fixed target ok not_ok istate =
         try
           ok ();
           Type_check.check_exp (env_of_annot annot) exp (typ_of_annot annot)
-        with Type_error (l, err) ->
+        with Type_error.Type_error (l, err) ->
           (* A type error here would be unexpected, so don't ignore it! *)
           Reporting.warn "" l
             ("Type error when folding constants in "

src/lib/interpreter.ml

@@ -122,12 +122,13 @@ let value_of_exp = function E_aux (E_internal_value v, _) -> v | _ -> failwith "
 
 let fallthrough =
   let open Type_check in
+  let open Type_error in
   try
     let env = initial_env |> Env.add_scattered_variant (mk_id "exception") (mk_typquant []) in
     check_case env exc_typ
       (mk_pexp (Pat_exp (mk_pat (P_id (mk_id "exn")), mk_exp (E_throw (mk_exp (E_id (mk_id "exn")))))))
       unit_typ
-  with Type_error (l, err) -> Reporting.unreachable l __POS__ (Type_error.string_of_type_error err)
+  with Type_error (l, err) -> Reporting.unreachable l __POS__ (string_of_type_error err)
 
 (**************************************************************************)
 (* 1. Interpreter Monad                                                   *)
@@ -864,7 +865,7 @@ let rec eval_frame' = function
 
 let eval_frame frame =
   try eval_frame' frame
-  with Type_check.Type_error (l, err) -> raise (Reporting.err_typ l (Type_error.string_of_type_error err))
+  with Type_error.Type_error (l, err) -> raise (Reporting.err_typ l (Type_error.string_of_type_error err))
 
 let default_effect_interp state eff =
   let lstate, gstate = state in

src/lib/jib_compile.ml

@@ -560,7 +560,7 @@ module Make (C : CONFIG) = struct
       (* If we can't find a function in local_env, fall back to the
          global env - this happens when representing assertions, exit,
          etc as functions in the IR. *)
-      try Env.get_val_spec id ctx.local_env with Type_error _ -> Env.get_val_spec id ctx.tc_env
+      try Env.get_val_spec id ctx.local_env with Type_error.Type_error _ -> Env.get_val_spec id ctx.tc_env
     in
     let arg_typs, ret_typ = match fn_typ with Typ_fn (arg_typs, ret_typ) -> (arg_typs, ret_typ) | _ -> assert false in
     let ctx' = { ctx with local_env = Env.add_typquant (id_loc id) quant ctx.tc_env } in
@@ -1363,7 +1363,7 @@ module Make (C : CONFIG) = struct
   let compile_funcl ctx id pat guard exp =
     (* Find the function's type. *)
     let quant, Typ_aux (fn_typ, _) =
-      try Env.get_val_spec id ctx.local_env with Type_error _ -> Env.get_val_spec id ctx.tc_env
+      try Env.get_val_spec id ctx.local_env with Type_error.Type_error _ -> Env.get_val_spec id ctx.tc_env
     in
     let arg_typs, ret_typ = match fn_typ with Typ_fn (arg_typs, ret_typ) -> (arg_typs, ret_typ) | _ -> assert false in
 

src/lib/monomorphise.ml

@@ -77,6 +77,7 @@ open Ast_defs
 open Ast_util
 module Big_int = Nat_big_num
 open Type_check
+open Type_error
 
 let opt_mwords = ref false
 
@@ -3884,7 +3885,9 @@ module BitvectorSizeCasts = struct
             let arg_typ' = subst_unifiers unifiers arg_typ in
             arg_typ'
           end
-        | _ -> typ_error l ("Malformed constructor " ^ string_of_id f ^ " with type " ^ string_of_typ ctor_typ)
+        | _ ->
+            raise
+              (Reporting.err_typ l ("Malformed constructor " ^ string_of_id f ^ " with type " ^ string_of_typ ctor_typ))
       in
 
       (* Push the cast down, including through constructors *)

src/lib/property.ml

@@ -86,6 +86,7 @@ let find_properties { defs; _ } =
 
 let add_property_guards props ast =
   let open Type_check in
+  let open Type_error in
   let rec add_property_guards' acc = function
     | (DEF_aux (DEF_fundef (FD_aux (FD_function (r_opt, t_opt, funcls), fd_aux) as fdef), def_annot) as def) :: defs ->
       begin

src/lib/rewrites.ml

@@ -2131,7 +2131,7 @@ let rewrite_vector_concat_assignments env defs =
           in
           begin
             try check_exp env full_exp unit_typ
-            with Type_error (l, err) -> raise (Reporting.err_typ l (Type_error.string_of_type_error err))
+            with Type_error.Type_error (l, err) -> raise (Reporting.err_typ l (Type_error.string_of_type_error err))
           end
         )
         else E_aux (e_aux, annot)
@@ -2158,7 +2158,7 @@ let rewrite_tuple_assignments env defs =
         let let_exp = mk_exp (E_let (mk_letbind pat (strip_exp exp'), block)) in
         begin
           try check_exp env let_exp unit_typ
-          with Type_error (l, err) -> raise (Reporting.err_typ l (Type_error.string_of_type_error err))
+          with Type_error.Type_error (l, err) -> raise (Reporting.err_typ l (Type_error.string_of_type_error err))
         end
     | _ -> E_aux (e_aux, annot)
   in
@@ -2930,7 +2930,7 @@ let rewrite_ast_pat_string_append env =
         let mapping_inner_typ =
           match Env.get_val_spec (mk_id mapping_prefix_func) env with
           | _, Typ_aux (Typ_fn (_, Typ_aux (Typ_app (_, [A_aux (A_typ typ, _)]), _)), _) -> typ
-          | _ -> typ_error Parse_ast.Unknown "mapping prefix func without correct function type?"
+          | _ -> Reporting.unreachable Parse_ast.Unknown __POS__ "mapping prefix func without correct function type?"
         in
 
         let s_id = fresh_stringappend_id () in
@@ -4032,30 +4032,6 @@ let rewrite_ast_realize_mappings effect_info env ast =
         )
     in
 
-    typ_debug
-      ( lazy
-        (Printf.sprintf "forwards for mapping %s: %s\n%!" (string_of_id id)
-           (Pretty_print_sail.doc_fundef forwards_fun |> Pretty_print_sail.to_string)
-        )
-        );
-    typ_debug
-      ( lazy
-        (Printf.sprintf "backwards for mapping %s: %s\n%!" (string_of_id id)
-           (Pretty_print_sail.doc_fundef backwards_fun |> Pretty_print_sail.to_string)
-        )
-        );
-    typ_debug
-      ( lazy
-        (Printf.sprintf "forwards matches for mapping %s: %s\n%!" (string_of_id id)
-           (Pretty_print_sail.doc_fundef forwards_matches_fun |> Pretty_print_sail.to_string)
-        )
-        );
-    typ_debug
-      ( lazy
-        (Printf.sprintf "backwards matches for mapping %s: %s\n%!" (string_of_id id)
-           (Pretty_print_sail.doc_fundef backwards_matches_fun |> Pretty_print_sail.to_string)
-        )
-        );
     let forwards_fun, _ = Type_check.check_fundef env def_annot forwards_fun in
     let backwards_fun, _ = Type_check.check_fundef env def_annot backwards_fun in
     let forwards_matches_fun, _ = Type_check.check_fundef env def_annot forwards_matches_fun in
@@ -4084,12 +4060,6 @@ let rewrite_ast_realize_mappings effect_info env ast =
             FD_aux
               (FD_function (non_rec, no_tannot, [mk_funcl prefix_id arg_pat forwards_prefix_match]), (l, empty_uannot))
           in
-          typ_debug
-            ( lazy
-              (Printf.sprintf "forwards prefix matches for mapping %s: %s\n%!" (string_of_id id)
-                 (Pretty_print_sail.doc_fundef forwards_prefix_fun |> Pretty_print_sail.to_string)
-              )
-              );
           let forwards_prefix_fun, _ = Type_check.check_fundef env def_annot forwards_prefix_fun in
           forwards_prefix_fun
         end
@@ -4110,12 +4080,6 @@ let rewrite_ast_realize_mappings effect_info env ast =
             FD_aux
               (FD_function (non_rec, no_tannot, [mk_funcl prefix_id arg_pat backwards_prefix_match]), (l, empty_uannot))
           in
-          typ_debug
-            ( lazy
-              (Printf.sprintf "backwards prefix matches for mapping %s: %s\n%!" (string_of_id id)
-                 (Pretty_print_sail.doc_fundef backwards_prefix_fun |> Pretty_print_sail.to_string)
-              )
-              );
           let backwards_prefix_fun, _ = Type_check.check_fundef env def_annot backwards_prefix_fun in
           backwards_prefix_fun
         end
@@ -5141,7 +5105,7 @@ let rewrite effect_info env rewriters ast =
          (1, (ast, effect_info, env))
          rewriters
       )
-  with Type_check.Type_error (l, err) -> raise (Reporting.err_typ l (Type_error.string_of_type_error err))
+  with Type_error.Type_error (l, err) -> raise (Reporting.err_typ l (Type_error.string_of_type_error err))
 
 let () =
   let open Interactive in