aboutsummaryrefslogtreecommitdiffhomepage
path: root/library
diff options
context:
space:
mode:
Diffstat (limited to 'library')
-rw-r--r--library/declare.ml14
-rw-r--r--library/declaremods.ml4
-rw-r--r--library/decls.ml10
-rw-r--r--library/goptions.ml2
-rw-r--r--library/impargs.ml27
-rw-r--r--library/lib.ml39
-rw-r--r--library/lib.mli3
-rw-r--r--library/library.ml36
-rw-r--r--library/nametab.ml18
-rw-r--r--library/nametab.mli3
-rw-r--r--library/universes.ml2
11 files changed, 73 insertions, 85 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/decls.ml b/library/decls.ml
index 6e21880f1..2952c258a 100644
--- a/library/decls.ml
+++ b/library/decls.ml
@@ -14,6 +14,8 @@ open Names
open Decl_kinds
open Libnames
+module NamedDecl = Context.Named.Declaration
+
(** Datas associated to section variables and local definitions *)
type variable_data =
@@ -46,20 +48,18 @@ let constant_kind kn = Cmap.find kn !csttab
(** Miscellaneous functions. *)
-open Context.Named.Declaration
-
let initialize_named_context_for_proof () =
let sign = Global.named_context () in
List.fold_right
(fun d signv ->
- let id = get_id d in
- let d = if variable_opacity id then LocalAssum (id, get_type d) else d in
+ let id = NamedDecl.get_id d in
+ let d = if variable_opacity id then NamedDecl.LocalAssum (id, NamedDecl.get_type d) else d in
Environ.push_named_context_val d signv) sign Environ.empty_named_context_val
let last_section_hyps dir =
Context.Named.fold_outside
(fun d sec_ids ->
- let id = get_id d in
+ let id = NamedDecl.get_id d in
try if DirPath.equal dir (variable_path id) then id::sec_ids else sec_ids
with Not_found -> sec_ids)
(Environ.named_context (Global.env()))
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 bce7a15cb..ea2805b67 100644
--- a/library/impargs.ml
+++ b/library/impargs.ml
@@ -22,6 +22,9 @@ open Constrexpr
open Termops
open Namegen
open Decl_kinds
+open Context.Named.Declaration
+
+module NamedDecl = Context.Named.Declaration
(*s Flags governing the computation of implicit arguments *)
@@ -164,7 +167,6 @@ let update pos rig (na,st) =
(* modified is_rigid_reference with a truncated env *)
let is_flexible_reference env bound depth f =
- let open Context.Named.Declaration in
match kind_of_term f with
| Rel n when n >= bound+depth -> (* inductive type *) false
| Rel n when n >= depth -> (* previous argument *) true
@@ -173,7 +175,7 @@ let is_flexible_reference env bound depth f =
let cb = Environ.lookup_constant kn env in
(match cb.const_body with Def _ -> true | _ -> false)
| Var id ->
- Environ.lookup_named id env |> is_local_def
+ env |> Environ.lookup_named id |> is_local_def
| Ind _ | Construct _ -> false
| _ -> true
@@ -338,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
@@ -449,8 +451,7 @@ let compute_all_mib_implicits flags manual kn =
let compute_var_implicits flags manual id =
let env = Global.env () in
- let open Context.Named.Declaration in
- compute_semi_auto_implicits env flags manual (get_type (lookup_named id env))
+ compute_semi_auto_implicits env flags manual (NamedDecl.get_type (lookup_named id env))
(* Implicits of a global reference. *)
@@ -515,15 +516,11 @@ let subst_implicits (subst,(req,l)) =
(ImplLocal,List.smartmap (subst_implicits_decl subst) l)
let impls_of_context ctx =
- let map (id, impl, _, _) = match impl with
- | Implicit -> Some (id, Manual, (true, true))
+ let map (decl, impl) = match impl with
+ | Implicit -> Some (NamedDecl.get_id decl, Manual, (true, true))
| _ -> None
in
- let is_set (_, _, b, _) = match b with
- | None -> true
- | Some _ -> false
- in
- List.rev_map map (List.filter is_set ctx)
+ List.rev_map map (List.filter (fst %> is_local_assum) ctx)
let adjust_side_condition p = function
| LessArgsThan n -> LessArgsThan (n+p)
@@ -664,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 7218950da..9401bc55b 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -13,6 +13,9 @@ open Libnames
open Globnames
open Nameops
open Libobject
+open Context.Named.Declaration
+
+module NamedDecl = Context.Named.Declaration
type is_type = bool (* Module Type or just Module *)
type export = bool option (* None for a Module Type *)
@@ -75,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
@@ -267,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
@@ -277,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 =
@@ -322,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 -> ()
@@ -374,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."
@@ -388,7 +391,7 @@ let find_opening_node id =
- the list of substitution to do at section closing
*)
-type variable_info = Names.Id.t * Decl_kinds.binding_kind * Term.constr option * Term.types
+type variable_info = Context.Named.Declaration.t * Decl_kinds.binding_kind
type variable_context = variable_info list
type abstr_info = variable_context * Univ.universe_level_subst * Univ.UContext.t
@@ -428,12 +431,10 @@ let add_section_context ctx =
sectab := (Context ctx :: vars,repl,abs)::sl
let extract_hyps (secs,ohyps) =
- let open Context.Named.Declaration in
let rec aux = function
- | (Variable (id,impl,poly,ctx)::idl, decl::hyps) when Names.Id.equal id (get_id decl) ->
- let (id',b,t) = to_tuple decl in
+ | (Variable (id,impl,poly,ctx)::idl, decl::hyps) when Names.Id.equal id (NamedDecl.get_id decl) ->
let l, r = aux (idl,hyps) in
- (id',impl,b,t) :: l, if poly then Univ.ContextSet.union r ctx else r
+ (decl,impl) :: l, if poly then Univ.ContextSet.union r ctx else r
| (Variable (_,_,poly,ctx)::idl,hyps) ->
let l, r = aux (idl,hyps) in
l, if poly then Univ.ContextSet.union r ctx else r
@@ -443,17 +444,11 @@ let extract_hyps (secs,ohyps) =
| [], _ -> [],Univ.ContextSet.empty
in aux (secs,ohyps)
-let instance_from_variable_context sign =
- let rec inst_rec = function
- | (id,b,None,_) :: sign -> id :: inst_rec sign
- | _ :: sign -> inst_rec sign
- | [] -> [] in
- Array.of_list (inst_rec sign)
-
-let named_of_variable_context ctx = let open Context.Named.Declaration in
- List.map (function id,_,None,t -> LocalAssum (id,t)
- | id,_,Some b,t -> LocalDef (id,b,t))
- ctx
+let instance_from_variable_context =
+ List.map fst %> List.filter is_local_assum %> List.map NamedDecl.get_id %> Array.of_list
+
+let named_of_variable_context =
+ List.map fst
let add_section_replacement f g poly hyps =
match !sectab with
@@ -518,7 +513,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/lib.mli b/library/lib.mli
index 0a70152ef..845727059 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -160,8 +160,7 @@ val xml_open_section : (Names.Id.t -> unit) Hook.t
val xml_close_section : (Names.Id.t -> unit) Hook.t
(** {6 Section management for discharge } *)
-type variable_info = Names.Id.t * Decl_kinds.binding_kind *
- Term.constr option * Term.types
+type variable_info = Context.Named.Declaration.t * Decl_kinds.binding_kind
type variable_context = variable_info list
type abstr_info = variable_context * Univ.universe_level_subst * Univ.UContext.t
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 ()
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-12 12:20:48 +0000