aboutsummaryrefslogtreecommitdiff
path: root/library
diff options
context:
space:
mode:
Diffstat (limited to 'library')
-rw-r--r--library/coqlib.ml8
-rw-r--r--library/declare.ml6
-rw-r--r--library/declaremods.ml4
-rw-r--r--library/global.ml2
-rw-r--r--library/globnames.ml2
-rw-r--r--library/goptions.ml14
-rw-r--r--library/heads.ml3
-rw-r--r--library/impargs.ml8
-rw-r--r--library/kindops.ml4
-rw-r--r--library/lib.ml6
-rw-r--r--library/loadpath.ml2
-rw-r--r--library/nameops.ml97
-rw-r--r--library/nameops.mli61
-rw-r--r--library/nametab.ml2
-rw-r--r--library/summary.ml6
15 files changed, 160 insertions, 65 deletions
diff --git a/library/coqlib.ml b/library/coqlib.ml
index 955ff4c089..0cb8c7afcf 100644
--- a/library/coqlib.ml
+++ b/library/coqlib.ml
@@ -52,14 +52,14 @@ let gen_reference_in_modules locstr dirs s =
| [] ->
anomaly ~label:locstr (str "cannot find " ++ str s ++
str " in module" ++ str (if List.length dirs > 1 then "s " else " ") ++
- prlist_with_sep pr_comma pr_dirpath dirs)
+ prlist_with_sep pr_comma pr_dirpath dirs ++ str ".")
| l ->
anomaly ~label:locstr
(str "ambiguous name " ++ str s ++ str " can represent " ++
prlist_with_sep pr_comma
(fun x -> Libnames.pr_path (Nametab.path_of_global x)) l ++
str " in module" ++ str (if List.length dirs > 1 then "s " else " ") ++
- prlist_with_sep pr_comma pr_dirpath dirs)
+ prlist_with_sep pr_comma pr_dirpath dirs ++ str ".")
(* For tactics/commands requiring vernacular libraries *)
@@ -185,7 +185,7 @@ let build_bool_type () =
andb_prop = init_reference ["Datatypes"] "andb_prop";
andb_true_intro = init_reference ["Datatypes"] "andb_true_intro" }
-let build_sigma_set () = anomaly (Pp.str "Use build_sigma_type")
+let build_sigma_set () = anomaly (Pp.str "Use build_sigma_type.")
let build_sigma_type () =
{ proj1 = init_reference ["Specif"] "projT1";
@@ -368,7 +368,7 @@ let coq_eq_ref = lazy (init_reference ["Logic"] "eq")
let coq_identity_ref = lazy (init_reference ["Datatypes"] "identity")
let coq_jmeq_ref = lazy (find_reference "Coqlib" [coq;"Logic";"JMeq"] "JMeq")
let coq_eq_true_ref = lazy (find_reference "Coqlib" [coq;"Init";"Datatypes"] "eq_true")
-let coq_existS_ref = lazy (anomaly (Pp.str "use coq_existT_ref"))
+let coq_existS_ref = lazy (anomaly (Pp.str "use coq_existT_ref."))
let coq_existT_ref = lazy (init_reference ["Specif"] "existT")
let coq_exist_ref = lazy (init_reference ["Specif"] "exist")
let coq_not_ref = lazy (init_reference ["Logic"] "not")
diff --git a/library/declare.ml b/library/declare.ml
index 95b3674c3e..7d0edbc8b3 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -149,7 +149,7 @@ let cache_constant ((sp,kn), obj) =
obj.cst_was_seff <- false;
if Global.exists_objlabel (Label.of_id (basename sp))
then constant_of_kn kn
- else CErrors.anomaly Pp.(str"Ex seff not found: " ++ Id.print(basename sp))
+ else CErrors.anomaly Pp.(str"Ex seff not found: " ++ Id.print(basename sp) ++ str".")
end else
let () = check_exists sp in
let kn', exported = Global.add_constant dir id obj.cst_decl in
@@ -385,7 +385,7 @@ let declare_projections mind =
let declare_mind mie =
let id = match mie.mind_entry_inds with
| ind::_ -> ind.mind_entry_typename
- | [] -> anomaly (Pp.str "cannot declare an empty list of inductives") in
+ | [] -> anomaly (Pp.str "cannot declare an empty list of inductives.") in
let (sp,kn as oname) = add_leaf id (inInductive ([],mie)) in
let mind = Global.mind_of_delta_kn kn in
let isrecord,isprim = declare_projections mind in
@@ -400,7 +400,7 @@ let pr_rank i = pr_nth (i+1)
let fixpoint_message indexes l =
Flags.if_verbose Feedback.msg_info (match l with
- | [] -> anomaly (Pp.str "no recursive definition")
+ | [] -> anomaly (Pp.str "no recursive definition.")
| [id] -> pr_id id ++ str " is recursively defined" ++
(match indexes with
| Some [|i|] -> str " (decreasing on "++pr_rank i++str " argument)"
diff --git a/library/declaremods.ml b/library/declaremods.ml
index 08c33b5c15..c98d4a7f31 100644
--- a/library/declaremods.ml
+++ b/library/declaremods.ml
@@ -252,7 +252,7 @@ let in_modkeep : Lib.lib_objects -> obj =
let do_modtype i sp mp sobjs =
if Nametab.exists_modtype sp then
- anomaly (pr_path sp ++ str " already exists");
+ anomaly (pr_path sp ++ str " already exists.");
Nametab.push_modtype (Nametab.Until i) sp mp;
ModSubstObjs.set mp sobjs
@@ -883,7 +883,7 @@ let register_library dir cenv (objs:library_objects) digest univ =
(* If not, let's do it now ... *)
let mp' = Global.import cenv univ digest in
if not (ModPath.equal mp mp') then
- anomaly (Pp.str "Unexpected disk module name");
+ anomaly (Pp.str "Unexpected disk module name.");
in
let sobjs,keepobjs = objs in
do_module false Lib.load_objects 1 dir mp ([],Objs sobjs) keepobjs
diff --git a/library/global.ml b/library/global.ml
index 5fa710b360..1ba86699d3 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -44,7 +44,7 @@ let () =
let assert_not_parsing () =
if !Flags.we_are_parsing then
CErrors.anomaly (
- Pp.strbrk"The global environment cannot be accessed during parsing")
+ Pp.strbrk"The global environment cannot be accessed during parsing.")
let safe_env () = assert_not_parsing(); !global_env
diff --git a/library/globnames.ml b/library/globnames.ml
index a78f5f13a9..9aeb379737 100644
--- a/library/globnames.ml
+++ b/library/globnames.ml
@@ -242,4 +242,4 @@ let pop_global_reference = function
| ConstRef con -> ConstRef (pop_con con)
| IndRef (kn,i) -> IndRef (pop_kn kn,i)
| ConstructRef ((kn,i),j) -> ConstructRef ((pop_kn kn,i),j)
- | VarRef id -> anomaly (Pp.str "VarRef not poppable")
+ | VarRef id -> anomaly (Pp.str "VarRef not poppable.")
diff --git a/library/goptions.ml b/library/goptions.ml
index a803771cbc..a305214e82 100644
--- a/library/goptions.ml
+++ b/library/goptions.ml
@@ -273,23 +273,23 @@ type 'a write_function = 'a -> unit
let declare_int_option =
declare_option
(fun v -> IntValue v)
- (function IntValue v -> v | _ -> anomaly (Pp.str "async_option"))
- (fun _ _ -> anomaly (Pp.str "async_option"))
+ (function IntValue v -> v | _ -> anomaly (Pp.str "async_option."))
+ (fun _ _ -> anomaly (Pp.str "async_option."))
let declare_bool_option =
declare_option
(fun v -> BoolValue v)
- (function BoolValue v -> v | _ -> anomaly (Pp.str "async_option"))
- (fun _ _ -> anomaly (Pp.str "async_option"))
+ (function BoolValue v -> v | _ -> anomaly (Pp.str "async_option."))
+ (fun _ _ -> anomaly (Pp.str "async_option."))
let declare_string_option =
declare_option
(fun v -> StringValue v)
- (function StringValue v -> v | _ -> anomaly (Pp.str "async_option"))
+ (function StringValue v -> v | _ -> anomaly (Pp.str "async_option."))
(fun x y -> x^","^y)
let declare_stringopt_option =
declare_option
(fun v -> StringOptValue v)
- (function StringOptValue v -> v | _ -> anomaly (Pp.str "async_option"))
- (fun _ _ -> anomaly (Pp.str "async_option"))
+ (function StringOptValue v -> v | _ -> anomaly (Pp.str "async_option."))
+ (fun _ _ -> anomaly (Pp.str "async_option."))
(* 3- User accessible commands *)
diff --git a/library/heads.ml b/library/heads.ml
index 02465f22fc..6aee63c744 100644
--- a/library/heads.ml
+++ b/library/heads.ml
@@ -72,7 +72,8 @@ let kind_of_head env t =
with Not_found ->
CErrors.anomaly
Pp.(str "constant not found in kind_of_head: " ++
- str (Names.Constant.to_string cst)))
+ Names.Constant.print cst ++
+ str "."))
| Construct _ | CoFix _ ->
if b then NotImmediatelyComputableHead else ConstructorHead
| Sort _ | Ind _ | Prod _ -> RigidHead RigidType
diff --git a/library/impargs.ml b/library/impargs.ml
index 885185da1a..8f3bfc17e4 100644
--- a/library/impargs.ml
+++ b/library/impargs.ml
@@ -291,16 +291,16 @@ let is_status_implicit = function
| _ -> true
let name_of_implicit = function
- | None -> anomaly (Pp.str "Not an implicit argument")
+ | None -> anomaly (Pp.str "Not an implicit argument.")
| Some (id,_,_) -> id
let maximal_insertion_of = function
| Some (_,_,(b,_)) -> b
- | None -> anomaly (Pp.str "Not an implicit argument")
+ | None -> anomaly (Pp.str "Not an implicit argument.")
let force_inference_of = function
| Some (_, _, (_, b)) -> b
- | None -> anomaly (Pp.str "Not an implicit argument")
+ | None -> anomaly (Pp.str "Not an implicit argument.")
(* [in_ctx] means we know the expected type, [n] is the index of the argument *)
let is_inferable_implicit in_ctx n = function
@@ -324,7 +324,7 @@ let positions_of_implicits (_,impls) =
let rec prepare_implicits f = function
| [] -> []
- | (Anonymous, Some _)::_ -> anomaly (Pp.str "Unnamed implicit")
+ | (Anonymous, Some _)::_ -> anomaly (Pp.str "Unnamed implicit.")
| (Name id, Some imp)::imps ->
let imps' = prepare_implicits f imps in
Some (id,imp,(set_maximality imps' f.maximal,true)) :: imps'
diff --git a/library/kindops.ml b/library/kindops.ml
index 21b1bec33c..623d2537aa 100644
--- a/library/kindops.ml
+++ b/library/kindops.ml
@@ -25,7 +25,7 @@ let string_of_theorem_kind = function
let string_of_definition_kind def =
let (locality, poly, kind) = def in
- let error () = CErrors.anomaly (Pp.str "Internal definition kind") in
+ let error () = CErrors.anomaly (Pp.str "Internal definition kind.") in
match kind with
| Definition ->
begin match locality with
@@ -64,4 +64,4 @@ let string_of_definition_kind def =
| Global -> "Global Instance"
end
| (StructureComponent|Scheme|CoFixpoint|Fixpoint|IdentityCoercion|Method) ->
- CErrors.anomaly (Pp.str "Internal definition kind")
+ CErrors.anomaly (Pp.str "Internal definition kind.")
diff --git a/library/lib.ml b/library/lib.ml
index 4ad4e261d7..9d71a854f0 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -350,7 +350,7 @@ let end_compilation_checks dir =
try match find_entry_p is_opening_lib with
| (oname, CompilingLibrary prefix) -> oname
| _ -> assert false
- with Not_found -> anomaly (Pp.str "No module declared")
+ with Not_found -> anomaly (Pp.str "No module declared.")
in
let _ =
match !lib_state.comp_name with
@@ -358,7 +358,7 @@ let end_compilation_checks dir =
| Some m ->
if not (Names.DirPath.equal m dir) then anomaly
(str "The current open module has name" ++ spc () ++ pr_dirpath m ++
- spc () ++ str "and not" ++ spc () ++ pr_dirpath m);
+ spc () ++ str "and not" ++ spc () ++ pr_dirpath m ++ str ".");
in
oname
@@ -547,7 +547,7 @@ let discharge_item ((sp,_ as oname),e) =
| FrozenState _ -> None
| ClosedSection _ | ClosedModule _ -> None
| OpenedSection _ | OpenedModule _ | CompilingLibrary _ ->
- anomaly (Pp.str "discharge_item")
+ anomaly (Pp.str "discharge_item.")
let close_section () =
let oname,fs =
diff --git a/library/loadpath.ml b/library/loadpath.ml
index 529b9502b0..ad429ea840 100644
--- a/library/loadpath.ml
+++ b/library/loadpath.ml
@@ -29,7 +29,7 @@ let physical p = p.path_physical
let get_load_paths () = !load_paths
let anomaly_too_many_paths path =
- anomaly (str "Several logical paths are associated to" ++ spc () ++ str path)
+ anomaly (str "Several logical paths are associated to" ++ spc () ++ str path ++ str ".")
let find_load_path phys_dir =
let phys_dir = CUnix.canonical_path_name phys_dir in
diff --git a/library/nameops.ml b/library/nameops.ml
index 098f5112fd..0b5dfd8d0e 100644
--- a/library/nameops.ml
+++ b/library/nameops.ml
@@ -6,7 +6,6 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-open Pp
open Util
open Names
@@ -14,10 +13,6 @@ open Names
let pr_id id = Id.print id
-let pr_name = function
- | Anonymous -> str "_"
- | Name id -> pr_id id
-
(* Utilities *)
let code_of_0 = Char.code '0'
@@ -124,34 +119,82 @@ let atompart_of_id id = fst (repr_ident id)
(* Names *)
-let out_name = function
- | Name id -> id
- | Anonymous -> failwith "Nameops.out_name"
+module type ExtName =
+sig
+
+ include module type of struct include Names.Name end
+
+ exception IsAnonymous
+
+ val fold_left : ('a -> Id.t -> 'a) -> 'a -> t -> 'a
+ val fold_right : (Id.t -> 'a -> 'a) -> t -> 'a -> 'a
+ val iter : (Id.t -> unit) -> t -> unit
+ val map : (Id.t -> Id.t) -> t -> t
+ val fold_map : ('a -> Id.t -> 'a * Id.t) -> 'a -> t -> 'a * t
+ val get_id : t -> Id.t
+ val pick : t -> t -> t
+ val cons : t -> Id.t list -> Id.t list
+ val to_option : Name.t -> Id.t option
+
+end
+
+module Name : ExtName =
+struct
+
+ include Names.Name
+
+ exception IsAnonymous
+
+ let fold_left f a = function
+ | Name id -> f a id
+ | Anonymous -> a
+
+ let fold_right f na a =
+ match na with
+ | Name id -> f id a
+ | Anonymous -> a
+
+ let iter f na = fold_right (fun x () -> f x) na ()
+
+ let map f = function
+ | Name id -> Name (f id)
+ | Anonymous -> Anonymous
+
+ let fold_map f a = function
+ | Name id -> let (a, id) = f a id in (a, Name id)
+ | Anonymous -> a, Anonymous
+
+ let get_id = function
+ | Name id -> id
+ | Anonymous -> raise IsAnonymous
-let name_fold f na a =
- match na with
- | Name id -> f id a
- | Anonymous -> a
+ let pick na1 na2 =
+ match na1 with
+ | Name _ -> na1
+ | Anonymous -> na2
-let name_iter f na = name_fold (fun x () -> f x) na ()
+ let cons na l =
+ match na with
+ | Anonymous -> l
+ | Name id -> id::l
-let name_cons na l =
- match na with
- | Anonymous -> l
- | Name id -> id::l
+ let to_option = function
+ | Anonymous -> None
+ | Name id -> Some id
-let name_app f = function
- | Name id -> Name (f id)
- | Anonymous -> Anonymous
+end
-let name_fold_map f e = function
- | Name id -> let (e,id) = f e id in (e,Name id)
- | Anonymous -> e,Anonymous
+open Name
-let name_max na1 na2 =
- match na1 with
- | Name _ -> na1
- | Anonymous -> na2
+(* Compatibility *)
+let out_name = get_id
+let name_fold = fold_right
+let name_iter = iter
+let name_app = map
+let name_fold_map = fold_map
+let name_cons = cons
+let name_max = pick
+let pr_name = print
let pr_lab l = Label.print l
diff --git a/library/nameops.mli b/library/nameops.mli
index 3a67b61a13..abfc09db8d 100644
--- a/library/nameops.mli
+++ b/library/nameops.mli
@@ -9,8 +9,6 @@
open Names
(** Identifiers and names *)
-val pr_id : Id.t -> Pp.std_ppcmds
-val pr_name : Name.t -> Pp.std_ppcmds
val make_ident : string -> int option -> Id.t
val repr_ident : Id.t -> string * int option
@@ -50,16 +48,69 @@ val increment_subscript : Id.t -> Id.t
val forget_subscript : Id.t -> Id.t
+module Name : sig
+
+ include module type of struct include Names.Name end
+
+ exception IsAnonymous
+
+ val fold_left : ('a -> Id.t -> 'a) -> 'a -> Name.t -> 'a
+ (** [fold_left f na a] is [f id a] if [na] is [Name id], and [a] otherwise. *)
+
+ val fold_right : (Id.t -> 'a -> 'a) -> Name.t -> 'a -> 'a
+ (** [fold_right f a na] is [f a id] if [na] is [Name id], and [a] otherwise. *)
+
+ val iter : (Id.t -> unit) -> Name.t -> unit
+ (** [iter f na] does [f id] if [na] equals [Name id], nothing otherwise. *)
+
+ val map : (Id.t -> Id.t) -> Name.t -> t
+ (** [map f na] is [Anonymous] if [na] is [Anonymous] and [Name (f id)] if [na] is [Name id]. *)
+
+ val fold_map : ('a -> Id.t -> 'a * Id.t) -> 'a -> Name.t -> 'a * Name.t
+ (** [fold_map f na a] is [a',Name id'] when [na] is [Name id] and [f a id] is [(a',id')].
+ It is [a,Anonymous] otherwise. *)
+
+ val get_id : Name.t -> Id.t
+ (** [get_id] associates [id] to [Name id]. @raise IsAnonymous otherwise. *)
+
+ val pick : Name.t -> Name.t -> Name.t
+ (** [pick na na'] returns [Anonymous] if both names are [Anonymous].
+ Pick one of [na] or [na'] otherwise. *)
+
+ val cons : Name.t -> Id.t list -> Id.t list
+ (** [cons na l] returns [id::l] if [na] is [Name id] and [l] otherwise. *)
+
+ val to_option : Name.t -> Id.t option
+ (** [to_option Anonymous] is [None] and [to_option (Name id)] is [Some id] *)
+
+end
+
val out_name : Name.t -> Id.t
-(** [out_name] associates [id] to [Name id]. Raises [Failure "Nameops.out_name"]
- otherwise. *)
+(** @deprecated Same as [Name.get_id] *)
val name_fold : (Id.t -> 'a -> 'a) -> Name.t -> 'a -> 'a
+(** @deprecated Same as [Name.fold_right] *)
+
val name_iter : (Id.t -> unit) -> Name.t -> unit
-val name_cons : Name.t -> Id.t list -> Id.t list
+(** @deprecated Same as [Name.iter] *)
+
val name_app : (Id.t -> Id.t) -> Name.t -> Name.t
+(** @deprecated Same as [Name.map] *)
+
val name_fold_map : ('a -> Id.t -> 'a * Id.t) -> 'a -> Name.t -> 'a * Name.t
+(** @deprecated Same as [Name.fold_map] *)
+
val name_max : Name.t -> Name.t -> Name.t
+(** @deprecated Same as [Name.pick] *)
+
+val name_cons : Name.t -> Id.t list -> Id.t list
+(** @deprecated Same as [Name.cons] *)
+
+val pr_name : Name.t -> Pp.std_ppcmds
+(** @deprecated Same as [Name.print] *)
+
+val pr_id : Id.t -> Pp.std_ppcmds
+(** @deprecated Same as [Names.Id.print] *)
val pr_lab : Label.t -> Pp.std_ppcmds
diff --git a/library/nametab.ml b/library/nametab.ml
index 2e4e98013e..93e9c03cee 100644
--- a/library/nametab.ml
+++ b/library/nametab.ml
@@ -294,7 +294,7 @@ module DirPath' =
struct
include DirPath
let repr dir = match DirPath.repr dir with
- | [] -> anomaly (Pp.str "Empty dirpath")
+ | [] -> anomaly (Pp.str "Empty dirpath.")
| id :: l -> (id, l)
end
diff --git a/library/summary.ml b/library/summary.ml
index d9f6441003..c7bf95fd41 100644
--- a/library/summary.ml
+++ b/library/summary.ml
@@ -46,7 +46,7 @@ let declare_summary sumname decl =
let () = if Int.Map.mem hash !summaries then
let (name, _) = Int.Map.find hash !summaries in
anomaly ~label:"Summary.declare_summary"
- (str "Colliding summary names: " ++ str sumname ++ str " vs. " ++ str name)
+ (str "Colliding summary names: " ++ str sumname ++ str " vs. " ++ str name ++ str ".")
in
all_declared_summaries := Int.Set.add hash !all_declared_summaries;
summary_names := (hash, sumname) :: !summary_names;
@@ -85,10 +85,10 @@ let unfreeze_summaries fs =
* may modify the content of [summaries] ny loading new ML modules *)
let (_, decl) =
try Int.Map.find ml_modules_summary !summaries
- with Not_found -> anomaly (str "Undeclared summary " ++ str ml_modules)
+ with Not_found -> anomaly (str "Undeclared summary " ++ str ml_modules ++ str ".")
in
let () = match fs.ml_module with
- | None -> anomaly (str "Undeclared summary " ++ str ml_modules)
+ | None -> anomaly (str "Undeclared summary " ++ str ml_modules ++ str ".")
| Some state -> decl.unfreeze_function state
in
let fold id (_, decl) states =
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-08 05:47:38 +0000