performance tuning: make_size accounts for boxes, i.e. pointer derefs required in "count";

--- a/src/Pure/General/set.ML	Mon Apr 10 14:13:48 2023 +0200
+++ b/src/Pure/General/set.ML	Mon Apr 10 14:59:40 2023 +0200
@@ -84,9 +84,6 @@
 (* 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
@@ -95,8 +92,23 @@
     | 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 (Size (m, _)) n = m + n;
+
+  fun box (Branch2 _) = 1
+    | box (Branch3 _) = 1
+    | box _ = 0;
+
+  fun bound arg b =
+    if b > 0 then
+      (case arg of
+        Branch2 (left, _, right) =>
+          bound right (bound left (b - box left - box right))
+      | Branch3 (left, _, mid, _, right) =>
+          bound right (bound mid (bound left (b - box left - box mid - box right)))
+      | _ => b)
+    else b;
 in
-  val size = Integer.build o count;
+  fun size arg = count arg 0;
+  fun make_size m arg = if bound arg 3 <= 0 then Size (m, arg) else arg;
 end;
 
 
@@ -426,7 +438,6 @@
     ML_Pretty.to_polyml
       (ML_Pretty.enum "," "{" "}" (ML_Pretty.from_polyml o ML_system_pretty) (dest set, depth)));
 
-
 (*final declarations of this structure!*)
 val fold = fold_set;
 val fold_rev = fold_rev_set;

--- a/src/Pure/General/table.ML	Mon Apr 10 14:13:48 2023 +0200
+++ b/src/Pure/General/table.ML	Mon Apr 10 14:59:40 2023 +0200
@@ -121,10 +121,7 @@
 (* 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
     | count (Leaf1 _) n = n + 1
     | count (Leaf2 _) n = n + 2
@@ -132,8 +129,23 @@
     | 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 (Size (m, _)) n = m + n;
+
+  fun box (Branch2 _) = 1
+    | box (Branch3 _) = 1
+    | box _ = 0;
+
+  fun bound arg b =
+    if b > 0 then
+      (case arg of
+        Branch2 (left, _, right) =>
+          bound right (bound left (b - box left - box right))
+      | Branch3 (left, _, mid, _, right) =>
+          bound right (bound mid (bound left (b - box left - box mid - box right)))
+      | _ => b)
+    else b;
 in
-  fun size tab = Integer.build (count tab);
+  fun size arg = count arg 0;
+  fun make_size m arg = if bound arg 3 <= 0 then Size (m, arg) else arg;
 end;