16464
|
1 |
(* Title: Pure/General/ord_list.ML
|
|
2 |
ID: $Id$
|
|
3 |
Author: Makarius
|
|
4 |
|
|
5 |
Ordered lists without duplicates -- a light-weight representation of
|
|
6 |
finite sets.
|
|
7 |
*)
|
|
8 |
|
|
9 |
signature ORD_LIST =
|
|
10 |
sig
|
|
11 |
val member: ('b * 'a -> order) -> 'a list -> 'b -> bool
|
|
12 |
val insert: ('a * 'a -> order) -> 'a -> 'a list -> 'a list
|
|
13 |
val remove: ('b * 'a -> order) -> 'b -> 'a list -> 'a list
|
|
14 |
val union: ('a * 'a -> order) -> 'a list -> 'a list -> 'a list
|
|
15 |
val inter: ('a * 'a -> order) -> 'a list -> 'a list -> 'a list
|
|
16 |
end;
|
|
17 |
|
|
18 |
structure OrdList: ORD_LIST =
|
|
19 |
struct
|
|
20 |
|
|
21 |
fun member ord list x =
|
|
22 |
let
|
|
23 |
fun memb [] = false
|
|
24 |
| memb (y :: ys) =
|
|
25 |
(case ord (x, y) of
|
|
26 |
LESS => false
|
|
27 |
| EQUAL => true
|
|
28 |
| GREATER => memb ys);
|
|
29 |
in memb list end;
|
|
30 |
|
|
31 |
exception SAME;
|
|
32 |
|
|
33 |
fun insert ord x list =
|
|
34 |
let
|
|
35 |
fun insrt [] = [x]
|
|
36 |
| insrt (lst as y :: ys) =
|
|
37 |
(case ord (x, y) of
|
|
38 |
LESS => x :: lst
|
|
39 |
| EQUAL => raise SAME
|
|
40 |
| GREATER => y :: insrt ys);
|
|
41 |
in insrt list handle SAME => list end;
|
|
42 |
|
|
43 |
fun remove ord x list =
|
|
44 |
let
|
16467
|
45 |
fun rmove [] = raise SAME
|
16468
|
46 |
| rmove (y :: ys) =
|
16464
|
47 |
(case ord (x, y) of
|
|
48 |
LESS => raise SAME
|
|
49 |
| EQUAL => ys
|
|
50 |
| GREATER => y :: rmove ys);
|
|
51 |
in rmove list handle SAME => list end;
|
|
52 |
|
|
53 |
nonfix union;
|
|
54 |
fun union _ xs [] = xs
|
|
55 |
| union _ [] ys = ys
|
|
56 |
| union ord (lst1 as x :: xs) (lst2 as y :: ys) =
|
|
57 |
(case ord (x, y) of
|
|
58 |
LESS => x :: union ord xs lst2
|
|
59 |
| EQUAL => x :: union ord xs ys
|
|
60 |
| GREATER => y :: union ord lst1 ys);
|
|
61 |
|
|
62 |
nonfix inter;
|
|
63 |
fun inter _ _ [] = []
|
|
64 |
| inter _ [] _ = []
|
|
65 |
| inter ord (lst1 as x :: xs) (lst2 as y :: ys) =
|
|
66 |
(case ord (x, y) of
|
|
67 |
LESS => inter ord xs lst2
|
|
68 |
| EQUAL => x :: inter ord xs ys
|
|
69 |
| GREATER => inter ord lst1 ys);
|
|
70 |
|
|
71 |
end;
|