prerr_endine ==> debug_print everywhere

diff --git a/components/tactics/paramodulation/equality.ml b/components/tactics/paramodulation/equality.ml
index d9e16a255e362ed58d5592e1c9fe33e491e7f22a..30138b378f9eac358305f3ffbcc4170e05de44c7 100644 (file)
--- a/components/tactics/paramodulation/equality.ml
+++ b/components/tactics/paramodulation/equality.ml
@@ -260,7 +260,7 @@ let open_pred pred =
   match pred with 
   | Cic.Lambda (_,_,(Cic.Appl [Cic.MutInd (uri, 0,_);ty;l;r])) 
      when LibraryObjects.is_eq_URI uri -> ty,uri,l,r
-  | _ -> prerr_endline (CicPp.ppterm pred); assert false   
+  | _ -> Utils.debug_print (lazy (CicPp.ppterm pred)); assert false   
 ;;
 
 let is_not_fixed t =
@@ -290,7 +290,7 @@ let canonical t context menv =
        [] -> List.rev acc
      | (l',p)::tl when l=l' -> 
 if acc <> [] then
-prerr_endline ("!!! RISPARMIO " ^ string_of_int (List.length acc) ^ " PASSI");
+Utils.debug_print (lazy ("!!! RISPARMIO " ^ string_of_int (List.length acc) ^ " PASSI"));
          cut_to_last_duplicate l [l',p] tl
      | (l',p)::tl ->
          cut_to_last_duplicate l ((l',p)::acc) tl
@@ -358,7 +358,7 @@ prerr_endline ("!!! RISPARMIO " ^ string_of_int (List.length acc) ^ " PASSI");
                    Cic.Const (LibraryObjects.eq_f_sym_URI ~eq, [])
                  in
                  let rc = Cic.Appl [eq_f_sym;ty1;ty2;f;x;y;p] in
-                 prerr_endline ("CANONICAL " ^ CicPp.ppterm rc);
+                 Utils.debug_print (lazy ("CANONICAL " ^ CicPp.ppterm rc));
                  rc
              | Cic.Appl [Cic.MutConstruct (uri, 0, 1,_);_;_] as t
                  when LibraryObjects.is_eq_URI uri -> t
@@ -1328,7 +1328,7 @@ let draw_proof bag names goal_proof proof id =
   let oc = open_out "/tmp/matita_paramod.dot" in
   Buffer.output_buffer oc b;
   close_out oc;
-  prerr_endline "dot!";
+  Utils.debug_print (lazy "dot!");
   ignore(Unix.system 
     "dot -Tps -o /tmp/matita_paramod.eps /tmp/matita_paramod.dot"
 (* "cat /tmp/matita_paramod.dot| tred | dot -Tps -o /tmp/matita_paramod.eps" *)

diff --git a/components/tactics/paramodulation/saturation.ml b/components/tactics/paramodulation/saturation.ml
index f8b0ff45fcc088dcc5c799c93e8831c9be2f3b2b..6e792201964824db331fce7d3fc7813bac10be2a 100644 (file)
--- a/components/tactics/paramodulation/saturation.ml
+++ b/components/tactics/paramodulation/saturation.ml
@@ -31,6 +31,7 @@
 
 let connect_to_auto = true;;
 
+let debug_print = Utils.debug_print;;
 
 (* profiling statistics... *)
 let infer_time = ref 0.;;
@@ -801,13 +802,13 @@ let print_goals goals =
               
 let pp_goal_set msg goals names = 
   let active_goals, passive_goals = goals in
-  prerr_endline ("////" ^ msg);
-  prerr_endline ("ACTIVE G: " ^
+  debug_print (lazy ("////" ^ msg));
+  debug_print (lazy ("ACTIVE G: " ^
     (String.concat "\n " (List.map (fun (_,_,g) -> CicPp.pp g names)
-    active_goals)));
-  prerr_endline ("PASSIVE G: " ^
+    active_goals))));
+  debug_print (lazy ("PASSIVE G: " ^
     (String.concat "\n " (List.map (fun (_,_,g) -> CicPp.pp g names)
-    passive_goals)))
+    passive_goals))))
 ;;
 
 let check_if_goal_is_subsumed bag ((_,ctx,_) as env) table (goalproof,menv,ty) =
@@ -990,21 +991,21 @@ let pp_goals label goals context =
   let names = Utils.names_of_context context in
   List.iter                 
     (fun _,_,g -> 
-      prerr_endline 
-        (Printf.sprintf  "Current goal: %s = %s\n" label (CicPp.pp g names))) 
+      debug_print (lazy 
+        (Printf.sprintf  "Current goal: %s = %s\n" label (CicPp.pp g names))))
     (fst goals);
   List.iter                 
     (fun _,_,g -> 
-      prerr_endline 
-        (Printf.sprintf  "PASSIVE goal: %s = %s\n" label (CicPp.pp g names))) 
+      debug_print (lazy 
+        (Printf.sprintf  "PASSIVE goal: %s = %s\n" label (CicPp.pp g names))))
       (snd goals);
 ;;
 
 let print_status iterno goals active passive =
-  prerr_endline 
+  debug_print (lazy 
     (Printf.sprintf "\n%d #ACTIVES: %d #PASSIVES: %d #GOALSET: %d(%d)"
       iterno (size_of_active active) (size_of_passive passive)
-      (size_of_goal_set_a goals) (size_of_goal_set_p goals)) 
+      (size_of_goal_set_a goals) (size_of_goal_set_p goals)))
 ;;
 
 (** given-clause algorithm with full reduction strategy: NEW implementation *)
@@ -1055,9 +1056,9 @@ let given_clause
       in
       match check_if_goals_set_is_solved bag env active goals with
       | Some p -> 
-          prerr_endline 
+          debug_print (lazy 
             (Printf.sprintf "\nFound a proof in: %f\n" 
-              (Unix.gettimeofday() -. initial_time));
+              (Unix.gettimeofday() -. initial_time)));
           ParamodulationSuccess (p,active,passive)
       | None -> 
           (* SELECTION *)
@@ -1083,9 +1084,9 @@ let given_clause
                 if s_iterno < saturation_steps then
                   let current, passive = select env goals passive in
                   (* SIMPLIFICATION OF CURRENT *)
-                  prerr_endline
+                  debug_print (lazy
                         ("Selected : " ^ 
-                          Equality.string_of_equality ~env  current);
+                          Equality.string_of_equality ~env  current));
                   forward_simplify bag eq_uri env current active, passive
                 else
                   None, passive
@@ -1255,7 +1256,7 @@ let fix_proof metasenv context all_implicits p =
            try 
            let _ = CicUtil.lookup_meta i metasenv in metasenv
            with CicUtil.Meta_not_found _ ->
-            prerr_endline ("not found: "^(string_of_int i));
+            debug_print (lazy ("not found: "^(string_of_int i)));
            let metasenv,j = CicMkImplicit.mk_implicit_type metasenv [] context in
              (i,context,Cic.Meta(j,irl))::metasenv
          in
@@ -1316,17 +1317,17 @@ let build_proof
   bag status  
   goalproof newproof subsumption_id subsumption_subst proof_menv
 =
-  if proof_menv = [] then prerr_endline "+++++++++++++++VUOTA"
-  else prerr_endline (CicMetaSubst.ppmetasenv [] proof_menv);
+  if proof_menv = [] then debug_print (lazy "+++++++++++++++VUOTA")
+  else debug_print (lazy (CicMetaSubst.ppmetasenv [] proof_menv));
   let proof, goalno = status in
   let uri, metasenv, _subst, meta_proof, term_to_prove, attrs = proof in
   let _, context, type_of_goal = CicUtil.lookup_meta goalno metasenv in
   let eq_uri = eq_of_goal type_of_goal in 
   let names = Utils.names_of_context context in
-  prerr_endline "Proof:";
-  prerr_endline 
+  debug_print (lazy "Proof:");
+  debug_print (lazy 
     (Equality.pp_proof bag names goalproof newproof subsumption_subst
-       subsumption_id type_of_goal);
+       subsumption_id type_of_goal));
 (*
       prerr_endline ("max weight: " ^ 
        (string_of_int (Equality.max_weight goalproof newproof)));
@@ -1363,7 +1364,7 @@ let build_proof
   let goal_proof,goal_ty,real_menv,_ = 
     (* prerr_endline ("parte la refine per: " ^ (CicPp.pp goal_proof names)); *)
     try
-            prerr_endline (CicPp.ppterm goal_proof);
+            debug_print (lazy (CicPp.ppterm goal_proof));
       CicRefine.type_of_aux' real_menv context goal_proof CicUniv.empty_ugraph
     with 
       | CicRefine.RefineFailure s 
@@ -1385,7 +1386,7 @@ let build_proof
       | CicUnification.AssertFailure s -> assert false
          (*            fail "Maybe the local context of metas in the goal was not an IRL" s *)
   in
-  prerr_endline "+++++++++++++ FINE UNIF";
+  Utils.debug_print (lazy "+++++++++++++ FINE UNIF");
   let final_subst = 
     (goalno,(context,goal_proof,type_of_goal))::subst_side_effects
   in
@@ -1573,7 +1574,7 @@ let all_subsumed bag maxm status active passive =
   let env = metasenv,context,CicUniv.empty_ugraph in
   let cleaned_goal = Utils.remove_local_context type_of_goal in
   let goal = [], List.filter (fun (i,_,_)->i<>goalno) metasenv, cleaned_goal in
-  prerr_endline (string_of_int (List.length (fst active)));
+  debug_print (lazy (string_of_int (List.length (fst active))));
    (* we simplify using both actives passives *)
   let table = 
     List.fold_left 
@@ -1581,7 +1582,7 @@ let all_subsumed bag maxm status active passive =
       active (list_of_passive passive) in
   let _,goal = simplify_goal bag env goal table in
   let (_,_,ty) = goal in
-  prerr_endline (CicPp.ppterm ty);
+  debug_print (lazy (CicPp.ppterm ty));
   let subsumed = find_all_subsumed bag env (snd table) goal in
   let subsumed_or_id =
     match (check_if_goal_is_identity env goal) with
@@ -1623,10 +1624,10 @@ let given_clause
   let metasenv' = List.filter (fun (i,_,_)->i<>goalno) metasenv in
   let goal = [], metasenv', cleaned_goal in
   let env = metasenv,context,CicUniv.empty_ugraph in
-  prerr_endline ">>>>>> ACTIVES >>>>>>>>"; 
-  List.iter (fun e -> prerr_endline (Equality.string_of_equality ~env e))
+  debug_print (lazy ">>>>>> ACTIVES >>>>>>>>");
+  List.iter (fun e -> debug_print (lazy (Equality.string_of_equality ~env e)))
   active_l;
-  prerr_endline ">>>>>>>>>>>>>>"; 
+  debug_print (lazy ">>>>>>>>>>>>>>"); 
   let goals = make_goal_set goal in
   match 
 (* given_caluse non prende in input maxm ????? *)

diff --git a/components/tactics/paramodulation/utils.ml b/components/tactics/paramodulation/utils.ml
index 00d745fd906fb1ec2ac0aa6fa88a11faa17b7515..c6e64b898753f435e54a959a4d5c09dfc216e1c6 100644 (file)
--- a/components/tactics/paramodulation/utils.ml
+++ b/components/tactics/paramodulation/utils.ml
@@ -753,8 +753,7 @@ let guarded_simpl ?(debug=false) context t =
     if t = t' then t else
       begin
        let simpl_order = !compare_terms t t' in
-       if debug then
-         prerr_endline ("comparing "^(CicPp.ppterm t)^(CicPp.ppterm t'));
+        debug_print (lazy ("comparing "^(CicPp.ppterm t)^(CicPp.ppterm t')));
        if simpl_order = Gt then (if debug then prerr_endline "GT";t')
        else (if debug then prerr_endline "NO_GT";t)
       end