added map_split
authorhaftmann
Tue Jan 22 23:07:24 2008 +0100 (2008-01-22)
changeset 25943d431d65346a1
parent 25942 a52309ac4a4d
child 25944 f0301d6c7b79
added map_split
src/Pure/library.ML
     1.1 --- a/src/Pure/library.ML	Tue Jan 22 23:07:21 2008 +0100
     1.2 +++ b/src/Pure/library.ML	Tue Jan 22 23:07:24 2008 +0100
     1.3 @@ -107,6 +107,7 @@
     1.4    val fold2: ('a -> 'b -> 'c -> 'c) -> 'a list -> 'b list -> 'c -> 'c
     1.5    val zip_options: 'a list -> 'b option list -> ('a * 'b) list
     1.6    val ~~ : 'a list * 'b list -> ('a * 'b) list
     1.7 +  val map_split: ('a -> 'b * 'c) -> 'a list -> 'b list * 'c list
     1.8    val split_list: ('a * 'b) list -> 'a list * 'b list
     1.9    val separate: 'a -> 'a list -> 'a list
    1.10    val replicate: int -> 'a -> 'a list
    1.11 @@ -573,6 +574,13 @@
    1.12    | fold2 f (x :: xs) (y :: ys) z = fold2 f xs ys (f x y z)
    1.13    | fold2 f _ _ _ = raise UnequalLengths;
    1.14  
    1.15 +fun map_split f [] = ([], [])
    1.16 +  | map_split f (x :: xs) =
    1.17 +      let
    1.18 +        val (y, w) = f x;
    1.19 +        val (ys, ws) = map_split f xs;
    1.20 +      in (y :: ys, w :: ws) end;
    1.21 +
    1.22  fun zip_options (x :: xs) (SOME y :: ys) = (x, y) :: zip_options xs ys
    1.23    | zip_options (_ :: xs) (NONE :: ys) = zip_options xs ys
    1.24    | zip_options _ [] = []