Source file synterp.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
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
open Pp
open CErrors
open CAst
open Util
open Names
open Libnames
open Vernacexpr
open Locality
open Attributes
let proof_mode_opt_name = ["Default";"Proof";"Mode"]
let { Goptions.get = get_default_proof_mode } =
Goptions.declare_interpreted_string_option_and_ref
~stage:Summary.Stage.Synterp
~key:proof_mode_opt_name
~value:(Pvernac.register_proof_mode "Noedit" Pvernac.Vernac_.noedit_mode)
(fun name -> match Pvernac.lookup_proof_mode name with
| Some pm -> pm
| None -> CErrors.user_err Pp.(str (Format.sprintf "No proof mode named \"%s\"." name)))
Pvernac.proof_mode_to_string
()
let module_locality = Attributes.Notations.(locality >>= fun l -> return (make_module_locality l))
let with_locality ~atts f =
let local = Attributes.(parse locality atts) in
f ~local
let with_module_locality ~atts f =
let module_local = Attributes.(parse module_locality atts) in
f ~module_local
let warn_legacy_export_set =
CWarnings.create ~name:"legacy-export-set" ~category:Deprecation.Version.v8_18
Pp.(fun () -> strbrk "Syntax \"Export Set\" is deprecated, use the attribute syntax \"#[export] Set\" instead.")
let deprecated_nonuniform =
CWarnings.create ~name:"deprecated-nonuniform-attribute"
~category:Deprecation.Version.v8_18
Pp.(fun () -> strbrk "Attribute '#[nonuniform]' is deprecated, \
use '#[warning=\"-uniform-inheritance\"]' instead.")
let warnings_att =
Attributes.attribute_of_list [
"warnings", Attributes.payload_parser ~cat:(^) ~name:"warnings";
"warning", Attributes.payload_parser ~cat:(^) ~name:"warning";
]
let with_generic_atts ~check atts f =
let atts, warnings = Attributes.parse_with_extra warnings_att atts in
let atts, nonuniform = Attributes.parse_with_extra ComCoercion.nonuniform atts in
let warnings =
let () = if nonuniform <> None && check then deprecated_nonuniform () in
if nonuniform <> Some true then warnings else
let ui = "-uniform-inheritance" in
Some (match warnings with Some w -> w ^ "," ^ ui | None -> ui) in
match warnings with
| None -> f ~atts
| Some warnings ->
if check then CWarnings.check_unknown_warnings warnings;
CWarnings.with_warn warnings (fun () -> f ~atts) ()
type module_entry = Modintern.module_struct_expr * Names.ModPath.t * Modintern.module_kind * Entries.inline
type synterp_entry =
| EVernacNoop
| EVernacNotation of { local : bool; decl : Metasyntax.notation_interpretation_decl }
| EVernacBeginSection of lident
| EVernacEndSegment of lident
| EVernacRequire of
Library.library_t list * DirPath.t list * export_with_cats option * (qualid * import_filter_expr) list
| EVernacImport of (export_flag *
Libobject.open_filter) *
(Names.ModPath.t CAst.t * import_filter_expr) list
| EVernacDeclareModule of Lib.export * lident *
Declaremods.module_params_expr *
module_entry
| EVernacDefineModule of Lib.export * lident *
Declaremods.module_params_expr *
((export_flag * Libobject.open_filter) * Names.ModPath.t) list *
module_entry Declaremods.module_signature *
module_entry list
| EVernacDeclareModuleType of lident *
Declaremods.module_params_expr *
((export_flag * Libobject.open_filter) * Names.ModPath.t) list *
module_entry list *
module_entry list
| EVernacInclude of Declaremods.module_expr list
| EVernacSetOption of { export : bool; key : Goptions.option_name; value : Vernacexpr.option_setting }
| EVernacLoad of Vernacexpr.verbose_flag * (vernac_control_entry * Vernacstate.Synterp.t) list
| EVernacExtend of Vernactypes.typed_vernac
and vernac_entry = synterp_entry Vernacexpr.vernac_expr_gen
and vernac_control_entry =
(Vernacstate.Synterp.t VernacControl.control_entry, synterp_entry)
Vernacexpr.vernac_control_gen_r CAst.t
let synterp_reserved_notation ~module_local ~infix l =
Metasyntax.add_reserved_notation ~local:module_local ~infix l
let synterp_custom_entry ~module_local s =
Metasyntax.declare_custom_entry module_local s
let import_module_syntax_with_filter ~export cats m f =
match f with
| ImportAll -> Declaremods.Synterp.import_module cats ~export m
| ImportNames ns -> ()
let synterp_import_mod (export,cats) qid f =
let loc = qid.loc in
let m = try Nametab.locate_module qid
with Not_found ->
CErrors.user_err ?loc Pp.(str "Cannot find module " ++ pr_qualid qid)
in
import_module_syntax_with_filter ~export cats m f; m
let synterp_import_cats cats =
Option.cata
(fun cats -> Libobject.make_filter ~finite:(not cats.negative) cats.import_cats)
Libobject.unfiltered
cats
let check_no_filter_when_using_cats l =
List.iter (function
| _, ImportAll -> ()
| q, ImportNames _ ->
CErrors.user_err ?loc:q.loc
Pp.(str "Cannot combine importing by categories and importing by names."))
l
let synterp_import export refl =
if Option.has_some (snd export) then check_no_filter_when_using_cats refl;
let export = on_snd synterp_import_cats export in
export, List.map (fun (qid,f) -> CAst.make ?loc:qid.loc @@ synterp_import_mod export qid f, f) refl
let synterp_define_module export {loc;v=id} (binders_ast : module_binder list) mty_ast_o mexpr_ast_l =
if Lib.sections_are_opened () then
user_err Pp.(str "Modules and Module Types are not allowed inside sections.");
let export = Option.map (on_snd synterp_import_cats) export in
match mexpr_ast_l with
| [] ->
let binders_ast,argsexport =
List.fold_right
(fun (export,idl,ty) (args,argsexport) ->
(idl,ty)::args, (List.map (fun {v=i} -> Option.map (on_snd synterp_import_cats) export,i)idl)@argsexport) binders_ast
([],[]) in
let mp, args, sign = Declaremods.Synterp.start_module export id binders_ast mty_ast_o in
let argsexports = List.map_filter
(fun (export,id) ->
Option.map (fun export ->
export, synterp_import_mod export (qualid_of_ident id) ImportAll
) export
) argsexport
in
export, args, argsexports, [], sign
| _::_ ->
let binders_ast = List.map
(fun (export,idl,ty) ->
if not (Option.is_empty export) then
user_err Pp.(str "Arguments of a functor definition can be imported only if the definition is interactive. Remove the \"Export\" and \"Import\" keywords from every functor argument.")
else (idl,ty)) binders_ast in
let mp, args, expr, sign =
Declaremods.Synterp.declare_module
id binders_ast mty_ast_o mexpr_ast_l
in
Option.iter (fun (export,cats) ->
ignore (synterp_import_mod (export,cats) (qualid_of_ident id) ImportAll)) export;
export, args, [], expr, sign
let synterp_declare_module_type_syntax {loc;v=id} binders_ast mty_sign mty_ast_l =
if Lib.sections_are_opened () then
user_err Pp.(str "Modules and Module Types are not allowed inside sections.");
match mty_ast_l with
| [] ->
let binders_ast,argsexport =
List.fold_right
(fun (export,idl,ty) (args,argsexport) ->
(idl,ty)::args, (List.map (fun {v=i} -> Option.map (on_snd synterp_import_cats) export,i)idl)@argsexport) binders_ast
([],[]) in
let mp, args, sign = Declaremods.Synterp.start_modtype id binders_ast mty_sign in
let argsexport =
List.map_filter
(fun (export,id) ->
Option.map
(fun export -> export, synterp_import_mod export (qualid_of_ident ?loc id) ImportAll) export
) argsexport
in
args, argsexport, [], sign
| _ :: _ ->
let binders_ast = List.map
(fun (export,idl,ty) ->
if not (Option.is_empty export) then
user_err Pp.(str "Arguments of a functor definition can be imported only if the definition is interactive. Remove the \"Export\" and \"Import\" keywords from every functor argument.")
else (idl,ty)) binders_ast in
let mp, args, expr, sign = Declaremods.Synterp.declare_modtype id binders_ast mty_sign mty_ast_l in
args, [], expr, sign
let synterp_declare_module export {loc;v=id} binders_ast mty_ast =
let binders_ast = List.map
(fun (export,idl,ty) ->
if not (Option.is_empty export) then
user_err Pp.(str "Arguments of a functor declaration cannot be exported. Remove the \"Export\" and \"Import\" keywords from every functor argument.")
else (idl,ty)) binders_ast in
let mp, args, expr, sign =
Declaremods.Synterp.declare_module id binders_ast (Declaremods.Enforce mty_ast) []
in
assert (List.is_empty expr);
let sign = match sign with Declaremods.Enforce x -> x | _ -> assert false in
let export = Option.map (on_snd synterp_import_cats) export in
Option.iter (fun export -> ignore @@ synterp_import_mod export (qualid_of_ident id) ImportAll) export;
mp, export, args, sign
let synterp_include l = Declaremods.Synterp.declare_include l
let synterp_end_module export {loc;v=id} =
let _ = Declaremods.Synterp.end_module () in
Option.map (fun export -> synterp_import_mod export (qualid_of_ident ?loc id) ImportAll) export
let synterp_end_section {CAst.loc; v} =
Dumpglob.dump_reference ?loc
(DirPath.to_string (Lib.current_dirpath true)) "<>" "sec";
Declaremods.Synterp.close_section ()
let synterp_end_segment ({v=id;loc} as lid) =
let ss = Lib.Synterp.find_opening_node ?loc id in
match ss with
| Lib.OpenedModule (false,export,_,_) -> ignore (synterp_end_module export lid)
| Lib.OpenedModule (true,_,_,_) -> ignore (Declaremods.Synterp.end_modtype ())
| Lib.OpenedSection _ -> synterp_end_section lid
| _ -> assert false
let err_unmapped_library ?from qid =
let prefix = match from with
| None -> mt ()
| Some from ->
str " with prefix " ++ DirPath.print from
in
strbrk "Cannot find a physical path bound to logical path "
++ pr_qualid qid ++ prefix ++ str "."
let err_notfound_library ?from qid =
let prefix = match from with
| None -> mt ()
| Some from -> str " with prefix " ++ DirPath.print from
in
let bonus =
if !Flags.load_vos_libraries then mt ()
else str " (while searching for a .vos file)"
in
strbrk "Unable to locate library " ++ pr_qualid qid ++ prefix ++ bonus
++ str "."
exception UnmappedLibrary of Names.DirPath.t option * Libnames.qualid
exception NotFoundLibrary of Names.DirPath.t option * Libnames.qualid
let _ = CErrors.register_handler begin function
| UnmappedLibrary (from, qid) -> Some (err_unmapped_library ?from qid)
| NotFoundLibrary (from, qid) -> Some (err_notfound_library ?from qid)
| _ -> None
end
let warn_deprecated_from_Coq =
CWarnings.create_with_quickfix ~name:"deprecated-from-Coq"
~category:Deprecation.Version.v9_0
(fun () -> strbrk
"\"From Coq\" has been replaced by \"From Stdlib\".")
let deprecated_Coq from qidl =
let coq_id = Id.of_string "Coq" in
let stdlib_id =
let qidl =
let qid2idl qid =
let p, id = Libnames.repr_qualid qid in
List.rev (id :: DirPath.repr p) in
let from = match from with None -> [] | Some from -> qid2idl from in
List.map (fun (qid, _) -> from @ qid2idl qid) qidl in
let ids' = List.map Id.of_string ["Init"; "Setoids"; "Ltac"] in
let in_rocq idl = match idl with
| id :: id' :: _ -> Id.equal id coq_id && (CList.mem_f Id.equal id' ids')
| _ -> false in
Id.of_string (if List.for_all in_rocq qidl then "Corelib" else "Stdlib") in
let repl_id id =
if Id.equal id coq_id then true, stdlib_id else false, id in
let repl_Coq_qid qid =
let p, id = Libnames.repr_qualid qid in
let warn, p, id =
if DirPath.is_empty p then let w, id = repl_id id in w, p, id else
let warn, p = match List.rev (DirPath.repr p) with
| id :: p' -> let w, id' = repl_id id in w, (id' :: p')
| [] -> false, [] in
warn, DirPath.make (List.rev p), id in
let qid = Libnames.make_qualid ?loc:qid.loc p id in
let warn = if warn then Some qid else None in
warn, Libnames.make_qualid ?loc:qid.loc p id in
let warn, from, qidl = match from with
| Some from -> let w, from = repl_Coq_qid from in w, Some from, qidl
| None ->
let w, qidl = CList.fold_left_map (fun w (qid, fe) ->
let w', qid = repl_Coq_qid qid in Option.append w w', (qid, fe))
None qidl in
w, from, qidl in
let () = match warn with None -> () | Some qid ->
let quickfix = Option.map (fun loc ->
[Quickfix.make ~loc (Libnames.pr_qualid qid)]) qid.loc in
warn_deprecated_from_Coq ?quickfix () in
from, qidl
let synterp_require ~intern from export qidl =
let from, qidl = deprecated_Coq from qidl in
let root = match from with
| None -> None
| Some from ->
let (hd, tl) = Libnames.repr_qualid from in
Some (Libnames.add_dirpath_suffix hd tl)
in
let locate (qid,_) =
let open Loadpath in
match locate_qualified_library ?root qid with
| Ok (dir,_) -> (qid.loc, dir)
| Error LibUnmappedDir -> Loc.raise ?loc:qid.loc (UnmappedLibrary (root, qid))
| Error LibNotFound -> Loc.raise ?loc:qid.loc (NotFoundLibrary (root, qid))
in
let modrefl = List.map locate qidl in
let filenames = Library.require_library_syntax_from_dirpath ~intern modrefl in
Option.iter (fun (export,cats) ->
let cats = synterp_import_cats cats in
List.iter2 (fun (_, m) (_, f) ->
import_module_syntax_with_filter ~export cats (MPfile m) f)
modrefl qidl)
export;
filenames, List.map snd modrefl
let expand filename =
Envars.expand_path_macros ~warn:(fun x -> Feedback.msg_warning (str x)) filename
let synterp_declare_ml_module ~local l =
let local = Option.default false local in
Mltop.declare_ml_modules local l
let warn_chdir = CWarnings.create ~name:"change-dir-deprecated" ~category:Deprecation.Version.v8_20
(fun () -> strbrk "Command \"Cd\" is deprecated." ++ spc () ++
strbrk "Use command-line \"-output-directory dir\" instead, or, alternatively, " ++
strbrk "for extraction, \"Set Extraction Output Directory\".")
let synterp_chdir = function
| None -> Feedback.msg_notice (str (Sys.getcwd()))
| Some path ->
warn_chdir ();
begin
try Sys.chdir (expand path)
with Sys_error err ->
user_err Pp.(str ("Cd failed: " ^ err))
end;
Flags.if_verbose Feedback.msg_info (str (Sys.getcwd()))
let ?loc from file id =
if Lib.sections_are_opened () then
user_err ?loc Pp.(str "Extra Dependencies cannot be declared inside sections.");
let hd, tl = Libnames.repr_qualid from in
let from = Libnames.add_dirpath_suffix hd tl in
ComExtraDeps.declare_extra_dep ?loc ~from ~file id
let synterp_begin_section ({v=id} as lid) =
Dumpglob.dump_definition lid true "sec";
Lib.Synterp.open_section id
let with_synterp_state =
let with_local_state () f =
let st = Vernacstate.Synterp.freeze () in
let v = f () in
let transient_st = Vernacstate.Synterp.freeze () in
Vernacstate.Synterp.unfreeze st;
transient_st, v
in
{ VernacControl.with_local_state }
let rec synterp ~intern ?loc ~atts v =
match v with
| VernacSynterp v0 ->
let e = begin match v0 with
| VernacReservedNotation (infix, sl) ->
with_module_locality ~atts synterp_reserved_notation ~infix sl;
EVernacNoop
| VernacNotation (infix,ntn_decl) ->
let local, user_warns = Attributes.(parse Notations.(module_locality ++ user_warns) atts) in
let decl = Metasyntax.add_notation_syntax ~local ~infix user_warns ntn_decl in
EVernacNotation { local; decl }
| VernacDeclareCustomEntry s ->
with_module_locality ~atts synterp_custom_entry s;
EVernacNoop
| VernacDefineModule (export,lid,bl,mtys,mexprl) ->
let export, args, argsexport, expr, sign = synterp_define_module export lid bl mtys mexprl in
EVernacDefineModule (export,lid,args,argsexport,sign,expr)
| VernacDeclareModuleType (lid,bl,mtys,mtyo) ->
let args, argsexport, expr, sign = synterp_declare_module_type_syntax lid bl mtys mtyo in
EVernacDeclareModuleType (lid,args,argsexport,sign,expr)
| VernacDeclareModule (export,lid,bl,mtyo) ->
let mp, export, args, sign =
synterp_declare_module export lid bl mtyo
in
EVernacDeclareModule (export,lid,args,sign)
| VernacInclude in_asts ->
EVernacInclude (synterp_include in_asts)
| VernacBeginSection lid ->
synterp_begin_section lid;
EVernacBeginSection lid
| VernacEndSegment lid ->
synterp_end_segment lid;
EVernacEndSegment lid
| VernacRequire (from, export, qidl) ->
let needed, modrefl = synterp_require ~intern from export qidl in
EVernacRequire (needed, modrefl, export, qidl)
| VernacImport (export,qidl) ->
let export, mpl = synterp_import export qidl in
EVernacImport (export,mpl)
| VernacDeclareMLModule l ->
with_locality ~atts synterp_declare_ml_module l;
EVernacNoop
| VernacChdir s ->
unsupported_attributes atts;
synterp_chdir s;
EVernacNoop
| VernacExtraDependency(from,file,id) ->
unsupported_attributes atts;
synterp_extra_dep ?loc from file id;
EVernacNoop
| VernacSetOption (export,key,value) ->
let atts = if export then begin
warn_legacy_export_set ?loc ();
CAst.make ?loc ("export", VernacFlagEmpty) :: atts
end
else atts
in
let locality = parse option_locality atts in
Vernacoptions.vernac_set_option ~locality ~stage:Summary.Stage.Synterp key value;
EVernacSetOption { export; key; value }
| VernacProofMode mn ->
unsupported_attributes atts;
EVernacNoop
| VernacLoad (verbosely, fname) ->
unsupported_attributes atts;
synterp_load ~intern verbosely fname
| VernacExtend (opn,args) ->
let f = Vernacextend.type_vernac ?loc ~atts opn args () in
EVernacExtend(f)
end in
VernacSynterp e
| VernacSynPure x -> VernacSynPure x
and synterp_load ~intern verbosely fname =
let fname =
Envars.expand_path_macros ~warn:(fun x -> Feedback.msg_warning (Pp.str x)) fname in
let fname = CUnix.make_suffix fname ".v" in
let input =
let longfname = Loadpath.locate_file fname in
let in_chan = Util.open_utf8_file_in longfname in
Procq.Parsable.make ~loc:Loc.(initial (InFile { dirpath=None; file=longfname}))
(Gramlib.Stream.of_channel in_chan) in
let v_mod = if verbosely then Flags.verbosely else Flags.silently in
let parse_sentence proof_mode =
Procq.Entry.parse (Pvernac.main_entry proof_mode)
in
let proof_mode = Some (get_default_proof_mode ()) in
let rec load_loop entries =
match parse_sentence proof_mode input with
| None -> entries
| Some cmd ->
let entry = v_mod (synterp_control ~intern) cmd in
let st = Vernacstate.Synterp.freeze () in
(load_loop [@ocaml.tailcall]) ((entry,st)::entries)
in
let entries = List.rev @@ load_loop [] in
EVernacLoad(verbosely, entries)
and synterp_control ~intern CAst.{ loc; v = cmd } =
let fn expr =
with_generic_atts ~check:true cmd.attrs (fun ~atts ->
synterp ~intern ?loc ~atts cmd.expr)
in
let control, expr =
VernacControl.under_control ~loc ~with_local_state:with_synterp_state
(VernacControl.from_syntax cmd.control)
~noop:(VernacSynterp EVernacNoop)
(fun () -> fn cmd.expr)
in
CAst.make ?loc { expr; control; attrs = cmd.attrs }
let synterp_control ~intern cmd =
Flags.with_option Flags.in_synterp_phase (synterp_control ~intern) cmd