renamed mapfilter to map_filter, made pervasive (again);
authorwenzelm
Thu Apr 27 15:06:39 2006 +0200 (2006-04-27)
changeset 1948355ee839198bd
parent 19482 9f11af8f7ef9
child 19484 89484a62184a
renamed mapfilter to map_filter, made pervasive (again);
made flat pervasive (again);
added maps;
src/Pure/library.ML
     1.1 --- a/src/Pure/library.ML	Thu Apr 27 15:06:35 2006 +0200
     1.2 +++ b/src/Pure/library.ML	Thu Apr 27 15:06:39 2006 +0200
     1.3 @@ -144,6 +144,7 @@
     1.4    val product: 'a list -> 'b list -> ('a * 'b) list
     1.5    val filter: ('a -> bool) -> 'a list -> 'a list
     1.6    val filter_out: ('a -> bool) -> 'a list -> 'a list
     1.7 +  val map_filter: ('a -> 'b option) -> 'a list -> 'b list
     1.8    val equal_lists: ('a * 'b -> bool) -> 'a list * 'b list -> bool
     1.9    val is_prefix: ('a * 'a -> bool) -> 'a list -> 'a list -> bool
    1.10    val take_prefix: ('a -> bool) -> 'a list -> 'a list * 'a list
    1.11 @@ -289,7 +290,6 @@
    1.12    val last_elem: 'a list -> 'a
    1.13    val seq: ('a -> unit) -> 'a list -> unit
    1.14    val partition: ('a -> bool) -> 'a list -> 'a list * 'a list
    1.15 -  val mapfilter: ('a -> 'b option) -> 'a list -> 'b list
    1.16  end;
    1.17  
    1.18  structure Library: LIBRARY =
    1.19 @@ -579,6 +579,9 @@
    1.20  
    1.21  (* basic list functions *)
    1.22  
    1.23 +fun maps f [] = []
    1.24 +  | maps f (x :: xs) = f x @ maps f xs;
    1.25 +
    1.26  fun chop 0 xs = ([], xs)
    1.27    | chop _ [] = ([], [])
    1.28    | chop n (x :: xs) = chop (n - 1) xs |>> cons x;
    1.29 @@ -660,8 +663,6 @@
    1.30  
    1.31  val flat = List.concat;
    1.32  
    1.33 -fun maps f = flat o map f;
    1.34 -
    1.35  fun unflat (xs :: xss) ys =
    1.36        let val (ps, qs) = chop (length xs) ys
    1.37        in ps :: unflat xss qs end
    1.38 @@ -708,7 +709,7 @@
    1.39  (*copy the list preserving elements that satisfy the predicate*)
    1.40  val filter = List.filter;
    1.41  fun filter_out f = filter (not o f);
    1.42 -val mapfilter = List.mapPartial;
    1.43 +val map_filter = List.mapPartial;
    1.44  
    1.45  
    1.46  (* lists of pairs *)