# HG changeset patch
# User wenzelm
# Date 1450706975 -3600
# Node ID acdfc76a6c33f4b6e99b37d508dfb224aa5ed64e
# Parent  d4c89ea5e6dc9bd8cffbe063f4b334566e85bef9
more explicit ML profiling, with official Isabelle output;

diff -r d4c89ea5e6dc -r acdfc76a6c33 NEWS
--- a/NEWS	Mon Dec 21 14:18:57 2015 +0100
+++ b/NEWS	Mon Dec 21 15:09:35 2015 +0100
@@ -669,6 +669,13 @@
 tools, but can also cause INCOMPATIBILITY for tools that don't observe
 the proof context discipline.
 
+* The following combinators for low-level profiling of the ML runtime
+system are available:
+
+  profile_time          (*CPU time*)
+  profile_time_thread   (*CPU time on this thread*)
+  profile_allocations   (*overall heap allocations*)
+
 
 *** System ***
 
diff -r d4c89ea5e6dc -r acdfc76a6c33 src/Pure/General/output.ML
--- a/src/Pure/General/output.ML	Mon Dec 21 14:18:57 2015 +0100
+++ b/src/Pure/General/output.ML	Mon Dec 21 15:09:35 2015 +0100
@@ -10,6 +10,9 @@
   val tracing: string -> unit
   val warning: string -> unit
   val legacy_feature: string -> unit
+  val profile_time: ('a -> 'b) -> 'a -> 'b
+  val profile_time_thread: ('a -> 'b) -> 'a -> 'b
+  val profile_allocations: ('a -> 'b) -> 'a -> 'b
 end;
 
 signature OUTPUT =
@@ -131,6 +134,40 @@
 fun protocol_message props ss = ! protocol_message_fn props (map output ss);
 fun try_protocol_message props ss = protocol_message props ss handle Protocol_Message _ => ();
 
+
+(* profiling *)
+
+local
+
+fun output_profile title entries =
+  let
+    val body = entries
+      |> sort (int_ord o apply2 fst)
+      |> map (fn (count, name) =>
+          let
+            val c = string_of_int count;
+            val prefix = replicate_string (Int.max (0, 10 - size c)) " ";
+          in prefix ^ c ^ " " ^ name end);
+    val total = fold (curry (op +) o fst) entries 0;
+  in
+    if total = 0 then ()
+    else warning (cat_lines (title :: (body @ ["total: " ^ string_of_int total])))
+  end;
+
+in
+
+fun profile_time f x =
+  ML_Profiling.profile_time (output_profile "time profile:") f x;
+
+fun profile_time_thread f x =
+  ML_Profiling.profile_time_thread (output_profile "time profile (this thread):") f x;
+
+fun profile_allocations f x =
+  ML_Profiling.profile_allocations (output_profile "allocations profile:") f x;
+
+end;
+
+
 end;
 
 structure Basic_Output: BASIC_OUTPUT = Output;
diff -r d4c89ea5e6dc -r acdfc76a6c33 src/Pure/ML-Systems/ml_profiling_polyml-5.6.ML
--- a/src/Pure/ML-Systems/ml_profiling_polyml-5.6.ML	Mon Dec 21 14:18:57 2015 +0100
+++ b/src/Pure/ML-Systems/ml_profiling_polyml-5.6.ML	Mon Dec 21 15:09:35 2015 +0100
@@ -4,14 +4,16 @@
 Profiling for Poly/ML 5.6.
 *)
 
-fun profile 0 f x = f x
-  | profile n f x =
-      let
-        val mode =
-          (case n of
-            1 => PolyML.Profiling.ProfileTime
-          | 2 => PolyML.Profiling.ProfileAllocations
-          | 3 => PolyML.Profiling.ProfileLongIntEmulation
-          | 6 => PolyML.Profiling.ProfileTimeThisThread
-          | _ => raise Fail ("Bad profile mode: " ^ Int.toString n));
-      in PolyML.Profiling.profile mode f x end;
+structure ML_Profiling =
+struct
+
+fun profile_time pr f x =
+  PolyML.Profiling.profileStream pr PolyML.Profiling.ProfileTime f x;
+
+fun profile_time_thread pr f x =
+  PolyML.Profiling.profileStream pr PolyML.Profiling.ProfileTimeThisThread f x;
+
+fun profile_allocations pr f x =
+  PolyML.Profiling.profileStream pr PolyML.Profiling.ProfileAllocations f x;
+
+end;
diff -r d4c89ea5e6dc -r acdfc76a6c33 src/Pure/ML-Systems/ml_profiling_polyml.ML
--- a/src/Pure/ML-Systems/ml_profiling_polyml.ML	Mon Dec 21 14:18:57 2015 +0100
+++ b/src/Pure/ML-Systems/ml_profiling_polyml.ML	Mon Dec 21 15:09:35 2015 +0100
@@ -4,10 +4,24 @@
 Profiling for Poly/ML.
 *)
 
-fun profile 0 f x = f x
-  | profile n f x =
-      let
-        val _ = RunCall.run_call1 RuntimeCalls.POLY_SYS_profiler n;
-        val res = Exn.capture f x;
-        val _ = RunCall.run_call1 RuntimeCalls.POLY_SYS_profiler 0;
-      in Exn.release res end;
+structure ML_Profiling =
+struct
+
+local
+
+fun profile n f x =
+  let
+    val _ = RunCall.run_call1 RuntimeCalls.POLY_SYS_profiler n;
+    val res = Exn.capture f x;
+    val _ = RunCall.run_call1 RuntimeCalls.POLY_SYS_profiler 0;
+  in Exn.release res end;
+
+in
+
+fun profile_time (_: (int * string) list -> unit) f x = profile 1 f x;
+fun profile_time_thread (_: (int * string) list -> unit) f x = profile 6 f x;
+fun profile_allocations (_: (int * string) list -> unit) f x = profile 2 f x;
+
+end;
+
+end;
diff -r d4c89ea5e6dc -r acdfc76a6c33 src/Pure/ML-Systems/smlnj.ML
--- a/src/Pure/ML-Systems/smlnj.ML	Mon Dec 21 14:18:57 2015 +0100
+++ b/src/Pure/ML-Systems/smlnj.ML	Mon Dec 21 15:09:35 2015 +0100
@@ -74,7 +74,12 @@
   (Control.primaryPrompt := p1; Control.secondaryPrompt := p2);
 
 (*dummy implementation*)
-fun profile (n: int) f x = f x;
+structure ML_Profiling =
+struct
+  fun profile_time (_: (int * string) list -> unit) f x = f x;
+  fun profile_time_thread (_: (int * string) list -> unit) f x = f x;
+  fun profile_allocations (_: (int * string) list -> unit) f x = f x;
+end;
 
 (*dummy implementation*)
 fun print_exception_trace (_: exn -> string) (_: string -> unit) f = f ();