From 21cb46a26fdff17b94e0a2e247bd144325f53f1e Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Thu, 30 Jun 2005 11:36:49 +0000
Subject: [PATCH] The tactic change is now working again. Moreover, it now
 receives a pattern in input; moreover it handles correctly the with_what
 argument when it must be put in a context different from the one it was
 parsed in.

---
 helm/ocaml/tactics/primitiveTactics.ml | 121 ++++++++++++++++---------
 1 file changed, 76 insertions(+), 45 deletions(-)

diff --git a/helm/ocaml/tactics/primitiveTactics.ml b/helm/ocaml/tactics/primitiveTactics.ml
index 07cdd5bfe..606ae89d0 100644
--- a/helm/ocaml/tactics/primitiveTactics.ml
+++ b/helm/ocaml/tactics/primitiveTactics.ml
@@ -592,51 +592,82 @@ let elim_intros_simpl_tac ~term =
 
 exception NotConvertible
 
-(*CSC: Bug (or feature?). [with_what] is parsed in the context of the goal,  *)
-(*CSC: while [what] can have a richer context (because of binders)           *)
-(*CSC: So it is _NOT_ possible to use those binders in the [with_what] term. *)
-(*CSC: Is that evident? Is that right? Or should it be changed?              *)
+(* Note: this code is almost identical to ReductionTactics.reduction_tac and
+*  it could be unified by making the change function a callback *)
+(* CSC: with_what is parsed in the context of the goal, but it should replace
+        something that lives in a completely different context. Thus we
+        perform a delift + lift phase to move it in the right context. However,
+        in this way the tactic is less powerful than expected: with_what cannot
+        reference variables that are local to the term that is going to be
+        replaced. To fix this we should parse with_what in the context of the
+        term(s) to be replaced. *)
 let change_tac ~pattern with_what  =
-(*
-  let change_tac ~what ~with_what ~pattern (proof, goal) =
-    let curi,metasenv,pbo,pty = proof in
-    let metano,context,ty = CicUtil.lookup_meta goal metasenv in
-      (* are_convertible works only on well-typed terms *)
-    let _,u = 
-      CicTypeChecker.type_of_aux' metasenv context with_what 
-	CicUniv.empty_ugraph
-    in (* TASSI: FIXME *)
-    let b,_ = 
-      CicReduction.are_convertible context what with_what u 
+ let change_tac ~pattern ~with_what (proof, goal) =
+  let curi,metasenv,pbo,pty = proof in
+  let (metano,context,ty) as conjecture = CicUtil.lookup_meta goal metasenv in
+  let context_len = List.length context in
+  let change context'_len where terms =
+   if terms = [] then where
+   else
+    let terms, terms' = 
+      List.split
+       (List.map
+        (fun (context_of_t, t) ->
+          let context_of_t_len = List.length context_of_t in
+          let with_what_in_context' =
+            if context_len > context'_len then
+             begin
+              let with_what,subst,metasenv' =
+               CicMetaSubst.delift_rels [] metasenv
+                (context_len - context'_len) with_what
+              in
+               assert (subst = []);
+               assert (metasenv = metasenv');
+               with_what
+             end
+            else
+             with_what in
+          let with_what_in_context_of_t =
+           if context_of_t_len > context'_len then
+            CicSubstitution.lift (context_of_t_len - context'_len)
+             with_what_in_context'
+           else
+            with_what
+          in
+           t, with_what_in_context_of_t) terms)
     in
-      if b then
-	begin
-	  let replace =
-	    ProofEngineReduction.replace
-	      ~equality:(==) ~what:[what] ~with_what:[with_what]
-	  in
-	  let ty' = replace ty in
-	  let context' =
-	    List.map
-	      (function
-		   Some (name,Cic.Def (t,None))->
-		     Some (name,Cic.Def ((replace t),None))
-		 | Some (name,Cic.Decl t) -> Some (name,Cic.Decl (replace t))
-		 | None -> None
-		 | Some (_,Cic.Def (_,Some _)) -> assert false
-	      ) context
-	  in
-	  let metasenv' = 
-	    List.map
-              (function
-		   (n,_,_) when n = metano -> (metano,context',ty')
-		 | _ as t -> t
-              ) metasenv
-	  in
-	    (curi,metasenv',pbo,pty), [metano]
-	end
-      else
-	raise (ProofEngineTypes.Fail "Not convertible")
+     ProofEngineReduction.replace ~equality:(==) ~what:terms ~with_what:terms'
+      ~where:where in
+  let (selected_context,selected_ty) =
+   ProofEngineHelpers.select ~metasenv ~conjecture ~pattern in
+  let ty' = change context_len ty selected_ty in
+  let context' =
+   List.fold_right2
+    (fun entry selected_entry context' ->
+     let context'_len = List.length context' in
+     match entry,selected_entry with
+         None,None -> None::context'
+       | Some (name,Cic.Decl ty),Some (`Decl selected_ty) ->
+          let ty' = change context'_len ty selected_ty in
+           Some (name,Cic.Decl ty')::context'
+       | Some (name,Cic.Def (bo,ty)),Some (`Def (selected_bo,selected_ty)) ->
+          let bo' = change context'_len bo selected_bo in
+          let ty' =
+           match ty,selected_ty with
+              None,None -> None
+            | Some ty,Some selected_ty ->
+               Some (change context'_len ty selected_ty)
+            | _,_ -> assert false
+          in
+           Some (name,Cic.Def (bo',ty'))::context'
+       | _,_ -> assert false
+    ) context selected_context [] in
+ let metasenv' = 
+   List.map (function 
+     | (n,_,_) when n = metano -> (metano,context',ty')
+     | _ as t -> t
+   ) metasenv
+ in
+  (curi,metasenv',pbo,pty), [metano]
   in
-    mk_tactic (change_tac ~what ~with_what ~pattern)
-*) assert false
+    mk_tactic (change_tac ~pattern ~with_what)
-- 
2.39.2