# HG changeset patch
# User wenzelm
# Date 1681126991 -7200
# Node ID 9a30b76a6f60368742d9e43dde2a97cae3ad93a7
# Parent  3fb2c47a7605eb39d50e5ce33447acb5703b2b3c
performance tuning;

diff -r 3fb2c47a7605 -r 9a30b76a6f60 src/Pure/General/set.ML
--- a/src/Pure/General/set.ML	Sun Apr 09 23:09:24 2023 +0200
+++ b/src/Pure/General/set.ML	Mon Apr 10 13:43:11 2023 +0200
@@ -46,7 +46,8 @@
   Leaf2 of elem * elem |
   Leaf3 of elem * elem * elem |
   Branch2 of T * elem * T |
-  Branch3 of T * elem * T * elem * T;
+  Branch3 of T * elem * T * elem * T |
+  Size of int * T;
 
 (*literal copy from table.ML*)
 fun make2 (Empty, e, Empty) = Leaf1 e
@@ -76,19 +77,24 @@
   | unmake (Leaf2 (e1, e2)) = Branch3 (Empty, e1, Empty, e2, Empty)
   | unmake (Leaf3 (e1, e2, e3)) =
       Branch2 (Branch2 (Empty, e1, Empty), e2, Branch2 (Empty, e3, Empty))
+  | unmake (Size (_, arg)) = arg
   | unmake arg = arg;
 
 
 (* size *)
 
 (*literal copy from table.ML*)
+fun make_size m arg = if m > 12 then Size (m, arg) else arg;
+
+(*literal copy from table.ML*)
 local
   fun count Empty n = n
     | count (Leaf1 _) n = n + 1
     | count (Leaf2 _) n = n + 2
     | count (Leaf3 _) n = n + 3
     | count (Branch2 (left, _, right)) n = count right (count left (n + 1))
-    | count (Branch3 (left, _, mid, _, right)) n = count right (count mid (count left (n + 2)));
+    | count (Branch3 (left, _, mid, _, right)) n = count right (count mid (count left (n + 2)))
+    | count (Size (m, _)) n = m + n;
 in
   val size = Integer.build o count;
 end;
@@ -100,7 +106,9 @@
 
 fun build (f: T -> T) = f empty;
 
+(*literal copy from table.ML*)
 fun is_empty Empty = true
+  | is_empty (Size (_, arg)) = is_empty arg
   | is_empty _ = false;
 
 
@@ -115,7 +123,8 @@
       | fold (Branch2 (left, e, right)) x =
           fold right (f e (fold left x))
       | fold (Branch3 (left, e1, mid, e2, right)) x =
-          fold right (f e2 (fold mid (f e1 (fold left x))));
+          fold right (f e2 (fold mid (f e1 (fold left x))))
+      | fold (Size (_, arg)) x = fold arg x;
   in fold end;
 
 fun fold_rev_set f =
@@ -127,7 +136,8 @@
       | fold_rev (Branch2 (left, e, right)) x =
           fold_rev left (f e (fold_rev right x))
       | fold_rev (Branch3 (left, e1, mid, e2, right)) x =
-          fold_rev left (f e1 (fold_rev mid (f e2 (fold_rev right x))));
+          fold_rev left (f e1 (fold_rev mid (f e2 (fold_rev right x))))
+      | fold_rev (Size (_, arg)) x = fold_rev arg x;
   in fold_rev end;
 
 val dest = Library.build o fold_rev_set cons;
@@ -144,7 +154,8 @@
       | ex (Branch2 (left, e, right)) =
           ex left orelse pred e orelse ex right
       | ex (Branch3 (left, e1, mid, e2, right)) =
-          ex left orelse pred e1 orelse ex mid orelse pred e2 orelse ex right;
+          ex left orelse pred e1 orelse ex mid orelse pred e2 orelse ex right
+      | ex (Size (_, arg)) = ex arg;
   in ex end;
 
 fun forall pred = not o exists (not o pred);
@@ -186,7 +197,8 @@
                       | some => some)
                   | some => some)
               | some => some)
-          | some => some);
+          | some => some)
+      | get (Size (_, arg)) = get arg;
   in get end;
 
 
@@ -222,7 +234,8 @@
               (case elem_ord e2 of
                 LESS => mem mid
               | EQUAL => true
-              | GREATER => mem right));
+              | GREATER => mem right))
+      | mem (Size (_, arg)) = mem arg;
   in mem set end;
 
 
@@ -285,11 +298,13 @@
                     (case ins right of
                       Stay right' => Stay (make3 (left, e1, mid, e2, right'))
                     | Sprout (right1, e', right2) =>
-                        Sprout (make2 (left, e1, mid), e2, make2 (right1, e', right2)))));
+                        Sprout (make2 (left, e1, mid), e2, make2 (right1, e', right2)))))
+        | ins (Size (_, arg)) = ins arg;
     in
-      (case ins set of
-        Stay set' => set'
-      | Sprout br => make2 br)
+      make_size (size set + 1)
+        (case ins set of
+          Stay set' => set'
+        | Sprout br => make2 br)
     end;
 
 fun make elems = build (fold insert elems);
@@ -389,12 +404,15 @@
                   make2 (mr, if_equal ord q' q, r'))
             | (Branch3 (ll, lp, lm, lq, lr), Branch2 (ml, mp, mr)) =>
                 make3 (make2 (ll, lp, lm), lq, make2 (lr, p, ml), mp,
-                  make2 (mr, if_equal ord q' q, r'))))));
+                  make2 (mr, if_equal ord q' q, r'))))))
+  | del k (Size (_, arg)) = del k arg;
 
 in
 
 fun remove elem set =
-  if member set elem then snd (snd (del (SOME elem) set)) else set;
+  if member set elem
+  then make_size (size set - 1) (snd (snd (del (SOME elem) set)))
+  else set;
 
 val subtract = fold_set remove;
 
diff -r 3fb2c47a7605 -r 9a30b76a6f60 src/Pure/General/table.ML
--- a/src/Pure/General/table.ML	Sun Apr 09 23:09:24 2023 +0200
+++ b/src/Pure/General/table.ML	Mon Apr 10 13:43:11 2023 +0200
@@ -83,7 +83,8 @@
   Leaf2 of (key * 'a) * (key * 'a) |
   Leaf3 of (key * 'a) * (key * 'a) * (key * 'a) |
   Branch2 of 'a table * (key * 'a) * 'a table |
-  Branch3 of 'a table * (key * 'a) * 'a table * (key * 'a) * 'a table;
+  Branch3 of 'a table * (key * 'a) * 'a table * (key * 'a) * 'a table |
+  Size of int * 'a table;
 
 (*literal copy from set.ML*)
 fun make2 (Empty, e, Empty) = Leaf1 e
@@ -113,11 +114,15 @@
   | unmake (Leaf2 (e1, e2)) = Branch3 (Empty, e1, Empty, e2, Empty)
   | unmake (Leaf3 (e1, e2, e3)) =
       Branch2 (Branch2 (Empty, e1, Empty), e2, Branch2 (Empty, e3, Empty))
+  | unmake (Size (_, arg)) = arg
   | unmake arg = arg;
 
 
 (* size *)
 
+(*literal copy from set.ML*)
+fun make_size m arg = if m > 12 then Size (m, arg) else arg;
+
 local
   (*literal copy from set.ML*)
   fun count Empty n = n
@@ -125,7 +130,8 @@
     | count (Leaf2 _) n = n + 2
     | count (Leaf3 _) n = n + 3
     | count (Branch2 (left, _, right)) n = count right (count left (n + 1))
-    | count (Branch3 (left, _, mid, _, right)) n = count right (count mid (count left (n + 2)));
+    | count (Branch3 (left, _, mid, _, right)) n = count right (count mid (count left (n + 2)))
+    | count (Size (m, _)) n = m + n;
 in
   fun size tab = Integer.build (count tab);
 end;
@@ -137,7 +143,9 @@
 
 fun build (f: 'a table -> 'a table) = f empty;
 
+(*literal copy from set.ML*)
 fun is_empty Empty = true
+  | is_empty (Size (_, arg)) = is_empty arg
   | is_empty _ = false;
 
 
@@ -153,7 +161,8 @@
       | map (Branch2 (left, (k, x), right)) =
           Branch2 (map left, (k, f k x), map right)
       | map (Branch3 (left, (k1, x1), mid, (k2, x2), right)) =
-          Branch3 (map left, (k1, f k1 x1), map mid, (k2, f k2 x2), map right);
+          Branch3 (map left, (k1, f k1 x1), map mid, (k2, f k2 x2), map right)
+      | map (Size (m, arg)) = Size (m, map arg);
   in map end;
 
 fun fold_table f =
@@ -165,7 +174,8 @@
       | fold (Branch2 (left, e, right)) x =
           fold right (f e (fold left x))
       | fold (Branch3 (left, e1, mid, e2, right)) x =
-          fold right (f e2 (fold mid (f e1 (fold left x))));
+          fold right (f e2 (fold mid (f e1 (fold left x))))
+      | fold (Size (_, arg)) x = fold arg x;
   in fold end;
 
 fun fold_rev_table f =
@@ -177,7 +187,8 @@
       | fold_rev (Branch2 (left, e, right)) x =
           fold_rev left (f e (fold_rev right x))
       | fold_rev (Branch3 (left, e1, mid, e2, right)) x =
-          fold_rev left (f e1 (fold_rev mid (f e2 (fold_rev right x))));
+          fold_rev left (f e1 (fold_rev mid (f e2 (fold_rev right x))))
+      | fold_rev (Size (_, arg)) x = fold_rev arg x;
   in fold_rev end;
 
 fun dest tab = Library.build (fold_rev_table cons tab);
@@ -193,7 +204,8 @@
   | min (Branch2 (Empty, e, _)) = SOME e
   | min (Branch3 (Empty, e, _, _, _)) = SOME e
   | min (Branch2 (left, _, _)) = min left
-  | min (Branch3 (left, _, _, _, _)) = min left;
+  | min (Branch3 (left, _, _, _, _)) = min left
+  | min (Size (_, arg)) = min arg;
 
 fun max Empty = NONE
   | max (Leaf1 e) = SOME e
@@ -202,7 +214,8 @@
   | max (Branch2 (_, e, Empty)) = SOME e
   | max (Branch3 (_, _, _, e, Empty)) = SOME e
   | max (Branch2 (_, _, right)) = max right
-  | max (Branch3 (_, _, _, _, right)) = max right;
+  | max (Branch3 (_, _, _, _, right)) = max right
+  | max (Size (_, arg)) = max arg;
 
 
 (* exists and forall *)
@@ -216,7 +229,8 @@
       | ex (Branch2 (left, e, right)) =
           ex left orelse pred e orelse ex right
       | ex (Branch3 (left, e1, mid, e2, right)) =
-          ex left orelse pred e1 orelse ex mid orelse pred e2 orelse ex right;
+          ex left orelse pred e1 orelse ex mid orelse pred e2 orelse ex right
+      | ex (Size (_, arg)) = ex arg;
   in ex end;
 
 fun forall pred = not o exists (not o pred);
@@ -258,7 +272,8 @@
                       | some => some)
                   | some => some)
               | some => some)
-          | some => some);
+          | some => some)
+      | get (Size (_, arg)) = get arg;
   in get end;
 
 
@@ -295,7 +310,8 @@
               (case key_ord k2 of
                 LESS => look mid
               | EQUAL => SOME x2
-              | GREATER => look right));
+              | GREATER => look right))
+      | look (Size (_, arg)) = look arg;
   in look tab end;
 
 fun lookup_key tab key =
@@ -329,7 +345,8 @@
               (case key_ord k2 of
                 LESS => look mid
               | EQUAL => SOME (k2, x2)
-              | GREATER => look right));
+              | GREATER => look right))
+      | look (Size (_, arg)) = look arg;
   in look tab end;
 
 fun defined tab key =
@@ -362,7 +379,8 @@
               (case key_ord k2 of
                 LESS => def mid
               | EQUAL => true
-              | GREATER => def right));
+              | GREATER => def right))
+      | def (Size (_, arg)) = def arg;
   in def tab end;
 
 
@@ -378,7 +396,11 @@
   let
     fun key_ord k = Key.ord (key, k);
 
-    fun modfy Empty = Sprout (Empty, (key, f NONE), Empty)
+    val inc = Unsynchronized.ref 0;
+    fun insert () = f NONE before ignore (Unsynchronized.inc inc);
+    fun update x = f (SOME x);
+
+    fun modfy Empty = Sprout (Empty, (key, insert ()), Empty)
       | modfy (t as Leaf1 _) = modfy (unmake t)
       | modfy (t as Leaf2 _) = modfy (unmake t)
       | modfy (t as Leaf3 _) = modfy (unmake t)
@@ -388,7 +410,7 @@
               (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, f (SOME x)), right))
+          | EQUAL => Stay (make2 (left, (k, update x), right))
           | GREATER =>
               (case modfy right of
                 Stay right' => Stay (make2 (left, p, right'))
@@ -401,7 +423,7 @@
                 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, f (SOME x1)), mid, p2, right))
+          | EQUAL => Stay (make3 (left, (k1, update x1), mid, p2, right))
           | GREATER =>
               (case key_ord k2 of
                 LESS =>
@@ -409,19 +431,21 @@
                     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, f (SOME x2)), right))
+              | EQUAL => Stay (make3 (left, p1, mid, (k2, update x2), right))
               | GREATER =>
                   (case modfy right of
                     Stay right' => Stay (make3 (left, p1, mid, p2, right'))
                   | Sprout (right1, q, right2) =>
-                      Sprout (make2 (left, p1, mid), p2, make2 (right1, q, right2)))));
+                      Sprout (make2 (left, p1, mid), p2, make2 (right1, q, right2)))))
+      | modfy (Size (_, arg)) = modfy arg;
 
+    val tab' =
+      (case modfy tab of
+        Stay tab' => tab'
+      | Sprout br => make2 br);
   in
-    (case modfy tab of
-      Stay tab' => tab'
-    | Sprout br => make2 br)
-    handle SAME => tab
-  end;
+    make_size (size tab + !inc) tab'
+  end handle SAME => tab;
 
 fun update (key, x) tab = modify key (fn _ => x) tab;
 fun update_new (key, x) tab = modify key (fn NONE => x | SOME _ => raise DUP key) tab;
@@ -516,11 +540,11 @@
                   make2 (mr, if_equal ord q' q, r'))
             | (Branch3 (ll, lp, lm, lq, lr), Branch2 (ml, mp, mr)) =>
                 make3 (make2 (ll, lp, lm), lq, make2 (lr, p, ml), mp,
-                  make2 (mr, if_equal ord q' q, r'))))));
-
+                  make2 (mr, if_equal ord q' q, r'))))))
+  | del k (Size (_, arg)) = del k arg;
 in
 
-fun delete key tab = snd (snd (del (SOME key) tab));
+fun delete key tab = make_size (size tab - 1) (snd (snd (del (SOME key) tab)));
 fun delete_safe key tab = if defined tab key then delete key tab else tab;
 
 end;