6118

1 
(* Title: Pure/General/table.ML

5015

2 
ID: $Id$

15014

3 
Author: Markus Wenzel and Stefan Berghofer, TU Muenchen

5015

4 

8806

5 
Generic tables and tables indexed by strings. Efficient purely

15014

6 
functional implementation using balanced 23 trees.

5015

7 
*)


8 


9 
signature KEY =


10 
sig


11 
type key


12 
val ord: key * key > order


13 
end;


14 


15 
signature TABLE =


16 
sig


17 
type key


18 
type 'a table


19 
exception DUP of key


20 
exception DUPS of key list

15014

21 
exception UNDEF of key

5015

22 
val empty: 'a table


23 
val is_empty: 'a table > bool

5681

24 
val map: ('a > 'b) > 'a table > 'b table


25 
val foldl: ('a * (key * 'b) > 'a) > 'a * 'b table > 'a

5015

26 
val dest: 'a table > (key * 'a) list

5681

27 
val keys: 'a table > key list

8409

28 
val min_key: 'a table > key option

7061

29 
val exists: (key * 'a > bool) > 'a table > bool

5015

30 
val lookup: 'a table * key > 'a option


31 
val update: (key * 'a) * 'a table > 'a table

12287

32 
val update_new: (key * 'a) * 'a table > 'a table (*exception DUP*)


33 
val make: (key * 'a) list > 'a table (*exception DUPS*)


34 
val extend: 'a table * (key * 'a) list > 'a table (*exception DUPS*)


35 
val join: ('a * 'a > 'a option) > 'a table * 'a table > 'a table (*exception DUPS*)


36 
val merge: ('a * 'a > bool) > 'a table * 'a table > 'a table (*exception DUPS*)

15014

37 
val delete: key > 'a table > 'a table (* exception UNDEF *)

5015

38 
val lookup_multi: 'a list table * key > 'a list

8606

39 
val update_multi: (key * 'a) * 'a list table > 'a list table

5015

40 
val make_multi: (key * 'a) list > 'a list table


41 
val dest_multi: 'a list table > (key * 'a) list

12287

42 
val merge_multi: ('a * 'a > bool) >


43 
'a list table * 'a list table > 'a list table (*exception DUPS*)


44 
val merge_multi': ('a * 'a > bool) >


45 
'a list table * 'a list table > 'a list table (*exception DUPS*)

5015

46 
end;


47 


48 
functor TableFun(Key: KEY): TABLE =


49 
struct


50 


51 


52 
(* datatype table *)


53 


54 
type key = Key.key;


55 


56 
datatype 'a table =


57 
Empty 


58 
Branch2 of 'a table * (key * 'a) * 'a table 


59 
Branch3 of 'a table * (key * 'a) * 'a table * (key * 'a) * 'a table;


60 


61 
exception DUP of key;


62 
exception DUPS of key list;


63 


64 

5681

65 
(* empty *)


66 

5015

67 
val empty = Empty;


68 


69 
fun is_empty Empty = true


70 
 is_empty _ = false;


71 

5681

72 


73 
(* map and fold combinators *)


74 


75 
fun map_table _ Empty = Empty


76 
 map_table f (Branch2 (left, (k, x), right)) =


77 
Branch2 (map_table f left, (k, f x), map_table f right)


78 
 map_table f (Branch3 (left, (k1, x1), mid, (k2, x2), right)) =


79 
Branch3 (map_table f left, (k1, f x1), map_table f mid, (k2, f x2), map_table f right);


80 


81 
fun foldl_table _ (x, Empty) = x


82 
 foldl_table f (x, Branch2 (left, p, right)) =


83 
foldl_table f (f (foldl_table f (x, left), p), right)


84 
 foldl_table f (x, Branch3 (left, p1, mid, p2, right)) =


85 
foldl_table f (f (foldl_table f (f (foldl_table f (x, left), p1), mid), p2), right);


86 


87 
fun dest tab = rev (foldl_table (fn (rev_ps, p) => p :: rev_ps) ([], tab));


88 
fun keys tab = rev (foldl_table (fn (rev_ks, (k, _)) => k :: rev_ks) ([], tab));

7061

89 
fun exists P tab = foldl_table (fn (false, e) => P e  (b, _) => b) (false, tab);

5015

90 

8409

91 
fun min_key Empty = None


92 
 min_key (Branch2 (left, (k, _), _)) = Some (if_none (min_key left) k)


93 
 min_key (Branch3 (left, (k, _), _, _, _)) = Some (if_none (min_key left) k);


94 

5015

95 


96 
(* lookup *)


97 


98 
fun lookup (Empty, _) = None


99 
 lookup (Branch2 (left, (k, x), right), key) =


100 
(case Key.ord (key, k) of


101 
LESS => lookup (left, key)


102 
 EQUAL => Some x


103 
 GREATER => lookup (right, key))


104 
 lookup (Branch3 (left, (k1, x1), mid, (k2, x2), right), key) =


105 
(case Key.ord (key, k1) of


106 
LESS => lookup (left, key)


107 
 EQUAL => Some x1


108 
 GREATER =>


109 
(case Key.ord (key, k2) of


110 
LESS => lookup (mid, key)


111 
 EQUAL => Some x2


112 
 GREATER => lookup (right, key)));


113 


114 


115 
(* update *)


116 


117 
fun compare (k1, _) (k2, _) = Key.ord (k1, k2);


118 


119 
datatype 'a growth =


120 
Stay of 'a table 


121 
Sprout of 'a table * (key * 'a) * 'a table;


122 


123 
fun insert pair Empty = Sprout (Empty, pair, Empty)


124 
 insert pair (Branch2 (left, p, right)) =


125 
(case compare pair p of


126 
LESS =>


127 
(case insert pair left of


128 
Stay left' => Stay (Branch2 (left', p, right))


129 
 Sprout (left1, q, left2) => Stay (Branch3 (left1, q, left2, p, right)))


130 
 EQUAL => Stay (Branch2 (left, pair, right))


131 
 GREATER =>


132 
(case insert pair right of


133 
Stay right' => Stay (Branch2 (left, p, right'))


134 
 Sprout (right1, q, right2) =>


135 
Stay (Branch3 (left, p, right1, q, right2))))


136 
 insert pair (Branch3 (left, p1, mid, p2, right)) =


137 
(case compare pair p1 of


138 
LESS =>


139 
(case insert pair left of


140 
Stay left' => Stay (Branch3 (left', p1, mid, p2, right))


141 
 Sprout (left1, q, left2) =>


142 
Sprout (Branch2 (left1, q, left2), p1, Branch2 (mid, p2, right)))


143 
 EQUAL => Stay (Branch3 (left, pair, mid, p2, right))


144 
 GREATER =>


145 
(case compare pair p2 of


146 
LESS =>


147 
(case insert pair mid of


148 
Stay mid' => Stay (Branch3 (left, p1, mid', p2, right))


149 
 Sprout (mid1, q, mid2) =>


150 
Sprout (Branch2 (left, p1, mid1), q, Branch2 (mid2, p2, right)))


151 
 EQUAL => Stay (Branch3 (left, p1, mid, pair, right))


152 
 GREATER =>


153 
(case insert pair right of


154 
Stay right' => Stay (Branch3 (left, p1, mid, p2, right'))


155 
 Sprout (right1, q, right2) =>


156 
Sprout (Branch2 (left, p1, mid), p2, Branch2 (right1, q, right2)))));


157 


158 
fun update (pair, tab) =


159 
(case insert pair tab of


160 
Stay tab => tab


161 
 Sprout br => Branch2 br);


162 


163 
fun update_new (pair as (key, _), tab) =


164 
if is_none (lookup (tab, key)) then update (pair, tab)


165 
else raise DUP key;


166 


167 

12287

168 
(* extend and make *)

5015

169 

12287

170 
fun extend (table, pairs) =


171 
let


172 
fun add ((tab, dups), (key, x)) =


173 
(case lookup (tab, key) of


174 
None => (update ((key, x), tab), dups)


175 
 _ => (tab, key :: dups));


176 
in


177 
(case foldl add ((table, []), pairs) of


178 
(table', []) => table'


179 
 (_, dups) => raise DUPS (rev dups))


180 
end;


181 


182 
fun make pairs = extend (empty, pairs);


183 

5015

184 

15014

185 
(* delete *)


186 


187 
fun compare' None (k2, _) = LESS


188 
 compare' (Some k1) (k2, _) = Key.ord (k1, k2);


189 


190 
fun if_eq EQUAL x y = x


191 
 if_eq _ x y = y;


192 


193 
exception UNDEF of key;


194 


195 
fun del (Some k) Empty = raise UNDEF k


196 
 del None (Branch2 (Empty, p, Empty)) = (p, (true, Empty))


197 
 del None (Branch3 (Empty, p, Empty, q, Empty)) =


198 
(p, (false, Branch2 (Empty, q, Empty)))


199 
 del k (Branch2 (Empty, p, Empty)) = (case compare' k p of


200 
EQUAL => (p, (true, Empty))  _ => raise UNDEF (the k))


201 
 del k (Branch3 (Empty, p, Empty, q, Empty)) = (case compare' k p of


202 
EQUAL => (p, (false, Branch2 (Empty, q, Empty)))


203 
 _ => (case compare' k q of


204 
EQUAL => (q, (false, Branch2 (Empty, p, Empty)))


205 
 _ => raise UNDEF (the k)))


206 
 del k (Branch2 (l, p, r)) = (case compare' k p of


207 
LESS => (case del k l of


208 
(p', (false, l')) => (p', (false, Branch2 (l', p, r)))


209 
 (p', (true, l')) => (p', case r of


210 
Branch2 (rl, rp, rr) =>


211 
(true, Branch3 (l', p, rl, rp, rr))


212 
 Branch3 (rl, rp, rm, rq, rr) => (false, Branch2


213 
(Branch2 (l', p, rl), rp, Branch2 (rm, rq, rr)))))


214 
 ord => (case del (if_eq ord None k) r of


215 
(p', (false, r')) => (p', (false, Branch2 (l, if_eq ord p' p, r')))


216 
 (p', (true, r')) => (p', case l of


217 
Branch2 (ll, lp, lr) =>


218 
(true, Branch3 (ll, lp, lr, if_eq ord p' p, r'))


219 
 Branch3 (ll, lp, lm, lq, lr) => (false, Branch2


220 
(Branch2 (ll, lp, lm), lq, Branch2 (lr, if_eq ord p' p, r'))))))


221 
 del k (Branch3 (l, p, m, q, r)) = (case compare' k q of


222 
LESS => (case compare' k p of


223 
LESS => (case del k l of


224 
(p', (false, l')) => (p', (false, Branch3 (l', p, m, q, r)))


225 
 (p', (true, l')) => (p', (false, case (m, r) of


226 
(Branch2 (ml, mp, mr), Branch2 _) =>


227 
Branch2 (Branch3 (l', p, ml, mp, mr), q, r)


228 
 (Branch3 (ml, mp, mm, mq, mr), _) =>


229 
Branch3 (Branch2 (l', p, ml), mp, Branch2 (mm, mq, mr), q, r)


230 
 (Branch2 (ml, mp, mr), Branch3 (rl, rp, rm, rq, rr)) =>


231 
Branch3 (Branch2 (l', p, ml), mp, Branch2 (mr, q, rl), rp,


232 
Branch2 (rm, rq, rr)))))


233 
 ord => (case del (if_eq ord None k) m of


234 
(p', (false, m')) =>


235 
(p', (false, Branch3 (l, if_eq ord p' p, m', q, r)))


236 
 (p', (true, m')) => (p', (false, case (l, r) of


237 
(Branch2 (ll, lp, lr), Branch2 _) =>


238 
Branch2 (Branch3 (ll, lp, lr, if_eq ord p' p, m'), q, r)


239 
 (Branch3 (ll, lp, lm, lq, lr), _) =>


240 
Branch3 (Branch2 (ll, lp, lm), lq,


241 
Branch2 (lr, if_eq ord p' p, m'), q, r)


242 
 (_, Branch3 (rl, rp, rm, rq, rr)) =>


243 
Branch3 (l, if_eq ord p' p, Branch2 (m', q, rl), rp,


244 
Branch2 (rm, rq, rr))))))


245 
 ord => (case del (if_eq ord None k) r of


246 
(q', (false, r')) =>


247 
(q', (false, Branch3 (l, p, m, if_eq ord q' q, r')))


248 
 (q', (true, r')) => (q', (false, case (l, m) of


249 
(Branch2 _, Branch2 (ml, mp, mr)) =>


250 
Branch2 (l, p, Branch3 (ml, mp, mr, if_eq ord q' q, r'))


251 
 (_, Branch3 (ml, mp, mm, mq, mr)) =>


252 
Branch3 (l, p, Branch2 (ml, mp, mm), mq,


253 
Branch2 (mr, if_eq ord q' q, r'))


254 
 (Branch3 (ll, lp, lm, lq, lr), Branch2 (ml, mp, mr)) =>


255 
Branch3 (Branch2 (ll, lp, lm), lq, Branch2 (lr, p, ml), mp,


256 
Branch2 (mr, if_eq ord q' q, r'))))));


257 


258 
fun delete k t = snd (snd (del (Some k) t));


259 


260 

12287

261 
(* join and merge *)

5015

262 

12287

263 
fun join f (table1, table2) =


264 
let


265 
fun add ((tab, dups), (key, x)) =


266 
(case lookup (tab, key) of


267 
None => (update ((key, x), tab), dups)


268 
 Some y =>


269 
(case f (y, x) of


270 
Some z => (update ((key, z), tab), dups)


271 
 None => (tab, key :: dups)));


272 
in


273 
(case foldl_table add ((table1, []), table2) of


274 
(table', []) => table'


275 
 (_, dups) => raise DUPS (rev dups))


276 
end;


277 


278 
fun merge eq tabs = join (fn (y, x) => if eq (y, x) then Some y else None) tabs;

5015

279 


280 


281 
(* tables with multiple entries per key (preserving order) *)


282 


283 
fun lookup_multi tab_key = if_none (lookup tab_key) [];

12287

284 
fun update_multi ((key, x), tab) = update ((key, x :: lookup_multi (tab, key)), tab);

5015

285 

8606

286 
fun make_multi pairs = foldr update_multi (pairs, empty);

12287

287 
fun dest_multi tab = flat (map (fn (key, xs) => map (Library.pair key) xs) (dest tab));


288 
fun merge_multi eq tabs = join (fn (xs, xs') => Some (gen_merge_lists eq xs xs')) tabs;


289 
fun merge_multi' eq tabs = join (fn (xs, xs') => Some (gen_merge_lists' eq xs xs')) tabs;

5015

290 


291 

5681

292 
(*final declarations of this structure!*)


293 
val map = map_table;


294 
val foldl = foldl_table;

5015

295 


296 
end;


297 


298 


299 
(*tables indexed by strings*)


300 
structure Symtab = TableFun(type key = string val ord = string_ord);
