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;