got rid of ~status label so that tactics can now be applied partially,

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

diff --git a/helm/ocaml/tactics/variousTactics.ml b/helm/ocaml/tactics/variousTactics.ml
index 395768db96088a65abb4b63fed6bb5650d665095..98c13e80b8b742b775df418788b1eaa215fc17e1 100644 (file)
--- a/helm/ocaml/tactics/variousTactics.ml
+++ b/helm/ocaml/tactics/variousTactics.ml
@@ -23,17 +23,100 @@
  * http://cs.unibo.it/helm/.
  *)
 
+let search_theorems_in_context status =
+  let (proof, goal) = status in
+  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 (proof,goal))@ 
+    (TacticChaser.searchTheorems mqi_handle (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 goal ->
+              (* It may happen that to close the first open goal
+                 also some other goals are closed *)
+              let _,metasenv,_,_ = proof in
+               if List.exists (fun (i,_,_) -> i = goal) metasenv then
+                let newproof =
+                 auto_tac mqi_handle (level-1) proof goal
+                in
+                 newproof
+               else
+                (* goal already closed *)
+                proof)
+          proof goallist
+        with 
+       | MaxDepth
+        | NotApplicableTheorem ->
+            try_choices tl) in
+ try_choices choices;;
+
+let auto_tac mqi_handle (proof,goal) =
+  prerr_endline "Entro in Auto";
+  try 
+    let proof = auto_tac mqi_handle depth proof goal in
+prerr_endline "AUTO_TAC HA FINITO";
+    (proof,[])
+  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
 funzione di callback che restituisce la (sola) hyp da applicare *)
 
-let assumption_tac ~status:((proof,goal) as status) =
+let assumption_tac status =
+  let (proof, goal) = status in
   let module C = Cic in
   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
@@ -47,7 +130,7 @@ let assumption_tac ~status:((proof,goal) as status) =
            | _ -> find (n+1) tl
          )
       | [] -> raise (ProofEngineTypes.Fail "Assumption: No such assumption")
-     in PrimitiveTactics.apply_tac ~status ~term:(C.Rel (find 1 context))
+     in PrimitiveTactics.apply_tac status ~term:(C.Rel (find 1 context))
 ;;
 
 (* ANCORA DA DEBUGGARE *)
@@ -59,14 +142,15 @@ 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)
- terms ~status:((proof,goal) as status)
+ ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name)
+ terms status
 =
+  let (proof, goal) = status in
   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 +167,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:(==) 
@@ -92,7 +176,7 @@ let generalize_tac
              ~where:ty)
          )))
       ~continuations: [(P.apply_tac ~term:(C.Rel 1)) ; T.id_tac]
-      ~status
+      status
 ;;