author | wenzelm |
Tue, 08 Jun 2021 23:34:06 +0200 | |
changeset 73838 | 0e6a5a6cc767 |
parent 73835 | 5dae03d50db1 |
child 73840 | a5200fa7cb4c |
permissions | -rw-r--r-- |
62508
d0b68218ea55
discontinued RAW session: bootstrap directly from isabelle_process RAW_ML_SYSTEM;
wenzelm
parents:
62501
diff
changeset
|
1 |
(* Title: Pure/ML/ml_profiling.ML |
61715
5dc95d957569
speculative support for polyml-5.6, according to git commit 3527f4ba7b8b;
wenzelm
parents:
diff
changeset
|
2 |
Author: Makarius |
5dc95d957569
speculative support for polyml-5.6, according to git commit 3527f4ba7b8b;
wenzelm
parents:
diff
changeset
|
3 |
|
62945 | 4 |
ML profiling. |
61715
5dc95d957569
speculative support for polyml-5.6, according to git commit 3527f4ba7b8b;
wenzelm
parents:
diff
changeset
|
5 |
*) |
5dc95d957569
speculative support for polyml-5.6, according to git commit 3527f4ba7b8b;
wenzelm
parents:
diff
changeset
|
6 |
|
62824 | 7 |
signature ML_PROFILING = |
8 |
sig |
|
73834 | 9 |
val profile_time: ('a -> 'b) -> 'a -> 'b |
10 |
val profile_time_thread: ('a -> 'b) -> 'a -> 'b |
|
11 |
val profile_allocations: ('a -> 'b) -> 'a -> 'b |
|
62824 | 12 |
end; |
13 |
||
14 |
structure ML_Profiling: ML_PROFILING = |
|
61885
acdfc76a6c33
more explicit ML profiling, with official Isabelle output;
wenzelm
parents:
61715
diff
changeset
|
15 |
struct |
acdfc76a6c33
more explicit ML profiling, with official Isabelle output;
wenzelm
parents:
61715
diff
changeset
|
16 |
|
73835 | 17 |
fun print_entry count name = |
18 |
let |
|
19 |
val c = string_of_int count; |
|
20 |
val prefix = Symbol.spaces (Int.max (0, 10 - size c)); |
|
21 |
in prefix ^ c ^ " " ^ name end; |
|
22 |
||
23 |
fun profile mode kind title f x = |
|
24 |
PolyML.Profiling.profileStream (fn entries => |
|
25 |
(case fold (curry (op +) o fst) entries 0 of |
|
26 |
0 => () |
|
27 |
| total => |
|
28 |
let |
|
29 |
val body = entries |
|
30 |
|> sort (int_ord o apply2 fst) |
|
31 |
|> map (fn (count, name) => |
|
32 |
let val markup = Markup.ML_profiling_entry {name = name, count = count} |
|
33 |
in XML.Elem (markup, [XML.Text (print_entry count name ^ "\n")]) end); |
|
34 |
val xml = |
|
35 |
XML.Elem (Markup.ML_profiling kind, |
|
36 |
XML.Text (title ^ "\n") :: body @ [XML.Text (print_entry total "TOTAL")]); |
|
73838 | 37 |
in tracing (YXML.string_of xml) end)) mode f x; |
61885
acdfc76a6c33
more explicit ML profiling, with official Isabelle output;
wenzelm
parents:
61715
diff
changeset
|
38 |
|
73834 | 39 |
fun profile_time f = |
73835 | 40 |
profile PolyML.Profiling.ProfileTime "time" "time profile:" f; |
61885
acdfc76a6c33
more explicit ML profiling, with official Isabelle output;
wenzelm
parents:
61715
diff
changeset
|
41 |
|
73834 | 42 |
fun profile_time_thread f = |
73835 | 43 |
profile PolyML.Profiling.ProfileTimeThisThread "time_thread" "time profile (single thread):" f; |
73834 | 44 |
|
45 |
fun profile_allocations f = |
|
73835 | 46 |
profile PolyML.Profiling.ProfileAllocations "allocations" "allocations profile:" f; |
61885
acdfc76a6c33
more explicit ML profiling, with official Isabelle output;
wenzelm
parents:
61715
diff
changeset
|
47 |
|
acdfc76a6c33
more explicit ML profiling, with official Isabelle output;
wenzelm
parents:
61715
diff
changeset
|
48 |
end; |
73834 | 49 |
|
50 |
open ML_Profiling; |