added zip_options;
authorwenzelm
Tue Jun 06 20:42:30 2006 +0200 (2006-06-06)
changeset 19799666de5708ae8
parent 19798 94f12468bbba
child 19800 5f764272183e
added zip_options;
src/Pure/library.ML
     1.1 --- a/src/Pure/library.ML	Tue Jun 06 20:42:28 2006 +0200
     1.2 +++ b/src/Pure/library.ML	Tue Jun 06 20:42:30 2006 +0200
     1.3 @@ -132,6 +132,7 @@
     1.4    val eq_list: ('a * 'b -> bool) -> 'a list * 'b list -> bool
     1.5    val map2: ('a -> 'b -> 'c) -> 'a list -> 'b list -> 'c list
     1.6    val fold2: ('a -> 'b -> 'c -> 'c) -> 'a list -> 'b list -> 'c -> 'c
     1.7 +  val zip_options: 'a list -> 'b option list -> ('a * 'b) list
     1.8    val ~~ : 'a list * 'b list -> ('a * 'b) list
     1.9    val split_list: ('a * 'b) list -> 'a list * 'b list
    1.10    val separate: 'a -> 'a list -> 'a list
    1.11 @@ -714,6 +715,10 @@
    1.12        | fold_aux _ _ _ = raise UnequalLengths;
    1.13    in fold_aux end;
    1.14  
    1.15 +fun zip_options (x :: xs) (SOME y :: ys) = (x, y) :: zip_options xs ys
    1.16 +  | zip_options (_ :: xs) (NONE :: ys) = zip_options xs ys
    1.17 +  | zip_options _ [] = []
    1.18 +  | zip_options [] _ = raise UnequalLengths;
    1.19  
    1.20  (*combine two lists forming a list of pairs:
    1.21    [x1, ..., xn] ~~ [y1, ..., yn]  ===>  [(x1, y1), ..., (xn, yn)]*)