1(* Title: Pure/library.ML 2 Author: Lawrence C Paulson, Cambridge University Computer Laboratory 3 Author: Markus Wenzel, TU Muenchen 4 5Basic library: functions, pairs, booleans, lists, integers, 6strings, lists as sets, orders, current directory, misc. 7 8See also General/basics.ML for the most fundamental concepts. 9*) 10 11infixr 0 <<< 12infix 2 ? 13infix 3 o oo ooo oooo 14infix 4 ~~ upto downto 15infix orf andf 16 17signature BASIC_LIBRARY = 18sig 19 (*functions*) 20 val undefined: 'a -> 'b 21 val I: 'a -> 'a 22 val K: 'a -> 'b -> 'a 23 val curry: ('a * 'b -> 'c) -> 'a -> 'b -> 'c 24 val uncurry: ('a -> 'b -> 'c) -> 'a * 'b -> 'c 25 val ? : bool * ('a -> 'a) -> 'a -> 'a 26 val oo: ('a -> 'b) * ('c -> 'd -> 'a) -> 'c -> 'd -> 'b 27 val ooo: ('a -> 'b) * ('c -> 'd -> 'e -> 'a) -> 'c -> 'd -> 'e -> 'b 28 val oooo: ('a -> 'b) * ('c -> 'd -> 'e -> 'f -> 'a) -> 'c -> 'd -> 'e -> 'f -> 'b 29 val funpow: int -> ('a -> 'a) -> 'a -> 'a 30 val funpow_yield: int -> ('a -> 'b * 'a) -> 'a -> 'b list * 'a 31 32 (*pairs*) 33 val pair: 'a -> 'b -> 'a * 'b 34 val rpair: 'a -> 'b -> 'b * 'a 35 val fst: 'a * 'b -> 'a 36 val snd: 'a * 'b -> 'b 37 val eq_fst: ('a * 'c -> bool) -> ('a * 'b) * ('c * 'd) -> bool 38 val eq_snd: ('b * 'd -> bool) -> ('a * 'b) * ('c * 'd) -> bool 39 val eq_pair: ('a * 'c -> bool) -> ('b * 'd -> bool) -> ('a * 'b) * ('c * 'd) -> bool 40 val swap: 'a * 'b -> 'b * 'a 41 val apfst: ('a -> 'b) -> 'a * 'c -> 'b * 'c 42 val apsnd: ('a -> 'b) -> 'c * 'a -> 'c * 'b 43 val apply2: ('a -> 'b) -> 'a * 'a -> 'b * 'b 44 45 (*booleans*) 46 val equal: ''a -> ''a -> bool 47 val not_equal: ''a -> ''a -> bool 48 val orf: ('a -> bool) * ('a -> bool) -> 'a -> bool 49 val andf: ('a -> bool) * ('a -> bool) -> 'a -> bool 50 val exists: ('a -> bool) -> 'a list -> bool 51 val forall: ('a -> bool) -> 'a list -> bool 52 53 (*lists*) 54 val single: 'a -> 'a list 55 val the_single: 'a list -> 'a 56 val singleton: ('a list -> 'b list) -> 'a -> 'b 57 val yield_singleton: ('a list -> 'c -> 'b list * 'c) -> 'a -> 'c -> 'b * 'c 58 val perhaps_apply: ('a -> 'a option) list -> 'a -> 'a option 59 val perhaps_loop: ('a -> 'a option) -> 'a -> 'a option 60 val foldl1: ('a * 'a -> 'a) -> 'a list -> 'a 61 val foldr1: ('a * 'a -> 'a) -> 'a list -> 'a 62 val eq_list: ('a * 'a -> bool) -> 'a list * 'a list -> bool 63 val maps: ('a -> 'b list) -> 'a list -> 'b list 64 val filter: ('a -> bool) -> 'a list -> 'a list 65 val filter_out: ('a -> bool) -> 'a list -> 'a list 66 val map_filter: ('a -> 'b option) -> 'a list -> 'b list 67 val take: int -> 'a list -> 'a list 68 val drop: int -> 'a list -> 'a list 69 val chop: int -> 'a list -> 'a list * 'a list 70 val chop_groups: int -> 'a list -> 'a list list 71 val nth: 'a list -> int -> 'a 72 val nth_list: 'a list list -> int -> 'a list 73 val nth_map: int -> ('a -> 'a) -> 'a list -> 'a list 74 val nth_drop: int -> 'a list -> 'a list 75 val map_index: (int * 'a -> 'b) -> 'a list -> 'b list 76 val fold_index: (int * 'a -> 'b -> 'b) -> 'a list -> 'b -> 'b 77 val map_range: (int -> 'a) -> int -> 'a list 78 val fold_range: (int -> 'a -> 'a) -> int -> 'a -> 'a 79 val split_last: 'a list -> 'a list * 'a 80 val find_first: ('a -> bool) -> 'a list -> 'a option 81 val find_index: ('a -> bool) -> 'a list -> int 82 val get_first: ('a -> 'b option) -> 'a list -> 'b option 83 val get_index: ('a -> 'b option) -> 'a list -> (int * 'b) option 84 val flat: 'a list list -> 'a list 85 val unflat: 'a list list -> 'b list -> 'b list list 86 val grouped: int -> (('a list -> 'b list) -> 'c list list -> 'd list list) -> 87 ('a -> 'b) -> 'c list -> 'd list 88 val burrow: ('a list -> 'b list) -> 'a list list -> 'b list list 89 val burrow_options: ('a list -> 'b list) -> 'a option list -> 'b option list 90 val fold_burrow: ('a list -> 'c -> 'b list * 'd) -> 'a list list -> 'c -> 'b list list * 'd 91 val separate: 'a -> 'a list -> 'a list 92 val surround: 'a -> 'a list -> 'a list 93 val replicate: int -> 'a -> 'a list 94 val map_product: ('a -> 'b -> 'c) -> 'a list -> 'b list -> 'c list 95 val fold_product: ('a -> 'b -> 'c -> 'c) -> 'a list -> 'b list -> 'c -> 'c 96 val map2: ('a -> 'b -> 'c) -> 'a list -> 'b list -> 'c list 97 val fold2: ('a -> 'b -> 'c -> 'c) -> 'a list -> 'b list -> 'c -> 'c 98 val map_split: ('a -> 'b * 'c) -> 'a list -> 'b list * 'c list 99 val zip_options: 'a list -> 'b option list -> ('a * 'b) list 100 val ~~ : 'a list * 'b list -> ('a * 'b) list 101 val split_list: ('a * 'b) list -> 'a list * 'b list 102 val burrow_fst: ('a list -> 'b list) -> ('a * 'c) list -> ('b * 'c) list 103 val take_prefix: ('a -> bool) -> 'a list -> 'a list 104 val drop_prefix: ('a -> bool) -> 'a list -> 'a list 105 val chop_prefix: ('a -> bool) -> 'a list -> 'a list * 'a list 106 val take_suffix: ('a -> bool) -> 'a list -> 'a list 107 val drop_suffix: ('a -> bool) -> 'a list -> 'a list 108 val chop_suffix: ('a -> bool) -> 'a list -> 'a list * 'a list 109 val is_prefix: ('a * 'a -> bool) -> 'a list -> 'a list -> bool 110 val chop_common_prefix: ('a * 'b -> bool) -> 'a list * 'b list -> 'a list * ('a list * 'b list) 111 val prefixes1: 'a list -> 'a list list 112 val prefixes: 'a list -> 'a list list 113 val suffixes1: 'a list -> 'a list list 114 val suffixes: 'a list -> 'a list list 115 val trim: ('a -> bool) -> 'a list -> 'a list 116 117 (*integers*) 118 val upto: int * int -> int list 119 val downto: int * int -> int list 120 val hex_digit: int -> string 121 val radixpand: int * int -> int list 122 val radixstring: int * string * int -> string 123 val string_of_int: int -> string 124 val signed_string_of_int: int -> string 125 val string_of_indexname: string * int -> string 126 val read_radix_int: int -> string list -> int * string list 127 val read_int: string list -> int * string list 128 val oct_char: string -> string 129 130 (*strings*) 131 val nth_string: string -> int -> string 132 val fold_string: (string -> 'a -> 'a) -> string -> 'a -> 'a 133 val exists_string: (string -> bool) -> string -> bool 134 val forall_string: (string -> bool) -> string -> bool 135 val first_field: string -> string -> (string * string) option 136 val enclose: string -> string -> string -> string 137 val unenclose: string -> string 138 val quote: string -> string 139 val cartouche: string -> string 140 val space_implode: string -> string list -> string 141 val commas: string list -> string 142 val commas_quote: string list -> string 143 val cat_lines: string list -> string 144 val space_explode: string -> string -> string list 145 val split_lines: string -> string list 146 val plain_words: string -> string 147 val prefix_lines: string -> string -> string 148 val prefix: string -> string -> string 149 val suffix: string -> string -> string 150 val unprefix: string -> string -> string 151 val unsuffix: string -> string -> string 152 val trim_line: string -> string 153 val trim_split_lines: string -> string list 154 val normalize_lines: string -> string 155 val replicate_string: int -> string -> string 156 val translate_string: (string -> string) -> string -> string 157 val encode_lines: string -> string 158 val decode_lines: string -> string 159 val align_right: string -> int -> string -> string 160 val match_string: string -> string -> bool 161 162 (*reals*) 163 val string_of_real: real -> string 164 val signed_string_of_real: real -> string 165 166 (*lists as sets -- see also Pure/General/ord_list.ML*) 167 val member: ('b * 'a -> bool) -> 'a list -> 'b -> bool 168 val insert: ('a * 'a -> bool) -> 'a -> 'a list -> 'a list 169 val remove: ('b * 'a -> bool) -> 'b -> 'a list -> 'a list 170 val update: ('a * 'a -> bool) -> 'a -> 'a list -> 'a list 171 val union: ('a * 'a -> bool) -> 'a list -> 'a list -> 'a list 172 val subtract: ('b * 'a -> bool) -> 'b list -> 'a list -> 'a list 173 val inter: ('a * 'b -> bool) -> 'b list -> 'a list -> 'a list 174 val merge: ('a * 'a -> bool) -> 'a list * 'a list -> 'a list 175 val subset: ('a * 'b -> bool) -> 'a list * 'b list -> bool 176 val eq_set: ('a * 'a -> bool) -> 'a list * 'a list -> bool 177 val distinct: ('a * 'a -> bool) -> 'a list -> 'a list 178 val duplicates: ('a * 'a -> bool) -> 'a list -> 'a list 179 val has_duplicates: ('a * 'a -> bool) -> 'a list -> bool 180 val map_transpose: ('a list -> 'b) -> 'a list list -> 'b list 181 182 (*lists as multisets*) 183 val remove1: ('b * 'a -> bool) -> 'b -> 'a list -> 'a list 184 val combine: ('a * 'a -> bool) -> 'a list -> 'a list -> 'a list 185 val submultiset: ('a * 'b -> bool) -> 'a list * 'b list -> bool 186 187 (*orders*) 188 type 'a ord = 'a * 'a -> order 189 val is_equal: order -> bool 190 val is_less: order -> bool 191 val is_less_equal: order -> bool 192 val is_greater: order -> bool 193 val is_greater_equal: order -> bool 194 val rev_order: order -> order 195 val make_ord: ('a * 'a -> bool) -> 'a ord 196 val bool_ord: bool ord 197 val int_ord: int ord 198 val string_ord: string ord 199 val fast_string_ord: string ord 200 val option_ord: ('a * 'b -> order) -> 'a option * 'b option -> order 201 val <<< : ('a -> order) * ('a -> order) -> 'a -> order 202 val prod_ord: ('a * 'b -> order) -> ('c * 'd -> order) -> ('a * 'c) * ('b * 'd) -> order 203 val dict_ord: ('a * 'b -> order) -> 'a list * 'b list -> order 204 val list_ord: ('a * 'b -> order) -> 'a list * 'b list -> order 205 val sort: 'a ord -> 'a list -> 'a list 206 val sort_distinct: 'a ord -> 'a list -> 'a list 207 val sort_strings: string list -> string list 208 val sort_by: ('a -> string) -> 'a list -> 'a list 209 val tag_list: int -> 'a list -> (int * 'a) list 210 val untag_list: (int * 'a) list -> 'a list 211 val order_list: (int * 'a) list -> 'a list 212 213 (*misc*) 214 val divide_and_conquer: ('a -> 'a list * ('b list -> 'b)) -> 'a -> 'b 215 val divide_and_conquer': ('a -> 'b -> ('a list * ('c list * 'b -> 'c * 'b)) * 'b) -> 216 'a -> 'b -> 'c * 'b 217 val partition_eq: ('a * 'a -> bool) -> 'a list -> 'a list list 218 val partition_list: (int -> 'a -> bool) -> int -> int -> 'a list -> 'a list list 219 type serial = int 220 val serial: unit -> serial 221 val serial_string: unit -> string 222 eqtype stamp 223 val stamp: unit -> stamp 224 structure Any: sig type T = exn end 225 val getenv: string -> string 226 val getenv_strict: string -> string 227end; 228 229signature LIBRARY = 230sig 231 include BASIC_LIBRARY 232 val foldl: ('a * 'b -> 'a) -> 'a * 'b list -> 'a 233 val foldr: ('a * 'b -> 'b) -> 'a list * 'b -> 'b 234end; 235 236structure Library: LIBRARY = 237struct 238 239(* functions *) 240 241fun undefined _ = raise Match; 242 243fun I x = x; 244fun K x = fn _ => x; 245fun curry f x y = f (x, y); 246fun uncurry f (x, y) = f x y; 247 248(*conditional application*) 249fun b ? f = fn x => if b then f x else x; 250 251(*composition with multiple args*) 252fun (f oo g) x y = f (g x y); 253fun (f ooo g) x y z = f (g x y z); 254fun (f oooo g) x y z w = f (g x y z w); 255 256(*function exponentiation: f (... (f x) ...) with n applications of f*) 257fun funpow (0: int) _ x = x 258 | funpow n f x = funpow (n - 1) f (f x); 259 260fun funpow_yield (0 : int) _ x = ([], x) 261 | funpow_yield n f x = x |> f ||>> funpow_yield (n - 1) f |>> op ::; 262 263 264(* pairs *) 265 266fun pair x y = (x, y); 267fun rpair x y = (y, x); 268 269fun fst (x, y) = x; 270fun snd (x, y) = y; 271 272fun eq_fst eq ((x1, _), (x2, _)) = eq (x1, x2); 273fun eq_snd eq ((_, y1), (_, y2)) = eq (y1, y2); 274fun eq_pair eqx eqy ((x1, y1), (x2, y2)) = eqx (x1, x2) andalso eqy (y1, y2); 275 276fun swap (x, y) = (y, x); 277 278fun apfst f (x, y) = (f x, y); 279fun apsnd f (x, y) = (x, f y); 280fun apply2 f (x, y) = (f x, f y); 281 282 283(* booleans *) 284 285(*polymorphic equality*) 286fun equal x y = x = y; 287fun not_equal x y = x <> y; 288 289(*combining predicates*) 290fun p orf q = fn x => p x orelse q x; 291fun p andf q = fn x => p x andalso q x; 292 293val exists = List.exists; 294val forall = List.all; 295 296 297 298(** lists **) 299 300fun single x = [x]; 301 302fun the_single [x] = x 303 | the_single _ = raise List.Empty; 304 305fun singleton f x = the_single (f [x]); 306 307fun yield_singleton f x = f [x] #>> the_single; 308 309fun perhaps_apply funs arg = 310 let 311 fun app [] res = res 312 | app (f :: fs) (changed, x) = 313 (case f x of 314 NONE => app fs (changed, x) 315 | SOME x' => app fs (true, x')); 316 in (case app funs (false, arg) of (false, _) => NONE | (true, arg') => SOME arg') end; 317 318fun perhaps_loop f arg = 319 let 320 fun loop (changed, x) = 321 (case f x of 322 NONE => (changed, x) 323 | SOME x' => loop (true, x')); 324 in (case loop (false, arg) of (false, _) => NONE | (true, arg') => SOME arg') end; 325 326 327(* fold -- old versions *) 328 329(*the following versions of fold are designed to fit nicely with infixes*) 330 331(* (op @) (e, [x1, ..., xn]) ===> ((e @ x1) @ x2) ... @ xn 332 for operators that associate to the left (TAIL RECURSIVE)*) 333fun foldl (f: 'a * 'b -> 'a) : 'a * 'b list -> 'a = 334 let fun itl (e, []) = e 335 | itl (e, a::l) = itl (f(e, a), l) 336 in itl end; 337 338(* (op @) ([x1, ..., xn], e) ===> x1 @ (x2 ... @ (xn @ e)) 339 for operators that associate to the right (not tail recursive)*) 340fun foldr f (l, e) = 341 let fun itr [] = e 342 | itr (a::l) = f(a, itr l) 343 in itr l end; 344 345(* (op @) [x1, ..., xn] ===> ((x1 @ x2) @ x3) ... @ xn 346 for operators that associate to the left (TAIL RECURSIVE)*) 347fun foldl1 f [] = raise List.Empty 348 | foldl1 f (x :: xs) = foldl f (x, xs); 349 350(* (op @) [x1, ..., xn] ===> x1 @ (x2 ... @ (x[n-1] @ xn)) 351 for n > 0, operators that associate to the right (not tail recursive)*) 352fun foldr1 f [] = raise List.Empty 353 | foldr1 f l = 354 let fun itr [x] = x 355 | itr (x::l) = f(x, itr l) 356 in itr l end; 357 358 359(* basic list functions *) 360 361fun eq_list eq (list1, list2) = 362 pointer_eq (list1, list2) orelse 363 let 364 fun eq_lst (x :: xs, y :: ys) = eq (x, y) andalso eq_lst (xs, ys) 365 | eq_lst _ = true; 366 in length list1 = length list2 andalso eq_lst (list1, list2) end; 367 368fun maps f [] = [] 369 | maps f (x :: xs) = f x @ maps f xs; 370 371val filter = List.filter; 372fun filter_out f = filter (not o f); 373val map_filter = List.mapPartial; 374 375fun take (0: int) xs = [] 376 | take _ [] = [] 377 | take n (x :: xs) = x :: take (n - 1) xs; 378 379fun drop (0: int) xs = xs 380 | drop _ [] = [] 381 | drop n (x :: xs) = drop (n - 1) xs; 382 383fun chop (0: int) xs = ([], xs) 384 | chop _ [] = ([], []) 385 | chop n (x :: xs) = chop (n - 1) xs |>> cons x; 386 387fun chop_groups n list = 388 (case chop (Int.max (n, 1)) list of 389 ([], _) => [] 390 | (g, rest) => g :: chop_groups n rest); 391 392 393(*return nth element of a list, where 0 designates the first element; 394 raise Subscript if list too short*) 395fun nth xs i = List.nth (xs, i); 396 397fun nth_list xss i = nth xss i handle General.Subscript => []; 398 399fun nth_map 0 f (x :: xs) = f x :: xs 400 | nth_map n f (x :: xs) = x :: nth_map (n - 1) f xs 401 | nth_map (_: int) _ [] = raise Subscript; 402 403fun nth_drop n xs = 404 List.take (xs, n) @ List.drop (xs, n + 1); 405 406fun map_index f = 407 let 408 fun map_aux (_: int) [] = [] 409 | map_aux i (x :: xs) = f (i, x) :: map_aux (i + 1) xs 410 in map_aux 0 end; 411 412fun fold_index f = 413 let 414 fun fold_aux (_: int) [] y = y 415 | fold_aux i (x :: xs) y = fold_aux (i + 1) xs (f (i, x) y) 416 in fold_aux 0 end; 417 418fun map_range f i = 419 let 420 fun map_aux (k: int) = 421 if k < i then f k :: map_aux (k + 1) else [] 422 in map_aux 0 end; 423 424fun fold_range f i = 425 let 426 fun fold_aux (k: int) y = 427 if k < i then fold_aux (k + 1) (f k y) else y 428 in fold_aux 0 end; 429 430 431(*rear decomposition*) 432fun split_last [] = raise List.Empty 433 | split_last [x] = ([], x) 434 | split_last (x :: xs) = apfst (cons x) (split_last xs); 435 436(*find first element satisfying predicate*) 437val find_first = List.find; 438 439(*find position of first element satisfying a predicate*) 440fun find_index pred = 441 let fun find (_: int) [] = ~1 442 | find n (x :: xs) = if pred x then n else find (n + 1) xs; 443 in find 0 end; 444 445(*get first element by lookup function*) 446fun get_first _ [] = NONE 447 | get_first f (x :: xs) = 448 (case f x of 449 NONE => get_first f xs 450 | some => some); 451 452fun get_index f = 453 let 454 fun get_aux (_: int) [] = NONE 455 | get_aux i (x :: xs) = 456 (case f x of 457 NONE => get_aux (i + 1) xs 458 | SOME y => SOME (i, y)) 459 in get_aux 0 end; 460 461val flat = List.concat; 462 463fun unflat (xs :: xss) ys = 464 let val (ps, qs) = chop (length xs) ys 465 in ps :: unflat xss qs end 466 | unflat [] [] = [] 467 | unflat _ _ = raise ListPair.UnequalLengths; 468 469fun grouped n comb f = chop_groups n #> comb (map f) #> flat; 470 471fun burrow f xss = unflat xss (f (flat xss)); 472 473fun burrow_options f os = map (try hd) (burrow f (map the_list os)); 474 475fun fold_burrow f xss s = 476 apfst (unflat xss) (f (flat xss) s); 477 478(*separate s [x1, x2, ..., xn] ===> [x1, s, x2, s, ..., s, xn]*) 479fun separate s (x :: (xs as _ :: _)) = x :: s :: separate s xs 480 | separate _ xs = xs; 481 482fun surround s (x :: xs) = s :: x :: surround s xs 483 | surround s [] = [s]; 484 485(*make the list [x, x, ..., x] of length n*) 486fun replicate (n: int) x = 487 let fun rep (0, xs) = xs 488 | rep (n, xs) = rep (n - 1, x :: xs) 489 in 490 if n < 0 then raise Subscript 491 else rep (n, []) 492 end; 493 494 495(* direct product *) 496 497fun map_product f _ [] = [] 498 | map_product f [] _ = [] 499 | map_product f (x :: xs) ys = map (f x) ys @ map_product f xs ys; 500 501fun fold_product f _ [] z = z 502 | fold_product f [] _ z = z 503 | fold_product f (x :: xs) ys z = z |> fold (f x) ys |> fold_product f xs ys; 504 505 506(* lists of pairs *) 507 508fun map2 _ [] [] = [] 509 | map2 f (x :: xs) (y :: ys) = f x y :: map2 f xs ys 510 | map2 _ _ _ = raise ListPair.UnequalLengths; 511 512fun fold2 _ [] [] z = z 513 | fold2 f (x :: xs) (y :: ys) z = fold2 f xs ys (f x y z) 514 | fold2 _ _ _ _ = raise ListPair.UnequalLengths; 515 516fun map_split _ [] = ([], []) 517 | map_split f (x :: xs) = 518 let 519 val (y, w) = f x; 520 val (ys, ws) = map_split f xs; 521 in (y :: ys, w :: ws) end; 522 523fun zip_options (x :: xs) (SOME y :: ys) = (x, y) :: zip_options xs ys 524 | zip_options (_ :: xs) (NONE :: ys) = zip_options xs ys 525 | zip_options _ [] = [] 526 | zip_options [] _ = raise ListPair.UnequalLengths; 527 528(*combine two lists forming a list of pairs: 529 [x1, ..., xn] ~~ [y1, ..., yn] ===> [(x1, y1), ..., (xn, yn)]*) 530fun [] ~~ [] = [] 531 | (x :: xs) ~~ (y :: ys) = (x, y) :: (xs ~~ ys) 532 | _ ~~ _ = raise ListPair.UnequalLengths; 533 534(*inverse of ~~; the old 'split': 535 [(x1, y1), ..., (xn, yn)] ===> ([x1, ..., xn], [y1, ..., yn])*) 536val split_list = ListPair.unzip; 537 538fun burrow_fst f xs = split_list xs |>> f |> op ~~; 539 540 541(* take, drop, chop, trim according to predicate *) 542 543fun take_prefix pred list = 544 let 545 fun take res (x :: xs) = if pred x then take (x :: res) xs else rev res 546 | take res [] = rev res; 547 in take [] list end; 548 549fun drop_prefix pred list = 550 let 551 fun drop (x :: xs) = if pred x then drop xs else x :: xs 552 | drop [] = []; 553 in drop list end; 554 555fun chop_prefix pred list = 556 let 557 val prfx = take_prefix pred list; 558 val sffx = drop (length prfx) list; 559 in (prfx, sffx) end; 560 561fun take_suffix pred list = 562 let 563 fun take res (x :: xs) = if pred x then take (x :: res) xs else res 564 | take res [] = res; 565 in take [] (rev list) end; 566 567fun drop_suffix pred list = 568 let 569 fun drop (x :: xs) = if pred x then drop xs else rev (x :: xs) 570 | drop [] = []; 571 in drop (rev list) end; 572 573fun chop_suffix pred list = 574 let 575 val prfx = drop_suffix pred list; 576 val sffx = drop (length prfx) list; 577 in (prfx, sffx) end; 578 579fun trim pred = drop_prefix pred #> drop_suffix pred; 580 581 582(* prefixes, suffixes *) 583 584fun is_prefix _ [] _ = true 585 | is_prefix eq (x :: xs) (y :: ys) = eq (x, y) andalso is_prefix eq xs ys 586 | is_prefix eq _ _ = false; 587 588fun chop_common_prefix eq ([], ys) = ([], ([], ys)) 589 | chop_common_prefix eq (xs, []) = ([], (xs, [])) 590 | chop_common_prefix eq (xs as x :: xs', ys as y :: ys') = 591 if eq (x, y) then 592 let val (ps', xys'') = chop_common_prefix eq (xs', ys') 593 in (x :: ps', xys'') end 594 else ([], (xs, ys)); 595 596fun prefixes1 [] = [] 597 | prefixes1 (x :: xs) = map (cons x) ([] :: prefixes1 xs); 598 599fun prefixes xs = [] :: prefixes1 xs; 600 601fun suffixes1 xs = map rev (prefixes1 (rev xs)); 602fun suffixes xs = [] :: suffixes1 xs; 603 604 605 606(** integers **) 607 608(* lists of integers *) 609 610(*make the list [from, from + 1, ..., to]*) 611fun ((i: int) upto j) = 612 if i > j then [] else i :: (i + 1 upto j); 613 614(*make the list [from, from - 1, ..., to]*) 615fun ((i: int) downto j) = 616 if i < j then [] else i :: (i - 1 downto j); 617 618 619(* convert integers to strings *) 620 621(*hexadecimal*) 622fun hex_digit i = 623 if i < 10 then chr (Char.ord #"0" + i) else chr (Char.ord #"a" + i - 10); 624 625(*expand the number in the given base; 626 example: radixpand (2, 8) gives [1, 0, 0, 0]*) 627fun radixpand (base, num) : int list = 628 let 629 fun radix (n, tail) = 630 if n < base then n :: tail 631 else radix (n div base, (n mod base) :: tail) 632 in radix (num, []) end; 633 634(*expands a number into a string of characters starting from "zerochar"; 635 example: radixstring (2, "0", 8) gives "1000"*) 636fun radixstring (base, zerochar, num) = 637 let val offset = ord zerochar; 638 fun chrof n = chr (offset + n) 639 in implode (map chrof (radixpand (base, num))) end; 640 641 642local 643 val zero = Char.ord #"0"; 644 val small_int = 10000: int; 645 val small_int_table = Vector.tabulate (small_int, Int.toString); 646in 647 648fun string_of_int i = 649 if i < 0 then Int.toString i 650 else if i < 10 then chr (zero + i) 651 else if i < small_int then Vector.sub (small_int_table, i) 652 else Int.toString i; 653 654end; 655 656fun signed_string_of_int i = 657 if i < 0 then "-" ^ string_of_int (~ i) else string_of_int i; 658 659fun string_of_indexname (a, 0) = a 660 | string_of_indexname (a, i) = a ^ "_" ^ string_of_int i; 661 662 663(* read integers *) 664 665fun read_radix_int radix cs = 666 let 667 val zero = Char.ord #"0"; 668 val limit = zero + radix; 669 fun scan (num, []) = (num, []) 670 | scan (num, c :: cs) = 671 if zero <= ord c andalso ord c < limit then 672 scan (radix * num + (ord c - zero), cs) 673 else (num, c :: cs); 674 in scan (0, cs) end; 675 676val read_int = read_radix_int 10; 677 678fun oct_char s = chr (#1 (read_radix_int 8 (raw_explode s))); 679 680 681 682(** strings **) 683 684(* functions tuned for strings, avoiding explode *) 685 686fun nth_string str i = 687 (case try String.substring (str, i, 1) of 688 SOME s => s 689 | NONE => raise Subscript); 690 691fun fold_string f str x0 = 692 let 693 val n = size str; 694 fun iter (x, i) = 695 if i < n then iter (f (String.substring (str, i, 1)) x, i + 1) else x; 696 in iter (x0, 0) end; 697 698fun exists_string pred str = 699 let 700 val n = size str; 701 fun ex i = i < n andalso (pred (String.substring (str, i, 1)) orelse ex (i + 1)); 702 in ex 0 end; 703 704fun forall_string pred = not o exists_string (not o pred); 705 706fun first_field sep str = 707 let 708 val n = size sep; 709 val len = size str; 710 fun find i = 711 if i + n > len then NONE 712 else if String.substring (str, i, n) = sep then SOME i 713 else find (i + 1); 714 in 715 (case find 0 of 716 NONE => NONE 717 | SOME i => SOME (String.substring (str, 0, i), String.extract (str, i + n, NONE))) 718 end; 719 720(*enclose in brackets*) 721fun enclose lpar rpar str = lpar ^ str ^ rpar; 722fun unenclose str = String.substring (str, 1, size str - 2); 723 724(*simple quoting (does not escape special chars)*) 725val quote = enclose "\"" "\""; 726 727val cartouche = enclose "\<open>" "\<close>"; 728 729val space_implode = String.concatWith; 730 731val commas = space_implode ", "; 732val commas_quote = commas o map quote; 733 734val cat_lines = space_implode "\n"; 735 736(*space_explode "." "h.e..l.lo" = ["h", "e", "", "l", "lo"]*) 737fun space_explode _ "" = [] 738 | space_explode sep s = String.fields (fn c => str c = sep) s; 739 740val split_lines = space_explode "\n"; 741 742fun plain_words s = space_explode "_" s |> space_implode " "; 743 744fun prefix_lines "" txt = txt 745 | prefix_lines prfx txt = txt |> split_lines |> map (fn s => prfx ^ s) |> cat_lines; 746 747fun prefix prfx s = prfx ^ s; 748fun suffix sffx s = s ^ sffx; 749 750fun unprefix prfx s = 751 if String.isPrefix prfx s then String.substring (s, size prfx, size s - size prfx) 752 else raise Fail "unprefix"; 753 754fun unsuffix sffx s = 755 if String.isSuffix sffx s then String.substring (s, 0, size s - size sffx) 756 else raise Fail "unsuffix"; 757 758fun trim_line s = 759 if String.isSuffix "\r\n" s 760 then String.substring (s, 0, size s - 2) 761 else if String.isSuffix "\r" s orelse String.isSuffix "\n" s 762 then String.substring (s, 0, size s - 1) 763 else s; 764 765val trim_split_lines = trim_line #> split_lines #> map trim_line; 766 767fun normalize_lines str = 768 if exists_string (fn s => s = "\r") str then 769 split_lines str |> map trim_line |> cat_lines 770 else str; 771 772fun replicate_string (0: int) _ = "" 773 | replicate_string 1 a = a 774 | replicate_string k a = 775 if k mod 2 = 0 then replicate_string (k div 2) (a ^ a) 776 else replicate_string (k div 2) (a ^ a) ^ a; 777 778fun translate_string f = String.translate (f o String.str); 779 780val encode_lines = translate_string (fn "\n" => "\v" | c => c); 781val decode_lines = translate_string (fn "\v" => "\n" | c => c); 782 783fun align_right c k s = 784 let 785 val _ = if size c <> 1 orelse size s > k 786 then raise Fail "align_right" else () 787 in replicate_string (k - size s) c ^ s end; 788 789(*crude matching of str against simple glob pat*) 790fun match_string pat str = 791 let 792 fun match [] _ = true 793 | match (p :: ps) s = 794 size p <= size s andalso 795 (case try (unprefix p) s of 796 SOME s' => match ps s' 797 | NONE => match (p :: ps) (String.substring (s, 1, size s - 1))); 798 in match (space_explode "*" pat) str end; 799 800 801 802(** reals **) 803 804val string_of_real = Real.fmt (StringCvt.GEN NONE); 805 806fun signed_string_of_real x = 807 if x < 0.0 then "-" ^ string_of_real (~ x) else string_of_real x; 808 809 810 811(** lists as sets -- see also Pure/General/ord_list.ML **) 812 813(* canonical operations *) 814 815fun member eq list x = 816 let 817 fun memb [] = false 818 | memb (y :: ys) = eq (x, y) orelse memb ys; 819 in memb list end; 820 821fun insert eq x xs = if member eq xs x then xs else x :: xs; 822fun remove eq x xs = if member eq xs x then filter_out (fn y => eq (x, y)) xs else xs; 823fun update eq x xs = cons x (remove eq x xs); 824 825fun inter eq xs = filter (member eq xs); 826 827fun union eq = fold (insert eq); 828fun subtract eq = fold (remove eq); 829 830fun merge eq (xs, ys) = 831 if pointer_eq (xs, ys) then xs 832 else if null xs then ys 833 else fold_rev (insert eq) ys xs; 834 835 836(* subset and set equality *) 837 838fun subset eq (xs, ys) = forall (member eq ys) xs; 839 840fun eq_set eq (xs, ys) = 841 eq_list eq (xs, ys) orelse 842 (subset eq (xs, ys) andalso subset (eq o swap) (ys, xs)); 843 844 845(*makes a list of the distinct members of the input; preserves order, takes 846 first of equal elements*) 847fun distinct eq lst = 848 let 849 fun dist (rev_seen, []) = rev rev_seen 850 | dist (rev_seen, x :: xs) = 851 if member eq rev_seen x then dist (rev_seen, xs) 852 else dist (x :: rev_seen, xs); 853 in dist ([], lst) end; 854 855(*returns a list containing all repeated elements exactly once; preserves 856 order, takes first of equal elements*) 857fun duplicates eq lst = 858 let 859 fun dups (rev_dups, []) = rev rev_dups 860 | dups (rev_dups, x :: xs) = 861 if member eq rev_dups x orelse not (member eq xs x) then 862 dups (rev_dups, xs) 863 else dups (x :: rev_dups, xs); 864 in dups ([], lst) end; 865 866fun has_duplicates eq = 867 let 868 fun dups [] = false 869 | dups (x :: xs) = member eq xs x orelse dups xs; 870 in dups end; 871 872 873(* matrices *) 874 875fun map_transpose f xss = 876 let 877 val n = 878 (case distinct (op =) (map length xss) of 879 [] => 0 880 | [n] => n 881 | _ => raise ListPair.UnequalLengths); 882 in map_range (fn m => f (map (fn xs => nth xs m) xss)) n end; 883 884 885 886(** lists as multisets **) 887 888fun remove1 eq x [] = [] 889 | remove1 eq x (y :: ys) = if eq (x, y) then ys else y :: remove1 eq x ys; 890 891fun combine eq xs ys = fold (remove1 eq) ys xs @ ys; 892 893fun submultiset _ ([], _) = true 894 | submultiset eq (x :: xs, ys) = member eq ys x andalso submultiset eq (xs, remove1 eq x ys); 895 896 897 898(** orders **) 899 900type 'a ord = 'a * 'a -> order; 901 902fun is_equal ord = ord = EQUAL; 903fun is_less ord = ord = LESS; 904fun is_less_equal ord = ord = LESS orelse ord = EQUAL; 905fun is_greater ord = ord = GREATER; 906fun is_greater_equal ord = ord = GREATER orelse ord = EQUAL; 907 908fun rev_order LESS = GREATER 909 | rev_order EQUAL = EQUAL 910 | rev_order GREATER = LESS; 911 912(*compose orders*) 913fun (a_ord <<< b_ord) p = (case a_ord p of EQUAL => b_ord p | ord => ord); 914 915(*assume rel is a linear strict order*) 916fun make_ord rel (x, y) = 917 if rel (x, y) then LESS 918 else if rel (y, x) then GREATER 919 else EQUAL; 920 921fun bool_ord (false, true) = LESS 922 | bool_ord (true, false) = GREATER 923 | bool_ord _ = EQUAL; 924 925val int_ord = Int.compare; 926val string_ord = String.compare; 927 928fun fast_string_ord (s1, s2) = 929 if pointer_eq (s1, s2) then EQUAL 930 else (case int_ord (size s1, size s2) of EQUAL => string_ord (s1, s2) | ord => ord); 931 932fun option_ord ord (SOME x, SOME y) = ord (x, y) 933 | option_ord _ (NONE, NONE) = EQUAL 934 | option_ord _ (NONE, SOME _) = LESS 935 | option_ord _ (SOME _, NONE) = GREATER; 936 937(*lexicographic product*) 938fun prod_ord a_ord b_ord ((x, y), (x', y')) = 939 (case a_ord (x, x') of EQUAL => b_ord (y, y') | ord => ord); 940 941(*dictionary order -- in general NOT well-founded!*) 942fun dict_ord elem_ord (x :: xs, y :: ys) = 943 (case elem_ord (x, y) of EQUAL => dict_ord elem_ord (xs, ys) | ord => ord) 944 | dict_ord _ ([], []) = EQUAL 945 | dict_ord _ ([], _ :: _) = LESS 946 | dict_ord _ (_ :: _, []) = GREATER; 947 948(*lexicographic product of lists*) 949fun list_ord elem_ord (xs, ys) = 950 (case int_ord (length xs, length ys) of EQUAL => dict_ord elem_ord (xs, ys) | ord => ord); 951 952 953(* sorting *) 954 955(*stable mergesort -- preserves order of equal elements*) 956fun mergesort unique ord = 957 let 958 fun merge (xs as x :: xs') (ys as y :: ys') = 959 (case ord (x, y) of 960 LESS => x :: merge xs' ys 961 | EQUAL => 962 if unique then merge xs ys' 963 else x :: merge xs' ys 964 | GREATER => y :: merge xs ys') 965 | merge [] ys = ys 966 | merge xs [] = xs; 967 968 fun merge_all [xs] = xs 969 | merge_all xss = merge_all (merge_pairs xss) 970 and merge_pairs (xs :: ys :: xss) = merge xs ys :: merge_pairs xss 971 | merge_pairs xss = xss; 972 973 fun runs (x :: y :: xs) = 974 (case ord (x, y) of 975 LESS => ascending y [x] xs 976 | EQUAL => 977 if unique then runs (x :: xs) 978 else ascending y [x] xs 979 | GREATER => descending y [x] xs) 980 | runs xs = [xs] 981 982 and ascending x xs (zs as y :: ys) = 983 (case ord (x, y) of 984 LESS => ascending y (x :: xs) ys 985 | EQUAL => 986 if unique then ascending x xs ys 987 else ascending y (x :: xs) ys 988 | GREATER => rev (x :: xs) :: runs zs) 989 | ascending x xs [] = [rev (x :: xs)] 990 991 and descending x xs (zs as y :: ys) = 992 (case ord (x, y) of 993 GREATER => descending y (x :: xs) ys 994 | EQUAL => 995 if unique then descending x xs ys 996 else (x :: xs) :: runs zs 997 | LESS => (x :: xs) :: runs zs) 998 | descending x xs [] = [x :: xs]; 999 1000 in merge_all o runs end; 1001 1002fun sort ord = mergesort false ord; 1003fun sort_distinct ord = mergesort true ord; 1004 1005val sort_strings = sort string_ord; 1006fun sort_by key xs = sort (string_ord o apply2 key) xs; 1007 1008 1009(* items tagged by integer index *) 1010 1011(*insert tags*) 1012fun tag_list k [] = [] 1013 | tag_list k (x :: xs) = (k:int, x) :: tag_list (k + 1) xs; 1014 1015(*remove tags and suppress duplicates -- list is assumed sorted!*) 1016fun untag_list [] = [] 1017 | untag_list [(k: int, x)] = [x] 1018 | untag_list ((k, x) :: (rest as (k', x') :: _)) = 1019 if k = k' then untag_list rest 1020 else x :: untag_list rest; 1021 1022(*return list elements in original order*) 1023fun order_list list = untag_list (sort (int_ord o apply2 fst) list); 1024 1025 1026 1027(** misc **) 1028 1029fun divide_and_conquer decomp x = 1030 let val (ys, recomb) = decomp x 1031 in recomb (map (divide_and_conquer decomp) ys) end; 1032 1033fun divide_and_conquer' decomp x s = 1034 let val ((ys, recomb), s') = decomp x s 1035 in recomb (fold_map (divide_and_conquer' decomp) ys s') end; 1036 1037 1038(*Partition a list into buckets [ bi, b(i+1), ..., bj ] 1039 putting x in bk if p(k)(x) holds. Preserve order of elements if possible.*) 1040fun partition_list p i j = 1041 let 1042 fun part (k: int) xs = 1043 if k > j then 1044 (case xs of 1045 [] => [] 1046 | _ => raise Fail "partition_list") 1047 else 1048 let val (ns, rest) = List.partition (p k) xs 1049 in ns :: part (k + 1) rest end; 1050 in part (i: int) end; 1051 1052fun partition_eq (eq: 'a * 'a -> bool) = 1053 let 1054 fun part [] = [] 1055 | part (x :: ys) = 1056 let val (xs, xs') = List.partition (fn y => eq (x, y)) ys 1057 in (x :: xs) :: part xs' end; 1058 in part end; 1059 1060 1061(* serial numbers and abstract stamps *) 1062 1063type serial = int; 1064val serial = Counter.make (); 1065val serial_string = string_of_int o serial; 1066 1067datatype stamp = Stamp of serial; 1068fun stamp () = Stamp (serial ()); 1069 1070 1071(* values of any type *) 1072 1073(*note that the builtin exception datatype may be extended by new 1074 constructors at any time*) 1075structure Any = struct type T = exn end; 1076 1077 1078(* getenv *) 1079 1080fun getenv x = 1081 (case OS.Process.getEnv x of 1082 NONE => "" 1083 | SOME y => y); 1084 1085fun getenv_strict x = 1086 (case getenv x of 1087 "" => error ("Undefined Isabelle environment variable: " ^ quote x) 1088 | y => y); 1089 1090end; 1091 1092structure Basic_Library: BASIC_LIBRARY = Library; 1093open Basic_Library; 1094