wenzelm@41: (* Title: Pure/library.ML clasohm@0: ID: $Id$ wenzelm@233: Author: Lawrence C Paulson, Cambridge University Computer Laboratory clasohm@0: Copyright 1992 University of Cambridge clasohm@0: wenzelm@233: Basic library: functions, options, pairs, booleans, lists, integers, wenzelm@4212: strings, lists as sets, association lists, generic tables, balanced wenzelm@4212: trees, orders, diagnostics, timing, misc functions. clasohm@0: *) clasohm@0: wenzelm@4212: infix |> ~~ \ \\ ins ins_string ins_int orf andf prefix upto downto wenzelm@4212: mem mem_int mem_string union union_int union_string inter inter_int wenzelm@4212: inter_string subset subset_int subset_string; clasohm@1364: clasohm@1364: clasohm@1364: structure Library = clasohm@1364: struct clasohm@0: wenzelm@233: (** functions **) clasohm@0: wenzelm@233: (*handy combinators*) wenzelm@233: fun curry f x y = f (x, y); wenzelm@233: fun uncurry f (x, y) = f x y; wenzelm@233: fun I x = x; wenzelm@233: fun K x y = x; clasohm@0: wenzelm@380: (*reverse apply*) wenzelm@410: fun (x |> f) = f x; wenzelm@380: wenzelm@233: (*application of (infix) operator to its left or right argument*) wenzelm@233: fun apl (x, f) y = f (x, y); wenzelm@233: fun apr (f, y) x = f (x, y); clasohm@0: wenzelm@233: (*function exponentiation: f(...(f x)...) with n applications of f*) wenzelm@233: fun funpow n f x = wenzelm@233: let fun rep (0, x) = x wenzelm@233: | rep (n, x) = rep (n - 1, f x) wenzelm@233: in rep (n, x) end; wenzelm@160: wenzelm@160: wenzelm@160: wenzelm@2471: (** stamps **) wenzelm@2471: wenzelm@2471: type stamp = unit ref; wenzelm@2471: val stamp: unit -> stamp = ref; wenzelm@2471: wenzelm@2471: wenzelm@2471: wenzelm@233: (** options **) clasohm@0: clasohm@0: datatype 'a option = None | Some of 'a; clasohm@0: wenzelm@4139: exception OPTION; clasohm@0: clasohm@0: fun the (Some x) = x wenzelm@4139: | the None = raise OPTION; clasohm@0: wenzelm@4212: (*strict!*) wenzelm@255: fun if_none None y = y wenzelm@255: | if_none (Some x) _ = x; wenzelm@255: clasohm@0: fun is_some (Some _) = true clasohm@0: | is_some None = false; clasohm@0: clasohm@0: fun is_none (Some _) = false clasohm@0: | is_none None = true; clasohm@0: wenzelm@233: fun apsome f (Some x) = Some (f x) wenzelm@233: | apsome _ None = None; clasohm@0: wenzelm@4139: (*handle partial functions*) wenzelm@4181: fun can f x = (f x; true) handle _ => false; wenzelm@4139: fun try f x = Some (f x) handle _ => None; wenzelm@4139: wenzelm@4139: wenzelm@4139: wenzelm@233: (** pairs **) wenzelm@233: wenzelm@233: fun pair x y = (x, y); wenzelm@233: fun rpair x y = (y, x); wenzelm@233: wenzelm@233: fun fst (x, y) = x; wenzelm@233: fun snd (x, y) = y; wenzelm@233: wenzelm@233: fun eq_fst ((x1, _), (x2, _)) = x1 = x2; wenzelm@233: fun eq_snd ((_, y1), (_, y2)) = y1 = y2; wenzelm@233: wenzelm@233: fun swap (x, y) = (y, x); wenzelm@233: wenzelm@4212: (*apply function to components*) wenzelm@233: fun apfst f (x, y) = (f x, y); wenzelm@233: fun apsnd f (x, y) = (x, f y); wenzelm@4212: fun pairself f (x, y) = (f x, f y); wenzelm@233: wenzelm@233: wenzelm@233: wenzelm@233: (** booleans **) wenzelm@233: wenzelm@233: (* equality *) wenzelm@233: wenzelm@233: fun equal x y = x = y; wenzelm@233: fun not_equal x y = x <> y; wenzelm@233: wenzelm@233: wenzelm@233: (* operators for combining predicates *) wenzelm@233: paulson@2175: fun (p orf q) = fn x => p x orelse q x; paulson@2175: fun (p andf q) = fn x => p x andalso q x; wenzelm@233: wenzelm@233: wenzelm@233: (* predicates on lists *) wenzelm@233: wenzelm@233: (*exists pred [x1, ..., xn] ===> pred x1 orelse ... orelse pred xn*) wenzelm@233: fun exists (pred: 'a -> bool) : 'a list -> bool = wenzelm@233: let fun boolf [] = false wenzelm@233: | boolf (x :: xs) = pred x orelse boolf xs wenzelm@233: in boolf end; wenzelm@233: wenzelm@233: (*forall pred [x1, ..., xn] ===> pred x1 andalso ... andalso pred xn*) wenzelm@233: fun forall (pred: 'a -> bool) : 'a list -> bool = wenzelm@233: let fun boolf [] = true wenzelm@233: | boolf (x :: xs) = pred x andalso boolf xs wenzelm@233: in boolf end; clasohm@0: wenzelm@233: wenzelm@380: (* flags *) wenzelm@380: wenzelm@380: fun set flag = (flag := true; true); wenzelm@380: fun reset flag = (flag := false; false); wenzelm@380: fun toggle flag = (flag := not (! flag); ! flag); wenzelm@380: wenzelm@4212: (*temporarily set flag, handling errors*) wenzelm@2978: fun setmp flag value f x = wenzelm@2958: let wenzelm@2958: val orig_value = ! flag; wenzelm@2958: fun return y = (flag := orig_value; y); wenzelm@2958: in wenzelm@2958: flag := value; wenzelm@2958: return (f x handle exn => (return (); raise exn)) wenzelm@2958: end; wenzelm@2958: wenzelm@380: wenzelm@233: wenzelm@233: (** lists **) wenzelm@233: wenzelm@233: exception LIST of string; wenzelm@233: wenzelm@233: fun null [] = true wenzelm@233: | null (_ :: _) = false; wenzelm@233: wenzelm@233: fun hd [] = raise LIST "hd" wenzelm@233: | hd (x :: _) = x; wenzelm@233: wenzelm@233: fun tl [] = raise LIST "tl" wenzelm@233: | tl (_ :: xs) = xs; wenzelm@233: wenzelm@233: fun cons x xs = x :: xs; wenzelm@233: wenzelm@233: wenzelm@233: (* fold *) wenzelm@233: wenzelm@233: (*the following versions of fold are designed to fit nicely with infixes*) clasohm@0: wenzelm@233: (* (op @) (e, [x1, ..., xn]) ===> ((e @ x1) @ x2) ... @ xn wenzelm@233: for operators that associate to the left (TAIL RECURSIVE)*) wenzelm@233: fun foldl (f: 'a * 'b -> 'a) : 'a * 'b list -> 'a = wenzelm@233: let fun itl (e, []) = e wenzelm@233: | itl (e, a::l) = itl (f(e, a), l) wenzelm@233: in itl end; wenzelm@233: wenzelm@233: (* (op @) ([x1, ..., xn], e) ===> x1 @ (x2 ... @ (xn @ e)) wenzelm@233: for operators that associate to the right (not tail recursive)*) wenzelm@233: fun foldr f (l, e) = wenzelm@233: let fun itr [] = e wenzelm@233: | itr (a::l) = f(a, itr l) wenzelm@233: in itr l end; wenzelm@233: wenzelm@233: (* (op @) [x1, ..., xn] ===> x1 @ (x2 ... @ (x[n-1] @ xn)) wenzelm@233: for n > 0, operators that associate to the right (not tail recursive)*) wenzelm@233: fun foldr1 f l = wenzelm@4181: let fun itr [x] = x wenzelm@233: | itr (x::l) = f(x, itr l) wenzelm@233: in itr l end; wenzelm@233: wenzelm@233: wenzelm@233: (* basic list functions *) wenzelm@233: wenzelm@233: (*length of a list, should unquestionably be a standard function*) wenzelm@233: local fun length1 (n, []) = n (*TAIL RECURSIVE*) wenzelm@233: | length1 (n, x :: xs) = length1 (n + 1, xs) wenzelm@233: in fun length l = length1 (0, l) end; wenzelm@233: wenzelm@233: (*take the first n elements from a list*) wenzelm@233: fun take (n, []) = [] wenzelm@233: | take (n, x :: xs) = wenzelm@233: if n > 0 then x :: take (n - 1, xs) else []; wenzelm@233: wenzelm@233: (*drop the first n elements from a list*) wenzelm@233: fun drop (n, []) = [] wenzelm@233: | drop (n, x :: xs) = wenzelm@233: if n > 0 then drop (n - 1, xs) else x :: xs; clasohm@0: wenzelm@233: (*return nth element of a list, where 0 designates the first element; wenzelm@233: raise EXCEPTION if list too short*) wenzelm@233: fun nth_elem NL = wenzelm@233: (case drop NL of wenzelm@233: [] => raise LIST "nth_elem" wenzelm@233: | x :: _ => x); wenzelm@233: wenzelm@233: (*last element of a list*) wenzelm@233: fun last_elem [] = raise LIST "last_elem" wenzelm@233: | last_elem [x] = x wenzelm@233: | last_elem (_ :: xs) = last_elem xs; wenzelm@233: wenzelm@3762: (*rear decomposition*) wenzelm@3762: fun split_last [] = raise LIST "split_last" wenzelm@3762: | split_last [x] = ([], x) wenzelm@3762: | split_last (x :: xs) = apfst (cons x) (split_last xs); wenzelm@3762: wenzelm@4212: (*find the position of an element in a list*) wenzelm@4212: fun find_index pred = wenzelm@4212: let fun find _ [] = ~1 wenzelm@4212: | find n (x :: xs) = if pred x then n else find (n + 1) xs; wenzelm@4212: in find 0 end; wenzelm@3762: wenzelm@4224: fun find_index_eq x = find_index (equal x); wenzelm@4212: wenzelm@4212: (*find first element satisfying predicate*) wenzelm@4212: fun find_first _ [] = None wenzelm@4212: | find_first pred (x :: xs) = wenzelm@4212: if pred x then Some x else find_first pred xs; wenzelm@233: wenzelm@233: (*flatten a list of lists to a list*) wenzelm@233: fun flat (ls: 'c list list) : 'c list = foldr (op @) (ls, []); wenzelm@233: wenzelm@233: (*like Lisp's MAPC -- seq proc [x1, ..., xn] evaluates wenzelm@233: (proc x1; ...; proc xn) for side effects*) wenzelm@233: fun seq (proc: 'a -> unit) : 'a list -> unit = wenzelm@233: let fun seqf [] = () wenzelm@233: | seqf (x :: xs) = (proc x; seqf xs) wenzelm@233: in seqf end; wenzelm@233: wenzelm@233: (*separate s [x1, x2, ..., xn] ===> [x1, s, x2, s, ..., s, xn]*) wenzelm@233: fun separate s (x :: (xs as _ :: _)) = x :: s :: separate s xs wenzelm@233: | separate _ xs = xs; wenzelm@233: wenzelm@233: (*make the list [x, x, ..., x] of length n*) wenzelm@233: fun replicate n (x: 'a) : 'a list = wenzelm@233: let fun rep (0, xs) = xs wenzelm@233: | rep (n, xs) = rep (n - 1, x :: xs) wenzelm@233: in wenzelm@233: if n < 0 then raise LIST "replicate" wenzelm@233: else rep (n, []) wenzelm@233: end; wenzelm@233: wenzelm@4248: (*multiply [a, b, c, ...] * [xs, ys, zs, ...]*) wenzelm@4248: fun multiply ([], _) = [] wenzelm@4248: | multiply (x :: xs, yss) = map (cons x) yss @ multiply (xs, yss); wenzelm@4248: wenzelm@233: wenzelm@233: (* filter *) wenzelm@233: wenzelm@233: (*copy the list preserving elements that satisfy the predicate*) wenzelm@233: fun filter (pred: 'a->bool) : 'a list -> 'a list = clasohm@0: let fun filt [] = [] wenzelm@233: | filt (x :: xs) = if pred x then x :: filt xs else filt xs wenzelm@233: in filt end; clasohm@0: clasohm@0: fun filter_out f = filter (not o f); clasohm@0: wenzelm@233: fun mapfilter (f: 'a -> 'b option) ([]: 'a list) = [] : 'b list wenzelm@233: | mapfilter f (x :: xs) = wenzelm@233: (case f x of wenzelm@233: None => mapfilter f xs wenzelm@233: | Some y => y :: mapfilter f xs); wenzelm@233: wenzelm@233: wenzelm@233: (* lists of pairs *) wenzelm@233: wenzelm@380: fun map2 _ ([], []) = [] wenzelm@380: | map2 f (x :: xs, y :: ys) = (f (x, y) :: map2 f (xs, ys)) wenzelm@380: | map2 _ _ = raise LIST "map2"; wenzelm@380: wenzelm@380: fun exists2 _ ([], []) = false wenzelm@380: | exists2 pred (x :: xs, y :: ys) = pred (x, y) orelse exists2 pred (xs, ys) wenzelm@380: | exists2 _ _ = raise LIST "exists2"; wenzelm@380: wenzelm@380: fun forall2 _ ([], []) = true wenzelm@380: | forall2 pred (x :: xs, y :: ys) = pred (x, y) andalso forall2 pred (xs, ys) wenzelm@380: | forall2 _ _ = raise LIST "forall2"; wenzelm@380: wenzelm@233: (*combine two lists forming a list of pairs: wenzelm@233: [x1, ..., xn] ~~ [y1, ..., yn] ===> [(x1, y1), ..., (xn, yn)]*) wenzelm@233: fun [] ~~ [] = [] wenzelm@233: | (x :: xs) ~~ (y :: ys) = (x, y) :: (xs ~~ ys) wenzelm@233: | _ ~~ _ = raise LIST "~~"; wenzelm@233: wenzelm@233: (*inverse of ~~; the old 'split': wenzelm@233: [(x1, y1), ..., (xn, yn)] ===> ([x1, ..., xn], [y1, ..., yn])*) wenzelm@233: fun split_list (l: ('a * 'b) list) = (map #1 l, map #2 l); wenzelm@233: wenzelm@233: wenzelm@233: (* prefixes, suffixes *) wenzelm@233: wenzelm@233: fun [] prefix _ = true wenzelm@233: | (x :: xs) prefix (y :: ys) = x = y andalso (xs prefix ys) wenzelm@233: | _ prefix _ = false; wenzelm@233: wenzelm@233: (* [x1, ..., xi, ..., xn] ---> ([x1, ..., x(i-1)], [xi, ..., xn]) wenzelm@233: where xi is the first element that does not satisfy the predicate*) wenzelm@233: fun take_prefix (pred : 'a -> bool) (xs: 'a list) : 'a list * 'a list = wenzelm@233: let fun take (rxs, []) = (rev rxs, []) wenzelm@255: | take (rxs, x :: xs) = wenzelm@255: if pred x then take(x :: rxs, xs) else (rev rxs, x :: xs) wenzelm@233: in take([], xs) end; wenzelm@233: wenzelm@233: (* [x1, ..., xi, ..., xn] ---> ([x1, ..., xi], [x(i+1), ..., xn]) wenzelm@233: where xi is the last element that does not satisfy the predicate*) wenzelm@233: fun take_suffix _ [] = ([], []) wenzelm@233: | take_suffix pred (x :: xs) = wenzelm@233: (case take_suffix pred xs of wenzelm@233: ([], sffx) => if pred x then ([], x :: sffx) else ([x], sffx) wenzelm@233: | (prfx, sffx) => (x :: prfx, sffx)); wenzelm@233: wenzelm@233: wenzelm@233: wenzelm@233: (** integers **) wenzelm@233: wenzelm@2958: fun inc i = (i := ! i + 1; ! i); wenzelm@2958: fun dec i = (i := ! i - 1; ! i); wenzelm@233: wenzelm@233: wenzelm@233: (* lists of integers *) wenzelm@233: wenzelm@233: (*make the list [from, from + 1, ..., to]*) paulson@2175: fun (from upto to) = wenzelm@233: if from > to then [] else from :: ((from + 1) upto to); wenzelm@233: wenzelm@233: (*make the list [from, from - 1, ..., to]*) paulson@2175: fun (from downto to) = wenzelm@233: if from < to then [] else from :: ((from - 1) downto to); wenzelm@233: wenzelm@233: (*predicate: downto0 (is, n) <=> is = [n, n - 1, ..., 0]*) wenzelm@233: fun downto0 (i :: is, n) = i = n andalso downto0 (is, n - 1) wenzelm@233: | downto0 ([], n) = n = ~1; wenzelm@233: wenzelm@233: wenzelm@233: (* convert integers to strings *) wenzelm@233: wenzelm@233: (*expand the number in the given base; wenzelm@233: example: radixpand (2, 8) gives [1, 0, 0, 0]*) wenzelm@233: fun radixpand (base, num) : int list = wenzelm@233: let wenzelm@233: fun radix (n, tail) = wenzelm@233: if n < base then n :: tail wenzelm@233: else radix (n div base, (n mod base) :: tail) wenzelm@233: in radix (num, []) end; wenzelm@233: wenzelm@233: (*expands a number into a string of characters starting from "zerochar"; wenzelm@233: example: radixstring (2, "0", 8) gives "1000"*) wenzelm@233: fun radixstring (base, zerochar, num) = wenzelm@233: let val offset = ord zerochar; wenzelm@233: fun chrof n = chr (offset + n) wenzelm@233: in implode (map chrof (radixpand (base, num))) end; wenzelm@233: wenzelm@233: paulson@3407: val string_of_int = Int.toString; wenzelm@233: paulson@3407: fun string_of_indexname (a,0) = a paulson@3407: | string_of_indexname (a,i) = a ^ "_" ^ Int.toString i; wenzelm@233: wenzelm@233: wenzelm@4212: wenzelm@233: (** strings **) wenzelm@233: wenzelm@233: fun is_letter ch = wenzelm@233: ord "A" <= ord ch andalso ord ch <= ord "Z" orelse wenzelm@233: ord "a" <= ord ch andalso ord ch <= ord "z"; wenzelm@233: wenzelm@233: fun is_digit ch = wenzelm@233: ord "0" <= ord ch andalso ord ch <= ord "9"; wenzelm@233: wenzelm@233: (*letter or _ or prime (')*) wenzelm@233: fun is_quasi_letter "_" = true wenzelm@233: | is_quasi_letter "'" = true wenzelm@233: | is_quasi_letter ch = is_letter ch; wenzelm@233: lcp@512: (*white space: blanks, tabs, newlines, formfeeds*) wenzelm@233: val is_blank : string -> bool = wenzelm@3393: fn " " => true | "\t" => true | "\n" => true | "\^L" => true | "\160" => true wenzelm@3063: | _ => false; wenzelm@233: wenzelm@233: val is_letdig = is_quasi_letter orf is_digit; wenzelm@233: wenzelm@2196: (*printable chars*) wenzelm@2196: fun is_printable c = ord c > ord " " andalso ord c <= ord "~"; wenzelm@2196: wenzelm@233: (*lower all chars of string*) wenzelm@233: val to_lower = wenzelm@233: let wenzelm@233: fun lower ch = wenzelm@233: if ch >= "A" andalso ch <= "Z" then wenzelm@233: chr (ord ch - ord "A" + ord "a") wenzelm@233: else ch; wenzelm@233: in implode o (map lower) o explode end; wenzelm@233: lcp@512: (*enclose in brackets*) lcp@512: fun enclose lpar rpar str = lpar ^ str ^ rpar; wenzelm@255: wenzelm@233: (*simple quoting (does not escape special chars)*) lcp@512: val quote = enclose "\"" "\""; wenzelm@233: wenzelm@4212: (*space_implode "..." (explode "hello") = "h...e...l...l...o"*) wenzelm@233: fun space_implode a bs = implode (separate a bs); wenzelm@233: wenzelm@255: val commas = space_implode ", "; wenzelm@380: val commas_quote = commas o map quote; wenzelm@255: wenzelm@233: (*concatenate messages, one per line, into a string*) wenzelm@255: val cat_lines = space_implode "\n"; wenzelm@233: wenzelm@4212: (*space_explode "." "h.e..l.lo" = ["h", "e", "", "l", "lo"]*) wenzelm@3832: fun space_explode _ "" = [] wenzelm@3832: | space_explode sep str = wenzelm@3832: let wenzelm@3832: fun expl chs = wenzelm@3832: (case take_prefix (not_equal sep) chs of wenzelm@3832: (cs, []) => [implode cs] wenzelm@3832: | (cs, _ :: cs') => implode cs :: expl cs'); wenzelm@3832: in expl (explode str) end; wenzelm@3832: wenzelm@3832: val split_lines = space_explode "\n"; wenzelm@3832: wenzelm@3832: wenzelm@233: wenzelm@233: (** lists as sets **) wenzelm@233: wenzelm@233: (*membership in a list*) wenzelm@233: fun x mem [] = false wenzelm@233: | x mem (y :: ys) = x = y orelse x mem ys; clasohm@0: paulson@2175: (*membership in a list, optimized version for ints*) berghofe@1576: fun (x:int) mem_int [] = false berghofe@1576: | x mem_int (y :: ys) = x = y orelse x mem_int ys; berghofe@1576: paulson@2175: (*membership in a list, optimized version for strings*) berghofe@1576: fun (x:string) mem_string [] = false berghofe@1576: | x mem_string (y :: ys) = x = y orelse x mem_string ys; berghofe@1576: clasohm@0: (*generalized membership test*) wenzelm@233: fun gen_mem eq (x, []) = false wenzelm@233: | gen_mem eq (x, y :: ys) = eq (x, y) orelse gen_mem eq (x, ys); wenzelm@233: wenzelm@233: wenzelm@233: (*insertion into list if not already there*) paulson@2175: fun (x ins xs) = if x mem xs then xs else x :: xs; clasohm@0: paulson@2175: (*insertion into list, optimized version for ints*) paulson@2175: fun (x ins_int xs) = if x mem_int xs then xs else x :: xs; berghofe@1576: paulson@2175: (*insertion into list, optimized version for strings*) paulson@2175: fun (x ins_string xs) = if x mem_string xs then xs else x :: xs; berghofe@1576: clasohm@0: (*generalized insertion*) wenzelm@233: fun gen_ins eq (x, xs) = if gen_mem eq (x, xs) then xs else x :: xs; wenzelm@233: wenzelm@233: wenzelm@233: (*union of sets represented as lists: no repetitions*) wenzelm@233: fun xs union [] = xs wenzelm@233: | [] union ys = ys wenzelm@233: | (x :: xs) union ys = xs union (x ins ys); clasohm@0: paulson@2175: (*union of sets, optimized version for ints*) berghofe@1576: fun (xs:int list) union_int [] = xs berghofe@1576: | [] union_int ys = ys berghofe@1576: | (x :: xs) union_int ys = xs union_int (x ins_int ys); berghofe@1576: paulson@2175: (*union of sets, optimized version for strings*) berghofe@1576: fun (xs:string list) union_string [] = xs berghofe@1576: | [] union_string ys = ys berghofe@1576: | (x :: xs) union_string ys = xs union_string (x ins_string ys); berghofe@1576: clasohm@0: (*generalized union*) wenzelm@233: fun gen_union eq (xs, []) = xs wenzelm@233: | gen_union eq ([], ys) = ys wenzelm@233: | gen_union eq (x :: xs, ys) = gen_union eq (xs, gen_ins eq (x, ys)); wenzelm@233: wenzelm@233: wenzelm@233: (*intersection*) wenzelm@233: fun [] inter ys = [] wenzelm@233: | (x :: xs) inter ys = wenzelm@233: if x mem ys then x :: (xs inter ys) else xs inter ys; wenzelm@233: paulson@2175: (*intersection, optimized version for ints*) berghofe@1576: fun ([]:int list) inter_int ys = [] berghofe@1576: | (x :: xs) inter_int ys = berghofe@1576: if x mem_int ys then x :: (xs inter_int ys) else xs inter_int ys; berghofe@1576: paulson@2175: (*intersection, optimized version for strings *) berghofe@1576: fun ([]:string list) inter_string ys = [] berghofe@1576: | (x :: xs) inter_string ys = berghofe@1576: if x mem_string ys then x :: (xs inter_string ys) else xs inter_string ys; berghofe@1576: wenzelm@233: wenzelm@233: (*subset*) wenzelm@233: fun [] subset ys = true wenzelm@233: | (x :: xs) subset ys = x mem ys andalso xs subset ys; wenzelm@233: paulson@2175: (*subset, optimized version for ints*) berghofe@1576: fun ([]:int list) subset_int ys = true berghofe@1576: | (x :: xs) subset_int ys = x mem_int ys andalso xs subset_int ys; berghofe@1576: paulson@2175: (*subset, optimized version for strings*) berghofe@1576: fun ([]:string list) subset_string ys = true berghofe@1576: | (x :: xs) subset_string ys = x mem_string ys andalso xs subset_string ys; berghofe@1576: wenzelm@4363: (*set equality*) wenzelm@4363: fun eq_set (xs, ys) = wenzelm@4363: xs = ys orelse (xs subset ys andalso ys subset xs); wenzelm@4363: paulson@2182: (*set equality for strings*) berghofe@1576: fun eq_set_string ((xs:string list), ys) = berghofe@1576: xs = ys orelse (xs subset_string ys andalso ys subset_string xs); berghofe@1576: paulson@2182: fun gen_subset eq (xs, ys) = forall (fn x => gen_mem eq (x, ys)) xs; paulson@2182: wenzelm@265: wenzelm@233: (*removing an element from a list WITHOUT duplicates*) wenzelm@233: fun (y :: ys) \ x = if x = y then ys else y :: (ys \ x) wenzelm@233: | [] \ x = []; wenzelm@233: paulson@2243: fun ys \\ xs = foldl (op \) (ys,xs); clasohm@0: wenzelm@233: (*removing an element from a list -- possibly WITH duplicates*) wenzelm@233: fun gen_rem eq (xs, y) = filter_out (fn x => eq (x, y)) xs; wenzelm@233: paulson@2243: fun gen_rems eq = foldl (gen_rem eq); wenzelm@233: wenzelm@233: wenzelm@233: (*makes a list of the distinct members of the input; preserves order, takes wenzelm@233: first of equal elements*) wenzelm@233: fun gen_distinct eq lst = wenzelm@233: let wenzelm@233: val memb = gen_mem eq; clasohm@0: wenzelm@233: fun dist (rev_seen, []) = rev rev_seen wenzelm@233: | dist (rev_seen, x :: xs) = wenzelm@233: if memb (x, rev_seen) then dist (rev_seen, xs) wenzelm@233: else dist (x :: rev_seen, xs); wenzelm@233: in wenzelm@233: dist ([], lst) wenzelm@233: end; wenzelm@233: paulson@2243: fun distinct l = gen_distinct (op =) l; wenzelm@233: wenzelm@4102: (*tuned version of distinct -- eq wrt. strings in fst component*) wenzelm@4102: fun distinct_fst_string lst = wenzelm@4102: let wenzelm@4102: fun mem_str ((_:string, _), []) = false wenzelm@4102: | mem_str (p as (x, _), ((y, _) :: qs)) = x = y orelse mem_str (p, qs); wenzelm@4102: wenzelm@4102: fun dist (rev_seen, []) = rev rev_seen wenzelm@4102: | dist (rev_seen, p :: ps) = wenzelm@4102: if mem_str (p, rev_seen) then dist (rev_seen, ps) wenzelm@4102: else dist (p :: rev_seen, ps); wenzelm@4102: in wenzelm@4102: dist ([], lst) wenzelm@4102: end; wenzelm@4102: wenzelm@233: wenzelm@233: (*returns the tail beginning with the first repeated element, or []*) wenzelm@233: fun findrep [] = [] wenzelm@233: | findrep (x :: xs) = if x mem xs then x :: xs else findrep xs; wenzelm@233: wenzelm@233: wenzelm@255: (*returns a list containing all repeated elements exactly once; preserves wenzelm@255: order, takes first of equal elements*) wenzelm@255: fun gen_duplicates eq lst = wenzelm@255: let wenzelm@255: val memb = gen_mem eq; wenzelm@255: wenzelm@255: fun dups (rev_dups, []) = rev rev_dups wenzelm@255: | dups (rev_dups, x :: xs) = wenzelm@255: if memb (x, rev_dups) orelse not (memb (x, xs)) then wenzelm@255: dups (rev_dups, xs) wenzelm@255: else dups (x :: rev_dups, xs); wenzelm@255: in wenzelm@255: dups ([], lst) wenzelm@255: end; wenzelm@255: paulson@2243: fun duplicates l = gen_duplicates (op =) l; wenzelm@255: wenzelm@255: wenzelm@233: wenzelm@233: (** association lists **) clasohm@0: wenzelm@233: (*association list lookup*) wenzelm@233: fun assoc ([], key) = None wenzelm@233: | assoc ((keyi, xi) :: pairs, key) = wenzelm@233: if key = keyi then Some xi else assoc (pairs, key); wenzelm@233: paulson@2175: (*association list lookup, optimized version for ints*) berghofe@1576: fun assoc_int ([], (key:int)) = None berghofe@1576: | assoc_int ((keyi, xi) :: pairs, key) = berghofe@1576: if key = keyi then Some xi else assoc_int (pairs, key); berghofe@1576: paulson@2175: (*association list lookup, optimized version for strings*) berghofe@1576: fun assoc_string ([], (key:string)) = None berghofe@1576: | assoc_string ((keyi, xi) :: pairs, key) = berghofe@1576: if key = keyi then Some xi else assoc_string (pairs, key); berghofe@1576: paulson@2175: (*association list lookup, optimized version for string*ints*) berghofe@1576: fun assoc_string_int ([], (key:string*int)) = None berghofe@1576: | assoc_string_int ((keyi, xi) :: pairs, key) = berghofe@1576: if key = keyi then Some xi else assoc_string_int (pairs, key); berghofe@1576: wenzelm@233: fun assocs ps x = wenzelm@233: (case assoc (ps, x) of wenzelm@233: None => [] wenzelm@233: | Some ys => ys); wenzelm@233: wenzelm@255: (*two-fold association list lookup*) wenzelm@255: fun assoc2 (aal, (key1, key2)) = wenzelm@255: (case assoc (aal, key1) of wenzelm@255: Some al => assoc (al, key2) wenzelm@255: | None => None); wenzelm@255: wenzelm@233: (*generalized association list lookup*) wenzelm@233: fun gen_assoc eq ([], key) = None wenzelm@233: | gen_assoc eq ((keyi, xi) :: pairs, key) = wenzelm@233: if eq (key, keyi) then Some xi else gen_assoc eq (pairs, key); wenzelm@233: wenzelm@233: (*association list update*) wenzelm@233: fun overwrite (al, p as (key, _)) = wenzelm@233: let fun over ((q as (keyi, _)) :: pairs) = wenzelm@233: if keyi = key then p :: pairs else q :: (over pairs) wenzelm@233: | over [] = [p] wenzelm@233: in over al end; wenzelm@233: wenzelm@2522: fun gen_overwrite eq (al, p as (key, _)) = wenzelm@2522: let fun over ((q as (keyi, _)) :: pairs) = wenzelm@2522: if eq (keyi, key) then p :: pairs else q :: (over pairs) wenzelm@2522: | over [] = [p] wenzelm@2522: in over al end; wenzelm@2522: wenzelm@233: wenzelm@233: wenzelm@233: (** generic tables **) clasohm@0: wenzelm@233: (*Tables are supposed to be 'efficient' encodings of lists of elements distinct wenzelm@233: wrt. an equality "eq". The extend and merge operations below are optimized wenzelm@233: for long-term space efficiency.*) wenzelm@233: wenzelm@233: (*append (new) elements to a table*) wenzelm@233: fun generic_extend _ _ _ tab [] = tab wenzelm@233: | generic_extend eq dest_tab mk_tab tab1 lst2 = wenzelm@233: let wenzelm@233: val lst1 = dest_tab tab1; wenzelm@233: val new_lst2 = gen_rems eq (lst2, lst1); wenzelm@233: in wenzelm@233: if null new_lst2 then tab1 wenzelm@233: else mk_tab (lst1 @ new_lst2) wenzelm@233: end; clasohm@0: wenzelm@233: (*append (new) elements of 2nd table to 1st table*) wenzelm@233: fun generic_merge eq dest_tab mk_tab tab1 tab2 = wenzelm@233: let wenzelm@233: val lst1 = dest_tab tab1; wenzelm@233: val lst2 = dest_tab tab2; wenzelm@233: val new_lst2 = gen_rems eq (lst2, lst1); wenzelm@233: in wenzelm@233: if null new_lst2 then tab1 wenzelm@233: else if gen_subset eq (lst1, lst2) then tab2 wenzelm@233: else mk_tab (lst1 @ new_lst2) wenzelm@233: end; clasohm@0: wenzelm@233: wenzelm@233: (*lists as tables*) paulson@2243: fun extend_list tab = generic_extend (op =) I I tab; paulson@2243: fun merge_lists tab = generic_merge (op =) I I tab; wenzelm@233: wenzelm@380: fun merge_rev_lists xs [] = xs wenzelm@380: | merge_rev_lists [] ys = ys wenzelm@380: | merge_rev_lists xs (y :: ys) = wenzelm@380: (if y mem xs then I else cons y) (merge_rev_lists xs ys); wenzelm@380: clasohm@0: clasohm@0: wenzelm@233: (** balanced trees **) wenzelm@233: wenzelm@233: exception Balance; (*indicates non-positive argument to balancing fun*) wenzelm@233: wenzelm@233: (*balanced folding; avoids deep nesting*) wenzelm@233: fun fold_bal f [x] = x wenzelm@233: | fold_bal f [] = raise Balance wenzelm@233: | fold_bal f xs = wenzelm@233: let val k = length xs div 2 wenzelm@233: in f (fold_bal f (take(k, xs)), wenzelm@233: fold_bal f (drop(k, xs))) wenzelm@233: end; wenzelm@233: wenzelm@233: (*construct something of the form f(...g(...(x)...)) for balanced access*) wenzelm@233: fun access_bal (f, g, x) n i = wenzelm@233: let fun acc n i = (*1<=i<=n*) wenzelm@233: if n=1 then x else wenzelm@233: let val n2 = n div 2 wenzelm@233: in if i<=n2 then f (acc n2 i) wenzelm@233: else g (acc (n-n2) (i-n2)) wenzelm@233: end wenzelm@233: in if 1<=i andalso i<=n then acc n i else raise Balance end; wenzelm@233: wenzelm@233: (*construct ALL such accesses; could try harder to share recursive calls!*) wenzelm@233: fun accesses_bal (f, g, x) n = wenzelm@233: let fun acc n = wenzelm@233: if n=1 then [x] else wenzelm@233: let val n2 = n div 2 wenzelm@233: val acc2 = acc n2 wenzelm@233: in if n-n2=n2 then map f acc2 @ map g acc2 wenzelm@233: else map f acc2 @ map g (acc (n-n2)) end wenzelm@233: in if 1<=n then acc n else raise Balance end; wenzelm@233: wenzelm@233: wenzelm@233: wenzelm@2506: (** orders **) wenzelm@2506: wenzelm@2506: datatype order = LESS | EQUAL | GREATER; wenzelm@2506: wenzelm@4445: fun rev_order LESS = GREATER wenzelm@4445: | rev_order EQUAL = EQUAL wenzelm@4445: | rev_order GREATER = LESS; wenzelm@4445: wenzelm@4479: (*assume rel is a linear strict order*) wenzelm@4445: fun make_ord rel (x, y) = wenzelm@4445: if rel (x, y) then LESS wenzelm@4445: else if rel (y, x) then GREATER wenzelm@4445: else EQUAL; wenzelm@4445: wenzelm@4343: fun int_ord (i, j: int) = wenzelm@2506: if i < j then LESS wenzelm@2506: else if i = j then EQUAL wenzelm@2506: else GREATER; wenzelm@2506: wenzelm@4343: fun string_ord (a, b: string) = wenzelm@2506: if a < b then LESS wenzelm@2506: else if a = b then EQUAL wenzelm@2506: else GREATER; wenzelm@2506: wenzelm@4343: (*lexicographic product*) wenzelm@4343: fun prod_ord a_ord b_ord ((x, y), (x', y')) = wenzelm@4343: (case a_ord (x, x') of EQUAL => b_ord (y, y') | ord => ord); wenzelm@4343: wenzelm@4343: (*dictionary order -- in general NOT well-founded!*) wenzelm@4343: fun dict_ord _ ([], []) = EQUAL wenzelm@4343: | dict_ord _ ([], _ :: _) = LESS wenzelm@4343: | dict_ord _ (_ :: _, []) = GREATER wenzelm@4343: | dict_ord elem_ord (x :: xs, y :: ys) = wenzelm@4343: (case elem_ord (x, y) of EQUAL => dict_ord elem_ord (xs, ys) | ord => ord); wenzelm@4343: wenzelm@4343: (*lexicographic product of lists*) wenzelm@4343: fun list_ord elem_ord (xs, ys) = wenzelm@4343: prod_ord int_ord (dict_ord elem_ord) ((length xs, xs), (length ys, ys)); wenzelm@4343: wenzelm@2506: wenzelm@2506: wenzelm@3525: (** input / output and diagnostics **) wenzelm@233: paulson@2243: val cd = OS.FileSys.chDir; wenzelm@2317: val pwd = OS.FileSys.getDir; paulson@2243: wenzelm@3525: wenzelm@3525: local wenzelm@3525: fun out s = wenzelm@3525: (TextIO.output (TextIO.stdOut, s); TextIO.flushOut TextIO.stdOut); wenzelm@3525: wenzelm@3525: fun prefix_lines prfx txt = wenzelm@3832: txt |> split_lines |> map (fn s => prfx ^ s ^ "\n") |> implode; wenzelm@3525: in wenzelm@3525: wenzelm@3525: (*hooks for output channels: normal, warning, error*) wenzelm@3525: val prs_fn = ref (fn s => out s); wenzelm@3525: val warning_fn = ref (fn s => out (prefix_lines "### " s)); wenzelm@3525: val error_fn = ref (fn s => out (prefix_lines "*** " s)); wenzelm@3525: wenzelm@3525: end; berghofe@1580: berghofe@1580: fun prs s = !prs_fn s; wenzelm@233: fun writeln s = prs (s ^ "\n"); wenzelm@233: wenzelm@3525: fun warning s = !warning_fn s; wenzelm@233: wenzelm@233: (*print error message and abort to top level*) wenzelm@233: exception ERROR; wenzelm@4212: fun error_msg s = !error_fn s; (*promise to raise ERROR later!*) wenzelm@3553: fun error s = (error_msg s; raise ERROR); wenzelm@3553: fun sys_error msg = (error_msg " !! SYSTEM ERROR !!\n"; error msg); wenzelm@233: wenzelm@233: fun assert p msg = if p then () else error msg; wenzelm@233: fun deny p msg = if p then error msg else (); wenzelm@233: lcp@544: (*Assert pred for every member of l, generating a message if pred fails*) wenzelm@4212: fun assert_all pred l msg_fn = lcp@544: let fun asl [] = () wenzelm@4212: | asl (x::xs) = if pred x then asl xs else error (msg_fn x) wenzelm@4212: in asl l end; wenzelm@233: wenzelm@3624: wenzelm@4212: (* handle errors capturing messages *) wenzelm@3699: wenzelm@3699: datatype 'a error = wenzelm@3699: Error of string | wenzelm@3699: OK of 'a; wenzelm@3699: wenzelm@4248: fun get_error (Error msg) = Some msg wenzelm@4248: | get_error _ = None; wenzelm@4248: wenzelm@4248: fun get_ok (OK x) = Some x wenzelm@4248: | get_ok _ = None; wenzelm@4248: wenzelm@3699: fun handle_error f x = wenzelm@3699: let wenzelm@3699: val buffer = ref ""; wenzelm@3699: fun capture s = buffer := ! buffer ^ s ^ "\n"; wenzelm@3699: val result = Some (setmp error_fn capture f x) handle ERROR => None; wenzelm@3699: in wenzelm@4212: (case result of wenzelm@3699: None => Error (! buffer) wenzelm@4212: | Some y => OK y) wenzelm@3624: end; wenzelm@3624: wenzelm@3624: wenzelm@233: wenzelm@233: (** timing **) wenzelm@233: paulson@4326: (*a conditional timing function: applies f to () and, if the flag is true, paulson@4326: prints its runtime*) paulson@4326: fun cond_timeit flag f = paulson@4326: if flag then paulson@4326: let val start = startTiming() paulson@4326: val result = f () paulson@4326: in paulson@4326: writeln (endTiming start); result paulson@4326: end paulson@4326: else f (); paulson@4326: wenzelm@233: (*unconditional timing function*) paulson@2243: fun timeit x = cond_timeit true x; wenzelm@233: wenzelm@233: (*timed application function*) wenzelm@233: fun timeap f x = timeit (fn () => f x); wenzelm@233: berghofe@3606: wenzelm@233: wenzelm@233: (** misc functions **) wenzelm@233: wenzelm@233: (*use the keyfun to make a list of (x, key) pairs*) clasohm@0: fun make_keylist (keyfun: 'a->'b) : 'a list -> ('a * 'b) list = wenzelm@233: let fun keypair x = (x, keyfun x) wenzelm@233: in map keypair end; clasohm@0: wenzelm@233: (*given a list of (x, key) pairs and a searchkey clasohm@0: return the list of xs from each pair whose key equals searchkey*) clasohm@0: fun keyfilter [] searchkey = [] wenzelm@233: | keyfilter ((x, key) :: pairs) searchkey = wenzelm@233: if key = searchkey then x :: keyfilter pairs searchkey wenzelm@233: else keyfilter pairs searchkey; clasohm@0: clasohm@0: clasohm@0: (*Partition list into elements that satisfy predicate and those that don't. wenzelm@233: Preserves order of elements in both lists.*) clasohm@0: fun partition (pred: 'a->bool) (ys: 'a list) : ('a list * 'a list) = clasohm@0: let fun part ([], answer) = answer wenzelm@233: | part (x::xs, (ys, ns)) = if pred(x) wenzelm@233: then part (xs, (x::ys, ns)) wenzelm@233: else part (xs, (ys, x::ns)) wenzelm@233: in part (rev ys, ([], [])) end; clasohm@0: clasohm@0: clasohm@0: fun partition_eq (eq:'a * 'a -> bool) = clasohm@0: let fun part [] = [] wenzelm@233: | part (x::ys) = let val (xs, xs') = partition (apl(x, eq)) ys wenzelm@233: in (x::xs)::(part xs') end clasohm@0: in part end; clasohm@0: clasohm@0: wenzelm@233: (*Partition a list into buckets [ bi, b(i+1), ..., bj ] clasohm@0: putting x in bk if p(k)(x) holds. Preserve order of elements if possible.*) clasohm@0: fun partition_list p i j = wenzelm@233: let fun part k xs = wenzelm@233: if k>j then clasohm@0: (case xs of [] => [] clasohm@0: | _ => raise LIST "partition_list") clasohm@0: else wenzelm@233: let val (ns, rest) = partition (p k) xs; wenzelm@233: in ns :: part(k+1)rest end clasohm@0: in part i end; clasohm@0: clasohm@0: wenzelm@233: (* sorting *) wenzelm@233: wenzelm@4445: (*quicksort (stable, i.e. does not reorder equal elements)*) wenzelm@4445: fun sort ord = wenzelm@4445: let wenzelm@4445: fun qsort xs = wenzelm@4445: let val len = length xs in wenzelm@4445: if len <= 1 then xs wenzelm@4445: else wenzelm@4445: let val (lts, eqs, gts) = part (nth_elem (len div 2, xs)) xs in wenzelm@4445: qsort lts @ eqs @ qsort gts wenzelm@4445: end wenzelm@4445: end wenzelm@4445: and part _ [] = ([], [], []) wenzelm@4445: | part pivot (x :: xs) = add (ord (x, pivot)) x (part pivot xs) wenzelm@4445: and add LESS x (lts, eqs, gts) = (x :: lts, eqs, gts) wenzelm@4445: | add EQUAL x (lts, eqs, gts) = (lts, x :: eqs, gts) wenzelm@4445: | add GREATER x (lts, eqs, gts) = (lts, eqs, x :: gts); wenzelm@4445: in qsort end; clasohm@0: wenzelm@41: (*sort strings*) wenzelm@4445: val sort_strings = sort string_ord; wenzelm@4445: fun sort_wrt sel xs = sort (string_ord o pairself sel) xs; wenzelm@41: wenzelm@41: wenzelm@233: (* transitive closure (not Warshall's algorithm) *) clasohm@0: wenzelm@233: fun transitive_closure [] = [] wenzelm@233: | transitive_closure ((x, ys)::ps) = wenzelm@233: let val qs = transitive_closure ps paulson@2182: val zs = foldl (fn (zs, y) => assocs qs y union_string zs) (ys, ys) paulson@2182: fun step(u, us) = (u, if x mem_string us then zs union_string us paulson@2243: else us) wenzelm@233: in (x, zs) :: map step qs end; clasohm@0: clasohm@0: wenzelm@233: (* generating identifiers *) clasohm@0: paulson@4063: (** Freshly generated identifiers; supplied prefix MUST start with a letter **) clasohm@0: local paulson@4063: (*Maps 0-63 to A-Z, a-z, 0-9 or _ or ' for generating random identifiers*) paulson@4063: fun char i = if i<26 then chr (ord "A" + i) paulson@4063: else if i<52 then chr (ord "a" + i - 26) paulson@4063: else if i<62 then chr (ord"0" + i - 52) paulson@4063: else if i=62 then "_" paulson@4063: else (*i=63*) "'"; paulson@4063: paulson@4063: val charVec = Vector.tabulate (64, char); paulson@4063: paulson@4063: fun newid n = paulson@4063: let wenzelm@4284: in implode (map (fn i => Vector.sub(charVec,i)) (radixpand (64,n))) end; paulson@2003: wenzelm@4284: val seedr = ref 0; clasohm@0: paulson@4063: in wenzelm@4284: paulson@4063: fun init_gensym() = (seedr := 0); paulson@2003: wenzelm@4284: fun gensym pre = pre ^ (#1(newid (!seedr), inc seedr)); paulson@4063: end; paulson@4063: paulson@4063: paulson@4063: local paulson@4063: (*Identifies those character codes legal in identifiers. paulson@4063: chould use Basis Library character functions if Poly/ML provided characters*) paulson@4063: fun idCode k = (ord "a" <= k andalso k < ord "z") orelse paulson@4063: (ord "A" <= k andalso k < ord "Z") orelse paulson@4063: (ord "0" <= k andalso k < ord "9"); paulson@4063: paulson@4063: val idCodeVec = Vector.tabulate (256, idCode); paulson@4063: paulson@4063: in paulson@2003: clasohm@0: (*Increment a list of letters like a reversed base 26 number. wenzelm@233: If head is "z", bumps chars in tail. clasohm@0: Digits are incremented as if they were integers. clasohm@0: "_" and "'" are not changed. wenzelm@233: For making variants of identifiers.*) clasohm@0: paulson@4063: fun bump_int_list(c::cs) = paulson@4063: if c="9" then "0" :: bump_int_list cs paulson@4063: else paulson@4063: if "0" <= c andalso c < "9" then chr(ord(c)+1) :: cs wenzelm@233: else "1" :: c :: cs clasohm@0: | bump_int_list([]) = error("bump_int_list: not an identifier"); clasohm@0: wenzelm@233: fun bump_list([], d) = [d] wenzelm@233: | bump_list(["'"], d) = [d, "'"] wenzelm@233: | bump_list("z"::cs, _) = "a" :: bump_list(cs, "a") wenzelm@233: | bump_list("Z"::cs, _) = "A" :: bump_list(cs, "A") wenzelm@233: | bump_list("9"::cs, _) = "0" :: bump_int_list cs paulson@4063: | bump_list(c::cs, _) = paulson@4063: let val k = ord(c) paulson@4063: in if Vector.sub(idCodeVec,k) then chr(k+1) :: cs paulson@4063: else paulson@4063: if c="'" orelse c="_" then c :: bump_list(cs, "") paulson@4063: else error("bump_list: not legal in identifier: " ^ paulson@4063: implode(rev(c::cs))) wenzelm@233: end; clasohm@0: clasohm@0: end; clasohm@0: wenzelm@233: fun bump_string s : string = implode (rev (bump_list(rev(explode s), ""))); wenzelm@41: wenzelm@41: wenzelm@233: (* lexical scanning *) clasohm@0: wenzelm@233: (*scan a list of characters into "words" composed of "letters" (recognized by wenzelm@233: is_let) and separated by any number of non-"letters"*) wenzelm@233: fun scanwords is_let cs = clasohm@0: let fun scan1 [] = [] wenzelm@233: | scan1 cs = wenzelm@233: let val (lets, rest) = take_prefix is_let cs wenzelm@233: in implode lets :: scanwords is_let rest end; wenzelm@233: in scan1 (#2 (take_prefix (not o is_let) cs)) end; clasohm@24: wenzelm@4212: wenzelm@4212: wenzelm@4212: (* Variable-branching trees: for proof terms etc. *) wenzelm@4212: datatype 'a mtree = Join of 'a * 'a mtree list; wenzelm@4212: wenzelm@4212: wenzelm@4255: (* generic objects -- fool the ML type system via exception constructors *) wenzelm@4255: type object = exn; wenzelm@4255: wenzelm@4255: clasohm@1364: end; clasohm@1364: clasohm@1364: open Library;