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
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
open CErrors
open Util
open Names
open Cic
open Term
open Inductive
open Reduction
open Typeops
open Pp
open Declarations
open Environ
let rec debug_string_of_mp = function
| MPfile sl -> DirPath.to_string sl
| MPbound uid -> "bound("^MBId.to_string uid^")"
| MPdot (mp,l) -> debug_string_of_mp mp ^ "." ^ Label.to_string l
let rec string_of_mp = function
| MPfile sl -> DirPath.to_string sl
| MPbound uid -> MBId.to_string uid
| MPdot (mp,l) -> string_of_mp mp ^ "." ^ Label.to_string l
let string_of_mp mp =
if !Flags.debug then debug_string_of_mp mp else string_of_mp mp
let prkn kn =
let (mp,_,l) = KerName.repr kn in
str(string_of_mp mp ^ "." ^ Label.to_string l)
let prcon c =
let ck = Constant.canonical c in
let uk = Constant.user c in
if KerName.equal ck uk then prkn uk else (prkn uk ++str"(="++prkn ck++str")")
(* Same as noccur_between but may perform reductions.
Could be refined more... *)
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
let is_constructor_head t =
match fst(decompose_app t) with
| Rel _ -> true
| _ -> false
let conv_ctxt_prefix env (ctx1:rel_context) ctx2 =
let rec chk env rctx1 rctx2 =
match rctx1, rctx2 with
(LocalAssum (_,ty1) as d1)::rctx1', LocalAssum (_,ty2)::rctx2' ->
conv env ty1 ty2;
chk (push_rel d1 env) rctx1' rctx2'
| (LocalDef (_,bd1,ty1) as d1)::rctx1', LocalDef (_,bd2,ty2)::rctx2' ->
conv env ty1 ty2;
conv env bd1 bd2;
chk (push_rel d1 env) rctx1' rctx2'
| [],_ -> ()
| _ -> failwith "non convertible contexts" in
chk env (List.rev ctx1) (List.rev ctx2)
(************************************************************************)
(* Various well-formedness check for inductive declarations *)
(* Errors related to inductive constructions *)
type inductive_error =
| NonPos of env * constr * constr
| NotEnoughArgs of env * constr * constr
| NotConstructor of env * constr * constr
| NonPar of env * constr * int * constr * constr
| SameNamesTypes of Id.t
| SameNamesConstructors of Id.t
| SameNamesOverlap of Id.t list
| NotAnArity of Id.t
| BadEntry
exception InductiveError of inductive_error
(************************************************************************)
(************************************************************************)
(* Typing the arities and constructor types *)
let rec sorts_of_constr_args env t =
let t = whd_allnolet env t in
match t with
| Prod (name,c1,c2) ->
let varj = infer_type env c1 in
let env1 = push_rel (LocalAssum (name,c1)) env in
varj :: sorts_of_constr_args env1 c2
| LetIn (name,def,ty,c) ->
let env1 = push_rel (LocalDef (name,def,ty)) env in
sorts_of_constr_args env1 c
| _ when is_constructor_head t -> []
| _ -> anomaly ~label:"infos_and_sort" (Pp.str "not a positive constructor")
(* Prop and Set are small *)
let is_small_sort = function
| Prop _ -> true
| _ -> false
let is_logic_sort = function
| Prop Null -> true
| _ -> false
(* [infos] is a sequence of pair [islogic,issmall] for each type in
the product of a constructor or arity *)
let is_small_constr infos = List.for_all (fun s -> is_small_sort s) infos
let is_logic_constr infos = List.for_all (fun s -> is_logic_sort s) infos
(* An inductive definition is a "unit" if it has only one constructor
and that all arguments expected by this constructor are
logical, this is the case for equality, conjunction of logical properties
*)
let is_unit constrsinfos =
match constrsinfos with (* One info = One constructor *)
| [|constrinfos|] -> is_logic_constr constrinfos
| [||] -> (* type without constructors *) true
| _ -> false
let small_unit constrsinfos =
let issmall = Array.for_all is_small_constr constrsinfos
and isunit = is_unit constrsinfos in
issmall, isunit
(* check information related to inductive arity *)
let typecheck_arity env params inds =
let nparamargs = rel_context_nhyps params in
let nparamdecls = rel_context_length params in
let check_arity arctxt = function
| RegularArity mar ->
let ar = mar.mind_user_arity in
let _ = infer_type env ar in
conv env (it_mkProd_or_LetIn (Sort mar.mind_sort) arctxt) ar;
ar
| TemplateArity par ->
check_polymorphic_arity env params par;
it_mkProd_or_LetIn (Sort(Type par.template_level)) arctxt
in
let env_arities =
Array.fold_left
(fun env_ar ind ->
let ar_ctxt = ind.mind_arity_ctxt in
let _ = check_ctxt env ar_ctxt in
conv_ctxt_prefix env params ar_ctxt;
(* Arities (with params) are typed-checked here *)
let arity = check_arity ar_ctxt ind.mind_arity in
(* mind_nrealargs *)
let nrealargs = rel_context_nhyps ar_ctxt - nparamargs in
if ind.mind_nrealargs <> nrealargs then
failwith "bad number of real inductive arguments";
let nrealargs_ctxt = rel_context_length ar_ctxt - nparamdecls in
if ind.mind_nrealdecls <> nrealargs_ctxt then
failwith "bad length of real inductive arguments signature";
(* We do not need to generate the universe of full_arity; if
later, after the validation of the inductive definition,
full_arity is used as argument or subject to cast, an
upper universe will be generated *)
let id = ind.mind_typename in
let env_ar' = push_rel (LocalAssum (Name id, arity)) env_ar in
env_ar')
env
inds in
env_arities
(* Allowed eliminations *)
let check_predicativity env s small level =
match s, engagement env with
Type u, _ ->
(* let u' = fresh_local_univ () in *)
(* let cst = *)
(* merge_constraints (enforce_leq u u' empty_constraint) *)
(* (universes env) in *)
if not (Univ.check_leq (universes env) level u) then
failwith "impredicative Type inductive type"
| Prop Pos, ImpredicativeSet -> ()
| Prop Pos, _ ->
if not small then failwith "impredicative Set inductive type"
| Prop Null,_ -> ()
let sort_of_ind = function
| RegularArity mar -> mar.mind_sort
| TemplateArity par -> Type par.template_level
let all_sorts = [InProp;InSet;InType]
let small_sorts = [InProp;InSet]
let logical_sorts = [InProp]
let allowed_sorts issmall isunit s =
match family_of_sort s with
(* Type: all elimination allowed *)
| InType -> all_sorts
(* Small Set is predicative: all elimination allowed *)
| InSet when issmall -> all_sorts
(* Large Set is necessarily impredicative: forbids large elimination *)
| InSet -> small_sorts
(* Unitary/empty Prop: elimination to all sorts are realizable *)
(* unless the type is large. If it is large, forbids large elimination *)
(* which otherwise allows simulating the inconsistent system Type:Type *)
| InProp when isunit -> if issmall then all_sorts else small_sorts
(* Other propositions: elimination only to Prop *)
| InProp -> logical_sorts
let compute_elim_sorts env_ar params mib arity lc =
let inst = extended_rel_list 0 params in
let env_params = push_rel_context params env_ar in
let lc = Array.map
(fun c ->
hnf_prod_applist env_params (lift (rel_context_length params) c) inst)
lc in
let s = sort_of_ind arity in
let infos = Array.map (sorts_of_constr_args env_params) lc in
let (small,unit) = small_unit infos in
(* We accept recursive unit types... *)
(* compute the max of the sorts of the products of the constructor type *)
let level = max_inductive_sort
(Array.concat (Array.to_list (Array.map Array.of_list infos))) in
check_predicativity env_ar s small level;
allowed_sorts small unit s
let typecheck_one_inductive env params mib mip =
(* mind_typename and mind_consnames not checked *)
(* mind_reloc_tbl, mind_nb_constant, mind_nb_args not checked (VM) *)
(* mind_arity_ctxt, mind_arity, mind_nrealargs DONE (typecheck_arity) *)
(* mind_user_lc *)
let _ = Array.map (infer_type env) mip.mind_user_lc in
(* mind_nf_lc *)
let _ = Array.map (infer_type env) mip.mind_nf_lc in
Array.iter2 (conv env) mip.mind_nf_lc mip.mind_user_lc;
(* mind_consnrealdecls *)
let check_cons_args c n =
let ctx,_ = decompose_prod_assum c in
if n <> rel_context_length ctx - rel_context_length params then
failwith "bad number of real constructor arguments" in
Array.iter2 check_cons_args mip.mind_nf_lc mip.mind_consnrealdecls;
(* mind_kelim: checked by positivity criterion ? *)
let sorts =
compute_elim_sorts env params mib mip.mind_arity mip.mind_nf_lc in
let reject_sort s = not (List.mem_f family_equal s sorts) in
if List.exists reject_sort mip.mind_kelim then
failwith "elimination not allowed";
(* mind_recargs: checked by positivity criterion *)
()
(************************************************************************)
(************************************************************************)
(* Positivity *)
type ill_formed_ind =
| LocalNonPos of int
| LocalNotEnoughArgs of int
| LocalNotConstructor
| LocalNonPar of int * int * int
exception IllFormedInd of ill_formed_ind
(* [mind_extract_params mie] extracts the params from an inductive types
declaration, and checks that they are all present (and all the same)
for all the given types. *)
let mind_extract_params = decompose_prod_n_assum
let explain_ind_err ntyp env0 nbpar c err =
let (lpar,c') = mind_extract_params nbpar c in
let env = push_rel_context lpar env0 in
match err with
| LocalNonPos kt ->
raise (InductiveError (NonPos (env,c',Rel (kt+nbpar))))
| LocalNotEnoughArgs kt ->
raise (InductiveError
(NotEnoughArgs (env,c',Rel (kt+nbpar))))
| LocalNotConstructor ->
raise (InductiveError
(NotConstructor (env,c',Rel (ntyp+nbpar))))
| LocalNonPar (n,i,l) ->
raise (InductiveError
(NonPar (env,c',n,Rel i,Rel (l+nbpar))))
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")
(* Conclusion of constructors: check the inductive type is called with
the expected parameters *)
let check_correct_par (env,n,ntypes,_) hyps l largs =
let nparams = rel_context_nhyps hyps in
let largs = Array.of_list largs in
if Array.length largs < nparams then
raise (IllFormedInd (LocalNotEnoughArgs l));
let (lpar,largs') = Array.chop nparams largs in
let nhyps = List.length hyps in
let rec check k index = function
| [] -> ()
| LocalDef _ :: hyps -> check k (index+1) hyps
| _::hyps ->
match whd_all env lpar.(k) with
| Rel w when w = index -> check (k-1) (index+1) hyps
| _ -> raise (IllFormedInd (LocalNonPar (k+1,index,l)))
in check (nparams-1) (n-nhyps) hyps;
if not (Array.for_all (noccur_between n ntypes) largs') then
failwith_non_pos_vect n ntypes largs'
(* Arguments of constructor: check the number of recursive parameters nrecp.
the first parameters which are constant in recursive arguments
n is the current depth, nmr is the maximum number of possible
recursive parameters *)
let check_rec_par (env,n,_,_) hyps nrecp largs =
let (lpar,_) = List.chop nrecp largs in
let rec find index =
function
| ([],_) -> ()
| (_,[]) ->
failwith "number of recursive parameters cannot be greater than the number of parameters."
| (lp,LocalDef _ :: hyps) -> find (index-1) (lp,hyps)
| (p::lp,_::hyps) ->
(match whd_all env p with
| Rel w when w = index -> find (index-1) (lp,hyps)
| _ -> failwith "bad number of recursive parameters")
in find (n-1) (lpar,List.rev hyps)
let lambda_implicit_lift n a =
let lambda_implicit a = Lambda(Anonymous,Evar(0,[||]),a) in
iterate lambda_implicit n (lift n a)
(* This removes global parameters of the inductive types in lc (for
nested inductive types only ) *)
let abstract_mind_lc env ntyps npars lc =
if npars = 0 then
lc
else
let make_abs =
List.init ntyps
(function i -> lambda_implicit_lift npars (Rel (i+1)))
in
Array.map (substl make_abs) lc
(* [env] is the typing environment
[n] is the dB of the last inductive type
[ntypes] is the number of inductive types in the definition
(i.e. range of inductives is [n; n+ntypes-1])
[lra] is the list of recursive tree of each variable
*)
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),lpar) =
let auxntyp = 1 in
let specif = lookup_mind_specif env mi in
let env' =
let decl = LocalAssum (Anonymous,
hnf_prod_applist env (type_of_inductive env (specif,u)) lpar) in
push_rel decl env in
let ra_env' =
(Imbr mi,(Rtree.mk_rec_calls 1).(0)) ::
List.map (fun (r,t) -> (r,Rtree.lift 1 t)) ra_env in
(* New index of the inductive types *)
let newidx = n + auxntyp in
(env', newidx, ntypes, ra_env')
let rec ienv_decompose_prod (env,_,_,_ as ienv) n c =
if n=0 then (ienv,c) else
let c' = whd_all env c in
match 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
(* The recursive function that checks positivity and builds the list
of recursive arguments *)
let check_positivity_one (env, _,ntypes,_ as ienv) hyps nrecp (_,i as ind) indlc =
let lparams = rel_context_length hyps in
(* check the inductive types occur positively in [c] *)
let rec check_pos (env, n, ntypes, ra_env as ienv) c =
let x,largs = decompose_app (whd_all env c) in
match x with
| Prod (na,b,d) ->
assert (List.is_empty largs);
(match weaker_noccur_between env n ntypes b with
None -> failwith_non_pos_list n ntypes [b]
| Some b ->
check_pos (ienv_push_var ienv (na, b, mk_norec)) d)
| Rel k ->
(try
let (ra,rarg) = List.nth ra_env (k-1) in
(match ra with
Mrec _ -> check_rec_par ienv hyps nrecp largs
| _ -> ());
if not (List.for_all (noccur_between n ntypes) largs)
then failwith_non_pos_list n ntypes largs
else rarg
with Failure _ | Invalid_argument _ -> mk_norec)
| Ind ind_kn ->
(* If the inductive type being defined appears in a
parameter, then we have an imbricated type *)
if List.for_all (noccur_between n ntypes) largs then mk_norec
else check_positive_imbr ienv (ind_kn, largs)
| err ->
if noccur_between n ntypes x &&
List.for_all (noccur_between n ntypes) largs
then mk_norec
else failwith_non_pos_list n ntypes (x::largs)
(* accesses to the environment are not factorised, but is it worth it? *)
and check_positive_imbr (env,n,ntypes,ra_env as ienv) ((mi,u), largs) =
let (mib,mip) = lookup_mind_specif env mi in
let auxnpar = mib.mind_nparams_rec in
let nonrecpar = mib.mind_nparams - auxnpar in
let (lpar,auxlargs) =
try List.chop auxnpar largs
with Failure _ -> raise (IllFormedInd (LocalNonPos n)) in
(* If the inductive appears in the args (non params) then the
definition is not positive. *)
if not (List.for_all (noccur_between n ntypes) auxlargs) then
raise (IllFormedInd (LocalNonPos n));
(* We do not deal with imbricated mutual inductive types *)
let auxntyp = mib.mind_ntypes in
if auxntyp <> 1 then raise (IllFormedInd (LocalNonPos n));
(* The nested inductive type with parameters removed *)
let auxlcvect = abstract_mind_lc env auxntyp auxnpar mip.mind_nf_lc in
(* Extends the environment with a variable corresponding to
the inductive def *)
let (env',_,_,_ as ienv') = ienv_push_inductive ienv ((mi,u),lpar) in
(* Parameters expressed in env' *)
let lpar' = List.map (lift auxntyp) lpar in
let irecargs =
(* fails if the inductive type occurs non positively *)
(* with recursive parameters substituted *)
Array.map
(function c ->
let c' = hnf_prod_applist env' c lpar' in
(* skip non-recursive parameters *)
let (ienv',c') = ienv_decompose_prod ienv' nonrecpar c' in
check_constructors ienv' false c')
auxlcvect in
(Rtree.mk_rec [|mk_paths (Imbr mi) irecargs|]).(0)
(* check the inductive types occur positively in the products of C, if
check_head=true, also check the head corresponds to a constructor of
the ith type *)
and check_constructors ienv check_head c =
let rec check_constr_rec (env,n,ntypes,ra_env as ienv) lrec c =
let x,largs = decompose_app (whd_all env c) in
match x with
| Prod (na,b,d) ->
assert (List.is_empty largs);
let recarg = check_pos ienv b in
let ienv' = ienv_push_var ienv (na,b,mk_norec) in
check_constr_rec ienv' (recarg::lrec) d
| hd ->
if check_head then
match hd with
| Rel j when j = (n + ntypes - i - 1) ->
check_correct_par ienv hyps (ntypes-i) largs
| _ ->
raise (IllFormedInd LocalNotConstructor)
else
if not (List.for_all (noccur_between n ntypes) largs)
then raise (IllFormedInd (LocalNonPos n));
List.rev lrec
in check_constr_rec ienv [] c
in
let irecargs =
Array.map
(fun c ->
let _,rawc = mind_extract_params lparams c in
try
check_constructors ienv true rawc
with IllFormedInd err ->
explain_ind_err (ntypes-i) env lparams c err)
indlc
in mk_paths (Mrec ind) irecargs
let check_subtree t1 t2 =
let cmp_labels l1 l2 = l1 == Norec || eq_recarg l1 l2 in
if not (Rtree.equiv eq_recarg cmp_labels t1 t2)
then failwith "bad recursive trees"
(* if t1=t2 then () else msg_warning (str"TODO: check recursive positions")*)
let check_positivity env_ar mind params nrecp inds =
let ntypes = Array.length inds in
let rc =
Array.mapi (fun j t -> (Mrec(mind,j),t)) (Rtree.mk_rec_calls ntypes) in
let lra_ind = List.rev (Array.to_list rc) in
let lparams = rel_context_length params in
let check_one i mip =
let ra_env =
List.init lparams (fun _ -> (Norec,mk_norec)) @ lra_ind in
let ienv = (env_ar, 1+lparams, ntypes, ra_env) in
check_positivity_one ienv params nrecp (mind,i) mip.mind_nf_lc
in
let irecargs = Array.mapi check_one inds in
let wfp = Rtree.mk_rec irecargs in
Array.iter2 (fun ind wfpi -> check_subtree ind.mind_recargs wfpi) inds wfp
(************************************************************************)
(************************************************************************)
let check_inductive env kn mib =
Flags.if_verbose Feedback.msg_notice (str " checking ind: " ++ MutInd.print kn);
(* check mind_constraints: should be consistent with env *)
let env = add_constraints (Univ.UContext.constraints mib.mind_universes) env in
(* check mind_record : TODO ? check #constructor = 1 ? *)
(* check mind_finite : always OK *)
(* check mind_ntypes *)
if Array.length mib.mind_packets <> mib.mind_ntypes then
error "not the right number of packets";
(* check mind_params_ctxt *)
let params = mib.mind_params_ctxt in
let _ = check_ctxt env params in
(* check mind_nparams *)
if rel_context_nhyps params <> mib.mind_nparams then
error "number the right number of parameters";
(* mind_packets *)
(* - check arities *)
let env_ar = typecheck_arity env params mib.mind_packets in
(* - check constructor types *)
Array.iter (typecheck_one_inductive env_ar params mib) mib.mind_packets;
(* check mind_nparams_rec: positivity condition *)
check_positivity env_ar kn params mib.mind_nparams_rec mib.mind_packets;
(* check mind_equiv... *)
(* Now we can add the inductive *)
add_mind kn mib env
|