blob: ea94e21ff333145879a1c444b9e1ca53f444174d (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
|
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
(* Defines additional productions and edits for use in documentation. Not compiled into Coq *)
DOC_GRAMMAR
(* additional nts to be spliced *)
LEFTQMARK: [
| "?"
]
SPLICE: [
| LEFTQMARK
]
hyp: [
| var
]
tactic_then_gen: [
| EDIT ADD_OPT tactic_expr5 "|" tactic_then_gen
| EDIT ADD_OPT tactic_expr5 ".." tactic_then_last
]
SPLICE: [
| hyp
| identref
| pattern_ident (* depends on previous LEFTQMARK splice todo: improve *)
| constr_eval (* splices as multiple prods *)
| tactic_then_last (* todo: dependency on c.edit_mlg edit?? really useful? *)
| Prim.name
| ltac_selector
| Constr.ident
| tactic_then_locality (* todo: cleanup *)
| attribute_list
]
RENAME: [
(* map missing names for rhs *)
| _binders binders
| Constr.constr term
| Constr.constr_pattern constr_pattern
| Constr.global global
| Constr.lconstr lconstr
| Constr.lconstr_pattern lconstr_pattern
| G_vernac.query_command query_command
| G_vernac.section_subset_expr section_subset_expr
| nonsimple_intropattern intropattern
| Pltac.tactic tactic
| Pltac.tactic_expr ltac_expr
| Prim.ident ident
| Prim.reference reference
| Pvernac.Vernac_.main_entry vernac_control
| Tactic.tactic tactic
| tactic3 ltac_expr3 (* todo: can't figure out how this gets mapped by coqpp *)
| tactic1 ltac_expr1 (* todo: can't figure out how this gets mapped by coqpp *)
| tactic0 ltac_expr0 (* todo: can't figure out how this gets mapped by coqpp *)
| tactic_expr5 ltac_expr
| tactic_expr4 ltac_expr4
| tactic_expr3 ltac_expr3
| tactic_expr2 ltac_expr2
| tactic_expr1 ltac_expr1
| tactic_expr0 ltac_expr0
(* elementary renaming/OCaml-defined productions *)
| clause clause_dft_concl
| in_clause' in_clause
| l_constr lconstr (* todo: should delete the production *)
(* SSR *)
| G_vernac.def_body def_body
| Pcoq.Constr.constr term
| Prim.by_notation by_notation
| Prim.identref ident
| Prim.natural natural
| Vernac.rec_definition rec_definition
(* rename on lhs *)
| intropatterns intropattern_list_opt
| Constr.closed_binder closed_binder
(* historical name *)
| constr term
]
DELETE: [
| check_for_coloneq
| impl_ident_head
| local_test_lpar_id_colon
| lookup_at_as_comma
| only_starredidentrefs
| test_bracket_ident
| test_lpar_id_coloneq
| test_lpar_id_rpar
| test_lpar_idnum_coloneq
| test_show_goal
(* SSR *)
(* | ssr_null_entry *)
| ssrtermkind (* todo: rename as "test..." *)
| term_annotation (* todo: rename as "test..." *)
| test_idcomma
| test_nohidden
| test_not_ssrslashnum
| test_ssr_rw_syntax
| test_ssreqid
| test_ssrfwdid
| test_ssrseqvar
| test_ssrslashnum00
| test_ssrslashnum01
| test_ssrslashnum10
| test_ssrslashnum11
| test_ident_no_do
| ssrdoarg (* todo: this and the next one should be removed from the grammar? *)
| ssrseqdir
]
ident: [
| DELETE IDENT ssr_null_entry
]
natural: [
| DELETE _natural
]
(* added productions *)
empty: [ (* todo: (bug) this is getting converted to empty -> empty *)
|
]
lpar_id_coloneq: [
| "(" IDENT; ":="
]
name_colon: [
| IDENT; ":"
| "_" ":" (* todo: should "_" be a keyword or an identifier? *)
]
int: [ (* todo: probably should be NUMERAL *)
| integer
]
command_entry: [
| noedit_mode
]
binders: [
| DELETE Pcoq.Constr.binders (* todo: not sure why there are 2 "binders:" *)
]
(* edits to simplify *)
ltac_expr1: [
| EDIT match_key ADD_OPT "reverse" "goal" "with" match_context_list "end"
]
match_context_list: [
| EDIT ADD_OPT "|" LIST1 match_context_rule SEP "|"
]
match_hyps: [
| REPLACE name ":=" "[" match_pattern "]" ":" match_pattern
| WITH name ":=" OPT ("[" match_pattern "]" ":") match_pattern
| DELETE name ":=" match_pattern
]
match_list: [
| EDIT ADD_OPT "|" LIST1 match_rule SEP "|"
]
selector_body: [
| REPLACE range_selector_or_nth (* depends on whether range_selector_or_nth is deleted first *)
| WITH LIST1 range_selector SEP ","
]
range_selector_or_nth: [
| DELETENT
]
simple_tactic: [
| DELETE "intros"
| REPLACE "intros" ne_intropatterns
| WITH "intros" intropattern_list_opt
| DELETE "eintros"
| REPLACE "eintros" ne_intropatterns
| WITH "eintros" intropattern_list_opt
]
intropattern_list_opt: [
| DELETE LIST0 intropattern
| intropattern_list_opt intropattern
| empty
]
ne_intropatterns: [
| DELETENT (* todo: don't use DELETENT for this *)
]
or_and_intropattern: [
| DELETE "()"
| DELETE "(" simple_intropattern ")"
| REPLACE "(" simple_intropattern "," LIST1 simple_intropattern SEP "," ")"
| WITH "(" LIST0 simple_intropattern SEP "," ")"
| EDIT "[" USE_NT intropattern_or LIST1 intropattern_list_opt SEP "|" "]"
]
|
