5015

1 
(* Title: Pure/table.ML


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


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


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


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


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


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


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


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


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


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


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


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


34 
end;


35 


36 
functor TableFun(Key: KEY): TABLE =


37 
struct


38 


39 


40 
(* datatype table *)


41 


42 
type key = Key.key;


43 


44 
datatype 'a table =


45 
Empty 


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


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


48 


49 
exception DUP of key;


50 
exception DUPS of key list;


51 


52 


53 
val empty = Empty;


54 


55 
fun is_empty Empty = true


56 
 is_empty _ = false;


57 


58 
fun dest Empty = []


59 
 dest (Branch2 (left, p, right)) = dest left @ [p] @ dest right


60 
 dest (Branch3 (left, p1, mid, p2, right)) =


61 
dest left @ [p1] @ dest mid @ [p2] @ dest right;


62 


63 


64 
(* lookup *)


65 


66 
fun lookup (Empty, _) = None


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


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


69 
LESS => lookup (left, key)


70 
 EQUAL => Some x


71 
 GREATER => lookup (right, key))


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


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


74 
LESS => lookup (left, key)


75 
 EQUAL => Some x1


76 
 GREATER =>


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


78 
LESS => lookup (mid, key)


79 
 EQUAL => Some x2


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


81 


82 


83 
(* update *)


84 


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


86 


87 
datatype 'a growth =


88 
Stay of 'a table 


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


90 


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


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


93 
(case compare pair p of


94 
LESS =>


95 
(case insert pair left of


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


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


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


99 
 GREATER =>


100 
(case insert pair right of


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


102 
 Sprout (right1, q, right2) =>


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


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


105 
(case compare pair p1 of


106 
LESS =>


107 
(case insert pair left of


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


109 
 Sprout (left1, q, left2) =>


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


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


112 
 GREATER =>


113 
(case compare pair p2 of


114 
LESS =>


115 
(case insert pair mid of


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


117 
 Sprout (mid1, q, mid2) =>


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


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


120 
 GREATER =>


121 
(case insert pair right of


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


123 
 Sprout (right1, q, right2) =>


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


125 


126 
fun update (pair, tab) =


127 
(case insert pair tab of


128 
Stay tab => tab


129 
 Sprout br => Branch2 br);


130 


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


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


133 
else raise DUP key;


134 


135 


136 
(* make, extend, merge tables *)


137 


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


139 
(case lookup (tab, key) of


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


141 
 Some x' =>


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


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


144 


145 
fun enter eq (tab, pairs) =


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


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


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


149 


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


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


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


153 


154 


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


156 


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


158 


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


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


161 


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


163 


164 
fun dest_multi tab =


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


166 


167 


168 
(* map *)


169 


170 
fun map _ Empty = Empty


171 
 map f (Branch2 (left, (k, x), right)) =


172 
Branch2 (map f left, (k, f x), map f right)


173 
 map f (Branch3 (left, (k1, x1), mid, (k2, x2), right)) =


174 
Branch3 (map f left, (k1, f x1), map f mid, (k2, f x2), map f right);


175 


176 


177 
end;


178 


179 


180 
(*tables indexed by strings*)


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