# HG changeset patch
# User wenzelm
# Date 1147777287 -7200
# Node ID 0b01436e184305d65caed5c76973349b89f0832c
# Parent  213e12ad2c0328e88ba814354b7fded82c3e7ccd
added divide_and_conquer combinator (by Amine Chaieb);
removed remains of old option type;
removed obsolete eq_opt;
removed obsolete string_of_bool (use Bool.toString instead);
tuned;

diff -r 213e12ad2c03 -r 0b01436e1843 src/Pure/library.ML
--- a/src/Pure/library.ML	Tue May 16 13:01:26 2006 +0200
+++ b/src/Pure/library.ML	Tue May 16 13:01:27 2006 +0200
@@ -38,10 +38,6 @@
   val oooo: ('a -> 'b) * ('c -> 'd -> 'e -> 'f -> 'a) -> 'c -> 'd -> 'e -> 'f -> 'b
   val funpow: int -> ('a -> 'a) -> 'a -> 'a
 
-  (*old options -- invalidated*)
-  datatype invalid = None of invalid
-  exception OPTION of invalid
-
   (*options*)
   val the: 'a option -> 'a
   val these: 'a list option -> 'a list
@@ -50,9 +46,7 @@
   val is_some: 'a option -> bool
   val is_none: 'a option -> bool
   val perhaps: ('a -> 'a option) -> 'a -> 'a
-  val eq_opt: ('a * 'b -> bool) -> 'a option * 'b option -> bool
   val merge_opt: ('a * 'a -> bool) -> 'a option * 'a option -> 'a option
-  val string_of_option: ('a -> string) -> 'a option -> string
 
   (*exceptions*)
   val try: ('a -> 'b) -> 'a -> 'b option
@@ -103,7 +97,6 @@
   val change: 'a ref -> ('a -> 'a) -> unit
   val setmp: 'a ref -> 'a -> ('b -> 'c) -> 'b -> 'c
   val conditional: bool -> (unit -> unit) -> unit
-  val string_of_bool: bool -> string
 
   (*lists*)
   exception UnequalLengths
@@ -156,7 +149,6 @@
   val prefixes: 'a list -> 'a list list
   val suffixes1: 'a list -> 'a list list
   val suffixes: 'a list -> 'a list list
-  val string_of_list: ('a -> string) -> 'a list -> string
 
   (*integers*)
   val gcd: IntInf.int * IntInf.int -> IntInf.int
@@ -196,6 +188,8 @@
   val unsuffix: string -> string -> string
   val replicate_string: int -> string -> string
   val translate_string: (string -> string) -> string -> string
+  val string_of_list: ('a -> string) -> 'a list -> string
+  val string_of_option: ('a -> string) -> 'a option -> string
 
   (*lists as sets -- see also Pure/General/ord_list.ML*)
   val member: ('b * 'a -> bool) -> 'a list -> 'b -> bool
@@ -272,6 +266,7 @@
   val pwd: unit -> string
 
   (*misc*)
+  val divide_and_conquer: ('a -> 'a list * ('b list -> 'b)) -> 'a -> 'b
   val partition_eq: ('a * 'a -> bool) -> 'a list -> 'a list list
   val partition_list: (int -> 'a -> bool) -> int -> int -> 'a list -> 'a list list
   val gensym: string -> string
@@ -340,10 +335,6 @@
 
 (** options **)
 
-(*invalidate former constructors to prevent accidental use as match-all patterns!*)
-datatype invalid = None of invalid;
-exception OPTION of invalid;
-
 val the = Option.valOf;
 
 fun these (SOME x) = x
@@ -363,17 +354,10 @@
 
 fun perhaps f x = the_default x (f x);
 
-fun eq_opt eq (NONE, NONE) = true
-  | eq_opt eq (SOME x, SOME y) = eq (x, y)
-  | eq_opt _ _ = false;
-
 fun merge_opt _ (NONE, y) = y
   | merge_opt _ (x, NONE) = x
   | merge_opt eq (SOME x, SOME y) = if eq (x, y) then SOME y else raise Option;
 
-fun string_of_option f NONE     = "NONE"
-  | string_of_option f (SOME x) = "SOME (" ^ f x ^ ")";
-
 
 (* exceptions *)
 
@@ -478,6 +462,7 @@
         | boolf (x :: xs) = pred x andalso boolf xs
   in boolf end;
 
+
 (* flags *)
 
 fun set flag = (flag := true; true);
@@ -495,14 +480,11 @@
     val _ = flag := orig_value;
   in release result end;
 
+
 (* conditional execution *)
 
 fun conditional b f = if b then f () else ();
 
-(* convert a bool to a string *)
-
-fun string_of_bool b = if b then "true" else "false";
-
 
 (** lists **)
 
@@ -851,11 +833,6 @@
 
 fun oct_char s = chr (#1 (read_radixint (8, explode s)));
 
-(* convert a list to a string *)
-
-fun string_of_list f xs =
-  let val fxs = separate ", " (map f xs)
-  in  String.concat ("[" :: fxs @ ["]"])  end;
 
 
 (** strings **)
@@ -943,6 +920,11 @@
       if k mod 2 = 0 then replicate_string (k div 2) (a ^ a)
       else replicate_string (k div 2) (a ^ a) ^ a;
 
+fun string_of_list f = enclose "[" "]" o commas o map f;
+
+fun string_of_option f NONE = "NONE"
+  | string_of_option f (SOME x) = "SOME (" ^ f x ^ ")";
+
 
 
 (** lists as sets -- see also Pure/General/ord_list.ML **)
@@ -1143,11 +1125,6 @@
   else if rel (y, x) then GREATER
   else EQUAL;
 
-fun eq_ord ord xy =
-  case ord xy
-   of EQUAL => true
-    | _ => false;
-
 val int_ord = Int.compare;
 val string_ord = String.compare;
 
@@ -1244,8 +1221,13 @@
 val pwd = OS.FileSys.getDir;
 
 
+
 (** misc **)
 
+fun divide_and_conquer decomp x =
+  let val (ys, recomb) = decomp x
+  in recomb (map (divide_and_conquer decomp) ys) end;
+
 (*Partition list into elements that satisfy predicate and those that don't.
   Preserves order of elements in both lists.*)
 val partition = List.partition;