Writing rename_hyps in the new monad.

This new implementation now allows for simultaneous replacing of hypotheses,
thus fixing bug #2149.

5 files changed, 61 insertions, 12 deletions

diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml
index 9d64efdeda..4bc60fffff 100644
--- a/plugins/decl_mode/decl_proof_instr.ml
+++ b/plugins/decl_mode/decl_proof_instr.ml
@@ -712,7 +712,7 @@ let rec consider_match may_intro introduced available expected gls =
 		  consider_match may_intro ((id,false)::introduced) rest_ids rest
 	      | Name hid ->
 		  tclTHENLIST
-		    [rename_hyp [id,hid];
+		    [Proofview.V82.of_tactic (rename_hyp [id,hid]);
 		     consider_match may_intro ((hid,true)::introduced) rest_ids rest]
 	  end
 	  begin
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index c530cbdeac..8e6bbcefdd 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -180,7 +180,7 @@ let change_hyp_with_using msg hyp_id t tac : tactic =
       [tclTHENLIST
       [
 	(* observe_tac "change_hyp_with_using thin" *) (thin [hyp_id]);
-	(* observe_tac "change_hyp_with_using rename " *) (rename_hyp [prov_id,hyp_id])
+	(* observe_tac "change_hyp_with_using rename " *) (Proofview.V82.of_tactic (rename_hyp [prov_id,hyp_id]))
       ]] g
 
 exception TOREMOVE
@@ -642,7 +642,7 @@ let instanciate_hyps_with_args (do_prove:Id.t list -> tactic) hyps args_id =
             Refiner.tclEVARS evm;
 	    Proofview.V82.of_tactic (pose_proof (Name prov_hid) c);
 	    thin [hid];
-	    rename_hyp [prov_hid,hid]
+	    Proofview.V82.of_tactic (rename_hyp [prov_hid,hid])
 	  ] g
       )
       ( (*
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index d589f0c180..dd9816eafd 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -2034,13 +2034,12 @@ and interp_atomic ist tac : unit Proofview.tactic =
   | TacRename l ->
       (* spiwack: until the tactic is in the monad *)
       Proofview.Trace.name_tactic (fun () -> Pp.str"<rename>") begin
-      Proofview.V82.tactic begin fun gl ->
-        let env = pf_env gl in
-        let sigma = project gl in
+      Proofview.Goal.enter begin fun gl ->
+        let env = Tacmach.New.pf_env gl in
+        let sigma = Proofview.Goal.sigma gl in
         Tactics.rename_hyp (List.map (fun (id1,id2) ->
 	  interp_hyp ist env sigma id1,
 	  interp_fresh_ident ist env sigma (snd id2)) l)
-          gl
       end
       end
 
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index e26be98b53..2e634e24b8 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -229,7 +229,57 @@ let apply_clear_request clear_flag dft c =
 let move_hyp        = Tacmach.move_hyp
 
 (* Renaming hypotheses *)
-let rename_hyp      = Tacmach.rename_hyp
+let rename_hyp repl =
+  let fold accu (src, dst) = match accu with
+  | None -> None
+  | Some (srcs, dsts) ->
+    if Id.Set.mem src srcs then None
+    else if Id.Set.mem dst dsts then None
+    else
+      let srcs = Id.Set.add src srcs in
+      let dsts = Id.Set.add dst dsts in
+      Some (srcs, dsts)
+  in
+  let init = Some (Id.Set.empty, Id.Set.empty) in
+  let dom = List.fold_left fold init repl in
+  match dom with
+  | None -> Tacticals.New.tclZEROMSG (str "Not a one-to-one name mapping")
+  | Some (src, dst) ->
+    Proofview.Goal.enter begin fun gl ->
+      let gl = Proofview.Goal.assume gl in
+      let hyps = Proofview.Goal.hyps gl in
+      let concl = Proofview.Goal.concl gl in
+      (** Check that we do not mess variables *)
+      let fold accu (id, _, _) = Id.Set.add id accu in
+      let vars = List.fold_left fold Id.Set.empty hyps in
+      let () =
+        if not (Id.Set.subset src vars) then
+          let hyp = Id.Set.choose (Id.Set.diff src vars) in
+          raise (RefinerError (NoSuchHyp hyp))
+      in
+      let mods = Id.Set.diff vars src in
+      let () =
+        try
+          let elt = Id.Set.choose (Id.Set.inter dst mods) in
+          Errors.errorlabstrm "" (pr_id elt ++ str " is already used")
+        with Not_found -> ()
+      in
+      (** All is well *)
+      let make_subst (src, dst) = (src, mkVar dst) in
+      let subst = List.map make_subst repl in
+      let subst c = Vars.replace_vars subst c in
+      let map (id, body, t) =
+        let id = try List.assoc_f Id.equal id repl with Not_found -> id in
+        (id, Option.map subst body, subst t)
+      in
+      let nhyps = List.map map hyps in
+      let nconcl = subst concl in
+      let nctx = Environ.val_of_named_context nhyps in
+      let instance = List.map (fun (id, _, _) -> mkVar id) hyps in
+      Proofview.Refine.refine ~unsafe:true begin fun sigma ->
+        Evarutil.new_evar_instance nctx sigma nconcl instance
+      end
+    end
 
 (**************************************************************)
 (*          Fresh names                                       *)
@@ -1962,7 +2012,7 @@ let check_thin_clash_then id thin avoid tac =
     let newid = next_ident_away (add_suffix id "'") avoid in
     let thin =
       List.map (on_snd (fun id' -> if Id.equal id id' then newid else id')) thin in
-    Tacticals.New.tclTHEN (Proofview.V82.tactic (rename_hyp [id,newid])) (tac thin)
+    Tacticals.New.tclTHEN (rename_hyp [id,newid]) (tac thin)
   else
     tac thin
 
@@ -2326,7 +2376,7 @@ let revert hyps =
 let generalized_name c t ids cl = function
   | Name id as na ->
       if Id.List.mem id ids then
-	errorlabstrm "" (pr_id id ++ str " is already used");
+	errorlabstrm "" (pr_id id ++ str " is already used.");
       na
   | Anonymous ->
       match kind_of_term c with
@@ -3173,7 +3223,7 @@ let abstract_generalize ?(generalize_vars=true) ?(force_dep=false) id =
       | Some (newc, dep, n, vars) ->
 	  let tac =
 	    if dep then
-	      Tacticals.New.tclTHENLIST [Proofview.V82.tactic (refine newc); Proofview.V82.tactic (rename_hyp [(id, oldid)]); Tacticals.New.tclDO n intro;
+	      Tacticals.New.tclTHENLIST [Proofview.V82.tactic (refine newc); rename_hyp [(id, oldid)]; Tacticals.New.tclDO n intro;
 			   Proofview.V82.tactic (generalize_dep ~with_let:true (mkVar oldid))]
 	    else
 	      Tacticals.New.tclTHENLIST [Proofview.V82.tactic (refine newc); Proofview.V82.tactic (clear [id]); Tacticals.New.tclDO n intro]
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index 5a78bff338..beab271142 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -171,7 +171,7 @@ val apply_clear_request : clear_flag -> bool -> constr -> unit Proofview.tactic
 val specialize    : constr with_bindings -> tactic
 
 val move_hyp      : bool -> Id.t -> Id.t move_location -> tactic
-val rename_hyp    : (Id.t * Id.t) list -> tactic
+val rename_hyp    : (Id.t * Id.t) list -> unit Proofview.tactic
 
 val revert        : Id.t list -> unit Proofview.tactic