--- 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'