Source file comInductive.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
module CVars = Vars
open Pp
open CErrors
open Sorts
open Util
open Context
open Environ
open Names
open Libnames
open Constrexpr
open Constrexpr_ops
open Constrintern
open Type_errors
open Pretyping
open Context.Rel.Declaration
open Entries
open EConstr
module RelDecl = Context.Rel.Declaration
let warn_auto_template =
CWarnings.create ~name:"auto-template" ~default:CWarnings.Disabled
(fun id ->
Pp.(strbrk "Automatically declaring " ++ Id.print id ++
strbrk " as template polymorphic. Use attributes or " ++
strbrk "disable Auto Template Polymorphism to avoid this warning."))
let should_auto_template =
let open Goptions in
let auto = ref true in
let () = declare_bool_option
{ optstage = Summary.Stage.Interp;
optdepr = None;
optkey = ["Auto";"Template";"Polymorphism"];
optread = (fun () -> !auto);
optwrite = (fun b -> auto := b); }
in
fun id would_auto ->
let b = !auto && would_auto in
if b then warn_auto_template id;
b
let push_types env idl rl tl =
List.fold_left3 (fun env id r t -> EConstr.push_rel (LocalAssum (make_annot (Name id) r,t)) env)
env idl rl tl
type structured_one_inductive_expr = {
ind_name : Id.t;
ind_arity_explicit : bool;
ind_arity : constr_expr;
ind_lc : (Id.t * constr_expr) list
}
exception Same of Id.t
let check_all_names_different indl =
let rec elements = function
| [] -> Id.Set.empty
| id :: l ->
let s = elements l in
if Id.Set.mem id s then raise (Same id) else Id.Set.add id s
in
let ind_names = List.map (fun ind -> ind.ind_name) indl in
let cstr_names = List.map_append (fun ind -> List.map fst ind.ind_lc) indl in
let ind_names = match elements ind_names with
| s -> s
| exception (Same t) -> raise (InductiveError (SameNamesTypes t))
in
let cstr_names = match elements cstr_names with
| s -> s
| exception (Same c) -> raise (InductiveError (SameNamesConstructors c))
in
let l = Id.Set.inter ind_names cstr_names in
if not (Id.Set.is_empty l) then
raise (InductiveError (SameNamesOverlap (Id.Set.elements l)))
(** Make the arity conclusion flexible to avoid generating an upper bound universe now,
only if the universe does not appear anywhere else.
This is really a hack to stay compatible with the semantics of template polymorphic
inductives which are recognized when a "Type" appears at the end of the conlusion in
the source syntax. *)
let rec check_type_conclusion ind =
let open Glob_term in
match DAst.get ind with
| GSort s ->
begin match s with
| (None, UAnonymous {rigid=UnivRigid}) ->
assert false
| (None, UAnonymous {rigid=UnivFlexible _}) -> false
| _ -> true
end
| GProd (_, _, _, _, e)
| GLetIn (_, _, _, _, e) ->
check_type_conclusion e
| _ -> false
let rec make_anonymous_conclusion_flexible ind =
let open Glob_term in
match DAst.get ind with
| GSort (None, UAnonymous {rigid=UnivRigid}) ->
Some (DAst.make ?loc:ind.loc (GSort (None, UAnonymous {rigid=UnivFlexible true})))
| GSort _ -> None
| GProd (a, b, c, d, e) -> begin match make_anonymous_conclusion_flexible e with
| None -> None
| Some e -> Some (DAst.make ?loc:ind.loc (GProd (a, b, c, d, e)))
end
| GLetIn (a, b, c, d, e) -> begin match make_anonymous_conclusion_flexible e with
| None -> None
| Some e -> Some (DAst.make ?loc:ind.loc (GLetIn (a, b, c, d, e)))
end
| _ -> None
type syntax_allows_template_poly = SyntaxAllowsTemplatePoly | SyntaxNoTemplatePoly
let intern_ind_arity env sigma ind =
let c = intern_gen IsType env sigma ind.ind_arity in
let impls = Implicit_quantifiers.implicits_of_glob_constr ~with_products:true c in
let pseudo_poly, c = match make_anonymous_conclusion_flexible c with
| None -> check_type_conclusion c, c
| Some c -> true, c
in
let template_syntax = if pseudo_poly then SyntaxAllowsTemplatePoly else SyntaxNoTemplatePoly in
(constr_loc ind.ind_arity, c, impls, template_syntax)
let pretype_ind_arity ~unconstrained_sorts env sigma (loc, c, impls, template_syntax) =
let flags = { Pretyping.all_no_fail_flags with unconstrained_sorts } in
let sigma,t = understand_tcc ~flags env sigma ~expected_type:IsType c in
match Reductionops.sort_of_arity env sigma t with
| exception Reduction.NotArity ->
user_err ?loc (str "Not an arity")
| s ->
sigma, (t, Retyping.relevance_of_sort s, template_syntax, impls)
let model_conclusion env sigma ind_rel params n arity_indices =
let model_head = EConstr.mkRel (n + Context.Rel.length params + ind_rel) in
let model_params = Context.Rel.instance EConstr.mkRel n params in
let sigma,model_indices =
List.fold_right
(fun (_,t) (sigma, subst) ->
let t = EConstr.Vars.substl subst (EConstr.Vars.liftn n (List.length subst + 1) t) in
let sigma, c = Evarutil.new_evar env sigma t in
sigma, c::subst)
arity_indices (sigma, []) in
sigma, mkApp (mkApp (model_head, model_params), Array.of_list (List.rev model_indices))
let interp_cstrs env (sigma, ind_rel) impls params ind arity =
let cnames,ctyps = List.split ind.ind_lc in
let arity_indices, cstr_sort = Reductionops.splay_arity env sigma arity in
let interp_cstr sigma ctyp =
let flags =
Pretyping.{ all_no_fail_flags with
use_typeclasses = UseTCForConv;
solve_unification_constraints = false }
in
let sigma, (ctyp, cimpl) = interp_type_evars_impls ~flags env sigma ~impls ctyp in
let ctx, concl = Reductionops.whd_decompose_prod_decls env sigma ctyp in
let concl_env = EConstr.push_rel_context ctx env in
let sigma_with_model_evars, model =
model_conclusion concl_env sigma ind_rel params (Context.Rel.length ctx) arity_indices
in
let sigma =
try Evarconv.unify concl_env sigma_with_model_evars Conversion.CONV concl model
with Evarconv.UnableToUnify (sigma,e) ->
user_err (Himsg.explain_pretype_error concl_env sigma
(Pretype_errors.CannotUnify (concl, model, (Some e))))
in
sigma, (ctyp, cimpl)
in
let sigma, (ctyps, cimpls) =
on_snd List.split @@
List.fold_left_map interp_cstr sigma ctyps
in
(sigma, pred ind_rel), (cnames, ctyps, cimpls)
let compute_constructor_levels env evd sign =
fst (List.fold_right
(fun d (lev,env) ->
match d with
| LocalDef _ -> lev, EConstr.push_rel d env
| LocalAssum _ ->
let s = Retyping.get_sort_of env evd (RelDecl.get_type d) in
(s :: lev, EConstr.push_rel d env))
sign ([],env))
let do_auto_prop_lowering = ref true
let () =
Goptions.declare_bool_option {
optstage = Interp;
optdepr = None;
optkey = ["Automatic";"Proposition";"Inductives"];
optread = (fun () -> !do_auto_prop_lowering);
optwrite = (fun b -> do_auto_prop_lowering := b);
}
let warn_auto_prop_lowering =
CWarnings.create ~name:"automatic-prop-lowering" ~category:Deprecation.Version.v8_20
Pp.(fun na ->
strbrk "Automatically putting " ++ Id.print na ++ strbrk " in Prop" ++ spc() ++
strbrk "even though it was declared with Type." ++ fnl() ++
strbrk "Unset Automatic Proposition Inductives to prevent this" ++ spc() ++
strbrk "(it will become the default in a future version)." ++ fnl() ++
strbrk "If you instead put " ++ Id.print na ++ strbrk " explicitly in Prop," ++ spc() ++
strbrk "set Dependent Proposition Eliminators around the declaration for full backwards compatibility.")
let is_flexible_sort evd s = match ESorts.kind evd s with
| Set | Prop | SProp -> false
| Type u | QSort (_, u) ->
match Univ.Universe.level u with
| Some l -> Evd.is_flexible_level evd l
| None -> false
let prop_lowering_candidates evd ~arities_explicit inds =
let less_than_2 = function [] | [_] -> true | _ :: _ :: _ -> false in
let is_prop_candidate_arity (raw_arity,(_,s),indices,ctors) =
less_than_2 ctors
&& EConstr.isArity evd raw_arity
&& is_flexible_sort evd s
&& not (Evd.check_leq evd ESorts.set s)
in
let candidates = List.filter_map (fun (explicit,(_,(_,s),_,_ as ind)) ->
if (!do_auto_prop_lowering || not explicit) && is_prop_candidate_arity ind
then Some s else None)
(List.combine arities_explicit inds)
in
let in_candidates s candidates = List.mem_f (ESorts.equal evd) s candidates in
let is_prop_candidate_size candidates (_,_,indices,ctors) =
List.for_all
(List.for_all (fun s -> match ESorts.kind evd s with
| SProp | Prop -> true
| Set -> false
| Type _ | QSort _ ->
not (Evd.check_leq evd ESorts.set s)
&& in_candidates s candidates))
(Option.List.cons indices ctors)
in
let rec spread_nonprop candidates =
let (changed, candidates) = List.fold_left
(fun (changed, candidates as acc) (raw_arity,(_,s),indices,ctors as ind) ->
if is_prop_candidate_size candidates ind
then acc
else if in_candidates s candidates
then (true, List.remove (ESorts.equal evd) s candidates)
else acc)
(false,candidates)
inds
in
if changed then spread_nonprop candidates
else candidates
in
let candidates = spread_nonprop candidates in
candidates
let include_constructor_argument env evd ~poly ~ctor_sort ~inductive_sort =
if poly then
let univ_of_sort s =
match ESorts.kind evd s with
| SProp | Prop -> None
| Set -> Some Univ.Universe.type0
| Type u | QSort (_,u) -> Some u
in
match univ_of_sort ctor_sort, univ_of_sort inductive_sort with
| _, None ->
assert false
| None, Some _ -> evd
| Some uctor, Some uind ->
let mk u = ESorts.make (Sorts.sort_of_univ u) in
Evd.set_leq_sort env evd (mk uctor) (mk uind)
else
match ESorts.kind evd ctor_sort with
| SProp | Prop -> evd
| Set | Type _ | QSort _ ->
Evd.set_leq_sort env evd ctor_sort inductive_sort
type default_dep_elim = DeclareInd.default_dep_elim = DefaultElim | PropButDepElim
let inductive_levels env evd ~poly ~indnames ~arities_explicit arities ctors =
let inds = List.map2 (fun x ctors ->
let ctx, s = Reductionops.dest_arity env evd x in
x, (ctx, s), List.map (compute_constructor_levels env evd) ctors)
arities ctors
in
let is_impredicative_sort evd s = is_impredicative_sort env (ESorts.kind evd s) in
let less_than_2 = function [] | [_] -> true | _ :: _ :: _ -> false in
let evd = List.fold_left (fun evd (raw_arity,(_,s),ctors) ->
if less_than_2 ctors || is_impredicative_sort evd s then evd
else
include_constructor_argument env evd ~poly ~ctor_sort:ESorts.set ~inductive_sort:s)
evd inds
in
let inds =
List.map (fun (raw_arity,(ctx,_ as arity),ctors) ->
let indices = if indices_matter env then
Some (compute_constructor_levels env evd ctx)
else None
in
(raw_arity,arity,indices,ctors))
inds
in
let candidates = prop_lowering_candidates evd ~arities_explicit inds in
let inds = List.map3 (fun na explicit (raw_arity,(ctx,s),indices,ctors) ->
if List.mem_f (ESorts.equal evd) s candidates then
let () = if explicit then warn_auto_prop_lowering na in
((PropButDepElim, mkArity (ctx, ESorts.prop)),ESorts.prop,indices,ctors)
else ((DefaultElim, raw_arity), s, indices, ctors))
indnames
arities_explicit
inds
in
let evd = List.fold_left (fun evd (_,s,indices,ctors) ->
if is_impredicative_sort evd s then evd
else List.fold_left
(List.fold_left (fun evd ctor_sort ->
include_constructor_argument env evd ~poly ~ctor_sort ~inductive_sort:s))
evd (Option.List.cons indices ctors))
evd inds
in
let arities = List.map (fun (arity,_,_,_) -> arity) inds in
evd, List.split arities
(** Template poly ***)
let check_named {CAst.loc;v=na} = match na with
| Name _ -> ()
| Anonymous ->
let msg = str "Parameters must be named." in
user_err ?loc msg
let template_polymorphic_univs ~ctor_levels uctx paramsctxt u =
let unbounded_from_below u cstrs =
let open Univ in
Univ.Constraints.for_all (fun (l, d, r) ->
match d with
| Eq -> not (Univ.Level.equal l u) && not (Univ.Level.equal r u)
| Lt | Le -> not (Univ.Level.equal r u))
cstrs
in
let fold_params accu decl = match decl with
| LocalAssum (_, p) ->
let c = Term.strip_prod_decls p in
begin match Constr.kind c with
| Constr.Sort (Type u) ->
begin match Univ.Universe.level u with
| Some l -> Univ.Level.Set.add l accu
| None -> accu
end
| _ -> accu
end
| LocalDef _ -> accu
in
let paramslevels = List.fold_left fold_params Univ.Level.Set.empty paramsctxt in
let check_level l =
Univ.Level.Set.mem l (Univ.ContextSet.levels uctx) &&
Univ.Level.Set.mem l paramslevels &&
(let () = assert (not @@ Univ.Level.is_set l) in true) &&
unbounded_from_below l (Univ.ContextSet.constraints uctx) &&
not (Univ.Level.Set.mem l ctor_levels)
in
let univs = Univ.Universe.levels u in
let univs = Univ.Level.Set.filter (fun l -> check_level l) univs in
univs
let template_polymorphism_candidate uctx params entry template_syntax = match template_syntax with
| SyntaxNoTemplatePoly -> Univ.Level.Set.empty
| SyntaxAllowsTemplatePoly ->
let _, concl = Term.destArity entry.mind_entry_arity in
match concl with
| Set | SProp | Prop -> Univ.Level.Set.empty
| Type u ->
let ctor_levels =
let add_levels c levels = Univ.Level.Set.union levels (CVars.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.Level.Set.empty params
in
List.fold_left (fun levels c -> add_levels c levels)
param_levels entry.mind_entry_lc
in
let univs = template_polymorphic_univs ~ctor_levels uctx params u in
univs
| QSort _ -> assert false
let split_universe_context subset (univs, csts) =
let subfilter (l, _, r) =
let () = assert (not @@ Univ.Level.Set.mem r subset) in
Univ.Level.Set.mem l subset
in
let subcst = Univ.Constraints.filter subfilter csts in
let rem = Univ.Level.Set.diff univs subset in
let remfilter (l, _, r) =
not (Univ.Level.Set.mem l subset) && not (Univ.Level.Set.mem r subset)
in
let remcst = Univ.Constraints.filter remfilter csts in
(subset, subcst), (rem, remcst)
let warn_no_template_universe =
CWarnings.create ~name:"no-template-universe"
(fun () -> Pp.str "This inductive type has no template universes.")
let compute_template_inductive ~user_template ~ctx_params ~univ_entry entry template_syntax =
match user_template, univ_entry with
| Some false, UState.Monomorphic_entry uctx ->
Monomorphic_ind_entry, uctx
| Some false, UState.Polymorphic_entry uctx ->
Polymorphic_ind_entry uctx, Univ.ContextSet.empty
| Some true, UState.Monomorphic_entry uctx ->
let template_universes = template_polymorphism_candidate uctx ctx_params entry template_syntax in
let template, global = split_universe_context template_universes uctx in
let () = if Univ.Level.Set.is_empty (fst template) then warn_no_template_universe () in
Template_ind_entry template, global
| Some true, UState.Polymorphic_entry _ ->
user_err Pp.(strbrk "Template-polymorphism and universe polymorphism are not compatible.")
| None, UState.Polymorphic_entry uctx ->
Polymorphic_ind_entry uctx, Univ.ContextSet.empty
| None, UState.Monomorphic_entry uctx ->
let template_candidate = template_polymorphism_candidate uctx ctx_params entry template_syntax in
let has_template = not @@ Univ.Level.Set.is_empty template_candidate in
let template = should_auto_template entry.mind_entry_typename has_template in
if template then
let template, global = split_universe_context template_candidate uctx in
Template_ind_entry template, global
else Monomorphic_ind_entry, uctx
let check_param = function
| CLocalDef (na, _, _, _) -> check_named na
| CLocalAssum (nas, _, Default _, _) -> List.iter check_named nas
| CLocalAssum (nas, _, Generalized _, _) -> ()
| CLocalPattern {CAst.loc} ->
Loc.raise ?loc (Gramlib.Grammar.Error "pattern with quote not allowed here")
let restrict_inductive_universes ~lbound sigma ctx_params arities constructors =
let merge_universes_of_constr c =
Univ.Level.Set.union (snd (EConstr.universes_of_constr sigma (EConstr.of_constr c))) in
let uvars = Univ.Level.Set.empty in
let uvars = Context.Rel.(fold_outside (Declaration.fold_constr merge_universes_of_constr) ctx_params ~init:uvars) in
let uvars = List.fold_right merge_universes_of_constr arities uvars in
let uvars = List.fold_right (fun (_,ctypes) -> List.fold_right merge_universes_of_constr ctypes) constructors uvars in
Evd.restrict_universe_context ~lbound sigma uvars
let check_trivial_variances variances =
Array.iter (function
| None | Some UVars.Variance.Invariant -> ()
| Some _ ->
CErrors.user_err
Pp.(strbrk "Universe variance was specified but this inductive will not be cumulative."))
variances
let variance_of_entry ~cumulative ~variances uctx =
match uctx with
| Monomorphic_ind_entry | Template_ind_entry _ -> check_trivial_variances variances; None
| Polymorphic_ind_entry uctx ->
if not cumulative then begin check_trivial_variances variances; None end
else
let lvs = Array.length variances in
let _, lus = UVars.UContext.size uctx in
assert (lvs <= lus);
Some (Array.append variances (Array.make (lus - lvs) None))
let interp_mutual_inductive_constr ~sigma ~template ~udecl ~variances ~ctx_params ~indnames ~arities_explicit ~arities ~template_syntax ~constructors ~env_ar_params ~cumulative ~poly ~private_ind ~finite =
let ctor_args = List.map (fun (_,tys) ->
List.map (fun ty ->
let ctx = fst (Reductionops.whd_decompose_prod_decls env_ar_params sigma ty) in
ctx)
tys)
constructors
in
let sigma, (default_dep_elim, arities) = inductive_levels env_ar_params sigma ~poly ~indnames ~arities_explicit arities ctor_args in
let lbound = if poly then UGraph.Bound.Set else UGraph.Bound.Prop in
let sigma = Evd.minimize_universes ~lbound sigma in
let arities = List.map EConstr.(to_constr sigma) arities in
let constructors = List.map (on_snd (List.map (EConstr.to_constr sigma))) constructors in
let ctx_params = List.map (fun d -> EConstr.to_rel_decl sigma d) ctx_params in
let sigma = restrict_inductive_universes ~lbound sigma ctx_params arities constructors in
let univ_entry, binders = Evd.check_univ_decl ~poly sigma udecl in
let entries = List.map3 (fun indname arity (cnames,ctypes) ->
{ mind_entry_typename = indname;
mind_entry_arity = arity;
mind_entry_consnames = cnames;
mind_entry_lc = ctypes
})
indnames arities constructors
in
let univ_entry, ctx = match entries, template_syntax with
| [entry], [template_syntax] ->
compute_template_inductive ~user_template:template ~ctx_params ~univ_entry entry template_syntax
| _ ->
let () = match template with
| Some true -> user_err Pp.(str "Template-polymorphism not allowed with mutual inductives.")
| _ -> ()
in
match univ_entry with
| UState.Monomorphic_entry ctx -> Monomorphic_ind_entry, ctx
| UState.Polymorphic_entry uctx -> Polymorphic_ind_entry uctx, Univ.ContextSet.empty
in
let variance = variance_of_entry ~cumulative ~variances univ_entry in
let mind_ent =
{ mind_entry_params = ctx_params;
mind_entry_record = None;
mind_entry_finite = finite;
mind_entry_inds = entries;
mind_entry_private = if private_ind then Some false else None;
mind_entry_universes = univ_entry;
mind_entry_variance = variance;
}
in
default_dep_elim, mind_ent, binders, ctx
let interp_params ~unconstrained_sorts env udecl uparamsl paramsl =
let sigma, udecl, variances = interp_cumul_univ_decl_opt env udecl in
let sigma, (uimpls, ((env_uparams, ctx_uparams), useruimpls)) =
interp_context_evars ~program_mode:false ~unconstrained_sorts env sigma uparamsl in
let sigma, (impls, ((env_params, ctx_params), userimpls)) =
interp_context_evars ~program_mode:false ~unconstrained_sorts ~impl_env:uimpls env_uparams sigma paramsl
in
sigma, env_params, (ctx_params, env_uparams, ctx_uparams,
userimpls, useruimpls, impls, udecl, variances)
let maybe_unify_params_in env_ar_par sigma ~ninds ~nparams ~binders:k c =
let is_ind sigma k c = match EConstr.kind sigma c with
| Constr.Rel n ->
n > k + nparams && n <= k + nparams + ninds
| _ -> false
in
let rec aux (env,k as envk) sigma c = match EConstr.kind sigma c with
| Constr.App (h,args) when is_ind sigma k h ->
Array.fold_left_i (fun i sigma arg ->
if i >= nparams || not (EConstr.isEvar sigma arg) then sigma
else begin try Evarconv.unify_delay env sigma arg (EConstr.mkRel (k+nparams-i))
with Evarconv.UnableToUnify _ ->
sigma
end)
sigma args
| _ -> Termops.fold_constr_with_full_binders
env sigma
(fun d (env,k) -> EConstr.push_rel d env, k+1)
aux envk sigma c
in
aux (env_ar_par,k) sigma c
let interp_mutual_inductive_gen env0 ~template udecl (uparamsl,paramsl,indl) notations ~cumulative ~poly ~private_ind finite =
check_all_names_different indl;
List.iter check_param paramsl;
if not (List.is_empty uparamsl) && not (List.is_empty notations)
then user_err (str "Inductives with uniform parameters may not have attached notations.");
let indnames = List.map (fun ind -> ind.ind_name) indl in
let ninds = List.length indl in
let unconstrained_sorts = not poly in
let sigma, env_params, (ctx_params, env_uparams, ctx_uparams, userimpls, useruimpls, impls, udecl, variances) =
interp_params ~unconstrained_sorts env0 udecl uparamsl paramsl
in
let arities = List.map (intern_ind_arity env_params sigma) indl in
let sigma, arities = List.fold_left_map (pretype_ind_arity ~unconstrained_sorts env_params) sigma arities in
let arities, relevances, template_syntax, indimpls = List.split4 arities in
let lift_ctx n ctx =
let t = EConstr.it_mkProd_or_LetIn EConstr.mkProp ctx in
let t = EConstr.Vars.lift n t in
let ctx, _ = EConstr.decompose_prod_decls sigma t in
ctx
in
let ctx_params_lifted, fullarities =
lift_ctx ninds ctx_params,
CList.map_i
(fun i c -> EConstr.Vars.lift i (EConstr.it_mkProd_or_LetIn c ctx_params))
0 arities
in
let env_ar = push_types env_uparams indnames relevances fullarities in
let env_ar_params = EConstr.push_rel_context ctx_params_lifted env_ar in
let indimpls = List.map (fun impls -> userimpls @ impls) indimpls in
let impls = compute_internalization_env env_uparams sigma ~impls Inductive indnames fullarities indimpls in
let ntn_impls = compute_internalization_env env_uparams sigma Inductive indnames fullarities indimpls in
let (sigma, _), constructors =
Metasyntax.with_syntax_protection (fun () ->
List.iter (Metasyntax.set_notation_for_interpretation env_params ntn_impls) notations;
List.fold_left2_map
(fun (sigma, ind_rel) ind arity ->
interp_cstrs env_ar_params (sigma, ind_rel) impls ctx_params_lifted
ind (EConstr.Vars.liftn ninds (Rel.length ctx_params + 1) arity))
(sigma, ninds) indl arities)
()
in
let nparams = Context.Rel.length ctx_params in
let sigma =
List.fold_left (fun sigma (_,ctyps,_) ->
List.fold_left (fun sigma ctyp ->
maybe_unify_params_in env_ar_params sigma ~ninds ~nparams ~binders:0 ctyp)
sigma ctyps)
sigma constructors
in
let nuparams = Context.Rel.length ctx_uparams in
let uargs = Context.Rel.instance EConstr.mkRel 0 ctx_uparams in
let uparam_subst =
List.init ninds EConstr.(fun i -> mkApp (mkRel (i + 1 + nuparams), uargs))
@ List.init nuparams EConstr.(fun i -> mkRel (i + 1)) in
let generalize_constructor c = EConstr.Vars.substnl uparam_subst nparams c in
let cimpls = List.map pi3 constructors in
let constructors = List.map (fun (cnames,ctypes,cimpls) ->
(cnames,List.map generalize_constructor ctypes))
constructors
in
let ctx_params = ctx_params @ ctx_uparams in
let userimpls = useruimpls @ userimpls in
let indimpls = List.map (fun iimpl -> useruimpls @ iimpl) indimpls in
let fullarities = List.map (fun c -> EConstr.it_mkProd_or_LetIn c ctx_uparams) fullarities in
let env_ar = push_types env0 indnames relevances fullarities in
let env_ar_params = EConstr.push_rel_context ctx_params env_ar in
let sigma = solve_remaining_evars all_and_fail_flags env_params sigma in
let impls =
List.map2 (fun indimpls cimpls ->
indimpls, List.map (fun impls ->
userimpls @ impls) cimpls)
indimpls cimpls
in
let arities_explicit = List.map (fun ar -> ar.ind_arity_explicit) indl in
let default_dep_elim, mie, binders, ctx = interp_mutual_inductive_constr ~template ~sigma ~ctx_params ~udecl ~variances ~arities_explicit ~arities ~template_syntax ~constructors ~env_ar_params ~poly ~finite ~cumulative ~private_ind ~indnames in
(default_dep_elim, mie, binders, impls, ctx)
let eq_local_binders bl1 bl2 =
List.equal local_binder_eq bl1 bl2
let eq_params (up1,p1) (up2,p2) =
eq_local_binders up1 up2 && Option.equal eq_local_binders p1 p2
let indl =
let mkqid (_,({CAst.v=id},_)) = qualid_of_ident id in
let iscoe (_, coe, inst) = match inst with
| Vernacexpr.(NoInstance | BackInstanceWarning) -> coe = Vernacexpr.AddCoercion
| _ -> user_err (Pp.str "'::' not allowed in inductives.") in
let lc = List.filter (fun (coe,_) -> iscoe coe) lc in
List.map mkqid (List.flatten(List.map (fun (_,_,_,lc) -> extract lc) indl))
exception DifferingParams of
string
* (Id.t * Vernacexpr.inductive_params_expr)
* (Id.t * Vernacexpr.inductive_params_expr)
let explain_differing_params kind (ind,p) (ind',p') =
let pr_params = function
| ([],None) -> str "no parameters"
| (up,p) ->
let env = Global.env() in
let sigma = Evd.from_env env in
let pr_binders = Ppconstr.pr_binders env sigma in
str "parameters" ++ spc() ++ hov 1 (quote (pr_binders up ++ pr_opt (fun p -> str "|" ++ spc() ++ pr_binders p) p))
in
v 0
(str "Parameters should be syntactically the same for each " ++ str kind ++ str " type." ++ spc() ++
hov 0 (str "Type " ++ quote (Id.print ind) ++ str " has " ++ pr_params p) ++ spc() ++
hov 0 (str "but type " ++ quote (Id.print ind') ++ str " has " ++ pr_params p') ++ str ".")
let () = CErrors.register_handler (function
| DifferingParams (kind, a, b) -> Some (explain_differing_params kind a b)
| _ -> None)
let error_differing_params ~kind (ind,p) (ind',p') =
Loc.raise ?loc:ind'.CAst.loc (DifferingParams (kind, (ind.CAst.v,p), (ind'.CAst.v,p')))
let indl =
match indl with
| [] -> anomaly (Pp.str "empty list of inductive types.")
| (ind,params,_,_)::rest ->
match List.find_opt (fun (_,p',_,_) -> not @@ eq_params params p') rest with
| None -> params
| Some (ind',p',_,_) ->
error_differing_params ~kind:"inductive" (ind,params) (ind',p')
let indl =
List.map (fun ({CAst.v=indname},_,ar,lc) -> {
ind_name = indname;
ind_arity_explicit = Option.has_some ar;
ind_arity = Option.default (CAst.make @@ CSort Constrexpr_ops.expr_Type_sort) ar;
ind_lc = List.map (fun (_,({CAst.v=id},t)) -> (id,t)) lc
}) indl
let indl =
let indl,ntnl = List.split indl in
let params = extract_params indl in
let coes = extract_coercions indl in
let indl = extract_inductive indl in
(params,indl), coes, List.flatten ntnl
type uniform_inductive_flag =
| UniformParameters
| NonUniformParameters
module Mind_decl = struct
type t = {
mie : Entries.mutual_inductive_entry;
default_dep_elim : default_dep_elim list;
nuparams : int option;
univ_binders : UnivNames.universe_binders;
implicits : DeclareInd.one_inductive_impls list;
uctx : Univ.ContextSet.t;
where_notations : Metasyntax.notation_interpretation_decl list;
coercions : Libnames.qualid list;
indlocs : Loc.t option list;
}
end
let rec count_binder_expr = function
| [] -> 0
| CLocalAssum(l,_,_,_) :: rest -> List.length l + count_binder_expr rest
| CLocalDef _ :: rest -> 1 + count_binder_expr rest
| CLocalPattern {CAst.loc} :: _ ->
Loc.raise ?loc (Gramlib.Grammar.Error "pattern with quote not allowed here")
let interp_mutual_inductive ~env ~template udecl indl ~cumulative ~poly ?typing_flags ~private_ind ~uniform finite =
let indlocs = List.map (fun ((n,_,_,_),_) -> n.CAst.loc) indl in
let (params,indl),coercions,ntns = extract_mutual_inductive_declaration_components indl in
let where_notations = List.map Metasyntax.prepare_where_notation ntns in
let indl, nuparams = match params with
| uparams, Some params -> (uparams, params, indl), Some (count_binder_expr params)
| params, None -> match uniform with
| UniformParameters -> (params, [], indl), Some 0
| NonUniformParameters -> ([], params, indl), None
in
let env = Environ.update_typing_flags ?typing_flags env in
let default_dep_elim, mie, univ_binders, implicits, uctx = interp_mutual_inductive_gen env ~template udecl indl where_notations ~cumulative ~poly ~private_ind finite in
let open Mind_decl in
{ mie; default_dep_elim; nuparams; univ_binders; implicits; uctx; where_notations; coercions; indlocs }
let do_mutual_inductive ~template udecl indl ~cumulative ~poly ?typing_flags ~private_ind ~uniform finite =
let open Mind_decl in
let env = Global.env () in
let { mie; default_dep_elim; univ_binders; implicits; uctx; where_notations; coercions; indlocs} =
interp_mutual_inductive ~env ~template udecl indl ~cumulative ~poly ?typing_flags ~private_ind ~uniform finite in
let binders = match mie.mind_entry_universes with
| Monomorphic_ind_entry -> (UState.Monomorphic_entry uctx, univ_binders)
| Template_ind_entry ctx -> (UState.Monomorphic_entry ctx, univ_binders)
| Polymorphic_ind_entry uctx -> (UState.Polymorphic_entry uctx, UnivNames.empty_binders)
in
Global.push_context_set ~strict:true uctx;
ignore (DeclareInd.declare_mutual_inductive_with_eliminations ~default_dep_elim ?typing_flags ~indlocs mie binders implicits);
List.iter (Metasyntax.add_notation_interpretation ~local:false (Global.env ())) where_notations;
List.iter (fun qid -> ComCoercion.try_add_new_coercion (Nametab.locate qid) ~local:false ~reversible:true) coercions
(** Prepare a "match" template for a given inductive type.
For each branch of the match, we list the constructor name
followed by enough pattern variables.
[Not_found] is raised if the given string isn't the qualid of
a known inductive type. *)
let make_cases ind =
let open Declarations in
let mib, mip = Global.lookup_inductive ind in
Util.Array.fold_right_i
(fun i (ctx, _) l ->
let al = Util.List.skipn (List.length mib.mind_params_ctxt) (List.rev ctx) in
let rec rename avoid = function
| [] -> []
| RelDecl.LocalDef _ :: l -> "_" :: rename avoid l
| RelDecl.LocalAssum (n, _)::l ->
let n' = Namegen.next_name_away_with_default (Id.to_string Namegen.default_dependent_ident) n.Context.binder_name avoid in
Id.to_string n' :: rename (Id.Set.add n' avoid) l in
let al' = rename Id.Set.empty al in
let consref = GlobRef.ConstructRef (ith_constructor_of_inductive ind (i + 1)) in
(Libnames.string_of_qualid (Nametab.shortest_qualid_of_global Id.Set.empty consref) :: al') :: l)
mip.mind_nf_lc []
module Internal =
struct
let inductive_levels = inductive_levels
let do_auto_prop_lowering = do_auto_prop_lowering
let error_differing_params = error_differing_params
end