X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2FprimitiveTactics.ml;h=16cff94d7796493f52a05658332a8261f564be4f;hb=7278063faf0ebb5fd08af2191989a12e2a27f522;hp=7a732a57257304dd89835b7e31aac819f047bea2;hpb=55b82bd235d82ff7f0a40d980effe1efde1f5073;p=helm.git

diff --git a/helm/software/components/tactics/primitiveTactics.ml b/helm/software/components/tactics/primitiveTactics.ml
index 7a732a572..16cff94d7 100644
--- a/helm/software/components/tactics/primitiveTactics.ml
+++ b/helm/software/components/tactics/primitiveTactics.ml
@@ -25,7 +25,6 @@
 
 (* $Id$ *)
 
-open ProofEngineHelpers
 open ProofEngineTypes
 
 exception TheTypeOfTheCurrentGoalIsAMetaICannotChooseTheRightElimiantionPrinciple
@@ -232,7 +231,8 @@ let
 
 let new_metasenv_and_unify_and_t newmeta' metasenv' context term' ty termty goal_arity =
   let (consthead,newmetasenv,arguments,_) =
-   saturate_term newmeta' metasenv' context termty goal_arity in
+   ProofEngineHelpers.saturate_term newmeta' metasenv' context termty
+    goal_arity in
   let subst,newmetasenv',_ = 
    CicUnification.fo_unif newmetasenv context consthead ty CicUniv.empty_ugraph
   in
@@ -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 ~maxmeta (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 = max (CicMkImplicit.new_meta metasenv subst) maxmeta in
    let exp_named_subst_diff,newmeta',newmetasenvfragment,term' =
     match term with
        C.Var (uri,exp_named_subst) ->
@@ -318,18 +318,20 @@ let apply_tac_verbose_with_subst ~term (proof, goal) =
      CicMetaSubst.apply_subst ((metano,(context,bo',Cic.Implicit None))::subst)
    in
    let (newproof, newmetasenv''') = 
-     subst_meta_and_metasenv_in_proof proof metano subst_in newmetasenv''
+    ProofEngineHelpers.subst_meta_and_metasenv_in_proof proof metano subst_in
+     newmetasenv''
    in
-   (((metano,(context,bo',Cic.Implicit None))::subst)(* subst_in *), (* ALB *)
-    (newproof, 
-     List.map (function (i,_,_) -> i) new_uninstantiatedmetas))
+   let subst = ((metano,(context,bo',Cic.Implicit None))::subst) in
+   subst,
+   (newproof, List.map (function (i,_,_) -> i) new_uninstantiatedmetas),
+   max maxmeta (CicMkImplicit.new_meta newmetasenv''' subst)
 
 
 (* ALB *)
-let apply_tac_verbose_with_subst ~term status =
+let apply_with_subst ~term ?(subst=[]) ?(maxmeta=0) status =
   try
 (*     apply_tac_verbose ~term status *)
-    apply_tac_verbose_with_subst ~term status
+    apply_with_subst ~term ~subst ~maxmeta status
       (* TODO cacciare anche altre eccezioni? *)
   with 
   | CicUnification.UnificationFailure msg
@@ -338,7 +340,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)
@@ -366,12 +368,13 @@ let intros_tac ?howmany ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_
   let module R = CicReduction 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 = ProofEngineHelpers.new_meta_of_proof ~proof in
      let (context',ty',bo') =
       lambda_abstract ?howmany metasenv context newmeta ty mk_fresh_name_callback
      in
       let (newproof, _) =
-        subst_meta_in_proof proof metano bo' [newmeta,context',ty']
+       ProofEngineHelpers.subst_meta_in_proof proof metano bo'
+        [newmeta,context',ty']
       in
        (newproof, [newmeta])
  in
@@ -385,7 +388,7 @@ let cut_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:
   let module C = Cic in
    let curi,metasenv,pbo,pty = proof in
    let metano,context,ty = CicUtil.lookup_meta goal metasenv in
-    let newmeta1 = new_meta_of_proof ~proof in
+    let newmeta1 = ProofEngineHelpers.new_meta_of_proof ~proof in
     let newmeta2 = newmeta1 + 1 in
     let fresh_name =
      mk_fresh_name_callback metasenv context (Cic.Name "Hcut") ~typ:term in
@@ -405,7 +408,7 @@ let cut_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:
         C.Meta (newmeta2,irl2)]
      in
       let (newproof, _) =
-       subst_meta_in_proof proof metano bo'
+       ProofEngineHelpers.subst_meta_in_proof proof metano bo'
         [newmeta2,context,term; newmeta1,context_for_newmeta1,newmeta1ty];
       in
        (newproof, [newmeta1 ; newmeta2])
@@ -419,10 +422,19 @@ 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 newmeta = ProofEngineHelpers.new_meta_of_proof ~proof in
      let fresh_name =
       mk_fresh_name_callback metasenv context (Cic.Name "Hletin") ~typ:term in
      let context_for_newmeta =
@@ -434,7 +446,7 @@ let letin_tac ?(mk_fresh_name_callback=FreshNamesGenerator.mk_fresh_name ~subst:
       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
+         ProofEngineHelpers.subst_meta_in_proof
            proof metano bo'[newmeta,context_for_newmeta,newmetaty]
        in
         (newproof, [newmeta])
@@ -454,7 +466,7 @@ let exact_tac ~term =
   if b then
    begin
     let (newproof, metasenv') =
-      subst_meta_in_proof proof metano term [] in
+      ProofEngineHelpers.subst_meta_in_proof proof metano term [] in
     (newproof, [])
    end
   else
@@ -472,6 +484,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 +578,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 = ProofEngineHelpers.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, _ = ProofEngineHelpers.subst_meta_in_proof proof metano bo'[newmeta,context_for_newmeta,newmetaty] in
+      newproof, [newmeta]
+   in
+   mk_tactic letout_tac