Creating a module Nameops.Name extending module Names.Name.

This module collects the functions of Nameops which are about Name.t
and somehow standardize or improve their name, resulting in particular
from discussions in working group.

Note the use of a dedicated exception rather than a failwith for
Nameops.Name.out.

Drawback of the approach: one needs to open Nameops, or to use long
prefix Nameops.Name.

2 files changed, 126 insertions, 31 deletions

diff --git a/library/nameops.ml b/library/nameops.ml
index 098f5112f..b73bd7eb3 100644
--- a/library/nameops.ml
+++ b/library/nameops.ml
@@ -14,10 +14,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 +120,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 3a67b61a1..abfc09db8 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