X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2FmetadataQuery.ml;h=962aad8e7cac5e93999ccba089737116340ebc7d;hb=ff981d975589f8d21a364e7cfe875647f7483cd9;hp=f26dae805be9e085a6a8d6d3d58ae7b4265c92c8;hpb=87955f4aa47c0f5f416f24bae4848eccb1cc23d5;p=helm.git

diff --git a/helm/ocaml/tactics/metadataQuery.ml b/helm/ocaml/tactics/metadataQuery.ml
index f26dae805..962aad8e7 100644
--- 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))
@@ -250,17 +252,6 @@ let experimental_hint
   ~(dbd:Mysql.dbd) ?(facts=false) ?signature ((proof, goal) as status) =
   let (_, metasenv, _, _) = proof in
   let (_, context, ty) = CicUtil.lookup_meta goal metasenv in
-  let uris = 
-    if facts then
-      ["cic:/Coq/Init/Logic/eq.ind#xpointer(1/1/1)"]
-    else
-      ["cic:/Coq/Init/Logic/eq.ind#xpointer(1/1/1)";
-       (* "cic:/Coq/Init/Logic/trans_eq.con"; *)
-       "cic:/Coq/Init/Logic/f_equal.con";
-       "cic:/Coq/Init/Logic/f_equal2.con";
-       "cic:/Coq/Init/Logic/f_equal3.con"] 
-  in
-  (* 
   let (uris, (main, sig_constants)) =
     match signature with
     | Some signature -> 
@@ -295,31 +286,31 @@ 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
-  in *)
+  in 
   let rec aux = function
     | [] -> []
     | uri :: tl ->
         (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
@@ -368,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
@@ -390,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
@@ -399,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 =