Implement name mangling option

9 files changed, 271 insertions, 7 deletions

diff --git a/CHANGES b/CHANGES
index 8d344d4f0..449d346b0 100644
--- a/CHANGES
+++ b/CHANGES
@@ -74,6 +74,13 @@ Universes
 - Fix #5726: Notations that start with `Type` now support universe instances
   with `@{u}`.
 
+Tools
+
+- Coq can now be run with the option -mangle-names to change the auto-generated
+  name scheme. This is intended to function as a linter for developments that
+  want to be robust to changes in auto-generated names. This feature is experimental,
+  and may change or dissapear without warning.
+
 Checker
 
 - The checker now accepts filenames in addition to logical paths.
diff --git a/doc/refman/RefMan-com.tex b/doc/refman/RefMan-com.tex
index 04a8a25c1..5b73ac00a 100644
--- a/doc/refman/RefMan-com.tex
+++ b/doc/refman/RefMan-com.tex
@@ -241,6 +241,20 @@ The following command-line options are recognized by the commands {\tt
   Collapse the universe hierarchy of {\Coq}. Warning: this makes the
   logic inconsistent.
 
+\item[{\tt -mangle-names} {\em ident}]\ %
+
+  Experimental: Do not depend on this option.
+
+  Replace Coq's auto-generated name scheme with names of the form
+  {\tt ident0}, {\tt ident1}, \ldots etc.
+  The command {\tt Set Mangle Names}\optindex{Mangle Names} turns
+  the behavior on in a document, and {\tt Set Mangle Names Prefix "ident"}
+  \optindex{Mangle Names Prefix} changes the used prefix.
+
+  This feature is intended to be used as a linter for developments that want
+  to be robust to changes in the auto-generated name scheme. The options are
+  provided to facilitate tracking down problems.
+
 \item[{\tt -compat} {\em version}]\ %
 
   Attempt to maintain some backward-compatibility with a previous version.
diff --git a/engine/namegen.ml b/engine/namegen.ml
index ff0b5a74e..c8cc78f17 100644
--- a/engine/namegen.ml
+++ b/engine/namegen.ml
@@ -190,9 +190,45 @@ let it_mkLambda_or_LetIn_name env sigma b hyps =
 (**********************************************************************)
 (* Fresh names *)
 
+(* Introduce a mode where auto-generated names are mangled
+   to test dependence of scripts on auto-generated names *)
+
+let mangle_names = ref false
+
+let _ = Goptions.(
+    declare_bool_option
+      { optdepr  = false;
+        optname  = "mangle auto-generated names";
+        optkey   = ["Mangle";"Names"];
+        optread  = (fun () -> !mangle_names);
+        optwrite = (:=) mangle_names; })
+
+let mangle_names_prefix = ref (Id.of_string "_0")
+let set_prefix x = mangle_names_prefix := forget_subscript x
+
+let set_mangle_names_mode x = begin
+    set_prefix x;
+    mangle_names := true
+  end
+
+let _ = Goptions.(
+    declare_string_option
+      { optdepr  = false;
+        optname  = "mangled names prefix";
+        optkey   = ["Mangle";"Names";"Prefix"];
+        optread  = (fun () -> Id.to_string !mangle_names_prefix);
+        optwrite = begin fun x ->
+                   set_prefix
+                     (try Id.of_string x
+                      with CErrors.UserError _ -> CErrors.user_err Pp.(str ("Not a valid identifier: \"" ^ x ^ "\".")))
+                   end })
+
+let mangle_id id = if !mangle_names then !mangle_names_prefix else id
+
 (* Looks for next "good" name by lifting subscript *)
 
 let next_ident_away_from id bad =
+  let id = mangle_id id in
   let rec name_rec id = if bad id then name_rec (increment_subscript id) else id in
   name_rec id
 
@@ -291,6 +327,7 @@ let next_global_ident_away id avoid =
    looks for same name with lower available subscript *)
 
 let next_ident_away id avoid =
+  let id = mangle_id id in
   if Id.Set.mem id avoid then
     next_ident_away_from (restart_subscript id) (fun id -> Id.Set.mem id avoid)
   else id
diff --git a/engine/namegen.mli b/engine/namegen.mli
index abeed9f62..2efbea1fe 100644
--- a/engine/namegen.mli
+++ b/engine/namegen.mli
@@ -118,3 +118,9 @@ val compute_displayed_name_in_gen :
 (* Naming strategy for arguments in Prop when eliminating inductive types *)
 
 val use_h_based_elimination_names : unit -> bool
+
+(**********************************************************************)
+
+val set_mangle_names_mode : Id.t -> unit
+(** Turn on mangled names mode and with the given prefix.
+    @raise UserError if the argument is invalid as an identifier. *)
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 9fded04db..ae1b69516 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -411,12 +411,11 @@ let find_name mayrepl decl naming gl = match naming with
       new_fresh_id idl (default_id env sigma decl) gl
   | NamingBasedOn (id,idl) ->  new_fresh_id idl id gl
   | NamingMustBe (loc,id) ->
-      (* When name is given, we allow to hide a global name *)
-      let ids_of_hyps = Tacmach.New.pf_ids_set_of_hyps gl in
-      let id' = next_ident_away id ids_of_hyps in
-      if not mayrepl && not (Id.equal id' id) then
-        user_err ?loc  (Id.print id ++ str" is already used.");
-      id
+     (* When name is given, we allow to hide a global name *)
+     let ids_of_hyps = Tacmach.New.pf_ids_set_of_hyps gl in
+     if not mayrepl && Id.Set.mem id ids_of_hyps then
+       user_err ?loc  (Id.print id ++ str" is already used.");
+     id
 
 (**************************************************************)
 (*   Computing position of hypotheses for replacing           *)
diff --git a/test-suite/success/name_mangling.v b/test-suite/success/name_mangling.v
new file mode 100644
index 000000000..571dde880
--- /dev/null
+++ b/test-suite/success/name_mangling.v
@@ -0,0 +1,192 @@
+(* -*- coq-prog-args: ("-mangle-names" "_") -*- *)
+
+(* Check that refine policy of redefining previous names make these names private *)
+(* abstract can change names in the environment! See bug #3146 *)
+
+Goal True -> True.
+intro.
+Fail exact H.
+exact _0.
+Abort.
+
+Unset Mangle Names.
+Goal True -> True.
+intro; exact H.
+Abort.
+
+Set Mangle Names.
+Set Mangle Names Prefix "baz".
+Goal True -> True.
+intro.
+Fail exact H.
+Fail exact _0.
+exact baz0.
+Abort.
+
+Goal True -> True.
+intro; assumption.
+Abort.
+
+Goal True -> True.
+intro x; exact x.
+Abort.
+
+Goal forall x y, x+y=0.
+intro x.
+refine (fun x => _).
+Fail Check x0.
+Check x.
+Abort.
+
+(* Example from Emilio *)
+
+Goal forall b : False, b = b.
+intro b.
+refine (let b := I in _).
+Fail destruct b0.
+Abort.
+
+(* Example from Cyprien *)
+
+Goal True -> True.
+Proof.
+  refine (fun _ => _).
+  Fail exact t.
+Abort.
+
+(* Example from Jason *)
+
+Goal False -> False.
+intro H.
+Fail abstract exact H.
+Abort.
+
+(* Variant *)
+
+Goal False -> False.
+intro.
+Fail abstract exact H.
+Abort.
+
+(* Example from Jason *)
+
+Goal False -> False.
+intro H.
+(* Name H' is from Ltac here, so it preserves the privacy *)
+(* But abstract messes everything up *)
+Fail let H' := H in abstract exact H'.
+let H' := H in exact H'.
+Qed.
+
+(* Variant *)
+
+Goal False -> False.
+intro.
+Fail let H' := H in abstract exact H'.
+Abort.
+
+(* Indirectly testing preservation of names by move (derived from Jason) *)
+
+Inductive nat2 := S2 (_ _ : nat2).
+Goal forall t : nat2, True.
+  intro t.
+  let IHt1 := fresh "IHt1" in
+  let IHt2 := fresh "IHt2" in
+  induction t as [? IHt1 ? IHt2].
+  Fail exact IHt1.
+Abort.
+
+(* Example on "pose proof" (from Jason) *)
+
+Goal False -> False.
+intro; pose proof I as H0.
+Fail exact H.
+Abort.
+
+(* Testing the approach for which non alpha-renamed quantified names are user-generated *)
+
+Section foo.
+Context (b : True).
+Goal forall b : False, b = b.
+Fail destruct b0.
+Abort.
+
+Goal forall b : False, b = b.
+now destruct b.
+Qed.
+End foo.
+
+(* Test stability of "fix" *)
+
+Lemma a : forall n, n = 0.
+Proof.
+fix a 1.
+Check a.
+fix 1.
+Fail Check a0.
+Abort.
+
+(* Test stability of "induction" *)
+
+Lemma a : forall n : nat, n = n.
+Proof.
+intro n; induction n as [ | n IHn ].
+- auto.
+- Check n.
+  Check IHn.
+Abort.
+
+Inductive I := C : I -> I -> I.
+
+Lemma a : forall n : I, n = n.
+Proof.
+intro n; induction n as [ n1 IHn1 n2 IHn2 ].
+Check n1.
+Check n2.
+apply f_equal2.
++ apply IHn1.
++ apply IHn2.
+Qed.
+
+(* Testing remember *)
+
+Lemma c : 0 = 0.
+Proof.
+remember 0 as x eqn:Heqx.
+Check Heqx.
+Abort.
+
+Lemma c : forall Heqx, Heqx -> 0 = 0.
+Proof.
+intros Heqx X.
+remember 0 as x.
+Fail Check Heqx0. (* Heqx0 is not canonical *)
+Abort.
+
+(* An example by Jason from the discussion for PR #268 *)
+
+Goal nat -> Set -> True.
+  intros x y.
+  match goal with
+  | [ x : _, y : _ |- _ ]
+    => let z := fresh "z" in
+      rename y into z, x into y;
+        let x' := fresh "x" in
+        rename z into x'
+  end.
+  revert y. (* x has been explicitly moved to y *)
+  Fail revert x. (* x comes from "fresh" *)
+Abort.
+
+Goal nat -> Set -> True.
+  intros.
+  match goal with
+  | [ x : _, y : _ |- _ ]
+    => let z := fresh "z" in
+      rename y into z, x into y;
+        let x' := fresh "x" in
+        rename z into x'
+  end.
+  Fail revert y. (* generated by intros *)
+  Fail revert x. (* generated by intros *)
+Abort.
diff --git a/tools/coqc.ml b/tools/coqc.ml
index b381c5ba4..11c3e4f78 100644
--- a/tools/coqc.ml
+++ b/tools/coqc.ml
@@ -109,7 +109,7 @@ let parse_args () =
       |"-load-ml-source"|"-require"|"-load-ml-object"
       |"-init-file"|"-dump-glob"|"-compat"|"-coqlib"|"-top"
       |"-async-proofs-j" |"-async-proofs-private-flags" |"-async-proofs" |"-w"
-      |"-o"|"-profile-ltac-cutoff"
+      |"-o"|"-profile-ltac-cutoff"|"-mangle-names"
       as o) :: rem ->
 	begin
 	  match rem with
diff --git a/toplevel/coqargs.ml b/toplevel/coqargs.ml
index 5b73471c5..1fdcd2bd4 100644
--- a/toplevel/coqargs.ml
+++ b/toplevel/coqargs.ml
@@ -270,6 +270,11 @@ let get_cache opt = function
   | "force" -> Some Stm.AsyncOpts.Force
   | _ -> prerr_endline ("Error: force expected after "^opt); exit 1
 
+let get_identifier opt s =
+  try Names.Id.of_string s
+  with CErrors.UserError _ ->
+    prerr_endline ("Error: valid identifier expected after option "^opt); exit 1
+
 let is_not_dash_option = function
   | Some f when String.length f > 0 && f.[0] <> '-' -> true
   | _ -> false
@@ -465,6 +470,9 @@ let parse_args arglist : coq_cmdopts * string list =
     |"-load-vernac-source-verbose"|"-lv" ->
       add_load_vernacular oval true (next ())
 
+    |"-mangle-names" ->
+      Namegen.set_mangle_names_mode (get_identifier opt (next ())); oval
+
     |"-print-mod-uid" ->
       let s = String.concat " " (List.map get_native_name rem) in print_endline s; exit 0
 
diff --git a/toplevel/usage.ml b/toplevel/usage.ml
index f0215b678..e28637f2e 100644
--- a/toplevel/usage.ml
+++ b/toplevel/usage.ml
@@ -77,6 +77,7 @@ let print_usage_channel co command =
 \n  -impredicative-set     set sort Set impredicative\
 \n  -indices-matter        levels of indices (and nonuniform parameters) contribute to the level of inductives\
 \n  -type-in-type          disable universe consistency checking\
+\n  -mangle-names x        mangle auto-generated names using prefix x\
 \n  -time                  display the time taken by each command\
 \n  -profile-ltac          display the time taken by each (sub)tactic\
 \n  -m, --memory           display total heap size at program exit\