From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Tue, 4 Oct 2005 09:35:39 +0000 (+0000)
Subject: added filter_map
X-Git-Tag: V_0_7_2_3~259
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=0f553c84d45f6f57977ae200291fd38882655ad3;p=helm.git

added filter_map
---

diff --git a/helm/ocaml/extlib/hExtlib.ml b/helm/ocaml/extlib/hExtlib.ml
index 06ac37b13..d3ae69402 100644
--- a/helm/ocaml/extlib/hExtlib.ml
+++ b/helm/ocaml/extlib/hExtlib.ml
@@ -96,6 +96,14 @@ let rec list_uniq = function
   | h1::h2::tl when h1 = h2 -> list_uniq (h2 :: tl) 
   | h1::tl (* when h1 <> h2 *) -> h1 :: list_uniq tl
 
+let rec filter_map f =
+  function
+  | [] -> []
+  | hd :: tl ->
+      (match f hd with
+      | None -> filter_map f tl
+      | Some v -> v :: filter_map f tl)
+
 (** {2 File predicates} *)
 
 let is_dir fname =
diff --git a/helm/ocaml/extlib/hExtlib.mli b/helm/ocaml/extlib/hExtlib.mli
index cd4cc276e..2565f7861 100644
--- a/helm/ocaml/extlib/hExtlib.mli
+++ b/helm/ocaml/extlib/hExtlib.mli
@@ -52,6 +52,7 @@ val trim_blanks: string -> string (** strip heading and trailing blanks *)
 (** {2 List processing} *)
 
 val list_uniq: 'a list -> 'a list (* uniq unix filter on lists *)
+val filter_map: ('a -> 'b option) -> 'a list -> 'b list (* filter + map *)
 
 (** {2 Debugging & Profiling} *)