diff options
author | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-09-08 14:56:33 +0200 |
---|---|---|
committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-09-08 15:41:16 +0200 |
commit | 13266ce4c37cb648b5e4e391aa5d7486bbcdb4ee (patch) | |
tree | f76fd37023c71c20520e34e4a51c487e7a0388a0 /library | |
parent | 79e7a0de25bcb2f10a7f3d1960a8f16eefdbb5a6 (diff) | |
parent | fc579fdc83b751a44a18d2373e86ab38806e7306 (diff) |
Merge PR #244.
Diffstat (limited to 'library')
-rw-r--r-- | library/declare.ml | 14 | ||||
-rw-r--r-- | library/declaremods.ml | 4 | ||||
-rw-r--r-- | library/goptions.ml | 2 | ||||
-rw-r--r-- | library/impargs.ml | 8 | ||||
-rw-r--r-- | library/lib.ml | 12 | ||||
-rw-r--r-- | library/library.ml | 36 | ||||
-rw-r--r-- | library/nametab.ml | 18 | ||||
-rw-r--r-- | library/nametab.mli | 3 | ||||
-rw-r--r-- | library/universes.ml | 2 |
9 files changed, 48 insertions, 51 deletions
diff --git a/library/declare.ml b/library/declare.ml index 3d063225f..cc8415cf4 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -462,8 +462,8 @@ let do_universe poly l = let in_section = Lib.sections_are_opened () in let () = if poly && not in_section then - user_err_loc (Loc.ghost, "Constraint", - str"Cannot declare polymorphic universes outside sections") + user_err ~hdr:"Constraint" + (str"Cannot declare polymorphic universes outside sections") in let l = List.map (fun (l, id) -> @@ -496,20 +496,20 @@ let do_constraint poly l = fun (loc, id) -> try Idmap.find id names with Not_found -> - user_err_loc (loc, "Constraint", str "Undeclared universe " ++ pr_id id) + user_err ~loc ~hdr:"Constraint" (str "Undeclared universe " ++ pr_id id) in let in_section = Lib.sections_are_opened () in let () = if poly && not in_section then - user_err_loc (Loc.ghost, "Constraint", - str"Cannot declare polymorphic constraints outside sections") + user_err ~hdr:"Constraint" + (str"Cannot declare polymorphic constraints outside sections") in let check_poly loc p loc' p' = if poly then () else if p || p' then let loc = if p then loc else loc' in - user_err_loc (loc, "Constraint", - str "Cannot declare a global constraint on " ++ + user_err ~loc ~hdr:"Constraint" + (str "Cannot declare a global constraint on " ++ str "a polymorphic universe, use " ++ str "Polymorphic Constraint instead") in diff --git a/library/declaremods.ml b/library/declaremods.ml index b2806a1ac..3a263b1e1 100644 --- a/library/declaremods.ml +++ b/library/declaremods.ml @@ -166,13 +166,13 @@ let consistency_checks exists dir dirinfo = let globref = try Nametab.locate_dir (qualid_of_dirpath dir) with Not_found -> - errorlabstrm "consistency_checks" + user_err ~hdr:"consistency_checks" (pr_dirpath dir ++ str " should already exist!") in assert (eq_global_dir_reference globref dirinfo) else if Nametab.exists_dir dir then - errorlabstrm "consistency_checks" + user_err ~hdr:"consistency_checks" (pr_dirpath dir ++ str " already exists") let compute_visibility exists i = diff --git a/library/goptions.ml b/library/goptions.ml index 1cf25987b..813bf30a3 100644 --- a/library/goptions.ml +++ b/library/goptions.ml @@ -36,7 +36,7 @@ type option_state = { let nickname table = String.concat " " table let error_undeclared_key key = - errorlabstrm "Goptions" (str (nickname key) ++ str ": no table or option of this type") + user_err ~hdr:"Goptions" (str (nickname key) ++ str ": no table or option of this type") (****************************************************************************) (* 1- Tables *) diff --git a/library/impargs.ml b/library/impargs.ml index 07b6b2bae..ea2805b67 100644 --- a/library/impargs.ml +++ b/library/impargs.ml @@ -340,14 +340,14 @@ let check_correct_manual_implicits autoimps l = List.iter (function | ExplByName id,(b,fi,forced) -> if not forced then - errorlabstrm "" + user_err (str "Wrong or non-dependent implicit argument name: " ++ pr_id id ++ str ".") | ExplByPos (i,_id),_t -> if i<1 || i>List.length autoimps then - errorlabstrm "" + user_err (str "Bad implicit argument number: " ++ int i ++ str ".") else - errorlabstrm "" + user_err (str "Cannot set implicit argument number " ++ int i ++ str ": it has no name.")) l @@ -661,7 +661,7 @@ let check_inclusion l = let check_rigidity isrigid = if not isrigid then - errorlabstrm "" (strbrk "Multiple sequences of implicit arguments available only for references that cannot be applied to an arbitrarily large number of arguments.") + user_err (strbrk "Multiple sequences of implicit arguments available only for references that cannot be applied to an arbitrarily large number of arguments.") let projection_implicits env p impls = let pb = Environ.lookup_projection p env in diff --git a/library/lib.ml b/library/lib.ml index a5a9a0194..749cc4ff3 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -78,7 +78,7 @@ let classify_segment seg = | (_,ClosedModule _) :: stk -> clean acc stk | (_,OpenedSection _) :: _ -> error "there are still opened sections" | (_,OpenedModule (ty,_,_,_)) :: _ -> - errorlabstrm "Lib.classify_segment" + user_err ~hdr:"Lib.classify_segment" (str "there are still opened " ++ str (module_kind ty) ++ str "s") | (_,FrozenState _) :: stk -> clean acc stk in @@ -270,7 +270,7 @@ let start_mod is_type export id mp fs = else Nametab.exists_module dir in if exists then - errorlabstrm "open_module" (pr_id id ++ str " already exists"); + user_err ~hdr:"open_module" (pr_id id ++ str " already exists"); add_entry (make_oname id) (OpenedModule (is_type,export,prefix,fs)); path_prefix := prefix; prefix @@ -280,7 +280,7 @@ let start_modtype = start_mod true None let error_still_opened string oname = let id = basename (fst oname) in - errorlabstrm "" + user_err (str "The " ++ str string ++ str " " ++ pr_id id ++ str " is still opened.") let end_mod is_type = @@ -325,7 +325,7 @@ let end_compilation_checks dir = try match snd (find_entry_p is_opening_node) with | OpenedSection _ -> error "There are some open sections." | OpenedModule (ty,_,_,_) -> - errorlabstrm "Lib.end_compilation_checks" + user_err ~hdr:"Lib.end_compilation_checks" (str "There are some open " ++ str (module_kind ty) ++ str "s.") | _ -> assert false with Not_found -> () @@ -377,7 +377,7 @@ let find_opening_node id = let oname,entry = find_entry_p is_opening_node in let id' = basename (fst oname) in if not (Names.Id.equal id id') then - errorlabstrm "Lib.find_opening_node" + user_err ~hdr:"Lib.find_opening_node" (str "Last block to end has name " ++ pr_id id' ++ str "."); entry with Not_found -> error "There is nothing to end." @@ -520,7 +520,7 @@ let open_section id = let dir = add_dirpath_suffix olddir id in let prefix = dir, (mp, add_dirpath_suffix oldsec id) in if Nametab.exists_section dir then - errorlabstrm "open_section" (pr_id id ++ str " already exists."); + user_err ~hdr:"open_section" (pr_id id ++ str " already exists."); let fs = Summary.freeze_summaries ~marshallable:`No in add_entry (make_oname id) (OpenedSection (prefix, fs)); (*Pushed for the lifetime of the section: removed by unfrozing the summary*) diff --git a/library/library.ml b/library/library.ml index d44f796a7..3086e3d18 100644 --- a/library/library.ml +++ b/library/library.ml @@ -131,7 +131,7 @@ let find_library dir = let try_find_library dir = try find_library dir with Not_found -> - errorlabstrm "Library.find_library" + user_err ~hdr:"Library.find_library" (str "Unknown library " ++ pr_dirpath dir) let register_library_filename dir f = @@ -329,12 +329,12 @@ let locate_qualified_library ?root ?(warn = true) qid = let error_unmapped_dir qid = let prefix, _ = repr_qualid qid in - errorlabstrm "load_absolute_library_from" + user_err ~hdr:"load_absolute_library_from" (str "Cannot load " ++ pr_qualid qid ++ str ":" ++ spc () ++ str "no physical path bound to" ++ spc () ++ pr_dirpath 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_qualid qid ++ str" in loadpath") let try_locate_absolute_library dir = @@ -378,7 +378,7 @@ let access_table what tables dp i = let t = try fetch_delayed f with Faulty f -> - errorlabstrm "Library.access_table" + user_err ~hdr:"Library.access_table" (str "The file " ++ str f ++ str " (bound to " ++ str dir_path ++ str ") is inaccessible or corrupted,\ncannot load some " ++ str what ++ str " in it.\n") @@ -463,7 +463,7 @@ let rec intern_library (needed, contents) (dir, f) from = let f = match f with Some f -> f | None -> try_locate_absolute_library dir in let m = intern_from_file f in if not (DirPath.equal dir m.library_name) then - errorlabstrm "load_physical_library" + user_err ~hdr:"load_physical_library" (str "The file " ++ str f ++ str " contains library" ++ spc () ++ pr_dirpath m.library_name ++ spc () ++ str "and not library" ++ spc() ++ pr_dirpath dir); @@ -477,7 +477,7 @@ and intern_library_deps libs dir m from = and intern_mandatory_library caller from libs (dir,d) = let digest, libs = intern_library libs (dir, None) (Some from) in if not (Safe_typing.digest_match ~actual:digest ~required:d) then - errorlabstrm "" (str "Compiled library " ++ pr_dirpath caller ++ + user_err (str "Compiled library " ++ pr_dirpath caller ++ str " (in file " ++ str from ++ str ") makes inconsistent assumptions \ over library " ++ pr_dirpath dir); libs @@ -582,8 +582,8 @@ let require_library_from_dirpath modrefl export = let safe_locate_module (loc,qid) = try Nametab.locate_module qid with Not_found -> - user_err_loc - (loc,"import_library", pr_qualid qid ++ str " is not a module") + user_err ~loc ~hdr:"import_library" + (pr_qualid qid ++ str " is not a module") let import_module export modl = (* Optimization: libraries in a raw in the list are imported @@ -607,8 +607,8 @@ let import_module export modl = flush acc; try Declaremods.import_module export mp; aux [] l with Not_found -> - user_err_loc (loc,"import_library", - pr_qualid dir ++ str " is not a module")) + user_err ~loc ~hdr:"import_library" + (pr_qualid dir ++ str " is not a module")) | [] -> flush acc in aux [] modl @@ -619,7 +619,7 @@ let check_coq_overwriting p id = let l = DirPath.repr p in let is_empty = match l with [] -> true | _ -> false in if not !Flags.boot && not is_empty && Id.equal (List.last l) coq_root then - errorlabstrm "" + user_err (str "Cannot build module " ++ pr_dirpath p ++ str "." ++ pr_id id ++ str "." ++ spc () ++ str "it starts with prefix \"Coq\" which is reserved for the Coq library.") @@ -632,7 +632,7 @@ let check_module_name s = (if c = '\'' then str "\"'\"" else (str "'" ++ str (String.make 1 c) ++ str "'")) ++ strbrk " is not allowed in module names\n" in - let err c = errorlabstrm "" (msg c) in + let err c = user_err (msg c) in match String.get s 0 with | 'a' .. 'z' | 'A' .. 'Z' -> for i = 1 to (String.length s)-1 do @@ -668,10 +668,10 @@ let load_library_todo f = let tasks, _, _ = System.marshal_in_segment f ch in let (s5 : seg_proofs), _, _ = System.marshal_in_segment f ch in close_in ch; - if tasks = None then errorlabstrm "restart" (str"not a .vio file"); - if s2 = None then errorlabstrm "restart" (str"not a .vio file"); - if s3 = None then errorlabstrm "restart" (str"not a .vio file"); - if pi3 (Option.get s2) then errorlabstrm "restart" (str"not a .vio file"); + if tasks = None then user_err ~hdr:"restart" (str"not a .vio file"); + if s2 = None then user_err ~hdr:"restart" (str"not a .vio file"); + if s3 = None then user_err ~hdr:"restart" (str"not a .vio file"); + if pi3 (Option.get s2) then user_err ~hdr:"restart" (str"not a .vio file"); longf, s0, s1, Option.get s2, Option.get s3, Option.get tasks, s5 (************************************************************************) @@ -687,7 +687,7 @@ let current_deps () = let current_reexports () = !libraries_exports_list let error_recursively_dependent_library dir = - errorlabstrm "" + user_err (strbrk "Unable to use logical name " ++ pr_dirpath dir ++ strbrk " to save current library because" ++ strbrk " it already depends on a library of this name.") @@ -734,7 +734,7 @@ let save_library_to ?todo dir f otab = except Int.Set.empty in let is_done_or_todo i x = Future.is_val x || Int.Set.mem i except in Array.iteri (fun i x -> - if not(is_done_or_todo i x) then CErrors.errorlabstrm "library" + if not(is_done_or_todo i x) then CErrors.user_err ~hdr:"library" Pp.(str"Proof object "++int i++str" is not checked nor to be checked")) opaque_table; let sd = { diff --git a/library/nametab.ml b/library/nametab.ml index fa5db37ed..b76048e89 100644 --- a/library/nametab.ml +++ b/library/nametab.ml @@ -16,10 +16,8 @@ open Globnames exception GlobalizationError of qualid -let error_global_not_found_loc loc q = - Loc.raise loc (GlobalizationError q) - -let error_global_not_found q = raise (GlobalizationError q) +let error_global_not_found ?loc q = + Loc.raise ?loc (GlobalizationError q) (* Kinds of global names *) @@ -455,11 +453,11 @@ let global r = try match locate_extended qid with | TrueGlobal ref -> ref | SynDef _ -> - user_err_loc (loc,"global", - str "Unexpected reference to a notation: " ++ - pr_qualid qid) + user_err ~loc ~hdr:"global" + (str "Unexpected reference to a notation: " ++ + pr_qualid qid) with Not_found -> - error_global_not_found_loc loc qid + error_global_not_found ~loc qid (* Exists functions ********************************************************) @@ -534,8 +532,8 @@ let global_inductive r = match global r with | IndRef ind -> ind | ref -> - user_err_loc (loc_of_reference r,"global_inductive", - pr_reference r ++ spc () ++ str "is not an inductive type") + user_err ~loc:(loc_of_reference r) ~hdr:"global_inductive" + (pr_reference r ++ spc () ++ str "is not an inductive type") (********************************************************************) diff --git a/library/nametab.mli b/library/nametab.mli index a8a0572b3..d20c399b6 100644 --- a/library/nametab.mli +++ b/library/nametab.mli @@ -60,8 +60,7 @@ open Globnames exception GlobalizationError of qualid (** Raises a globalization error *) -val error_global_not_found_loc : Loc.t -> qualid -> 'a -val error_global_not_found : qualid -> 'a +val error_global_not_found : ?loc:Loc.t -> qualid -> 'a (** {6 Register visibility of things } *) diff --git a/library/universes.ml b/library/universes.ml index db95607f1..32eb35386 100644 --- a/library/universes.ml +++ b/library/universes.ml @@ -337,7 +337,7 @@ let existing_instance ctx inst = and a2 = Instance.to_array (UContext.instance ctx) in let len1 = Array.length a1 and len2 = Array.length a2 in if not (len1 == len2) then - CErrors.errorlabstrm "Universes" + CErrors.user_err ~hdr:"Universes" (str "Polymorphic constant expected " ++ int len2 ++ str" levels but was given " ++ int len1) else () |