57 |
57 |
58 |
58 |
59 (* compiler-independent timing functions *) |
59 (* compiler-independent timing functions *) |
60 |
60 |
61 fun start_timing () = |
61 fun start_timing () = |
62 let val CPUtimer = Timer.startCPUTimer(); |
62 let |
63 val time = Timer.checkCPUTimer(CPUtimer) |
63 val timer = Timer.startCPUTimer (); |
64 in (CPUtimer,time) end; |
64 val time = Timer.checkCPUTimer timer; |
65 |
65 in (timer, time) end; |
66 fun end_timing (CPUtimer, {sys,usr}) = |
66 |
67 let open Time (*...for Time.toString, Time.+ and Time.- *) |
67 fun end_timing (timer, {sys, usr}) = |
68 val {sys=sys2,usr=usr2} = Timer.checkCPUTimer(CPUtimer) |
68 let |
69 in "User " ^ toString (usr2-usr) ^ |
69 open Time; (*...for Time.toString, Time.+ and Time.- *) |
70 " All "^ toString (sys2-sys + usr2-usr) ^ |
70 val {sys = sys2, usr = usr2} = Timer.checkCPUTimer timer; |
71 " secs" |
71 val user = usr2 - usr; |
72 handle Time => "" |
72 val all = user + sys2 - sys; |
73 end; |
73 val message = "User " ^ toString user ^ " All "^ toString all ^ " secs" handle Time => ""; |
|
74 in {message = message, user = user, all = all} end; |
74 |
75 |
75 fun check_timer timer = |
76 fun check_timer timer = |
76 let |
77 let |
77 val {sys, usr} = Timer.checkCPUTimer timer; |
78 val {sys, usr} = Timer.checkCPUTimer timer; |
78 val gc = Timer.checkGCTime timer; (* FIXME already included in usr? *) |
79 val gc = Timer.checkGCTime timer; (* FIXME already included in usr? *) |