parameter sintax added to axiom statement

[helm.git] / helm / software / components / tactics / fwdSimplTactic.ml

diff --git a/helm/software/components/tactics/fwdSimplTactic.ml b/helm/software/components/tactics/fwdSimplTactic.ml
index 5d78a4ed6949ef4fc57567a2aff7ab8400587fcc..10df83c5db482f34dfe30dbd734dee126ca67245 100644 (file)
--- a/helm/software/components/tactics/fwdSimplTactic.ml
+++ b/helm/software/components/tactics/fwdSimplTactic.ml
@@ -35,6 +35,7 @@ module T = Tacticals
 module FNG = FreshNamesGenerator
 module MI = CicMkImplicit
 module PESR = ProofEngineStructuralRules
+module HEL = HExtlib
 
 let fail_msg0 = "unexported clearbody: invalid argument"
 let fail_msg2 = "fwd: no applicable simplification"
@@ -46,7 +47,7 @@ let error msg = raise (PET.Fail (lazy msg))
 let id_tac = 
    let id_tac (proof,goal) = 
       try
-         let _, metasenv, _, _ = proof in
+         let _, metasenv, _subst, _, _, _ = proof in
          let _, _, _ = CicUtil.lookup_meta goal metasenv in
          (proof,[goal])
       with CicUtil.Meta_not_found _ -> (proof, [])
@@ -61,7 +62,7 @@ let clearbody ~index =
    in
    let clearbody status =
       let (proof, goal) = status in
-      let _, metasenv, _, _ = proof in
+      let _, metasenv, _subst, _, _, _ = proof in
       let _, context, _ = CicUtil.lookup_meta goal metasenv in
       PET.apply_tactic (PESR.clearbody ~hyp:(find_name index context)) status
    in
@@ -95,23 +96,32 @@ let strip_prods metasenv context ?how_many to_what term =
       | _, t                                  -> metasenv, metas, conts 
    in
    aux metasenv [] [] to_what (how_many, term)
-   
-let lapply_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[]) 
+
+let get_clearables context terms =
+   let aux = function
+      | Cic.Rel i 
+      | Cic.Appl (Cic.Rel i :: _) -> PEH.get_name context i
+      | _                         -> None
+   in
+   HEL.list_rev_map_filter aux terms 
+
+let lapply_tac_aux ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[]) 
                (* ?(substs = []) *) ?how_many ?(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 xuri, metasenv, _subst, u, t, attrs = 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, _ = TC.type_of_aux' metasenv context what U.oblivion_ugraph in
       let lemma = FNG.clean_dummy_dependent_types lemma in
-      let metasenv, metas, conts = strip_prods metasenv context ?how_many to_what lemma in      
+      let metasenv, metas, conts = strip_prods metasenv context ?how_many to_what lemma in
       let conclusion =  
          match metas with [] -> what | _ -> Cic.Appl (what :: List.rev metas)
       in
-      let tac = T.then_ ~start:(letin_tac conclusion) 
-        ~continuation:(clearbody ~index:1)
+      let tac =
+        T.then_ ~start:(letin_tac conclusion) 
+                 ~continuation:(clearbody ~index:1)     
       in
-      let proof = (xuri, metasenv, u, t) in
+      let proof = (xuri, metasenv, _subst, u, t, attrs) in
       let aux (proof, goals) (tac, goal) = 
          let proof, new_goals = PET.apply_tactic tac (proof, goal) in
         proof, goals @ new_goals
@@ -119,7 +129,26 @@ let lapply_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~sub
       List.fold_left aux (proof, []) ((tac, goal) :: conts)
    in
    PET.mk_tactic lapply_tac
-        
+
+let lapply_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[]) 
+               (* ?(substs = []) *) ?(linear = false) ?how_many ?(to_what = []) what =
+   let lapply_tac status =
+      let proof, goal = status in
+      let _, metasenv, _subst, _, _, _ = proof in
+      let _, context, _ = CicUtil.lookup_meta goal metasenv in
+      let lapply = lapply_tac_aux ~mk_fresh_name_callback ?how_many ~to_what what in
+      let tac =  
+         if linear then 
+            let hyps = get_clearables context (what :: to_what) in
+           T.then_ ~start:lapply
+                   ~continuation:(PESR.clear ~hyps) (* T.try_tactic ~tactic: *)
+        else 
+           lapply    
+        in
+        PET.apply_tactic tac status
+   in
+   PET.mk_tactic lapply_tac
+
 (* fwd **********************************************************************)
 
 let fwd_simpl_tac
@@ -130,7 +159,7 @@ let fwd_simpl_tac
    in
    let fwd_simpl_tac status =
       let (proof, goal) = status in
-      let _, metasenv, _, _ = proof in
+      let _, metasenv, _subst, _, _, _ = proof in
       let _, context, ty = CicUtil.lookup_meta goal metasenv in
       let index, major = PEH.lookup_type metasenv context hyp in 
       match FwdQueries.fwd_simpl ~dbd major with