Skip to content
GitLab
Menu
Projects
Groups
Snippets
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Menu
Open sidebar
Lennard Gäher
Iris
Commits
2f748fb4
Commit
2f748fb4
authored
Mar 23, 2021
by
Tej Chajed
Committed by
Ralf Jung
Mar 23, 2021
Browse files
Provide string_ident natively
Fixes #404
parent
66943a85
Changes
7
Hide whitespace changes
Inline
Side-by-side
CHANGELOG.md
View file @
2f748fb4
...
@@ -52,6 +52,12 @@ lemma.
...
@@ -52,6 +52,12 @@ lemma.
*
Rename
`Build_loc`
constructor for
`loc`
type to
`Loc`
.
*
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,
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`
).
replace
`sed`
by
`gsed`
, installed via e.g.
`brew install gnu-sed`
).
Note that the script is not idempotent, do not run it twice.
Note that the script is not idempotent, do not run it twice.
...
...
_CoqProject
View file @
2f748fb4
...
@@ -117,6 +117,7 @@ iris/program_logic/total_ectx_lifting.v
...
@@ -117,6 +117,7 @@ iris/program_logic/total_ectx_lifting.v
iris/program_logic/atomic.v
iris/program_logic/atomic.v
iris/proofmode/base.v
iris/proofmode/base.v
iris/proofmode/ident_name.v
iris/proofmode/ident_name.v
iris/proofmode/string_ident.v
iris/proofmode/tokens.v
iris/proofmode/tokens.v
iris/proofmode/coq_tactics.v
iris/proofmode/coq_tactics.v
iris/proofmode/ltac_tactics.v
iris/proofmode/ltac_tactics.v
...
...
iris/proofmode/ltac_tactics.v
View file @
2f748fb4
From
stdpp
Require
Import
namespaces
hlist
pretty
.
From
stdpp
Require
Import
namespaces
hlist
pretty
.
From
iris
.
bi
Require
Export
bi
telescopes
.
From
iris
.
bi
Require
Export
bi
telescopes
.
From
iris
.
proofmode
Require
Import
base
intro_patterns
spec_patterns
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
.
proofmode
Require
Export
classes
notation
.
From
iris
.
prelude
Require
Import
options
.
From
iris
.
prelude
Require
Import
options
.
Export
ident
.
Export
ident
.
...
@@ -1421,30 +1422,6 @@ Tactic Notation "iModCore" constr(H) :=
...
@@ -1421,30 +1422,6 @@ Tactic Notation "iModCore" constr(H) :=
|
iSolveSideCondition
|
iSolveSideCondition
|
pm_reduce
;
pm_prettify
(* subgoal *)
].
|
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
.
(** * Basic destruct tactic *)
(** * Basic destruct tactic *)
(** [pat0] is the unparsed pattern, and is only used in error messages *)
(** [pat0] is the unparsed pattern, and is only used in error messages *)
...
...
iris/proofmode/string_ident.v
0 → 100644
View file @
2f748fb4
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
.
(** [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
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] 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
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
.
(** 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
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
.
tests/proofmode.v
View file @
2f748fb4
...
@@ -1356,14 +1356,6 @@ End error_tests_bi.
...
@@ -1356,14 +1356,6 @@ End error_tests_bi.
Section
pure_name_tests
.
Section
pure_name_tests
.
Context
{
PROP
:
bi
}.
Context
{
PROP
:
bi
}.
Implicit
Types
P
Q
R
:
PROP
.
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"
.
Check
"test_pure_name"
.
Lemma
test_pure_name
P
(
φ
1
φ
2
:
Prop
)
(
Himpl
:
φ
1
→
φ
2
)
:
Lemma
test_pure_name
P
(
φ
1
φ
2
:
Prop
)
(
Himpl
:
φ
1
→
φ
2
)
:
...
...
tests/string_ident.ref
0 → 100644
View file @
2f748fb4
"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))
tests/string_ident.v
0 → 100644
View file @
2f748fb4
From
iris
.
proofmode
Require
Import
string_ident
.
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
.
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
.
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment