removed debug prerr_endline

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

diff --git a/helm/ocaml/tactics/metadataQuery.ml b/helm/ocaml/tactics/metadataQuery.ml
index fc5328e9ffa3c252267d44b77e2d1b21614a02ac..962aad8e7cac5e93999ccba089737116340ebc7d 100644 (file)
--- a/helm/ocaml/tactics/metadataQuery.ml
+++ b/helm/ocaml/tactics/metadataQuery.ml
@@ -28,6 +28,8 @@ open Printf
 module Constr = MetadataConstraints
 module PET = ProofEngineTypes 
 
+let debug_print = fun _ -> ()
+
   (** maps a shell like pattern (which uses '*' and '?') to a sql pattern for
   * the "like" operator (which uses '%' and '_'). Does not support escaping. *)
 let sqlpat_of_shellglob =
@@ -60,7 +62,7 @@ let locate ~(dbd:Mysql.dbd) ?(vars = false) pat =
       (fun cols -> match cols.(0) with Some s -> s | _ -> assert false))
 
 let match_term ~(dbd:Mysql.dbd) ty =
-(*   prerr_endline (CicPp.ppterm ty); *)
+(*   debug_print (CicPp.ppterm ty); *)
   let metadata = MetadataExtractor.compute ~body:None ~ty in
   let constants_no =
     MetadataConstraints.StringSet.cardinal (MetadataConstraints.constants_of ty)
@@ -188,13 +190,13 @@ let hint ~(dbd:Mysql.dbd) ?(facts=false) ?signature ((proof, goal) as status) =
   let hyp_constants =
     Constr.StringSet.diff (signature_of_hypothesis context) types_constants
   in
-(* Constr.StringSet.iter prerr_endline hyp_constants; *)
+(* Constr.StringSet.iter debug_print hyp_constants; *)
   let other_constants = Constr.StringSet.union sig_constants hyp_constants in
   let uris = 
     let pow = 2 ** (Constr.StringSet.cardinal other_constants) in
     if ((List.length uris < pow) or (pow <= 0))
     then begin
-(*       prerr_endline "MetadataQuery: large sig, falling back to old method"; *)
+(*       debug_print "MetadataQuery: large sig, falling back to old method"; *)
       filter_uris_forward ~dbd (main, other_constants) uris
     end else
       filter_uris_backward ~dbd ~facts (main, other_constants) uris
@@ -205,7 +207,7 @@ let hint ~(dbd:Mysql.dbd) ?(facts=false) ?signature ((proof, goal) as status) =
         (let status' =
             try
               let (proof, goal_list) =
-(*                prerr_endline ("STO APPLICANDO " ^ uri); *)
+(*                debug_print ("STO APPLICANDO " ^ uri); *)
                PET.apply_tactic
                   (PrimitiveTactics.apply_tac
                    ~term:(CicUtil.term_of_uri uri))
@@ -284,20 +286,20 @@ let experimental_hint
     in
     Constr.StringSet.union main hyp_and_sug
   in
-(* Constr.StringSet.iter prerr_endline hyp_constants; *)
+(* Constr.StringSet.iter debug_print hyp_constants; *)
   let all_constants_closed = close_with_types all_constants metasenv context in
   let other_constants = 
     Constr.StringSet.diff all_constants_closed types_constants
   in
-  prerr_endline "all_constants_closed";
-  Constr.StringSet.iter prerr_endline all_constants_closed;
-  prerr_endline "other_constants";
-  Constr.StringSet.iter prerr_endline other_constants;
+  debug_print "all_constants_closed";
+  Constr.StringSet.iter debug_print all_constants_closed;
+  debug_print "other_constants";
+  Constr.StringSet.iter debug_print other_constants;
   let uris = 
     let pow = 2 ** (Constr.StringSet.cardinal other_constants) in
     if ((List.length uris < pow) or (pow <= 0))
     then begin
-      prerr_endline "MetadataQuery: large sig, falling back to old method";
+      debug_print "MetadataQuery: large sig, falling back to old method";
       filter_uris_forward ~dbd (main, other_constants) uris
     end else
       filter_uris_backward ~dbd ~facts (main, other_constants) uris
@@ -308,7 +310,7 @@ let experimental_hint
         (let status' =
             try
               let (subst,(proof, goal_list)) =
-                  (* prerr_endline ("STO APPLICANDO" ^ uri); *)
+                  (* debug_print ("STO APPLICANDO" ^ uri); *)
                   PrimitiveTactics.apply_tac_verbose 
                    ~term:(CicUtil.term_of_uri uri)
                   status
@@ -357,7 +359,7 @@ let instance ~dbd t =
   let metadata = MetadataExtractor.compute ~body:None ~ty:t' in
 (*   List.iter 
     (fun x -> 
-       prerr_endline 
+       debug_print 
          (MetadataPp.pp_constr (MetadataTypes.constr_of_metadata x))) 
     metadata; *)
   let no_concl = MetadataDb.count_distinct `Conclusion metadata in
@@ -379,7 +381,7 @@ let instance ~dbd t =
   in
   match (look_for_dummy_main metadata) with
     | None->
-(*         prerr_endline "Caso None"; *)
+(*         debug_print "Caso None"; *)
         (* no dummy in main position *)
         let metadata = List.filter is_dummy metadata in
         let constraints = List.map MetadataTypes.constr_of_metadata metadata in
@@ -388,7 +390,7 @@ let instance ~dbd t =
         let diff = Some (MetadataConstraints.Eq (no_hyp - no_concl)) in
           Constr.at_least ~dbd ?concl_card ?full_card ?diff constraints
     | Some (depth, dummy_type) ->
-(*         prerr_endline 
+(*         debug_print 
           (sprintf "Caso Some %d %s" depth (CicPp.ppterm dummy_type)); *)
         (* a dummy in main position *)
         let metadata_for_dummy_type =