# HG changeset patch
# User wenzelm
# Date 1701347106 -3600
# Node ID 6c5ca8f04d60956edb4646cdec052a6c932eea29
# Parent  06176f4e2e707d9e912f82cbdfa01c7d86dd6271
misc tuning and clarification;

diff -r 06176f4e2e70 -r 6c5ca8f04d60 src/Pure/General/table.ML
--- a/src/Pure/General/table.ML	Thu Nov 30 12:23:47 2023 +0100
+++ b/src/Pure/General/table.ML	Thu Nov 30 13:25:06 2023 +0100
@@ -289,111 +289,45 @@
   in get end;
 
 
-(* lookup *)
-
-fun lookup tab key =
-  let
-    fun key_ord k = Key.ord (key, k);
-    val key_eq = is_equal o key_ord;
+(* retrieve *)
 
-    fun look Empty = NONE
-      | look (Leaf1 (k, x)) =
-          if key_eq k then SOME x else NONE
-      | look (Leaf2 ((k1, x1), (k2, x2))) =
-          (case key_ord k1 of
-            LESS => NONE
-          | EQUAL => SOME x1
-          | GREATER => if key_eq k2 then SOME x2 else NONE)
-      | look (Leaf3 ((k1, x1), (k2, x2), (k3, x3))) =
-          (case key_ord k2 of
-            LESS => if key_eq k1 then SOME x1 else NONE
-          | EQUAL => SOME x2
-          | GREATER => if key_eq k3 then SOME x3 else NONE)
-      | look (Branch2 (left, (k, x), right)) =
-          (case key_ord k of
-            LESS => look left
-          | EQUAL => SOME x
-          | GREATER => look right)
-      | look (Branch3 (left, (k1, x1), mid, (k2, x2), right)) =
-          (case key_ord k1 of
-            LESS => look left
-          | EQUAL => SOME x1
-          | GREATER =>
-              (case key_ord k2 of
-                LESS => look mid
-              | EQUAL => SOME x2
-              | GREATER => look right))
-      | look (Size (_, arg)) = look arg;
-  in look tab end;
-
-fun lookup_key tab key =
+fun retrieve {result, no_result} tab (key: key) =
   let
-    fun key_ord k = Key.ord (key, k);
-    val key_eq = is_equal o key_ord;
+    fun compare (k, _) = Key.ord (key, k)
+    fun result_equal e = if is_equal (compare e) then result e else no_result;
 
-    fun look Empty = NONE
-      | look (Leaf1 (k, x)) =
-          if key_eq k then SOME (k, x) else NONE
-      | look (Leaf2 ((k1, x1), (k2, x2))) =
-          (case key_ord k1 of
-            LESS => NONE
-          | EQUAL => SOME (k1, x1)
-          | GREATER => if key_eq k2 then SOME (k2, x2) else NONE)
-      | look (Leaf3 ((k1, x1), (k2, x2), (k3, x3))) =
-          (case key_ord k2 of
-            LESS => if key_eq k1 then SOME (k1, x1) else NONE
-          | EQUAL => SOME (k2, x2)
-          | GREATER => if key_eq k3 then SOME (k3, x3) else NONE)
-      | look (Branch2 (left, (k, x), right)) =
-          (case key_ord k of
-            LESS => look left
-          | EQUAL => SOME (k, x)
-          | GREATER => look right)
-      | look (Branch3 (left, (k1, x1), mid, (k2, x2), right)) =
-          (case key_ord k1 of
-            LESS => look left
-          | EQUAL => SOME (k1, x1)
+    fun find Empty = no_result
+      | find (Leaf1 e) = result_equal e
+      | find (Leaf2 (e1, e2)) =
+          (case compare e1 of
+            LESS => no_result
+          | EQUAL => result e1
+          | GREATER => result_equal e2)
+      | find (Leaf3 (e1, e2, e3)) =
+          (case compare e2 of
+            LESS => result_equal e1
+          | EQUAL => result e2
+          | GREATER => result_equal e3)
+      | find (Branch2 (left, e, right)) =
+          (case compare e of
+            LESS => find left
+          | EQUAL => result e
+          | GREATER => find right)
+      | find (Branch3 (left, e1, mid, e2, right)) =
+          (case compare e1 of
+            LESS => find left
+          | EQUAL => result e1
           | GREATER =>
-              (case key_ord k2 of
-                LESS => look mid
-              | EQUAL => SOME (k2, x2)
-              | GREATER => look right))
-      | look (Size (_, arg)) = look arg;
-  in look tab end;
+              (case compare e2 of
+                LESS => find mid
+              | EQUAL => result e2
+              | GREATER => find right))
+      | find (Size (_, arg)) = find arg;
+  in find tab end;
 
-fun defined tab key =
-  let
-    fun key_ord k = Key.ord (key, k);
-    val key_eq = is_equal o key_ord;
-
-    fun def Empty = false
-      | def (Leaf1 (k, _)) = key_eq k
-      | def (Leaf2 ((k1, _), (k2, _))) =
-          (case key_ord k1 of
-            LESS => false
-          | EQUAL => true
-          | GREATER => key_eq k2)
-      | def (Leaf3 ((k1, _), (k2, _), (k3, _))) =
-          (case key_ord k2 of
-            LESS => key_eq k1
-          | EQUAL => true
-          | GREATER => key_eq k3)
-      | def (Branch2 (left, (k, _), right)) =
-          (case key_ord k of
-            LESS => def left
-          | EQUAL => true
-          | GREATER => def right)
-      | def (Branch3 (left, (k1, _), mid, (k2, _), right)) =
-          (case key_ord k1 of
-            LESS => def left
-          | EQUAL => true
-          | GREATER =>
-              (case key_ord k2 of
-                LESS => def mid
-              | EQUAL => true
-              | GREATER => def right))
-      | def (Size (_, arg)) = def arg;
-  in def tab end;
+fun lookup tab key = retrieve {result = SOME o #2, no_result = NONE} tab key;
+fun lookup_key tab key = retrieve {result = SOME, no_result = NONE} tab key;
+fun defined tab key = retrieve {result = K true, no_result = false} tab key;
 
 
 (* modify *)
@@ -406,68 +340,68 @@
 
 fun modify key f tab =
   let
-    fun key_ord k = Key.ord (key, k);
+    fun compare (k, _) = Key.ord (key, k)
 
     val inc = Unsynchronized.ref 0;
-    fun insert () = f NONE before ignore (Unsynchronized.inc inc);
-    fun update x = f (SOME x);
+    fun insert (k: key) = (k, f NONE) before ignore (Unsynchronized.inc inc);
+    fun update (k: key, x) = (k, f (SOME x));
 
-    fun modfy Empty = Sprout (Empty, (key, insert ()), Empty)
+    fun modfy Empty = Sprout (Empty, (insert key), Empty)
       | modfy (t as Leaf1 _) = modfy (unmake t)
       | modfy (t as Leaf2 _) = modfy (unmake t)
       | modfy (t as Leaf3 _) = modfy (unmake t)
-      | modfy (Branch2 (left, p as (k, x), right)) =
-          (case key_ord k of
+      | modfy (Branch2 (left, e, right)) =
+          (case compare e of
             LESS =>
               (case modfy left of
-                Stay left' => Stay (make2 (left', p, right))
-              | Sprout (left1, q, left2) => Stay (make3 (left1, q, left2, p, right)))
-          | EQUAL => Stay (make2 (left, (k, update x), right))
+                Stay left' => Stay (make2 (left', e, right))
+              | Sprout (left1, e', left2) => Stay (make3 (left1, e', left2, e, right)))
+          | EQUAL => Stay (make2 (left, update e, right))
           | GREATER =>
               (case modfy right of
-                Stay right' => Stay (make2 (left, p, right'))
-              | Sprout (right1, q, right2) =>
-                  Stay (make3 (left, p, right1, q, right2))))
-      | modfy (Branch3 (left, p1 as (k1, x1), mid, p2 as (k2, x2), right)) =
-          (case key_ord k1 of
+                Stay right' => Stay (make2 (left, e, right'))
+              | Sprout (right1, e', right2) =>
+                  Stay (make3 (left, e, right1, e', right2))))
+      | modfy (Branch3 (left, e1, mid, e2, right)) =
+          (case compare e1 of
             LESS =>
               (case modfy left of
-                Stay left' => Stay (make3 (left', p1, mid, p2, right))
-              | Sprout (left1, q, left2) =>
-                  Sprout (make2 (left1, q, left2), p1, make2 (mid, p2, right)))
-          | EQUAL => Stay (make3 (left, (k1, update x1), mid, p2, right))
+                Stay left' => Stay (make3 (left', e1, mid, e2, right))
+              | Sprout (left1, e', left2) =>
+                  Sprout (make2 (left1, e', left2), e1, make2 (mid, e2, right)))
+          | EQUAL => Stay (make3 (left, update e1, mid, e2, right))
           | GREATER =>
-              (case key_ord k2 of
+              (case compare e2 of
                 LESS =>
                   (case modfy mid of
-                    Stay mid' => Stay (make3 (left, p1, mid', p2, right))
-                  | Sprout (mid1, q, mid2) =>
-                      Sprout (make2 (left, p1, mid1), q, make2 (mid2, p2, right)))
-              | EQUAL => Stay (make3 (left, p1, mid, (k2, update x2), right))
+                    Stay mid' => Stay (make3 (left, e1, mid', e2, right))
+                  | Sprout (mid1, e', mid2) =>
+                      Sprout (make2 (left, e1, mid1), e', make2 (mid2, e2, right)))
+              | EQUAL => Stay (make3 (left, e1, mid, update e2, right))
               | GREATER =>
                   (case modfy right of
-                    Stay right' => Stay (make3 (left, p1, mid, p2, right'))
+                    Stay right' => Stay (make3 (left, e1, mid, e2, right'))
                   | Sprout (right1, q, right2) =>
-                      Sprout (make2 (left, p1, mid), p2, make2 (right1, q, right2)))))
+                      Sprout (make2 (left, e1, mid), e2, make2 (right1, q, right2)))))
       | modfy (Size (_, arg)) = modfy arg;
 
     val tab' =
       (case tab of
-        Empty => Leaf1 (key, insert ())
-      | Leaf1 (k, x) =>
-          (case key_ord k of
-            LESS => Leaf2 ((key, insert ()), (k, x))
-          | EQUAL => Leaf1 ((k, update x))
-          | GREATER => Leaf2 ((k, x), (key, insert ())))
-      | Leaf2 ((k1, x1), (k2, x2)) =>
-          (case key_ord k1 of
-            LESS => Leaf3 ((key, insert ()), (k1, x1), (k2, x2))
-          | EQUAL => Leaf2 ((k1, update x1), (k2, x2))
+        Empty => Leaf1 (insert key)
+      | Leaf1 e =>
+          (case compare e of
+            LESS => Leaf2 (insert key, e)
+          | EQUAL => Leaf1 (update e)
+          | GREATER => Leaf2 (e, insert key))
+      | Leaf2 (e1, e2) =>
+          (case compare e1 of
+            LESS => Leaf3 (insert key, e1, e2)
+          | EQUAL => Leaf2 (update e1, e2)
           | GREATER =>
-              (case key_ord k2 of
-                LESS => Leaf3 ((k1, x1), (key, insert ()), (k2, x2))
-              | EQUAL => Leaf2 ((k1, x1), (k2, update x2))
-              | GREATER => Leaf3 ((k1, x1), (k2, x2), (key, insert ()))))
+              (case compare e2 of
+                LESS => Leaf3 (e1, insert key, e2)
+              | EQUAL => Leaf2 (e1, update e2)
+              | GREATER => Leaf3 (e1, e2, insert key)))
       | _ =>
           (case modfy tab of
             Stay tab' => tab'