aboutsummaryrefslogtreecommitdiffhomepage
path: root/library
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2017-08-31 15:48:30 +0200
committerGravatar Maxime Dénès <mail@maximedenes.fr>2017-08-31 15:48:30 +0200
commit5639933c1b8ad7cf96ec592eb3104aa8282f16f5 (patch)
tree36e68ca1d3dfe664469edd8f1ecb1f46396312e0 /library
parent13fb8de9aff07e4346ca4bdc866507503e9be12e (diff)
parent6b4d8df891ff964fb267eec54337a96ccc610ef3 (diff)
Merge PR #980: Adding combinators + a canonical renaming in List, Option, Name
Diffstat (limited to 'library')
-rw-r--r--library/nameops.ml11
-rw-r--r--library/nameops.mli10
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] *)