Improved debugging code.

diff --git a/helm/software/components/disambiguation/multiPassDisambiguator.ml b/helm/software/components/disambiguation/multiPassDisambiguator.ml
index 86d037742652c99085ff07092dceaf371447d5dd..5767aa3e3f04f09564beb9aa1d70d64f846f9335 100644 (file)
--- a/helm/software/components/disambiguation/multiPassDisambiguator.ml
+++ b/helm/software/components/disambiguation/multiPassDisambiguator.ml
@@ -27,9 +27,9 @@
 
 open Printf
 
-let debug = false;;
+let debug = ref false;;
 let debug_print s =
- if debug then prerr_endline (Lazy.force s);;
+ if !debug then prerr_endline (Lazy.force s) else ();;
 
 exception DisambiguationError of
  int *

diff --git a/helm/software/components/disambiguation/multiPassDisambiguator.mli b/helm/software/components/disambiguation/multiPassDisambiguator.mli
index 4977a81d9cec60e9e370cce909d9164009bcb46f..a5b5def32df25efaa6eead61293d1970e95d2020 100644 (file)
--- a/helm/software/components/disambiguation/multiPassDisambiguator.mli
+++ b/helm/software/components/disambiguation/multiPassDisambiguator.mli
@@ -23,6 +23,8 @@
  * http://helm.cs.unibo.it/
  *)
 
+val debug: bool ref
+
 (* the integer is an offset to be added to each location *)
 exception DisambiguationError of
  int *

diff --git a/helm/software/components/ng_refiner/nCicRefiner.ml b/helm/software/components/ng_refiner/nCicRefiner.ml
index 757fceea2a4a5dd83e728fb88e069a7f28f54957..225c1898e022f78fa5758e5d51c83e9b8e2afa31 100644 (file)
--- a/helm/software/components/ng_refiner/nCicRefiner.ml
+++ b/helm/software/components/ng_refiner/nCicRefiner.ml
@@ -18,17 +18,27 @@ exception AssertFailure of string Lazy.t;;
 module C = NCic
 module Ref = NReference
 
+let debug = ref false;;
 let indent = ref "";;
-let inside c = indent := !indent ^ String.make 1 c;;
-let outside () = indent := String.sub !indent 0 (String.length !indent -1);;
+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 ^ " ")
+;;
+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 := "??"; ()
+;;
 
-let debug = ref false;;
-let pp s = 
-  if !debug then
-    prerr_endline (Printf.sprintf "%-20s" !indent ^ " " ^ Lazy.force s)
-  else 
-    ()
-;;  
 
 let wrap_exc msg = function
   | NCicUnification.Uncertain _ -> Uncertain msg
@@ -94,7 +104,7 @@ let check_allowed_sort_elimination rdb localise r orig =
         with exc -> raise (wrap_exc (lazy (localise orig, 
           "Sort elimination not allowed ")) exc))
      | _ -> assert false
-     (*D*)in outside(); rc with exc -> outside (); raise exc
+     (*D*)in outside true; rc with exc -> outside false; raise exc
    in
     aux
 ;;
@@ -119,7 +129,7 @@ let rec typeof rdb
              let metasenv, subst =
     (*D*)inside 'U'; try let rc = 
                NCicUnification.unify rdb metasenv subst context infty expty 
-    (*D*)in outside(); rc with exc -> outside (); raise exc
+    (*D*)in outside true; rc with exc -> outside false; raise exc
              in
              metasenv, subst, t, expty
            with 
@@ -128,7 +138,7 @@ let rec typeof rdb
              try_coercions rdb ~localise 
                metasenv subst context t orig infty expty true exc)
     | None -> metasenv, subst, t, infty
-    (*D*)in outside(); rc with exc -> outside (); raise exc
+    (*D*)in outside true; rc with exc -> outside false; raise exc
   in
   let rec typeof_aux metasenv subst context expty = 
     fun t as orig -> 
@@ -366,7 +376,7 @@ let rec typeof rdb
     pp (lazy (NCicPp.ppterm ~metasenv ~subst ~context t ^ " ::inf:: "^
          NCicPp.ppterm ~metasenv ~subst ~context infty ));
       force_ty true true metasenv subst context orig t infty expty
-    (*D*)in outside(); rc with exc -> outside (); raise exc
+    (*D*)in outside true; rc with exc -> outside false; raise exc
   in
     typeof_aux metasenv subst context expty term
 
@@ -579,7 +589,7 @@ and eat_prods rdb ~localise force_ty metasenv subst context expty orig_t orig_he
     List.partition (fun (i,_) -> i <= highest_meta) metasenv
    in
     (List.rev metasenv_new) @ metasenv_old, subst, newhead, newheadty
-  (*D*)in outside(); rc with exc -> outside (); raise exc
+  (*D*)in outside true; rc with exc -> outside false; raise exc
 ;;
 
 let rec first f l1 l2 =

diff --git a/helm/software/matita/matita.ml b/helm/software/matita/matita.ml
index ec97442ace47dfa50e3123ea6cee8f9b87fcfbb1..6a4635c5d6477513caf4097ad8353f854ac79b58 100644 (file)
--- a/helm/software/matita/matita.ml
+++ b/helm/software/matita/matita.ml
@@ -206,9 +206,9 @@ let _ =
       (fun _ -> MatitaGui.all_disambiguation_passes := false);
     addDebugSeparator ();
     addDebugItem "enable refiner/unification logging"
-      (fun _ -> NCicRefiner.debug := true; NCicUnification.debug := true;);
+      (fun _ -> NCicRefiner.debug := true; NCicUnification.debug := true; MultiPassDisambiguator.debug := true);
     addDebugItem "disable refiner/unification logging"
-      (fun _ -> NCicRefiner.debug := false; NCicUnification.debug := false;);
+      (fun _ -> NCicRefiner.debug := false; NCicUnification.debug := false; MultiPassDisambiguator.debug := false);
     addDebugSeparator ();
     addDebugItem "enable reduction logging"
       (fun _ -> NCicReduction.debug := true);