From 489268fda04c2eb838a6423292df43a26e431fdd Mon Sep 17 00:00:00 2001 From: Tej Chajed Date: Mon, 15 Feb 2021 15:15:00 -0600 Subject: [PATCH 1/7] Provide string_ident natively Fixes #404 --- _CoqProject | 1 + iris/proofmode/ltac_tactics.v | 35 ++++--------- iris/proofmode/string_ident.v | 99 +++++++++++++++++++++++++++++++++++ tests/proofmode.v | 8 --- tests/string_ident.ref | 12 +++++ tests/string_ident.v | 36 +++++++++++++ 6 files changed, 159 insertions(+), 32 deletions(-) create mode 100644 iris/proofmode/string_ident.v create mode 100644 tests/string_ident.ref create mode 100644 tests/string_ident.v diff --git a/_CoqProject b/_CoqProject index fcb681128..4737f7f4c 100644 --- a/_CoqProject +++ b/_CoqProject @@ -117,6 +117,7 @@ iris/program_logic/total_ectx_lifting.v iris/program_logic/atomic.v iris/proofmode/base.v iris/proofmode/ident_name.v +iris/proofmode/string_ident.v iris/proofmode/tokens.v iris/proofmode/coq_tactics.v iris/proofmode/ltac_tactics.v diff --git a/iris/proofmode/ltac_tactics.v b/iris/proofmode/ltac_tactics.v index ad529cf61..7b661ce69 100644 --- a/iris/proofmode/ltac_tactics.v +++ b/iris/proofmode/ltac_tactics.v @@ -1,7 +1,8 @@ From stdpp Require Import namespaces hlist pretty. From iris.bi Require Export bi telescopes. From iris.proofmode Require Import base intro_patterns spec_patterns - sel_patterns coq_tactics reduction. + sel_patterns coq_tactics reduction + string_ident. From iris.proofmode Require Export classes notation. From iris.prelude Require Import options. Export ident. @@ -1421,29 +1422,15 @@ Tactic Notation "iModCore" constr(H) := |iSolveSideCondition |pm_reduce; pm_prettify(* subgoal *)]. -(* This tactic should take a string [s] and solve the goal with [exact (λ -(s:unit), tt)], where the name of the binder is the string as an identifier. -We use this API (rather than simply returning the identifier) since it works -correctly when replaced with [fail]. - -One way to implement such a function is to use Ltac2 on Coq 8.11+. Another -option is https://github.com/ppedrot/coq-string-ident for Coq 8.10. *) -Ltac string_to_ident_hook := fun s => fail 100 "string_to_ident is unavailable in this version of Coq". - -(* Turn a string_to_ident that produces an ident value into one that solves the -goal with a [unit → unit] function instead, as expected for -[string_to_ident_hook]. *) -Ltac make_string_to_ident_hook string_to_ident := - fun s => let x := string_to_ident s in - exact (λ (x:unit), tt). - -(* [string_to_ident] uses [string_to_ident_hook] to turn [s] into an identifier -and return it. *) -Local Ltac string_to_ident s := - let ident_fun := constr:(ltac:(string_to_ident_hook s)) in - lazymatch ident_fun with - | λ (x:_), _ => x - end. +(* These two definitions are unused but present for backwards compatibility with +https://gitlab.mpi-sws.org/iris/string-ident. + +Previosly (for Coq 8.10) this feature required a separate Ltac2 implementation, +which would override [string_to_ident_hook]. Now the proofmode ships with an +Ltac2 string_to_ident implementation. *) + +Ltac make_string_to_ident_hook string_to_ident := fun s => fail "hooks are no longer used". +Ltac string_to_ident_hook := fail "this hook is no longer used". (** * Basic destruct tactic *) diff --git a/iris/proofmode/string_ident.v b/iris/proofmode/string_ident.v new file mode 100644 index 000000000..cc042a595 --- /dev/null +++ b/iris/proofmode/string_ident.v @@ -0,0 +1,99 @@ +From Ltac2 Require Import Ltac2. +From Coq Require Import Strings.String. +From Coq Require Import Init.Byte. +From iris.prelude Require Import options. + +Import List.ListNotations. +Local Open Scope list. + +Ltac2 Type exn ::= [ NotStringLiteral(constr) | InvalidIdent(string) ]. + +Module StringToIdent. + + Ltac2 coq_byte_to_int b := + (match! b with + (* generate this line with python3 -c 'print(" ".join([\'| x%02x => %d\' % (x,x) for x in range(256)]))' *) + | x00 => 0 | x01 => 1 | x02 => 2 | x03 => 3 | x04 => 4 | x05 => 5 | x06 => 6 | x07 => 7 | x08 => 8 | x09 => 9 | x0a => 10 | x0b => 11 | x0c => 12 | x0d => 13 | x0e => 14 | x0f => 15 | x10 => 16 | x11 => 17 | x12 => 18 | x13 => 19 | x14 => 20 | x15 => 21 | x16 => 22 | x17 => 23 | x18 => 24 | x19 => 25 | x1a => 26 | x1b => 27 | x1c => 28 | x1d => 29 | x1e => 30 | x1f => 31 | x20 => 32 | x21 => 33 | x22 => 34 | x23 => 35 | x24 => 36 | x25 => 37 | x26 => 38 | x27 => 39 | x28 => 40 | x29 => 41 | x2a => 42 | x2b => 43 | x2c => 44 | x2d => 45 | x2e => 46 | x2f => 47 | x30 => 48 | x31 => 49 | x32 => 50 | x33 => 51 | x34 => 52 | x35 => 53 | x36 => 54 | x37 => 55 | x38 => 56 | x39 => 57 | x3a => 58 | x3b => 59 | x3c => 60 | x3d => 61 | x3e => 62 | x3f => 63 | x40 => 64 | x41 => 65 | x42 => 66 | x43 => 67 | x44 => 68 | x45 => 69 | x46 => 70 | x47 => 71 | x48 => 72 | x49 => 73 | x4a => 74 | x4b => 75 | x4c => 76 | x4d => 77 | x4e => 78 | x4f => 79 | x50 => 80 | x51 => 81 | x52 => 82 | x53 => 83 | x54 => 84 | x55 => 85 | x56 => 86 | x57 => 87 | x58 => 88 | x59 => 89 | x5a => 90 | x5b => 91 | x5c => 92 | x5d => 93 | x5e => 94 | x5f => 95 | x60 => 96 | x61 => 97 | x62 => 98 | x63 => 99 | x64 => 100 | x65 => 101 | x66 => 102 | x67 => 103 | x68 => 104 | x69 => 105 | x6a => 106 | x6b => 107 | x6c => 108 | x6d => 109 | x6e => 110 | x6f => 111 | x70 => 112 | x71 => 113 | x72 => 114 | x73 => 115 | x74 => 116 | x75 => 117 | x76 => 118 | x77 => 119 | x78 => 120 | x79 => 121 | x7a => 122 | x7b => 123 | x7c => 124 | x7d => 125 | x7e => 126 | x7f => 127 | x80 => 128 | x81 => 129 | x82 => 130 | x83 => 131 | x84 => 132 | x85 => 133 | x86 => 134 | x87 => 135 | x88 => 136 | x89 => 137 | x8a => 138 | x8b => 139 | x8c => 140 | x8d => 141 | x8e => 142 | x8f => 143 | x90 => 144 | x91 => 145 | x92 => 146 | x93 => 147 | x94 => 148 | x95 => 149 | x96 => 150 | x97 => 151 | x98 => 152 | x99 => 153 | x9a => 154 | x9b => 155 | x9c => 156 | x9d => 157 | x9e => 158 | x9f => 159 | xa0 => 160 | xa1 => 161 | xa2 => 162 | xa3 => 163 | xa4 => 164 | xa5 => 165 | xa6 => 166 | xa7 => 167 | xa8 => 168 | xa9 => 169 | xaa => 170 | xab => 171 | xac => 172 | xad => 173 | xae => 174 | xaf => 175 | xb0 => 176 | xb1 => 177 | xb2 => 178 | xb3 => 179 | xb4 => 180 | xb5 => 181 | xb6 => 182 | xb7 => 183 | xb8 => 184 | xb9 => 185 | xba => 186 | xbb => 187 | xbc => 188 | xbd => 189 | xbe => 190 | xbf => 191 | xc0 => 192 | xc1 => 193 | xc2 => 194 | xc3 => 195 | xc4 => 196 | xc5 => 197 | xc6 => 198 | xc7 => 199 | xc8 => 200 | xc9 => 201 | xca => 202 | xcb => 203 | xcc => 204 | xcd => 205 | xce => 206 | xcf => 207 | xd0 => 208 | xd1 => 209 | xd2 => 210 | xd3 => 211 | xd4 => 212 | xd5 => 213 | xd6 => 214 | xd7 => 215 | xd8 => 216 | xd9 => 217 | xda => 218 | xdb => 219 | xdc => 220 | xdd => 221 | xde => 222 | xdf => 223 | xe0 => 224 | xe1 => 225 | xe2 => 226 | xe3 => 227 | xe4 => 228 | xe5 => 229 | xe6 => 230 | xe7 => 231 | xe8 => 232 | xe9 => 233 | xea => 234 | xeb => 235 | xec => 236 | xed => 237 | xee => 238 | xef => 239 | xf0 => 240 | xf1 => 241 | xf2 => 242 | xf3 => 243 | xf4 => 244 | xf5 => 245 | xf6 => 246 | xf7 => 247 | xf8 => 248 | xf9 => 249 | xfa => 250 | xfb => 251 | xfc => 252 | xfd => 253 | xfe => 254 | xff => 255 + end). + + Ltac2 coq_byte_to_char b := + Char.of_int (coq_byte_to_int b). + + 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 + end. + + (* copy a list of Coq byte constrs into a string (already of the right length) *) + Ltac2 rec coq_byte_list_blit_list (pos:int) (ls: constr) (str: string) := + match! ls with + | nil => () + | ?c :: ?ls => + let b := coq_byte_to_char c in + String.set str pos b; coq_byte_list_blit_list (Int.add pos 1) ls str + end. + + Ltac2 rec coq_string_length (s: constr) := + match! s with + | EmptyString => 0 + | String _ ?s' => Int.add 1 (coq_string_length s') + | _ => Control.throw (NotStringLiteral(s)) + end. + + Ltac2 compute c := + Std.eval_vm None c. + + (* now we have enough to convert a Gallina string in a constr to an Ltac2 + native string *) + Ltac2 coq_string_to_string (s: constr) := + let l := coq_string_length s in + let str := String.make l (Char.of_int 0) in + let bytes := compute constr:(coq_string_to_list_byte $s) in + 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 + | None => Control.throw (InvalidIdent s) + end. + + (* [coq_string_to_ident] is the Ltac2 function we want *) + 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 get_opt o := match o with None => Control.throw Not_found | Some x => x end. + + (** this Ltac solves a goal of the form [unit -> unit] with a function that + has the appropriate name *) + + Ltac coq_string_to_ident_lambda := + 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). +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. *) +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 + match x with + | (fun (name:_) => _) => name + end. diff --git a/tests/proofmode.v b/tests/proofmode.v index bf5c427a0..9940220a3 100644 --- a/tests/proofmode.v +++ b/tests/proofmode.v @@ -1356,14 +1356,6 @@ End error_tests_bi. Section pure_name_tests. Context {PROP : bi}. Implicit Types P Q R : PROP. -(* mock string_to_ident for just these tests *) -Ltac ltac_tactics.string_to_ident_hook ::= - make_string_to_ident_hook ltac:(fun s => lazymatch s with - | "HP2" => ident:(HP2) - | "H" => ident:(H) - | "y" => ident:(y) - | _ => fail 100 s - end). Check "test_pure_name". Lemma test_pure_name P (φ1 φ2 : Prop) (Himpl : φ1 → φ2) : diff --git a/tests/string_ident.ref b/tests/string_ident.ref new file mode 100644 index 000000000..f42f19c8c --- /dev/null +++ b/tests/string_ident.ref @@ -0,0 +1,12 @@ +"test_invalid_ident" + : string +The command has indeed failed with message: +Uncaught Ltac2 exception: InvalidIdent ("has a space") +"test_not_string" + : string +The command has indeed failed with message: +Uncaught Ltac2 exception: NotStringLiteral (constr:(4)) +"test_not_literal" + : string +The command has indeed failed with message: +Uncaught Ltac2 exception: NotStringLiteral (constr:(s)) diff --git a/tests/string_ident.v b/tests/string_ident.v new file mode 100644 index 000000000..ba7a3f815 --- /dev/null +++ b/tests/string_ident.v @@ -0,0 +1,36 @@ +From iris.proofmode Require Import string_ident. +From Coq Require Import Strings.String. +Open Scope string. + +Lemma test_basic_ident : forall (n:nat), n = n. +Proof. + let x := string_to_ident "n" in + intros x. + 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. +Proof. + Fail let x := string_to_ident "has a space" in + idtac x. +Abort. + +Check "test_not_string". +Lemma test_not_string : True. +Proof. + Fail let x := string_to_ident 4 in + idtac x. +Abort. + +Check "test_not_literal". +Lemma test_not_literal (s:string) : True. +Proof. + Fail let x := string_to_ident s in + idtac x. +Abort. -- GitLab From 4a368f19a688f1674aed6beb2a11cbdd3a188553 Mon Sep 17 00:00:00 2001 From: Tej Chajed Date: Wed, 17 Mar 2021 17:19:04 -0500 Subject: [PATCH 2/7] Remove hooks entirely --- iris/proofmode/ltac_tactics.v | 10 ---------- 1 file changed, 10 deletions(-) diff --git a/iris/proofmode/ltac_tactics.v b/iris/proofmode/ltac_tactics.v index 7b661ce69..180eeee01 100644 --- a/iris/proofmode/ltac_tactics.v +++ b/iris/proofmode/ltac_tactics.v @@ -1422,16 +1422,6 @@ Tactic Notation "iModCore" constr(H) := |iSolveSideCondition |pm_reduce; pm_prettify(* subgoal *)]. -(* These two definitions are unused but present for backwards compatibility with -https://gitlab.mpi-sws.org/iris/string-ident. - -Previosly (for Coq 8.10) this feature required a separate Ltac2 implementation, -which would override [string_to_ident_hook]. Now the proofmode ships with an -Ltac2 string_to_ident implementation. *) - -Ltac make_string_to_ident_hook string_to_ident := fun s => fail "hooks are no longer used". -Ltac string_to_ident_hook := fail "this hook is no longer used". - (** * Basic destruct tactic *) (** [pat0] is the unparsed pattern, and is only used in error messages *) -- GitLab From f52c885a58ae48aca1a49824fcb02e4d64524550 Mon Sep 17 00:00:00 2001 From: Tej Chajed Date: Wed, 17 Mar 2021 17:23:24 -0500 Subject: [PATCH 3/7] Add changelog entry --- CHANGELOG.md | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/CHANGELOG.md b/CHANGELOG.md index 7ddf92e20..71c246bd9 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -52,6 +52,12 @@ lemma. * Rename `Build_loc` constructor for `loc` type to `Loc`. +Changes in `proof_mode`: + +* Add support for pure names `%H` in intro patterns. This is now natively +supported whereas the previous experimental support required installing +https://gitlab.mpi-sws.org/iris/string-ident. + The following `sed` script helps adjust your code to the renaming (on macOS, replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`). Note that the script is not idempotent, do not run it twice. -- GitLab From 7fa76d96b885e86f07c7a8bbc92040a3829b099a Mon Sep 17 00:00:00 2001 From: Tej Chajed Date: Tue, 23 Mar 2021 14:30:56 -0400 Subject: [PATCH 4/7] Fix changelog formatting --- CHANGELOG.md | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 71c246bd9..de0d390c2 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -52,11 +52,11 @@ lemma. * Rename `Build_loc` constructor for `loc` type to `Loc`. -Changes in `proof_mode`: +**Changes in `proof_mode`:** * Add support for pure names `%H` in intro patterns. This is now natively -supported whereas the previous experimental support required installing -https://gitlab.mpi-sws.org/iris/string-ident. + supported whereas the previous experimental support required installing + https://gitlab.mpi-sws.org/iris/string-ident. The following `sed` script helps adjust your code to the renaming (on macOS, replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`). -- GitLab From 82ccd751c5f2e01708d979a0cab225a7c73cff93 Mon Sep 17 00:00:00 2001 From: Tej Chajed Date: Tue, 23 Mar 2021 14:38:46 -0400 Subject: [PATCH 5/7] Address some review feedback --- iris/proofmode/string_ident.v | 15 +++++++-------- tests/string_ident.v | 3 +-- 2 files changed, 8 insertions(+), 10 deletions(-) diff --git a/iris/proofmode/string_ident.v b/iris/proofmode/string_ident.v index cc042a595..c3fdb62d6 100644 --- a/iris/proofmode/string_ident.v +++ b/iris/proofmode/string_ident.v @@ -25,7 +25,7 @@ Module StringToIdent. | String c s => Ascii.byte_of_ascii c :: coq_string_to_list_byte s end. - (* copy a list of Coq byte constrs into a string (already of the right length) *) + (** copy a list of Coq byte constrs into a string (already of the right length) *) Ltac2 rec coq_byte_list_blit_list (pos:int) (ls: constr) (str: string) := match! ls with | nil => () @@ -44,7 +44,7 @@ Module StringToIdent. Ltac2 compute c := Std.eval_vm None c. - (* now we have enough to convert a Gallina string in a constr to an Ltac2 + (** [coq_string_to_string] converts a Gallina string in a constr to an Ltac2 native string *) Ltac2 coq_string_to_string (s: constr) := let l := coq_string_length s in @@ -63,22 +63,21 @@ Module StringToIdent. | None => Control.throw (InvalidIdent s) end. - (* [coq_string_to_ident] is the Ltac2 function we want *) + (** [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 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 + 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 get_opt o := match o with None => Control.throw Not_found | Some x => x end. - (** this Ltac solves a goal of the form [unit -> unit] with a function that - has the appropriate name *) - + (** solve a goal of the form [unit -> unit] with a function that has the + appropriate name *) Ltac coq_string_to_ident_lambda := ltac2:(s1 |- let s := get_opt (Ltac1.to_constr s1) in let ident := coq_string_to_ident s in @@ -88,7 +87,7 @@ Module StringToIdent. exact tt). End StringToIdent. -(* Finally we wrap everything up by running coq_string_to_ident_lambda in a new +(** 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. *) Ltac string_to_ident s := diff --git a/tests/string_ident.v b/tests/string_ident.v index ba7a3f815..fe4f5479f 100644 --- a/tests/string_ident.v +++ b/tests/string_ident.v @@ -5,8 +5,7 @@ Open Scope string. Lemma test_basic_ident : forall (n:nat), n = n. Proof. let x := string_to_ident "n" in - intros x. - exact (eq_refl n). + intros x; exact (eq_refl x). Qed. Lemma test_in_scope (n:nat) : n = n. -- GitLab From 216fd72bda7bd28f1fb9f87b42c53f94c71fd9e4 Mon Sep 17 00:00:00 2001 From: Tej Chajed Date: Tue, 23 Mar 2021 14:42:04 -0400 Subject: [PATCH 6/7] Follow Iris formatting --- iris/proofmode/string_ident.v | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) diff --git a/iris/proofmode/string_ident.v b/iris/proofmode/string_ident.v index c3fdb62d6..1241e3928 100644 --- a/iris/proofmode/string_ident.v +++ b/iris/proofmode/string_ident.v @@ -19,14 +19,14 @@ 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 end. (** copy a list of Coq byte constrs into a string (already of the right length) *) - Ltac2 rec coq_byte_list_blit_list (pos:int) (ls: constr) (str: string) := + Ltac2 rec coq_byte_list_blit_list (pos : int) (ls : constr) (str : string) := match! ls with | nil => () | ?c :: ?ls => @@ -34,7 +34,7 @@ Module StringToIdent. String.set str pos b; coq_byte_list_blit_list (Int.add pos 1) ls str end. - Ltac2 rec coq_string_length (s: constr) := + Ltac2 rec coq_string_length (s : constr) := match! s with | EmptyString => 0 | String _ ?s' => Int.add 1 (coq_string_length s') @@ -46,7 +46,7 @@ Module StringToIdent. (** [coq_string_to_string] converts a Gallina string in a constr to an Ltac2 native string *) - Ltac2 coq_string_to_string (s: constr) := + Ltac2 coq_string_to_string (s : constr) := let l := coq_string_length s in let str := String.make l (Char.of_int 0) in let bytes := compute constr:(coq_string_to_list_byte $s) in @@ -57,20 +57,20 @@ Module StringToIdent. 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) := + Ltac2 ident_from_string (s : string) := match Ident.of_string s with | Some id => Fresh.fresh (Fresh.Free.of_ids []) id | None => Control.throw (InvalidIdent s) end. (** [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). + 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 + (** 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 + 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. *) -- GitLab From 08d54acf5ef80f80ac6d8e0b6e320b20c5258c59 Mon Sep 17 00:00:00 2001 From: Tej Chajed Date: Tue, 23 Mar 2021 15:17:18 -0400 Subject: [PATCH 7/7] Some test fixes --- tests/string_ident.v | 10 ++++++++-- 1 file changed, 8 insertions(+), 2 deletions(-) diff --git a/tests/string_ident.v b/tests/string_ident.v index fe4f5479f..379ba3011 100644 --- a/tests/string_ident.v +++ b/tests/string_ident.v @@ -1,11 +1,17 @@ From iris.proofmode Require Import string_ident. From Coq Require Import Strings.String. +From stdpp Require Import base. Open Scope string. -Lemma test_basic_ident : forall (n:nat), n = n. +(* 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; exact (eq_refl x). + intros x. + exact (eq_refl n). Qed. Lemma test_in_scope (n:nat) : n = n. -- GitLab