Generic tables (lacking delete operation). Implemented as 2-3 trees.
authorwenzelm
Sat Dec 27 21:49:45 1997 +0100 (1997-12-27)
changeset 448243620c417579
parent 4481 b595116eb3c4
child 4483 caf8ae95c61f
Generic tables (lacking delete operation). Implemented as 2-3 trees.
src/Pure/table.ML
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Pure/table.ML	Sat Dec 27 21:49:45 1997 +0100
     1.3 @@ -0,0 +1,186 @@
     1.4 +(*  Title:      Pure/table.ML
     1.5 +    ID:         $Id$
     1.6 +    Author:     Markus Wenzel, TU Muenchen
     1.7 +
     1.8 +Generic tables (lacking delete operation).  Implemented as 2-3 trees.
     1.9 +*)
    1.10 +
    1.11 +signature TABLE_DATA =
    1.12 +sig
    1.13 +  type key
    1.14 +  val ord: key * key -> order
    1.15 +end;
    1.16 +
    1.17 +signature TABLE =
    1.18 +sig
    1.19 +  type key
    1.20 +  type 'a table
    1.21 +  exception DUP of key
    1.22 +  exception DUPS of key list
    1.23 +  val empty: 'a table
    1.24 +  val is_empty: 'a table -> bool
    1.25 +  val dest: 'a table -> (key * 'a) list
    1.26 +  val lookup: 'a table * key -> 'a option
    1.27 +  val update: (key * 'a) * 'a table -> 'a table
    1.28 +  val update_new: (key * 'a) * 'a table -> 'a table                     (*exception DUP*)
    1.29 +  val make: (key * 'a) list -> 'a table                                 (*exception DUPS*)
    1.30 +  val extend: 'a table * (key * 'a) list -> 'a table                    (*exception DUPS*)
    1.31 +  val merge: ('a * 'a -> bool) -> 'a table * 'a table -> 'a table       (*exception DUPS*)
    1.32 +  val lookup_multi: 'a list table * key -> 'a list
    1.33 +  val make_multi: (key * 'a) list -> 'a list table
    1.34 +  val dest_multi: 'a list table -> (key * 'a) list
    1.35 +  val map: ('a -> 'b) -> 'a table -> 'b table
    1.36 +end;
    1.37 +
    1.38 +functor TableFun(Data: TABLE_DATA): TABLE =
    1.39 +struct
    1.40 +
    1.41 +
    1.42 +(* datatype table *)
    1.43 +
    1.44 +type key = Data.key;
    1.45 +
    1.46 +datatype 'a table =
    1.47 +  Empty |
    1.48 +  Branch2 of 'a table * (key * 'a) * 'a table |
    1.49 +  Branch3 of 'a table * (key * 'a) * 'a table * (key * 'a) * 'a table;
    1.50 +
    1.51 +exception DUP of key;
    1.52 +exception DUPS of key list;
    1.53 +
    1.54 +
    1.55 +val empty = Empty;
    1.56 +
    1.57 +fun is_empty Empty = true
    1.58 +  | is_empty _ = false;
    1.59 +
    1.60 +fun dest Empty = []
    1.61 +  | dest (Branch2 (left, p, right)) = dest left @ [p] @ dest right
    1.62 +  | dest (Branch3 (left, p1, mid, p2, right)) =
    1.63 +      dest left @ [p1] @ dest mid @ [p2] @ dest right;
    1.64 +
    1.65 +
    1.66 +(* lookup *)
    1.67 +
    1.68 +fun lookup (Empty, _) = None
    1.69 +  | lookup (Branch2 (left, (k, x), right), key) =
    1.70 +      (case Data.ord (key, k) of
    1.71 +        LESS => lookup (left, key)
    1.72 +      | EQUAL => Some x
    1.73 +      | GREATER => lookup (right, key))
    1.74 +  | lookup (Branch3 (left, (k1, x1), mid, (k2, x2), right), key) =
    1.75 +      (case Data.ord (key, k1) of
    1.76 +        LESS => lookup (left, key)
    1.77 +      | EQUAL => Some x1
    1.78 +      | GREATER =>
    1.79 +          (case Data.ord (key, k2) of
    1.80 +            LESS => lookup (mid, key)
    1.81 +          | EQUAL => Some x2
    1.82 +          | GREATER => lookup (right, key)));
    1.83 +
    1.84 +
    1.85 +(* update *)
    1.86 +
    1.87 +fun compare (k1, _) (k2, _) = Data.ord (k1, k2);
    1.88 +
    1.89 +datatype 'a growth =
    1.90 +  Stay of 'a table |
    1.91 +  Sprout of 'a table * (key * 'a) * 'a table;
    1.92 +
    1.93 +fun insert pair Empty = Sprout (Empty, pair, Empty)
    1.94 +  | insert pair (Branch2 (left, p, right)) =
    1.95 +      (case compare pair p of
    1.96 +        LESS =>
    1.97 +          (case insert pair left of
    1.98 +            Stay left' => Stay (Branch2 (left', p, right))
    1.99 +          | Sprout (left1, q, left2) => Stay (Branch3 (left1, q, left2, p, right)))
   1.100 +      | EQUAL => Stay (Branch2 (left, pair, right))
   1.101 +      | GREATER =>
   1.102 +          (case insert pair right of
   1.103 +            Stay right' => Stay (Branch2 (left, p, right'))
   1.104 +          | Sprout (right1, q, right2) =>
   1.105 +              Stay (Branch3 (left, p, right1, q, right2))))
   1.106 +  | insert pair (Branch3 (left, p1, mid, p2, right)) =
   1.107 +      (case compare pair p1 of
   1.108 +        LESS =>
   1.109 +          (case insert pair left of
   1.110 +            Stay left' => Stay (Branch3 (left', p1, mid, p2, right))
   1.111 +          | Sprout (left1, q, left2) =>
   1.112 +              Sprout (Branch2 (left1, q, left2), p1, Branch2 (mid, p2, right)))
   1.113 +      | EQUAL => Stay (Branch3 (left, pair, mid, p2, right))
   1.114 +      | GREATER =>
   1.115 +          (case compare pair p2 of
   1.116 +            LESS =>
   1.117 +              (case insert pair mid of
   1.118 +                Stay mid' => Stay (Branch3 (left, p1, mid', p2, right))
   1.119 +              | Sprout (mid1, q, mid2) =>
   1.120 +                  Sprout (Branch2 (left, p1, mid1), q, Branch2 (mid2, p2, right)))
   1.121 +          | EQUAL => Stay (Branch3 (left, p1, mid, pair, right))
   1.122 +          | GREATER =>
   1.123 +              (case insert pair right of
   1.124 +                Stay right' => Stay (Branch3 (left, p1, mid, p2, right'))
   1.125 +              | Sprout (right1, q, right2) =>
   1.126 +                  Sprout (Branch2 (left, p1, mid), p2, Branch2 (right1, q, right2)))));
   1.127 +
   1.128 +fun update (pair, tab) =
   1.129 +  (case insert pair tab of
   1.130 +    Stay tab => tab
   1.131 +  | Sprout br => Branch2 br);
   1.132 +
   1.133 +fun update_new (pair as (key, _), tab) =
   1.134 +  (case lookup (tab, key) of
   1.135 +    None => update (pair, tab)
   1.136 +  | Some _ => raise DUP key);
   1.137 +
   1.138 +
   1.139 +(* make, extend, merge tables *)
   1.140 +
   1.141 +fun add eq ((tab, dups), (key, x)) =
   1.142 +  (case lookup (tab, key) of
   1.143 +    None => (update ((key, x), tab), dups)
   1.144 +  | Some x' =>
   1.145 +      if eq (x, x') then (tab, dups)
   1.146 +      else (tab, dups @ [key]));
   1.147 +
   1.148 +fun enter eq (tab, pairs) =
   1.149 +  (case foldl (add eq) ((tab, []), pairs) of
   1.150 +    (tab', []) => tab'
   1.151 +  | (_, dups) => raise DUPS dups);
   1.152 +
   1.153 +fun extend tab_pairs = enter (K false) tab_pairs;
   1.154 +fun make pairs = extend (empty, pairs);
   1.155 +fun merge eq (tab1, tab2) = enter eq (tab1, dest tab2);
   1.156 +
   1.157 +
   1.158 +(* tables with multiple entries per key (preserving order) *)
   1.159 +
   1.160 +fun lookup_multi tab_key = if_none (lookup tab_key) [];
   1.161 +
   1.162 +fun cons_entry ((key, entry), tab) =
   1.163 +  update ((key, entry :: lookup_multi (tab, key)), tab);
   1.164 +
   1.165 +fun make_multi pairs = foldr cons_entry (pairs, empty);
   1.166 +
   1.167 +fun dest_multi tab =
   1.168 +  flat (map (fn (key, xs) => map (pair key) xs) (dest tab));
   1.169 +
   1.170 +
   1.171 +(* map *)
   1.172 +
   1.173 +fun map _ Empty = Empty
   1.174 +  | map f (Branch2 (left, (k, x), right)) =
   1.175 +      Branch2 (map f left, (k, f x), map f right)
   1.176 +  | map f (Branch3 (left, (k1, x1), mid, (k2, x2), right)) =
   1.177 +      Branch3 (map f left, (k1, f x1), map f mid, (k2, f x2), map f right);
   1.178 +
   1.179 +
   1.180 +end;
   1.181 +
   1.182 +
   1.183 +(*tables indexed by strings*)
   1.184 +structure Symtab = TableFun(type key = string val ord = string_ord);
   1.185 +
   1.186 +(* FIXME demo *)
   1.187 +structure IntTab = TableFun(type key = int val ord = int_ord);
   1.188 +val make = IntTab.make o map (rpair ());
   1.189 +fun dest tab = IntTab.dest tab |> map fst;