removed debug prerr_endline

[helm.git] / helm / ocaml / tactics / autoTactic.ml

diff --git a/helm/ocaml/tactics/autoTactic.ml b/helm/ocaml/tactics/autoTactic.ml
index 88f72ffa09d4d9b194f5f62b2eccbe67ce9882d4..6afef50e050f2fb69a5f4e7ad0b9292f7cea9dd1 100644 (file)
--- a/helm/ocaml/tactics/autoTactic.ml
+++ b/helm/ocaml/tactics/autoTactic.ml
@@ -23,6 +23,8 @@
  * http://cs.unibo.it/helm/.
  *)
 
+let debug_print = fun _ -> ()
+
 (* Da rimuovere, solo per debug*)
 let print_context ctx =
     let print_name =
@@ -106,9 +108,9 @@ let rec auto dbd = function
          Some (ey, ty) ->
             (* the goal is still there *)
             (*
-           prerr_endline ("CURRENT GOAL = " ^ (CicPp.ppterm ty));
-           prerr_endline ("CURRENT PROOF = " ^ (CicPp.ppterm p));
-           prerr_endline ("CURRENT HYP = " ^ (fst (print_context ey)));
+           debug_print ("CURRENT GOAL = " ^ (CicPp.ppterm ty));
+           debug_print ("CURRENT PROOF = " ^ (CicPp.ppterm p));
+           debug_print ("CURRENT HYP = " ^ (fst (print_context ey)));
             *)
             (* if the goal contains metavariables we use the input
                signature for at_most constraints *)
@@ -156,12 +158,12 @@ let rec auto dbd = function
 
 let auto_tac  ?num ~(dbd:Mysql.dbd) =
   let auto_tac dbh (proof,goal) =
-  prerr_endline "Entro in Auto";
+  debug_print "Entro in Auto";
   match (auto dbd [(proof, [(goal,depth)],None)]) with
-      [] ->  prerr_endline("Auto failed");
+      [] ->  debug_print("Auto failed");
        raise (ProofEngineTypes.Fail "No Applicable theorem")
     | (proof,[],_)::_ ->  
-       prerr_endline "AUTO_TAC HA FINITO";
+       debug_print "AUTO_TAC HA FINITO";
        (proof,[])
     | _ -> assert false
   in
@@ -335,8 +337,8 @@ let rec auto_single dbd proof goal ey ty depth width sign already_seen_goals
       match exitus with
          Yes (bo,_) ->
             (*
-              prerr_endline "ALREADY PROVED!!!!!!!!!!!!!!!!!!!!!!!!!!!!";
-             prerr_endline (CicPp.ppterm ty);
+              debug_print "ALREADY PROVED!!!!!!!!!!!!!!!!!!!!!!!!!!!!";
+             debug_print (CicPp.ppterm ty);
             *)
             let subst_in =
               (* if we just apply the subtitution, the type 
@@ -349,14 +351,14 @@ let rec auto_single dbd proof goal ey ty depth width sign already_seen_goals
                proof goal subst_in metasenv in
              [(subst_in,(proof,[],sign))]
         | No d when (d >= depth) -> 
-           (* prerr_endline "PRUNED!!!!!!!!!!!!!!!!!!!!!!!!!!!!"; *)
+           (* debug_print "PRUNED!!!!!!!!!!!!!!!!!!!!!!!!!!!!"; *)
            [] (* the empty list means no choices, i.e. failure *)
        | No _ 
        | NotYetInspected ->
              (*
-             prerr_endline ("CURRENT GOAL = " ^ (CicPp.ppterm ty));
-             prerr_endline ("CURRENT PROOF = " ^ (CicPp.ppterm p));
-             prerr_endline ("CURRENT HYP = " ^ (fst (print_context ey)));
+             debug_print ("CURRENT GOAL = " ^ (CicPp.ppterm ty));
+             debug_print ("CURRENT PROOF = " ^ (CicPp.ppterm p));
+             debug_print ("CURRENT HYP = " ^ (fst (print_context ey)));
              *)
            let sign, new_sign =
              if is_meta_closed then
@@ -409,8 +411,8 @@ let rec auto_single dbd proof goal ey ty depth width sign already_seen_goals
                             in
                               if not (cty = ty) then
                                 begin
-                                  prerr_endline ("ty =  "^CicPp.ppterm ty);
-                                  prerr_endline ("cty =  "^CicPp.ppterm cty);
+                                  debug_print ("ty =  "^CicPp.ppterm ty);
+                                  debug_print ("cty =  "^CicPp.ppterm cty);
                                   assert false
                                 end
                                   Hashtbl.add inspected_goals 
@@ -456,7 +458,7 @@ and auto_new_aux dbd width already_seen_goals = function
       let maxdepthgoals = reorder_goals dbd sign proof maxdepthgoals in
       let len2 = List.length maxdepthgoals in
        match maxdepthgoals with
-         [] -> prerr_endline 
+         [] -> debug_print 
            ("caso sospetto " ^ (string_of_int (List.length othergoals)) ^ " " ^ string_of_int depth);
            auto_new dbd 
              width already_seen_goals((subst,(proof, othergoals, sign))::tl) 
@@ -492,7 +494,7 @@ and auto_new_aux dbd width already_seen_goals = function
                        auto_new dbd width already_seen_goals all_choices 
                  | _ -> assert false
            end
-         | None -> prerr_endline "caso none";
+         | None -> debug_print "caso none";
              auto_new 
                dbd width already_seen_goals ((subst,(proof, gtl, sign))::tl)
              end
@@ -502,15 +504,15 @@ and auto_new_aux dbd width already_seen_goals = function
 let auto_tac_new  ~(dbd:Mysql.dbd) =
   let auto_tac dbd (proof,goal) =
   Hashtbl.clear inspected_goals;
-  prerr_endline "Entro in Auto";
+  debug_print "Entro in Auto";
   let id t = t in
   match (auto_new dbd width [] [id,(proof, [(goal,depth)],None)]) with
-      [] ->  prerr_endline("Auto failed");
+      [] ->  debug_print("Auto failed");
        raise (ProofEngineTypes.Fail "No Applicable theorem")
     | (_,(proof,[],_))::_ ->  
-       prerr_endline "AUTO_TAC HA FINITO";
+       debug_print "AUTO_TAC HA FINITO";
        let _,_,p,_ = proof in
-       prerr_endline (CicPp.ppterm p);
+       debug_print (CicPp.ppterm p);
        (proof,[])
     | _ -> assert false
   in