src/Pure/library.ML
changeset 19799 666de5708ae8
parent 19691 dd9ccb370f52
child 19973 07cf246f76a3
equal deleted inserted replaced
19798:94f12468bbba 19799:666de5708ae8
   130   val get_index: ('a -> 'b option) -> 'a list -> (int * 'b) option
   130   val get_index: ('a -> 'b option) -> 'a list -> (int * 'b) option
   131   val get_first: ('a -> 'b option) -> 'a list -> 'b option
   131   val get_first: ('a -> 'b option) -> 'a list -> 'b option
   132   val eq_list: ('a * 'b -> bool) -> 'a list * 'b list -> bool
   132   val eq_list: ('a * 'b -> bool) -> 'a list * 'b list -> bool
   133   val map2: ('a -> 'b -> 'c) -> 'a list -> 'b list -> 'c list
   133   val map2: ('a -> 'b -> 'c) -> 'a list -> 'b list -> 'c list
   134   val fold2: ('a -> 'b -> 'c -> 'c) -> 'a list -> 'b list -> 'c -> 'c
   134   val fold2: ('a -> 'b -> 'c -> 'c) -> 'a list -> 'b list -> 'c -> 'c
       
   135   val zip_options: 'a list -> 'b option list -> ('a * 'b) list
   135   val ~~ : 'a list * 'b list -> ('a * 'b) list
   136   val ~~ : 'a list * 'b list -> ('a * 'b) list
   136   val split_list: ('a * 'b) list -> 'a list * 'b list
   137   val split_list: ('a * 'b) list -> 'a list * 'b list
   137   val separate: 'a -> 'a list -> 'a list
   138   val separate: 'a -> 'a list -> 'a list
   138   val replicate: int -> 'a -> 'a list
   139   val replicate: int -> 'a -> 'a list
   139   val multiply: 'a list -> 'a list list -> 'a list list
   140   val multiply: 'a list -> 'a list list -> 'a list list
   712     fun fold_aux [] [] z = z
   713     fun fold_aux [] [] z = z
   713       | fold_aux (x :: xs) (y :: ys) z = fold_aux xs ys (f x y z)
   714       | fold_aux (x :: xs) (y :: ys) z = fold_aux xs ys (f x y z)
   714       | fold_aux _ _ _ = raise UnequalLengths;
   715       | fold_aux _ _ _ = raise UnequalLengths;
   715   in fold_aux end;
   716   in fold_aux end;
   716 
   717 
       
   718 fun zip_options (x :: xs) (SOME y :: ys) = (x, y) :: zip_options xs ys
       
   719   | zip_options (_ :: xs) (NONE :: ys) = zip_options xs ys
       
   720   | zip_options _ [] = []
       
   721   | zip_options [] _ = raise UnequalLengths;
   717 
   722 
   718 (*combine two lists forming a list of pairs:
   723 (*combine two lists forming a list of pairs:
   719   [x1, ..., xn] ~~ [y1, ..., yn]  ===>  [(x1, y1), ..., (xn, yn)]*)
   724   [x1, ..., xn] ~~ [y1, ..., yn]  ===>  [(x1, y1), ..., (xn, yn)]*)
   720 fun [] ~~ [] = []
   725 fun [] ~~ [] = []
   721   | (x :: xs) ~~ (y :: ys) = (x, y) :: (xs ~~ ys)
   726   | (x :: xs) ~~ (y :: ys) = (x, y) :: (xs ~~ ys)