From a806d6607af696065af3c9b0e3373de2846bf174 Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Mon, 12 Oct 2009 13:34:42 +0000
Subject: [PATCH] Improved debugging code.

---
 .../disambiguation/multiPassDisambiguator.ml  |  4 +-
 .../disambiguation/multiPassDisambiguator.mli |  2 +
 .../components/ng_refiner/nCicRefiner.ml      | 38 ++++++++++++-------
 helm/software/matita/matita.ml                |  4 +-
 4 files changed, 30 insertions(+), 18 deletions(-)

diff --git a/helm/software/components/disambiguation/multiPassDisambiguator.ml b/helm/software/components/disambiguation/multiPassDisambiguator.ml
index 86d037742..5767aa3e3 100644
--- 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 4977a81d9..a5b5def32 100644
--- 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 757fceea2..225c1898e 100644
--- 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 ec97442ac..6a4635c5d 100644
--- 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);
-- 
2.39.2