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: inductive.ml 11647 2008-12-02 10:40:11Z barras $ *)
21
type mind_specif = mutual_inductive_body * one_inductive_body
23
(* raise Not_found if not an inductive type *)
24
let lookup_mind_specif env (kn,tyi) =
25
let mib = Environ.lookup_mind kn env in
26
if tyi >= Array.length mib.mind_packets then
27
error "Inductive.lookup_mind_specif: invalid inductive index";
28
(mib, mib.mind_packets.(tyi))
30
let find_rectype env c =
31
let (t, l) = decompose_app (whd_betadeltaiota env c) in
32
match kind_of_term t with
34
| _ -> raise Not_found
36
let find_inductive env c =
37
let (t, l) = decompose_app (whd_betadeltaiota env c) in
38
match kind_of_term t with
40
when (fst (lookup_mind_specif env ind)).mind_finite -> (ind, l)
41
| _ -> raise Not_found
43
let find_coinductive env c =
44
let (t, l) = decompose_app (whd_betadeltaiota env c) in
45
match kind_of_term t with
47
when not (fst (lookup_mind_specif env ind)).mind_finite -> (ind, l)
48
| _ -> raise Not_found
50
let inductive_params (mib,_) = mib.mind_nparams
52
(************************************************************************)
54
(* Build the substitution that replaces Rels by the appropriate *)
56
let ind_subst mind mib =
57
let ntypes = mib.mind_ntypes in
58
let make_Ik k = mkInd (mind,ntypes-k-1) in
59
list_tabulate make_Ik ntypes
61
(* Instantiate inductives in constructor type *)
62
let constructor_instantiate mind mib c =
63
let s = ind_subst mind mib in
66
let instantiate_params full t args sign =
68
anomaly "instantiate_params: type, ctxt and args mismatch" in
69
let (rem_args, subs, ty) =
71
(fun (_,copt,_) (largs,subs,ty) ->
72
match (copt, largs, kind_of_term ty) with
73
| (None, a::args, Prod(_,_,t)) -> (args, a::subs, t)
74
| (Some b,_,LetIn(_,_,_,t)) -> (largs, (substl subs b)::subs, t)
75
| (_,[],_) -> if full then fail() else ([], subs, ty)
80
if rem_args <> [] then fail();
83
let instantiate_partial_params = instantiate_params false
85
let full_inductive_instantiate mib params sign =
86
let dummy = prop_sort in
87
let t = mkArity (sign,dummy) in
88
fst (destArity (instantiate_params true t params mib.mind_params_ctxt))
90
let full_constructor_instantiate ((mind,_),(mib,_),params) =
91
let inst_ind = constructor_instantiate mind mib in
93
instantiate_params true (inst_ind t) params mib.mind_params_ctxt)
95
(************************************************************************)
96
(************************************************************************)
98
(* Functions to build standard types related to inductive *)
101
let number_of_inductives mib = Array.length mib.mind_packets
102
let number_of_constructors mip = Array.length mip.mind_consnames
105
Computing the actual sort of an applied or partially applied inductive type:
107
I_i: forall uniformparams:utyps, forall otherparams:otyps, Type(a)
110
I_1:forall ...,s_1;...I_n:forall ...,s_n |- sort(C_kj(uniformargs)) = s_kj
112
merge(..s'_k..) = ..s''_k..
113
--------------------------------------------------------------------
114
Gamma |- I_i uniformargs otherargs : phi(s''_i)
118
- if p=0, phi() = Prop
120
- if p<>1, phi(s) = sup(Set,s)
122
Remark: Set (predicative) is encoded as Type(0)
125
let sort_as_univ = function
127
| Prop Null -> type0m_univ
128
| Prop Pos -> type0_univ
130
let cons_subst u su subst =
131
try (u, sup su (List.assoc u subst)) :: List.remove_assoc u subst
132
with Not_found -> (u, su) :: subst
134
let actualize_decl_level env lev t =
135
let sign,s = dest_arity env t in
138
let polymorphism_on_non_applied_parameters = false
140
(* Bind expected levels of parameters to actual levels *)
141
(* Propagate the new levels in the signature *)
142
let rec make_subst env = function
143
| (_,Some _,_ as t)::sign, exp, args ->
144
let ctx,subst = make_subst env (sign, exp, args) in
146
| d::sign, None::exp, args ->
147
let args = match args with _::args -> args | [] -> [] in
148
let ctx,subst = make_subst env (sign, exp, args) in
150
| d::sign, Some u::exp, a::args ->
151
(* We recover the level of the argument, but we don't change the *)
152
(* level in the corresponding type in the arity; this level in the *)
153
(* arity is a global level which, at typing time, will be enforce *)
154
(* to be greater than the level of the argument; this is probably *)
155
(* a useless extra constraint *)
156
let s = sort_as_univ (snd (dest_arity env a)) in
157
let ctx,subst = make_subst env (sign, exp, args) in
158
d::ctx, cons_subst u s subst
159
| (na,None,t as d)::sign, Some u::exp, [] ->
160
(* No more argument here: we instantiate the type with a fresh level *)
161
(* which is first propagated to the corresponding premise in the arity *)
162
(* (actualize_decl_level), then to the conclusion of the arity (via *)
163
(* the substitution) *)
164
let ctx,subst = make_subst env (sign, exp, []) in
165
if polymorphism_on_non_applied_parameters then
166
let s = fresh_local_univ () in
167
let t = actualize_decl_level env (Type s) t in
168
(na,None,t)::ctx, cons_subst u s subst
172
(* Uniform parameters are exhausted *)
177
let instantiate_universes env ctx ar argsorts =
178
let args = Array.to_list argsorts in
179
let ctx,subst = make_subst env (ctx,ar.poly_param_levels,args) in
180
let level = subst_large_constraints subst ar.poly_level in
182
(* Singleton type not containing types are interpretable in Prop *)
183
if is_type0m_univ level then prop_sort
184
(* Non singleton type not containing types are interpretable in Set *)
185
else if is_type0_univ level then set_sort
186
(* This is a Type with constraints *)
189
let type_of_inductive_knowing_parameters env mip paramtyps =
190
match mip.mind_arity with
194
let ctx = List.rev mip.mind_arity_ctxt in
195
let ctx,s = instantiate_universes env ctx ar paramtyps in
196
mkArity (List.rev ctx,s)
198
(* Type of a (non applied) inductive type *)
200
let type_of_inductive env (_,mip) =
201
type_of_inductive_knowing_parameters env mip [||]
203
(* The max of an array of universes *)
205
let cumulate_constructor_univ u = function
207
| Prop Pos -> sup type0_univ u
208
| Type u' -> sup u u'
210
let max_inductive_sort =
211
Array.fold_left cumulate_constructor_univ type0m_univ
213
(************************************************************************)
214
(* Type of a constructor *)
216
let type_of_constructor cstr (mib,mip) =
217
let ind = inductive_of_constructor cstr in
218
let specif = mip.mind_user_lc in
219
let i = index_of_constructor cstr in
220
let nconstr = Array.length mip.mind_consnames in
221
if i > nconstr then error "Not enough constructors in the type.";
222
constructor_instantiate (fst ind) mib specif.(i-1)
224
let arities_of_specif kn (mib,mip) =
225
let specif = mip.mind_nf_lc in
226
Array.map (constructor_instantiate kn mib) specif
228
let arities_of_constructors ind specif =
229
arities_of_specif (fst ind) specif
231
let type_of_constructors ind (mib,mip) =
232
let specif = mip.mind_user_lc in
233
Array.map (constructor_instantiate (fst ind) mib) specif
235
(************************************************************************)
237
let error_elim_expln kp ki =
239
| (InType | InSet), InProp -> NonInformativeToInformative
240
| InType, InSet -> StrongEliminationOnNonSmallType (* if Set impredicative *)
243
(* Type of case predicates *)
245
let local_rels ctxt =
247
Sign.fold_rel_context_reverse
248
(fun (rels,n) (_,copt,_) ->
250
None -> (mkRel n :: rels, n+1)
251
| Some _ -> (rels, n+1))
257
(* Get type of inductive, with parameters instantiated *)
259
let inductive_sort_family mip =
260
match mip.mind_arity with
261
| Monomorphic s -> family_of_sort s.mind_sort
262
| Polymorphic _ -> InType
265
mip.mind_arity_ctxt, inductive_sort_family mip
267
let get_instantiated_arity (mib,mip) params =
268
let sign, s = mind_arity mip in
269
full_inductive_instantiate mib params sign, s
271
let elim_sorts (_,mip) = mip.mind_kelim
275
if p>m then l else reln (mkRel(n+p)::l) (p+1)
279
let build_dependent_inductive ind (_,mip) params =
280
let nrealargs = mip.mind_nrealargs in
282
(mkInd ind, (List.map (lift nrealargs) params)@(rel_list 0 nrealargs))
284
(* This exception is local *)
285
exception LocalArity of (sorts_family * sorts_family * arity_error) option
287
let check_allowed_sort ksort specif =
288
if not (List.exists ((=) ksort) (elim_sorts specif)) then
289
let s = inductive_sort_family (snd specif) in
290
raise (LocalArity (Some(ksort,s,error_elim_expln ksort s)))
292
let is_correct_arity env c pj ind specif params =
293
let arsign,_ = get_instantiated_arity specif params in
294
let rec srec env pt ar u =
295
let pt' = whd_betadeltaiota env pt in
296
match kind_of_term pt', ar with
297
| Prod (na1,a1,t), (_,None,a1')::ar' ->
300
with NotConvertible -> raise (LocalArity None) in
301
srec (push_rel (na1,None,a1) env) t ar' (Constraint.union u univ)
302
| Prod (_,a1,a2), [] -> (* whnf of t was not needed here! *)
303
let ksort = match kind_of_term (whd_betadeltaiota env a2) with
304
| Sort s -> family_of_sort s
305
| _ -> raise (LocalArity None) in
306
let dep_ind = build_dependent_inductive ind specif params in
308
try conv env a1 dep_ind
309
with NotConvertible -> raise (LocalArity None) in
310
check_allowed_sort ksort specif;
311
(true, Constraint.union u univ)
313
check_allowed_sort (family_of_sort s') specif;
316
raise (LocalArity None)
318
try srec env pj.uj_type (List.rev arsign) Constraint.empty
319
with LocalArity kinds ->
320
error_elim_arity env ind (elim_sorts specif) c pj kinds
323
(************************************************************************)
324
(* Type of case branches *)
326
(* [p] is the predicate, [i] is the constructor number (starting from 0),
327
and [cty] is the type of the constructor (params not instantiated) *)
328
let build_branches_type ind (_,mip as specif) params dep p =
329
let build_one_branch i cty =
330
let typi = full_constructor_instantiate (ind,specif,params) cty in
331
let (args,ccl) = decompose_prod_assum typi in
332
let nargs = rel_context_length args in
333
let (_,allargs) = decompose_app ccl in
334
let (lparams,vargs) = list_chop (inductive_params specif) allargs in
337
let cstr = ith_constructor_of_inductive ind (i+1) in
338
let dep_cstr = applist (mkConstruct cstr,lparams@(local_rels args)) in
342
let base = beta_appvect (lift nargs p) (Array.of_list cargs) in
343
it_mkProd_or_LetIn base args in
344
Array.mapi build_one_branch mip.mind_nf_lc
346
(* [p] is the predicate, [c] is the match object, [realargs] is the
347
list of real args of the inductive type *)
348
let build_case_type dep p c realargs =
349
let args = if dep then realargs@[c] else realargs in
350
beta_appvect p (Array.of_list args)
352
let type_case_branches env (ind,largs) pj c =
353
let specif = lookup_mind_specif env ind in
354
let nparams = inductive_params specif in
355
let (params,realargs) = list_chop nparams largs in
357
let (dep,univ) = is_correct_arity env c pj ind specif params in
358
let lc = build_branches_type ind specif params dep p in
359
let ty = build_case_type dep p c realargs in
363
(************************************************************************)
364
(* Checking the case annotation is relevent *)
366
let rec inductive_kn_equiv env kn1 kn2 =
367
match (lookup_mind kn1 env).mind_equiv with
368
| Some kn1' -> inductive_kn_equiv env kn2 kn1'
369
| None -> match (lookup_mind kn2 env).mind_equiv with
370
| Some kn2' -> inductive_kn_equiv env kn2' kn1
373
let inductive_equiv env (kn1,i1) (kn2,i2) =
374
i1=i2 & inductive_kn_equiv env kn1 kn2
376
let check_case_info env indsp ci =
377
let (mib,mip) = lookup_mind_specif env indsp in
379
not (Closure.mind_equiv env indsp ci.ci_ind) or
380
(mib.mind_nparams <> ci.ci_npar) or
381
(mip.mind_consnrealdecls <> ci.ci_cstr_nargs)
382
then raise (TypeError(env,WrongCaseInfo(indsp,ci)))
384
(************************************************************************)
385
(************************************************************************)
387
(* Guard conditions for fix and cofix-points *)
389
(* Check if t is a subterm of Rel n, and gives its specification,
390
assuming lst already gives index of
391
subterms with corresponding specifications of recursive arguments *)
393
(* A powerful notion of subterm *)
395
(* To each inductive definition corresponds an array describing the
396
structure of recursive arguments for each constructor, we call it
397
the recursive spec of the type (it has type recargs vect). For
398
checking the guard, we start from the decreasing argument (Rel n)
399
with its recursive spec. During checking the guardness condition,
400
we collect patterns variables corresponding to subterms of n, each
401
of them with its recursive spec. They are organised in a list lst
402
of type (int * recargs) list which is sorted with respect to the
406
(*************************************************************)
407
(* Environment annotated with marks on recursive arguments *)
409
(* tells whether it is a strict or loose subterm *)
410
type size = Large | Strict
412
(* merging information *)
415
Strict, Strict -> Strict
418
(* possible specifications for a term:
419
- Not_subterm: when the size of a term is not related to the
420
recursive argument of the fixpoint
421
- Subterm: when the term is a subterm of the recursive argument
422
the wf_paths argument specifies which subterms are recursive
423
- Dead_code: when the term has been built by elimination over an
428
Subterm of (size * wf_paths)
433
if Rtree.eq_rtree (=) t mk_norec then Not_subterm else Subterm(Strict,t)
435
let subterm_spec_glb =
440
| Not_subterm, _ -> Not_subterm
441
| _, Not_subterm -> Not_subterm
442
| Subterm (a1,t1), Subterm (a2,t2) ->
443
if Rtree.eq_rtree (=) t1 t2 then Subterm (size_glb a1 a2, t1)
444
(* branches do not return objects with same spec *)
446
Array.fold_left glb2 Dead_code
450
(* dB of last fixpoint *)
452
(* inductive of recarg of each fixpoint *)
453
inds : inductive array;
454
(* the recarg information of inductive family *)
455
recvec : wf_paths array;
456
(* dB of variables denoting subterms *)
457
genv : subterm_spec list;
460
let make_renv env minds recarg (kn,tyi) =
461
let mib = Environ.lookup_mind kn env in
463
Array.map (fun mip -> mip.mind_recargs) mib.mind_packets in
467
recvec = mind_recvec;
468
genv = [Subterm(Large,mind_recvec.(tyi))] }
470
let push_var renv (x,ty,spec) =
472
env = push_rel (x,None,ty) renv.env;
473
rel_min = renv.rel_min+1;
474
genv = spec:: renv.genv }
476
let assign_var_spec renv (i,spec) =
477
{ renv with genv = list_assign renv.genv (i-1) spec }
479
let push_var_renv renv (x,ty) =
480
push_var renv (x,ty,Not_subterm)
482
(* Fetch recursive information about a variable p *)
483
let subterm_var p renv =
484
try List.nth renv.genv (p-1)
485
with Failure _ | Invalid_argument _ -> Not_subterm
487
(* Add a variable and mark it as strictly smaller with information [spec]. *)
488
let add_subterm renv (x,a,spec) =
489
push_var renv (x,a,spec_of_tree spec)
491
let push_ctxt_renv renv ctxt =
492
let n = rel_context_length ctxt in
494
env = push_rel_context ctxt renv.env;
495
rel_min = renv.rel_min+n;
496
genv = iterate (fun ge -> Not_subterm::ge) n renv.genv }
498
let push_fix_renv renv (_,v,_ as recdef) =
499
let n = Array.length v in
501
env = push_rec_types recdef renv.env;
502
rel_min = renv.rel_min+n;
503
genv = iterate (fun ge -> Not_subterm::ge) n renv.genv }
506
(******************************)
507
(* Computing the recursive subterms of a term (propagation of size
508
information through Cases). *)
511
c is a branch of an inductive definition corresponding to the spec
512
lrec. mind_recvec is the recursive spec of the inductive
513
definition of the decreasing argument n.
515
case_branches_specif renv lrec lc will pass the lambdas
516
of c corresponding to pattern variables and collect possibly new
517
subterms variables and returns the bodies of the branches with the
518
correct envs and decreasing args.
521
let lookup_subterms env ind =
522
let (_,mip) = lookup_mind_specif env ind in
525
(*********************************)
527
(* Propagation of size information through Cases: if the matched
528
object is a recursive subterm then compute the information
529
associated to its own subterms.
530
Rq: if branch is not eta-long, then the recursive information
531
is not propagated to the missing abstractions *)
532
let case_branches_specif renv c_spec ind lbr =
533
let rec push_branch_args renv lrec c =
536
let c' = whd_betadeltaiota renv.env c in
537
(match kind_of_term c' with
539
let renv' = push_var renv (x,a,ra) in
540
push_branch_args renv' lr b
541
| _ -> (* branch not in eta-long form: cannot perform rec. calls *)
546
let sub_spec = Array.map (List.map spec_of_tree) (dest_subterms t) in
547
assert (Array.length sub_spec = Array.length lbr);
548
array_map2 (push_branch_args renv) sub_spec lbr
550
let t = dest_subterms (lookup_subterms renv.env ind) in
551
let sub_spec = Array.map (List.map (fun _ -> Dead_code)) t in
552
assert (Array.length sub_spec = Array.length lbr);
553
array_map2 (push_branch_args renv) sub_spec lbr
554
| Not_subterm -> Array.map (fun c -> (renv,c)) lbr
556
(* [subterm_specif renv t] computes the recursive structure of [t] and
557
compare its size with the size of the initial recursive argument of
558
the fixpoint we are checking. [renv] collects such information
562
let rec subterm_specif renv t =
563
(* maybe reduction is not always necessary! *)
564
let f,l = decompose_app (whd_betadeltaiota renv.env t) in
565
match kind_of_term f with
566
| Rel k -> subterm_var k renv
568
| Case (ci,_,c,lbr) ->
569
if Array.length lbr = 0 then Dead_code
571
let c_spec = subterm_specif renv c in
572
let lbr_spec = case_branches_specif renv c_spec ci.ci_ind lbr in
574
Array.map (fun (renv',br') -> subterm_specif renv' br')
578
| Fix ((recindxs,i),(_,typarray,bodies as recdef)) ->
579
(* when proving that the fixpoint f(x)=e is less than n, it is enough
580
to prove that e is less than n assuming f is less than n
581
furthermore when f is applied to a term which is strictly less than
582
n, one may assume that x itself is strictly less than n
584
let (ctxt,clfix) = dest_prod renv.env typarray.(i) in
586
let env' = push_rel_context ctxt renv.env in
587
try Some(fst(find_inductive env' clfix))
588
with Not_found -> None in
590
None -> Not_subterm (* happens if fix is polymorphic *)
592
let nbfix = Array.length typarray in
593
let recargs = lookup_subterms renv.env ind in
594
(* pushing the fixpoints *)
595
let renv' = push_fix_renv renv recdef in
597
(* Why Strict here ? To be general, it could also be
599
assign_var_spec renv' (nbfix-i, Subterm(Strict,recargs)) in
600
let decrArg = recindxs.(i) in
601
let theBody = bodies.(i) in
602
let nbOfAbst = decrArg+1 in
603
let sign,strippedBody = decompose_lam_n_assum nbOfAbst theBody in
604
(* pushing the fix parameters *)
605
let renv'' = push_ctxt_renv renv' sign in
607
if List.length l < nbOfAbst then renv''
609
let theDecrArg = List.nth l decrArg in
610
let arg_spec = subterm_specif renv theDecrArg in
611
assign_var_spec renv'' (1, arg_spec) in
612
subterm_specif renv'' strippedBody)
616
subterm_specif (push_var_renv renv (x,a)) b
618
(* Metas and evars are considered OK *)
619
| (Meta _|Evar _) -> Dead_code
621
(* Other terms are not subterms *)
625
(* Check term c can be applied to one of the mutual fixpoints. *)
626
let check_is_subterm renv c =
627
match subterm_specif renv c with
628
Subterm (Strict,_) | Dead_code -> true
631
(************************************************************************)
633
exception FixGuardError of env * guard_error
635
let error_illegal_rec_call renv fx arg =
636
let (_,le_vars,lt_vars) =
638
(fun (i,le,lt) sbt ->
640
(Subterm(Strict,_) | Dead_code) -> (i+1, le, i::lt)
641
| (Subterm(Large,_)) -> (i+1, i::le, lt)
642
| _ -> (i+1, le ,lt))
643
(1,[],[]) renv.genv in
644
raise (FixGuardError (renv.env,
645
RecursionOnIllegalTerm(fx,arg,le_vars,lt_vars)))
647
let error_partial_apply renv fx =
648
raise (FixGuardError (renv.env,NotEnoughArgumentsForFixCall fx))
650
(* Check if [def] is a guarded fixpoint body with decreasing arg.
651
given [recpos], the decreasing arguments of each mutually defined
653
let check_one_fix renv recpos def =
654
let nfi = Array.length recpos in
656
(* Checks if [t] only make valid recursive calls *)
657
let rec check_rec_call renv t =
658
(* if [t] does not make recursive calls, it is guarded: *)
659
if noccur_with_meta renv.rel_min nfi t then ()
661
let (f,l) = decompose_app (whd_betaiotazeta t) in
662
match kind_of_term f with
664
(* Test if [p] is a fixpoint (recursive call) *)
665
if renv.rel_min <= p & p < renv.rel_min+nfi then
667
List.iter (check_rec_call renv) l;
668
(* the position of the invoked fixpoint: *)
669
let glob = renv.rel_min+nfi-1-p in
670
(* the decreasing arg of the rec call: *)
671
let np = recpos.(glob) in
672
if List.length l <= np then error_partial_apply renv glob
674
(* Check the decreasing arg is smaller *)
675
let z = List.nth l np in
676
if not (check_is_subterm renv z) then
677
error_illegal_rec_call renv glob z
681
match pi2 (lookup_rel p renv.env) with
683
List.iter (check_rec_call renv) l
685
try List.iter (check_rec_call renv) l
686
with FixGuardError _ ->
687
check_rec_call renv (applist(lift p c,l))
690
| Case (ci,p,c_0,lrest) ->
691
List.iter (check_rec_call renv) (c_0::p::l);
692
(* compute the recarg information for the arguments of
694
let c_spec = subterm_specif renv c_0 in
695
let lbr = case_branches_specif renv c_spec ci.ci_ind lrest in
696
Array.iter (fun (renv',br') -> check_rec_call renv' br') lbr
698
(* Enables to traverse Fixpoint definitions in a more intelligent
700
if - g = Fix g/p := [y1:T1]...[yp:Tp]e &
701
- f is guarded with respect to the set of pattern variables S
703
- f is guarded with respect to the set of pattern variables S
705
- ap is a sub-term of the formal argument of f &
706
- f is guarded with respect to the set of pattern variables
708
then f is guarded with respect to S in (g a1 ... am).
711
| Fix ((recindxs,i),(_,typarray,bodies as recdef)) ->
712
List.iter (check_rec_call renv) l;
713
Array.iter (check_rec_call renv) typarray;
714
let decrArg = recindxs.(i) in
715
let renv' = push_fix_renv renv recdef in
716
if (List.length l < (decrArg+1)) then
717
Array.iter (check_rec_call renv') bodies
722
let theDecrArg = List.nth l decrArg in
723
let arg_spec = subterm_specif renv theDecrArg in
724
check_nested_fix_body renv' (decrArg+1) arg_spec body
725
else check_rec_call renv' body)
729
if evaluable_constant kn renv.env then
730
try List.iter (check_rec_call renv) l
731
with (FixGuardError _ ) ->
732
check_rec_call renv(applist(constant_value renv.env kn, l))
733
else List.iter (check_rec_call renv) l
735
(* The cases below simply check recursively the condition on the
738
List.iter (check_rec_call renv) (a::b::l)
741
List.iter (check_rec_call renv) (a::l);
742
check_rec_call (push_var_renv renv (x,a)) b
745
List.iter (check_rec_call renv) (a::l);
746
check_rec_call (push_var_renv renv (x,a)) b
748
| CoFix (i,(_,typarray,bodies as recdef)) ->
749
List.iter (check_rec_call renv) l;
750
Array.iter (check_rec_call renv) typarray;
751
let renv' = push_fix_renv renv recdef in
752
Array.iter (check_rec_call renv') bodies
754
| (Ind _ | Construct _ | Sort _) ->
755
List.iter (check_rec_call renv) l
759
match pi2 (lookup_named id renv.env) with
761
List.iter (check_rec_call renv) l
763
try List.iter (check_rec_call renv) l
764
with (FixGuardError _) -> check_rec_call renv (applist(c,l))
767
(* l is not checked because it is considered as the meta's context *)
768
| (Evar _ | Meta _) -> ()
770
| (App _ | LetIn _) -> assert false (* beta zeta reduction *)
772
and check_nested_fix_body renv decr recArgsDecrArg body =
774
check_rec_call (assign_var_spec renv (1,recArgsDecrArg)) body
776
match kind_of_term body with
778
check_rec_call renv a;
779
let renv' = push_var_renv renv (x,a) in
780
check_nested_fix_body renv' (decr-1) recArgsDecrArg b
781
| _ -> anomaly "Not enough abstractions in fix body"
784
check_rec_call renv def
786
let judgment_of_fixpoint (_, types, bodies) =
787
array_map2 (fun typ body -> { uj_val = body ; uj_type = typ }) types bodies
789
let inductive_of_mutfix env ((nvect,bodynum),(names,types,bodies as recdef)) =
790
let nbfix = Array.length bodies in
792
or Array.length nvect <> nbfix
793
or Array.length types <> nbfix
794
or Array.length names <> nbfix
797
then anomaly "Ill-formed fix term";
798
let fixenv = push_rec_types recdef env in
799
let vdefj = judgment_of_fixpoint recdef in
800
let raise_err env i err =
801
error_ill_formed_rec_body env err names i fixenv vdefj in
802
(* Check the i-th definition with recarg k *)
803
let find_ind i k def =
804
(* check fi does not appear in the k+1 first abstractions,
805
gives the type of the k+1-eme abstraction (must be an inductive) *)
806
let rec check_occur env n def =
807
match kind_of_term (whd_betadeltaiota env def) with
809
if noccur_with_meta n nbfix a then
810
let env' = push_rel (x, None, a) env in
812
(* get the inductive type of the fixpoint *)
814
try find_inductive env a
816
raise_err env i (RecursionNotOnInductiveType a) in
818
else check_occur env' (n+1) b
819
else anomaly "check_one_fix: Bad occurrence of recursive call"
820
| _ -> raise_err env i NotEnoughAbstractionInFixBody in
821
check_occur fixenv 1 def in
822
(* Do it on every fixpoint *)
823
let rv = array_map2_i find_ind nvect bodies in
824
(Array.map fst rv, Array.map snd rv)
827
let check_fix env ((nvect,_),(names,_,bodies as recdef) as fix) =
828
let (minds, rdef) = inductive_of_mutfix env fix in
829
for i = 0 to Array.length bodies - 1 do
830
let (fenv,body) = rdef.(i) in
831
let renv = make_renv fenv minds nvect.(i) minds.(i) in
832
try check_one_fix renv nvect body
833
with FixGuardError (fixenv,err) ->
834
error_ill_formed_rec_body fixenv err names i
835
(push_rec_types recdef env) (judgment_of_fixpoint recdef)
839
let cfkey = Profile.declare_profile "check_fix";;
840
let check_fix env fix = Profile.profile3 cfkey check_fix env fix;;
843
(************************************************************************)
846
exception CoFixGuardError of env * guard_error
848
let anomaly_ill_typed () =
849
anomaly "check_one_cofix: too many arguments applied to constructor"
851
let rec codomain_is_coind env c =
852
let b = whd_betadeltaiota env c in
853
match kind_of_term b with
855
codomain_is_coind (push_rel (x, None, a) env) b
857
(try find_coinductive env b
859
raise (CoFixGuardError (env, CodomainNotInductiveType b)))
861
let check_one_cofix env nbfix def deftype =
862
let rec check_rec_call env alreadygrd n vlra t =
863
if not (noccur_with_meta n nbfix t) then
864
let c,args = decompose_app (whd_betadeltaiota env t) in
865
match kind_of_term c with
866
| Rel p when n <= p && p < n+nbfix ->
867
(* recursive call: must be guarded and no nested recursive
869
if not alreadygrd then
870
raise (CoFixGuardError (env,UnguardedRecursiveCall t))
871
else if not(List.for_all (noccur_with_meta n nbfix) args) then
872
raise (CoFixGuardError (env,NestedRecursiveOccurrences))
874
| Construct (_,i as cstr_kn) ->
875
let lra = vlra.(i-1) in
876
let mI = inductive_of_constructor cstr_kn in
877
let (mib,mip) = lookup_mind_specif env mI in
878
let realargs = list_skipn mib.mind_nparams args in
879
let rec process_args_of_constr = function
880
| (t::lr), (rar::lrar) ->
881
if rar = mk_norec then
882
if noccur_with_meta n nbfix t
883
then process_args_of_constr (lr, lrar)
884
else raise (CoFixGuardError
885
(env,RecCallInNonRecArgOfConstructor t))
887
let spec = dest_subterms rar in
888
check_rec_call env true n spec t;
889
process_args_of_constr (lr, lrar)
891
| _ -> anomaly_ill_typed ()
892
in process_args_of_constr (realargs, lra)
896
if noccur_with_meta n nbfix a then
897
let env' = push_rel (x, None, a) env in
898
check_rec_call env' alreadygrd (n+1) vlra b
900
raise (CoFixGuardError (env,RecCallInTypeOfAbstraction a))
902
| CoFix (j,(_,varit,vdefs as recdef)) ->
903
if (List.for_all (noccur_with_meta n nbfix) args)
905
let nbfix = Array.length vdefs in
906
if (array_for_all (noccur_with_meta n nbfix) varit) then
907
let env' = push_rec_types recdef env in
908
(Array.iter (check_rec_call env' alreadygrd (n+1) vlra) vdefs;
909
List.iter (check_rec_call env alreadygrd n vlra) args)
911
raise (CoFixGuardError (env,RecCallInTypeOfDef c))
913
raise (CoFixGuardError (env,UnguardedRecursiveCall c))
915
| Case (_,p,tm,vrest) ->
916
if (noccur_with_meta n nbfix p) then
917
if (noccur_with_meta n nbfix tm) then
918
if (List.for_all (noccur_with_meta n nbfix) args) then
919
Array.iter (check_rec_call env alreadygrd n vlra) vrest
921
raise (CoFixGuardError (env,RecCallInCaseFun c))
923
raise (CoFixGuardError (env,RecCallInCaseArg c))
925
raise (CoFixGuardError (env,RecCallInCasePred c))
929
List.iter (check_rec_call env alreadygrd n vlra) args
931
| _ -> raise (CoFixGuardError (env,NotGuardedForm t)) in
933
let (mind, _) = codomain_is_coind env deftype in
934
let vlra = lookup_subterms env mind in
935
check_rec_call env false 1 (dest_subterms vlra) def
937
(* The function which checks that the whole block of definitions
938
satisfies the guarded condition *)
940
let check_cofix env (bodynum,(names,types,bodies as recdef)) =
941
let nbfix = Array.length bodies in
942
for i = 0 to nbfix-1 do
943
let fixenv = push_rec_types recdef env in
944
try check_one_cofix fixenv nbfix bodies.(i) types.(i)
945
with CoFixGuardError (errenv,err) ->
946
error_ill_formed_rec_body errenv err names i
947
fixenv (judgment_of_fixpoint recdef)
added
removed
kernel/inductive.ml
