snaphot

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

diff --git a/helm/ocaml/tactics/metadataQuery.ml b/helm/ocaml/tactics/metadataQuery.ml
index a232c67e4e621244ebae425102b1303b6c6608b1..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))
@@ -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
@@ -342,7 +333,7 @@ let experimental_hint
 let elim ~dbd uri =
   let constraints =
     [`Rel [`MainConclusion None];
-     `Sort (Cic.Prop,[`MainHypothesis (Some (MetadataTypes.Gt 1))]);
+     `Sort (Cic.Prop,[`MainHypothesis (Some (MetadataTypes.Ge 1))]);
      `Obj (uri,[`MainHypothesis (Some (MetadataTypes.Eq 0))]);
      `Obj (uri,[`InHypothesis]);
     ]
@@ -366,11 +357,11 @@ let fill_with_dummy_constants t =
 let instance ~dbd t =
   let t',types = fill_with_dummy_constants t in 
   let metadata = MetadataExtractor.compute ~body:None ~ty:t' in
-  List.iter 
+(*   List.iter 
     (fun x -> 
-       prerr_endline 
-        (MetadataPp.pp_constr (MetadataTypes.constr_of_metadata x))) 
-    metadata;
+       debug_print 
+         (MetadataPp.pp_constr (MetadataTypes.constr_of_metadata x))) 
+    metadata; *)
   let no_concl = MetadataDb.count_distinct `Conclusion metadata in
   let no_hyp = MetadataDb.count_distinct `Hypothesis metadata in
   let no_full = MetadataDb.count_distinct `Statement 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,8 +390,8 @@ 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 
-          (sprintf "Caso Some %d %s" depth (CicPp.ppterm dummy_type));
+(*         debug_print 
+          (sprintf "Caso Some %d %s" depth (CicPp.ppterm dummy_type)); *)
         (* a dummy in main position *)
         let metadata_for_dummy_type = 
           MetadataExtractor.compute ~body:None ~ty:dummy_type in