summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
authorAlasdair Armstrong2018-10-31 15:43:56 +0000
committerAlasdair Armstrong2018-10-31 15:43:56 +0000
commit001e28b487c8a4cb2a25519a3acc8ac8c1aaabf5 (patch)
treec50d5a7bb026e875db96af53fd44d58387d7a7c6 /src
parent5298e209f0ae12e51f3050888e18ad9be09543e4 (diff)
Rename Reporting_basic to Reporting
There is no Reporting_complex, so it's not clear what the basic is intended to signify anyway. Add a GitHub issue link to any err_unreachable errors (as they are all bugs)
Diffstat (limited to 'src')
-rw-r--r--src/anf.ml4
-rw-r--r--src/ast_util.ml20
-rw-r--r--src/c_backend.ml2
-rw-r--r--src/extra_pervasives.ml2
-rw-r--r--src/initial_check.ml26
-rw-r--r--src/interpreter.ml2
-rw-r--r--src/isail.ml6
-rw-r--r--src/latex.ml2
-rw-r--r--src/lexer.mll7
-rw-r--r--src/monomorphise.ml98
-rw-r--r--src/ocaml_backend.ml22
-rw-r--r--src/parser.mly2
-rw-r--r--src/pattern_completeness.ml6
-rw-r--r--src/pretty_print_common.ml1
-rw-r--r--src/pretty_print_coq.ml84
-rw-r--r--src/pretty_print_lem.ml64
-rw-r--r--src/pretty_print_sail.ml2
-rw-r--r--src/process_file.ml42
-rw-r--r--src/reporting.ml (renamed from src/reporting_basic.ml)17
-rw-r--r--src/reporting.mli (renamed from src/reporting_basic.mli)2
-rw-r--r--src/rewriter.ml6
-rw-r--r--src/rewrites.ml84
-rw-r--r--src/sail.ml4
-rw-r--r--src/spec_analysis.ml2
-rw-r--r--src/state.ml4
-rw-r--r--src/type_check.ml24
-rw-r--r--src/type_check.mli2
-rw-r--r--src/type_error.ml4
28 files changed, 274 insertions, 267 deletions
diff --git a/src/anf.ml b/src/anf.ml
index 2e7b6b65..4b22b9ad 100644
--- a/src/anf.ml
+++ b/src/anf.ml
@@ -58,7 +58,7 @@ open PPrint
module Big_int = Nat_big_num
let anf_error ?loc:(l=Parse_ast.Unknown) message =
- raise (Reporting_basic.err_general l ("\nANF translation: " ^ message))
+ raise (Reporting.err_general l ("\nANF translation: " ^ message))
(**************************************************************************)
(* 1. Conversion to A-normal form (ANF) *)
@@ -510,7 +510,7 @@ let rec anf (E_aux (e_aux, ((l, _) as exp_annot)) as exp) =
| E_lit lit -> mk_aexp (ae_lit lit (typ_of exp))
| E_block [] ->
- Util.warn (Reporting_basic.loc_to_string l
+ Util.warn (Reporting.loc_to_string l
^ "\n\nTranslating empty block (possibly assigning to an uninitialized variable at the end of a block?)");
mk_aexp (ae_lit (L_aux (L_unit, l)) (typ_of exp))
| E_block exps ->
diff --git a/src/ast_util.ml b/src/ast_util.ml
index 9490366f..a0b75fc2 100644
--- a/src/ast_util.ml
+++ b/src/ast_util.ml
@@ -344,7 +344,7 @@ let rec nc_negate (NC_aux (nc, l)) =
| NC_set (kid, int :: ints) ->
mk_nc (NC_and (nc_neq (nvar kid) (nconstant int), nc_negate (mk_nc (NC_set (kid, ints)))))
| NC_app _ ->
- raise (Reporting_basic.err_unreachable l __POS__ "tried to negate constraint with unexpanded synonym")
+ raise (Reporting.err_unreachable l __POS__ "tried to negate constraint with unexpanded synonym")
let mk_typschm typq typ = TypSchm_aux (TypSchm_ts (typq, typ), Parse_ast.Unknown)
@@ -828,13 +828,13 @@ let id_of_fundef (FD_aux (FD_function (_, _, _, funcls), (l, _))) =
(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 raise (Reporting_basic.err_typ l
+ else raise (Reporting.err_typ 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 -> raise (Reporting_basic.err_typ l "funcl list is empty")
+ | None -> raise (Reporting.err_typ l "funcl list is empty")
let id_of_type_def_aux = function
| TD_abbrev (id, _, _)
@@ -959,7 +959,7 @@ module TypMap = Map.Make(Typ)
let rec nexp_frees (Nexp_aux (nexp, l)) =
match nexp with
- | Nexp_id _ -> raise (Reporting_basic.err_typ l "Unimplemented Nexp_id in nexp_frees")
+ | Nexp_id _ -> raise (Reporting.err_typ l "Unimplemented Nexp_id in nexp_frees")
| Nexp_var kid -> KidSet.singleton kid
| Nexp_constant _ -> KidSet.empty
| Nexp_times (n1, n2) -> KidSet.union (nexp_frees n1) (nexp_frees n2)
@@ -977,7 +977,7 @@ let rec lexp_to_exp (LEXP_aux (lexp_aux, annot) as le) =
let get_id (LEXP_aux(lexp,((l,_) as annot)) as le) = match lexp with
| LEXP_id id | LEXP_cast (_, id) -> E_aux (E_id id, annot)
| _ ->
- raise (Reporting_basic.err_unreachable l __POS__
+ raise (Reporting.err_unreachable l __POS__
("Unsupported sub-lexp " ^ string_of_lexp le ^ " in tuple")) in
rewrap (E_tuple (List.map get_id les))
| LEXP_vector (lexp, e) -> rewrap (E_vector_access (lexp_to_exp lexp, e))
@@ -1016,7 +1016,7 @@ let typ_app_args_of = function
| Typ_aux (Typ_app (Id_aux (Id c,_), targs), l) ->
(c, List.map (fun (Typ_arg_aux (a,_)) -> a) targs, l)
| Typ_aux (_, l) as typ ->
- raise (Reporting_basic.err_typ l
+ raise (Reporting.err_typ l
("typ_app_args_of called on non-app type " ^ string_of_typ typ))
let rec vector_typ_args_of typ = match typ_app_args_of typ with
@@ -1024,7 +1024,7 @@ let rec vector_typ_args_of typ = match typ_app_args_of typ with
(nexp_simp len, ord, etyp)
| ("register", [Typ_arg_typ rtyp], _) -> vector_typ_args_of rtyp
| (_, _, l) ->
- raise (Reporting_basic.err_typ l
+ raise (Reporting.err_typ l
("vector_typ_args_of called on non-vector type " ^ string_of_typ typ))
let vector_start_index typ =
@@ -1032,13 +1032,13 @@ let vector_start_index typ =
match ord with
| Ord_aux (Ord_inc, _) -> nint 0
| Ord_aux (Ord_dec, _) -> nexp_simp (nminus len (nint 1))
- | _ -> raise (Reporting_basic.err_typ (typ_loc typ) "Can't calculate start index without order")
+ | _ -> raise (Reporting.err_typ (typ_loc typ) "Can't calculate start index without order")
let is_order_inc = function
| Ord_aux (Ord_inc, _) -> true
| Ord_aux (Ord_dec, _) -> false
| Ord_aux (Ord_var _, l) ->
- raise (Reporting_basic.err_unreachable l __POS__ "is_order_inc called on vector with variable ordering")
+ raise (Reporting.err_unreachable l __POS__ "is_order_inc called on vector with variable ordering")
let is_bit_typ = function
| Typ_aux (Typ_id (Id_aux (Id "bit", _)), _) -> true
@@ -1506,7 +1506,7 @@ and nexp_subst_aux sv subst = function
| Nexp_neg nexp -> Nexp_neg (nexp_subst sv subst nexp)
let rec nexp_set_to_or l subst = function
- | [] -> raise (Reporting_basic.err_unreachable l __POS__ "Empty set in constraint")
+ | [] -> raise (Reporting.err_unreachable l __POS__ "Empty set in constraint")
| [int] -> NC_equal (subst, nconstant int)
| (int :: ints) -> NC_or (mk_nc (NC_equal (subst, nconstant int)), mk_nc (nexp_set_to_or l subst ints))
diff --git a/src/c_backend.ml b/src/c_backend.ml
index 392f2349..6dca1f8a 100644
--- a/src/c_backend.ml
+++ b/src/c_backend.ml
@@ -75,7 +75,7 @@ let c_debug str =
if !c_verbosity > 0 then prerr_endline (Lazy.force str) else ()
let c_error ?loc:(l=Parse_ast.Unknown) message =
- raise (Reporting_basic.err_general l ("\nC backend: " ^ message))
+ raise (Reporting.err_general l ("\nC backend: " ^ message))
let zencode_id = function
| Id_aux (Id str, l) -> Id_aux (Id (Util.zencode_string str), l)
diff --git a/src/extra_pervasives.ml b/src/extra_pervasives.ml
index a7808a95..8001c647 100644
--- a/src/extra_pervasives.ml
+++ b/src/extra_pervasives.ml
@@ -49,4 +49,4 @@
(**************************************************************************)
let unreachable l pos msg =
- raise (Reporting_basic.err_unreachable l pos msg)
+ raise (Reporting.err_unreachable l pos msg)
diff --git a/src/initial_check.ml b/src/initial_check.ml
index 36513ba1..f98b11d8 100644
--- a/src/initial_check.ml
+++ b/src/initial_check.ml
@@ -112,13 +112,13 @@ let typquant_to_quantkinds k_env typquant =
| KOpt_aux(KOpt_none(v),l) | KOpt_aux(KOpt_kind(_,v),l) ->
(match Envmap.apply k_env (var_to_string v) with
| Some(typ) -> typ::rst
- | None -> raise (Reporting_basic.err_unreachable l __POS__ "Envmap didn't get an entry during typschm processing"))
+ | None -> raise (Reporting.err_unreachable l __POS__ "Envmap didn't get an entry during typschm processing"))
end)
qlist
[])
let typ_error l msg opt_id opt_var opt_kind =
- raise (Reporting_basic.err_typ
+ raise (Reporting.err_typ
l
(msg ^
(match opt_id, opt_var, opt_kind with
@@ -157,7 +157,7 @@ let to_ast_base_kind (Parse_ast.BK_aux(k,l')) =
let to_ast_kind (k_env : kind Envmap.t) (Parse_ast.K_aux(Parse_ast.K_kind(klst),l)) : (Ast.kind * kind) =
match klst with
- | [] -> raise (Reporting_basic.err_unreachable l __POS__ "Kind with empty kindlist encountered")
+ | [] -> raise (Reporting.err_unreachable l __POS__ "Kind with empty kindlist encountered")
| [k] -> let k_ast,k_typ = to_ast_base_kind k in
K_aux(K_kind([k_ast]),l), k_typ
| ks -> let k_pairs = List.map to_ast_base_kind ks in
@@ -211,7 +211,7 @@ let rec to_ast_typ (k_env : kind Envmap.t) (def_ord : order) (t: Parse_ast.atyp)
let rise = match def_ord with
| Ord_aux(Ord_inc,dl) -> to_ast_nexp k_env (make_r b r)
| Ord_aux(Ord_dec,dl) -> to_ast_nexp k_env (make_r r b)
- | _ -> raise (Reporting_basic.err_unreachable l __POS__ "Default order not inc or dec") in
+ | _ -> raise (Reporting.err_unreachable l __POS__ "Default order not inc or dec") in
Typ_app(Id_aux(Id "vector",il),
[Typ_arg_aux (Typ_arg_nexp base,Parse_ast.Unknown);
Typ_arg_aux (Typ_arg_nexp rise,Parse_ast.Unknown);
@@ -227,7 +227,7 @@ let rec to_ast_typ (k_env : kind Envmap.t) (def_ord : order) (t: Parse_ast.atyp)
let (base,rise) = match def_ord with
| Ord_aux(Ord_inc,dl) -> (to_ast_nexp k_env b), (to_ast_nexp k_env r)
| Ord_aux(Ord_dec,dl) -> (to_ast_nexp k_env (make_sub_one r)), (to_ast_nexp k_env r)
- | _ -> raise (Reporting_basic.err_unreachable l __POS__ "Default order not inc or dec") in
+ | _ -> raise (Reporting.err_unreachable l __POS__ "Default order not inc or dec") in
Typ_app(Id_aux(Id "vector",il),
[Typ_arg_aux (Typ_arg_nexp base,Parse_ast.Unknown);
Typ_arg_aux (Typ_arg_nexp rise,Parse_ast.Unknown);
@@ -341,7 +341,7 @@ and to_ast_typ_arg (k_env : kind Envmap.t) (def_ord : order) (kind : kind) (arg
| K_Typ -> Typ_arg_typ (to_ast_typ k_env def_ord arg)
| K_Nat -> Typ_arg_nexp (to_ast_nexp k_env arg)
| K_Ord -> Typ_arg_order (to_ast_order k_env def_ord arg)
- | _ -> raise (Reporting_basic.err_unreachable l __POS__ ("To_ast_typ_arg received Lam kind or infer kind: " ^ kind_to_string kind))),
+ | _ -> raise (Reporting.err_unreachable l __POS__ ("To_ast_typ_arg received Lam kind or infer kind: " ^ kind_to_string kind))),
l)
and to_ast_nexp_constraint (k_env : kind Envmap.t) (c : Parse_ast.n_constraint) : n_constraint =
@@ -400,7 +400,7 @@ let to_ast_typquant (k_env: kind Envmap.t) (tq : Parse_ast.typquant) : typquant
let kopt,k_env,k_env_local = (match kind,ktyp with
| Some(k),Some(kt) -> KOpt_kind(k,v), (Envmap.insert k_env (key,kt)), (Envmap.insert local_env (key,kt))
| None, Some(kt) -> KOpt_none(v), (Envmap.insert k_env (key,kt)), (Envmap.insert local_env (key,kt))
- | _ -> raise (Reporting_basic.err_unreachable l __POS__ "Envmap in dom is true but apply gives None")) in
+ | _ -> raise (Reporting.err_unreachable l __POS__ "Envmap in dom is true but apply gives None")) in
KOpt_aux(kopt,l),k_env,local_names,k_env_local
in
match tq with
@@ -538,11 +538,11 @@ and to_ast_exp (k_env : kind Envmap.t) (def_ord : order) (Parse_ast.E_aux(exp,l)
| Parse_ast.E_record fexps ->
(match to_ast_fexps true k_env def_ord fexps with
| Some fexps -> E_record fexps
- | None -> raise (Reporting_basic.err_unreachable l __POS__ "to_ast_fexps with true returned none"))
+ | None -> raise (Reporting.err_unreachable l __POS__ "to_ast_fexps with true returned none"))
| Parse_ast.E_record_update(exp,fexps) ->
(match to_ast_fexps true k_env def_ord fexps with
| Some(fexps) -> E_record_update(to_ast_exp k_env def_ord exp, fexps)
- | _ -> raise (Reporting_basic.err_unreachable l __POS__ "to_ast_fexps with true returned none"))
+ | _ -> raise (Reporting.err_unreachable l __POS__ "to_ast_fexps with true returned none"))
| Parse_ast.E_field(exp,id) -> E_field(to_ast_exp k_env def_ord exp, to_ast_id id)
| Parse_ast.E_case(exp,pexps) -> E_case(to_ast_exp k_env def_ord exp, List.map (to_ast_case k_env def_ord) pexps)
| Parse_ast.E_try (exp, pexps) -> E_try (to_ast_exp k_env def_ord exp, List.map (to_ast_case k_env def_ord) pexps)
@@ -555,7 +555,7 @@ and to_ast_exp (k_env : kind Envmap.t) (def_ord : order) (Parse_ast.E_aux(exp,l)
| Parse_ast.E_throw exp -> E_throw (to_ast_exp k_env def_ord exp)
| Parse_ast.E_return exp -> E_return(to_ast_exp k_env def_ord exp)
| Parse_ast.E_assert(cond,msg) -> E_assert(to_ast_exp k_env def_ord cond, to_ast_exp k_env def_ord msg)
- | _ -> raise (Reporting_basic.err_unreachable l __POS__ "Unparsable construct in to_ast_exp")
+ | _ -> raise (Reporting.err_unreachable l __POS__ "Unparsable construct in to_ast_exp")
), (l,()))
and to_ast_lexp (k_env : kind Envmap.t) (def_ord : order) (Parse_ast.E_aux(exp,l) : Parse_ast.exp) : unit lexp =
@@ -858,7 +858,7 @@ let to_ast_alias_spec k_env def_ord (Parse_ast.E_aux(e,le)) =
Parse_ast.E_aux(Parse_ast.E_id second,ls)) ->
AL_concat(RI_aux(RI_id (to_ast_id first),(lf,())),
RI_aux(RI_id (to_ast_id second),(ls,())))
- | _ -> raise (Reporting_basic.err_unreachable le __POS__ "Found an expression not supported by parser in to_ast_alias_spec")
+ | _ -> raise (Reporting.err_unreachable le __POS__ "Found an expression not supported by parser in to_ast_alias_spec")
), (le,()))
let to_ast_dec (names,k_env,def_ord) (Parse_ast.DEC_aux(regdec,l)) =
@@ -1008,7 +1008,7 @@ let to_ast_def (names, k_env, def_ord) partial_defs def : def_progress envs_out
((Finished def), envs),partial_defs
| _, true ->
typ_error l "Scattered definition ended multiple times" (Some id) None None
- | _ -> raise (Reporting_basic.err_unreachable l __POS__ "Something in partial_defs other than fundef and type"))))
+ | _ -> raise (Reporting.err_unreachable l __POS__ "Something in partial_defs other than fundef and type"))))
let rec to_ast_defs_helper envs partial_defs = function
| [] -> ([],envs,partial_defs)
@@ -1021,7 +1021,7 @@ let rec to_ast_defs_helper envs partial_defs = function
(match (def_in_progress id partial_defs) with
| None ->
raise
- (Reporting_basic.err_unreachable l __POS__ "Id stored in place holder not retrievable from partial defs")
+ (Reporting.err_unreachable l __POS__ "Id stored in place holder not retrievable from partial defs")
| Some(d,k) ->
if (snd !d)
then (fst !d) :: defs, envs, partial_defs
diff --git a/src/interpreter.ml b/src/interpreter.ml
index 540e96a1..07a4b4ae 100644
--- a/src/interpreter.ml
+++ b/src/interpreter.ml
@@ -672,7 +672,7 @@ let rec eval_frame' = function
let eval_frame frame =
try eval_frame' frame with
| Type_check.Type_error (l, err) ->
- raise (Reporting_basic.err_typ l (Type_error.string_of_type_error err))
+ raise (Reporting.err_typ l (Type_error.string_of_type_error err))
let rec run_frame frame =
match frame with
diff --git a/src/isail.ml b/src/isail.ml
index c3f869a3..7ec0848d 100644
--- a/src/isail.ml
+++ b/src/isail.ml
@@ -80,7 +80,7 @@ let rec user_input callback =
mode_clear ();
begin
try callback v with
- | Reporting_basic.Fatal_error e -> Reporting_basic.report_error e
+ | Reporting.Fatal_error e -> Reporting.report_error e
end;
user_input callback
@@ -390,8 +390,8 @@ let handle_input input =
try handle_input' input with
| Type_check.Type_error (l, err) ->
print_endline (Type_error.string_of_type_error err)
- | Reporting_basic.Fatal_error err ->
- Reporting_basic.print_error err
+ | Reporting.Fatal_error err ->
+ Reporting.print_error err
| exn ->
print_endline (Printexc.to_string exn)
diff --git a/src/latex.ml b/src/latex.ml
index 39db43db..4944c5e9 100644
--- a/src/latex.ml
+++ b/src/latex.ml
@@ -105,7 +105,7 @@ let latex_loc no_loc l =
begin
let using_color = !Util.opt_colors in
Util.opt_colors := false;
- let code = Util.split_on_char '\n' (Reporting_basic.loc_to_string l) in
+ let code = Util.split_on_char '\n' (Reporting.loc_to_string l) in
let doc = match code with
| _ :: _ :: code -> string (add_links (String.concat "\n" code))
| _ -> empty
diff --git a/src/lexer.mll b/src/lexer.mll
index cbefa601..8b229772 100644
--- a/src/lexer.mll
+++ b/src/lexer.mll
@@ -163,7 +163,6 @@ let kw_table =
("do", (fun _ -> Do));
("mutual", (fun _ -> Mutual));
("bitfield", (fun _ -> Bitfield));
- ("tuple", (fun _ -> Tuple));
("where", (fun _ -> Where));
("barr", (fun x -> Barr));
@@ -329,12 +328,12 @@ and string pos b = parse
| ([^'"''\n''\\']* as i) { Buffer.add_string b i; string pos b lexbuf }
| escape_sequence as i { Buffer.add_string b i; string pos b lexbuf }
| '\\' '\n' ws { Lexing.new_line lexbuf; string pos b lexbuf }
- | '\\' { assert false (*raise (Reporting_basic.Fatal_error (Reporting_basic.Err_syntax (pos,
+ | '\\' { assert false (*raise (Reporting.Fatal_error (Reporting.Err_syntax (pos,
"illegal backslash escape in string"*) }
| '"' { let s = unescaped(Buffer.contents b) in
(*try Ulib.UTF8.validate s; s
with Ulib.UTF8.Malformed_code ->
- raise (Reporting_basic.Fatal_error (Reporting_basic.Err_syntax (pos,
+ raise (Reporting.Fatal_error (Reporting.Err_syntax (pos,
"String literal is not valid utf8"))) *) s }
- | eof { assert false (*raise (Reporting_basic.Fatal_error (Reporting_basic.Err_syntax (pos,
+ | eof { assert false (*raise (Reporting.Fatal_error (Reporting.Err_syntax (pos,
"String literal not terminated")))*) }
diff --git a/src/monomorphise.ml b/src/monomorphise.ml
index 258b4e1f..c43b4a56 100644
--- a/src/monomorphise.ml
+++ b/src/monomorphise.ml
@@ -115,7 +115,7 @@ let rec subst_nc substs (NC_aux (nc,l) as n_constraint) =
| Nexp_aux (Nexp_constant i,_) ->
if List.exists (fun j -> Big_int.equal i j) is then re NC_true else re NC_false
| nexp ->
- raise (Reporting_basic.err_general l
+ raise (Reporting.err_general l
("Unable to substitute " ^ string_of_nexp nexp ^
" into set constraint " ^ string_of_n_constraint n_constraint))
| exception Not_found -> n_constraint
@@ -180,7 +180,7 @@ let rec is_value (E_aux (e,(l,annot))) =
let is_constructor id =
match destruct_tannot annot with
| None ->
- (Reporting_basic.print_err false true l "Monomorphisation"
+ (Reporting.print_err false true l "Monomorphisation"
("Missing type information for identifier " ^ string_of_id id);
false) (* Be conservative if we have no info *)
| Some (env,_,_) ->
@@ -281,7 +281,7 @@ let extract_set_nc l var nc =
| None, Some (is,nc2') -> Some (is, re (NC_and (nc1,nc2')))
| Some (is,nc1'), None -> Some (is, re (NC_and (nc1',nc2)))
| Some _, Some _ ->
- raise (Reporting_basic.err_general l ("Multiple set constraints for " ^ string_of_kid var)))
+ raise (Reporting.err_general l ("Multiple set constraints for " ^ string_of_kid var)))
| NC_or _ ->
(match aux_or nc_full with
| Some is -> Some (is, re NC_true)
@@ -290,7 +290,7 @@ let extract_set_nc l var nc =
in match aux nc with
| Some is -> is
| None ->
- raise (Reporting_basic.err_general l ("No set constraint for " ^ string_of_kid var ^
+ raise (Reporting.err_general l ("No set constraint for " ^ string_of_kid var ^
" in " ^ string_of_n_constraint nc))
let rec peel = function
@@ -315,9 +315,9 @@ let rec inst_src_type insts (Typ_aux (ty,l) as typ) =
| Typ_var _
-> insts,typ
| Typ_fn _ ->
- raise (Reporting_basic.err_general l "Function type in constructor")
+ raise (Reporting.err_general l "Function type in constructor")
| Typ_bidir _ ->
- raise (Reporting_basic.err_general l "Mapping type in constructor")
+ raise (Reporting.err_general l "Mapping type in constructor")
| Typ_tup ts ->
let insts,ts =
List.fold_right
@@ -393,9 +393,9 @@ let split_src_type id ty (TypQ_aux (q,ql)) =
| Typ_var _
-> (KidSet.empty,[[],typ])
| Typ_fn _ ->
- raise (Reporting_basic.err_general l ("Function type in constructor " ^ i))
+ raise (Reporting.err_general l ("Function type in constructor " ^ i))
| Typ_bidir _ ->
- raise (Reporting_basic.err_general l ("Mapping type in constructor " ^ i))
+ raise (Reporting.err_general l ("Mapping type in constructor " ^ i))
| Typ_tup ts ->
let (vars,tys) = List.split (List.map size_nvars_ty ts) in
let insttys = List.map (fun x -> let (insts,tys) = List.split x in
@@ -450,10 +450,10 @@ let split_src_type id ty (TypQ_aux (q,ql)) =
| Typ_aux (Typ_tup _,_) -> Typ_aux (Typ_tup [ty],Unknown)
| _ -> ty) tys in
if contains_exist t then
- raise (Reporting_basic.err_general l
+ raise (Reporting.err_general l
"Only prenex types in unions are supported by monomorphisation")
else if List.length kids > 1 then
- raise (Reporting_basic.err_general l
+ raise (Reporting.err_general l
"Only single-variable existential types in unions are currently supported by monomorphisation")
else tys
end
@@ -465,7 +465,7 @@ let split_src_type id ty (TypQ_aux (q,ql)) =
| [] -> None
| sample::__ ->
let () = if List.length variants > size_set_limit then
- raise (Reporting_basic.err_general ql
+ raise (Reporting.err_general ql
(string_of_int (List.length variants) ^ "variants for constructor " ^ i ^
"bigger than limit " ^ string_of_int size_set_limit)) else ()
in
@@ -490,7 +490,7 @@ let reduce_nexp subst ne =
| Nexp_exp n -> Big_int.shift_left (eval n) 1
| Nexp_neg n -> Big_int.negate (eval n)
| _ ->
- raise (Reporting_basic.err_general Unknown ("Couldn't turn nexp " ^
+ raise (Reporting.err_general Unknown ("Couldn't turn nexp " ^
string_of_nexp nexp ^ " into concrete value"))
in eval ne
@@ -539,7 +539,7 @@ let refine_constructor refinements l env id args =
match List.find matches_refinement irefinements with
| (_,new_id,_) -> Some (E_app (new_id,args))
| exception Not_found ->
- (Reporting_basic.print_err false true l "Monomorphisation"
+ (Reporting.print_err false true l "Monomorphisation"
("Unable to refine constructor " ^ string_of_id id);
None)
end
@@ -723,7 +723,7 @@ let fabricate_nexp_exist env l typ kids nc typ' =
when Kid.compare kid kid'' = 0 &&
Kid.compare kid kid''' = 0 ->
nint 32
- | _ -> raise (Reporting_basic.err_general l
+ | _ -> raise (Reporting.err_general l
("Undefined value at unsupported type " ^ string_of_typ typ))
let fabricate_nexp l tannot =
@@ -753,7 +753,7 @@ let reduce_cast typ exp l annot =
let nc_env = Env.add_constraint (nc_eq (nvar kid) (nconstant n)) nc_env in
if prove nc_env nc
then exp
- else raise (Reporting_basic.err_unreachable l __POS__
+ else raise (Reporting.err_unreachable l __POS__
("Constant propagation error: literal " ^ Big_int.to_string n ^
" does not satisfy constraint " ^ string_of_n_constraint nc))
| E_aux (E_lit (L_aux (L_undef,_)),_), Some ([kid],nc,typ'') when atom_typ_kid kid typ'' ->
@@ -1154,10 +1154,10 @@ let apply_pat_choices choices =
List.fold_left (fun e (id,e') ->
E_let (LB_aux (LB_val (P_aux (P_id id, dummyannot),e'),dummyannot),E_aux (e,dummyannot))) e subst
| Pat_aux (Pat_when _,(l,_)) ->
- raise (Reporting_basic.err_unreachable l __POS__
+ raise (Reporting.err_unreachable l __POS__
"Pattern acquired a guard after analysis!")
| exception Not_found ->
- raise (Reporting_basic.err_unreachable (exp_loc e) __POS__
+ raise (Reporting.err_unreachable (exp_loc e) __POS__
"Unable to find case I found earlier!"))
| exception Not_found -> E_case (e,cases)
in
@@ -1458,7 +1458,7 @@ let split_defs all_errors splits defs =
| E_internal_plet _
| E_internal_return _
| E_internal_value _
- -> raise (Reporting_basic.err_unreachable l __POS__
+ -> raise (Reporting.err_unreachable l __POS__
("Unexpected expression encountered in monomorphisation: " ^ string_of_exp exp))
and const_prop_fexps ref_vars substs assigns (FES_aux (FES_Fexps (fes,flag), annot)) =
FES_aux (FES_Fexps (List.map (const_prop_fexp ref_vars substs assigns) fes, flag), annot)
@@ -1528,7 +1528,7 @@ let split_defs all_errors splits defs =
and can_match_with_env ref_vars env (E_aux (e,(l,annot)) as exp0) cases (substs,ksubsts) assigns =
let rec findpat_generic check_pat description assigns = function
- | [] -> (Reporting_basic.print_err false true l "Monomorphisation"
+ | [] -> (Reporting.print_err false true l "Monomorphisation"
("Failed to find a case for " ^ description); None)
| [Pat_aux (Pat_exp (P_aux (P_wild,_),exp),_)] -> Some (exp,[],[])
| (Pat_aux (Pat_exp (P_aux (P_typ (_,p),_),exp),ann))::tl ->
@@ -1575,7 +1575,7 @@ let split_defs all_errors splits defs =
| P_aux (P_app (id',[]),_) ->
if Id.compare id id' = 0 then DoesMatch ([],[]) else DoesNotMatch
| P_aux (_,(l',_)) ->
- (Reporting_basic.print_err false true l' "Monomorphisation"
+ (Reporting.print_err false true l' "Monomorphisation"
"Unexpected kind of pattern for enumeration"; GiveUp)
in findpat_generic checkpat (string_of_id id) assigns cases
| _ -> None)
@@ -1598,11 +1598,11 @@ let split_defs all_errors splits defs =
DoesMatch ([id, E_aux (E_cast (typ,E_aux (e,(l,empty_tannot))),(l,empty_tannot))],
[kid,nexp])
| _ ->
- (Reporting_basic.print_err false true lit_l "Monomorphisation"
+ (Reporting.print_err false true lit_l "Monomorphisation"
"Unexpected kind of literal for var match"; GiveUp)
end
| P_aux (_,(l',_)) ->
- (Reporting_basic.print_err false true l' "Monomorphisation"
+ (Reporting.print_err false true l' "Monomorphisation"
"Unexpected kind of pattern for literal"; GiveUp)
in findpat_generic checkpat "literal" assigns cases
| E_vector es when List.for_all (function (E_aux (E_lit _,_)) -> true | _ -> false) es ->
@@ -1622,11 +1622,11 @@ let split_defs all_errors splits defs =
| _ -> DoesNotMatch) (DoesMatch ([],[])) matches in
(match final with
| GiveUp ->
- (Reporting_basic.print_err false true l "Monomorphisation"
+ (Reporting.print_err false true l "Monomorphisation"
"Unexpected kind of pattern for vector literal"; GiveUp)
| _ -> final)
| _ ->
- (Reporting_basic.print_err false true l "Monomorphisation"
+ (Reporting.print_err false true l "Monomorphisation"
"Unexpected kind of pattern for vector literal"; GiveUp)
in findpat_generic checkpat "vector literal" assigns cases
@@ -1644,7 +1644,7 @@ let split_defs all_errors splits defs =
DoesMatch ([id, E_aux (E_cast (typ,e_undef),(l,empty_tannot))],
KBindings.bindings ksubst)
| P_aux (_,(l',_)) ->
- (Reporting_basic.print_err false true l' "Monomorphisation"
+ (Reporting.print_err false true l' "Monomorphisation"
"Unexpected kind of pattern for literal"; GiveUp)
in findpat_generic checkpat "literal" assigns cases
| _ -> None
@@ -1670,7 +1670,7 @@ let split_defs all_errors splits defs =
let new_l = Generated l in
let renew_id (Id_aux (id,l)) = Id_aux (id,new_l) in
let cannot msg =
- let open Reporting_basic in
+ let open Reporting in
let error =
Err_general (pat_l,
("Cannot split type " ^ string_of_typ typ ^ " for variable " ^ v ^ ": " ^ msg))
@@ -1726,7 +1726,7 @@ let split_defs all_errors splits defs =
let nc = List.fold_left nc_and nc_true ncs in
(match extract_set_nc l kvar nc with
| (is,_) -> List.map (mk_lit (Some kvar)) is
- | exception Reporting_basic.Fatal_error (Reporting_basic.Err_general (_,msg)) -> cannot msg)
+ | exception Reporting.Fatal_error (Reporting.Err_general (_,msg)) -> cannot msg)
| _ -> cannot ("unsupport atom nexp " ^ string_of_nexp nexp)
end
| _ -> cannot ("unsupported type " ^ string_of_typ typ)
@@ -1799,10 +1799,10 @@ let split_defs all_errors splits defs =
| P_not p ->
(* todo: not sure that I can't split - but can't figure out how at
* the moment *)
- raise (Reporting_basic.err_general l
+ raise (Reporting.err_general l
("Cannot split on 'not' pattern"))
| P_as (p',id) when id_match id <> None ->
- raise (Reporting_basic.err_general l
+ raise (Reporting.err_general l
("Cannot split " ^ string_of_id id ^ " on 'as' pattern"))
| P_as (p',id) ->
re (fun p -> P_as (p,id)) p'
@@ -1907,7 +1907,7 @@ let split_defs all_errors splits defs =
match args with
| [P_aux (P_var (_, TP_aux (TP_var kid, _)),ann)] -> kid,ann
| _ ->
- raise (Reporting_basic.err_general l
+ raise (Reporting.err_general l
"Pattern match not currently supported by monomorphisation")
in
let map_inst (insts,id',_) =
@@ -1941,7 +1941,7 @@ let split_defs all_errors splits defs =
let overlap = List.exists (fun (v,_) -> List.mem v pvs) lvs in
let () =
if overlap then
- Reporting_basic.print_err false true l "Monomorphisation"
+ Reporting.print_err false true l "Monomorphisation"
"Splitting a singleton pattern is not possible"
in p
in
@@ -1949,7 +1949,7 @@ let split_defs all_errors splits defs =
let check_split_size lst l =
let size = List.length lst in
if size > size_set_limit then
- let open Reporting_basic in
+ let open Reporting in
let error =
Err_general (l, "Case split is too large (" ^ string_of_int size ^
" > limit " ^ string_of_int size_set_limit ^ ")")
@@ -2184,9 +2184,9 @@ let rec sizes_of_typ (Typ_aux (t,l)) =
| Typ_id _
| Typ_var _
-> KidSet.empty
- | Typ_fn _ -> raise (Reporting_basic.err_general l
+ | Typ_fn _ -> raise (Reporting.err_general l
"Function type on expression")
- | Typ_bidir _ -> raise (Reporting_basic.err_general l "Mapping type on expression")
+ | Typ_bidir _ -> raise (Reporting.err_general l "Mapping type on expression")
| Typ_tup typs -> kidset_bigunion (List.map sizes_of_typ typs)
| Typ_exist (kids,_,typ) ->
List.fold_left (fun s k -> KidSet.remove k s) (sizes_of_typ typ) kids
@@ -2221,7 +2221,7 @@ let change_parameter_pat i = function
mk_id "==",
E_aux (E_lit lit,annot)), annot) in
P_aux (P_id var, (l,empty_tannot)), ([],[test])
- | P_aux (_,(l,_)) -> raise (Reporting_basic.err_unreachable l __POS__
+ | P_aux (_,(l,_)) -> raise (Reporting.err_unreachable l __POS__
"Expected variable pattern")
(* TODO: make more precise, preferably with a proper free variables function
@@ -2277,7 +2277,7 @@ let replace_with_the_value bound_nexps (E_aux (_,(l,_)) as exp) =
| Typ_aux (Typ_app (Id_aux (Id "atom",_),
[Typ_arg_aux (Typ_arg_nexp nexp,l')]),_) ->
mk_exp nexp l l'
- | _ -> raise (Reporting_basic.err_unreachable l __POS__
+ | _ -> raise (Reporting.err_unreachable l __POS__
"atom stopped being an atom?")
let replace_type env typ =
@@ -2291,7 +2291,7 @@ let replace_type env typ =
[Typ_arg_aux (Typ_arg_nexp nexp,l')]) ->
Typ_aux (Typ_app (Id_aux (Id "itself",Generated Unknown),
[Typ_arg_aux (Typ_arg_nexp nexp,l')]),Generated l)
- | _ -> raise (Reporting_basic.err_unreachable l __POS__
+ | _ -> raise (Reporting.err_unreachable l __POS__
"atom stopped being an atom?")
@@ -2305,7 +2305,7 @@ let rewrite_size_parameters env (Defs defs) =
let _, typ = Env.get_val_spec_orig id env in
let types = match typ with
| Typ_aux (Typ_fn (arg_typs,_,_),_) -> List.map (Env.expand_synonyms env) arg_typs
- | _ -> raise (Reporting_basic.err_unreachable l __POS__ "Function clause does not have a function type")
+ | _ -> raise (Reporting.err_unreachable l __POS__ "Function clause does not have a function type")
in
let add_parameter (i,nmap) typ =
let nmap =
@@ -2628,7 +2628,7 @@ let string_of_callerkidset s =
let string_of_dep = function
| Have (args,extras) ->
"Have (" ^ string_of_argsplits args ^ ";" ^ string_of_extra_splits extras ^ ")"
- | Unknown (l,msg) -> "Unknown " ^ msg ^ " at " ^ Reporting_basic.loc_to_string l
+ | Unknown (l,msg) -> "Unknown " ^ msg ^ " at " ^ Reporting.loc_to_string l
(* If a callee uses a type variable as a size, does it need to be split in the
current function, or is it also a parameter? (Note that there may be multiple
@@ -2902,8 +2902,8 @@ let refine_dependency env (E_aux (e,(l,annot)) as exp) pexps =
with
| Some pats ->
if l = Parse_ast.Unknown then
- (Reporting_basic.print_error
- (Reporting_basic.Err_general
+ (Reporting.print_error
+ (Reporting.Err_general
(l, "No location for pattern match: " ^ string_of_exp exp));
None)
else
@@ -3165,7 +3165,7 @@ let rec analyse_exp fn_id env assigns (E_aux (e,(l,annot)) as exp) =
| E_internal_plet _
| E_internal_return _
| E_internal_value _
- -> raise (Reporting_basic.err_unreachable l __POS__
+ -> raise (Reporting.err_unreachable l __POS__
("Unexpected expression encountered in monomorphisation: " ^ string_of_exp exp))
| E_var (lexp,e1,e2) ->
@@ -3500,7 +3500,7 @@ let print_result r =
let _ = print_endline (" kid_in_caller: " ^ string_of_callerkidset r.kid_in_caller) in
let _ = print_endline (" failures: \n " ^
(String.concat "\n "
- (List.map (fun (l,s) -> Reporting_basic.loc_to_string l ^ ":\n " ^
+ (List.map (fun (l,s) -> Reporting.loc_to_string l ^ ":\n " ^
String.concat "\n " (StringSet.elements s))
(Failures.bindings r.failures)))) in
()
@@ -3585,7 +3585,7 @@ let analyse_defs debug env (Defs defs) =
then (true,splits,extras) else
begin
Failures.iter (fun l msgs ->
- Reporting_basic.print_err false false l "Monomorphisation" (String.concat "\n" (StringSet.elements msgs)))
+ Reporting.print_err false false l "Monomorphisation" (String.concat "\n" (StringSet.elements msgs)))
fails;
(false, splits,extras)
end
@@ -3610,7 +3610,7 @@ let add_extra_splits extras (Defs defs) =
let loc = match Analysis.translate_loc l with
| Some l -> l
| None ->
- (Reporting_basic.print_err false false l "Monomorphisation"
+ (Reporting.print_err false false l "Monomorphisation"
"Internal error: bad location for added case";
("",0))
in
@@ -4134,7 +4134,7 @@ let add_bitvector_casts (Defs defs) =
match typ with
| Typ_aux (Typ_fn (_,ret,_),_) -> ret
| Typ_aux (_,l) as typ ->
- raise (Reporting_basic.err_unreachable l __POS__
+ raise (Reporting.err_unreachable l __POS__
("Function clause must have function type: " ^ string_of_typ typ ^
" is not a function type"))
in
@@ -4356,19 +4356,19 @@ let monomorphise opts splits defs =
let f,r,ex = Analysis.analyse_defs opts.debug_analysis env defs in
if f || opts.all_split_errors || opts.continue_anyway
then f, r, ex
- else raise (Reporting_basic.err_general Unknown "Unable to monomorphise program")
+ else raise (Reporting.err_general Unknown "Unable to monomorphise program")
else true, [], Analysis.ExtraSplits.empty in
let splits = new_splits @ (List.map (fun (loc,id) -> (loc,id,None)) splits) in
let ok_extras, defs, extra_splits = add_extra_splits extra_splits defs in
let splits = splits @ extra_splits in
let () = if ok_extras || opts.all_split_errors || opts.continue_anyway
then ()
- else raise (Reporting_basic.err_general Unknown "Unable to monomorphise program")
+ else raise (Reporting.err_general Unknown "Unable to monomorphise program")
in
let ok_split, defs = split_defs opts.all_split_errors splits defs in
let () = if (ok_analysis && ok_extras && ok_split) || opts.continue_anyway
then ()
- else raise (Reporting_basic.err_general Unknown "Unable to monomorphise program")
+ else raise (Reporting.err_general Unknown "Unable to monomorphise program")
in defs
let add_bitvector_casts = BitvectorSizeCasts.add_bitvector_casts
diff --git a/src/ocaml_backend.ml b/src/ocaml_backend.ml
index 77e3072b..3ad4c07f 100644
--- a/src/ocaml_backend.ml
+++ b/src/ocaml_backend.ml
@@ -121,7 +121,7 @@ let rec ocaml_string_typ (Typ_aux (typ_aux, l)) arg =
| Typ_bidir (t1, t2) -> string "\"BIDIR\""
| Typ_var kid -> string "\"VAR\""
| Typ_exist _ -> assert false
- | Typ_internal_unknown -> raise (Reporting_basic.err_unreachable l __POS__ "escaped Typ_internal_unknown")
+ | Typ_internal_unknown -> raise (Reporting.err_unreachable l __POS__ "escaped Typ_internal_unknown")
let ocaml_typ_id ctx = function
| id when Id.compare id (mk_id "string") = 0 -> string "string"
@@ -143,10 +143,10 @@ let rec ocaml_typ ctx (Typ_aux (typ_aux, l)) =
| Typ_app (id, typs) -> parens (separate_map (string ", ") (ocaml_typ_arg ctx) typs) ^^ space ^^ ocaml_typ_id ctx id
| Typ_tup typs -> parens (separate_map (string " * ") (ocaml_typ ctx) typs)
| Typ_fn (typs, typ, _) -> separate space [ocaml_typ ctx (Typ_aux (Typ_tup typs, l)); string "->"; ocaml_typ ctx typ]
- | Typ_bidir (t1, t2) -> raise (Reporting_basic.err_general l "Ocaml doesn't support bidir types")
+ | Typ_bidir (t1, t2) -> raise (Reporting.err_general l "Ocaml doesn't support bidir types")
| Typ_var kid -> zencode_kid kid
| Typ_exist _ -> assert false
- | Typ_internal_unknown -> raise (Reporting_basic.err_unreachable l __POS__ "escaped Typ_internal_unknown")
+ | Typ_internal_unknown -> raise (Reporting.err_unreachable l __POS__ "escaped Typ_internal_unknown")
and ocaml_typ_arg ctx (Typ_arg_aux (typ_arg_aux, _) as typ_arg) =
match typ_arg_aux with
| Typ_arg_typ typ -> ocaml_typ ctx typ
@@ -674,7 +674,7 @@ let ocaml_pp_generators ctx defs orig_types required =
if Bindings.mem id Type_check.Env.builtin_typs
then IdSet.add id required
else
- raise (Reporting_basic.err_unreachable (id_loc id) __POS__
+ raise (Reporting.err_unreachable (id_loc id) __POS__
("Required generator of unknown type " ^ string_of_id id))
and add_req_from_id required id =
if IdSet.mem id required then required
@@ -687,13 +687,13 @@ let ocaml_pp_generators ctx defs orig_types required =
| Typ_internal_unknown
| Typ_fn _
| Typ_bidir _
- -> raise (Reporting_basic.err_unreachable (typ_loc full_typ) __POS__
+ -> raise (Reporting.err_unreachable (typ_loc full_typ) __POS__
("Required generator for type that should not appear: " ^
string_of_typ full_typ))
| Typ_tup typs ->
List.fold_left add_req_from_typ required typs
| Typ_exist _ ->
- raise (Reporting_basic.err_todo (typ_loc full_typ)
+ raise (Reporting.err_todo (typ_loc full_typ)
("Generators for existential types not yet supported: " ^
string_of_typ full_typ))
| Typ_app (id,args) ->
@@ -714,7 +714,7 @@ let ocaml_pp_generators ctx defs orig_types required =
List.fold_left (fun req (Tu_aux (Tu_ty_id (typ,_),_)) ->
add_req_from_typ req typ) required variants
| TD_enum _ -> required
- | TD_bitfield _ -> raise (Reporting_basic.err_todo l "Generators for bitfields not yet supported")
+ | TD_bitfield _ -> raise (Reporting.err_todo l "Generators for bitfields not yet supported")
in
let required = IdSet.fold (fun id req -> always_add_req_from_id req id) required required in
let type_name id = zencode_string (string_of_id id) in
@@ -770,7 +770,7 @@ let ocaml_pp_generators ctx defs orig_types required =
let typ_str, args_pp = match typ with
| Typ_id id -> type_name id, [string "g"]
| Typ_app (id,args) -> type_name id, string "g"::List.map typearg args
- | _ -> raise (Reporting_basic.err_todo l
+ | _ -> raise (Reporting.err_todo l
("Unsupported type for generators: " ^ string_of_typ full_typ))
in
let args_pp = match args_pp with [] -> empty
@@ -783,7 +783,7 @@ let ocaml_pp_generators ctx defs orig_types required =
(match nexp with
| Nexp_constant c -> string (Big_int.to_string c) (* TODO: overflow *)
| Nexp_var v -> mk_arg v
- | _ -> raise (Reporting_basic.err_todo l
+ | _ -> raise (Reporting.err_todo l
("Unsupported nexp for generators: " ^ string_of_nexp full_nexp)))
| Typ_arg_order (Ord_aux (ord,_)) ->
(match ord with
@@ -797,7 +797,7 @@ let ocaml_pp_generators ctx defs orig_types required =
match typ with
| Typ_id id -> type_name id, []
| Typ_app (id,args) -> type_name id, List.map typearg args
- | _ -> raise (Reporting_basic.err_todo l
+ | _ -> raise (Reporting.err_todo l
("Unsupported type for generators: " ^ string_of_typ full_typ))
in
let args_pp = match args_pp with [] -> empty
@@ -860,7 +860,7 @@ let ocaml_pp_generators ctx defs orig_types required =
Some (separate_map (string ";" ^^ break 1) enum_constructor variants),
Some (separate_map (break 1) build_enum_constructor variants)
| _ ->
- raise (Reporting_basic.err_todo l "Generators for records and bitfields not yet supported")
+ raise (Reporting.err_todo l "Generators for records and bitfields not yet supported")
in
let name = type_name id in
let constructors_pp = match constructors with
diff --git a/src/parser.mly b/src/parser.mly
index 070dee50..bd7c2f62 100644
--- a/src/parser.mly
+++ b/src/parser.mly
@@ -175,7 +175,7 @@ let rec desugar_rchain chain s e =
/*Terminals with no content*/
-%token And As Assert Bitzero Bitone By Match Clause Dec Default Effect End Op Tuple Where
+%token And As Assert Bitzero Bitone By Match Clause Dec Default Effect End Op Where
%token Enum Else False Forall Foreach Overload Function_ Mapping If_ In Inc Let_ Int Order Cast
%token Pure Register Return Scattered Sizeof Struct Then True TwoCaret TYPE Typedef
%token Undefined Union Newtype With Val Constraint Throw Try Catch Exit Bitfield
diff --git a/src/pattern_completeness.ml b/src/pattern_completeness.ml
index d54bbd3f..514eb5c0 100644
--- a/src/pattern_completeness.ml
+++ b/src/pattern_completeness.ml
@@ -269,7 +269,7 @@ let combine ctx gpat (l, pat) =
(* This warning liable to false positives as join returns a
pattern that overapproximates what can match, so we only
report when the second match is a constructor. *)
- Util.warn (Printf.sprintf "Possible redundant pattern match at %s\n" (Reporting_basic.loc_to_string l));
+ Util.warn (Printf.sprintf "Possible redundant pattern match at %s\n" (Reporting.loc_to_string l));
GP_wild
| _, gpat' -> join ctx gpat gpat'
@@ -287,7 +287,7 @@ let shrink_loc = function
let check l ctx cases =
match cases_to_pats cases with
- | [] -> Util.warn (Printf.sprintf "No non-guarded patterns at %s\n" (Reporting_basic.loc_to_string (shrink_loc l)))
+ | [] -> Util.warn (Printf.sprintf "No non-guarded patterns at %s\n" (Reporting.loc_to_string (shrink_loc l)))
| (_, pat) :: pats ->
let top_pat = List.fold_left (combine ctx) (generalize ctx pat) pats in
if is_wild top_pat then
@@ -295,7 +295,7 @@ let check l ctx cases =
else
let message =
Printf.sprintf "Possible incomplete pattern match at %s\n\nMost general matched pattern is %s\n"
- (Reporting_basic.loc_to_string (shrink_loc l))
+ (Reporting.loc_to_string (shrink_loc l))
(string_of_gpat top_pat |> Util.cyan |> Util.clear)
in
Util.warn message
diff --git a/src/pretty_print_common.ml b/src/pretty_print_common.ml
index 1fb35158..6825259c 100644
--- a/src/pretty_print_common.ml
+++ b/src/pretty_print_common.ml
@@ -207,6 +207,7 @@ let doc_typ, doc_atomic_typ, doc_nexp, doc_nexp_constraint =
separate space [nexp_constraint nc1; string "&"; nexp_constraint nc2]
| NC_true -> string "true"
| NC_false -> string "false"
+ | NC_app (id, args) -> doc_id id ^^ parens (separate_map (comma ^^ space) nexp args)
(* expose doc_typ, doc_atomic_typ, doc_nexp and doc_nexp_constraint *)
in typ, atomic_typ, nexp, nexp_constraint
diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml
index 2810d0ee..66c13678 100644
--- a/src/pretty_print_coq.ml
+++ b/src/pretty_print_coq.ml
@@ -240,7 +240,7 @@ let doc_nexp ctx ?(skip_vars=KidSet.empty) nexp =
| Nexp_app (Id_aux (Id "abs_atom",_), [_])
-> parens (plussub nexp)
| _ ->
- raise (Reporting_basic.err_unreachable l __POS__
+ raise (Reporting.err_unreachable l __POS__
("cannot pretty-print nexp \"" ^ string_of_nexp nexp ^ "\""))
in atomic nexp
@@ -427,7 +427,7 @@ let doc_typ, doc_atomic_typ =
| Typ_id (Id_aux (Id "nat", _)) ->
(match maybe_expand_range_type ty with
| Some typ -> atomic_typ atyp_needed typ
- | None -> raise (Reporting_basic.err_unreachable l __POS__ "Bad range type"))
+ | None -> raise (Reporting.err_unreachable l __POS__ "Bad range type"))
| Typ_app(Id_aux (Id "implicit", _),_) ->
(string "Z")
| Typ_app(Id_aux (Id "atom", _), [Typ_arg_aux(Typ_arg_nexp n,_)]) ->
@@ -491,7 +491,7 @@ let doc_typ, doc_atomic_typ =
ampersand;
doc_arithfact ctx ~exists:kids ?extra:length_constraint_pp nc])
| _ ->
- raise (Reporting_basic.err_todo l
+ raise (Reporting.err_todo l
("Non-atom existential type not yet supported in Coq: " ^
string_of_typ ty))
end
@@ -584,8 +584,8 @@ let doc_lit (L_aux(lit,l)) =
let denom = Big_int.pow_int_positive 10 (String.length f) in
(Big_int.add (Big_int.mul (Big_int.of_string i) denom) (Big_int.of_string f), denom)
| _ ->
- raise (Reporting_basic.Fatal_error
- (Reporting_basic.Err_syntax_locn (l, "could not parse real literal"))) in
+ raise (Reporting.Fatal_error
+ (Reporting.Err_syntax_locn (l, "could not parse real literal"))) in
parens (separate space (List.map string [
"realFromFrac"; Big_int.to_string num; Big_int.to_string denom]))
@@ -720,34 +720,34 @@ let rec doc_pat ctxt apat_needed exists_as_pairs (P_aux (p,(l,annot)) as pat, ty
let el_typ =
match destruct_vector env typ with
| Some (_,_,t) -> t
- | None -> raise (Reporting_basic.err_unreachable l __POS__ "vector pattern doesn't have vector type")
+ | None -> raise (Reporting.err_unreachable l __POS__ "vector pattern doesn't have vector type")
in
let ppp = brackets (separate_map semi (fun p -> doc_pat ctxt true exists_as_pairs (p,el_typ)) pats) in
if apat_needed then parens ppp else ppp
| P_vector_concat pats ->
- raise (Reporting_basic.err_unreachable l __POS__
+ raise (Reporting.err_unreachable l __POS__
"vector concatenation patterns should have been removed before pretty-printing")
| P_tup pats ->
let typs = match typ with
| Typ_aux (Typ_tup typs, _) -> typs
- | _ -> raise (Reporting_basic.err_unreachable l __POS__ "tuple pattern doesn't have tuple type")
+ | _ -> raise (Reporting.err_unreachable l __POS__ "tuple pattern doesn't have tuple type")
in
(match pats, typs with
| [p], [typ'] -> doc_pat ctxt apat_needed exists_as_pairs (p, typ')
- | [_], _ -> raise (Reporting_basic.err_unreachable l __POS__ "tuple pattern length does not match tuple type length")
+ | [_], _ -> raise (Reporting.err_unreachable l __POS__ "tuple pattern length does not match tuple type length")
| _ -> parens (separate_map comma_sp (doc_pat ctxt false exists_as_pairs) (List.combine pats typs)))
| P_list pats ->
let el_typ = match typ with
| Typ_aux (Typ_app (f, [Typ_arg_aux (Typ_arg_typ el_typ,_)]),_)
when Id.compare f (mk_id "list") = 0 -> el_typ
- | _ -> raise (Reporting_basic.err_unreachable l __POS__ "list pattern not a list")
+ | _ -> raise (Reporting.err_unreachable l __POS__ "list pattern not a list")
in
brackets (separate_map semi (fun p -> doc_pat ctxt false true (p, el_typ)) pats)
| P_cons (p,p') ->
let el_typ = match typ with
| Typ_aux (Typ_app (f, [Typ_arg_aux (Typ_arg_typ el_typ,_)]),_)
when Id.compare f (mk_id "list") = 0 -> el_typ
- | _ -> raise (Reporting_basic.err_unreachable l __POS__ "list pattern not a list")
+ | _ -> raise (Reporting.err_unreachable l __POS__ "list pattern not a list")
in
doc_op (string "::") (doc_pat ctxt true true (p, el_typ)) (doc_pat ctxt true true (p', typ))
| P_string_append _ -> unreachable l __POS__
@@ -775,7 +775,7 @@ let typ_id_of (Typ_aux (typ, l)) = match typ with
| Typ_app (register, [Typ_arg_aux (Typ_arg_typ (Typ_aux (Typ_id id, _)), _)])
when string_of_id register = "register" -> id
| Typ_app (id, _) -> id
- | _ -> raise (Reporting_basic.err_unreachable l __POS__ "failed to get type id")
+ | _ -> raise (Reporting.err_unreachable l __POS__ "failed to get type id")
(* TODO: maybe Nexp_exp, division? *)
(* Evaluation of constant nexp subexpressions, because Coq will be able to do those itself *)
@@ -873,7 +873,7 @@ let general_typ_of_annot annot =
let general_typ_of (E_aux (_,annot)) = general_typ_of_annot annot
let prefix_recordtype = true
-let report = Reporting_basic.err_unreachable
+let report = Reporting.err_unreachable
let doc_exp, doc_let =
let rec top_exp (ctxt : context) (aexp_needed : bool)
(E_aux (e, (l,annot)) as full_exp) =
@@ -1002,7 +1002,7 @@ let doc_exp, doc_let =
| _ ->
liftR ((prefix 2 1) (string "write_reg") (doc_lexp_deref ctxt le ^/^ expY e)))
| E_vector_append(le,re) ->
- raise (Reporting_basic.err_unreachable l __POS__
+ raise (Reporting.err_unreachable l __POS__
"E_vector_append should have been rewritten before pretty-printing")
| E_cons(le,re) -> doc_op (group (colon^^colon)) (expY le) (expY re)
| E_if(c,t,e) ->
@@ -1036,11 +1036,11 @@ let doc_exp, doc_let =
| (P_aux (P_var (P_aux (P_id id, _), _), _))
| (P_aux (P_id id, _))), _), _),
body), _), _), _)), _)), _) -> id, body
- | _ -> raise (Reporting_basic.err_unreachable l __POS__ ("Unable to find loop variable in " ^ string_of_exp body)) in
+ | _ -> raise (Reporting.err_unreachable l __POS__ ("Unable to find loop variable in " ^ string_of_exp body)) in
let dir = match ord_exp with
| E_aux (E_lit (L_aux (L_false, _)), _) -> "_down"
| E_aux (E_lit (L_aux (L_true, _)), _) -> "_up"
- | _ -> raise (Reporting_basic.err_unreachable l __POS__ ("Unexpected loop direction " ^ string_of_exp ord_exp))
+ | _ -> raise (Reporting.err_unreachable l __POS__ ("Unexpected loop direction " ^ string_of_exp ord_exp))
in
let combinator = if effectful (effect_of body) then "foreach_ZM" else "foreach_Z" in
let combinator = combinator ^ dir in
@@ -1069,7 +1069,7 @@ let doc_exp, doc_let =
(prefix 2 1 (group body_lambda) (expN body))
)
)
- | _ -> raise (Reporting_basic.err_unreachable l __POS__
+ | _ -> raise (Reporting.err_unreachable l __POS__
"Unexpected number of arguments for loop combinator")
end
| Id_aux (Id (("while" | "until") as combinator), _) ->
@@ -1106,7 +1106,7 @@ let doc_exp, doc_let =
(parens (prefix 2 1 (group lambda) (expN cond)))
(parens (prefix 2 1 (group lambda) (expN body))))
)
- | _ -> raise (Reporting_basic.err_unreachable l __POS__
+ | _ -> raise (Reporting.err_unreachable l __POS__
"Unexpected number of arguments for loop combinator")
end
| Id_aux (Id "early_return", _) ->
@@ -1129,7 +1129,7 @@ let doc_exp, doc_let =
doc_atomic_typ ctxt false (typ_of exp)] in
true, doc_op colon epp tannot in
if aexp_needed then parens tepp else tepp
- | _ -> raise (Reporting_basic.err_unreachable l __POS__
+ | _ -> raise (Reporting.err_unreachable l __POS__
"Unexpected number of arguments for early_return builtin")
end
| _ ->
@@ -1143,7 +1143,7 @@ let doc_exp, doc_let =
let (tqs,fn_ty) = Env.get_val_spec_orig f env in
let arg_typs, ret_typ, eff = match fn_ty with
| Typ_aux (Typ_fn (arg_typs,ret_typ,eff),_) -> arg_typs, ret_typ, eff
- | _ -> raise (Reporting_basic.err_unreachable l __POS__ "Function not a function type")
+ | _ -> raise (Reporting.err_unreachable l __POS__ "Function not a function type")
in
let inst =
match instantiation_of_without_type full_exp with
@@ -1244,10 +1244,10 @@ let doc_exp, doc_let =
liftR (if aexp_needed then parens (align epp) else epp)
end
| E_vector_access (v,e) ->
- raise (Reporting_basic.err_unreachable l __POS__
+ raise (Reporting.err_unreachable l __POS__
"E_vector_access should have been rewritten before pretty-printing")
| E_vector_subrange (v,e1,e2) ->
- raise (Reporting_basic.err_unreachable l __POS__
+ raise (Reporting.err_unreachable l __POS__
"E_vector_subrange should have been rewritten before pretty-printing")
| E_field((E_aux(_,(l,fannot)) as fexp),id) ->
(match destruct_tannot fannot with
@@ -1402,7 +1402,7 @@ let doc_exp, doc_let =
let t = Env.base_typ_of (env_of full_exp) (typ_of full_exp) in
let start, (len, order, etyp) =
if is_vector_typ t then vector_start_index t, vector_typ_args_of t
- else raise (Reporting_basic.err_unreachable l __POS__
+ else raise (Reporting.err_unreachable l __POS__
"E_vector of non-vector type") in
let dir,dir_out = if is_order_inc order then (true,"true") else (false, "false") in
let expspp =
@@ -1427,10 +1427,10 @@ let doc_exp, doc_let =
(vepp,aexp_needed) in
if aexp_needed then parens (align epp) else epp
| E_vector_update(v,e1,e2) ->
- raise (Reporting_basic.err_unreachable l __POS__
+ raise (Reporting.err_unreachable l __POS__
"E_vector_update should have been rewritten before pretty-printing")
| E_vector_update_subrange(v,e1,e2,e3) ->
- raise (Reporting_basic.err_unreachable l __POS__
+ raise (Reporting.err_unreachable l __POS__
"E_vector_update should have been rewritten before pretty-printing")
| E_list exps ->
brackets (separate_map semi (expN) exps)
@@ -1451,7 +1451,7 @@ let doc_exp, doc_let =
(string "end)")) in
if aexp_needed then parens (align epp) else align epp
else
- raise (Reporting_basic.err_todo l "Warning: try-block around pure expression")
+ raise (Reporting.err_todo l "Warning: try-block around pure expression")
| E_throw e ->
let epp = liftR (separate space [string "throw"; expY e]) in
if aexp_needed then parens (align epp) else align epp
@@ -1460,7 +1460,7 @@ let doc_exp, doc_let =
let epp = liftR (separate space [string "assert_exp"; expY e1; expY e2]) in
if aexp_needed then parens (align epp) else align epp
| E_app_infix (e1,id,e2) ->
- raise (Reporting_basic.err_unreachable l __POS__
+ raise (Reporting.err_unreachable l __POS__
"E_app_infix should have been rewritten before pretty-printing")
| E_var(lexp, eq_exp, in_exp) ->
raise (report l __POS__ "E_vars should have been removed before pretty-printing")
@@ -1548,7 +1548,7 @@ let doc_exp, doc_let =
(match nexp_simp nexp with
| Nexp_aux (Nexp_constant i, _) -> doc_lit (L_aux (L_num i, l))
| _ ->
- raise (Reporting_basic.err_unreachable l __POS__
+ raise (Reporting.err_unreachable l __POS__
"pretty-printing non-constant sizeof expressions to Lem not supported"))
| E_return r ->
let ret_monad = " : MR" in
@@ -1567,7 +1567,7 @@ let doc_exp, doc_let =
align (parens (string "early_return" ^//^ exp_pp ^//^ ta))
| E_constraint nc -> wrap_parens (doc_nc_exp ctxt nc)
| E_internal_value _ ->
- raise (Reporting_basic.err_unreachable l __POS__
+ raise (Reporting.err_unreachable l __POS__
"unsupported internal expression encountered while pretty-printing")
and if_exp ctxt (elseif : bool) c t e =
let if_pp = string (if elseif then "else if" else "if") in
@@ -1620,7 +1620,7 @@ let doc_exp, doc_let =
group (prefix 3 1 (separate space [pipe; doc_pat ctxt false false (pat,typ);bigarrow])
(group (top_exp ctxt false e)))
| Pat_aux(Pat_when(_,_,_),(l,_)) ->
- raise (Reporting_basic.err_unreachable l __POS__
+ raise (Reporting.err_unreachable l __POS__
"guarded pattern expression should have been rewritten before pretty-printing")
and doc_lexp_deref ctxt ((LEXP_aux(lexp,(l,annot)))) = match lexp with
@@ -1630,7 +1630,7 @@ let doc_exp, doc_let =
| LEXP_cast (typ,id) -> doc_id (append_id id "_ref")
| LEXP_tup lexps -> parens (separate_map comma_sp (doc_lexp_deref ctxt) lexps)
| _ ->
- raise (Reporting_basic.err_unreachable l __POS__ ("doc_lexp_deref: Unsupported lexp"))
+ raise (Reporting.err_unreachable l __POS__ ("doc_lexp_deref: Unsupported lexp"))
(* expose doc_exp and doc_let *)
in top_exp, let_exp
@@ -1698,7 +1698,7 @@ let doc_typdef (TD_aux(td, (l, annot))) = match td with
match nexp_simp start with
| Nexp_aux (Nexp_constant i, _) -> (i, is_order_inc ord)
| _ ->
- raise (Reporting_basic.err_unreachable Parse_ast.Unknown __POS__
+ raise (Reporting.err_unreachable Parse_ast.Unknown __POS__
("register " ^ string_of_id id ^ " has non-constant start index " ^ string_of_nexp start))
with
| _ -> (Big_int.zero, true) in
@@ -1759,7 +1759,7 @@ let doc_typdef (TD_aux(td, (l, annot))) = match td with
string "forall (x y : " ^^ id_pp ^^ string "), Decidable (x = y) :=" ^/^
string "Decidable_eq_from_dec " ^^ id_pp ^^ string "_eq_dec." in
typ_pp ^^ dot ^^ hardline ^^ eq1_pp ^^ hardline ^^ eq2_pp ^^ hardline)
- | _ -> raise (Reporting_basic.err_unreachable l __POS__ "register with non-constant indices")
+ | _ -> raise (Reporting.err_unreachable l __POS__ "register with non-constant indices")
let args_of_typ l env typs =
let arg i typ =
@@ -1888,7 +1888,7 @@ let merge_kids_atoms pats =
| Some (Nexp_aux (Nexp_var kid,l)) ->
if KidSet.mem kid seen then
let () =
- Reporting_basic.print_err false true l "merge_kids_atoms"
+ Reporting.print_err false true l "merge_kids_atoms"
("want to merge tyvar and argument for " ^ string_of_kid kid ^
" but rearranging arguments isn't supported yet") in
gone,map,seen
@@ -2021,7 +2021,7 @@ let doc_funcl (FCL_aux(FCL_Funcl(id, pexp), annot)) =
let _ = match guard with
| None -> ()
| _ ->
- raise (Reporting_basic.err_unreachable l __POS__
+ raise (Reporting.err_unreachable l __POS__
"guarded pattern expression should have been rewritten before pretty-printing") in
let bodypp = doc_fun_body ctxt exp in
let bodypp = if effectful eff || not build_ex then bodypp else string "build_ex" ^^ parens bodypp in
@@ -2076,8 +2076,8 @@ let doc_dec (DEC_aux (reg, ((l, _) as annot))) =
string o;
string "[]"]))
^/^ hardline
- else raise (Reporting_basic.err_unreachable l __POS__ ("can't deal with register type " ^ string_of_typ typ))
- else raise (Reporting_basic.err_unreachable l __POS__ ("can't deal with register type " ^ string_of_typ typ)) *)
+ else raise (Reporting.err_unreachable l __POS__ ("can't deal with register type " ^ string_of_typ typ))
+ else raise (Reporting.err_unreachable l __POS__ ("can't deal with register type " ^ string_of_typ typ)) *)
| DEC_config _ -> empty
| DEC_alias(id,alspec) -> empty
| DEC_typ_alias(typ,id,alspec) -> empty
@@ -2094,7 +2094,7 @@ let is_field_accessor regtypes fdef =
let doc_regtype_fields (tname, (n1, n2, fields)) =
let i1, i2 = match n1, n2 with
| Nexp_aux(Nexp_constant i1,_),Nexp_aux(Nexp_constant i2,_) -> i1, i2
- | _ -> raise (Reporting_basic.err_typ Parse_ast.Unknown
+ | _ -> raise (Reporting.err_typ Parse_ast.Unknown
("Non-constant indices in register type " ^ tname)) in
let dir_b = i1 < i2 in
let dir = (if dir_b then "true" else "false") in
@@ -2102,7 +2102,7 @@ let doc_regtype_fields (tname, (n1, n2, fields)) =
let i, j = match fr with
| BF_aux (BF_single i, _) -> (i, i)
| BF_aux (BF_range (i, j), _) -> (i, j)
- | _ -> raise (Reporting_basic.err_unreachable Parse_ast.Unknown __POS__
+ | _ -> raise (Reporting.err_unreachable Parse_ast.Unknown __POS__
("Unsupported type in field " ^ string_of_id fid ^ " of " ^ tname)) in
let fsize = Big_int.succ (Big_int.abs (Big_int.sub i j)) in
(* TODO Assumes normalised, decreasing bitvector slices; however, since
@@ -2184,7 +2184,7 @@ let doc_val pat exp =
id, None
| P_aux (P_typ (typ, P_aux (P_var (P_aux (P_id id, _), TP_aux (TP_var kid, _)),_)),_) when Id.compare id (id_of_kid kid) == 0 ->
id, Some typ
- | _ -> raise (Reporting_basic.err_todo (pat_loc pat)
+ | _ -> raise (Reporting.err_todo (pat_loc pat)
"Top-level value definition with complex pattern not supported for Coq yet")
in
let typpp = match pat_typ with
@@ -2272,7 +2272,7 @@ try
let register_refs = State.register_refs_coq (State.find_registers defs) in
let unimplemented = find_unimplemented defs in
let () = if !opt_undef_axioms || IdSet.is_empty unimplemented then () else
- Reporting_basic.print_err false false Parse_ast.Unknown "Warning"
+ Reporting.print_err false false Parse_ast.Unknown "Warning"
("The following functions were declared but are undefined:\n" ^
String.concat "\n" (List.map string_of_id (IdSet.elements unimplemented)))
in
@@ -2316,4 +2316,4 @@ with Type_check.Type_error (l,err) ->
then "\n" ^ Printexc.get_backtrace ()
else "(backtracing unavailable)"
in
- raise (Reporting_basic.err_typ l (Type_error.string_of_type_error err ^ extra))
+ raise (Reporting.err_typ l (Type_error.string_of_type_error err ^ extra))
diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml
index 68825c8f..15d945ac 100644
--- a/src/pretty_print_lem.ml
+++ b/src/pretty_print_lem.ml
@@ -194,7 +194,7 @@ let doc_nexp_lem nexp =
| Nexp_exp n -> "exp_" ^ mangle_nexp n
| Nexp_neg n -> "neg_" ^ mangle_nexp n
| _ ->
- raise (Reporting_basic.err_unreachable l __POS__
+ raise (Reporting.err_unreachable l __POS__
("cannot pretty-print nexp \"" ^ string_of_nexp full_nexp ^ "\""))
end in
string ("'" ^ mangle_nexp full_nexp)
@@ -240,8 +240,8 @@ let rec lem_nexps_of_typ (Typ_aux (t,l)) =
List.fold_left (fun s ta -> NexpSet.union s (lem_nexps_of_typ_arg ta))
NexpSet.empty tas
| Typ_exist (kids,_,t) -> trec t
- | Typ_bidir _ -> raise (Reporting_basic.err_unreachable l __POS__ "Lem doesn't support bidir types")
- | Typ_internal_unknown -> raise (Reporting_basic.err_unreachable l __POS__ "escaped Typ_internal_unknown")
+ | Typ_bidir _ -> raise (Reporting.err_unreachable l __POS__ "Lem doesn't support bidir types")
+ | Typ_internal_unknown -> raise (Reporting.err_unreachable l __POS__ "escaped Typ_internal_unknown")
and lem_nexps_of_typ_arg (Typ_arg_aux (ta,_)) =
match ta with
| Typ_arg_nexp nexp -> NexpSet.singleton (nexp_simp (orig_nexp nexp))
@@ -283,7 +283,7 @@ let doc_typ_lem, doc_atomic_typ_lem =
(* (match nexp_simp m with
| (Nexp_aux(Nexp_constant i,_)) -> string "bitvector ty" ^^ doc_int i
| (Nexp_aux(Nexp_var _, _)) -> separate space [string "bitvector"; doc_nexp m]
- | _ -> raise (Reporting_basic.err_unreachable l __POS__
+ | _ -> raise (Reporting.err_unreachable l __POS__
"cannot pretty-print bitvector type with non-constant length")) *)
| _ -> string "list" ^^ space ^^ typ elem_typ in
if atyp_needed then parens tpp else tpp
@@ -318,7 +318,7 @@ let doc_typ_lem, doc_atomic_typ_lem =
let visible_vars = lem_tyvars_of_typ ty in
match List.filter (fun kid -> KidSet.mem kid visible_vars) kids with
| [] -> if atyp_needed then parens tpp else tpp
- | bad -> raise (Reporting_basic.err_general l
+ | bad -> raise (Reporting.err_general l
("Existential type variable(s) " ^
String.concat ", " (List.map string_of_kid bad) ^
" escape into Lem"))
@@ -405,8 +405,8 @@ let doc_lit_lem (L_aux(lit,l)) =
let denom = Big_int.pow_int_positive 10 (String.length f) in
(Big_int.add (Big_int.mul (Big_int.of_string i) denom) (Big_int.of_string f), denom)
| _ ->
- raise (Reporting_basic.Fatal_error
- (Reporting_basic.Err_syntax_locn (l, "could not parse real literal"))) in
+ raise (Reporting.Fatal_error
+ (Reporting.Err_syntax_locn (l, "could not parse real literal"))) in
parens (separate space (List.map string [
"realFromFrac"; Big_int.to_string num; Big_int.to_string denom]))
@@ -513,7 +513,7 @@ let rec doc_pat_lem ctxt apat_needed (P_aux (p,(l,annot)) as pa) = match p with
let ppp = brackets (separate_map semi (doc_pat_lem ctxt true) pats) in
if apat_needed then parens ppp else ppp
| P_vector_concat pats ->
- raise (Reporting_basic.err_unreachable l __POS__
+ raise (Reporting.err_unreachable l __POS__
"vector concatenation patterns should have been removed before pretty-printing")
| P_tup pats ->
(match pats with
@@ -556,10 +556,10 @@ let typ_id_of (Typ_aux (typ, l)) = match typ with
| Typ_app (register, [Typ_arg_aux (Typ_arg_typ (Typ_aux (Typ_id id, _)), _)])
when string_of_id register = "register" -> id
| Typ_app (id, _) -> id
- | _ -> raise (Reporting_basic.err_unreachable l __POS__ "failed to get type id")
+ | _ -> raise (Reporting.err_unreachable l __POS__ "failed to get type id")
let prefix_recordtype = true
-let report = Reporting_basic.err_unreachable
+let report = Reporting.err_unreachable
let doc_exp_lem, doc_let_lem =
let rec top_exp (ctxt : context) (aexp_needed : bool)
(E_aux (e, (l,annot)) as full_exp) =
@@ -632,7 +632,7 @@ let doc_exp_lem, doc_let_lem =
| _ ->
liftR ((prefix 2 1) (string "write_reg") (doc_lexp_deref_lem ctxt le ^/^ expY e)))
| E_vector_append(le,re) ->
- raise (Reporting_basic.err_unreachable l __POS__
+ raise (Reporting.err_unreachable l __POS__
"E_vector_append should have been rewritten before pretty-printing")
| E_cons(le,re) -> doc_op (group (colon^^colon)) (expY le) (expY re)
| E_if(c,t,e) -> wrap_parens (align (if_exp ctxt false c t e))
@@ -663,7 +663,7 @@ let doc_exp_lem, doc_let_lem =
| (P_aux (P_var (P_aux (P_id id, _), _), _))
| (P_aux (P_id id, _))), _), _),
body), _), _), _)), _)), _) -> id, body
- | _ -> raise (Reporting_basic.err_unreachable l __POS__ ("Unable to find loop variable in " ^ string_of_exp body)) in
+ | _ -> raise (Reporting.err_unreachable l __POS__ ("Unable to find loop variable in " ^ string_of_exp body)) in
let step = match ord_exp with
| E_aux (E_lit (L_aux (L_false, _)), _) ->
parens (separate space [string "integerNegate"; expY exp3])
@@ -694,7 +694,7 @@ let doc_exp_lem, doc_let_lem =
(prefix 2 1 (group body_lambda) (expN body))
)
)
- | _ -> raise (Reporting_basic.err_unreachable l __POS__
+ | _ -> raise (Reporting.err_unreachable l __POS__
"Unexpected number of arguments for loop combinator")
end
| Id_aux (Id (("while" | "until") as combinator), _) ->
@@ -731,7 +731,7 @@ let doc_exp_lem, doc_let_lem =
(parens (prefix 2 1 (group lambda) (expN cond)))
(parens (prefix 2 1 (group lambda) (expN body))))
)
- | _ -> raise (Reporting_basic.err_unreachable l __POS__
+ | _ -> raise (Reporting.err_unreachable l __POS__
"Unexpected number of arguments for loop combinator")
end
| Id_aux (Id "early_return", _) ->
@@ -751,7 +751,7 @@ let doc_exp_lem, doc_let_lem =
| _ -> aexp_needed, epp
in
if aexp_needed then parens tepp else tepp
- | _ -> raise (Reporting_basic.err_unreachable l __POS__
+ | _ -> raise (Reporting.err_unreachable l __POS__
"Unexpected number of arguments for early_return builtin")
end
| _ ->
@@ -787,10 +787,10 @@ let doc_exp_lem, doc_let_lem =
end
end
| E_vector_access (v,e) ->
- raise (Reporting_basic.err_unreachable l __POS__
+ raise (Reporting.err_unreachable l __POS__
"E_vector_access should have been rewritten before pretty-printing")
| E_vector_subrange (v,e1,e2) ->
- raise (Reporting_basic.err_unreachable l __POS__
+ raise (Reporting.err_unreachable l __POS__
"E_vector_subrange should have been rewritten before pretty-printing")
| E_field((E_aux(_,(l,fannot)) as fexp),id) ->
let ft = typ_of_annot (l,fannot) in
@@ -847,7 +847,7 @@ let doc_exp_lem, doc_let_lem =
let t = Env.base_typ_of (env_of full_exp) (typ_of full_exp) in
let start, (len, order, etyp) =
if is_vector_typ t then vector_start_index t, vector_typ_args_of t
- else raise (Reporting_basic.err_unreachable l __POS__
+ else raise (Reporting.err_unreachable l __POS__
"E_vector of non-vector type") in
let dir,dir_out = if is_order_inc order then (true,"true") else (false, "false") in
let start = match nexp_simp start with
@@ -874,10 +874,10 @@ let doc_exp_lem, doc_let_lem =
else (epp,aexp_needed) in
if aexp_needed then parens (align epp) else epp
| E_vector_update(v,e1,e2) ->
- raise (Reporting_basic.err_unreachable l __POS__
+ raise (Reporting.err_unreachable l __POS__
"E_vector_update should have been rewritten before pretty-printing")
| E_vector_update_subrange(v,e1,e2,e3) ->
- raise (Reporting_basic.err_unreachable l __POS__
+ raise (Reporting.err_unreachable l __POS__
"E_vector_update should have been rewritten before pretty-printing")
| E_list exps ->
brackets (separate_map semi (expN) exps)
@@ -895,7 +895,7 @@ let doc_exp_lem, doc_let_lem =
(separate_map (break 1) (doc_case ctxt) pexps) ^/^
(string "end)")))
else
- raise (Reporting_basic.err_todo l "Warning: try-block around pure expression")
+ raise (Reporting.err_todo l "Warning: try-block around pure expression")
| E_throw e ->
align (liftR (separate space [string "throw"; expY e]))
| E_exit e -> liftR (separate space [string "exit"; expY e])
@@ -932,7 +932,7 @@ let doc_exp_lem, doc_let_lem =
(match nexp_simp nexp with
| Nexp_aux (Nexp_constant i, _) -> doc_lit_lem (L_aux (L_num i, l))
| _ ->
- raise (Reporting_basic.err_unreachable l __POS__
+ raise (Reporting.err_unreachable l __POS__
"pretty-printing non-constant sizeof expressions to Lem not supported"))
| E_return r ->
let ta =
@@ -948,7 +948,7 @@ let doc_exp_lem, doc_let_lem =
align (parens (string "early_return" ^//^ expV true r ^//^ ta))
| E_constraint _ -> string "true"
| E_internal_value _ ->
- raise (Reporting_basic.err_unreachable l __POS__
+ raise (Reporting.err_unreachable l __POS__
"unsupported internal expression encountered while pretty-printing")
and if_exp ctxt (elseif : bool) c t e =
let if_pp = string (if elseif then "else if" else "if") in
@@ -981,7 +981,7 @@ let doc_exp_lem, doc_let_lem =
group (prefix 3 1 (separate space [pipe; doc_pat_lem ctxt false pat;arrow])
(group (top_exp ctxt false e)))
| Pat_aux(Pat_when(_,_,_),(l,_)) ->
- raise (Reporting_basic.err_unreachable l __POS__
+ raise (Reporting.err_unreachable l __POS__
"guarded pattern expression should have been rewritten before pretty-printing")
and doc_lexp_deref_lem ctxt ((LEXP_aux(lexp,(l,annot))) as le) = match lexp with
@@ -991,7 +991,7 @@ let doc_exp_lem, doc_let_lem =
| LEXP_cast (typ,id) -> doc_id_lem (append_id id "_ref")
| LEXP_tup lexps -> parens (separate_map comma_sp (doc_lexp_deref_lem ctxt) lexps)
| _ ->
- raise (Reporting_basic.err_unreachable l __POS__ ("doc_lexp_deref_lem: Unsupported lexp"))
+ raise (Reporting.err_unreachable l __POS__ ("doc_lexp_deref_lem: Unsupported lexp"))
(* expose doc_exp_lem and doc_let *)
in top_exp, let_exp
@@ -1046,7 +1046,7 @@ let doc_typdef_lem (TD_aux(td, (l, annot))) = match td with
match nexp_simp start with
| Nexp_aux (Nexp_constant i, _) -> (i, is_order_inc ord)
| _ ->
- raise (Reporting_basic.err_unreachable Parse_ast.Unknown __POS__
+ raise (Reporting.err_unreachable Parse_ast.Unknown __POS__
("register " ^ string_of_id id ^ " has non-constant start index " ^ string_of_nexp start))
with
| _ -> (Big_int.zero, true) in
@@ -1226,7 +1226,7 @@ let doc_typdef_lem (TD_aux(td, (l, annot))) = match td with
fromInterpValuePP ^^ hardline ^^ hardline ^^
fromToInterpValuePP ^^ hardline
else empty)
- | _ -> raise (Reporting_basic.err_unreachable l __POS__ "register with non-constant indices")
+ | _ -> raise (Reporting.err_unreachable l __POS__ "register with non-constant indices")
let args_of_typs l env typs =
let arg i typ =
@@ -1288,7 +1288,7 @@ let doc_funcl_lem (FCL_aux(FCL_Funcl(id, pexp), annot)) =
let _ = match guard with
| None -> ()
| _ ->
- raise (Reporting_basic.err_unreachable l __POS__
+ raise (Reporting.err_unreachable l __POS__
"guarded pattern expression should have been rewritten before pretty-printing") in
group (prefix 3 1
(separate space [doc_id_lem id; patspp; equals])
@@ -1342,8 +1342,8 @@ let doc_dec_lem (DEC_aux (reg, ((l, _) as annot))) =
string o;
string "[]"]))
^/^ hardline
- else raise (Reporting_basic.err_unreachable l __POS__ ("can't deal with register type " ^ string_of_typ typ))
- else raise (Reporting_basic.err_unreachable l __POS__ ("can't deal with register type " ^ string_of_typ typ)) *)
+ else raise (Reporting.err_unreachable l __POS__ ("can't deal with register type " ^ string_of_typ typ))
+ else raise (Reporting.err_unreachable l __POS__ ("can't deal with register type " ^ string_of_typ typ)) *)
| DEC_alias(id,alspec) -> empty
| DEC_typ_alias(typ,id,alspec) -> empty
@@ -1369,7 +1369,7 @@ let is_field_accessor regtypes fdef =
let doc_regtype_fields (tname, (n1, n2, fields)) =
let i1, i2 = match n1, n2 with
| Nexp_aux(Nexp_constant i1,_),Nexp_aux(Nexp_constant i2,_) -> i1, i2
- | _ -> raise (Reporting_basic.err_typ Parse_ast.Unknown
+ | _ -> raise (Reporting.err_typ Parse_ast.Unknown
("Non-constant indices in register type " ^ tname)) in
let dir_b = i1 < i2 in
let dir = (if dir_b then "true" else "false") in
@@ -1377,7 +1377,7 @@ let doc_regtype_fields (tname, (n1, n2, fields)) =
let i, j = match fr with
| BF_aux (BF_single i, _) -> (i, i)
| BF_aux (BF_range (i, j), _) -> (i, j)
- | _ -> raise (Reporting_basic.err_unreachable Parse_ast.Unknown __POS__
+ | _ -> raise (Reporting.err_unreachable Parse_ast.Unknown __POS__
("Unsupported type in field " ^ string_of_id fid ^ " of " ^ tname)) in
let fsize = Big_int.succ (Big_int.abs (Big_int.sub i j)) in
(* TODO Assumes normalised, decreasing bitvector slices; however, since
diff --git a/src/pretty_print_sail.ml b/src/pretty_print_sail.ml
index 37c48220..7de4dd40 100644
--- a/src/pretty_print_sail.ml
+++ b/src/pretty_print_sail.ml
@@ -162,7 +162,7 @@ let rec doc_typ (Typ_aux (typ_aux, l)) =
separate space [doc_arg_typs typs; string "->"; doc_typ typ; string "effect"; ocaml_eff]
| Typ_bidir (typ1, typ2) ->
separate space [doc_typ typ1; string "<->"; doc_typ typ2]
- | Typ_internal_unknown -> raise (Reporting_basic.err_unreachable l __POS__ "escaped Typ_internal_unknown")
+ | Typ_internal_unknown -> raise (Reporting.err_unreachable l __POS__ "escaped Typ_internal_unknown")
and doc_typ_arg (Typ_arg_aux (ta_aux, _)) =
match ta_aux with
| Typ_arg_typ typ -> doc_typ typ
diff --git a/src/process_file.ml b/src/process_file.ml
index 2dfd9571..bb789d0a 100644
--- a/src/process_file.ml
+++ b/src/process_file.ml
@@ -65,7 +65,7 @@ let get_lexbuf f =
lexbuf, in_chan
let parse_file ?loc:(l=Parse_ast.Unknown) (f : string) : Parse_ast.defs =
- let open Reporting_basic in
+ let open Reporting in
try
let lexbuf, in_chan = get_lexbuf f in
begin
@@ -111,7 +111,7 @@ let cond_pragma l defs =
decr depth; push_def def; scan defs
| def :: defs ->
push_def def; scan defs
- | [] -> raise (Reporting_basic.err_general l "$ifdef or $ifndef never ended by $endif")
+ | [] -> raise (Reporting.err_general l "$ifdef or $ifndef never ended by $endif")
in
scan defs
@@ -123,19 +123,24 @@ let parseid_to_string (Parse_ast.Id_aux (id, _)) =
match id with
| Parse_ast.Id x | Parse_ast.DeIid x -> x
-let rec realise_union_anon_rec_types (Parse_ast.TD_variant (union_id, name_scm_opt, typq, _, flag) as orig_union) arms =
- match arms with
- | [] -> []
- | arm :: arms ->
- match arm with
- | (Parse_ast.Tu_aux ((Parse_ast.Tu_ty_id _), _)) -> (None, arm) :: realise_union_anon_rec_types orig_union arms
- | (Parse_ast.Tu_aux ((Parse_ast.Tu_ty_anon_rec (fields, id)), l)) ->
- let open Parse_ast in
- let record_str = "_" ^ parseid_to_string union_id ^ "_" ^ parseid_to_string id ^ "_record" in
- let record_id = Id_aux (Id record_str, Generated l) in
- let new_arm = Tu_aux ((Tu_ty_id ((ATyp_aux (ATyp_id record_id, Generated l)), id)), Generated l) in
- let new_rec_def = DEF_type (TD_aux (TD_record (record_id, name_scm_opt, typq, fields, flag), Generated l)) in
- (Some new_rec_def, new_arm) :: (realise_union_anon_rec_types orig_union arms)
+let rec realise_union_anon_rec_types orig_union arms =
+ match orig_union with
+ | Parse_ast.TD_variant (union_id, name_scm_opt, typq, _, flag) ->
+ begin match arms with
+ | [] -> []
+ | arm :: arms ->
+ match arm with
+ | (Parse_ast.Tu_aux ((Parse_ast.Tu_ty_id _), _)) -> (None, arm) :: realise_union_anon_rec_types orig_union arms
+ | (Parse_ast.Tu_aux ((Parse_ast.Tu_ty_anon_rec (fields, id)), l)) ->
+ let open Parse_ast in
+ let record_str = "_" ^ parseid_to_string union_id ^ "_" ^ parseid_to_string id ^ "_record" in
+ let record_id = Id_aux (Id record_str, Generated l) in
+ let new_arm = Tu_aux ((Tu_ty_id ((ATyp_aux (ATyp_id record_id, Generated l)), id)), Generated l) in
+ let new_rec_def = DEF_type (TD_aux (TD_record (record_id, name_scm_opt, typq, fields, flag), Generated l)) in
+ (Some new_rec_def, new_arm) :: (realise_union_anon_rec_types orig_union arms)
+ end
+ | _ ->
+ raise (Reporting.err_unreachable Parse_ast.Unknown __POS__ "Non union type-definition passed to realise_union_anon_rec_typs")
let rec preprocess opts = function
| [] -> []
@@ -149,11 +154,10 @@ let rec preprocess opts = function
let args = Str.split (Str.regexp " +") command in
Arg.parse_argv ~current:(ref 0) (Array.of_list ("sail" :: args)) opts (fun _ -> ()) "";
with
- | Arg.Bad message | Arg.Help message -> raise (Reporting_basic.err_general l message)
+ | Arg.Bad message | Arg.Help message -> raise (Reporting.err_general l message)
end;
preprocess opts defs
-
| Parse_ast.DEF_pragma ("ifndef", symbol, l) :: defs ->
let then_defs, else_defs, defs = cond_pragma l defs in
if not (StringSet.mem symbol !symbols) then
@@ -309,7 +313,7 @@ let output_lem filename libs defs =
open_output_with_check_unformatted (filename ^ ".lem") in
(Pretty_print.pp_defs_lem
(ot, base_imports)
- (o, base_imports @ (String.capitalize types_module :: libs))
+ (o, base_imports @ (String.capitalize_ascii types_module :: libs))
defs generated_line);
close_output_with_check ext_ot;
close_output_with_check ext_o;
@@ -378,7 +382,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) ->
- raise (Reporting_basic.err_typ l (Type_error.string_of_type_error err))
+ raise (Reporting.err_typ l (Type_error.string_of_type_error err))
let rewrite_ast = rewrite [("initial", Rewriter.rewrite_defs)]
let rewrite_undefined bitvectors = rewrite [("undefined", fun x -> Rewrites.rewrite_undefined bitvectors x)]
diff --git a/src/reporting_basic.ml b/src/reporting.ml
index a90c2bcd..fffae5a7 100644
--- a/src/reporting_basic.ml
+++ b/src/reporting.ml
@@ -189,7 +189,7 @@ let read_from_file_pos2 p1 p2 =
(* Destruct a location by splitting all the Internal strings except possibly the
last one into a string list and keeping only the last location *)
-let dest_loc (l : Parse_ast.l) : (Parse_ast.l * string list) =
+let dest_loc (l : Parse_ast.l) : (Parse_ast.l * string list) =
let rec aux acc l = match l with
| Parse_ast.Int(s, Some l') -> aux (s::acc) l'
| _ -> (l, acc)
@@ -207,12 +207,12 @@ let rec format_loc_aux ff l =
in
()
-let format_loc_source ff l =
- match dest_loc l with
- | (Parse_ast.Range (p1, p2), _) ->
+let format_loc_source ff l =
+ match dest_loc l with
+ | (Parse_ast.Range (p1, p2), _) ->
begin
let (s, multi_line) = read_from_file_pos2 p1 p2 in
- if multi_line then
+ if multi_line then
Format.fprintf ff " original input:\n%s\n" (Bytes.to_string s)
else
Format.fprintf ff " original input: \"%s\"\n" (Bytes.to_string s)
@@ -265,9 +265,12 @@ type error =
| 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"
+
let dest_err = function
| Err_general (l, m) -> ("Error", false, Loc l, m)
- | Err_unreachable (l, (file, line, _, _), m) -> ((Printf.sprintf "Internal error: Unreachable code (at \"%s\" line %d)" file line), false, Loc l, m)
+ | Err_unreachable (l, (file, line, _, _), m) ->
+ ((Printf.sprintf "Internal error: Unreachable code (at \"%s\" line %d)" file line), false, Loc l, m ^ issues)
| Err_todo (l, m) -> ("Todo" ^ m, false, Loc l, "")
| Err_syntax (p, m) -> ("Syntax error", false, Pos p, m)
| Err_syntax_locn (l, m) -> ("Syntax error", false, Loc l, m)
@@ -284,7 +287,7 @@ 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 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)
diff --git a/src/reporting_basic.mli b/src/reporting.mli
index 39ac32f0..a6878d6a 100644
--- a/src/reporting_basic.mli
+++ b/src/reporting.mli
@@ -50,7 +50,7 @@
(** Basic error reporting
- [Reporting_basic] contains functions to report errors and warnings.
+ [Reporting] contains functions to report errors and warnings.
It contains functions to print locations ([Parse_ast.l] and [Ast.l]) and lexing positions.
The main functionality is reporting errors. This is done by raising a
diff --git a/src/rewriter.ml b/src/rewriter.ml
index 3eb0ffe6..cf04eef4 100644
--- a/src/rewriter.ml
+++ b/src/rewriter.ml
@@ -319,8 +319,8 @@ let rewrite_exp rewriters (E_aux (exp,(l,annot)) as orig_exp) =
| E_assert(e1,e2) -> rewrap (E_assert(rewrite e1,rewrite e2))
| E_var (lexp, e1, e2) ->
rewrap (E_var (rewriters.rewrite_lexp rewriters lexp, rewriters.rewrite_exp rewriters e1, rewriters.rewrite_exp rewriters e2))
- | E_internal_return _ -> raise (Reporting_basic.err_unreachable l __POS__ "Internal return found before it should have been introduced")
- | E_internal_plet _ -> raise (Reporting_basic.err_unreachable l __POS__ " Internal plet found before it should have been introduced")
+ | E_internal_return _ -> raise (Reporting.err_unreachable l __POS__ "Internal return found before it should have been introduced")
+ | E_internal_plet _ -> raise (Reporting.err_unreachable l __POS__ " Internal plet found before it should have been introduced")
| _ -> rewrap exp
let rewrite_let rewriters (LB_aux(letbind,(l,annot))) =
@@ -358,7 +358,7 @@ let rewrite_def rewriters d = match d with
| DEF_fundef fdef -> DEF_fundef (rewriters.rewrite_fun rewriters fdef)
| DEF_internal_mutrec fdefs -> DEF_internal_mutrec (List.map (rewriters.rewrite_fun rewriters) fdefs)
| DEF_val letbind -> DEF_val (rewriters.rewrite_let rewriters letbind)
- | DEF_scattered _ -> raise (Reporting_basic.err_unreachable Parse_ast.Unknown __POS__ "DEF_scattered survived to rewritter")
+ | DEF_scattered _ -> raise (Reporting.err_unreachable Parse_ast.Unknown __POS__ "DEF_scattered survived to rewritter")
let rewrite_defs_base rewriters (Defs defs) =
let rec rewrite ds = match ds with
diff --git a/src/rewrites.ml b/src/rewrites.ml
index 313d30e5..25d1467f 100644
--- a/src/rewrites.ml
+++ b/src/rewrites.ml
@@ -169,16 +169,16 @@ let vector_string_to_bit_list l lit =
| 'D' -> ['1';'1';'0';'1']
| 'E' -> ['1';'1';'1';'0']
| 'F' -> ['1';'1';'1';'1']
- | _ -> raise (Reporting_basic.err_unreachable l __POS__ "hexchar_to_binlist given unrecognized character") in
+ | _ -> raise (Reporting.err_unreachable l __POS__ "hexchar_to_binlist given unrecognized character") in
let s_bin = match lit with
| L_hex s_hex -> List.flatten (List.map hexchar_to_binlist (explode (String.uppercase_ascii s_hex)))
| L_bin s_bin -> explode s_bin
- | _ -> raise (Reporting_basic.err_unreachable l __POS__ "s_bin given non vector literal") in
+ | _ -> raise (Reporting.err_unreachable l __POS__ "s_bin given non vector literal") in
List.map (function '0' -> L_aux (L_zero, gen_loc l)
| '1' -> L_aux (L_one, gen_loc l)
- | _ -> raise (Reporting_basic.err_unreachable (gen_loc l) __POS__ "binary had non-zero or one")) s_bin
+ | _ -> raise (Reporting.err_unreachable (gen_loc l) __POS__ "binary had non-zero or one")) s_bin
let find_used_vars exp =
(* Overapproximates the set of used identifiers, but for the use cases below
@@ -461,7 +461,7 @@ let rewrite_sizeof (Defs defs) =
let inst =
try instantiation_of orig_exp with
| Type_error (l, err) ->
- raise (Reporting_basic.err_typ l (Type_error.string_of_type_error err)) in
+ 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 *)
let inst = KBindings.fold (fun kid uvar b -> KBindings.add (orig_kid kid) uvar b) inst KBindings.empty in
@@ -474,13 +474,13 @@ let rewrite_sizeof (Defs defs) =
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) ->
- raise (Reporting_basic.err_typ l (Type_error.string_of_type_error 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
a variable in scope. It can't be an existential because the assert rules that out. *)
| None -> annot_exp (E_id (id_of_kid (orig_kid kid))) l env (atom_typ (nvar (orig_kid kid)))
| _ ->
- raise (Reporting_basic.err_unreachable l __POS__
+ raise (Reporting.err_unreachable l __POS__
("failed to infer nexp for type variable " ^ string_of_kid kid ^
" of function " ^ string_of_id f))
end in
@@ -605,10 +605,10 @@ let rewrite_sizeof (Defs defs) =
| P_as (_, id) | P_id id ->
(* adding parameters here would change the type of id;
we should remove the P_as/P_id here and add a let-binding to the body *)
- raise (Reporting_basic.err_todo l
+ raise (Reporting.err_todo l
"rewriting as- or id-patterns for sizeof expressions not yet implemented")
| _ ->
- raise (Reporting_basic.err_unreachable l __POS__
+ raise (Reporting.err_unreachable l __POS__
"unexpected pattern while rewriting function parameters for sizeof expressions"))
| ptyp ->
let ptyp' = Typ_aux (Typ_tup (kid_typs @ [ptyp]), l) in
@@ -661,7 +661,7 @@ let rewrite_sizeof (Defs defs) =
| Typ_aux (Typ_fn (vtyp_args, vtyp_ret, declared_eff), vl) ->
Typ_aux (Typ_fn (kid_typs @ vtyp_args, vtyp_ret, declared_eff), vl)
| _ ->
- raise (Reporting_basic.err_typ l "val spec with non-function type") in
+ raise (Reporting.err_typ l "val spec with non-function type") in
TypSchm_aux (TypSchm_ts (tq, typ'), l)
else ts in
match def with
@@ -758,7 +758,7 @@ let remove_vector_concat_pat pat =
P_aux (P_app (id, List.map aux pats), a)
| _ ->
raise
- (Reporting_basic.err_unreachable
+ (Reporting.err_unreachable
l __POS__ "name_vector_concat_elements: Non-vector in vector-concat pattern") in
P_vector_concat (List.map aux pats) in
{id_pat_alg with p_vector_concat = p_vector_concat} in
@@ -806,7 +806,7 @@ let remove_vector_concat_pat pat =
then Big_int.sub (Big_int.add start length) (Big_int.of_int 1)
else Big_int.add (Big_int.sub start length) (Big_int.of_int 1))
| _ ->
- raise (Reporting_basic.err_unreachable (fst rannot') __POS__
+ raise (Reporting.err_unreachable (fst rannot') __POS__
("unname_vector_concat_elements: vector of unspecified length in vector-concat pattern"))) in
let rec aux typ_opt (pos,pat_acc,decl_acc) (P_aux (p,cannot),is_last) =
let ctyp = Env.base_typ_of (env_of_annot cannot) (typ_of_annot cannot) in
@@ -820,7 +820,7 @@ let remove_vector_concat_pat pat =
if is_last then (pos,last_idx)
else
raise
- (Reporting_basic.err_unreachable
+ (Reporting.err_unreachable
l __POS__ ("unname_vector_concat_elements: vector of unspecified length in vector-concat pattern")) in
(match p with
(* if we see a named vector pattern, remove the name and remember to
@@ -930,7 +930,7 @@ let remove_vector_concat_pat pat =
| _, _ ->
(*if is_last then*) acc @ [wild Big_int.zero]
else raise
- (Reporting_basic.err_unreachable l __POS__
+ (Reporting.err_unreachable l __POS__
("remove_vector_concats: Non-vector in vector-concat pattern " ^
string_of_typ (typ_of_annot annot))) in
@@ -1160,7 +1160,7 @@ let rec pat_to_exp ((P_aux (pat,(l,annot))) as p_aux) =
let typ = typ_of_pat p_aux in
match pat with
| P_lit lit -> rewrap (E_lit lit)
- | P_wild -> raise (Reporting_basic.err_unreachable l __POS__
+ | P_wild -> raise (Reporting.err_unreachable l __POS__
"pat_to_exp given wildcard pattern")
| P_or(pat1, pat2) -> (* todo: insert boolean or *) pat_to_exp pat1
| P_not(pat) -> (* todo: insert boolean not *) pat_to_exp pat
@@ -1248,7 +1248,7 @@ let rewrite_guarded_clauses l cs =
| ((pat,guard,body,annot) as c) :: cs ->
group_aux (remove_wildcards "g__" pat, [c], annot) [] cs
| _ ->
- raise (Reporting_basic.err_unreachable l __POS__
+ raise (Reporting.err_unreachable l __POS__
"group given empty list in rewrite_guarded_clauses") in
let add_group cs groups = (if_pexp (groups @ fallthrough) cs) :: groups in
List.fold_right add_group groups []
@@ -1260,7 +1260,7 @@ let rewrite_guarded_clauses l cs =
let (Pat_aux (_,annot)) = pexp in
(pat, body, annot)
| [] ->
- raise (Reporting_basic.err_unreachable l __POS__
+ raise (Reporting.err_unreachable l __POS__
"if_pexp given empty list in rewrite_guarded_clauses"))
and if_exp fallthrough current_pat = (function
| (pat,guard,body,annot) :: ((pat',guard',body',annot') as c') :: cs ->
@@ -1284,7 +1284,7 @@ let rewrite_guarded_clauses l cs =
fix_eff_exp (annot_exp (E_if (exp,body,else_exp)) (fst annot) (env_of exp) (typ_of body))
| _, _ -> body)
| [] ->
- raise (Reporting_basic.err_unreachable l __POS__
+ raise (Reporting.err_unreachable l __POS__
"if_exp given empty list in rewrite_guarded_clauses")) in
group [] cs
@@ -1419,7 +1419,7 @@ let remove_bitvector_pat (P_aux (_, (l, _)) as pat) =
let start_idx = match start with
| Nexp_aux (Nexp_constant s, _) -> s
| _ ->
- raise (Reporting_basic.err_unreachable l __POS__
+ raise (Reporting.err_unreachable l __POS__
"guard_bitvector_pat called on pattern with non-constant start index") in
let add_bit_pat (idx, current, guards, dls) pat =
let idx' =
@@ -1727,9 +1727,9 @@ let rec rewrite_lexp_to_rhs ((LEXP_aux(lexp,((l,_) as annot))) as le) =
| Typ_aux (Typ_id rectyp_id, _) | Typ_aux (Typ_app (rectyp_id, _), _) when Env.is_record rectyp_id env ->
let field_update exp = FES_aux (FES_Fexps ([FE_aux (FE_Fexp (id, exp), annot)], false), annot) in
(lhs, (fun exp -> rhs (E_aux (E_record_update (lexp_to_exp lexp, field_update exp), lannot))))
- | _ -> raise (Reporting_basic.err_unreachable l __POS__ ("Unsupported lexp: " ^ string_of_lexp le))
+ | _ -> raise (Reporting.err_unreachable l __POS__ ("Unsupported lexp: " ^ string_of_lexp le))
end
- | _ -> raise (Reporting_basic.err_unreachable l __POS__ ("Unsupported lexp: " ^ string_of_lexp le))
+ | _ -> raise (Reporting.err_unreachable l __POS__ ("Unsupported lexp: " ^ string_of_lexp le))
let updates_vars exp =
let e_assign ((_, lexp), (u, exp)) =
@@ -2093,7 +2093,7 @@ let rewrite_defs_early_return (Defs defs) =
let swaptyp typ (l,tannot) = match destruct_tannot tannot with
| Some (env, typ', eff) -> (l, mk_tannot env typ eff)
- | _ -> raise (Reporting_basic.err_unreachable l __POS__ "swaptyp called with empty type annotation")
+ | _ -> raise (Reporting.err_unreachable l __POS__ "swaptyp called with empty type annotation")
let is_funcl_rec (FCL_aux (FCL_Funcl (id, pexp), _)) =
let pat,guard,exp,pannot = destruct_pexp pexp in
@@ -2174,7 +2174,7 @@ let rewrite_split_fun_constr_pats fun_name (Defs defs) =
let pat, _, exp, _ = destruct_pexp pexp in
env_of exp, typ_of_pat pat, typ_of exp
| _ ->
- raise (Reporting_basic.err_unreachable l __POS__
+ raise (Reporting.err_unreachable l __POS__
"rewrite_split_fun_constr_pats: empty auxiliary function")
in
let eff = List.fold_left
@@ -2242,7 +2242,7 @@ let rewrite_fix_val_specs (Defs defs) =
begin
try Env.get_val_spec id env with
| _ ->
- raise (Reporting_basic.err_unreachable (Parse_ast.Unknown) __POS__
+ raise (Reporting.err_unreachable (Parse_ast.Unknown) __POS__
("No val spec found for " ^ string_of_id id))
end
in
@@ -2570,7 +2570,7 @@ let rewrite_vector_concat_assignments defs =
begin
try check_exp env e_aux unit_typ with
| Type_error (l, err) ->
- raise (Reporting_basic.err_typ l (Type_error.string_of_type_error err))
+ raise (Reporting.err_typ l (Type_error.string_of_type_error err))
end
else E_aux (e_aux, annot)
| _ -> E_aux (e_aux, annot)
@@ -2596,7 +2596,7 @@ let rewrite_tuple_assignments defs =
begin
try check_exp env let_exp unit_typ with
| Type_error (l, err) ->
- raise (Reporting_basic.err_typ l (Type_error.string_of_type_error err))
+ raise (Reporting.err_typ l (Type_error.string_of_type_error err))
end
| _ -> E_aux (e_aux, annot)
in
@@ -2672,7 +2672,7 @@ let letbind (v : 'a exp) (body : 'a exp -> 'a exp) : 'a exp =
let body = body (annot_exp (E_id id) l env typ) in
fix_eff_exp (annot_exp (E_let (lb, body)) l env (typ_of body))
| None ->
- raise (Reporting_basic.err_unreachable l __POS__ "no type information")
+ raise (Reporting.err_unreachable l __POS__ "no type information")
let rec mapCont (f : 'b -> ('b -> 'a exp) -> 'a exp) (l : 'b list) (k : 'b list -> 'a exp) : 'a exp =
@@ -2968,7 +2968,7 @@ let rewrite_defs_internal_lets =
| LEXP_id id -> P_aux (P_id id, annot)
| LEXP_cast (typ, id) -> add_p_typ typ (P_aux (P_id id, annot))
| LEXP_tup lexps -> P_aux (P_tup (List.map pat_of_local_lexp lexps), annot)
- | _ -> raise (Reporting_basic.err_unreachable l __POS__ "unexpected local lexp") in
+ | _ -> raise (Reporting.err_unreachable l __POS__ "unexpected local lexp") in
let e_let (lb,body) =
match lb with
@@ -3834,7 +3834,7 @@ let rec rewrite_var_updates ((E_aux (expaux,((l,_) as annot))) as exp) =
let ord_exp, kids, constr, lower, upper, lower_exp, upper_exp =
match destruct_numeric env (typ_of exp1), destruct_numeric env (typ_of exp2) with
| None, _ | _, None ->
- raise (Reporting_basic.err_unreachable el __POS__ "Could not determine loop bounds")
+ raise (Reporting.err_unreachable el __POS__ "Could not determine loop bounds")
| Some (kids1, constr1, n1), Some (kids2, constr2, n2) ->
let kids = kids1 @ kids2 in
let constr = nc_and constr1 constr2 in
@@ -3940,7 +3940,7 @@ let rec rewrite_var_updates ((E_aux (expaux,((l,_) as annot))) as exp) =
let pannot = (l, mk_tannot (env_of exp) (typ_of exp) (effect_of exp)) in
Pat_aux (Pat_exp (pat, exp), pannot)
| Pat_when _ ->
- raise (Reporting_basic.err_unreachable l __POS__
+ raise (Reporting.err_unreachable l __POS__
"Guarded patterns should have been rewritten already") in
let ps = List.map rewrite_pexp ps in
let expaux = if is_case then E_case (e1, ps) else E_try (e1, ps) in
@@ -3954,7 +3954,7 @@ let rec rewrite_var_updates ((E_aux (expaux,((l,_) as annot))) as exp) =
| Local (_, typ) ->
add_p_typ typ (annot_pat (P_id id) pl env typ)
| _ ->
- raise (Reporting_basic.err_unreachable pl __POS__
+ raise (Reporting.err_unreachable pl __POS__
("Failed to look up type of variable " ^ string_of_id id)) in
if effectful exp then
Same_vars (E_aux (E_assign (lexp,vexp),annot))
@@ -4000,7 +4000,7 @@ let rec rewrite_var_updates ((E_aux (expaux,((l,_) as annot))) as exp) =
| LEXP_aux (LEXP_cast (typ, id), _) ->
unaux_pat (add_p_typ typ (annot_pat (P_id id) l env (typ_of v))), typ
| _ ->
- raise (Reporting_basic.err_unreachable l __POS__
+ raise (Reporting.err_unreachable l __POS__
"E_var with a lexp that is not a variable") in
let lb = fix_eff_lb (annot_letbind (paux, v) l env typ) in
let exp = fix_eff_exp (annot_exp (E_let (lb, body)) l env (typ_of body)) in
@@ -4553,7 +4553,7 @@ let rec remove_clause_from_pattern ctx (P_aux (rm_pat,ann)) res_pat =
in aux [] res_pats res_pats'
in
let inconsistent () =
- raise (Reporting_basic.err_unreachable (fst ann) __POS__
+ raise (Reporting.err_unreachable (fst ann) __POS__
("Inconsistency during exhaustiveness analysis with " ^
string_of_rp res_pat))
in
@@ -4637,12 +4637,12 @@ let rec remove_clause_from_pattern ctx (P_aux (rm_pat,ann)) res_pat =
rp' @ List.map (function [rp1;rp2] -> RP_cons (rp1,rp2) | _ -> assert false) res_pats
end
| P_record _ ->
- raise (Reporting_basic.err_unreachable (fst ann) __POS__
+ raise (Reporting.err_unreachable (fst ann) __POS__
"Record pattern not supported")
| P_vector _
| P_vector_concat _
| P_string_append _ ->
- raise (Reporting_basic.err_unreachable (fst ann) __POS__
+ raise (Reporting.err_unreachable (fst ann) __POS__
"Found pattern that should have been rewritten away in earlier stage")
(*in let _ = printprefix := String.sub (!printprefix) 0 (String.length !printprefix - 2)
@@ -4658,7 +4658,7 @@ let process_pexp env =
| Pat_aux (Pat_exp (p,_),_) ->
List.concat (List.map (remove_clause_from_pattern ctx p) rps)
| Pat_aux (Pat_when _,(l,_)) ->
- raise (Reporting_basic.err_unreachable l __POS__
+ raise (Reporting.err_unreachable l __POS__
"Guarded pattern should have been rewritten away")
(* We do some minimal redundancy checking to remove bogus wildcard patterns here *)
@@ -4666,7 +4666,7 @@ let check_cases process is_wild loc_of cases =
let rec aux rps acc = function
| [] -> acc, rps
| [p] when is_wild p && match rps with [] -> true | _ -> false ->
- let () = Reporting_basic.print_err false false
+ let () = Reporting.print_err false false
(loc_of p) "Match checking" "Redundant wildcard clause" in
acc, []
| h::t -> aux (process rps h) (h::acc) t
@@ -4706,7 +4706,7 @@ let rewrite_case (e,ann) =
let _ =
if !opt_coq_warn_nonexhaustive
- then Reporting_basic.print_err false false
+ then Reporting.print_err false false
(fst ann) "Non-exhaustive matching" ("Example: " ^ string_of_rp example) in
let l = Parse_ast.Generated Parse_ast.Unknown in
@@ -4726,7 +4726,7 @@ let rewrite_case (e,ann) =
| (example::_) ->
let _ =
if !opt_coq_warn_nonexhaustive
- then Reporting_basic.print_err false false
+ then Reporting.print_err false false
(fst ann) "Non-exhaustive let" ("Example: " ^ string_of_rp example) in
let l = Parse_ast.Generated Parse_ast.Unknown in
let p = P_aux (P_wild, (l, empty_tannot)) in
@@ -4742,7 +4742,7 @@ let rewrite_fun rewriters (FD_aux (FD_function (r,t,e,fcls),f_ann)) =
let id,fcl_ann =
match fcls with
| FCL_aux (FCL_Funcl (id,_),ann) :: _ -> id,ann
- | [] -> raise (Reporting_basic.err_unreachable (fst f_ann) __POS__
+ | [] -> raise (Reporting.err_unreachable (fst f_ann) __POS__
"Empty function")
in
let env = env_of_annot fcl_ann in
@@ -4756,7 +4756,7 @@ let rewrite_fun rewriters (FD_aux (FD_function (r,t,e,fcls),f_ann)) =
| (example::_) ->
let _ =
if !opt_coq_warn_nonexhaustive
- then Reporting_basic.print_err false false
+ then Reporting.print_err false false
(fst f_ann) "Non-exhaustive matching" ("Example: " ^ string_of_rp example) in
let l = Parse_ast.Generated Parse_ast.Unknown in
@@ -5021,12 +5021,12 @@ let rewrite_check_annot =
let typ1 = typ_of exp in
let typ2 = Env.expand_synonyms (env_of exp) (typ_of exp) in
(if not (alpha_equivalent (env_of exp) typ1 typ2)
- then raise (Reporting_basic.err_typ Parse_ast.Unknown
+ then raise (Reporting.err_typ Parse_ast.Unknown
("Found synonym in annotation " ^ string_of_typ typ1 ^ " vs " ^ string_of_typ typ2))
else ());
exp
with
- Type_error (l, err) -> raise (Reporting_basic.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 c1c965fe..4fd35902 100644
--- a/src/sail.ml
+++ b/src/sail.ml
@@ -373,6 +373,6 @@ let main() =
let _ = try
begin
try ignore(main ())
- with Failure(s) -> raise (Reporting_basic.err_general Parse_ast.Unknown ("Failure "^s))
+ with Failure(s) -> raise (Reporting.err_general Parse_ast.Unknown ("Failure "^s))
end
- with Reporting_basic.Fatal_error e -> Reporting_basic.report_error e
+ with Reporting.Fatal_error e -> Reporting.report_error e
diff --git a/src/spec_analysis.ml b/src/spec_analysis.ml
index 56c488ff..fd43de16 100644
--- a/src/spec_analysis.ml
+++ b/src/spec_analysis.ml
@@ -598,7 +598,7 @@ let def_of_component graph defset comp =
| DEF_fundef fundef -> [fundef]
| DEF_internal_mutrec fundefs -> fundefs
| _ ->
- raise (Reporting_basic.err_unreachable (def_loc def) __POS__
+ raise (Reporting.err_unreachable (def_loc def) __POS__
"Trying to merge non-function definition with mutually recursive functions") in
let fundefs = List.concat (List.map get_fundefs defs) in
print_dot graph (List.map (fun fd -> string_of_id (id_of_fundef fd)) fundefs);
diff --git a/src/state.ml b/src/state.ml
index 70e53a52..31f5c7eb 100644
--- a/src/state.ml
+++ b/src/state.ml
@@ -187,12 +187,12 @@ let rec regval_constr_id mwords (Typ_aux (t, l) as typ) = match t with
| Typ_arg_order (Ord_aux (Ord_inc, _)) -> "inc"
| Typ_arg_order (Ord_aux (Ord_dec, _)) -> "dec"
| _ ->
- raise (Reporting_basic.err_typ l "Unsupported register type")
+ raise (Reporting.err_typ l "Unsupported register type")
in
let builtins = IdSet.of_list (List.map mk_id ["vector"; "list"; "option"]) in
if IdSet.mem id builtins && not (mwords && is_bitvector_typ typ) then id else
append_id id (String.concat "_" ("" :: List.map name_arg args))
- | _ -> raise (Reporting_basic.err_typ l "Unsupported register type")
+ | _ -> raise (Reporting.err_typ l "Unsupported register type")
let register_base_types mwords typs =
let rec add_base_typs typs (Typ_aux (t, _) as typ) =
diff --git a/src/type_check.ml b/src/type_check.ml
index 3e6ec2a3..acba67fe 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -1295,7 +1295,7 @@ let rec nc_constraint env var_of (NC_aux (nc, l)) =
(List.map (fun i -> Constraint.eq (nexp_constraint env var_of (nvar kid)) (Constraint.constant i)) ints)
| NC_or (nc1, nc2) -> Constraint.disj (nc_constraint env var_of nc1) (nc_constraint env var_of nc2)
| NC_and (nc1, nc2) -> Constraint.conj (nc_constraint env var_of nc1) (nc_constraint env var_of nc2)
- | NC_app (id, nexps) -> raise (Reporting_basic.err_unreachable l __POS__ "constraint synonym reached smt generation")
+ | NC_app (id, nexps) -> raise (Reporting.err_unreachable l __POS__ "constraint synonym reached smt generation")
| NC_false -> Constraint.literal false
| NC_true -> Constraint.literal true
@@ -2026,17 +2026,17 @@ let destruct_vec_typ l env typ =
let env_of_annot (l, tannot) = match tannot with
| Some ((env, _, _),_) -> env
- | None -> raise (Reporting_basic.err_unreachable l __POS__ "no type annotation")
+ | None -> raise (Reporting.err_unreachable l __POS__ "no type annotation")
let env_of (E_aux (_, (l, tannot))) = env_of_annot (l, tannot)
let typ_of_annot (l, tannot) = match tannot with
| Some ((_, typ, _), _) -> typ
- | None -> raise (Reporting_basic.err_unreachable l __POS__ "no type annotation")
+ | None -> raise (Reporting.err_unreachable l __POS__ "no type annotation")
let env_of_annot (l, tannot) = match tannot with
| Some ((env, _, _), _) -> env
- | None -> raise (Reporting_basic.err_unreachable l __POS__ "no type annotation")
+ | None -> raise (Reporting.err_unreachable l __POS__ "no type annotation")
let typ_of (E_aux (_, (l, tannot))) = typ_of_annot (l, tannot)
@@ -2064,7 +2064,7 @@ let lexp_env_of (LEXP_aux (_, (l, tannot))) = env_of_annot (l, tannot)
let expected_typ_of (l, tannot) = match tannot with
| Some ((_, _, _), exp_typ) -> exp_typ
- | None -> raise (Reporting_basic.err_unreachable l __POS__ "no type annotation")
+ | None -> raise (Reporting.err_unreachable l __POS__ "no type annotation")
(* Flow typing *)
@@ -2592,7 +2592,7 @@ and bind_pat env (P_aux (pat_aux, (l, ())) as pat) (Typ_aux (typ_aux, _) as typ)
if Env.is_union_constructor v env then
Util.warn (Printf.sprintf "Identifier %s found in pattern is also a union constructor at %s\n"
(string_of_id v)
- (Reporting_basic.loc_to_string l))
+ (Reporting.loc_to_string l))
else ();
match Env.lookup_id v env with
| Local _ | Unbound -> annot_pat (P_id v) typ, Env.add_local v (Immutable, typ) env, []
@@ -3479,7 +3479,7 @@ and bind_mpat allow_unknown other_env env (MP_aux (mpat_aux, (l, ())) as mpat) (
if Env.is_union_constructor v env then
Util.warn (Printf.sprintf "Identifier %s found in mapping-pattern is also a union constructor at %s\n"
(string_of_id v)
- (Reporting_basic.loc_to_string l))
+ (Reporting.loc_to_string l))
else ();
match Env.lookup_id v env with
| Local (Immutable, _) | Unbound -> annot_mpat (MP_id v) typ, Env.add_local v (Immutable, typ) env, []
@@ -4264,7 +4264,7 @@ let check_fundef env (FD_aux (FD_function (recopt, tannotopt, effectopt, funcls)
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 was not a function type"
+ | _ -> typ_error 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)));
@@ -4412,7 +4412,7 @@ let mk_synonym typq typ =
^ " with " ^ string_of_list ", " string_of_n_constraint (Env.get_constraints env))
let check_kinddef env (KD_aux (kdef, (l, _))) =
- let kd_err () = raise (Reporting_basic.err_unreachable Parse_ast.Unknown __POS__ "Unimplemented kind def") in
+ let kd_err () = raise (Reporting.err_unreachable Parse_ast.Unknown __POS__ "Unimplemented kind def") in
match kdef with
| KD_nabbrev ((K_aux(K_kind([BK_aux (BK_int, _)]),_) as kind), id, nmscm, nexp) ->
[DEF_kind (KD_aux (KD_nabbrev (kind, id, nmscm, nexp), (l, None)))],
@@ -4421,7 +4421,7 @@ let check_kinddef env (KD_aux (kdef, (l, _))) =
let rec check_typedef : 'a. Env.t -> 'a type_def -> (tannot def) list * Env.t =
fun env (TD_aux (tdef, (l, _))) ->
- let td_err () = raise (Reporting_basic.err_unreachable Parse_ast.Unknown __POS__ "Unimplemented Typedef") in
+ let td_err () = raise (Reporting.err_unreachable Parse_ast.Unknown __POS__ "Unimplemented Typedef") in
match tdef with
| TD_abbrev (id, nmscm, (TypSchm_aux (TypSchm_ts (typq, typ), _))) ->
[DEF_type (TD_aux (tdef, (l, None)))], Env.add_typ_synonym id (mk_synonym typq typ) env
@@ -4454,7 +4454,7 @@ let rec check_typedef : 'a. Env.t -> 'a type_def -> (tannot def) list * Env.t =
and check_def : 'a. Env.t -> 'a def -> (tannot def) list * Env.t =
fun env def ->
- let cd_err () = raise (Reporting_basic.err_unreachable Parse_ast.Unknown __POS__ "Unimplemented Case") in
+ let cd_err () = raise (Reporting.err_unreachable Parse_ast.Unknown __POS__ "Unimplemented Case") in
match def with
| DEF_kind kdef -> check_kinddef env kdef
| DEF_type tdef -> check_typedef env tdef
@@ -4485,7 +4485,7 @@ and check_def : 'a. Env.t -> 'a def -> (tannot def) list * Env.t =
[DEF_reg_dec (DEC_aux (DEC_config (id, typ, checked_exp), (l, Some ((env, typ, no_effect), Some typ))))], env
| DEF_reg_dec (DEC_aux (DEC_alias (id, aspec), (l, annot))) -> cd_err ()
| DEF_reg_dec (DEC_aux (DEC_typ_alias (typ, id, aspec), (l, tannot))) -> cd_err ()
- | DEF_scattered _ -> raise (Reporting_basic.err_unreachable Parse_ast.Unknown __POS__ "Scattered given to type checker")
+ | DEF_scattered _ -> raise (Reporting.err_unreachable Parse_ast.Unknown __POS__ "Scattered given to type checker")
and check : 'a. Env.t -> 'a defs -> tannot defs * Env.t =
fun env (Defs defs) ->
diff --git a/src/type_check.mli b/src/type_check.mli
index ae46d956..1cb54770 100644
--- a/src/type_check.mli
+++ b/src/type_check.mli
@@ -405,7 +405,7 @@ Some invariants that will hold of a fully checked AST are:
for them to have type annotations.
check throws type_errors rather than Sail generic errors from
- Reporting_basic. For a function that uses generic errors, use
+ Reporting. For a function that uses generic errors, use
Type_error.check *)
val check : Env.t -> 'a defs -> tannot defs * Env.t
diff --git a/src/type_error.ml b/src/type_error.ml
index 5e2ce628..39c22cde 100644
--- a/src/type_error.ml
+++ b/src/type_error.ml
@@ -170,7 +170,7 @@ let rec pp_type_error = function
^/^ string "in context"
^/^ bullet pp_n_constraint constrs
^/^ string "where"
- ^/^ bullet (fun (kid, l) -> string (string_of_kid kid ^ " bound at " ^ Reporting_basic.loc_to_string l ^ "\n")) (KBindings.bindings locs)
+ ^/^ bullet (fun (kid, l) -> string (string_of_kid kid ^ " bound at " ^ Reporting.loc_to_string l ^ "\n")) (KBindings.bindings locs)
| Err_no_num_ident id ->
string "No num identifier" ^^ space ^^ string (string_of_id id)
@@ -192,4 +192,4 @@ let rec string_of_type_error 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_basic.err_typ l (string_of_type_error err))
+ | Type_error (l, err) -> raise (Reporting.err_typ l (string_of_type_error err))
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-02 05:26:55 +0000