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 10172 2007-10-04 13:02:03Z herbelin $ *)
20
let inductive_of_constructor = fst
21
let index_of_constructor = snd
22
let ith_constructor_of_inductive ind i = (ind,i)
24
type mind_specif = mutual_inductive_body * one_inductive_body
26
(* raise Not_found if not an inductive type *)
27
let lookup_mind_specif env (kn,tyi) =
28
let mib = lookup_mind kn env in
29
if tyi >= Array.length mib.mind_packets then
30
error "Inductive.lookup_mind_specif: invalid inductive index";
31
(mib, mib.mind_packets.(tyi))
33
let find_rectype env c =
34
let (t, l) = decompose_app (whd_betadeltaiota env c) in
37
| _ -> raise Not_found
39
let find_inductive env c =
40
let (t, l) = decompose_app (whd_betadeltaiota env c) in
43
when (fst (lookup_mind_specif env ind)).mind_finite -> (ind, l)
44
| _ -> raise Not_found
46
let find_coinductive env c =
47
let (t, l) = decompose_app (whd_betadeltaiota env c) in
50
when not (fst (lookup_mind_specif env ind)).mind_finite -> (ind, l)
51
| _ -> raise Not_found
53
let inductive_params (mib,_) = mib.mind_nparams
55
(************************************************************************)
57
(* Build the substitution that replaces Rels by the appropriate *)
59
let ind_subst mind mib =
60
let ntypes = mib.mind_ntypes in
61
let make_Ik k = Ind (mind,ntypes-k-1) in
62
list_tabulate make_Ik ntypes
64
(* Instantiate inductives in constructor type *)
65
let constructor_instantiate mind mib c =
66
let s = ind_subst mind mib in
69
let instantiate_params full t args sign =
71
anomaly "instantiate_params: type, ctxt and args mismatch" in
72
let (rem_args, subs, ty) =
74
(fun (_,copt,_) (largs,subs,ty) ->
75
match (copt, largs, ty) with
76
| (None, a::args, Prod(_,_,t)) -> (args, a::subs, t)
77
| (Some b,_,LetIn(_,_,_,t)) -> (largs, (substl subs b)::subs, t)
78
| (_,[],_) -> if full then fail() else ([], subs, ty)
83
if rem_args <> [] then fail();
86
let instantiate_partial_params = instantiate_params false
88
let full_inductive_instantiate mib params sign =
89
let dummy = Prop Null in
90
let t = mkArity (sign,dummy) in
91
fst (destArity (instantiate_params true t params mib.mind_params_ctxt))
93
let full_constructor_instantiate ((mind,_),(mib,_),params) =
94
let inst_ind = constructor_instantiate mind mib in
96
instantiate_params true (inst_ind t) params mib.mind_params_ctxt)
98
(************************************************************************)
99
(************************************************************************)
101
(* Functions to build standard types related to inductive *)
104
let number_of_inductives mib = Array.length mib.mind_packets
105
let number_of_constructors mip = Array.length mip.mind_consnames
108
Computing the actual sort of an applied or partially applied inductive type:
110
I_i: forall uniformparams:utyps, forall otherparams:otyps, Type(a)
113
I_1:forall ...,s_1;...I_n:forall ...,s_n |- sort(C_kj(uniformargs)) = s_kj
115
merge(..s'_k..) = ..s''_k..
116
--------------------------------------------------------------------
117
Gamma |- I_i uniformargs otherargs : phi(s''_i)
121
- if p=0, phi() = Prop
123
- if p<>1, phi(s) = sup(Set,s)
125
Remark: Set (predicative) is encoded as Type(0)
128
let sort_as_univ = function
130
| Prop Null -> type0m_univ
131
| Prop Pos -> type0_univ
133
let cons_subst u su subst =
134
try (u, sup su (List.assoc u subst)) :: List.remove_assoc u subst
135
with Not_found -> (u, su) :: subst
137
let actualize_decl_level env lev t =
138
let sign,s = dest_arity env t in
141
let polymorphism_on_non_applied_parameters = false
143
(* Bind expected levels of parameters to actual levels *)
144
(* Propagate the new levels in the signature *)
145
let rec make_subst env = function
146
| (_,Some _,_ as t)::sign, exp, args ->
147
let ctx,subst = make_subst env (sign, exp, args) in
149
| d::sign, None::exp, args ->
150
let args = match args with _::args -> args | [] -> [] in
151
let ctx,subst = make_subst env (sign, exp, args) in
153
| d::sign, Some u::exp, a::args ->
154
(* We recover the level of the argument, but we don't change the *)
155
(* level in the corresponding type in the arity; this level in the *)
156
(* arity is a global level which, at typing time, will be enforce *)
157
(* to be greater than the level of the argument; this is probably *)
158
(* a useless extra constraint *)
159
let s = sort_as_univ (snd (dest_arity env a)) in
160
let ctx,subst = make_subst env (sign, exp, args) in
161
d::ctx, cons_subst u s subst
162
| (na,None,t as d)::sign, Some u::exp, [] ->
163
(* No more argument here: we instantiate the type with a fresh level *)
164
(* which is first propagated to the corresponding premise in the arity *)
165
(* (actualize_decl_level), then to the conclusion of the arity (via *)
166
(* the substitution) *)
167
let ctx,subst = make_subst env (sign, exp, []) in
168
if polymorphism_on_non_applied_parameters then
169
let s = fresh_local_univ () in
170
let t = actualize_decl_level env (Type s) t in
171
(na,None,t)::ctx, cons_subst u s subst
175
(* Uniform parameters are exhausted *)
180
let instantiate_universes env ctx ar argsorts =
181
let args = Array.to_list argsorts in
182
let ctx,subst = make_subst env (ctx,ar.poly_param_levels,args) in
183
let level = subst_large_constraints subst ar.poly_level in
185
if is_type0m_univ level then Prop Null
186
else if is_type0_univ level then Prop Pos
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
230
(************************************************************************)
232
let error_elim_expln kp ki =
234
| (InType | InSet), InProp -> NonInformativeToInformative
235
| InType, InSet -> StrongEliminationOnNonSmallType (* if Set impredicative *)
238
(* Type of case predicates *)
240
(* Get type of inductive, with parameters instantiated *)
242
let inductive_sort_family mip =
243
match mip.mind_arity with
244
| Monomorphic s -> family_of_sort s.mind_sort
245
| Polymorphic _ -> InType
248
mip.mind_arity_ctxt, inductive_sort_family mip
250
let get_instantiated_arity (mib,mip) params =
251
let sign, s = mind_arity mip in
252
full_inductive_instantiate mib params sign, s
254
let elim_sorts (_,mip) = mip.mind_kelim
258
if p>m then l else reln (Rel(n+p)::l) (p+1)
262
let build_dependent_inductive ind (_,mip) params =
263
let nrealargs = mip.mind_nrealargs in
265
(Ind ind, (List.map (lift nrealargs) params)@(rel_list 0 nrealargs))
267
(* This exception is local *)
268
exception LocalArity of (sorts_family * sorts_family * arity_error) option
270
let check_allowed_sort ksort specif =
271
if not (List.exists ((=) ksort) (elim_sorts specif)) then
272
let s = inductive_sort_family (snd specif) in
273
raise (LocalArity (Some(ksort,s,error_elim_expln ksort s)))
275
let is_correct_arity env c (p,pj) ind specif params =
276
let arsign,_ = get_instantiated_arity specif params in
277
let rec srec env pt ar =
278
let pt' = whd_betadeltaiota env pt in
280
| Prod (na1,a1,t), (_,None,a1')::ar' ->
282
with NotConvertible -> raise (LocalArity None));
283
srec (push_rel (na1,None,a1) env) t ar'
284
| Prod (_,a1,a2), [] -> (* whnf of t was not needed here! *)
285
let ksort = match (whd_betadeltaiota env a2) with
286
| Sort s -> family_of_sort s
287
| _ -> raise (LocalArity None) in
288
let dep_ind = build_dependent_inductive ind specif params in
289
(try conv env a1 dep_ind
290
with NotConvertible -> raise (LocalArity None));
291
check_allowed_sort ksort specif;
294
check_allowed_sort (family_of_sort s') specif;
297
raise (LocalArity None)
299
try srec env pj (List.rev arsign)
300
with LocalArity kinds ->
301
error_elim_arity env ind (elim_sorts specif) c (p,pj) kinds
304
(************************************************************************)
305
(* Type of case branches *)
307
(* [p] is the predicate, [i] is the constructor number (starting from 0),
308
and [cty] is the type of the constructor (params not instantiated) *)
309
let build_branches_type ind (_,mip as specif) params dep p =
310
let build_one_branch i cty =
311
let typi = full_constructor_instantiate (ind,specif,params) cty in
312
let (args,ccl) = decompose_prod_assum typi in
313
let nargs = rel_context_length args in
314
let (_,allargs) = decompose_app ccl in
315
let (lparams,vargs) = list_chop (inductive_params specif) allargs in
318
let cstr = ith_constructor_of_inductive ind (i+1) in
320
applist (Construct cstr,lparams@extended_rel_list 0 args) in
324
let base = beta_appvect (lift nargs p) (Array.of_list cargs) in
325
it_mkProd_or_LetIn base args in
326
Array.mapi build_one_branch mip.mind_nf_lc
328
(* [p] is the predicate, [c] is the match object, [realargs] is the
329
list of real args of the inductive type *)
330
let build_case_type dep p c realargs =
331
let args = if dep then realargs@[c] else realargs in
332
beta_appvect p (Array.of_list args)
334
let type_case_branches env (ind,largs) (p,pj) c =
335
let specif = lookup_mind_specif env ind in
336
let nparams = inductive_params specif in
337
let (params,realargs) = list_chop nparams largs in
338
let dep = is_correct_arity env c (p,pj) ind specif params in
339
let lc = build_branches_type ind specif params dep p in
340
let ty = build_case_type dep p c realargs in
344
(************************************************************************)
345
(* Checking the case annotation is relevent *)
347
let check_case_info env indsp ci =
348
let (mib,mip) = lookup_mind_specif env indsp in
350
not (mind_equiv env indsp ci.ci_ind) or
351
(mib.mind_nparams <> ci.ci_npar) or
352
(mip.mind_consnrealdecls <> ci.ci_cstr_nargs)
353
then raise (TypeError(env,WrongCaseInfo(indsp,ci)))
355
(************************************************************************)
356
(************************************************************************)
358
(* Guard conditions for fix and cofix-points *)
360
(* Check if t is a subterm of Rel n, and gives its specification,
361
assuming lst already gives index of
362
subterms with corresponding specifications of recursive arguments *)
364
(* A powerful notion of subterm *)
366
(* To each inductive definition corresponds an array describing the
367
structure of recursive arguments for each constructor, we call it
368
the recursive spec of the type (it has type recargs vect). For
369
checking the guard, we start from the decreasing argument (Rel n)
370
with its recursive spec. During checking the guardness condition,
371
we collect patterns variables corresponding to subterms of n, each
372
of them with its recursive spec. They are organised in a list lst
373
of type (int * recargs) list which is sorted with respect to the
377
(*************************************************************)
378
(* Environment annotated with marks on recursive arguments *)
380
(* tells whether it is a strict or loose subterm *)
381
type size = Large | Strict
383
(* merging information *)
386
Strict, Strict -> Strict
389
(* possible specifications for a term:
390
- Not_subterm: when the size of a term is not related to the
391
recursive argument of the fixpoint
392
- Subterm: when the term is a subterm of the recursive argument
393
the wf_paths argument specifies which subterms are recursive
394
- Dead_code: when the term has been built by elimination over an
399
Subterm of (size * wf_paths)
404
if Rtree.eq_rtree (=) t mk_norec then Not_subterm else Subterm(Strict,t)
406
let subterm_spec_glb =
411
| Not_subterm, _ -> Not_subterm
412
| _, Not_subterm -> Not_subterm
413
| Subterm (a1,t1), Subterm (a2,t2) ->
414
if Rtree.eq_rtree (=) t1 t2 then Subterm (size_glb a1 a2, t1)
415
(* branches do not return objects with same spec *)
417
Array.fold_left glb2 Dead_code
421
(* dB of last fixpoint *)
423
(* inductive of recarg of each fixpoint *)
424
inds : inductive array;
425
(* the recarg information of inductive family *)
426
recvec : wf_paths array;
427
(* dB of variables denoting subterms *)
428
genv : subterm_spec list;
431
let make_renv env minds recarg (kn,tyi) =
432
let mib = lookup_mind kn env in
434
Array.map (fun mip -> mip.mind_recargs) mib.mind_packets in
438
recvec = mind_recvec;
439
genv = [Subterm(Large,mind_recvec.(tyi))] }
441
let push_var renv (x,ty,spec) =
443
env = push_rel (x,None,ty) renv.env;
444
rel_min = renv.rel_min+1;
445
genv = spec:: renv.genv }
447
let assign_var_spec renv (i,spec) =
448
{ renv with genv = list_assign renv.genv (i-1) spec }
450
let push_var_renv renv (x,ty) =
451
push_var renv (x,ty,Not_subterm)
453
(* Fetch recursive information about a variable p *)
454
let subterm_var p renv =
455
try List.nth renv.genv (p-1)
456
with Failure _ | Invalid_argument _ -> Not_subterm
458
(* Add a variable and mark it as strictly smaller with information [spec]. *)
459
let add_subterm renv (x,a,spec) =
460
push_var renv (x,a,spec_of_tree spec)
462
let push_ctxt_renv renv ctxt =
463
let n = rel_context_length ctxt in
465
env = push_rel_context ctxt renv.env;
466
rel_min = renv.rel_min+n;
467
genv = iterate (fun ge -> Not_subterm::ge) n renv.genv }
469
let push_fix_renv renv (_,v,_ as recdef) =
470
let n = Array.length v in
472
env = push_rec_types recdef renv.env;
473
rel_min = renv.rel_min+n;
474
genv = iterate (fun ge -> Not_subterm::ge) n renv.genv }
477
(******************************)
478
(* Computing the recursive subterms of a term (propagation of size
479
information through Cases). *)
482
c is a branch of an inductive definition corresponding to the spec
483
lrec. mind_recvec is the recursive spec of the inductive
484
definition of the decreasing argument n.
486
case_branches_specif renv lrec lc will pass the lambdas
487
of c corresponding to pattern variables and collect possibly new
488
subterms variables and returns the bodies of the branches with the
489
correct envs and decreasing args.
492
let lookup_subterms env ind =
493
let (_,mip) = lookup_mind_specif env ind in
496
(*********************************)
498
(* Propagation of size information through Cases: if the matched
499
object is a recursive subterm then compute the information
500
associated to its own subterms.
501
Rq: if branch is not eta-long, then the recursive information
502
is not propagated to the missing abstractions *)
503
let case_branches_specif renv c_spec ind lbr =
504
let rec push_branch_args renv lrec c =
507
let c' = whd_betadeltaiota renv.env c in
510
let renv' = push_var renv (x,a,ra) in
511
push_branch_args renv' lr b
512
| _ -> (* branch not in eta-long form: cannot perform rec. calls *)
517
let sub_spec = Array.map (List.map spec_of_tree) (dest_subterms t) in
518
assert (Array.length sub_spec = Array.length lbr);
519
array_map2 (push_branch_args renv) sub_spec lbr
521
let t = dest_subterms (lookup_subterms renv.env ind) in
522
let sub_spec = Array.map (List.map (fun _ -> Dead_code)) t in
523
assert (Array.length sub_spec = Array.length lbr);
524
array_map2 (push_branch_args renv) sub_spec lbr
525
| Not_subterm -> Array.map (fun c -> (renv,c)) lbr
527
(* [subterm_specif renv t] computes the recursive structure of [t] and
528
compare its size with the size of the initial recursive argument of
529
the fixpoint we are checking. [renv] collects such information
533
let rec subterm_specif renv t =
534
(* maybe reduction is not always necessary! *)
535
let f,l = decompose_app (whd_betadeltaiota renv.env t) in
537
| Rel k -> subterm_var k renv
539
| Case (ci,_,c,lbr) ->
540
if Array.length lbr = 0 then Dead_code
542
let c_spec = subterm_specif renv c in
543
let lbr_spec = case_branches_specif renv c_spec ci.ci_ind lbr in
545
Array.map (fun (renv',br') -> subterm_specif renv' br')
549
| Fix ((recindxs,i),(_,typarray,bodies as recdef)) ->
550
(* when proving that the fixpoint f(x)=e is less than n, it is enough
551
to prove that e is less than n assuming f is less than n
552
furthermore when f is applied to a term which is strictly less than
553
n, one may assume that x itself is strictly less than n
555
let (ctxt,clfix) = dest_prod renv.env typarray.(i) in
557
let env' = push_rel_context ctxt renv.env in
558
try Some(fst(find_inductive env' clfix))
559
with Not_found -> None in
561
None -> Not_subterm (* happens if fix is polymorphic *)
563
let nbfix = Array.length typarray in
564
let recargs = lookup_subterms renv.env ind in
565
(* pushing the fixpoints *)
566
let renv' = push_fix_renv renv recdef in
568
(* Why Strict here ? To be general, it could also be
570
assign_var_spec renv' (nbfix-i, Subterm(Strict,recargs)) in
571
let decrArg = recindxs.(i) in
572
let theBody = bodies.(i) in
573
let nbOfAbst = decrArg+1 in
574
let sign,strippedBody = decompose_lam_n_assum nbOfAbst theBody in
575
(* pushing the fix parameters *)
576
let renv'' = push_ctxt_renv renv' sign in
578
if List.length l < nbOfAbst then renv''
580
let theDecrArg = List.nth l decrArg in
581
let arg_spec = subterm_specif renv theDecrArg in
582
assign_var_spec renv'' (1, arg_spec) in
583
subterm_specif renv'' strippedBody)
587
subterm_specif (push_var_renv renv (x,a)) b
589
(* Metas and evars are considered OK *)
590
| (Meta _|Evar _) -> Dead_code
592
(* Other terms are not subterms *)
596
(* Check term c can be applied to one of the mutual fixpoints. *)
597
let check_is_subterm renv c =
598
match subterm_specif renv c with
599
Subterm (Strict,_) | Dead_code -> true
602
(************************************************************************)
604
exception FixGuardError of env * guard_error
606
let error_illegal_rec_call renv fx arg =
607
let (_,le_vars,lt_vars) =
609
(fun (i,le,lt) sbt ->
611
(Subterm(Strict,_) | Dead_code) -> (i+1, le, i::lt)
612
| (Subterm(Large,_)) -> (i+1, i::le, lt)
613
| _ -> (i+1, le ,lt))
614
(1,[],[]) renv.genv in
615
raise (FixGuardError (renv.env,
616
RecursionOnIllegalTerm(fx,arg,le_vars,lt_vars)))
618
let error_partial_apply renv fx =
619
raise (FixGuardError (renv.env,NotEnoughArgumentsForFixCall fx))
621
(* Check if [def] is a guarded fixpoint body with decreasing arg.
622
given [recpos], the decreasing arguments of each mutually defined
624
let check_one_fix renv recpos def =
625
let nfi = Array.length recpos in
627
(* Checks if [t] only make valid recursive calls *)
628
let rec check_rec_call renv t =
629
(* if [t] does not make recursive calls, it is guarded: *)
630
if noccur_with_meta renv.rel_min nfi t then ()
632
let (f,l) = decompose_app (whd_betaiotazeta renv.env t) in
635
(* Test if [p] is a fixpoint (recursive call) *)
636
if renv.rel_min <= p & p < renv.rel_min+nfi then
638
List.iter (check_rec_call renv) l;
639
(* the position of the invoked fixpoint: *)
640
let glob = renv.rel_min+nfi-1-p in
641
(* the decreasing arg of the rec call: *)
642
let np = recpos.(glob) in
643
if List.length l <= np then error_partial_apply renv glob
645
(* Check the decreasing arg is smaller *)
646
let z = List.nth l np in
647
if not (check_is_subterm renv z) then
648
error_illegal_rec_call renv glob z
652
match pi2 (lookup_rel p renv.env) with
654
List.iter (check_rec_call renv) l
656
try List.iter (check_rec_call renv) l
657
with FixGuardError _ -> check_rec_call renv (applist(c,l))
660
| Case (ci,p,c_0,lrest) ->
661
List.iter (check_rec_call renv) (c_0::p::l);
662
(* compute the recarg information for the arguments of
664
let c_spec = subterm_specif renv c_0 in
665
let lbr = case_branches_specif renv c_spec ci.ci_ind lrest in
666
Array.iter (fun (renv',br') -> check_rec_call renv' br') lbr
668
(* Enables to traverse Fixpoint definitions in a more intelligent
670
if - g = Fix g/p := [y1:T1]...[yp:Tp]e &
671
- f is guarded with respect to the set of pattern variables S
673
- f is guarded with respect to the set of pattern variables S
675
- ap is a sub-term of the formal argument of f &
676
- f is guarded with respect to the set of pattern variables
678
then f is guarded with respect to S in (g a1 ... am).
681
| Fix ((recindxs,i),(_,typarray,bodies as recdef)) ->
682
List.iter (check_rec_call renv) l;
683
Array.iter (check_rec_call renv) typarray;
684
let decrArg = recindxs.(i) in
685
let renv' = push_fix_renv renv recdef in
686
if (List.length l < (decrArg+1)) then
687
Array.iter (check_rec_call renv') bodies
692
let theDecrArg = List.nth l decrArg in
693
let arg_spec = subterm_specif renv theDecrArg in
694
check_nested_fix_body renv' (decrArg+1) arg_spec body
695
else check_rec_call renv' body)
699
if evaluable_constant kn renv.env then
700
try List.iter (check_rec_call renv) l
701
with (FixGuardError _ ) ->
702
check_rec_call renv(applist(constant_value renv.env kn, l))
703
else List.iter (check_rec_call renv) l
705
(* The cases below simply check recursively the condition on the
708
List.iter (check_rec_call renv) (a::b::l)
711
List.iter (check_rec_call renv) (a::l);
712
check_rec_call (push_var_renv renv (x,a)) b
715
List.iter (check_rec_call renv) (a::l);
716
check_rec_call (push_var_renv renv (x,a)) b
718
| CoFix (i,(_,typarray,bodies as recdef)) ->
719
List.iter (check_rec_call renv) l;
720
Array.iter (check_rec_call renv) typarray;
721
let renv' = push_fix_renv renv recdef in
722
Array.iter (check_rec_call renv') bodies
724
| (Ind _ | Construct _ | Sort _) ->
725
List.iter (check_rec_call renv) l
729
match pi2 (lookup_named id renv.env) with
731
List.iter (check_rec_call renv) l
733
try List.iter (check_rec_call renv) l
734
with (FixGuardError _) -> check_rec_call renv (applist(c,l))
737
(* l is not checked because it is considered as the meta's context *)
738
| (Evar _ | Meta _) -> ()
740
| (App _|LetIn _) -> assert false (* beta zeta reduction *)
742
and check_nested_fix_body renv decr recArgsDecrArg body =
744
check_rec_call (assign_var_spec renv (1,recArgsDecrArg)) body
748
check_rec_call renv a;
749
let renv' = push_var_renv renv (x,a) in
750
check_nested_fix_body renv' (decr-1) recArgsDecrArg b
751
| _ -> anomaly "Not enough abstractions in fix body"
754
check_rec_call renv def
757
let inductive_of_mutfix env ((nvect,bodynum),(names,types,bodies as recdef)) =
758
let nbfix = Array.length bodies in
760
or Array.length nvect <> nbfix
761
or Array.length types <> nbfix
762
or Array.length names <> nbfix
765
then anomaly "Ill-formed fix term";
766
let fixenv = push_rec_types recdef env in
767
let raise_err env i err =
768
error_ill_formed_rec_body env err names i in
769
(* Check the i-th definition with recarg k *)
770
let find_ind i k def =
771
(* check fi does not appear in the k+1 first abstractions,
772
gives the type of the k+1-eme abstraction (must be an inductive) *)
773
let rec check_occur env n def =
774
match (whd_betadeltaiota env def) with
776
if noccur_with_meta n nbfix a then
777
let env' = push_rel (x, None, a) env in
779
(* get the inductive type of the fixpoint *)
781
try find_inductive env a
783
raise_err env i (RecursionNotOnInductiveType a) in
785
else check_occur env' (n+1) b
786
else anomaly "check_one_fix: Bad occurrence of recursive call"
787
| _ -> raise_err env i NotEnoughAbstractionInFixBody in
788
check_occur fixenv 1 def in
789
(* Do it on every fixpoint *)
790
let rv = array_map2_i find_ind nvect bodies in
791
(Array.map fst rv, Array.map snd rv)
794
let check_fix env ((nvect,_),(names,_,bodies as _recdef) as fix) =
795
let (minds, rdef) = inductive_of_mutfix env fix in
796
for i = 0 to Array.length bodies - 1 do
797
let (fenv,body) = rdef.(i) in
798
let renv = make_renv fenv minds nvect.(i) minds.(i) in
799
try check_one_fix renv nvect body
800
with FixGuardError (fixenv,err) ->
801
error_ill_formed_rec_body fixenv err names i
805
let cfkey = Profile.declare_profile "check_fix";;
806
let check_fix env fix = Profile.profile3 cfkey check_fix env fix;;
809
(************************************************************************)
812
exception CoFixGuardError of env * guard_error
814
let anomaly_ill_typed () =
815
anomaly "check_one_cofix: too many arguments applied to constructor"
817
let rec codomain_is_coind env c =
818
let b = whd_betadeltaiota env c in
821
codomain_is_coind (push_rel (x, None, a) env) b
823
(try find_coinductive env b
825
raise (CoFixGuardError (env, CodomainNotInductiveType b)))
827
let check_one_cofix env nbfix def deftype =
828
let rec check_rec_call env alreadygrd n vlra t =
829
if not (noccur_with_meta n nbfix t) then
830
let c,args = decompose_app (whd_betadeltaiota env t) in
832
| Rel p when n <= p && p < n+nbfix ->
833
(* recursive call: must be guarded and no nested recursive
835
if not alreadygrd then
836
raise (CoFixGuardError (env,UnguardedRecursiveCall t))
837
else if not(List.for_all (noccur_with_meta n nbfix) args) then
838
raise (CoFixGuardError (env,NestedRecursiveOccurrences))
840
| Construct (_,i as cstr_kn) ->
841
let lra = vlra.(i-1) in
842
let mI = inductive_of_constructor cstr_kn in
843
let (mib,mip) = lookup_mind_specif env mI in
844
let realargs = list_skipn mib.mind_nparams args in
845
let rec process_args_of_constr = function
846
| (t::lr), (rar::lrar) ->
847
if rar = mk_norec then
848
if noccur_with_meta n nbfix t
849
then process_args_of_constr (lr, lrar)
850
else raise (CoFixGuardError
851
(env,RecCallInNonRecArgOfConstructor t))
853
let spec = dest_subterms rar in
854
check_rec_call env true n spec t;
855
process_args_of_constr (lr, lrar)
857
| _ -> anomaly_ill_typed ()
858
in process_args_of_constr (realargs, lra)
862
if noccur_with_meta n nbfix a then
863
let env' = push_rel (x, None, a) env in
864
check_rec_call env' alreadygrd (n+1) vlra b
866
raise (CoFixGuardError (env,RecCallInTypeOfAbstraction a))
868
| CoFix (j,(_,varit,vdefs as recdef)) ->
869
if (List.for_all (noccur_with_meta n nbfix) args)
871
let nbfix = Array.length vdefs in
872
if (array_for_all (noccur_with_meta n nbfix) varit) then
873
let env' = push_rec_types recdef env in
874
(Array.iter (check_rec_call env' alreadygrd (n+1) vlra) vdefs;
875
List.iter (check_rec_call env alreadygrd n vlra) args)
877
raise (CoFixGuardError (env,RecCallInTypeOfDef c))
879
raise (CoFixGuardError (env,UnguardedRecursiveCall c))
881
| Case (_,p,tm,vrest) ->
882
if (noccur_with_meta n nbfix p) then
883
if (noccur_with_meta n nbfix tm) then
884
if (List.for_all (noccur_with_meta n nbfix) args) then
885
Array.iter (check_rec_call env alreadygrd n vlra) vrest
887
raise (CoFixGuardError (env,RecCallInCaseFun c))
889
raise (CoFixGuardError (env,RecCallInCaseArg c))
891
raise (CoFixGuardError (env,RecCallInCasePred c))
895
List.iter (check_rec_call env alreadygrd n vlra) args
897
| _ -> raise (CoFixGuardError (env,NotGuardedForm t)) in
899
let (mind, _) = codomain_is_coind env deftype in
900
let vlra = lookup_subterms env mind in
901
check_rec_call env false 1 (dest_subterms vlra) def
903
(* The function which checks that the whole block of definitions
904
satisfies the guarded condition *)
906
let check_cofix env (bodynum,(names,types,bodies as recdef)) =
907
let nbfix = Array.length bodies in
908
for i = 0 to nbfix-1 do
909
let fixenv = push_rec_types recdef env in
910
try check_one_cofix fixenv nbfix bodies.(i) types.(i)
911
with CoFixGuardError (errenv,err) ->
912
error_ill_formed_rec_body errenv err names i
added
removed
checker/inductive.ml
