Merge branch 'ralf/rename-by-string' into 'master'

rename_by_string: avoid revert-intros hack

See merge request iris/iris!920

CHANGELOG.md

@@ -94,13 +94,15 @@ Coq 8.13 is no longer supported.
   `CombineSepGives` typeclass. The 'gives' clause is still experimental;
   in future versions of Iris it will combine `own` connectives based on the
   validity rules for cameras.
-- Make sure that `iStartProof` fails with a proper error message on goals with
+* Make sure that `iStartProof` fails with a proper error message on goals with
   `let`. These `let`s should either be `simpl`ed or introduced into the Coq
   context using `intros x`, `iIntros (x)`, or `iIntros "%x"`.
   This can break some proofs that did `iIntros "?"` on a goal of the shape
   `let ... in P ⊢ Q`.
-- Make `iApply`/`iPoseProof`/`iDestruct` more reliable for lemmas whose
+* Make `iApply`/`iPoseProof`/`iDestruct` more reliable for lemmas whose
   statement involves `let`.
+* Remove `string_to_ident`; use `string_to_ident_cps` instead which is in CPS
+  form and hence does not require awful hacks.
 
 **Changes in `base_logic`:**
 

iris/proofmode/string_ident.v

@@ -63,36 +63,22 @@ Module StringToIdent.
   (** [coq_string_to_ident] implements the ident to string conversion in Ltac2 *)
   Ltac2 coq_string_to_ident (s : constr) := ident_from_string (coq_string_to_string s).
 
-  (** We want to wrap this in an Ltac1 API, which requires passing a string to
-      Ltac2 and then performing an intros.
-      TODO: Once we require Coq 8.14, we should be able to pass idents across
-      the Ltac/Ltac2 barrier, which can be used to avoid the revert/intros.
+  (** We want to wrap this in an Ltac1 API, but Ltac1-2 FFI does not support
+      returning values from Ltac2 to Ltac1. So we wrute this in CPS instead.
    *)
 
   Ltac2 get_opt o := match o with None => Control.throw Not_found | Some x => x end.
 
-  Ltac intros_by_string :=
-    ltac2:(s1 |- let s := get_opt (Ltac1.to_constr s1) in
-                 let ident := coq_string_to_ident s in
-                 intros $ident).
+  Ltac string_to_ident_cps :=
+    ltac2:(s1 r |- let s := get_opt (Ltac1.to_constr s1) in
+                   let ident := coq_string_to_ident s in
+                   Ltac1.apply r [Ltac1.of_ident ident] Ltac1.run).
 End StringToIdent.
 
 (** Finally we wrap everything up intro a tactic that renames a variable given
-by ident [id] into the name given by string [s].
-Only works if [id] can be reverted, i.e. if nothing else depends on it. *)
+by ident [id] into the name given by string [s]. *)
 Ltac rename_by_string id s :=
-  revert id;
-  StringToIdent.intros_by_string s.
-
-(** We can also use this to write Ltac that *returns* the desired ident.
-However, this function will produce wrong results under [Set Mangle Names], so
-use with caution. *)
-Ltac string_to_ident s :=
-  let s := (eval cbv in s) in
-  let x := constr:(ltac:(clear; (* needed since s might already be in scope
-                         where this is called *)
-                         StringToIdent.intros_by_string s;
-                         exact tt) : unit -> unit) in
-  match x with
-  | (fun (name:_) => _) => name
-  end.
+  StringToIdent.string_to_ident_cps s ltac:(fun x => rename id into x).
+
+(* We also directly expose the CPS primitive. *)
+Ltac string_to_ident_cps := StringToIdent.string_to_ident_cps.

tests/string_ident.v

@@ -32,7 +32,7 @@ Lemma test_string_to_ident_not_fresh (n:nat) : ∀ (n:nat), nat.
 Proof.
   (* we want to check that this [string_to_ident "n"] call succeeds even with
   [n] in the context *)
-  let x := string_to_ident "n" in
+  string_to_ident_cps "n" ltac:(fun x =>
   let x := fresh x in
-  intros x.
+  intros x).
 Abort.