X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2FfwdSimplTactic.ml;h=fb9c0481796953d8e402eb5214510457dfa9d4b0;hb=8c5a76439368f52a7df7c7b524c726b1f9d4eb39;hp=918ecd60597e1ebfff35fe5b1704b2c5d3e9d824;hpb=98c386d8d12a2fe4d64017e0b1bf684b22fe6423;p=helm.git

diff --git a/helm/ocaml/tactics/fwdSimplTactic.ml b/helm/ocaml/tactics/fwdSimplTactic.ml
index 918ecd605..fb9c04817 100644
--- 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,61 +39,51 @@ let error msg = raise (PET.Fail msg)
 (* lapply *******************************************************************)
 
 let lapply_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[]) 
-               (* ?(substs = []) *) what =
-   let count_dependent_prods context t =
-      let rec aux context p = function
-         | Cic.Prod (name, t1, t2) -> 
-            if TC.does_not_occur context 0 1 t2 then p else 
-            let e = Some (name, Cic.Decl t1) in
-	    aux (e :: context) (succ p) t2
-         | t                       -> p
+               (* ?(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 context 0 t
+      aux metasenv 0 context t
    in
-   let rec pad_context p context add_context =
-      if List.length add_context >= p then add_context @ context
-      else pad_context p context (None :: add_context)
-   in
-   let strip_dependent_prods metasenv context p t =
-      let rec aux metasenv add_context q = function
-         | Cic.Prod (name, t1, t2) when q > 0 ->
-	    let context_for_meta = pad_context p context add_context in
-	    let metasenv, index = MI.mk_implicit metasenv [] context_for_meta in
-	    let rs = MI.identity_relocation_list_for_metavariable context_for_meta in
-            let e, s = Some (name, Cic.Decl t1), Cic.Meta (index, rs) in    
-	    aux metasenv (e :: add_context) (pred q) (S.subst s t2)
-         | t                                  -> metasenv, add_context, t
-      in
-      aux metasenv [] p t
-   in
-   let mk_body bo = function
-      | Some (name, Cic.Decl t1) -> Cic.Lambda (name, t1, bo)
-      | _                        -> failwith "mk_body"
+   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
-(* preliminaries *)      
-      let metano, context, ty = CicUtil.lookup_meta goal metasenv in
+      let _, context, _ = CicUtil.lookup_meta goal metasenv in
       let lemma, _ = TC.type_of_aux' metasenv context what U.empty_ugraph in
-      let p = count_dependent_prods context lemma in
-(* stripping *)
-      let metasenv, add_context, holed_lemma = strip_dependent_prods metasenv context p lemma in
-      let proof = xuri, metasenv, u, t in
-      let newmeta = MI.new_meta metasenv [] in
-      let context = add_context @ context in      
-      let irl = MI.identity_relocation_list_for_metavariable context in      
-      let bo = List.fold_left mk_body (Cic.Meta (newmeta, irl)) add_context in
-      let ty = S.lift p ty in
-      let (xuri, metasenv, u, t), _ = 
-         PEH.subst_meta_in_proof proof metano bo [newmeta, context, ty]
-      in
-      prerr_endline (CicPp.ppterm holed_lemma);
-(* cut *)
-      let status = (xuri, metasenv, u, t), newmeta in
-      PET.apply_tactic (PT.cut_tac ~mk_fresh_name_callback holed_lemma) status
+      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
-
+   
 (* fwd **********************************************************************)
 
 let fwd_simpl_tac ~what ~dbd =