forked from coq/coq
-
Notifications
You must be signed in to change notification settings - Fork 0
/
g_rewrite.mlg
348 lines (288 loc) · 14.5 KB
/
g_rewrite.mlg
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
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
(* v * Copyright INRIA, CNRS and contributors *)
(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \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) *)
(************************************************************************)
(* Syntax for rewriting with strategies *)
{
open Names
open Locus
open Constrexpr
open Glob_term
open Genintern
open Geninterp
open Extraargs
open Rewrite
open ComRewrite
open Stdarg
open Tactypes
open Pcoq.Prim
open Pcoq.Constr
open Pvernac.Vernac_
open Pltac
open Vernacextend
}
DECLARE PLUGIN "coq-core.plugins.ltac"
{
type constr_expr_with_bindings = constr_expr with_bindings
type glob_constr_with_bindings = glob_constr_and_expr with_bindings
type glob_constr_with_bindings_sign = interp_sign * glob_constr_and_expr with_bindings
let pr_glob_constr_with_bindings_sign env sigma _ _ _ (ge : glob_constr_with_bindings_sign) =
Printer.pr_glob_constr_env env sigma (fst (fst (snd ge)))
let pr_glob_constr_with_bindings env sigma _ _ _ (ge : glob_constr_with_bindings) =
Printer.pr_glob_constr_env env sigma (fst (fst ge))
let pr_constr_expr_with_bindings env sigma prc _ _ (ge : constr_expr_with_bindings) = prc env sigma (fst ge)
let interp_glob_constr_with_bindings ist _ _ c = (ist, c)
let glob_glob_constr_with_bindings ist l = Tacintern.intern_constr_with_bindings ist l
let subst_glob_constr_with_bindings s c =
Tacsubst.subst_glob_with_bindings s c
}
ARGUMENT EXTEND glob_constr_with_bindings
PRINTED BY { pr_glob_constr_with_bindings_sign env sigma }
INTERPRETED BY { interp_glob_constr_with_bindings }
GLOBALIZED BY { glob_glob_constr_with_bindings }
SUBSTITUTED BY { subst_glob_constr_with_bindings }
RAW_PRINTED BY { pr_constr_expr_with_bindings env sigma }
GLOB_PRINTED BY { pr_glob_constr_with_bindings env sigma }
| [ constr_with_bindings(bl) ] -> { bl }
END
{
let subst_strategy sub = map_strategy
(Tacsubst.subst_glob_constr_and_expr sub)
(Tacsubst.subst_redexp sub)
(fun x -> x)
let pr_strategy _ _ _ (s : strategy) = Pp.str "<strategy>"
let pr_raw_strategy env sigma prc prlc _ (s : Tacexpr.raw_strategy) =
let prr = Pptactic.pr_red_expr env sigma (prc, prlc, Pputils.pr_or_by_notation Libnames.pr_qualid, prc) in
Rewrite.pr_strategy (prc env sigma) prr Pputils.pr_lident s
let pr_glob_strategy env sigma prc prlc _ (s : Tacexpr.glob_strategy) =
let prpat env sigma (_,c,_) = prc env sigma c in
let prcst = Pputils.pr_or_var Pptactic.(pr_and_short_name (pr_evaluable_reference_env env)) in
let prr = Pptactic.pr_red_expr env sigma (prc, prlc, prcst, prpat) in
Rewrite.pr_strategy (prc env sigma) prr Id.print s
}
ARGUMENT EXTEND rewstrategy
PRINTED BY { pr_strategy }
INTERPRETED BY { Tacinterp.interp_strategy }
GLOBALIZED BY { Tacintern.intern_strategy }
SUBSTITUTED BY { subst_strategy }
RAW_PRINTED BY { pr_raw_strategy env sigma }
GLOB_PRINTED BY { pr_glob_strategy env sigma }
END
GRAMMAR EXTEND Gram
GLOBAL: rewstrategy;
rewstrategy:
[ NONA
[ IDENT "fix"; id = identref; ":="; s = rewstrategy1 -> { StratFix (id, s) }
| h = rewstrategy1_list -> { h } ] ]
;
rewstrategy1_list:
[ LEFTA
[ h = SELF; ";"; h' = rewstrategy1 -> { StratBinary (Compose, h, h') }
| h = rewstrategy1 -> { h } ] ]
;
rewstrategy1:
[ RIGHTA
[ "<-"; c = constr -> { StratConstr (c, false) }
| IDENT "subterms"; h = SELF -> { StratUnary (Subterms, h) }
| IDENT "subterm"; h = SELF -> { StratUnary (Subterm, h) }
| IDENT "innermost"; h = SELF -> { StratUnary(Innermost, h) }
| IDENT "outermost"; h = SELF -> { StratUnary(Outermost, h) }
| IDENT "bottomup"; h = SELF -> { StratUnary(Bottomup, h) }
| IDENT "topdown"; h = SELF -> { StratUnary(Topdown, h) }
| IDENT "progress"; h = SELF -> { StratUnary (Progress, h) }
| IDENT "try"; h = SELF -> { StratUnary (Try, h) }
| IDENT "any"; h = SELF -> { StratUnary (Any, h) }
| IDENT "repeat"; h = SELF -> { StratUnary (Repeat, h) }
| IDENT "choice"; h = LIST1 rewstrategy0 -> { StratNAry (Choice, h) }
| IDENT "old_hints"; h = preident -> { StratHints (true, h) }
| IDENT "hints"; h = preident -> { StratHints (false, h) }
| IDENT "terms"; h = LIST0 constr -> { StratTerms h }
| IDENT "eval"; r = red_expr -> { StratEval r }
| IDENT "fold"; c = constr -> { StratFold c }
| h = rewstrategy0 -> { h } ] ]
;
rewstrategy0:
[ NONA
[ c = constr -> { StratConstr (c, true) }
| IDENT "id" -> { StratId }
| IDENT "fail" -> { StratFail }
| IDENT "refl" -> { StratRefl }
| "("; h = rewstrategy; ")" -> { h } ] ]
;
END
(* By default the strategy for "rewrite_db" is top-down *)
{
let db_strat db = StratUnary (Topdown, StratHints (false, db))
let cl_rewrite_clause_db ist db = cl_rewrite_clause_strat (strategy_of_ast (db_strat db))
let cl_rewrite_clause (ist, c) b occ cl =
let c env sigma = Tacinterp.interp_open_constr_with_bindings ist env sigma c in
cl_rewrite_clause c b occ cl
}
TACTIC EXTEND rewrite_strat
| [ "rewrite_strat" rewstrategy(s) "in" hyp(id) ] -> { cl_rewrite_clause_strat s (Some id) }
| [ "rewrite_strat" rewstrategy(s) ] -> { cl_rewrite_clause_strat s None }
| [ "rewrite_db" preident(db) "in" hyp(id) ] -> { cl_rewrite_clause_db ist db (Some id) }
| [ "rewrite_db" preident(db) ] -> { cl_rewrite_clause_db ist db None }
END
{
let clsubstitute o c =
Proofview.Goal.enter begin fun gl ->
let is_tac id = match DAst.get (fst (fst (snd c))) with GVar id' when Id.equal id' id -> true | _ -> false in
let hyps = Tacmach.pf_ids_of_hyps gl in
Tacticals.tclMAP
(fun cl ->
match cl with
| Some id when is_tac id -> Tacticals.tclIDTAC
| _ -> cl_rewrite_clause c o AllOccurrences cl)
(None :: List.map (fun id -> Some id) hyps)
end
}
TACTIC EXTEND substitute
| [ "substitute" orient(o) glob_constr_with_bindings(c) ] -> { clsubstitute o c }
END
(* Compatibility with old Setoids *)
TACTIC EXTEND setoid_rewrite
| [ "setoid_rewrite" orient(o) glob_constr_with_bindings(c) ]
-> { cl_rewrite_clause c o AllOccurrences None }
| [ "setoid_rewrite" orient(o) glob_constr_with_bindings(c) "in" hyp(id) ] ->
{ cl_rewrite_clause c o AllOccurrences (Some id) }
| [ "setoid_rewrite" orient(o) glob_constr_with_bindings(c) "at" occurrences(occ) ] ->
{ cl_rewrite_clause c o (occurrences_of occ) None }
| [ "setoid_rewrite" orient(o) glob_constr_with_bindings(c) "at" occurrences(occ) "in" hyp(id)] ->
{ cl_rewrite_clause c o (occurrences_of occ) (Some id) }
| [ "setoid_rewrite" orient(o) glob_constr_with_bindings(c) "in" hyp(id) "at" occurrences(occ)] ->
{ cl_rewrite_clause c o (occurrences_of occ) (Some id) }
END
{
let declare_relation atts a ?binders aeq n refl symm trans =
declare_relation atts a ?binders aeq n.CAst.v refl symm trans
}
VERNAC COMMAND EXTEND AddRelation CLASSIFIED AS SIDEFF
| #[ atts = rewrite_attributes; ] [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1)
"symmetry" "proved" "by" constr(lemma2) "as" identref(n) ] ->
{ declare_relation atts a aeq n (Some lemma1) (Some lemma2) None }
| #[ atts = rewrite_attributes; ] [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1)
"as" identref(n) ] ->
{ declare_relation atts a aeq n (Some lemma1) None None }
| #[ atts = rewrite_attributes; ] [ "Add" "Relation" constr(a) constr(aeq) "as" identref(n) ] ->
{ declare_relation atts a aeq n None None None }
END
VERNAC COMMAND EXTEND AddRelation2 CLASSIFIED AS SIDEFF
| #[ atts = rewrite_attributes; ] [ "Add" "Relation" constr(a) constr(aeq) "symmetry" "proved" "by" constr(lemma2)
"as" identref(n) ] ->
{ declare_relation atts a aeq n None (Some lemma2) None }
| #[ atts = rewrite_attributes; ] [ "Add" "Relation" constr(a) constr(aeq) "symmetry" "proved" "by" constr(lemma2) "transitivity" "proved" "by" constr(lemma3) "as" identref(n) ] ->
{ declare_relation atts a aeq n None (Some lemma2) (Some lemma3) }
END
VERNAC COMMAND EXTEND AddRelation3 CLASSIFIED AS SIDEFF
| #[ atts = rewrite_attributes; ] [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1)
"transitivity" "proved" "by" constr(lemma3) "as" identref(n) ] ->
{ declare_relation atts a aeq n (Some lemma1) None (Some lemma3) }
| #[ atts = rewrite_attributes; ] [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1)
"symmetry" "proved" "by" constr(lemma2) "transitivity" "proved" "by" constr(lemma3)
"as" identref(n) ] ->
{ declare_relation atts a aeq n (Some lemma1) (Some lemma2) (Some lemma3) }
| #[ atts = rewrite_attributes; ] [ "Add" "Relation" constr(a) constr(aeq) "transitivity" "proved" "by" constr(lemma3)
"as" identref(n) ] ->
{ declare_relation atts a aeq n None None (Some lemma3) }
END
{
type binders_argtype = local_binder_expr list
let wit_binders =
(Genarg.create_arg "binders" : binders_argtype Genarg.uniform_genarg_type)
let binders = Pcoq.create_generic_entry2 "binders" (Genarg.rawwit wit_binders)
let () =
let raw_printer env sigma _ _ _ l = Pp.pr_non_empty_arg (Ppconstr.pr_binders env sigma) l in
Pptactic.declare_extra_vernac_genarg_pprule wit_binders raw_printer
}
GRAMMAR EXTEND Gram
GLOBAL: binders;
binders:
[ [ b = Pcoq.Constr.binders -> { b } ] ];
END
VERNAC COMMAND EXTEND AddParametricRelation CLASSIFIED AS SIDEFF
| #[ atts = rewrite_attributes; ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq)
"reflexivity" "proved" "by" constr(lemma1)
"symmetry" "proved" "by" constr(lemma2) "as" identref(n) ] ->
{ declare_relation atts ~binders:b a aeq n (Some lemma1) (Some lemma2) None }
| #[ atts = rewrite_attributes; ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq)
"reflexivity" "proved" "by" constr(lemma1)
"as" identref(n) ] ->
{ declare_relation atts ~binders:b a aeq n (Some lemma1) None None }
| #[ atts = rewrite_attributes; ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "as" identref(n) ] ->
{ declare_relation atts ~binders:b a aeq n None None None }
END
VERNAC COMMAND EXTEND AddParametricRelation2 CLASSIFIED AS SIDEFF
| #[ atts = rewrite_attributes; ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "symmetry" "proved" "by" constr(lemma2)
"as" identref(n) ] ->
{ declare_relation atts ~binders:b a aeq n None (Some lemma2) None }
| #[ atts = rewrite_attributes; ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "symmetry" "proved" "by" constr(lemma2) "transitivity" "proved" "by" constr(lemma3) "as" identref(n) ] ->
{ declare_relation atts ~binders:b a aeq n None (Some lemma2) (Some lemma3) }
END
VERNAC COMMAND EXTEND AddParametricRelation3 CLASSIFIED AS SIDEFF
| #[ atts = rewrite_attributes; ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1)
"transitivity" "proved" "by" constr(lemma3) "as" identref(n) ] ->
{ declare_relation atts ~binders:b a aeq n (Some lemma1) None (Some lemma3) }
| #[ atts = rewrite_attributes; ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1)
"symmetry" "proved" "by" constr(lemma2) "transitivity" "proved" "by" constr(lemma3)
"as" identref(n) ] ->
{ declare_relation atts ~binders:b a aeq n (Some lemma1) (Some lemma2) (Some lemma3) }
| #[ atts = rewrite_attributes; ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "transitivity" "proved" "by" constr(lemma3)
"as" identref(n) ] ->
{ declare_relation atts ~binders:b a aeq n None None (Some lemma3) }
END
{
let add_setoid atts binders a aeq t n =
add_setoid atts binders a aeq t n.CAst.v
let morphism_tactic =
let open Tacexpr in
let name = "Coq.Classes.SetoidTactics.add_morphism_tactic" in
let tacqid = Libnames.qualid_of_string name in
let tac = CAst.make @@ TacArg (TacCall (CAst.make (tacqid, []))) in
Tacinterp.interp tac
}
VERNAC COMMAND EXTEND AddSetoid1 CLASSIFIED AS SIDEFF
| #[ atts = rewrite_attributes; ] [ "Add" "Setoid" constr(a) constr(aeq) constr(t) "as" identref(n) ] ->
{
add_setoid atts [] a aeq t n
}
| #[ atts = rewrite_attributes; ] [ "Add" "Parametric" "Setoid" binders(binders) ":" constr(a) constr(aeq) constr(t) "as" identref(n) ] ->
{
add_setoid atts binders a aeq t n
}
| #[ atts = rewrite_attributes; ] ![ open_proof ] [ "Add" "Morphism" constr(m) ":" identref(n) ]
=> { VtStartProof(GuaranteesOpacity, [n.CAst.v]) }
-> { if Lib.is_modtype () then
CErrors.user_err Pp.(str "Add Morphism cannot be used in a module type. Use Parameter Morphism instead.");
add_morphism_interactive atts ~tactic:morphism_tactic m n.CAst.v }
| #[ atts = rewrite_attributes; ] [ "Declare" "Morphism" constr(m) ":" identref(n) ]
=> { VtSideff([n.CAst.v], VtLater) }
-> { add_morphism_as_parameter atts m n.CAst.v }
| #[ atts = rewrite_attributes; ] ![ open_proof ] [ "Add" "Morphism" constr(m) "with" "signature" lconstr(s) "as" identref(n) ]
=> { VtStartProof(GuaranteesOpacity,[n.CAst.v]) }
-> { add_morphism atts ~tactic:morphism_tactic [] m s n.CAst.v }
| #[ atts = rewrite_attributes; ] ![ open_proof ] [ "Add" "Parametric" "Morphism" binders(binders) ":" constr(m)
"with" "signature" lconstr(s) "as" identref(n) ]
=> { VtStartProof(GuaranteesOpacity,[n.CAst.v]) }
-> { add_morphism atts ~tactic:morphism_tactic binders m s n.CAst.v }
END
TACTIC EXTEND setoid_symmetry
| [ "setoid_symmetry" ] -> { setoid_symmetry }
| [ "setoid_symmetry" "in" hyp(n) ] -> { setoid_symmetry_in n }
END
TACTIC EXTEND setoid_reflexivity
| [ "setoid_reflexivity" ] -> { setoid_reflexivity }
END
TACTIC EXTEND setoid_transitivity
| [ "setoid_transitivity" constr(t) ] -> { setoid_transitivity (Some t) }
| [ "setoid_etransitivity" ] -> { setoid_transitivity None }
END
VERNAC COMMAND EXTEND PrintRewriteHintDb CLASSIFIED AS QUERY
| [ "Print" "Rewrite" "HintDb" preident(s) ] ->
{ Feedback.msg_notice (Autorewrite.print_rewrite_hintdb s) }
END