[ssr] under: Rename bound variables a posteriori for cosmetic purpose

Rename the bound variables of the last (lambda) argument of the redex
w.r.t. the varnames specified by the user.

Co-authored-by: Erik Martin-Dorel <erik.martin-dorel@irit.fr>

1 files changed, 39 insertions, 1 deletions

diff --git a/plugins/ssr/ssrfwd.ml b/plugins/ssr/ssrfwd.ml
index ff7b891319..29983e7504 100644
--- a/plugins/ssr/ssrfwd.ml
+++ b/plugins/ssr/ssrfwd.ml
@@ -377,8 +377,46 @@ let rec intro_lock names = Proofview.Goal.enter begin fun gl ->
 
 end
 
+let rec pretty_rename evar_map term = function
+  | [] -> term
+  | varname :: varnames ->
+     try begin
+       match EConstr.destLambda evar_map term
+       with ({ Context.binder_relevance = r }, types, body) ->
+           let res = pretty_rename evar_map body varnames in
+           let name = Names.Name.mk_name varname in
+           (* Note: we don't explicitly check name \notin free_vars(res) here *)
+           EConstr.mkLambda (Context.make_annot name r, types, res)
+         end
+     with
+     | DestKO ->
+        ppdebug(lazy Pp.(str"under: cannot pretty-rename all bound variables with destLambda"));
+        term
+
 let undertac ist varnames ((dir,mult),_ as rule) =
   if mult <> Ssrequality.nomult then
     Ssrcommon.errorstrm Pp.(str"Multiplicity not supported");
-  Proofview.V82.tactic (Ssrequality.ssrrewritetac ~under:true ist [rule]) <*>
+
+  let map_redex env evar_map ~before:_ ~after:t =
+    ppdebug(lazy Pp.(str("under vars: " ^
+      (List.fold_right (fun e r -> Names.Id.to_string e ^ " " ^ r) varnames ""))));
+    ppdebug(lazy Pp.(str"under: mapping:" ++ pr_econstr_env env evar_map t));
+
+    let evar_map, ty = Typing.type_of env evar_map t in
+    let new_t = (* pretty-rename the bound variables *)
+      try begin match EConstr.destApp evar_map t with (f, ar) ->
+            let lam = Array.last ar in
+            let new_lam = pretty_rename evar_map lam varnames in
+            let new_ar, len1 = Array.copy ar, pred (Array.length ar) in
+            new_ar.(len1) <- new_lam;
+            EConstr.mkApp (f, new_ar)
+          end with
+      | DestKO ->
+        ppdebug(lazy Pp.(str"under: cannot pretty-rename bound variables with destApp"));
+        t
+    in
+    ppdebug(lazy Pp.(str"under: to:" ++ pr_econstr_env env evar_map new_t));
+    evar_map, new_t
+  in
+  Proofview.V82.tactic (Ssrequality.ssrrewritetac ~under:true ~map_redex ist [rule]) <*>
   intro_lock varnames