author | wenzelm |
Sat, 27 Dec 1997 21:49:45 +0100 | |
changeset 4482 | 43620c417579 |
child 4485 | 697972696f71 |
permissions | -rw-r--r-- |
4482
43620c417579
Generic tables (lacking delete operation). Implemented as 2-3 trees.
wenzelm
parents:
diff
changeset
|
1 |
(* Title: Pure/table.ML |
43620c417579
Generic tables (lacking delete operation). Implemented as 2-3 trees.
wenzelm
parents:
diff
changeset
|
2 |
ID: $Id$ |
43620c417579
Generic tables (lacking delete operation). Implemented as 2-3 trees.
wenzelm
parents:
diff
changeset
|
3 |
Author: Markus Wenzel, TU Muenchen |
43620c417579
Generic tables (lacking delete operation). Implemented as 2-3 trees.
wenzelm
parents:
diff
changeset
|
4 |
|
43620c417579
Generic tables (lacking delete operation). Implemented as 2-3 trees.
wenzelm
parents:
diff
changeset
|
5 |
Generic tables (lacking delete operation). Implemented as 2-3 trees. |
43620c417579
Generic tables (lacking delete operation). Implemented as 2-3 trees.
wenzelm
parents:
diff
changeset
|
6 |
*) |
43620c417579
Generic tables (lacking delete operation). Implemented as 2-3 trees.
wenzelm
parents:
diff
changeset
|
7 |
|
43620c417579
Generic tables (lacking delete operation). Implemented as 2-3 trees.
wenzelm
parents:
diff
changeset
|
8 |
signature TABLE_DATA = |
43620c417579
Generic tables (lacking delete operation). Implemented as 2-3 trees.
wenzelm
parents:
diff
changeset
|
9 |
sig |
43620c417579
Generic tables (lacking delete operation). Implemented as 2-3 trees.
wenzelm
parents:
diff
changeset
|
10 |
type key |
43620c417579
Generic tables (lacking delete operation). Implemented as 2-3 trees.
wenzelm
parents:
diff
changeset
|
11 |
val ord: key * key -> order |
43620c417579
Generic tables (lacking delete operation). Implemented as 2-3 trees.
wenzelm
parents:
diff
changeset
|
12 |
end; |
43620c417579
Generic tables (lacking delete operation). Implemented as 2-3 trees.
wenzelm
parents:
diff
changeset
|
13 |
|
43620c417579
Generic tables (lacking delete operation). Implemented as 2-3 trees.
wenzelm
parents:
diff
changeset
|
14 |
signature TABLE = |
43620c417579
Generic tables (lacking delete operation). Implemented as 2-3 trees.
wenzelm
parents:
diff
changeset
|
15 |
sig |
43620c417579
Generic tables (lacking delete operation). Implemented as 2-3 trees.
wenzelm
parents:
diff
changeset
|
16 |
type key |
43620c417579
Generic tables (lacking delete operation). Implemented as 2-3 trees.
wenzelm
parents:
diff
changeset
|
17 |
type 'a table |
43620c417579
Generic tables (lacking delete operation). Implemented as 2-3 trees.
wenzelm
parents:
diff
changeset
|
18 |
exception DUP of key |
43620c417579
Generic tables (lacking delete operation). Implemented as 2-3 trees.
wenzelm
parents:
diff
changeset
|
19 |
exception DUPS of key list |
43620c417579
Generic tables (lacking delete operation). Implemented as 2-3 trees.
wenzelm
parents:
diff
changeset
|
20 |
val empty: 'a table |
43620c417579
Generic tables (lacking delete operation). Implemented as 2-3 trees.
wenzelm
parents:
diff
changeset
|
21 |
val is_empty: 'a table -> bool |
43620c417579
Generic tables (lacking delete operation). Implemented as 2-3 trees.
wenzelm
parents:
diff
changeset
|
22 |
val dest: 'a table -> (key * 'a) list |
43620c417579
Generic tables (lacking delete operation). Implemented as 2-3 trees.
wenzelm
parents:
diff
changeset
|
23 |
val lookup: 'a table * key -> 'a option |
43620c417579
Generic tables (lacking delete operation). Implemented as 2-3 trees.
wenzelm
parents:
diff
changeset
|
24 |
val update: (key * 'a) * 'a table -> 'a table |
43620c417579
Generic tables (lacking delete operation). Implemented as 2-3 trees.
wenzelm
parents:
diff
changeset
|
25 |
val update_new: (key * 'a) * 'a table -> 'a table (*exception DUP*) |
43620c417579
Generic tables (lacking delete operation). Implemented as 2-3 trees.
wenzelm
parents:
diff
changeset
|
26 |
val make: (key * 'a) list -> 'a table (*exception DUPS*) |
43620c417579
Generic tables (lacking delete operation). Implemented as 2-3 trees.
wenzelm
parents:
diff
changeset
|
27 |
val extend: 'a table * (key * 'a) list -> 'a table (*exception DUPS*) |
43620c417579
Generic tables (lacking delete operation). Implemented as 2-3 trees.
wenzelm
parents:
diff
changeset
|
28 |
val merge: ('a * 'a -> bool) -> 'a table * 'a table -> 'a table (*exception DUPS*) |
43620c417579
Generic tables (lacking delete operation). Implemented as 2-3 trees.
wenzelm
parents:
diff
changeset
|
29 |
val lookup_multi: 'a list table * key -> 'a list |
43620c417579
Generic tables (lacking delete operation). Implemented as 2-3 trees.
wenzelm
parents:
diff
changeset
|
30 |
val make_multi: (key * 'a) list -> 'a list table |
43620c417579
Generic tables (lacking delete operation). Implemented as 2-3 trees.
wenzelm
parents:
diff
changeset
|
31 |
val dest_multi: 'a list table -> (key * 'a) list |
43620c417579
Generic tables (lacking delete operation). Implemented as 2-3 trees.
wenzelm
parents:
diff
changeset
|
32 |
val map: ('a -> 'b) -> 'a table -> 'b table |
43620c417579
Generic tables (lacking delete operation). Implemented as 2-3 trees.
wenzelm
parents:
diff
changeset
|
33 |
end; |
43620c417579
Generic tables (lacking delete operation). Implemented as 2-3 trees.
wenzelm
parents:
diff
changeset
|
34 |
|
43620c417579
Generic tables (lacking delete operation). Implemented as 2-3 trees.
wenzelm
parents:
diff
changeset
|
35 |
functor TableFun(Data: TABLE_DATA): TABLE = |
43620c417579
Generic tables (lacking delete operation). Implemented as 2-3 trees.
wenzelm
parents:
diff
changeset
|
36 |
struct |
43620c417579
Generic tables (lacking delete operation). Implemented as 2-3 trees.
wenzelm
parents:
diff
changeset
|
37 |
|
43620c417579
Generic tables (lacking delete operation). Implemented as 2-3 trees.
wenzelm
parents:
diff
changeset
|
38 |
|
43620c417579
Generic tables (lacking delete operation). Implemented as 2-3 trees.
wenzelm
parents:
diff
changeset
|
39 |
(* datatype table *) |
43620c417579
Generic tables (lacking delete operation). Implemented as 2-3 trees.
wenzelm
parents:
diff
changeset
|
40 |
|
43620c417579
Generic tables (lacking delete operation). Implemented as 2-3 trees.
wenzelm
parents:
diff
changeset
|
41 |
type key = Data.key; |
43620c417579
Generic tables (lacking delete operation). Implemented as 2-3 trees.
wenzelm
parents:
diff
changeset
|
42 |
|
43620c417579
Generic tables (lacking delete operation). Implemented as 2-3 trees.
wenzelm
parents:
diff
changeset
|
43 |
datatype 'a table = |
43620c417579
Generic tables (lacking delete operation). Implemented as 2-3 trees.
wenzelm
parents:
diff
changeset
|
44 |
Empty | |
43620c417579
Generic tables (lacking delete operation). Implemented as 2-3 trees.
wenzelm
parents:
diff
changeset
|
45 |
Branch2 of 'a table * (key * 'a) * 'a table | |
43620c417579
Generic tables (lacking delete operation). Implemented as 2-3 trees.
wenzelm
parents:
diff
changeset
|
46 |
Branch3 of 'a table * (key * 'a) * 'a table * (key * 'a) * 'a table; |
43620c417579
Generic tables (lacking delete operation). Implemented as 2-3 trees.
wenzelm
parents:
diff
changeset
|
47 |
|
43620c417579
Generic tables (lacking delete operation). Implemented as 2-3 trees.
wenzelm
parents:
diff
changeset
|
48 |
exception DUP of key; |
43620c417579
Generic tables (lacking delete operation). Implemented as 2-3 trees.
wenzelm
parents:
diff
changeset
|
49 |
exception DUPS of key list; |
43620c417579
Generic tables (lacking delete operation). Implemented as 2-3 trees.
wenzelm
parents:
diff
changeset
|
50 |
|
43620c417579
Generic tables (lacking delete operation). Implemented as 2-3 trees.
wenzelm
parents:
diff
changeset
|
51 |
|
43620c417579
Generic tables (lacking delete operation). Implemented as 2-3 trees.
wenzelm
parents:
diff
changeset
|
52 |
val empty = Empty; |
43620c417579
Generic tables (lacking delete operation). Implemented as 2-3 trees.
wenzelm
parents:
diff
changeset
|
53 |
|
43620c417579
Generic tables (lacking delete operation). Implemented as 2-3 trees.
wenzelm
parents:
diff
changeset
|
54 |
fun is_empty Empty = true |
43620c417579
Generic tables (lacking delete operation). Implemented as 2-3 trees.
wenzelm
parents:
diff
changeset
|
55 |
| is_empty _ = false; |
43620c417579
Generic tables (lacking delete operation). Implemented as 2-3 trees.
wenzelm
parents:
diff
changeset
|
56 |
|
43620c417579
Generic tables (lacking delete operation). Implemented as 2-3 trees.
wenzelm
parents:
diff
changeset
|
57 |
fun dest Empty = [] |
43620c417579
Generic tables (lacking delete operation). Implemented as 2-3 trees.
wenzelm
parents:
diff
changeset
|
58 |
| dest (Branch2 (left, p, right)) = dest left @ [p] @ dest right |
43620c417579
Generic tables (lacking delete operation). Implemented as 2-3 trees.
wenzelm
parents:
diff
changeset
|
59 |
| dest (Branch3 (left, p1, mid, p2, right)) = |
43620c417579
Generic tables (lacking delete operation). Implemented as 2-3 trees.
wenzelm
parents:
diff
changeset
|
60 |
dest left @ [p1] @ dest mid @ [p2] @ dest right; |
43620c417579
Generic tables (lacking delete operation). Implemented as 2-3 trees.
wenzelm
parents:
diff
changeset
|
61 |
|
43620c417579
Generic tables (lacking delete operation). Implemented as 2-3 trees.
wenzelm
parents:
diff
changeset
|
62 |
|
43620c417579
Generic tables (lacking delete operation). Implemented as 2-3 trees.
wenzelm
parents:
diff
changeset
|
63 |
(* lookup *) |
43620c417579
Generic tables (lacking delete operation). Implemented as 2-3 trees.
wenzelm
parents:
diff
changeset
|
64 |
|
43620c417579
Generic tables (lacking delete operation). Implemented as 2-3 trees.
wenzelm
parents:
diff
changeset
|
65 |
fun lookup (Empty, _) = None |
43620c417579
Generic tables (lacking delete operation). Implemented as 2-3 trees.
wenzelm
parents:
diff
changeset
|
66 |
| lookup (Branch2 (left, (k, x), right), key) = |
43620c417579
Generic tables (lacking delete operation). Implemented as 2-3 trees.
wenzelm
parents:
diff
changeset
|
67 |
(case Data.ord (key, k) of |
43620c417579
Generic tables (lacking delete operation). Implemented as 2-3 trees.
wenzelm
parents:
diff
changeset
|
68 |
LESS => lookup (left, key) |
43620c417579
Generic tables (lacking delete operation). Implemented as 2-3 trees.
wenzelm
parents:
diff
changeset
|
69 |
| EQUAL => Some x |
43620c417579
Generic tables (lacking delete operation). Implemented as 2-3 trees.
wenzelm
parents:
diff
changeset
|
70 |
| GREATER => lookup (right, key)) |
43620c417579
Generic tables (lacking delete operation). Implemented as 2-3 trees.
wenzelm
parents:
diff
changeset
|
71 |
| lookup (Branch3 (left, (k1, x1), mid, (k2, x2), right), key) = |
43620c417579
Generic tables (lacking delete operation). Implemented as 2-3 trees.
wenzelm
parents:
diff
changeset
|
72 |
(case Data.ord (key, k1) of |
43620c417579
Generic tables (lacking delete operation). Implemented as 2-3 trees.
wenzelm
parents:
diff
changeset
|
73 |
LESS => lookup (left, key) |
43620c417579
Generic tables (lacking delete operation). Implemented as 2-3 trees.
wenzelm
parents:
diff
changeset
|
74 |
| EQUAL => Some x1 |
43620c417579
Generic tables (lacking delete operation). Implemented as 2-3 trees.
wenzelm
parents:
diff
changeset
|
75 |
| GREATER => |
43620c417579
Generic tables (lacking delete operation). Implemented as 2-3 trees.
wenzelm
parents:
diff
changeset
|
76 |
(case Data.ord (key, k2) of |
43620c417579
Generic tables (lacking delete operation). Implemented as 2-3 trees.
wenzelm
parents:
diff
changeset
|
77 |
LESS => lookup (mid, key) |
43620c417579
Generic tables (lacking delete operation). Implemented as 2-3 trees.
wenzelm
parents:
diff
changeset
|
78 |
| EQUAL => Some x2 |
43620c417579
Generic tables (lacking delete operation). Implemented as 2-3 trees.
wenzelm
parents:
diff
changeset
|
79 |
| GREATER => lookup (right, key))); |
43620c417579
Generic tables (lacking delete operation). Implemented as 2-3 trees.
wenzelm
parents:
diff
changeset
|
80 |
|
43620c417579
Generic tables (lacking delete operation). Implemented as 2-3 trees.
wenzelm
parents:
diff
changeset
|
81 |
|
43620c417579
Generic tables (lacking delete operation). Implemented as 2-3 trees.
wenzelm
parents:
diff
changeset
|
82 |
(* update *) |
43620c417579
Generic tables (lacking delete operation). Implemented as 2-3 trees.
wenzelm
parents:
diff
changeset
|
83 |
|
43620c417579
Generic tables (lacking delete operation). Implemented as 2-3 trees.
wenzelm
parents:
diff
changeset
|
84 |
fun compare (k1, _) (k2, _) = Data.ord (k1, k2); |
43620c417579
Generic tables (lacking delete operation). Implemented as 2-3 trees.
wenzelm
parents:
diff
changeset
|
85 |
|
43620c417579
Generic tables (lacking delete operation). Implemented as 2-3 trees.
wenzelm
parents:
diff
changeset
|
86 |
datatype 'a growth = |
43620c417579
Generic tables (lacking delete operation). Implemented as 2-3 trees.
wenzelm
parents:
diff
changeset
|
87 |
Stay of 'a table | |
43620c417579
Generic tables (lacking delete operation). Implemented as 2-3 trees.
wenzelm
parents:
diff
changeset
|
88 |
Sprout of 'a table * (key * 'a) * 'a table; |
43620c417579
Generic tables (lacking delete operation). Implemented as 2-3 trees.
wenzelm
parents:
diff
changeset
|
89 |
|
43620c417579
Generic tables (lacking delete operation). Implemented as 2-3 trees.
wenzelm
parents:
diff
changeset
|
90 |
fun insert pair Empty = Sprout (Empty, pair, Empty) |
43620c417579
Generic tables (lacking delete operation). Implemented as 2-3 trees.
wenzelm
parents:
diff
changeset
|
91 |
| insert pair (Branch2 (left, p, right)) = |
43620c417579
Generic tables (lacking delete operation). Implemented as 2-3 trees.
wenzelm
parents:
diff
changeset
|
92 |
(case compare pair p of |
43620c417579
Generic tables (lacking delete operation). Implemented as 2-3 trees.
wenzelm
parents:
diff
changeset
|
93 |
LESS => |
43620c417579
Generic tables (lacking delete operation). Implemented as 2-3 trees.
wenzelm
parents:
diff
changeset
|
94 |
(case insert pair left of |
43620c417579
Generic tables (lacking delete operation). Implemented as 2-3 trees.
wenzelm
parents:
diff
changeset
|
95 |
Stay left' => Stay (Branch2 (left', p, right)) |
43620c417579
Generic tables (lacking delete operation). Implemented as 2-3 trees.
wenzelm
parents:
diff
changeset
|
96 |
| Sprout (left1, q, left2) => Stay (Branch3 (left1, q, left2, p, right))) |
43620c417579
Generic tables (lacking delete operation). Implemented as 2-3 trees.
wenzelm
parents:
diff
changeset
|
97 |
| EQUAL => Stay (Branch2 (left, pair, right)) |
43620c417579
Generic tables (lacking delete operation). Implemented as 2-3 trees.
wenzelm
parents:
diff
changeset
|
98 |
| GREATER => |
43620c417579
Generic tables (lacking delete operation). Implemented as 2-3 trees.
wenzelm
parents:
diff
changeset
|
99 |
(case insert pair right of |
43620c417579
Generic tables (lacking delete operation). Implemented as 2-3 trees.
wenzelm
parents:
diff
changeset
|
100 |
Stay right' => Stay (Branch2 (left, p, right')) |
43620c417579
Generic tables (lacking delete operation). Implemented as 2-3 trees.
wenzelm
parents:
diff
changeset
|
101 |
| Sprout (right1, q, right2) => |
43620c417579
Generic tables (lacking delete operation). Implemented as 2-3 trees.
wenzelm
parents:
diff
changeset
|
102 |
Stay (Branch3 (left, p, right1, q, right2)))) |
43620c417579
Generic tables (lacking delete operation). Implemented as 2-3 trees.
wenzelm
parents:
diff
changeset
|
103 |
| insert pair (Branch3 (left, p1, mid, p2, right)) = |
43620c417579
Generic tables (lacking delete operation). Implemented as 2-3 trees.
wenzelm
parents:
diff
changeset
|
104 |
(case compare pair p1 of |
43620c417579
Generic tables (lacking delete operation). Implemented as 2-3 trees.
wenzelm
parents:
diff
changeset
|
105 |
LESS => |
43620c417579
Generic tables (lacking delete operation). Implemented as 2-3 trees.
wenzelm
parents:
diff
changeset
|
106 |
(case insert pair left of |
43620c417579
Generic tables (lacking delete operation). Implemented as 2-3 trees.
wenzelm
parents:
diff
changeset
|
107 |
Stay left' => Stay (Branch3 (left', p1, mid, p2, right)) |
43620c417579
Generic tables (lacking delete operation). Implemented as 2-3 trees.
wenzelm
parents:
diff
changeset
|
108 |
| Sprout (left1, q, left2) => |
43620c417579
Generic tables (lacking delete operation). Implemented as 2-3 trees.
wenzelm
parents:
diff
changeset
|
109 |
Sprout (Branch2 (left1, q, left2), p1, Branch2 (mid, p2, right))) |
43620c417579
Generic tables (lacking delete operation). Implemented as 2-3 trees.
wenzelm
parents:
diff
changeset
|
110 |
| EQUAL => Stay (Branch3 (left, pair, mid, p2, right)) |
43620c417579
Generic tables (lacking delete operation). Implemented as 2-3 trees.
wenzelm
parents:
diff
changeset
|
111 |
| GREATER => |
43620c417579
Generic tables (lacking delete operation). Implemented as 2-3 trees.
wenzelm
parents:
diff
changeset
|
112 |
(case compare pair p2 of |
43620c417579
Generic tables (lacking delete operation). Implemented as 2-3 trees.
wenzelm
parents:
diff
changeset
|
113 |
LESS => |
43620c417579
Generic tables (lacking delete operation). Implemented as 2-3 trees.
wenzelm
parents:
diff
changeset
|
114 |
(case insert pair mid of |
43620c417579
Generic tables (lacking delete operation). Implemented as 2-3 trees.
wenzelm
parents:
diff
changeset
|
115 |
Stay mid' => Stay (Branch3 (left, p1, mid', p2, right)) |
43620c417579
Generic tables (lacking delete operation). Implemented as 2-3 trees.
wenzelm
parents:
diff
changeset
|
116 |
| Sprout (mid1, q, mid2) => |
43620c417579
Generic tables (lacking delete operation). Implemented as 2-3 trees.
wenzelm
parents:
diff
changeset
|
117 |
Sprout (Branch2 (left, p1, mid1), q, Branch2 (mid2, p2, right))) |
43620c417579
Generic tables (lacking delete operation). Implemented as 2-3 trees.
wenzelm
parents:
diff
changeset
|
118 |
| EQUAL => Stay (Branch3 (left, p1, mid, pair, right)) |
43620c417579
Generic tables (lacking delete operation). Implemented as 2-3 trees.
wenzelm
parents:
diff
changeset
|
119 |
| GREATER => |
43620c417579
Generic tables (lacking delete operation). Implemented as 2-3 trees.
wenzelm
parents:
diff
changeset
|
120 |
(case insert pair right of |
43620c417579
Generic tables (lacking delete operation). Implemented as 2-3 trees.
wenzelm
parents:
diff
changeset
|
121 |
Stay right' => Stay (Branch3 (left, p1, mid, p2, right')) |
43620c417579
Generic tables (lacking delete operation). Implemented as 2-3 trees.
wenzelm
parents:
diff
changeset
|
122 |
| Sprout (right1, q, right2) => |
43620c417579
Generic tables (lacking delete operation). Implemented as 2-3 trees.
wenzelm
parents:
diff
changeset
|
123 |
Sprout (Branch2 (left, p1, mid), p2, Branch2 (right1, q, right2))))); |
43620c417579
Generic tables (lacking delete operation). Implemented as 2-3 trees.
wenzelm
parents:
diff
changeset
|
124 |
|
43620c417579
Generic tables (lacking delete operation). Implemented as 2-3 trees.
wenzelm
parents:
diff
changeset
|
125 |
fun update (pair, tab) = |
43620c417579
Generic tables (lacking delete operation). Implemented as 2-3 trees.
wenzelm
parents:
diff
changeset
|
126 |
(case insert pair tab of |
43620c417579
Generic tables (lacking delete operation). Implemented as 2-3 trees.
wenzelm
parents:
diff
changeset
|
127 |
Stay tab => tab |
43620c417579
Generic tables (lacking delete operation). Implemented as 2-3 trees.
wenzelm
parents:
diff
changeset
|
128 |
| Sprout br => Branch2 br); |
43620c417579
Generic tables (lacking delete operation). Implemented as 2-3 trees.
wenzelm
parents:
diff
changeset
|
129 |
|
43620c417579
Generic tables (lacking delete operation). Implemented as 2-3 trees.
wenzelm
parents:
diff
changeset
|
130 |
fun update_new (pair as (key, _), tab) = |
43620c417579
Generic tables (lacking delete operation). Implemented as 2-3 trees.
wenzelm
parents:
diff
changeset
|
131 |
(case lookup (tab, key) of |
43620c417579
Generic tables (lacking delete operation). Implemented as 2-3 trees.
wenzelm
parents:
diff
changeset
|
132 |
None => update (pair, tab) |
43620c417579
Generic tables (lacking delete operation). Implemented as 2-3 trees.
wenzelm
parents:
diff
changeset
|
133 |
| Some _ => raise DUP key); |
43620c417579
Generic tables (lacking delete operation). Implemented as 2-3 trees.
wenzelm
parents:
diff
changeset
|
134 |
|
43620c417579
Generic tables (lacking delete operation). Implemented as 2-3 trees.
wenzelm
parents:
diff
changeset
|
135 |
|
43620c417579
Generic tables (lacking delete operation). Implemented as 2-3 trees.
wenzelm
parents:
diff
changeset
|
136 |
(* make, extend, merge tables *) |
43620c417579
Generic tables (lacking delete operation). Implemented as 2-3 trees.
wenzelm
parents:
diff
changeset
|
137 |
|
43620c417579
Generic tables (lacking delete operation). Implemented as 2-3 trees.
wenzelm
parents:
diff
changeset
|
138 |
fun add eq ((tab, dups), (key, x)) = |
43620c417579
Generic tables (lacking delete operation). Implemented as 2-3 trees.
wenzelm
parents:
diff
changeset
|
139 |
(case lookup (tab, key) of |
43620c417579
Generic tables (lacking delete operation). Implemented as 2-3 trees.
wenzelm
parents:
diff
changeset
|
140 |
None => (update ((key, x), tab), dups) |
43620c417579
Generic tables (lacking delete operation). Implemented as 2-3 trees.
wenzelm
parents:
diff
changeset
|
141 |
| Some x' => |
43620c417579
Generic tables (lacking delete operation). Implemented as 2-3 trees.
wenzelm
parents:
diff
changeset
|
142 |
if eq (x, x') then (tab, dups) |
43620c417579
Generic tables (lacking delete operation). Implemented as 2-3 trees.
wenzelm
parents:
diff
changeset
|
143 |
else (tab, dups @ [key])); |
43620c417579
Generic tables (lacking delete operation). Implemented as 2-3 trees.
wenzelm
parents:
diff
changeset
|
144 |
|
43620c417579
Generic tables (lacking delete operation). Implemented as 2-3 trees.
wenzelm
parents:
diff
changeset
|
145 |
fun enter eq (tab, pairs) = |
43620c417579
Generic tables (lacking delete operation). Implemented as 2-3 trees.
wenzelm
parents:
diff
changeset
|
146 |
(case foldl (add eq) ((tab, []), pairs) of |
43620c417579
Generic tables (lacking delete operation). Implemented as 2-3 trees.
wenzelm
parents:
diff
changeset
|
147 |
(tab', []) => tab' |
43620c417579
Generic tables (lacking delete operation). Implemented as 2-3 trees.
wenzelm
parents:
diff
changeset
|
148 |
| (_, dups) => raise DUPS dups); |
43620c417579
Generic tables (lacking delete operation). Implemented as 2-3 trees.
wenzelm
parents:
diff
changeset
|
149 |
|
43620c417579
Generic tables (lacking delete operation). Implemented as 2-3 trees.
wenzelm
parents:
diff
changeset
|
150 |
fun extend tab_pairs = enter (K false) tab_pairs; |
43620c417579
Generic tables (lacking delete operation). Implemented as 2-3 trees.
wenzelm
parents:
diff
changeset
|
151 |
fun make pairs = extend (empty, pairs); |
43620c417579
Generic tables (lacking delete operation). Implemented as 2-3 trees.
wenzelm
parents:
diff
changeset
|
152 |
fun merge eq (tab1, tab2) = enter eq (tab1, dest tab2); |
43620c417579
Generic tables (lacking delete operation). Implemented as 2-3 trees.
wenzelm
parents:
diff
changeset
|
153 |
|
43620c417579
Generic tables (lacking delete operation). Implemented as 2-3 trees.
wenzelm
parents:
diff
changeset
|
154 |
|
43620c417579
Generic tables (lacking delete operation). Implemented as 2-3 trees.
wenzelm
parents:
diff
changeset
|
155 |
(* tables with multiple entries per key (preserving order) *) |
43620c417579
Generic tables (lacking delete operation). Implemented as 2-3 trees.
wenzelm
parents:
diff
changeset
|
156 |
|
43620c417579
Generic tables (lacking delete operation). Implemented as 2-3 trees.
wenzelm
parents:
diff
changeset
|
157 |
fun lookup_multi tab_key = if_none (lookup tab_key) []; |
43620c417579
Generic tables (lacking delete operation). Implemented as 2-3 trees.
wenzelm
parents:
diff
changeset
|
158 |
|
43620c417579
Generic tables (lacking delete operation). Implemented as 2-3 trees.
wenzelm
parents:
diff
changeset
|
159 |
fun cons_entry ((key, entry), tab) = |
43620c417579
Generic tables (lacking delete operation). Implemented as 2-3 trees.
wenzelm
parents:
diff
changeset
|
160 |
update ((key, entry :: lookup_multi (tab, key)), tab); |
43620c417579
Generic tables (lacking delete operation). Implemented as 2-3 trees.
wenzelm
parents:
diff
changeset
|
161 |
|
43620c417579
Generic tables (lacking delete operation). Implemented as 2-3 trees.
wenzelm
parents:
diff
changeset
|
162 |
fun make_multi pairs = foldr cons_entry (pairs, empty); |
43620c417579
Generic tables (lacking delete operation). Implemented as 2-3 trees.
wenzelm
parents:
diff
changeset
|
163 |
|
43620c417579
Generic tables (lacking delete operation). Implemented as 2-3 trees.
wenzelm
parents:
diff
changeset
|
164 |
fun dest_multi tab = |
43620c417579
Generic tables (lacking delete operation). Implemented as 2-3 trees.
wenzelm
parents:
diff
changeset
|
165 |
flat (map (fn (key, xs) => map (pair key) xs) (dest tab)); |
43620c417579
Generic tables (lacking delete operation). Implemented as 2-3 trees.
wenzelm
parents:
diff
changeset
|
166 |
|
43620c417579
Generic tables (lacking delete operation). Implemented as 2-3 trees.
wenzelm
parents:
diff
changeset
|
167 |
|
43620c417579
Generic tables (lacking delete operation). Implemented as 2-3 trees.
wenzelm
parents:
diff
changeset
|
168 |
(* map *) |
43620c417579
Generic tables (lacking delete operation). Implemented as 2-3 trees.
wenzelm
parents:
diff
changeset
|
169 |
|
43620c417579
Generic tables (lacking delete operation). Implemented as 2-3 trees.
wenzelm
parents:
diff
changeset
|
170 |
fun map _ Empty = Empty |
43620c417579
Generic tables (lacking delete operation). Implemented as 2-3 trees.
wenzelm
parents:
diff
changeset
|
171 |
| map f (Branch2 (left, (k, x), right)) = |
43620c417579
Generic tables (lacking delete operation). Implemented as 2-3 trees.
wenzelm
parents:
diff
changeset
|
172 |
Branch2 (map f left, (k, f x), map f right) |
43620c417579
Generic tables (lacking delete operation). Implemented as 2-3 trees.
wenzelm
parents:
diff
changeset
|
173 |
| map f (Branch3 (left, (k1, x1), mid, (k2, x2), right)) = |
43620c417579
Generic tables (lacking delete operation). Implemented as 2-3 trees.
wenzelm
parents:
diff
changeset
|
174 |
Branch3 (map f left, (k1, f x1), map f mid, (k2, f x2), map f right); |
43620c417579
Generic tables (lacking delete operation). Implemented as 2-3 trees.
wenzelm
parents:
diff
changeset
|
175 |
|
43620c417579
Generic tables (lacking delete operation). Implemented as 2-3 trees.
wenzelm
parents:
diff
changeset
|
176 |
|
43620c417579
Generic tables (lacking delete operation). Implemented as 2-3 trees.
wenzelm
parents:
diff
changeset
|
177 |
end; |
43620c417579
Generic tables (lacking delete operation). Implemented as 2-3 trees.
wenzelm
parents:
diff
changeset
|
178 |
|
43620c417579
Generic tables (lacking delete operation). Implemented as 2-3 trees.
wenzelm
parents:
diff
changeset
|
179 |
|
43620c417579
Generic tables (lacking delete operation). Implemented as 2-3 trees.
wenzelm
parents:
diff
changeset
|
180 |
(*tables indexed by strings*) |
43620c417579
Generic tables (lacking delete operation). Implemented as 2-3 trees.
wenzelm
parents:
diff
changeset
|
181 |
structure Symtab = TableFun(type key = string val ord = string_ord); |
43620c417579
Generic tables (lacking delete operation). Implemented as 2-3 trees.
wenzelm
parents:
diff
changeset
|
182 |
|
43620c417579
Generic tables (lacking delete operation). Implemented as 2-3 trees.
wenzelm
parents:
diff
changeset
|
183 |
(* FIXME demo *) |
43620c417579
Generic tables (lacking delete operation). Implemented as 2-3 trees.
wenzelm
parents:
diff
changeset
|
184 |
structure IntTab = TableFun(type key = int val ord = int_ord); |
43620c417579
Generic tables (lacking delete operation). Implemented as 2-3 trees.
wenzelm
parents:
diff
changeset
|
185 |
val make = IntTab.make o map (rpair ()); |
43620c417579
Generic tables (lacking delete operation). Implemented as 2-3 trees.
wenzelm
parents:
diff
changeset
|
186 |
fun dest tab = IntTab.dest tab |> map fst; |