apply now uses both menv and subst to decide the fresh meta number

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

diff --git a/helm/software/components/tactics/primitiveTactics.ml b/helm/software/components/tactics/primitiveTactics.ml
index 63c51d9efad86cfd359a1cd4dbc444a9d14bf9c7..e09f0a1f7dc890ecbee234b53042677fea3aab91 100644 (file)
--- a/helm/software/components/tactics/primitiveTactics.ml
+++ b/helm/software/components/tactics/primitiveTactics.ml
@@ -246,14 +246,14 @@ let rec count_prods context ty =
     Cic.Prod (n,s,t) -> 1 + count_prods (Some (n,Cic.Decl s)::context) t
   | _ -> 0
 
-let apply_tac_verbose_with_subst ~term (proof, goal) =
+let apply_with_subst ~term ~subst (proof, goal) =
   (* Assumption: The term "term" must be closed in the current context *)
  let module T = CicTypeChecker in
  let module R = CicReduction in
  let module C = Cic in
   let (_,metasenv,_,_) = proof in
   let metano,context,ty = CicUtil.lookup_meta goal metasenv in
-  let newmeta = new_meta_of_proof ~proof in
+  let newmeta = CicMkImplicit.new_meta metasenv subst in
    let exp_named_subst_diff,newmeta',newmetasenvfragment,term' =
     match term with
        C.Var (uri,exp_named_subst) ->
@@ -326,10 +326,10 @@ let apply_tac_verbose_with_subst ~term (proof, goal) =
 
 
 (* ALB *)
-let apply_tac_verbose_with_subst ~term status =
+let apply_with_subst ~term ?(subst=[]) status =
   try
 (*     apply_tac_verbose ~term status *)
-    apply_tac_verbose_with_subst ~term status
+    apply_with_subst ~term ~subst status
       (* TODO cacciare anche altre eccezioni? *)
   with 
   | CicUnification.UnificationFailure msg
@@ -338,7 +338,7 @@ let apply_tac_verbose_with_subst ~term status =
 
 (* ALB *)
 let apply_tac_verbose ~term status =
-  let subst, status = apply_tac_verbose_with_subst ~term status in
+  let subst, status = apply_with_subst ~term status in
   (CicMetaSubst.apply_subst subst), status
 
 let apply_tac ~term status = snd (apply_tac_verbose ~term status)
@@ -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 =
@@ -566,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