lapply reimplemented using letin_tac

diff --git a/helm/ocaml/tactics/fwdSimplTactic.ml b/helm/ocaml/tactics/fwdSimplTactic.ml
index 5160ea929c678e967d7abd872828546c0f2eb5f7..ded28cc18dce03a0a9e3c2f690f0da59ee5a88d6 100644 (file)
--- a/helm/ocaml/tactics/fwdSimplTactic.ml
+++ b/helm/ocaml/tactics/fwdSimplTactic.ml
@@ -31,6 +31,7 @@ module U  = CicUniv
 module S = CicSubstitution
 module PT = PrimitiveTactics
 module T = Tacticals
+module FNG = FreshNamesGenerator
 
 let fail_msg1 = "no applicable simplification"
 
@@ -40,16 +41,45 @@ let error msg = raise (PET.Fail msg)
 
 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 
+   let mk_meta metasenv  t =  
+      let index = MI.new_meta metasenv [] in
+      let metasenv = [index, context, t] @ metasenv in
+      metasenv, Cic.Meta (index, irl)
    in
-   aux metasenv 0 context t
+   let rec aux metasenv metas = function
+      | Cic.Prod (Cic.Name _ as name, t1, t2) ->  
+         let metasenv, meta = mk_meta metasenv t1 in    
+        aux metasenv (meta :: metas) (S.subst meta t2)
+      | Cic.Prod (Cic.Anonymous, t1, _)       -> 
+         let metasenv, meta = mk_meta metasenv t1 in    
+        metasenv, metas, Some meta  
+      | t                                     -> metasenv, metas, None 
+   in
+   aux metasenv [] t
+   
+let lapply_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[]) 
+               (* ?(substs = []) *) ?to_what what =
+   let letin_tac term = PT.letin_tac ~mk_fresh_name_callback term 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
+      let lemma = FNG.clean_dummy_dependent_types lemma in
+      match strip_dependent_prods metasenv context lemma with
+         | metasenv, metas, Some meta ->
+           let pippo =  Cic.Appl (what :: List.rev (meta :: metas)) in
+           Printf.eprintf "lapply: %s\n" (CicPp.ppterm pippo); flush stderr;
+           let outer_tac = letin_tac pippo in   
+           let status = (xuri, metasenv, u, t), goal in
+           PET.apply_tactic outer_tac status
+         | metasenv, metas, None      ->
+           failwith "lapply_tac: not implemented"
+   in
+   PET.mk_tactic lapply_tac
+        
+(* 
+
+   
 
 let skip_metas p =
    let rec aux conts p =
@@ -97,8 +127,8 @@ let lapply_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~sub
       T.then_ ~start:(intros_tac ())
              ~continuation:(  
          T.thens ~start:(PT.apply_tac what)
-                ~continuations:( 
-           skip_metas p @ solve_independents ?with_what deps 
+                ~continuations:( [ T.id_tac; T.id_tac; T.id_tac ]
+(*         skip_metas p @ solve_independents ?with_what deps *) 
         )
       )
    in
@@ -106,6 +136,7 @@ let lapply_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~sub
       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
+      let lemma = FNG.clean_dummy_dependent_types lemma in
       match strip_dependent_prods metasenv context lemma with
          | metasenv, p, Some premise, conclusion ->
            let deps = get_conclusion_dependences context conclusion in
@@ -121,15 +152,9 @@ let lapply_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~sub
            in      
            let outer_tac =
               T.thens ~start:(cut_tac conclusion)
-                      ~continuations:[T.id_tac; inner_tac]
+                      ~continuations:[T.id_tac; T.id_tac (* inner_tac *)]
            in
-           let status = (xuri, metasenv, u, t), goal in
-           PET.apply_tactic outer_tac status
-         | metasenv, p, None, conclusion         ->
-           failwith "lapply_tac: not implemented"
-   in
-   PET.mk_tactic lapply_tac
-   
+*)   
 (* fwd **********************************************************************)
 
 let fwd_simpl_tac ~what ~dbd =