aboutsummaryrefslogtreecommitdiff
path: root/checker
diff options
context:
space:
mode:
Diffstat (limited to 'checker')
-rw-r--r--checker/analyze.ml15
-rw-r--r--checker/check.ml2
-rw-r--r--checker/checker.ml4
-rw-r--r--checker/environ.ml2
-rw-r--r--checker/indtypes.ml4
-rw-r--r--checker/inductive.ml4
-rw-r--r--checker/modops.ml16
-rw-r--r--checker/reduction.ml2
-rw-r--r--checker/safe_typing.ml4
-rw-r--r--checker/subtyping.ml8
-rw-r--r--checker/term.ml8
-rw-r--r--checker/votour.ml24
12 files changed, 45 insertions, 48 deletions
diff --git a/checker/analyze.ml b/checker/analyze.ml
index c48b830119..df75d5b93c 100644
--- a/checker/analyze.ml
+++ b/checker/analyze.ml
@@ -4,6 +4,7 @@ let prefix_small_block = 0x80
let prefix_small_int = 0x40
let prefix_small_string = 0x20
+[@@@ocaml.warning "-32"]
let code_int8 = 0x00
let code_int16 = 0x01
let code_int32 = 0x02
@@ -25,6 +26,7 @@ let code_infixpointer = 0x11
let code_custom = 0x12
let code_block64 = 0x13
+[@@@ocaml.warning "-37"]
type code_descr =
| CODE_INT8
| CODE_INT16
@@ -101,11 +103,11 @@ let input_binary_int chan =
input_binary_int chan
let input_char chan = Char.chr (input_byte chan)
+let input_string len chan = String.init len (fun _ -> input_char chan)
let parse_header chan =
let () = current_offset := 0 in
- let magic = String.create 4 in
- let () = for i = 0 to 3 do magic.[i] <- input_char chan done in
+ let magic = input_string 4 chan in
let length = input_binary_int chan in
let objects = input_binary_int chan in
let size32 = input_binary_int chan in
@@ -204,13 +206,6 @@ let input_header64 chan =
in
(tag, len)
-let input_string len chan =
- let ans = String.create len in
- for i = 0 to pred len do
- ans.[i] <- input_char chan;
- done;
- ans
-
let parse_object chan =
let data = input_byte chan in
if prefix_small_block <= data then
@@ -251,7 +246,7 @@ let parse_object chan =
RString (input_string len chan)
| CODE_CODEPOINTER ->
let addr = input_int32u chan in
- for i = 0 to 15 do ignore (input_byte chan); done;
+ for _i = 0 to 15 do ignore (input_byte chan); done;
RCode addr
| CODE_DOUBLE_ARRAY32_LITTLE
| CODE_DOUBLE_BIG
diff --git a/checker/check.ml b/checker/check.ml
index 11678fa6bb..6d93c11eac 100644
--- a/checker/check.ml
+++ b/checker/check.ml
@@ -72,7 +72,7 @@ let find_library dir =
let try_find_library dir =
try find_library dir
with Not_found ->
- error ("Unknown library " ^ (DirPath.to_string dir))
+ user_err Pp.(str ("Unknown library " ^ (DirPath.to_string dir)))
let library_full_filename dir = (find_library dir).library_filename
diff --git a/checker/checker.ml b/checker/checker.ml
index 5cadfe7b94..e00f47a540 100644
--- a/checker/checker.ml
+++ b/checker/checker.ml
@@ -335,7 +335,7 @@ let parse_args argv =
| "-debug" :: rem -> set_debug (); parse rem
| "-where" :: _ ->
- Envars.set_coqlib ~fail:CErrors.error;
+ Envars.set_coqlib ~fail:(fun x -> CErrors.user_err Pp.(str x));
print_endline (Envars.coqlib ());
exit 0
@@ -373,7 +373,7 @@ let init_with_argv argv =
try
parse_args argv;
if !Flags.debug then Printexc.record_backtrace true;
- Envars.set_coqlib ~fail:CErrors.error;
+ Envars.set_coqlib ~fail:(fun x -> CErrors.user_err Pp.(str x));
if_verbose print_header ();
init_load_path ();
engage ();
diff --git a/checker/environ.ml b/checker/environ.ml
index 7b59c6b986..bce40861cf 100644
--- a/checker/environ.ml
+++ b/checker/environ.ml
@@ -45,7 +45,7 @@ let set_engagement (impr_set as c) env =
env.env_stratification.env_engagement in
begin
match impr_set,expected_impr_set with
- | PredicativeSet, ImpredicativeSet -> error "Incompatible engagement"
+ | PredicativeSet, ImpredicativeSet -> user_err Pp.(str "Incompatible engagement")
| _ -> ()
end;
{ env with env_stratification =
diff --git a/checker/indtypes.ml b/checker/indtypes.ml
index 27f79e7963..0482912b0a 100644
--- a/checker/indtypes.ml
+++ b/checker/indtypes.ml
@@ -535,13 +535,13 @@ let check_inductive env kn mib =
(* check mind_finite : always OK *)
(* check mind_ntypes *)
if Array.length mib.mind_packets <> mib.mind_ntypes then
- error "not the right number of packets";
+ user_err Pp.(str "not the right number of packets");
(* check mind_params_ctxt *)
let params = mib.mind_params_ctxt in
let _ = check_ctxt env params in
(* check mind_nparams *)
if rel_context_nhyps params <> mib.mind_nparams then
- error "number the right number of parameters";
+ user_err Pp.(str "number the right number of parameters");
(* mind_packets *)
(* - check arities *)
let env_ar = typecheck_arity env params mib.mind_packets in
diff --git a/checker/inductive.ml b/checker/inductive.ml
index 8f23a38afc..9e417a8eb5 100644
--- a/checker/inductive.ml
+++ b/checker/inductive.ml
@@ -27,7 +27,7 @@ type mind_specif = mutual_inductive_body * one_inductive_body
let lookup_mind_specif env (kn,tyi) =
let mib = lookup_mind kn env in
if tyi >= Array.length mib.mind_packets then
- error "Inductive.lookup_mind_specif: invalid inductive index";
+ user_err Pp.(str "Inductive.lookup_mind_specif: invalid inductive index");
(mib, mib.mind_packets.(tyi))
let find_rectype env c =
@@ -232,7 +232,7 @@ let type_of_constructor_subst cstr u (mib,mip) =
let specif = mip.mind_user_lc in
let i = index_of_constructor cstr in
let nconstr = Array.length mip.mind_consnames in
- if i > nconstr then error "Not enough constructors in the type.";
+ if i > nconstr then user_err Pp.(str "Not enough constructors in the type.");
constructor_instantiate (fst ind) u mib specif.(i-1)
let type_of_constructor_gen (cstr,u) (mib,mip as mspec) =
diff --git a/checker/modops.ml b/checker/modops.ml
index 07dda8a06d..bed31143bf 100644
--- a/checker/modops.ml
+++ b/checker/modops.ml
@@ -16,21 +16,21 @@ open Declarations
(*i*)
let error_not_a_constant l =
- error ("\""^(Label.to_string l)^"\" is not a constant")
+ user_err Pp.(str ("\""^(Label.to_string l)^"\" is not a constant"))
-let error_not_a_functor () = error "Application of not a functor"
+let error_not_a_functor () = user_err Pp.(str "Application of not a functor")
-let error_incompatible_modtypes _ _ = error "Incompatible module types"
+let error_incompatible_modtypes _ _ = user_err Pp.(str "Incompatible module types")
let error_not_match l _ =
- error ("Signature components for label "^Label.to_string l^" do not match")
+ user_err Pp.(str ("Signature components for label "^Label.to_string l^" do not match"))
-let error_no_such_label l = error ("No such label "^Label.to_string l)
+let error_no_such_label l = user_err Pp.(str ("No such label "^Label.to_string l))
let error_no_such_label_sub l l1 =
let l1 = ModPath.to_string l1 in
- error ("The field "^
- Label.to_string l^" is missing in "^l1^".")
+ user_err Pp.(str ("The field "^
+ Label.to_string l^" is missing in "^l1^"."))
let error_not_a_module_loc ?loc s =
user_err ?loc (str ("\""^Label.to_string s^"\" is not a module"))
@@ -38,7 +38,7 @@ let error_not_a_module_loc ?loc s =
let error_not_a_module s = error_not_a_module_loc s
let error_with_module () =
- error "Unsupported 'with' constraint in module implementation"
+ user_err Pp.(str "Unsupported 'with' constraint in module implementation")
let is_functor = function
| MoreFunctor _ -> true
diff --git a/checker/reduction.ml b/checker/reduction.ml
index 28c0126b41..82f09cf4b0 100644
--- a/checker/reduction.ml
+++ b/checker/reduction.ml
@@ -536,5 +536,5 @@ let dest_arity env c =
let l, c = dest_prod_assum env c in
match c with
| Sort s -> l,s
- | _ -> error "not an arity"
+ | _ -> user_err Pp.(str "not an arity")
diff --git a/checker/safe_typing.ml b/checker/safe_typing.ml
index 53d80c6d55..c70cd5c8ce 100644
--- a/checker/safe_typing.ml
+++ b/checker/safe_typing.ml
@@ -40,7 +40,7 @@ let check_engagement env expected_impredicative_set =
begin
match impredicative_set, expected_impredicative_set with
| PredicativeSet, ImpredicativeSet ->
- CErrors.error "Needs option -impredicative-set."
+ CErrors.user_err Pp.(str "Needs option -impredicative-set.")
| _ -> ()
end;
()
@@ -61,7 +61,7 @@ let check_imports f caller env needed =
let actual_stamp = lookup_digest env dp in
if stamp <> actual_stamp then report_clash f caller dp
with Not_found ->
- error ("Reference to unknown module " ^ (DirPath.to_string dp))
+ user_err Pp.(str ("Reference to unknown module " ^ (DirPath.to_string dp)))
in
Array.iter check needed
diff --git a/checker/subtyping.ml b/checker/subtyping.ml
index a290b240d8..2d04b77e46 100644
--- a/checker/subtyping.ml
+++ b/checker/subtyping.ml
@@ -302,22 +302,22 @@ let check_constant env mp1 l info1 cb2 spec2 subst1 subst2 =
let c2 = force_constr lc2 in
check_conv conv env c1 c2))
| IndType ((kn,i),mind1) ->
- ignore (CErrors.error (
+ ignore (CErrors.user_err (Pp.str (
"The kernel does not recognize yet that a parameter can be " ^
"instantiated by an inductive type. Hint: you can rename the " ^
"inductive type and give a definition to map the old name to the new " ^
- "name."));
+ "name.")));
if constant_has_body cb2 then error () ;
let u = inductive_instance mind1 in
let arity1 = type_of_inductive env ((mind1,mind1.mind_packets.(i)),u) in
let typ2 = Typeops.type_of_constant_type env cb2.const_type in
check_conv conv_leq env arity1 typ2
| IndConstr (((kn,i),j) as cstr,mind1) ->
- ignore (CErrors.error (
+ ignore (CErrors.user_err (Pp.str (
"The kernel does not recognize yet that a parameter can be " ^
"instantiated by a constructor. Hint: you can rename the " ^
"constructor and give a definition to map the old name to the new " ^
- "name."));
+ "name.")));
if constant_has_body cb2 then error () ;
let u1 = inductive_instance mind1 in
let ty1 = type_of_constructor (cstr,u1) (mind1,mind1.mind_packets.(i)) in
diff --git a/checker/term.ml b/checker/term.ml
index 24e6008d34..8cac783753 100644
--- a/checker/term.ml
+++ b/checker/term.ml
@@ -273,14 +273,14 @@ let decompose_lam =
abstractions *)
let decompose_lam_n_assum n =
if n < 0 then
- error "decompose_lam_n_assum: integer parameter must be positive";
+ user_err Pp.(str "decompose_lam_n_assum: integer parameter must be positive");
let rec lamdec_rec l n c =
if Int.equal n 0 then l,c
else match c with
| Lambda (x,t,c) -> lamdec_rec (LocalAssum (x,t) :: l) (n-1) c
| LetIn (x,b,t,c) -> lamdec_rec (LocalDef (x,b,t) :: l) n c
| Cast (c,_,_) -> lamdec_rec l n c
- | c -> error "decompose_lam_n_assum: not enough abstractions"
+ | c -> user_err Pp.(str "decompose_lam_n_assum: not enough abstractions")
in
lamdec_rec empty_rel_context n
@@ -306,14 +306,14 @@ let decompose_prod_assum =
let decompose_prod_n_assum n =
if n < 0 then
- error "decompose_prod_n_assum: integer parameter must be positive";
+ user_err Pp.(str "decompose_prod_n_assum: integer parameter must be positive");
let rec prodec_rec l n c =
if Int.equal n 0 then l,c
else match c with
| Prod (x,t,c) -> prodec_rec (LocalAssum (x,t) :: l) (n-1) c
| LetIn (x,b,t,c) -> prodec_rec (LocalDef (x,b,t) :: l) (n-1) c
| Cast (c,_,_) -> prodec_rec l n c
- | c -> error "decompose_prod_n_assum: not enough assumptions"
+ | c -> user_err Pp.(str "decompose_prod_n_assum: not enough assumptions")
in
prodec_rec empty_rel_context n
diff --git a/checker/votour.ml b/checker/votour.ml
index 48f9f45e7e..c255e5cdb2 100644
--- a/checker/votour.ml
+++ b/checker/votour.ml
@@ -19,14 +19,14 @@ let rec read_num max =
if l = "u" then None
else if l = "x" then quit ()
else
- try
- let v = int_of_string l in
+ match int_of_string l with
+ | v ->
if v < 0 || v >= max then
let () =
Printf.printf "Out-of-range input! (only %d children)\n%!" max in
read_num max
else Some v
- with Failure "int_of_string" ->
+ | exception Failure _ ->
Printf.printf "Unrecognized input! <n> enters the <n>-th child, u goes up 1 level, x exits\n%!";
read_num max
@@ -149,16 +149,17 @@ let rec get_name ?(extra=false) = function
(** For tuples, its quite handy to display the inner 1st string (if any).
Cf. [structure_body] for instance *)
+exception TupleString of string
let get_string_in_tuple o =
try
for i = 0 to Array.length o - 1 do
match Repr.repr o.(i) with
| STRING s ->
- failwith (Printf.sprintf " [..%s..]" s)
+ raise (TupleString (Printf.sprintf " [..%s..]" s))
| _ -> ()
done;
""
- with Failure s -> s
+ with TupleString s -> s
(** Some details : tags, integer value for non-block, etc etc *)
@@ -205,6 +206,7 @@ let access_block o = match Repr.repr o with
let access_int o = match Repr.repr o with INT i -> i | _ -> raise Exit
(** raises Exit if the object has not the expected structure *)
+exception Forbidden
let rec get_children v o pos = match v with
|Tuple (_, v) ->
let (_, os) = access_block o in
@@ -236,7 +238,7 @@ let rec get_children v o pos = match v with
[|(Int, id, 0 :: pos); (tpe, o, 1 :: pos)|]
| _ -> raise Exit
end
- |Fail s -> failwith "forbidden"
+ |Fail s -> raise Forbidden
let get_children v o pos =
try get_children v o pos
@@ -257,9 +259,10 @@ let init () = stk := []
let push name v o p = stk := { nam = name; typ = v; obj = o; pos = p } :: !stk
+exception EmptyStack
let pop () = match !stk with
| i::s -> stk := s; i
- | _ -> failwith "empty stack"
+ | _ -> raise EmptyStack
let rec visit v o pos =
Printf.printf "\nDepth %d Pos %s Context %s\n"
@@ -283,8 +286,8 @@ let rec visit v o pos =
push (get_name v) v o pos;
visit v' o' pos'
with
- | Failure "empty stack" -> ()
- | Failure "forbidden" -> let info = pop () in visit info.typ info.obj info.pos
+ | EmptyStack -> ()
+ | Forbidden -> let info = pop () in visit info.typ info.obj info.pos
| Failure _ | Invalid_argument _ -> visit v o pos
end
@@ -313,8 +316,7 @@ let dummy_header = {
}
let parse_header chan =
- let magic = String.create 4 in
- let () = for i = 0 to 3 do magic.[i] <- input_char chan done in
+ let magic = really_input_string chan 4 in
let length = input_binary_int chan in
let objects = input_binary_int chan in
let size32 = input_binary_int chan in
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-02 10:14:52 +0000