first working (?) version of lapply

[helm.git] / helm / ocaml / tactics / fwdSimplTactic.ml

diff --git a/helm/ocaml/tactics/fwdSimplTactic.ml b/helm/ocaml/tactics/fwdSimplTactic.ml
index c1a5347f42d034a157a7e7aec3852b631a0a031f..fb9c0481796953d8e402eb5214510457dfa9d4b0 100644 (file)
--- a/helm/ocaml/tactics/fwdSimplTactic.ml
+++ b/helm/ocaml/tactics/fwdSimplTactic.ml
@@ -26,62 +26,74 @@
 module MI = CicMkImplicit
 module TC = CicTypeChecker 
 module PET = ProofEngineTypes 
+module PEH = ProofEngineHelpers 
 module U  = CicUniv
 module S = CicSubstitution
 module PT = PrimitiveTactics
+module T = Tacticals
 
-(*
-let module R = CicReduction
-*)
-
-let fail_msg0 = "not a declaration of the current context"
 let fail_msg1 = "no applicable simplification"
 
 let error msg = raise (PET.Fail msg)
 
-let rec declaration name = function 
-   | []                                           -> error fail_msg0
-   | Some (hyp, Cic.Decl ty) :: _ when hyp = name -> ty
-   | _ :: tail                                    -> declaration name tail 
-
 (* lapply *******************************************************************)
 
-let lapply_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[])
-               ?(substs = []) 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 = []) *) ?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 update_metasenv metasenv ((xuri, _, u,t), goal) =
-      ((xuri, metasenv, u,t), goal)
+   let rec mk_continuations p l =
+      if p <= 0 then l else mk_continuations (pred p) (T.id_tac :: l)
    in
-   let lapply_tac status =
-      let (proof, goal) = status in
-      let _,metasenv,_,_ = proof in
-      let _,context,ty = CicUtil.lookup_meta goal metasenv 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 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      
-      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 ~hyp ~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 = declaration hyp context 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 uri; (proof, [])  
+         | uri :: _ -> prerr_endline (UriManager.string_of_uri uri); (proof, [])  
    in
    PET.mk_tactic fwd_simpl_tac