Source file vernacextend.ml
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
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
open Util
open Pp
open CErrors
type vernac_keep_as = VtKeepAxiom | VtKeepDefined | VtKeepOpaque
type vernac_qed_type = VtKeep of vernac_keep_as | VtDrop
type vernac_when =
| VtNow
| VtLater
type vernac_classification =
| VtStartProof of vernac_start
| VtSideff of vernac_sideff_type
| VtQed of vernac_qed_type
| VtProofStep of {
proof_block_detection : proof_block_name option
}
| VtQuery
| VtProofMode of Pvernac.proof_mode
| VtMeta
and vernac_start = opacity_guarantee * Names.Id.t list
and vernac_sideff_type = Names.Id.t list * vernac_when
and opacity_guarantee =
| GuaranteesOpacity (** Only generates opaque terms at [Qed] *)
| Doesn'tGuaranteeOpacity (** May generate transparent terms even with [Qed].*)
and solving_tac = bool (** a terminator *)
and anon_abstracting_tac = bool (** abstracting anonymously its result *)
and proof_block_name = string (** open type of delimiters *)
module InProg = struct
type _ t =
| Ignore : unit t
| Use : Declare.OblState.t t
let cast (type a) (x:Declare.OblState.t) (ty:a t) : a =
match ty with
| Ignore -> ()
| Use -> x
end
module OutProg = struct
type _ t =
| No : unit t
| Yes : Declare.OblState.t t
| Push
| Pop
let cast (type a) (x:a) (ty:a t) (orig:Declare.OblState.t NeList.t) : Declare.OblState.t NeList.t =
match ty with
| No -> orig
| Yes -> NeList.map_head (fun _ -> x) orig
| Push -> NeList.push Declare.OblState.empty (Some orig)
| Pop -> (match NeList.tail orig with Some tl -> tl | None -> assert false)
end
module InProof = struct
type _ t =
| Ignore : unit t
| Reject : unit t
| Use : Declare.Proof.t t
| UseOpt : Declare.Proof.t option t
let cast (type a) (x:Declare.Proof.t option) (ty:a t) : a =
match x, ty with
| _, Ignore -> ()
| None, Reject -> ()
| Some _, Reject -> CErrors.user_err (Pp.str "Command not supported (Open proofs remain).")
| Some x, Use -> x
| None, Use -> CErrors.user_err (Pp.str "Command not supported (No proof-editing in progress).")
| _, UseOpt -> x
end
module OutProof = struct
type _ t =
| No : unit t
| Close : unit t
| Update : Declare.Proof.t t
| New : Declare.Proof.t t
end
type ('inprog,'outprog,'inproof,'outproof) vernac_type = {
inprog : 'inprog InProg.t;
outprog : 'outprog InProg.t;
inproof : 'inproof InProof.t;
outproof : 'outproof OutProof.t;
}
type typed_vernac =
TypedVernac : {
inprog : 'inprog InProg.t;
outprog : 'outprog OutProg.t;
inproof : 'inproof InProof.t;
outproof : 'outproof OutProof.t;
run : pm:'inprog -> proof:'inproof -> 'outprog * 'outproof;
} -> typed_vernac
let vtdefault f =
TypedVernac { inprog = Ignore; outprog = No; inproof = Ignore; outproof = No;
run = (fun ~pm:() ~proof:() ->
let () = f () in
(), ()) }
let vtnoproof f =
TypedVernac { inprog = Ignore; outprog = No; inproof = Ignore; outproof = No;
run = (fun ~pm:() ~proof:() ->
let () = f () in
(), ())
}
let vtcloseproof f =
TypedVernac { inprog = Use; outprog = Yes; inproof = Use; outproof = Close;
run = (fun ~pm ~proof ->
let pm = f ~lemma:proof ~pm in
pm, ())
}
let vtopenproof f =
TypedVernac { inprog = Ignore; outprog = No; inproof = Ignore; outproof = New;
run = (fun ~pm:() ~proof:() ->
let proof = f () in
(), proof)
}
let vtmodifyproof f =
TypedVernac { inprog = Ignore; outprog = No; inproof = Use; outproof = Update;
run = (fun ~pm:() ~proof ->
let proof = f ~pstate:proof in
(), proof)
}
let vtreadproofopt f =
TypedVernac { inprog = Ignore; outprog = No; inproof = UseOpt; outproof = No;
run = (fun ~pm:() ~proof ->
let () = f ~pstate:proof in
(), ())
}
let vtreadproof f =
TypedVernac { inprog = Ignore; outprog = No; inproof = Use; outproof = No;
run = (fun ~pm:() ~proof ->
let () = f ~pstate:proof in
(), ())
}
let vtreadprogram f =
TypedVernac { inprog = Use; outprog = No; inproof = Ignore; outproof = No;
run = (fun ~pm ~proof:() ->
let () = f ~pm in
(), ())
}
let vtmodifyprogram f =
TypedVernac { inprog = Use; outprog = Yes; inproof = Ignore; outproof = No;
run = (fun ~pm ~proof:() ->
let pm = f ~pm in
pm, ())
}
let vtdeclareprogram f =
TypedVernac { inprog = Use; outprog = No; inproof = Ignore; outproof = New;
run = (fun ~pm ~proof:() ->
let proof = f ~pm in
(), proof)
}
let vtopenproofprogram f =
TypedVernac { inprog = Use; outprog = Yes; inproof = Ignore; outproof = New;
run = (fun ~pm ~proof:() ->
let pm, proof = f ~pm in
pm, proof)
}
type vernac_command = ?loc:Loc.t -> atts:Attributes.vernac_flags -> unit -> typed_vernac
type plugin_args = Genarg.raw_generic_argument list
let vernac_tab =
(Hashtbl.create 211 :
(Vernacexpr.extend_name, bool * (plugin_args -> vernac_command)) Hashtbl.t)
let vinterp_add depr s f =
try
Hashtbl.add vernac_tab s (depr, f)
with Failure _ ->
user_err
(str"Cannot add the vernac command " ++ str (fst s) ++ str" twice.")
let vinterp_map s =
try
Hashtbl.find vernac_tab s
with Failure _ | Not_found ->
user_err
(str"Cannot find vernac command " ++ str (fst s) ++ str".")
let warn_deprecated_command =
let open CWarnings in
create ~name:"deprecated-command" ~category:"deprecated"
(fun pr -> str "Deprecated vernacular command: " ++ pr)
let type_vernac opn converted_args ?loc ~atts () =
let depr, callback = vinterp_map opn in
let () = if depr then
let rules = Egramml.get_extend_vernac_rule opn in
let pr_gram = function
| Egramml.GramTerminal s -> str s
| Egramml.GramNonTerminal _ -> str "_"
in
let pr = pr_sequence pr_gram rules in
warn_deprecated_command pr;
in
let hunk = callback converted_args in
hunk ?loc ~atts ()
(** VERNAC EXTEND registering *)
type classifier = Genarg.raw_generic_argument list -> vernac_classification
(** Classifiers *)
let classifiers : classifier array String.Map.t ref = ref String.Map.empty
let get_vernac_classifier (name, i) args =
(String.Map.find name !classifiers).(i) args
let declare_vernac_classifier name f =
classifiers := String.Map.add name f !classifiers
let classify_as_query = VtQuery
let classify_as_sideeff = VtSideff ([], VtLater)
let classify_as_proofstep = VtProofStep { proof_block_detection = None}
type (_, _) ty_sig =
| TyNil : (vernac_command, vernac_classification) ty_sig
| TyTerminal : string * ('r, 's) ty_sig -> ('r, 's) ty_sig
| TyNonTerminal : ('a, 'b, 'c) Extend.ty_user_symbol * ('r, 's) ty_sig -> ('a -> 'r, 'a -> 's) ty_sig
type ty_ml = TyML : bool * ('r, 's) ty_sig * 'r * 's option -> ty_ml
let type_error () = CErrors.anomaly (Pp.str "Ill-typed VERNAC EXTEND")
let rec untype_classifier : type r s. (r, s) ty_sig -> s -> classifier = function
| TyNil -> fun f args ->
begin match args with
| [] -> f
| _ :: _ -> type_error ()
end
| TyTerminal (_, ty) -> fun f args -> untype_classifier ty f args
| TyNonTerminal (tu, ty) -> fun f args ->
let open Genarg in
begin match args with
| [] -> type_error ()
| GenArg (Rawwit tag, v) :: args ->
match Genarg.genarg_type_eq tag (Egramml.proj_symbol tu) with
| None -> type_error ()
| Some Refl -> untype_classifier ty (f v) args
end
(** Stupid GADTs forces us to duplicate the definition just for typing *)
let rec untype_command : type r s. (r, s) ty_sig -> r -> plugin_args -> vernac_command = function
| TyNil -> fun f args ->
begin match args with
| [] -> f
| _ :: _ -> type_error ()
end
| TyTerminal (_, ty) -> fun f args -> untype_command ty f args
| TyNonTerminal (tu, ty) -> fun f args ->
let open Genarg in
begin match args with
| [] -> type_error ()
| GenArg (Rawwit tag, v) :: args ->
match genarg_type_eq tag (Egramml.proj_symbol tu) with
| None -> type_error ()
| Some Refl -> untype_command ty (f v) args
end
let rec untype_user_symbol : type s a b c. (a, b, c) Extend.ty_user_symbol -> (s, Gramlib.Grammar.norec, a) Pcoq.Symbol.t =
let open Extend in function
| TUlist1 l -> Pcoq.Symbol.list1 (untype_user_symbol l)
| TUlist1sep (l, s) -> Pcoq.Symbol.list1sep (untype_user_symbol l) (Pcoq.Symbol.tokens [Pcoq.TPattern (CLexer.terminal s)]) false
| TUlist0 l -> Pcoq.Symbol.list0 (untype_user_symbol l)
| TUlist0sep (l, s) -> Pcoq.Symbol.list0sep (untype_user_symbol l) (Pcoq.Symbol.tokens [Pcoq.TPattern (CLexer.terminal s)]) false
| TUopt o -> Pcoq.Symbol.opt (untype_user_symbol o)
| TUentry a -> Pcoq.Symbol.nterm (Pcoq.genarg_grammar (Genarg.ExtraArg a))
| TUentryl (a, i) -> Pcoq.Symbol.nterml (Pcoq.genarg_grammar (Genarg.ExtraArg a)) (string_of_int i)
let rec untype_grammar : type r s. (r, s) ty_sig -> 'a Egramml.grammar_prod_item list = function
| TyNil -> []
| TyTerminal (tok, ty) -> Egramml.GramTerminal tok :: untype_grammar ty
| TyNonTerminal (tu, ty) ->
let t = Genarg.rawwit (Egramml.proj_symbol tu) in
let symb = untype_user_symbol tu in
Egramml.GramNonTerminal (Loc.tag (t, symb)) :: untype_grammar ty
let vernac_extend ?plugin ~command ?classifier ?entry ext =
let get_classifier (TyML (_, ty, _, cl)) = match cl with
| Some cl -> untype_classifier ty cl
| None ->
match classifier with
| Some cl -> fun _ -> cl command
| None ->
let e = match entry with
| None -> "COMMAND"
| Some e -> Pcoq.Entry.name e
in
let msg = Printf.sprintf "\
Vernac entry \"%s\" misses a classifier. \
A classifier is a function that returns an expression \
of type vernac_classification (see Vernacexpr). You can: \n\
- Use '... EXTEND %s CLASSIFIED AS QUERY ...' if the \
new vernacular command does not alter the system state;\n\
- Use '... EXTEND %s CLASSIFIED AS SIDEFF ...' if the \
new vernacular command alters the system state but not the \
parser nor it starts a proof or ends one;\n\
- Use '... EXTEND %s CLASSIFIED BY f ...' to specify \
a global function f. The function f will be called passing\
\"%s\" as the only argument;\n\
- Add a specific classifier in each clause using the syntax:\n\
'[...] => [ f ] -> [...]'.\n\
Specific classifiers have precedence over global \
classifiers. Only one classifier is called."
command e e e command
in
CErrors.user_err (Pp.strbrk msg)
in
let cl = Array.map_of_list get_classifier ext in
let iter i (TyML (depr, ty, f, _)) =
let f = untype_command ty f in
let r = untype_grammar ty in
let () = vinterp_add depr (command, i) f in
let () =
Egramml.declare_vernac_command_grammar ~allow_override:(Option.is_empty plugin)
(command, i) entry r
in
let () = match plugin with
| None -> Egramml.extend_vernac_command_grammar ~undoable:false (command, i)
| Some plugin ->
Mltop.add_init_function plugin (fun () ->
Egramml.extend_vernac_command_grammar ~undoable:true (command, i))
in
()
in
let () = declare_vernac_classifier command cl in
let () = List.iteri iter ext in
()
(** VERNAC ARGUMENT EXTEND registering *)
type 'a argument_rule =
| Arg_alias of 'a Pcoq.Entry.t
| Arg_rules of 'a Pcoq.Production.t list
type 'a vernac_argument = {
arg_printer : Environ.env -> Evd.evar_map -> 'a -> Pp.t;
arg_parsing : 'a argument_rule;
}
let vernac_argument_extend ~plugin ~name arg =
let wit = Genarg.create_arg name in
let entry = match arg.arg_parsing with
| Arg_alias e ->
let () = Pcoq.register_grammar wit e in
e
| Arg_rules rules ->
let e = Pcoq.create_generic_entry2 name (Genarg.rawwit wit) in
let plugin_uid = (plugin, "vernacargextend:"^name) in
let () = Egramml.grammar_extend ~plugin_uid e
(Pcoq.Fresh (Gramlib.Gramext.First, [None, None, rules]))
in
e
in
let pr = arg.arg_printer in
let pr x = Genprint.PrinterBasic (fun env sigma -> pr env sigma x) in
let () = Genprint.register_vernac_print0 wit pr in
(wit, entry)