6 Basic library: functions, options, pairs, booleans, lists, integers, |
6 Basic library: functions, options, pairs, booleans, lists, integers, |
7 strings, lists as sets, association lists, generic tables, balanced trees, |
7 strings, lists as sets, association lists, generic tables, balanced trees, |
8 input / output, timing, filenames, misc functions. |
8 input / output, timing, filenames, misc functions. |
9 *) |
9 *) |
10 |
10 |
|
11 infix |> ~~ \ \\ orelf ins orf andf prefix upto downto mem union inter subset; |
|
12 |
|
13 |
|
14 structure Library = |
|
15 struct |
11 |
16 |
12 (** functions **) |
17 (** functions **) |
13 |
18 |
14 (*handy combinators*) |
19 (*handy combinators*) |
15 fun curry f x y = f (x, y); |
20 fun curry f x y = f (x, y); |
16 fun uncurry f (x, y) = f x y; |
21 fun uncurry f (x, y) = f x y; |
17 fun I x = x; |
22 fun I x = x; |
18 fun K x y = x; |
23 fun K x y = x; |
19 |
24 |
20 (*reverse apply*) |
25 (*reverse apply*) |
21 infix |>; |
|
22 fun (x |> f) = f x; |
26 fun (x |> f) = f x; |
23 |
27 |
24 (*combine two functions forming the union of their domains*) |
28 (*combine two functions forming the union of their domains*) |
25 infix orelf; |
|
26 fun f orelf g = fn x => f x handle Match => g x; |
29 fun f orelf g = fn x => f x handle Match => g x; |
27 |
30 |
28 (*application of (infix) operator to its left or right argument*) |
31 (*application of (infix) operator to its left or right argument*) |
29 fun apl (x, f) y = f (x, y); |
32 fun apl (x, f) y = f (x, y); |
30 fun apr (f, y) x = f (x, y); |
33 fun apr (f, y) x = f (x, y); |
90 fun not_equal x y = x <> y; |
93 fun not_equal x y = x <> y; |
91 |
94 |
92 |
95 |
93 (* operators for combining predicates *) |
96 (* operators for combining predicates *) |
94 |
97 |
95 infix orf; |
|
96 fun p orf q = fn x => p x orelse q x; |
98 fun p orf q = fn x => p x orelse q x; |
97 |
99 |
98 infix andf; |
|
99 fun p andf q = fn x => p x andalso q x; |
100 fun p andf q = fn x => p x andalso q x; |
100 |
101 |
101 fun notf p x = not (p x); |
102 fun notf p x = not (p x); |
102 |
103 |
103 |
104 |
270 | forall2 pred (x :: xs, y :: ys) = pred (x, y) andalso forall2 pred (xs, ys) |
271 | forall2 pred (x :: xs, y :: ys) = pred (x, y) andalso forall2 pred (xs, ys) |
271 | forall2 _ _ = raise LIST "forall2"; |
272 | forall2 _ _ = raise LIST "forall2"; |
272 |
273 |
273 (*combine two lists forming a list of pairs: |
274 (*combine two lists forming a list of pairs: |
274 [x1, ..., xn] ~~ [y1, ..., yn] ===> [(x1, y1), ..., (xn, yn)]*) |
275 [x1, ..., xn] ~~ [y1, ..., yn] ===> [(x1, y1), ..., (xn, yn)]*) |
275 infix ~~; |
|
276 fun [] ~~ [] = [] |
276 fun [] ~~ [] = [] |
277 | (x :: xs) ~~ (y :: ys) = (x, y) :: (xs ~~ ys) |
277 | (x :: xs) ~~ (y :: ys) = (x, y) :: (xs ~~ ys) |
278 | _ ~~ _ = raise LIST "~~"; |
278 | _ ~~ _ = raise LIST "~~"; |
279 |
279 |
280 |
280 |
283 fun split_list (l: ('a * 'b) list) = (map #1 l, map #2 l); |
283 fun split_list (l: ('a * 'b) list) = (map #1 l, map #2 l); |
284 |
284 |
285 |
285 |
286 (* prefixes, suffixes *) |
286 (* prefixes, suffixes *) |
287 |
287 |
288 infix prefix; |
|
289 fun [] prefix _ = true |
288 fun [] prefix _ = true |
290 | (x :: xs) prefix (y :: ys) = x = y andalso (xs prefix ys) |
289 | (x :: xs) prefix (y :: ys) = x = y andalso (xs prefix ys) |
291 | _ prefix _ = false; |
290 | _ prefix _ = false; |
292 |
291 |
293 (* [x1, ..., xi, ..., xn] ---> ([x1, ..., x(i-1)], [xi, ..., xn]) |
292 (* [x1, ..., xi, ..., xn] ---> ([x1, ..., x(i-1)], [xi, ..., xn]) |
315 |
314 |
316 |
315 |
317 (* lists of integers *) |
316 (* lists of integers *) |
318 |
317 |
319 (*make the list [from, from + 1, ..., to]*) |
318 (*make the list [from, from + 1, ..., to]*) |
320 infix upto; |
|
321 fun from upto to = |
319 fun from upto to = |
322 if from > to then [] else from :: ((from + 1) upto to); |
320 if from > to then [] else from :: ((from + 1) upto to); |
323 |
321 |
324 (*make the list [from, from - 1, ..., to]*) |
322 (*make the list [from, from - 1, ..., to]*) |
325 infix downto; |
|
326 fun from downto to = |
323 fun from downto to = |
327 if from < to then [] else from :: ((from - 1) downto to); |
324 if from < to then [] else from :: ((from - 1) downto to); |
328 |
325 |
329 (*predicate: downto0 (is, n) <=> is = [n, n - 1, ..., 0]*) |
326 (*predicate: downto0 (is, n) <=> is = [n, n - 1, ..., 0]*) |
330 fun downto0 (i :: is, n) = i = n andalso downto0 (is, n - 1) |
327 fun downto0 (i :: is, n) = i = n andalso downto0 (is, n - 1) |
427 |
424 |
428 |
425 |
429 (** lists as sets **) |
426 (** lists as sets **) |
430 |
427 |
431 (*membership in a list*) |
428 (*membership in a list*) |
432 infix mem; |
|
433 fun x mem [] = false |
429 fun x mem [] = false |
434 | x mem (y :: ys) = x = y orelse x mem ys; |
430 | x mem (y :: ys) = x = y orelse x mem ys; |
435 |
431 |
436 (*generalized membership test*) |
432 (*generalized membership test*) |
437 fun gen_mem eq (x, []) = false |
433 fun gen_mem eq (x, []) = false |
438 | gen_mem eq (x, y :: ys) = eq (x, y) orelse gen_mem eq (x, ys); |
434 | gen_mem eq (x, y :: ys) = eq (x, y) orelse gen_mem eq (x, ys); |
439 |
435 |
440 |
436 |
441 (*insertion into list if not already there*) |
437 (*insertion into list if not already there*) |
442 infix ins; |
|
443 fun x ins xs = if x mem xs then xs else x :: xs; |
438 fun x ins xs = if x mem xs then xs else x :: xs; |
444 |
439 |
445 (*generalized insertion*) |
440 (*generalized insertion*) |
446 fun gen_ins eq (x, xs) = if gen_mem eq (x, xs) then xs else x :: xs; |
441 fun gen_ins eq (x, xs) = if gen_mem eq (x, xs) then xs else x :: xs; |
447 |
442 |
448 |
443 |
449 (*union of sets represented as lists: no repetitions*) |
444 (*union of sets represented as lists: no repetitions*) |
450 infix union; |
|
451 fun xs union [] = xs |
445 fun xs union [] = xs |
452 | [] union ys = ys |
446 | [] union ys = ys |
453 | (x :: xs) union ys = xs union (x ins ys); |
447 | (x :: xs) union ys = xs union (x ins ys); |
454 |
448 |
455 (*generalized union*) |
449 (*generalized union*) |
457 | gen_union eq ([], ys) = ys |
451 | gen_union eq ([], ys) = ys |
458 | gen_union eq (x :: xs, ys) = gen_union eq (xs, gen_ins eq (x, ys)); |
452 | gen_union eq (x :: xs, ys) = gen_union eq (xs, gen_ins eq (x, ys)); |
459 |
453 |
460 |
454 |
461 (*intersection*) |
455 (*intersection*) |
462 infix inter; |
|
463 fun [] inter ys = [] |
456 fun [] inter ys = [] |
464 | (x :: xs) inter ys = |
457 | (x :: xs) inter ys = |
465 if x mem ys then x :: (xs inter ys) else xs inter ys; |
458 if x mem ys then x :: (xs inter ys) else xs inter ys; |
466 |
459 |
467 |
460 |
468 (*subset*) |
461 (*subset*) |
469 infix subset; |
|
470 fun [] subset ys = true |
462 fun [] subset ys = true |
471 | (x :: xs) subset ys = x mem ys andalso xs subset ys; |
463 | (x :: xs) subset ys = x mem ys andalso xs subset ys; |
472 |
464 |
473 fun gen_subset eq (xs, ys) = forall (fn x => gen_mem eq (x, ys)) xs; |
465 fun gen_subset eq (xs, ys) = forall (fn x => gen_mem eq (x, ys)) xs; |
474 |
466 |
478 fun eq_set (xs, ys) = |
470 fun eq_set (xs, ys) = |
479 xs = ys orelse (xs subset ys andalso ys subset xs); |
471 xs = ys orelse (xs subset ys andalso ys subset xs); |
480 |
472 |
481 |
473 |
482 (*removing an element from a list WITHOUT duplicates*) |
474 (*removing an element from a list WITHOUT duplicates*) |
483 infix \; |
|
484 fun (y :: ys) \ x = if x = y then ys else y :: (ys \ x) |
475 fun (y :: ys) \ x = if x = y then ys else y :: (ys \ x) |
485 | [] \ x = []; |
476 | [] \ x = []; |
486 |
477 |
487 infix \\; |
|
488 val op \\ = foldl (op \); |
478 val op \\ = foldl (op \); |
489 |
479 |
490 (*removing an element from a list -- possibly WITH duplicates*) |
480 (*removing an element from a list -- possibly WITH duplicates*) |
491 fun gen_rem eq (xs, y) = filter_out (fn x => eq (x, y)) xs; |
481 fun gen_rem eq (xs, y) = filter_out (fn x => eq (x, y)) xs; |
492 |
482 |