--- a/src/Pure/General/set.ML Wed Mar 29 12:05:56 2023 +0200
+++ b/src/Pure/General/set.ML Wed Mar 29 12:24:50 2023 +0200
@@ -37,8 +37,6 @@
structure Key = Key;
type elem = Key.key;
-val eq_key = is_equal o Key.ord;
-
(* datatype *)
@@ -197,29 +195,32 @@
fun member set elem =
let
+ fun elem_ord e = Key.ord (elem, e)
+ val elem_eq = is_equal o elem_ord;
+
fun mem Empty = false
- | mem (Leaf1 e) = eq_key (elem, e)
+ | mem (Leaf1 e) = elem_eq e
| mem (Leaf2 (e1, e2)) =
- (case Key.ord (elem, e1) of
+ (case elem_ord e1 of
LESS => false
| EQUAL => true
- | GREATER => eq_key (elem, e2))
+ | GREATER => elem_eq e2)
| mem (Leaf3 (e1, e2, e3)) =
- (case Key.ord (elem, e2) of
- LESS => eq_key (elem, e1)
+ (case elem_ord e2 of
+ LESS => elem_eq e1
| EQUAL => true
- | GREATER => eq_key (elem, e3))
+ | GREATER => elem_eq e3)
| mem (Branch2 (left, e, right)) =
- (case Key.ord (elem, e) of
+ (case elem_ord e of
LESS => mem left
| EQUAL => true
| GREATER => mem right)
| mem (Branch3 (left, e1, mid, e2, right)) =
- (case Key.ord (elem, e1) of
+ (case elem_ord e1 of
LESS => mem left
| EQUAL => true
| GREATER =>
- (case Key.ord (elem, e2) of
+ (case elem_ord e2 of
LESS => mem mid
| EQUAL => true
| GREATER => mem right));
@@ -247,12 +248,14 @@
if member set elem then set
else
let
+ fun elem_ord e = Key.ord (elem, e)
+
fun ins Empty = Sprout (Empty, elem, Empty)
| ins (t as Leaf1 _) = ins (unmake t)
| ins (t as Leaf2 _) = ins (unmake t)
| ins (t as Leaf3 _) = ins (unmake t)
| ins (Branch2 (left, e, right)) =
- (case Key.ord (elem, e) of
+ (case elem_ord e of
LESS =>
(case ins left of
Stay left' => Stay (make2 (left', e, right))
@@ -264,7 +267,7 @@
| Sprout (right1, e', right2) =>
Stay (make3 (left, e, right1, e', right2))))
| ins (Branch3 (left, e1, mid, e2, right)) =
- (case Key.ord (elem, e1) of
+ (case elem_ord e1 of
LESS =>
(case ins left of
Stay left' => Stay (make3 (left', e1, mid, e2, right))
@@ -272,7 +275,7 @@
Sprout (make2 (left1, e', left2), e1, make2 (mid, e2, right)))
| EQUAL => Stay (make3 (left, e1, mid, e2, right))
| GREATER =>
- (case Key.ord (elem, e2) of
+ (case elem_ord e2 of
LESS =>
(case ins mid of
Stay mid' => Stay (make3 (left, e1, mid', e2, right))
--- a/src/Pure/General/table.ML Wed Mar 29 12:05:56 2023 +0200
+++ b/src/Pure/General/table.ML Wed Mar 29 12:24:50 2023 +0200
@@ -71,8 +71,6 @@
structure Key = Key;
type key = Key.key;
-val eq_key = is_equal o Key.ord;
-
exception DUP of key;
@@ -252,30 +250,33 @@
fun lookup tab key =
let
+ fun key_ord k = Key.ord (key, k);
+ val key_eq = is_equal o key_ord;
+
fun look Empty = NONE
| look (Leaf1 (k, x)) =
- if eq_key (key, k) then SOME x else NONE
+ if key_eq k then SOME x else NONE
| look (Leaf2 ((k1, x1), (k2, x2))) =
- (case Key.ord (key, k1) of
+ (case key_ord k1 of
LESS => NONE
| EQUAL => SOME x1
- | GREATER => if eq_key (key, k2) then SOME x2 else NONE)
+ | GREATER => if key_eq k2 then SOME x2 else NONE)
| look (Leaf3 ((k1, x1), (k2, x2), (k3, x3))) =
- (case Key.ord (key, k2) of
- LESS => if eq_key (key, k1) then SOME x1 else NONE
+ (case key_ord k2 of
+ LESS => if key_eq k1 then SOME x1 else NONE
| EQUAL => SOME x2
- | GREATER => if eq_key (key, k3) then SOME x3 else NONE)
+ | GREATER => if key_eq k3 then SOME x3 else NONE)
| look (Branch2 (left, (k, x), right)) =
- (case Key.ord (key, k) of
+ (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 (key, k1) of
+ (case key_ord k1 of
LESS => look left
| EQUAL => SOME x1
| GREATER =>
- (case Key.ord (key, k2) of
+ (case key_ord k2 of
LESS => look mid
| EQUAL => SOME x2
| GREATER => look right));
@@ -283,30 +284,33 @@
fun lookup_key tab key =
let
+ fun key_ord k = Key.ord (key, k);
+ val key_eq = is_equal o key_ord;
+
fun look Empty = NONE
| look (Leaf1 (k, x)) =
- if eq_key (key, k) then SOME (k, x) else NONE
+ if key_eq k then SOME (k, x) else NONE
| look (Leaf2 ((k1, x1), (k2, x2))) =
- (case Key.ord (key, k1) of
+ (case key_ord k1 of
LESS => NONE
| EQUAL => SOME (k1, x1)
- | GREATER => if eq_key (key, k2) then SOME (k2, x2) else NONE)
+ | GREATER => if key_eq k2 then SOME (k2, x2) else NONE)
| look (Leaf3 ((k1, x1), (k2, x2), (k3, x3))) =
- (case Key.ord (key, k2) of
- LESS => if eq_key (key, k1) then SOME (k1, x1) else NONE
+ (case key_ord k2 of
+ LESS => if key_eq k1 then SOME (k1, x1) else NONE
| EQUAL => SOME (k2, x2)
- | GREATER => if eq_key (key, k3) then SOME (k3, x3) else NONE)
+ | GREATER => if key_eq k3 then SOME (k3, x3) else NONE)
| look (Branch2 (left, (k, x), right)) =
- (case Key.ord (key, k) of
+ (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 (key, k1) of
+ (case key_ord k1 of
LESS => look left
| EQUAL => SOME (k1, x1)
| GREATER =>
- (case Key.ord (key, k2) of
+ (case key_ord k2 of
LESS => look mid
| EQUAL => SOME (k2, x2)
| GREATER => look right));
@@ -314,29 +318,32 @@
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, _)) = eq_key (key, k)
+ | def (Leaf1 (k, _)) = key_eq k
| def (Leaf2 ((k1, _), (k2, _))) =
- (case Key.ord (key, k1) of
+ (case key_ord k1 of
LESS => false
| EQUAL => true
- | GREATER => eq_key (key, k2))
+ | GREATER => key_eq k2)
| def (Leaf3 ((k1, _), (k2, _), (k3, _))) =
- (case Key.ord (key, k2) of
- LESS => eq_key (key, k1)
+ (case key_ord k2 of
+ LESS => key_eq k1
| EQUAL => true
- | GREATER => eq_key (key, k3))
+ | GREATER => key_eq k3)
| def (Branch2 (left, (k, _), right)) =
- (case Key.ord (key, k) of
+ (case key_ord k of
LESS => def left
| EQUAL => true
| GREATER => def right)
| def (Branch3 (left, (k1, _), mid, (k2, _), right)) =
- (case Key.ord (key, k1) of
+ (case key_ord k1 of
LESS => def left
| EQUAL => true
| GREATER =>
- (case Key.ord (key, k2) of
+ (case key_ord k2 of
LESS => def mid
| EQUAL => true
| GREATER => def right));
@@ -353,12 +360,14 @@
fun modify key f tab =
let
+ fun key_ord k = Key.ord (key, k);
+
fun modfy Empty = Sprout (Empty, (key, f NONE), 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 (key, k) of
+ (case key_ord k of
LESS =>
(case modfy left of
Stay left' => Stay (make2 (left', p, right))
@@ -370,7 +379,7 @@
| 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 (key, k1) of
+ (case key_ord k1 of
LESS =>
(case modfy left of
Stay left' => Stay (make3 (left', p1, mid, p2, right))
@@ -378,7 +387,7 @@
Sprout (make2 (left1, q, left2), p1, make2 (mid, p2, right)))
| EQUAL => Stay (make3 (left, (k1, f (SOME x1)), mid, p2, right))
| GREATER =>
- (case Key.ord (key, k2) of
+ (case key_ord k2 of
LESS =>
(case modfy mid of
Stay mid' => Stay (make3 (left, p1, mid', p2, right))