# HG changeset patch
# User wenzelm
# Date 897472417 -7200
# Node ID 44fd9e09c6377542c287f48ac2e4d64bf19ef1ba
# Parent  32e6cab5e7d482027ced6a69c38b5b7f5db902d3
moved table.ML to General/table.ML;

diff -r 32e6cab5e7d4 -r 44fd9e09c637 src/Pure/General/table.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/General/table.ML	Wed Jun 10 11:53:37 1998 +0200
@@ -0,0 +1,181 @@
+(*  Title:      Pure/table.ML
+    ID:         $Id$
+    Author:     Markus Wenzel, TU Muenchen
+
+Generic tables and tables indexed by strings.  No delete operation.
+Implemented as balanced 2-3 trees.
+*)
+
+signature KEY =
+sig
+  type key
+  val ord: key * key -> order
+end;
+
+signature TABLE =
+sig
+  type key
+  type 'a table
+  exception DUP of key
+  exception DUPS of key list
+  val empty: 'a table
+  val is_empty: 'a table -> bool
+  val dest: 'a table -> (key * 'a) list
+  val lookup: 'a table * key -> 'a option
+  val update: (key * 'a) * 'a table -> 'a table
+  val update_new: (key * 'a) * 'a table -> 'a table                 (*exception DUP*)
+  val make: (key * 'a) list -> 'a table                             (*exception DUPS*)
+  val extend: 'a table * (key * 'a) list -> 'a table                (*exception DUPS*)
+  val merge: ('a * 'a -> bool) -> 'a table * 'a table -> 'a table   (*exception DUPS*)
+  val lookup_multi: 'a list table * key -> 'a list
+  val make_multi: (key * 'a) list -> 'a list table
+  val dest_multi: 'a list table -> (key * 'a) list
+  val map: ('a -> 'b) -> 'a table -> 'b table
+end;
+
+functor TableFun(Key: KEY): TABLE =
+struct
+
+
+(* datatype table *)
+
+type key = Key.key;
+
+datatype 'a table =
+  Empty |
+  Branch2 of 'a table * (key * 'a) * 'a table |
+  Branch3 of 'a table * (key * 'a) * 'a table * (key * 'a) * 'a table;
+
+exception DUP of key;
+exception DUPS of key list;
+
+
+val empty = Empty;
+
+fun is_empty Empty = true
+  | is_empty _ = false;
+
+fun dest Empty = []
+  | dest (Branch2 (left, p, right)) = dest left @ [p] @ dest right
+  | dest (Branch3 (left, p1, mid, p2, right)) =
+      dest left @ [p1] @ dest mid @ [p2] @ dest right;
+
+
+(* lookup *)
+
+fun lookup (Empty, _) = None
+  | lookup (Branch2 (left, (k, x), right), key) =
+      (case Key.ord (key, k) of
+        LESS => lookup (left, key)
+      | EQUAL => Some x
+      | GREATER => lookup (right, key))
+  | lookup (Branch3 (left, (k1, x1), mid, (k2, x2), right), key) =
+      (case Key.ord (key, k1) of
+        LESS => lookup (left, key)
+      | EQUAL => Some x1
+      | GREATER =>
+          (case Key.ord (key, k2) of
+            LESS => lookup (mid, key)
+          | EQUAL => Some x2
+          | GREATER => lookup (right, key)));
+
+
+(* update *)
+
+fun compare (k1, _) (k2, _) = Key.ord (k1, k2);
+
+datatype 'a growth =
+  Stay of 'a table |
+  Sprout of 'a table * (key * 'a) * 'a table;
+
+fun insert pair Empty = Sprout (Empty, pair, Empty)
+  | insert pair (Branch2 (left, p, right)) =
+      (case compare pair p of
+        LESS =>
+          (case insert pair left of
+            Stay left' => Stay (Branch2 (left', p, right))
+          | Sprout (left1, q, left2) => Stay (Branch3 (left1, q, left2, p, right)))
+      | EQUAL => Stay (Branch2 (left, pair, right))
+      | GREATER =>
+          (case insert pair right of
+            Stay right' => Stay (Branch2 (left, p, right'))
+          | Sprout (right1, q, right2) =>
+              Stay (Branch3 (left, p, right1, q, right2))))
+  | insert pair (Branch3 (left, p1, mid, p2, right)) =
+      (case compare pair p1 of
+        LESS =>
+          (case insert pair left of
+            Stay left' => Stay (Branch3 (left', p1, mid, p2, right))
+          | Sprout (left1, q, left2) =>
+              Sprout (Branch2 (left1, q, left2), p1, Branch2 (mid, p2, right)))
+      | EQUAL => Stay (Branch3 (left, pair, mid, p2, right))
+      | GREATER =>
+          (case compare pair p2 of
+            LESS =>
+              (case insert pair mid of
+                Stay mid' => Stay (Branch3 (left, p1, mid', p2, right))
+              | Sprout (mid1, q, mid2) =>
+                  Sprout (Branch2 (left, p1, mid1), q, Branch2 (mid2, p2, right)))
+          | EQUAL => Stay (Branch3 (left, p1, mid, pair, right))
+          | GREATER =>
+              (case insert pair right of
+                Stay right' => Stay (Branch3 (left, p1, mid, p2, right'))
+              | Sprout (right1, q, right2) =>
+                  Sprout (Branch2 (left, p1, mid), p2, Branch2 (right1, q, right2)))));
+
+fun update (pair, tab) =
+  (case insert pair tab of
+    Stay tab => tab
+  | Sprout br => Branch2 br);
+
+fun update_new (pair as (key, _), tab) =
+  if is_none (lookup (tab, key)) then update (pair, tab)
+  else raise DUP key;
+
+
+(* make, extend, merge tables *)
+
+fun add eq ((tab, dups), (key, x)) =
+  (case lookup (tab, key) of
+    None => (update ((key, x), tab), dups)
+  | Some x' =>
+      if eq (x, x') then (tab, dups)
+      else (tab, dups @ [key]));
+
+fun enter eq (tab, pairs) =
+  (case foldl (add eq) ((tab, []), pairs) of
+    (tab', []) => tab'
+  | (_, dups) => raise DUPS dups);
+
+fun extend tab_pairs = enter (K false) tab_pairs;
+fun make pairs = extend (empty, pairs);
+fun merge eq (tab1, tab2) = enter eq (tab1, dest tab2);
+
+
+(* tables with multiple entries per key (preserving order) *)
+
+fun lookup_multi tab_key = if_none (lookup tab_key) [];
+
+fun cons_entry ((key, x), tab) =
+  update ((key, x :: lookup_multi (tab, key)), tab);
+
+fun make_multi pairs = foldr cons_entry (pairs, empty);
+
+fun dest_multi tab =
+  flat (map (fn (key, xs) => map (Library.pair key) xs) (dest tab));
+
+
+(* map *)
+
+fun map _ Empty = Empty
+  | map f (Branch2 (left, (k, x), right)) =
+      Branch2 (map f left, (k, f x), map f right)
+  | map f (Branch3 (left, (k1, x1), mid, (k2, x2), right)) =
+      Branch3 (map f left, (k1, f x1), map f mid, (k2, f x2), map f right);
+
+
+end;
+
+
+(*tables indexed by strings*)
+structure Symtab = TableFun(type key = string val ord = string_ord);
diff -r 32e6cab5e7d4 -r 44fd9e09c637 src/Pure/table.ML
--- a/src/Pure/table.ML	Wed Jun 10 11:52:59 1998 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,181 +0,0 @@
-(*  Title:      Pure/table.ML
-    ID:         $Id$
-    Author:     Markus Wenzel, TU Muenchen
-
-Generic tables and tables indexed by strings.  No delete operation.
-Implemented as balanced 2-3 trees.
-*)
-
-signature KEY =
-sig
-  type key
-  val ord: key * key -> order
-end;
-
-signature TABLE =
-sig
-  type key
-  type 'a table
-  exception DUP of key
-  exception DUPS of key list
-  val empty: 'a table
-  val is_empty: 'a table -> bool
-  val dest: 'a table -> (key * 'a) list
-  val lookup: 'a table * key -> 'a option
-  val update: (key * 'a) * 'a table -> 'a table
-  val update_new: (key * 'a) * 'a table -> 'a table                 (*exception DUP*)
-  val make: (key * 'a) list -> 'a table                             (*exception DUPS*)
-  val extend: 'a table * (key * 'a) list -> 'a table                (*exception DUPS*)
-  val merge: ('a * 'a -> bool) -> 'a table * 'a table -> 'a table   (*exception DUPS*)
-  val lookup_multi: 'a list table * key -> 'a list
-  val make_multi: (key * 'a) list -> 'a list table
-  val dest_multi: 'a list table -> (key * 'a) list
-  val map: ('a -> 'b) -> 'a table -> 'b table
-end;
-
-functor TableFun(Key: KEY): TABLE =
-struct
-
-
-(* datatype table *)
-
-type key = Key.key;
-
-datatype 'a table =
-  Empty |
-  Branch2 of 'a table * (key * 'a) * 'a table |
-  Branch3 of 'a table * (key * 'a) * 'a table * (key * 'a) * 'a table;
-
-exception DUP of key;
-exception DUPS of key list;
-
-
-val empty = Empty;
-
-fun is_empty Empty = true
-  | is_empty _ = false;
-
-fun dest Empty = []
-  | dest (Branch2 (left, p, right)) = dest left @ [p] @ dest right
-  | dest (Branch3 (left, p1, mid, p2, right)) =
-      dest left @ [p1] @ dest mid @ [p2] @ dest right;
-
-
-(* lookup *)
-
-fun lookup (Empty, _) = None
-  | lookup (Branch2 (left, (k, x), right), key) =
-      (case Key.ord (key, k) of
-        LESS => lookup (left, key)
-      | EQUAL => Some x
-      | GREATER => lookup (right, key))
-  | lookup (Branch3 (left, (k1, x1), mid, (k2, x2), right), key) =
-      (case Key.ord (key, k1) of
-        LESS => lookup (left, key)
-      | EQUAL => Some x1
-      | GREATER =>
-          (case Key.ord (key, k2) of
-            LESS => lookup (mid, key)
-          | EQUAL => Some x2
-          | GREATER => lookup (right, key)));
-
-
-(* update *)
-
-fun compare (k1, _) (k2, _) = Key.ord (k1, k2);
-
-datatype 'a growth =
-  Stay of 'a table |
-  Sprout of 'a table * (key * 'a) * 'a table;
-
-fun insert pair Empty = Sprout (Empty, pair, Empty)
-  | insert pair (Branch2 (left, p, right)) =
-      (case compare pair p of
-        LESS =>
-          (case insert pair left of
-            Stay left' => Stay (Branch2 (left', p, right))
-          | Sprout (left1, q, left2) => Stay (Branch3 (left1, q, left2, p, right)))
-      | EQUAL => Stay (Branch2 (left, pair, right))
-      | GREATER =>
-          (case insert pair right of
-            Stay right' => Stay (Branch2 (left, p, right'))
-          | Sprout (right1, q, right2) =>
-              Stay (Branch3 (left, p, right1, q, right2))))
-  | insert pair (Branch3 (left, p1, mid, p2, right)) =
-      (case compare pair p1 of
-        LESS =>
-          (case insert pair left of
-            Stay left' => Stay (Branch3 (left', p1, mid, p2, right))
-          | Sprout (left1, q, left2) =>
-              Sprout (Branch2 (left1, q, left2), p1, Branch2 (mid, p2, right)))
-      | EQUAL => Stay (Branch3 (left, pair, mid, p2, right))
-      | GREATER =>
-          (case compare pair p2 of
-            LESS =>
-              (case insert pair mid of
-                Stay mid' => Stay (Branch3 (left, p1, mid', p2, right))
-              | Sprout (mid1, q, mid2) =>
-                  Sprout (Branch2 (left, p1, mid1), q, Branch2 (mid2, p2, right)))
-          | EQUAL => Stay (Branch3 (left, p1, mid, pair, right))
-          | GREATER =>
-              (case insert pair right of
-                Stay right' => Stay (Branch3 (left, p1, mid, p2, right'))
-              | Sprout (right1, q, right2) =>
-                  Sprout (Branch2 (left, p1, mid), p2, Branch2 (right1, q, right2)))));
-
-fun update (pair, tab) =
-  (case insert pair tab of
-    Stay tab => tab
-  | Sprout br => Branch2 br);
-
-fun update_new (pair as (key, _), tab) =
-  if is_none (lookup (tab, key)) then update (pair, tab)
-  else raise DUP key;
-
-
-(* make, extend, merge tables *)
-
-fun add eq ((tab, dups), (key, x)) =
-  (case lookup (tab, key) of
-    None => (update ((key, x), tab), dups)
-  | Some x' =>
-      if eq (x, x') then (tab, dups)
-      else (tab, dups @ [key]));
-
-fun enter eq (tab, pairs) =
-  (case foldl (add eq) ((tab, []), pairs) of
-    (tab', []) => tab'
-  | (_, dups) => raise DUPS dups);
-
-fun extend tab_pairs = enter (K false) tab_pairs;
-fun make pairs = extend (empty, pairs);
-fun merge eq (tab1, tab2) = enter eq (tab1, dest tab2);
-
-
-(* tables with multiple entries per key (preserving order) *)
-
-fun lookup_multi tab_key = if_none (lookup tab_key) [];
-
-fun cons_entry ((key, x), tab) =
-  update ((key, x :: lookup_multi (tab, key)), tab);
-
-fun make_multi pairs = foldr cons_entry (pairs, empty);
-
-fun dest_multi tab =
-  flat (map (fn (key, xs) => map (Library.pair key) xs) (dest tab));
-
-
-(* map *)
-
-fun map _ Empty = Empty
-  | map f (Branch2 (left, (k, x), right)) =
-      Branch2 (map f left, (k, f x), map f right)
-  | map f (Branch3 (left, (k1, x1), mid, (k2, x2), right)) =
-      Branch3 (map f left, (k1, f x1), map f mid, (k2, f x2), map f right);
-
-
-end;
-
-
-(*tables indexed by strings*)
-structure Symtab = TableFun(type key = string val ord = string_ord);