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
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
module RelDecl = Context.Rel.Declaration
let warn_auto_template =
CWarnings.create ~name:"auto-template" ~category:"vernacular" ~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
{ optdepr = false;
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 : 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 (UAnonymous {rigid=true}) -> (Some true)
| GSort (UNamed _) -> (Some false)
| GProd ( _, _, _, e)
| GLetIn (_, _, _, e)
| GLambda (_, _, _, e)
| GApp (e, _)
| GCast (e, _, _) -> check_type_conclusion e
| _ -> None
let make_anonymous_conclusion_flexible sigma = function
| None -> sigma
| Some (false, _) -> sigma
| Some (true, s) ->
(match EConstr.ESorts.kind sigma s with
| Type u ->
(match Univ.universe_level u with
| Some u ->
Evd.make_flexible_variable sigma ~algebraic:true u
| None -> sigma)
| _ -> sigma)
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 = check_type_conclusion c in
(constr_loc ind.ind_arity, c, impls, pseudo_poly)
let pretype_ind_arity env sigma (loc, c, impls, pseudo_poly) =
let sigma,t = understand_tcc 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 ->
let concl = match pseudo_poly with
| Some b -> Some (b, s)
| None -> None
in
sigma, (t, Retyping.relevance_of_sort s, concl, 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, EConstr.mkApp (EConstr.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.splay_prod_assum 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 Reduction.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 sign_level env evd sign =
fst (List.fold_right
(fun d (lev,env) ->
match d with
| LocalDef _ -> lev, push_rel d env
| LocalAssum _ ->
let s = Retyping.get_sort_of env evd (EConstr.of_constr (RelDecl.get_type d)) in
let u = univ_of_sort s in
(Univ.sup u lev, push_rel d env))
sign (Univ.Universe.sprop,env))
let sup_list min = List.fold_left Univ.sup min
let env evd min tys =
let sorts = List.map (fun ty ->
let ctx, concl = Reduction.dest_prod_assum env ty in
sign_level env evd (LocalAssum (make_annot Anonymous Sorts.Relevant, concl) :: ctx)) tys
in sup_list min sorts
let is_flexible_sort evd u =
match Univ.Universe.level u with
| Some l -> Evd.is_flexible_level evd l
| None -> false
let is_direct_sort_constraint s v = match s with
| Some u -> Univ.univ_level_mem u v
| None -> false
let solve_constraints_system levels level_bounds =
let open Univ in
let levels =
Array.mapi (fun i o ->
match o with
| Some u ->
(match Universe.level u with
| Some u -> Some u
| _ -> level_bounds.(i) <- Universe.sup level_bounds.(i) u; None)
| None -> None)
levels in
let v = Array.copy level_bounds in
let nind = Array.length v in
let clos = Array.map (fun _ -> Int.Set.empty) levels in
for i=0 to nind-1 do
for j=0 to nind-1 do
if not (Int.equal i j) && is_direct_sort_constraint levels.(j) v.(i) then
clos.(i) <- Int.Set.add j clos.(i);
done;
done;
let rec closure () =
let continue = ref false in
Array.iteri (fun i deps ->
let deps' =
Int.Set.fold (fun j acc -> Int.Set.union acc clos.(j)) deps deps
in
if Int.Set.equal deps deps' then ()
else (clos.(i) <- deps'; continue := true))
clos;
if !continue then closure ()
else ()
in
closure ();
for i=0 to nind-1 do
for j=0 to nind-1 do
if not (Int.equal i j) && Int.Set.mem j clos.(i) then
(v.(i) <- Universe.sup v.(i) level_bounds.(j));
done;
done;
v
let inductive_levels env evd arities inds =
let destarities = List.map (fun x -> x, Reduction.dest_arity env x) arities in
let levels = List.map (fun (x,(ctx,a)) ->
if Sorts.is_prop a || Sorts.is_sprop a then None
else Some (univ_of_sort a)) destarities
in
let cstrs_levels, sizes =
CList.split (List.map2 (fun (_,tys) (arity,(ctx,du)) ->
let len = List.length tys in
let minlev = Sorts.univ_of_sort du in
let minlev =
if len > 1 && not (is_impredicative_sort env du) then
Univ.sup minlev Univ.type0_univ
else minlev
in
let minlev =
if indices_matter env then begin
let ilev = sign_level env evd ctx in
Univ.sup ilev minlev
end
else minlev
in
let clev = extract_level env evd minlev tys in
(clev, len))
inds destarities)
in
let levels' = solve_constraints_system (Array.of_list levels)
(Array.of_list cstrs_levels)
in
let evd, arities =
CList.fold_left3 (fun (evd, arities) cu (arity,(ctx,du)) len ->
if is_impredicative_sort env du then
evd, (false, arity) :: arities
else
let evd =
if Sorts.is_set du then
if not (Evd.check_leq evd cu Univ.type0_univ) then
raise (InductiveError LargeNonPropInductiveNotInType)
else evd
else evd
in
let evd =
if len >= 2 && Univ.is_type0m_univ cu then
Evd.set_leq_sort env evd Sorts.set du
else evd
in
let duu = Sorts.univ_of_sort du in
let template_prop, evd =
if not (Univ.is_small_univ duu) && Univ.Universe.equal cu duu then
if is_flexible_sort evd duu && not (Evd.check_leq evd Univ.type0_univ duu)
then if Term.isArity arity
then true, Evd.set_eq_sort env evd Sorts.prop du
else false, Evd.set_eq_sort env evd Sorts.set du
else false, evd
else false, Evd.set_eq_sort env evd (sort_of_univ cu) du
in
(evd, (template_prop, arity) :: arities))
(evd,[]) (Array.to_list levels') destarities sizes
in evd, List.rev arities
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_polymorphism_candidate ~ctor_levels uctx params concl =
match uctx with
| UState.Monomorphic_entry uctx ->
let concltemplate = Option.cata (fun s -> not (Sorts.is_small s)) false concl in
if not concltemplate then false
else
let conclu = Option.cata Sorts.univ_of_sort Univ.type0m_univ concl in
Option.has_some @@ IndTyping.template_polymorphic_univs ~ctor_levels uctx params conclu
| UState.Polymorphic_entry _ -> false
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 (Stream.Error "pattern with quote not allowed here")
let restrict_inductive_universes sigma ctx_params arities constructors =
let merge_universes_of_constr c =
Univ.Level.Set.union (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 sigma uvars
let check_trivial_variances variances =
Array.iter (function
| None | Some Univ.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 = Univ.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 ~arityconcl ~constructors ~env_ar_params ~cumulative ~poly ~private_ind ~finite =
let sigma = Evd.minimize_universes sigma in
let nf = Evarutil.nf_evars_universes sigma in
let constructors = List.map (on_snd (List.map nf)) constructors in
let arities = List.map EConstr.(to_constr sigma) arities in
let sigma = List.fold_left make_anonymous_conclusion_flexible sigma arityconcl in
let sigma, arities = inductive_levels env_ar_params sigma arities constructors in
let sigma = Evd.minimize_universes sigma in
let nf = Evarutil.nf_evars_universes sigma in
let arities = List.map (on_snd nf) arities in
let constructors = List.map (on_snd (List.map nf)) constructors in
let ctx_params = List.map Termops.(map_rel_decl (EConstr.to_constr sigma)) ctx_params in
let arityconcl = List.map (Option.map (fun (_anon, s) -> EConstr.ESorts.kind sigma s)) arityconcl in
let sigma = restrict_inductive_universes sigma ctx_params (List.map snd arities) constructors in
let univ_entry, binders = Evd.check_univ_decl ~poly sigma udecl in
let entries = List.map4 (fun indname (templatearity, arity) concl (cnames,ctypes) ->
{ mind_entry_typename = indname;
mind_entry_arity = arity;
mind_entry_consnames = cnames;
mind_entry_lc = ctypes
})
indnames arities arityconcl constructors
in
let template = List.map4 (fun indname (templatearity, _) concl (_, ctypes) ->
let template_candidate () =
templatearity ||
let ctor_levels =
let add_levels c levels = Univ.Level.Set.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.Level.Set.empty ctx_params
in
List.fold_left (fun levels c -> add_levels c levels)
param_levels ctypes
in
template_polymorphism_candidate ~ctor_levels univ_entry ctx_params concl
in
match template with
| Some template ->
if poly && template then user_err
Pp.(strbrk "Template-polymorphism and universe polymorphism are not compatible.");
template
| None ->
should_auto_template indname (template_candidate ())
)
indnames arities arityconcl constructors
in
let is_template = List.for_all (fun t -> t) template in
let univ_entry, ctx = match univ_entry with
| UState.Monomorphic_entry ctx ->
if is_template then Template_ind_entry ctx, Univ.ContextSet.empty
else 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
mind_ent, binders, ctx
let interp_params 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 env sigma uparamsl in
let sigma, (impls, ((env_params, ctx_params), userimpls)) =
interp_context_evars ~program_mode:false ~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 env0 = if poly then env0 else Environ.set_universes_lbound env0 UGraph.Bound.Prop in
let sigma, env_params, (ctx_params, env_uparams, ctx_uparams, userimpls, useruimpls, impls, udecl, variances) =
interp_params 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 env_params) sigma arities in
let arities, relevances, arityconcl, 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_assum 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.Unsafe.to_constr (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 mie, binders, ctx = interp_mutual_inductive_constr ~template ~sigma ~ctx_params ~udecl ~variances ~arities ~arityconcl ~constructors ~env_ar_params ~poly ~finite ~cumulative ~private_ind ~indnames in
(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 lc = List.filter (fun (iscoe,_) -> iscoe) lc in
List.map mkqid (List.flatten(List.map (fun (_,_,_,lc) -> extract lc) indl))
let indl =
let paramsl = List.map (fun (_,params,_,_) -> params) indl in
match paramsl with
| [] -> anomaly (Pp.str "empty list of inductive types.")
| params::paramsl ->
if not (List.for_all (eq_params params) paramsl) then user_err Pp.(str
"Parameters should be syntactically the same for each inductive type.");
params
let indl =
List.map (fun ({CAst.v=indname},_,ar,lc) -> {
ind_name = indname;
ind_arity = Option.cata (fun x -> x) (CAst.make @@ CSort (Glob_term.UAnonymous {rigid=true})) 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
let do_mutual_inductive ~template udecl indl ~cumulative ~poly ?typing_flags ~private_ind ~uniform finite =
let (params,indl),coes,ntns = extract_mutual_inductive_declaration_components indl in
let ntns = List.map Metasyntax.prepare_where_notation ntns in
let indl = match params with
| uparams, Some params -> (uparams, params, indl)
| params, None -> match uniform with
| UniformParameters -> (params, [], indl)
| NonUniformParameters -> ([], params, indl)
in
let env = Global.env () in
let env = Environ.update_typing_flags ?typing_flags env in
let mie,binders,impls,ctx = interp_mutual_inductive_gen env ~template udecl indl ntns ~cumulative ~poly ~private_ind finite in
let binders = match mie.mind_entry_universes with
| Monomorphic_ind_entry -> (UState.Monomorphic_entry ctx, binders)
| Template_ind_entry ctx -> (UState.Monomorphic_entry ctx, binders)
| Polymorphic_ind_entry uctx -> (UState.Polymorphic_entry uctx, UnivNames.empty_binders)
in
DeclareUctx.declare_universe_context ~poly:false ctx;
ignore (DeclareInd.declare_mutual_inductive_with_eliminations ?typing_flags mie binders impls);
List.iter (Metasyntax.add_notation_interpretation ~local:false (Global.env ())) ntns;
List.iter (fun qid -> ComCoercion.try_add_new_coercion (Nametab.locate qid) ~local:false ~poly) coes
(** 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 []