lapply improved

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

diff --git a/helm/ocaml/tactics/fwdSimplTactic.ml b/helm/ocaml/tactics/fwdSimplTactic.ml
index fb9c0481796953d8e402eb5214510457dfa9d4b0..5160ea929c678e967d7abd872828546c0f2eb5f7 100644 (file)
--- a/helm/ocaml/tactics/fwdSimplTactic.ml
+++ b/helm/ocaml/tactics/fwdSimplTactic.ml
@@ -38,25 +38,69 @@ let error msg = raise (PET.Fail msg)
 
 (* lapply *******************************************************************)
 
+let strip_dependent_prods metasenv context t =
+   let irl = MI.identity_relocation_list_for_metavariable context in
+   let rec aux metasenv p xcontext = function
+      | Cic.Prod (name, t1, t2) when not (TC.does_not_occur xcontext 0 1 t2) ->  
+         let index = MI.new_meta metasenv [] in
+         let metasenv = [index, context, t1] @ metasenv in
+         let e, s = Some (name, Cic.Decl t1), Cic.Meta (index, irl) in    
+        aux metasenv (succ p) (e :: xcontext) (S.subst s t2)
+      | Cic.Prod (name, t1, t2) -> metasenv, p, Some t1, (S.subst (Cic.Rel 1) t2)
+      | t                       -> metasenv, p, None, t 
+   in
+   aux metasenv 0 context t
+
+let skip_metas p =
+   let rec aux conts p =
+      if p <= 0 then conts else aux (T.id_tac :: conts) (pred p) 
+   in
+   aux [] p
+   
+let get_conclusion context t =
+   let rec aux p context = function 
+      | Cic.Prod (name, t1, t2)  -> 
+         aux (succ p) (Some (name, Cic.Decl t1) :: context) t2
+      | Cic.LetIn (name, u1, t2) -> 
+         aux (succ p) (Some (name, Cic.Def (u1, None)) :: context) t2
+     | Cic.Cast (t2, t1)         -> aux p context t2
+     | t                         -> p, context, t
+   in aux 0 context t
+
+let get_conclusion_dependences context t =
+   let p, context, conclusion = get_conclusion context t in
+   let rec aux l q = 
+      if q <= 0 then l else 
+      let b = TC.does_not_occur context (pred q) q conclusion in
+      aux (b :: l) (pred q)
+   in
+   aux [] p
+
+let solve_independents ?with_what deps =
+  let rec aux p conts = function
+     | []          -> p, conts
+     | true :: tl  -> 
+        let cont = PT.apply_tac ~term:(Cic.Rel (succ p)) in
+       aux (succ p) (cont :: conts) tl
+     | false :: tl -> aux (succ p) conts tl
+   in 
+   let p, conts = aux 0 [] deps in
+   match with_what with
+      | None   -> conts
+      | Some t -> PT.apply_tac ~term:(S.lift p t) :: conts
+        
 let lapply_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[]) 
                (* ?(substs = []) *) ?to_what what =
    let cut_tac term = PT.cut_tac ~mk_fresh_name_callback term in
-   let apply_tac term = PT.apply_tac term in
-   let strip_dependent_prods metasenv context t =
-      let irl = MI.identity_relocation_list_for_metavariable context in
-      let rec aux metasenv p xcontext = function
-         | Cic.Prod (name, t1, t2) when not (TC.does_not_occur xcontext 0 1 t2) ->  
-            let index = MI.new_meta metasenv [] in
-            let metasenv = [index, context, t1] @ metasenv in
-            let e, s = Some (name, Cic.Decl t1), Cic.Meta (index, irl) in    
-           aux metasenv (succ p) (e :: xcontext) (S.subst s t2)
-         | Cic.Prod (name, t1, t2) -> metasenv, p, Some t1, t2
-         | t                       -> metasenv, p, None, t 
-      in
-      aux metasenv 0 context t
-   in
-   let rec mk_continuations p l =
-      if p <= 0 then l else mk_continuations (pred p) (T.id_tac :: l)
+   let intros_tac () = PT.intros_tac ~mk_fresh_name_callback () in
+   let solve_conclusion_tac ?with_what p deps = 
+      T.then_ ~start:(intros_tac ())
+             ~continuation:(  
+         T.thens ~start:(PT.apply_tac what)
+                ~continuations:( 
+           skip_metas p @ solve_independents ?with_what deps 
+        )
+      )
    in
    let lapply_tac (proof, goal) =
       let xuri, metasenv, u, t = proof in
@@ -64,21 +108,23 @@ let lapply_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~sub
       let lemma, _ = TC.type_of_aux' metasenv context what U.empty_ugraph in
       match strip_dependent_prods metasenv context lemma with
          | metasenv, p, Some premise, conclusion ->
-           let premise_tac = 
-              match to_what with
-                 | None      -> T.id_tac 
-                 | Some term -> PT.apply_tac term 
+           let deps = get_conclusion_dependences context conclusion in
+           let inner_tac = match to_what with
+              | None      -> 
+                 T.thens ~start:(cut_tac premise)
+                         ~continuations:[
+                     solve_conclusion_tac ~with_what:(Cic.Rel 1) p deps;
+                    T.id_tac
+                 ]
+              | Some with_what -> 
+                  solve_conclusion_tac ~with_what p deps
+           in      
+           let outer_tac =
+              T.thens ~start:(cut_tac conclusion)
+                      ~continuations:[T.id_tac; inner_tac]
            in
            let status = (xuri, metasenv, u, t), goal in
-            let tac = T.thens ~start:(cut_tac premise)
-                             ~continuations:[  
-                     T.thens ~start:(cut_tac conclusion)
-                             ~continuations:[ T.id_tac; 
-                     T.thens ~start:(PT.apply_tac what)
-                             ~continuations:(mk_continuations p [PT.apply_tac ~term:(Cic.Rel 1)])
-                                            ]; premise_tac ]
-           in
-           PET.apply_tactic tac status
+           PET.apply_tactic outer_tac status
          | metasenv, p, None, conclusion         ->
            failwith "lapply_tac: not implemented"
    in