Source file record.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
open Pp
open CErrors
open Term
open Util
open Names
open Constr
open Context
open Environ
open Declarations
open Entries
open Type_errors
open Constrexpr
open Constrexpr_ops
open Context.Rel.Declaration
open Structures
module RelDecl = Context.Rel.Declaration
(** Flag governing use of primitive projections. Disabled by default. *)
let primitive_flag =
Goptions.declare_bool_option_and_ref
~depr:false
~key:["Primitive";"Projections"]
~value:false
let typeclasses_strict =
Goptions.declare_bool_option_and_ref
~depr:false
~key:["Typeclasses";"Strict";"Resolution"]
~value:false
let typeclasses_unique =
Goptions.declare_bool_option_and_ref
~depr:false
~key:["Typeclasses";"Unique";"Instances"]
~value:false
let interp_fields_evars env sigma ~ninds ~nparams impls_env nots l =
let _, sigma, impls, newfs, _ =
List.fold_left2
(fun (env, sigma, uimpls, params, impls_env) no d ->
let sigma, (i, b, t), impl = match d with
| Vernacexpr.AssumExpr({CAst.loc;v=id},bl,t) ->
let t = if bl = [] then t else mkCProdN bl t in
let sigma, t, impl =
ComAssumption.interp_assumption ~program_mode:false env sigma impls_env [] t in
sigma, (id, None, t), impl
| Vernacexpr.DefExpr({CAst.loc;v=id},bl,b,t) ->
let sigma, (b, t), impl =
ComDefinition.interp_definition ~program_mode:false env sigma impls_env bl None b t in
let t = match t with Some t -> t | None -> Retyping.get_type_of env sigma b in
sigma, (id, Some b, t), impl in
let r = Retyping.relevance_of_type env sigma t in
let impls_env =
match i with
| Anonymous -> impls_env
| Name id ->
Id.Map.add id (Constrintern.compute_internalization_data env sigma id Constrintern.Method t impl) impls_env
in
let d = match b with
| None -> LocalAssum (make_annot i r,t)
| Some b -> LocalDef (make_annot i r,b,t)
in
List.iter (Metasyntax.set_notation_for_interpretation env impls_env) no;
(EConstr.push_rel d env, sigma, impl :: uimpls, d::params, impls_env))
(env, sigma, [], [], impls_env) nots l
in
let _, _, sigma = Context.Rel.fold_outside ~init:(env,0,sigma) (fun f (env,k,sigma) ->
let sigma = RelDecl.fold_constr (fun c sigma ->
ComInductive.maybe_unify_params_in env sigma ~ninds ~nparams ~binders:k c)
f sigma
in
EConstr.push_rel f env, k+1, sigma)
newfs
in
sigma, (impls, newfs)
let compute_constructor_level evars env l =
List.fold_right (fun d (env, univ) ->
let univ =
if is_local_assum d then
let s = Retyping.get_sort_of env evars (RelDecl.get_type d) in
Univ.sup (Sorts.univ_of_sort s) univ
else univ
in (EConstr.push_rel d env, univ))
l (env, Univ.Universe.sprop)
let check_anonymous_type ind =
match ind with
| { CAst.v = CSort (Glob_term.UAnonymous {rigid=true}) } -> true
| _ -> false
let error_parameters_must_be_named bk {CAst.loc; v=name} =
match bk, name with
| Default _, Anonymous ->
CErrors.user_err ?loc ~hdr:"record" (str "Record parameters must be named")
| _ -> ()
let check_parameters_must_be_named = function
| CLocalDef (b, _, _) ->
error_parameters_must_be_named default_binder_kind b
| CLocalAssum (ls, bk, ce) ->
List.iter (error_parameters_must_be_named bk) ls
| CLocalPattern {CAst.loc} ->
Loc.raise ?loc (Stream.Error "pattern with quote not allowed in record parameters")
(** [DataI.t] contains the information used in record interpretation,
it is a strict subset of [Ast.t] thus this should be
eventually removed or merged with [Ast.t] *)
module DataI = struct
type t =
{ name : Id.t
; arity : Constrexpr.constr_expr option
(** declared sort for the record *)
; nots : Vernacexpr.decl_notation list list
(** notations for fields *)
; fs : Vernacexpr.local_decl_expr list
}
end
type projection_flags = {
pf_subclass: bool;
pf_canonical: bool;
}
(** [DataR.t] contains record data after interpretation /
type-inference *)
module DataR = struct
type t =
{ min_univ : Univ.Universe.t
; arity : Constr.t
; implfs : Impargs.manual_implicits list
; fields : Constr.rel_declaration list
}
end
module Data = struct
type t =
{ id : Id.t
; idbuild : Id.t
; is_coercion : bool
; coers : projection_flags list
; rdata : DataR.t
}
end
let build_type_telescope newps env0 (sigma, template) { DataI.arity; _ } = match arity with
| None ->
let uvarkind = Evd.univ_flexible_alg in
let sigma, s = Evd.new_sort_variable uvarkind sigma in
(sigma, template), (EConstr.mkSort s, s)
| Some t ->
let env = EConstr.push_rel_context newps env0 in
let poly =
match t with
| { CAst.v = CSort (Glob_term.UAnonymous {rigid=true}) } -> true | _ -> false in
let impls = Constrintern.empty_internalization_env in
let sigma, s = Constrintern.interp_type_evars ~program_mode:false env sigma ~impls t in
let sred = Reductionops.whd_allnolet env sigma s in
(match EConstr.kind sigma sred with
| Sort s' ->
let s' = EConstr.ESorts.kind sigma s' in
(if poly then
match Evd.is_sort_variable sigma s' with
| Some l ->
let sigma = Evd.make_flexible_variable sigma ~algebraic:true l in
(sigma, template), (s, s')
| None ->
(sigma, false), (s, s')
else (sigma, false), (s, s'))
| _ -> user_err ?loc:(constr_loc t) (str"Sort expected."))
type tc_result =
bool
* Impargs.manual_implicits
* UnivNames.universe_binders
* Entries.universes_entry
* Entries.variance_entry
* Constr.rel_context
* DataR.t list
let typecheck_params_and_fields def poly udecl ps (records : DataI.t list) : tc_result =
let env0 = Global.env () in
let is_template =
List.exists (fun { DataI.arity; _} -> Option.cata check_anonymous_type true arity) records in
let env0 = if not poly && is_template then Environ.set_universes_lbound env0 UGraph.Bound.Prop else env0 in
let sigma, decl, variances = Constrintern.interp_cumul_univ_decl_opt env0 udecl in
let () = List.iter check_parameters_must_be_named ps in
let sigma, (impls_env, ((env1,newps), imps)) =
Constrintern.interp_context_evars ~program_mode:false env0 sigma ps in
let (sigma, template), typs =
List.fold_left_map (build_type_telescope newps env0) (sigma, true) records in
let arities = List.map (fun (typ, _) -> EConstr.it_mkProd_or_LetIn typ newps) typs in
let relevances = List.map (fun (_,s) -> Sorts.relevance_of_sort s) typs in
let fold accu { DataI.name; _ } arity r =
EConstr.push_rel (LocalAssum (make_annot (Name name) r,arity)) accu in
let env_ar = EConstr.push_rel_context newps (List.fold_left3 fold env0 records arities relevances) in
let impls_env =
let ids = List.map (fun { DataI.name; _ } -> name) records in
let imps = List.map (fun _ -> imps) arities in
Constrintern.compute_internalization_env env0 sigma ~impls:impls_env Constrintern.Inductive ids arities imps
in
let ninds = List.length arities in
let nparams = List.length newps in
let fold sigma { DataI.nots; fs; _ } arity =
interp_fields_evars env_ar sigma ~ninds ~nparams impls_env nots fs
in
let (sigma, data) = List.fold_left2_map fold sigma records arities in
let sigma =
Pretyping.solve_remaining_evars Pretyping.all_and_fail_flags env_ar sigma in
let fold sigma (typ, sort) (_, newfs) =
let _, univ = compute_constructor_level sigma env_ar newfs in
let univ = if Sorts.is_sprop sort then univ else Univ.Universe.sup univ Univ.type0m_univ in
if not def && is_impredicative_sort env0 sort then
sigma, (univ, typ)
else
let sigma = Evd.set_leq_sort env_ar sigma (Sorts.sort_of_univ univ) sort in
if Univ.is_small_univ univ &&
Option.cata (Evd.is_flexible_level sigma) false (Evd.is_sort_variable sigma sort) then
Evd.set_eq_sort env_ar sigma Sorts.set sort, (univ, EConstr.mkSort (Sorts.sort_of_univ univ))
else sigma, (univ, typ)
in
let (sigma, typs) = List.fold_left2_map fold sigma typs data in
let sigma, (newps, ans) = Evarutil.finalize sigma (fun nf ->
let newps = List.map (RelDecl.map_constr_het nf) newps in
let map (implfs, fields) (min_univ, typ) =
let fields = List.map (RelDecl.map_constr_het nf) fields in
let arity = nf typ in
{ DataR.min_univ; arity; implfs; fields }
in
let ans = List.map2 map data typs in
newps, ans)
in
let univs = Evd.check_univ_decl ~poly sigma decl in
let ubinders = Evd.universe_binders sigma in
let ce t = Pretyping.check_evars env0 sigma (EConstr.of_constr t) in
let () = List.iter (iter_constr ce) (List.rev newps) in
template, imps, ubinders, univs, variances, newps, ans
type record_error =
| MissingProj of Id.t * Id.t list
| BadTypedProj of Id.t * env * Type_errors.type_error
let warn_cannot_define_projection =
CWarnings.create ~name:"cannot-define-projection" ~category:"records"
(fun msg -> hov 0 msg)
let warning_or_error ~info coe indsp err =
let st = match err with
| MissingProj (fi,projs) ->
let s,have = if List.length projs > 1 then "s","were" else "","was" in
(Id.print fi ++
strbrk" cannot be defined because the projection" ++ str s ++ spc () ++
prlist_with_sep pr_comma Id.print projs ++ spc () ++ str have ++
strbrk " not defined.")
| BadTypedProj (fi,ctx,te) ->
match te with
| ElimArity (_,_,_,Some (_,_,_,NonInformativeToInformative)) ->
(Id.print fi ++
strbrk" cannot be defined because it is informative and " ++
Printer.pr_inductive (Global.env()) indsp ++
strbrk " is not.")
| ElimArity (_,_,_,Some (_,_,_,StrongEliminationOnNonSmallType)) ->
(Id.print fi ++
strbrk" cannot be defined because it is large and " ++
Printer.pr_inductive (Global.env()) indsp ++
strbrk " is not.")
| _ ->
(Id.print fi ++ strbrk " cannot be defined because it is not typable.")
in
if coe then user_err ~hdr:"structure" ~info st;
warn_cannot_define_projection (hov 0 st)
type field_status =
| NoProjection of Name.t
| Projection of constr
exception NotDefinable of record_error
let subst_projection fid l c =
let lv = List.length l in
let bad_projs = ref [] in
let rec substrec depth c = match Constr.kind c with
| Rel k ->
if k <= depth+1 then
c
else if k-depth-1 <= lv then
match List.nth l (k-depth-2) with
| Projection t -> lift depth t
| NoProjection (Name id) -> bad_projs := id :: !bad_projs; mkRel k
| NoProjection Anonymous ->
user_err (str "Field " ++ Id.print fid ++
str " depends on the " ++ pr_nth (k-depth-1) ++ str
" field which has no name.")
else
mkRel (k-lv)
| _ -> Constr.map_with_binders succ substrec depth c
in
let c' = lift 1 c in
let c'' = substrec 0 c' in
if not (List.is_empty !bad_projs) then
raise (NotDefinable (MissingProj (fid,List.rev !bad_projs)));
c''
let instantiate_possibly_recursive_type ind u ntypes paramdecls fields =
let subst = List.map_i (fun i _ -> mkRel i) 1 paramdecls in
let subst' = List.init ntypes (fun i -> mkIndU ((ind, ntypes - i - 1), u)) in
Termops.substl_rel_context (subst @ subst') fields
(** This builds and _declares_ a named projection, the code looks
tricky due to the term manipulation. It also handles declaring the
implicits parameters, coercion status, etc... of the projection;
this could be refactored as noted above by moving to the
higher-level declare constant API *)
let build_named_proj ~primitive ~flags ~poly ~univs ~uinstance ~kind env paramdecls
paramargs decl impls fid subst nfi ti i indsp mib lifted_fields x rp =
let ccl = subst_projection fid subst ti in
let body, p_opt = match decl with
| LocalDef (_,ci,_) -> subst_projection fid subst ci, None
| LocalAssum ({binder_relevance=rci},_) ->
if primitive then
let p = Projection.Repr.make indsp
~proj_npars:mib.mind_nparams ~proj_arg:i (Label.of_id fid) in
mkProj (Projection.make p true, mkRel 1), Some p
else
let ccl' = liftn 1 2 ccl in
let p = mkLambda (x, lift 1 rp, ccl') in
let branch = it_mkLambda_or_LetIn (mkRel nfi) lifted_fields in
let ci = Inductiveops.make_case_info env indsp rci LetStyle in
mkCase (Inductive.contract_case env (ci, p, NoInvert, mkRel 1, [|branch|])), None
in
let proj = it_mkLambda_or_LetIn (mkLambda (x,rp,body)) paramdecls in
let projtyp = it_mkProd_or_LetIn (mkProd (x,rp,ccl)) paramdecls in
let entry = Declare.definition_entry ~univs ~types:projtyp proj in
let kind = Decls.IsDefinition kind in
let kn =
try Declare.declare_constant ~name:fid ~kind (Declare.DefinitionEntry entry)
with Type_errors.TypeError (ctx,te) as exn when not primitive ->
let _, info = Exninfo.capture exn in
Exninfo.iraise (NotDefinable (BadTypedProj (fid,ctx,te)),info)
in
Declare.definition_message fid;
let term = match p_opt with
| Some p ->
let _ = DeclareInd.declare_primitive_projection p kn in
mkProj (Projection.make p false,mkRel 1)
| None ->
let proj_args = paramargs@[mkRel 1] in
match decl with
| LocalDef (_,ci,_) when primitive -> body
| _ -> applist (mkConstU (kn,uinstance),proj_args)
in
let refi = GlobRef.ConstRef kn in
Impargs.maybe_declare_manual_implicits false refi impls;
if flags.pf_subclass then begin
let cl = ComCoercion.class_of_global (GlobRef.IndRef indsp) in
ComCoercion.try_add_new_coercion_with_source refi ~local:false ~poly ~source:cl
end;
let i = if is_local_assum decl then i+1 else i in
(Some kn, i, Projection term::subst)
(** [build_proj] will build a projection for each field, or skip if
the field is anonymous, i.e. [_ : t] *)
let build_proj env mib indsp primitive x rp lifted_fields ~poly paramdecls paramargs ~uinstance ~kind ~univs
(nfi,i,kinds,subst) flags decl impls =
let fi = RelDecl.get_name decl in
let ti = RelDecl.get_type decl in
let (sp_proj,i,subst) =
match fi with
| Anonymous ->
(None,i,NoProjection fi::subst)
| Name fid ->
try build_named_proj
~primitive ~flags ~poly ~univs ~uinstance ~kind env paramdecls paramargs decl impls fid
subst nfi ti i indsp mib lifted_fields x rp
with NotDefinable why as exn ->
let _, info = Exninfo.capture exn in
warning_or_error ~info flags.pf_subclass indsp why;
(None,i,NoProjection fi::subst)
in
(nfi - 1, i,
{ Structure.proj_name = fi
; proj_true = is_local_assum decl
; proj_canonical = flags.pf_canonical
; proj_body = sp_proj } :: kinds
, subst)
(** [declare_projections] prepares the common context for all record
projections and then calls [build_proj] for each one. *)
let declare_projections indsp univs ?(kind=Decls.StructureComponent) binder_name flags fieldimpls fields =
let env = Global.env() in
let (mib,mip) = Global.lookup_inductive indsp in
let poly = Declareops.inductive_is_polymorphic mib in
let uinstance = match univs with
| Polymorphic_entry (_, ctx) -> Univ.UContext.instance ctx
| Monomorphic_entry ctx -> Univ.Instance.empty
in
let paramdecls = Inductive.inductive_paramdecls (mib, uinstance) in
let r = mkIndU (indsp,uinstance) in
let rp = applist (r, Context.Rel.to_extended_list mkRel 0 paramdecls) in
let paramargs = Context.Rel.to_extended_list mkRel 1 paramdecls in
let x = make_annot (Name binder_name) mip.mind_relevance in
let fields = instantiate_possibly_recursive_type (fst indsp) uinstance mib.mind_ntypes paramdecls fields in
let lifted_fields = Termops.lift_rel_context 1 fields in
let primitive =
match mib.mind_record with
| PrimRecord _ -> true
| FakeRecord | NotRecord -> false
in
let (_,_,canonical_projections,_) =
List.fold_left3
(build_proj env mib indsp primitive x rp lifted_fields ~poly paramdecls paramargs ~uinstance ~kind ~univs)
(List.length fields,0,[],[]) flags (List.rev fields) (List.rev fieldimpls)
in
List.rev canonical_projections
open Typeclasses
let check_template ~template ~poly ~univs ~params { Data.id; rdata = { DataR.min_univ; fields; _ }; _ } =
let template_candidate () =
let add_levels c levels = Univ.LSet.union levels (Vars.universes_of_constr c) in
let param_levels =
List.fold_left (fun levels d -> match d with
| LocalAssum _ -> levels
| LocalDef (_,b,t) -> add_levels b (add_levels t levels))
Univ.LSet.empty params
in
let ctor_levels = List.fold_left
(fun univs d ->
let univs =
RelDecl.fold_constr (fun c univs -> add_levels c univs) d univs
in
univs)
param_levels fields
in
ComInductive.template_polymorphism_candidate ~ctor_levels univs params
(Some (Sorts.sort_of_univ min_univ))
in
match template with
| Some template, _ ->
if poly && template then user_err Pp.(strbrk "template and polymorphism not compatible");
template
| None, template ->
ComInductive.should_auto_template id (template && template_candidate ())
let load_structure i (_, structure) = Structure.register structure
let cache_structure o = load_structure 1 o
let subst_structure (subst, obj) = Structure.subst subst obj
let discharge_structure (_, x) = Some x
let rebuild_structure s = Structure.rebuild (Global.env()) s
let inStruc : Structure.t -> Libobject.obj =
let open Libobject in
declare_object {(default_object "STRUCTURE") with
cache_function = cache_structure;
load_function = load_structure;
subst_function = subst_structure;
classify_function = (fun x -> Substitute x);
discharge_function = discharge_structure;
rebuild_function = rebuild_structure; }
let declare_structure_entry o =
Lib.add_anonymous_leaf (inStruc o)
(** In the type of every projection, the record is bound to a variable named
using the first character of the record type. We rename it to avoid
collisions with names already used in the field types.
*)
(** Get all names bound at the head of [t]. *)
let rec add_bound_names_constr (names : Id.Set.t) (t : constr) : Id.Set.t =
match destProd t with
| (b, _, t) ->
let names =
match b.binder_name with
| Name.Anonymous -> names
| Name.Name n -> Id.Set.add n names
in add_bound_names_constr names t
| exception DestKO -> names
(** Get all names bound in any record field. *)
let bound_names_rdata { DataR.fields; _ } : Id.Set.t =
let add_names names field = add_bound_names_constr names (RelDecl.get_type field) in
List.fold_left add_names Id.Set.empty fields
(** Pick a variable name for a record, avoiding names bound in its fields. *)
let data_name { Data.id; Data.rdata; _ } =
let name = Id.of_string (Unicode.lowercase_first_char (Id.to_string id)) in
Namegen.next_ident_away name (bound_names_rdata rdata)
(** Main record declaration part:
The entry point is [definition_structure], which will match on the
declared [kind] and then either follow the regular record
declaration path to [declare_structure] or handle the record as a
class declaration with [declare_class].
*)
(** [declare_structure] does two principal things:
- prepares and declares the low-level (mutual) inductive corresponding to [record_data]
- prepares and declares the corresponding record projections, mainly taken care of by
[declare_projections]
*)
let declare_structure ~cumulative finite ~ubind ~univs ~variances paramimpls params template ?(kind=Decls.StructureComponent) ?name (record_data : Data.t list) =
let nparams = List.length params in
let poly, ctx =
match univs with
| Monomorphic_entry ctx ->
false, Monomorphic_entry Univ.ContextSet.empty
| Polymorphic_entry (nas, ctx) ->
true, Polymorphic_entry (nas, ctx)
in
let binder_name =
match name with
| None -> Array.map_of_list data_name record_data
| Some n -> n
in
let ntypes = List.length record_data in
let mk_block i { Data.id; idbuild; rdata = { DataR.min_univ; arity; fields; _ }; _ } =
let nfields = List.length fields in
let args = Context.Rel.to_extended_list mkRel nfields params in
let ind = applist (mkRel (ntypes - i + nparams + nfields), args) in
let type_constructor = it_mkProd_or_LetIn ind fields in
{ mind_entry_typename = id;
mind_entry_arity = arity;
mind_entry_consnames = [idbuild];
mind_entry_lc = [type_constructor] }
in
let blocks = List.mapi mk_block record_data in
let template = List.for_all (check_template ~template ~univs ~poly ~params) record_data in
let primitive =
primitive_flag () &&
List.for_all (fun { Data.rdata = { DataR.fields; _ }; _ } -> List.exists is_local_assum fields) record_data
in
let mie =
{ mind_entry_params = params;
mind_entry_record = Some (if primitive then Some binder_name else None);
mind_entry_finite = finite;
mind_entry_inds = blocks;
mind_entry_private = None;
mind_entry_universes = univs;
mind_entry_template = template;
mind_entry_variance = ComInductive.variance_of_entry ~cumulative ~variances univs;
}
in
let impls = List.map (fun _ -> paramimpls, []) record_data in
let kn = DeclareInd.declare_mutual_inductive_with_eliminations mie ubind impls
~primitive_expected:(primitive_flag ())
in
let map i { Data.is_coercion; coers; rdata = { DataR.implfs; fields; _}; _ } =
let rsp = (kn, i) in
let cstr = (rsp, 1) in
let projections = declare_projections rsp ctx ~kind binder_name.(i) coers implfs fields in
let build = GlobRef.ConstructRef cstr in
let () = if is_coercion then ComCoercion.try_add_new_coercion build ~local:false ~poly in
let struc = Structure.make (Global.env ()) rsp projections in
let () = declare_structure_entry struc in
rsp
in
List.mapi map record_data
let implicits_of_context ctx =
List.map (fun name -> CAst.make (Some (name,true)))
(List.rev (Anonymous :: (List.map RelDecl.get_name ctx)))
let build_class_constant ~univs ~rdata field implfs params paramimpls coers binder id proj_name =
let class_body = it_mkLambda_or_LetIn field params in
let class_type = it_mkProd_or_LetIn rdata.DataR.arity params in
let class_entry =
Declare.definition_entry ~types:class_type ~univs class_body in
let cst = Declare.declare_constant ~name:id
(Declare.DefinitionEntry class_entry) ~kind:Decls.(IsDefinition Definition)
in
let inst, univs = match univs with
| Polymorphic_entry (_, uctx) -> Univ.UContext.instance uctx, univs
| Monomorphic_entry _ -> Univ.Instance.empty, Monomorphic_entry Univ.ContextSet.empty
in
let cstu = (cst, inst) in
let inst_type = appvectc (mkConstU cstu)
(Termops.rel_vect 0 (List.length params)) in
let proj_type =
it_mkProd_or_LetIn (mkProd(binder, inst_type, lift 1 field)) params in
let proj_body =
it_mkLambda_or_LetIn (mkLambda (binder, inst_type, mkRel 1)) params in
let proj_entry = Declare.definition_entry ~types:proj_type ~univs proj_body in
let proj_cst = Declare.declare_constant ~name:proj_name
(Declare.DefinitionEntry proj_entry) ~kind:Decls.(IsDefinition Definition)
in
let cref = GlobRef.ConstRef cst in
Impargs.declare_manual_implicits false cref paramimpls;
Impargs.declare_manual_implicits false (GlobRef.ConstRef proj_cst) (List.hd implfs);
Classes.set_typeclass_transparency (Tacred.EvalConstRef cst) false false;
let sub = List.hd coers in
let m = {
meth_name = Name proj_name;
meth_info = sub;
meth_const = Some proj_cst;
} in
[cref, [m]]
let build_record_constant ~rdata ~ubind ~univs ~variances ~cumulative ~template
fields params paramimpls coers id idbuild binder_name =
let record_data =
{ Data.id
; idbuild
; is_coercion = false
; coers = List.map (fun _ -> { pf_subclass = false ; pf_canonical = true }) fields
; rdata
} in
let inds = declare_structure ~cumulative Declarations.BiFinite ~ubind ~univs ~variances paramimpls
params template ~kind:Decls.Method ~name:[|binder_name|] [record_data]
in
let map ind =
let map decl b y = {
meth_name = RelDecl.get_name decl;
meth_info = b;
meth_const = y;
} in
let l = List.map3 map (List.rev fields) coers (Structure.find_projections ind) in
GlobRef.IndRef ind, l
in
List.map map inds
(** [declare_class] will prepare and declare a [Class]. This is done in
2 steps:
1. two markely different paths are followed depending on whether the
class declaration refers to a constant "definitional classes" or to
a record, that is to say:
Class foo := bar : T.
which is equivalent to
Definition foo := T.
Definition bar (x:foo) : T := x.
Existing Class foo.
vs
Class foo := { ... }.
2. declare the class, using the information from 1. in the form of [Classes.typeclass]
*)
let declare_class def ~cumulative ~ubind ~univs ~variances id idbuild paramimpls params
rdata template ?(kind=Decls.StructureComponent) coers =
let implfs =
let impls = implicits_of_context params in
List.map (fun x -> impls @ x) rdata.DataR.implfs
in
let rdata = { rdata with DataR.implfs } in
let binder_name = Namegen.next_ident_away id (Termops.vars_of_env (Global.env())) in
let fields = rdata.DataR.fields in
let data =
match fields with
| [ LocalAssum ({binder_name=Name proj_name} as binder, field)
| LocalDef ({binder_name=Name proj_name} as binder, _, field) ] when def ->
let binder = {binder with binder_name=Name binder_name} in
build_class_constant ~rdata ~univs field implfs params paramimpls coers binder id proj_name
| _ ->
build_record_constant ~rdata ~ubind ~univs ~variances ~cumulative ~template
fields params paramimpls coers id idbuild binder_name
in
let univs, params, fields =
match univs with
| Polymorphic_entry (nas, univs) ->
let usubst, auctx = Univ.abstract_universes nas univs in
let usubst = Univ.make_instance_subst usubst in
let map c = Vars.subst_univs_level_constr usubst c in
let fields = Context.Rel.map map fields in
let params = Context.Rel.map map params in
auctx, params, fields
| Monomorphic_entry _ ->
Univ.AUContext.empty, params, fields
in
let map (impl, projs) =
let k =
{ cl_univs = univs;
cl_impl = impl;
cl_strict = typeclasses_strict ();
cl_unique = typeclasses_unique ();
cl_context = params;
cl_props = fields;
cl_projs = projs }
in
let env = Global.env () in
let sigma = Evd.from_env env in
Classes.add_class env sigma k; impl
in
List.map map data
let add_constant_class env sigma cst =
let ty, univs = Typeops.type_of_global_in_context env (GlobRef.ConstRef cst) in
let r = (Environ.lookup_constant cst env).const_relevance in
let ctx, _ = decompose_prod_assum ty in
let args = Context.Rel.to_extended_vect Constr.mkRel 0 ctx in
let t = mkApp (mkConstU (cst, Univ.make_abstract_instance univs), args) in
let tc =
{ cl_univs = univs;
cl_impl = GlobRef.ConstRef cst;
cl_context = ctx;
cl_props = [LocalAssum (make_annot Anonymous r, t)];
cl_projs = [];
cl_strict = typeclasses_strict ();
cl_unique = typeclasses_unique ()
}
in
Classes.add_class env sigma tc;
Classes.set_typeclass_transparency (Tacred.EvalConstRef cst) false false
let add_inductive_class env sigma ind =
let mind, oneind = Inductive.lookup_mind_specif env ind in
let k =
let ctx = oneind.mind_arity_ctxt in
let univs = Declareops.inductive_polymorphic_context mind in
let inst = Univ.make_abstract_instance univs in
let ty = Inductive.type_of_inductive ((mind, oneind), inst) in
let r = oneind.mind_relevance in
{ cl_univs = univs;
cl_impl = GlobRef.IndRef ind;
cl_context = ctx;
cl_props = [LocalAssum (make_annot Anonymous r, ty)];
cl_projs = [];
cl_strict = typeclasses_strict ();
cl_unique = typeclasses_unique () }
in
Classes.add_class env sigma k
let warn_already_existing_class =
CWarnings.create ~name:"already-existing-class" ~category:"automation" Pp.(fun g ->
Printer.pr_global g ++ str " is already declared as a typeclass.")
let declare_existing_class g =
let env = Global.env () in
let sigma = Evd.from_env env in
if Typeclasses.is_class g then warn_already_existing_class g
else
match g with
| GlobRef.ConstRef x -> add_constant_class env sigma x
| GlobRef.IndRef x -> add_inductive_class env sigma x
| _ -> user_err ~hdr:"declare_existing_class"
(Pp.str"Unsupported class type, only constants and inductives are allowed")
open Vernacexpr
module Ast = struct
type t =
{ name : Names.lident
; is_coercion : coercion_flag
; binders: local_binder_expr list
; cfs : (local_decl_expr * record_field_attr) list
; idbuild : Id.t
; sort : constr_expr option
}
let to_datai { name; is_coercion; cfs; idbuild; sort } =
let fs = List.map fst cfs in
{ DataI.name = name.CAst.v
; arity = sort
; nots = List.map (fun (_, { rf_notation }) -> rf_notation) cfs
; fs
}
end
let check_unique_names records =
let acc (rf_decl, _) = match rf_decl with
Vernacexpr.AssumExpr({CAst.v=Name id},_,_) -> id::acc
| Vernacexpr.DefExpr ({CAst.v=Name id},_,_,_) -> id::acc
| _ -> acc in
let allnames =
List.fold_left (fun acc { Ast.name; cfs; _ } ->
name.CAst.v :: (List.fold_left extract_name acc cfs)) [] records
in
match List.duplicates Id.equal allnames with
| [] -> ()
| id :: _ -> user_err (str "Two objects have the same name" ++ spc () ++ quote (Id.print id))
let check_priorities kind records =
let isnot_class = match kind with Class false -> false | _ -> true in
let has_priority { Ast.cfs; _ } =
List.exists (fun (_, { rf_priority }) -> not (Option.is_empty rf_priority)) cfs
in
if isnot_class && List.exists has_priority records then
user_err Pp.(str "Priorities only allowed for type class substructures")
let records =
let data = List.map Ast.to_datai records in
let pss = List.map (fun { Ast.binders; _ } -> binders) records in
let ps = match pss with
| [] -> CErrors.anomaly (str "Empty record block")
| ps :: rem ->
let eq_local_binders bl1 bl2 = List.equal local_binder_eq bl1 bl2 in
let () =
if not (List.for_all (eq_local_binders ps) rem) then
user_err (str "Parameters should be syntactically the \
same for each inductive type.")
in
ps
in
ps, data
let class_struture ~cumulative ~template ~ubind ~impargs ~univs ~params def records data =
let { Ast.name; cfs; idbuild; _ }, rdata = match records, data with
| [r], [d] -> r, d
| _, _ ->
CErrors.user_err (str "Mutual definitional classes are not handled")
in
let coers = List.map (fun (_, { rf_subclass; rf_priority }) ->
match rf_subclass with
| Vernacexpr.BackInstance -> Some {hint_priority = rf_priority; hint_pattern = None}
| Vernacexpr.NoInstance -> None)
cfs
in
declare_class def ~cumulative ~ubind ~univs name.CAst.v idbuild
impargs params rdata template coers
let regular_structure ~cumulative ~template ~ubind ~impargs ~univs ~variances ~params ~finite
records data =
let adjust_impls impls = impargs @ [CAst.make None] @ impls in
let data = List.map (fun ({ DataR.implfs; _ } as d) -> { d with DataR.implfs = List.map adjust_impls implfs }) data in
let map rdata { Ast.name; is_coercion; cfs; idbuild; _ } =
let coers = List.map (fun (_, { rf_subclass ; rf_canonical }) ->
{ pf_subclass =
(match rf_subclass with Vernacexpr.BackInstance -> true | Vernacexpr.NoInstance -> false);
pf_canonical = rf_canonical })
cfs
in
{ Data.id = name.CAst.v; idbuild; rdata; is_coercion; coers }
in
let data = List.map2 map data records in
let inds = declare_structure ~cumulative finite ~ubind ~univs ~variances
impargs params template data
in
List.map (fun ind -> GlobRef.IndRef ind) inds
(** [fs] corresponds to fields and [ps] to parameters; [coers] is a
list telling if the corresponding fields must me declared as coercions
or subinstances. *)
let definition_structure udecl kind ~template ~cumulative ~poly
finite (records : Ast.t list) : GlobRef.t list =
let () = check_unique_names records in
let () = check_priorities kind records in
let ps, data = extract_record_data records in
let auto_template, impargs, ubind, univs, variances, params, data =
Vernacstate.System.protect (fun () ->
typecheck_params_and_fields (kind = Class true) poly udecl ps data) ()
in
let template = template, auto_template in
match kind with
| Class def ->
class_struture ~template ~ubind ~impargs ~cumulative ~params ~univs ~variances
def records data
| Inductive_kw | CoInductive | Variant | Record | Structure ->
regular_structure ~cumulative ~template ~ubind ~impargs ~univs ~variances ~params ~finite
records data
module Internal = struct
type nonrec projection_flags = projection_flags = {
pf_subclass: bool;
pf_canonical: bool;
}
let declare_projections = declare_projections
let declare_structure_entry = declare_structure_entry
end