Source file indtypes.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
open CErrors
open Util
open Names
open Term
open Constr
open Vars
open Declarations
open Declareops
open Inductive
open Environ
open Reduction
open Entries
open Context.Rel.Declaration
let weaker_noccur_between env x nvars t =
if noccur_between x nvars t then Some t
else
let t' = whd_all env t in
if noccur_between x nvars t' then Some t'
else None
exception InductiveError = Type_errors.InductiveError
type ill_formed_ind =
| LocalNonPos of int
| LocalNotEnoughArgs of int
| LocalNotConstructor of Constr.rel_context * int
| LocalNonPar of int * int * int
exception IllFormedInd of ill_formed_ind
let = decompose_prod_n_decls
let explain_ind_err id ntyp env nparamsctxt c err =
let open Type_errors in
let (_lparams,c') = mind_extract_params nparamsctxt c in
match err with
| LocalNonPos kt ->
raise (InductiveError (env, NonPos (c',mkRel (kt+nparamsctxt))))
| LocalNotEnoughArgs kt ->
raise (InductiveError
(env, NotEnoughArgs (c',mkRel (kt+nparamsctxt))))
| LocalNotConstructor (paramsctxt,nargs)->
let nparams = Context.Rel.nhyps paramsctxt in
raise (InductiveError
(env, NotConstructor (id,c',mkRel (ntyp+nparamsctxt),
nparams,nargs)))
| LocalNonPar (n,i,l) ->
raise (InductiveError
(env, NonPar (c',n,mkRel i,mkRel (l+nparamsctxt))))
let failwith_non_pos n ntypes c =
for k = n to n + ntypes - 1 do
if not (noccurn k c) then raise (IllFormedInd (LocalNonPos (k-n+1)))
done
let failwith_non_pos_vect n ntypes v =
Array.iter (failwith_non_pos n ntypes) v;
anomaly ~label:"failwith_non_pos_vect" (Pp.str "some k in [n;n+ntypes-1] should occur.")
let failwith_non_pos_list n ntypes l =
List.iter (failwith_non_pos n ntypes) l;
anomaly ~label:"failwith_non_pos_list" (Pp.str "some k in [n;n+ntypes-1] should occur.")
let check_correct_par ~chkpos (env,n,ntypes,_) paramdecls ind_index args =
let nparams = Context.Rel.nhyps paramdecls in
let args = Array.of_list args in
if Array.length args < nparams then
raise (IllFormedInd (LocalNotEnoughArgs ind_index));
let (params,realargs) = Array.chop nparams args in
let nparamdecls = List.length paramdecls in
let rec check param_index paramdecl_index = function
| [] -> ()
| LocalDef _ :: paramdecls ->
check param_index (paramdecl_index+1) paramdecls
| _::paramdecls ->
match kind (whd_all env params.(param_index)) with
| Rel w when Int.equal w paramdecl_index ->
check (param_index-1) (paramdecl_index+1) paramdecls
| _ ->
let paramdecl_index_in_env = paramdecl_index-n+nparamdecls+1 in
let err =
LocalNonPar (param_index+1, paramdecl_index_in_env, ind_index) in
raise (IllFormedInd err)
in check (nparams-1) (n-nparamdecls) paramdecls;
if chkpos && not (Array.for_all (noccur_between n ntypes) realargs) then
failwith_non_pos_vect n ntypes realargs
let compute_rec_par (env,n,_,_) paramsctxt nmr largs =
if Int.equal nmr 0 then 0 else
let (lpar,_) = List.chop nmr largs in
let rec find k index =
function
([],_) -> nmr
| (_,[]) -> assert false
| (lp, LocalDef _ :: paramsctxt) -> find k (index-1) (lp,paramsctxt)
| (p::lp,_::paramsctxt) ->
( match kind (whd_all env p) with
| Rel w when Int.equal w index -> find (k+1) (index-1) (lp,paramsctxt)
| _ -> k)
in find 0 (n-1) (lpar,List.rev paramsctxt)
let ienv_push_var (env, n, ntypes, lra) (x,a,ra) =
(push_rel (LocalAssum (x,a)) env, n+1, ntypes, (Norec,ra)::lra)
let ienv_push_inductive (env, n, ntypes, ra_env) ((mi,u),lrecparams) =
let auxntyp = 1 in
let specif = (lookup_mind_specif env mi, u) in
let ty = type_of_inductive specif in
let env' =
let r = Inductive.relevance_of_ind_body (snd (fst specif)) u in
let anon = Context.make_annot Anonymous r in
let decl = LocalAssum (anon, hnf_prod_applist env ty lrecparams) in
push_rel decl env in
let ra_env' =
(Mrec (RecArgInd mi),(Rtree.mk_rec_calls 1).(0)) ::
List.map (fun (r,t) -> (r,Rtree.lift 1 t)) ra_env in
let newidx = n + auxntyp in
(env', newidx, ntypes, ra_env')
let rec ienv_decompose_prod (env,_,_,_ as ienv) n c =
if Int.equal n 0 then (ienv,c) else
let c' = whd_all env c in
match kind c' with
Prod(na,a,b) ->
let ienv' = ienv_push_var ienv (na,a,mk_norec) in
ienv_decompose_prod ienv' (n-1) b
| _ -> assert false
let array_min nmr a = if Int.equal nmr 0 then 0 else
Array.fold_left (fun k (nmri,_) -> min k nmri) nmr a
(** [check_positivity_one ienv paramsctxt (mind,i) nnonrecargs lcnames indlc]
checks the positivity of the [i]-th member of the mutually
inductive definition [mind]. It returns an [Rtree.t] which
represents the position of the recursive calls of inductive in [i]
for use by the guard condition (terms at these positions are
considered sub-terms) as well as the number of of non-uniform
arguments (used to generate induction schemes, so a priori less
relevant to the kernel).
If [chkpos] is [false] then positivity is assumed, and
[check_positivity_one] computes the subterms occurrences in a
best-effort fashion. *)
let check_positivity_one ~chkpos recursive (env,_,ntypes,_ as ienv) paramsctxt (mind,i as ind) nnonrecargs lcnames indlc =
let nparamsctxt = Context.Rel.length paramsctxt in
let nmr = Context.Rel.nhyps paramsctxt in
(** Positivity of one argument [c] of a constructor (i.e. the
constructor [cn] has a type of the shape [… -> c … -> P], where,
more generally, the arrows may be dependent). *)
let rec check_strict_positivity (env, n, ntypes, ra_env as ienv) nmr c =
let x,largs = decompose_app_list (whd_all env c) in
match kind x with
| Prod (na,b,d) ->
let () = assert (List.is_empty largs) in
(** If one of the inductives of the mutually inductive
block occurs in the left-hand side of a product, then
such an occurrence is a non-strictly-positive
recursive call. Occurrences in the right-hand side of
the product must be strictly positive.*)
(match weaker_noccur_between env n ntypes b with
| None when chkpos ->
failwith_non_pos_list n ntypes [b]
| None ->
check_strict_positivity (ienv_push_var ienv (na, b, mk_norec)) nmr d
| Some b ->
check_strict_positivity (ienv_push_var ienv (na, b, mk_norec)) nmr d)
| Rel k ->
(match List.nth_opt ra_env (k-1) with
| Some (ra,rarg) ->
let largs = List.map (whd_all env) largs in
let nmr1 =
(match ra with
| Mrec (RecArgInd (mind',_)) ->
if Names.MutInd.CanOrd.equal mind mind'
then compute_rec_par ienv paramsctxt nmr largs
else nmr
| Norec | Mrec (RecArgPrim _) -> nmr)
in
(** The case where one of the inductives of the mutually
inductive block occurs as an argument of another is not
known to be safe. So Rocq rejects it. *)
if chkpos &&
not (List.for_all (noccur_between n ntypes) largs)
then failwith_non_pos_list n ntypes largs
else (nmr1,rarg)
| None -> (nmr,mk_norec))
| Ind ind_kn ->
(** If one of the inductives of the mutually inductive
block being defined appears in a parameter, then we
have a nested inductive type. The positivity is then
discharged to the [check_positivity_nested] function. *)
if List.for_all (noccur_between n ntypes) largs then (nmr,mk_norec)
else check_positivity_nested ienv nmr (ind_kn, largs)
| Const (c,_) when is_primitive_positive_container env c ->
if List.for_all (noccur_between n ntypes) largs then (nmr,mk_norec)
else check_positivity_nested_primitive ienv nmr (c, largs)
| _err ->
(** If an inductive of the mutually inductive block
appears in any other way, then the positivy check gives
up. *)
if not chkpos ||
(noccur_between n ntypes x &&
List.for_all (noccur_between n ntypes) largs)
then (nmr,mk_norec)
else failwith_non_pos_list n ntypes (x::largs)
(** [check_positivity_nested] handles the case of nested inductive
calls, that is, when an inductive types from the mutually
inductive block is called as an argument of an inductive types
(for the moment, this inductive type must be a previously
defined types, not one of the types of the mutually inductive
block being defined). *)
and check_positivity_nested (env,n,ntypes,_ra_env as ienv) nmr (((mind,_ as ind),u), largs) =
let (mib,mip) = lookup_mind_specif env ind in
let auxnrecpar = mib.mind_nparams_rec in
let auxnnonrecpar = mib.mind_nparams - auxnrecpar in
let (auxrecparams,auxnonrecargs) =
try List.chop auxnrecpar largs
with Failure _ -> raise (IllFormedInd (LocalNonPos n)) in
(** Inductives of the inductive block being defined are only
allowed to appear nested in the parameters of another inductive
type. Not in the proper indices. *)
if chkpos && not (List.for_all (noccur_between n ntypes) auxnonrecargs) then
failwith_non_pos_list n ntypes auxnonrecargs;
let auxntyp = mib.mind_ntypes in
if not (Int.equal auxntyp 1) then raise (IllFormedInd (LocalNonPos n));
let auxlcvect = abstract_mind_lc auxntyp auxnrecpar mind mip.mind_nf_lc in
let (env',_,_,_ as ienv') = ienv_push_inductive ienv ((ind,u),auxrecparams) in
let auxrecparams' = List.map (lift auxntyp) auxrecparams in
let irecargs_nmr =
(** Checks that the "nesting" inductive type is covariant in
the relevant parameters. In other words, that the
(nested) parameters which are instantiated with
inductives of the mutually inductive block occur
positively in the types of the nested constructors. *)
Array.map
(function c ->
let c' = hnf_prod_applist env' c auxrecparams' in
let (ienv',c') = ienv_decompose_prod ienv' auxnnonrecpar c' in
check_constructors ienv' false nmr c')
auxlcvect
in
let irecargs = Array.map snd irecargs_nmr
and nmr' = array_min nmr irecargs_nmr
in
(nmr',(Rtree.mk_rec [|mk_paths (Mrec (RecArgInd ind)) irecargs|]).(0))
and check_positivity_nested_primitive (env,n,ntypes,ra_env) nmr (c, largs) =
let ra_env = List.map (fun (r,t) -> (r,Rtree.lift 1 t)) ra_env in
let ienv = (env,n,ntypes,ra_env) in
let nmr',recargs = List.fold_left_map (check_strict_positivity ienv) nmr largs in
(nmr', (Rtree.mk_rec [| mk_paths (Mrec (RecArgPrim c)) [| recargs |] |]).(0))
(** [check_constructors ienv check_head nmr c] checks the positivity
condition in the type [c] of a constructor (i.e. that recursive
calls to the inductives of the mutually inductive definition
appear strictly positively in each of the arguments of the
constructor, see also [check_strict_positivity]). If [check_head] is [true],
then the type of the fully applied constructor (the "head" of
the type [c]) is checked to be the right (properly applied)
inductive type. *)
and check_constructors ienv check_head nmr c =
let rec check_constr_rec (env,n,ntypes,_ra_env as ienv) nmr lrec c =
let x,largs = decompose_app_list (whd_all env c) in
match kind x with
| Prod (na,b,d) ->
let () = assert (List.is_empty largs) in
if not recursive && not (noccur_between n ntypes b) then
raise (InductiveError (env,Type_errors.BadEntry));
let nmr',recarg = check_strict_positivity ienv nmr b in
let ienv' = ienv_push_var ienv (na,b,mk_norec) in
check_constr_rec ienv' nmr' (recarg::lrec) d
| hd ->
let () =
if check_head then
begin match hd with
| Rel j when Int.equal j (n + ntypes - i - 1) ->
check_correct_par ~chkpos ienv paramsctxt (ntypes - i) largs
| _ -> raise (IllFormedInd (LocalNotConstructor(paramsctxt,nnonrecargs)))
end
else
if chkpos &&
not (List.for_all (noccur_between n ntypes) largs)
then failwith_non_pos_list n ntypes largs
in
(nmr, List.rev lrec)
in check_constr_rec ienv nmr [] c
in
let irecargs_nmr =
Array.map2
(fun id c ->
let _,rawc = mind_extract_params nparamsctxt c in
try
check_constructors ienv true nmr rawc
with IllFormedInd err ->
explain_ind_err id (ntypes-i) env nparamsctxt c err)
(Array.of_list lcnames) indlc
in
let irecargs = Array.map snd irecargs_nmr
and nmr' = array_min nmr irecargs_nmr
in (nmr', mk_paths (Mrec (RecArgInd ind)) irecargs)
(** [check_positivity ~chkpos kn env_ar paramsctxt inds] checks that the mutually
inductive block [inds] is strictly positive.
If [chkpos] is [false] then positivity is assumed, and
[check_positivity_one] computes the subterms occurrences in a
best-effort fashion. *)
let check_positivity ~chkpos kn names env_ar_par paramsctxt finite inds =
let ntypes = Array.length inds in
let recursive = finite != BiFinite in
if not recursive && Array.length inds <> 1 then raise (InductiveError (env_ar_par,Type_errors.BadEntry));
let rc = Array.mapi (fun j t -> (Mrec (RecArgInd (kn,j)),t)) (Rtree.mk_rec_calls ntypes) in
let ra_env_ar = Array.rev_to_list rc in
let nparamsctxt = Context.Rel.length paramsctxt in
let nmr = Context.Rel.nhyps paramsctxt in
let check_one i (_,lcnames) (nindices,lc) =
let ra_env_ar_par =
List.init nparamsctxt (fun _ -> (Norec,mk_norec)) @ ra_env_ar in
let ienv = (env_ar_par, 1+nparamsctxt, ntypes, ra_env_ar_par) in
check_positivity_one ~chkpos recursive ienv paramsctxt (kn,i) nindices lcnames lc
in
let irecargs_nmr = Array.map2_i check_one names inds in
let irecargs = Array.map snd irecargs_nmr
and nmr' = array_min nmr irecargs_nmr
in (nmr',Rtree.mk_rec irecargs)
let fold_arity f acc params arity indices = match arity with
| RegularArity ar -> f acc ar.mind_user_arity
| TemplateArity _ ->
let fold_ctx acc ctx =
List.fold_left (fun acc d ->
Context.Rel.Declaration.fold_constr (fun c acc -> f acc c) d acc)
acc
ctx
in
fold_ctx (fold_ctx acc params) indices
let fold_inductive_blocks f acc params inds =
Array.fold_left (fun acc ((arity,lc),(indices,_),_) ->
fold_arity f (Array.fold_left f acc lc) params arity indices)
acc inds
let used_section_variables env params inds =
let fold l c = Id.Set.union (Environ.global_vars_set env c) l in
let ids = fold_inductive_blocks fold Id.Set.empty params inds in
keep_hyps env ids
let rel_vect n m = Array.init m (fun i -> mkRel(n+m-i))
(** From a rel context describing the constructor arguments,
build an expansion function.
The term built is expecting to be substituted first by
a substitution of the form [params, x : ind params] *)
let compute_projections (_, i as ind) mib =
let pkt = mib.mind_packets.(i) in
let (ctx, _) = pkt.mind_nf_lc.(0) in
let ctx, paramslet = List.chop pkt.mind_consnrealdecls.(0) ctx in
(** We build a substitution smashing the lets in the record parameters so
that typechecking projections requires just a substitution and not
matching with a parameter context. *)
let paramsletsubst =
let inst' = rel_vect 0 mib.mind_nparams in
let subst = subst_of_rel_context_instance paramslet inst' in
let subst =
mkRel 1 :: List.map (lift 1) subst in
subst
in
let projections decl (i, j, labs, rs, pbs, letsubst) =
match decl with
| LocalDef (_na,c,_t) ->
let c = liftn 1 j c in
let c2 = substl letsubst c in
let letsubst = c2 :: letsubst in
(i, j+1, labs, rs, pbs, letsubst)
| LocalAssum (na,t) ->
match na.Context.binder_name with
| Name id ->
let r = na.Context.binder_relevance in
let lab = Label.of_id id in
let kn = Projection.Repr.make ind ~proj_npars:mib.mind_nparams ~proj_arg:i lab in
let t = liftn 1 j t in
let projty = substl letsubst t in
let fterm = mkProj (Projection.make kn false, r, mkRel 1) in
(i + 1, j + 1, lab :: labs, r :: rs, projty :: pbs, fterm :: letsubst)
| Anonymous -> assert false
in
let (_, _, labs, rs, pbs, _letsubst) =
List.fold_right projections ctx (0, 1, [], [], [], paramsletsubst)
in
Array.of_list (List.rev labs),
Array.of_list (List.rev rs),
Array.of_list (List.rev pbs)
let build_inductive env ~sec_univs names prv univs template variance
paramsctxt kn isrecord isfinite inds nmr recargs =
let ntypes = Array.length inds in
let hyps = used_section_variables env paramsctxt inds in
let nparamargs = Context.Rel.nhyps paramsctxt in
let u = UVars.make_abstract_instance (universes_context univs) in
let subst = List.init ntypes (fun i -> mkIndU ((kn, ntypes - i - 1), u)) in
let build_one_packet (id,cnames) ((arity,lc),(indices,splayed_lc),squashed) recarg =
let lc = Array.map (substl subst) lc in
let nf_lc =
Array.map (fun (d, b) ->
decompose_prod_decls (substl subst (it_mkProd_or_LetIn b (d@paramsctxt))))
splayed_lc in
let consnrealdecls =
Array.map (fun (d,_) -> Context.Rel.length d)
splayed_lc in
let consnrealargs =
Array.map (fun (d,_) -> Context.Rel.nhyps d)
splayed_lc in
let mind_relevance = match arity with
| RegularArity { mind_sort;_ } -> Sorts.relevance_of_sort mind_sort
| TemplateArity a -> Sorts.relevance_of_sort a.template_level
in
let nconst, nblock = ref 0, ref 0 in
let transf arity =
if Int.equal arity 0 then
let p = (!nconst, 0) in
incr nconst; p
else
let p = (!nblock + 1, arity) in
incr nblock; p
in
let rtbl = Array.map transf consnrealargs in
{ mind_typename = id;
mind_arity = arity;
mind_arity_ctxt = indices @ paramsctxt;
mind_nrealargs = Context.Rel.nhyps indices;
mind_nrealdecls = Context.Rel.length indices;
mind_squashed = squashed;
mind_consnames = Array.of_list cnames;
mind_consnrealdecls = consnrealdecls;
mind_consnrealargs = consnrealargs;
mind_user_lc = lc;
mind_nf_lc = nf_lc;
mind_recargs = recarg;
mind_relevance;
mind_nb_constant = !nconst;
mind_nb_args = !nblock;
mind_reloc_tbl = rtbl;
} in
let packets = Array.map3 build_one_packet names inds recargs in
let variance, sec_variance = match variance with
| None -> None, None
| Some variance -> match sec_univs with
| None -> Some variance, None
| Some sec_univs ->
let _nsecq, nsecu = UVars.Instance.length sec_univs in
Some (Array.sub variance nsecu (Array.length variance - nsecu)),
Some (Array.sub variance 0 nsecu)
in
let univ_hyps = match sec_univs with
| None -> UVars.Instance.empty
| Some univs -> univs
in
let mib =
{ mind_record = NotRecord;
mind_ntypes = ntypes;
mind_finite = isfinite;
mind_hyps = hyps;
mind_univ_hyps = univ_hyps;
mind_nparams = nparamargs;
mind_nparams_rec = nmr;
mind_params_ctxt = paramsctxt;
mind_packets = packets;
mind_universes = univs;
mind_template = template;
mind_variance = variance;
mind_sec_variance = sec_variance;
mind_private = prv;
mind_typing_flags = Environ.typing_flags env;
}
in
let record_info = match isrecord with
| Some (Some rid) ->
(** The elimination criterion ensures that all projections can be defined. *)
let map i id =
let labs, rs, projs = compute_projections (kn, i) mib in
(id, labs, rs, projs)
in
PrimRecord (Array.mapi map rid)
| Some None -> FakeRecord
| None -> NotRecord
in
{ mib with mind_record = record_info }
let check_inductive env ~sec_univs kn mie =
let (env_ar_par, univs, template, variance, record, why_not_prim_record, paramsctxt, inds) =
IndTyping.typecheck_inductive env ~sec_univs mie
in
let chkpos = (Environ.typing_flags env).check_positive in
let names = Array.map_of_list (fun entry -> entry.mind_entry_typename, entry.mind_entry_consnames)
mie.mind_entry_inds
in
let (nmr,recargs) = check_positivity ~chkpos kn names
env_ar_par paramsctxt mie.mind_entry_finite
(Array.map (fun ((_,lc),(indices,_),_) -> Context.Rel.nhyps indices,lc) inds)
in
let mib =
build_inductive env ~sec_univs names mie.mind_entry_private univs template variance
paramsctxt kn record mie.mind_entry_finite
inds nmr recargs
in
mib, why_not_prim_record