--- a/src/Pure/library.ML Thu Jul 14 19:28:23 2005 +0200
+++ b/src/Pure/library.ML Thu Jul 14 19:28:24 2005 +0200
@@ -8,19 +8,20 @@
tables, balanced trees, orders, current directory, misc.
*)
-infix |> |-> ||> ||>> |>> |>>> #> #-> ~~ \ \\ ins ins_string ins_int orf andf prefix upto downto
- mem mem_int mem_string union union_int union_string inter inter_int
- inter_string subset subset_int subset_string;
+infix |> |-> ||> ||>> |>> |>>> #> #-> ~~ \ \\ ins ins_string ins_int
+ orf andf prefix upto downto mem mem_int mem_string union union_int
+ union_string inter inter_int inter_string subset subset_int
+ subset_string;
infix 3 oo ooo oooo;
signature BASIC_LIBRARY =
sig
(*functions*)
+ val I: 'a -> 'a
+ val K: 'a -> 'b -> 'a
val curry: ('a * 'b -> 'c) -> 'a -> 'b -> 'c
val uncurry: ('a -> 'b -> 'c) -> 'a * 'b -> 'c
- val I: 'a -> 'a
- val K: 'a -> 'b -> 'a
val |> : 'a * ('a -> 'b) -> 'b
val |-> : ('c * 'a) * ('c -> 'a -> 'b) -> 'b
val ||> : ('c * 'a) * ('a -> 'b) -> 'c * 'b
@@ -33,9 +34,9 @@
val oo: ('a -> 'b) * ('c -> 'd -> 'a) -> 'c -> 'd -> 'b
val ooo: ('a -> 'b) * ('c -> 'd -> 'e -> 'a) -> 'c -> 'd -> 'e -> 'b
val oooo: ('a -> 'b) * ('c -> 'd -> 'e -> 'f -> 'a) -> 'c -> 'd -> 'e -> 'f -> 'b
+ val funpow: int -> ('a -> 'a) -> 'a -> 'a
val apl: 'a * ('a * 'b -> 'c) -> 'b -> 'c
val apr: ('a * 'b -> 'c) * 'b -> 'a -> 'c
- val funpow: int -> ('a -> 'a) -> 'a -> 'a
(*old options -- invalidated*)
datatype invalid = None of invalid
@@ -295,11 +296,10 @@
(** functions **)
-(*handy combinators*)
+fun I x = x;
+fun K x = fn _ => x;
fun curry f x y = f (x, y);
fun uncurry f (x, y) = f x y;
-fun I x = x;
-fun K x = fn _ => x;
(*reverse application and structured results*)
fun x |> f = f x;
@@ -308,25 +308,28 @@
fun (x, y) ||> f = (x, f y);
fun (x, y) |>>> f = let val (x', z) = f x in (x', (y, z)) end;
fun (x, y) ||>> f = let val (z, y') = f y in ((x, z), y') end;
+
+(*reverse composition*)
fun f #> g = g o f;
-fun f #-> g = fn s => let val (v, s') = f s in g v s' end;
-fun ` h = fn s => (h s, s)
+fun f #-> g = uncurry g o f;
+
+(*view results*)
+fun `f = fn x => (f x, x);
(*composition with multiple args*)
fun (f oo g) x y = f (g x y);
fun (f ooo g) x y z = f (g x y z);
fun (f oooo g) x y z w = f (g x y z w);
-(*application of (infix) operator to its left or right argument*)
-fun apl (x, f) y = f (x, y);
-fun apr (f, y) x = f (x, y);
-
(*function exponentiation: f(...(f x)...) with n applications of f*)
fun funpow n f x =
let fun rep (0, x) = x
| rep (n, x) = rep (n - 1, f x)
in rep (n, x) end;
+(*application of (infix) operator to its left or right argument*)
+fun apl (x, f) y = f (x, y);
+fun apr (f, y) x = f (x, y);
(** options **)
@@ -1268,12 +1271,13 @@
Preserves order of elements in both lists.*)
val partition = List.partition;
-
fun partition_eq (eq:'a * 'a -> bool) =
- let fun part [] = []
- | part (x::ys) = let val (xs, xs') = partition (apl(x, eq)) ys
- in (x::xs)::(part xs') end
- in part end;
+ let
+ fun part [] = []
+ | part (x :: ys) =
+ let val (xs, xs') = partition (fn y => eq (x, y)) ys
+ in (x::xs)::(part xs') end
+ in part end;
(*Partition a list into buckets [ bi, b(i+1), ..., bj ]