removed no longer used METAs

[helm.git] / helm / ocaml / tactics / paramodulation / saturation.ml

diff --git a/helm/ocaml/tactics/paramodulation/saturation.ml b/helm/ocaml/tactics/paramodulation/saturation.ml
index 9c4dce4603cd055d9db0709beb7d2ad18caaceeb..6a700d868a30fd792279e13affc4e7a0b10ae2d6 100644 (file)
--- a/helm/ocaml/tactics/paramodulation/saturation.ml
+++ b/helm/ocaml/tactics/paramodulation/saturation.ml
@@ -28,6 +28,25 @@
 open Inference;;
 open Utils;;
 
+(*
+for debugging 
+let check_equation env equation msg =
+  let w, proof, (eq_ty, left, right, order), metas, args = equation in
+  let metasenv, context, ugraph = env in
+  let metasenv' = metasenv @ metas in
+    try
+      CicTypeChecker.type_of_aux' metasenv' context left ugraph;
+      CicTypeChecker.type_of_aux' metasenv' context right ugraph;
+      ()
+    with 
+       CicUtil.Meta_not_found _ as exn ->
+         begin
+           prerr_endline msg; 
+           prerr_endline (CicPp.ppterm left);
+           prerr_endline (CicPp.ppterm right);
+           raise exn
+         end 
+*)
 
 (* set to false to disable paramodulation inside auto_tac *)
 let connect_to_auto = true;;
@@ -483,22 +502,6 @@ let forward_simplify env (sign, current) ?passive (active_list, active_table) =
   
   let demodulate table current = 
     let newmeta, newcurrent =
-      let _ =
-        let w, proof, (eq_ty, left, right, order), metas, args = current in
-       let metasenv, context, ugraph = env in
-       let metasenv' = metasenv @ metas in
-       try
-         CicTypeChecker.type_of_aux' metasenv' context left ugraph;
-         CicTypeChecker.type_of_aux' metasenv' context right ugraph;
-       with 
-           CicUtil.Meta_not_found _ as exn ->
-             begin
-               prerr_endline "siamo in forward_simplify"; 
-               prerr_endline (CicPp.ppterm left);
-               prerr_endline (CicPp.ppterm right);
-               raise exn
-             end 
-      in
       Indexing.demodulation_equality !maxmeta env table sign current in
     maxmeta := newmeta;
     if is_identity env newcurrent then
@@ -584,22 +587,6 @@ let forward_simplify_new env (new_neg, new_pos) ?passive active =
   
   let demodulate sign table target =
     let newmeta, newtarget =
-      let _ =
-        let w, proof, (eq_ty, left, right, order), metas, args = target in
-       let metasenv, context, ugraph = env in
-       let metasenv' = metasenv @ metas in
-       try
-         CicTypeChecker.type_of_aux' metasenv' context left ugraph;
-         CicTypeChecker.type_of_aux' metasenv' context right ugraph;
-       with 
-           CicUtil.Meta_not_found _ as exn ->
-             begin
-               prerr_endline "siamo in forward_simplify_new"; 
-               prerr_endline (CicPp.ppterm left);
-               prerr_endline (CicPp.ppterm right);
-               raise exn
-             end 
-      in
       Indexing.demodulation_equality !maxmeta env table sign target in
     maxmeta := newmeta;
     newtarget
@@ -609,11 +596,14 @@ let forward_simplify_new env (new_neg, new_pos) ?passive active =
   let new_neg, new_pos =
     let new_neg = List.map (demodulate Negative active_table) new_neg
     and new_pos = List.map (demodulate Positive active_table) new_pos in
+      new_neg,new_pos
+
+(* PROVA
     match passive_table with
     | None -> new_neg, new_pos
     | Some passive_table ->
         List.map (demodulate Negative passive_table) new_neg,
-        List.map (demodulate Positive passive_table) new_pos
+        List.map (demodulate Positive passive_table) new_pos *)
   in
 
   let t2 = Unix.gettimeofday () in
@@ -1853,6 +1843,7 @@ let main dbd full term metasenv ugraph =
   let _, context, goal = CicUtil.lookup_meta goal' metasenv in
   let eq_indexes, equalities, maxm = find_equalities context proof in
   let lib_eq_uris, library_equalities, maxm =
+
     find_library_equalities dbd context (proof, goal') (maxm+2)
   in
   let library_equalities = List.map snd library_equalities in
@@ -2137,7 +2128,18 @@ let saturate
           raise (ProofEngineTypes.Fail
                   (lazy "Found a proof, but it doesn't typecheck"))
       in
+      let tall = fs_time_info.build_all in
+      let tdemodulate = fs_time_info.demodulate in
+      let tsubsumption = fs_time_info.subsumption in
       debug_print (lazy (Printf.sprintf "\nTIME NEEDED: %.9f" time));
+      debug_print (lazy (Printf.sprintf "\ntall: %.9f" tall));
+      debug_print (lazy (Printf.sprintf "\ntdemod: %.9f" tdemodulate));
+      debug_print (lazy (Printf.sprintf "\ntsubsumption: %.9f" tsubsumption));
+      debug_print (lazy (Printf.sprintf "\ninfer_time: %.9f" !infer_time));
+      debug_print (lazy (Printf.sprintf "\nforward_simpl_times: %.9f" !forward_simpl_time));
+      debug_print (lazy (Printf.sprintf "\nforward_simpl_new_times: %.9f" !forward_simpl_new_time));
+      debug_print (lazy (Printf.sprintf "\nbackward_simpl_times: %.9f" !backward_simpl_time));
+      debug_print (lazy (Printf.sprintf "\npassive_maintainance_time: %.9f" !passive_maintainance_time));
       newstatus          
   | _ ->
       raise (ProofEngineTypes.Fail (lazy "NO proof found"))