Merge PR #12499: Clean future goals

Ack-by: SkySkimmer
Ack-by: ejgallego
Reviewed-by: mattam82
Reviewed-by: ppedrot

2 files changed, 5 insertions, 0 deletions

diff --git a/clib/option.ml b/clib/option.ml
index c335e836c2..d1775ae3ae 100644
--- a/clib/option.ml
+++ b/clib/option.ml
@@ -55,6 +55,8 @@ let make x = Some x
 (** [bind x f] is [f y] if [x] is [Some y] and [None] otherwise *)
 let bind x f = match x with Some y -> f y | None -> None
 
+let filter f x = bind x (fun v -> if f v then x else None)
+
 (** [init b x] returns [Some x] if [b] is [true] and [None] otherwise. *)
 let init b x =
   if b then
diff --git a/clib/option.mli b/clib/option.mli
index 4c5df30179..4672780cab 100644
--- a/clib/option.mli
+++ b/clib/option.mli
@@ -46,6 +46,9 @@ val make : 'a -> 'a option
 (** [bind x f] is [f y] if [x] is [Some y] and [None] otherwise *)
 val bind : 'a option -> ('a -> 'b option) -> 'b option
 
+(** [filter f x] is [x] if [x] [Some y] and [f y] is true, [None] otherwise *)
+val filter : ('a -> bool) -> 'a option -> 'a option
+
 (** [init b x] returns [Some x] if [b] is [true] and [None] otherwise. *)
 val init : bool -> 'a -> 'a option