1
(************************************************************************)
2
(* v * The Coq Proof Assistant / The Coq Development Team *)
3
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
4
(* \VV/ **************************************************************)
5
(* // * This file is distributed under the terms of the *)
6
(* * GNU Lesser General Public License Version 2.1 *)
7
(************************************************************************)
9
(* $Id: indtypes.ml 11784 2009-01-14 11:36:32Z herbelin $ *)
23
(* Same as noccur_between but may perform reductions.
24
Could be refined more... *)
25
let weaker_noccur_between env x nvars t =
26
if noccur_between x nvars t then Some t
28
let t' = whd_betadeltaiota env t in
29
if noccur_between x nvars t' then Some t'
32
let is_constructor_head t =
33
isRel(fst(decompose_app t))
35
(************************************************************************)
36
(* Various well-formedness check for inductive declarations *)
38
(* Errors related to inductive constructions *)
39
type inductive_error =
40
| NonPos of env * constr * constr
41
| NotEnoughArgs of env * constr * constr
42
| NotConstructor of env * identifier * constr * constr * int * int
43
| NonPar of env * constr * int * constr * constr
44
| SameNamesTypes of identifier
45
| SameNamesConstructors of identifier
46
| SameNamesOverlap of identifier list
47
| NotAnArity of identifier
49
| LargeNonPropInductiveNotInType
51
exception InductiveError of inductive_error
53
(* [check_constructors_names id s cl] checks that all the constructors names
54
appearing in [l] are not present in the set [s], and returns the new set
55
of names. The name [id] is the name of the current inductive type, used
56
when reporting the error. *)
58
let check_constructors_names =
59
let rec check idset = function
62
if Idset.mem c idset then
63
raise (InductiveError (SameNamesConstructors c))
65
check (Idset.add c idset) cl
69
(* [mind_check_names mie] checks the names of an inductive types declaration,
70
and raises the corresponding exceptions when two types or two constructors
71
have the same name. *)
73
let mind_check_names mie =
74
let rec check indset cstset = function
77
let id = ind.mind_entry_typename in
78
let cl = ind.mind_entry_consnames in
79
if Idset.mem id indset then
80
raise (InductiveError (SameNamesTypes id))
82
let cstset' = check_constructors_names cstset cl in
83
check (Idset.add id indset) cstset' inds
85
check Idset.empty Idset.empty mie.mind_entry_inds
86
(* The above verification is not necessary from the kernel point of
87
vue since inductive and constructors are not referred to by their
88
name, but only by the name of the inductive packet and an index. *)
90
let mind_check_arities env mie =
91
let check_arity id c =
92
if not (is_arity env c) then
93
raise (InductiveError (NotAnArity id))
96
(fun {mind_entry_typename=id; mind_entry_arity=ar} -> check_arity id ar)
99
(************************************************************************)
100
(************************************************************************)
102
(* Typing the arities and constructor types *)
104
let is_logic_type t = (t.utj_type = prop_sort)
106
(* [infos] is a sequence of pair [islogic,issmall] for each type in
107
the product of a constructor or arity *)
109
let is_small infos = List.for_all (fun (logic,small) -> small) infos
110
let is_logic_constr infos = List.for_all (fun (logic,small) -> logic) infos
112
(* An inductive definition is a "unit" if it has only one constructor
113
and that all arguments expected by this constructor are
114
logical, this is the case for equality, conjunction of logical properties
116
let is_unit constrsinfos =
117
match constrsinfos with (* One info = One constructor *)
118
| [constrinfos] -> is_logic_constr constrinfos
119
| [] -> (* type without constructors *) true
122
let rec infos_and_sort env t =
123
let t = whd_betadeltaiota env t in
124
match kind_of_term t with
125
| Prod (name,c1,c2) ->
126
let (varj,_) = infer_type env c1 in
127
let env1 = Environ.push_rel (name,None,varj.utj_val) env in
128
let logic = is_logic_type varj in
129
let small = Term.is_small varj.utj_type in
130
(logic,small) :: (infos_and_sort env1 c2)
131
| _ when is_constructor_head t -> []
132
| _ -> (* don't fail if not positive, it is tested later *) []
134
let small_unit constrsinfos =
135
let issmall = List.for_all is_small constrsinfos
136
and isunit = is_unit constrsinfos in
139
(* Computing the levels of polymorphic inductive types
141
For each inductive type of a block that is of level u_i, we have
142
the constraints that u_i >= v_i where v_i is the type level of the
143
types of the constructors of this inductive type. Each v_i depends
144
of some of the u_i and of an extra (maybe non variable) universe,
145
say w_i that summarize all the other constraints. Typically, for
146
three inductive types, we could have
152
From this system of inequations, we shall deduce
159
let extract_level (_,_,_,lc,lev) =
160
(* Enforce that the level is not in Prop if more than two constructors *)
161
if Array.length lc >= 2 then sup type0_univ lev else lev
163
let inductive_levels arities inds =
164
let levels = Array.map pi3 arities in
165
let cstrs_levels = Array.map extract_level inds in
166
(* Take the transitive closure of the system of constructors *)
167
(* level constraints and remove the recursive dependencies *)
168
solve_constraints_system levels cstrs_levels
170
(* This (re)computes informations relevant to extraction and the sort of an
171
arity or type constructor; we do not to recompute universes constraints *)
173
let constraint_list_union =
174
List.fold_left Constraint.union Constraint.empty
176
let infer_constructor_packet env_ar params lc =
177
(* builds the typing context "Gamma, I1:A1, ... In:An, params" *)
178
let env_ar_par = push_rel_context params env_ar in
179
(* type-check the constructors *)
180
let jlc,cstl = List.split (List.map (infer_type env_ar_par) lc) in
181
let cst = constraint_list_union cstl in
182
let jlc = Array.of_list jlc in
183
(* generalize the constructor over the parameters *)
184
let lc'' = Array.map (fun j -> it_mkProd_or_LetIn j.utj_val params) jlc in
185
(* compute the max of the sorts of the products of the constructor type *)
186
let level = max_inductive_sort (Array.map (fun j -> j.utj_type) jlc) in
188
let info = small_unit (List.map (infos_and_sort env_ar_par) lc) in
190
(info,lc'',level,cst)
192
(* Type-check an inductive definition. Does not check positivity
194
let typecheck_inductive env mie =
195
if mie.mind_entry_inds = [] then anomaly "empty inductive types declaration";
196
(* Check unicity of names *)
197
mind_check_names mie;
198
mind_check_arities env mie;
199
(* Params are typed-checked here *)
200
let env_params, params, cst1 = infer_local_decls env mie.mind_entry_params in
201
(* We first type arity of each inductive definition *)
202
(* This allows to build the environment of arities and to share *)
203
(* the set of constraints *)
204
let cst, env_arities, rev_arity_list =
206
(fun (cst,env_ar,l) ind ->
207
(* Arities (without params) are typed-checked here *)
208
let arity, cst2 = infer_type env_params ind.mind_entry_arity in
209
(* We do not need to generate the universe of full_arity; if
210
later, after the validation of the inductive definition,
211
full_arity is used as argument or subject to cast, an
212
upper universe will be generated *)
213
let full_arity = it_mkProd_or_LetIn arity.utj_val params in
214
let cst = Constraint.union cst cst2 in
215
let id = ind.mind_entry_typename in
216
let env_ar' = push_rel (Name id, None, full_arity) env_ar in
218
(* Decide that if the conclusion is not explicitly Type *)
219
(* then the inductive type is not polymorphic *)
220
match kind_of_term (snd (decompose_prod_assum arity.utj_val)) with
221
| Sort (Type u) -> Some u
223
(cst,env_ar',(id,full_arity,lev)::l))
225
mie.mind_entry_inds in
227
let arity_list = List.rev rev_arity_list in
229
(* Now, we type the constructors (without params) *)
232
(fun ind arity_data (inds,cst) ->
233
let (info,lc',cstrs_univ,cst') =
234
infer_constructor_packet env_arities params ind.mind_entry_lc in
235
let consnames = ind.mind_entry_consnames in
236
let ind' = (arity_data,consnames,info,lc',cstrs_univ) in
237
(ind'::inds, Constraint.union cst cst'))
242
let inds = Array.of_list inds in
243
let arities = Array.of_list arity_list in
244
let param_ccls = List.fold_left (fun l (_,b,p) ->
246
let _,c = dest_prod_assum env p in
247
let u = match kind_of_term c with Sort (Type u) -> Some u | _ -> None in
252
(* Compute/check the sorts of the inductive types *)
253
let ind_min_levels = inductive_levels arities inds in
255
array_fold_map2' (fun ((id,full_arity,ar_level),cn,info,lc,_) lev cst ->
256
let sign, s = dest_arity env full_arity in
257
let status,cst = match s with
258
| Type u when ar_level <> None (* Explicitly polymorphic *)
259
&& no_upper_constraints u cst ->
260
(* The polymorphic level is a function of the level of the *)
261
(* conclusions of the parameters *)
262
(* We enforce [u >= lev] in case [lev] has a strict upper *)
263
(* constraints over [u] *)
264
Inr (param_ccls, lev), enforce_geq u lev cst
265
| Type u (* Not an explicit occurrence of Type *) ->
266
Inl (info,full_arity,s), enforce_geq u lev cst
267
| Prop Pos when engagement env <> Some ImpredicativeSet ->
268
(* Predicative set: check that the content is indeed predicative *)
269
if not (is_type0m_univ lev) & not (is_type0_univ lev) then
270
raise (InductiveError LargeNonPropInductiveNotInType);
271
Inl (info,full_arity,s), cst
273
Inl (info,full_arity,s), cst in
274
(id,cn,lc,(sign,status)),cst)
275
inds ind_min_levels cst in
277
(env_arities, params, inds, cst)
279
(************************************************************************)
280
(************************************************************************)
283
type ill_formed_ind =
285
| LocalNotEnoughArgs of int
286
| LocalNotConstructor
287
| LocalNonPar of int * int
289
exception IllFormedInd of ill_formed_ind
291
(* [mind_extract_params mie] extracts the params from an inductive types
292
declaration, and checks that they are all present (and all the same)
293
for all the given types. *)
295
let mind_extract_params = decompose_prod_n_assum
297
let explain_ind_err id ntyp env0 nbpar c nargs err =
298
let (lpar,c') = mind_extract_params nbpar c in
299
let env = push_rel_context lpar env0 in
302
raise (InductiveError (NonPos (env,c',mkRel (kt+nbpar))))
303
| LocalNotEnoughArgs kt ->
304
raise (InductiveError
305
(NotEnoughArgs (env,c',mkRel (kt+nbpar))))
306
| LocalNotConstructor ->
307
raise (InductiveError
308
(NotConstructor (env,id,c',mkRel (ntyp+nbpar),nbpar,nargs)))
309
| LocalNonPar (n,l) ->
310
raise (InductiveError
311
(NonPar (env,c',n,mkRel (nbpar-n+1), mkRel (l+nbpar))))
313
let failwith_non_pos n ntypes c =
314
for k = n to n + ntypes - 1 do
315
if not (noccurn k c) then raise (IllFormedInd (LocalNonPos (k-n+1)))
318
let failwith_non_pos_vect n ntypes v =
319
Array.iter (failwith_non_pos n ntypes) v;
320
anomaly "failwith_non_pos_vect: some k in [n;n+ntypes-1] should occur"
322
let failwith_non_pos_list n ntypes l =
323
List.iter (failwith_non_pos n ntypes) l;
324
anomaly "failwith_non_pos_list: some k in [n;n+ntypes-1] should occur"
326
(* Check the inductive type is called with the expected parameters *)
327
let check_correct_par (env,n,ntypes,_) hyps l largs =
328
let nparams = rel_context_nhyps hyps in
329
let largs = Array.of_list largs in
330
if Array.length largs < nparams then
331
raise (IllFormedInd (LocalNotEnoughArgs l));
332
let (lpar,largs') = array_chop nparams largs in
333
let nhyps = List.length hyps in
334
let rec check k index = function
336
| (_,Some _,_)::hyps -> check k (index+1) hyps
338
match kind_of_term (whd_betadeltaiota env lpar.(k)) with
339
| Rel w when w = index -> check (k-1) (index+1) hyps
340
| _ -> raise (IllFormedInd (LocalNonPar (k+1,l)))
341
in check (nparams-1) (n-nhyps) hyps;
342
if not (array_for_all (noccur_between n ntypes) largs') then
343
failwith_non_pos_vect n ntypes largs'
345
(* Computes the maximum number of recursive parameters :
346
the first parameters which are constant in recursive arguments
347
n is the current depth, nmr is the maximum number of possible
348
recursive parameters *)
350
let compute_rec_par (env,n,_,_) hyps nmr largs =
351
if nmr = 0 then 0 else
352
(* start from 0, hyps will be in reverse order *)
353
let (lpar,_) = list_chop nmr largs in
354
let rec find k index =
357
| (_,[]) -> assert false (* |hyps|>=nmr *)
358
| (lp,(_,Some _,_)::hyps) -> find k (index-1) (lp,hyps)
360
( match kind_of_term (whd_betadeltaiota env p) with
361
| Rel w when w = index -> find (k+1) (index-1) (lp,hyps)
363
in find 0 (n-1) (lpar,List.rev hyps)
365
(* This removes global parameters of the inductive types in lc (for
366
nested inductive types only ) *)
367
let abstract_mind_lc env ntyps npars lc =
373
(function i -> lambda_implicit_lift npars (mkRel (i+1))) ntyps
375
Array.map (substl make_abs) lc
377
(* [env] is the typing environment
378
[n] is the dB of the last inductive type
379
[ntypes] is the number of inductive types in the definition
380
(i.e. range of inductives is [n; n+ntypes-1])
381
[lra] is the list of recursive tree of each variable
383
let ienv_push_var (env, n, ntypes, lra) (x,a,ra) =
384
(push_rel (x,None,a) env, n+1, ntypes, (Norec,ra)::lra)
386
let ienv_push_inductive (env, n, ntypes, ra_env) (mi,lpar) =
388
let specif = lookup_mind_specif env mi in
390
push_rel (Anonymous,None,
391
hnf_prod_applist env (type_of_inductive env specif) lpar) env in
393
(Imbr mi,(Rtree.mk_rec_calls 1).(0)) ::
394
List.map (fun (r,t) -> (r,Rtree.lift 1 t)) ra_env in
395
(* New index of the inductive types *)
396
let newidx = n + auxntyp in
397
(env', newidx, ntypes, ra_env')
399
let array_min nmr a = if nmr = 0 then 0 else
400
Array.fold_left (fun k (nmri,_) -> min k nmri) nmr a
402
(* The recursive function that checks positivity and builds the list
403
of recursive arguments *)
404
let check_positivity_one (env, _,ntypes,_ as ienv) hyps i nargs lcnames indlc =
405
let lparams = rel_context_length hyps in
406
let nmr = rel_context_nhyps hyps in
407
(* check the inductive types occur positively in [c] *)
408
let rec check_pos (env, n, ntypes, ra_env as ienv) nmr c =
409
let x,largs = decompose_app (whd_betadeltaiota env c) in
410
match kind_of_term x with
413
(match weaker_noccur_between env n ntypes b with
414
None -> failwith_non_pos_list n ntypes [b]
416
check_pos (ienv_push_var ienv (na, b, mk_norec)) nmr d)
418
(try let (ra,rarg) = List.nth ra_env (k-1) in
421
Mrec _ -> compute_rec_par ienv hyps nmr largs
424
if not (List.for_all (noccur_between n ntypes) largs)
425
then failwith_non_pos_list n ntypes largs
427
with Failure _ | Invalid_argument _ -> (nmr,mk_norec))
429
(* If the inductive type being defined appears in a
430
parameter, then we have an imbricated type *)
431
if List.for_all (noccur_between n ntypes) largs then (nmr,mk_norec)
432
else check_positive_imbr ienv nmr (ind_kn, largs)
434
if noccur_between n ntypes x &&
435
List.for_all (noccur_between n ntypes) largs
437
else failwith_non_pos_list n ntypes (x::largs)
439
(* accesses to the environment are not factorised, but is it worth? *)
440
and check_positive_imbr (env,n,ntypes,ra_env as ienv) nmr (mi, largs) =
441
let (mib,mip) = lookup_mind_specif env mi in
442
let auxnpar = mib.mind_nparams_rec in
443
let (lpar,auxlargs) =
444
try list_chop auxnpar largs
445
with Failure _ -> raise (IllFormedInd (LocalNonPos n)) in
446
(* If the inductive appears in the args (non params) then the
447
definition is not positive. *)
448
if not (List.for_all (noccur_between n ntypes) auxlargs) then
449
raise (IllFormedInd (LocalNonPos n));
450
(* We do not deal with imbricated mutual inductive types *)
451
let auxntyp = mib.mind_ntypes in
452
if auxntyp <> 1 then raise (IllFormedInd (LocalNonPos n));
453
(* The nested inductive type with parameters removed *)
454
let auxlcvect = abstract_mind_lc env auxntyp auxnpar mip.mind_nf_lc in
455
(* Extends the environment with a variable corresponding to
457
let (env',_,_,_ as ienv') = ienv_push_inductive ienv (mi,lpar) in
458
(* Parameters expressed in env' *)
459
let lpar' = List.map (lift auxntyp) lpar in
461
(* fails if the inductive type occurs non positively *)
462
(* when substituted *)
465
let c' = hnf_prod_applist env' c lpar' in
466
check_constructors ienv' false nmr c')
469
let irecargs = Array.map snd irecargs_nmr
470
and nmr' = array_min nmr irecargs_nmr
472
(nmr',(Rtree.mk_rec [|mk_paths (Imbr mi) irecargs|]).(0))
474
(* check the inductive types occur positively in the products of C, if
475
check_head=true, also check the head corresponds to a constructor of
478
and check_constructors ienv check_head nmr c =
479
let rec check_constr_rec (env,n,ntypes,ra_env as ienv) nmr lrec c =
480
let x,largs = decompose_app (whd_betadeltaiota env c) in
481
match kind_of_term x with
485
let nmr',recarg = check_pos ienv nmr b in
486
let ienv' = ienv_push_var ienv (na,b,mk_norec) in
487
check_constr_rec ienv' nmr' (recarg::lrec) d
491
if hd = Rel (n+ntypes-i-1) then
492
check_correct_par ienv hyps (ntypes-i) largs
494
raise (IllFormedInd LocalNotConstructor)
496
if not (List.for_all (noccur_between n ntypes) largs)
497
then raise (IllFormedInd (LocalNonPos n));
499
in check_constr_rec ienv nmr [] c
504
let _,rawc = mind_extract_params lparams c in
506
check_constructors ienv true nmr rawc
507
with IllFormedInd err ->
508
explain_ind_err id (ntypes-i) env lparams c nargs err)
509
(Array.of_list lcnames) indlc
511
let irecargs = Array.map snd irecargs_nmr
512
and nmr' = array_min nmr irecargs_nmr
513
in (nmr', mk_paths (Mrec i) irecargs)
515
let check_positivity env_ar params inds =
516
let ntypes = Array.length inds in
517
let rc = Array.mapi (fun j t -> (Mrec j,t)) (Rtree.mk_rec_calls ntypes) in
518
let lra_ind = List.rev (Array.to_list rc) in
519
let lparams = rel_context_length params in
520
let nmr = rel_context_nhyps params in
521
let check_one i (_,lcnames,lc,(sign,_)) =
523
list_tabulate (fun _ -> (Norec,mk_norec)) lparams @ lra_ind in
524
let ienv = (env_ar, 1+lparams, ntypes, ra_env) in
525
let nargs = rel_context_nhyps sign - nmr in
526
check_positivity_one ienv params i nargs lcnames lc
528
let irecargs_nmr = Array.mapi check_one inds in
529
let irecargs = Array.map snd irecargs_nmr
530
and nmr' = array_min nmr irecargs_nmr
531
in (nmr',Rtree.mk_rec irecargs)
534
(************************************************************************)
535
(************************************************************************)
536
(* Build the inductive packet *)
538
(* Elimination sorts *)
539
let is_recursive = Rtree.is_infinite
540
(* let rec one_is_rec rvec =
541
List.exists (function Mrec(i) -> List.mem i listind
542
| Imbr(_,lvec) -> array_exists one_is_rec lvec
543
| Norec -> false) rvec
545
array_exists one_is_rec
548
(* Allowed eliminations *)
550
let all_sorts = [InProp;InSet;InType]
551
let small_sorts = [InProp;InSet]
552
let logical_sorts = [InProp]
554
let allowed_sorts issmall isunit s =
555
match family_of_sort s with
556
(* Type: all elimination allowed *)
557
| InType -> all_sorts
559
(* Small Set is predicative: all elimination allowed *)
560
| InSet when issmall -> all_sorts
562
(* Large Set is necessarily impredicative: forbids large elimination *)
563
| InSet -> small_sorts
565
(* Unitary/empty Prop: elimination to all sorts are realizable *)
566
(* unless the type is large. If it is large, forbids large elimination *)
567
(* which otherwise allows to simulate the inconsistent system Type:Type *)
568
| InProp when isunit -> if issmall then all_sorts else small_sorts
570
(* Other propositions: elimination only to Prop *)
571
| InProp -> logical_sorts
573
let fold_inductive_blocks f =
574
Array.fold_left (fun acc (_,_,lc,(arsign,_)) ->
575
f (Array.fold_left f acc lc) (it_mkProd_or_LetIn (* dummy *) mkSet arsign))
577
let used_section_variables env inds =
578
let ids = fold_inductive_blocks
579
(fun l c -> Idset.union (Environ.global_vars_set env c) l)
583
let build_inductive env env_ar params isrecord isfinite inds nmr recargs cst =
584
let ntypes = Array.length inds in
585
(* Compute the set of used section variables *)
586
let hyps = used_section_variables env inds in
587
let nparamargs = rel_context_nhyps params in
588
(* Check one inductive *)
589
let build_one_packet (id,cnames,lc,(ar_sign,ar_kind)) recarg =
590
(* Type of constructors in normal form *)
591
let splayed_lc = Array.map (dest_prod_assum env_ar) lc in
592
let nf_lc = Array.map (fun (d,b) -> it_mkProd_or_LetIn b d) splayed_lc in
593
let nf_lc = if nf_lc = lc then lc else nf_lc in
595
Array.map (fun (d,_) -> rel_context_length d - rel_context_length params)
597
(* Elimination sorts *)
598
let arkind,kelim = match ar_kind with
599
| Inr (param_levels,lev) ->
601
poly_param_levels = param_levels;
604
| Inl ((issmall,isunit),ar,s) ->
605
let kelim = allowed_sorts issmall isunit s in
607
mind_user_arity = ar;
610
let nconst, nblock = ref 0, ref 0 in
612
let arity = List.length (dest_subterms recarg).(num) in
614
let p = (!nconst, 0) in
617
let p = (!nblock + 1, arity) in
619
(* les tag des constructeur constant commence a 0,
620
les tag des constructeur non constant a 1 (0 => accumulator) *)
622
let rtbl = Array.init (List.length cnames) transf in
623
(* Build the inductive packet *)
624
{ mind_typename = id;
626
mind_arity_ctxt = ar_sign;
627
mind_nrealargs = rel_context_nhyps ar_sign - nparamargs;
629
mind_consnames = Array.of_list cnames;
630
mind_consnrealdecls = consnrealargs;
633
mind_recargs = recarg;
634
mind_nb_constant = !nconst;
635
mind_nb_args = !nblock;
636
mind_reloc_tbl = rtbl;
638
let packets = array_map2 build_one_packet inds recargs in
639
(* Build the mutual inductive *)
640
{ mind_record = isrecord;
641
mind_ntypes = ntypes;
642
mind_finite = isfinite;
644
mind_nparams = nparamargs;
645
mind_nparams_rec = nmr;
646
mind_params_ctxt = params;
647
mind_packets = packets;
648
mind_constraints = cst;
652
(************************************************************************)
653
(************************************************************************)
655
let check_inductive env mie =
656
(* First type-check the inductive definition *)
657
let (env_ar, params, inds, cst) = typecheck_inductive env mie in
658
(* Then check positivity conditions *)
659
let (nmr,recargs) = check_positivity env_ar params inds in
660
(* Build the inductive packets *)
661
build_inductive env env_ar params mie.mind_entry_record mie.mind_entry_finite
added
removed
kernel/indtypes.ml
