From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Wed, 29 Jun 2005 15:00:26 +0000 (+0000)
Subject: lapply reimplemented using letin_tac
X-Git-Tag: INDEXING_NO_PROOFS~2
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=f1d49aeeb0ddcc3773a393ebef57c9cfa1e87f8e;p=helm.git

lapply reimplemented using letin_tac
---

diff --git a/helm/ocaml/tactics/fwdSimplTactic.ml b/helm/ocaml/tactics/fwdSimplTactic.ml
index 5160ea929..ded28cc18 100644
--- 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 =