From 04cfb486c3fe1609839c6a435bc2db6d6cae581d Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Fri, 1 Jul 2005 13:06:43 +0000
Subject: [PATCH] replace tactic reimplemented. It is now able to replace
 several terms at once. NOTE: it is still unable to replace terms in the
 hypotheses.

---
 helm/ocaml/tactics/equalityTactics.ml | 82 +++++++++++++++------------
 1 file changed, 47 insertions(+), 35 deletions(-)

diff --git a/helm/ocaml/tactics/equalityTactics.ml b/helm/ocaml/tactics/equalityTactics.ml
index a07a06837..31c9b60b4 100644
--- a/helm/ocaml/tactics/equalityTactics.ml
+++ b/helm/ocaml/tactics/equalityTactics.ml
@@ -23,7 +23,6 @@
  * http://cs.unibo.it/helm/.
  *)
  
-
 let rewrite_tac ~direction ~pattern equality =
  let rewrite_tac ~direction ~pattern:(wanted,hyps_pat,concl_pat) equality status
  =
@@ -118,7 +117,7 @@ let replace_tac ~pattern ~with_what =
   let module P = PrimitiveTactics in
   let module T = Tacticals in
   let _,metasenv,_,_ = proof in
-  let (_,context,_) as conjecture = CicUtil.lookup_meta goal metasenv in
+  let (_,context,ty) as conjecture = CicUtil.lookup_meta goal metasenv in
   assert (hyps_pat = []); (*CSC: not implemented yet *)
   let context_len = List.length context in
   let _,selected_terms_with_context =
@@ -155,43 +154,56 @@ let replace_tac ~pattern ~with_what =
            CicUniv.empty_ugraph in
          let b,u = CicReduction.are_convertible ~metasenv context
           ty_of_with_what ty_of_t_in_context u in
-         if b then t_in_context
+         if b then
+          let concl_pat_for_t = ProofEngineHelpers.pattern_of ~term:ty [t] in
+          let pattern_for_t = None,[],concl_pat_for_t in
+           t_in_context,pattern_for_t
          else
           raise
            (ProofEngineTypes.Fail
              "Replace: one of the selected terms and the term to be replaced with have not convertible types")
-       ) l
-  in
-   let rec aux whats status =
-    match whats with
-       [] -> ProofEngineTypes.apply_tactic T.id_tac status
-     | what::tl ->
-        ProofEngineTypes.apply_tactic
-          (T.thens
-             ~start:(
-               P.cut_tac 
-                (C.Appl [
-                  (C.MutInd (HelmLibraryObjects.Logic.eq_URI, 0, [])) ;
-                  ty_of_with_what ; 
-                  what ; 
-                  with_what]))
-             ~continuations:[            
-               T.then_
-                 ~start:(
-                   rewrite_simpl_tac ~direction:`LeftToRight ~pattern (C.Rel 1))
-                  ~continuation:(
-                    let hyp =
-                     try
-                      match List.hd context with
-                         Some (Cic.Name name,_) -> name
-                       | _ -> assert false
-                     with (Failure "hd") -> assert false
-                    in
-                     ProofEngineStructuralRules.clear ~hyp) ;
-               aux_tac tl])
-          status
-   and aux_tac tl = ProofEngineTypes.mk_tactic (aux tl) in
-    aux whats status
+       ) l in
+  let rec aux n whats status =
+   match whats with
+      [] -> ProofEngineTypes.apply_tactic T.id_tac status
+    | (what,pattern)::tl ->
+       let what = CicSubstitution.lift n what in
+       let with_what = CicSubstitution.lift n with_what in
+       let ty_of_with_what = CicSubstitution.lift n ty_of_with_what in
+       ProofEngineTypes.apply_tactic
+         (T.thens
+            ~start:(
+              P.cut_tac 
+               (C.Appl [
+                 (C.MutInd (HelmLibraryObjects.Logic.eq_URI, 0, [])) ;
+                 ty_of_with_what ; 
+                 what ; 
+                 with_what]))
+            ~continuations:[            
+              T.then_
+                ~start:(
+                  rewrite_tac ~direction:`LeftToRight ~pattern (C.Rel 1))
+                 ~continuation:(
+                   T.then_
+                    ~start:(
+                      ProofEngineTypes.mk_tactic
+                       (function ((proof,goal) as status) ->
+                         let _,metasenv,_,_ = proof in
+                         let _,context,_ = CicUtil.lookup_meta goal metasenv in
+                         let hyp =
+                          try
+                           match List.hd context with
+                              Some (Cic.Name name,_) -> name
+                            | _ -> assert false
+                          with (Failure "hd") -> assert false
+                         in
+                          ProofEngineTypes.apply_tactic
+                           (ProofEngineStructuralRules.clear ~hyp) status))
+                    ~continuation:(aux_tac (n + 1) tl));
+              T.id_tac])
+         status
+  and aux_tac n tl = ProofEngineTypes.mk_tactic (aux n tl) in
+   aux 0 whats status
  in
    ProofEngineTypes.mk_tactic (replace_tac ~pattern ~with_what)
 ;;
-- 
2.39.2