X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2FvariousTactics.ml;h=70952d84d5157d2d6a73f1aec8b89165261824f4;hb=78cf601fd8b8dbb386b0db315dcbfdbe8256c15f;hp=04959e6962fdc2bd246db1282ae516682e5c837b;hpb=f5b6be7239a35e1d0aba504605b5a0df5cf06726;p=helm.git

diff --git a/helm/ocaml/tactics/variousTactics.ml b/helm/ocaml/tactics/variousTactics.ml
index 04959e696..70952d84d 100644
--- a/helm/ocaml/tactics/variousTactics.ml
+++ b/helm/ocaml/tactics/variousTactics.ml
@@ -23,6 +23,78 @@
  * http://cs.unibo.it/helm/.
  *)
 
+let search_theorems_in_context ~status:((proof,goal) as status) =
+  let module C = Cic in
+  let module R = CicReduction in
+  let module S = CicSubstitution in
+  prerr_endline "Entro in search_context";
+  let _,metasenv,_,_ = proof in
+  let _,context,ty = CicUtil.lookup_meta goal metasenv in
+  let rec find n = function 
+      [] -> []
+    | hd::tl ->
+	let res =
+	  try 
+            Some (PrimitiveTactics.apply_tac ~status ~term:(C.Rel n)) 
+	  with 
+	    ProofEngineTypes.Fail _ -> None in
+	(match res with
+	  Some res -> res::(find (n+1) tl)
+	| None -> find (n+1) tl)
+  in
+  try 
+    let res = find 1 context in
+    prerr_endline "Ho finito context";
+    res 
+  with Failure s -> 
+    prerr_endline ("SIAM QUI = " ^ s); []
+;;     
+
+
+exception NotApplicableTheorem;;
+exception MaxDepth;;
+
+let depth = 5;;
+
+let rec auto_tac mqi_handle level proof goal = 
+prerr_endline "Entro in Auto_rec";
+if level = 0 then
+  (* (proof, [goal]) *)
+  (prerr_endline ("NON ci credo");
+   raise MaxDepth)
+else 
+  (* choices is a list of pairs proof and goallist *)
+  let choices  =
+    (search_theorems_in_context ~status:(proof,goal))@ 
+    (TacticChaser.searchTheorems mqi_handle ~status:(proof,goal)) 
+  in
+  let rec try_choices = function
+    [] -> raise NotApplicableTheorem
+  | (proof,goallist)::tl ->
+prerr_endline ("GOALLIST = " ^ string_of_int (List.length goallist));
+       (try 
+          List.fold_left 
+            (fun (proof,opengoals) goal ->
+              let newproof, newgoals = auto_tac mqi_handle (level-1) proof goal in
+              (newproof, newgoals@opengoals))
+          (proof,[]) goallist
+        with 
+	| MaxDepth
+        | NotApplicableTheorem ->
+            try_choices tl) in
+ try_choices choices;;
+
+let auto_tac mqi_handle ~status:(proof,goal) = 
+  prerr_endline "Entro in Auto";
+  try 
+    let res = auto_tac mqi_handle depth proof goal in
+prerr_endline "AUTO_TAC HA FINITO";
+    res
+  with 
+  | MaxDepth -> assert false (* this should happens only if depth is 0 above *)
+  | NotApplicableTheorem -> 
+      prerr_endline("No applicable theorem");
+      raise (ProofEngineTypes.Fail "No Applicable theorem");;
 
 (* TODO se ce n'e' piu' di una, prende la prima che trova... sarebbe meglio
 chiedere: find dovrebbe restituire una lista di hyp (?) da passare all'utonto con una
@@ -59,7 +131,7 @@ e li aggiunga nel context, poi si conta la lunghezza di questo nuovo
 contesto e si lifta di tot... COSA SIGNIFICA TUTTO CIO'?????? *)
 
 let generalize_tac
- ?(mk_fresh_name_callback = ProofEngineHelpers.mk_fresh_name)
+ ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name)
  terms ~status:((proof,goal) as status)
 =
   let module C = Cic in
@@ -83,7 +155,7 @@ let generalize_tac
       ~start:
         (P.cut_tac 
          (C.Prod(
-           (mk_fresh_name_callback context C.Anonymous typ), 
+           (mk_fresh_name_callback metasenv context C.Anonymous typ), 
            typ,
            (ProofEngineReduction.replace_lifting_csc 1
              ~equality:(==)