- reimplemented tacticChaser and friends in term of Metadata module and friends

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

diff --git a/helm/ocaml/tactics/variousTactics.ml b/helm/ocaml/tactics/variousTactics.ml
index 9293d14399756c7eb5ee677982700f42b819f16c..f986bc867dcf5c1ed61655bc95267fa2a867e1ab 100644 (file)
--- a/helm/ocaml/tactics/variousTactics.ml
+++ b/helm/ocaml/tactics/variousTactics.ml
@@ -181,12 +181,12 @@ let new_search_theorems f proof goal depth gtl =
 
 exception NoOtherChoices;;
 
-let rec auto_new mqi_handle = function
+let rec auto_new dbh = function
     [] -> raise NoOtherChoices
   | (proof, [])::tl -> (proof, [])::tl
-  | (proof, (goal,0)::gtl)::tl -> auto_new mqi_handle tl
+  | (proof, (goal,0)::gtl)::tl -> auto_new dbh tl
   | (proof, (goal,depth)::gtl)::tl ->
-      let _,metasenv,_,_ = proof in
+      let _,metasenv,proof_obj,_ = proof in
       let meta_inf = 
        (try 
           let (_, ey ,ty) = CicUtil.lookup_meta goal metasenv in
@@ -196,12 +196,14 @@ let rec auto_new mqi_handle = function
            Some (ey, ty) ->
               prerr_endline ("CURRENT GOAL = " ^ (CicPp.ppterm ty));
                prerr_endline ("CURRENT HYP = " ^ (fst (print_context ey)));
+               prerr_endline ("CURRENT PROOF = " ^ (CicPp.ppterm proof_obj));
              let local_choices =
                new_search_theorems 
                  search_theorems_in_context proof goal (depth-1) gtl in
              let global_choices =
                new_search_theorems 
-                 (TacticChaser.searchTheorems mqi_handle) 
+                  (fun status -> List.map snd (MetadataQuery.hint ~dbh status))
+(*               (TacticChaser.searchTheorems mqi_handle)  *)
                  proof goal (depth-1) gtl in
              let all_choices =
                local_choices@global_choices@tl in
@@ -214,17 +216,17 @@ let rec auto_new mqi_handle = function
              let reorder = 
                List.stable_sort sorting_list all_choices
              in
-               auto_new mqi_handle reorder
-         | None -> auto_new mqi_handle ((proof,gtl)::tl)
+               auto_new dbh reorder
+         | None -> auto_new dbh ((proof,gtl)::tl)
 ;;
 
 
-let auto_tac mqi_handle =
+let auto_tac ~(dbh:Dbi.connection) =
 (*   CicMetaSubst.reset_counters (); *)
- let auto_tac mqi_handle (proof,goal) =
+ let auto_tac dbh (proof,goal) =
   prerr_endline "Entro in Auto";
   try 
-    (match auto_new mqi_handle [(proof, [(goal,depth)])] with
+    (match auto_new dbh [(proof, [(goal,depth)])] with
     | (proof,_)::_  ->
       prerr_endline "AUTO_TAC HA FINITO";
   (*     CicMetaSubst.print_counters (); *)
@@ -235,7 +237,7 @@ let auto_tac mqi_handle =
       prerr_endline("Auto failed");
       raise (ProofEngineTypes.Fail "No Applicable theorem")
  in
-  ProofEngineTypes.mk_tactic (auto_tac mqi_handle)
+  ProofEngineTypes.mk_tactic (auto_tac dbh)
 ;;
 
 (* TODO se ce n'e' piu' di una, prende la prima che trova... sarebbe meglio