equal
deleted
inserted
replaced
63 |
63 |
64 (*A conditional timing function: applies f to () and, if the flag is true, |
64 (*A conditional timing function: applies f to () and, if the flag is true, |
65 prints its runtime. *) |
65 prints its runtime. *) |
66 fun cond_timeit flag f = |
66 fun cond_timeit flag f = |
67 if flag then |
67 if flag then |
68 let open Time; |
68 let open Time (*...for Time.toString, Time.+ and Time.- *) |
69 open Timer; |
69 val {gc=gct1,sys=syst1,usr=usrt1} = Timer.checkCPUTimer(CPUtimer); |
70 val {gc=gct1,sys=syst1,usr=usrt1} = checkCPUTimer(CPUtimer); |
|
71 val result = f(); |
70 val result = f(); |
72 val {gc=gct2,sys=syst2,usr=usrt2} = checkCPUTimer(CPUtimer) |
71 val {gc=gct2,sys=syst2,usr=usrt2} = Timer.checkCPUTimer(CPUtimer) |
73 in print("Non GC " ^ toString (usrt2-usrt1) ^ |
72 in print("User " ^ toString (usrt2-usrt1) ^ |
74 " GC " ^ toString (gct2-gct1) ^ |
73 " GC " ^ toString (gct2-gct1) ^ |
75 " both+sys "^ toString (syst2-syst1 + usrt2-usrt1 + gct2-gct1) ^ |
74 " All "^ toString (syst2-syst1 + usrt2-usrt1 + gct2-gct1) ^ |
76 " secs\n"); |
75 " secs\n") |
|
76 handle Time => (); |
77 result |
77 result |
78 end |
78 end |
79 else f(); |
79 else f(); |
80 |
80 |
81 |
81 |