Benchmarking integrated in folding/unfolding.

diff --git a/helm/software/components/ng_refiner/nCicRefiner.ml b/helm/software/components/ng_refiner/nCicRefiner.ml
index ac280e81fdae91f4c2c367f6e4f123789688660d..63231324237aaffb44a8386a61e4bfab239a8ed6 100644 (file)
--- a/helm/software/components/ng_refiner/nCicRefiner.ml
+++ b/helm/software/components/ng_refiner/nCicRefiner.ml
@@ -20,6 +20,7 @@ module Ref = NReference
 
 let debug = ref false;;
 let indent = ref "";;
+let times = ref [];;
 let pp s =
  if !debug then
   prerr_endline (Printf.sprintf "%-20s" !indent ^ " " ^ Lazy.force s)
@@ -27,16 +28,27 @@ let pp s =
   ()
 ;;
 let inside c =
- indent := !indent ^ String.make 1 c;
- if !debug then prerr_endline ("{{{" ^ !indent ^ " ")
+ if !debug then
+  begin
+   let time1 = Unix.gettimeofday () in
+   indent := !indent ^ String.make 1 c;
+   times := time1 :: !times;
+   prerr_endline ("{{{" ^ !indent ^ " ")
+  end
 ;;
 let outside ok =
- if !debug then prerr_endline "}}}";
- if not ok then pp (lazy "exception raised!");
- try
-  indent := String.sub !indent 0 (String.length !indent -1)
- with
-  Invalid_argument _ -> indent := "??"; ()
+ if !debug then
+  begin
+   let time2 = Unix.gettimeofday () in
+   let time1 =
+    match !times with time1::tl -> times := tl; time1 | [] -> assert false in
+   prerr_endline ("}}} " ^ string_of_float (time2 -. time1));
+   if not ok then prerr_endline "exception raised!";
+   try
+    indent := String.sub !indent 0 (String.length !indent -1)
+   with
+    Invalid_argument _ -> indent := "??"; ()
+ end
 ;;
 
 
@@ -848,4 +860,12 @@ let typeof_obj
       uri, height, metasenv, subst, C.Inductive (ind, leftno, itl, attr)
 ;;
 
+let typeof st ?localise m s c t1 t2 =
+let time1 = Unix.gettimeofday () in
+let res = typeof st ?localise m s c t1 t2 in
+let time2 = Unix.gettimeofday () in
+prerr_endline ("OVERALL TYPEOF TIME: " ^ string_of_float (time2 -. time1));
+res
+;;
+
 (* vim:set foldmethod=marker: *)