First implementation of the Auto tactic.

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

diff --git a/helm/ocaml/tactics/variousTactics.ml b/helm/ocaml/tactics/variousTactics.ml
index 64b9ff790618c6305938d685229ecbb73c6801be..70952d84d5157d2d6a73f1aec8b89165261824f4 100644 (file)
--- 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