| author | wenzelm |
| Mon, 15 Feb 2016 14:55:44 +0100 | |
| changeset 62337 | d3996d5873dd |
| parent 61925 | ab52f183f020 |
| permissions | -rw-r--r-- |
| 61925 | 1 |
(* Title: Pure/RAW/ml_profiling_polyml.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 |
|
|
5dc95d957569
speculative support for polyml-5.6, according to git commit 3527f4ba7b8b;
wenzelm
parents:
diff
changeset
|
4 |
Profiling for Poly/ML. |
|
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 |
|
|
61885
acdfc76a6c33
more explicit ML profiling, with official Isabelle output;
wenzelm
parents:
61715
diff
changeset
|
7 |
structure ML_Profiling = |
|
acdfc76a6c33
more explicit ML profiling, with official Isabelle output;
wenzelm
parents:
61715
diff
changeset
|
8 |
struct |
|
acdfc76a6c33
more explicit ML profiling, with official Isabelle output;
wenzelm
parents:
61715
diff
changeset
|
9 |
|
|
acdfc76a6c33
more explicit ML profiling, with official Isabelle output;
wenzelm
parents:
61715
diff
changeset
|
10 |
local |
|
acdfc76a6c33
more explicit ML profiling, with official Isabelle output;
wenzelm
parents:
61715
diff
changeset
|
11 |
|
|
acdfc76a6c33
more explicit ML profiling, with official Isabelle output;
wenzelm
parents:
61715
diff
changeset
|
12 |
fun profile n f x = |
|
acdfc76a6c33
more explicit ML profiling, with official Isabelle output;
wenzelm
parents:
61715
diff
changeset
|
13 |
let |
|
acdfc76a6c33
more explicit ML profiling, with official Isabelle output;
wenzelm
parents:
61715
diff
changeset
|
14 |
val _ = RunCall.run_call1 RuntimeCalls.POLY_SYS_profiler n; |
|
acdfc76a6c33
more explicit ML profiling, with official Isabelle output;
wenzelm
parents:
61715
diff
changeset
|
15 |
val res = Exn.capture f x; |
|
acdfc76a6c33
more explicit ML profiling, with official Isabelle output;
wenzelm
parents:
61715
diff
changeset
|
16 |
val _ = RunCall.run_call1 RuntimeCalls.POLY_SYS_profiler 0; |
|
acdfc76a6c33
more explicit ML profiling, with official Isabelle output;
wenzelm
parents:
61715
diff
changeset
|
17 |
in Exn.release res end; |
|
acdfc76a6c33
more explicit ML profiling, with official Isabelle output;
wenzelm
parents:
61715
diff
changeset
|
18 |
|
|
acdfc76a6c33
more explicit ML profiling, with official Isabelle output;
wenzelm
parents:
61715
diff
changeset
|
19 |
in |
|
acdfc76a6c33
more explicit ML profiling, with official Isabelle output;
wenzelm
parents:
61715
diff
changeset
|
20 |
|
|
acdfc76a6c33
more explicit ML profiling, with official Isabelle output;
wenzelm
parents:
61715
diff
changeset
|
21 |
fun profile_time (_: (int * string) list -> unit) f x = profile 1 f x; |
|
acdfc76a6c33
more explicit ML profiling, with official Isabelle output;
wenzelm
parents:
61715
diff
changeset
|
22 |
fun profile_time_thread (_: (int * string) list -> unit) f x = profile 6 f x; |
|
acdfc76a6c33
more explicit ML profiling, with official Isabelle output;
wenzelm
parents:
61715
diff
changeset
|
23 |
fun profile_allocations (_: (int * string) list -> unit) f x = profile 2 f x; |
|
acdfc76a6c33
more explicit ML profiling, with official Isabelle output;
wenzelm
parents:
61715
diff
changeset
|
24 |
|
|
acdfc76a6c33
more explicit ML profiling, with official Isabelle output;
wenzelm
parents:
61715
diff
changeset
|
25 |
end; |
|
acdfc76a6c33
more explicit ML profiling, with official Isabelle output;
wenzelm
parents:
61715
diff
changeset
|
26 |
|
|
acdfc76a6c33
more explicit ML profiling, with official Isabelle output;
wenzelm
parents:
61715
diff
changeset
|
27 |
end; |