src/Pure/library.ML
author lcp
Wed Mar 15 10:56:39 1995 +0100 (1995-03-15 ago)
changeset 955 aa0c5f9daf5b
parent 544 c53386a5bcf1
child 1290 ee8f41456d28
permissions -rw-r--r--
Declares the function exit_use to behave like use but fail if
errors are detected. It can be used in all Makefiles except Pure, which will
write the exception handler explicitly ("exit" will have been declared
already).
wenzelm@41
     1
(*  Title:      Pure/library.ML
clasohm@0
     2
    ID:         $Id$
wenzelm@233
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
clasohm@0
     4
    Copyright   1992  University of Cambridge
clasohm@0
     5
wenzelm@233
     6
Basic library: functions, options, pairs, booleans, lists, integers,
wenzelm@233
     7
strings, lists as sets, association lists, generic tables, balanced trees,
wenzelm@233
     8
input / output, timing, filenames, misc functions.
clasohm@0
     9
*)
clasohm@0
    10
clasohm@0
    11
wenzelm@233
    12
(** functions **)
clasohm@0
    13
wenzelm@233
    14
(*handy combinators*)
wenzelm@233
    15
fun curry f x y = f (x, y);
wenzelm@233
    16
fun uncurry f (x, y) = f x y;
wenzelm@233
    17
fun I x = x;
wenzelm@233
    18
fun K x y = x;
clasohm@0
    19
wenzelm@380
    20
(*reverse apply*)
wenzelm@410
    21
infix |>;
wenzelm@410
    22
fun (x |> f) = f x;
wenzelm@380
    23
wenzelm@233
    24
(*combine two functions forming the union of their domains*)
wenzelm@233
    25
infix orelf;
wenzelm@233
    26
fun f orelf g = fn x => f x handle Match => g x;
clasohm@0
    27
wenzelm@233
    28
(*application of (infix) operator to its left or right argument*)
wenzelm@233
    29
fun apl (x, f) y = f (x, y);
wenzelm@233
    30
fun apr (f, y) x = f (x, y);
clasohm@0
    31
wenzelm@233
    32
(*functional for pairs*)
wenzelm@233
    33
fun pairself f (x, y) = (f x, f y);
clasohm@0
    34
wenzelm@233
    35
(*function exponentiation: f(...(f x)...) with n applications of f*)
wenzelm@233
    36
fun funpow n f x =
wenzelm@233
    37
  let fun rep (0, x) = x
wenzelm@233
    38
        | rep (n, x) = rep (n - 1, f x)
wenzelm@233
    39
  in rep (n, x) end;
wenzelm@160
    40
wenzelm@160
    41
wenzelm@160
    42
wenzelm@233
    43
(** options **)
clasohm@0
    44
clasohm@0
    45
datatype 'a option = None | Some of 'a;
clasohm@0
    46
clasohm@0
    47
exception OPTION of string;
clasohm@0
    48
clasohm@0
    49
fun the (Some x) = x
clasohm@0
    50
  | the None = raise OPTION "the";
clasohm@0
    51
wenzelm@255
    52
fun if_none None y = y
wenzelm@255
    53
  | if_none (Some x) _ = x;
wenzelm@255
    54
clasohm@0
    55
fun is_some (Some _) = true
clasohm@0
    56
  | is_some None = false;
clasohm@0
    57
clasohm@0
    58
fun is_none (Some _) = false
clasohm@0
    59
  | is_none None = true;
clasohm@0
    60
wenzelm@233
    61
fun apsome f (Some x) = Some (f x)
wenzelm@233
    62
  | apsome _ None = None;
clasohm@0
    63
wenzelm@233
    64
wenzelm@233
    65
wenzelm@233
    66
(** pairs **)
wenzelm@233
    67
wenzelm@233
    68
fun pair x y = (x, y);
wenzelm@233
    69
fun rpair x y = (y, x);
wenzelm@233
    70
wenzelm@233
    71
fun fst (x, y) = x;
wenzelm@233
    72
fun snd (x, y) = y;
wenzelm@233
    73
wenzelm@233
    74
fun eq_fst ((x1, _), (x2, _)) = x1 = x2;
wenzelm@233
    75
fun eq_snd ((_, y1), (_, y2)) = y1 = y2;
wenzelm@233
    76
wenzelm@233
    77
fun swap (x, y) = (y, x);
wenzelm@233
    78
wenzelm@233
    79
(*apply the function to a component of a pair*)
wenzelm@233
    80
fun apfst f (x, y) = (f x, y);
wenzelm@233
    81
fun apsnd f (x, y) = (x, f y);
wenzelm@233
    82
wenzelm@233
    83
wenzelm@233
    84
wenzelm@233
    85
(** booleans **)
wenzelm@233
    86
wenzelm@233
    87
(* equality *)
wenzelm@233
    88
wenzelm@233
    89
fun equal x y = x = y;
wenzelm@233
    90
fun not_equal x y = x <> y;
wenzelm@233
    91
wenzelm@233
    92
wenzelm@233
    93
(* operators for combining predicates *)
wenzelm@233
    94
wenzelm@233
    95
infix orf;
wenzelm@233
    96
fun p orf q = fn x => p x orelse q x;
wenzelm@233
    97
wenzelm@233
    98
infix andf;
wenzelm@233
    99
fun p andf q = fn x => p x andalso q x;
wenzelm@233
   100
wenzelm@233
   101
fun notf p x = not (p x);
clasohm@0
   102
wenzelm@233
   103
wenzelm@233
   104
(* predicates on lists *)
wenzelm@233
   105
wenzelm@233
   106
fun orl [] = false
wenzelm@233
   107
  | orl (x :: xs) = x orelse orl xs;
wenzelm@233
   108
wenzelm@233
   109
fun andl [] = true
wenzelm@233
   110
  | andl (x :: xs) = x andalso andl xs;
wenzelm@233
   111
wenzelm@233
   112
(*exists pred [x1, ..., xn] ===> pred x1 orelse ... orelse pred xn*)
wenzelm@233
   113
fun exists (pred: 'a -> bool) : 'a list -> bool =
wenzelm@233
   114
  let fun boolf [] = false
wenzelm@233
   115
        | boolf (x :: xs) = pred x orelse boolf xs
wenzelm@233
   116
  in boolf end;
wenzelm@233
   117
wenzelm@233
   118
(*forall pred [x1, ..., xn] ===> pred x1 andalso ... andalso pred xn*)
wenzelm@233
   119
fun forall (pred: 'a -> bool) : 'a list -> bool =
wenzelm@233
   120
  let fun boolf [] = true
wenzelm@233
   121
        | boolf (x :: xs) = pred x andalso boolf xs
wenzelm@233
   122
  in boolf end;
clasohm@0
   123
wenzelm@233
   124
wenzelm@380
   125
(* flags *)
wenzelm@380
   126
wenzelm@380
   127
fun set flag = (flag := true; true);
wenzelm@380
   128
fun reset flag = (flag := false; false);
wenzelm@380
   129
fun toggle flag = (flag := not (! flag); ! flag);
wenzelm@380
   130
wenzelm@380
   131
wenzelm@233
   132
wenzelm@233
   133
(** lists **)
wenzelm@233
   134
wenzelm@233
   135
exception LIST of string;
wenzelm@233
   136
wenzelm@233
   137
fun null [] = true
wenzelm@233
   138
  | null (_ :: _) = false;
wenzelm@233
   139
wenzelm@233
   140
fun hd [] = raise LIST "hd"
wenzelm@233
   141
  | hd (x :: _) = x;
wenzelm@233
   142
wenzelm@233
   143
fun tl [] = raise LIST "tl"
wenzelm@233
   144
  | tl (_ :: xs) = xs;
wenzelm@233
   145
wenzelm@233
   146
fun cons x xs = x :: xs;
wenzelm@233
   147
wenzelm@233
   148
wenzelm@233
   149
(* fold *)
wenzelm@233
   150
wenzelm@233
   151
(*the following versions of fold are designed to fit nicely with infixes*)
clasohm@0
   152
wenzelm@233
   153
(*  (op @) (e, [x1, ..., xn])  ===>  ((e @ x1) @ x2) ... @ xn
wenzelm@233
   154
    for operators that associate to the left (TAIL RECURSIVE)*)
wenzelm@233
   155
fun foldl (f: 'a * 'b -> 'a) : 'a * 'b list -> 'a =
wenzelm@233
   156
  let fun itl (e, [])  = e
wenzelm@233
   157
        | itl (e, a::l) = itl (f(e, a), l)
wenzelm@233
   158
  in  itl end;
wenzelm@233
   159
wenzelm@233
   160
(*  (op @) ([x1, ..., xn], e)  ===>   x1 @ (x2 ... @ (xn @ e))
wenzelm@233
   161
    for operators that associate to the right (not tail recursive)*)
wenzelm@233
   162
fun foldr f (l, e) =
wenzelm@233
   163
  let fun itr [] = e
wenzelm@233
   164
        | itr (a::l) = f(a, itr l)
wenzelm@233
   165
  in  itr l  end;
wenzelm@233
   166
wenzelm@233
   167
(*  (op @) [x1, ..., xn]  ===>   x1 @ (x2 ... @ (x[n-1] @ xn))
wenzelm@233
   168
    for n > 0, operators that associate to the right (not tail recursive)*)
wenzelm@233
   169
fun foldr1 f l =
wenzelm@233
   170
  let fun itr [x] = x                       (* FIXME [] case: elim warn (?) *)
wenzelm@233
   171
        | itr (x::l) = f(x, itr l)
wenzelm@233
   172
  in  itr l  end;
wenzelm@233
   173
wenzelm@233
   174
wenzelm@233
   175
(* basic list functions *)
wenzelm@233
   176
wenzelm@233
   177
(*length of a list, should unquestionably be a standard function*)
wenzelm@233
   178
local fun length1 (n, [])  = n   (*TAIL RECURSIVE*)
wenzelm@233
   179
        | length1 (n, x :: xs) = length1 (n + 1, xs)
wenzelm@233
   180
in  fun length l = length1 (0, l) end;
wenzelm@233
   181
wenzelm@233
   182
(*take the first n elements from a list*)
wenzelm@233
   183
fun take (n, []) = []
wenzelm@233
   184
  | take (n, x :: xs) =
wenzelm@233
   185
      if n > 0 then x :: take (n - 1, xs) else [];
wenzelm@233
   186
wenzelm@233
   187
(*drop the first n elements from a list*)
wenzelm@233
   188
fun drop (n, []) = []
wenzelm@233
   189
  | drop (n, x :: xs) =
wenzelm@233
   190
      if n > 0 then drop (n - 1, xs) else x :: xs;
clasohm@0
   191
wenzelm@233
   192
(*return nth element of a list, where 0 designates the first element;
wenzelm@233
   193
  raise EXCEPTION if list too short*)
wenzelm@233
   194
fun nth_elem NL =
wenzelm@233
   195
  (case drop NL of
wenzelm@233
   196
    [] => raise LIST "nth_elem"
wenzelm@233
   197
  | x :: _ => x);
wenzelm@233
   198
wenzelm@233
   199
(*last element of a list*)
wenzelm@233
   200
fun last_elem [] = raise LIST "last_elem"
wenzelm@233
   201
  | last_elem [x] = x
wenzelm@233
   202
  | last_elem (_ :: xs) = last_elem xs;
wenzelm@233
   203
wenzelm@233
   204
(*find the position of an element in a list*)
wenzelm@233
   205
fun find (x, ys) =
wenzelm@233
   206
  let fun f (y :: ys, i) = if x = y then i else f (ys, i + 1)
wenzelm@233
   207
        | f (_, _) = raise LIST "find"
wenzelm@233
   208
  in f (ys, 0) end;
wenzelm@233
   209
wenzelm@233
   210
(*flatten a list of lists to a list*)
wenzelm@233
   211
fun flat (ls: 'c list list) : 'c list = foldr (op @) (ls, []);
wenzelm@233
   212
wenzelm@233
   213
wenzelm@233
   214
(*like Lisp's MAPC -- seq proc [x1, ..., xn] evaluates
wenzelm@233
   215
  (proc x1; ...; proc xn) for side effects*)
wenzelm@233
   216
fun seq (proc: 'a -> unit) : 'a list -> unit =
wenzelm@233
   217
  let fun seqf [] = ()
wenzelm@233
   218
        | seqf (x :: xs) = (proc x; seqf xs)
wenzelm@233
   219
  in seqf end;
wenzelm@233
   220
wenzelm@233
   221
wenzelm@233
   222
(*separate s [x1, x2, ..., xn]  ===>  [x1, s, x2, s, ..., s, xn]*)
wenzelm@233
   223
fun separate s (x :: (xs as _ :: _)) = x :: s :: separate s xs
wenzelm@233
   224
  | separate _ xs = xs;
wenzelm@233
   225
wenzelm@233
   226
(*make the list [x, x, ..., x] of length n*)
wenzelm@233
   227
fun replicate n (x: 'a) : 'a list =
wenzelm@233
   228
  let fun rep (0, xs) = xs
wenzelm@233
   229
        | rep (n, xs) = rep (n - 1, x :: xs)
wenzelm@233
   230
  in
wenzelm@233
   231
    if n < 0 then raise LIST "replicate"
wenzelm@233
   232
    else rep (n, [])
wenzelm@233
   233
  end;
wenzelm@233
   234
wenzelm@233
   235
wenzelm@233
   236
(* filter *)
wenzelm@233
   237
wenzelm@233
   238
(*copy the list preserving elements that satisfy the predicate*)
wenzelm@233
   239
fun filter (pred: 'a->bool) : 'a list -> 'a list =
clasohm@0
   240
  let fun filt [] = []
wenzelm@233
   241
        | filt (x :: xs) = if pred x then x :: filt xs else filt xs
wenzelm@233
   242
  in filt end;
clasohm@0
   243
clasohm@0
   244
fun filter_out f = filter (not o f);
clasohm@0
   245
clasohm@0
   246
wenzelm@233
   247
fun mapfilter (f: 'a -> 'b option) ([]: 'a list) = [] : 'b list
wenzelm@233
   248
  | mapfilter f (x :: xs) =
wenzelm@233
   249
      (case f x of
wenzelm@233
   250
        None => mapfilter f xs
wenzelm@233
   251
      | Some y => y :: mapfilter f xs);
wenzelm@233
   252
wenzelm@233
   253
wenzelm@380
   254
fun find_first _ [] = None
wenzelm@380
   255
  | find_first pred (x :: xs) =
wenzelm@380
   256
      if pred x then Some x else find_first pred xs;
wenzelm@380
   257
wenzelm@380
   258
wenzelm@233
   259
(* lists of pairs *)
wenzelm@233
   260
wenzelm@380
   261
fun map2 _ ([], []) = []
wenzelm@380
   262
  | map2 f (x :: xs, y :: ys) = (f (x, y) :: map2 f (xs, ys))
wenzelm@380
   263
  | map2 _ _ = raise LIST "map2";
wenzelm@380
   264
wenzelm@380
   265
fun exists2 _ ([], []) = false
wenzelm@380
   266
  | exists2 pred (x :: xs, y :: ys) = pred (x, y) orelse exists2 pred (xs, ys)
wenzelm@380
   267
  | exists2 _ _ = raise LIST "exists2";
wenzelm@380
   268
wenzelm@380
   269
fun forall2 _ ([], []) = true
wenzelm@380
   270
  | forall2 pred (x :: xs, y :: ys) = pred (x, y) andalso forall2 pred (xs, ys)
wenzelm@380
   271
  | forall2 _ _ = raise LIST "forall2";
wenzelm@380
   272
wenzelm@233
   273
(*combine two lists forming a list of pairs:
wenzelm@233
   274
  [x1, ..., xn] ~~ [y1, ..., yn]  ===>  [(x1, y1), ..., (xn, yn)]*)
wenzelm@233
   275
infix ~~;
wenzelm@233
   276
fun [] ~~ [] = []
wenzelm@233
   277
  | (x :: xs) ~~ (y :: ys) = (x, y) :: (xs ~~ ys)
wenzelm@233
   278
  | _ ~~ _ = raise LIST "~~";
wenzelm@233
   279
wenzelm@233
   280
wenzelm@233
   281
(*inverse of ~~; the old 'split':
wenzelm@233
   282
  [(x1, y1), ..., (xn, yn)]  ===>  ([x1, ..., xn], [y1, ..., yn])*)
wenzelm@233
   283
fun split_list (l: ('a * 'b) list) = (map #1 l, map #2 l);
wenzelm@233
   284
wenzelm@233
   285
wenzelm@233
   286
(* prefixes, suffixes *)
wenzelm@233
   287
wenzelm@233
   288
infix prefix;
wenzelm@233
   289
fun [] prefix _ = true
wenzelm@233
   290
  | (x :: xs) prefix (y :: ys) = x = y andalso (xs prefix ys)
wenzelm@233
   291
  | _ prefix _ = false;
wenzelm@233
   292
wenzelm@233
   293
(* [x1, ..., xi, ..., xn]  --->  ([x1, ..., x(i-1)], [xi, ..., xn])
wenzelm@233
   294
   where xi is the first element that does not satisfy the predicate*)
wenzelm@233
   295
fun take_prefix (pred : 'a -> bool)  (xs: 'a list) : 'a list * 'a list =
wenzelm@233
   296
  let fun take (rxs, []) = (rev rxs, [])
wenzelm@255
   297
        | take (rxs, x :: xs) =
wenzelm@255
   298
            if  pred x  then  take(x :: rxs, xs)  else  (rev rxs, x :: xs)
wenzelm@233
   299
  in  take([], xs)  end;
wenzelm@233
   300
wenzelm@233
   301
(* [x1, ..., xi, ..., xn]  --->  ([x1, ..., xi], [x(i+1), ..., xn])
wenzelm@233
   302
   where xi is the last element that does not satisfy the predicate*)
wenzelm@233
   303
fun take_suffix _ [] = ([], [])
wenzelm@233
   304
  | take_suffix pred (x :: xs) =
wenzelm@233
   305
      (case take_suffix pred xs of
wenzelm@233
   306
        ([], sffx) => if pred x then ([], x :: sffx) else ([x], sffx)
wenzelm@233
   307
      | (prfx, sffx) => (x :: prfx, sffx));
wenzelm@233
   308
wenzelm@233
   309
wenzelm@233
   310
wenzelm@233
   311
(** integers **)
wenzelm@233
   312
wenzelm@233
   313
fun inc i = i := ! i + 1;
wenzelm@233
   314
fun dec i = i := ! i - 1;
wenzelm@233
   315
wenzelm@233
   316
wenzelm@233
   317
(* lists of integers *)
wenzelm@233
   318
wenzelm@233
   319
(*make the list [from, from + 1, ..., to]*)
wenzelm@233
   320
infix upto;
wenzelm@233
   321
fun from upto to =
wenzelm@233
   322
  if from > to then [] else from :: ((from + 1) upto to);
wenzelm@233
   323
wenzelm@233
   324
(*make the list [from, from - 1, ..., to]*)
wenzelm@233
   325
infix downto;
wenzelm@233
   326
fun from downto to =
wenzelm@233
   327
  if from < to then [] else from :: ((from - 1) downto to);
wenzelm@233
   328
wenzelm@233
   329
(*predicate: downto0 (is, n) <=> is = [n, n - 1, ..., 0]*)
wenzelm@233
   330
fun downto0 (i :: is, n) = i = n andalso downto0 (is, n - 1)
wenzelm@233
   331
  | downto0 ([], n) = n = ~1;
wenzelm@233
   332
wenzelm@233
   333
wenzelm@233
   334
(* operations on integer lists *)
clasohm@0
   335
wenzelm@233
   336
fun sum [] = 0
wenzelm@233
   337
  | sum (n :: ns) = n + sum ns;
wenzelm@233
   338
wenzelm@233
   339
fun max [m:int] = m
wenzelm@233
   340
  | max (m :: n :: ns) = if m > n then max (m :: ns) else max (n :: ns)
wenzelm@233
   341
  | max [] = raise LIST "max";
wenzelm@233
   342
wenzelm@233
   343
fun min [m:int] = m
wenzelm@233
   344
  | min (m :: n :: ns) = if m < n then min (m :: ns) else min (n :: ns)
wenzelm@233
   345
  | min [] = raise LIST "min";
wenzelm@233
   346
wenzelm@233
   347
wenzelm@233
   348
(* convert integers to strings *)
wenzelm@233
   349
wenzelm@233
   350
(*expand the number in the given base;
wenzelm@233
   351
  example: radixpand (2, 8) gives [1, 0, 0, 0]*)
wenzelm@233
   352
fun radixpand (base, num) : int list =
wenzelm@233
   353
  let
wenzelm@233
   354
    fun radix (n, tail) =
wenzelm@233
   355
      if n < base then n :: tail
wenzelm@233
   356
      else radix (n div base, (n mod base) :: tail)
wenzelm@233
   357
  in radix (num, []) end;
wenzelm@233
   358
wenzelm@233
   359
(*expands a number into a string of characters starting from "zerochar";
wenzelm@233
   360
  example: radixstring (2, "0", 8) gives "1000"*)
wenzelm@233
   361
fun radixstring (base, zerochar, num) =
wenzelm@233
   362
  let val offset = ord zerochar;
wenzelm@233
   363
      fun chrof n = chr (offset + n)
wenzelm@233
   364
  in implode (map chrof (radixpand (base, num))) end;
wenzelm@233
   365
wenzelm@233
   366
wenzelm@233
   367
fun string_of_int n =
wenzelm@233
   368
  if n < 0 then "~" ^ radixstring (10, "0", ~n) else radixstring (10, "0", n);
wenzelm@233
   369
wenzelm@233
   370
wenzelm@233
   371
wenzelm@233
   372
(** strings **)
wenzelm@233
   373
wenzelm@233
   374
fun is_letter ch =
wenzelm@233
   375
  ord "A" <= ord ch andalso ord ch <= ord "Z" orelse
wenzelm@233
   376
  ord "a" <= ord ch andalso ord ch <= ord "z";
wenzelm@233
   377
wenzelm@233
   378
fun is_digit ch =
wenzelm@233
   379
  ord "0" <= ord ch andalso ord ch <= ord "9";
wenzelm@233
   380
wenzelm@233
   381
(*letter or _ or prime (')*)
wenzelm@233
   382
fun is_quasi_letter "_" = true
wenzelm@233
   383
  | is_quasi_letter "'" = true
wenzelm@233
   384
  | is_quasi_letter ch = is_letter ch;
wenzelm@233
   385
lcp@512
   386
(*white space: blanks, tabs, newlines, formfeeds*)
wenzelm@233
   387
val is_blank : string -> bool =
lcp@512
   388
  fn " " => true | "\t" => true | "\n" => true | "\^L" => true | _ => false;
wenzelm@233
   389
wenzelm@233
   390
val is_letdig = is_quasi_letter orf is_digit;
wenzelm@233
   391
wenzelm@233
   392
wenzelm@233
   393
(*lower all chars of string*)
wenzelm@233
   394
val to_lower =
wenzelm@233
   395
  let
wenzelm@233
   396
    fun lower ch =
wenzelm@233
   397
      if ch >= "A" andalso ch <= "Z" then
wenzelm@233
   398
        chr (ord ch - ord "A" + ord "a")
wenzelm@233
   399
      else ch;
wenzelm@233
   400
  in implode o (map lower) o explode end;
wenzelm@233
   401
wenzelm@233
   402
lcp@512
   403
(*enclose in brackets*)
lcp@512
   404
fun enclose lpar rpar str = lpar ^ str ^ rpar;
wenzelm@255
   405
wenzelm@233
   406
(*simple quoting (does not escape special chars)*)
lcp@512
   407
val quote = enclose "\"" "\"";
wenzelm@233
   408
wenzelm@233
   409
(*space_implode "..." (explode "hello"); gives "h...e...l...l...o"*)
wenzelm@233
   410
fun space_implode a bs = implode (separate a bs);
wenzelm@233
   411
wenzelm@255
   412
val commas = space_implode ", ";
wenzelm@380
   413
val commas_quote = commas o map quote;
wenzelm@255
   414
wenzelm@233
   415
(*concatenate messages, one per line, into a string*)
wenzelm@255
   416
val cat_lines = space_implode "\n";
wenzelm@233
   417
wenzelm@233
   418
wenzelm@233
   419
wenzelm@233
   420
(** lists as sets **)
wenzelm@233
   421
wenzelm@233
   422
(*membership in a list*)
wenzelm@233
   423
infix mem;
wenzelm@233
   424
fun x mem [] = false
wenzelm@233
   425
  | x mem (y :: ys) = x = y orelse x mem ys;
clasohm@0
   426
clasohm@0
   427
(*generalized membership test*)
wenzelm@233
   428
fun gen_mem eq (x, []) = false
wenzelm@233
   429
  | gen_mem eq (x, y :: ys) = eq (x, y) orelse gen_mem eq (x, ys);
wenzelm@233
   430
wenzelm@233
   431
wenzelm@233
   432
(*insertion into list if not already there*)
wenzelm@233
   433
infix ins;
wenzelm@233
   434
fun x ins xs = if x mem xs then xs else x :: xs;
clasohm@0
   435
clasohm@0
   436
(*generalized insertion*)
wenzelm@233
   437
fun gen_ins eq (x, xs) = if gen_mem eq (x, xs) then xs else x :: xs;
wenzelm@233
   438
wenzelm@233
   439
wenzelm@233
   440
(*union of sets represented as lists: no repetitions*)
wenzelm@233
   441
infix union;
wenzelm@233
   442
fun xs union [] = xs
wenzelm@233
   443
  | [] union ys = ys
wenzelm@233
   444
  | (x :: xs) union ys = xs union (x ins ys);
clasohm@0
   445
clasohm@0
   446
(*generalized union*)
wenzelm@233
   447
fun gen_union eq (xs, []) = xs
wenzelm@233
   448
  | gen_union eq ([], ys) = ys
wenzelm@233
   449
  | gen_union eq (x :: xs, ys) = gen_union eq (xs, gen_ins eq (x, ys));
wenzelm@233
   450
wenzelm@233
   451
wenzelm@233
   452
(*intersection*)
wenzelm@233
   453
infix inter;
wenzelm@233
   454
fun [] inter ys = []
wenzelm@233
   455
  | (x :: xs) inter ys =
wenzelm@233
   456
      if x mem ys then x :: (xs inter ys) else xs inter ys;
wenzelm@233
   457
wenzelm@233
   458
wenzelm@233
   459
(*subset*)
wenzelm@233
   460
infix subset;
wenzelm@233
   461
fun [] subset ys = true
wenzelm@233
   462
  | (x :: xs) subset ys = x mem ys andalso xs subset ys;
wenzelm@233
   463
wenzelm@233
   464
fun gen_subset eq (xs, ys) = forall (fn x => gen_mem eq (x, ys)) xs;
wenzelm@233
   465
wenzelm@233
   466
wenzelm@265
   467
(*eq_set*)
wenzelm@265
   468
wenzelm@265
   469
fun eq_set (xs, ys) =
wenzelm@265
   470
  xs = ys orelse (xs subset ys andalso ys subset xs);
wenzelm@265
   471
wenzelm@265
   472
wenzelm@233
   473
(*removing an element from a list WITHOUT duplicates*)
wenzelm@233
   474
infix \;
wenzelm@233
   475
fun (y :: ys) \ x = if x = y then ys else y :: (ys \ x)
wenzelm@233
   476
  | [] \ x = [];
wenzelm@233
   477
wenzelm@233
   478
infix \\;
wenzelm@233
   479
val op \\ = foldl (op \);
clasohm@0
   480
wenzelm@233
   481
(*removing an element from a list -- possibly WITH duplicates*)
wenzelm@233
   482
fun gen_rem eq (xs, y) = filter_out (fn x => eq (x, y)) xs;
wenzelm@233
   483
wenzelm@233
   484
val gen_rems = foldl o gen_rem;
wenzelm@233
   485
wenzelm@233
   486
wenzelm@233
   487
(*makes a list of the distinct members of the input; preserves order, takes
wenzelm@233
   488
  first of equal elements*)
wenzelm@233
   489
fun gen_distinct eq lst =
wenzelm@233
   490
  let
wenzelm@233
   491
    val memb = gen_mem eq;
clasohm@0
   492
wenzelm@233
   493
    fun dist (rev_seen, []) = rev rev_seen
wenzelm@233
   494
      | dist (rev_seen, x :: xs) =
wenzelm@233
   495
          if memb (x, rev_seen) then dist (rev_seen, xs)
wenzelm@233
   496
          else dist (x :: rev_seen, xs);
wenzelm@233
   497
  in
wenzelm@233
   498
    dist ([], lst)
wenzelm@233
   499
  end;
wenzelm@233
   500
wenzelm@233
   501
val distinct = gen_distinct (op =);
wenzelm@233
   502
wenzelm@233
   503
wenzelm@233
   504
(*returns the tail beginning with the first repeated element, or []*)
wenzelm@233
   505
fun findrep [] = []
wenzelm@233
   506
  | findrep (x :: xs) = if x mem xs then x :: xs else findrep xs;
wenzelm@233
   507
wenzelm@233
   508
wenzelm@255
   509
(*returns a list containing all repeated elements exactly once; preserves
wenzelm@255
   510
  order, takes first of equal elements*)
wenzelm@255
   511
fun gen_duplicates eq lst =
wenzelm@255
   512
  let
wenzelm@255
   513
    val memb = gen_mem eq;
wenzelm@255
   514
wenzelm@255
   515
    fun dups (rev_dups, []) = rev rev_dups
wenzelm@255
   516
      | dups (rev_dups, x :: xs) =
wenzelm@255
   517
          if memb (x, rev_dups) orelse not (memb (x, xs)) then
wenzelm@255
   518
            dups (rev_dups, xs)
wenzelm@255
   519
          else dups (x :: rev_dups, xs);
wenzelm@255
   520
  in
wenzelm@255
   521
    dups ([], lst)
wenzelm@255
   522
  end;
wenzelm@255
   523
wenzelm@255
   524
val duplicates = gen_duplicates (op =);
wenzelm@255
   525
wenzelm@255
   526
wenzelm@233
   527
wenzelm@233
   528
(** association lists **)
clasohm@0
   529
wenzelm@233
   530
(*association list lookup*)
wenzelm@233
   531
fun assoc ([], key) = None
wenzelm@233
   532
  | assoc ((keyi, xi) :: pairs, key) =
wenzelm@233
   533
      if key = keyi then Some xi else assoc (pairs, key);
wenzelm@233
   534
wenzelm@233
   535
fun assocs ps x =
wenzelm@233
   536
  (case assoc (ps, x) of
wenzelm@233
   537
    None => []
wenzelm@233
   538
  | Some ys => ys);
wenzelm@233
   539
wenzelm@255
   540
(*two-fold association list lookup*)
wenzelm@255
   541
fun assoc2 (aal, (key1, key2)) =
wenzelm@255
   542
  (case assoc (aal, key1) of
wenzelm@255
   543
    Some al => assoc (al, key2)
wenzelm@255
   544
  | None => None);
wenzelm@255
   545
wenzelm@233
   546
(*generalized association list lookup*)
wenzelm@233
   547
fun gen_assoc eq ([], key) = None
wenzelm@233
   548
  | gen_assoc eq ((keyi, xi) :: pairs, key) =
wenzelm@233
   549
      if eq (key, keyi) then Some xi else gen_assoc eq (pairs, key);
wenzelm@233
   550
wenzelm@233
   551
(*association list update*)
wenzelm@233
   552
fun overwrite (al, p as (key, _)) =
wenzelm@233
   553
  let fun over ((q as (keyi, _)) :: pairs) =
wenzelm@233
   554
            if keyi = key then p :: pairs else q :: (over pairs)
wenzelm@233
   555
        | over [] = [p]
wenzelm@233
   556
  in over al end;
wenzelm@233
   557
wenzelm@233
   558
wenzelm@233
   559
wenzelm@233
   560
(** generic tables **)
clasohm@0
   561
wenzelm@233
   562
(*Tables are supposed to be 'efficient' encodings of lists of elements distinct
wenzelm@233
   563
  wrt. an equality "eq". The extend and merge operations below are optimized
wenzelm@233
   564
  for long-term space efficiency.*)
wenzelm@233
   565
wenzelm@233
   566
(*append (new) elements to a table*)
wenzelm@233
   567
fun generic_extend _ _ _ tab [] = tab
wenzelm@233
   568
  | generic_extend eq dest_tab mk_tab tab1 lst2 =
wenzelm@233
   569
      let
wenzelm@233
   570
        val lst1 = dest_tab tab1;
wenzelm@233
   571
        val new_lst2 = gen_rems eq (lst2, lst1);
wenzelm@233
   572
      in
wenzelm@233
   573
        if null new_lst2 then tab1
wenzelm@233
   574
        else mk_tab (lst1 @ new_lst2)
wenzelm@233
   575
      end;
clasohm@0
   576
wenzelm@233
   577
(*append (new) elements of 2nd table to 1st table*)
wenzelm@233
   578
fun generic_merge eq dest_tab mk_tab tab1 tab2 =
wenzelm@233
   579
  let
wenzelm@233
   580
    val lst1 = dest_tab tab1;
wenzelm@233
   581
    val lst2 = dest_tab tab2;
wenzelm@233
   582
    val new_lst2 = gen_rems eq (lst2, lst1);
wenzelm@233
   583
  in
wenzelm@233
   584
    if null new_lst2 then tab1
wenzelm@233
   585
    else if gen_subset eq (lst1, lst2) then tab2
wenzelm@233
   586
    else mk_tab (lst1 @ new_lst2)
wenzelm@233
   587
  end;
clasohm@0
   588
wenzelm@233
   589
wenzelm@233
   590
(*lists as tables*)
wenzelm@233
   591
val extend_list = generic_extend (op =) I I;
wenzelm@233
   592
val merge_lists = generic_merge (op =) I I;
wenzelm@233
   593
wenzelm@380
   594
fun merge_rev_lists xs [] = xs
wenzelm@380
   595
  | merge_rev_lists [] ys = ys
wenzelm@380
   596
  | merge_rev_lists xs (y :: ys) =
wenzelm@380
   597
      (if y mem xs then I else cons y) (merge_rev_lists xs ys);
wenzelm@380
   598
clasohm@0
   599
clasohm@0
   600
wenzelm@233
   601
(** balanced trees **)
wenzelm@233
   602
wenzelm@233
   603
exception Balance;      (*indicates non-positive argument to balancing fun*)
wenzelm@233
   604
wenzelm@233
   605
(*balanced folding; avoids deep nesting*)
wenzelm@233
   606
fun fold_bal f [x] = x
wenzelm@233
   607
  | fold_bal f [] = raise Balance
wenzelm@233
   608
  | fold_bal f xs =
wenzelm@233
   609
      let val k = length xs div 2
wenzelm@233
   610
      in  f (fold_bal f (take(k, xs)),
wenzelm@233
   611
             fold_bal f (drop(k, xs)))
wenzelm@233
   612
      end;
wenzelm@233
   613
wenzelm@233
   614
(*construct something of the form f(...g(...(x)...)) for balanced access*)
wenzelm@233
   615
fun access_bal (f, g, x) n i =
wenzelm@233
   616
  let fun acc n i =     (*1<=i<=n*)
wenzelm@233
   617
          if n=1 then x else
wenzelm@233
   618
          let val n2 = n div 2
wenzelm@233
   619
          in  if i<=n2 then f (acc n2 i)
wenzelm@233
   620
                       else g (acc (n-n2) (i-n2))
wenzelm@233
   621
          end
wenzelm@233
   622
  in  if 1<=i andalso i<=n then acc n i else raise Balance  end;
wenzelm@233
   623
wenzelm@233
   624
(*construct ALL such accesses; could try harder to share recursive calls!*)
wenzelm@233
   625
fun accesses_bal (f, g, x) n =
wenzelm@233
   626
  let fun acc n =
wenzelm@233
   627
          if n=1 then [x] else
wenzelm@233
   628
          let val n2 = n div 2
wenzelm@233
   629
              val acc2 = acc n2
wenzelm@233
   630
          in  if n-n2=n2 then map f acc2 @ map g acc2
wenzelm@233
   631
                         else map f acc2 @ map g (acc (n-n2)) end
wenzelm@233
   632
  in  if 1<=n then acc n else raise Balance  end;
wenzelm@233
   633
wenzelm@233
   634
wenzelm@233
   635
wenzelm@233
   636
(** input / output **)
wenzelm@233
   637
wenzelm@233
   638
fun prs s = output (std_out, s);
wenzelm@233
   639
fun writeln s = prs (s ^ "\n");
wenzelm@233
   640
wenzelm@233
   641
wenzelm@233
   642
(*print error message and abort to top level*)
wenzelm@233
   643
exception ERROR;
wenzelm@233
   644
fun error msg = (writeln msg; raise ERROR);
wenzelm@380
   645
fun sys_error msg = (writeln "*** SYSTEM ERROR ***"; error msg);
wenzelm@233
   646
wenzelm@233
   647
fun assert p msg = if p then () else error msg;
wenzelm@233
   648
fun deny p msg = if p then error msg else ();
wenzelm@233
   649
lcp@544
   650
(*Assert pred for every member of l, generating a message if pred fails*)
lcp@544
   651
fun assert_all pred l msg_fn = 
lcp@544
   652
  let fun asl [] = ()
lcp@544
   653
	| asl (x::xs) = if pred x then asl xs
lcp@544
   654
	                else error (msg_fn x)
lcp@544
   655
  in  asl l  end;
wenzelm@233
   656
wenzelm@233
   657
(* FIXME close file (?) *)
wenzelm@233
   658
(*for the "test" target in Makefiles -- signifies successful termination*)
wenzelm@233
   659
fun maketest msg =
wenzelm@233
   660
  (writeln msg; output (open_out "test", "Test examples ran successfully\n"));
wenzelm@233
   661
wenzelm@233
   662
wenzelm@233
   663
(*print a list surrounded by the brackets lpar and rpar, with comma separator
wenzelm@233
   664
  print nothing for empty list*)
wenzelm@233
   665
fun print_list (lpar, rpar, pre: 'a -> unit) (l : 'a list) =
wenzelm@233
   666
  let fun prec x = (prs ","; pre x)
wenzelm@233
   667
  in
wenzelm@233
   668
    (case l of
wenzelm@233
   669
      [] => ()
wenzelm@233
   670
    | x::l => (prs lpar; pre x; seq prec l; prs rpar))
wenzelm@233
   671
  end;
wenzelm@233
   672
wenzelm@233
   673
(*print a list of items separated by newlines*)
wenzelm@233
   674
fun print_list_ln (pre: 'a -> unit) : 'a list -> unit =
wenzelm@233
   675
  seq (fn x => (pre x; writeln ""));
wenzelm@233
   676
wenzelm@233
   677
wenzelm@233
   678
val print_int = prs o string_of_int;
wenzelm@233
   679
wenzelm@233
   680
wenzelm@233
   681
wenzelm@233
   682
(** timing **)
wenzelm@233
   683
wenzelm@233
   684
(*unconditional timing function*)
wenzelm@233
   685
val timeit = cond_timeit true;
wenzelm@233
   686
wenzelm@233
   687
(*timed application function*)
wenzelm@233
   688
fun timeap f x = timeit (fn () => f x);
wenzelm@233
   689
wenzelm@233
   690
(*timed "use" function, printing filenames*)
wenzelm@233
   691
fun time_use fname = timeit (fn () =>
wenzelm@233
   692
  (writeln ("\n**** Starting " ^ fname ^ " ****"); use fname;
wenzelm@233
   693
   writeln ("\n**** Finished " ^ fname ^ " ****")));
wenzelm@233
   694
lcp@955
   695
(*For Makefiles: use the file, but exit with error code if errors found.*)
lcp@955
   696
fun exit_use fname = use fname handle _ => exit 1;
wenzelm@233
   697
wenzelm@233
   698
wenzelm@233
   699
(** filenames **)
wenzelm@233
   700
wenzelm@233
   701
(*convert UNIX filename of the form "path/file" to "path/" and "file";
wenzelm@233
   702
  if filename contains no slash, then it returns "" and "file"*)
wenzelm@233
   703
val split_filename =
wenzelm@233
   704
  (pairself implode) o take_suffix (not_equal "/") o explode;
wenzelm@233
   705
wenzelm@233
   706
val base_name = #2 o split_filename;
wenzelm@233
   707
wenzelm@233
   708
(*merge splitted filename (path and file);
wenzelm@233
   709
  if path does not end with one a slash is appended*)
wenzelm@233
   710
fun tack_on "" name = name
wenzelm@233
   711
  | tack_on path name =
wenzelm@233
   712
      if last_elem (explode path) = "/" then path ^ name
wenzelm@233
   713
      else path ^ "/" ^ name;
wenzelm@233
   714
wenzelm@233
   715
(*remove the extension of a filename, i.e. the part after the last '.'*)
wenzelm@233
   716
val remove_ext = implode o #1 o take_suffix (not_equal ".") o explode;
wenzelm@233
   717
wenzelm@233
   718
wenzelm@233
   719
wenzelm@233
   720
(** misc functions **)
wenzelm@233
   721
wenzelm@233
   722
(*use the keyfun to make a list of (x, key) pairs*)
clasohm@0
   723
fun make_keylist (keyfun: 'a->'b) : 'a list -> ('a * 'b) list =
wenzelm@233
   724
  let fun keypair x = (x, keyfun x)
wenzelm@233
   725
  in map keypair end;
clasohm@0
   726
wenzelm@233
   727
(*given a list of (x, key) pairs and a searchkey
clasohm@0
   728
  return the list of xs from each pair whose key equals searchkey*)
clasohm@0
   729
fun keyfilter [] searchkey = []
wenzelm@233
   730
  | keyfilter ((x, key) :: pairs) searchkey =
wenzelm@233
   731
      if key = searchkey then x :: keyfilter pairs searchkey
wenzelm@233
   732
      else keyfilter pairs searchkey;
clasohm@0
   733
clasohm@0
   734
clasohm@0
   735
(*Partition list into elements that satisfy predicate and those that don't.
wenzelm@233
   736
  Preserves order of elements in both lists.*)
clasohm@0
   737
fun partition (pred: 'a->bool) (ys: 'a list) : ('a list * 'a list) =
clasohm@0
   738
    let fun part ([], answer) = answer
wenzelm@233
   739
          | part (x::xs, (ys, ns)) = if pred(x)
wenzelm@233
   740
            then  part (xs, (x::ys, ns))
wenzelm@233
   741
            else  part (xs, (ys, x::ns))
wenzelm@233
   742
    in  part (rev ys, ([], []))  end;
clasohm@0
   743
clasohm@0
   744
clasohm@0
   745
fun partition_eq (eq:'a * 'a -> bool) =
clasohm@0
   746
    let fun part [] = []
wenzelm@233
   747
          | part (x::ys) = let val (xs, xs') = partition (apl(x, eq)) ys
wenzelm@233
   748
                           in (x::xs)::(part xs') end
clasohm@0
   749
    in part end;
clasohm@0
   750
clasohm@0
   751
wenzelm@233
   752
(*Partition a list into buckets  [ bi, b(i+1), ..., bj ]
clasohm@0
   753
   putting x in bk if p(k)(x) holds.  Preserve order of elements if possible.*)
clasohm@0
   754
fun partition_list p i j =
wenzelm@233
   755
  let fun part k xs =
wenzelm@233
   756
            if k>j then
clasohm@0
   757
              (case xs of [] => []
clasohm@0
   758
                         | _ => raise LIST "partition_list")
clasohm@0
   759
            else
wenzelm@233
   760
            let val (ns, rest) = partition (p k) xs;
wenzelm@233
   761
            in  ns :: part(k+1)rest  end
clasohm@0
   762
  in  part i end;
clasohm@0
   763
clasohm@0
   764
wenzelm@233
   765
(* sorting *)
wenzelm@233
   766
wenzelm@233
   767
(*insertion sort; stable (does not reorder equal elements)
wenzelm@233
   768
  'less' is less-than test on type 'a*)
wenzelm@233
   769
fun sort (less: 'a*'a -> bool) =
clasohm@0
   770
  let fun insert (x, []) = [x]
wenzelm@233
   771
        | insert (x, y::ys) =
wenzelm@233
   772
              if less(y, x) then y :: insert (x, ys) else x::y::ys;
clasohm@0
   773
      fun sort1 [] = []
clasohm@0
   774
        | sort1 (x::xs) = insert (x, sort1 xs)
clasohm@0
   775
  in  sort1  end;
clasohm@0
   776
wenzelm@41
   777
(*sort strings*)
wenzelm@41
   778
val sort_strings = sort (op <= : string * string -> bool);
wenzelm@41
   779
wenzelm@41
   780
wenzelm@233
   781
(* transitive closure (not Warshall's algorithm) *)
clasohm@0
   782
wenzelm@233
   783
fun transitive_closure [] = []
wenzelm@233
   784
  | transitive_closure ((x, ys)::ps) =
wenzelm@233
   785
      let val qs = transitive_closure ps
wenzelm@233
   786
          val zs = foldl (fn (zs, y) => assocs qs y union zs) (ys, ys)
wenzelm@233
   787
          fun step(u, us) = (u, if x mem us then zs union us else us)
wenzelm@233
   788
      in (x, zs) :: map step qs end;
clasohm@0
   789
clasohm@0
   790
wenzelm@233
   791
(* generating identifiers *)
clasohm@0
   792
clasohm@0
   793
local
wenzelm@233
   794
  val a = ord "a" and z = ord "z" and A = ord "A" and Z = ord "Z"
wenzelm@233
   795
  and k0 = ord "0" and k9 = ord "9"
clasohm@0
   796
in
clasohm@0
   797
clasohm@0
   798
(*Increment a list of letters like a reversed base 26 number.
wenzelm@233
   799
  If head is "z", bumps chars in tail.
clasohm@0
   800
  Digits are incremented as if they were integers.
clasohm@0
   801
  "_" and "'" are not changed.
wenzelm@233
   802
  For making variants of identifiers.*)
clasohm@0
   803
clasohm@0
   804
fun bump_int_list(c::cs) = if c="9" then "0" :: bump_int_list cs else
wenzelm@233
   805
        if k0 <= ord(c) andalso ord(c) < k9 then chr(ord(c)+1) :: cs
wenzelm@233
   806
        else "1" :: c :: cs
clasohm@0
   807
  | bump_int_list([]) = error("bump_int_list: not an identifier");
clasohm@0
   808
wenzelm@233
   809
fun bump_list([], d) = [d]
wenzelm@233
   810
  | bump_list(["'"], d) = [d, "'"]
wenzelm@233
   811
  | bump_list("z"::cs, _) = "a" :: bump_list(cs, "a")
wenzelm@233
   812
  | bump_list("Z"::cs, _) = "A" :: bump_list(cs, "A")
wenzelm@233
   813
  | bump_list("9"::cs, _) = "0" :: bump_int_list cs
wenzelm@233
   814
  | bump_list(c::cs, _) = let val k = ord(c)
wenzelm@233
   815
        in if (a <= k andalso k < z) orelse (A <= k andalso k < Z) orelse
wenzelm@233
   816
              (k0 <= k andalso k < k9) then chr(k+1) :: cs else
wenzelm@233
   817
           if c="'" orelse c="_" then c :: bump_list(cs, "") else
wenzelm@233
   818
                error("bump_list: not legal in identifier: " ^
wenzelm@233
   819
                        implode(rev(c::cs)))
wenzelm@233
   820
        end;
clasohm@0
   821
clasohm@0
   822
end;
clasohm@0
   823
wenzelm@233
   824
fun bump_string s : string = implode (rev (bump_list(rev(explode s), "")));
wenzelm@41
   825
wenzelm@41
   826
wenzelm@233
   827
(* lexical scanning *)
clasohm@0
   828
wenzelm@233
   829
(*scan a list of characters into "words" composed of "letters" (recognized by
wenzelm@233
   830
  is_let) and separated by any number of non-"letters"*)
wenzelm@233
   831
fun scanwords is_let cs =
clasohm@0
   832
  let fun scan1 [] = []
wenzelm@233
   833
        | scan1 cs =
wenzelm@233
   834
            let val (lets, rest) = take_prefix is_let cs
wenzelm@233
   835
            in implode lets :: scanwords is_let rest end;
wenzelm@233
   836
  in scan1 (#2 (take_prefix (not o is_let) cs)) end;
clasohm@24
   837