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