author | wenzelm |
Fri, 17 Mar 2017 20:33:27 +0100 | |
changeset 65292 | e3bd1e7ddd23 |
parent 63511 | 1c2c045decb3 |
child 66935 | d0f12783cd80 |
permissions | -rw-r--r-- |
6118 | 1 |
(* Title: Pure/General/table.ML |
15014 | 2 |
Author: Markus Wenzel and Stefan Berghofer, TU Muenchen |
5015 | 3 |
|
16342 | 4 |
Generic tables. Efficient purely functional implementation using |
5 |
balanced 2-3 trees. |
|
5015 | 6 |
*) |
7 |
||
8 |
signature KEY = |
|
9 |
sig |
|
10 |
type key |
|
11 |
val ord: key * key -> order |
|
12 |
end; |
|
13 |
||
14 |
signature TABLE = |
|
15 |
sig |
|
16 |
type key |
|
17 |
type 'a table |
|
18 |
exception DUP of key |
|
19031 | 19 |
exception SAME |
15014 | 20 |
exception UNDEF of key |
5015 | 21 |
val empty: 'a table |
22 |
val is_empty: 'a table -> bool |
|
39020 | 23 |
val map: (key -> 'a -> 'b) -> 'a table -> 'b table |
16446 | 24 |
val fold: (key * 'b -> 'a -> 'a) -> 'b table -> 'a -> 'a |
28334 | 25 |
val fold_rev: (key * 'b -> 'a -> 'a) -> 'b table -> 'a -> 'a |
5015 | 26 |
val dest: 'a table -> (key * 'a) list |
5681 | 27 |
val keys: 'a table -> key list |
52049 | 28 |
val min: 'a table -> (key * 'a) option |
29 |
val max: 'a table -> (key * 'a) option |
|
35012
c3e3ac3ca091
removed unused "boundary" of Table/Graph.get_first;
wenzelm
parents:
33162
diff
changeset
|
30 |
val get_first: (key * 'a -> 'b option) -> 'a table -> 'b option |
27508 | 31 |
val exists: (key * 'a -> bool) -> 'a table -> bool |
32 |
val forall: (key * 'a -> bool) -> 'a table -> bool |
|
43792
d5803c3d537a
Table.lookup_key and Graph.get_entry allow to retrieve the original key, which is not necessarily identical to the given one;
wenzelm
parents:
39020
diff
changeset
|
33 |
val lookup_key: 'a table -> key -> (key * 'a) option |
31616 | 34 |
val lookup: 'a table -> key -> 'a option |
16887 | 35 |
val defined: 'a table -> key -> bool |
31209 | 36 |
val update: key * 'a -> 'a table -> 'a table |
37 |
val update_new: key * 'a -> 'a table -> 'a table (*exception DUP*) |
|
17179 | 38 |
val default: key * 'a -> 'a table -> 'a table |
56051 | 39 |
val map_entry: key -> ('a -> 'a) (*exception SAME*) -> 'a table -> 'a table |
31209 | 40 |
val map_default: key * 'a -> ('a -> 'a) -> 'a table -> 'a table |
23655
d2d1138e0ddc
replaced exception TableFun/GraphFun.DUPS by TableFun/GraphFun.DUP;
wenzelm
parents:
21065
diff
changeset
|
41 |
val make: (key * 'a) list -> 'a table (*exception DUP*) |
56051 | 42 |
val join: (key -> 'a * 'a -> 'a) (*exception SAME*) -> |
23655
d2d1138e0ddc
replaced exception TableFun/GraphFun.DUPS by TableFun/GraphFun.DUP;
wenzelm
parents:
21065
diff
changeset
|
43 |
'a table * 'a table -> 'a table (*exception DUP*) |
d2d1138e0ddc
replaced exception TableFun/GraphFun.DUPS by TableFun/GraphFun.DUP;
wenzelm
parents:
21065
diff
changeset
|
44 |
val merge: ('a * 'a -> bool) -> 'a table * 'a table -> 'a table (*exception DUP*) |
15665 | 45 |
val delete: key -> 'a table -> 'a table (*exception UNDEF*) |
15761 | 46 |
val delete_safe: key -> 'a table -> 'a table |
16466 | 47 |
val member: ('b * 'a -> bool) -> 'a table -> key * 'b -> bool |
15761 | 48 |
val insert: ('a * 'a -> bool) -> key * 'a -> 'a table -> 'a table (*exception DUP*) |
16139 | 49 |
val remove: ('b * 'a -> bool) -> key * 'b -> 'a table -> 'a table |
18946 | 50 |
val lookup_list: 'a list table -> key -> 'a list |
31209 | 51 |
val cons_list: key * 'a -> 'a list table -> 'a list table |
19506 | 52 |
val insert_list: ('a * 'a -> bool) -> key * 'a -> 'a list table -> 'a list table |
18946 | 53 |
val remove_list: ('b * 'a -> bool) -> key * 'b -> 'a list table -> 'a list table |
25391 | 54 |
val update_list: ('a * 'a -> bool) -> key * 'a -> 'a list table -> 'a list table |
18946 | 55 |
val make_list: (key * 'a) list -> 'a list table |
56 |
val dest_list: 'a list table -> (key * 'a) list |
|
33162 | 57 |
val merge_list: ('a * 'a -> bool) -> 'a list table * 'a list table -> 'a list table |
50234 | 58 |
type set = unit table |
63511 | 59 |
val insert_set: key -> set -> set |
59012
f4e9bd04e1d5
clarified Table.make_set: duplicate arguments are allowed, like Table.make_list or Scala Set() formation;
wenzelm
parents:
56051
diff
changeset
|
60 |
val make_set: key list -> set |
5015 | 61 |
end; |
62 |
||
31971
8c1b845ed105
renamed functor TableFun to Table, and GraphFun to Graph;
wenzelm
parents:
31621
diff
changeset
|
63 |
functor Table(Key: KEY): TABLE = |
5015 | 64 |
struct |
65 |
||
66 |
||
67 |
(* datatype table *) |
|
68 |
||
69 |
type key = Key.key; |
|
70 |
||
71 |
datatype 'a table = |
|
72 |
Empty | |
|
73 |
Branch2 of 'a table * (key * 'a) * 'a table | |
|
74 |
Branch3 of 'a table * (key * 'a) * 'a table * (key * 'a) * 'a table; |
|
75 |
||
76 |
exception DUP of key; |
|
77 |
||
78 |
||
5681 | 79 |
(* empty *) |
80 |
||
5015 | 81 |
val empty = Empty; |
82 |
||
83 |
fun is_empty Empty = true |
|
84 |
| is_empty _ = false; |
|
85 |
||
5681 | 86 |
|
87 |
(* map and fold combinators *) |
|
88 |
||
16657 | 89 |
fun map_table f = |
90 |
let |
|
91 |
fun map Empty = Empty |
|
92 |
| map (Branch2 (left, (k, x), right)) = |
|
93 |
Branch2 (map left, (k, f k x), map right) |
|
94 |
| map (Branch3 (left, (k1, x1), mid, (k2, x2), right)) = |
|
95 |
Branch3 (map left, (k1, f k1 x1), map mid, (k2, f k2 x2), map right); |
|
96 |
in map end; |
|
5681 | 97 |
|
16657 | 98 |
fun fold_table f = |
99 |
let |
|
100 |
fun fold Empty x = x |
|
101 |
| fold (Branch2 (left, p, right)) x = |
|
102 |
fold right (f p (fold left x)) |
|
103 |
| fold (Branch3 (left, p1, mid, p2, right)) x = |
|
104 |
fold right (f p2 (fold mid (f p1 (fold left x)))); |
|
105 |
in fold end; |
|
5681 | 106 |
|
28334 | 107 |
fun fold_rev_table f = |
108 |
let |
|
109 |
fun fold Empty x = x |
|
110 |
| fold (Branch2 (left, p, right)) x = |
|
111 |
fold left (f p (fold right x)) |
|
112 |
| fold (Branch3 (left, p1, mid, p2, right)) x = |
|
113 |
fold left (f p1 (fold mid (f p2 (fold right x)))); |
|
114 |
in fold end; |
|
115 |
||
116 |
fun dest tab = fold_rev_table cons tab []; |
|
117 |
fun keys tab = fold_rev_table (cons o #1) tab []; |
|
16192 | 118 |
|
27508 | 119 |
|
52049 | 120 |
(* min/max entries *) |
5015 | 121 |
|
52049 | 122 |
fun min Empty = NONE |
123 |
| min (Branch2 (Empty, p, _)) = SOME p |
|
124 |
| min (Branch3 (Empty, p, _, _, _)) = SOME p |
|
125 |
| min (Branch2 (left, _, _)) = min left |
|
126 |
| min (Branch3 (left, _, _, _, _)) = min left; |
|
8409 | 127 |
|
52049 | 128 |
fun max Empty = NONE |
129 |
| max (Branch2 (_, p, Empty)) = SOME p |
|
130 |
| max (Branch3 (_, _, _, p, Empty)) = SOME p |
|
131 |
| max (Branch2 (_, _, right)) = max right |
|
132 |
| max (Branch3 (_, _, _, _, right)) = max right; |
|
15665 | 133 |
|
5015 | 134 |
|
31616 | 135 |
(* get_first *) |
136 |
||
35012
c3e3ac3ca091
removed unused "boundary" of Table/Graph.get_first;
wenzelm
parents:
33162
diff
changeset
|
137 |
fun get_first f = |
31616 | 138 |
let |
35012
c3e3ac3ca091
removed unused "boundary" of Table/Graph.get_first;
wenzelm
parents:
33162
diff
changeset
|
139 |
fun get Empty = NONE |
31618
2e4430b84303
improved get_first: check boundary before entering subtrees;
wenzelm
parents:
31616
diff
changeset
|
140 |
| get (Branch2 (left, (k, x), right)) = |
35012
c3e3ac3ca091
removed unused "boundary" of Table/Graph.get_first;
wenzelm
parents:
33162
diff
changeset
|
141 |
(case get left of |
31616 | 142 |
NONE => |
35012
c3e3ac3ca091
removed unused "boundary" of Table/Graph.get_first;
wenzelm
parents:
33162
diff
changeset
|
143 |
(case f (k, x) of |
31616 | 144 |
NONE => get right |
145 |
| some => some) |
|
146 |
| some => some) |
|
31618
2e4430b84303
improved get_first: check boundary before entering subtrees;
wenzelm
parents:
31616
diff
changeset
|
147 |
| get (Branch3 (left, (k1, x1), mid, (k2, x2), right)) = |
35012
c3e3ac3ca091
removed unused "boundary" of Table/Graph.get_first;
wenzelm
parents:
33162
diff
changeset
|
148 |
(case get left of |
31616 | 149 |
NONE => |
35012
c3e3ac3ca091
removed unused "boundary" of Table/Graph.get_first;
wenzelm
parents:
33162
diff
changeset
|
150 |
(case f (k1, x1) of |
31616 | 151 |
NONE => |
35012
c3e3ac3ca091
removed unused "boundary" of Table/Graph.get_first;
wenzelm
parents:
33162
diff
changeset
|
152 |
(case get mid of |
31616 | 153 |
NONE => |
35012
c3e3ac3ca091
removed unused "boundary" of Table/Graph.get_first;
wenzelm
parents:
33162
diff
changeset
|
154 |
(case f (k2, x2) of |
31616 | 155 |
NONE => get right |
156 |
| some => some) |
|
157 |
| some => some) |
|
158 |
| some => some) |
|
159 |
| some => some); |
|
35012
c3e3ac3ca091
removed unused "boundary" of Table/Graph.get_first;
wenzelm
parents:
33162
diff
changeset
|
160 |
in get end; |
31616 | 161 |
|
35012
c3e3ac3ca091
removed unused "boundary" of Table/Graph.get_first;
wenzelm
parents:
33162
diff
changeset
|
162 |
fun exists pred = is_some o get_first (fn entry => if pred entry then SOME () else NONE); |
31616 | 163 |
fun forall pred = not o exists (not o pred); |
164 |
||
165 |
||
5015 | 166 |
(* lookup *) |
167 |
||
43792
d5803c3d537a
Table.lookup_key and Graph.get_entry allow to retrieve the original key, which is not necessarily identical to the given one;
wenzelm
parents:
39020
diff
changeset
|
168 |
fun lookup_key tab key = |
19031 | 169 |
let |
170 |
fun look Empty = NONE |
|
171 |
| look (Branch2 (left, (k, x), right)) = |
|
172 |
(case Key.ord (key, k) of |
|
173 |
LESS => look left |
|
43792
d5803c3d537a
Table.lookup_key and Graph.get_entry allow to retrieve the original key, which is not necessarily identical to the given one;
wenzelm
parents:
39020
diff
changeset
|
174 |
| EQUAL => SOME (k, x) |
19031 | 175 |
| GREATER => look right) |
176 |
| look (Branch3 (left, (k1, x1), mid, (k2, x2), right)) = |
|
177 |
(case Key.ord (key, k1) of |
|
178 |
LESS => look left |
|
43792
d5803c3d537a
Table.lookup_key and Graph.get_entry allow to retrieve the original key, which is not necessarily identical to the given one;
wenzelm
parents:
39020
diff
changeset
|
179 |
| EQUAL => SOME (k1, x1) |
19031 | 180 |
| GREATER => |
181 |
(case Key.ord (key, k2) of |
|
182 |
LESS => look mid |
|
43792
d5803c3d537a
Table.lookup_key and Graph.get_entry allow to retrieve the original key, which is not necessarily identical to the given one;
wenzelm
parents:
39020
diff
changeset
|
183 |
| EQUAL => SOME (k2, x2) |
19031 | 184 |
| GREATER => look right)); |
185 |
in look tab end; |
|
5015 | 186 |
|
43792
d5803c3d537a
Table.lookup_key and Graph.get_entry allow to retrieve the original key, which is not necessarily identical to the given one;
wenzelm
parents:
39020
diff
changeset
|
187 |
fun lookup tab key = Option.map #2 (lookup_key tab key); |
d5803c3d537a
Table.lookup_key and Graph.get_entry allow to retrieve the original key, which is not necessarily identical to the given one;
wenzelm
parents:
39020
diff
changeset
|
188 |
|
19031 | 189 |
fun defined tab key = |
190 |
let |
|
191 |
fun def Empty = false |
|
192 |
| def (Branch2 (left, (k, x), right)) = |
|
193 |
(case Key.ord (key, k) of |
|
194 |
LESS => def left |
|
195 |
| EQUAL => true |
|
196 |
| GREATER => def right) |
|
197 |
| def (Branch3 (left, (k1, x1), mid, (k2, x2), right)) = |
|
198 |
(case Key.ord (key, k1) of |
|
199 |
LESS => def left |
|
200 |
| EQUAL => true |
|
201 |
| GREATER => |
|
202 |
(case Key.ord (key, k2) of |
|
203 |
LESS => def mid |
|
204 |
| EQUAL => true |
|
205 |
| GREATER => def right)); |
|
206 |
in def tab end; |
|
16887 | 207 |
|
5015 | 208 |
|
19031 | 209 |
(* modify *) |
5015 | 210 |
|
211 |
datatype 'a growth = |
|
212 |
Stay of 'a table | |
|
213 |
Sprout of 'a table * (key * 'a) * 'a table; |
|
214 |
||
15761 | 215 |
exception SAME; |
216 |
||
15665 | 217 |
fun modify key f tab = |
218 |
let |
|
219 |
fun modfy Empty = Sprout (Empty, (key, f NONE), Empty) |
|
220 |
| modfy (Branch2 (left, p as (k, x), right)) = |
|
221 |
(case Key.ord (key, k) of |
|
222 |
LESS => |
|
223 |
(case modfy left of |
|
224 |
Stay left' => Stay (Branch2 (left', p, right)) |
|
225 |
| Sprout (left1, q, left2) => Stay (Branch3 (left1, q, left2, p, right))) |
|
226 |
| EQUAL => Stay (Branch2 (left, (k, f (SOME x)), right)) |
|
227 |
| GREATER => |
|
228 |
(case modfy right of |
|
229 |
Stay right' => Stay (Branch2 (left, p, right')) |
|
230 |
| Sprout (right1, q, right2) => |
|
231 |
Stay (Branch3 (left, p, right1, q, right2)))) |
|
232 |
| modfy (Branch3 (left, p1 as (k1, x1), mid, p2 as (k2, x2), right)) = |
|
233 |
(case Key.ord (key, k1) of |
|
5015 | 234 |
LESS => |
15665 | 235 |
(case modfy left of |
236 |
Stay left' => Stay (Branch3 (left', p1, mid, p2, right)) |
|
237 |
| Sprout (left1, q, left2) => |
|
238 |
Sprout (Branch2 (left1, q, left2), p1, Branch2 (mid, p2, right))) |
|
239 |
| EQUAL => Stay (Branch3 (left, (k1, f (SOME x1)), mid, p2, right)) |
|
5015 | 240 |
| GREATER => |
15665 | 241 |
(case Key.ord (key, k2) of |
242 |
LESS => |
|
243 |
(case modfy mid of |
|
244 |
Stay mid' => Stay (Branch3 (left, p1, mid', p2, right)) |
|
245 |
| Sprout (mid1, q, mid2) => |
|
246 |
Sprout (Branch2 (left, p1, mid1), q, Branch2 (mid2, p2, right))) |
|
247 |
| EQUAL => Stay (Branch3 (left, p1, mid, (k2, f (SOME x2)), right)) |
|
248 |
| GREATER => |
|
249 |
(case modfy right of |
|
250 |
Stay right' => Stay (Branch3 (left, p1, mid, p2, right')) |
|
251 |
| Sprout (right1, q, right2) => |
|
252 |
Sprout (Branch2 (left, p1, mid), p2, Branch2 (right1, q, right2))))); |
|
5015 | 253 |
|
15665 | 254 |
in |
255 |
(case modfy tab of |
|
256 |
Stay tab' => tab' |
|
257 |
| Sprout br => Branch2 br) |
|
258 |
handle SAME => tab |
|
259 |
end; |
|
5015 | 260 |
|
17412 | 261 |
fun update (key, x) tab = modify key (fn _ => x) tab; |
262 |
fun update_new (key, x) tab = modify key (fn NONE => x | SOME _ => raise DUP key) tab; |
|
17709 | 263 |
fun default (key, x) tab = modify key (fn NONE => x | SOME _ => raise SAME) tab; |
15761 | 264 |
fun map_entry key f = modify key (fn NONE => raise SAME | SOME x => f x); |
27783 | 265 |
fun map_default (key, x) f = modify key (fn NONE => f x | SOME y => f y); |
5015 | 266 |
|
267 |
||
15014 | 268 |
(* delete *) |
269 |
||
15665 | 270 |
exception UNDEF of key; |
271 |
||
272 |
local |
|
273 |
||
274 |
fun compare NONE (k2, _) = LESS |
|
275 |
| compare (SOME k1) (k2, _) = Key.ord (k1, k2); |
|
15014 | 276 |
|
277 |
fun if_eq EQUAL x y = x |
|
278 |
| if_eq _ x y = y; |
|
279 |
||
15531 | 280 |
fun del (SOME k) Empty = raise UNDEF k |
281 |
| del NONE (Branch2 (Empty, p, Empty)) = (p, (true, Empty)) |
|
282 |
| del NONE (Branch3 (Empty, p, Empty, q, Empty)) = |
|
15014 | 283 |
(p, (false, Branch2 (Empty, q, Empty))) |
15665 | 284 |
| del k (Branch2 (Empty, p, Empty)) = (case compare k p of |
16002 | 285 |
EQUAL => (p, (true, Empty)) | _ => raise UNDEF (the k)) |
15665 | 286 |
| del k (Branch3 (Empty, p, Empty, q, Empty)) = (case compare k p of |
15014 | 287 |
EQUAL => (p, (false, Branch2 (Empty, q, Empty))) |
15665 | 288 |
| _ => (case compare k q of |
15014 | 289 |
EQUAL => (q, (false, Branch2 (Empty, p, Empty))) |
16002 | 290 |
| _ => raise UNDEF (the k))) |
15665 | 291 |
| del k (Branch2 (l, p, r)) = (case compare k p of |
15014 | 292 |
LESS => (case del k l of |
293 |
(p', (false, l')) => (p', (false, Branch2 (l', p, r))) |
|
294 |
| (p', (true, l')) => (p', case r of |
|
295 |
Branch2 (rl, rp, rr) => |
|
296 |
(true, Branch3 (l', p, rl, rp, rr)) |
|
297 |
| Branch3 (rl, rp, rm, rq, rr) => (false, Branch2 |
|
298 |
(Branch2 (l', p, rl), rp, Branch2 (rm, rq, rr))))) |
|
15531 | 299 |
| ord => (case del (if_eq ord NONE k) r of |
15014 | 300 |
(p', (false, r')) => (p', (false, Branch2 (l, if_eq ord p' p, r'))) |
301 |
| (p', (true, r')) => (p', case l of |
|
302 |
Branch2 (ll, lp, lr) => |
|
303 |
(true, Branch3 (ll, lp, lr, if_eq ord p' p, r')) |
|
304 |
| Branch3 (ll, lp, lm, lq, lr) => (false, Branch2 |
|
305 |
(Branch2 (ll, lp, lm), lq, Branch2 (lr, if_eq ord p' p, r')))))) |
|
15665 | 306 |
| del k (Branch3 (l, p, m, q, r)) = (case compare k q of |
307 |
LESS => (case compare k p of |
|
15014 | 308 |
LESS => (case del k l of |
309 |
(p', (false, l')) => (p', (false, Branch3 (l', p, m, q, r))) |
|
310 |
| (p', (true, l')) => (p', (false, case (m, r) of |
|
311 |
(Branch2 (ml, mp, mr), Branch2 _) => |
|
312 |
Branch2 (Branch3 (l', p, ml, mp, mr), q, r) |
|
313 |
| (Branch3 (ml, mp, mm, mq, mr), _) => |
|
314 |
Branch3 (Branch2 (l', p, ml), mp, Branch2 (mm, mq, mr), q, r) |
|
315 |
| (Branch2 (ml, mp, mr), Branch3 (rl, rp, rm, rq, rr)) => |
|
316 |
Branch3 (Branch2 (l', p, ml), mp, Branch2 (mr, q, rl), rp, |
|
317 |
Branch2 (rm, rq, rr))))) |
|
15531 | 318 |
| ord => (case del (if_eq ord NONE k) m of |
15014 | 319 |
(p', (false, m')) => |
320 |
(p', (false, Branch3 (l, if_eq ord p' p, m', q, r))) |
|
321 |
| (p', (true, m')) => (p', (false, case (l, r) of |
|
322 |
(Branch2 (ll, lp, lr), Branch2 _) => |
|
323 |
Branch2 (Branch3 (ll, lp, lr, if_eq ord p' p, m'), q, r) |
|
324 |
| (Branch3 (ll, lp, lm, lq, lr), _) => |
|
325 |
Branch3 (Branch2 (ll, lp, lm), lq, |
|
326 |
Branch2 (lr, if_eq ord p' p, m'), q, r) |
|
327 |
| (_, Branch3 (rl, rp, rm, rq, rr)) => |
|
328 |
Branch3 (l, if_eq ord p' p, Branch2 (m', q, rl), rp, |
|
329 |
Branch2 (rm, rq, rr)))))) |
|
15531 | 330 |
| ord => (case del (if_eq ord NONE k) r of |
15014 | 331 |
(q', (false, r')) => |
332 |
(q', (false, Branch3 (l, p, m, if_eq ord q' q, r'))) |
|
333 |
| (q', (true, r')) => (q', (false, case (l, m) of |
|
334 |
(Branch2 _, Branch2 (ml, mp, mr)) => |
|
335 |
Branch2 (l, p, Branch3 (ml, mp, mr, if_eq ord q' q, r')) |
|
336 |
| (_, Branch3 (ml, mp, mm, mq, mr)) => |
|
337 |
Branch3 (l, p, Branch2 (ml, mp, mm), mq, |
|
338 |
Branch2 (mr, if_eq ord q' q, r')) |
|
339 |
| (Branch3 (ll, lp, lm, lq, lr), Branch2 (ml, mp, mr)) => |
|
340 |
Branch3 (Branch2 (ll, lp, lm), lq, Branch2 (lr, p, ml), mp, |
|
341 |
Branch2 (mr, if_eq ord q' q, r')))))); |
|
342 |
||
15665 | 343 |
in |
344 |
||
15761 | 345 |
fun delete key tab = snd (snd (del (SOME key) tab)); |
44336
59ff5a93eef4
tuned Table.delete_safe: avoid potentially expensive attempt of delete;
wenzelm
parents:
43792
diff
changeset
|
346 |
fun delete_safe key tab = if defined tab key then delete key tab else tab; |
15014 | 347 |
|
15665 | 348 |
end; |
349 |
||
15014 | 350 |
|
19031 | 351 |
(* membership operations *) |
16466 | 352 |
|
353 |
fun member eq tab (key, x) = |
|
17412 | 354 |
(case lookup tab key of |
16466 | 355 |
NONE => false |
356 |
| SOME y => eq (x, y)); |
|
15761 | 357 |
|
358 |
fun insert eq (key, x) = |
|
359 |
modify key (fn NONE => x | SOME y => if eq (x, y) then raise SAME else raise DUP key); |
|
360 |
||
361 |
fun remove eq (key, x) tab = |
|
17412 | 362 |
(case lookup tab key of |
15761 | 363 |
NONE => tab |
364 |
| SOME y => if eq (x, y) then delete key tab else tab); |
|
365 |
||
366 |
||
19031 | 367 |
(* simultaneous modifications *) |
368 |
||
29004 | 369 |
fun make entries = fold update_new entries empty; |
5015 | 370 |
|
12287 | 371 |
fun join f (table1, table2) = |
55727
7e330ae052bb
optimize special case according to Library.merge (see also 8fbc355100f2, 520872460b7b);
wenzelm
parents:
52049
diff
changeset
|
372 |
let |
7e330ae052bb
optimize special case according to Library.merge (see also 8fbc355100f2, 520872460b7b);
wenzelm
parents:
52049
diff
changeset
|
373 |
fun add (key, y) tab = modify key (fn NONE => y | SOME x => f key (x, y)) tab; |
7e330ae052bb
optimize special case according to Library.merge (see also 8fbc355100f2, 520872460b7b);
wenzelm
parents:
52049
diff
changeset
|
374 |
in |
7e330ae052bb
optimize special case according to Library.merge (see also 8fbc355100f2, 520872460b7b);
wenzelm
parents:
52049
diff
changeset
|
375 |
if pointer_eq (table1, table2) then table1 |
7e330ae052bb
optimize special case according to Library.merge (see also 8fbc355100f2, 520872460b7b);
wenzelm
parents:
52049
diff
changeset
|
376 |
else if is_empty table1 then table2 |
7e330ae052bb
optimize special case according to Library.merge (see also 8fbc355100f2, 520872460b7b);
wenzelm
parents:
52049
diff
changeset
|
377 |
else fold_table add table2 table1 |
7e330ae052bb
optimize special case according to Library.merge (see also 8fbc355100f2, 520872460b7b);
wenzelm
parents:
52049
diff
changeset
|
378 |
end; |
12287 | 379 |
|
19031 | 380 |
fun merge eq = join (fn key => fn xy => if eq xy then raise SAME else raise DUP key); |
5015 | 381 |
|
382 |
||
19031 | 383 |
(* list tables *) |
15761 | 384 |
|
18946 | 385 |
fun lookup_list tab key = these (lookup tab key); |
25391 | 386 |
|
387 |
fun cons_list (key, x) tab = modify key (fn NONE => [x] | SOME xs => x :: xs) tab; |
|
5015 | 388 |
|
20124 | 389 |
fun insert_list eq (key, x) = |
390 |
modify key (fn NONE => [x] | SOME xs => if Library.member eq xs x then raise SAME else x :: xs); |
|
25391 | 391 |
|
18946 | 392 |
fun remove_list eq (key, x) tab = |
15761 | 393 |
map_entry key (fn xs => (case Library.remove eq x xs of [] => raise UNDEF key | ys => ys)) tab |
394 |
handle UNDEF _ => delete key tab; |
|
5015 | 395 |
|
25391 | 396 |
fun update_list eq (key, x) = |
397 |
modify key (fn NONE => [x] | SOME [] => [x] | SOME (xs as y :: _) => |
|
398 |
if eq (x, y) then raise SAME else Library.update eq x xs); |
|
399 |
||
400 |
fun make_list args = fold_rev cons_list args empty; |
|
19482
9f11af8f7ef9
tuned basic list operators (flat, maps, map_filter);
wenzelm
parents:
19073
diff
changeset
|
401 |
fun dest_list tab = maps (fn (key, xs) => map (pair key) xs) (dest tab); |
19031 | 402 |
fun merge_list eq = join (fn _ => Library.merge eq); |
5015 | 403 |
|
404 |
||
50234 | 405 |
(* unit tables *) |
406 |
||
407 |
type set = unit table; |
|
408 |
||
63511 | 409 |
fun insert_set x = update (x, ()); |
410 |
fun make_set entries = fold insert_set entries empty; |
|
50234 | 411 |
|
412 |
||
47980
c81801f881b3
simplified Poly/ML setup -- 5.3.0 is now the common base-line;
wenzelm
parents:
44336
diff
changeset
|
413 |
(* ML pretty-printing *) |
38635
f76ad0771f67
added ML toplevel pretty-printing for tables, using dummy for anything other than Poly/ML 5.3.0 (or later);
wenzelm
parents:
35012
diff
changeset
|
414 |
|
f76ad0771f67
added ML toplevel pretty-printing for tables, using dummy for anything other than Poly/ML 5.3.0 (or later);
wenzelm
parents:
35012
diff
changeset
|
415 |
val _ = |
62819
d3ff367a16a0
careful export of type-dependent functions, without losing their special status;
wenzelm
parents:
62503
diff
changeset
|
416 |
ML_system_pp (fn depth => fn pretty => fn tab => |
62503 | 417 |
ML_Pretty.to_polyml |
38635
f76ad0771f67
added ML toplevel pretty-printing for tables, using dummy for anything other than Poly/ML 5.3.0 (or later);
wenzelm
parents:
35012
diff
changeset
|
418 |
(ML_Pretty.enum "," "{" "}" |
62503 | 419 |
(ML_Pretty.pair |
62819
d3ff367a16a0
careful export of type-dependent functions, without losing their special status;
wenzelm
parents:
62503
diff
changeset
|
420 |
(ML_Pretty.from_polyml o ML_system_pretty) |
62503 | 421 |
(ML_Pretty.from_polyml o pretty)) |
38635
f76ad0771f67
added ML toplevel pretty-printing for tables, using dummy for anything other than Poly/ML 5.3.0 (or later);
wenzelm
parents:
35012
diff
changeset
|
422 |
(dest tab, depth))); |
f76ad0771f67
added ML toplevel pretty-printing for tables, using dummy for anything other than Poly/ML 5.3.0 (or later);
wenzelm
parents:
35012
diff
changeset
|
423 |
|
f76ad0771f67
added ML toplevel pretty-printing for tables, using dummy for anything other than Poly/ML 5.3.0 (or later);
wenzelm
parents:
35012
diff
changeset
|
424 |
|
5681 | 425 |
(*final declarations of this structure!*) |
39020 | 426 |
val map = map_table; |
16446 | 427 |
val fold = fold_table; |
28334 | 428 |
val fold_rev = fold_rev_table; |
5015 | 429 |
|
430 |
end; |
|
431 |
||
31971
8c1b845ed105
renamed functor TableFun to Table, and GraphFun to Graph;
wenzelm
parents:
31621
diff
changeset
|
432 |
structure Inttab = Table(type key = int val ord = int_ord); |
8c1b845ed105
renamed functor TableFun to Table, and GraphFun to Graph;
wenzelm
parents:
31621
diff
changeset
|
433 |
structure Symtab = Table(type key = string val ord = fast_string_ord); |
8c1b845ed105
renamed functor TableFun to Table, and GraphFun to Graph;
wenzelm
parents:
31621
diff
changeset
|
434 |
structure Symreltab = Table(type key = string * string |
30647
ef8f46c3158a
added Symreltab (binary relations of symbols) instance of TableFun
haftmann
parents:
30290
diff
changeset
|
435 |
val ord = prod_ord fast_string_ord fast_string_ord); |
ef8f46c3158a
added Symreltab (binary relations of symbols) instance of TableFun
haftmann
parents:
30290
diff
changeset
|
436 |