From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Thu, 8 Oct 2009 16:13:54 +0000 (+0000)
Subject: A new switch to activate/deactive nCicReduction pretty printing.
X-Git-Tag: make_still_working~3346
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=cdd019ea6419fc058a92b1aca950a4eff11188d1;p=helm.git

A new switch to activate/deactive nCicReduction pretty printing.
---

diff --git a/helm/software/components/ng_kernel/nCicReduction.ml b/helm/software/components/ng_kernel/nCicReduction.ml
index 2417f718b..717644ac5 100644
--- a/helm/software/components/ng_kernel/nCicReduction.ml
+++ b/helm/software/components/ng_kernel/nCicReduction.ml
@@ -17,6 +17,9 @@ module E = NCicEnvironment
 
 exception AssertFailure of string Lazy.t;;
 
+let debug = ref false;;
+let pp m = if !debug then prerr_endline (Lazy.force m) else ();;
+
 module type Strategy = sig
   type stack_term
   type env_term
diff --git a/helm/software/components/ng_kernel/nCicReduction.mli b/helm/software/components/ng_kernel/nCicReduction.mli
index 9cff07d8f..713edd170 100644
--- a/helm/software/components/ng_kernel/nCicReduction.mli
+++ b/helm/software/components/ng_kernel/nCicReduction.mli
@@ -13,6 +13,8 @@
 
 exception AssertFailure of string Lazy.t;;
 
+val debug: bool ref
+
 val whd : 
   ?delta:int -> subst:NCic.substitution -> 
   NCic.context -> NCic.term -> 
diff --git a/helm/software/matita/matita.ml b/helm/software/matita/matita.ml
index 5abd0139c..ec97442ac 100644
--- a/helm/software/matita/matita.ml
+++ b/helm/software/matita/matita.ml
@@ -210,6 +210,11 @@ let _ =
     addDebugItem "disable refiner/unification logging"
       (fun _ -> NCicRefiner.debug := false; NCicUnification.debug := false;);
     addDebugSeparator ();
+    addDebugItem "enable reduction logging"
+      (fun _ -> NCicReduction.debug := true);
+    addDebugItem "disable reduction logging"
+      (fun _ -> NCicReduction.debug := false);
+    addDebugSeparator ();
     addDebugItem "Expand virtuals"
     (fun _ -> (MatitaScript.current ())#expandAllVirtuals);
   end