1) new-style debugging/profiling code for old reduction

2) aliases are now dumped to stderr

diff --git a/helm/software/components/cic_proof_checking/cicReduction.ml b/helm/software/components/cic_proof_checking/cicReduction.ml
index 6e34360850caf0f2f5f48f85cee3c65e060833c7..5c5db75b4bb88f93ef54640b0952e77067338567 100644 (file)
--- a/helm/software/components/cic_proof_checking/cicReduction.ml
+++ b/helm/software/components/cic_proof_checking/cicReduction.ml
@@ -34,6 +34,37 @@ exception ReferenceToVariable;;
 exception ReferenceToCurrentProof;;
 exception ReferenceToInductiveDefinition;;
 
+let ndebug = ref false;;
+let indent = ref "";;
+let times = ref [];;
+let pp s =
+ if !ndebug then
+  prerr_endline (Printf.sprintf "%-20s" !indent ^ " " ^ Lazy.force s)
+;;
+let inside c =
+ if !ndebug then
+  begin
+   let time1 = Unix.gettimeofday () in
+   indent := !indent ^ String.make 1 c;
+   times := time1 :: !times;
+   prerr_endline ("{{{" ^ !indent ^ " ")
+  end
+;;
+let outside ok =
+ if !ndebug 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 debug = false
 let profile = false
 let debug_print s = if debug then prerr_endline (Lazy.force s)
@@ -805,6 +836,8 @@ let (===) x y =
 let are_convertible whd ?(subst=[]) ?(metasenv=[])  =
  let heuristic = ref true in
  let rec aux test_equality_only context t1 t2 ugraph =
+ (*D*)inside 'B'; try let rc = 
+  pp (lazy (CicPp.ppterm t1 ^ " vs " ^ CicPp.ppterm t2));
   let rec aux2 test_equality_only t1 t2 ugraph =
 
    (* this trivial euristic cuts down the total time of about five times ;-) *)
@@ -1102,6 +1135,7 @@ in
     aux2 test_equality_only t1' t2' ugraph
 *)
 end
+ (*D*)in outside true; rc with exc -> outside false; raise exc
  in
   aux false (*c t1 t2 ugraph *)
 ;;

diff --git a/helm/software/components/cic_proof_checking/cicReduction.mli b/helm/software/components/cic_proof_checking/cicReduction.mli
index 82be7fd3f5f43eface9449152ca330d64757c84e..fd98c4c0b99538c73e48ec7053388e130382689f 100644 (file)
--- a/helm/software/components/cic_proof_checking/cicReduction.mli
+++ b/helm/software/components/cic_proof_checking/cicReduction.mli
@@ -28,6 +28,7 @@ exception ReferenceToConstant
 exception ReferenceToVariable
 exception ReferenceToCurrentProof
 exception ReferenceToInductiveDefinition
+val ndebug : bool ref
 val fdebug : int ref
 val whd : 
   ?delta:bool -> ?subst:Cic.substitution -> Cic.context -> Cic.term -> Cic.term

diff --git a/helm/software/matita/matita.ml b/helm/software/matita/matita.ml
index dfb4e8ebd52b792333f32987a7be93a79d229d36..9699bdaa2fd21b14d0120b4cea19540e28afd4e4 100644 (file)
--- a/helm/software/matita/matita.ml
+++ b/helm/software/matita/matita.ml
@@ -150,7 +150,7 @@ let _ =
     in
     addDebugItem "dump aliases" (fun _ ->
       let status = script#grafite_status in
-      LexiconEngine.dump_aliases HLog.debug "" status);
+      LexiconEngine.dump_aliases prerr_endline "" status);
 (* FG: DEBUGGING   
     addDebugItem "dump interpretations" (fun _ ->
       let status = script#lexicon_status in
@@ -217,7 +217,7 @@ let _ =
       (fun mi () -> NCicRefiner.debug := mi#active; NCicUnification.debug :=
               mi#active; MultiPassDisambiguator.debug := mi#active);
     addDebugCheckbox "reduction logging"
-      (fun mi () -> NCicReduction.debug := mi#active);
+      (fun mi () -> NCicReduction.debug := mi#active; CicReduction.ndebug := mi#active);
     addDebugSeparator ();
     addDebugItem "Expand virtuals"
     (fun _ -> (MatitaScript.current ())#expandAllVirtuals);