lapply tactic continued

diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml
index 522a5157053161e990ebdef8172cef7070e2b5a7..37143ea236603d76f31ff37072786797a758e1b7 100644 (file)
--- a/helm/matita/matitaEngine.ml
+++ b/helm/matita/matitaEngine.ml
@@ -78,7 +78,7 @@ let tactic_of_ast = function
       else
         EqualityTactics.rewrite_back_tac ~where:pattern ~term:t ()
   | TacticAst.FwdSimpl (_, term) -> 
-     Tactics.fwd_simpl ~term ~dbd:(MatitaDb.instance ())
+     Tactics.fwd_simpl ~what:term ~dbd:(MatitaDb.instance ())
   | TacticAst.LApply (_, term) ->
      let f (name, term) = Cic.Name name, term in
      Tactics.lapply term

diff --git a/helm/ocaml/tactics/fwdSimplTactic.ml b/helm/ocaml/tactics/fwdSimplTactic.ml
index 98125f5e738d447986bdb88f74aed4825ef646e6..918ecd60597e1ebfff35fe5b1704b2c5d3e9d824 100644 (file)
--- a/helm/ocaml/tactics/fwdSimplTactic.ml
+++ b/helm/ocaml/tactics/fwdSimplTactic.ml
@@ -26,6 +26,7 @@
 module MI = CicMkImplicit
 module TC = CicTypeChecker 
 module PET = ProofEngineTypes 
+module PEH = ProofEngineHelpers 
 module U  = CicUniv
 module S = CicSubstitution
 module PT = PrimitiveTactics
@@ -36,42 +37,71 @@ let error msg = raise (PET.Fail msg)
 
 (* lapply *******************************************************************)
 
-let lapply_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[]) what =
-   let rec strip_dependent_prods metasenv context ss = function
-      | Cic.Prod (name, t1, t2) as t -> 
-        if TC.does_not_occur context 0 1 t2 then metasenv, ss, t else 
-       let metasenv, index = MI.mk_implicit metasenv [] context in 
-       let rs = MI.identity_relocation_list_for_metavariable context in
-        let e, s = Some (name, Cic.Decl t1), Some (Cic.Meta (index, rs)) in
-       strip_dependent_prods metasenv (e :: context) (s :: ss) t2
-      | t    -> metasenv, ss, t
+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
+      in
+      aux context 0 t
    in
-   let update_metasenv metasenv ((xuri, _, u,t), goal) =
-      ((xuri, metasenv, u,t), goal)
+   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 lapply_tac status =
-      let (proof, goal) = status in
-      let _,metasenv,_,_ = proof in
-      let _,context,ty = CicUtil.lookup_meta goal metasenv 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"
+   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 lemma, _ = TC.type_of_aux' metasenv context what U.empty_ugraph in
-      let metasenv, substs, stripped_lemma = strip_dependent_prods metasenv context [] lemma in
-      let status = update_metasenv metasenv status in
-      let holed_lemma = S.subst_meta substs stripped_lemma 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
    in
    PET.mk_tactic lapply_tac
 
 (* fwd **********************************************************************)
 
-let fwd_simpl_tac ~term ~dbd =
+let fwd_simpl_tac ~what ~dbd =
    let fwd_simpl_tac status =
       let (proof, goal) = status in
-      let _,metasenv,_,_ = proof in
-      let _,context,ty = CicUtil.lookup_meta goal metasenv in
-      let major,_ =
-       CicTypeChecker.type_of_aux' metasenv context term CicUniv.empty_ugraph
-      in 
-      match  MetadataQuery.fwd_simpl ~dbd major with
+      let _, metasenv, _, _ = proof in
+      let _, context, ty = CicUtil.lookup_meta goal metasenv in
+      let major, _ = TC.type_of_aux' metasenv context what U.empty_ugraph in 
+      match MetadataQuery.fwd_simpl ~dbd major with
          | []       -> error fail_msg1
          | uri :: _ -> prerr_endline (UriManager.string_of_uri uri); (proof, [])  
    in

diff --git a/helm/ocaml/tactics/fwdSimplTactic.mli b/helm/ocaml/tactics/fwdSimplTactic.mli
index 705569fdca06a06dd93055714faa8dcf29317395..1c221ee010b7143e132ecd93b958ce03ee3ef2da 100644 (file)
--- a/helm/ocaml/tactics/fwdSimplTactic.mli
+++ b/helm/ocaml/tactics/fwdSimplTactic.mli
@@ -28,4 +28,4 @@ val lapply_tac:
    Cic.term -> ProofEngineTypes.tactic
 
 val fwd_simpl_tac:
-   term:Cic.term -> dbd:Mysql.dbd -> ProofEngineTypes.tactic
+   what:Cic.term -> dbd:Mysql.dbd -> ProofEngineTypes.tactic

diff --git a/helm/ocaml/tactics/tactics.mli b/helm/ocaml/tactics/tactics.mli
index cddc6d3b2bc7bacc761de5cf6e1993941979d11c..9e5a4ce47fa686bdb57de1918bde1c37dfde61db 100644 (file)
--- a/helm/ocaml/tactics/tactics.mli
+++ b/helm/ocaml/tactics/tactics.mli
@@ -32,7 +32,7 @@ val fold :
   reduction:(Cic.context -> Cic.term -> Cic.term) ->
   also_in_hypotheses:bool -> term:Cic.term -> ProofEngineTypes.tactic
 val fourier : ProofEngineTypes.tactic
-val fwd_simpl : term:Cic.term -> dbd:Mysql.dbd -> ProofEngineTypes.tactic
+val fwd_simpl : what:Cic.term -> dbd:Mysql.dbd -> ProofEngineTypes.tactic
 val generalize :
   ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->
   term:Cic.term -> ProofEngineTypes.pattern -> ProofEngineTypes.tactic