clarified signature: more uniform Table() vs. Set();
--- a/src/Pure/General/set.ML Sun Apr 02 12:34:13 2023 +0200
+++ b/src/Pure/General/set.ML Mon Apr 03 21:13:46 2023 +0200
@@ -81,6 +81,7 @@
(* size *)
+(*literal copy from table.ML*)
local
fun count Empty n = n
| count (Leaf1 _) n = n + 1
--- a/src/Pure/General/table.ML Sun Apr 02 12:34:13 2023 +0200
+++ b/src/Pure/General/table.ML Mon Apr 03 21:13:46 2023 +0200
@@ -19,6 +19,7 @@
exception DUP of key
exception SAME
exception UNDEF of key
+ val size: 'a table -> int
val empty: 'a table
val build: ('a table -> 'a table) -> 'a table
val is_empty: 'a table -> bool
@@ -115,6 +116,21 @@
| unmake arg = arg;
+(* size *)
+
+local
+ (*literal copy from set.ML*)
+ 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)));
+in
+ fun size tab = Integer.build (count tab);
+end;
+
+
(* empty *)
val empty = Empty;