added divide_and_conquer combinator (by Amine Chaieb);
authorwenzelm
Tue May 16 13:01:27 2006 +0200 (2006-05-16)
changeset 196440b01436e1843
parent 19643 213e12ad2c03
child 19645 bbda28f2d379
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;
src/Pure/library.ML
     1.1 --- a/src/Pure/library.ML	Tue May 16 13:01:26 2006 +0200
     1.2 +++ b/src/Pure/library.ML	Tue May 16 13:01:27 2006 +0200
     1.3 @@ -38,10 +38,6 @@
     1.4    val oooo: ('a -> 'b) * ('c -> 'd -> 'e -> 'f -> 'a) -> 'c -> 'd -> 'e -> 'f -> 'b
     1.5    val funpow: int -> ('a -> 'a) -> 'a -> 'a
     1.6  
     1.7 -  (*old options -- invalidated*)
     1.8 -  datatype invalid = None of invalid
     1.9 -  exception OPTION of invalid
    1.10 -
    1.11    (*options*)
    1.12    val the: 'a option -> 'a
    1.13    val these: 'a list option -> 'a list
    1.14 @@ -50,9 +46,7 @@
    1.15    val is_some: 'a option -> bool
    1.16    val is_none: 'a option -> bool
    1.17    val perhaps: ('a -> 'a option) -> 'a -> 'a
    1.18 -  val eq_opt: ('a * 'b -> bool) -> 'a option * 'b option -> bool
    1.19    val merge_opt: ('a * 'a -> bool) -> 'a option * 'a option -> 'a option
    1.20 -  val string_of_option: ('a -> string) -> 'a option -> string
    1.21  
    1.22    (*exceptions*)
    1.23    val try: ('a -> 'b) -> 'a -> 'b option
    1.24 @@ -103,7 +97,6 @@
    1.25    val change: 'a ref -> ('a -> 'a) -> unit
    1.26    val setmp: 'a ref -> 'a -> ('b -> 'c) -> 'b -> 'c
    1.27    val conditional: bool -> (unit -> unit) -> unit
    1.28 -  val string_of_bool: bool -> string
    1.29  
    1.30    (*lists*)
    1.31    exception UnequalLengths
    1.32 @@ -156,7 +149,6 @@
    1.33    val prefixes: 'a list -> 'a list list
    1.34    val suffixes1: 'a list -> 'a list list
    1.35    val suffixes: 'a list -> 'a list list
    1.36 -  val string_of_list: ('a -> string) -> 'a list -> string
    1.37  
    1.38    (*integers*)
    1.39    val gcd: IntInf.int * IntInf.int -> IntInf.int
    1.40 @@ -196,6 +188,8 @@
    1.41    val unsuffix: string -> string -> string
    1.42    val replicate_string: int -> string -> string
    1.43    val translate_string: (string -> string) -> string -> string
    1.44 +  val string_of_list: ('a -> string) -> 'a list -> string
    1.45 +  val string_of_option: ('a -> string) -> 'a option -> string
    1.46  
    1.47    (*lists as sets -- see also Pure/General/ord_list.ML*)
    1.48    val member: ('b * 'a -> bool) -> 'a list -> 'b -> bool
    1.49 @@ -272,6 +266,7 @@
    1.50    val pwd: unit -> string
    1.51  
    1.52    (*misc*)
    1.53 +  val divide_and_conquer: ('a -> 'a list * ('b list -> 'b)) -> 'a -> 'b
    1.54    val partition_eq: ('a * 'a -> bool) -> 'a list -> 'a list list
    1.55    val partition_list: (int -> 'a -> bool) -> int -> int -> 'a list -> 'a list list
    1.56    val gensym: string -> string
    1.57 @@ -340,10 +335,6 @@
    1.58  
    1.59  (** options **)
    1.60  
    1.61 -(*invalidate former constructors to prevent accidental use as match-all patterns!*)
    1.62 -datatype invalid = None of invalid;
    1.63 -exception OPTION of invalid;
    1.64 -
    1.65  val the = Option.valOf;
    1.66  
    1.67  fun these (SOME x) = x
    1.68 @@ -363,17 +354,10 @@
    1.69  
    1.70  fun perhaps f x = the_default x (f x);
    1.71  
    1.72 -fun eq_opt eq (NONE, NONE) = true
    1.73 -  | eq_opt eq (SOME x, SOME y) = eq (x, y)
    1.74 -  | eq_opt _ _ = false;
    1.75 -
    1.76  fun merge_opt _ (NONE, y) = y
    1.77    | merge_opt _ (x, NONE) = x
    1.78    | merge_opt eq (SOME x, SOME y) = if eq (x, y) then SOME y else raise Option;
    1.79  
    1.80 -fun string_of_option f NONE     = "NONE"
    1.81 -  | string_of_option f (SOME x) = "SOME (" ^ f x ^ ")";
    1.82 -
    1.83  
    1.84  (* exceptions *)
    1.85  
    1.86 @@ -478,6 +462,7 @@
    1.87          | boolf (x :: xs) = pred x andalso boolf xs
    1.88    in boolf end;
    1.89  
    1.90 +
    1.91  (* flags *)
    1.92  
    1.93  fun set flag = (flag := true; true);
    1.94 @@ -495,14 +480,11 @@
    1.95      val _ = flag := orig_value;
    1.96    in release result end;
    1.97  
    1.98 +
    1.99  (* conditional execution *)
   1.100  
   1.101  fun conditional b f = if b then f () else ();
   1.102  
   1.103 -(* convert a bool to a string *)
   1.104 -
   1.105 -fun string_of_bool b = if b then "true" else "false";
   1.106 -
   1.107  
   1.108  (** lists **)
   1.109  
   1.110 @@ -851,11 +833,6 @@
   1.111  
   1.112  fun oct_char s = chr (#1 (read_radixint (8, explode s)));
   1.113  
   1.114 -(* convert a list to a string *)
   1.115 -
   1.116 -fun string_of_list f xs =
   1.117 -  let val fxs = separate ", " (map f xs)
   1.118 -  in  String.concat ("[" :: fxs @ ["]"])  end;
   1.119  
   1.120  
   1.121  (** strings **)
   1.122 @@ -943,6 +920,11 @@
   1.123        if k mod 2 = 0 then replicate_string (k div 2) (a ^ a)
   1.124        else replicate_string (k div 2) (a ^ a) ^ a;
   1.125  
   1.126 +fun string_of_list f = enclose "[" "]" o commas o map f;
   1.127 +
   1.128 +fun string_of_option f NONE = "NONE"
   1.129 +  | string_of_option f (SOME x) = "SOME (" ^ f x ^ ")";
   1.130 +
   1.131  
   1.132  
   1.133  (** lists as sets -- see also Pure/General/ord_list.ML **)
   1.134 @@ -1143,11 +1125,6 @@
   1.135    else if rel (y, x) then GREATER
   1.136    else EQUAL;
   1.137  
   1.138 -fun eq_ord ord xy =
   1.139 -  case ord xy
   1.140 -   of EQUAL => true
   1.141 -    | _ => false;
   1.142 -
   1.143  val int_ord = Int.compare;
   1.144  val string_ord = String.compare;
   1.145  
   1.146 @@ -1244,8 +1221,13 @@
   1.147  val pwd = OS.FileSys.getDir;
   1.148  
   1.149  
   1.150 +
   1.151  (** misc **)
   1.152  
   1.153 +fun divide_and_conquer decomp x =
   1.154 +  let val (ys, recomb) = decomp x
   1.155 +  in recomb (map (divide_and_conquer decomp) ys) end;
   1.156 +
   1.157  (*Partition list into elements that satisfy predicate and those that don't.
   1.158    Preserves order of elements in both lists.*)
   1.159  val partition = List.partition;