57 val implode = String.concat; |
57 val implode = String.concat; |
58 |
58 |
59 |
59 |
60 (*** Timing functions ***) |
60 (*** Timing functions ***) |
61 |
61 |
62 val CPUtimer = Timer.startCPUTimer(); |
|
63 |
|
64 (*A conditional timing function: applies f to () and, if the flag is true, |
62 (*A conditional timing function: applies f to () and, if the flag is true, |
65 prints its runtime. *) |
63 prints its runtime. *) |
66 fun cond_timeit flag f = |
64 fun cond_timeit flag f = |
67 if flag then |
65 if flag then |
68 let open Time (*...for Time.toString, Time.+ and Time.- *) |
66 let open Time (*...for Time.toString, Time.+ and Time.- *) |
69 val {gc=gct1,sys=syst1,usr=usrt1} = Timer.checkCPUTimer(CPUtimer); |
67 val CPUtimer = Timer.startCPUTimer(); |
|
68 val {gc=gct1,sys=syst1,usr=usrt1} = Timer.checkCPUTimer(CPUtimer); |
70 val result = f(); |
69 val result = f(); |
71 val {gc=gct2,sys=syst2,usr=usrt2} = Timer.checkCPUTimer(CPUtimer) |
70 val {gc=gct2,sys=syst2,usr=usrt2} = Timer.checkCPUTimer(CPUtimer) |
72 in print("User " ^ toString (usrt2-usrt1) ^ |
71 in print("User " ^ toString (usrt2-usrt1) ^ |
73 " GC " ^ toString (gct2-gct1) ^ |
72 " GC " ^ toString (gct2-gct1) ^ |
74 " All "^ toString (syst2-syst1 + usrt2-usrt1 + gct2-gct1) ^ |
73 " All "^ toString (syst2-syst1 + usrt2-usrt1 + gct2-gct1) ^ |