aboutsummaryrefslogtreecommitdiffhomepage
path: root/checker
diff options
context:
space:
mode:
Diffstat (limited to 'checker')
-rw-r--r--checker/Makefile88
-rw-r--r--checker/analyze.ml15
-rw-r--r--checker/check.ml18
-rw-r--r--checker/checker.ml12
-rw-r--r--checker/closure.ml16
-rw-r--r--checker/declarations.ml13
-rw-r--r--checker/environ.ml14
-rw-r--r--checker/include2
-rw-r--r--checker/indtypes.ml10
-rw-r--r--checker/inductive.ml25
-rw-r--r--checker/modops.ml22
-rw-r--r--checker/reduction.ml14
-rw-r--r--checker/safe_typing.ml6
-rw-r--r--checker/subtyping.ml10
-rw-r--r--checker/term.ml14
-rw-r--r--checker/term.mli2
-rw-r--r--checker/typeops.ml13
-rw-r--r--checker/univ.ml23
-rw-r--r--checker/votour.ml24
19 files changed, 103 insertions, 238 deletions
diff --git a/checker/Makefile b/checker/Makefile
deleted file mode 100644
index 2bcc9d365..000000000
--- a/checker/Makefile
+++ /dev/null
@@ -1,88 +0,0 @@
-OCAMLC=ocamlc
-OCAMLOPT=ocamlopt
-
-COQSRC=..
-
-MLDIRS=-I $(COQSRC)/config -I $(COQSRC)/lib -I $(COQSRC)/kernel -I +camlp4
-BYTEFLAGS=$(MLDIRS)
-OPTFLAGS=$(MLDIRS)
-
-CHECKERNAME=coqchk
-
-BINARIES=../bin/$(CHECKERNAME)$(EXE) ../bin/$(CHECKERNAME).opt$(EXE)
-MCHECKERLOCAL :=\
- declarations.cmo environ.cmo \
- closure.cmo reduction.cmo \
- type_errors.cmo \
- modops.cmo \
- inductive.cmo typeops.cmo \
- indtypes.cmo subtyping.cmo mod_checking.cmo \
-validate.cmo \
- safe_typing.cmo check.cmo \
- check_stat.cmo checker.cmo
-
-MCHECKER:=\
- $(COQSRC)/config/coq_config.cmo \
- $(COQSRC)/lib/pp_control.cmo $(COQSRC)/lib/pp.cmo $(COQSRC)/lib/compat.cmo \
- $(COQSRC)/lib/util.cmo $(COQSRC)/lib/option.cmo $(COQSRC)/lib/hashcons.cmo \
- $(COQSRC)/lib/system.cmo $(COQSRC)/lib/flags.cmo \
- $(COQSRC)/lib/predicate.cmo $(COQSRC)/lib/rtree.cmo \
- $(COQSRC)/kernel/names.cmo $(COQSRC)/kernel/univ.cmo \
- $(COQSRC)/kernel/esubst.cmo term.cmo \
- $(MCHECKERLOCAL)
-
-all: $(BINARIES)
-
-byte : ../bin/$(CHECKERNAME)$(EXE)
-opt : ../bin/$(CHECKERNAME).opt$(EXE)
-
-check.cma: $(MCHECKERLOCAL)
- ocamlc $(BYTEFLAGS) -a -o $@ $(MCHECKER)
-
-check.cmxa: $(MCHECKERLOCAL:.cmo=.cmx)
- ocamlopt $(OPTFLAGS) -a -o $@ $(MCHECKER:.cmo=.cmx)
-
-../bin/$(CHECKERNAME)$(EXE): check.cma
- ocamlc $(BYTEFLAGS) -o $@ unix.cma gramlib.cma check.cma main.ml
-
-../bin/$(CHECKERNAME).opt$(EXE): check.cmxa
- ocamlopt $(OPTFLAGS) -o $@ unix.cmxa gramlib.cmxa check.cmxa main.ml
-
-stats:
- @echo STRUCTURE
- @wc names.ml term.ml declarations.ml environ.ml type_errors.ml
- @echo
- @echo REDUCTION
- @-wc esubst.ml closure.ml reduction.ml
- @echo
- @echo TYPAGE
- @wc univ.ml inductive.ml indtypes.ml typeops.ml safe_typing.ml
- @echo
- @echo MODULES
- @wc modops.ml subtyping.ml
- @echo
- @echo INTERFACE
- @wc check*.ml main.ml
- @echo
- @echo TOTAL
- @wc *.ml | tail -1
-
-.SUFFIXES:.ml .mli .cmi .cmo .cmx
-
-.ml.cmo:
- $(OCAMLC) -c $(BYTEFLAGS) $<
-
-.ml.cmx:
- $(OCAMLOPT) -c $(OPTFLAGS) $<
-
-.mli.cmi:
- $(OCAMLC) -c $(BYTEFLAGS) $<
-
-
-depend::
- ocamldep *.ml* > .depend
-
-clean::
- rm -f *.cm* *.o *.a *~ $(BINARIES)
-
--include .depend
diff --git a/checker/analyze.ml b/checker/analyze.ml
index c48b83011..df75d5b93 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 8b299bf2a..b3b403425 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
@@ -165,7 +165,7 @@ let find_logical_path phys_dir =
match List.filter2 (fun p d -> p = phys_dir) physical logical with
| _,[dir] -> dir
| _,[] -> default_root_prefix
- | _,l -> anomaly (Pp.str ("Two logical paths are associated to "^phys_dir))
+ | _,l -> anomaly (Pp.str ("Two logical paths are associated to "^phys_dir^"."))
let remove_load_path dir =
let physical, logical = !load_paths in
@@ -197,7 +197,7 @@ let add_load_path (phys_path,coq_path) =
end
| _,[] ->
load_paths := (phys_path :: fst !load_paths, coq_path :: snd !load_paths)
- | _ -> anomaly (Pp.str ("Two logical paths are associated to "^phys_path))
+ | _ -> anomaly (Pp.str ("Two logical paths are associated to "^phys_path^"."))
let load_paths_of_dir_path dir =
let physical, logical = !load_paths in
@@ -248,12 +248,12 @@ let locate_qualified_library qid =
let error_unmapped_dir qid =
let prefix = qid.dirpath in
- errorlabstrm "load_absolute_library_from"
+ user_err ~hdr:"load_absolute_library_from"
(str "Cannot load " ++ pr_path qid ++ str ":" ++ spc () ++
str "no physical path bound to" ++ spc () ++ pr_dirlist prefix ++ fnl ())
let error_lib_not_found qid =
- errorlabstrm "load_absolute_library_from"
+ user_err ~hdr:"load_absolute_library_from"
(str"Cannot find library " ++ pr_path qid ++ str" in loadpath")
let try_locate_absolute_library dir =
@@ -314,18 +314,18 @@ let intern_from_file (dir, f) =
let () = close_in ch in
let ch = open_in_bin f in
if not (String.equal (Digest.channel ch pos) checksum) then
- errorlabstrm "intern_from_file" (str "Checksum mismatch");
+ user_err ~hdr:"intern_from_file" (str "Checksum mismatch");
let () = close_in ch in
if dir <> sd.md_name then
- errorlabstrm "intern_from_file"
+ user_err ~hdr:"intern_from_file"
(name_clash_message dir sd.md_name f);
if tasks <> None || discharging <> None then
- errorlabstrm "intern_from_file"
+ user_err ~hdr:"intern_from_file"
(str "The file "++str f++str " contains unfinished tasks");
if opaque_csts <> None then begin
chk_pp (str " (was a vio file) ");
Option.iter (fun (_,_,b) -> if not b then
- errorlabstrm "intern_from_file"
+ user_err ~hdr:"intern_from_file"
(str "The file "++str f++str " is still a .vio"))
opaque_csts;
Validate.validate !Flags.debug Values.v_univopaques opaque_csts;
diff --git a/checker/checker.ml b/checker/checker.ml
index 8dbb7e011..e00f47a54 100644
--- a/checker/checker.ml
+++ b/checker/checker.ml
@@ -216,10 +216,12 @@ let report () = (str "." ++ spc () ++ str "Please report" ++
let guill s = str "\"" ++ str s ++ str "\""
-let where s =
+let where = function
+| None -> mt ()
+| Some s ->
if !Flags.debug then (str"in " ++ str s ++ str":" ++ spc ()) else (mt ())
-let rec explain_exn = function
+let explain_exn = function
| Stream.Failure ->
hov 0 (anomaly_string () ++ str "uncaught Stream.Failure.")
| Stream.Error txt ->
@@ -333,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
@@ -352,7 +354,7 @@ let parse_args argv =
| "-norec" :: [] -> usage ()
| "-silent" :: rem ->
- Flags.make_silent true; parse rem
+ Flags.quiet := true; parse rem
| s :: _ when s<>"" && s.[0]='-' ->
fatal_error (str "Unknown option " ++ str s) false
@@ -371,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/closure.ml b/checker/closure.ml
index cef1d31a6..b8294e795 100644
--- a/checker/closure.ml
+++ b/checker/closure.ml
@@ -651,22 +651,6 @@ let drop_parameters depth n argstk =
(** Projections and eta expansion *)
-let rec get_parameters depth n argstk =
- match argstk with
- Zapp args::s ->
- let q = Array.length args in
- if n > q then Array.append args (get_parameters depth (n-q) s)
- else if Int.equal n q then [||]
- else Array.sub args 0 n
- | Zshift(k)::s ->
- get_parameters (depth-k) n s
- | [] -> (* we know that n < stack_args_size(argstk) (if well-typed term) *)
- if Int.equal n 0 then [||]
- else raise Not_found (* Trying to eta-expand a partial application..., should do
- eta expansion first? *)
- | _ -> assert false
- (* strip_update_shift_app only produces Zapp and Zshift items *)
-
let eta_expand_ind_stack env ind m s (f, s') =
let mib = lookup_mind (fst ind) env in
match mib.mind_record with
diff --git a/checker/declarations.ml b/checker/declarations.ml
index 1fe02c8b6..ad93146d5 100644
--- a/checker/declarations.ml
+++ b/checker/declarations.ml
@@ -6,6 +6,7 @@ open Term
(** Substitutions, code imported from kernel/mod_subst *)
module Deltamap = struct
+ [@@@ocaml.warning "-32-34"]
type t = delta_resolver
let empty = MPmap.empty, KNmap.empty
let is_empty (mm, km) = MPmap.is_empty mm && KNmap.is_empty km
@@ -25,6 +26,7 @@ end
let empty_delta_resolver = Deltamap.empty
module Umap = struct
+ [@@@ocaml.warning "-32-34"]
type 'a t = 'a umap_t
let empty = MPmap.empty, MBImap.empty
let is_empty (m1,m2) = MPmap.is_empty m1 && MBImap.is_empty m2
@@ -461,13 +463,6 @@ let is_opaque cb = match cb.const_body with
let opaque_univ_context cb = force_lazy_constr_univs cb.const_body
-let subst_rel_declaration sub (id,copt,t as x) =
- let copt' = Option.smartmap (subst_mps sub) copt in
- let t' = subst_mps sub t in
- if copt == copt' && t == t' then x else (id,copt',t')
-
-let subst_rel_context sub = List.smartmap (subst_rel_declaration sub)
-
let subst_recarg sub r = match r with
| Norec -> r
| (Mrec(kn,i)|Imbr (kn,i)) -> let kn' = subst_ind sub kn in
@@ -515,10 +510,6 @@ let subst_decl_arity f g sub ar =
if x' == x then ar
else TemplateArity x'
-let map_decl_arity f g = function
- | RegularArity a -> RegularArity (f a)
- | TemplateArity a -> TemplateArity (g a)
-
let subst_rel_declaration sub =
Term.map_rel_decl (subst_mps sub)
diff --git a/checker/environ.ml b/checker/environ.ml
index 7b59c6b98..22d1eec17 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 =
@@ -106,7 +106,7 @@ let anomaly s = anomaly (Pp.str s)
let add_constant kn cs env =
if Cmap_env.mem kn env.env_globals.env_constants then
- Printf.ksprintf anomaly ("Constant %s is already defined")
+ Printf.ksprintf anomaly ("Constant %s is already defined.")
(Constant.to_string kn);
let new_constants =
Cmap_env.add kn cs env.env_globals.env_constants in
@@ -161,7 +161,7 @@ let is_projection cst env =
let lookup_projection p env =
match (lookup_constant (Projection.constant p) env).const_proj with
| Some pb -> pb
- | None -> anomaly ("lookup_projection: constant is not a projection")
+ | None -> anomaly ("lookup_projection: constant is not a projection.")
(* Mutual Inductives *)
let scrape_mind env kn=
@@ -182,7 +182,7 @@ let lookup_mind kn env =
let add_mind kn mib env =
if Mindmap_env.mem kn env.env_globals.env_inductives then
- Printf.ksprintf anomaly ("Inductive %s is already defined")
+ Printf.ksprintf anomaly ("Inductive %s is already defined.")
(MutInd.to_string kn);
let new_inds = Mindmap_env.add kn mib env.env_globals.env_inductives in
let kn1,kn2 = MutInd.user kn, MutInd.canonical kn in
@@ -201,7 +201,7 @@ let add_mind kn mib env =
let add_modtype ln mtb env =
if MPmap.mem ln env.env_globals.env_modtypes then
- Printf.ksprintf anomaly ("Module type %s is already defined")
+ Printf.ksprintf anomaly ("Module type %s is already defined.")
(ModPath.to_string ln);
let new_modtypes = MPmap.add ln mtb env.env_globals.env_modtypes in
let new_globals =
@@ -211,7 +211,7 @@ let add_modtype ln mtb env =
let shallow_add_module mp mb env =
if MPmap.mem mp env.env_globals.env_modules then
- Printf.ksprintf anomaly ("Module %s is already defined")
+ Printf.ksprintf anomaly ("Module %s is already defined.")
(ModPath.to_string mp);
let new_mods = MPmap.add mp mb env.env_globals.env_modules in
let new_globals =
@@ -221,7 +221,7 @@ let shallow_add_module mp mb env =
let shallow_remove_module mp env =
if not (MPmap.mem mp env.env_globals.env_modules) then
- Printf.ksprintf anomaly ("Module %s is unknown")
+ Printf.ksprintf anomaly ("Module %s is unknown.")
(ModPath.to_string mp);
let new_mods = MPmap.remove mp env.env_globals.env_modules in
let new_globals =
diff --git a/checker/include b/checker/include
index 6bea3c91a..09bf2826c 100644
--- a/checker/include
+++ b/checker/include
@@ -116,7 +116,7 @@ let prsub s =
#install_printer prsub;;*)
Checker.init_with_argv [|"";"-coqlib";"."|];;
-Flags.make_silent false;;
+Flags.quiet := false;;
Flags.debug := true;;
Sys.catch_break true;;
diff --git a/checker/indtypes.ml b/checker/indtypes.ml
index 9ccaaa7cb..6c38f38e2 100644
--- a/checker/indtypes.ml
+++ b/checker/indtypes.ml
@@ -100,7 +100,7 @@ let rec sorts_of_constr_args env t =
let env1 = push_rel (LocalDef (name,def,ty)) env in
sorts_of_constr_args env1 c
| _ when is_constructor_head t -> []
- | _ -> anomaly ~label:"infos_and_sort" (Pp.str "not a positive constructor")
+ | _ -> anomaly ~label:"infos_and_sort" (Pp.str "not a positive constructor.")
(* Prop and Set are small *)
@@ -302,11 +302,11 @@ let failwith_non_pos n ntypes c =
let failwith_non_pos_vect n ntypes v =
Array.iter (failwith_non_pos n ntypes) v;
- anomaly ~label:"failwith_non_pos_vect" (Pp.str "some k in [n;n+ntypes-1] should occur")
+ anomaly ~label:"failwith_non_pos_vect" (Pp.str "some k in [n;n+ntypes-1] should occur.")
let failwith_non_pos_list n ntypes l =
List.iter (failwith_non_pos n ntypes) l;
- anomaly ~label:"failwith_non_pos_list" (Pp.str "some k in [n;n+ntypes-1] should occur")
+ anomaly ~label:"failwith_non_pos_list" (Pp.str "some k in [n;n+ntypes-1] should occur.")
(* Conclusion of constructors: check the inductive type is called with
the expected parameters *)
@@ -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 c4ffc141f..f890adba9 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 =
@@ -75,7 +75,7 @@ let constructor_instantiate mind u mib c =
let instantiate_params full t u args sign =
let fail () =
- anomaly ~label:"instantiate_params" (Pp.str "type, ctxt and args mismatch") in
+ anomaly ~label:"instantiate_params" (Pp.str "type, ctxt and args mismatch.") in
let (rem_args, subs, ty) =
fold_rel_context
(fun decl (largs,subs,ty) ->
@@ -149,7 +149,7 @@ let remember_subst u subst =
(* Bind expected levels of parameters to actual levels *)
(* Propagate the new levels in the signature *)
-let rec make_subst env =
+let make_subst env =
let rec make subst = function
| LocalDef _ :: sign, exp, args ->
make subst (sign, exp, args)
@@ -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) =
@@ -436,13 +436,6 @@ let eq_recarg r1 r2 = match r1, r2 with
let eq_wf_paths = Rtree.equal eq_recarg
-let pp_recarg = function
- | Norec -> Pp.str "Norec"
- | Mrec i -> Pp.str ("Mrec "^MutInd.to_string (fst i))
- | Imbr i -> Pp.str ("Imbr "^MutInd.to_string (fst i))
-
-let pp_wf_paths = Rtree.pp_tree pp_recarg
-
let inter_recarg r1 r2 = match r1, r2 with
| Norec, Norec -> Some r1
| Mrec i1, Mrec i2
@@ -993,7 +986,7 @@ let check_one_fix renv recpos trees def =
List.iter (check_rec_call renv []) l;
check_rec_call renv [] c
- | Var _ -> anomaly (Pp.str "Section variable in Coqchk !")
+ | Var _ -> anomaly (Pp.str "Section variable in Coqchk!")
| Sort _ -> assert (l = [])
@@ -1011,7 +1004,7 @@ let check_one_fix renv recpos trees def =
check_rec_call renv [] a;
let renv' = push_var_renv renv (x,a) in
check_nested_fix_body renv' (decr-1) recArgsDecrArg b
- | _ -> anomaly (Pp.str "Not enough abstractions in fix body")
+ | _ -> anomaly (Pp.str "Not enough abstractions in fix body.")
in
check_rec_call renv [] def
@@ -1025,7 +1018,7 @@ let inductive_of_mutfix env ((nvect,bodynum),(names,types,bodies as recdef)) =
|| Array.length names <> nbfix
|| bodynum < 0
|| bodynum >= nbfix
- then anomaly (Pp.str "Ill-formed fix term");
+ then anomaly (Pp.str "Ill-formed fix term.");
let fixenv = push_rec_types recdef env in
let raise_err env i err =
error_ill_formed_rec_body env err names i in
@@ -1046,7 +1039,7 @@ let inductive_of_mutfix env ((nvect,bodynum),(names,types,bodies as recdef)) =
raise_err env i (RecursionNotOnInductiveType a) in
(mind, (env', b))
else check_occur env' (n+1) b
- else anomaly ~label:"check_one_fix" (Pp.str "Bad occurrence of recursive call")
+ else anomaly ~label:"check_one_fix" (Pp.str "Bad occurrence of recursive call.")
| _ -> raise_err env i NotEnoughAbstractionInFixBody in
check_occur fixenv 1 def in
(* Do it on every fixpoint *)
@@ -1080,7 +1073,7 @@ let check_fix env fix = Profile.profile3 cfkey check_fix env fix;;
exception CoFixGuardError of env * guard_error
let anomaly_ill_typed () =
- anomaly ~label:"check_one_cofix" (Pp.str "too many arguments applied to constructor")
+ anomaly ~label:"check_one_cofix" (Pp.str "too many arguments applied to constructor.")
let rec codomain_is_coind env c =
let b = whd_all env c in
diff --git a/checker/modops.ml b/checker/modops.ml
index b720fb621..bed31143b 100644
--- a/checker/modops.ml
+++ b/checker/modops.ml
@@ -16,29 +16,29 @@ 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 (loc,"",str ("\""^Label.to_string s^"\" is not a module"))
+let error_not_a_module_loc ?loc s =
+ user_err ?loc (str ("\""^Label.to_string s^"\" is not a module"))
-let error_not_a_module s = error_not_a_module_loc Loc.ghost 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 ec16aa261..ba0b01784 100644
--- a/checker/reduction.ml
+++ b/checker/reduction.ml
@@ -176,9 +176,9 @@ let sort_cmp env univ pb s0 s1 =
then begin
if !Flags.debug then begin
let op = match pb with CONV -> "=" | CUMUL -> "<=" in
- Printf.eprintf "sort_cmp: %s\n%!" Pp.(string_of_ppcmds
- (str"Error: " ++ Univ.pr_uni u1 ++ str op ++ Univ.pr_uni u2 ++ str ":" ++ cut()
- ++ Univ.pr_universes univ))
+ Format.eprintf "sort_cmp: @[%a@]\n%!" Pp.pp_with Pp.(
+ str"Error: " ++ Univ.pr_uni u1 ++ str op ++ Univ.pr_uni u2 ++ str ":" ++ cut()
+ ++ Univ.pr_universes univ)
end;
raise NotConvertible
end
@@ -333,13 +333,13 @@ and eqappr univ cv_pb infos (lft1,st1) (lft2,st2) =
(* Eta-expansion on the fly *)
| (FLambda _, _) ->
if v1 <> [] then
- anomaly (Pp.str "conversion was given unreduced term (FLambda)");
+ anomaly (Pp.str "conversion was given unreduced term (FLambda).");
let (_,_ty1,bd1) = destFLambda mk_clos hd1 in
eqappr univ CONV infos
(el_lift lft1,(bd1,[])) (el_lift lft2,(hd2,eta_expand_stack v2))
| (_, FLambda _) ->
if v2 <> [] then
- anomaly (Pp.str "conversion was given unreduced term (FLambda)");
+ anomaly (Pp.str "conversion was given unreduced term (FLambda).");
let (_,_ty2,bd2) = destFLambda mk_clos hd2 in
eqappr univ CONV infos
(el_lift lft1,(hd1,eta_expand_stack v1)) (el_lift lft2,(bd2,[]))
@@ -479,7 +479,7 @@ let vm_conv cv_pb = fconv cv_pb true
let hnf_prod_app env t n =
match whd_all env t with
| Prod (_,_,b) -> subst1 n b
- | _ -> anomaly ~label:"hnf_prod_app" (Pp.str "Need a product")
+ | _ -> anomaly ~label:"hnf_prod_app" (Pp.str "Need a product.")
let hnf_prod_applist env t nl =
List.fold_left (hnf_prod_app env) t nl
@@ -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 11cd742ba..c70cd5c8c 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
@@ -89,6 +89,6 @@ let import file clib univs digest =
let unsafe_import file clib univs digest =
let env = !genv in
if !Flags.debug then check_imports Feedback.msg_warning clib.comp_name env clib.comp_deps
- else check_imports (errorlabstrm"unsafe_import") clib.comp_name env clib.comp_deps;
+ else check_imports (user_err ~hdr:"unsafe_import") clib.comp_name env clib.comp_deps;
check_engagement env clib.comp_enga;
full_add_module clib.comp_name clib.comp_mod univs digest
diff --git a/checker/subtyping.ml b/checker/subtyping.ml
index 7eae9b831..2d04b77e4 100644
--- a/checker/subtyping.ml
+++ b/checker/subtyping.ml
@@ -113,7 +113,7 @@ let check_inductive env mp1 l info1 mib2 spec2 subst1 subst2=
in
let check_inductive_type env t1 t2 =
- (* Due to sort-polymorphism in inductive types, the conclusions of
+ (* Due to template polymorphism, the conclusions of
t1 and t2, if in Type, are generated as the least upper bounds
of the types of the constructors.
@@ -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 591348cb6..75c566aeb 100644
--- a/checker/term.ml
+++ b/checker/term.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* This module instantiates the structure of generic deBruijn terms to Coq *)
+(* This module instantiates the structure of generic de Bruijn terms to Coq *)
open CErrors
open Util
@@ -94,7 +94,7 @@ let closedn n c =
in
try closed_rec n c; true with LocalOccur -> false
-(* [closed0 M] is true iff [M] is a (deBruijn) closed term *)
+(* [closed0 M] is true iff [M] is a (de Bruijn) closed term *)
let closed0 = closedn 0
@@ -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
@@ -333,7 +333,7 @@ let destArity =
| LetIn (x,b,t,c) -> prodec_rec (LocalDef (x,b,t)::l) c
| Cast (c,_,_) -> prodec_rec l c
| Sort s -> l,s
- | _ -> anomaly ~label:"destArity" (Pp.str "not an arity")
+ | _ -> anomaly ~label:"destArity" (Pp.str "not an arity.")
in
prodec_rec []
diff --git a/checker/term.mli b/checker/term.mli
index 0af83e05d..6b026d056 100644
--- a/checker/term.mli
+++ b/checker/term.mli
@@ -4,8 +4,6 @@ open Cic
val family_of_sort : sorts -> sorts_family
val family_equal : sorts_family -> sorts_family -> bool
-val strip_outer_cast : constr -> constr
-val collapse_appl : constr -> constr
val decompose_app : constr -> constr * constr list
val applist : constr * constr list -> constr
val iter_constr_with_binders :
diff --git a/checker/typeops.ml b/checker/typeops.ml
index 173e19ce1..0163db334 100644
--- a/checker/typeops.ml
+++ b/checker/typeops.ml
@@ -85,9 +85,6 @@ let type_of_constant_knowing_parameters env cst paramtyps =
let type_of_constant_type env t =
type_of_constant_type_knowing_parameters env t [||]
-let type_of_constant env cst =
- type_of_constant_knowing_parameters env cst [||]
-
let judge_of_constant_knowing_parameters env (kn,u as cst) paramstyp =
let _cb =
try lookup_constant kn env
@@ -265,7 +262,7 @@ let rec execute env cstr =
| Rel n -> judge_of_relative env n
- | Var _ -> anomaly (Pp.str "Section variable in Coqchk !")
+ | Var _ -> anomaly (Pp.str "Section variable in Coqchk!")
| Const c -> judge_of_constant env c
@@ -278,13 +275,11 @@ let rec execute env cstr =
let j =
match f with
| Ind ind ->
- (* Sort-polymorphism of inductive types *)
judge_of_inductive_knowing_parameters env ind jl
| Const cst ->
- (* Sort-polymorphism of constant *)
judge_of_constant_knowing_parameters env cst jl
| _ ->
- (* No sort-polymorphism *)
+ (* No template polymorphism *)
execute env f
in
let jl = Array.map2 (fun c ty -> c,ty) args jl in
@@ -349,10 +344,10 @@ let rec execute env cstr =
(* Partial proofs: unsupported by the kernel *)
| Meta _ ->
- anomaly (Pp.str "the kernel does not support metavariables")
+ anomaly (Pp.str "the kernel does not support metavariables.")
| Evar _ ->
- anomaly (Pp.str "the kernel does not support existential variables")
+ anomaly (Pp.str "the kernel does not support existential variables.")
and execute_type env constr =
let j = execute env constr in
diff --git a/checker/univ.ml b/checker/univ.ml
index 668f3a058..571743231 100644
--- a/checker/univ.ml
+++ b/checker/univ.ml
@@ -87,7 +87,6 @@ module HList = struct
val exists : (elt -> bool) -> t -> bool
val for_all : (elt -> bool) -> t -> bool
val for_all2 : (elt -> elt -> bool) -> t -> t -> bool
- val remove : elt -> t -> t
val to_list : t -> elt list
end
@@ -128,12 +127,6 @@ module HList = struct
| Nil -> []
| Cons (x, _, l) -> x :: to_list l
- let rec remove x = function
- | Nil -> nil
- | Cons (y, _, l) ->
- if H.eq x y then l
- else cons y (remove x l)
-
end
end
@@ -552,7 +545,7 @@ let repr g u =
let a =
try UMap.find u g
with Not_found -> anomaly ~label:"Univ.repr"
- (str"Universe " ++ Level.pr u ++ str" undefined")
+ (str"Universe " ++ Level.pr u ++ str" undefined.")
in
match a with
| Equiv v -> repr_rec v
@@ -855,7 +848,7 @@ let merge g arcu arcv =
else (max_rank, old_max_rank, best_arc, arc::rest)
in
match between g arcu arcv with
- | [] -> anomaly (str "Univ.between")
+ | [] -> anomaly (str "Univ.between.")
| arc::rest ->
let (max_rank, old_max_rank, best_arc, rest) =
List.fold_left best_ranked (arc.rank, min_int, arc, []) rest in
@@ -918,7 +911,7 @@ let enforce_univ_eq u v g =
| FastLT -> error_inconsistency Eq u v
| FastLE -> merge g arcv arcu
| FastNLE -> merge_disc g arcu arcv
- | FastEQ -> anomaly (Pp.str "Univ.compare"))
+ | FastEQ -> anomaly (Pp.str "Univ.compare."))
(* enforce_univ_leq : Level.t -> Level.t -> unit *)
(* enforce_univ_leq u v will force u<=v if possible, will fail otherwise *)
@@ -931,7 +924,7 @@ let enforce_univ_leq u v g =
| FastLT -> error_inconsistency Le u v
| FastLE -> merge g arcv arcu
| FastNLE -> fst (setleq g arcu arcv)
- | FastEQ -> anomaly (Pp.str "Univ.compare")
+ | FastEQ -> anomaly (Pp.str "Univ.compare.")
(* enforce_univ_lt u v will force u<v if possible, will fail otherwise *)
let enforce_univ_lt u v g =
@@ -944,7 +937,7 @@ let enforce_univ_lt u v g =
| FastNLE ->
match fast_compare_neq false g arcv arcu with
FastNLE -> fst (setlt g arcu arcv)
- | FastEQ -> anomaly (Pp.str "Univ.compare")
+ | FastEQ -> anomaly (Pp.str "Univ.compare.")
| FastLE | FastLT -> error_inconsistency Lt u v
(* Prop = Set is forbidden here. *)
@@ -1002,13 +995,13 @@ let constraint_add_leq v u c =
else if j <= -1 (* n = m+k, v+k <= u <-> v+(k-1) < u *) then
if Level.equal x y then (* u+(k+1) <= u *)
raise (UniverseInconsistency (Le, Universe.tip v, Universe.tip u))
- else anomaly (Pp.str"Unable to handle arbitrary u+k <= v constraints")
+ else anomaly (Pp.str"Unable to handle arbitrary u+k <= v constraints.")
else if j = 0 then
Constraint.add (x,Le,y) c
else (* j >= 1 *) (* m = n + k, u <= v+k *)
if Level.equal x y then c (* u <= u+k, trivial *)
else if Level.is_small x then c (* Prop,Set <= u+S k, trivial *)
- else anomaly (Pp.str"Unable to handle arbitrary u <= v+k constraints")
+ else anomaly (Pp.str"Unable to handle arbitrary u <= v+k constraints.")
let check_univ_leq_one u v = Universe.exists (Expr.leq u) v
@@ -1019,7 +1012,7 @@ let enforce_leq u v c =
match v with
| Universe.Huniv.Cons (v, _, Universe.Huniv.Nil) ->
Universe.Huniv.fold (fun u -> constraint_add_leq u v) u c
- | _ -> anomaly (Pp.str"A universe bound can only be a variable")
+ | _ -> anomaly (Pp.str"A universe bound can only be a variable.")
let enforce_leq u v c =
if check_univ_leq u v then c
diff --git a/checker/votour.ml b/checker/votour.ml
index 48f9f45e7..c255e5cdb 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.39.1) at 2024-06-29 01:39:28 +0000