added map_filter;
authorwenzelm
Thu Apr 27 15:06:40 2006 +0200 (2006-04-27)
changeset 1948489484a62184a
parent 19483 55ee839198bd
child 19485 5385c9d86c2a
added map_filter;
src/Pure/General/seq.ML
     1.1 --- a/src/Pure/General/seq.ML	Thu Apr 27 15:06:39 2006 +0200
     1.2 +++ b/src/Pure/General/seq.ML	Thu Apr 27 15:06:40 2006 +0200
     1.3 @@ -29,6 +29,7 @@
     1.4    val flat: 'a seq seq -> 'a seq
     1.5    val map: ('a -> 'b) -> 'a seq -> 'b seq
     1.6    val maps: ('a -> 'b seq) -> 'a seq -> 'b seq
     1.7 +  val map_filter: ('a -> 'b option) -> 'a seq -> 'b seq
     1.8    val lift: ('a -> 'b -> 'c) -> 'a seq -> 'b -> 'c seq
     1.9    val lifts: ('a -> 'b -> 'c seq) -> 'a seq -> 'b -> 'c seq
    1.10    val print: (int -> 'a -> unit) -> int -> 'a seq -> unit
    1.11 @@ -156,6 +157,7 @@
    1.12      | SOME (x, xq') => SOME (f x, map f xq')));
    1.13  
    1.14  fun maps f = flat o map f;
    1.15 +fun map_filter f = maps (fn x => (case f x of NONE => empty | SOME y => single y));
    1.16  
    1.17  fun lift f xq y = map (fn x => f x y) xq;
    1.18  fun lifts f xq y = maps (fn x => f x y) xq;