clarified operations for ML object sizes;

--- a/NEWS	Sun Mar 19 18:55:48 2023 +0000
+++ b/NEWS	Mon Mar 20 10:59:27 2023 +0100
@@ -267,6 +267,19 @@
 
 *** ML ***
 
+* Operations ML_Heap.sizeof1 and ML_Heap.sizeof determine the object
+size on the heap in bytes. The latter works simultaneously on multiple
+objects, taking implicit sharing of values into account. Examples for
+the default 64_32 platform (4 bytes per machine word):
+
+  val s = "aaaabbbbcccc";
+  val a = ML_Heap.sizeof1 s;
+    (*20: 2 words descriptor + 3 words content*)
+  val b = ML_Heap.sizeof [s, s];
+    (*20: shared values without list structure*)
+  val c = ML_Heap.sizeof1 [s, s];
+    (*44 = 20 + 24: shared values + 2 * 3 words per list cons*)
+
 * Operations for Zstd compression (via Isabelle/Scala):
 
   Zstd.compress: Bytes.T -> Bytes.T

--- a/src/Pure/ML/ml_heap.ML	Sun Mar 19 18:55:48 2023 +0000
+++ b/src/Pure/ML/ml_heap.ML	Mon Mar 20 10:59:27 2023 +0100
@@ -7,6 +7,8 @@
 signature ML_HEAP =
 sig
   val obj_size: 'a -> int
+  val sizeof1: 'a -> int
+  val sizeof: 'a list -> int
   val full_gc: unit -> unit
   val gc_now: unit -> Time.time
   val share_common_data: unit -> unit
@@ -18,6 +20,9 @@
 
 val obj_size = PolyML.objSize;
 
+fun sizeof1 x = obj_size x * ML_System.platform_obj_size;
+fun sizeof xs = (obj_size xs - 3 * length xs) * ML_System.platform_obj_size;
+
 val full_gc = PolyML.fullGC;
 
 fun gc_now () = #timeGCReal (PolyML.Statistics.getLocalStats ());

--- a/src/Pure/ML/ml_system.ML	Sun Mar 19 18:55:48 2023 +0000
+++ b/src/Pure/ML/ml_system.ML	Mon Mar 20 10:59:27 2023 +0100
@@ -12,8 +12,9 @@
   val platform_is_macos: bool
   val platform_is_windows: bool
   val platform_is_unix: bool
+  val platform_is_arm: bool
   val platform_is_64: bool
-  val platform_is_arm: bool
+  val platform_obj_size: int
   val platform_path: string -> string
   val standard_path: string -> string
 end;
@@ -28,8 +29,10 @@
 val platform_is_macos = String.isSuffix "darwin" platform;
 val platform_is_windows = String.isSuffix "windows" platform;
 val platform_is_unix = platform_is_linux orelse platform_is_macos;
+val platform_is_arm = String.isPrefix "arm64_32-" platform orelse String.isPrefix "arm64-" platform;
 val platform_is_64 = String.isPrefix "x86_64-" platform orelse String.isPrefix "arm64-" platform;
-val platform_is_arm = String.isPrefix "arm64_32-" platform orelse String.isPrefix "arm64-" platform;
+
+val platform_obj_size = if platform_is_64 then 8 else 4;
 
 val platform_path =
   if platform_is_windows then