aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2016-10-12 17:43:51 +0200
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2016-10-12 17:44:34 +0200
commit112e974ec90b2afc51a7cffeba49e5777f3ea80f (patch)
tree1bf579fca94adea5ee4a423c0a96c8832e68861e /lib
parent8b2a08ecd123515778584596918666e5f49076f7 (diff)
parent6d55121c90ec50319a3de6a6907726fbcdc2f835 (diff)
Merge branch 'v8.5' into v8.6
Diffstat (limited to 'lib')
-rw-r--r--lib/monad.ml11
-rw-r--r--lib/monad.mli3
2 files changed, 14 insertions, 0 deletions
diff --git a/lib/monad.ml b/lib/monad.ml
index a1714a41b..2e55e9698 100644
--- a/lib/monad.ml
+++ b/lib/monad.ml
@@ -64,6 +64,9 @@ module type ListS = sig
its second argument in a tail position. *)
val iter : ('a -> unit t) -> 'a list -> unit t
+ (** Like the regular {!CList.map_filter}. The monadic effects are threaded left*)
+ val map_filter : ('a -> 'b option t) -> 'a list -> 'b list t
+
(** {6 Two-list iterators} *)
@@ -138,6 +141,14 @@ module Make (M:Def) : S with type +'a t = 'a M.t = struct
| a::b::l -> f a >> f b >> iter f l
+ let rec map_filter f = function
+ | [] -> return []
+ | a::l ->
+ f a >>= function
+ | None -> map_filter f l
+ | Some b ->
+ map_filter f l >>= fun filtered ->
+ return (b::filtered)
let rec fold_left2 r f x l1 l2 =
match l1,l2 with
diff --git a/lib/monad.mli b/lib/monad.mli
index c8655efa0..f7de71f53 100644
--- a/lib/monad.mli
+++ b/lib/monad.mli
@@ -66,6 +66,9 @@ module type ListS = sig
its second argument in a tail position. *)
val iter : ('a -> unit t) -> 'a list -> unit t
+ (** Like the regular {!CList.map_filter}. The monadic effects are threaded left*)
+ val map_filter : ('a -> 'b option t) -> 'a list -> 'b list t
+
(** {6 Two-list iterators} *)