src/Pure/library.ML
changeset 16721 e2427ea379a9
parent 16705 33f38450cab6
child 16780 aa284c1b72ad
     1.1 --- a/src/Pure/library.ML	Wed Jul 06 20:00:25 2005 +0200
     1.2 +++ b/src/Pure/library.ML	Wed Jul 06 20:00:27 2005 +0200
     1.3 @@ -27,12 +27,12 @@
     1.4    val ||> : ('c * 'a) * ('a -> 'b) -> 'c * 'b
     1.5    val |>>> : ('a * 'c) * ('a -> 'b * 'd) -> 'b * ('c * 'd)
     1.6    val ||>> : ('c * 'a) * ('a -> 'd * 'b) -> ('c * 'd) * 'b
     1.7 +  val oo: ('a -> 'b) * ('c -> 'd -> 'a) -> 'c -> 'd -> 'b
     1.8 +  val ooo: ('a -> 'b) * ('c -> 'd -> 'e -> 'a) -> 'c -> 'd -> 'e -> 'b
     1.9 +  val oooo: ('a -> 'b) * ('c -> 'd -> 'e -> 'f -> 'a) -> 'c -> 'd -> 'e -> 'f -> 'b
    1.10    val apl: 'a * ('a * 'b -> 'c) -> 'b -> 'c
    1.11    val apr: ('a * 'b -> 'c) * 'b -> 'a -> 'c
    1.12    val funpow: int -> ('a -> 'a) -> 'a -> 'a
    1.13 -  val oo: ('a -> 'b) * ('c -> 'd -> 'a) -> 'c -> 'd -> 'b
    1.14 -  val ooo: ('a -> 'b) * ('c -> 'd -> 'e -> 'a) -> 'c -> 'd -> 'e -> 'b
    1.15 -  val oooo: ('a -> 'b) * ('c -> 'd -> 'e -> 'f -> 'a) -> 'c -> 'd -> 'e -> 'f -> 'b
    1.16  
    1.17    (*old options -- invalidated*)
    1.18    datatype invalid = None of invalid
    1.19 @@ -296,7 +296,7 @@
    1.20  fun curry f x y = f (x, y);
    1.21  fun uncurry f (x, y) = f x y;
    1.22  fun I x = x;
    1.23 -fun K x = fn y => x;
    1.24 +fun K x = fn _ => x;
    1.25  
    1.26  (*reverse application and structured results*)
    1.27  fun x |> f = f x;
    1.28 @@ -306,6 +306,11 @@
    1.29  fun (x, y) |>>> f = let val (x', z) = f x in (x', (y, z)) end;
    1.30  fun (x, y) ||>> f = let val (z, y') = f y in ((x, z), y') end;
    1.31  
    1.32 +(*composition with multiple args*)
    1.33 +fun (f oo g) x y = f (g x y);
    1.34 +fun (f ooo g) x y z = f (g x y z);
    1.35 +fun (f oooo g) x y z w = f (g x y z w);
    1.36 +
    1.37  (*application of (infix) operator to its left or right argument*)
    1.38  fun apl (x, f) y = f (x, y);
    1.39  fun apr (f, y) x = f (x, y);
    1.40 @@ -316,11 +321,6 @@
    1.41          | rep (n, x) = rep (n - 1, f x)
    1.42    in rep (n, x) end;
    1.43  
    1.44 -(*concatenation: 2 and 3 args*)
    1.45 -fun (f oo g) x y = f (g x y);
    1.46 -fun (f ooo g) x y z = f (g x y z);
    1.47 -fun (f oooo g) x y z w = f (g x y z w);
    1.48 -
    1.49  
    1.50  
    1.51  (** options **)
    1.52 @@ -399,8 +399,8 @@
    1.53  
    1.54  (* operators for combining predicates *)
    1.55  
    1.56 -fun (p orf q) = fn x => p x orelse q x;
    1.57 -fun (p andf q) = fn x => p x andalso q x;
    1.58 +fun p orf q = fn x => p x orelse q x;
    1.59 +fun p andf q = fn x => p x andalso q x;
    1.60  
    1.61  
    1.62  (* predicates on lists *)
    1.63 @@ -470,7 +470,7 @@
    1.64        | fold_aux (x :: xs) y = f x (fold_aux xs y);
    1.65    in fold_aux end;
    1.66  
    1.67 -fun fold_map f = 
    1.68 +fun fold_map f =
    1.69    let
    1.70      fun fold_aux [] y = ([], y)
    1.71        | fold_aux (x :: xs) y =