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: indrec.ml 11897 2009-02-09 19:28:02Z barras $ *)
30
(* Errors related to recursors building *)
31
type recursion_scheme_error =
32
| NotAllowedCaseAnalysis of (*isrec:*) bool * sorts * inductive
33
| NotMutualInScheme of inductive * inductive
35
exception RecursionSchemeError of recursion_scheme_error
37
let make_prod_dep dep env = if dep then prod_name env else mkProd
38
let mkLambda_string s t c = mkLambda (Name (id_of_string s), t, c)
40
(*******************************************)
41
(* Building curryfied elimination *)
42
(*******************************************)
44
(**********************************************************************)
45
(* Building case analysis schemes *)
46
(* Nouvelle version, plus concise mais plus co�teuse � cause de
47
lift_constructor et lift_inductive_family qui ne se contentent pas de
48
lifter les param�tres globaux *)
50
let mis_make_case_com depopt env sigma ind (mib,mip as specif) kind =
51
let lnamespar = mib.mind_params_ctxt in
52
let dep = match depopt with
53
| None -> inductive_sort_family mip <> InProp
56
if not (List.mem kind (elim_sorts specif)) then
59
(NotAllowedCaseAnalysis (false,new_sort_in_family kind,ind)));
61
let ndepar = mip.mind_nrealargs + 1 in
63
(* Pas g�nant car env ne sert pas � typer mais juste � renommer les Anonym *)
64
(* mais pas tr�s joli ... (mais manque get_sort_of � ce niveau) *)
65
let env' = push_rel_context lnamespar env in
67
let indf = make_ind_family(ind, extended_rel_list 0 lnamespar) in
68
let constrs = get_constructors env indf in
70
let rec add_branch env k =
71
if k = Array.length mip.mind_consnames then
74
let indf' = lift_inductive_family nbprod indf in
75
let arsign,_ = get_arity env indf' in
76
let depind = build_dependent_inductive env indf' in
77
let deparsign = (Anonymous,None,depind)::arsign in
79
let ci = make_case_info env ind RegularStyle in
82
(mkRel (ndepar + nbprod),
83
if dep then extended_rel_vect 0 deparsign
84
else extended_rel_vect 1 arsign) in
86
it_mkLambda_or_LetIn_name env'
87
((if dep then mkLambda_name env' else mkLambda)
88
(Anonymous,depind,pbody))
91
it_mkLambda_or_LetIn_name env'
92
(mkCase (ci, lift ndepar p,
97
let cs = lift_constructor (k+1) constrs.(k) in
98
let t = build_branch_type env dep (mkRel (k+1)) cs in
100
(add_branch (push_rel (Anonymous, None, t) env) (k+1))
102
let typP = make_arity env' dep indf (new_sort_in_family kind) in
103
it_mkLambda_or_LetIn_name env
104
(mkLambda_string "P" typP
105
(add_branch (push_rel (Anonymous,None,typP) env') 0)) lnamespar
107
(* check if the type depends recursively on one of the inductive scheme *)
109
(**********************************************************************)
110
(* Building the recursive elimination *)
113
* t is the type of the constructor co and recargs is the information on
114
* the recursive calls. (It is assumed to be in form given by the user).
115
* build the type of the corresponding branch of the recurrence principle
116
* assuming f has this type, branch_rec gives also the term
117
* [x1]..[xk](f xi (F xi) ...) to be put in the corresponding branch of
119
* FPvect gives for each inductive definition if we want an elimination
120
* on it with which predicate and which recursive function.
123
let type_rec_branch is_rec dep env sigma (vargs,depPvect,decP) tyi cs recargs =
124
let make_prod = make_prod_dep dep in
125
let nparams = List.length vargs in
126
let process_pos env depK pk =
127
let rec prec env i sign p =
128
let p',largs = whd_betadeltaiota_nolet_stack env sigma p in
129
match kind_of_term p' with
131
let d = (n,None,t) in
132
make_prod env (n,t,prec (push_rel d env) (i+1) (d::sign) c)
134
let d = (n,Some b,t) in
135
mkLetIn (n,b,t,prec (push_rel d env) (i+1) (d::sign) c)
137
let realargs = list_skipn nparams largs in
138
let base = applist (lift i pk,realargs) in
140
Reduction.beta_appvect
141
base [|applist (mkRel (i+1),extended_rel_list 0 sign)|]
148
let rec process_constr env i c recargs nhyps li =
149
if nhyps > 0 then match kind_of_term c with
151
let (optionpos,rest) =
155
(match dest_recarg ra with
156
| Mrec j when is_rec -> (depPvect.(j),rest)
158
Flags.if_verbose warning "Ignoring recursive call";
162
(match optionpos with
166
process_constr (push_rel (n,None,t) env) (i+1) c_0 rest
169
let nP = lift (i+1+decP) p in
170
let env' = push_rel (n,None,t) env in
171
let t_0 = process_pos env' dep' nP (lift 1 t) in
172
make_prod_dep (dep or dep') env
176
(push_rel (Anonymous,None,t_0) env')
177
(i+2) (lift 1 c_0) rest (nhyps-1) (i::li))))
178
| LetIn (n,b,t,c_0) ->
181
(push_rel (n,Some b,t) env)
182
(i+1) c_0 recargs (nhyps-1) li)
186
let realargs = List.map (fun k -> mkRel (i-k)) (List.rev li) in
187
let params = List.map (lift i) vargs in
188
let co = applist (mkConstruct cs.cs_cstr,params@realargs) in
189
Reduction.beta_appvect c [|co|]
192
let nhyps = List.length cs.cs_args in
193
let nP = match depPvect.(tyi) with
194
| Some(_,p) -> lift (nhyps+decP) p
195
| _ -> assert false in
196
let base = appvect (nP,cs.cs_concl_realargs) in
197
let c = it_mkProd_or_LetIn base cs.cs_args in
198
process_constr env 0 c recargs nhyps []
200
let make_rec_branch_arg env sigma (nparrec,fvect,decF) f cstr recargs =
201
let process_pos env fk =
202
let rec prec env i hyps p =
203
let p',largs = whd_betadeltaiota_nolet_stack env sigma p in
204
match kind_of_term p' with
206
let d = (n,None,t) in
207
lambda_name env (n,t,prec (push_rel d env) (i+1) (d::hyps) c)
209
let d = (n,Some b,t) in
210
mkLetIn (n,b,t,prec (push_rel d env) (i+1) (d::hyps) c)
212
let realargs = list_skipn nparrec largs
213
and arg = appvect (mkRel (i+1),extended_rel_vect 0 hyps) in
214
applist(lift i fk,realargs@[arg])
219
(* ici, cstrprods est la liste des produits du constructeur instanti� *)
220
let rec process_constr env i f = function
221
| (n,None,t as d)::cprest, recarg::rest ->
223
match dest_recarg recarg with
226
| Mrec i -> fvect.(i)
228
(match optionpos with
231
(n,t,process_constr (push_rel d env) (i+1)
232
(whd_beta Evd.empty (applist (lift 1 f, [(mkRel 1)])))
235
let nF = lift (i+1+decF) f_0 in
236
let env' = push_rel d env in
237
let arg = process_pos env' nF (lift 1 t) in
239
(n,t,process_constr env' (i+1)
240
(whd_beta Evd.empty (applist (lift 1 f, [(mkRel 1); arg])))
242
| (n,Some c,t as d)::cprest, rest ->
245
process_constr (push_rel d env) (i+1) (lift 1 f)
248
| _,[] | [],_ -> anomaly "process_constr"
251
process_constr env 0 f (List.rev cstr.cs_args, recargs)
254
(* Cut a context ctx in 2 parts (ctx1,ctx2) with ctx1 containing k
256
let context_chop k ctx =
257
let rec chop_aux acc = function
258
| (0, l2) -> (List.rev acc, l2)
259
| (n, ((_,Some _,_ as h)::t)) -> chop_aux (h::acc) (n, t)
260
| (n, (h::t)) -> chop_aux (h::acc) (pred n, t)
261
| (_, []) -> failwith "context_chop"
262
in chop_aux [] (k,ctx)
266
let mis_make_indrec env sigma listdepkind mib =
267
let nparams = mib.mind_nparams in
268
let nparrec = mib. mind_nparams_rec in
269
let lnonparrec,lnamesparrec =
270
context_chop (nparams-nparrec) mib.mind_params_ctxt in
271
let nrec = List.length listdepkind in
273
Array.create mib.mind_ntypes (None : (bool * constr) option) in
278
| (indi,mibi,mipi,dep,_)::rest ->
279
(Array.set depPvec (snd indi) (Some(dep,mkRel k));
282
assign nrec listdepkind in
284
Array.map (fun mip -> mip.mind_recargs) mib.mind_packets in
285
(* recarg information for non recursive parameters *)
286
let rec recargparn l n =
287
if n = 0 then l else recargparn (mk_norec::l) (n-1) in
288
let recargpar = recargparn [] (nparams-nparrec) in
290
let makefix nbconstruct =
291
let rec mrec i ln ltyp ldef = function
292
| (indi,mibi,mipi,dep,_)::rest ->
293
let tyi = snd indi in
295
Array.length mipi.mind_consnames in (* nb constructeurs du type*)
297
(* arity in the context of the fixpoint, i.e.
298
P1..P_nrec f1..f_nbconstruct *)
299
let args = extended_rel_list (nrec+nbconstruct) lnamesparrec in
300
let indf = make_ind_family(indi,args) in
302
let arsign,_ = get_arity env indf in
303
let depind = build_dependent_inductive env indf in
304
let deparsign = (Anonymous,None,depind)::arsign in
306
let nonrecpar = rel_context_length lnonparrec in
307
let larsign = rel_context_length deparsign in
308
let ndepar = larsign - nonrecpar in
309
let dect = larsign+nrec+nbconstruct in
311
(* constructors in context of the Cases expr, i.e.
312
P1..P_nrec f1..f_nbconstruct F_1..F_nrec a_1..a_nar x:I *)
313
let args' = extended_rel_list (dect+nrec) lnamesparrec in
314
let args'' = extended_rel_list ndepar lnonparrec in
315
let indf' = make_ind_family(indi,args'@args'') in
318
let constrs = get_constructors env indf' in
319
let fi = rel_vect (dect-i-nctyi) nctyi in
320
let vecfi = Array.map
321
(fun f -> appvect (f,extended_rel_vect ndepar lnonparrec))
325
(make_rec_branch_arg env sigma
326
(nparrec,depPvec,larsign))
327
vecfi constrs (dest_subterms recargsvec.(tyi))
330
let j = (match depPvec.(tyi) with
331
| Some (_,c) when isRel c -> destRel c
335
(* Predicate in the context of the case *)
337
let depind' = build_dependent_inductive env indf' in
338
let arsign',_ = get_arity env indf' in
339
let deparsign' = (Anonymous,None,depind')::arsign' in
342
let nrpar = extended_rel_list (2*ndepar) lnonparrec
343
and nrar = if dep then extended_rel_list 0 deparsign'
344
else extended_rel_list 1 arsign'
349
(* body of i-th component of the mutual fixpoint *)
351
let ci = make_case_info env indi RegularStyle in
352
let concl = applist (mkRel (dect+j+ndepar),pargs) in
354
it_mkLambda_or_LetIn_name env
355
((if dep then mkLambda_name env else mkLambda)
356
(Anonymous,depind',concl))
359
it_mkLambda_or_LetIn_name env
363
(lift_rel_context nrec deparsign)
366
(* type of i-th component of the mutual fixpoint *)
370
let pargs = if dep then extended_rel_vect 0 deparsign
371
else extended_rel_vect 1 arsign
372
in appvect (mkRel (nbconstruct+ndepar+nonrecpar+j),pargs)
373
in it_mkProd_or_LetIn_name env
377
mrec (i+nctyi) (rel_context_nhyps arsign ::ln) (typtyi::ltyp)
380
let fixn = Array.of_list (List.rev ln) in
381
let fixtyi = Array.of_list (List.rev ltyp) in
382
let fixdef = Array.of_list (List.rev ldef) in
383
let names = Array.create nrec (Name(id_of_string "F")) in
384
mkFix ((fixn,p),(names,fixtyi,fixdef))
388
let rec make_branch env i = function
389
| (indi,mibi,mipi,dep,_)::rest ->
390
let tyi = snd indi in
391
let nconstr = Array.length mipi.mind_consnames in
392
let rec onerec env j =
394
make_branch env (i+j) rest
396
let recarg = (dest_subterms recargsvec.(tyi)).(j) in
397
let recarg = recargpar@recarg in
398
let vargs = extended_rel_list (nrec+i+j) lnamesparrec in
399
let cs = get_constructor (indi,mibi,mipi,vargs) (j+1) in
402
true dep env sigma (vargs,depPvec,i+j) tyi cs recarg
404
mkLambda_string "f" p_0
405
(onerec (push_rel (Anonymous,None,p_0) env) (j+1))
408
makefix i listdepkind
410
let rec put_arity env i = function
411
| (indi,_,_,dep,kinds)::rest ->
412
let indf = make_ind_family (indi,extended_rel_list i lnamesparrec) in
413
let typP = make_arity env dep indf (new_sort_in_family kinds) in
414
mkLambda_string "P" typP
415
(put_arity (push_rel (Anonymous,None,typP) env) (i+1) rest)
417
make_branch env 0 listdepkind
420
(* Body on make_one_rec *)
421
let (indi,mibi,mipi,dep,kind) = List.nth listdepkind p in
423
if (mis_is_recursive_subset
424
(List.map (fun (indi,_,_,_,_) -> snd indi) listdepkind)
427
let env' = push_rel_context lnamesparrec env in
428
it_mkLambda_or_LetIn_name env (put_arity env' 0 listdepkind)
431
mis_make_case_com (Some dep) env sigma indi (mibi,mipi) kind
433
(* Body of mis_make_indrec *)
434
list_tabulate make_one_rec nrec
436
(**********************************************************************)
437
(* This builds elimination predicate for Case tactic *)
439
let make_case_com depopt env sigma ity kind =
440
let (mib,mip) = lookup_mind_specif env ity in
441
mis_make_case_com depopt env sigma ity (mib,mip) kind
443
let make_case_dep env = make_case_com (Some true) env
444
let make_case_nodep env = make_case_com (Some false) env
445
let make_case_gen env = make_case_com None env
448
(**********************************************************************)
449
(* [instantiate_indrec_scheme s rec] replace the sort of the scheme
452
let change_sort_arity sort =
453
let rec drec a = match kind_of_term a with
454
| Cast (c,_,_) -> drec c
455
| Prod (n,t,c) -> mkProd (n, t, drec c)
456
| LetIn (n,b,t,c) -> mkLetIn (n,b, t, drec c)
457
| Sort _ -> mkSort sort
462
(* [npar] is the number of expected arguments (then excluding letin's) *)
463
let instantiate_indrec_scheme sort =
464
let rec drec npar elim =
465
match kind_of_term elim with
468
mkLambda (n, change_sort_arity sort t, c)
470
mkLambda (n, t, drec (npar-1) c)
471
| LetIn (n,b,t,c) -> mkLetIn (n,b,t,drec npar c)
472
| _ -> anomaly "instantiate_indrec_scheme: wrong elimination type"
476
(* Change the sort in the type of an inductive definition, builds the
477
corresponding eta-expanded term *)
478
let instantiate_type_indrec_scheme sort npars term =
479
let rec drec np elim =
480
match kind_of_term elim with
483
let t' = change_sort_arity sort t in
485
mkLambda (n, t', mkApp(term,Termops.rel_vect 0 (npars+1)))
487
let c',term' = drec (np-1) c in
488
mkProd (n, t, c'), mkLambda (n, t, term')
489
| LetIn (n,b,t,c) -> let c',term' = drec np c in
490
mkLetIn (n,b,t,c'), mkLetIn (n,b,t,term')
491
| _ -> anomaly "instantiate_type_indrec_scheme: wrong elimination type"
495
(**********************************************************************)
496
(* Interface to build complex Scheme *)
497
(* Check inductive types only occurs once
498
(otherwise we obtain a meaning less scheme) *)
500
let check_arities listdepkind =
501
let _ = List.fold_left
502
(fun ln ((_,ni as mind),mibi,mipi,dep,kind) ->
503
let kelim = elim_sorts (mibi,mipi) in
504
if not (List.exists ((=) kind) kelim) then raise
505
(RecursionSchemeError
506
(NotAllowedCaseAnalysis (true,new_sort_in_family kind,mind)))
507
else if List.mem ni ln then raise
508
(RecursionSchemeError (NotMutualInScheme (mind,mind)))
513
let build_mutual_indrec env sigma = function
514
| (mind,mib,mip,dep,s)::lrecspec ->
515
let (sp,tyi) = mind in
517
(mind,mib,mip, dep,s)::
519
(function (mind',mibi',mipi',dep',s') ->
520
let (sp',_) = mind' in
522
let (mibi',mipi') = lookup_mind_specif env mind' in
523
(mind',mibi',mipi',dep',s')
525
raise (RecursionSchemeError (NotMutualInScheme (mind,mind'))))
528
let _ = check_arities listdepkind in
529
mis_make_indrec env sigma listdepkind mib
530
| _ -> anomaly "build_indrec expects a non empty list of inductive types"
532
let build_indrec env sigma ind =
533
let (mib,mip) = lookup_mind_specif env ind in
534
let kind = inductive_sort_family mip in
535
let dep = kind <> InProp in
536
List.hd (mis_make_indrec env sigma [(ind,mib,mip,dep,kind)] mib)
538
(**********************************************************************)
539
(* To handle old Case/Match syntax in Pretyping *)
541
(*****************************************)
542
(* To interpret Case and Match operators *)
543
(* Expects a dependent predicate *)
545
let type_rec_branches recursive env sigma indt p c =
546
let IndType (indf,realargs) = indt in
547
let (ind,params) = dest_ind_family indf in
548
let (mib,mip) = lookup_mind_specif env ind in
549
let recargs = mip.mind_recargs in
551
let init_depPvec i = if i = tyi then Some(true,p) else None in
552
let depPvec = Array.init mib.mind_ntypes init_depPvec in
553
let constructors = get_constructors env indf in
556
(type_rec_branch recursive true env sigma (params,depPvec,0) tyi)
557
constructors (dest_subterms recargs) in
558
(lft,Reduction.beta_appvect p (Array.of_list (realargs@[c])))
559
(* Non recursive case. Pb: does not deal with unification
560
let (p,ra,_) = type_case_branches env (ind,params@realargs) pj c in
566
let elimination_suffix = function
571
let make_elimination_ident id s = add_suffix id (elimination_suffix s)
573
(* Look up function for the default elimination constant *)
575
let lookup_eliminator ind_sp s =
577
let mp,dp,l = repr_kn kn in
578
let ind_id = (Global.lookup_mind kn).mind_packets.(i).mind_typename in
579
let id = add_suffix ind_id (elimination_suffix s) in
580
(* Try first to get an eliminator defined in the same section as the *)
582
let ref = ConstRef (make_con mp dp (label_of_id id)) in
584
let _ = sp_of_global ref in
587
(* Then try to get a user-defined eliminator in some other places *)
588
(* using short name (e.g. for "eq_rec") *)
589
try constr_of_global (Nametab.locate (make_short_qualid id))
591
errorlabstrm "default_elim"
592
(strbrk "Cannot find the elimination combinator " ++
593
pr_id id ++ strbrk ", the elimination of the inductive definition " ++
594
pr_global_env Idset.empty (IndRef ind_sp) ++
595
strbrk " on sort " ++ pr_sort_family s ++
596
strbrk " is probably not allowed.")
599
(* let env = Global.env() in
600
let path = sp_of_global None (IndRef ind_sp) in
601
let dir, base = repr_path path in
602
let id = add_suffix base (elimination_suffix s) in
603
(* Try first to get an eliminator defined in the same section as the *)
605
try construct_absolute_reference (Names.make_path dir id)
607
(* Then try to get a user-defined eliminator in some other places *)
608
(* using short name (e.g. for "eq_rec") *)
609
try constr_of_global (Nametab.locate (make_short_qualid id))
611
errorlabstrm "default_elim"
612
(str "Cannot find the elimination combinator " ++
613
pr_id id ++ spc () ++
614
str "The elimination of the inductive definition " ++
615
pr_id base ++ spc () ++ str "on sort " ++
616
spc () ++ pr_sort_family s ++
617
str " is probably not allowed")
added
removed
pretyping/indrec.ml
