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 10296 2007-11-07 11:02:42Z barras $ *)
22
let rec debug_string_of_mp = function
23
| MPfile sl -> string_of_dirpath sl
24
| MPbound uid -> "bound("^string_of_mbid uid^")"
25
| MPself uid -> "self("^string_of_msid uid^")"
26
| MPdot (mp,l) -> string_of_mp mp ^ "." ^ string_of_label l
28
let rec string_of_mp = function
29
| MPfile sl -> string_of_dirpath sl
30
| MPbound uid -> string_of_mbid uid
31
| MPself uid -> string_of_msid uid
32
| MPdot (mp,l) -> string_of_mp mp ^ "." ^ string_of_label l
35
if !Flags.debug then debug_string_of_mp mp else string_of_mp mp
38
let (mp,_,l) = repr_kn kn in
39
str(string_of_mp mp ^ "." ^ string_of_label l)
41
let (mp,_,l) = repr_con c in
42
str(string_of_mp mp ^ "." ^ string_of_label l)
44
(* Same as noccur_between but may perform reductions.
45
Could be refined more... *)
46
let weaker_noccur_between env x nvars t =
47
if noccur_between x nvars t then Some t
49
let t' = whd_betadeltaiota env t in
50
if noccur_between x nvars t' then Some t'
53
let is_constructor_head t =
54
match fst(decompose_app t) with
58
let conv_ctxt_prefix env (ctx1:rel_context) ctx2 =
59
let rec chk env rctx1 rctx2 =
60
match rctx1, rctx2 with
61
(_,None,ty1 as d1)::rctx1', (_,None,ty2)::rctx2' ->
63
chk (push_rel d1 env) rctx1' rctx2'
64
| (_,Some bd1,ty1 as d1)::rctx1', (_,Some bd2,ty2)::rctx2' ->
67
chk (push_rel d1 env) rctx1' rctx2'
69
| _ -> failwith "non convertible contexts" in
70
chk env (List.rev ctx1) (List.rev ctx2)
72
(************************************************************************)
73
(* Various well-formedness check for inductive declarations *)
75
(* Errors related to inductive constructions *)
76
type inductive_error =
77
| NonPos of env * constr * constr
78
| NotEnoughArgs of env * constr * constr
79
| NotConstructor of env * constr * constr
80
| NonPar of env * constr * int * constr * constr
81
| SameNamesTypes of identifier
82
| SameNamesConstructors of identifier
83
| SameNamesOverlap of identifier list
84
| NotAnArity of identifier
87
exception InductiveError of inductive_error
89
(************************************************************************)
90
(************************************************************************)
92
(* Typing the arities and constructor types *)
94
let rec sorts_of_constr_args env t =
95
let t = whd_betadeltaiota_nolet env t in
97
| Prod (name,c1,c2) ->
98
let varj = infer_type env c1 in
99
let env1 = push_rel (name,None,c1) env in
100
varj :: sorts_of_constr_args env1 c2
101
| LetIn (name,def,ty,c) ->
102
let env1 = push_rel (name,Some def,ty) env in
103
sorts_of_constr_args env1 c
104
| _ when is_constructor_head t -> []
105
| _ -> anomaly "infos_and_sort: not a positive constructor"
108
(* Prop and Set are small *)
109
let is_small_sort = function
113
let is_logic_sort s = (s = Prop Null)
115
(* [infos] is a sequence of pair [islogic,issmall] for each type in
116
the product of a constructor or arity *)
118
let is_small_constr infos = List.for_all (fun s -> is_small_sort s) infos
119
let is_logic_constr infos = List.for_all (fun s -> is_logic_sort s) infos
121
(* An inductive definition is a "unit" if it has only one constructor
122
and that all arguments expected by this constructor are
123
logical, this is the case for equality, conjunction of logical properties
125
let is_unit constrsinfos =
126
match constrsinfos with (* One info = One constructor *)
127
| [|constrinfos|] -> is_logic_constr constrinfos
128
| [||] -> (* type without constructors *) true
131
let small_unit constrsinfos =
132
let issmall = array_for_all is_small_constr constrsinfos
133
and isunit = is_unit constrsinfos in
136
(* check information related to inductive arity *)
137
let typecheck_arity env params inds =
138
let nparamargs = rel_context_nhyps params in
139
let check_arity arctxt = function
141
let ar = mar.mind_user_arity in
142
let _ = infer_type env ar in
143
conv env (it_mkProd_or_LetIn (Sort mar.mind_sort) arctxt) ar;
146
check_polymorphic_arity env params par;
147
it_mkProd_or_LetIn (Sort(Type par.poly_level)) arctxt in
151
let ar_ctxt = ind.mind_arity_ctxt in
152
let _ = check_ctxt env ar_ctxt in
153
conv_ctxt_prefix env params ar_ctxt;
154
(* Arities (with params) are typed-checked here *)
155
let arity = check_arity ar_ctxt ind.mind_arity in
157
if ind.mind_nrealargs <> rel_context_nhyps ar_ctxt - nparamargs then
158
failwith "bad number of real inductive arguments";
159
(* We do not need to generate the universe of full_arity; if
160
later, after the validation of the inductive definition,
161
full_arity is used as argument or subject to cast, an
162
upper universe will be generated *)
163
let id = ind.mind_typename in
164
let env_ar' = push_rel (Name id, None, arity) env_ar in
170
(* Allowed eliminations *)
172
let check_predicativity env s small level =
173
match s, engagement env with
175
let u' = fresh_local_univ () in
177
merge_constraints (enforce_geq u' u Constraint.empty)
179
if not (check_geq cst u' level) then
180
failwith "impredicative Type inductive type"
181
| Prop Pos, Some ImpredicativeSet -> ()
183
if not small then failwith "impredicative Set inductive type"
187
let sort_of_ind = function
188
Monomorphic mar -> mar.mind_sort
189
| Polymorphic par -> Type par.poly_level
191
let all_sorts = [InProp;InSet;InType]
192
let small_sorts = [InProp;InSet]
193
let logical_sorts = [InProp]
195
let allowed_sorts issmall isunit s =
196
match family_of_sort s with
197
(* Type: all elimination allowed *)
198
| InType -> all_sorts
200
(* Small Set is predicative: all elimination allowed *)
201
| InSet when issmall -> all_sorts
203
(* Large Set is necessarily impredicative: forbids large elimination *)
204
| InSet -> small_sorts
206
(* Unitary/empty Prop: elimination to all sorts are realizable *)
207
(* unless the type is large. If it is large, forbids large elimination *)
208
(* which otherwise allows to simulate the inconsistent system Type:Type *)
209
| InProp when isunit -> if issmall then all_sorts else small_sorts
211
(* Other propositions: elimination only to Prop *)
212
| InProp -> logical_sorts
216
let compute_elim_sorts env_ar params mib arity lc =
217
let inst = extended_rel_list 0 params in
218
let env_params = push_rel_context params env_ar in
221
hnf_prod_applist env_params (lift (rel_context_length params) c) inst)
223
let s = sort_of_ind arity in
224
let infos = Array.map (sorts_of_constr_args env_params) lc in
225
let (small,unit) = small_unit infos in
226
(* We accept recursive unit types... *)
227
let unit = unit && mib.mind_ntypes = 1 in
228
(* compute the max of the sorts of the products of the constructor type *)
229
let level = max_inductive_sort
230
(Array.concat (Array.to_list (Array.map Array.of_list infos))) in
231
check_predicativity env_ar s small level;
232
allowed_sorts small unit s
235
let typecheck_one_inductive env params mib mip =
236
(* mind_typename and mind_consnames not checked *)
237
(* mind_reloc_tbl, mind_nb_constant, mind_nb_args not checked (VM) *)
238
(* mind_arity_ctxt, mind_arity, mind_nrealargs DONE (typecheck_arity) *)
240
let _ = Array.map (infer_type env) mip.mind_user_lc in
242
let _ = Array.map (infer_type env) mip.mind_nf_lc in
243
array_iter2 (conv env) mip.mind_nf_lc mip.mind_user_lc;
244
(* mind_consnrealdecls *)
245
let check_cons_args c n =
246
let ctx,_ = decompose_prod_assum c in
247
if n <> rel_context_length ctx - rel_context_length params then
248
failwith "bad number of real constructor arguments" in
249
array_iter2 check_cons_args mip.mind_nf_lc mip.mind_consnrealdecls;
250
(* mind_kelim: checked by positivity criterion ? *)
252
compute_elim_sorts env params mib mip.mind_arity mip.mind_nf_lc in
253
if List.exists (fun s -> not (List.mem s sorts)) mip.mind_kelim then
254
failwith "elimination not allowed";
255
(* mind_recargs: checked by positivity criterion *)
258
(************************************************************************)
259
(************************************************************************)
262
type ill_formed_ind =
264
| LocalNotEnoughArgs of int
265
| LocalNotConstructor
266
| LocalNonPar of int * int
268
exception IllFormedInd of ill_formed_ind
270
(* [mind_extract_params mie] extracts the params from an inductive types
271
declaration, and checks that they are all present (and all the same)
272
for all the given types. *)
274
let mind_extract_params = decompose_prod_n_assum
276
let explain_ind_err ntyp env0 nbpar c err =
277
let (lpar,c') = mind_extract_params nbpar c in
278
let env = push_rel_context lpar env0 in
281
raise (InductiveError (NonPos (env,c',Rel (kt+nbpar))))
282
| LocalNotEnoughArgs kt ->
283
raise (InductiveError
284
(NotEnoughArgs (env,c',Rel (kt+nbpar))))
285
| LocalNotConstructor ->
286
raise (InductiveError
287
(NotConstructor (env,c',Rel (ntyp+nbpar))))
288
| LocalNonPar (n,l) ->
289
raise (InductiveError
290
(NonPar (env,c',n,Rel (nbpar-n+1), Rel (l+nbpar))))
292
let failwith_non_pos n ntypes c =
293
for k = n to n + ntypes - 1 do
294
if not (noccurn k c) then raise (IllFormedInd (LocalNonPos (k-n+1)))
297
let failwith_non_pos_vect n ntypes v =
298
Array.iter (failwith_non_pos n ntypes) v;
299
anomaly "failwith_non_pos_vect: some k in [n;n+ntypes-1] should occur"
301
let failwith_non_pos_list n ntypes l =
302
List.iter (failwith_non_pos n ntypes) l;
303
anomaly "failwith_non_pos_list: some k in [n;n+ntypes-1] should occur"
305
(* Conclusion of constructors: check the inductive type is called with
306
the expected parameters *)
307
let check_correct_par (env,n,ntypes,_) hyps l largs =
308
let nparams = rel_context_nhyps hyps in
309
let largs = Array.of_list largs in
310
if Array.length largs < nparams then
311
raise (IllFormedInd (LocalNotEnoughArgs l));
312
let (lpar,largs') = array_chop nparams largs in
313
let nhyps = List.length hyps in
314
let rec check k index = function
316
| (_,Some _,_)::hyps -> check k (index+1) hyps
318
match whd_betadeltaiota env lpar.(k) with
319
| Rel w when w = index -> check (k-1) (index+1) hyps
320
| _ -> raise (IllFormedInd (LocalNonPar (k+1,l)))
321
in check (nparams-1) (n-nhyps) hyps;
322
if not (array_for_all (noccur_between n ntypes) largs') then
323
failwith_non_pos_vect n ntypes largs'
325
(* Arguments of constructor: check the number of recursive parameters nrecp.
326
the first parameters which are constant in recursive arguments
327
n is the current depth, nmr is the maximum number of possible
328
recursive parameters *)
330
let check_rec_par (env,n,_,_) hyps nrecp largs =
331
let (lpar,_) = list_chop nrecp largs in
336
failwith "number of recursive parameters cannot be greater than the number of parameters."
337
| (lp,(_,Some _,_)::hyps) -> find (index-1) (lp,hyps)
339
(match whd_betadeltaiota env p with
340
| Rel w when w = index -> find (index-1) (lp,hyps)
341
| _ -> failwith "bad number of recursive parameters")
342
in find (n-1) (lpar,List.rev hyps)
344
let lambda_implicit_lift n a =
345
let lambda_implicit a = Lambda(Anonymous,Evar(0,[||]),a) in
346
iterate lambda_implicit n (lift n a)
348
(* This removes global parameters of the inductive types in lc (for
349
nested inductive types only ) *)
350
let abstract_mind_lc env ntyps npars lc =
356
(function i -> lambda_implicit_lift npars (Rel (i+1))) ntyps
358
Array.map (substl make_abs) lc
360
(* [env] is the typing environment
361
[n] is the dB of the last inductive type
362
[ntypes] is the number of inductive types in the definition
363
(i.e. range of inductives is [n; n+ntypes-1])
364
[lra] is the list of recursive tree of each variable
366
let ienv_push_var (env, n, ntypes, lra) (x,a,ra) =
367
(push_rel (x,None,a) env, n+1, ntypes, (Norec,ra)::lra)
369
let ienv_push_inductive (env, n, ntypes, ra_env) (mi,lpar) =
371
let specif = lookup_mind_specif env mi in
373
push_rel (Anonymous,None,
374
hnf_prod_applist env (type_of_inductive env specif) lpar) env in
376
(Imbr mi,(Rtree.mk_rec_calls 1).(0)) ::
377
List.map (fun (r,t) -> (r,Rtree.lift 1 t)) ra_env in
378
(* New index of the inductive types *)
379
let newidx = n + auxntyp in
380
(env', newidx, ntypes, ra_env')
382
(* The recursive function that checks positivity and builds the list
383
of recursive arguments *)
384
let check_positivity_one (env, _,ntypes,_ as ienv) hyps nrecp i indlc =
385
let lparams = rel_context_length hyps in
386
(* check the inductive types occur positively in [c] *)
387
let rec check_pos (env, n, ntypes, ra_env as ienv) c =
388
let x,largs = decompose_app (whd_betadeltaiota env c) in
392
(match weaker_noccur_between env n ntypes b with
393
None -> failwith_non_pos_list n ntypes [b]
395
check_pos (ienv_push_var ienv (na, b, mk_norec)) d)
398
let (ra,rarg) = List.nth ra_env (k-1) in
400
Mrec _ -> check_rec_par ienv hyps nrecp largs
402
if not (List.for_all (noccur_between n ntypes) largs)
403
then failwith_non_pos_list n ntypes largs
405
with Failure _ | Invalid_argument _ -> mk_norec)
407
(* If the inductive type being defined appears in a
408
parameter, then we have an imbricated type *)
409
if List.for_all (noccur_between n ntypes) largs then mk_norec
410
else check_positive_imbr ienv (ind_kn, largs)
412
if noccur_between n ntypes x &&
413
List.for_all (noccur_between n ntypes) largs
415
else failwith_non_pos_list n ntypes (x::largs)
417
(* accesses to the environment are not factorised, but is it worth it? *)
418
and check_positive_imbr (env,n,ntypes,ra_env as ienv) (mi, largs) =
419
let (mib,mip) = lookup_mind_specif env mi in
420
let auxnpar = mib.mind_nparams_rec in
421
let (lpar,auxlargs) =
422
try list_chop auxnpar largs
423
with Failure _ -> raise (IllFormedInd (LocalNonPos n)) in
424
(* If the inductive appears in the args (non params) then the
425
definition is not positive. *)
426
if not (List.for_all (noccur_between n ntypes) auxlargs) then
427
raise (IllFormedInd (LocalNonPos n));
428
(* We do not deal with imbricated mutual inductive types *)
429
let auxntyp = mib.mind_ntypes in
430
if auxntyp <> 1 then raise (IllFormedInd (LocalNonPos n));
431
(* The nested inductive type with parameters removed *)
432
let auxlcvect = abstract_mind_lc env auxntyp auxnpar mip.mind_nf_lc in
433
(* Extends the environment with a variable corresponding to
435
let (env',_,_,_ as ienv') = ienv_push_inductive ienv (mi,lpar) in
436
(* Parameters expressed in env' *)
437
let lpar' = List.map (lift auxntyp) lpar in
439
(* fails if the inductive type occurs non positively *)
440
(* when substituted *)
443
let c' = hnf_prod_applist env' c lpar' in
444
check_constructors ienv' false c')
446
(Rtree.mk_rec [|mk_paths (Imbr mi) irecargs|]).(0)
448
(* check the inductive types occur positively in the products of C, if
449
check_head=true, also check the head corresponds to a constructor of
452
and check_constructors ienv check_head c =
453
let rec check_constr_rec (env,n,ntypes,ra_env as ienv) lrec c =
454
let x,largs = decompose_app (whd_betadeltaiota env c) in
458
let recarg = check_pos ienv b in
459
let ienv' = ienv_push_var ienv (na,b,mk_norec) in
460
check_constr_rec ienv' (recarg::lrec) d
464
if hd = Rel (n+ntypes-i-1) then
465
check_correct_par ienv hyps (ntypes-i) largs
467
raise (IllFormedInd LocalNotConstructor)
469
if not (List.for_all (noccur_between n ntypes) largs)
470
then raise (IllFormedInd (LocalNonPos n));
472
in check_constr_rec ienv [] c
477
let _,rawc = mind_extract_params lparams c in
479
check_constructors ienv true rawc
480
with IllFormedInd err ->
481
explain_ind_err (ntypes-i) env lparams c err)
483
in mk_paths (Mrec i) irecargs
485
let check_subtree (t1:'a) (t2:'a) =
486
if not (Rtree.compare_rtree (fun t1 t2 ->
487
let l1 = fst(Rtree.dest_node t1) in
488
let l2 = fst(Rtree.dest_node t2) in
489
if l1 = Norec || l1 = l2 then 0 else -1)
491
failwith "bad recursive trees"
492
(* if t1=t2 then () else msg_warning (str"TODO: check recursive positions")*)
494
let check_positivity env_ar params nrecp inds =
495
let ntypes = Array.length inds in
496
let rc = Array.mapi (fun j t -> (Mrec j,t)) (Rtree.mk_rec_calls ntypes) in
497
let lra_ind = List.rev (Array.to_list rc) in
498
let lparams = rel_context_length params in
499
let check_one i mip =
501
list_tabulate (fun _ -> (Norec,mk_norec)) lparams @ lra_ind in
502
let ienv = (env_ar, 1+lparams, ntypes, ra_env) in
503
check_positivity_one ienv params nrecp i mip.mind_nf_lc
505
let irecargs = Array.mapi check_one inds in
506
let wfp = Rtree.mk_rec irecargs in
507
array_iter2 (fun ind wfpi -> check_subtree ind.mind_recargs wfpi) inds wfp
509
(************************************************************************)
510
(************************************************************************)
512
let check_inductive env kn mib =
513
Flags.if_verbose msgnl (str " checking ind: " ++ prkn kn);
514
(* check mind_constraints: should be consistent with env *)
515
let env = add_constraints mib.mind_constraints env in
516
(* check mind_record : TODO ? check #constructor = 1 ? *)
517
(* check mind_finite : always OK *)
518
(* check mind_ntypes *)
519
if Array.length mib.mind_packets <> mib.mind_ntypes then
520
error "not the right number of packets";
521
(* check mind_hyps: should be empty *)
522
if mib.mind_hyps <> empty_named_context then
523
error "section context not empty";
524
(* check mind_params_ctxt *)
525
let params = mib.mind_params_ctxt in
526
let _ = check_ctxt env params in
527
(* check mind_nparams *)
528
if rel_context_nhyps params <> mib.mind_nparams then
529
error "number the right number of parameters";
531
(* - check arities *)
532
let env_ar = typecheck_arity env params mib.mind_packets in
533
(* - check constructor types *)
534
Array.iter (typecheck_one_inductive env_ar params mib) mib.mind_packets;
535
(* check mind_nparams_rec: positivity condition *)
536
check_positivity env_ar params mib.mind_nparams_rec mib.mind_packets;
537
(* check mind_equiv... *)
538
if mib.mind_equiv <> None then
539
msg_warning (str"TODO: mind_equiv not checked");
540
(* Now we can add the inductive *)
added
removed
checker/indtypes.ml
