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
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
open Pp
open Util
open Names
open Pcoq
open Constrexpr
open Misctypes
open Tac2expr
open Ltac_plugin
let tac2expr = Tac2entries.Pltac.tac2expr
let tac2type = Gram.entry_create "tactic:tac2type"
let tac2def_val = Gram.entry_create "tactic:tac2def_val"
let tac2def_typ = Gram.entry_create "tactic:tac2def_typ"
let tac2def_ext = Gram.entry_create "tactic:tac2def_ext"
let tac2def_syn = Gram.entry_create "tactic:tac2def_syn"
let tac2mode = Gram.entry_create "vernac:ltac2_command"
let inj_wit wit loc x = CTacExt (loc, Genarg.in_gen (Genarg.rawwit wit) x)
let inj_constr loc c = inj_wit Stdarg.wit_constr loc c
let inj_open_constr loc c = inj_wit Stdarg.wit_open_constr loc c
let inj_ident loc c = inj_wit Stdarg.wit_ident loc c
GEXTEND Gram
GLOBAL: tac2expr tac2type tac2def_val tac2def_typ tac2def_ext tac2def_syn;
tac2pat:
[ "1" LEFTA
[ id = Prim.qualid; pl = LIST1 tac2pat LEVEL "0" -> CPatRef (!@loc, RelId id, pl)
| id = Prim.qualid -> CPatRef (!@loc, RelId id, [])
| "["; "]" -> CPatRef (!@loc, AbsKn Tac2core.Core.c_nil, [])
| p1 = tac2pat; "::"; p2 = tac2pat ->
CPatRef (!@loc, AbsKn Tac2core.Core.c_cons, [p1; p2])
]
| "0"
[ "_" -> CPatAny (!@loc)
| "()" -> CPatTup (Loc.tag ~loc:!@loc [])
| id = Prim.qualid -> CPatRef (!@loc, RelId id, [])
| "("; pl = LIST0 tac2pat LEVEL "1" SEP ","; ")" -> CPatTup (Loc.tag ~loc:!@loc pl) ]
]
;
tac2expr:
[ "5"
[ "fun"; it = LIST1 input_fun ; "=>"; body = tac2expr LEVEL "5" -> CTacFun (!@loc, it, body)
| "let"; isrec = rec_flag;
lc = LIST1 let_clause SEP "with"; "in";
e = tac2expr LEVEL "5" -> CTacLet (!@loc, isrec, lc, e)
| "match"; e = tac2expr LEVEL "5"; "with"; bl = branches ;"end" ->
CTacCse (!@loc, e, bl)
]
| "2" LEFTA
[ e1 = tac2expr; ";"; e2 = tac2expr -> CTacSeq (!@loc, e1, e2) ]
| "1" LEFTA
[ e = tac2expr; el = LIST1 tac2expr LEVEL "0" -> CTacApp (!@loc, e, el)
| e = SELF; ".("; qid = Prim.qualid; ")" -> CTacPrj (!@loc, e, RelId qid)
| e = SELF; ".("; qid = Prim.qualid; ")"; ":="; r = tac2expr LEVEL "1" -> CTacSet (!@loc, e, RelId qid, r)
| e0 = tac2expr; ","; el = LIST1 tac2expr LEVEL "1" SEP "," -> CTacTup (Loc.tag ~loc:!@loc (e0 :: el)) ]
| "0"
[ "("; a = tac2expr LEVEL "5"; ")" -> a
| "("; a = tac2expr; ":"; t = tac2type; ")" -> CTacCnv (!@loc, a, t)
| "()" -> CTacTup (Loc.tag ~loc:!@loc [])
| "("; ")" -> CTacTup (Loc.tag ~loc:!@loc [])
| "["; a = LIST0 tac2expr LEVEL "1" SEP ";"; "]" -> CTacLst (Loc.tag ~loc:!@loc a)
| "{"; a = tac2rec_fieldexprs; "}" -> CTacRec (!@loc, a)
| a = tactic_atom -> a ]
]
;
branches:
[ [ -> []
| "|"; bl = LIST1 branch SEP "|" -> bl
| bl = LIST1 branch SEP "|" -> bl ]
]
;
branch:
[ [ pat = tac2pat LEVEL "1"; "=>"; e = tac2expr LEVEL "5" -> (pat, e) ] ]
;
rec_flag:
[ [ IDENT "rec" -> true
| -> false ] ]
;
typ_param:
[ [ "'"; id = Prim.ident -> id ] ]
;
tactic_atom:
[ [ n = Prim.integer -> CTacAtm (Loc.tag ~loc:!@loc (AtmInt n))
| s = Prim.string -> CTacAtm (Loc.tag ~loc:!@loc (AtmStr s))
| id = Prim.qualid -> CTacRef (RelId id)
| "@"; id = Prim.ident -> inj_ident !@loc id
| "'"; c = Constr.constr -> inj_open_constr !@loc c
| IDENT "constr"; ":"; "("; c = Constr.lconstr; ")" -> inj_constr !@loc c
| IDENT "open_constr"; ":"; "("; c = Constr.lconstr; ")" -> inj_open_constr !@loc c
| IDENT "ident"; ":"; "("; c = Prim.ident; ")" -> inj_ident !@loc c
] ]
;
let_clause:
[ [ id = binder; ":="; te = tac2expr ->
(id, None, te)
| id = binder; args = LIST1 input_fun; ":="; te = tac2expr ->
(id, None, CTacFun (!@loc, args, te)) ] ]
;
tac2type:
[ "5" RIGHTA
[ t1 = tac2type; "->"; t2 = tac2type -> CTypArrow (!@loc, t1, t2) ]
| "2"
[ t = tac2type; "*"; tl = LIST1 tac2type SEP "*" -> CTypTuple (!@loc, t :: tl) ]
| "1" LEFTA
[ t = SELF; qid = Prim.qualid -> CTypRef (!@loc, RelId qid, [t]) ]
| "0"
[ "("; t = tac2type LEVEL "5"; ")" -> t
| id = typ_param -> CTypVar (Loc.tag ~loc:!@loc (Name id))
| "_" -> CTypVar (Loc.tag ~loc:!@loc Anonymous)
| qid = Prim.qualid -> CTypRef (!@loc, RelId qid, [])
| "("; p = LIST1 tac2type LEVEL "5" SEP ","; ")"; qid = Prim.qualid ->
CTypRef (!@loc, RelId qid, p) ]
];
locident:
[ [ id = Prim.ident -> Loc.tag ~loc:!@loc id ] ]
;
binder:
[ [ "_" -> Loc.tag ~loc:!@loc Anonymous
| l = Prim.ident -> Loc.tag ~loc:!@loc (Name l) ] ]
;
input_fun:
[ [ b = tac2pat LEVEL "0" -> (b, None)
| "("; b = tac2pat; t = OPT [ ":"; t = tac2type -> t ]; ")" -> (b, t) ] ]
;
tac2def_body:
[ [ name = binder; it = LIST0 input_fun; ":="; e = tac2expr ->
let e = if List.is_empty it then e else CTacFun (!@loc, it, e) in
(name, e)
] ]
;
tac2def_val:
[ [ isrec = rec_flag; l = LIST1 tac2def_body SEP "with" ->
StrVal (isrec, l)
] ]
;
tac2typ_knd:
[ [ t = tac2type -> CTydDef (Some t)
| "["; ".."; "]" -> CTydOpn
| "["; t = tac2alg_constructors; "]" -> CTydAlg t
| "{"; t = tac2rec_fields; "}"-> CTydRec t ] ]
;
tac2alg_constructors:
[ [ "|"; cs = LIST1 tac2alg_constructor SEP "|" -> cs
| cs = LIST0 tac2alg_constructor SEP "|" -> cs ] ]
;
tac2alg_constructor:
[ [ c = Prim.ident -> (c, [])
| c = Prim.ident; "("; args = LIST0 tac2type SEP ","; ")"-> (c, args) ] ]
;
tac2rec_fields:
[ [ f = tac2rec_field; ";"; l = tac2rec_fields -> f :: l
| f = tac2rec_field; ";" -> [f]
| f = tac2rec_field -> [f]
| -> [] ] ]
;
tac2rec_field:
[ [ mut = [ -> false | IDENT "mutable" -> true]; id = Prim.ident; ":"; t = tac2type -> (id, mut, t) ] ]
;
tac2rec_fieldexprs:
[ [ f = tac2rec_fieldexpr; ";"; l = tac2rec_fieldexprs -> f :: l
| f = tac2rec_fieldexpr; ";" -> [f]
| f = tac2rec_fieldexpr-> [f]
| -> [] ] ]
;
tac2rec_fieldexpr:
[ [ qid = Prim.qualid; ":="; e = tac2expr LEVEL "1" -> RelId qid, e ] ]
;
tac2typ_prm:
[ [ -> []
| id = typ_param -> [Loc.tag ~loc:!@loc id]
| "("; ids = LIST1 [ id = typ_param -> Loc.tag ~loc:!@loc id ] SEP "," ;")" -> ids
] ]
;
tac2typ_def:
[ [ prm = tac2typ_prm; id = Prim.qualid; (r, e) = tac2type_body -> (id, r, (prm, e)) ] ]
;
tac2type_body:
[ [ -> false, CTydDef None
| ":="; e = tac2typ_knd -> false, e
| "::="; e = tac2typ_knd -> true, e
] ]
;
tac2def_typ:
[ [ "Type"; isrec = rec_flag; l = LIST1 tac2typ_def SEP "with" ->
StrTyp (isrec, l)
] ]
;
tac2def_ext:
[ [ "@"; IDENT "external"; id = locident; ":"; t = tac2type LEVEL "5"; ":=";
plugin = Prim.string; name = Prim.string ->
let ml = { mltac_plugin = plugin; mltac_tactic = name } in
StrPrm (id, t, ml)
] ]
;
syn_node:
[ [ "_" -> Loc.tag ~loc:!@loc None
| id = Prim.ident -> Loc.tag ~loc:!@loc (Some id)
] ]
;
sexpr:
[ [ s = Prim.string -> SexprStr (Loc.tag ~loc:!@loc s)
| n = Prim.integer -> SexprInt (Loc.tag ~loc:!@loc n)
| id = syn_node -> SexprRec (!@loc, id, [])
| id = syn_node; "("; tok = LIST1 sexpr SEP "," ; ")" ->
SexprRec (!@loc, id, tok)
] ]
;
syn_level:
[ [ -> None
| ":"; n = Prim.integer -> Some n
] ]
;
tac2def_syn:
[ [ "Notation"; toks = LIST1 sexpr; n = syn_level; ":=";
e = tac2expr ->
StrSyn (toks, n, e)
] ]
;
END
GEXTEND Gram
Pcoq.Constr.operconstr: LEVEL "0"
[ [ IDENT "ltac2"; ":"; "("; tac = tac2expr; ")" ->
let arg = Genarg.in_gen (Genarg.rawwit Tac2env.wit_ltac2) tac in
CAst.make ~loc:!@loc (CHole (None, IntroAnonymous, Some arg)) ] ]
;
END
let pr_ltac2entry _ = mt () (** FIXME *)
let pr_ltac2expr _ = mt () (** FIXME *)
VERNAC ARGUMENT EXTEND ltac2_entry
PRINTED BY pr_ltac2entry
| [ tac2def_val(v) ] -> [ v ]
| [ tac2def_typ(t) ] -> [ t ]
| [ tac2def_ext(e) ] -> [ e ]
| [ tac2def_syn(e) ] -> [ e ]
END
VERNAC COMMAND EXTEND VernacDeclareTactic2Definition CLASSIFIED AS SIDEFF
| [ "Ltac2" ltac2_entry(e) ] -> [
let local = Locality.LocalityFixme.consume () in
Tac2entries.register_struct ?local e
]
END
let _ =
let mode = {
Proof_global.name = "Ltac2";
set = (fun () -> set_command_entry tac2mode);
reset = (fun () -> set_command_entry Pcoq.Vernac_.noedit_mode);
} in
Proof_global.register_proof_mode mode
VERNAC ARGUMENT EXTEND ltac2_expr
PRINTED BY pr_ltac2expr
| [ tac2expr(e) ] -> [ e ]
END
open G_ltac
open Vernac_classifier
VERNAC tac2mode EXTEND VernacLtac2
| [ - ltac2_expr(t) ltac_use_default(default) ] =>
[ classify_as_proofstep ] -> [
(* let g = Option.default (Proof_global.get_default_goal_selector ()) g in *)
Tac2entries.call ~default t
]
END
open Stdarg
VERNAC COMMAND EXTEND Ltac2Print CLASSIFIED AS SIDEFF
| [ "Print" "Ltac2" reference(tac) ] -> [ Tac2entries.print_ltac tac ]
END
|
