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

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