src/Pure/library.ML
changeset 25538 58e8ba3b792b
parent 25224 6d4d26e878f4
child 25549 7040555f20c7
     1.1 --- a/src/Pure/library.ML	Wed Dec 05 14:15:59 2007 +0100
     1.2 +++ b/src/Pure/library.ML	Wed Dec 05 14:16:05 2007 +0100
     1.3 @@ -100,13 +100,14 @@
     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 map_product: ('a -> 'b -> 'c) -> 'a list -> 'b list -> 'c list
     1.8 +  val fold_product: ('a -> 'b -> 'c -> 'c) -> 'a list -> 'b list -> 'c -> 'c
     1.9    val zip_options: 'a list -> 'b option list -> ('a * 'b) list
    1.10    val ~~ : 'a list * 'b list -> ('a * 'b) list
    1.11    val split_list: ('a * 'b) list -> 'a list * 'b list
    1.12    val separate: 'a -> 'a list -> 'a list
    1.13    val replicate: int -> 'a -> 'a list
    1.14    val multiply: 'a list -> 'a list list -> 'a list list
    1.15 -  val product: 'a list -> 'b list -> ('a * 'b) list
    1.16    val filter: ('a -> bool) -> 'a list -> 'a list
    1.17    val filter_out: ('a -> bool) -> 'a list -> 'a list
    1.18    val map_filter: ('a -> 'b option) -> 'a list -> 'b list
    1.19 @@ -429,6 +430,11 @@
    1.20  fun maps f [] = []
    1.21    | maps f (x :: xs) = f x @ maps f xs;
    1.22  
    1.23 +(*copy the list preserving elements that satisfy the predicate*)
    1.24 +val filter = List.filter;
    1.25 +fun filter_out f = filter (not o f);
    1.26 +val map_filter = List.mapPartial;
    1.27 +
    1.28  fun chop (0: int) xs = ([], xs)
    1.29    | chop _ [] = ([], [])
    1.30    | chop n (x :: xs) = chop (n - 1) xs |>> cons x;
    1.31 @@ -540,20 +546,15 @@
    1.32    | multiply (x :: xs) yss = map (cons x) yss @ multiply xs yss;
    1.33  
    1.34  (*direct product*)
    1.35 -fun product _ [] = []
    1.36 -  | product [] _ = []
    1.37 -  | product (x :: xs) ys = map (pair x) ys @ product xs ys;
    1.38 -
    1.39 -
    1.40 -(* filter *)
    1.41 +fun map_product f _ [] = []
    1.42 +  | map_product f [] _ = []
    1.43 +  | map_product f (x :: xs) ys = map (f x) ys @ map_product f xs ys;
    1.44  
    1.45 -(*copy the list preserving elements that satisfy the predicate*)
    1.46 -val filter = List.filter;
    1.47 -fun filter_out f = filter (not o f);
    1.48 -val map_filter = List.mapPartial;
    1.49 +fun fold_product f _ [] z = z
    1.50 +  | fold_product f [] _ z = z
    1.51 +  | fold_product f (x :: xs) ys z = z |> fold (f x) ys |> fold_product f xs ys;
    1.52  
    1.53 -
    1.54 -(* lists of pairs *)
    1.55 +(*lists of pairs*)
    1.56  
    1.57  exception UnequalLengths;
    1.58