added a missing <br> tag

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

diff --git a/helm/ocaml/tactics/variousTactics.ml b/helm/ocaml/tactics/variousTactics.ml
index 395768db96088a65abb4b63fed6bb5650d665095..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
@@ -33,7 +105,7 @@ let assumption_tac ~status:((proof,goal) as status) =
   let module R = CicReduction in
   let module S = CicSubstitution in
    let _,metasenv,_,_ = proof in
-    let _,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
+    let _,context,ty = CicUtil.lookup_meta goal metasenv in
      let rec find n = function 
         hd::tl -> 
          (match hd with
@@ -59,14 +131,14 @@ 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
   let module P = PrimitiveTactics in
   let module T = Tacticals in
    let _,metasenv,_,_ = proof in
-   let _,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
+   let _,context,ty = CicUtil.lookup_meta goal metasenv in
     let typ =
      match terms with
         [] -> assert false
@@ -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:(==)