Merge PR #980: Adding combinators + a canonical renaming in List, Option, Name

2 files changed, 15 insertions, 6 deletions

diff --git a/library/nameops.ml b/library/nameops.ml
index adfe6f5a5..d598a63b8 100644
--- a/library/nameops.ml
+++ b/library/nameops.ml
@@ -130,7 +130,8 @@ sig
   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 fold_left_map : ('a -> Id.t -> 'a * Id.t) -> 'a -> t -> 'a * t
+  val fold_right_map : (Id.t -> 'a -> Id.t * 'a) -> Name.t -> 'a -> Name.t * 'a
   val get_id : t -> Id.t
   val pick : t -> t -> t
   val cons : t -> Id.t list -> Id.t list
@@ -160,10 +161,14 @@ struct
     | Name id -> Name (f id)
     | Anonymous -> Anonymous
 
-  let fold_map f a = function
+  let fold_left_map f a = function
     | Name id -> let (a, id) = f a id in (a, Name id)
     | Anonymous -> a, Anonymous
 
+  let fold_right_map f na a = match na with
+    | Name id -> let (id, a) = f id a in (Name id, a)
+    | Anonymous -> Anonymous, a
+
   let get_id = function
     | Name id -> id
     | Anonymous -> raise IsAnonymous
@@ -191,7 +196,7 @@ 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_fold_map = fold_left_map
 let name_cons = cons
 let name_max = pick
 let pr_name = print
diff --git a/library/nameops.mli b/library/nameops.mli
index 89aba2447..58cd6ed4e 100644
--- a/library/nameops.mli
+++ b/library/nameops.mli
@@ -66,10 +66,14 @@ module Name : sig
   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')].
+  val fold_left_map : ('a -> Id.t -> 'a * Id.t) -> 'a -> Name.t -> 'a * Name.t
+  (** [fold_left_map f a na] is [a',Name id'] when [na] is [Name id] and [f a id] is [(a',id')].
       It is [a,Anonymous] otherwise. *)
 
+  val fold_right_map : (Id.t -> 'a -> Id.t * 'a) -> Name.t -> 'a -> Name.t * 'a
+  (** [fold_right_map f na a] is [Name id',a'] when [na] is [Name id] and [f id a] is [(id',a')].
+      It is [Anonymous,a] otherwise. *)
+
   val get_id : Name.t -> Id.t
   (** [get_id] associates [id] to [Name id]. @raise IsAnonymous otherwise. *)
 
@@ -98,7 +102,7 @@ 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] *)
+(** @deprecated Same as [Name.fold_left_map] *)
 
 val name_max : Name.t -> Name.t -> Name.t
 (** @deprecated Same as [Name.pick] *)