X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2FvariousTactics.ml;h=f986bc867dcf5c1ed61655bc95267fa2a867e1ab;hb=a7ab0ef67114c3152920f03ae1d7bfaaf1fae290;hp=0566564dc276c863954bf4c43facd662ad5f7223;hpb=655906d74521fa49de332f54ec34bfc9d9744151;p=helm.git

diff --git a/helm/ocaml/tactics/variousTactics.ml b/helm/ocaml/tactics/variousTactics.ml
index 0566564dc..f986bc867 100644
--- 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,24 +216,28 @@ 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 mqi_handle (proof,goal) =
+let auto_tac ~(dbh:Dbi.connection) =
+(*   CicMetaSubst.reset_counters (); *)
+ let auto_tac dbh (proof,goal) =
   prerr_endline "Entro in Auto";
   try 
-    let (proof,_)::_ = auto_new mqi_handle [(proof, [(goal,depth)])] in
-prerr_endline "AUTO_TAC HA FINITO";
-    (proof,[])
+    (match auto_new dbh [(proof, [(goal,depth)])] with
+    | (proof,_)::_  ->
+      prerr_endline "AUTO_TAC HA FINITO";
+  (*     CicMetaSubst.print_counters (); *)
+      (proof,[])
+    | _ -> assert false)
   with 
   | NoOtherChoices ->
       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