diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 5f157ca4284d73f28f30dac6c65b4e3e4c4284a0..38e2540db6f4b4b024485b9d49d42fcbc92ea5ff 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -31,7 +31,7 @@ build-coq.dev:
<<: *template
variables:
OPAM_PINS: "coq version dev"
- #MANGLE_NAMES: "1" name mangling causes issues with string_ident
+ MANGLE_NAMES: "1"
build-coq.8.13.1:
<<: *template
diff --git a/iris/proofmode/ltac_tactics.v b/iris/proofmode/ltac_tactics.v
index 8320613240aa776a3e26573ab6d699f4cd7cf9b9..5aa750a9e83712c8839541820db1aca6a7f26edd 100644
--- a/iris/proofmode/ltac_tactics.v
+++ b/iris/proofmode/ltac_tactics.v
@@ -1450,7 +1450,9 @@ Local Ltac iDestructHypGo Hz pat0 pat :=
| IList [[IPure IGallinaAnon; ?pat2]] =>
iExistDestruct Hz as ? Hz; iDestructHypGo Hz pat0 pat2
| IList [[IPure (IGallinaNamed ?s); ?pat2]] =>
- let x := string_to_ident s in iExistDestruct Hz as x Hz;
+ let x := fresh in
+ iExistDestruct Hz as x Hz;
+ rename_by_string x s;
iDestructHypGo Hz pat0 pat2
| IList [[?pat1; ?pat2]] =>
let Hy := iFresh in iAndDestruct Hz as Hz Hy;
@@ -1468,8 +1470,10 @@ Local Ltac iDestructHypGo Hz pat0 pat :=
| IList [_;_] => fail "iDestruct: in" pat0 "a disjunct has multiple patterns"
| IPure IGallinaAnon => iPure Hz as ?
- | IPure (IGallinaNamed ?s) => let x := string_to_ident s in
- iPure Hz as x
+ | IPure (IGallinaNamed ?s) =>
+ let x := fresh in
+ iPure Hz as x;
+ rename_by_string x s
| IRewrite Right => iPure Hz as ->
| IRewrite Left => iPure Hz as <-
| IIntuitionistic ?pat => iIntuitionistic Hz; iDestructHypGo Hz pat0 pat
@@ -1568,8 +1572,11 @@ Ltac iIntros_go pats startproof :=
| false => idtac
end
(* Optimizations to avoid generating fresh names *)
- | IPure (IGallinaNamed ?s) :: ?pats => let i := string_to_ident s in
- iIntro (i); iIntros_go pats startproof
+ | IPure (IGallinaNamed ?s) :: ?pats =>
+ let i := fresh in
+ iIntro (i);
+ rename_by_string i s;
+ iIntros_go pats startproof
| IPure IGallinaAnon :: ?pats => iIntro (?); iIntros_go pats startproof
| IIntuitionistic (IIdent ?H) :: ?pats => iIntro #H; iIntros_go pats false
| IDrop :: ?pats => iIntro _; iIntros_go pats startproof
diff --git a/iris/proofmode/string_ident.v b/iris/proofmode/string_ident.v
index 1241e3928880fe1c7dcb469fa245a99022adad7c..600951aab25427f6d6a276a0872ccf7134565fe0 100644
--- a/iris/proofmode/string_ident.v
+++ b/iris/proofmode/string_ident.v
@@ -1,4 +1,4 @@
-From Ltac2 Require Import Ltac2.
+From Ltac2 Require Ltac2.
From Coq Require Import Strings.String.
From Coq Require Import Init.Byte.
From iris.prelude Require Import options.
@@ -6,9 +6,10 @@ From iris.prelude Require Import options.
Import List.ListNotations.
Local Open Scope list.
-Ltac2 Type exn ::= [ NotStringLiteral(constr) | InvalidIdent(string) ].
-
Module StringToIdent.
+ Import Ltac2.
+
+ Ltac2 Type exn ::= [ NotStringLiteral(constr) | InvalidIdent(string) ].
Ltac2 coq_byte_to_int b :=
(match! b with
@@ -19,7 +20,7 @@ Module StringToIdent.
Ltac2 coq_byte_to_char b :=
Char.of_int (coq_byte_to_int b).
- Fixpoint coq_string_to_list_byte (s : string): list byte :=
+ Fixpoint coq_string_to_list_byte (s : string) : list byte :=
match s with
| EmptyString => []
| String c s => Ascii.byte_of_ascii c :: coq_string_to_list_byte s
@@ -53,13 +54,9 @@ Module StringToIdent.
let _ := coq_byte_list_blit_list 0 bytes str in
str.
- (* to convert the string to an identifier we have to use the tools from Fresh;
- note we pass Fresh.fresh and empty set of identifiers to avoid, so this
- isn't necessarily fresh in the context, but if that's desired we can always
- do it later with Ltac1's fresh. *)
Ltac2 ident_from_string (s : string) :=
match Ident.of_string s with
- | Some id => Fresh.fresh (Fresh.Free.of_ids []) id
+ | Some id => id
| None => Control.throw (InvalidIdent s)
end.
@@ -67,32 +64,34 @@ Module StringToIdent.
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 returning the resulting identifier.
-
- The only FFI from Ltac1 to Ltac2 is to call an Ltac2 expression that solves
- a goal. We'll solve that goal with [fun (x:unit) => tt] where the name [x] is
- the desired identifier - Coq remembers the identifier and we can extract it
- with Ltac1 pattern matching. *)
+ 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.
+ *)
Ltac2 get_opt o := match o with None => Control.throw Not_found | Some x => x end.
- (** solve a goal of the form [unit -> unit] with a function that has the
- appropriate name *)
- Ltac coq_string_to_ident_lambda :=
+ Ltac intros_by_string :=
ltac2:(s1 |- let s := get_opt (Ltac1.to_constr s1) in
let ident := coq_string_to_ident s in
- clear; (* needed since ident might already be in scope where
- this is called *)
- intros $ident;
- exact tt).
+ intros $ident).
End StringToIdent.
-(** Finally we wrap everything up by running [coq_string_to_ident_lambda] in a new
-context using a tactic-in-terms, extracting just the identifier from the
-produced lambda, and returning it as an Ltac1 value. *)
+Open Scope string_scope.
+
+(** 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. *)
+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:(StringToIdent.coq_string_to_ident_lambda s) : unit -> unit) in
+ let x := constr:(ltac:(StringToIdent.intros_by_string s; exact tt) : unit -> unit) in
match x with
| (fun (name:_) => _) => name
end.
diff --git a/tests/proofmode.v b/tests/proofmode.v
index 97aa9604a368e42f51c25460be84c568ee01ae9f..9d5336d56944da28a4d63c66ffd636ad3d6f0538 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -480,11 +480,18 @@ Proof.
Qed.
(* Ensure that [% %] works as a pattern for an existential with a pure body. *)
-Lemma test_exist_pure_destruct :
+Lemma test_exist_pure_destruct_1 :
(∃ x, ⌜ x = 0 âŒ) ⊢@{PROP} True.
Proof.
iIntros "[% %]". done.
Qed.
+(* Also test nested existentials where the type of the 2nd depends on the first
+(which could cause trouble if we do things in the wrong order) *)
+Lemma test_exist_pure_destruct_2 :
+ (∃ x (_:x=0), True) ⊢@{PROP} True.
+Proof.
+ iIntros "(% & % & $)".
+Qed.
Lemma test_fresh P Q:
(P ∗ Q) -∗ (P ∗ Q).
diff --git a/tests/string_ident.ref b/tests/string_ident.ref
index f42f19c8c7f259392d3c40e7d35cfdb8e0efce9c..8486db4a4328db101b9a23c5080ba734d202bb7c 100644
--- a/tests/string_ident.ref
+++ b/tests/string_ident.ref
@@ -1,12 +1,12 @@
"test_invalid_ident"
: string
The command has indeed failed with message:
-Uncaught Ltac2 exception: InvalidIdent ("has a space")
+Uncaught Ltac2 exception: StringToIdent.InvalidIdent ("has a space")
"test_not_string"
: string
The command has indeed failed with message:
-Uncaught Ltac2 exception: NotStringLiteral (constr:(4))
+Uncaught Ltac2 exception: StringToIdent.NotStringLiteral (constr:(4))
"test_not_literal"
: string
The command has indeed failed with message:
-Uncaught Ltac2 exception: NotStringLiteral (constr:(s))
+Uncaught Ltac2 exception: StringToIdent.NotStringLiteral (constr:(s))
diff --git a/tests/string_ident.v b/tests/string_ident.v
index 379ba301107b4aad130f07b58821dd0d7a1bcf3e..bc42e01062337d0f9b0f2e9f2a59124c2a87effc 100644
--- a/tests/string_ident.v
+++ b/tests/string_ident.v
@@ -3,39 +3,26 @@ From Coq Require Import Strings.String.
From stdpp Require Import base.
Open Scope string.
-(* these tests should test name generation directly, which Mangle Names
-interferes with *)
-Unset Mangle Names.
-
Lemma test_basic_ident : ∀ (n:nat), n = n.
Proof.
- let x := string_to_ident "n" in
- intros x.
+ let x := fresh in intros x; rename_by_string x "n".
exact (eq_refl n).
Qed.
-Lemma test_in_scope (n:nat) : n = n.
-Proof.
- let x := string_to_ident "n" in exact (eq_refl n).
-Qed.
-
Check "test_invalid_ident".
-Lemma test_invalid_ident : True.
+Lemma test_invalid_ident : ∀ (n:nat), True.
Proof.
- Fail let x := string_to_ident "has a space" in
- idtac x.
+ Fail let x := fresh in intros x; rename_by_string x "has a space".
Abort.
Check "test_not_string".
-Lemma test_not_string : True.
+Lemma test_not_string : ∀ (n:nat), True.
Proof.
- Fail let x := string_to_ident 4 in
- idtac x.
+ Fail let x := fresh in intros x; rename_by_string x 4.
Abort.
Check "test_not_literal".
-Lemma test_not_literal (s:string) : True.
+Lemma test_not_literal (s:string) : ∀ (n:nat), True.
Proof.
- Fail let x := string_to_ident s in
- idtac x.
+ Fail let x := fresh in intros x; rename_by_string x s.
Abort.