X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Facic_procedural%2FproceduralOptimizer.ml;h=3ac5670956e91e3c4407985007b3a519b118d386;hb=a677e0d09755766c61ce9b30a98bec10cb8902b3;hp=20e04d322a1ae41c04a4180f54f7a8eba43ea8f2;hpb=04f22df647f35080b499b720bca7bc0eb1794c64;p=helm.git

diff --git a/helm/software/components/acic_procedural/proceduralOptimizer.ml b/helm/software/components/acic_procedural/proceduralOptimizer.ml
index 20e04d322..3ac567095 100644
--- a/helm/software/components/acic_procedural/proceduralOptimizer.ml
+++ b/helm/software/components/acic_procedural/proceduralOptimizer.ml
@@ -34,10 +34,15 @@ module HEL  = HExtlib
 module PEH  = ProofEngineHelpers
 module TC   = CicTypeChecker 
 module Un   = CicUniv
+module L    = Librarian
 
 module H    = ProceduralHelpers
 module Cl   = ProceduralClassify
 
+(* debugging ****************************************************************)
+
+let debug = ref false
+
 (* term preprocessing: optomization 1 ***************************************)
 
 let defined_premise = "DEFINED"
@@ -54,7 +59,7 @@ let clear_absts m =
       | C.Lambda (_, _, t) when n > 0 -> 
          aux 0 (pred n) (S.lift (-1) t)
       | t                  when n > 0 ->
-         Printf.eprintf "CicPPP clear_absts: %u %s\n" n (Pp.ppterm t);
+         Printf.eprintf "PO.clear_absts: %u %s\n" n (Pp.ppterm t);
 	 assert false 
       | t                                 -> t
    in 
@@ -275,15 +280,20 @@ let optimize_obj = function
    | C.Constant (name, Some bo, ty, pars, attrs) ->
       let bo, ty = H.cic_bc [] bo, H.cic_bc [] ty in 
       let g bo = 
-         Printf.eprintf "Optimized : %s\nPost Nodes: %u\n" 
-	    (Pp.ppterm bo) (I.count_nodes 0 bo);
-	 prerr_string "H.pp_term : ";
-	 H.pp_term prerr_string [] [] bo; prerr_newline ();
-	 let _ = H.get_type "opt" [] (C.Cast (bo, ty)) in
+         if !debug then begin 
+	    Printf.eprintf "Optimized : %s\nPost Nodes: %u\n" 
+	       (Pp.ppterm bo) (I.count_nodes 0 bo);
+	    prerr_string "H.pp_term : ";
+	    H.pp_term prerr_string [] [] bo; prerr_newline ()
+	 end;
+(*	 let _ = H.get_type "opt" [] (C.Cast (bo, ty)) in *)
+	 L.time_stamp ("PO: DONE       " ^ name);
 	 C.Constant (name, Some bo, ty, pars, attrs)
       in
-      Printf.eprintf "BEGIN: %s\nPre Nodes : %u\n" 
-         name (I.count_nodes 0 bo);
+         L.time_stamp ("PO: OPTIMIZING " ^ name);
+      if !debug then
+         Printf.eprintf "BEGIN: %s\nPre Nodes : %u\n" 
+            name (I.count_nodes 0 bo);
       begin try opt1_term g (* (opt2_term g []) *) true [] bo with
         | E.Object_not_found uri ->
 	   let msg = "optimize_obj: object not found: " ^ UM.string_of_uri uri in