-
Notifications
You must be signed in to change notification settings - Fork 632
/
vernacentries.ml
2496 lines (2231 loc) · 92.4 KB
/
vernacentries.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
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
(************************************************************************)
(* * 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) *)
(************************************************************************)
(* Concrete syntax of the mathematical vernacular MV V2.6 *)
open Pp
open CErrors
open CAst
open Util
open Names
open Printer
open Goptions
open Libnames
open Vernacexpr
open Locality
open Attributes
open Synterp
module NamedDecl = Context.Named.Declaration
(** TODO: make this function independent of Ltac *)
let (f_interp_redexp, interp_redexp_hook) = Hook.make ()
(* Utility functions, at some point they should all disappear and
instead enviroment/state selection should be done at the Vernac DSL
level. *)
let get_current_or_global_context ~pstate =
match pstate with
| None -> let env = Global.env () in Evd.(from_env env, env)
| Some p -> Declare.Proof.get_current_context p
let get_goal_or_global_context ~pstate glnum =
match pstate with
| None -> let env = Global.env () in Evd.(from_env env, env)
| Some p -> Declare.Proof.get_goal_context p glnum
let cl_of_qualid = function
| FunClass -> Coercionops.CL_FUN
| SortClass -> Coercionops.CL_SORT
| RefClass r -> ComCoercion.class_of_global (Smartlocate.smart_global ~head:true r)
let scope_class_of_qualid qid =
Notation.scope_class_of_class (cl_of_qualid qid)
(*******************)
(* "Show" commands *)
let show_proof ~pstate =
(* spiwack: this would probably be cooler with a bit of polishing. *)
try
let pstate = Option.get pstate in
let p = Declare.Proof.get pstate in
let sigma, _ = Declare.Proof.get_current_context pstate in
let pprf = Proof.partial_proof p in
(* In the absence of an environment explicitly attached to the
proof and on top of which side effects of the proof would be pushed, ,
we take the global environment which in practise should be a
superset of the initial environment in which the proof was
started *)
let env = Global.env() in
Pp.prlist_with_sep Pp.fnl (Printer.pr_econstr_env env sigma) pprf
(* We print nothing if there are no goals left *)
with
| Proof.NoSuchGoal _
| Option.IsNone ->
user_err (str "No goals to show.")
let show_top_evars ~proof =
(* spiwack: new as of Feb. 2010: shows goal evars in addition to non-goal evars. *)
let Proof.{goals; sigma} = Proof.data proof in
let shelf = Evd.shelf sigma in
let given_up = Evar.Set.elements @@ Evd.given_up sigma in
pr_evars_int sigma ~shelf ~given_up 1 (Evd.undefined_map sigma)
let show_universes ~proof =
let Proof.{goals;sigma} = Proof.data proof in
let ctx = Evd.universe_context_set (Evd.minimize_universes sigma) in
Termops.pr_evar_universe_context (Evd.evar_universe_context sigma) ++ fnl () ++
str "Normalized constraints:" ++ brk(1,1) ++ Univ.pr_universe_context_set (Termops.pr_evd_level sigma) ctx
(* Simulate the Intro(s) tactic *)
let show_intro ~proof all =
let open EConstr in
let Proof.{goals;sigma} = Proof.data proof in
if not (List.is_empty goals) then begin
let evi = Evd.find_undefined sigma (List.hd goals) in
let env = Evd.evar_filtered_env (Global.env ()) evi in
let l,_= decompose_prod_decls sigma (Termops.strip_outer_cast sigma (Evd.evar_concl evi)) in
if all then
let lid = Tactics.find_intro_names env sigma l in
hov 0 (prlist_with_sep spc Id.print lid)
else if not (List.is_empty l) then
let n = List.last l in
Id.print (List.hd (Tactics.find_intro_names env sigma [n]))
else mt ()
end else mt ()
(** Textual display of a generic "match" template *)
let show_match id =
let patterns =
try ComInductive.make_cases (Nametab.global_inductive id)
with Not_found -> user_err Pp.(str "Unknown inductive type.")
in
let pr_branch l =
str "| " ++ hov 1 (prlist_with_sep spc str l) ++ str " =>"
in
v 1 (str "match # with" ++ fnl () ++
prlist_with_sep fnl pr_branch patterns ++ fnl () ++ str "end" ++ fnl ())
(* "Print" commands *)
let print_loadpath dir =
let l = Loadpath.get_load_paths () in
let l = match dir with
| None -> l
| Some dir ->
let filter p = is_dirpath_prefix_of dir (Loadpath.logical p) in
List.filter filter l
in
str "Logical Path / Physical path:" ++ fnl () ++
prlist_with_sep fnl Loadpath.pp l
let print_libraries () =
let loaded = Library.loaded_libraries () in
str"Loaded library files: " ++
pr_vertical_list DirPath.print loaded
let print_module qid =
match Nametab.locate_module qid with
| mp -> Printmod.print_module ~with_body:true mp
| exception Not_found -> user_err (str"Unknown Module " ++ pr_qualid qid ++ str".")
let print_modtype qid =
try
let kn = Nametab.locate_modtype qid in
Printmod.print_modtype kn
with Not_found ->
(* Is there a module of this name ? If yes we display its type *)
try
let mp = Nametab.locate_module qid in
Printmod.print_module ~with_body:false mp
with Not_found ->
user_err (str"Unknown Module Type or Module " ++ pr_qualid qid ++ str".")
let print_namespace ~pstate ns =
let ns = List.rev (Names.DirPath.repr ns) in
(* [match_dirpath], [match_modulpath] are helpers for [matches]
which checks whether a constant is in the namespace [ns]. *)
let rec match_dirpath ns = function
| [] -> Some ns
| id::dir ->
begin match match_dirpath ns dir with
| Some [] as y -> y
| Some (a::ns') ->
if Names.Id.equal a id then Some ns'
else None
| None -> None
end
in
let rec match_modulepath ns = function
| MPbound _ -> None (* Not a proper namespace. *)
| MPfile dir -> match_dirpath ns (Names.DirPath.repr dir)
| MPdot (mp,lbl) ->
let id = Names.Label.to_id lbl in
begin match match_modulepath ns mp with
| Some [] as y -> y
| Some (a::ns') ->
if Names.Id.equal a id then Some ns'
else None
| None -> None
end
in
(* [qualified_minus n mp] returns a list of qualifiers representing
[mp] except the [n] first (in the concrete syntax order). The
idea is that if [mp] matches [ns], then [qualified_minus mp
(length ns)] will be the correct representation of [mp] assuming
[ns] is imported. *)
(* precondition: [mp] matches some namespace of length [n] *)
let qualified_minus n mp =
let rec list_of_modulepath = function
| MPbound _ -> assert false (* MPbound never matches *)
| MPfile dir -> Names.DirPath.repr dir
| MPdot (mp,lbl) -> (Names.Label.to_id lbl)::(list_of_modulepath mp)
in
snd (Util.List.chop n (List.rev (list_of_modulepath mp)))
in
let print_list pr l = prlist_with_sep (fun () -> str".") pr l in
let print_kn kn =
let (mp,lbl) = Names.KerName.repr kn in
let qn = (qualified_minus (List.length ns) mp)@[Names.Label.to_id lbl] in
print_list Id.print qn
in
let print_constant ~pstate k body =
(* FIXME: universes *)
let t = body.Declarations.const_type in
let sigma, env = get_current_or_global_context ~pstate in
print_kn k ++ str":" ++ spc() ++ Printer.pr_type_env env sigma t
in
let matches mp = match match_modulepath ns mp with
| Some [] -> true
| _ -> false in
let constants_in_namespace =
Environ.fold_constants (fun c body acc ->
let kn = Constant.user c in
if matches (KerName.modpath kn)
then acc++fnl()++hov 2 (print_constant ~pstate kn body)
else acc)
(Global.env ()) (str"")
in
(print_list Id.print ns)++str":"++fnl()++constants_in_namespace
let print_strategy r =
let open Conv_oracle in
let pr_level = function
| Expand -> str "expand"
| Level 0 -> str "transparent"
| Level n -> str "level" ++ spc() ++ int n
| Opaque -> str "opaque"
in
let pr_strategy (ref, lvl) = pr_global ref ++ str " : " ++ pr_level lvl in
let oracle = Environ.oracle (Global.env ()) in
match r with
| None ->
let fold key lvl (vacc, cacc) = match key with
| VarKey id -> ((GlobRef.VarRef id, lvl) :: vacc, cacc)
| ConstKey cst -> (vacc, (GlobRef.ConstRef cst, lvl) :: cacc)
| RelKey _ -> (vacc, cacc)
in
let var_lvl, cst_lvl = fold_strategy fold oracle ([], []) in
let var_msg =
if List.is_empty var_lvl then mt ()
else str "Variable strategies" ++ fnl () ++
hov 0 (prlist_with_sep fnl pr_strategy var_lvl) ++ fnl ()
in
let cst_msg =
if List.is_empty cst_lvl then mt ()
else str "Constant strategies" ++ fnl () ++
hov 0 (prlist_with_sep fnl pr_strategy cst_lvl)
in
var_msg ++ cst_msg
| Some r ->
let r = Smartlocate.smart_global r in
let key = let open GlobRef in match r with
| VarRef id -> VarKey id
| ConstRef cst -> ConstKey cst
| IndRef _ | ConstructRef _ -> user_err Pp.(str "The reference is not unfoldable.")
in
let lvl = get_strategy oracle key in
pr_strategy (r, lvl)
let print_registered () =
let pr_lib_ref (s,r) =
pr_global r ++ str " registered as " ++ str s
in
hov 0 (prlist_with_sep fnl pr_lib_ref @@ Coqlib.get_lib_refs ())
let dump_universes output g =
let open Univ in
let dump_arc u = function
| UGraph.Node ltle ->
Univ.Level.Map.iter (fun v strict ->
let typ = if strict then Lt else Le in
output typ u v) ltle;
| UGraph.Alias v ->
output Eq u v
in
Univ.Level.Map.iter dump_arc g
let dump_universes_gen prl g s =
let output = open_out s in
let output_constraint, close =
if Filename.check_suffix s ".dot" || Filename.check_suffix s ".gv" then begin
(* the lazy unit is to handle errors while printing the first line *)
let init = lazy (Printf.fprintf output "digraph universes {\n") in
begin fun kind left right ->
let () = Lazy.force init in
match kind with
| Univ.Lt ->
Printf.fprintf output " \"%s\" -> \"%s\" [style=bold];\n" right left
| Univ.Le ->
Printf.fprintf output " \"%s\" -> \"%s\" [style=solid];\n" right left
| Univ.Eq ->
Printf.fprintf output " \"%s\" -> \"%s\" [style=dashed];\n" left right
end, begin fun () ->
if Lazy.is_val init then Printf.fprintf output "}\n";
close_out output
end
end else begin
begin fun kind left right ->
let kind = match kind with
| Univ.Lt -> "<"
| Univ.Le -> "<="
| Univ.Eq -> "="
in
Printf.fprintf output "%s %s %s ;\n" left kind right
end, (fun () -> close_out output)
end
in
let output_constraint k l r = output_constraint k (prl l) (prl r) in
try
dump_universes output_constraint g;
close ();
str "Universes written to file \"" ++ str s ++ str "\"."
with reraise ->
let reraise = Exninfo.capture reraise in
close ();
Exninfo.iraise reraise
let universe_subgraph ?loc kept univ =
let open Univ in
let parse q =
try Level.make (Nametab.locate_universe q)
with Not_found ->
CErrors.user_err Pp.(str "Undeclared universe " ++ pr_qualid q ++ str".")
in
let kept = List.fold_left (fun kept q -> Level.Set.add (parse q) kept) Level.Set.empty kept in
let csts = UGraph.constraints_for ~kept univ in
let add u newgraph =
let strict = UGraph.check_constraint univ (Level.set,Lt,u) in
UGraph.add_universe u ~lbound:UGraph.Bound.Set ~strict newgraph
in
let univ = Level.Set.fold add kept UGraph.initial_universes in
UGraph.merge_constraints csts univ
let sort_universes g =
let open Univ in
let rec normalize u = match Level.Map.find u g with
| UGraph.Alias u -> normalize u
| UGraph.Node _ -> u
in
let get_next u = match Level.Map.find u g with
| UGraph.Alias u -> assert false (* nodes are normalized *)
| UGraph.Node ltle -> ltle
in
(* Compute the longest chain of Lt constraints from Set to any universe *)
let rec traverse accu todo = match todo with
| [] -> accu
| (u, n) :: todo ->
let () = assert (Level.equal (normalize u) u) in
let n = match Level.Map.find u accu with
| m -> if m < n then Some n else None
| exception Not_found -> Some n
in
match n with
| None -> traverse accu todo
| Some n ->
let accu = Level.Map.add u n accu in
let next = get_next u in
let fold v lt todo =
let v = normalize v in
if lt then (v, n + 1) :: todo else (v, n) :: todo
in
let todo = Level.Map.fold fold next todo in
traverse accu todo
in
(* Only contains normalized nodes *)
let levels = traverse Level.Map.empty [normalize Level.set, 0] in
let max_level = Level.Map.fold (fun _ n accu -> max n accu) levels 0 in
let dummy_mp = Names.DirPath.make [Names.Id.of_string "Type"] in
let ulevels = Array.init max_level (fun i -> Level.(make (UGlobal.make dummy_mp "" i))) in
(* Add the normal universes *)
let fold (cur, ans) u =
let ans = Level.Map.add cur (UGraph.Node (Level.Map.singleton u true)) ans in
(u, ans)
in
let _, ans = Array.fold_left fold (Level.set, Level.Map.empty) ulevels in
let ulevels = Array.cons Level.set ulevels in
(* Add alias pointers *)
let fold u _ ans =
if Level.is_set u then ans
else
let n = Level.Map.find (normalize u) levels in
Level.Map.add u (UGraph.Alias ulevels.(n)) ans
in
Level.Map.fold fold g ans
let print_universes ?loc ~sort ~subgraph dst =
let univ = Global.universes () in
let univ = match subgraph with
| None -> univ
| Some g -> universe_subgraph ?loc g univ
in
let univ = UGraph.repr univ in
let univ = if sort then sort_universes univ else univ in
let pr_remaining =
if Global.is_joined_environment () then mt ()
else str"There may remain asynchronous universe constraints"
in
let prl = UnivNames.pr_with_global_universes in
begin match dst with
| None -> UGraph.pr_universes prl univ ++ pr_remaining
| Some s -> dump_universes_gen (fun u -> Pp.string_of_ppcmds (prl u)) univ s
end
(*********************)
(* "Locate" commands *)
let locate_file f =
let file = Flags.silently Loadpath.locate_file f in
str file
let msg_found_library (fulldir, file) =
if Library.library_is_loaded fulldir then
hov 0 (DirPath.print fulldir ++ strbrk " has been loaded from file " ++ str file)
else
hov 0 (DirPath.print fulldir ++ strbrk " is bound to file " ++ str file)
let print_located_library qid =
let open Loadpath in
match locate_qualified_library qid with
| Ok lib -> msg_found_library lib
| Error LibUnmappedDir -> raise (UnmappedLibrary (None, qid))
| Error LibNotFound -> raise (NotFoundLibrary (None, qid))
let smart_global r =
let gr = Smartlocate.smart_global r in
Dumpglob.add_glob ?loc:r.loc gr;
gr
let dump_global r =
try
let gr = Smartlocate.smart_global r in
Dumpglob.add_glob ?loc:r.loc gr
with e when CErrors.noncritical e -> ()
let dump_qualid q = dump_global (make ?loc:q.loc @@ Constrexpr.AN q)
(**********)
(* Syntax *)
let vernac_declare_scope ~module_local sc =
Metasyntax.declare_scope module_local sc
let vernac_delimiters ~module_local sc action =
match action with
| Some lr -> Metasyntax.add_delimiters module_local sc lr
| None -> Metasyntax.remove_delimiters module_local sc
let vernac_bind_scope ~atts sc cll =
let module_local, where = Attributes.(parse Notations.(module_locality ++ bind_scope_where) atts) in
Metasyntax.add_class_scope module_local sc where (List.map scope_class_of_qualid cll)
let vernac_open_close_scope ~section_local (to_open,s) =
Metasyntax.open_close_scope section_local ~to_open s
let interp_enable_notation_rule on ntn interp flags scope =
let open Notation in
let rule = Option.map (function
| Inl ntn -> Inl (interpret_notation_string ntn)
| Inr (vars,qid) -> Inr qid) ntn in
let rec parse_notation_enable_flags all query = function
| [] -> all, query
| EnableNotationEntry CAst.{loc;v=entry} :: flags ->
(match entry with InCustomEntry s when not (Egramcoq.exists_custom_entry s) -> user_err ?loc (str "Unknown custom entry.") | _ -> ());
parse_notation_enable_flags all { query with notation_entry_pattern = entry :: query.notation_entry_pattern } flags
| EnableNotationOnly use :: flags ->
parse_notation_enable_flags all { query with use_pattern = use } flags
| EnableNotationAll :: flags -> parse_notation_enable_flags true query flags in
let interp = Option.map (fun c ->
let vars, recvars =
match ntn with
| None ->
(* We expect the right-hand side to mention "_" in place of proper variables *)
(* Or should we instead deactivate the check of free variables? *)
([], [])
| Some (Inl ntn) -> let {recvars; mainvars} = decompose_raw_notation ntn in (mainvars, recvars)
| Some (Inr (vars,qid)) -> (vars, [])
in
let ninterp_var_type = Id.Map.of_list (List.map (fun x -> (x, Notation_term.NtnInternTypeAny None)) vars) in
let ninterp_rec_vars = Id.Map.of_list recvars in
let nenv = Notation_term.{ ninterp_var_type; ninterp_rec_vars } in
let (_acvars, ac, _reversibility) = Constrintern.interp_notation_constr (Global.env ()) nenv c in
([], ac)) interp in
let default_notation_enable_pattern = {
notation_entry_pattern = [];
interp_rule_key_pattern = rule;
use_pattern = ParsingAndPrinting;
scope_pattern = scope;
interpretation_pattern = interp;
}
in
let all, notation_pattern =
parse_notation_enable_flags false default_notation_enable_pattern flags in
on, all, notation_pattern
let vernac_enable_notation ~module_local on rule interp flags scope =
let () = match rule, interp, scope with
| None, None, None -> user_err (str "No notation provided.") | _ -> () in
let on, all, notation_pattern = interp_enable_notation_rule on rule interp flags scope in
Metasyntax.declare_notation_toggle module_local ~on ~all notation_pattern
(***********)
(* Gallina *)
let check_name_freshness locality {CAst.loc;v=id} : unit =
(* We check existence here: it's a bit late at Qed time *)
if Nametab.exists_cci (Lib.make_path id) || Termops.is_section_variable (Global.env ()) id ||
locality <> Locality.Discharge && Nametab.exists_cci (Lib.make_path_except_section id)
then
user_err ?loc (Id.print id ++ str " already exists.")
let program_inference_hook env sigma ev =
let tac = !Declare.Obls.default_tactic in
let evi = Evd.find_undefined sigma ev in
let evi = Evarutil.nf_evar_info sigma evi in
let env = Evd.evar_filtered_env env evi in
try
let concl = Evd.evar_concl evi in
if not (Evarutil.is_ground_env sigma env &&
Evarutil.is_ground_term sigma concl)
then None
else
let c, _, _, _, ctx =
Declare.build_by_tactic ~poly:false env ~uctx:(Evd.evar_universe_context sigma) ~typ:concl tac
in
Some (Evd.set_universe_context sigma ctx, EConstr.of_constr c)
with
| Logic_monad.TacticFailure e when noncritical e ->
user_err Pp.(str "The statement obligations could not be resolved \
automatically, write a statement definition first.")
let vernac_set_used_variables ~pstate using : Declare.Proof.t =
let env = Global.env () in
let sigma, _ = Declare.Proof.get_current_context pstate in
let initial_goals pf = Proofview.initial_goals Proof.((data pf).entry) in
let terms = List.map pi3 (initial_goals (Declare.Proof.get pstate)) in
let using = Proof_using.definition_using env sigma ~using ~terms in
let vars = Environ.named_context env in
Names.Id.Set.iter (fun id ->
if not (List.exists (NamedDecl.get_id %> Id.equal id) vars) then
user_err
(str "Unknown variable: " ++ Id.print id ++ str "."))
using;
let _, pstate = Declare.Proof.set_used_variables pstate ~using in
pstate
let vernac_set_used_variables_opt ?using pstate =
match using with
| None -> pstate
| Some expr -> vernac_set_used_variables ~pstate expr
(* XXX: Interpretation of lemma command, duplication with ComFixpoint
/ ComDefinition ? *)
let interp_lemma ~program_mode ~flags ~scope env0 evd thms =
let inference_hook = if program_mode then Some program_inference_hook else None in
List.fold_left_map (fun evd ((id, _), (bl, t)) ->
let evd, (impls, ((env, ctx), imps)) =
Constrintern.interp_context_evars ~program_mode env0 evd bl
in
let evd, (t', imps') = Constrintern.interp_type_evars_impls ~flags ~impls env evd t in
let flags = Pretyping.{ all_and_fail_flags with program_mode } in
let evd = Pretyping.solve_remaining_evars ?hook:inference_hook flags env evd in
let ids = List.map Context.Rel.Declaration.get_name ctx in
check_name_freshness scope id;
let thm = Declare.CInfo.make ~name:id.CAst.v ~typ:(EConstr.it_mkProd_or_LetIn t' ctx)
~args:ids ~impargs:(imps @ imps') () in
evd, thm)
evd thms
(* Checks done in start_lemma_com *)
let post_check_evd ~udecl ~poly evd =
let () =
if not UState.(udecl.univdecl_extensible_instance &&
udecl.univdecl_extensible_constraints) then
ignore (Evd.check_univ_decl ~poly evd udecl)
in
if poly then evd
else (* We fix the variables to ensure they won't be lowered to Set *)
Evd.fix_undefined_variables evd
let start_lemma_com ~typing_flags ~program_mode ~poly ~scope ~kind ?using ?hook thms =
let env0 = Global.env () in
let env0 = Environ.update_typing_flags ?typing_flags env0 in
let flags = Pretyping.{ all_no_fail_flags with program_mode } in
let decl = fst (List.hd thms) in
let evd, udecl = Constrintern.interp_univ_decl_opt env0 (snd decl) in
let evd, thms = interp_lemma ~program_mode ~flags ~scope env0 evd thms in
let mut_analysis = RecLemmas.look_for_possibly_mutual_statements evd thms in
let evd = Evd.minimize_universes evd in
let info = Declare.Info.make ?hook ~poly ~scope ~kind ~udecl ?typing_flags () in
begin
match mut_analysis with
| RecLemmas.NonMutual thm ->
let thm = Declare.CInfo.to_constr evd thm in
let evd = post_check_evd ~udecl ~poly evd in
Declare.Proof.start_with_initialization ~info ~cinfo:thm evd
| RecLemmas.Mutual { mutual_info; cinfo ; possible_guards } ->
let cinfo = List.map (Declare.CInfo.to_constr evd) cinfo in
let evd = post_check_evd ~udecl ~poly evd in
Declare.Proof.start_mutual_with_initialization ~info ~cinfo evd ~mutual_info (Some possible_guards)
end
(* XXX: This should be handled in start_with_initialization, see duplicate using in declare.ml *)
|> vernac_set_used_variables_opt ?using
let vernac_definition_hook ~canonical_instance ~local ~poly ~nonuniform ~reversible = let open Decls in function
| Coercion ->
Some (ComCoercion.add_coercion_hook ~poly ~nonuniform ~reversible)
| CanonicalStructure ->
Some (Declare.Hook.(make (fun { S.dref } -> Canonical.declare_canonical_structure ?local dref)))
| SubClass ->
Some (ComCoercion.add_subclass_hook ~poly ~reversible)
| Definition when canonical_instance ->
Some (Declare.Hook.(make (fun { S.dref } -> Canonical.declare_canonical_structure ?local dref)))
| Let when canonical_instance ->
Some (Declare.Hook.(make (fun { S.dref } -> Canonical.declare_canonical_structure dref)))
| _ -> None
let default_thm_id = Id.of_string "Unnamed_thm"
let fresh_name_for_anonymous_theorem () =
Namegen.next_global_ident_away default_thm_id Id.Set.empty
let vernac_definition_name lid local =
let lid =
match lid with
| { v = Name.Anonymous; loc } ->
CAst.make ?loc (fresh_name_for_anonymous_theorem ())
| { v = Name.Name n; loc } -> CAst.make ?loc n in
let () =
match local with
| Discharge -> Dumpglob.dump_definition lid true "var"
| Global _ -> Dumpglob.dump_definition lid false "def"
in
lid
let vernac_definition_interactive ~atts (discharge, kind) (lid, pl) bl t =
let open DefAttributes in
let local = enforce_locality_exp atts.locality discharge in
let hook = vernac_definition_hook ~canonical_instance:atts.canonical_instance ~local:atts.locality ~poly:atts.polymorphic ~nonuniform:atts.nonuniform ~reversible:atts.reversible kind in
let program_mode = atts.program in
let poly = atts.polymorphic in
let typing_flags = atts.typing_flags in
let name = vernac_definition_name lid local in
start_lemma_com ~typing_flags ~program_mode ~poly ~scope:local ~kind:(Decls.IsDefinition kind) ?using:atts.using ?hook [(name, pl), (bl, t)]
let vernac_definition ~atts ~pm (discharge, kind) (lid, pl) bl red_option c typ_opt =
let open DefAttributes in
let scope = enforce_locality_exp atts.locality discharge in
let hook = vernac_definition_hook ~canonical_instance:atts.canonical_instance ~local:atts.locality ~poly:atts.polymorphic kind ~nonuniform:atts.nonuniform ~reversible:atts.reversible in
let program_mode = atts.program in
let typing_flags = atts.typing_flags in
let name = vernac_definition_name lid scope in
let red_option = match red_option with
| None -> None
| Some r ->
let env = Global.env () in
let sigma = Evd.from_env env in
Some (snd (Hook.get f_interp_redexp env sigma r)) in
if program_mode then
let kind = Decls.IsDefinition kind in
ComDefinition.do_definition_program ~pm ~name:name.v
~poly:atts.polymorphic ?typing_flags ~scope ~kind pl bl red_option c typ_opt ?hook
else
let () =
ComDefinition.do_definition ~name:name.v
~poly:atts.polymorphic ?typing_flags ~scope ~kind ?using:atts.using pl bl red_option c typ_opt ?hook in
pm
(* NB: pstate argument to use combinators easily *)
let vernac_start_proof ~atts kind l =
let open DefAttributes in
let scope = enforce_locality_exp atts.locality NoDischarge in
if Dumpglob.dump () then
List.iter (fun ((id, _), _) -> Dumpglob.dump_definition id false "prf") l;
start_lemma_com
~typing_flags:atts.typing_flags
~program_mode:atts.program
~poly:atts.polymorphic
~scope ~kind:(Decls.IsProof kind) ?using:atts.using l
let vernac_end_proof ~lemma ~pm = let open Vernacexpr in function
| Admitted ->
Declare.Proof.save_admitted ~pm ~proof:lemma
| Proved (opaque,idopt) ->
let pm, _ = Declare.Proof.save ~pm ~proof:lemma ~opaque ~idopt
in pm
let vernac_abort ~lemma:_ ~pm = pm
let vernac_exact_proof ~lemma ~pm c =
(* spiwack: for simplicity I do not enforce that "Proof proof_term" is
called only at the beginning of a proof. *)
let lemma, status = Declare.Proof.by (Tactics.exact_proof c) lemma in
let pm, _ = Declare.Proof.save ~pm ~proof:lemma ~opaque:Opaque ~idopt:None in
if not status then Feedback.feedback Feedback.AddedAxiom;
pm
let vernac_assumption ~atts discharge kind l nl =
let open DefAttributes in
let scope = enforce_locality_exp atts.locality discharge in
List.iter (fun (is_coe,(idl,c)) ->
if Dumpglob.dump () then
List.iter (fun (lid, _) ->
match scope with
| Global _ -> Dumpglob.dump_definition lid false "ax"
| Discharge -> Dumpglob.dump_definition lid true "var") idl) l;
if Option.has_some atts.using then
Attributes.unsupported_attributes [CAst.make ("using",VernacFlagEmpty)];
ComAssumption.do_assumptions ~poly:atts.polymorphic ~program_mode:atts.program ~scope ~kind nl l
let is_polymorphic_inductive_cumulativity =
declare_bool_option_and_ref
~stage:Summary.Stage.Interp
~depr:false
~value:false
~key:["Polymorphic";"Inductive";"Cumulativity"]
let polymorphic_cumulative ~is_defclass =
let error_poly_context () =
user_err
Pp.(str "The cumulative attribute can only be used in a polymorphic context.");
in
let open Attributes in
let open Notations in
(* EJGA: this seems redudant with code in attributes.ml *)
qualify_attribute "universes"
(bool_attribute ~name:"polymorphic"
++ bool_attribute ~name:"cumulative")
>>= fun (poly,cumul) ->
if is_defclass && Option.has_some cumul
then user_err Pp.(str "Definitional classes do not support the inductive cumulativity attribute.");
match poly, cumul with
| Some poly, Some cumul ->
(* Case of Polymorphic|Monomorphic Cumulative|NonCumulative Inductive
and #[ universes(polymorphic|monomorphic,cumulative|noncumulative) ] Inductive *)
if poly then return (true, cumul)
else error_poly_context ()
| Some poly, None ->
(* Case of Polymorphic|Monomorphic Inductive
and #[ universes(polymorphic|monomorphic) ] Inductive *)
if poly then return (true, is_polymorphic_inductive_cumulativity ())
else return (false, false)
| None, Some cumul ->
(* Case of Cumulative|NonCumulative Inductive *)
if is_universe_polymorphism () then return (true, cumul)
else error_poly_context ()
| None, None ->
(* Case of Inductive *)
if is_universe_polymorphism () then
return (true, is_polymorphic_inductive_cumulativity ())
else
return (false, false)
let get_uniform_inductive_parameters =
Goptions.declare_bool_option_and_ref
~stage:Summary.Stage.Interp
~depr:false
~key:["Uniform"; "Inductive"; "Parameters"]
~value:false
let should_treat_as_uniform () =
if get_uniform_inductive_parameters ()
then ComInductive.UniformParameters
else ComInductive.NonUniformParameters
let vernac_record ~template udecl ~cumulative k ~poly ?typing_flags ~primitive_proj finite records =
let map ((is_coercion, name), binders, sort, nameopt, cfs, ido) =
let idbuild = match nameopt with
| None -> Nameops.add_prefix "Build_" name.v
| Some lid -> lid.v
in
let default_inhabitant_id = Option.map (fun CAst.{v=id} -> id) ido in
Record.Ast.{ name; is_coercion; binders; cfs; idbuild; sort; default_inhabitant_id }
in
let records = List.map map records in
match typing_flags with
| Some _ ->
CErrors.user_err (Pp.str "Typing flags are not yet supported for records.")
| None -> records
let extract_inductive_udecl (indl:(inductive_expr * notation_declaration list) list) =
match indl with
| [] -> assert false
| (((coe,(id,udecl)),b,c,d),e) :: rest ->
let rest = List.map (fun (((coe,(id,udecl)),b,c,d),e) ->
if Option.has_some udecl
then user_err Pp.(strbrk "Universe binders must be on the first inductive of the block.")
else (((coe,id),b,c,d),e))
rest
in
udecl, (((coe,id),b,c,d),e) :: rest
let finite_of_kind = let open Declarations in function
| Inductive_kw -> Finite
| CoInductive -> CoFinite
| Variant | Record | Structure | Class _ -> BiFinite
let private_ind =
let open Attributes in
let open Notations in
attribute_of_list
[ "matching"
, single_key_parser ~name:"Private (matching) inductive type" ~key:"matching" ()
]
|> qualify_attribute "private"
>>= function
| Some () -> return true
| None -> return false
(** Flag governing use of primitive projections. Disabled by default. *)
let primitive_flag =
Goptions.declare_bool_option_and_ref
~stage:Summary.Stage.Interp
~depr:false
~key:["Primitive";"Projections"]
~value:false
let primitive_proj =
let open Attributes in
let open Notations in
qualify_attribute "projections" (bool_attribute ~name:"primitive")
>>= function
| Some t -> return t
| None -> return (primitive_flag ())
module Preprocessed_Mind_decl = struct
type flags = {
template : bool option;
udecl : Constrexpr.cumul_univ_decl_expr option;
cumulative : bool;
poly : bool;
finite : Declarations.recursivity_kind;
}
type record = {
flags : flags;
primitive_proj : bool;
kind : Vernacexpr.inductive_kind;
records : Record.Ast.t list;
}
type inductive = {
flags : flags;
typing_flags : Declarations.typing_flags option;
private_ind : bool;
uniform : ComInductive.uniform_inductive_flag;
inductives : (Vernacexpr.one_inductive_expr * Vernacexpr.notation_declaration list) list;
}
type t =
| Record of record
| Inductive of inductive
end
let preprocess_inductive_decl ~atts kind indl =
let udecl, indl = extract_inductive_udecl indl in
let is_defclass = match kind, indl with
| Class _, [ ( id , bl , c , Constructors [l]), [] ] -> Some (id, bl, c, l)
| _ -> None
in
let finite = finite_of_kind kind in
let is_record = function
| ((_ , _ , _ , RecordDecl _), _) -> true
| _ -> false
in
let is_constructor = function
| ((_ , _ , _ , Constructors _), _) -> true
| _ -> false
in
(* We only allow the #[projections(primitive)] attribute
for records. *)
let prim_proj_attr : bool Attributes.Notations.t =
if List.for_all is_record indl then primitive_proj
else Notations.return false
in
let (((template, (poly, cumulative)), private_ind), typing_flags), primitive_proj =
Attributes.(
parse Notations.(
template
++ polymorphic_cumulative ~is_defclass:(Option.has_some is_defclass)
++ private_ind ++ typing_flags ++ prim_proj_attr)
atts)
in
if Option.has_some is_defclass then
(* Definitional class case *)
let (id, bl, c, l) = Option.get is_defclass in
let bl = match bl with
| bl, None -> bl
| _ -> CErrors.user_err Pp.(str "Definitional classes do not support the \"|\" syntax.")
in
if fst id = AddCoercion then
user_err Pp.(str "Definitional classes do not support the \">\" syntax.");
let ((rf_coercion, rf_instance), (lid, ce)) = l in
let f = AssumExpr ((make ?loc:lid.loc @@ Name lid.v), [], ce),
{ rf_coercion ; rf_reversible = None ; rf_instance ; rf_priority = None ;
rf_locality = Goptions.OptDefault ; rf_notation = [] ; rf_canonical = true } in
let recordl = [id, bl, c, None, [f], None] in
let kind = Class true in
let records = vernac_record ~template udecl ~cumulative kind ~poly ?typing_flags ~primitive_proj finite recordl in
indl, Preprocessed_Mind_decl.(Record { flags = { template; udecl; cumulative; poly; finite; }; primitive_proj; kind; records })
else if List.for_all is_record indl then
(* Mutual record case *)
let () = match kind with
| Variant ->
user_err (str "The Variant keyword does not support syntax { ... }.")
| Record | Structure | Class _ | Inductive_kw | CoInductive -> ()
in
let check_where ((_, _, _, _), wh) = match wh with
| [] -> ()
| _ :: _ ->
user_err (str "\"where\" clause not supported for records.")
in
let () = List.iter check_where indl in
let unpack ((id, bl, c, decl), _) = match decl with
| RecordDecl (oc, fs, ido) ->
let bl = match bl with
| bl, None -> bl
| _ -> CErrors.user_err Pp.(str "Records do not support the \"|\" syntax.")
in
(id, bl, c, oc, fs, ido)
| Constructors _ -> assert false (* ruled out above *)
in
let kind = match kind with Class _ -> Class false | _ -> kind in
let recordl = List.map unpack indl in
let records = vernac_record ~template udecl ~cumulative kind ~poly ?typing_flags ~primitive_proj finite recordl in
indl, Preprocessed_Mind_decl.(Record { flags = { template; udecl; cumulative; poly; finite; }; primitive_proj; kind; records })
else if List.for_all is_constructor indl then
(* Mutual inductive case *)
let () = match kind with
| (Record | Structure) ->
user_err (str "The Record keyword is for types defined using the syntax { ... }.")
| Class _ ->
user_err (str "Inductive classes not supported.")
| Variant | Inductive_kw | CoInductive -> ()
in
let check_name ((na, _, _, _), _) = match na with
| (AddCoercion, _) ->
user_err (str "Variant types do not handle the \"> Name\" \
syntax, which is reserved for records. Use the \":>\" \
syntax on constructors instead.")
| _ -> ()
in
let () = List.iter check_name indl in
let unpack (((_, id) , bl, c, decl), ntn) = match decl with
| Constructors l -> (id, bl, c, l), ntn
| RecordDecl _ -> assert false (* ruled out above *)
in
let inductives = List.map unpack indl in
let uniform = should_treat_as_uniform () in
indl, Preprocessed_Mind_decl.(Inductive { flags = { template; udecl; cumulative; poly; finite }; typing_flags; private_ind; uniform; inductives })
else
user_err (str "Mixed record-inductive definitions are not allowed.")
let dump_inductive indl_for_glob decl =
let open Preprocessed_Mind_decl in
if Dumpglob.dump () then begin
List.iter (fun (((coe,lid), _, _, cstrs), _) ->
match cstrs with
| Constructors cstrs ->
Dumpglob.dump_definition lid false "ind";
List.iter (fun (_, (lid, _)) ->
Dumpglob.dump_definition lid false "constr") cstrs
| _ -> ())
indl_for_glob;
match decl with
| Record { flags = { template; udecl; cumulative; poly; finite; }; kind; primitive_proj; records } ->
let dump_glob_proj (x, _) = match x with
| Vernacexpr.(AssumExpr ({loc;v=Name id}, _, _) | DefExpr ({loc;v=Name id}, _, _, _)) ->
Dumpglob.dump_definition (make ?loc id) false "proj"
| _ -> () in
records |> List.iter (fun { Record.Ast.cfs; name } ->
let () = Dumpglob.dump_definition name false "rec" in
List.iter dump_glob_proj cfs)
| Inductive _ -> ()
end
let vernac_inductive ~atts kind indl =
let open Preprocessed_Mind_decl in
let indl_for_glob, decl = preprocess_inductive_decl ~atts kind indl in
dump_inductive indl_for_glob decl;
match decl with
| Record { flags = { template; udecl; cumulative; poly; finite; }; kind; primitive_proj; records } ->
let _ : _ list =
Record.definition_structure ~template udecl kind ~cumulative ~poly ~primitive_proj finite records in
()
| Inductive { flags = { template; udecl; cumulative; poly; finite; }; typing_flags; private_ind; uniform; inductives } ->
ComInductive.do_mutual_inductive ~template udecl inductives ~cumulative ~poly ?typing_flags ~private_ind ~uniform finite
let preprocess_inductive_decl ~atts kind indl =
snd @@ preprocess_inductive_decl ~atts kind indl
let vernac_fixpoint_common ~atts discharge l =
if Dumpglob.dump () then
List.iter (fun { fname } -> Dumpglob.dump_definition fname false "def") l;
enforce_locality_exp atts.DefAttributes.locality discharge
let vernac_fixpoint_interactive ~atts discharge l =
let open DefAttributes in
let scope = vernac_fixpoint_common ~atts discharge l in
if atts.program then
CErrors.user_err Pp.(str"Program Fixpoint requires a body.");
let typing_flags = atts.typing_flags in
ComFixpoint.do_fixpoint_interactive ~scope ~poly:atts.polymorphic ?typing_flags l