src/Pure/library.ML
changeset 18330 444f16d232a2
parent 18286 7273cf5085ed
child 18333 b356f7837921
     1.1 --- a/src/Pure/library.ML	Thu Dec 01 22:43:15 2005 +0100
     1.2 +++ b/src/Pure/library.ML	Fri Dec 02 08:06:59 2005 +0100
     1.3 @@ -97,7 +97,6 @@
     1.4    val fold: ('a -> 'b -> 'b) -> 'a list -> 'b -> 'b
     1.5    val fold_rev: ('a -> 'b -> 'b) -> 'a list -> 'b -> 'b
     1.6    val fold_map: ('a -> 'b -> 'c * 'b) -> 'a list -> 'b -> 'c list * 'b
     1.7 -  val fold2: ('a -> 'b -> 'c -> 'c) -> 'a list -> 'b list -> 'c -> 'c
     1.8    val fold_index: (int * 'a -> 'b -> 'b) -> 'a list -> 'b -> 'b
     1.9    val foldr1: ('a * 'a -> 'a) -> 'a list -> 'a
    1.10    val foldl_map: ('a * 'b -> 'a * 'c) -> 'a * 'b list -> 'a * 'c list
    1.11 @@ -113,18 +112,16 @@
    1.12    val find_index_eq: ''a -> ''a list -> int
    1.13    val find_first: ('a -> bool) -> 'a list -> 'a option
    1.14    val get_first: ('a -> 'b option) -> 'a list -> 'b option
    1.15 +  val map2: ('a -> 'b -> 'c) -> 'a list -> 'b list -> 'c list
    1.16 +  val fold2: ('a -> 'b -> 'c -> 'c) -> 'a list -> 'b list -> 'c -> 'c
    1.17 +  val ~~ : 'a list * 'b list -> ('a * 'b) list
    1.18 +  val split_list: ('a * 'b) list -> 'a list * 'b list
    1.19    val separate: 'a -> 'a list -> 'a list
    1.20    val replicate: int -> 'a -> 'a list
    1.21    val multiply: 'a list -> 'a list list -> 'a list list
    1.22    val product: 'a list -> 'b list -> ('a * 'b) list
    1.23    val filter: ('a -> bool) -> 'a list -> 'a list
    1.24    val filter_out: ('a -> bool) -> 'a list -> 'a list
    1.25 -  val map2: ('a * 'b -> 'c) -> 'a list * 'b list -> 'c list
    1.26 -  val exists2: ('a * 'b -> bool) -> 'a list * 'b list -> bool
    1.27 -  val forall2: ('a * 'b -> bool) -> 'a list * 'b list -> bool
    1.28 -  val seq2: ('a * 'b -> unit) -> 'a list * 'b list -> unit
    1.29 -  val ~~ : 'a list * 'b list -> ('a * 'b) list
    1.30 -  val split_list: ('a * 'b) list -> 'a list * 'b list
    1.31    val equal_lists: ('a * 'b -> bool) -> 'a list * 'b list -> bool
    1.32    val prefix: ''a list * ''a list -> bool
    1.33    val take_prefix: ('a -> bool) -> 'a list -> 'a list * 'a list
    1.34 @@ -467,13 +464,6 @@
    1.35        | fold_aux (x :: xs) y = fold_aux xs (f x y);
    1.36    in fold_aux end;
    1.37  
    1.38 -fun fold2 f =
    1.39 -  let
    1.40 -    fun fold_aux [] [] z = z
    1.41 -      | fold_aux (x :: xs) (y :: ys) z = fold_aux xs ys (f x y z)
    1.42 -      | fold_aux _ _ _ = raise UnequalLengths;
    1.43 -  in fold_aux end;
    1.44 -
    1.45  fun fold_rev f =
    1.46    let
    1.47      fun fold_aux [] y = y
    1.48 @@ -643,21 +633,17 @@
    1.49  
    1.50  exception UnequalLengths;
    1.51  
    1.52 -fun map2 _ ([], []) = []
    1.53 -  | map2 f (x :: xs, y :: ys) = f (x, y) :: map2 f (xs, ys)
    1.54 -  | map2 _ _ = raise UnequalLengths;
    1.55 -
    1.56 -fun exists2 _ ([], []) = false
    1.57 -  | exists2 pred (x :: xs, y :: ys) = pred (x, y) orelse exists2 pred (xs, ys)
    1.58 -  | exists2 _ _ = raise UnequalLengths;
    1.59 +fun map2 _ [] [] = []
    1.60 +  | map2 f (x :: xs) (y :: ys) = f x y :: map2 f xs ys
    1.61 +  | map2 _ _ _ = raise UnequalLengths;
    1.62  
    1.63 -fun forall2 _ ([], []) = true
    1.64 -  | forall2 pred (x :: xs, y :: ys) = pred (x, y) andalso forall2 pred (xs, ys)
    1.65 -  | forall2 _ _ = raise UnequalLengths;
    1.66 +fun fold2 f =
    1.67 +  let
    1.68 +    fun fold_aux [] [] z = z
    1.69 +      | fold_aux (x :: xs) (y :: ys) z = fold_aux xs ys (f x y z)
    1.70 +      | fold_aux _ _ _ = raise UnequalLengths;
    1.71 +  in fold_aux end;
    1.72  
    1.73 -fun seq2 _ ([], []) = ()
    1.74 -  | seq2 f (x :: xs, y :: ys) = (f (x, y); seq2 f (xs, ys))
    1.75 -  | seq2 _ _ = raise UnequalLengths;
    1.76  
    1.77  (*combine two lists forming a list of pairs:
    1.78    [x1, ..., xn] ~~ [y1, ..., yn]  ===>  [(x1, y1), ..., (xn, yn)]*)
    1.79 @@ -669,7 +655,11 @@
    1.80    [(x1, y1), ..., (xn, yn)]  ===>  ([x1, ..., xn], [y1, ..., yn])*)
    1.81  val split_list = ListPair.unzip;
    1.82  
    1.83 -fun equal_lists eq (xs, ys) = length xs = length ys andalso forall2 eq (xs, ys);
    1.84 +fun equal_lists eq (xs, ys) =
    1.85 +  let
    1.86 +    fun eq' [] [] = true
    1.87 +      | eq' (x :: xs) (y :: ys) = eq (x, y) andalso eq' xs ys
    1.88 +  in length xs = length ys andalso eq' xs ys end;
    1.89  
    1.90  
    1.91  (* prefixes, suffixes *)