unification pps can be activated by the menu debug

diff --git a/helm/software/components/ng_refiner/nCicRefiner.ml b/helm/software/components/ng_refiner/nCicRefiner.ml
index b84c23aae9db4cb27c8ad6d64cb5317d08c75207..757fceea2a4a5dd83e728fb88e069a7f28f54957 100644 (file)
--- a/helm/software/components/ng_refiner/nCicRefiner.ml
+++ b/helm/software/components/ng_refiner/nCicRefiner.ml
@@ -22,13 +22,14 @@ let indent = ref "";;
 let inside c = indent := !indent ^ String.make 1 c;;
 let outside () = indent := String.sub !indent 0 (String.length !indent -1);;
 
-
+let debug = ref false;;
 let pp s = 
-  prerr_endline (Printf.sprintf "%-20s" !indent ^ " " ^ Lazy.force s)
+  if !debug then
+    prerr_endline (Printf.sprintf "%-20s" !indent ^ " " ^ Lazy.force s)
+  else 
+    ()
 ;;  
 
-let pp _ = ();;
-
 let wrap_exc msg = function
   | NCicUnification.Uncertain _ -> Uncertain msg
   | NCicUnification.UnificationFailure _ -> RefineFailure msg

diff --git a/helm/software/components/ng_refiner/nCicRefiner.mli b/helm/software/components/ng_refiner/nCicRefiner.mli
index b75ee3a815c6cf07dc0c60a0c5239929ac7e67f6..1a04d2abde5f442348b0ea921bc6a66e35829147 100644 (file)
--- a/helm/software/components/ng_refiner/nCicRefiner.mli
+++ b/helm/software/components/ng_refiner/nCicRefiner.mli
@@ -28,3 +28,4 @@ val typeof_obj :
  ?localise:(NCic.term -> Stdpp.location) ->
   NCic.obj -> NCic.obj
 
+val debug : bool ref

diff --git a/helm/software/components/ng_refiner/nCicUnification.ml b/helm/software/components/ng_refiner/nCicUnification.ml
index b91585fbe51fe699813919511004a80ee7d877a3..5353363d507bcbac84e6e939daa89dc0a343c038 100644 (file)
--- a/helm/software/components/ng_refiner/nCicUnification.ml
+++ b/helm/software/components/ng_refiner/nCicUnification.ml
@@ -78,20 +78,20 @@ let eta_reduce subst t =
 module C = NCic;;
 module Ref = NReference;;
 
-let debug = false;;
+let debug = ref false;;
 let indent = ref "";;
-let pp =
- if debug then
-  fun s -> prerr_endline (Printf.sprintf "%-20s" !indent ^ " " ^ Lazy.force s)
+let pp s =
+ if !debug then
+  prerr_endline (Printf.sprintf "%-20s" !indent ^ " " ^ Lazy.force s)
  else 
-  fun _ -> ()
+  ()
 ;;
 let inside c =
  indent := !indent ^ String.make 1 c;
- if debug then prerr_endline ("{{{" ^ !indent ^ " ")
+ if !debug then prerr_endline ("{{{" ^ !indent ^ " ")
 ;;
 let outside ok =
- if debug then prerr_endline "}}}";
+ if !debug then prerr_endline "}}}";
  if not ok then pp (lazy "exception raised!");
  try
   indent := String.sub !indent 0 (String.length !indent -1)

diff --git a/helm/software/components/ng_refiner/nCicUnification.mli b/helm/software/components/ng_refiner/nCicUnification.mli
index 86f5fae1aafa86d8285d5149de8affa0c82d7a9a..83a59b64c550ad977d38148d7b19428fca9d2b72 100644 (file)
--- a/helm/software/components/ng_refiner/nCicUnification.mli
+++ b/helm/software/components/ng_refiner/nCicUnification.mli
@@ -35,3 +35,5 @@ val delift_type_wrt_terms:
   NCic.term -> NCic.term list -> 
    NCic.metasenv * NCic.substitution * NCic.term
 
+
+val debug : bool ref

diff --git a/helm/software/matita/matita.ml b/helm/software/matita/matita.ml
index 1bfdf8ce372c49ab9cf93afa6a2ffd1c26ab8577..5abd0139c920629d155e27ae3f4d9ecabf98dc91 100644 (file)
--- a/helm/software/matita/matita.ml
+++ b/helm/software/matita/matita.ml
@@ -154,43 +154,6 @@ let _ =
          (fun x l -> (LexiconAstPp.pp_command x)::l)
          (filter status.LexiconEngine.lexicon_content_rev) [])));
 *)
-    addDebugItem "dump environment to \"env.dump\"" (fun _ ->
-      let oc = open_out "env.dump" in
-      CicEnvironment.dump_to_channel oc;
-      close_out oc);
-    addDebugItem "load environment from \"env.dump\"" (fun _ ->
-      let ic = open_in "env.dump" in
-      CicEnvironment.restore_from_channel ic;
-      close_in ic);
-    addDebugItem "dump universes" (fun _ ->
-      List.iter (fun (u,_,g) -> 
-        prerr_endline (UriManager.string_of_uri u); 
-        CicUniv.print_ugraph g) (CicEnvironment.list_obj ())
-      );
-    addDebugItem "dump environment content" (fun _ ->
-      List.iter (fun (u,_,_) -> 
-        prerr_endline (UriManager.string_of_uri u)) 
-        (CicEnvironment.list_obj ()));
-    addDebugItem "dump script status" script#dump;
-    addDebugItem "dump configuration file to ./foo.conf.xml" (fun _ ->
-      Helm_registry.save_to "./foo.conf.xml");
-    addDebugItem "dump metasenv"
-      (fun _ ->
-         if script#onGoingProof () then
-           HLog.debug (CicMetaSubst.ppmetasenv [] script#proofMetasenv));
-    addDebugItem "print top-level grammar entries"
-      CicNotationParser.print_l2_pattern;
-    addDebugItem "dump moo to stderr" (fun _ ->
-      let grafite_status = (MatitaScript.current ())#grafite_status in
-      let moo = grafite_status#moo_content_rev in
-      List.iter
-        (fun cmd ->
-          prerr_endline
-           (GrafiteAstPp.pp_command
-             ~term_pp:(fun t -> CicPp.ppterm t)
-             ~obj_pp:(fun _ -> assert false)
-             cmd))
-        (List.rev moo));
     addDebugItem "print metasenv goals and stack to stderr"
       (fun _ ->
         prerr_endline ("metasenv goals: " ^ String.concat " "
@@ -227,48 +190,11 @@ let _ =
             | Proof (_,m,_subst,p,ty, attrs) -> 
                 Cic.CurrentProof ("current proof",m,Lazy.force p,ty,[],attrs)
             | Intermediate _ -> assert false)));
-(*     addDebugItem "ask record choice"
-      (fun _ ->
-        HLog.debug (string_of_int
-          (MatitaGtkMisc.ask_record_choice ~gui ~title:"title" ~message:"msg"
-          ~fields:["a"; "b"; "c"]
-          ~records:[
-            ["0"; "0"; "0"]; ["0"; "0"; "1"]; ["0"; "1"; "0"]; ["0"; "1"; "1"];
-            ["1"; "0"; "0"]; ["1"; "0"; "1"]; ["1"; "1"; "0"]; ["1"; "1"; "1"]]
-          ()))); *)
-(*     addDebugItem "rotate light bulbs"
-      (fun _ ->
-         let nb = gui#main#hintNotebook in
-         nb#goto_page ((nb#current_page + 1) mod 3)); *)
     addDebugSeparator ();
-(*
-    addDebugItem "meets between L and R" 
-      (fun _ -> 
-        let l = CoercDb.coerc_carr_of_term (CicUtil.term_of_uri
-          (UriManager.uri_of_string "cic:/matita/test/L.ind#xpointer(1/1)" )) 
-        in
-        let r = CoercDb.coerc_carr_of_term (CicUtil.term_of_uri
-          (UriManager.uri_of_string "cic:/matita/test/R.ind#xpointer(1/1)" )) 
-        in
-        let meets = CoercGraph.meets l r in
-        prerr_endline "MEETS:";
-        List.iter (fun carr -> prerr_endline (CicPp.ppterm (CoercDb.term_of_carr
-        carr))) meets
-    );
-    addDebugSeparator ();
-*)
     addDebugItem "disable high level pretty printer"
       (fun _ -> CicMetaSubst.use_low_level_ppterm_in_context := true);
     addDebugItem "enable high level pretty printer"
       (fun _ -> CicMetaSubst.use_low_level_ppterm_in_context := false);
-(* ZACK moved to the View menu
-    addDebugItem "disable all (pretty printing) notations"
-      (fun _ -> CicNotation.set_active_notations []);
-    addDebugItem "enable all (pretty printing) notations"
-      (fun _ ->
-        CicNotation.set_active_notations
-          (List.map fst (CicNotation.get_all_notations ())));
-*)
     addDebugSeparator ();
     addDebugItem "enable multiple disambiguation passes (default)"
       (fun _ -> MultiPassDisambiguator.only_one_pass := false);
@@ -279,37 +205,10 @@ let _ =
     addDebugItem "prune disambiguation errors"
       (fun _ -> MatitaGui.all_disambiguation_passes := false);
     addDebugSeparator ();
-(* ZACK moved to the View menu
-    addDebugItem "enable coercions hiding"
-      (fun _ -> Acic2content.hide_coercions := true);
-    addDebugItem "disable coercions hiding"
-      (fun _ -> Acic2content.hide_coercions := false);
-*)
-    addDebugItem "show coercions graph" (fun _ ->
-      let c = MatitaMathView.cicBrowser () in
-      c#load (`About `Coercions));
-    addDebugItem "show coercions graph (full)" (fun _ ->
-      let c = MatitaMathView.cicBrowser () in
-      c#load (`About `CoercionsFull));
-    addDebugItem "dump coercions Db" (fun _ ->
-      List.iter
-      (fun (s,t,ul) -> 
-          HLog.debug
-           ((String.concat ","
-              (List.map
-                (fun u,saturations,_ ->
-                  UriManager.name_of_uri u ^
-                   "(" ^ string_of_int saturations ^ ")")
-                ul)) ^ ":"
-             ^ CoercDb.string_of_carr s ^ " -> " ^ CoercDb.string_of_carr t))
-        (CoercDb.to_list (CoercDb.dump ())));
-    addDebugSeparator ();
-    let mview () = (MatitaMathView.sequentsViewer_instance ())#cicMathView in
-(*     addDebugItem "save (sequent) MathML to matita.xml"
-      (fun _ -> ignore ((Gdome.domImplementation ())#saveDocumentToFile
-        ~doc:(HExtlib.unopt (mview ())#get_document) ~name:"matita.xml" ())); *)
-    addDebugItem "load (sequent) MathML from matita.xml"
-      (fun _ -> (mview ())#load_uri ~filename:"matita.xml");
+    addDebugItem "enable refiner/unification logging"
+      (fun _ -> NCicRefiner.debug := true; NCicUnification.debug := true;);
+    addDebugItem "disable refiner/unification logging"
+      (fun _ -> NCicRefiner.debug := false; NCicUnification.debug := false;);
     addDebugSeparator ();
     addDebugItem "Expand virtuals"
     (fun _ -> (MatitaScript.current ())#expandAllVirtuals);