--- a/NEWS Mon Dec 21 17:08:52 2015 +0100
+++ b/NEWS Mon Dec 21 17:12:17 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 ***
--- a/src/Pure/General/output.ML Mon Dec 21 17:08:52 2015 +0100
+++ b/src/Pure/General/output.ML Mon Dec 21 17:12:17 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;
--- a/src/Pure/General/pretty.ML Mon Dec 21 17:08:52 2015 +0100
+++ b/src/Pure/General/pretty.ML Mon Dec 21 17:12:17 2015 +0100
@@ -118,11 +118,22 @@
| length (Break (_, wd, _)) = wd
| length (Str (_, len)) = len;
-fun body_length [] len = len
- | body_length (e :: es) len = body_length es (length e + len);
+fun make_block markup consistent indent body =
+ let
+ fun body_length prts len =
+ let
+ val (line, rest) = take_prefix (fn Break (true, _, _) => false | _ => true) prts;
+ val len' = Int.max (fold (Integer.add o length) line 0, len);
+ in
+ (case rest of
+ Break (true, _, ind) :: rest' =>
+ body_length (Break (false, indent + ind, 0) :: rest') len'
+ | [] => len')
+ end;
+ in Block (markup, consistent, indent, body, body_length body 0) end;
-fun make_block m consistent indent es = Block (m, consistent, indent, es, body_length es 0);
-fun markup_block m indent es = make_block (Markup.output m) false indent es;
+fun markup_block markup indent es =
+ make_block (Markup.output markup) false indent es;
--- a/src/Pure/General/pretty.scala Mon Dec 21 17:08:52 2015 +0100
+++ b/src/Pure/General/pretty.scala Mon Dec 21 17:12:17 2015 +0100
@@ -63,7 +63,20 @@
consistent: Boolean,
indent: Int,
body: List[Tree]): Tree =
- Block(markup, consistent, indent, body, (0.0 /: body) { case (n, t) => n + t.length })
+ {
+ def body_length(prts: List[Tree], len: Double): Double =
+ {
+ val (line, rest) =
+ Library.take_prefix[Tree]({ case Break(true, _, _) => false case _ => true }, prts)
+ val len1 = ((0.0 /: line) { case (l, t) => l + t.length }) max len
+ rest match {
+ case Break(true, _, ind) :: rest1 =>
+ body_length(Break(false, indent + ind, 0) :: rest1, len1)
+ case Nil => len1
+ }
+ }
+ Block(markup, consistent, indent, body, body_length(body, 0.0))
+ }
/* formatted output */
--- a/src/Pure/Isar/toplevel.ML Mon Dec 21 17:08:52 2015 +0100
+++ b/src/Pure/Isar/toplevel.ML Mon Dec 21 17:12:17 2015 +0100
@@ -26,7 +26,6 @@
val pretty_state: state -> Pretty.T list
val string_of_state: state -> string
val pretty_abstract: state -> Pretty.T
- val profiling: int Unsynchronized.ref
type transition
val empty: transition
val name_of: transition -> string
@@ -204,9 +203,6 @@
(** toplevel transitions **)
-val profiling = Unsynchronized.ref 0;
-
-
(* node transactions -- maintaining stable checkpoints *)
exception FAILURE of state * exn;
@@ -568,10 +564,7 @@
setmp_thread_position tr (fn state =>
let
val timing_start = Timing.start ();
-
- val (result, opt_err) =
- state |> (apply_trans int trans |> ! profiling > 0 ? profile (! profiling));
-
+ val (result, opt_err) = apply_trans int trans state;
val timing_result = Timing.result timing_start;
val timing_props =
Markup.command_timing :: (Markup.nameN, name_of tr) :: Position.properties_of (pos_of tr);
--- a/src/Pure/ML-Systems/ml_debugger.ML Mon Dec 21 17:08:52 2015 +0100
+++ b/src/Pure/ML-Systems/ml_debugger.ML Mon Dec 21 17:12:17 2015 +0100
@@ -21,6 +21,7 @@
val debug_function_result: state -> ML_Name_Space.valueVal
val debug_location: state -> 'location
val debug_name_space: state -> ML_Name_Space.T
+ val debug_local_name_space: state -> ML_Name_Space.T
end;
structure ML_Debugger: ML_DEBUGGER =
@@ -58,5 +59,6 @@
fun debug_function_result () = fail ();
fun debug_location () = fail ();
fun debug_name_space () = fail ();
+fun debug_local_name_space () = fail ();
end;
--- a/src/Pure/ML-Systems/ml_debugger_polyml-5.6.ML Mon Dec 21 17:08:52 2015 +0100
+++ b/src/Pure/ML-Systems/ml_debugger_polyml-5.6.ML Mon Dec 21 17:12:17 2015 +0100
@@ -22,6 +22,7 @@
val debug_function_result: state -> ML_Name_Space.valueVal
val debug_location: state -> location
val debug_name_space: state -> ML_Name_Space.T
+ val debug_local_name_space: state -> ML_Name_Space.T
end;
structure ML_Debugger: ML_DEBUGGER =
@@ -66,5 +67,6 @@
val debug_function_result = PolyML.DebuggerInterface.debugFunctionResult;
val debug_location = PolyML.DebuggerInterface.debugLocation;
val debug_name_space = PolyML.DebuggerInterface.debugNameSpace;
+val debug_local_name_space = PolyML.DebuggerInterface.debugLocalNameSpace;
end;
--- a/src/Pure/ML-Systems/ml_profiling_polyml-5.6.ML Mon Dec 21 17:08:52 2015 +0100
+++ b/src/Pure/ML-Systems/ml_profiling_polyml-5.6.ML Mon Dec 21 17:12:17 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;
--- a/src/Pure/ML-Systems/ml_profiling_polyml.ML Mon Dec 21 17:08:52 2015 +0100
+++ b/src/Pure/ML-Systems/ml_profiling_polyml.ML Mon Dec 21 17:12:17 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;
--- a/src/Pure/ML-Systems/smlnj.ML Mon Dec 21 17:08:52 2015 +0100
+++ b/src/Pure/ML-Systems/smlnj.ML Mon Dec 21 17:12:17 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 ();
--- a/src/Pure/Tools/debugger.ML Mon Dec 21 17:08:52 2015 +0100
+++ b/src/Pure/Tools/debugger.ML Mon Dec 21 17:12:17 2015 +0100
@@ -191,7 +191,7 @@
fun print x =
Pretty.from_ML (ML_Name_Space.display_val (x, ML_Options.get_print_depth (), space));
fun print_all () =
- #allVal (ML_Debugger.debug_name_space (the_debug_state thread_name index)) ()
+ #allVal (ML_Debugger.debug_local_name_space (the_debug_state thread_name index)) ()
|> sort_by #1 |> map (Pretty.item o single o print o #2)
|> Pretty.chunks |> Pretty.string_of |> writeln_message;
in Context.setmp_thread_data (SOME context) print_all () end;
--- a/src/Pure/library.scala Mon Dec 21 17:08:52 2015 +0100
+++ b/src/Pure/library.scala Mon Dec 21 17:12:17 2015 +0100
@@ -205,7 +205,10 @@
try { Some(new Regex(s)) } catch { case ERROR(_) => None }
- /* canonical list operations */
+ /* lists */
+
+ def take_prefix[A](pred: A => Boolean, xs: List[A]): (List[A], List[A]) =
+ (xs.takeWhile(pred), xs.dropWhile(pred))
def member[A, B](xs: List[A])(x: B): Boolean = xs.contains(x)
def insert[A](x: A)(xs: List[A]): List[A] = if (xs.contains(x)) xs else x :: xs