Add named timers to LtacProf

I'm not sure if they belong in profile_ltac, or in extratactics, or,
perhaps, in a separate plugin.  But I'd find it very useful to have a
version of `time` that works on constr evaluation, which is what this
commit provides.

I'm not sure that I've picked good naming conventions for the tactics,
either.

1 files changed, 21 insertions, 0 deletions

diff --git a/plugins/ltac/profile_ltac.ml b/plugins/ltac/profile_ltac.ml
index 5225420dc..97f43eaa8 100644
--- a/plugins/ltac/profile_ltac.ml
+++ b/plugins/ltac/profile_ltac.ml
@@ -397,6 +397,27 @@ let reset_profile () =
   reset_profile_tmp ();
   data := SM.empty
 
+(* ****************************** Named timers ****************************** *)
+
+let timer_data = ref M.empty
+
+let timer_name = function
+  | Some v -> v
+  | None -> ""
+
+let restart_timer name =
+  timer_data := M.add (timer_name name) (System.get_time ()) !timer_data
+
+let get_timer name =
+  try M.find (timer_name name) !timer_data
+  with Not_found -> System.get_time ()
+
+let finish_timing ~prefix name =
+  let tend = System.get_time () in
+  let tstart = get_timer name in
+  Feedback.msg_info(str prefix ++ pr_opt str name ++ str " ran for " ++
+                    System.fmt_time_difference tstart tend)
+
 (* ******************** *)
 
 let print_results_filter ~cutoff ~filter =