--- a/src/Pure/ML/ml_profiling.ML Mon Jun 07 15:13:34 2021 +0200
+++ b/src/Pure/ML/ml_profiling.ML Mon Jun 07 16:40:26 2021 +0200
@@ -6,21 +6,39 @@
signature ML_PROFILING =
sig
- val profile_time: ((int * string) list -> unit) -> ('a -> 'b) -> 'a -> 'b
- val profile_time_thread: ((int * string) list -> unit) -> ('a -> 'b) -> 'a -> 'b
- val profile_allocations: ((int * string) list -> unit) -> ('a -> 'b) -> 'a -> 'b
+ val profile_time: ('a -> 'b) -> 'a -> 'b
+ val profile_time_thread: ('a -> 'b) -> 'a -> 'b
+ val profile_allocations: ('a -> 'b) -> 'a -> 'b
end;
structure ML_Profiling: ML_PROFILING =
struct
-fun profile_time pr f x =
- PolyML.Profiling.profileStream pr PolyML.Profiling.ProfileTime f x;
+fun profile mode title =
+ mode |> PolyML.Profiling.profileStream (fn 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);
-fun profile_time_thread pr f x =
- PolyML.Profiling.profileStream pr PolyML.Profiling.ProfileTimeThisThread f x;
+fun profile_time f =
+ profile PolyML.Profiling.ProfileTime "time profile:" f;
-fun profile_allocations pr f x =
- PolyML.Profiling.profileStream pr PolyML.Profiling.ProfileAllocations f x;
+fun profile_time_thread f =
+ profile PolyML.Profiling.ProfileTimeThisThread "time profile (this thread):" f;
+
+fun profile_allocations f =
+ profile PolyML.Profiling.ProfileAllocations "allocations profile:" f;
end;
+
+open ML_Profiling;