src/Pure/library.ML
changeset 4212 68c7b37f8721
parent 4194 1c2553be1821
child 4224 79e205c3a82c
     1.1 --- a/src/Pure/library.ML	Wed Nov 12 16:21:26 1997 +0100
     1.2 +++ b/src/Pure/library.ML	Wed Nov 12 16:21:57 1997 +0100
     1.3 @@ -4,13 +4,13 @@
     1.4      Copyright   1992  University of Cambridge
     1.5  
     1.6  Basic library: functions, options, pairs, booleans, lists, integers,
     1.7 -strings, lists as sets, association lists, generic tables, balanced trees,
     1.8 -orders, input / output, timing, filenames, misc functions.
     1.9 +strings, lists as sets, association lists, generic tables, balanced
    1.10 +trees, orders, diagnostics, timing, misc functions.
    1.11  *)
    1.12  
    1.13 -infix |> ~~ \ \\ orelf ins ins_string ins_int orf andf prefix upto downto
    1.14 -      mem mem_int mem_string union union_int union_string  
    1.15 -      inter inter_int inter_string subset subset_int subset_string subdir_of;
    1.16 +infix |> ~~ \ \\ ins ins_string ins_int orf andf prefix upto downto
    1.17 +  mem mem_int mem_string union union_int union_string inter inter_int
    1.18 +  inter_string subset subset_int subset_string;
    1.19  
    1.20  
    1.21  structure Library =
    1.22 @@ -27,16 +27,10 @@
    1.23  (*reverse apply*)
    1.24  fun (x |> f) = f x;
    1.25  
    1.26 -(*combine two functions forming the union of their domains*)
    1.27 -fun (f orelf g) = fn x => f x handle Match => g x;
    1.28 -
    1.29  (*application of (infix) operator to its left or right argument*)
    1.30  fun apl (x, f) y = f (x, y);
    1.31  fun apr (f, y) x = f (x, y);
    1.32  
    1.33 -(*functional for pairs*)
    1.34 -fun pairself f (x, y) = (f x, f y);
    1.35 -
    1.36  (*function exponentiation: f(...(f x)...) with n applications of f*)
    1.37  fun funpow n f x =
    1.38    let fun rep (0, x) = x
    1.39 @@ -61,6 +55,7 @@
    1.40  fun the (Some x) = x
    1.41    | the None = raise OPTION;
    1.42  
    1.43 +(*strict!*)
    1.44  fun if_none None y = y
    1.45    | if_none (Some x) _ = x;
    1.46  
    1.47 @@ -97,9 +92,10 @@
    1.48  
    1.49  fun swap (x, y) = (y, x);
    1.50  
    1.51 -(*apply the function to a component of a pair*)
    1.52 +(*apply function to components*)
    1.53  fun apfst f (x, y) = (f x, y);
    1.54  fun apsnd f (x, y) = (x, f y);
    1.55 +fun pairself f (x, y) = (f x, f y);
    1.56  
    1.57  
    1.58  
    1.59 @@ -114,29 +110,11 @@
    1.60  (* operators for combining predicates *)
    1.61  
    1.62  fun (p orf q) = fn x => p x orelse q x;
    1.63 -
    1.64  fun (p andf q) = fn x => p x andalso q x;
    1.65  
    1.66 -fun notf p x = not (p x);
    1.67 -
    1.68  
    1.69  (* predicates on lists *)
    1.70  
    1.71 -fun orl [] = false
    1.72 -  | orl (x :: xs) = x orelse orl xs;
    1.73 -
    1.74 -fun andl [] = true
    1.75 -  | andl (x :: xs) = x andalso andl xs;
    1.76 -
    1.77 -(*Several object-logics declare theories named List or Option, hiding the
    1.78 -  eponymous basis library structures.*)
    1.79 -structure Basis_Library =
    1.80 -    struct
    1.81 -    structure List = List
    1.82 -    and       Option = Option
    1.83 -    end;
    1.84 -
    1.85 -
    1.86  (*exists pred [x1, ..., xn] ===> pred x1 orelse ... orelse pred xn*)
    1.87  fun exists (pred: 'a -> bool) : 'a list -> bool =
    1.88    let fun boolf [] = false
    1.89 @@ -156,6 +134,7 @@
    1.90  fun reset flag = (flag := false; false);
    1.91  fun toggle flag = (flag := not (! flag); ! flag);
    1.92  
    1.93 +(*temporarily set flag, handling errors*)
    1.94  fun setmp flag value f x =
    1.95    let
    1.96      val orig_value = ! flag;
    1.97 @@ -243,18 +222,22 @@
    1.98    | split_last [x] = ([], x)
    1.99    | split_last (x :: xs) = apfst (cons x) (split_last xs);
   1.100  
   1.101 +(*find the position of an element in a list*)
   1.102 +fun find_index pred =
   1.103 +  let fun find _ [] = ~1
   1.104 +        | find n (x :: xs) = if pred x then n else find (n + 1) xs;
   1.105 +  in find 0 end;
   1.106  
   1.107 -(*find the position of an element in a list*)
   1.108 -fun find_index (pred: 'a->bool) : 'a list -> int =
   1.109 -  let fun find _ []      = ~1
   1.110 -        | find n (x::xs) = if pred x then n else find (n+1) xs
   1.111 -  in find 0 end;
   1.112 -fun find_index_eq x = find_index (equal x);
   1.113 +val find_index_eq = find_index o equal;
   1.114 +
   1.115 +(*find first element satisfying predicate*)
   1.116 +fun find_first _ [] = None
   1.117 +  | find_first pred (x :: xs) =
   1.118 +      if pred x then Some x else find_first pred xs;
   1.119  
   1.120  (*flatten a list of lists to a list*)
   1.121  fun flat (ls: 'c list list) : 'c list = foldr (op @) (ls, []);
   1.122  
   1.123 -
   1.124  (*like Lisp's MAPC -- seq proc [x1, ..., xn] evaluates
   1.125    (proc x1; ...; proc xn) for side effects*)
   1.126  fun seq (proc: 'a -> unit) : 'a list -> unit =
   1.127 @@ -262,7 +245,6 @@
   1.128          | seqf (x :: xs) = (proc x; seqf xs)
   1.129    in seqf end;
   1.130  
   1.131 -
   1.132  (*separate s [x1, x2, ..., xn]  ===>  [x1, s, x2, s, ..., s, xn]*)
   1.133  fun separate s (x :: (xs as _ :: _)) = x :: s :: separate s xs
   1.134    | separate _ xs = xs;
   1.135 @@ -287,7 +269,6 @@
   1.136  
   1.137  fun filter_out f = filter (not o f);
   1.138  
   1.139 -
   1.140  fun mapfilter (f: 'a -> 'b option) ([]: 'a list) = [] : 'b list
   1.141    | mapfilter f (x :: xs) =
   1.142        (case f x of
   1.143 @@ -295,11 +276,6 @@
   1.144        | Some y => y :: mapfilter f xs);
   1.145  
   1.146  
   1.147 -fun find_first pred = let
   1.148 -  fun f [] = None
   1.149 -  |   f (x :: xs) = if pred x then Some x else f  xs
   1.150 -  in f end;
   1.151 -
   1.152  (* lists of pairs *)
   1.153  
   1.154  fun map2 _ ([], []) = []
   1.155 @@ -320,7 +296,6 @@
   1.156    | (x :: xs) ~~ (y :: ys) = (x, y) :: (xs ~~ ys)
   1.157    | _ ~~ _ = raise LIST "~~";
   1.158  
   1.159 -
   1.160  (*inverse of ~~; the old 'split':
   1.161    [(x1, y1), ..., (xn, yn)]  ===>  ([x1, ..., xn], [y1, ..., yn])*)
   1.162  fun split_list (l: ('a * 'b) list) = (map #1 l, map #2 l);
   1.163 @@ -396,6 +371,7 @@
   1.164    | string_of_indexname (a,i) = a ^ "_" ^ Int.toString i;
   1.165  
   1.166  
   1.167 +
   1.168  (** strings **)
   1.169  
   1.170  fun is_letter ch =
   1.171 @@ -420,7 +396,6 @@
   1.172  (*printable chars*)
   1.173  fun is_printable c = ord c > ord " " andalso ord c <= ord "~";
   1.174  
   1.175 -
   1.176  (*lower all chars of string*)
   1.177  val to_lower =
   1.178    let
   1.179 @@ -430,14 +405,13 @@
   1.180        else ch;
   1.181    in implode o (map lower) o explode end;
   1.182  
   1.183 -
   1.184  (*enclose in brackets*)
   1.185  fun enclose lpar rpar str = lpar ^ str ^ rpar;
   1.186  
   1.187  (*simple quoting (does not escape special chars)*)
   1.188  val quote = enclose "\"" "\"";
   1.189  
   1.190 -(*space_implode "..." (explode "hello"); gives "h...e...l...l...o"*)
   1.191 +(*space_implode "..." (explode "hello") = "h...e...l...l...o"*)
   1.192  fun space_implode a bs = implode (separate a bs);
   1.193  
   1.194  val commas = space_implode ", ";
   1.195 @@ -446,17 +420,7 @@
   1.196  (*concatenate messages, one per line, into a string*)
   1.197  val cat_lines = space_implode "\n";
   1.198  
   1.199 -(*BAD_space_explode "." "h.e..l.lo"; gives ["h", "e", "l", "lo"]*)
   1.200 -fun BAD_space_explode sep s =
   1.201 -  let fun divide [] "" = []
   1.202 -        | divide [] part = [part]
   1.203 -        | divide (c::s) part =
   1.204 -            if c = sep then
   1.205 -              (if part = "" then divide s "" else part :: divide s "")
   1.206 -            else divide s (part ^ c)
   1.207 -  in divide (explode s) "" end;
   1.208 -
   1.209 -(*space_explode "." "h.e..l.lo"; gives ["h", "e", "", "l", "lo"]*)
   1.210 +(*space_explode "." "h.e..l.lo" = ["h", "e", "", "l", "lo"]*)
   1.211  fun space_explode _ "" = []
   1.212    | space_explode sep str =
   1.213        let
   1.214 @@ -798,7 +762,7 @@
   1.215  
   1.216  (*print error message and abort to top level*)
   1.217  exception ERROR;
   1.218 -fun error_msg s = !error_fn s;			(*promise to raise ERROR later!*)
   1.219 +fun error_msg s = !error_fn s;	  (*promise to raise ERROR later!*)
   1.220  fun error s = (error_msg s; raise ERROR);
   1.221  fun sys_error msg = (error_msg " !! SYSTEM ERROR !!\n"; error msg);
   1.222  
   1.223 @@ -806,14 +770,13 @@
   1.224  fun deny p msg = if p then error msg else ();
   1.225  
   1.226  (*Assert pred for every member of l, generating a message if pred fails*)
   1.227 -fun assert_all pred l msg_fn = 
   1.228 +fun assert_all pred l msg_fn =
   1.229    let fun asl [] = ()
   1.230 -        | asl (x::xs) = if pred x then asl xs
   1.231 -                        else error (msg_fn x)
   1.232 -  in  asl l  end;
   1.233 +        | asl (x::xs) = if pred x then asl xs else error (msg_fn x)
   1.234 +  in asl l end;
   1.235  
   1.236  
   1.237 -(* handle errors (capturing messages) *)
   1.238 +(* handle errors capturing messages *)
   1.239  
   1.240  datatype 'a error =
   1.241    Error of string |
   1.242 @@ -825,64 +788,12 @@
   1.243      fun capture s = buffer := ! buffer ^ s ^ "\n";
   1.244      val result = Some (setmp error_fn capture f x) handle ERROR => None;
   1.245    in
   1.246 -    case result of
   1.247 +    (case result of
   1.248        None => Error (! buffer)
   1.249 -    | Some y => OK y
   1.250 -  end;
   1.251 -
   1.252 -
   1.253 -(* read / write files *)
   1.254 -
   1.255 -fun read_file name =
   1.256 -  let
   1.257 -    val instream  = TextIO.openIn name;
   1.258 -    val intext = TextIO.inputAll instream;
   1.259 -  in
   1.260 -    TextIO.closeIn instream;
   1.261 -    intext
   1.262 -  end;
   1.263 -
   1.264 -fun write_file name txt =
   1.265 -  let val outstream = TextIO.openOut name in
   1.266 -    TextIO.output (outstream, txt);
   1.267 -    TextIO.closeOut outstream
   1.268 -  end;
   1.269 -
   1.270 -fun append_file name txt =
   1.271 -  let val outstream = TextIO.openAppend name in
   1.272 -    TextIO.output (outstream, txt);
   1.273 -    TextIO.closeOut outstream
   1.274 +    | Some y => OK y)
   1.275    end;
   1.276  
   1.277  
   1.278 -(*for the "test" target in IsaMakefiles -- signifies successful termination*)
   1.279 -fun maketest msg =
   1.280 -  (writeln msg; write_file "test" "Test examples ran successfully\n");
   1.281 -
   1.282 -
   1.283 -(*print a list surrounded by the brackets lpar and rpar, with comma separator
   1.284 -  print nothing for empty list*)
   1.285 -fun print_list (lpar, rpar, pre: 'a -> unit) (l : 'a list) =
   1.286 -  let fun prec x = (prs ","; pre x)
   1.287 -  in
   1.288 -    (case l of
   1.289 -      [] => ()
   1.290 -    | x::l => (prs lpar; pre x; seq prec l; prs rpar))
   1.291 -  end;
   1.292 -
   1.293 -(*print a list of items separated by newlines*)
   1.294 -fun print_list_ln (pre: 'a -> unit) : 'a list -> unit =
   1.295 -  seq (fn x => (pre x; writeln ""));
   1.296 -
   1.297 -
   1.298 -val print_int = prs o string_of_int;
   1.299 -
   1.300 -
   1.301 -(* output to LaTeX / xdvi *)
   1.302 -fun latex s =
   1.303 -  execute ("( cd /tmp ; echo \"" ^ s ^
   1.304 -    "\" | isa2latex -s > $$.tex ; latex $$.tex ; xdvi $$.dvi ; rm $$.* ) > /dev/null &");
   1.305 -
   1.306  
   1.307  (** timing **)
   1.308  
   1.309 @@ -892,69 +803,6 @@
   1.310  (*timed application function*)
   1.311  fun timeap f x = timeit (fn () => f x);
   1.312  
   1.313 -(*timed "use" function, printing filenames*)
   1.314 -fun time_use fname = timeit (fn () =>
   1.315 -  (writeln ("\n**** Starting " ^ fname ^ " ****"); use fname;
   1.316 -   writeln ("\n**** Finished " ^ fname ^ " ****")));
   1.317 -
   1.318 -(*use the file, but exit with error code if errors found.*)
   1.319 -fun exit_use fname = use fname handle _ => exit 1;
   1.320 -
   1.321 -
   1.322 -(** filenames and paths **)
   1.323 -
   1.324 -(*Convert UNIX filename of the form "path/file" to "path/" and "file";
   1.325 -  if filename contains no slash, then it returns "" and "file"*)
   1.326 -val split_filename =
   1.327 -  (pairself implode) o take_suffix (not_equal "/") o explode;
   1.328 -
   1.329 -val base_name = #2 o split_filename;
   1.330 -
   1.331 -(*Merge splitted filename (path and file);
   1.332 -  if path does not end with one a slash is appended*)
   1.333 -fun tack_on "" name = name
   1.334 -  | tack_on path name =
   1.335 -      if last_elem (explode path) = "/" then path ^ name
   1.336 -      else path ^ "/" ^ name;
   1.337 -
   1.338 -(*Remove the extension of a filename, i.e. the part after the last '.'*)
   1.339 -val remove_ext = implode o #1 o take_suffix (not_equal ".") o explode;
   1.340 -
   1.341 -(*Make relative path to reach an absolute location from a different one*)
   1.342 -fun relative_path cur_path dest_path =
   1.343 -  let (*Remove common beginning of both paths and make relative path*)
   1.344 -      fun mk_relative [] [] = []
   1.345 -        | mk_relative [] ds = ds
   1.346 -        | mk_relative cs [] = map (fn _ => "..") cs
   1.347 -        | mk_relative (c::cs) (d::ds) =
   1.348 -            if c = d then mk_relative cs ds
   1.349 -            else ".." :: map (fn _ => "..") cs @ (d::ds);
   1.350 -  in if cur_path = "" orelse hd (explode cur_path) <> "/" orelse
   1.351 -        dest_path = "" orelse hd (explode dest_path) <> "/" then
   1.352 -       error "Relative or empty path passed to relative_path"
   1.353 -     else ();
   1.354 -     space_implode "/" (mk_relative (BAD_space_explode "/" cur_path)
   1.355 -                                    (BAD_space_explode "/" dest_path))
   1.356 -  end;
   1.357 -
   1.358 -(*Determine if absolute path1 is a subdirectory of absolute path2*)
   1.359 -fun path1 subdir_of path2 =
   1.360 -  if hd (explode path1) <> "/" orelse hd (explode path2) <> "/" then
   1.361 -    error "Relative or empty path passed to subdir_of"
   1.362 -  else (BAD_space_explode "/" path2) prefix (BAD_space_explode "/" path1);
   1.363 -
   1.364 -fun absolute_path cwd file =
   1.365 -  let fun rm_points [] result = rev result
   1.366 -        | rm_points (".."::ds) result = rm_points ds (tl result)
   1.367 -        | rm_points ("."::ds) result = rm_points ds result
   1.368 -        | rm_points (d::ds) result = rm_points ds (d::result);
   1.369 -  in if file = "" then ""
   1.370 -     else if hd (explode file) = "/" then file
   1.371 -     else "/" ^ space_implode "/"
   1.372 -                  (rm_points (BAD_space_explode "/" (tack_on cwd file)) [])
   1.373 -  end;
   1.374 -
   1.375 -fun file_exists file = (file_info file <> "");
   1.376  
   1.377  
   1.378  (** misc functions **)
   1.379 @@ -1112,9 +960,12 @@
   1.380              in implode lets :: scanwords is_let rest end;
   1.381    in scan1 (#2 (take_prefix (not o is_let) cs)) end;
   1.382  
   1.383 +
   1.384 +
   1.385 +(* Variable-branching trees: for proof terms etc. *)
   1.386 +datatype 'a mtree = Join of 'a * 'a mtree list;
   1.387 +
   1.388 +
   1.389  end;
   1.390  
   1.391 -(*Variable-branching trees: for proof terms*)
   1.392 -datatype 'a mtree = Join of 'a * 'a mtree list;
   1.393 -
   1.394  open Library;