From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Wed, 14 Oct 2009 21:01:12 +0000 (+0000)
Subject: Benchmarking integrated in folding/unfolding.
X-Git-Tag: make_still_working~3295
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=f81e6df71f8804c2f491034b951dcd34e0bd24c3;p=helm.git

Benchmarking integrated in folding/unfolding.
---

diff --git a/helm/software/components/ng_refiner/nCicRefiner.ml b/helm/software/components/ng_refiner/nCicRefiner.ml
index ac280e81f..632313242 100644
--- 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: *)