From 0d0b78958d6198e157171b3590516666d568c85f Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Fri, 1 Jul 2005 11:13:34 +0000
Subject: [PATCH] The replace tactic is now working again. It can now replace
 simultaneously n terms.

---
 helm/ocaml/tactics/equalityTactics.ml | 94 ++++++++++++++++++++-------
 1 file changed, 70 insertions(+), 24 deletions(-)

diff --git a/helm/ocaml/tactics/equalityTactics.ml b/helm/ocaml/tactics/equalityTactics.ml
index 93606201c..a07a06837 100644
--- a/helm/ocaml/tactics/equalityTactics.ml
+++ b/helm/ocaml/tactics/equalityTactics.ml
@@ -111,43 +111,89 @@ let rewrite_simpl_tac ~direction ~pattern equality =
 ;;
 
 let replace_tac ~pattern ~with_what =
-(*
- let replace_tac ~pattern ~with_what status =
+ let replace_tac ~pattern:(wanted,hyps_pat,concl_pat) ~with_what status =
   let (proof, goal) = status in
   let module C = Cic in
   let module U = UriManager in
   let module P = PrimitiveTactics in
   let module T = Tacticals in
   let _,metasenv,_,_ = proof in
-  let _,context,_ = CicUtil.lookup_meta goal metasenv in
-  let wty,u = (* TASSI: FIXME *)
-    CicTypeChecker.type_of_aux' metasenv context what CicUniv.empty_ugraph in
-  let wwty,_ = CicTypeChecker.type_of_aux' metasenv context with_what u in
-    try
-      if (wty = wwty) then
+  let (_,context,_) 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 =
+   ProofEngineHelpers.select ~metasenv ~conjecture ~pattern in
+  let ty_of_with_what,u =
+   CicTypeChecker.type_of_aux'
+    metasenv context with_what CicUniv.empty_ugraph in
+  let whats =
+   match selected_terms_with_context with
+      [] -> raise (ProofEngineTypes.Fail "Replace: no term selected")
+    | l ->
+      List.map
+       (fun (context_of_t,t) ->
+         let t_in_context =
+          try
+           let context_of_t_len = List.length context_of_t in
+           if context_of_t_len = context_len then t
+           else
+            (let t_in_context,subst,metasenv' =
+              CicMetaSubst.delift_rels [] metasenv
+               (context_of_t_len - context_len) t
+             in
+              assert (subst = []);
+              assert (metasenv = metasenv');
+              t_in_context)
+          with
+           CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable ->
+            (*CSC: we could implement something stronger by completely changing
+              the semantics of the tactic *)
+            raise (ProofEngineTypes.Fail
+             "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
+         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
+         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, [])) ;
-			  wty ; 
-			  what ; 
-			  with_what]))
+                (C.Appl [
+                  (C.MutInd (HelmLibraryObjects.Logic.eq_URI, 0, [])) ;
+                  ty_of_with_what ; 
+                  what ; 
+                  with_what]))
              ~continuations:[            
-	       
-	       T.then_ 	   ~start:(rewrite_simpl_tac ~term:(C.Rel 1) ())
-			   ~continuation:(
-				 ProofEngineStructuralRules.clear
-						~hyp:(List.hd context)) ;
-               T.id_tac])
+               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
-      else raise (ProofEngineTypes.Fail "Replace: terms not replaceable")
-    with (Failure "hd") -> 
-      raise (ProofEngineTypes.Fail "Replace: empty context")
+   and aux_tac tl = ProofEngineTypes.mk_tactic (aux tl) in
+    aux whats status
  in
-   ProofEngineTypes.mk_tactic (replace_tac ~what ~with_what)
-*) assert false
+   ProofEngineTypes.mk_tactic (replace_tac ~pattern ~with_what)
 ;;
 
 
-- 
2.39.2