X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2FequalityTactics.ml;h=16aa6d3b2d5925a10b1ab3bf7e47583885365c2f;hb=04dc7b17e463fa9c75ac91e1df88bf37ed009914;hp=f284a2d1d145dbdb6d2c49c6885098ae19904e9c;hpb=e436c170ce2b9154d3e090c2140e8a0172f4a016;p=helm.git

diff --git a/helm/software/components/tactics/equalityTactics.ml b/helm/software/components/tactics/equalityTactics.ml
index f284a2d1d..16aa6d3b2 100644
--- a/helm/software/components/tactics/equalityTactics.ml
+++ b/helm/software/components/tactics/equalityTactics.ml
@@ -44,10 +44,8 @@ let rec rewrite_tac ~direction ~pattern:(wanted,hyps_pat,concl_pat) equality =
  let _rewrite_tac status =
   assert (wanted = None);   (* this should be checked syntactically *)
   let proof,goal = status in
-  let curi, metasenv, pbo, pty, attrs = proof in
+  let curi, metasenv, _subst, pbo, pty, attrs = proof in
   let (metano,context,gty) = CicUtil.lookup_meta goal metasenv in
-  let gsort,_ =
-   CicTypeChecker.type_of_aux' metasenv context gty CicUniv.oblivion_ugraph in
   match hyps_pat with
      he::(_::_ as tl) ->
        PET.apply_tactic
@@ -70,15 +68,7 @@ let rec rewrite_tac ~direction ~pattern:(wanted,hyps_pat,concl_pat) equality =
    match hyps_pat with
       [] -> None,true,(fun ~term _ -> P.exact_tac term),concl_pat,gty
     | [name,pat] ->
-      let rec find_hyp n =
-       function
-          [] -> assert false
-        | Some (Cic.Name s,Cic.Decl ty)::_ when name = s ->
-           Cic.Rel n, S.lift n ty
-        | Some (Cic.Name s,Cic.Def _)::_ when name = s -> assert false (*CSC: not implemented yet! But does this make any sense?*)
-        | _::tl -> find_hyp (n+1) tl
-      in
-       let arg,gty = find_hyp 1 context in
+       let arg,gty = ProofEngineHelpers.find_hyp name context in
        let dummy = "dummy" in
         Some arg,false,
          (fun ~term typ ->
@@ -97,6 +87,8 @@ let rec rewrite_tac ~direction ~pattern:(wanted,hyps_pat,concl_pat) equality =
          Some pat,gty
     | _::_ -> assert false
   in
+  let gsort,_ =
+   CicTypeChecker.type_of_aux' metasenv context gty CicUniv.oblivion_ugraph in
   let if_right_to_left do_not_change a b = 
     match direction with
     | `RightToLeft -> if do_not_change then a else b
@@ -104,7 +96,7 @@ let rec rewrite_tac ~direction ~pattern:(wanted,hyps_pat,concl_pat) equality =
   in
   let ty_eq,ugraph = 
     CicTypeChecker.type_of_aux' metasenv context equality 
-      CicUniv.empty_ugraph in 
+      CicUniv.oblivion_ugraph in 
   let (ty_eq,metasenv',arguments,fresh_meta) =
    TermUtil.saturate_term
     (ProofEngineHelpers.new_meta_of_proof proof) metasenv context ty_eq 0 in  
@@ -174,6 +166,8 @@ let rec rewrite_tac ~direction ~pattern:(wanted,hyps_pat,concl_pat) equality =
   let abstr_gty =
    ProofEngineReduction.replace_lifting_csc 0
     ~equality:(==) ~what ~with_what:with_what ~where:lifted_gty in
+  if lifted_gty = abstr_gty then 
+    raise (ProofEngineTypes.Fail (lazy "nothing to do"));
   let abstr_gty = CicMetaSubst.apply_subst subst abstr_gty in
   let pred = C.Lambda (fresh_name, ty, abstr_gty) in
   (* The argument is either a meta if we are rewriting in the conclusion
@@ -196,7 +190,7 @@ let rec rewrite_tac ~direction ~pattern:(wanted,hyps_pat,concl_pat) equality =
   try 
     let (proof',goals) =
       PET.apply_tactic 
-        (tac ~term:exact_proof newtyp) ((curi,metasenv',pbo,pty, attrs),goal)
+        (tac ~term:exact_proof newtyp) ((curi,metasenv',_subst,pbo,pty, attrs),goal)
     in
     let goals =
      goals@(ProofEngineHelpers.compare_metasenvs ~oldmetasenv:metasenv
@@ -204,8 +198,8 @@ let rec rewrite_tac ~direction ~pattern:(wanted,hyps_pat,concl_pat) equality =
     in
      (proof',goals)
   with (* FG: this should be PET.Fail _ *)
-     TC.TypeCheckerFailure _ -> 
-      let msg = lazy "rewrite: nothing to rewrite" in
+     TC.TypeCheckerFailure m -> 
+      let msg = lazy ("rewrite: "^ Lazy.force m) in
       raise (PET.Fail msg)
  in    
   PET.mk_tactic _rewrite_tac 
@@ -229,7 +223,7 @@ let replace_tac ~(pattern: ProofEngineTypes.lazy_pattern) ~with_what =
  let replace_tac ~(pattern: ProofEngineTypes.lazy_pattern) ~with_what status =
   let _wanted, hyps_pat, concl_pat = pattern in
   let (proof, goal) = status in
-  let uri,metasenv,pbo,pty, attrs = proof in
+  let uri,metasenv,_subst,pbo,pty, attrs = proof in
   let (_,context,ty) as conjecture = CicUtil.lookup_meta goal metasenv in
   assert (hyps_pat = []); (*CSC: not implemented yet *)
   let eq_URI =
@@ -239,17 +233,17 @@ let replace_tac ~(pattern: ProofEngineTypes.lazy_pattern) ~with_what =
   in
   let context_len = List.length context in
   let subst,metasenv,u,_,selected_terms_with_context =
-   ProofEngineHelpers.select ~metasenv ~ugraph:CicUniv.empty_ugraph
+   ProofEngineHelpers.select ~metasenv ~ugraph:CicUniv.oblivion_ugraph
     ~conjecture ~pattern in
   let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
   let with_what, metasenv, u = with_what context metasenv u in
   let with_what = CicMetaSubst.apply_subst subst with_what in
   let pbo = CicMetaSubst.apply_subst subst pbo in
   let pty = CicMetaSubst.apply_subst subst pty in
-  let status = (uri,metasenv,pbo,pty, attrs),goal in
+  let status = (uri,metasenv,_subst,pbo,pty, attrs),goal in
   let ty_of_with_what,u =
    CicTypeChecker.type_of_aux'
-    metasenv context with_what CicUniv.empty_ugraph in
+    metasenv context with_what CicUniv.oblivion_ugraph in
   let whats =
    match selected_terms_with_context with
       [] -> raise (ProofEngineTypes.Fail (lazy "Replace: no term selected"))
@@ -276,7 +270,7 @@ let replace_tac ~(pattern: ProofEngineTypes.lazy_pattern) ~with_what =
              (lazy "Replace: one of the selected terms is not closed")) in
          let ty_of_t_in_context,u = (* TASSI: FIXME *)
           CicTypeChecker.type_of_aux' metasenv context t_in_context
-           CicUniv.empty_ugraph in
+           CicUniv.oblivion_ugraph in
          let b,u = CicReduction.are_convertible ~metasenv context
           ty_of_with_what ty_of_t_in_context u in
          if b then
@@ -288,7 +282,7 @@ let replace_tac ~(pattern: ProofEngineTypes.lazy_pattern) ~with_what =
            (ProofEngineTypes.Fail
              (lazy "Replace: one of the selected terms and the term to be replaced with have not convertible types"))
        ) l in
-  let rec aux n whats status =
+  let rec aux n whats (status : ProofEngineTypes.status) =
    match whats with
       [] -> ProofEngineTypes.apply_tactic T.id_tac status
     | (what,lazy_pattern)::tl ->
@@ -313,7 +307,7 @@ let replace_tac ~(pattern: ProofEngineTypes.lazy_pattern) ~with_what =
                     ~start:(
                       ProofEngineTypes.mk_tactic
                        (function ((proof,goal) as status) ->
-                         let _,metasenv,_,_, _ = proof in
+                         let _,metasenv,_subst,_,_, _ = proof in
                          let _,context,_ = CicUtil.lookup_meta goal metasenv in
                          let hyps =
                           try
@@ -328,7 +322,7 @@ let replace_tac ~(pattern: ProofEngineTypes.lazy_pattern) ~with_what =
               T.id_tac])
          status
   and aux_tac n tl = ProofEngineTypes.mk_tactic (aux n tl) in
-   aux 0 whats status
+   aux 0 whats (status : ProofEngineTypes.status)
  in
    ProofEngineTypes.mk_tactic (replace_tac ~pattern ~with_what)
 ;;
@@ -342,7 +336,7 @@ let reflexivity_tac =
 
 let symmetry_tac =
  let symmetry_tac (proof, goal) =
-   let (_,metasenv,_,_, _) = proof in
+   let (_,metasenv,_subst,_,_, _) = proof in
     let metano,context,ty = CicUtil.lookup_meta goal metasenv in
      match (R.whd context ty) with
         (C.Appl [(C.MutInd (uri, 0, [])); _; _; _])
@@ -360,7 +354,7 @@ let symmetry_tac =
 let transitivity_tac ~term =
  let transitivity_tac ~term status =
   let (proof, goal) = status in
-   let (_,metasenv,_,_, _) = proof in
+   let (_,metasenv,_subst,_,_, _) = proof in
     let metano,context,ty = CicUtil.lookup_meta goal metasenv in
      match (R.whd context ty) with
         (C.Appl [(C.MutInd (uri, 0, [])); _; _; _])