* More profiling code

* Debugging code restructured

diff --git a/helm/ocaml/cic_proof_checking/cicReduction.ml b/helm/ocaml/cic_proof_checking/cicReduction.ml
index fe0c09aaeff029c860c1d8abb07c4ab9cc0d2a41..29762b86d32d937bc0a2ec6932bce82cb879ebaf 100644 (file)
--- a/helm/ocaml/cic_proof_checking/cicReduction.ml
+++ b/helm/ocaml/cic_proof_checking/cicReduction.ml
@@ -33,7 +33,8 @@ exception ReferenceToVariable;;
 exception ReferenceToCurrentProof;;
 exception ReferenceToInductiveDefinition;;
 
-let debug_print = fun _ -> ()
+let debug = true
+let debug_print s = if debug then prerr_endline (Lazy.force s)
 
 let fdebug = ref 1;;
 let debug t env s =
@@ -509,8 +510,12 @@ if List.mem uri params then debug_print (lazy "---- OK2") ;
       unwind_aux m t          
   ;;
   
-  let unwind =
-   unwind' 0 
+let profiler_unwind = HExtlib.profile "are_convertible.unwind"
+  let unwind k e ens t =
+let foo () =
+   unwind' 0  k e ens t
+in
+ profiler_unwind.HExtlib.profile foo ()
   ;;
   
   let reduce ~delta ?(subst = []) context : config -> Cic.term = 
@@ -770,54 +775,39 @@ if List.mem uri params then debug_print (lazy "---- OK2") ;
   ;;
 
   
-(* DEBUGGING ONLY
-let whd context t =
- let res = whd context t in
- let rescsc = CicReductionNaif.whd context t in
-  if not (CicReductionNaif.are_convertible context res rescsc) then
-   begin
-    debug_print (lazy ("PRIMA: " ^ CicPp.ppterm t)) ;
-    flush stderr ;
-    debug_print (lazy ("DOPO: " ^ CicPp.ppterm res)) ;
-    flush stderr ;
-    debug_print (lazy ("CSC: " ^ CicPp.ppterm rescsc)) ;
-    flush stderr ;
-CicReductionNaif.fdebug := 0 ;
-let _ =  CicReductionNaif.are_convertible context res rescsc in
-    assert false ;
-   end
-  else 
-   res
-;;
-*)
  end
 ;;
 
 
-(*
-module R = Reduction CallByNameStrategy;;
-module R = Reduction CallByValueStrategy;;
-module R = Reduction CallByValueStrategyByNameOnConstants;;
-module R = Reduction LazyCallByValueStrategy;;
-module R = Reduction LazyCallByValueStrategyByNameOnConstants;;
-module R = Reduction LazyCallByNameStrategy;;
+(* ROTTO = rompe l'unificazione poiche' riduce gli argomenti di un'applicazione
+           senza ridurre la testa
+module R = Reduction CallByNameStrategy;; OK 56.368s
+module R = Reduction CallByValueStrategy;; ROTTO
+module R = Reduction CallByValueStrategyByNameOnConstants;; ROTTO
+module R = Reduction LazyCallByValueStrategy;; ROTTO
+module R = Reduction LazyCallByValueStrategyByNameOnConstants;; ROTTO
+module R = Reduction LazyCallByNameStrategy;; OK 0m56.398s
 module R = Reduction
  LazyCallByValueByNameOnConstantsWhenFromStack_ByNameStrategyWhenFromEnvOrEns;;
-module R = Reduction ClosuresOnStackByValueFromEnvOrEnsStrategy;;
+ OK 59.058s
+module R = Reduction ClosuresOnStackByValueFromEnvOrEnsStrategy;; OK 58.583s
 module R = Reduction
- ClosuresOnStackByValueFromEnvOrEnsByNameOnConstantsStrategy;;
+ ClosuresOnStackByValueFromEnvOrEnsByNameOnConstantsStrategy;; OK 58.094s
+module R = Reduction(ClosuresOnStackByValueFromEnvOrEnsStrategy);; OK 58.127s
 *)
 module R = Reduction(ClosuresOnStackByValueFromEnvOrEnsStrategy);;
 module U = UriManager;;
 
-let whd = R.whd;;
+let profiler_whd = HExtlib.profile "are_convertible.whd"
+let whd = R.whd
 
   (* mimic ocaml (<< 3.08) "=" behaviour. Tests physical equality first then
     * fallbacks to structural equality *)
-let (===) x y = (Pervasives.compare x y = 0)
+let (===) x y =
+  Pervasives.compare x y = 0
 
 (* t1, t2 must be well-typed *)
-let are_convertible ?(subst=[]) ?(metasenv=[])  =
+let are_convertible whd ?(subst=[]) ?(metasenv=[])  =
  let rec aux test_equality_only context t1 t2 ugraph =
   let aux2 test_equality_only t1 t2 ugraph =
 
@@ -1031,8 +1021,18 @@ let are_convertible ?(subst=[]) ?(metasenv=[])  =
            debug_print (lazy (CicPp.ppterm t2));
            debug_print (lazy (CicPp.ppterm (whd ~subst context t2)))
        | _ -> ()); *)
-     let t1' = whd ~subst context t1 in
-     let t2' = whd ~subst context t2 in
+     let t1' =
+ let foo () =
+whd ?delta:(Some true) ?subst:(Some subst) context t1
+ in
+  profiler_whd.HExtlib.profile foo ()
+in
+     let t2' =
+ let foo () =
+whd ?delta:(Some true) ?subst:(Some subst) context t2
+ in
+  profiler_whd.HExtlib.profile foo ()
+in
       debug t1' [t2'] "POSTWHD";
       aux2 test_equality_only t1' t2' ugraph
     end
@@ -1040,6 +1040,35 @@ let are_convertible ?(subst=[]) ?(metasenv=[])  =
   aux false (*c t1 t2 ugraph *)
 ;;
 
+(* DEBUGGING ONLY
+let whd ?(delta=true) ?(subst=[]) context t = 
+ let res = whd ~delta ~subst context t in
+ let rescsc = CicReductionNaif.whd ~delta ~subst context t in
+  if not (fst (are_convertible CicReductionNaif.whd ~subst context res rescsc CicUniv.empty_ugraph)) then
+   begin
+    debug_print (lazy ("PRIMA: " ^ CicPp.ppterm t)) ;
+    flush stderr ;
+    debug_print (lazy ("DOPO: " ^ CicPp.ppterm res)) ;
+    flush stderr ;
+    debug_print (lazy ("CSC: " ^ CicPp.ppterm rescsc)) ;
+    flush stderr ;
+fdebug := 0 ;
+let _ =  are_convertible CicReductionNaif.whd ~subst context res rescsc CicUniv.empty_ugraph in
+    assert false ;
+   end
+  else 
+   res
+;;
+*)
+
+let are_convertible = are_convertible whd
+
+let profiler_other_whd = HExtlib.profile "~are_convertible.whd"
+let whd ?(delta=true) ?(subst=[]) context t = 
+ let foo () =
+  whd ~delta ~subst context t
+ in
+  profiler_other_whd.HExtlib.profile foo ()
 
 let rec normalize ?(delta=true) ?(subst=[]) ctx term =
   let module C = Cic in