summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
authorAlasdair Armstrong2018-12-22 00:20:08 +0000
committerAlasdair Armstrong2018-12-22 00:20:08 +0000
commit0a65347ed2868b815dee532acfebb463f8be644b (patch)
tree662b9fb1b240984597b3050fe4c174ccfceecd0f /src
parentc745a9a8d8d7d2b04e72bbb8bda9d9f0a7aabbfb (diff)
Improve error messages and debugging
Work on improving the formatting and quality of error messages When sail is invoked with sail -i, any type errors now drop the user down to the interactive prompt, with the interactive environment being the environment at the point the type error occurred, this means the typechecker state can be interactively queried in the interpreter to help diagnose type errors.
Diffstat (limited to 'src')
-rw-r--r--src/c_backend.ml2
-rw-r--r--src/constant_fold.ml2
-rw-r--r--src/error_format.ml95
-rw-r--r--src/interactive.ml7
-rw-r--r--src/interactive.mli9
-rw-r--r--src/interpreter.ml2
-rw-r--r--src/isail.ml74
-rw-r--r--src/pretty_print_coq.ml2
-rw-r--r--src/process_file.ml2
-rw-r--r--src/reporting.ml24
-rw-r--r--src/reporting.mli8
-rw-r--r--src/rewrites.ml18
-rw-r--r--src/sail.ml20
-rw-r--r--src/type_check.ml486
-rw-r--r--src/type_check.mli10
-rw-r--r--src/type_error.ml150
16 files changed, 476 insertions, 435 deletions
diff --git a/src/c_backend.ml b/src/c_backend.ml
index 79d4693a..53e7dc88 100644
--- a/src/c_backend.ml
+++ b/src/c_backend.ml
@@ -3460,4 +3460,4 @@ let compile_ast ctx c_includes (Defs defs) =
^^ model_main)
|> print_endline
with
- Type_error (l, err) -> c_error ("Unexpected type error when compiling to C:\n" ^ Type_error.string_of_type_error err)
+ Type_error (_, l, err) -> c_error ("Unexpected type error when compiling to C:\n" ^ Type_error.string_of_type_error err)
diff --git a/src/constant_fold.ml b/src/constant_fold.ml
index 9e474912..7321a801 100644
--- a/src/constant_fold.ml
+++ b/src/constant_fold.ml
@@ -161,7 +161,7 @@ let rec rewrite_constant_function_calls' ast =
let v = run (Interpreter.Step (lazy "", (lstate, gstate), initial_monad, [])) in
let exp = exp_of_value v in
try (ok (); Type_check.check_exp (env_of_annot annot) exp (typ_of_annot annot)) with
- | Type_error (l, err) ->
+ | Type_error (env, l, err) ->
(* A type error here would be unexpected, so don't ignore it! *)
Util.warn ("Type error when folding constants in "
^ string_of_exp (E_aux (e_aux, annot))
diff --git a/src/error_format.ml b/src/error_format.ml
new file mode 100644
index 00000000..3e91f065
--- /dev/null
+++ b/src/error_format.ml
@@ -0,0 +1,95 @@
+
+let rec skip_lines in_chan = function
+ | n when n <= 0 -> ()
+ | n -> ignore (input_line in_chan); skip_lines in_chan (n - 1)
+
+let rec read_lines in_chan = function
+ | n when n <= 0 -> []
+ | n ->
+ let l = input_line in_chan in
+ let ls = read_lines in_chan (n - 1) in
+ l :: ls
+
+type formatter = {
+ indent : string;
+ endline : string -> unit;
+ loc_color : string -> string
+ }
+
+let err_formatter = {
+ indent = "";
+ endline = prerr_endline;
+ loc_color = Util.red
+ }
+
+let buffer_formatter b = {
+ indent = "";
+ endline = (fun str -> Buffer.add_string b (str ^ "\n"));
+ loc_color = Util.red
+ }
+
+let format_endline str ppf = ppf.endline (ppf.indent ^ (Str.global_replace (Str.regexp_string "\n") ("\n" ^ ppf.indent) str))
+
+let underline_single color cnum_from cnum_to =
+ if (cnum_from + 1) >= cnum_to then
+ Util.(String.make cnum_from ' ' ^ clear (color "^"))
+ else
+ Util.(String.make cnum_from ' ' ^ clear (color ("^" ^ String.make (cnum_to - cnum_from - 2) '-' ^ "^")))
+
+let format_code_single' fname in_chan lnum cnum_from cnum_to contents ppf =
+ skip_lines in_chan (lnum - 1);
+ let line = input_line in_chan in
+ let line_prefix = string_of_int lnum ^ Util.(clear (cyan " |")) in
+ let blank_prefix = String.make (String.length (string_of_int lnum)) ' ' ^ Util.(clear (ppf.loc_color " |")) in
+ format_endline (Printf.sprintf "[%s]:%d:%d-%d" Util.(fname |> cyan |> clear) lnum cnum_from cnum_to) ppf;
+ format_endline (line_prefix ^ line) ppf;
+ format_endline (blank_prefix ^ underline_single ppf.loc_color cnum_from cnum_to) ppf;
+ contents { ppf with indent = blank_prefix ^ " " }
+
+let format_code_single fname lnum cnum_from cnum_to contents ppf =
+ try
+ let in_chan = open_in fname in
+ begin
+ try format_code_single' fname in_chan lnum cnum_from cnum_to contents ppf
+ with
+ | _ -> close_in_noerr in_chan; ()
+ end
+ with
+ | _ -> ()
+
+let format_pos p1 p2 contents ppf =
+ let open Lexing in
+ if p1.pos_lnum == p2.pos_lnum
+ then format_code_single p1.pos_fname p1.pos_lnum (p1.pos_cnum - p1.pos_bol) (p2.pos_cnum - p2.pos_bol) contents ppf
+ else failwith "Range"
+
+let format_loc l contents =
+ match l with
+ | Parse_ast.Unknown -> failwith "No location"
+ | Parse_ast.Range (p1, p2) -> format_pos p1 p2 contents
+ | _ -> failwith "not range"
+
+type message =
+ | Location of Parse_ast.l * message
+ | Line of string
+ | List of (string * message) list
+ | Seq of message list
+ | With of (formatter -> formatter) * message
+
+let bullet = Util.(clear (blue "*"))
+
+let rec format_message msg =
+ match msg with
+ | Location (l, msg) ->
+ format_loc l (format_message msg)
+ | Line str ->
+ format_endline str
+ | Seq messages ->
+ fun ppf -> List.iter (fun msg -> format_message msg ppf) messages
+ | List list ->
+ let format_list_item ppf (header, msg) =
+ format_endline (Util.(clear (blue "*")) ^ " " ^ header) ppf;
+ format_message msg { ppf with indent = ppf.indent ^ " " }
+ in
+ fun ppf -> List.iter (format_list_item ppf) list
+ | With (f, msg) -> fun ppf -> format_message msg (f ppf)
diff --git a/src/interactive.ml b/src/interactive.ml
new file mode 100644
index 00000000..3c4619a0
--- /dev/null
+++ b/src/interactive.ml
@@ -0,0 +1,7 @@
+
+let opt_interactive = ref false
+let opt_suppress_banner = ref false
+
+let env = ref Type_check.initial_env
+
+let ast = ref (Ast.Defs [])
diff --git a/src/interactive.mli b/src/interactive.mli
new file mode 100644
index 00000000..7782f646
--- /dev/null
+++ b/src/interactive.mli
@@ -0,0 +1,9 @@
+open Ast
+open Type_check
+
+val opt_interactive : bool ref
+val opt_suppress_banner : bool ref
+
+val ast : tannot defs ref
+
+val env : Env.t ref
diff --git a/src/interpreter.ml b/src/interpreter.ml
index 194812ca..40ee251d 100644
--- a/src/interpreter.ml
+++ b/src/interpreter.ml
@@ -673,7 +673,7 @@ let rec eval_frame' = function
let eval_frame frame =
try eval_frame' frame with
- | Type_check.Type_error (l, err) ->
+ | Type_check.Type_error (env, l, err) ->
raise (Reporting.err_typ l (Type_error.string_of_type_error err))
let rec run_frame frame =
diff --git a/src/isail.ml b/src/isail.ml
index d8876cf0..a3dfe680 100644
--- a/src/isail.ml
+++ b/src/isail.ml
@@ -90,13 +90,15 @@ let rec user_input callback =
let sail_logo =
let banner str = str |> Util.bold |> Util.red |> Util.clear in
let logo =
- [ {| ___ ___ ___ ___ |};
- {| /\ \ /\ \ /\ \ /\__\|};
- {| /::\ \ /::\ \ _\:\ \ /:/ /|};
- {| /\:\:\__\ /::\:\__\ /\/::\__\ /:/__/ |};
- {| \:\:\/__/ \/\::/ / \::/\/__/ \:\ \ |};
- {| \::/ / /:/ / \:\__\ \:\__\|};
- {| \/__/ \/__/ \/__/ \/__/|} ]
+ if !Interactive.opt_suppress_banner then []
+ else
+ [ {| ___ ___ ___ ___ |};
+ {| /\ \ /\ \ /\ \ /\__\|};
+ {| /::\ \ /::\ \ _\:\ \ /:/ /|};
+ {| /\:\:\__\ /::\:\__\ /\/::\__\ /:/__/ |};
+ {| \:\:\/__/ \/\::/ / \::/\/__/ \:\ \ |};
+ {| \::/ / /:/ / \:\__\ \:\__\|};
+ {| \/__/ \/__/ \/__/ \/__/|} ]
in
let help =
[ "Type :commands for a list of commands, and :help <command> for help.";
@@ -104,9 +106,9 @@ let sail_logo =
in
List.map banner logo @ [""] @ help @ [""]
-let vs_ids = ref (Initial_check.val_spec_ids !interactive_ast)
+let vs_ids = ref (Initial_check.val_spec_ids !Interactive.ast)
-let interactive_state = ref (initial_state !interactive_ast Value.primops)
+let interactive_state = ref (initial_state !Interactive.ast Value.primops)
let interactive_bytecode = ref []
@@ -259,7 +261,7 @@ let handle_input' input =
| ":n" | ":normal" ->
current_mode := Normal
| ":t" | ":type" ->
- let typq, typ = Type_check.Env.get_val_spec (mk_id arg) !interactive_env in
+ let typq, typ = Type_check.Env.get_val_spec (mk_id arg) !Interactive.env in
pretty_sail stdout (doc_binding (typq, typ));
print_newline ();
| ":q" | ":quit" ->
@@ -267,15 +269,15 @@ let handle_input' input =
exit 0
| ":i" | ":infer" ->
let exp = Initial_check.exp_of_string arg in
- let exp = Type_check.infer_exp !interactive_env exp in
+ let exp = Type_check.infer_exp !Interactive.env exp in
pretty_sail stdout (doc_typ (Type_check.typ_of exp));
print_newline ()
| ":canon" ->
let typ = Initial_check.typ_of_string arg in
- print_endline (string_of_typ (Type_check.canonicalize !interactive_env typ))
+ print_endline (string_of_typ (Type_check.canonicalize !Interactive.env typ))
| ":prove" ->
let nc = Initial_check.constraint_of_string arg in
- print_endline (string_of_bool (Type_check.prove __POS__ !interactive_env nc))
+ print_endline (string_of_bool (Type_check.prove __POS__ !Interactive.env nc))
| ":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)
@@ -301,7 +303,7 @@ let handle_input' input =
| "Order" -> is_order_kopt
| _ -> failwith "Invalid kind"
in
- let ids = Specialize.polymorphic_functions is_kopt !interactive_ast in
+ let ids = Specialize.polymorphic_functions is_kopt !Interactive.ast in
List.iter (fun id -> print_endline (string_of_id id)) (IdSet.elements ids)
| ":option" ->
begin
@@ -312,17 +314,17 @@ let handle_input' input =
| Arg.Bad message | Arg.Help message -> print_endline message
end;
| ":spec" ->
- let ast, env = Specialize.specialize !interactive_ast !interactive_env in
- interactive_ast := ast;
- interactive_env := env;
- interactive_state := initial_state !interactive_ast Value.primops
+ let ast, env = Specialize.specialize !Interactive.ast !Interactive.env in
+ Interactive.ast := ast;
+ Interactive.env := env;
+ interactive_state := initial_state !Interactive.ast Value.primops
| ":pretty" ->
- print_endline (Pretty_print_sail.to_string (Latex.defs !interactive_ast))
+ print_endline (Pretty_print_sail.to_string (Latex.defs !Interactive.ast))
| ":compile" ->
let open PPrint in
let open C_backend in
- let ast = Process_file.rewrite_ast_c !interactive_ast in
- let ast, env = Specialize.specialize ast !interactive_env in
+ let ast = Process_file.rewrite_ast_c !Interactive.ast in
+ let ast, env = Specialize.specialize ast !Interactive.env in
let ctx = initial_ctx env in
interactive_bytecode := bytecode_ast ctx (List.map flatten_cdef) ast
| ":ir" ->
@@ -339,7 +341,7 @@ let handle_input' input =
print_endline (Pretty_print_sail.to_string (separate_map hardline pp_cdef cdefs))
| ":ast" ->
let chan = open_out arg in
- Pretty_print_sail.pp_defs chan !interactive_ast;
+ Pretty_print_sail.pp_defs chan !Interactive.ast;
close_out chan
| ":output" ->
let chan = open_out arg in
@@ -361,24 +363,24 @@ let handle_input' input =
| ":elf" -> Elf_loader.load_elf arg
| ":l" | ":load" ->
let files = Util.split_on_char ' ' arg in
- let (_, ast, env) = load_files !interactive_env files in
+ let (_, ast, env) = load_files !Interactive.env files in
let ast = Process_file.rewrite_ast_interpreter ast in
- interactive_ast := append_ast !interactive_ast ast;
- interactive_state := initial_state !interactive_ast Value.primops;
- interactive_env := env;
- vs_ids := Initial_check.val_spec_ids !interactive_ast
+ Interactive.ast := append_ast !Interactive.ast ast;
+ interactive_state := initial_state !Interactive.ast Value.primops;
+ Interactive.env := env;
+ vs_ids := Initial_check.val_spec_ids !Interactive.ast
| ":u" | ":unload" ->
- interactive_ast := Ast.Defs [];
- interactive_env := Type_check.initial_env;
- interactive_state := initial_state !interactive_ast Value.primops;
- vs_ids := Initial_check.val_spec_ids !interactive_ast;
+ Interactive.ast := Ast.Defs [];
+ Interactive.env := Type_check.initial_env;
+ interactive_state := initial_state !Interactive.ast Value.primops;
+ vs_ids := Initial_check.val_spec_ids !Interactive.ast;
(* See initial_check.mli for an explanation of why we need this. *)
Initial_check.have_undefined_builtins := false
| ":exec" ->
let open Bytecode_interpreter in
- let exp = Type_check.infer_exp !interactive_env (Initial_check.exp_of_string arg) in
+ let exp = Type_check.infer_exp !Interactive.env (Initial_check.exp_of_string arg) in
let anf = Anf.anf exp in
- let ctx = C_backend.initial_ctx !interactive_env in
+ let ctx = C_backend.initial_ctx !Interactive.env in
let ctyp = C_backend.ctyp_of_typ ctx (Type_check.typ_of exp) in
let setup, call, cleanup = C_backend.compile_aexp ctx anf in
let instrs = C_backend.flatten_instrs (setup @ [call (CL_id (mk_id "interactive#", ctyp))] @ cleanup) in
@@ -389,7 +391,7 @@ let handle_input' input =
| Expression str ->
(* An expression in normal mode is type checked, then puts
us in evaluation mode. *)
- let exp = Type_check.infer_exp !interactive_env (Initial_check.exp_of_string str) in
+ let exp = Type_check.infer_exp !Interactive.env (Initial_check.exp_of_string str) in
current_mode := Evaluation (eval_frame (Step (lazy "", !interactive_state, return exp, [])));
print_program ()
| Empty -> ()
@@ -444,7 +446,7 @@ let handle_input' input =
let handle_input input =
try handle_input' input with
- | Type_check.Type_error (l, err) ->
+ | Type_check.Type_error (env, l, err) ->
print_endline (Type_error.string_of_type_error err)
| Reporting.Fatal_error err ->
Reporting.print_error err
@@ -491,7 +493,7 @@ let () =
LNoise.history_load ~filename:"sail_history" |> ignore;
LNoise.history_set ~max_length:100 |> ignore;
- if !opt_interactive then
+ if !Interactive.opt_interactive then
begin
List.iter print_endline sail_logo;
user_input handle_input
diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml
index b408c6eb..a5478c31 100644
--- a/src/pretty_print_coq.ml
+++ b/src/pretty_print_coq.ml
@@ -2457,7 +2457,7 @@ try
hardline;
string "End Content.";
hardline])
-with Type_check.Type_error (l,err) ->
+with Type_check.Type_error (env,l,err) ->
let extra =
"\nError during Coq printing\n" ^
if Printexc.backtrace_status ()
diff --git a/src/process_file.ml b/src/process_file.ml
index 0194baa8..03fc36a2 100644
--- a/src/process_file.ml
+++ b/src/process_file.ml
@@ -384,7 +384,7 @@ let rewrite_step defs (name, rewriter) =
let rewrite rewriters defs =
try List.fold_left rewrite_step defs rewriters with
- | Type_check.Type_error (l, err) ->
+ | Type_check.Type_error (_, l, err) ->
raise (Reporting.err_typ l (Type_error.string_of_type_error err))
let rewrite_ast = rewrite [("initial", Rewriter.rewrite_defs)]
diff --git a/src/reporting.ml b/src/reporting.ml
index 858e5c41..f27e4c03 100644
--- a/src/reporting.ml
+++ b/src/reporting.ml
@@ -238,20 +238,15 @@ let loc_to_string ?code:(code=true) l =
let s = Format.flush_str_formatter () in
s
-type pos_or_loc = Loc of Parse_ast.l | LocD of Parse_ast.l * Parse_ast.l | Pos of Lexing.position
+type pos_or_loc = Loc of Parse_ast.l | Pos of Lexing.position
let print_err_internal fatal verb_loc p_l m1 m2 =
- Format.eprintf "%s at " m1;
- let _ = (match p_l with Pos p -> print_err_pos p
- | Loc l -> print_err_loc l
- | LocD (l1,l2) ->
- print_err_loc l1; Format.fprintf Format.err_formatter " and "; print_err_loc l2) in
- Format.eprintf "%s\n" m2;
- if verb_loc then (match p_l with Loc l ->
- format_loc_source Format.err_formatter l;
- Format.pp_print_newline Format.err_formatter (); | _ -> ());
- Format.pp_print_flush Format.err_formatter ();
- if fatal then (exit 1) else ()
+ let open Error_format in
+ begin match p_l with
+ | Loc l -> format_message (Location (l, Line m2)) err_formatter
+ | _ -> failwith "Pos"
+ end;
+ if fatal then exit 1 else ()
let print_err fatal verb_loc l m1 m2 =
print_err_internal fatal verb_loc (Loc l) m1 m2
@@ -264,7 +259,6 @@ type error =
| Err_syntax_locn of Parse_ast.l * string
| Err_lex of Lexing.position * string
| Err_type of Parse_ast.l * string
- | Err_type_dual of Parse_ast.l * Parse_ast.l * string
let issues = "\n\nPlease report this as an issue on GitHub at https://github.com/rems-project/sail/issues"
@@ -277,7 +271,6 @@ let dest_err = function
| Err_syntax_locn (l, m) -> ("Syntax error", false, Loc l, m)
| Err_lex (p, s) -> ("Lexical error", false, Pos p, s)
| Err_type (l, m) -> ("Type error", false, Loc l, m)
- | Err_type_dual(l1,l2,m) -> ("Type error", false, LocD (l1,l2), m)
exception Fatal_error of error
@@ -286,11 +279,10 @@ let err_todo l m = Fatal_error (Err_todo (l, m))
let err_unreachable l ocaml_pos m = Fatal_error (Err_unreachable (l, ocaml_pos, m))
let err_general l m = Fatal_error (Err_general (l, m))
let err_typ l m = Fatal_error (Err_type (l,m))
-let err_typ_dual l1 l2 m = Fatal_error (Err_type_dual (l1,l2,m))
let report_error e =
let (m1, verb_pos, pos_l, m2) = dest_err e in
- (print_err_internal verb_pos false pos_l m1 m2; exit 1)
+ print_err_internal verb_pos false pos_l m1 m2
let print_error e =
let (m1, verb_pos, pos_l, m2) = dest_err e in
diff --git a/src/reporting.mli b/src/reporting.mli
index 63ed3eee..4ce0ced8 100644
--- a/src/reporting.mli
+++ b/src/reporting.mli
@@ -90,8 +90,7 @@ type error =
| Err_syntax_locn of Parse_ast.l * string
| Err_lex of Lexing.position * string
| Err_type of Parse_ast.l * string
- | Err_type_dual of Parse_ast.l * Parse_ast.l * string
-
+
exception Fatal_error of error
(** [err_todo l m] is an abreviatiation for [Fatal_error (Err_todo (l, m))] *)
@@ -106,11 +105,8 @@ val err_unreachable : Parse_ast.l -> (string * int * int * int) -> string -> exn
(** [err_typ l m] is an abreviatiation for [Fatal_error (Err_type (l, m))] *)
val err_typ : Parse_ast.l -> string -> exn
-(** [err_typ_dual l1 l2 m] is an abreviatiation for [Fatal_error (Err_type_dual (l1, l2, m))] *)
-val err_typ_dual : Parse_ast.l -> Parse_ast.l -> string -> exn
-
(** Report error should only be used by main to print the error in the end. Everywhere else,
raising a [Fatal_error] exception is recommended. *)
-val report_error : error -> 'a
+val report_error : error -> unit
val print_error : error -> unit
diff --git a/src/rewrites.ml b/src/rewrites.ml
index 8df5ce02..1e3d319a 100644
--- a/src/rewrites.ml
+++ b/src/rewrites.ml
@@ -462,7 +462,7 @@ let rewrite_sizeof (Defs defs) =
for the given parameters in the original environment *)
let inst =
try instantiation_of orig_exp with
- | Type_error (l, err) ->
+ | Type_error (_, l, err) ->
raise (Reporting.err_typ l (Type_error.string_of_type_error err)) in
(* Rewrite the inst using orig_kid so that each type variable has it's
original name rather than a mangled typechecker name *)
@@ -475,7 +475,7 @@ let rewrite_sizeof (Defs defs) =
| Some (A_aux (A_nexp nexp, _)) ->
let sizeof = E_aux (E_sizeof nexp, (l, mk_tannot env (atom_typ nexp) no_effect)) in
(try rewrite_trivial_sizeof_exp sizeof with
- | Type_error (l, err) ->
+ | Type_error (_, l, err) ->
raise (Reporting.err_typ l (Type_error.string_of_type_error err)))
(* If the type variable is Not_found then it was probably
introduced by a P_var pattern, so it likely exists as
@@ -2474,7 +2474,7 @@ let rewrite_vector_concat_assignments defs =
mk_exp (E_assign (lexp, tup)))) in
begin
try check_exp env e_aux unit_typ with
- | Type_error (l, err) ->
+ | Type_error (_, l, err) ->
raise (Reporting.err_typ l (Type_error.string_of_type_error err))
end
else E_aux (e_aux, annot)
@@ -2503,7 +2503,7 @@ let rewrite_tuple_assignments defs =
let let_exp = mk_exp (E_let (letbind, block)) in
begin
try check_exp env let_exp unit_typ with
- | Type_error (l, err) ->
+ | Type_error (_, l, err) ->
raise (Reporting.err_typ l (Type_error.string_of_type_error err))
end
| _ -> E_aux (e_aux, annot)
@@ -3126,7 +3126,7 @@ let construct_toplevel_string_append_func env f_id pat =
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?"
+ | _ -> raise (Reporting.err_unreachable Parse_ast.Unknown __POS__ "mapping prefix func without correct function type?")
in
let s_id = fresh_stringappend_id () in
@@ -3302,7 +3302,7 @@ let rec rewrite_defs_pat_string_append =
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?"
+ | _ -> typ_error env Parse_ast.Unknown "mapping prefix func without correct function type?"
in
let s_id = fresh_stringappend_id () in
@@ -4304,12 +4304,12 @@ let rewrite_defs_realise_mappings (Defs defs) =
(* We need to make sure we get the environment for the last mapping clause *)
let env = match List.rev mapcls with
| MCL_aux (_, mapcl_annot) :: _ -> env_of_annot mapcl_annot
- | _ -> Type_check.typ_error l "mapping with no clauses?"
+ | _ -> raise (Reporting.err_unreachable l __POS__ "mapping with no clauses?")
in
let (typq, bidir_typ) = Env.get_val_spec id env in
let (typ1, typ2, l) = match bidir_typ with
| Typ_aux (Typ_bidir (typ1, typ2), l) -> typ1, typ2, l
- | _ -> Type_check.typ_error l "non-bidir type of mapping?"
+ | _ -> raise (Reporting.err_unreachable l __POS__ "non-bidir type of mapping?")
in
let forwards_typ = Typ_aux (Typ_fn ([typ1], typ2, no_effect), l) in
let forwards_matches_typ = Typ_aux (Typ_fn ([typ1], bool_typ, no_effect), l) in
@@ -5144,7 +5144,7 @@ let rewrite_check_annot =
else ());
exp
with
- Type_error (l, err) -> raise (Reporting.err_typ l (Type_error.string_of_type_error err))
+ Type_error (_, l, err) -> raise (Reporting.err_typ l (Type_error.string_of_type_error err))
in
let check_pat pat =
prerr_endline ("CHECKING PAT: " ^ string_of_pat pat ^ " : " ^ string_of_typ (typ_of_pat pat));
diff --git a/src/sail.ml b/src/sail.ml
index 247cae25..2777b7a5 100644
--- a/src/sail.ml
+++ b/src/sail.ml
@@ -54,7 +54,6 @@ module Big_int = Nat_big_num
let lib = ref ([] : string list)
let opt_file_out : string option ref = ref None
-let opt_interactive = ref false
let opt_interactive_script : string option ref = ref None
let opt_print_version = ref false
let opt_print_initial_env = ref false
@@ -79,10 +78,10 @@ let options = Arg.align ([
Arg.String (fun f -> opt_file_out := Some f),
"<prefix> select output filename prefix");
( "-i",
- Arg.Tuple [Arg.Set opt_interactive; Arg.Set Initial_check.opt_undefined_gen],
+ Arg.Tuple [Arg.Set Interactive.opt_interactive; Arg.Set Initial_check.opt_undefined_gen],
" start interactive interpreter");
( "-is",
- Arg.Tuple [Arg.Set opt_interactive; Arg.Set Initial_check.opt_undefined_gen;
+ Arg.Tuple [Arg.Set Interactive.opt_interactive; Arg.Set Initial_check.opt_undefined_gen;
Arg.String (fun s -> opt_interactive_script := Some s)],
"<filename> start interactive interpreter and execute commands in script");
( "-iout",
@@ -273,8 +272,6 @@ let _ =
opt_file_arguments := (!opt_file_arguments) @ [s])
usage_msg
-let interactive_ast = ref (Ast.Defs [])
-let interactive_env = ref Type_check.initial_env
let load_files type_envs files =
if !opt_memo_z3 then Constraint.load_digests () else ();
@@ -349,9 +346,9 @@ let main() =
(*let _ = Printf.eprintf "Type checked, next to pretty print" in*)
begin
- (if !(opt_interactive)
+ (if !(Interactive.opt_interactive)
then
- (interactive_ast := Process_file.rewrite_ast_interpreter ast; interactive_env := type_envs)
+ (Interactive.ast := Process_file.rewrite_ast_interpreter ast; Interactive.env := type_envs)
else ());
(if !(opt_sanity)
then
@@ -414,7 +411,10 @@ let main() =
let _ = try
begin
- try ignore(main ())
- with Failure(s) -> raise (Reporting.err_general Parse_ast.Unknown ("Failure "^s))
+ try ignore (main ())
+ with Failure s -> raise (Reporting.err_general Parse_ast.Unknown ("Failure " ^ s))
end
- with Reporting.Fatal_error e -> Reporting.report_error e
+ with Reporting.Fatal_error e ->
+ Reporting.report_error e;
+ Interactive.opt_suppress_banner := true;
+ if !Interactive.opt_interactive then () else exit 1
diff --git a/src/type_check.ml b/src/type_check.ml
index 1dfc5957..b362e813 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -96,13 +96,42 @@ type type_error =
| Err_subtype of typ * typ * n_constraint list * Ast.l KBindings.t
| Err_no_num_ident of id
| Err_other of string
- | Err_because of type_error * type_error
+ | Err_because of type_error * Parse_ast.l * type_error
+
+type env =
+ { top_val_specs : (typquant * typ) Bindings.t;
+ defined_val_specs : IdSet.t;
+ locals : (mut * typ) Bindings.t;
+ union_ids : (typquant * typ) Bindings.t;
+ registers : (effect * effect * typ) Bindings.t;
+ variants : (typquant * type_union list) Bindings.t;
+ mappings : (typquant * typ * typ) Bindings.t;
+ typ_vars : (Ast.l * kind_aux) KBindings.t;
+ shadow_vars : int KBindings.t;
+ typ_synonyms : (env -> typ_arg list -> typ_arg) Bindings.t;
+ num_defs : nexp Bindings.t;
+ overloads : (id list) Bindings.t;
+ flow : (typ -> typ) Bindings.t;
+ enums : IdSet.t Bindings.t;
+ records : (typquant * (typ * id) list) Bindings.t;
+ accessors : (typquant * typ) Bindings.t;
+ externs : (string -> string option) Bindings.t;
+ casts : id list;
+ allow_casts : bool;
+ allow_bindings : bool;
+ constraints : n_constraint list;
+ default_order : order option;
+ ret_typ : typ option;
+ poly_undefineds : bool;
+ prove : env -> n_constraint -> bool;
+ allow_unknowns : bool;
+ }
-exception Type_error of l * type_error;;
+exception Type_error of env * l * type_error;;
-let typ_error l m = raise (Type_error (l, Err_other m))
+let typ_error env l m = raise (Type_error (env, l, Err_other m))
-let typ_raise l err = raise (Type_error (l, err))
+let typ_raise env l err = raise (Type_error (env, l, err))
let deinfix = function
| Id_aux (Id v, l) -> Id_aux (DeIid v, l)
@@ -225,7 +254,7 @@ let rec name_pat (P_aux (aux, _)) =
| P_id id | P_as (_, id) -> Some ("_" ^ string_of_id id)
| P_typ (_, pat) | P_var (pat, _) -> name_pat pat
| _ -> None
-
+
let ex_counter = ref 0
let fresh_existential k =
@@ -299,7 +328,7 @@ let adding = Util.("Adding " |> darkgray |> clear)
(**************************************************************************)
module Env : sig
- type t
+ type t = env
val add_val_spec : id -> typquant * typ -> t -> t
val update_val_spec : id -> typquant * typ -> t -> t
val define_val_spec : id -> t -> t
@@ -389,34 +418,7 @@ module Env : sig
val builtin_typs : typquant Bindings.t
end = struct
- type t =
- { top_val_specs : (typquant * typ) Bindings.t;
- defined_val_specs : IdSet.t;
- locals : (mut * typ) Bindings.t;
- union_ids : (typquant * typ) Bindings.t;
- registers : (effect * effect * typ) Bindings.t;
- variants : (typquant * type_union list) Bindings.t;
- mappings : (typquant * typ * typ) Bindings.t;
- typ_vars : (Ast.l * kind_aux) KBindings.t;
- shadow_vars : int KBindings.t;
- typ_synonyms : (t -> typ_arg list -> typ_arg) Bindings.t;
- num_defs : nexp Bindings.t;
- overloads : (id list) Bindings.t;
- flow : (typ -> typ) Bindings.t;
- enums : IdSet.t Bindings.t;
- records : (typquant * (typ * id) list) Bindings.t;
- accessors : (typquant * typ) Bindings.t;
- externs : (string -> string option) Bindings.t;
- casts : id list;
- allow_casts : bool;
- allow_bindings : bool;
- constraints : n_constraint list;
- default_order : order option;
- ret_typ : typ option;
- poly_undefineds : bool;
- prove : t -> n_constraint -> bool;
- allow_unknowns : bool;
- }
+ type t = env
let empty =
{ top_val_specs = Bindings.empty;
@@ -454,11 +456,11 @@ end = struct
let get_typ_var kid env =
try snd (KBindings.find kid env.typ_vars) with
- | Not_found -> typ_error (kid_loc kid) ("No type variable " ^ string_of_kid kid)
+ | Not_found -> typ_error env (kid_loc kid) ("No type variable " ^ string_of_kid kid)
let get_typ_var_loc kid env =
try fst (KBindings.find kid env.typ_vars) with
- | Not_found -> typ_error (kid_loc kid) ("No type variable " ^ string_of_kid kid)
+ | Not_found -> typ_error env (kid_loc kid) ("No type variable " ^ string_of_kid kid)
let get_typ_vars env = KBindings.map snd env.typ_vars
let get_typ_var_locs env = KBindings.map fst env.typ_vars
@@ -519,9 +521,9 @@ end = struct
else if Bindings.mem id env.enums then
mk_typquant []
else if Bindings.mem id env.typ_synonyms then
- typ_error (id_loc id) ("Cannot infer kind of type synonym " ^ string_of_id id)
+ typ_error env (id_loc id) ("Cannot infer kind of type synonym " ^ string_of_id id)
else
- typ_error (id_loc id) ("Cannot infer kind of " ^ string_of_id id)
+ typ_error env (id_loc id) ("Cannot infer kind of " ^ string_of_id id)
let check_args_typquant id env args typq =
let kopts, ncs = quant_split typq in
@@ -536,13 +538,13 @@ end = struct
| kopt :: kopts, A_aux (A_bool arg, _) :: args when is_bool_kopt kopt ->
subst_args kopts args
| [], [] -> ncs
- | _, A_aux (_, l) :: _ -> typ_error l ("Error when processing type quantifer arguments " ^ string_of_typquant typq)
- | _, _ -> typ_error Parse_ast.Unknown ("Error when processing type quantifer arguments " ^ string_of_typquant typq)
+ | _, A_aux (_, l) :: _ -> typ_error env l ("Error when processing type quantifer arguments " ^ string_of_typquant typq)
+ | _, _ -> typ_error env Parse_ast.Unknown ("Error when processing type quantifer arguments " ^ string_of_typquant typq)
in
let ncs = subst_args kopts args in
if List.for_all (env.prove env) ncs
then ()
- else typ_error (id_loc id) ("Could not prove " ^ string_of_list ", " string_of_n_constraint ncs ^ " for type constructor " ^ string_of_id id)
+ else typ_error env (id_loc id) ("Could not prove " ^ string_of_list ", " string_of_n_constraint ncs ^ " for type constructor " ^ string_of_id id)
let rec expand_constraint_synonyms env (NC_aux (aux, l) as nc) =
typ_debug ~level:2 (lazy ("Expanding " ^ string_of_n_constraint nc));
@@ -553,7 +555,7 @@ end = struct
(try
begin match Bindings.find id env.typ_synonyms env args with
| A_aux (A_bool nc, _) -> expand_constraint_synonyms env nc
- | arg -> typ_error l ("Expected Bool when expanding synonym " ^ string_of_id id ^ " got " ^ string_of_typ_arg arg)
+ | arg -> typ_error env l ("Expected Bool when expanding synonym " ^ string_of_id id ^ " got " ^ string_of_typ_arg arg)
end
with Not_found -> NC_aux (NC_app (id, List.map (expand_synonyms_arg env) args), l))
| NC_true | NC_false | NC_equal _ | NC_not_equal _ | NC_bounded_le _ | NC_bounded_ge _ | NC_var _ | NC_set _ -> nc
@@ -568,7 +570,7 @@ end = struct
(try
begin match Bindings.find id env.typ_synonyms env args with
| A_aux (A_typ typ, _) -> expand_synonyms env typ
- | _ -> typ_error l ("Expected Type when expanding synonym " ^ string_of_id id)
+ | _ -> typ_error env l ("Expected Type when expanding synonym " ^ string_of_id id)
end
with
| Not_found -> Typ_aux (Typ_app (id, List.map (expand_synonyms_arg env) args), l))
@@ -576,7 +578,7 @@ end = struct
(try
begin match Bindings.find id env.typ_synonyms env [] with
| A_aux (A_typ typ, _) -> expand_synonyms env typ
- | _ -> typ_error l ("Expected Type when expanding synonym " ^ string_of_id id)
+ | _ -> typ_error env l ("Expected Type when expanding synonym " ^ string_of_id id)
end
with
| Not_found -> Typ_aux (Typ_id id, l))
@@ -644,31 +646,31 @@ end = struct
| Typ_id id when bound_typ_id env id ->
let typq = infer_kind env id in
if quant_kopts typq != []
- then typ_error l ("Type constructor " ^ string_of_id id ^ " expected " ^ string_of_typquant typq)
+ then typ_error env l ("Type constructor " ^ string_of_id id ^ " expected " ^ string_of_typquant typq)
else ()
- | Typ_id id -> typ_error l ("Undefined type " ^ string_of_id id)
+ | Typ_id id -> typ_error env l ("Undefined type " ^ string_of_id id)
| Typ_var kid -> begin
match KBindings.find kid env.typ_vars with
| (_, K_type) -> ()
- | (_, k) -> typ_error l ("Kind identifier " ^ string_of_kid kid ^ " in type " ^ string_of_typ typ
+ | (_, k) -> typ_error env l ("Kind identifier " ^ string_of_kid kid ^ " in type " ^ string_of_typ typ
^ " is " ^ string_of_kind_aux k ^ " rather than Type")
| exception Not_found ->
- typ_error l ("Unbound kind identifier " ^ string_of_kid kid ^ " in type " ^ string_of_typ typ)
+ typ_error env l ("Unbound kind identifier " ^ string_of_kid kid ^ " in type " ^ string_of_typ typ)
end
| Typ_fn (arg_typs, ret_typ, effs) -> List.iter (wf_typ ~exs:exs env) arg_typs; wf_typ ~exs:exs env ret_typ
| Typ_bidir (typ1, typ2) when strip_typ typ1 = strip_typ typ2 ->
- typ_error l "Bidirectional types cannot be the same on both sides"
+ typ_error env l "Bidirectional types cannot be the same on both sides"
| Typ_bidir (typ1, typ2) -> wf_typ ~exs:exs env typ1; wf_typ ~exs:exs env typ2
| Typ_tup typs -> List.iter (wf_typ ~exs:exs env) typs
| Typ_app (id, args) when bound_typ_id env id ->
List.iter (wf_typ_arg ~exs:exs env) args;
check_args_typquant id env args (infer_kind env id)
- | Typ_app (id, _) -> typ_error l ("Undefined type " ^ string_of_id id)
- | Typ_exist ([], _, _) -> typ_error l ("Existential must have some type variables")
+ | Typ_app (id, _) -> typ_error env l ("Undefined type " ^ string_of_id id)
+ | Typ_exist ([], _, _) -> typ_error env l ("Existential must have some type variables")
| Typ_exist (kopts, nc, typ) when KidSet.is_empty exs ->
wf_constraint ~exs:(KidSet.of_list (List.map kopt_kid kopts)) env nc;
wf_typ ~exs:(KidSet.of_list (List.map kopt_kid kopts)) { env with constraints = nc :: env.constraints } typ
- | Typ_exist (_, _, _) -> typ_error l ("Nested existentials are not allowed")
+ | Typ_exist (_, _, _) -> typ_error env l ("Nested existentials are not allowed")
| Typ_internal_unknown -> unreachable l __POS__ "escaped Typ_internal_unknown"
and wf_typ_arg ?exs:(exs=KidSet.empty) env (A_aux (typ_arg_aux, _)) =
match typ_arg_aux with
@@ -684,7 +686,7 @@ end = struct
| Nexp_var kid ->
begin match get_typ_var kid env with
| K_int -> ()
- | kind -> typ_error l ("Constraint is badly formed, "
+ | kind -> typ_error env l ("Constraint is badly formed, "
^ string_of_kid kid ^ " has kind "
^ string_of_kind_aux kind ^ " but should have kind Int")
end
@@ -701,7 +703,7 @@ end = struct
| Ord_var kid ->
begin match get_typ_var kid env with
| K_order -> ()
- | kind -> typ_error l ("Order is badly formed, "
+ | kind -> typ_error env l ("Order is badly formed, "
^ string_of_kid kid ^ " has kind "
^ string_of_kind_aux kind ^ " but should have kind Order")
end
@@ -717,7 +719,7 @@ end = struct
| NC_set (kid, _) ->
begin match get_typ_var kid env with
| K_int -> ()
- | kind -> typ_error l ("Set constraint is badly formed, "
+ | kind -> typ_error env l ("Set constraint is badly formed, "
^ string_of_kid kid ^ " has kind "
^ string_of_kind_aux kind ^ " but should have kind Int")
end
@@ -728,7 +730,7 @@ end = struct
| NC_var kid ->
begin match get_typ_var kid env with
| K_bool -> ()
- | kind -> typ_error l (string_of_kid kid ^ " has kind "
+ | kind -> typ_error env l (string_of_kid kid ^ " has kind "
^ string_of_kind_aux kind ^ " but should have kind Bool")
end
| NC_true | NC_false -> ()
@@ -754,7 +756,7 @@ end = struct
try
Bindings.find id env.top_val_specs
with
- | Not_found -> typ_error (id_loc id) ("No val spec found for " ^ string_of_id id)
+ | Not_found -> typ_error env (id_loc id) ("No val spec found for " ^ string_of_id id)
let get_val_spec id env =
try
@@ -764,7 +766,7 @@ end = struct
typ_debug (lazy ("get_val_spec: freshened to " ^ string_of_bind bind'));
bind'
with
- | Not_found -> typ_error (id_loc id) ("No val spec found for " ^ string_of_id id)
+ | Not_found -> typ_error env (id_loc id) ("No val spec found for " ^ string_of_id id)
let add_union_id id bind env =
typ_print (lazy (adding ^ "union identifier " ^ string_of_id id ^ " : " ^ string_of_bind bind));
@@ -775,7 +777,7 @@ end = struct
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)
+ | Not_found -> typ_error env (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
@@ -803,7 +805,7 @@ end = struct
typ_print (lazy (adding ^ "mapping " ^ string_of_id id ^ " : " ^ string_of_bind (typq, typ)));
{ env with top_val_specs = Bindings.add id (typq, typ) env.top_val_specs }
- | _ -> typ_error (id_loc id) "val definition must have a mapping or function type"
+ | _ -> typ_error env (id_loc id) "val definition must have a mapping or function type"
end
and add_val_spec id (bind_typq, bind_typ) env =
@@ -816,7 +818,7 @@ end = struct
let existing_cmp = (strip_typq existing_typq, strip_typ existing_typ) in
let bind_cmp = (strip_typq bind_typq, strip_typ bind_typ) in
if existing_cmp <> bind_cmp then
- 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))
+ typ_error env (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
*)
@@ -850,7 +852,7 @@ end = struct
let define_val_spec id env =
if IdSet.mem id env.defined_val_specs
- then typ_error (id_loc id) ("Function " ^ string_of_id id ^ " has already been declared")
+ then typ_error env (id_loc id) ("Function " ^ string_of_id id ^ " has already been declared")
else { env with defined_val_specs = IdSet.add id env.defined_val_specs }
let is_union_constructor id env =
@@ -875,7 +877,7 @@ end = struct
let add_enum id ids env =
if bound_typ_id env id
- then typ_error (id_loc id) ("Cannot create enum " ^ string_of_id id ^ ", type name is already bound")
+ then typ_error env (id_loc id) ("Cannot create enum " ^ string_of_id id ^ ", type name is already bound")
else
begin
typ_print (lazy (adding ^ "enum " ^ string_of_id id));
@@ -885,7 +887,7 @@ end = struct
let get_enum id env =
try IdSet.elements (Bindings.find id env.enums)
with
- | Not_found -> typ_error (id_loc id) ("Enumeration " ^ string_of_id id ^ " does not exist")
+ | Not_found -> typ_error env (id_loc id) ("Enumeration " ^ string_of_id id ^ " does not exist")
let is_record id env = Bindings.mem id env.records
@@ -893,7 +895,7 @@ end = struct
let add_record id typq fields env =
if bound_typ_id env id
- then typ_error (id_loc id) ("Cannot create record " ^ string_of_id id ^ ", type name is already bound")
+ then typ_error env (id_loc id) ("Cannot create record " ^ string_of_id id ^ ", type name is already bound")
else
begin
typ_print (lazy (adding ^ "record " ^ string_of_id id));
@@ -924,14 +926,14 @@ end = struct
let freshen_bind bind = List.fold_left (fun bind (kid, _) -> freshen_kid env kid bind) bind (KBindings.bindings env.typ_vars) in
try freshen_bind (Bindings.find (field_name rec_id id) env.accessors)
with
- | Not_found -> typ_error (id_loc id) ("No accessor found for " ^ string_of_id (field_name rec_id id))
+ | Not_found -> typ_error env (id_loc id) ("No accessor found for " ^ string_of_id (field_name rec_id id))
let get_accessor rec_id id env =
match get_accessor_fn rec_id id env with
(* All accessors should have a single argument (the record itself) *)
| (typq, Typ_aux (Typ_fn ([rec_typ], field_typ, effect), _)) ->
(typq, rec_typ, field_typ, effect)
- | _ -> typ_error (id_loc id) ("Accessor with non-function type found for " ^ string_of_id (field_name rec_id id))
+ | _ -> typ_error env (id_loc id) ("Accessor with non-function type found for " ^ string_of_id (field_name rec_id id))
let is_mutable id env =
try
@@ -948,10 +950,10 @@ end = struct
let add_local id mtyp env =
begin
- if not env.allow_bindings then typ_error (id_loc id) "Bindings are not allowed in this context" else ();
+ if not env.allow_bindings then typ_error env (id_loc id) "Bindings are not allowed in this context" else ();
wf_typ env (snd mtyp);
if Bindings.mem id env.top_val_specs then
- typ_error (id_loc id) ("Local variable " ^ string_of_id id ^ " is already bound as a function name")
+ typ_error env (id_loc id) ("Local variable " ^ string_of_id id ^ " is already bound as a function name")
else ();
typ_print (lazy (adding ^ "local binding " ^ string_of_id id ^ " : " ^ string_of_mtyp mtyp));
{ env with locals = Bindings.add id mtyp env.locals }
@@ -968,12 +970,12 @@ end = struct
let add_variant_clause id tu env =
match Bindings.find_opt id env.variants with
| Some (typq, tus) -> { env with variants = Bindings.add id (typq, tus @ [tu]) env.variants }
- | None -> typ_error (id_loc id) ("scattered union " ^ string_of_id id ^ " not found")
+ | None -> typ_error env (id_loc id) ("scattered union " ^ string_of_id id ^ " not found")
let get_variant id env =
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")
+ | None -> typ_error env (id_loc id) ("union " ^ string_of_id id ^ " not found")
let get_flow id env =
try Bindings.find id env.flow with
| Not_found -> fun typ -> typ
@@ -991,7 +993,7 @@ end = struct
let get_register id env =
try Bindings.find id env.registers with
- | Not_found -> typ_error (id_loc id) ("No register binding found for " ^ string_of_id id)
+ | Not_found -> typ_error env (id_loc id) ("No register binding found for " ^ string_of_id id)
let is_extern id env backend =
try not (Bindings.find id env.externs backend = None) with
@@ -1005,16 +1007,16 @@ end = struct
try
match Bindings.find id env.externs backend with
| Some ext -> ext
- | None -> typ_error (id_loc id) ("No extern binding found for " ^ string_of_id id)
+ | None -> typ_error env (id_loc id) ("No extern binding found for " ^ string_of_id id)
with
- | Not_found -> typ_error (id_loc id) ("No extern binding found for " ^ string_of_id id)
+ | Not_found -> typ_error env (id_loc id) ("No extern binding found for " ^ string_of_id id)
let get_casts env = env.casts
let add_register id reff weff typ env =
wf_typ env typ;
if Bindings.mem id env.registers
- then typ_error (id_loc id) ("Register " ^ string_of_id id ^ " is already bound")
+ then typ_error env (id_loc id) ("Register " ^ string_of_id id ^ " is already bound")
else
begin
typ_print (lazy (adding ^ "register binding " ^ string_of_id id ^ " :: " ^ string_of_typ typ));
@@ -1060,7 +1062,7 @@ end = struct
let add_num_def id nexp env =
if Bindings.mem id env.num_defs
- then typ_error (id_loc id) ("Num identifier " ^ string_of_id id ^ " is already bound")
+ then typ_error env (id_loc id) ("Num identifier " ^ string_of_id id ^ " is already bound")
else
begin
typ_print (lazy (adding ^ "Num identifier " ^ string_of_id id ^ " : " ^ string_of_nexp nexp));
@@ -1069,7 +1071,7 @@ end = struct
let get_num_def id env =
try Bindings.find id env.num_defs with
- | Not_found -> typ_raise (id_loc id) (Err_no_num_ident id)
+ | Not_found -> typ_raise env (id_loc id) (Err_no_num_ident id)
let get_constraints env = env.constraints
@@ -1099,7 +1101,7 @@ end = struct
let add_typ_synonym id synonym env =
if Bindings.mem id env.typ_synonyms
- then typ_error (id_loc id) ("Type synonym " ^ string_of_id id ^ " already exists")
+ then typ_error env (id_loc id) ("Type synonym " ^ string_of_id id ^ " already exists")
else
begin
typ_print (lazy (adding ^ "type synonym " ^ string_of_id id));
@@ -1110,13 +1112,13 @@ end = struct
let get_default_order env =
match env.default_order with
- | None -> typ_error Parse_ast.Unknown ("No default order has been set")
+ | None -> typ_error env Parse_ast.Unknown ("No default order has been set")
| Some ord -> ord
let set_default_order o env =
match env.default_order with
| None -> { env with default_order = Some (Ord_aux (o, Parse_ast.Unknown)) }
- | Some _ -> typ_error Parse_ast.Unknown ("Cannot change default order once already set")
+ | Some _ -> typ_error env Parse_ast.Unknown ("Cannot change default order once already set")
let set_default_order_inc = set_default_order Ord_inc
let set_default_order_dec = set_default_order Ord_dec
@@ -1192,7 +1194,7 @@ let bind_numeric l typ env =
match destruct_numeric (Env.expand_synonyms env typ) with
| Some (kids, nc, nexp) ->
nexp, add_existential l (List.map (mk_kopt K_int) kids) nc env
- | None -> typ_error l ("Expected " ^ string_of_typ typ ^ " to be numeric")
+ | None -> typ_error env l ("Expected " ^ string_of_typ typ ^ " to be numeric")
(** Pull an (potentially)-existentially qualified type into the global
typing environment **)
@@ -1597,7 +1599,7 @@ let unify l env goals typ1 typ2 =
^ " for " ^ Util.string_of_list ", " string_of_kid (KidSet.elements goals)));
let typ1, typ2 = Env.expand_synonyms env typ1, Env.expand_synonyms env typ2 in
if not (KidSet.is_empty (KidSet.inter goals (tyvars_of_typ typ2))) then
- typ_error l ("Occurs check failed: " ^ string_of_typ typ2 ^ " contains "
+ typ_error env l ("Occurs check failed: " ^ string_of_typ typ2 ^ " contains "
^ Util.string_of_list ", " string_of_kid (KidSet.elements goals))
else
unify_typ l env goals typ1 typ2
@@ -1675,7 +1677,7 @@ let rec kid_order kind_map (Typ_aux (aux, l) as typ) =
List.fold_left (fun (ord, kids) typ -> let (ord', kids) = kid_order kids typ in (ord @ ord', kids)) ([], kind_map) typs
| Typ_app (_, args) ->
List.fold_left (fun (ord, kids) arg -> let (ord', kids) = kid_order_arg kids arg in (ord @ ord', kids)) ([], kind_map) args
- | Typ_fn _ | Typ_bidir _ | Typ_exist _ -> typ_error l ("Existential or function type cannot appear within existential type: " ^ string_of_typ typ)
+ | Typ_fn _ | Typ_bidir _ | Typ_exist _ -> typ_error Env.empty l ("Existential or function type cannot appear within existential type: " ^ string_of_typ typ)
| Typ_internal_unknown -> unreachable l __POS__ "escaped Typ_internal_unknown"
and kid_order_arg kind_map (A_aux (aux, l) as arg) =
match aux with
@@ -1801,15 +1803,15 @@ let rec subtyp l env typ1 typ2 =
(* Special cases for two numeric (atom) types *)
| Some (kids1, nc1, nexp1), Some ([], _, nexp2) ->
let env = add_existential l (List.map (mk_kopt K_int) kids1) nc1 env in
- if prove __POS__ env (nc_eq nexp1 nexp2) then () else typ_raise l (Err_subtype (typ1, typ2, Env.get_constraints env, Env.get_typ_var_locs env))
+ if prove __POS__ env (nc_eq nexp1 nexp2) then () else typ_raise env l (Err_subtype (typ1, typ2, Env.get_constraints env, Env.get_typ_var_locs env))
| Some (kids1, nc1, nexp1), Some (kids2, nc2, nexp2) ->
let env = add_existential l (List.map (mk_kopt K_int) kids1) nc1 env in
let env = add_typ_vars l (List.map (mk_kopt K_int) (KidSet.elements (KidSet.inter (nexp_frees nexp2) (KidSet.of_list kids2)))) env in
let kids2 = KidSet.elements (KidSet.diff (KidSet.of_list kids2) (nexp_frees nexp2)) in
- if not (kids2 = []) then typ_error l ("Universally quantified constraint generated: " ^ Util.string_of_list ", " string_of_kid kids2) else ();
+ if not (kids2 = []) then typ_error env l ("Universally quantified constraint generated: " ^ Util.string_of_list ", " string_of_kid kids2) else ();
let env = Env.add_constraint (nc_eq nexp1 nexp2) env in
if prove __POS__ env nc2 then ()
- else typ_raise l (Err_subtype (typ1, typ2, Env.get_constraints env, Env.get_typ_var_locs env))
+ else typ_raise env l (Err_subtype (typ1, typ2, Env.get_constraints env, Env.get_typ_var_locs env))
| _, _ ->
match typ_aux1, typ_aux2 with
| _, Typ_internal_unknown when Env.allow_unknowns env -> ()
@@ -1837,16 +1839,16 @@ let rec subtyp l env typ1 typ2 =
let typ1 = canonicalize env typ1 in
let env = add_typ_vars l kopts env in
let kids' = KidSet.elements (KidSet.diff (KidSet.of_list (List.map kopt_kid kopts)) (tyvars_of_typ typ2)) in
- if not (kids' = []) then typ_error l "Universally quantified constraint generated" else ();
+ if not (kids' = []) then typ_error env l "Universally quantified constraint generated" else ();
let unifiers =
try unify l env (KidSet.diff (tyvars_of_typ typ2) (tyvars_of_typ typ1)) typ2 typ1 with
- | Unification_error (_, m) -> typ_error l m
+ | Unification_error (_, m) -> typ_error env l m
in
let nc = List.fold_left (fun nc (kid, uvar) -> constraint_subst kid uvar nc) nc (KBindings.bindings unifiers) in
let env = List.fold_left unifier_constraint env (KBindings.bindings unifiers) in
if prove __POS__ env nc then ()
- else typ_raise l (Err_subtype (typ1, typ2, Env.get_constraints env, Env.get_typ_var_locs env))
- | None, None -> typ_raise l (Err_subtype (typ1, typ2, Env.get_constraints env, Env.get_typ_var_locs env))
+ else typ_raise env l (Err_subtype (typ1, typ2, Env.get_constraints env, Env.get_typ_var_locs env))
+ | None, None -> typ_raise env l (Err_subtype (typ1, typ2, Env.get_constraints env, Env.get_typ_var_locs env))
and subtyp_arg l env (A_aux (aux1, _) as arg1) (A_aux (aux2, _) as arg2) =
typ_print (lazy (("Subtype arg " |> Util.green |> Util.clear) ^ string_of_typ_arg arg1 ^ " and " ^ string_of_typ_arg arg2));
@@ -1855,7 +1857,7 @@ and subtyp_arg l env (A_aux (aux1, _) as arg1) (A_aux (aux2, _) as arg2) =
| A_typ typ1, A_typ typ2 -> subtyp l env typ1 typ2
| A_order ord1, A_order ord2 when ord_identical ord1 ord2 -> ()
| A_bool nc1, A_bool nc2 when prove __POS__ env (nc_and (nc_or (nc_not nc1) nc2) (nc_or (nc_not nc2) nc1)) -> ()
- | _, _ -> typ_error l "Mismatched argument types in subtype check"
+ | _, _ -> typ_error env l "Mismatched argument types in subtype check"
let typ_equality l env typ1 typ2 =
subtyp l env typ1 typ2; subtyp l env typ2 typ1
@@ -1936,16 +1938,16 @@ let infer_lit env (L_aux (lit_aux, l) as lit) =
match Env.get_default_order env with
| Ord_aux (Ord_inc, _) | Ord_aux (Ord_dec, _) ->
dvector_typ env (nint (String.length str)) (mk_typ (Typ_id (mk_id "bit")))
- | Ord_aux (Ord_var _, _) -> typ_error l default_order_error_string
+ | Ord_aux (Ord_var _, _) -> typ_error env l default_order_error_string
end
| L_hex str ->
begin
match Env.get_default_order env with
| Ord_aux (Ord_inc, _) | Ord_aux (Ord_dec, _) ->
dvector_typ env (nint (String.length str * 4)) (mk_typ (Typ_id (mk_id "bit")))
- | Ord_aux (Ord_var _, _) -> typ_error l default_order_error_string
+ | Ord_aux (Ord_var _, _) -> typ_error env l default_order_error_string
end
- | L_undef -> typ_error l "Cannot infer the type of undefined"
+ | L_undef -> typ_error env l "Cannot infer the type of undefined"
let is_nat_kid kid = function
| KOpt_aux (KOpt_kind (K_aux (K_int, _), kid'), _) -> Kid.compare kid kid' = 0
@@ -1995,7 +1997,7 @@ let destruct_vec_typ l env typ =
A_aux (A_order o, _);
A_aux (A_typ vtyp, _)]
), _) when string_of_id id = "vector" -> (n1, o, vtyp)
- | typ -> typ_error l ("Expected vector type, got " ^ string_of_typ typ)
+ | typ -> typ_error env l ("Expected vector type, got " ^ string_of_typ typ)
in
destruct_vec_typ' l (Env.expand_synonyms env typ)
@@ -2052,7 +2054,7 @@ let to_simple_numeric l kids nc (Nexp_aux (aux, _) as n) =
| _, [] ->
Equal n
| _ ->
- typ_error l "Numeric type is non-simple"
+ typ_error Env.empty l "Numeric type is non-simple"
let union_simple_numeric ex1 ex2 =
match ex1, ex2 with
@@ -2205,7 +2207,7 @@ let crule r env exp typ =
Env.wf_typ env (typ_of checked_exp);
decr depth; checked_exp
with
- | Type_error (l, err) -> decr depth; typ_raise l err
+ | Type_error (env, l, err) -> decr depth; typ_raise env l err
let irule r env exp =
incr depth;
@@ -2216,7 +2218,7 @@ let irule r env exp =
decr depth;
inferred_exp
with
- | Type_error (l, err) -> decr depth; typ_raise l err
+ | Type_error (env, l, err) -> decr depth; typ_raise env l err
(* This function adds useful assertion messages to asserts missing them *)
@@ -2266,7 +2268,7 @@ let rec check_exp env (E_aux (exp_aux, (l, ())) as exp : unit exp) (Typ_aux (typ
let checked_xs = crule check_exp env xs typ in
let checked_x = crule check_exp env x elem_typ in
annot_exp (E_cons (checked_x, checked_xs)) typ
- | None -> typ_error l ("Cons " ^ string_of_exp exp ^ " must have list type, got " ^ string_of_typ typ)
+ | None -> typ_error env l ("Cons " ^ string_of_exp exp ^ " must have list type, got " ^ string_of_typ typ)
end
| E_list xs, _ ->
begin
@@ -2274,7 +2276,7 @@ let rec check_exp env (E_aux (exp_aux, (l, ())) as exp : unit exp) (Typ_aux (typ
| Some elem_typ ->
let checked_xs = List.map (fun x -> crule check_exp env x elem_typ) xs in
annot_exp (E_list checked_xs) typ
- | None -> typ_error l ("List " ^ string_of_exp exp ^ " must have list type, got " ^ string_of_typ typ)
+ | None -> typ_error env l ("List " ^ string_of_exp exp ^ " must have list type, got " ^ string_of_typ typ)
end
| E_record_update (exp, fexps), _ ->
(* TODO: this could also infer exp - also fix code duplication with E_record below *)
@@ -2282,11 +2284,11 @@ let rec check_exp env (E_aux (exp_aux, (l, ())) as exp : unit exp) (Typ_aux (typ
let rectyp_id = match Env.expand_synonyms env typ with
| Typ_aux (Typ_id rectyp_id, _) | Typ_aux (Typ_app (rectyp_id, _), _) when Env.is_record rectyp_id env ->
rectyp_id
- | _ -> typ_error l ("The type " ^ string_of_typ typ ^ " is not a record")
+ | _ -> typ_error env l ("The type " ^ string_of_typ typ ^ " is not a record")
in
let check_fexp (FE_aux (FE_Fexp (field, exp), (l, ()))) =
let (typq, rectyp_q, field_typ, _) = Env.get_accessor rectyp_id field env in
- let unifiers = try unify l env (tyvars_of_typ rectyp_q) rectyp_q typ with Unification_error (l, m) -> typ_error l ("Unification error: " ^ m) in
+ let unifiers = try unify l env (tyvars_of_typ rectyp_q) rectyp_q typ with Unification_error (l, m) -> typ_error env l ("Unification error: " ^ m) in
let field_typ' = subst_unifiers unifiers field_typ in
let checked_exp = crule check_exp env exp field_typ' in
FE_aux (FE_Fexp (field, checked_exp), (l, None))
@@ -2297,11 +2299,11 @@ let rec check_exp env (E_aux (exp_aux, (l, ())) as exp : unit exp) (Typ_aux (typ
let rectyp_id = match Env.expand_synonyms env typ with
| Typ_aux (Typ_id rectyp_id, _) | Typ_aux (Typ_app (rectyp_id, _), _) when Env.is_record rectyp_id env ->
rectyp_id
- | _ -> typ_error l ("The type " ^ string_of_typ typ ^ " is not a record")
+ | _ -> typ_error env l ("The type " ^ string_of_typ typ ^ " is not a record")
in
let check_fexp (FE_aux (FE_Fexp (field, exp), (l, ()))) =
let (typq, rectyp_q, field_typ, _) = Env.get_accessor rectyp_id field env in
- let unifiers = try unify l env (tyvars_of_typ rectyp_q) rectyp_q typ with Unification_error (l, m) -> typ_error l ("Unification error: " ^ m) in
+ let unifiers = try unify l env (tyvars_of_typ rectyp_q) rectyp_q typ with Unification_error (l, m) -> typ_error env l ("Unification error: " ^ m) in
let field_typ' = subst_unifiers unifiers field_typ in
let checked_exp = crule check_exp env exp field_typ' in
FE_aux (FE_Fexp (field, checked_exp), (l, None))
@@ -2326,11 +2328,11 @@ let rec check_exp env (E_aux (exp_aux, (l, ())) as exp : unit exp) (Typ_aux (typ
Env.wf_constraint env nc;
if prove __POS__ env nc
then annot_exp (E_lit (L_aux (L_unit, Parse_ast.Unknown))) unit_typ
- else typ_error l ("Cannot prove " ^ string_of_n_constraint nc)
+ else typ_error env l ("Cannot prove " ^ string_of_n_constraint nc)
| E_app (f, [E_aux (E_constraint nc, _)]), _ when string_of_id f = "_not_prove" ->
Env.wf_constraint env nc;
if prove __POS__ env nc
- then typ_error l ("Can prove " ^ string_of_n_constraint nc)
+ then typ_error env l ("Can prove " ^ string_of_n_constraint nc)
else annot_exp (E_lit (L_aux (L_unit, Parse_ast.Unknown))) unit_typ
| E_app (f, [E_aux (E_cast (typ, exp), _)]), _ when string_of_id f = "_check" ->
Env.wf_typ env typ;
@@ -2340,7 +2342,7 @@ let rec check_exp env (E_aux (exp_aux, (l, ())) as exp : unit exp) (Typ_aux (typ
Env.wf_typ env typ;
if (try (ignore (crule check_exp env exp typ); false) with Type_error _ -> true)
then annot_exp (E_lit (L_aux (L_unit, Parse_ast.Unknown))) unit_typ
- else typ_error l (Printf.sprintf "Expected _not_check(%s : %s) to fail" (string_of_exp exp) (string_of_typ typ))
+ else typ_error env l (Printf.sprintf "Expected _not_check(%s : %s) to fail" (string_of_exp exp) (string_of_typ typ))
(* All constructors and mappings are treated as having one argument
so Ctor(x, y) is checked as Ctor((x, y)) *)
| E_app (f, x :: y :: zs), _ when Env.is_union_constructor f env || Env.is_mapping f env ->
@@ -2351,22 +2353,22 @@ let rec check_exp env (E_aux (exp_aux, (l, ())) as exp : unit exp) (Typ_aux (typ
let backwards_id = mk_id (string_of_id mapping ^ "_backwards") in
typ_print (lazy("Trying forwards direction for mapping " ^ string_of_id mapping ^ "(" ^ string_of_list ", " string_of_exp xs ^ ")"));
begin try crule check_exp env (E_aux (E_app (forwards_id, xs), (l, ()))) typ with
- | Type_error (_, err1) ->
+ | Type_error (_, _, err1) ->
(* typ_print (lazy ("Error in forwards direction: " ^ string_of_type_error err1)); *)
typ_print (lazy ("Trying backwards direction for mapping " ^ string_of_id mapping ^ "(" ^ string_of_list ", " string_of_exp xs ^ ")"));
begin try crule check_exp env (E_aux (E_app (backwards_id, xs), (l, ()))) typ with
- | Type_error (_, err2) ->
+ | Type_error (_, _, err2) ->
(* typ_print (lazy ("Error in backwards direction: " ^ string_of_type_error err2)); *)
- typ_raise l (Err_no_overloading (mapping, [(forwards_id, err1); (backwards_id, err2)]))
+ typ_raise env l (Err_no_overloading (mapping, [(forwards_id, err1); (backwards_id, err2)]))
end
end
| E_app (f, xs), _ when List.length (Env.get_overloads f env) > 0 ->
let rec try_overload = function
- | (errs, []) -> typ_raise l (Err_no_overloading (f, errs))
+ | (errs, []) -> typ_raise env l (Err_no_overloading (f, errs))
| (errs, (f :: fs)) -> begin
typ_print (lazy ("Overload: " ^ string_of_id f ^ "(" ^ string_of_list ", " string_of_exp xs ^ ")"));
try crule check_exp env (E_aux (E_app (f, xs), (l, ()))) typ with
- | Type_error (_, err) ->
+ | Type_error (_, _, err) ->
typ_debug (lazy "Error");
try_overload (errs @ [(f, err)], fs)
end
@@ -2375,7 +2377,7 @@ let rec check_exp env (E_aux (exp_aux, (l, ())) as exp : unit exp) (Typ_aux (typ
| E_return exp, _ ->
let checked_exp = match Env.get_ret_typ env with
| Some ret_typ -> crule check_exp env exp ret_typ
- | None -> typ_error l "Cannot use return outside a function"
+ | None -> typ_error env l "Cannot use return outside a function"
in
annot_exp (E_return checked_exp) typ
| E_tuple exps, Typ_tup typs when List.length exps = List.length typs ->
@@ -2441,11 +2443,11 @@ let rec check_exp env (E_aux (exp_aux, (l, ())) as exp : unit exp) (Typ_aux (typ
let (len, ord, vtyp) = destruct_vec_typ l env typ in
let checked_items = List.map (fun i -> crule check_exp env i vtyp) vec in
if prove __POS__ env (nc_eq (nint (List.length vec)) (nexp_simp len)) then annot_exp (E_vector checked_items) typ
- else typ_error l "List length didn't match" (* FIXME: improve error message *)
+ else typ_error env l "List length didn't match" (* FIXME: improve error message *)
| E_lit (L_aux (L_undef, _) as lit), _ ->
if is_typ_monomorphic typ || Env.polymorphic_undefineds env
then annot_exp_effect (E_lit lit) typ (mk_effect [BE_undef])
- else typ_error l ("Type " ^ string_of_typ typ ^ " failed undefined monomorphism restriction")
+ else typ_error env l ("Type " ^ string_of_typ typ ^ " failed undefined monomorphism restriction")
| _, _ ->
let inferred_exp = irule infer_exp env exp in
type_coercion env inferred_exp typ
@@ -2554,14 +2556,14 @@ and type_coercion env (E_aux (_, (l, _)) as annotated_exp) typ =
| _ -> failwith "Cannot switch type for unannotated function"
in
let rec try_casts trigger errs = function
- | [] -> typ_raise l (Err_no_casts (strip_exp annotated_exp, typ_of annotated_exp, typ, trigger, errs))
+ | [] -> typ_raise env l (Err_no_casts (strip_exp annotated_exp, typ_of annotated_exp, typ, trigger, errs))
| (cast :: casts) -> begin
typ_print (lazy ("Casting with " ^ string_of_id cast ^ " expression " ^ string_of_exp annotated_exp ^ " to " ^ string_of_typ typ));
try
let checked_cast = crule check_exp (Env.no_casts env) (strip (E_app (cast, [annotated_exp]))) typ in
annot_exp (E_cast (typ, checked_cast)) typ
with
- | Type_error (_, err) -> try_casts trigger (err :: errs) casts
+ | Type_error (_, _, err) -> try_casts trigger (err :: errs) casts
end
in
begin
@@ -2569,10 +2571,10 @@ and type_coercion env (E_aux (_, (l, _)) as annotated_exp) typ =
typ_debug (lazy ("Performing type coercion: from " ^ string_of_typ (typ_of annotated_exp) ^ " to " ^ string_of_typ typ));
subtyp l env (typ_of annotated_exp) typ; switch_exp_typ annotated_exp
with
- | Type_error (_, trigger) when Env.allow_casts env ->
+ | Type_error (_, _, trigger) when Env.allow_casts env ->
let casts = filter_casts env (typ_of annotated_exp) typ (Env.get_casts env) in
try_casts trigger [] casts
- | Type_error (l, err) -> typ_raise l err
+ | Type_error (env, l, err) -> typ_raise env l err
end
(* type_coercion_unify env exp typ attempts to coerce exp to a type
@@ -2596,7 +2598,7 @@ and type_coercion_unify env goals (E_aux (_, (l, _)) as annotated_exp) typ =
let ityp, env = bind_existential l None (typ_of inferred_cast) env in
inferred_cast, unify l env goals typ ityp, env
with
- | Type_error (_, err) -> try_casts casts
+ | Type_error (_, _, err) -> try_casts casts
| Unification_error (_, err) -> try_casts casts
end
in
@@ -2613,7 +2615,7 @@ and type_coercion_unify env goals (E_aux (_, (l, _)) as annotated_exp) typ =
and bind_pat_no_guard env (P_aux (_,(l,_)) as pat) typ =
match bind_pat env pat typ with
- | _, _, _::_ -> typ_error l "Literal patterns not supported here"
+ | _, _, _::_ -> typ_error env l "Literal patterns not supported here"
| tpat, env, [] -> tpat, env
and bind_pat env (P_aux (pat_aux, (l, ())) as pat) (Typ_aux (typ_aux, _) as typ) =
@@ -2622,7 +2624,7 @@ and bind_pat env (P_aux (pat_aux, (l, ())) as pat) (Typ_aux (typ_aux, _) as typ)
let annot_pat pat typ' = P_aux (pat, (l, mk_expected_tannot env typ' no_effect (Some typ))) in
let switch_typ pat typ = match pat with
| P_aux (pat_aux, (l, Some tannot)) -> P_aux (pat_aux, (l, Some { tannot with typ = typ }))
- | _ -> typ_error l "Cannot switch type for unannotated pattern"
+ | _ -> typ_error env l "Cannot switch type for unannotated pattern"
in
let bind_tuple_pat (tpats, env, guards) pat typ =
let tpat, env, guards' = bind_pat env pat typ in tpat :: tpats, env, guards' @ guards
@@ -2640,7 +2642,7 @@ and bind_pat env (P_aux (pat_aux, (l, ())) as pat) (Typ_aux (typ_aux, _) as typ)
match Env.lookup_id v env with
| Local _ | Unbound -> annot_pat (P_id v) typ, Env.add_local v (Immutable, typ) env, []
| Register _ ->
- typ_error l ("Cannot shadow register in pattern " ^ string_of_pat pat)
+ typ_error env l ("Cannot shadow register in pattern " ^ string_of_pat pat)
| Enum enum -> subtyp l env enum typ; annot_pat (P_id v) typ, env, []
end
| P_var (pat, typ_pat) ->
@@ -2662,7 +2664,7 @@ and bind_pat env (P_aux (pat_aux, (l, ())) as pat) (Typ_aux (typ_aux, _) as typ)
let hd_pat, env, hd_guards = bind_pat env hd_pat ltyp in
let tl_pat, env, tl_guards = bind_pat env tl_pat typ in
annot_pat (P_cons (hd_pat, tl_pat)) typ, env, hd_guards @ tl_guards
- | _ -> typ_error l "Cannot match cons pattern against non-list type"
+ | _ -> typ_error env l "Cannot match cons pattern against non-list type"
end
| P_string_append pats ->
begin
@@ -2677,7 +2679,7 @@ and bind_pat env (P_aux (pat_aux, (l, ())) as pat) (Typ_aux (typ_aux, _) as typ)
in
let pats, env, guards = process_pats env pats in
annot_pat (P_string_append pats) typ, env, guards
- | _ -> typ_error l "Cannot match string-append pattern against non-string type"
+ | _ -> typ_error env l "Cannot match string-append pattern against non-string type"
end
| P_list pats ->
begin
@@ -2692,14 +2694,14 @@ and bind_pat env (P_aux (pat_aux, (l, ())) as pat) (Typ_aux (typ_aux, _) as typ)
in
let pats, env, guards = process_pats env pats in
annot_pat (P_list pats) typ, env, guards
- | _ -> typ_error l ("Cannot match list pattern " ^ string_of_pat pat ^ " against non-list type " ^ string_of_typ typ)
+ | _ -> typ_error env l ("Cannot match list pattern " ^ string_of_pat pat ^ " against non-list type " ^ string_of_typ typ)
end
| P_tup [] ->
begin
match Env.expand_synonyms env typ with
| Typ_aux (Typ_id typ_id, _) when string_of_id typ_id = "unit" ->
annot_pat (P_tup []) typ, env, []
- | _ -> typ_error l "Cannot match unit pattern against non-unit type"
+ | _ -> typ_error env l "Cannot match unit pattern against non-unit type"
end
| P_tup pats ->
begin
@@ -2707,11 +2709,11 @@ and bind_pat env (P_aux (pat_aux, (l, ())) as pat) (Typ_aux (typ_aux, _) as typ)
| Typ_aux (Typ_tup typs, _) ->
let tpats, env, guards =
try List.fold_left2 bind_tuple_pat ([], env, []) pats typs with
- | Invalid_argument _ -> typ_error l "Tuple pattern and tuple type have different length"
+ | Invalid_argument _ -> typ_error env l "Tuple pattern and tuple type have different length"
in
annot_pat (P_tup (List.rev tpats)) typ, env, guards
| _ ->
- typ_error l (Printf.sprintf "Cannot bind tuple pattern %s against non tuple type %s"
+ typ_error env l (Printf.sprintf "Cannot bind tuple pattern %s against non tuple type %s"
(string_of_pat pat) (string_of_typ typ))
end
| P_app (f, pats) when Env.is_union_constructor f env ->
@@ -2732,18 +2734,18 @@ and bind_pat env (P_aux (pat_aux, (l, ())) as pat) (Typ_aux (typ_aux, _) as typ)
let arg_typ' = subst_unifiers unifiers arg_typ in
let quants' = List.fold_left instantiate_quants quants (KBindings.bindings unifiers) in
if not (List.for_all (solve_quant env) quants') then
- typ_raise l (Err_unresolved_quants (f, quants', Env.get_locals env, Env.get_constraints env))
+ typ_raise env l (Err_unresolved_quants (f, quants', Env.get_locals env, Env.get_constraints env))
else ();
let ret_typ' = subst_unifiers unifiers ret_typ in
let tpats, env, guards =
try List.fold_left2 bind_tuple_pat ([], env, []) pats (untuple arg_typ') with
- | Invalid_argument _ -> typ_error l "Union constructor pattern arguments have incorrect length"
+ | Invalid_argument _ -> typ_error env l "Union constructor pattern arguments have incorrect length"
in
annot_pat (P_app (f, List.rev tpats)) typ, env, guards
with
- | Unification_error (l, m) -> typ_error l ("Unification error when pattern matching against union constructor: " ^ m)
+ | Unification_error (l, m) -> typ_error env l ("Unification error when pattern matching against union constructor: " ^ m)
end
- | _ -> typ_error l ("Mal-formed constructor " ^ string_of_id f ^ " with type " ^ string_of_typ ctor_typ)
+ | _ -> typ_error env l ("Mal-formed constructor " ^ string_of_id f ^ " with type " ^ string_of_typ ctor_typ)
end
| P_app (f, pats) when Env.is_mapping f env ->
@@ -2765,13 +2767,13 @@ and bind_pat env (P_aux (pat_aux, (l, ())) as pat) (Typ_aux (typ_aux, _) as typ)
let arg_typ' = subst_unifiers unifiers typ1 in
let quants' = List.fold_left instantiate_quants quants (KBindings.bindings unifiers) in
if (match quants' with [] -> false | _ -> true)
- then typ_error l ("Quantifiers " ^ string_of_list ", " string_of_quant_item quants' ^ " not resolved in pattern " ^ string_of_pat pat)
+ then typ_error env l ("Quantifiers " ^ string_of_list ", " string_of_quant_item quants' ^ " not resolved in pattern " ^ string_of_pat pat)
else ();
let ret_typ' = subst_unifiers unifiers typ2 in
let tpats, env, guards =
try List.fold_left2 bind_tuple_pat ([], env, []) pats (untuple arg_typ') with
- | Invalid_argument _ -> typ_error l "Mapping pattern arguments have incorrect length"
+ | Invalid_argument _ -> typ_error env l "Mapping pattern arguments have incorrect length"
in
annot_pat (P_app (f, List.rev tpats)) typ, env, guards
with
@@ -2783,22 +2785,22 @@ and bind_pat env (P_aux (pat_aux, (l, ())) as pat) (Typ_aux (typ_aux, _) as typ)
let arg_typ' = subst_unifiers unifiers typ2 in
let quants' = List.fold_left instantiate_quants quants (KBindings.bindings unifiers) in
if (match quants' with [] -> false | _ -> true)
- then typ_error l ("Quantifiers " ^ string_of_list ", " string_of_quant_item quants' ^ " not resolved in pattern " ^ string_of_pat pat)
+ then typ_error env l ("Quantifiers " ^ string_of_list ", " string_of_quant_item quants' ^ " not resolved in pattern " ^ string_of_pat pat)
else ();
let ret_typ' = subst_unifiers unifiers typ1 in
let tpats, env, guards =
try List.fold_left2 bind_tuple_pat ([], env, []) pats (untuple arg_typ') with
- | Invalid_argument _ -> typ_error l "Mapping pattern arguments have incorrect length"
+ | Invalid_argument _ -> typ_error env l "Mapping pattern arguments have incorrect length"
in
annot_pat (P_app (f, List.rev tpats)) typ, env, guards
with
- | Unification_error (l, m) -> typ_error l ("Unification error when pattern matching against mapping constructor: " ^ m)
+ | Unification_error (l, m) -> typ_error env l ("Unification error when pattern matching against mapping constructor: " ^ m)
end
- | _ -> typ_error l ("Mal-formed mapping " ^ string_of_id f)
+ | _ -> typ_error env l ("Mal-formed mapping " ^ string_of_id f)
end
| P_app (f, _) when (not (Env.is_union_constructor f env) && not (Env.is_mapping f env)) ->
- typ_error l (string_of_id f ^ " is not a union constructor or mapping in pattern " ^ string_of_pat pat)
+ typ_error env l (string_of_id f ^ " is not a union constructor or mapping in pattern " ^ string_of_pat pat)
| P_as (pat, id) ->
let (typed_pat, env, guards) = bind_pat env pat typ in
annot_pat (P_as (typed_pat, id)) (typ_of_pat typed_pat), Env.add_local id (Immutable, typ_of_pat typed_pat) env, guards
@@ -2832,9 +2834,9 @@ and infer_pat env (P_aux (pat_aux, (l, ())) as pat) =
begin
match Env.lookup_id v env with
| Local (Immutable, _) | Unbound ->
- typ_error l ("Cannot infer identifier in pattern " ^ string_of_pat pat ^ " - try adding a type annotation")
+ typ_error env l ("Cannot infer identifier in pattern " ^ string_of_pat pat ^ " - try adding a type annotation")
| Local (Mutable, _) | Register _ ->
- typ_error l ("Cannot shadow mutable local or register in switch statement pattern " ^ string_of_pat pat)
+ typ_error env l ("Cannot shadow mutable local or register in switch statement pattern " ^ string_of_pat pat)
| Enum enum -> annot_pat (P_id v) enum, env, []
end
| P_app (f, mpats) when Env.is_union_constructor f env ->
@@ -2843,7 +2845,7 @@ and infer_pat env (P_aux (pat_aux, (l, ())) as pat) =
match Env.expand_synonyms env ctor_typ with
| Typ_aux (Typ_fn (arg_typ, ret_typ, _), _) ->
bind_pat env pat ret_typ
- | _ -> typ_error l ("Mal-formed constructor " ^ string_of_id f)
+ | _ -> typ_error env l ("Mal-formed constructor " ^ string_of_id f)
end
| P_app (f, mpats) when Env.is_mapping f env ->
begin
@@ -2857,7 +2859,7 @@ and infer_pat env (P_aux (pat_aux, (l, ())) as pat) =
| Type_error _ ->
bind_pat env pat typ1
end
- | _ -> typ_error l ("Malformed mapping type " ^ string_of_id f)
+ | _ -> typ_error env l ("Malformed mapping type " ^ string_of_id f)
end
| P_typ (typ_annot, pat) ->
Env.wf_typ env typ_annot;
@@ -2905,7 +2907,7 @@ and infer_pat env (P_aux (pat_aux, (l, ())) as pat) =
annot_pat (P_as (typed_pat, id)) (typ_of_pat typed_pat),
Env.add_local id (Immutable, typ_of_pat typed_pat) env,
guards
- | _ -> typ_error l ("Couldn't infer type of pattern " ^ string_of_pat pat)
+ | _ -> typ_error env l ("Couldn't infer type of pattern " ^ string_of_pat pat)
and bind_typ_pat env (TP_aux (typ_pat_aux, l) as typ_pat) (Typ_aux (typ_aux, _) as typ) =
match typ_pat_aux, typ_aux with
@@ -2916,21 +2918,21 @@ and bind_typ_pat env (TP_aux (typ_pat_aux, l) as typ_pat) (Typ_aux (typ_aux, _)
| [nexp] ->
Env.add_constraint (nc_eq (nvar kid) nexp) (Env.add_typ_var l (mk_kopt K_int kid) env)
| [] ->
- typ_error l ("No numeric expressions in " ^ string_of_typ typ ^ " to bind " ^ string_of_kid kid ^ " to")
+ typ_error env l ("No numeric expressions in " ^ string_of_typ typ ^ " to bind " ^ string_of_kid kid ^ " to")
| nexps ->
- typ_error l ("Type " ^ string_of_typ typ ^ " has multiple numeric expressions. Cannot bind " ^ string_of_kid kid)
+ typ_error env l ("Type " ^ string_of_typ typ ^ " has multiple numeric expressions. Cannot bind " ^ string_of_kid kid)
end
| TP_app (f1, tpats), Typ_app (f2, typs) when Id.compare f1 f2 = 0 ->
List.fold_left2 bind_typ_pat_arg env tpats typs
- | _, _ -> typ_error l ("Couldn't bind type " ^ string_of_typ typ ^ " with " ^ string_of_typ_pat typ_pat)
+ | _, _ -> typ_error env l ("Couldn't bind type " ^ string_of_typ typ ^ " with " ^ string_of_typ_pat typ_pat)
and bind_typ_pat_arg env (TP_aux (typ_pat_aux, l) as typ_pat) (A_aux (typ_arg_aux, _) as typ_arg) =
match typ_pat_aux, typ_arg_aux with
| TP_wild, _ -> env
| TP_var kid, A_nexp nexp ->
Env.add_constraint (nc_eq (nvar kid) nexp) (Env.add_typ_var l (mk_kopt K_int kid) env)
| _, A_typ typ -> bind_typ_pat env typ_pat typ
- | _, A_order _ -> typ_error l "Cannot bind type pattern against order"
- | _, _ -> typ_error l ("Couldn't bind type argument " ^ string_of_typ_arg typ_arg ^ " with " ^ string_of_typ_pat typ_pat)
+ | _, A_order _ -> typ_error env l "Cannot bind type pattern against order"
+ | _, _ -> typ_error env l ("Couldn't bind type argument " ^ string_of_typ_arg typ_arg ^ " with " ^ string_of_typ_pat typ_pat)
and bind_assignment env (LEXP_aux (lexp_aux, _) as lexp) (E_aux (_, (l, ())) as exp) =
let annot_assign lexp exp = E_aux (E_assign (lexp, exp), (l, mk_tannot env (mk_typ (Typ_id (mk_id "unit"))) no_effect)) in
@@ -2949,14 +2951,14 @@ and bind_assignment env (LEXP_aux (lexp_aux, _) as lexp) (E_aux (_, (l, ())) as
begin match Env.lookup_id v env with
| Register (_, _, typ) -> typ, LEXP_id v, true
| Local (Mutable, typ) -> typ, LEXP_id v, false
- | _ -> typ_error l "l-expression field is not a register or a local mutable type"
+ | _ -> typ_error env l "l-expression field is not a register or a local mutable type"
end
| LEXP_vector (LEXP_aux (LEXP_id v, _), exp) ->
begin
(* Check: is this ok if the vector is immutable? *)
let is_immutable, vtyp, is_register = match Env.lookup_id v env with
- | Unbound -> typ_error l "Cannot assign to element of unbound vector"
- | Enum _ -> typ_error l "Cannot vector assign to enumeration element"
+ | Unbound -> typ_error env l "Cannot assign to element of unbound vector"
+ | Enum _ -> typ_error env l "Cannot vector assign to enumeration element"
| Local (Immutable, vtyp) -> true, vtyp, false
| Local (Mutable, vtyp) -> false, vtyp, false
| Register (_, _, vtyp) -> false, vtyp, true
@@ -2968,7 +2970,7 @@ and bind_assignment env (LEXP_aux (lexp_aux, _) as lexp) (E_aux (_, (l, ())) as
in
typ_of access, LEXP_vector (annot_lexp (LEXP_id v) vtyp, inferred_exp), is_register
end
- | _ -> typ_error l "Field l-expression must be either a vector or an identifier"
+ | _ -> typ_error env l "Field l-expression must be either a vector or an identifier"
in
let regtyp, inferred_flexp, is_register = infer_flexp flexp in
typ_debug (lazy ("REGTYP: " ^ string_of_typ regtyp ^ " / " ^ string_of_typ (Env.expand_synonyms env regtyp)));
@@ -2976,11 +2978,11 @@ and bind_assignment env (LEXP_aux (lexp_aux, _) as lexp) (E_aux (_, (l, ())) as
| Typ_aux (Typ_id rectyp_id, _) | Typ_aux (Typ_app (rectyp_id, _), _) when Env.is_record rectyp_id env ->
let eff = if is_register then mk_effect [BE_wreg] else no_effect in
let (typq, rectyp_q, field_typ, _) = Env.get_accessor rectyp_id field env in
- let unifiers = try unify l env (tyvars_of_typ rectyp_q) rectyp_q regtyp with Unification_error (l, m) -> typ_error l ("Unification error: " ^ m) in
+ let unifiers = try unify l env (tyvars_of_typ rectyp_q) rectyp_q regtyp with Unification_error (l, m) -> typ_error env l ("Unification error: " ^ m) in
let field_typ' = subst_unifiers unifiers field_typ in
let checked_exp = crule check_exp env exp field_typ' in
annot_assign (annot_lexp (LEXP_field (annot_lexp_effect inferred_flexp regtyp eff, field)) field_typ') checked_exp, env
- | _ -> typ_error l "Field l-expression has invalid type"
+ | _ -> typ_error env l "Field l-expression has invalid type"
end
| LEXP_memory (f, xs) ->
check_exp env (E_aux (E_app (f, xs @ [exp]), (l, ()))) unit_typ, env
@@ -3006,12 +3008,12 @@ and bind_assignment env (LEXP_aux (lexp_aux, _) as lexp) (E_aux (_, (l, ())) as
let tlexp, env' = bind_lexp env lexp (typ_of inferred_exp) in
annot_assign tlexp inferred_exp, env'
with
- | Type_error (l, err) ->
+ | Type_error (_, l, err) ->
try
let inferred_lexp = infer_lexp env lexp in
let checked_exp = crule check_exp env exp (lexp_typ_of inferred_lexp) in
annot_assign inferred_lexp checked_exp, env
- with Type_error (l, err') -> typ_raise l (Err_because (err', err))
+ with Type_error (env, l', err') -> typ_raise env l' (Err_because (err', l, err))
and bind_lexp env (LEXP_aux (lexp_aux, (l, ())) as lexp) typ =
typ_print (lazy ("Binding mutable " ^ string_of_lexp lexp ^ " to " ^ string_of_typ typ));
@@ -3021,7 +3023,7 @@ and bind_lexp env (LEXP_aux (lexp_aux, (l, ())) as lexp) typ =
| LEXP_cast (typ_annot, v) ->
begin match Env.lookup_id ~raw:true v env with
| Local (Immutable, _) | Enum _ ->
- typ_error l ("Cannot modify let-bound constant or enumeration constructor " ^ string_of_id v)
+ typ_error env l ("Cannot modify let-bound constant or enumeration constructor " ^ string_of_id v)
| Local (Mutable, vtyp) ->
subtyp l env typ typ_annot;
subtyp l env typ_annot vtyp;
@@ -3040,12 +3042,12 @@ and bind_lexp env (LEXP_aux (lexp_aux, (l, ())) as lexp) typ =
| Typ_aux (Typ_app (r, [A_aux (A_typ vtyp, _)]), _) when string_of_id r = "register" ->
subtyp l env typ vtyp; annot_lexp_effect (LEXP_deref inferred_exp) typ (mk_effect [BE_wreg]), env
| _ ->
- typ_error l (string_of_typ typ ^ " must be a register type in " ^ string_of_exp exp ^ ")")
+ typ_error env l (string_of_typ typ ^ " must be a register type in " ^ string_of_exp exp ^ ")")
end
| LEXP_id v ->
begin match Env.lookup_id ~raw:true v env with
| Local (Immutable, _) | Enum _ ->
- typ_error l ("Cannot modify let-bound constant or enumeration constructor " ^ string_of_id v)
+ typ_error env l ("Cannot modify let-bound constant or enumeration constructor " ^ string_of_id v)
| Local (Mutable, vtyp) -> subtyp l env typ vtyp; annot_lexp (LEXP_id v) typ, Env.remove_flow v env
| Register (_, weff, vtyp) -> subtyp l env typ vtyp; annot_lexp_effect (LEXP_id v) typ weff, env
| Unbound -> annot_lexp (LEXP_id v) typ, Env.add_local v (Mutable, typ) env
@@ -3061,10 +3063,10 @@ and bind_lexp env (LEXP_aux (lexp_aux, (l, ())) as lexp) typ =
in
let tlexps, env =
try List.fold_right2 bind_tuple_lexp lexps typs ([], env) with
- | Invalid_argument _ -> typ_error l "Tuple l-expression and tuple type have different length"
+ | Invalid_argument _ -> typ_error env l "Tuple l-expression and tuple type have different length"
in
annot_lexp (LEXP_tup tlexps) typ, env
- | _ -> typ_error l ("Cannot bind tuple l-expression against non tuple type " ^ string_of_typ typ)
+ | _ -> typ_error env l ("Cannot bind tuple l-expression against non tuple type " ^ string_of_typ typ)
end
| _ ->
let inferred_lexp = infer_lexp env lexp in
@@ -3081,9 +3083,9 @@ and infer_lexp env (LEXP_aux (lexp_aux, (l, ())) as lexp) =
(* Probably need to remove flows here *)
| Register (_, weff, typ) -> annot_lexp_effect (LEXP_id v) typ weff
| Local (Immutable, _) | Enum _ ->
- typ_error l ("Cannot modify let-bound constant or enumeration constructor " ^ string_of_id v)
+ typ_error env l ("Cannot modify let-bound constant or enumeration constructor " ^ string_of_id v)
| Unbound ->
- typ_error l ("Cannot create a new identifier in this l-expression " ^ string_of_lexp lexp)
+ typ_error env l ("Cannot create a new identifier in this l-expression " ^ string_of_lexp lexp)
end
| LEXP_vector_range (v_lexp, exp1, exp2) ->
begin
@@ -3103,9 +3105,9 @@ and infer_lexp env (LEXP_aux (lexp_aux, (l, ())) as lexp) =
| Ord_aux (Ord_dec, _) when !opt_no_lexp_bounds_check || prove __POS__ env (nc_gteq nexp1 nexp2) ->
let len = nexp_simp (nsum (nminus nexp1 nexp2) (nint 1)) in
annot_lexp (LEXP_vector_range (inferred_v_lexp, inferred_exp1, inferred_exp2)) (vector_typ len ord elem_typ)
- | _ -> typ_error l ("Could not infer length of vector slice assignment " ^ string_of_lexp lexp)
+ | _ -> typ_error env l ("Could not infer length of vector slice assignment " ^ string_of_lexp lexp)
end
- | _ -> typ_error l "Cannot assign slice of non vector type"
+ | _ -> typ_error env l "Cannot assign slice of non vector type"
end
| LEXP_vector (v_lexp, exp) ->
begin
@@ -3119,10 +3121,10 @@ and infer_lexp env (LEXP_aux (lexp_aux, (l, ())) as lexp) =
if !opt_no_lexp_bounds_check || prove __POS__ env (nc_and (nc_lteq (nint 0) nexp) (nc_lteq nexp (nexp_simp (nminus len (nint 1))))) then
annot_lexp (LEXP_vector (inferred_v_lexp, inferred_exp)) elem_typ
else
- typ_error l ("Vector assignment not provably in bounds " ^ string_of_lexp lexp)
- | _ -> typ_error l "Cannot assign vector element of non vector type"
+ typ_error env l ("Vector assignment not provably in bounds " ^ string_of_lexp lexp)
+ | _ -> typ_error env l "Cannot assign vector element of non vector type"
end
- | LEXP_vector_concat [] -> typ_error l "Cannot have empty vector concatenation l-expression"
+ | LEXP_vector_concat [] -> typ_error env l "Cannot have empty vector concatenation l-expression"
| LEXP_vector_concat (v_lexp :: v_lexps) ->
begin
let sum_lengths first_ord first_elem_typ acc (Typ_aux (v_typ_aux, _) as v_typ) =
@@ -3131,7 +3133,7 @@ and infer_lexp env (LEXP_aux (lexp_aux, (l, ())) as lexp) =
when Id.compare id (mk_id "vector") = 0 && ord_identical ord first_ord ->
typ_equality l env elem_typ first_elem_typ;
nsum acc len
- | _ -> typ_error l "Vector concatentation l-expression must only contain vector types of the same order"
+ | _ -> typ_error env l "Vector concatentation l-expression must only contain vector types of the same order"
in
let inferred_v_lexp = infer_lexp env v_lexp in
let inferred_v_lexps = List.map (infer_lexp env) v_lexps in
@@ -3142,21 +3144,21 @@ and infer_lexp env (LEXP_aux (lexp_aux, (l, ())) as lexp) =
when Id.compare id (mk_id "vector") = 0 ->
let len = List.fold_left (sum_lengths ord elem_typ) len v_typs in
annot_lexp (LEXP_vector_concat (inferred_v_lexp :: inferred_v_lexps)) (vector_typ (nexp_simp len) ord elem_typ)
- | _ -> typ_error l ("Vector concatentation l-expression must only contain vector types, found " ^ string_of_typ v_typ)
+ | _ -> typ_error env l ("Vector concatentation l-expression must only contain vector types, found " ^ string_of_typ v_typ)
end
| LEXP_field (LEXP_aux (LEXP_id v, _), fid) ->
(* FIXME: will only work for ASL *)
let rec_id, weff =
match Env.lookup_id v env with
| Register (_, weff, Typ_aux (Typ_id rec_id, _)) -> rec_id, weff
- | _ -> typ_error l (string_of_lexp lexp ^ " must be a record register here")
+ | _ -> typ_error env l (string_of_lexp lexp ^ " must be a record register here")
in
let typq, _, ret_typ, _ = Env.get_accessor rec_id fid env in
annot_lexp_effect (LEXP_field (annot_lexp (LEXP_id v) (mk_id_typ rec_id), fid)) ret_typ weff
| LEXP_tup lexps ->
let inferred_lexps = List.map (infer_lexp env) lexps in
annot_lexp (LEXP_tup inferred_lexps) (tuple_typ (List.map lexp_typ_of inferred_lexps))
- | _ -> typ_error l ("Could not infer the type of " ^ string_of_lexp lexp)
+ | _ -> typ_error env l ("Could not infer the type of " ^ string_of_lexp lexp)
and infer_exp env (E_aux (exp_aux, (l, ())) as exp) =
let annot_exp_effect exp typ eff = E_aux (exp, (l, mk_tannot env typ eff)) in
@@ -3173,7 +3175,7 @@ and infer_exp env (E_aux (exp_aux, (l, ())) as exp) =
match Env.lookup_id v env with
| Local (_, typ) | Enum typ -> annot_exp (E_id v) typ
| Register (reff, _, typ) -> annot_exp_effect (E_id v) typ reff
- | Unbound -> typ_error l ("Identifier " ^ string_of_id v ^ " is unbound")
+ | Unbound -> typ_error env l ("Identifier " ^ string_of_id v ^ " is unbound")
end
| E_lit lit -> annot_exp (E_lit lit) (infer_lit env lit)
| E_sizeof nexp ->
@@ -3201,7 +3203,7 @@ and infer_exp env (E_aux (exp_aux, (l, ())) as exp) =
| E_aux (E_app (field, [inferred_exp]) ,_) -> annot_exp (E_field (inferred_exp, field)) (typ_of inferred_acc)
| _ -> assert false (* Unreachable *)
end
- | _ -> typ_error l ("Field expression " ^ string_of_exp exp ^ " :: " ^ string_of_typ (typ_of inferred_exp) ^ " is not valid")
+ | _ -> typ_error env l ("Field expression " ^ string_of_exp exp ^ " :: " ^ string_of_typ (typ_of inferred_exp) ^ " is not valid")
end
| E_tuple exps ->
let inferred_exps = List.map (irule infer_exp env) exps in
@@ -3214,11 +3216,11 @@ and infer_exp env (E_aux (exp_aux, (l, ())) as exp) =
let rectyp_id = match Env.expand_synonyms env typ with
| Typ_aux (Typ_id rectyp_id, _) | Typ_aux (Typ_app (rectyp_id, _), _) when Env.is_record rectyp_id env ->
rectyp_id
- | _ -> typ_error l ("The type " ^ string_of_typ typ ^ " is not a record")
+ | _ -> typ_error env l ("The type " ^ string_of_typ typ ^ " is not a record")
in
let check_fexp (FE_aux (FE_Fexp (field, exp), (l, ()))) =
let (typq, rectyp_q, field_typ, _) = Env.get_accessor rectyp_id field env in
- let unifiers = try unify l env (tyvars_of_typ rectyp_q) rectyp_q typ with Unification_error (l, m) -> typ_error l ("Unification error: " ^ m) in
+ let unifiers = try unify l env (tyvars_of_typ rectyp_q) rectyp_q typ with Unification_error (l, m) -> typ_error env l ("Unification error: " ^ m) in
let field_typ' = subst_unifiers unifiers field_typ in
let inferred_exp = crule check_exp env exp field_typ' in
FE_aux (FE_Fexp (field, inferred_exp), (l, None))
@@ -3237,22 +3239,22 @@ and infer_exp env (E_aux (exp_aux, (l, ())) as exp) =
let backwards_id = mk_id (string_of_id mapping ^ "_backwards") in
typ_print (lazy ("Trying forwards direction for mapping " ^ string_of_id mapping ^ "(" ^ string_of_list ", " string_of_exp xs ^ ")"));
begin try irule infer_exp env (E_aux (E_app (forwards_id, xs), (l, ()))) with
- | Type_error (_, err1) ->
+ | Type_error (_, _, err1) ->
(* typ_print (lazy ("Error in forwards direction: " ^ string_of_type_error err1)); *)
typ_print (lazy ("Trying backwards direction for mapping " ^ string_of_id mapping ^ "(" ^ string_of_list ", " string_of_exp xs ^ ")"));
begin try irule infer_exp env (E_aux (E_app (backwards_id, xs), (l, ()))) with
- | Type_error (_, err2) ->
+ | Type_error (env, _, err2) ->
(* typ_print (lazy ("Error in backwards direction: " ^ string_of_type_error err2)); *)
- typ_raise l (Err_no_overloading (mapping, [(forwards_id, err1); (backwards_id, err2)]))
+ typ_raise env l (Err_no_overloading (mapping, [(forwards_id, err1); (backwards_id, err2)]))
end
end
| E_app (f, xs) when List.length (Env.get_overloads f env) > 0 ->
let rec try_overload = function
- | (errs, []) -> typ_raise l (Err_no_overloading (f, errs))
+ | (errs, []) -> typ_raise env l (Err_no_overloading (f, errs))
| (errs, (f :: fs)) -> begin
typ_print (lazy ("Overload: " ^ string_of_id f ^ "(" ^ string_of_list ", " string_of_exp xs ^ ")"));
try irule infer_exp env (E_aux (E_app (f, xs), (l, ()))) with
- | Type_error (_, err) ->
+ | Type_error (_, _, err) ->
typ_debug (lazy "Error");
try_overload (errs @ [(f, err)], fs)
end
@@ -3268,7 +3270,7 @@ and infer_exp env (E_aux (exp_aux, (l, ())) as exp) =
let f, t, is_dec = match ord with
| Ord_aux (Ord_inc, _) -> f, t, false
| Ord_aux (Ord_dec, _) -> t, f, true (* reverse direction to typechecking downto as upto loop *)
- | Ord_aux (Ord_var _, _) -> typ_error l "Cannot check a loop with variable direction!" (* This should never happen *)
+ | Ord_aux (Ord_var _, _) -> typ_error env l "Cannot check a loop with variable direction!" (* This should never happen *)
in
let inferred_f = irule infer_exp env f in
let inferred_t = irule infer_exp env t in
@@ -3284,7 +3286,7 @@ and infer_exp env (E_aux (exp_aux, (l, ())) as exp) =
if not is_dec (* undo reverse direction in annotated ast for downto loop *)
then annot_exp (E_for (v, inferred_f, inferred_t, checked_step, ord, checked_body)) unit_typ
else annot_exp (E_for (v, inferred_t, inferred_f, checked_step, ord, checked_body)) unit_typ
- | _, _ -> typ_error l "Ranges in foreach overlap"
+ | _, _ -> typ_error env l "Ranges in foreach overlap"
end
| E_if (cond, then_branch, else_branch) ->
let cond' = crule check_exp env cond (mk_typ (Typ_id (mk_id "bool"))) in
@@ -3299,7 +3301,7 @@ and infer_exp env (E_aux (exp_aux, (l, ())) as exp) =
let else_sn = to_simple_numeric l kids nc else_nexp in
let typ = typ_of_simple_numeric (union_simple_numeric then_sn else_sn) in
annot_exp (E_if (cond', then_branch', else_branch')) typ
- | None -> typ_error l ("Could not infer type of " ^ string_of_exp else_branch)
+ | None -> typ_error env l ("Could not infer type of " ^ string_of_exp else_branch)
end
| None ->
begin match typ_of then_branch' with
@@ -3317,7 +3319,7 @@ and infer_exp env (E_aux (exp_aux, (l, ())) as exp) =
| E_vector_append (v1, E_aux (E_vector [], _)) -> infer_exp env v1
| E_vector_append (v1, v2) -> infer_exp env (E_aux (E_app (mk_id "append", [v1; v2]), (l, ())))
| E_vector_subrange (v, n, m) -> infer_exp env (E_aux (E_app (mk_id "vector_subrange", [v; n; m]), (l, ())))
- | E_vector [] -> typ_error l "Cannot infer type of empty vector"
+ | E_vector [] -> typ_error env l "Cannot infer type of empty vector"
| E_vector ((item :: items) as vec) ->
let inferred_item = irule infer_exp env item in
let checked_items = List.map (fun i -> crule check_exp env i (typ_of inferred_item)) items in
@@ -3369,7 +3371,7 @@ and infer_exp env (E_aux (exp_aux, (l, ())) as exp) =
| E_ref id when Env.is_register id env ->
let _, _, typ = Env.get_register id env in
annot_exp (E_ref id) (register_typ typ)
- | _ -> typ_error l ("Cannot infer type of: " ^ string_of_exp exp)
+ | _ -> typ_error env l ("Cannot infer type of: " ^ string_of_exp exp)
and infer_funapp l env f xs ret_ctx_typ = infer_funapp' l env f (Env.get_val_spec f env) xs ret_ctx_typ
@@ -3412,7 +3414,7 @@ and infer_funapp' l env f (typq, f_typ) xs expected_ret_typ =
let quants, typ_args, typ_ret, eff =
match Env.expand_synonyms env f_typ with
| Typ_aux (Typ_fn (typ_args, typ_ret, eff), _) -> ref (quant_items typq), typ_args, ref typ_ret, eff
- | _ -> typ_error l (string_of_typ f_typ ^ " is not a function type")
+ | _ -> typ_error env l (string_of_typ f_typ ^ " is not a function type")
in
let unifiers = instantiate_simple_equations !quants in
@@ -3426,7 +3428,7 @@ and infer_funapp' l env f (typq, f_typ) xs expected_ret_typ =
typ_debug (lazy ("Quantifiers " ^ Util.string_of_list ", " string_of_quant_item !quants));
if not (List.length typ_args = List.length xs) then
- typ_error l (Printf.sprintf "Function %s applied to %d args, expected %d" (string_of_id f) (List.length xs) (List.length typ_args))
+ typ_error env l (Printf.sprintf "Function %s applied to %d args, expected %d" (string_of_id f) (List.length xs) (List.length typ_args))
else ();
let instantiate_quant (v, arg) (QI_aux (aux, l) as qi) =
@@ -3464,7 +3466,7 @@ and infer_funapp' l env f (typq, f_typ) xs expected_ret_typ =
let inferred_arg = irule infer_exp env arg in
let inferred_arg, unifiers, env =
try type_coercion_unify env goals inferred_arg typ with
- | Unification_error (l, m) -> typ_error l m
+ | Unification_error (l, m) -> typ_error env l m
in
record_unifiers unifiers;
let unifiers = KBindings.bindings unifiers in
@@ -3488,7 +3490,7 @@ and infer_funapp' l env f (typq, f_typ) xs expected_ret_typ =
let xs = List.rev xs in
if not (List.for_all (solve_quant env) !quants) then
- typ_raise l (Err_unresolved_quants (f, !quants, Env.get_locals env, Env.get_constraints env))
+ typ_raise env l (Err_unresolved_quants (f, !quants, Env.get_locals env, Env.get_constraints env))
else ();
let ty_vars = KBindings.bindings (Env.get_typ_vars env) |> List.map (fun (v, k) -> mk_kopt k v) in
@@ -3516,7 +3518,7 @@ and bind_mpat allow_unknown other_env env (MP_aux (mpat_aux, (l, ())) as mpat) (
let annot_mpat mpat typ' = MP_aux (mpat, (l, mk_expected_tannot env typ' no_effect (Some typ))) in
let switch_typ mpat typ = match mpat with
| MP_aux (pat_aux, (l, Some tannot)) -> MP_aux (pat_aux, (l, Some { tannot with typ = typ }))
- | _ -> typ_error l "Cannot switch type for unannotated mapping-pattern"
+ | _ -> typ_error env l "Cannot switch type for unannotated mapping-pattern"
in
let bind_tuple_mpat (tpats, env, guards) mpat typ =
let tpat, env, guards' = bind_mpat allow_unknown other_env env mpat typ in tpat :: tpats, env, guards' @ guards
@@ -3534,7 +3536,7 @@ and bind_mpat allow_unknown other_env env (MP_aux (mpat_aux, (l, ())) as mpat) (
match Env.lookup_id v env with
| Local (Immutable, _) | Unbound -> annot_mpat (MP_id v) typ, Env.add_local v (Immutable, typ) env, []
| Local (Mutable, _) | Register _ ->
- typ_error l ("Cannot shadow mutable local or register in switch statement mapping-pattern " ^ string_of_mpat mpat)
+ typ_error env l ("Cannot shadow mutable local or register in switch statement mapping-pattern " ^ string_of_mpat mpat)
| Enum enum -> subtyp l env enum typ; annot_mpat (MP_id v) typ, env, []
end
| MP_cons (hd_mpat, tl_mpat) ->
@@ -3544,7 +3546,7 @@ and bind_mpat allow_unknown other_env env (MP_aux (mpat_aux, (l, ())) as mpat) (
let hd_mpat, env, hd_guards = bind_mpat allow_unknown other_env env hd_mpat ltyp in
let tl_mpat, env, tl_guards = bind_mpat allow_unknown other_env env tl_mpat typ in
annot_mpat (MP_cons (hd_mpat, tl_mpat)) typ, env, hd_guards @ tl_guards
- | _ -> typ_error l "Cannot match cons mapping-pattern against non-list type"
+ | _ -> typ_error env l "Cannot match cons mapping-pattern against non-list type"
end
| MP_string_append mpats ->
begin
@@ -3559,7 +3561,7 @@ and bind_mpat allow_unknown other_env env (MP_aux (mpat_aux, (l, ())) as mpat) (
in
let pats, env, guards = process_mpats env mpats in
annot_mpat (MP_string_append pats) typ, env, guards
- | _ -> typ_error l "Cannot match string-append pattern against non-string type"
+ | _ -> typ_error env l "Cannot match string-append pattern against non-string type"
end
| MP_list mpats ->
begin
@@ -3574,14 +3576,14 @@ and bind_mpat allow_unknown other_env env (MP_aux (mpat_aux, (l, ())) as mpat) (
in
let mpats, env, guards = process_mpats env mpats in
annot_mpat (MP_list mpats) typ, env, guards
- | _ -> typ_error l ("Cannot match list mapping-pattern " ^ string_of_mpat mpat ^ " against non-list type " ^ string_of_typ typ)
+ | _ -> typ_error env l ("Cannot match list mapping-pattern " ^ string_of_mpat mpat ^ " against non-list type " ^ string_of_typ typ)
end
| MP_tup [] ->
begin
match Env.expand_synonyms env typ with
| Typ_aux (Typ_id typ_id, _) when string_of_id typ_id = "unit" ->
annot_mpat (MP_tup []) typ, env, []
- | _ -> typ_error l "Cannot match unit mapping-pattern against non-unit type"
+ | _ -> typ_error env l "Cannot match unit mapping-pattern against non-unit type"
end
| MP_tup mpats ->
begin
@@ -3589,10 +3591,10 @@ and bind_mpat allow_unknown other_env env (MP_aux (mpat_aux, (l, ())) as mpat) (
| Typ_aux (Typ_tup typs, _) ->
let tpats, env, guards =
try List.fold_left2 bind_tuple_mpat ([], env, []) mpats typs with
- | Invalid_argument _ -> typ_error l "Tuple mapping-pattern and tuple type have different length"
+ | Invalid_argument _ -> typ_error env l "Tuple mapping-pattern and tuple type have different length"
in
annot_mpat (MP_tup (List.rev tpats)) typ, env, guards
- | _ -> typ_error l "Cannot bind tuple mapping-pattern against non tuple type"
+ | _ -> typ_error env l "Cannot bind tuple mapping-pattern against non tuple type"
end
| MP_app (f, mpats) when Env.is_union_constructor f env ->
begin
@@ -3611,18 +3613,18 @@ and bind_mpat allow_unknown other_env env (MP_aux (mpat_aux, (l, ())) as mpat) (
let arg_typ' = subst_unifiers unifiers arg_typ in
let quants' = List.fold_left instantiate_quants quants (KBindings.bindings unifiers) in
if (match quants' with [] -> false | _ -> true)
- then typ_error l ("Quantifiers " ^ string_of_list ", " string_of_quant_item quants' ^ " not resolved in mapping-pattern " ^ string_of_mpat mpat)
+ then typ_error env l ("Quantifiers " ^ string_of_list ", " string_of_quant_item quants' ^ " not resolved in mapping-pattern " ^ string_of_mpat mpat)
else ();
let ret_typ' = subst_unifiers unifiers ret_typ in
let tpats, env, guards =
try List.fold_left2 bind_tuple_mpat ([], env, []) mpats (untuple arg_typ') with
- | Invalid_argument _ -> typ_error l "Union constructor mapping-pattern arguments have incorrect length"
+ | Invalid_argument _ -> typ_error env l "Union constructor mapping-pattern arguments have incorrect length"
in
annot_mpat (MP_app (f, List.rev tpats)) typ, env, guards
with
- | Unification_error (l, m) -> typ_error l ("Unification error when mapping-pattern matching against union constructor: " ^ m)
+ | Unification_error (l, m) -> typ_error env l ("Unification error when mapping-pattern matching against union constructor: " ^ m)
end
- | _ -> typ_error l ("Mal-formed constructor " ^ string_of_id f ^ " with type " ^ string_of_typ ctor_typ)
+ | _ -> typ_error env l ("Mal-formed constructor " ^ string_of_id f ^ " with type " ^ string_of_typ ctor_typ)
end
| MP_app (other, mpats) when Env.is_mapping other env ->
begin
@@ -3641,12 +3643,12 @@ and bind_mpat allow_unknown other_env env (MP_aux (mpat_aux, (l, ())) as mpat) (
let arg_typ' = subst_unifiers unifiers typ1 in
let quants' = List.fold_left instantiate_quants quants (KBindings.bindings unifiers) in
if (match quants' with [] -> false | _ -> true)
- then typ_error l ("Quantifiers " ^ string_of_list ", " string_of_quant_item quants' ^ " not resolved in mapping-pattern " ^ string_of_mpat mpat)
+ then typ_error env l ("Quantifiers " ^ string_of_list ", " string_of_quant_item quants' ^ " not resolved in mapping-pattern " ^ string_of_mpat mpat)
else ();
let ret_typ' = subst_unifiers unifiers typ2 in
let tpats, env, guards =
try List.fold_left2 bind_tuple_mpat ([], env, []) mpats (untuple arg_typ') with
- | Invalid_argument _ -> typ_error l "Mapping pattern arguments have incorrect length"
+ | Invalid_argument _ -> typ_error env l "Mapping pattern arguments have incorrect length"
in
annot_mpat (MP_app (other, List.rev tpats)) typ, env, guards
with
@@ -3658,22 +3660,22 @@ and bind_mpat allow_unknown other_env env (MP_aux (mpat_aux, (l, ())) as mpat) (
let arg_typ' = subst_unifiers unifiers typ2 in
let quants' = List.fold_left instantiate_quants quants (KBindings.bindings unifiers) in
if (match quants' with [] -> false | _ -> true)
- then typ_error l ("Quantifiers " ^ string_of_list ", " string_of_quant_item quants' ^ " not resolved in mapping-pattern " ^ string_of_mpat mpat)
+ then typ_error env l ("Quantifiers " ^ string_of_list ", " string_of_quant_item quants' ^ " not resolved in mapping-pattern " ^ string_of_mpat mpat)
else ();
let ret_typ' = subst_unifiers unifiers typ1 in
let tpats, env, guards =
try List.fold_left2 bind_tuple_mpat ([], env, []) mpats (untuple arg_typ') with
- | Invalid_argument _ -> typ_error l "Mapping pattern arguments have incorrect length"
+ | Invalid_argument _ -> typ_error env l "Mapping pattern arguments have incorrect length"
in
annot_mpat (MP_app (other, List.rev tpats)) typ, env, guards
with
- | Unification_error (l, m) -> typ_error l ("Unification error when pattern matching against mapping constructor: " ^ m)
+ | Unification_error (l, m) -> typ_error env l ("Unification error when pattern matching against mapping constructor: " ^ m)
end
| Typ_aux (typ, _) ->
- typ_error l ("unifying mapping type, expanded synonyms to non-mapping type??")
+ typ_error env l ("unifying mapping type, expanded synonyms to non-mapping type??")
end
| MP_app (f, _) when not (Env.is_union_constructor f env || Env.is_mapping f env) ->
- typ_error l (string_of_id f ^ " is not a union constructor or mapping in mapping-pattern " ^ string_of_mpat mpat)
+ typ_error env l (string_of_id f ^ " is not a union constructor or mapping in mapping-pattern " ^ string_of_mpat mpat)
| MP_as (mpat, id) ->
let (typed_mpat, env, guards) = bind_mpat allow_unknown other_env env mpat typ in
(annot_mpat (MP_as (typed_mpat, id)) (typ_of_mpat typed_mpat),
@@ -3713,11 +3715,11 @@ and infer_mpat allow_unknown other_env env (MP_aux (mpat_aux, (l, ())) as mpat)
| Local (Immutable, typ) -> bind_mpat allow_unknown other_env env (mk_mpat (MP_typ (mk_mpat (MP_id v), typ))) typ
| Unbound ->
if allow_unknown then annot_mpat (MP_id v) unknown_typ, env, [] else
- typ_error l ("Cannot infer identifier in mapping-pattern " ^ string_of_mpat mpat ^ " - try adding a type annotation")
+ typ_error env l ("Cannot infer identifier in mapping-pattern " ^ string_of_mpat mpat ^ " - try adding a type annotation")
| _ -> assert false
end
| Local (Mutable, _) | Register _ ->
- typ_error l ("Cannot shadow mutable local or register in mapping-pattern " ^ string_of_mpat mpat)
+ typ_error env l ("Cannot shadow mutable local or register in mapping-pattern " ^ string_of_mpat mpat)
| Enum enum -> annot_mpat (MP_id v) enum, env, []
end
| MP_app (f, mpats) when Env.is_union_constructor f env ->
@@ -3726,7 +3728,7 @@ and infer_mpat allow_unknown other_env env (MP_aux (mpat_aux, (l, ())) as mpat)
match Env.expand_synonyms env ctor_typ with
| Typ_aux (Typ_fn (arg_typ, ret_typ, _), _) ->
bind_mpat allow_unknown other_env env mpat ret_typ
- | _ -> typ_error l ("Mal-formed constructor " ^ string_of_id f)
+ | _ -> typ_error env l ("Mal-formed constructor " ^ string_of_id f)
end
| MP_app (f, mpats) when Env.is_mapping f env ->
begin
@@ -3740,7 +3742,7 @@ and infer_mpat allow_unknown other_env env (MP_aux (mpat_aux, (l, ())) as mpat)
| Type_error _ ->
bind_mpat allow_unknown other_env env mpat typ1
end
- | _ -> typ_error l ("Malformed mapping type " ^ string_of_id f)
+ | _ -> typ_error env l ("Malformed mapping type " ^ string_of_id f)
end
| MP_lit lit ->
annot_mpat (MP_lit lit) (infer_lit env lit), env, []
@@ -3793,7 +3795,7 @@ and infer_mpat allow_unknown other_env env (MP_aux (mpat_aux, (l, ())) as mpat)
guards)
| _ ->
- typ_error l ("Couldn't infer type of mapping-pattern " ^ string_of_mpat mpat)
+ typ_error env l ("Couldn't infer type of mapping-pattern " ^ string_of_mpat mpat)
(**************************************************************************)
(* 5. Effect system *)
@@ -3967,8 +3969,8 @@ and propagate_exp_effect_aux = function
| E_internal_return exp ->
let p_exp = propagate_exp_effect exp in
E_internal_return p_exp, effect_of p_exp
- | exp_aux -> typ_error Parse_ast.Unknown ("Unimplemented: Cannot propagate effect in expression "
- ^ string_of_exp (E_aux (exp_aux, (Parse_ast.Unknown, None))))
+ | exp_aux -> typ_error Env.empty Parse_ast.Unknown ("Unimplemented: Cannot propagate effect in expression "
+ ^ string_of_exp (E_aux (exp_aux, (Parse_ast.Unknown, None))))
and propagate_fexp_effect (FE_aux (FE_Fexp (id, exp), (l, _))) =
let p_exp = propagate_exp_effect exp in
@@ -4070,7 +4072,7 @@ and propagate_pat_effect_aux = function
| P_vector pats ->
let p_pats = List.map propagate_pat_effect pats in
P_vector p_pats, collect_effects_pat p_pats
- | _ -> typ_error Parse_ast.Unknown "Unimplemented: Cannot propagate effect in pat"
+ | _ -> raise (Reporting.err_unreachable Parse_ast.Unknown __POS__ "Unimplemented: Cannot propagate effect in pat")
and propagate_mpat_effect (MP_aux (mpat, annot)) =
let p_mpat, eff = propagate_mpat_effect_aux mpat in
@@ -4106,7 +4108,7 @@ and propagate_mpat_effect_aux = function
| MP_as (mpat, id) ->
let p_mpat = propagate_mpat_effect mpat in
MP_as (p_mpat, id), effect_of_mpat mpat
- | _ -> typ_error Parse_ast.Unknown "Unimplemented: Cannot propagate effect in mpat"
+ | _ -> raise (Reporting.err_unreachable Parse_ast.Unknown __POS__ "Unimplemented: Cannot propagate effect in mpat")
and propagate_letbind_effect (LB_aux (lb, (l, annot))) =
let p_lb, eff = propagate_letbind_effect_aux lb in
@@ -4166,14 +4168,14 @@ let check_letdef orig_env (LB_aux (letbind, (l, _))) =
if (BESet.is_empty (effect_set (effect_of checked_bind)) || !opt_no_effects)
then
[DEF_val (LB_aux (LB_val (tpat, checked_bind), (l, None)))], env
- else typ_error l ("Top-level definition with effects " ^ string_of_effect (effect_of checked_bind))
+ else typ_error env l ("Top-level definition with effects " ^ string_of_effect (effect_of checked_bind))
| LB_val (pat, bind) ->
let inferred_bind = propagate_exp_effect (irule infer_exp orig_env (strip_exp bind)) in
let tpat, env = bind_pat_no_guard orig_env (strip_pat pat) (typ_of inferred_bind) in
if (BESet.is_empty (effect_set (effect_of inferred_bind)) || !opt_no_effects)
then
[DEF_val (LB_aux (LB_val (tpat, inferred_bind), (l, None)))], env
- else typ_error l ("Top-level definition with effects " ^ string_of_effect (effect_of inferred_bind))
+ else typ_error env l ("Top-level definition with effects " ^ string_of_effect (effect_of inferred_bind))
end
let check_funcl env (FCL_aux (FCL_Funcl (id, pexp), (l, _))) typ =
@@ -4204,7 +4206,7 @@ let check_funcl env (FCL_aux (FCL_Funcl (id, pexp), (l, _))) typ =
in
FCL_aux (FCL_Funcl (id, typed_pexp), (l, mk_expected_tannot env typ prop_eff (Some typ)))
end
- | _ -> typ_error l ("Function clause must have function type: " ^ string_of_typ typ ^ " is not a function type")
+ | _ -> typ_error env l ("Function clause must have function type: " ^ string_of_typ typ ^ " is not a function type")
let check_mapcl : 'a. Env.t -> 'a mapcl -> typ -> tannot mapcl =
@@ -4240,7 +4242,7 @@ let check_mapcl : 'a. Env.t -> 'a mapcl -> typ -> tannot mapcl =
MCL_aux (MCL_backwards (typed_mpexp, typed_exp), (l, mk_expected_tannot env typ prop_effs (Some typ)))
end
end
- | _ -> typ_error l ("Mapping clause must have mapping type: " ^ string_of_typ typ ^ " is not a mapping type")
+ | _ -> typ_error env l ("Mapping clause must have mapping type: " ^ string_of_typ typ ^ " is not a mapping type")
let funcl_effect (FCL_aux (FCL_Funcl (id, typed_pexp), (l, annot))) =
match annot with
@@ -4261,7 +4263,7 @@ let infer_funtyp l env tannotopt funcls =
| P_lit lit -> infer_lit env lit
| P_typ (typ, _) -> typ
| P_tup pats -> mk_typ (Typ_tup (List.map typ_from_pat pats))
- | _ -> typ_error l ("Cannot infer type from pattern " ^ string_of_pat pat)
+ | _ -> typ_error env l ("Cannot infer type from pattern " ^ string_of_pat pat)
in
match funcls with
| [FCL_aux (FCL_Funcl (_, Pat_aux (pexp,_)), _)] ->
@@ -4276,9 +4278,9 @@ let infer_funtyp l env tannotopt funcls =
in
let fn_typ = mk_typ (Typ_fn (arg_typs, ret_typ, Effect_aux (Effect_set [], Parse_ast.Unknown))) in
(quant, fn_typ)
- | _ -> typ_error l "Cannot infer function type for function with multiple clauses"
+ | _ -> typ_error env l "Cannot infer function type for function with multiple clauses"
end
- | Typ_annot_opt_aux (Typ_annot_opt_none, _) -> typ_error l "Cannot infer function type for unannotated function"
+ | Typ_annot_opt_aux (Typ_annot_opt_none, _) -> typ_error env l "Cannot infer function type for unannotated function"
let mk_val_spec env typq typ id =
let eff =
@@ -4293,7 +4295,7 @@ let check_tannotopt env typq ret_typ = function
| Typ_annot_opt_aux (Typ_annot_opt_some (annot_typq, annot_ret_typ), l) ->
if typ_identical env ret_typ annot_ret_typ
then ()
- else typ_error l (string_of_bind (typq, ret_typ) ^ " and " ^ string_of_bind (annot_typq, annot_ret_typ) ^ " do not match between function and val spec")
+ else typ_error env l (string_of_bind (typq, ret_typ) ^ " and " ^ string_of_bind (annot_typq, annot_ret_typ) ^ " do not match between function and val spec")
let check_fundef env (FD_aux (FD_function (recopt, tannotopt, effectopt, funcls), (l, _)) as fd_aux) =
let id =
@@ -4301,23 +4303,23 @@ let check_fundef env (FD_aux (FD_function (recopt, tannotopt, effectopt, funcls)
(fun (FCL_aux (FCL_Funcl (id, _), _)) id' ->
match id' with
| Some id' -> if string_of_id id' = string_of_id id then Some id'
- else typ_error l ("Function declaration expects all definitions to have the same name, "
+ else typ_error env l ("Function declaration expects all definitions to have the same name, "
^ string_of_id id ^ " differs from other definitions of " ^ string_of_id id')
| None -> Some id) funcls None)
with
| Some id -> id
- | None -> typ_error l "funcl list is empty"
+ | None -> typ_error env l "funcl list is empty"
in
typ_print (lazy ("\n" ^ Util.("Check function " |> cyan |> clear) ^ string_of_id id));
let have_val_spec, (quant, typ), env =
try true, Env.get_val_spec id env, env with
- | Type_error (l, _) ->
+ | Type_error (_, l, _) ->
let (quant, typ) = infer_funtyp l env tannotopt funcls in
false, (quant, typ), env
in
let vtyp_args, vtyp_ret, declared_eff, vl = match typ with
| Typ_aux (Typ_fn (vtyp_args, vtyp_ret, declared_eff), vl) -> vtyp_args, vtyp_ret, declared_eff, vl
- | _ -> typ_error l "Function val spec is not a function type"
+ | _ -> typ_error env l "Function val spec is not a function type"
in
check_tannotopt env quant vtyp_ret tannotopt;
typ_debug (lazy ("Checking fundef " ^ string_of_id id ^ " has type " ^ string_of_bind (quant, typ)));
@@ -4345,14 +4347,14 @@ let check_fundef env (FD_aux (FD_function (recopt, tannotopt, effectopt, funcls)
if (equal_effects eff declared_eff || !opt_no_effects)
then
vs_def @ [DEF_fundef (FD_aux (FD_function (recopt, tannotopt, effectopt, funcls), (l, None)))], env
- else typ_error l ("Effects do not match: " ^ string_of_effect declared_eff ^ " declared and " ^ string_of_effect eff ^ " found")
+ else typ_error env l ("Effects do not match: " ^ string_of_effect declared_eff ^ " declared and " ^ string_of_effect eff ^ " found")
let check_mapdef env (MD_aux (MD_mapping (id, tannot_opt, mapcls), (l, _)) as md_aux) =
typ_print (lazy ("\nChecking mapping " ^ string_of_id id));
let have_val_spec, (quant, typ), env =
try true, Env.get_val_spec id env, env with
- | Type_error (l, _) as err ->
+ | Type_error (_, l, _) as err ->
match tannot_opt with
| Typ_annot_opt_aux (Typ_annot_opt_some (quant, typ), _) ->
false, (quant, typ), env
@@ -4361,13 +4363,13 @@ let check_mapdef env (MD_aux (MD_mapping (id, tannot_opt, mapcls), (l, _)) as md
in
let vtyp1, vtyp2, vl = match typ with
| Typ_aux (Typ_bidir (vtyp1, vtyp2), vl) -> vtyp1, vtyp2, vl
- | _ -> typ_error l "Mapping val spec was not a mapping type"
+ | _ -> typ_error env l "Mapping val spec was not a mapping type"
in
begin match tannot_opt with
| Typ_annot_opt_aux (Typ_annot_opt_none, _) -> ()
| Typ_annot_opt_aux (Typ_annot_opt_some (annot_typq, annot_typ), l) ->
if typ_identical env typ annot_typ then ()
- else typ_error l (string_of_bind (quant, typ) ^ " and " ^ string_of_bind (annot_typq, annot_typ) ^ " do not match between mapping and val spec")
+ else typ_error env l (string_of_bind (quant, typ) ^ " and " ^ string_of_bind (annot_typq, annot_typ) ^ " do not match between mapping and val spec")
end;
typ_debug (lazy ("Checking mapdef " ^ string_of_id id ^ " has type " ^ string_of_bind (quant, typ)));
let vs_def, env =
@@ -4383,7 +4385,7 @@ let check_mapdef env (MD_aux (MD_mapping (id, tannot_opt, mapcls), (l, _)) as md
if equal_effects eff no_effect || equal_effects eff (mk_effect [BE_escape]) || !opt_no_effects then
vs_def @ [DEF_mapdef (MD_aux (MD_mapping (id, tannot_opt, mapcls), (l, None)))], env
else
- typ_error l ("Mapping not pure (or escape only): " ^ string_of_effect eff ^ " found")
+ typ_error env l ("Mapping not pure (or escape only): " ^ string_of_effect eff ^ " found")
(* Checking a val spec simply adds the type as a binding in the
context. We have to destructure the various kinds of val specs, but
@@ -4415,7 +4417,7 @@ let check_default env (DT_aux (ds, l)) =
match ds with
| DT_order (Ord_aux (Ord_inc, _)) -> [DEF_default (DT_aux (ds, l))], Env.set_default_order_inc env
| DT_order (Ord_aux (Ord_dec, _)) -> [DEF_default (DT_aux (ds, l))], Env.set_default_order_dec env
- | DT_order (Ord_aux (Ord_var _, _)) -> typ_error l "Cannot have variable default order"
+ | DT_order (Ord_aux (Ord_var _, _)) -> typ_error env l "Cannot have variable default order"
let kinded_id_arg kind_id =
let typ_arg arg = A_aux (arg, Parse_ast.Unknown) in
@@ -4471,14 +4473,14 @@ let mk_synonym typq typ_arg =
let typ_arg, ncs = subst_args kopts args in
typ_arg_subst (kopt_kid kopt) (arg_bool arg) typ_arg, ncs
| [], [] -> typ_arg, ncs
- | _, A_aux (_, l) :: _ -> typ_error l "Synonym applied to bad arguments"
- | _, _ -> typ_error Parse_ast.Unknown "Synonym applied to bad arguments"
+ | _, A_aux (_, l) :: _ -> typ_error Env.empty l "Synonym applied to bad arguments"
+ | _, _ -> typ_error Env.empty Parse_ast.Unknown "Synonym applied to bad arguments"
in
fun env args ->
let typ_arg, ncs = subst_args kopts args in
if List.for_all (prove __POS__ env) ncs
then typ_arg
- else typ_error Parse_ast.Unknown ("Could not prove constraints " ^ string_of_list ", " string_of_n_constraint ncs
+ else typ_error env Parse_ast.Unknown ("Could not prove constraints " ^ string_of_list ", " string_of_n_constraint ncs
^ " in type synonym " ^ string_of_typ_arg typ_arg
^ " with " ^ string_of_list ", " string_of_n_constraint (Env.get_constraints env))
@@ -4520,7 +4522,7 @@ let rec check_typedef : 'a. Env.t -> 'a type_def -> (tannot def) list * Env.t =
let (Defs defs), env = check env (Bitfield.macro id size order ranges) in
defs, env
| _ ->
- typ_error l "Bad bitfield type"
+ typ_error env l "Bad bitfield type"
end
and check_scattered : 'a. Env.t -> 'a scattered_def -> (tannot def) list * Env.t =
diff --git a/src/type_check.mli b/src/type_check.mli
index d1061826..e3a22c8d 100644
--- a/src/type_check.mli
+++ b/src/type_check.mli
@@ -80,9 +80,11 @@ type type_error =
| Err_subtype of typ * typ * n_constraint list * Ast.l KBindings.t
| Err_no_num_ident of id
| Err_other of string
- | Err_because of type_error * type_error
+ | Err_because of type_error * Ast.l * type_error
-exception Type_error of l * type_error;;
+type env
+
+exception Type_error of env * l * type_error;;
val typ_debug : ?level:int -> string Lazy.t -> unit
val typ_print : string Lazy.t -> unit
@@ -93,7 +95,7 @@ val typ_print : string Lazy.t -> unit
contains functions that operate on that state. *)
module Env : sig
(** Env.t is the type of environments *)
- type t
+ type t = env
(** Note: Most get_ functions assume the identifiers exist, and throw
type errors if they don't. *)
@@ -316,7 +318,7 @@ val bind_pat : Env.t -> unit pat -> typ -> tannot pat * Env.t * unit Ast.exp lis
on patterns that have previously been type checked. *)
val bind_pat_no_guard : Env.t -> unit pat -> typ -> tannot pat * Env.t
-val typ_error : Ast.l -> string -> 'a
+val typ_error : Env.t -> Ast.l -> string -> 'a
(** {2 Destructuring type annotations} Partial functions: The
expressions and patterns passed to these functions must be
diff --git a/src/type_error.ml b/src/type_error.ml
index f28e4de8..6f856480 100644
--- a/src/type_error.ml
+++ b/src/type_error.ml
@@ -48,31 +48,16 @@
(* SUCH DAMAGE. *)
(**************************************************************************)
-open PPrint
open Util
open Ast
open Ast_util
open Type_check
-let bullet f xs =
- group (separate_map hardline (fun x -> string "* " ^^ nest 2 (f x)) xs)
-
-let pp_nexp, pp_n_constraint =
- let pp_nexp' nexp =
- string (string_of_nexp nexp)
- in
-
- let pp_n_constraint' nc =
- string (string_of_n_constraint nc)
- in
- pp_nexp', pp_n_constraint'
-
type suggestion =
| Suggest_add_constraint of n_constraint
| Suggest_none
-(* Temporary hack while I work on using these suggestions in asl_parser *)
-let rec analyze_unresolved_quant2 locals ncs = function
+let rec analyze_unresolved_quant locals ncs = function
| QI_aux (QI_const nc, _) ->
let gen_kids = List.filter is_kid_generated (KidSet.elements (tyvars_of_constraint nc)) in
if gen_kids = [] then
@@ -117,104 +102,53 @@ let rec analyze_unresolved_quant2 locals ncs = function
| QI_aux (QI_id kopt, _) ->
Suggest_none
-let rec analyze_unresolved_quant locals ncs = function
- | QI_aux (QI_const nc, _) ->
- let gen_kids = List.filter is_kid_generated (KidSet.elements (tyvars_of_constraint nc)) in
- if gen_kids = [] then
- string ("Try adding the constraint: " ^ string_of_n_constraint nc)
- else
- (* If there are generated kind-identifiers in the constraint,
- we don't want to make a suggestion based on them, so try to
- look for generated kid free nexps in the set of constraints
- that are equal to the generated identifier. This often
- occurs due to how the type-checker introduces new type
- variables. *)
- let is_subst v = function
- | NC_aux (NC_equal (Nexp_aux (Nexp_var v', _), nexp), _)
- when Kid.compare v v' = 0 && not (KidSet.exists is_kid_generated (tyvars_of_nexp nexp)) ->
- [(v, nexp)]
- | NC_aux (NC_equal (nexp, Nexp_aux (Nexp_var v', _)), _)
- when Kid.compare v v' = 0 && not (KidSet.exists is_kid_generated (tyvars_of_nexp nexp)) ->
- [(v, nexp)]
- | _ -> []
- in
- let substs = List.concat (List.map (fun v -> List.concat (List.map (fun nc -> is_subst v nc) ncs)) gen_kids) in
- let nc = List.fold_left (fun nc (v, nexp) -> constraint_subst v (arg_nexp nexp) nc) nc substs in
- if not (KidSet.exists is_kid_generated (tyvars_of_constraint nc)) then
- string ("Try adding the constraint " ^ string_of_n_constraint nc)
- else
- (* If we have a really anonymous type-variable, try to find a
- regular variable that corresponds to it. *)
- let is_linked v = function
- | (id, (Immutable, (Typ_aux (Typ_app (ty_id, [A_aux (A_nexp (Nexp_aux (Nexp_var v', _)), _)]), _) as typ)))
- when Id.compare ty_id (mk_id "atom") = 0 && Kid.compare v v' = 0 ->
- [(v, nid id, typ)]
- | (id, (mut, typ)) ->
- []
- in
- let substs = List.concat (List.map (fun v -> List.concat (List.map (fun nc -> is_linked v nc) (Bindings.bindings locals))) gen_kids) in
- (string "Try adding named type variables for"
- ^//^ string (Util.string_of_list ", " (fun (_, nexp, typ) -> string_of_nexp nexp ^ " : " ^ string_of_typ typ) substs))
- ^^ twice hardline ^^
- let nc = List.fold_left (fun nc (v, nexp, _) -> constraint_subst v (arg_nexp nexp) nc) nc substs in
- if not (KidSet.exists is_kid_generated (tyvars_of_constraint nc)) then
- string ("The property " ^ string_of_n_constraint nc ^ " must hold")
- else
- empty
+let message_of_type_error =
+ let open Error_format in
+ let rec msg = function
+ | Err_because (err, l', err') ->
+ Seq [msg err;
+ Line "This error occured because of a previous error:";
+ Location (l', msg err')]
- | QI_aux (QI_id kopt, _) ->
- empty
+ | Err_other str -> Line str
-let rec pp_type_error = function
- | Err_no_casts (exp, typ_from, typ_to, trigger, reasons) ->
- let coercion =
- group (string "Tried performing type coercion from" ^/^ Pretty_print_sail.doc_typ typ_from
- ^/^ string "to" ^/^ Pretty_print_sail.doc_typ typ_to
- ^/^ string "on" ^/^ Pretty_print_sail.doc_exp exp)
- in
- coercion ^^ hardline
- ^^ (string "Coercion failed because:" ^//^ pp_type_error trigger)
- ^^ if not (reasons = []) then
- hardline
- ^^ (string "Possible reasons:" ^//^ separate_map hardline pp_type_error reasons)
- else
- empty
+ | Err_no_overloading (id, errs) ->
+ Seq [Line ("No overloading for " ^ string_of_id id ^ ", tried:");
+ List (List.map (fun (id, err) -> string_of_id id, msg err) errs)]
- | Err_no_overloading (id, errs) ->
- string ("No overloadings for " ^ string_of_id id ^ ", tried:") ^//^
- group (separate_map hardline (fun (id, err) -> string (string_of_id id) ^^ colon ^//^ pp_type_error err) errs)
+ | Err_unresolved_quants (id, quants, locals, ncs) ->
+ Seq [Line ("Could not resolve quantifiers for " ^ string_of_id id);
+ Line (bullet ^ " " ^ Util.string_of_list ("\n" ^ bullet ^ " ") string_of_quant_item quants)]
- | Err_subtype (typ1, typ2, constrs, locs) ->
- (separate space [ string (string_of_typ typ1);
- string "is not a subtype of";
- string (string_of_typ typ2) ])
- ^/^ string "in context"
- ^/^ bullet pp_n_constraint constrs
- ^/^ string "where"
- ^/^ bullet (fun (kid, l) -> string (string_of_kid kid ^ " bound at " ^ Reporting.loc_to_string l ^ "\n")) (KBindings.bindings locs)
+ | Err_subtype (typ1, typ2, _, vars) ->
+ let vars = KBindings.bindings vars in
+ let vars = List.filter (fun (v, _) -> KidSet.mem v (KidSet.union (tyvars_of_typ typ1) (tyvars_of_typ typ2))) vars in
+ With ((fun ppf -> { ppf with loc_color = Util.yellow }),
+ Seq (Line (string_of_typ typ1 ^ " is not a subtype of " ^ string_of_typ typ2)
+ :: List.map (fun (kid, l) -> Location (l, Line (string_of_kid kid ^ " bound here"))) vars))
| Err_no_num_ident id ->
- string "No num identifier" ^^ space ^^ string (string_of_id id)
+ Line ("No num identifier " ^ string_of_id id)
- | Err_unresolved_quants (id, quants, locals, ncs) ->
- (string "Could not resolve quantifiers for" ^^ space ^^ string (string_of_id id)
- ^//^ group (separate_map hardline (fun quant -> string (string_of_quant_item quant)) quants))
- ^^ twice hardline
- ^^ group (separate_map hardline (analyze_unresolved_quant locals ncs) quants)
-
- (* We only got err, because of previous error, err' *)
- | Err_because (err, err') ->
- pp_type_error err
- ^^ hardline ^^ string "This error occured because of a previous error:"
- ^//^ pp_type_error err'
-
- | Err_other str -> string str
+ | Err_no_casts (exp, typ_from, typ_to, trigger, reasons) ->
+ let coercion =
+ Line ("Tried performing type coercion from " ^ string_of_typ typ_from
+ ^ " to " ^ string_of_typ typ_to
+ ^ " on " ^ string_of_exp exp)
+ in
+ Seq ([coercion; Line "Coercion failed because:"; msg trigger]
+ @ if not (reasons = []) then
+ Line "Possible reasons:" :: List.map msg reasons
+ else
+ [])
+ in
+ msg
let rec string_of_type_error err =
- let open PPrint in
+ let open Error_format in
let b = Buffer.create 20 in
- ToBuffer.pretty 1. 400 b (pp_type_error err);
- "\n" ^ Buffer.contents b
+ format_message (message_of_type_error err) (buffer_formatter b);
+ Buffer.contents b
let rec collapse_errors = function
| (Err_no_overloading (_, (err :: errs)) as no_collapse) ->
@@ -232,16 +166,18 @@ let rec collapse_errors = function
| Some _ -> err
| None -> no_collapse
end
- | Err_because (err1, err2) as no_collapse ->
+ | Err_because (err1, l, err2) as no_collapse ->
let err1 = collapse_errors err1 in
let err2 = collapse_errors err2 in
if string_of_type_error err1 = string_of_type_error err2 then
err1
else
- Err_because (err1, err2)
+ Err_because (err1, l, err2)
| err -> err
let check : 'a. Env.t -> 'a defs -> tannot defs * Env.t =
fun env defs ->
try Type_check.check env defs with
- | Type_error (l, err) -> raise (Reporting.err_typ l (string_of_type_error err))
+ | Type_error (env, l, err) ->
+ Interactive.env := env;
+ raise (Reporting.err_typ l (string_of_type_error err))
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 12:27:27 +0000