6118

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

5015

2 
ID: $Id$


3 
Author: Markus Wenzel, TU Muenchen


4 


5 
Generic tables and tables indexed by strings. No delete operation.


6 
Implemented as balanced 23 trees.


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


21 
val empty: 'a table


22 
val is_empty: 'a table > bool

5681

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


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

5015

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

5681

26 
val keys: 'a table > key list

5015

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


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


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


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


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


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


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


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


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


36 
end;


37 


38 
functor TableFun(Key: KEY): TABLE =


39 
struct


40 


41 


42 
(* datatype table *)


43 


44 
type key = Key.key;


45 


46 
datatype 'a table =


47 
Empty 


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


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


50 


51 
exception DUP of key;


52 
exception DUPS of key list;


53 


54 

5681

55 
(* empty *)


56 

5015

57 
val empty = Empty;


58 


59 
fun is_empty Empty = true


60 
 is_empty _ = false;


61 

5681

62 


63 
(* map and fold combinators *)


64 


65 
fun map_table _ Empty = Empty


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


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


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


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


70 


71 
fun foldl_table _ (x, Empty) = x


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


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


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


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


76 


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


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

5015

79 


80 


81 
(* lookup *)


82 


83 
fun lookup (Empty, _) = None


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


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


86 
LESS => lookup (left, key)


87 
 EQUAL => Some x


88 
 GREATER => lookup (right, key))


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


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


91 
LESS => lookup (left, key)


92 
 EQUAL => Some x1


93 
 GREATER =>


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


95 
LESS => lookup (mid, key)


96 
 EQUAL => Some x2


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


98 


99 


100 
(* update *)


101 


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


103 


104 
datatype 'a growth =


105 
Stay of 'a table 


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


107 


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


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


110 
(case compare pair p of


111 
LESS =>


112 
(case insert pair left of


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


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


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


116 
 GREATER =>


117 
(case insert pair right of


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


119 
 Sprout (right1, q, right2) =>


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


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


122 
(case compare pair p1 of


123 
LESS =>


124 
(case insert pair left of


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


126 
 Sprout (left1, q, left2) =>


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


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


129 
 GREATER =>


130 
(case compare pair p2 of


131 
LESS =>


132 
(case insert pair mid of


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


134 
 Sprout (mid1, q, mid2) =>


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


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


137 
 GREATER =>


138 
(case insert pair right of


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


140 
 Sprout (right1, q, right2) =>


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


142 


143 
fun update (pair, tab) =


144 
(case insert pair tab of


145 
Stay tab => tab


146 
 Sprout br => Branch2 br);


147 


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


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


150 
else raise DUP key;


151 


152 


153 
(* make, extend, merge tables *)


154 


155 
fun add eq ((tab, dups), (key, x)) =


156 
(case lookup (tab, key) of


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


158 
 Some x' =>


159 
if eq (x, x') then (tab, dups)


160 
else (tab, dups @ [key]));


161 


162 
fun enter eq (tab, pairs) =


163 
(case foldl (add eq) ((tab, []), pairs) of


164 
(tab', []) => tab'


165 
 (_, dups) => raise DUPS dups);


166 


167 
fun extend tab_pairs = enter (K false) tab_pairs;


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


169 
fun merge eq (tab1, tab2) = enter eq (tab1, dest tab2);


170 


171 


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


173 


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


175 


176 
fun cons_entry ((key, x), tab) =


177 
update ((key, x :: lookup_multi (tab, key)), tab);


178 


179 
fun make_multi pairs = foldr cons_entry (pairs, empty);


180 


181 
fun dest_multi tab =


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


183 


184 

5681

185 
(*final declarations of this structure!*)


186 
val map = map_table;


187 
val foldl = foldl_table;

5015

188 


189 


190 
end;


191 


192 


193 
(*tables indexed by strings*)


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