28 |
28 |
29 |
29 |
30 (* timing *) |
30 (* timing *) |
31 |
31 |
32 local |
32 local |
33 (*print microseconds, suppressing trailing zeroes*) |
33 |
34 fun umakestring 0 = "" |
34 (*print microseconds, suppressing trailing zeroes*) |
35 | umakestring n = |
35 fun umakestring 0 = "" |
36 chr (ord "0" + n div 100000) ^ umakestring (10 * (n mod 100000)); |
36 | umakestring n = |
|
37 chr (ord "0" + n div 100000) ^ umakestring (10 * (n mod 100000)); |
|
38 |
37 in |
39 in |
38 (*a conditional timing function: applies f to () and, if the flag is true, |
40 |
39 prints its runtime*) |
41 (*a conditional timing function: applies f to () and, if the flag is true, |
40 fun cond_timeit flag f = |
42 prints its runtime*) |
41 if flag then |
43 |
42 let fun string_of_time (System.Timer.TIME {sec, usec}) = |
44 fun cond_timeit flag f = |
43 makestring sec ^ "." ^ (if usec=0 then "0" else umakestring usec) |
45 if flag then |
44 open System.Timer; |
46 let fun string_of_time (System.Timer.TIME {sec, usec}) = |
45 val start = start_timer() |
47 makestring sec ^ "." ^ (if usec=0 then "0" else umakestring usec) |
46 val result = f(); |
48 open System.Timer; |
47 val nongc = check_timer(start) |
49 val start = start_timer() |
48 and gc = check_timer_gc(start); |
50 val result = f(); |
49 val both = add_time(nongc, gc) |
51 val nongc = check_timer(start) |
50 in print("Non GC " ^ string_of_time nongc ^ |
52 and gc = check_timer_gc(start); |
51 " GC " ^ string_of_time gc ^ |
53 val both = add_time(nongc, gc) |
52 " both "^ string_of_time both ^ " secs\n"); |
54 in print("Non GC " ^ string_of_time nongc ^ |
53 result |
55 " GC " ^ string_of_time gc ^ |
54 end |
56 " both "^ string_of_time both ^ " secs\n"); |
55 else f(); |
57 result |
|
58 end |
|
59 else f(); |
|
60 |
56 end; |
61 end; |
57 |
62 |
58 |
63 |
59 (* toplevel pretty printing (see also Pure/install_pp.ML) *) |
64 (* toplevel pretty printing (see also Pure/install_pp.ML) *) |
60 |
65 |