unification completed

[helm.git] / helm / software / components / acic_procedural / proceduralOptimizer.ml

diff --git a/helm/software/components/acic_procedural/proceduralOptimizer.ml b/helm/software/components/acic_procedural/proceduralOptimizer.ml
index 20e04d322a1ae41c04a4180f54f7a8eba43ea8f2..3ac5670956e91e3c4407985007b3a519b118d386 100644 (file)
--- 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