src/Pure/library.ML
 author wenzelm Wed Mar 18 20:03:01 2009 +0100 (2009-03-18) changeset 30572 8fbc355100f2 parent 30570 8fac7efcce0a child 31250 4b99b1214034 permissions -rw-r--r--
Library.merge/OrdList.union: optimize the important special case where the tables coincide -- NOTE: this changes both the operational behaviour and the result for non-standard eq/ord notion;
```     1 (*  Title:      Pure/library.ML
```
```     2     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
```
```     3     Author:     Markus Wenzel, TU Muenchen
```
```     4
```
```     5 Basic library: functions, pairs, booleans, lists, integers,
```
```     6 strings, lists as sets, orders, current directory, misc.
```
```     7
```
```     8 See also General/basics.ML for the most fundamental concepts.
```
```     9 *)
```
```    10
```
```    11 infix 2 ?
```
```    12 infix 3 o oo ooo oooo
```
```    13 infix 4 ~~ upto downto
```
```    14 infix orf andf \ \\ mem mem_int mem_string union union_int
```
```    15   union_string inter inter_int inter_string subset subset_int subset_string
```
```    16
```
```    17 signature BASIC_LIBRARY =
```
```    18 sig
```
```    19   (*functions*)
```
```    20   val undefined: 'a -> 'b
```
```    21   val I: 'a -> 'a
```
```    22   val K: 'a -> 'b -> 'a
```
```    23   val curry: ('a * 'b -> 'c) -> 'a -> 'b -> 'c
```
```    24   val uncurry: ('a -> 'b -> 'c) -> 'a * 'b -> 'c
```
```    25   val ? : bool * ('a -> 'a) -> 'a -> 'a
```
```    26   val oo: ('a -> 'b) * ('c -> 'd -> 'a) -> 'c -> 'd -> 'b
```
```    27   val ooo: ('a -> 'b) * ('c -> 'd -> 'e -> 'a) -> 'c -> 'd -> 'e -> 'b
```
```    28   val oooo: ('a -> 'b) * ('c -> 'd -> 'e -> 'f -> 'a) -> 'c -> 'd -> 'e -> 'f -> 'b
```
```    29   val funpow: int -> ('a -> 'a) -> 'a -> 'a
```
```    30
```
```    31   (*errors*)
```
```    32   exception SYS_ERROR of string
```
```    33   val sys_error: string -> 'a
```
```    34   exception ERROR of string
```
```    35   val error: string -> 'a
```
```    36   val cat_error: string -> string -> 'a
```
```    37   val assert_all: ('a -> bool) -> 'a list -> ('a -> string) -> unit
```
```    38
```
```    39   (*pairs*)
```
```    40   val pair: 'a -> 'b -> 'a * 'b
```
```    41   val rpair: 'a -> 'b -> 'b * 'a
```
```    42   val fst: 'a * 'b -> 'a
```
```    43   val snd: 'a * 'b -> 'b
```
```    44   val eq_fst: ('a * 'c -> bool) -> ('a * 'b) * ('c * 'd) -> bool
```
```    45   val eq_snd: ('b * 'd -> bool) -> ('a * 'b) * ('c * 'd) -> bool
```
```    46   val eq_pair: ('a * 'c -> bool) -> ('b * 'd -> bool) -> ('a * 'b) * ('c * 'd) -> bool
```
```    47   val swap: 'a * 'b -> 'b * 'a
```
```    48   val apfst: ('a -> 'b) -> 'a * 'c -> 'b * 'c
```
```    49   val apsnd: ('a -> 'b) -> 'c * 'a -> 'c * 'b
```
```    50   val pairself: ('a -> 'b) -> 'a * 'a -> 'b * 'b
```
```    51
```
```    52   (*booleans*)
```
```    53   val equal: ''a -> ''a -> bool
```
```    54   val not_equal: ''a -> ''a -> bool
```
```    55   val orf: ('a -> bool) * ('a -> bool) -> 'a -> bool
```
```    56   val andf: ('a -> bool) * ('a -> bool) -> 'a -> bool
```
```    57   val exists: ('a -> bool) -> 'a list -> bool
```
```    58   val forall: ('a -> bool) -> 'a list -> bool
```
```    59   val set: bool ref -> bool
```
```    60   val reset: bool ref -> bool
```
```    61   val toggle: bool ref -> bool
```
```    62   val change: 'a ref -> ('a -> 'a) -> unit
```
```    63   val change_result: 'a ref -> ('a -> 'b * 'a) -> 'b
```
```    64   val setmp_noncritical: 'a ref -> 'a -> ('b -> 'c) -> 'b -> 'c
```
```    65   val setmp: 'a ref -> 'a -> ('b -> 'c) -> 'b -> 'c
```
```    66   val setmp_thread_data: 'a Universal.tag -> 'a -> 'a -> ('b -> 'c) -> 'b -> 'c
```
```    67
```
```    68   (*lists*)
```
```    69   exception UnequalLengths
```
```    70   val single: 'a -> 'a list
```
```    71   val the_single: 'a list -> 'a
```
```    72   val singleton: ('a list -> 'b list) -> 'a -> 'b
```
```    73   val yield_singleton: ('a list -> 'c -> 'b list * 'c) -> 'a -> 'c -> 'b * 'c
```
```    74   val apply: ('a -> 'a) list -> 'a -> 'a
```
```    75   val perhaps_apply: ('a -> 'a option) list -> 'a -> 'a option
```
```    76   val perhaps_loop: ('a -> 'a option) -> 'a -> 'a option
```
```    77   val foldl1: ('a * 'a -> 'a) -> 'a list -> 'a
```
```    78   val foldr1: ('a * 'a -> 'a) -> 'a list -> 'a
```
```    79   val flat: 'a list list -> 'a list
```
```    80   val unflat: 'a list list -> 'b list -> 'b list list
```
```    81   val burrow: ('a list -> 'b list) -> 'a list list -> 'b list list
```
```    82   val burrow_options: ('a list -> 'b list) -> 'a option list -> 'b option list
```
```    83   val burrow_fst: ('a list -> 'b list) -> ('a * 'c) list -> ('b * 'c) list
```
```    84   val fold_burrow: ('a list -> 'c -> 'b list * 'd) -> 'a list list -> 'c -> 'b list list * 'd
```
```    85   val maps: ('a -> 'b list) -> 'a list -> 'b list
```
```    86   val filter: ('a -> bool) -> 'a list -> 'a list
```
```    87   val filter_out: ('a -> bool) -> 'a list -> 'a list
```
```    88   val map_filter: ('a -> 'b option) -> 'a list -> 'b list
```
```    89   val chop: int -> 'a list -> 'a list * 'a list
```
```    90   val dropwhile: ('a -> bool) -> 'a list -> 'a list
```
```    91   val nth: 'a list -> int -> 'a
```
```    92   val nth_map: int -> ('a -> 'a) -> 'a list -> 'a list
```
```    93   val nth_drop: int -> 'a list -> 'a list
```
```    94   val nth_list: 'a list list -> int -> 'a list
```
```    95   val map_index: (int * 'a -> 'b) -> 'a list -> 'b list
```
```    96   val fold_index: (int * 'a -> 'b -> 'b) -> 'a list -> 'b -> 'b
```
```    97   val split_last: 'a list -> 'a list * 'a
```
```    98   val find_index: ('a -> bool) -> 'a list -> int
```
```    99   val find_index_eq: ''a -> ''a list -> int
```
```   100   val find_first: ('a -> bool) -> 'a list -> 'a option
```
```   101   val get_index: ('a -> 'b option) -> 'a list -> (int * 'b) option
```
```   102   val get_first: ('a -> 'b option) -> 'a list -> 'b option
```
```   103   val eq_list: ('a * 'b -> bool) -> 'a list * 'b list -> bool
```
```   104   val map2: ('a -> 'b -> 'c) -> 'a list -> 'b list -> 'c list
```
```   105   val fold2: ('a -> 'b -> 'c -> 'c) -> 'a list -> 'b list -> 'c -> 'c
```
```   106   val zip_options: 'a list -> 'b option list -> ('a * 'b) list
```
```   107   val ~~ : 'a list * 'b list -> ('a * 'b) list
```
```   108   val map_split: ('a -> 'b * 'c) -> 'a list -> 'b list * 'c list
```
```   109   val split_list: ('a * 'b) list -> 'a list * 'b list
```
```   110   val map_product: ('a -> 'b -> 'c) -> 'a list -> 'b list -> 'c list
```
```   111   val fold_product: ('a -> 'b -> 'c -> 'c) -> 'a list -> 'b list -> 'c -> 'c
```
```   112   val separate: 'a -> 'a list -> 'a list
```
```   113   val surround: 'a -> 'a list -> 'a list
```
```   114   val replicate: int -> 'a -> 'a list
```
```   115   val is_prefix: ('a * 'a -> bool) -> 'a list -> 'a list -> bool
```
```   116   val take_prefix: ('a -> bool) -> 'a list -> 'a list * 'a list
```
```   117   val chop_prefix: ('a * 'b -> bool) -> 'a list * 'b list -> 'a list * ('a list * 'b list)
```
```   118   val take_suffix: ('a -> bool) -> 'a list -> 'a list * 'a list
```
```   119   val prefixes1: 'a list -> 'a list list
```
```   120   val prefixes: 'a list -> 'a list list
```
```   121   val suffixes1: 'a list -> 'a list list
```
```   122   val suffixes: 'a list -> 'a list list
```
```   123
```
```   124   (*integers*)
```
```   125   val inc: int ref -> int
```
```   126   val dec: int ref -> int
```
```   127   val upto: int * int -> int list
```
```   128   val downto: int * int -> int list
```
```   129   val radixpand: int * int -> int list
```
```   130   val radixstring: int * string * int -> string
```
```   131   val string_of_int: int -> string
```
```   132   val signed_string_of_int: int -> string
```
```   133   val string_of_indexname: string * int -> string
```
```   134   val read_radix_int: int -> string list -> int * string list
```
```   135   val read_int: string list -> int * string list
```
```   136   val oct_char: string -> string
```
```   137
```
```   138   (*strings*)
```
```   139   val nth_string: string -> int -> string
```
```   140   val fold_string: (string -> 'a -> 'a) -> string -> 'a -> 'a
```
```   141   val exists_string: (string -> bool) -> string -> bool
```
```   142   val forall_string: (string -> bool) -> string -> bool
```
```   143   val first_field: string -> string -> (string * string) option
```
```   144   val enclose: string -> string -> string -> string
```
```   145   val unenclose: string -> string
```
```   146   val quote: string -> string
```
```   147   val space_implode: string -> string list -> string
```
```   148   val commas: string list -> string
```
```   149   val commas_quote: string list -> string
```
```   150   val cat_lines: string list -> string
```
```   151   val space_explode: string -> string -> string list
```
```   152   val split_lines: string -> string list
```
```   153   val prefix_lines: string -> string -> string
```
```   154   val prefix: string -> string -> string
```
```   155   val suffix: string -> string -> string
```
```   156   val unprefix: string -> string -> string
```
```   157   val unsuffix: string -> string -> string
```
```   158   val replicate_string: int -> string -> string
```
```   159   val translate_string: (string -> string) -> string -> string
```
```   160   val multiply: 'a list -> 'a list list -> 'a list list
```
```   161   val match_string: string -> string -> bool
```
```   162
```
```   163   (*lists as sets -- see also Pure/General/ord_list.ML*)
```
```   164   val member: ('b * 'a -> bool) -> 'a list -> 'b -> bool
```
```   165   val insert: ('a * 'a -> bool) -> 'a -> 'a list -> 'a list
```
```   166   val remove: ('b * 'a -> bool) -> 'b -> 'a list -> 'a list
```
```   167   val update: ('a * 'a -> bool) -> 'a -> 'a list -> 'a list
```
```   168   val subtract: ('b * 'a -> bool) -> 'b list -> 'a list -> 'a list
```
```   169   val merge: ('a * 'a -> bool) -> 'a list * 'a list -> 'a list
```
```   170   val mem: ''a * ''a list -> bool
```
```   171   val mem_int: int * int list -> bool
```
```   172   val mem_string: string * string list -> bool
```
```   173   val union: ''a list * ''a list -> ''a list
```
```   174   val union_int: int list * int list -> int list
```
```   175   val union_string: string list * string list -> string list
```
```   176   val gen_union: ('a * 'a -> bool) -> 'a list * 'a list -> 'a list
```
```   177   val gen_inter: ('a * 'b -> bool) -> 'a list * 'b list -> 'a list
```
```   178   val inter: ''a list * ''a list -> ''a list
```
```   179   val inter_int: int list * int list -> int list
```
```   180   val inter_string: string list * string list -> string list
```
```   181   val subset: ''a list * ''a list -> bool
```
```   182   val subset_int: int list * int list -> bool
```
```   183   val subset_string: string list * string list -> bool
```
```   184   val eq_set: ''a list * ''a list -> bool
```
```   185   val eq_set_string: string list * string list -> bool
```
```   186   val gen_subset: ('a * 'b -> bool) -> 'a list * 'b list -> bool
```
```   187   val gen_eq_set: ('a * 'b -> bool) -> 'a list * 'b list -> bool
```
```   188   val \ : ''a list * ''a -> ''a list
```
```   189   val \\ : ''a list * ''a list -> ''a list
```
```   190   val distinct: ('a * 'a -> bool) -> 'a list -> 'a list
```
```   191   val duplicates: ('a * 'a -> bool) -> 'a list -> 'a list
```
```   192   val has_duplicates: ('a * 'a -> bool) -> 'a list -> bool
```
```   193
```
```   194   (*lists as multisets*)
```
```   195   val remove1: ('b * 'a -> bool) -> 'b -> 'a list -> 'a list
```
```   196   val submultiset: ('a * 'b -> bool) -> 'a list * 'b list -> bool
```
```   197
```
```   198   (*orders*)
```
```   199   val is_equal: order -> bool
```
```   200   val rev_order: order -> order
```
```   201   val make_ord: ('a * 'a -> bool) -> 'a * 'a -> order
```
```   202   val bool_ord: bool * bool -> order
```
```   203   val int_ord: int * int -> order
```
```   204   val string_ord: string * string -> order
```
```   205   val fast_string_ord: string * string -> order
```
```   206   val option_ord: ('a * 'b -> order) -> 'a option * 'b option -> order
```
```   207   val prod_ord: ('a * 'b -> order) -> ('c * 'd -> order) -> ('a * 'c) * ('b * 'd) -> order
```
```   208   val dict_ord: ('a * 'b -> order) -> 'a list * 'b list -> order
```
```   209   val list_ord: ('a * 'b -> order) -> 'a list * 'b list -> order
```
```   210   val sort: ('a * 'a -> order) -> 'a list -> 'a list
```
```   211   val sort_distinct: ('a * 'a -> order) -> 'a list -> 'a list
```
```   212   val sort_strings: string list -> string list
```
```   213   val sort_wrt: ('a -> string) -> 'a list -> 'a list
```
```   214   val tag_list: int -> 'a list -> (int * 'a) list
```
```   215   val untag_list: (int * 'a) list -> 'a list
```
```   216   val order_list: (int * 'a) list -> 'a list
```
```   217
```
```   218   (*random numbers*)
```
```   219   exception RANDOM
```
```   220   val random: unit -> real
```
```   221   val random_range: int -> int -> int
```
```   222   val one_of: 'a list -> 'a
```
```   223   val frequency: (int * 'a) list -> 'a
```
```   224
```
```   225   (*misc*)
```
```   226   val divide_and_conquer: ('a -> 'a list * ('b list -> 'b)) -> 'a -> 'b
```
```   227   val partition_eq: ('a * 'a -> bool) -> 'a list -> 'a list list
```
```   228   val partition_list: (int -> 'a -> bool) -> int -> int -> 'a list -> 'a list list
```
```   229   val gensym: string -> string
```
```   230   type stamp
```
```   231   val stamp: unit -> stamp
```
```   232   type serial
```
```   233   val serial: unit -> serial
```
```   234   val serial_string: unit -> string
```
```   235   structure Object: sig type T end
```
```   236 end;
```
```   237
```
```   238 signature LIBRARY =
```
```   239 sig
```
```   240   include BASIC_LIBRARY
```
```   241   val foldl: ('a * 'b -> 'a) -> 'a * 'b list -> 'a
```
```   242   val foldr: ('a * 'b -> 'b) -> 'a list * 'b -> 'b
```
```   243   val foldl_map: ('a * 'b -> 'a * 'c) -> 'a * 'b list -> 'a * 'c list
```
```   244   val take: int * 'a list -> 'a list
```
```   245   val drop: int * 'a list -> 'a list
```
```   246   val last_elem: 'a list -> 'a
```
```   247 end;
```
```   248
```
```   249 structure Library: LIBRARY =
```
```   250 struct
```
```   251
```
```   252 (* functions *)
```
```   253
```
```   254 fun undefined _ = raise Match;
```
```   255
```
```   256 fun I x = x;
```
```   257 fun K x = fn _ => x;
```
```   258 fun curry f x y = f (x, y);
```
```   259 fun uncurry f (x, y) = f x y;
```
```   260
```
```   261 (*conditional application*)
```
```   262 fun b ? f = fn x => if b then f x else x;
```
```   263
```
```   264 (*composition with multiple args*)
```
```   265 fun (f oo g) x y = f (g x y);
```
```   266 fun (f ooo g) x y z = f (g x y z);
```
```   267 fun (f oooo g) x y z w = f (g x y z w);
```
```   268
```
```   269 (*function exponentiation: f(...(f x)...) with n applications of f*)
```
```   270 fun funpow (0: int) _ x = x
```
```   271   | funpow n f x = funpow (n - 1) f (f x);
```
```   272
```
```   273
```
```   274 (* errors *)
```
```   275
```
```   276 exception SYS_ERROR of string;
```
```   277 fun sys_error msg = raise SYS_ERROR msg;
```
```   278
```
```   279 exception ERROR of string;
```
```   280 fun error msg = raise ERROR msg;
```
```   281
```
```   282 fun cat_error "" msg = error msg
```
```   283   | cat_error msg1 msg2 = error (msg1 ^ "\n" ^ msg2);
```
```   284
```
```   285 fun assert_all pred list msg =
```
```   286   let
```
```   287     fun ass [] = ()
```
```   288       | ass (x :: xs) = if pred x then ass xs else error (msg x);
```
```   289   in ass list end;
```
```   290
```
```   291
```
```   292 (* pairs *)
```
```   293
```
```   294 fun pair x y = (x, y);
```
```   295 fun rpair x y = (y, x);
```
```   296
```
```   297 fun fst (x, y) = x;
```
```   298 fun snd (x, y) = y;
```
```   299
```
```   300 fun eq_fst eq ((x1, _), (x2, _)) = eq (x1, x2);
```
```   301 fun eq_snd eq ((_, y1), (_, y2)) = eq (y1, y2);
```
```   302 fun eq_pair eqx eqy ((x1, y1), (x2, y2)) = eqx (x1, x2) andalso eqy (y1, y2);
```
```   303
```
```   304 fun swap (x, y) = (y, x);
```
```   305
```
```   306 fun apfst f (x, y) = (f x, y);
```
```   307 fun apsnd f (x, y) = (x, f y);
```
```   308 fun pairself f (x, y) = (f x, f y);
```
```   309
```
```   310
```
```   311 (* booleans *)
```
```   312
```
```   313 (*polymorphic equality*)
```
```   314 fun equal x y = x = y;
```
```   315 fun not_equal x y = x <> y;
```
```   316
```
```   317 (*combining predicates*)
```
```   318 fun p orf q = fn x => p x orelse q x;
```
```   319 fun p andf q = fn x => p x andalso q x;
```
```   320
```
```   321 val exists = List.exists;
```
```   322 val forall = List.all;
```
```   323
```
```   324
```
```   325 (* flags *)
```
```   326
```
```   327 fun set flag = (flag := true; true);
```
```   328 fun reset flag = (flag := false; false);
```
```   329 fun toggle flag = (flag := not (! flag); ! flag);
```
```   330
```
```   331 fun change r f = r := f (! r);
```
```   332 fun change_result r f = let val (x, y) = f (! r) in r := y; x end;
```
```   333
```
```   334 (*temporarily set flag during execution*)
```
```   335 fun setmp_noncritical flag value f x =
```
```   336   uninterruptible (fn restore_attributes => fn () =>
```
```   337     let
```
```   338       val orig_value = ! flag;
```
```   339       val _ = flag := value;
```
```   340       val result = Exn.capture (restore_attributes f) x;
```
```   341       val _ = flag := orig_value;
```
```   342     in Exn.release result end) ();
```
```   343
```
```   344 fun setmp flag value f x =
```
```   345   NAMED_CRITICAL "setmp" (fn () => setmp_noncritical flag value f x);
```
```   346
```
```   347 fun setmp_thread_data tag orig_data data f x =
```
```   348   uninterruptible (fn restore_attributes => fn () =>
```
```   349     let
```
```   350       val _ = Thread.setLocal (tag, data);
```
```   351       val result = Exn.capture (restore_attributes f) x;
```
```   352       val _ = Thread.setLocal (tag, orig_data);
```
```   353     in Exn.release result end) ();
```
```   354
```
```   355
```
```   356
```
```   357 (** lists **)
```
```   358
```
```   359 exception UnequalLengths;
```
```   360
```
```   361 fun single x = [x];
```
```   362
```
```   363 fun the_single [x] = x
```
```   364   | the_single _ = raise Empty;
```
```   365
```
```   366 fun singleton f x = the_single (f [x]);
```
```   367
```
```   368 fun yield_singleton f x = f [x] #>> the_single;
```
```   369
```
```   370 fun apply [] x = x
```
```   371   | apply (f :: fs) x = apply fs (f x);
```
```   372
```
```   373 fun perhaps_apply funs arg =
```
```   374   let
```
```   375     fun app [] res = res
```
```   376       | app (f :: fs) (changed, x) =
```
```   377           (case f x of
```
```   378             NONE => app fs (changed, x)
```
```   379           | SOME x' => app fs (true, x'));
```
```   380   in (case app funs (false, arg) of (false, _) => NONE | (true, arg') => SOME arg') end;
```
```   381
```
```   382 fun perhaps_loop f arg =
```
```   383   let
```
```   384     fun loop (changed, x) =
```
```   385       (case f x of
```
```   386         NONE => (changed, x)
```
```   387       | SOME x' => loop (true, x'));
```
```   388   in (case loop (false, arg) of (false, _) => NONE | (true, arg') => SOME arg') end;
```
```   389
```
```   390
```
```   391 (* fold -- old versions *)
```
```   392
```
```   393 (*the following versions of fold are designed to fit nicely with infixes*)
```
```   394
```
```   395 (*  (op @) (e, [x1, ..., xn])  ===>  ((e @ x1) @ x2) ... @ xn
```
```   396     for operators that associate to the left (TAIL RECURSIVE)*)
```
```   397 fun foldl (f: 'a * 'b -> 'a) : 'a * 'b list -> 'a =
```
```   398   let fun itl (e, [])  = e
```
```   399         | itl (e, a::l) = itl (f(e, a), l)
```
```   400   in  itl end;
```
```   401
```
```   402 (*  (op @) ([x1, ..., xn], e)  ===>   x1 @ (x2 ... @ (xn @ e))
```
```   403     for operators that associate to the right (not tail recursive)*)
```
```   404 fun foldr f (l, e) =
```
```   405   let fun itr [] = e
```
```   406         | itr (a::l) = f(a, itr l)
```
```   407   in  itr l  end;
```
```   408
```
```   409 (*  (op @) [x1, ..., xn]  ===>  ((x1 @ x2) @ x3) ... @ xn
```
```   410     for operators that associate to the left (TAIL RECURSIVE)*)
```
```   411 fun foldl1 f [] = raise Empty
```
```   412   | foldl1 f (x :: xs) = foldl f (x, xs);
```
```   413
```
```   414 (*  (op @) [x1, ..., xn]  ===>   x1 @ (x2 ... @ (x[n-1] @ xn))
```
```   415     for n > 0, operators that associate to the right (not tail recursive)*)
```
```   416 fun foldr1 f [] = raise Empty
```
```   417   | foldr1 f l =
```
```   418       let fun itr [x] = x
```
```   419             | itr (x::l) = f(x, itr l)
```
```   420       in  itr l  end;
```
```   421
```
```   422 fun foldl_map f =
```
```   423   let
```
```   424     fun fold_aux (x, []) = (x, [])
```
```   425       | fold_aux (x, y :: ys) =
```
```   426           let
```
```   427             val (x', y') = f (x, y);
```
```   428             val (x'', ys') = fold_aux (x', ys);
```
```   429           in (x'', y' :: ys') end;
```
```   430   in fold_aux end;
```
```   431
```
```   432
```
```   433 (* basic list functions *)
```
```   434
```
```   435 fun eq_list eq (list1, list2) =
```
```   436   let
```
```   437     fun eq_lst (x :: xs, y :: ys) = eq (x, y) andalso eq_lst (xs, ys)
```
```   438       | eq_lst _ = true;
```
```   439   in length list1 = length list2 andalso eq_lst (list1, list2) end;
```
```   440
```
```   441 fun maps f [] = []
```
```   442   | maps f (x :: xs) = f x @ maps f xs;
```
```   443
```
```   444 val filter = List.filter;
```
```   445 fun filter_out f = filter (not o f);
```
```   446 val map_filter = List.mapPartial;
```
```   447
```
```   448 fun chop (0: int) xs = ([], xs)
```
```   449   | chop _ [] = ([], [])
```
```   450   | chop n (x :: xs) = chop (n - 1) xs |>> cons x;
```
```   451
```
```   452 (*take the first n elements from a list*)
```
```   453 fun take (n: int, []) = []
```
```   454   | take (n, x :: xs) =
```
```   455       if n > 0 then x :: take (n - 1, xs) else [];
```
```   456
```
```   457 (*drop the first n elements from a list*)
```
```   458 fun drop (n: int, []) = []
```
```   459   | drop (n, x :: xs) =
```
```   460       if n > 0 then drop (n - 1, xs) else x :: xs;
```
```   461
```
```   462 fun dropwhile P [] = []
```
```   463   | dropwhile P (ys as x::xs) = if P x then dropwhile P xs else ys;
```
```   464
```
```   465 (*return nth element of a list, where 0 designates the first element;
```
```   466   raise Subscript if list too short*)
```
```   467 fun nth xs i = List.nth (xs, i);
```
```   468
```
```   469 fun nth_list xss i = nth xss i handle Subscript => [];
```
```   470
```
```   471 fun nth_map 0 f (x :: xs) = f x :: xs
```
```   472   | nth_map n f (x :: xs) = x :: nth_map (n - 1) f xs
```
```   473   | nth_map (_: int) _ [] = raise Subscript;
```
```   474
```
```   475 fun nth_drop n xs =
```
```   476   List.take (xs, n) @ List.drop (xs, n + 1);
```
```   477
```
```   478 fun map_index f =
```
```   479   let
```
```   480     fun mapp (_: int) [] = []
```
```   481       | mapp i (x :: xs) = f (i, x) :: mapp (i + 1) xs
```
```   482   in mapp 0 end;
```
```   483
```
```   484 fun fold_index f =
```
```   485   let
```
```   486     fun fold_aux (_: int) [] y = y
```
```   487       | fold_aux i (x :: xs) y = fold_aux (i + 1) xs (f (i, x) y);
```
```   488   in fold_aux 0 end;
```
```   489
```
```   490 val last_elem = List.last;
```
```   491
```
```   492 (*rear decomposition*)
```
```   493 fun split_last [] = raise Empty
```
```   494   | split_last [x] = ([], x)
```
```   495   | split_last (x :: xs) = apfst (cons x) (split_last xs);
```
```   496
```
```   497 (*find position of first element satisfying a predicate*)
```
```   498 fun find_index pred =
```
```   499   let fun find (_: int) [] = ~1
```
```   500         | find n (x :: xs) = if pred x then n else find (n + 1) xs;
```
```   501   in find 0 end;
```
```   502
```
```   503 fun find_index_eq x = find_index (equal x);
```
```   504
```
```   505 (*find first element satisfying predicate*)
```
```   506 val find_first = List.find;
```
```   507
```
```   508 (*get first element by lookup function*)
```
```   509 fun get_first _ [] = NONE
```
```   510   | get_first f (x :: xs) =
```
```   511       (case f x of
```
```   512         NONE => get_first f xs
```
```   513       | some => some);
```
```   514
```
```   515 fun get_index f =
```
```   516   let
```
```   517     fun get (_: int) [] = NONE
```
```   518       | get i (x :: xs) =
```
```   519           case f x
```
```   520            of NONE => get (i + 1) xs
```
```   521             | SOME y => SOME (i, y)
```
```   522   in get 0 end;
```
```   523
```
```   524 val flat = List.concat;
```
```   525
```
```   526 fun unflat (xs :: xss) ys =
```
```   527       let val (ps, qs) = chop (length xs) ys
```
```   528       in ps :: unflat xss qs end
```
```   529   | unflat [] [] = []
```
```   530   | unflat _ _ = raise UnequalLengths;
```
```   531
```
```   532 fun burrow f xss = unflat xss (f (flat xss));
```
```   533
```
```   534 fun burrow_options f os = map (try hd) (burrow f (map the_list os));
```
```   535
```
```   536 fun fold_burrow f xss s =
```
```   537   apfst (unflat xss) (f (flat xss) s);
```
```   538
```
```   539 (*separate s [x1, x2, ..., xn]  ===>  [x1, s, x2, s, ..., s, xn]*)
```
```   540 fun separate s (x :: (xs as _ :: _)) = x :: s :: separate s xs
```
```   541   | separate _ xs = xs;
```
```   542
```
```   543 fun surround s (x :: xs) = s :: x :: surround s xs
```
```   544   | surround s [] = [s];
```
```   545
```
```   546 (*make the list [x, x, ..., x] of length n*)
```
```   547 fun replicate (n: int) x =
```
```   548   let fun rep (0, xs) = xs
```
```   549         | rep (n, xs) = rep (n - 1, x :: xs)
```
```   550   in
```
```   551     if n < 0 then raise Subscript
```
```   552     else rep (n, [])
```
```   553   end;
```
```   554
```
```   555 fun translate_string f = String.translate (f o String.str);
```
```   556
```
```   557 (*multiply [a, b, c, ...] * [xs, ys, zs, ...]*)
```
```   558 fun multiply [] _ = []
```
```   559   | multiply (x :: xs) yss = map (cons x) yss @ multiply xs yss;
```
```   560
```
```   561 (* direct product *)
```
```   562
```
```   563 fun map_product f _ [] = []
```
```   564   | map_product f [] _ = []
```
```   565   | map_product f (x :: xs) ys = map (f x) ys @ map_product f xs ys;
```
```   566
```
```   567 fun fold_product f _ [] z = z
```
```   568   | fold_product f [] _ z = z
```
```   569   | fold_product f (x :: xs) ys z = z |> fold (f x) ys |> fold_product f xs ys;
```
```   570
```
```   571
```
```   572 (* lists of pairs *)
```
```   573
```
```   574 exception UnequalLengths;
```
```   575
```
```   576 fun map2 _ [] [] = []
```
```   577   | map2 f (x :: xs) (y :: ys) = f x y :: map2 f xs ys
```
```   578   | map2 _ _ _ = raise UnequalLengths;
```
```   579
```
```   580 fun fold2 f [] [] z = z
```
```   581   | fold2 f (x :: xs) (y :: ys) z = fold2 f xs ys (f x y z)
```
```   582   | fold2 f _ _ _ = raise UnequalLengths;
```
```   583
```
```   584 fun map_split f [] = ([], [])
```
```   585   | map_split f (x :: xs) =
```
```   586       let
```
```   587         val (y, w) = f x;
```
```   588         val (ys, ws) = map_split f xs;
```
```   589       in (y :: ys, w :: ws) end;
```
```   590
```
```   591 fun zip_options (x :: xs) (SOME y :: ys) = (x, y) :: zip_options xs ys
```
```   592   | zip_options (_ :: xs) (NONE :: ys) = zip_options xs ys
```
```   593   | zip_options _ [] = []
```
```   594   | zip_options [] _ = raise UnequalLengths;
```
```   595
```
```   596 (*combine two lists forming a list of pairs:
```
```   597   [x1, ..., xn] ~~ [y1, ..., yn]  ===>  [(x1, y1), ..., (xn, yn)]*)
```
```   598 fun [] ~~ [] = []
```
```   599   | (x :: xs) ~~ (y :: ys) = (x, y) :: (xs ~~ ys)
```
```   600   | _ ~~ _ = raise UnequalLengths;
```
```   601
```
```   602 (*inverse of ~~; the old 'split':
```
```   603   [(x1, y1), ..., (xn, yn)]  ===>  ([x1, ..., xn], [y1, ..., yn])*)
```
```   604 val split_list = ListPair.unzip;
```
```   605
```
```   606 fun burrow_fst f xs = split_list xs |>> f |> op ~~;
```
```   607
```
```   608
```
```   609 (* prefixes, suffixes *)
```
```   610
```
```   611 fun is_prefix _ [] _ = true
```
```   612   | is_prefix eq (x :: xs) (y :: ys) = eq (x, y) andalso is_prefix eq xs ys
```
```   613   | is_prefix eq _ _ = false;
```
```   614
```
```   615 (* [x1, ..., xi, ..., xn]  --->  ([x1, ..., x(i-1)], [xi, ..., xn])
```
```   616    where xi is the first element that does not satisfy the predicate*)
```
```   617 fun take_prefix (pred : 'a -> bool)  (xs: 'a list) : 'a list * 'a list =
```
```   618   let fun take (rxs, []) = (rev rxs, [])
```
```   619         | take (rxs, x :: xs) =
```
```   620             if  pred x  then  take(x :: rxs, xs)  else  (rev rxs, x :: xs)
```
```   621   in  take([], xs)  end;
```
```   622
```
```   623 fun chop_prefix eq ([], ys) = ([], ([], ys))
```
```   624   | chop_prefix eq (xs, []) = ([], (xs, []))
```
```   625   | chop_prefix eq (xs as x :: xs', ys as y :: ys') =
```
```   626       if eq (x, y) then
```
```   627         let val (ps', xys'') = chop_prefix eq (xs', ys')
```
```   628         in (x :: ps', xys'') end
```
```   629       else ([], (xs, ys));
```
```   630
```
```   631 (* [x1, ..., xi, ..., xn]  --->  ([x1, ..., xi], [x(i+1), ..., xn])
```
```   632    where xi is the last element that does not satisfy the predicate*)
```
```   633 fun take_suffix _ [] = ([], [])
```
```   634   | take_suffix pred (x :: xs) =
```
```   635       (case take_suffix pred xs of
```
```   636         ([], sffx) => if pred x then ([], x :: sffx) else ([x], sffx)
```
```   637       | (prfx, sffx) => (x :: prfx, sffx));
```
```   638
```
```   639 fun prefixes1 [] = []
```
```   640   | prefixes1 (x :: xs) = map (cons x) ([] :: prefixes1 xs);
```
```   641
```
```   642 fun prefixes xs = [] :: prefixes1 xs;
```
```   643
```
```   644 fun suffixes1 xs = map rev (prefixes1 (rev xs));
```
```   645 fun suffixes xs = [] :: suffixes1 xs;
```
```   646
```
```   647
```
```   648
```
```   649 (** integers **)
```
```   650
```
```   651 fun inc i = (i := ! i + (1: int); ! i);
```
```   652 fun dec i = (i := ! i - (1: int); ! i);
```
```   653
```
```   654
```
```   655 (* lists of integers *)
```
```   656
```
```   657 (*make the list [from, from + 1, ..., to]*)
```
```   658 fun ((i: int) upto j) =
```
```   659   if i > j then [] else i :: (i + 1 upto j);
```
```   660
```
```   661 (*make the list [from, from - 1, ..., to]*)
```
```   662 fun ((i: int) downto j) =
```
```   663   if i < j then [] else i :: (i - 1 downto j);
```
```   664
```
```   665
```
```   666 (* convert integers to strings *)
```
```   667
```
```   668 (*expand the number in the given base;
```
```   669   example: radixpand (2, 8) gives [1, 0, 0, 0]*)
```
```   670 fun radixpand (base, num) : int list =
```
```   671   let
```
```   672     fun radix (n, tail) =
```
```   673       if n < base then n :: tail
```
```   674       else radix (n div base, (n mod base) :: tail)
```
```   675   in radix (num, []) end;
```
```   676
```
```   677 (*expands a number into a string of characters starting from "zerochar";
```
```   678   example: radixstring (2, "0", 8) gives "1000"*)
```
```   679 fun radixstring (base, zerochar, num) =
```
```   680   let val offset = ord zerochar;
```
```   681       fun chrof n = chr (offset + n)
```
```   682   in implode (map chrof (radixpand (base, num))) end;
```
```   683
```
```   684
```
```   685 val string_of_int = Int.toString;
```
```   686
```
```   687 fun signed_string_of_int i =
```
```   688   if i < 0 then "-" ^ string_of_int (~ i) else string_of_int i;
```
```   689
```
```   690 fun string_of_indexname (a, 0) = a
```
```   691   | string_of_indexname (a, i) = a ^ "_" ^ string_of_int i;
```
```   692
```
```   693
```
```   694 (* read integers *)
```
```   695
```
```   696 fun read_radix_int radix cs =
```
```   697   let
```
```   698     val zero = ord "0";
```
```   699     val limit = zero + radix;
```
```   700     fun scan (num, []) = (num, [])
```
```   701       | scan (num, c :: cs) =
```
```   702         if zero <= ord c andalso ord c < limit then
```
```   703           scan (radix * num + (ord c - zero), cs)
```
```   704         else (num, c :: cs);
```
```   705   in scan (0, cs) end;
```
```   706
```
```   707 val read_int = read_radix_int 10;
```
```   708
```
```   709 fun oct_char s = chr (#1 (read_radix_int 8 (explode s)));
```
```   710
```
```   711
```
```   712
```
```   713 (** strings **)
```
```   714
```
```   715 (* functions tuned for strings, avoiding explode *)
```
```   716
```
```   717 fun nth_string str i =
```
```   718   (case try String.substring (str, i, 1) of
```
```   719     SOME s => s
```
```   720   | NONE => raise Subscript);
```
```   721
```
```   722 fun fold_string f str x0 =
```
```   723   let
```
```   724     val n = size str;
```
```   725     fun iter (x, i) =
```
```   726       if i < n then iter (f (String.substring (str, i, 1)) x, i + 1) else x;
```
```   727   in iter (x0, 0) end;
```
```   728
```
```   729 fun exists_string pred str =
```
```   730   let
```
```   731     val n = size str;
```
```   732     fun ex i = i < n andalso (pred (String.substring (str, i, 1)) orelse ex (i + 1));
```
```   733   in ex 0 end;
```
```   734
```
```   735 fun forall_string pred = not o exists_string (not o pred);
```
```   736
```
```   737 fun first_field sep str =
```
```   738   let
```
```   739     val n = size sep;
```
```   740     val len = size str;
```
```   741     fun find i =
```
```   742       if i + n > len then NONE
```
```   743       else if String.substring (str, i, n) = sep then SOME i
```
```   744       else find (i + 1);
```
```   745   in
```
```   746     (case find 0 of
```
```   747       NONE => NONE
```
```   748     | SOME i => SOME (String.substring (str, 0, i), String.extract (str, i + n, NONE)))
```
```   749   end;
```
```   750
```
```   751 (*enclose in brackets*)
```
```   752 fun enclose lpar rpar str = lpar ^ str ^ rpar;
```
```   753 fun unenclose str = String.substring (str, 1, size str - 2);
```
```   754
```
```   755 (*simple quoting (does not escape special chars)*)
```
```   756 val quote = enclose "\"" "\"";
```
```   757
```
```   758 (*space_implode "..." (explode "hello") = "h...e...l...l...o"*)
```
```   759 fun space_implode a bs = implode (separate a bs);
```
```   760
```
```   761 val commas = space_implode ", ";
```
```   762 val commas_quote = commas o map quote;
```
```   763
```
```   764 (*concatenate messages, one per line, into a string*)
```
```   765 val cat_lines = space_implode "\n";
```
```   766
```
```   767 (*space_explode "." "h.e..l.lo" = ["h", "e", "", "l", "lo"]*)
```
```   768 fun space_explode _ "" = []
```
```   769   | space_explode sep s = String.fields (fn c => str c = sep) s;
```
```   770
```
```   771 val split_lines = space_explode "\n";
```
```   772
```
```   773 fun prefix_lines "" txt = txt
```
```   774   | prefix_lines prfx txt = txt |> split_lines |> map (fn s => prfx ^ s) |> cat_lines;
```
```   775
```
```   776 fun prefix prfx s = prfx ^ s;
```
```   777 fun suffix sffx s = s ^ sffx;
```
```   778
```
```   779 fun unprefix prfx s =
```
```   780   if String.isPrefix prfx s then String.substring (s, size prfx, size s - size prfx)
```
```   781   else raise Fail "unprefix";
```
```   782
```
```   783 fun unsuffix sffx s =
```
```   784   if String.isSuffix sffx s then String.substring (s, 0, size s - size sffx)
```
```   785   else raise Fail "unsuffix";
```
```   786
```
```   787 fun replicate_string (0: int) _ = ""
```
```   788   | replicate_string 1 a = a
```
```   789   | replicate_string k a =
```
```   790       if k mod 2 = 0 then replicate_string (k div 2) (a ^ a)
```
```   791       else replicate_string (k div 2) (a ^ a) ^ a;
```
```   792
```
```   793 (*crude matching of str against simple glob pat*)
```
```   794 fun match_string pat str =
```
```   795   let
```
```   796     fun match [] _ = true
```
```   797       | match (p :: ps) s =
```
```   798           size p <= size s andalso
```
```   799             (case try (unprefix p) s of
```
```   800               SOME s' => match ps s'
```
```   801             | NONE => match (p :: ps) (String.substring (s, 1, size s - 1)));
```
```   802   in match (space_explode "*" pat) str end;
```
```   803
```
```   804 (** lists as sets -- see also Pure/General/ord_list.ML **)
```
```   805
```
```   806 (* canonical operations *)
```
```   807
```
```   808 fun member eq list x =
```
```   809   let
```
```   810     fun memb [] = false
```
```   811       | memb (y :: ys) = eq (x, y) orelse memb ys;
```
```   812   in memb list end;
```
```   813
```
```   814 fun insert eq x xs = if member eq xs x then xs else x :: xs;
```
```   815 fun remove eq x xs = if member eq xs x then filter_out (fn y => eq (x, y)) xs else xs;
```
```   816 fun update eq x xs = cons x (remove eq x xs);
```
```   817
```
```   818 fun subtract eq = fold (remove eq);
```
```   819
```
```   820 fun merge eq (xs, ys) =
```
```   821   if pointer_eq (xs, ys) then xs
```
```   822   else if null xs then ys
```
```   823   else fold_rev (insert eq) ys xs;
```
```   824
```
```   825
```
```   826 (* old-style infixes *)
```
```   827
```
```   828 fun x mem xs = member (op =) xs x;
```
```   829 fun (x: int) mem_int xs = member (op =) xs x;
```
```   830 fun (x: string) mem_string xs = member (op =) xs x;
```
```   831
```
```   832 (*union of sets represented as lists: no repetitions*)
```
```   833 fun xs union [] = xs
```
```   834   | [] union ys = ys
```
```   835   | (x :: xs) union ys = xs union (insert (op =) x ys);
```
```   836
```
```   837 (*union of sets, optimized version for ints*)
```
```   838 fun (xs:int list) union_int [] = xs
```
```   839   | [] union_int ys = ys
```
```   840   | (x :: xs) union_int ys = xs union_int (insert (op =) x ys);
```
```   841
```
```   842 (*union of sets, optimized version for strings*)
```
```   843 fun (xs:string list) union_string [] = xs
```
```   844   | [] union_string ys = ys
```
```   845   | (x :: xs) union_string ys = xs union_string (insert (op =) x ys);
```
```   846
```
```   847 (*generalized union*)
```
```   848 fun gen_union eq (xs, []) = xs
```
```   849   | gen_union eq ([], ys) = ys
```
```   850   | gen_union eq (x :: xs, ys) = gen_union eq (xs, insert eq x ys);
```
```   851
```
```   852
```
```   853 (*intersection*)
```
```   854 fun [] inter ys = []
```
```   855   | (x :: xs) inter ys =
```
```   856       if x mem ys then x :: (xs inter ys) else xs inter ys;
```
```   857
```
```   858 (*intersection, optimized version for ints*)
```
```   859 fun ([]:int list) inter_int ys = []
```
```   860   | (x :: xs) inter_int ys =
```
```   861       if x mem_int ys then x :: (xs inter_int ys) else xs inter_int ys;
```
```   862
```
```   863 (*intersection, optimized version for strings *)
```
```   864 fun ([]:string list) inter_string ys = []
```
```   865   | (x :: xs) inter_string ys =
```
```   866       if x mem_string ys then x :: (xs inter_string ys) else xs inter_string ys;
```
```   867
```
```   868 (*generalized intersection*)
```
```   869 fun gen_inter eq ([], ys) = []
```
```   870   | gen_inter eq (x::xs, ys) =
```
```   871       if member eq ys x then x :: gen_inter eq (xs, ys)
```
```   872       else gen_inter eq (xs, ys);
```
```   873
```
```   874
```
```   875 (*subset*)
```
```   876 fun [] subset ys = true
```
```   877   | (x :: xs) subset ys = x mem ys andalso xs subset ys;
```
```   878
```
```   879 (*subset, optimized version for ints*)
```
```   880 fun ([]: int list) subset_int ys = true
```
```   881   | (x :: xs) subset_int ys = x mem_int ys andalso xs subset_int ys;
```
```   882
```
```   883 (*subset, optimized version for strings*)
```
```   884 fun ([]: string list) subset_string ys = true
```
```   885   | (x :: xs) subset_string ys = x mem_string ys andalso xs subset_string ys;
```
```   886
```
```   887 (*set equality*)
```
```   888 fun eq_set (xs, ys) =
```
```   889   xs = ys orelse (xs subset ys andalso ys subset xs);
```
```   890
```
```   891 (*set equality for strings*)
```
```   892 fun eq_set_string ((xs: string list), ys) =
```
```   893   xs = ys orelse (xs subset_string ys andalso ys subset_string xs);
```
```   894
```
```   895 fun gen_subset eq (xs, ys) = forall (member eq ys) xs;
```
```   896
```
```   897 fun gen_eq_set eq (xs, ys) =
```
```   898   eq_list eq (xs, ys) orelse
```
```   899     (gen_subset eq (xs, ys) andalso gen_subset (eq o swap) (ys, xs));
```
```   900
```
```   901
```
```   902 (*removing an element from a list WITHOUT duplicates*)
```
```   903 fun (y :: ys) \ x = if x = y then ys else y :: (ys \ x)
```
```   904   | [] \ x = [];
```
```   905 fun ys \\ xs = foldl (op \) (ys,xs);
```
```   906
```
```   907
```
```   908 (*makes a list of the distinct members of the input; preserves order, takes
```
```   909   first of equal elements*)
```
```   910 fun distinct eq lst =
```
```   911   let
```
```   912     fun dist (rev_seen, []) = rev rev_seen
```
```   913       | dist (rev_seen, x :: xs) =
```
```   914           if member eq rev_seen x then dist (rev_seen, xs)
```
```   915           else dist (x :: rev_seen, xs);
```
```   916   in dist ([], lst) end;
```
```   917
```
```   918 (*returns a list containing all repeated elements exactly once; preserves
```
```   919   order, takes first of equal elements*)
```
```   920 fun duplicates eq lst =
```
```   921   let
```
```   922     fun dups (rev_dups, []) = rev rev_dups
```
```   923       | dups (rev_dups, x :: xs) =
```
```   924           if member eq rev_dups x orelse not (member eq xs x) then
```
```   925             dups (rev_dups, xs)
```
```   926           else dups (x :: rev_dups, xs);
```
```   927   in dups ([], lst) end;
```
```   928
```
```   929 fun has_duplicates eq =
```
```   930   let
```
```   931     fun dups [] = false
```
```   932       | dups (x :: xs) = member eq xs x orelse dups xs;
```
```   933   in dups end;
```
```   934
```
```   935
```
```   936
```
```   937 (** lists as multisets **)
```
```   938
```
```   939 fun remove1 _ _ [] = raise Empty
```
```   940   | remove1 eq y (x::xs) = if eq (y, x) then xs else x :: remove1 eq y xs;
```
```   941
```
```   942 fun submultiset _ ([], _)  = true
```
```   943   | submultiset eq (x :: xs, ys) = member eq ys x andalso submultiset eq (xs, remove1 eq x ys);
```
```   944
```
```   945
```
```   946
```
```   947 (** orders **)
```
```   948
```
```   949 fun is_equal EQUAL = true
```
```   950   | is_equal _ = false;
```
```   951
```
```   952 fun rev_order LESS = GREATER
```
```   953   | rev_order EQUAL = EQUAL
```
```   954   | rev_order GREATER = LESS;
```
```   955
```
```   956 (*assume rel is a linear strict order*)
```
```   957 fun make_ord rel (x, y) =
```
```   958   if rel (x, y) then LESS
```
```   959   else if rel (y, x) then GREATER
```
```   960   else EQUAL;
```
```   961
```
```   962 fun bool_ord (false, true) = LESS
```
```   963   | bool_ord (true, false) = GREATER
```
```   964   | bool_ord _ = EQUAL;
```
```   965
```
```   966 val int_ord = Int.compare;
```
```   967 val string_ord = String.compare;
```
```   968
```
```   969 fun fast_string_ord (s1, s2) =
```
```   970   (case int_ord (size s1, size s2) of EQUAL => string_ord (s1, s2) | ord => ord);
```
```   971
```
```   972 fun option_ord ord (SOME x, SOME y) = ord (x, y)
```
```   973   | option_ord _ (NONE, NONE) = EQUAL
```
```   974   | option_ord _ (NONE, SOME _) = LESS
```
```   975   | option_ord _ (SOME _, NONE) = GREATER;
```
```   976
```
```   977 (*lexicographic product*)
```
```   978 fun prod_ord a_ord b_ord ((x, y), (x', y')) =
```
```   979   (case a_ord (x, x') of EQUAL => b_ord (y, y') | ord => ord);
```
```   980
```
```   981 (*dictionary order -- in general NOT well-founded!*)
```
```   982 fun dict_ord elem_ord (x :: xs, y :: ys) =
```
```   983       (case elem_ord (x, y) of EQUAL => dict_ord elem_ord (xs, ys) | ord => ord)
```
```   984   | dict_ord _ ([], []) = EQUAL
```
```   985   | dict_ord _ ([], _ :: _) = LESS
```
```   986   | dict_ord _ (_ :: _, []) = GREATER;
```
```   987
```
```   988 (*lexicographic product of lists*)
```
```   989 fun list_ord elem_ord (xs, ys) =
```
```   990   (case int_ord (length xs, length ys) of EQUAL => dict_ord elem_ord (xs, ys) | ord => ord);
```
```   991
```
```   992
```
```   993 (* sorting *)
```
```   994
```
```   995 (*quicksort -- stable, i.e. does not reorder equal elements*)
```
```   996 fun quicksort unique ord =
```
```   997   let
```
```   998     fun qsort [] = []
```
```   999       | qsort (xs as [_]) = xs
```
```  1000       | qsort (xs as [x, y]) =
```
```  1001           (case ord (x, y) of
```
```  1002             LESS => xs
```
```  1003           | EQUAL => if unique then [x] else xs
```
```  1004           | GREATER => [y, x])
```
```  1005       | qsort xs =
```
```  1006           let val (lts, eqs, gts) = part (nth xs (length xs div 2)) xs
```
```  1007           in qsort lts @ eqs @ qsort gts end
```
```  1008     and part _ [] = ([], [], [])
```
```  1009       | part pivot (x :: xs) = add (ord (x, pivot)) x (part pivot xs)
```
```  1010     and add LESS x (lts, eqs, gts) = (x :: lts, eqs, gts)
```
```  1011       | add EQUAL x (lts, [], gts) = (lts, [x], gts)
```
```  1012       | add EQUAL x (res as (lts, eqs, gts)) = if unique then res else (lts, x :: eqs, gts)
```
```  1013       | add GREATER x (lts, eqs, gts) = (lts, eqs, x :: gts);
```
```  1014   in qsort end;
```
```  1015
```
```  1016 fun sort ord = quicksort false ord;
```
```  1017 fun sort_distinct ord = quicksort true ord;
```
```  1018
```
```  1019 val sort_strings = sort string_ord;
```
```  1020 fun sort_wrt sel xs = sort (string_ord o pairself sel) xs;
```
```  1021
```
```  1022
```
```  1023 (* items tagged by integer index *)
```
```  1024
```
```  1025 (*insert tags*)
```
```  1026 fun tag_list k [] = []
```
```  1027   | tag_list k (x :: xs) = (k:int, x) :: tag_list (k + 1) xs;
```
```  1028
```
```  1029 (*remove tags and suppress duplicates -- list is assumed sorted!*)
```
```  1030 fun untag_list [] = []
```
```  1031   | untag_list [(k: int, x)] = [x]
```
```  1032   | untag_list ((k, x) :: (rest as (k', x') :: _)) =
```
```  1033       if k = k' then untag_list rest
```
```  1034       else x :: untag_list rest;
```
```  1035
```
```  1036 (*return list elements in original order*)
```
```  1037 fun order_list list = untag_list (sort (int_ord o pairself fst) list);
```
```  1038
```
```  1039
```
```  1040
```
```  1041 (** random numbers **)
```
```  1042
```
```  1043 exception RANDOM;
```
```  1044
```
```  1045 fun rmod x y = x - y * Real.realFloor (x / y);
```
```  1046
```
```  1047 local
```
```  1048   val a = 16807.0;
```
```  1049   val m = 2147483647.0;
```
```  1050   val random_seed = ref 1.0;
```
```  1051 in
```
```  1052
```
```  1053 fun random () = CRITICAL (fn () =>
```
```  1054   let val r = rmod (a * ! random_seed) m
```
```  1055   in (random_seed := r; r) end);
```
```  1056
```
```  1057 end;
```
```  1058
```
```  1059 fun random_range l h =
```
```  1060   if h < l orelse l < 0 then raise RANDOM
```
```  1061   else l + Real.floor (rmod (random ()) (real (h - l + 1)));
```
```  1062
```
```  1063 fun one_of xs = nth xs (random_range 0 (length xs - 1));
```
```  1064
```
```  1065 fun frequency xs =
```
```  1066   let
```
```  1067     val sum = foldl op + (0, map fst xs);
```
```  1068     fun pick n ((k: int, x) :: xs) =
```
```  1069       if n <= k then x else pick (n - k) xs
```
```  1070   in pick (random_range 1 sum) xs end;
```
```  1071
```
```  1072
```
```  1073
```
```  1074 (** misc **)
```
```  1075
```
```  1076 fun divide_and_conquer decomp x =
```
```  1077   let val (ys, recomb) = decomp x
```
```  1078   in recomb (map (divide_and_conquer decomp) ys) end;
```
```  1079
```
```  1080
```
```  1081 (*Partition a list into buckets  [ bi, b(i+1), ..., bj ]
```
```  1082    putting x in bk if p(k)(x) holds.  Preserve order of elements if possible.*)
```
```  1083 fun partition_list p i j =
```
```  1084   let fun part k xs =
```
```  1085             if k>j then
```
```  1086               (case xs of [] => []
```
```  1087                          | _ => raise Fail "partition_list")
```
```  1088             else
```
```  1089             let val (ns, rest) = List.partition (p k) xs;
```
```  1090             in  ns :: part(k+1)rest  end
```
```  1091   in  part (i: int) end;
```
```  1092
```
```  1093 fun partition_eq (eq:'a * 'a -> bool) =
```
```  1094   let
```
```  1095     fun part [] = []
```
```  1096       | part (x :: ys) =
```
```  1097           let val (xs, xs') = List.partition (fn y => eq (x, y)) ys
```
```  1098           in (x::xs)::(part xs') end
```
```  1099   in part end;
```
```  1100
```
```  1101
```
```  1102
```
```  1103 (* generating identifiers *)
```
```  1104
```
```  1105 (** Freshly generated identifiers; supplied prefix MUST start with a letter **)
```
```  1106 local
```
```  1107 (*Maps 0-61 to A-Z, a-z, 0-9; exclude _ or ' to avoid clash with internal/unusual indentifiers*)
```
```  1108 fun gensym_char i =
```
```  1109   if i<26 then chr (ord "A" + i)
```
```  1110   else if i<52 then chr (ord "a" + i - 26)
```
```  1111   else chr (ord "0" + i - 52);
```
```  1112
```
```  1113 val char_vec = Vector.tabulate (62, gensym_char);
```
```  1114 fun newid n = implode (map (fn i => Vector.sub (char_vec, i)) (radixpand (62, n)));
```
```  1115
```
```  1116 val gensym_seed = ref (0: int);
```
```  1117
```
```  1118 in
```
```  1119   fun gensym pre = pre ^ newid (NAMED_CRITICAL "gensym" (fn () => inc gensym_seed));
```
```  1120 end;
```
```  1121
```
```  1122
```
```  1123 (* stamps and serial numbers *)
```
```  1124
```
```  1125 type stamp = unit ref;
```
```  1126 val stamp: unit -> stamp = ref;
```
```  1127
```
```  1128 type serial = int;
```
```  1129 val serial = Multithreading.serial;
```
```  1130 val serial_string = string_of_int o serial;
```
```  1131
```
```  1132
```
```  1133 (* generic objects *)
```
```  1134
```
```  1135 (*note that the builtin exception datatype may be extended by new
```
```  1136   constructors at any time*)
```
```  1137 structure Object = struct type T = exn end;
```
```  1138
```
```  1139 end;
```
```  1140
```
```  1141 structure BasicLibrary: BASIC_LIBRARY = Library;
```
```  1142 open BasicLibrary;
```