From a4c7f8bd98be2a200489325ff7c5061cf80ab4f3 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 27 Dec 2016 16:53:30 +0100 Subject: Imported Upstream version 8.6 --- checker/checker.ml | 48 ++++++++++++++++++------------------------------ 1 file changed, 18 insertions(+), 30 deletions(-) (limited to 'checker/checker.ml') diff --git a/checker/checker.ml b/checker/checker.ml index 825fb4dc..8dbb7e01 100644 --- a/checker/checker.ml +++ b/checker/checker.ml @@ -7,7 +7,7 @@ (************************************************************************) open Pp -open Errors +open CErrors open Util open System open Flags @@ -16,8 +16,10 @@ open Check let () = at_exit flush_all +let chk_pp = Pp.pp_with Format.std_formatter + let fatal_error info anomaly = - flush_all (); pperrnl info; flush_all (); + flush_all (); Feedback.msg_error info; flush_all (); exit (if anomaly then 129 else 1) let coq_root = Id.of_string "Coq" @@ -67,12 +69,12 @@ let add_path ~unix_path:dir ~coq_root:coq_dirpath = Check.add_load_path (dir,coq_dirpath) end else - msg_warning (str "Cannot open " ++ str dir) + Feedback.msg_warning (str "Cannot open " ++ str dir) let convert_string d = try Id.of_string d - with Errors.UserError _ -> - if_verbose msg_warning + with CErrors.UserError _ -> + if_verbose Feedback.msg_warning (str "Directory " ++ str d ++ str " cannot be used as a Coq identifier (skipped)"); raise Exit @@ -90,7 +92,7 @@ let add_rec_path ~unix_path ~coq_root = List.iter Check.add_load_path dirs; Check.add_load_path (unix_path, coq_root) else - msg_warning (str "Cannot open " ++ str unix_path) + Feedback.msg_warning (str "Cannot open " ++ str unix_path) (* By the option -include -I or -R of the command line *) let includes = ref [] @@ -123,7 +125,7 @@ let init_load_path () = add_rec_path ~unix_path:user_contrib ~coq_root:Check.default_root_prefix; (* then directories in XDG_DATA_DIRS and XDG_DATA_HOME *) List.iter (fun s -> add_rec_path ~unix_path:s ~coq_root:Check.default_root_prefix) - (xdg_dirs ~warn:(fun x -> msg_warning (str x))); + (xdg_dirs ~warn:(fun x -> Feedback.msg_warning (str x))); (* then directories in COQPATH *) List.iter (fun s -> add_rec_path ~unix_path:s ~coq_root:Check.default_root_prefix) coqpath; (* then current directory *) @@ -140,9 +142,7 @@ let set_debug () = Flags.debug := true let impredicative_set = ref Cic.PredicativeSet let set_impredicative_set () = impredicative_set := Cic.ImpredicativeSet -let type_in_type = ref Cic.StratifiedType -let set_type_in_type () = type_in_type := Cic.TypeInType -let engage () = Safe_typing.set_engagement (!impredicative_set,!type_in_type) +let engage () = Safe_typing.set_engagement (!impredicative_set) let admit_list = ref ([] : section_path list) @@ -179,10 +179,7 @@ let print_usage_channel co command = output_string co command; output_string co "coqchk options are:\n"; output_string co -" -I dir -as coqdir map physical dir to logical coqdir\ -\n -I dir map directory dir to the empty logical path\ -\n -include dir (idem)\ -\n -R dir coqdir recursively map physical dir to logical coqdir\ +" -R dir coqdir map physical dir to logical coqdir\ \n\ \n -admit module load module and dependencies without checking\ \n -norec module check module but admit dependencies without checking\ @@ -195,7 +192,6 @@ let print_usage_channel co command = \n -silent disable trace of constants being checked\ \n\ \n -impredicative-set set sort Set impredicative\ -\n -type-in-type collapse type hierarchy\ \n\ \n -h, --help print this list of options\ \n" @@ -215,14 +211,9 @@ let usage () = open Type_errors let anomaly_string () = str "Anomaly: " -let report () = (str "." ++ spc () ++ str "Please report.") +let report () = (str "." ++ spc () ++ str "Please report" ++ + strbrk "at " ++ str Coq_config.wwwbugtracker ++ str ".") -let print_loc loc = - if loc = Loc.ghost then - (str"") - else - let loc = Loc.unloc loc in - (int (fst loc) ++ str"-" ++ int (snd loc)) let guill s = str "\"" ++ str s ++ str "\"" let where s = @@ -294,7 +285,8 @@ let rec explain_exn = function Format.printf "@\nis not convertible with@\n"; Print.print_pure_constr a; Format.printf "@\n====== universes ====@\n"; - Pp.pp (Univ.pr_universes + chk_pp + (Univ.pr_universes (ctx.Environ.env_stratification.Environ.env_universes)); str "\nCantApplyBadType at argument " ++ int n | CantApplyNonFunctional _ -> str"CantApplyNonFunctional" @@ -315,15 +307,13 @@ let rec explain_exn = function str ", characters " ++ int e ++ str "-" ++ int (e+6) ++ str ")")) ++ report ()) - | e -> Errors.print e (* for anomalies and other uncaught exceptions *) + | e -> CErrors.print e (* for anomalies and other uncaught exceptions *) let parse_args argv = let rec parse = function | [] -> () | "-impredicative-set" :: rem -> set_impredicative_set (); parse rem - | "-type-in-type" :: rem -> - set_type_in_type (); parse rem | "-coqlib" :: s :: rem -> if not (exists_dir s) then @@ -337,15 +327,13 @@ let parse_args argv = | ("-I"|"-include") :: d :: rem -> set_default_include d; parse rem | ("-I"|"-include") :: [] -> usage () - | "-R" :: d :: "-as" :: p :: rem -> set_rec_include d p;parse rem - | "-R" :: d :: "-as" :: [] -> usage () | "-R" :: d :: p :: rem -> set_rec_include d p;parse rem | "-R" :: ([] | [_]) -> usage () | "-debug" :: rem -> set_debug (); parse rem | "-where" :: _ -> - Envars.set_coqlib ~fail:Errors.error; + Envars.set_coqlib ~fail:CErrors.error; print_endline (Envars.coqlib ()); exit 0 @@ -383,7 +371,7 @@ let init_with_argv argv = try parse_args argv; if !Flags.debug then Printexc.record_backtrace true; - Envars.set_coqlib ~fail:Errors.error; + Envars.set_coqlib ~fail:CErrors.error; if_verbose print_header (); init_load_path (); engage (); -- cgit v1.2.3