From 57c897b886b3cc52c62589b4a6e0b32566c6758a Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Thu, 15 Oct 2009 13:59:31 +0000
Subject: [PATCH] Profiling code integrated.

---
 .../components/ng_refiner/nCicUnification.ml  | 32 ++++++++++++-------
 1 file changed, 21 insertions(+), 11 deletions(-)

diff --git a/helm/software/components/ng_refiner/nCicUnification.ml b/helm/software/components/ng_refiner/nCicUnification.ml
index 5a3878a2b..7bec66a77 100644
--- a/helm/software/components/ng_refiner/nCicUnification.ml
+++ b/helm/software/components/ng_refiner/nCicUnification.ml
@@ -77,23 +77,33 @@ 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)
- else 
-  ()
 ;;
 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
 ;;
 
 let ppcontext ~metasenv ~subst c = 
@@ -720,7 +730,7 @@ and unify rdb test_eq_only metasenv subst context t1 t2 =
            " === " ^ 
            NCicPp.ppterm ~metasenv ~subst ~context 
              (NCicReduction.unwind (k2,e2,t2,s2))));
-pp (lazy (string_of_bool norm1 ^ " ?? " ^ string_of_bool norm2));
+         pp (lazy (string_of_bool norm1 ^ " ?? " ^ string_of_bool norm2));
           let relevance = [] (* TO BE UNDERSTOOD 
             match t1 with
             | C.Const r -> NCicEnvironment.get_relevance r
-- 
2.39.2