Injection now clears all intermediate results introduced.

[helm.git] / components / tactics / primitiveTactics.ml

diff --git a/components/tactics/primitiveTactics.ml b/components/tactics/primitiveTactics.ml
index 7a732a57257304dd89835b7e31aac819f047bea2..192460633d7577ff26a18e40d2d8ac4e8f699651 100644 (file)
--- a/components/tactics/primitiveTactics.ml
+++ b/components/tactics/primitiveTactics.ml
@@ -419,8 +419,17 @@ let letin_tac ?(mk_fresh_name_callback=FreshNamesGenerator.mk_fresh_name ~subst:
  =
   let module C = Cic in
    let curi,metasenv,pbo,pty = proof in
+   (* occur check *)
+   let occur i t =
+     let m = CicUtil.metas_of_term t in 
+     List.exists (fun (j,_) -> i=j) m
+   in
    let metano,context,ty = CicUtil.lookup_meta goal metasenv in
-    let _,_ = (* TASSI: FIXME *)
+   if occur metano term then
+     raise 
+       (ProofEngineTypes.Fail (lazy
+         "You can't letin a term containing the current goal"));
+    let _,_ =
       CicTypeChecker.type_of_aux' metasenv context term CicUniv.empty_ugraph in
      let newmeta = new_meta_of_proof ~proof in
      let fresh_name =
@@ -472,6 +481,7 @@ let elim_tac ~term =
    let (curi,metasenv,proofbo,proofty) = proof in
    let metano,context,ty = CicUtil.lookup_meta goal metasenv in
     let termty,_ = T.type_of_aux' metasenv context term CicUniv.empty_ugraph in
+    let termty = CicReduction.whd context termty in
     let (termty,metasenv',arguments,fresh_meta) =
      ProofEngineHelpers.saturate_term
       (ProofEngineHelpers.new_meta_of_proof proof) metasenv context termty 0 in
@@ -565,3 +575,24 @@ let elim_intros_simpl_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fres
        [ReductionTactics.simpl_tac
          ~pattern:(ProofEngineTypes.conclusion_pattern None)])
 ;;
+
+(* FG: insetrts a "hole" in the context (derived from letin_tac) *)
+
+module C = Cic
+
+let letout_tac =
+   let mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[] in
+   let term = C.Sort C.Set in
+   let letout_tac (proof, goal) =
+      let curi, metasenv, pbo, pty = proof in
+      let metano, context, ty = CicUtil.lookup_meta goal metasenv in
+      let newmeta = new_meta_of_proof ~proof in
+      let fresh_name = mk_fresh_name_callback metasenv context (Cic.Name "hole") ~typ:term in
+      let context_for_newmeta = None :: context in
+      let irl = CicMkImplicit.identity_relocation_list_for_metavariable context_for_newmeta in
+      let newmetaty = CicSubstitution.lift 1 ty in
+      let bo' = C.LetIn (fresh_name, term, C.Meta (newmeta,irl)) in
+      let newproof, _ = subst_meta_in_proof proof metano bo'[newmeta,context_for_newmeta,newmetaty] in
+      newproof, [newmeta]
+   in
+   mk_tactic letout_tac