1.1 --- a/src/Pure/library.ML	Thu Jul 14 19:28:23 2005 +0200
     1.2 +++ b/src/Pure/library.ML	Thu Jul 14 19:28:24 2005 +0200
     1.3 @@ -8,19 +8,20 @@
     1.4  tables, balanced trees, orders, current directory, misc.
     1.5  *)
     1.6  
     1.7 -infix |> |-> ||> ||>> |>> |>>> #> #-> ~~ \ \\ ins ins_string ins_int orf andf prefix upto downto
     1.8 -  mem mem_int mem_string union union_int union_string inter inter_int
     1.9 -  inter_string subset subset_int subset_string;
    1.10 +infix |> |-> ||> ||>> |>> |>>> #> #-> ~~ \ \\ ins ins_string ins_int
    1.11 +  orf andf prefix upto downto mem mem_int mem_string union union_int
    1.12 +  union_string inter inter_int inter_string subset subset_int
    1.13 +  subset_string;
    1.14  
    1.15  infix 3 oo ooo oooo;
    1.16  
    1.17  signature BASIC_LIBRARY =
    1.18  sig
    1.19    (*functions*)
    1.20 +  val I: 'a -> 'a
    1.21 +  val K: 'a -> 'b -> 'a
    1.22    val curry: ('a * 'b -> 'c) -> 'a -> 'b -> 'c
    1.23    val uncurry: ('a -> 'b -> 'c) -> 'a * 'b -> 'c
    1.24 -  val I: 'a -> 'a
    1.25 -  val K: 'a -> 'b -> 'a
    1.26    val |> : 'a * ('a -> 'b) -> 'b
    1.27    val |-> : ('c * 'a) * ('c -> 'a -> 'b) -> 'b
    1.28    val ||> : ('c * 'a) * ('a -> 'b) -> 'c * 'b
    1.29 @@ -33,9 +34,9 @@
    1.30    val oo: ('a -> 'b) * ('c -> 'd -> 'a) -> 'c -> 'd -> 'b
    1.31    val ooo: ('a -> 'b) * ('c -> 'd -> 'e -> 'a) -> 'c -> 'd -> 'e -> 'b
    1.32    val oooo: ('a -> 'b) * ('c -> 'd -> 'e -> 'f -> 'a) -> 'c -> 'd -> 'e -> 'f -> 'b
    1.33 +  val funpow: int -> ('a -> 'a) -> 'a -> 'a
    1.34    val apl: 'a * ('a * 'b -> 'c) -> 'b -> 'c
    1.35    val apr: ('a * 'b -> 'c) * 'b -> 'a -> 'c
    1.36 -  val funpow: int -> ('a -> 'a) -> 'a -> 'a
    1.37  
    1.38    (*old options -- invalidated*)
    1.39    datatype invalid = None of invalid
    1.40 @@ -295,11 +296,10 @@
    1.41  
    1.42  (** functions **)
    1.43  
    1.44 -(*handy combinators*)
    1.45 +fun I x = x;
    1.46 +fun K x = fn _ => x;
    1.47  fun curry f x y = f (x, y);
    1.48  fun uncurry f (x, y) = f x y;
    1.49 -fun I x = x;
    1.50 -fun K x = fn _ => x;
    1.51  
    1.52  (*reverse application and structured results*)
    1.53  fun x |> f = f x;
    1.54 @@ -308,25 +308,28 @@
    1.55  fun (x, y) ||> f = (x, f y);
    1.56  fun (x, y) |>>> f = let val (x', z) = f x in (x', (y, z)) end;
    1.57  fun (x, y) ||>> f = let val (z, y') = f y in ((x, z), y') end;
    1.58 +
    1.59 +(*reverse composition*)
    1.60  fun f #> g = g o f;
    1.61 -fun f #-> g = fn s => let val (v, s') = f s in g v s' end;
    1.62 -fun ` h = fn s => (h s, s)
    1.63 +fun f #-> g = uncurry g o f;
    1.64 +
    1.65 +(*view results*)
    1.66 +fun `f = fn x => (f x, x);
    1.67  
    1.68  (*composition with multiple args*)
    1.69  fun (f oo g) x y = f (g x y);
    1.70  fun (f ooo g) x y z = f (g x y z);
    1.71  fun (f oooo g) x y z w = f (g x y z w);
    1.72  
    1.73 -(*application of (infix) operator to its left or right argument*)
    1.74 -fun apl (x, f) y = f (x, y);
    1.75 -fun apr (f, y) x = f (x, y);
    1.76 -
    1.77  (*function exponentiation: f(...(f x)...) with n applications of f*)
    1.78  fun funpow n f x =
    1.79    let fun rep (0, x) = x
    1.80          | rep (n, x) = rep (n - 1, f x)
    1.81    in rep (n, x) end;
    1.82  
    1.83 +(*application of (infix) operator to its left or right argument*)
    1.84 +fun apl (x, f) y = f (x, y);
    1.85 +fun apr (f, y) x = f (x, y);
    1.86  
    1.87  
    1.88  (** options **)
    1.89 @@ -1268,12 +1271,13 @@
    1.90    Preserves order of elements in both lists.*)
    1.91  val partition = List.partition;
    1.92  
    1.93 -
    1.94  fun partition_eq (eq:'a * 'a -> bool) =
    1.95 -    let fun part [] = []
    1.96 -          | part (x::ys) = let val (xs, xs') = partition (apl(x, eq)) ys
    1.97 -                           in (x::xs)::(part xs') end
    1.98 -    in part end;
    1.99 +  let
   1.100 +    fun part [] = []
   1.101 +      | part (x :: ys) =
   1.102 +          let val (xs, xs') = partition (fn y => eq (x, y)) ys
   1.103 +          in (x::xs)::(part xs') end
   1.104 +  in part end;
   1.105  
   1.106  
   1.107  (*Partition a list into buckets  [ bi, b(i+1), ..., bj ]