firs wrking (?) version of lapply

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

diff --git a/helm/ocaml/tactics/fwdSimplTactic.ml b/helm/ocaml/tactics/fwdSimplTactic.ml
index 918ecd60597e1ebfff35fe5b1704b2c5d3e9d824..d75a7c5f8a7bb1ec624415677d6268b3774e1140 100644 (file)
--- a/helm/ocaml/tactics/fwdSimplTactic.ml
+++ b/helm/ocaml/tactics/fwdSimplTactic.ml
@@ -30,6 +30,7 @@ module PEH = ProofEngineHelpers
 module U  = CicUniv
 module S = CicSubstitution
 module PT = PrimitiveTactics
+module T = Tacticals
 
 let fail_msg1 = "no applicable simplification"
 
@@ -38,7 +39,60 @@ let error msg = raise (PET.Fail msg)
 (* lapply *******************************************************************)
 
 let lapply_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[]) 
-               (* ?(substs = []) *) what =
+               (* ?(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)
+   in
+   let lapply_tac (proof, goal) =
+      let xuri, metasenv, u, t = proof in
+      let _, context, _ = CicUtil.lookup_meta goal metasenv in
+      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 
+           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
+         | metasenv, p, None, conclusion         ->
+           failwith "lapply_tac: not implemented"
+   in
+   PET.mk_tactic lapply_tac
+   
+   
+   
+   
+   
+   
+   
+   
+   
+(*   
    let count_dependent_prods context t =
       let rec aux context p = function
          | Cic.Prod (name, t1, t2) -> 
@@ -92,7 +146,7 @@ let lapply_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~sub
       PET.apply_tactic (PT.cut_tac ~mk_fresh_name_callback holed_lemma) status
    in
    PET.mk_tactic lapply_tac
-
+*)
 (* fwd **********************************************************************)
 
 let fwd_simpl_tac ~what ~dbd =