summaryrefslogtreecommitdiff
path: root/pretyping/indrec.ml
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2010-07-21 09:46:51 +0200
committerGravatar Stephane Glondu <steph@glondu.net>2010-07-21 09:46:51 +0200
commit5b7eafd0f00a16d78f99a27f5c7d5a0de77dc7e6 (patch)
tree631ad791a7685edafeb1fb2e8faeedc8379318ae /pretyping/indrec.ml
parentda178a880e3ace820b41d38b191d3785b82991f5 (diff)
Imported Upstream snapshot 8.3~beta0+13298
Diffstat (limited to 'pretyping/indrec.ml')
-rw-r--r--pretyping/indrec.ml365
1 files changed, 161 insertions, 204 deletions
diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml
index 88a0c2a6..1352b383 100644
--- a/pretyping/indrec.ml
+++ b/pretyping/indrec.ml
@@ -6,7 +6,11 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: indrec.ml 11897 2009-02-09 19:28:02Z barras $ *)
+(* $Id$ *)
+
+(* File initially created by Christine Paulin, 1996 *)
+
+(* This file builds various inductive schemes *)
open Pp
open Util
@@ -15,6 +19,7 @@ open Libnames
open Nameops
open Term
open Termops
+open Namegen
open Declarations
open Entries
open Inductive
@@ -27,6 +32,8 @@ open Safe_typing
open Nametab
open Sign
+type dep_flag = bool
+
(* Errors related to recursors building *)
type recursion_scheme_error =
| NotAllowedCaseAnalysis of (*isrec:*) bool * sorts * inductive
@@ -34,7 +41,7 @@ type recursion_scheme_error =
exception RecursionSchemeError of recursion_scheme_error
-let make_prod_dep dep env = if dep then prod_name env else mkProd
+let make_prod_dep dep env = if dep then mkProd_name env else mkProd
let mkLambda_string s t c = mkLambda (Name (id_of_string s), t, c)
(*******************************************)
@@ -43,22 +50,16 @@ let mkLambda_string s t c = mkLambda (Name (id_of_string s), t, c)
(**********************************************************************)
(* Building case analysis schemes *)
-(* Nouvelle version, plus concise mais plus coûteuse à cause de
- lift_constructor et lift_inductive_family qui ne se contentent pas de
- lifter les paramètres globaux *)
+(* Christine Paulin, 1996 *)
-let mis_make_case_com depopt env sigma ind (mib,mip as specif) kind =
+let mis_make_case_com dep env sigma ind (mib,mip as specif) kind =
let lnamespar = mib.mind_params_ctxt in
- let dep = match depopt with
- | None -> inductive_sort_family mip <> InProp
- | Some d -> d
- in
if not (List.mem kind (elim_sorts specif)) then
raise
(RecursionSchemeError
(NotAllowedCaseAnalysis (false,new_sort_in_family kind,ind)));
- let ndepar = mip.mind_nrealargs + 1 in
+ let ndepar = mip.mind_nrealargs_ctxt + 1 in
(* Pas génant car env ne sert pas à typer mais juste à renommer les Anonym *)
(* mais pas très joli ... (mais manque get_sort_of à ce niveau) *)
@@ -67,7 +68,7 @@ let mis_make_case_com depopt env sigma ind (mib,mip as specif) kind =
let indf = make_ind_family(ind, extended_rel_list 0 lnamespar) in
let constrs = get_constructors env indf in
- let rec add_branch env k =
+ let rec add_branch env k =
if k = Array.length mip.mind_consnames then
let nbprod = k+1 in
@@ -82,7 +83,7 @@ let mis_make_case_com depopt env sigma ind (mib,mip as specif) kind =
(mkRel (ndepar + nbprod),
if dep then extended_rel_vect 0 deparsign
else extended_rel_vect 1 arsign) in
- let p =
+ let p =
it_mkLambda_or_LetIn_name env'
((if dep then mkLambda_name env' else mkLambda)
(Anonymous,depind,pbody))
@@ -100,27 +101,28 @@ let mis_make_case_com depopt env sigma ind (mib,mip as specif) kind =
(add_branch (push_rel (Anonymous, None, t) env) (k+1))
in
let typP = make_arity env' dep indf (new_sort_in_family kind) in
- it_mkLambda_or_LetIn_name env
+ it_mkLambda_or_LetIn_name env
(mkLambda_string "P" typP
(add_branch (push_rel (Anonymous,None,typP) env') 0)) lnamespar
-
+
(* check if the type depends recursively on one of the inductive scheme *)
(**********************************************************************)
(* Building the recursive elimination *)
+(* Christine Paulin, 1996 *)
(*
- * t is the type of the constructor co and recargs is the information on
+ * t is the type of the constructor co and recargs is the information on
* the recursive calls. (It is assumed to be in form given by the user).
* build the type of the corresponding branch of the recurrence principle
- * assuming f has this type, branch_rec gives also the term
- * [x1]..[xk](f xi (F xi) ...) to be put in the corresponding branch of
+ * assuming f has this type, branch_rec gives also the term
+ * [x1]..[xk](f xi (F xi) ...) to be put in the corresponding branch of
* the case operation
- * FPvect gives for each inductive definition if we want an elimination
- * on it with which predicate and which recursive function.
+ * FPvect gives for each inductive definition if we want an elimination
+ * on it with which predicate and which recursive function.
*)
-let type_rec_branch is_rec dep env sigma (vargs,depPvect,decP) tyi cs recargs =
+let type_rec_branch is_rec dep env sigma (vargs,depPvect,decP) tyi cs recargs =
let make_prod = make_prod_dep dep in
let nparams = List.length vargs in
let process_pos env depK pk =
@@ -136,39 +138,39 @@ let type_rec_branch is_rec dep env sigma (vargs,depPvect,decP) tyi cs recargs =
| Ind (_,_) ->
let realargs = list_skipn nparams largs in
let base = applist (lift i pk,realargs) in
- if depK then
+ if depK then
Reduction.beta_appvect
base [|applist (mkRel (i+1),extended_rel_list 0 sign)|]
- else
+ else
base
- | _ -> assert false
+ | _ -> assert false
in
prec env 0 []
in
let rec process_constr env i c recargs nhyps li =
- if nhyps > 0 then match kind_of_term c with
+ if nhyps > 0 then match kind_of_term c with
| Prod (n,t,c_0) ->
- let (optionpos,rest) =
- match recargs with
+ let (optionpos,rest) =
+ match recargs with
| [] -> None,[]
| ra::rest ->
- (match dest_recarg ra with
+ (match dest_recarg ra with
| Mrec j when is_rec -> (depPvect.(j),rest)
- | Imbr _ ->
- Flags.if_verbose warning "Ignoring recursive call";
- (None,rest)
+ | Imbr _ ->
+ Flags.if_verbose warning "Ignoring recursive call";
+ (None,rest)
| _ -> (None, rest))
- in
- (match optionpos with
- | None ->
+ in
+ (match optionpos with
+ | None ->
make_prod env
(n,t,
process_constr (push_rel (n,None,t) env) (i+1) c_0 rest
(nhyps-1) (i::li))
- | Some(dep',p) ->
+ | Some(dep',p) ->
let nP = lift (i+1+decP) p in
let env' = push_rel (n,None,t) env in
- let t_0 = process_pos env' dep' nP (lift 1 t) in
+ let t_0 = process_pos env' dep' nP (lift 1 t) in
make_prod_dep (dep or dep') env
(n,t,
mkArrow t_0
@@ -190,27 +192,27 @@ let type_rec_branch is_rec dep env sigma (vargs,depPvect,decP) tyi cs recargs =
else c
in
let nhyps = List.length cs.cs_args in
- let nP = match depPvect.(tyi) with
+ let nP = match depPvect.(tyi) with
| Some(_,p) -> lift (nhyps+decP) p
| _ -> assert false in
let base = appvect (nP,cs.cs_concl_realargs) in
let c = it_mkProd_or_LetIn base cs.cs_args in
process_constr env 0 c recargs nhyps []
-let make_rec_branch_arg env sigma (nparrec,fvect,decF) f cstr recargs =
+let make_rec_branch_arg env sigma (nparrec,fvect,decF) f cstr recargs =
let process_pos env fk =
let rec prec env i hyps p =
let p',largs = whd_betadeltaiota_nolet_stack env sigma p in
match kind_of_term p' with
| Prod (n,t,c) ->
let d = (n,None,t) in
- lambda_name env (n,t,prec (push_rel d env) (i+1) (d::hyps) c)
+ mkLambda_name env (n,t,prec (push_rel d env) (i+1) (d::hyps) c)
| LetIn (n,b,t,c) ->
let d = (n,Some b,t) in
mkLetIn (n,b,t,prec (push_rel d env) (i+1) (d::hyps) c)
- | Ind _ ->
+ | Ind _ ->
let realargs = list_skipn nparrec largs
- and arg = appvect (mkRel (i+1),extended_rel_vect 0 hyps) in
+ and arg = appvect (mkRel (i+1),extended_rel_vect 0 hyps) in
applist(lift i fk,realargs@[arg])
| _ -> assert false
in
@@ -218,24 +220,24 @@ let make_rec_branch_arg env sigma (nparrec,fvect,decF) f cstr recargs =
in
(* ici, cstrprods est la liste des produits du constructeur instantié *)
let rec process_constr env i f = function
- | (n,None,t as d)::cprest, recarg::rest ->
- let optionpos =
- match dest_recarg recarg with
+ | (n,None,t as d)::cprest, recarg::rest ->
+ let optionpos =
+ match dest_recarg recarg with
| Norec -> None
| Imbr _ -> None
| Mrec i -> fvect.(i)
- in
- (match optionpos with
+ in
+ (match optionpos with
| None ->
- lambda_name env
+ mkLambda_name env
(n,t,process_constr (push_rel d env) (i+1)
(whd_beta Evd.empty (applist (lift 1 f, [(mkRel 1)])))
(cprest,rest))
- | Some(_,f_0) ->
+ | Some(_,f_0) ->
let nF = lift (i+1+decF) f_0 in
let env' = push_rel d env in
- let arg = process_pos env' nF (lift 1 t) in
- lambda_name env
+ let arg = process_pos env' nF (lift 1 t) in
+ mkLambda_name env
(n,t,process_constr env' (i+1)
(whd_beta Evd.empty (applist (lift 1 f, [(mkRel 1); arg])))
(cprest,rest)))
@@ -251,9 +253,9 @@ let make_rec_branch_arg env sigma (nparrec,fvect,decF) f cstr recargs =
process_constr env 0 f (List.rev cstr.cs_args, recargs)
-(* Cut a context ctx in 2 parts (ctx1,ctx2) with ctx1 containing k
+(* Cut a context ctx in 2 parts (ctx1,ctx2) with ctx1 containing k
variables *)
-let context_chop k ctx =
+let context_chop k ctx =
let rec chop_aux acc = function
| (0, l2) -> (List.rev acc, l2)
| (n, ((_,Some _,_ as h)::t)) -> chop_aux (h::acc) (n, t)
@@ -266,24 +268,24 @@ let context_chop k ctx =
let mis_make_indrec env sigma listdepkind mib =
let nparams = mib.mind_nparams in
let nparrec = mib. mind_nparams_rec in
- let lnonparrec,lnamesparrec =
+ let lnonparrec,lnamesparrec =
context_chop (nparams-nparrec) mib.mind_params_ctxt in
let nrec = List.length listdepkind in
let depPvec =
- Array.create mib.mind_ntypes (None : (bool * constr) option) in
- let _ =
- let rec
- assign k = function
+ Array.create mib.mind_ntypes (None : (bool * constr) option) in
+ let _ =
+ let rec
+ assign k = function
| [] -> ()
- | (indi,mibi,mipi,dep,_)::rest ->
+ | (indi,mibi,mipi,dep,_)::rest ->
(Array.set depPvec (snd indi) (Some(dep,mkRel k));
assign (k-1) rest)
- in
- assign nrec listdepkind in
+ in
+ assign nrec listdepkind in
let recargsvec =
Array.map (fun mip -> mip.mind_recargs) mib.mind_packets in
(* recarg information for non recursive parameters *)
- let rec recargparn l n =
+ let rec recargparn l n =
if n = 0 then l else recargparn (mk_norec::l) (n-1) in
let recargpar = recargparn [] (nparams-nparrec) in
let make_one_rec p =
@@ -293,80 +295,80 @@ let mis_make_indrec env sigma listdepkind mib =
let tyi = snd indi in
let nctyi =
Array.length mipi.mind_consnames in (* nb constructeurs du type*)
-
+
(* arity in the context of the fixpoint, i.e.
P1..P_nrec f1..f_nbconstruct *)
let args = extended_rel_list (nrec+nbconstruct) lnamesparrec in
let indf = make_ind_family(indi,args) in
-
+
let arsign,_ = get_arity env indf in
let depind = build_dependent_inductive env indf in
let deparsign = (Anonymous,None,depind)::arsign in
-
+
let nonrecpar = rel_context_length lnonparrec in
let larsign = rel_context_length deparsign in
let ndepar = larsign - nonrecpar in
let dect = larsign+nrec+nbconstruct in
-
+
(* constructors in context of the Cases expr, i.e.
P1..P_nrec f1..f_nbconstruct F_1..F_nrec a_1..a_nar x:I *)
let args' = extended_rel_list (dect+nrec) lnamesparrec in
let args'' = extended_rel_list ndepar lnonparrec in
let indf' = make_ind_family(indi,args'@args'') in
-
- let branches =
+
+ let branches =
let constrs = get_constructors env indf' in
let fi = rel_vect (dect-i-nctyi) nctyi in
- let vecfi = Array.map
+ let vecfi = Array.map
(fun f -> appvect (f,extended_rel_vect ndepar lnonparrec))
- fi
+ fi
in
array_map3
- (make_rec_branch_arg env sigma
+ (make_rec_branch_arg env sigma
(nparrec,depPvec,larsign))
- vecfi constrs (dest_subterms recargsvec.(tyi))
+ vecfi constrs (dest_subterms recargsvec.(tyi))
in
-
- let j = (match depPvec.(tyi) with
- | Some (_,c) when isRel c -> destRel c
- | _ -> assert false)
+
+ let j = (match depPvec.(tyi) with
+ | Some (_,c) when isRel c -> destRel c
+ | _ -> assert false)
in
-
+
(* Predicate in the context of the case *)
-
+
let depind' = build_dependent_inductive env indf' in
let arsign',_ = get_arity env indf' in
let deparsign' = (Anonymous,None,depind')::arsign' in
-
+
let pargs =
- let nrpar = extended_rel_list (2*ndepar) lnonparrec
+ let nrpar = extended_rel_list (2*ndepar) lnonparrec
and nrar = if dep then extended_rel_list 0 deparsign'
else extended_rel_list 1 arsign'
in nrpar@nrar
-
+
in
(* body of i-th component of the mutual fixpoint *)
- let deftyi =
+ let deftyi =
let ci = make_case_info env indi RegularStyle in
- let concl = applist (mkRel (dect+j+ndepar),pargs) in
+ let concl = applist (mkRel (dect+j+ndepar),pargs) in
let pred =
- it_mkLambda_or_LetIn_name env
+ it_mkLambda_or_LetIn_name env
((if dep then mkLambda_name env else mkLambda)
(Anonymous,depind',concl))
arsign'
in
it_mkLambda_or_LetIn_name env
- (mkCase (ci, pred,
+ (mkCase (ci, pred,
mkRel 1,
branches))
(lift_rel_context nrec deparsign)
in
-
+
(* type of i-th component of the mutual fixpoint *)
-
+
let typtyi =
- let concl =
+ let concl =
let pargs = if dep then extended_rel_vect 0 deparsign
else extended_rel_vect 1 arsign
in appvect (mkRel (nbconstruct+ndepar+nonrecpar+j),pargs)
@@ -374,25 +376,25 @@ let mis_make_indrec env sigma listdepkind mib =
concl
deparsign
in
- mrec (i+nctyi) (rel_context_nhyps arsign ::ln) (typtyi::ltyp)
+ mrec (i+nctyi) (rel_context_nhyps arsign ::ln) (typtyi::ltyp)
(deftyi::ldef) rest
- | [] ->
+ | [] ->
let fixn = Array.of_list (List.rev ln) in
let fixtyi = Array.of_list (List.rev ltyp) in
- let fixdef = Array.of_list (List.rev ldef) in
+ let fixdef = Array.of_list (List.rev ldef) in
let names = Array.create nrec (Name(id_of_string "F")) in
mkFix ((fixn,p),(names,fixtyi,fixdef))
- in
- mrec 0 [] [] []
- in
- let rec make_branch env i = function
+ in
+ mrec 0 [] [] []
+ in
+ let rec make_branch env i = function
| (indi,mibi,mipi,dep,_)::rest ->
let tyi = snd indi in
let nconstr = Array.length mipi.mind_consnames in
- let rec onerec env j =
- if j = nconstr then
- make_branch env (i+j) rest
- else
+ let rec onerec env j =
+ if j = nconstr then
+ make_branch env (i+j) rest
+ else
let recarg = (dest_subterms recargsvec.(tyi)).(j) in
let recarg = recargpar@recarg in
let vargs = extended_rel_list (nrec+i+j) lnamesparrec in
@@ -400,106 +402,107 @@ let mis_make_indrec env sigma listdepkind mib =
let p_0 =
type_rec_branch
true dep env sigma (vargs,depPvec,i+j) tyi cs recarg
- in
+ in
mkLambda_string "f" p_0
(onerec (push_rel (Anonymous,None,p_0) env) (j+1))
in onerec env 0
- | [] ->
+ | [] ->
makefix i listdepkind
in
- let rec put_arity env i = function
- | (indi,_,_,dep,kinds)::rest ->
+ let rec put_arity env i = function
+ | (indi,_,_,dep,kinds)::rest ->
let indf = make_ind_family (indi,extended_rel_list i lnamesparrec) in
let typP = make_arity env dep indf (new_sort_in_family kinds) in
mkLambda_string "P" typP
(put_arity (push_rel (Anonymous,None,typP) env) (i+1) rest)
- | [] ->
- make_branch env 0 listdepkind
+ | [] ->
+ make_branch env 0 listdepkind
in
-
+
(* Body on make_one_rec *)
let (indi,mibi,mipi,dep,kind) = List.nth listdepkind p in
-
+
if (mis_is_recursive_subset
(List.map (fun (indi,_,_,_,_) -> snd indi) listdepkind)
- mipi.mind_recargs)
- then
+ mipi.mind_recargs)
+ then
let env' = push_rel_context lnamesparrec env in
- it_mkLambda_or_LetIn_name env (put_arity env' 0 listdepkind)
+ it_mkLambda_or_LetIn_name env (put_arity env' 0 listdepkind)
lnamesparrec
- else
- mis_make_case_com (Some dep) env sigma indi (mibi,mipi) kind
- in
+ else
+ mis_make_case_com dep env sigma indi (mibi,mipi) kind
+ in
(* Body of mis_make_indrec *)
list_tabulate make_one_rec nrec
(**********************************************************************)
(* This builds elimination predicate for Case tactic *)
-let make_case_com depopt env sigma ity kind =
- let (mib,mip) = lookup_mind_specif env ity in
- mis_make_case_com depopt env sigma ity (mib,mip) kind
+let build_case_analysis_scheme env sigma ity dep kind =
+ let (mib,mip) = lookup_mind_specif env ity in
+ mis_make_case_com dep env sigma ity (mib,mip) kind
-let make_case_dep env = make_case_com (Some true) env
-let make_case_nodep env = make_case_com (Some false) env
-let make_case_gen env = make_case_com None env
+let build_case_analysis_scheme_default env sigma ity kind =
+ let (mib,mip) = lookup_mind_specif env ity in
+ let dep = inductive_sort_family mip <> InProp in
+ mis_make_case_com dep env sigma ity (mib,mip) kind
(**********************************************************************)
-(* [instantiate_indrec_scheme s rec] replace the sort of the scheme
+(* [modify_sort_scheme s rec] replaces the sort of the scheme
[rec] by [s] *)
-let change_sort_arity sort =
+let change_sort_arity sort =
let rec drec a = match kind_of_term a with
- | Cast (c,_,_) -> drec c
+ | Cast (c,_,_) -> drec c
| Prod (n,t,c) -> mkProd (n, t, drec c)
| LetIn (n,b,t,c) -> mkLetIn (n,b, t, drec c)
| Sort _ -> mkSort sort
| _ -> assert false
- in
- drec
+ in
+ drec
(* [npar] is the number of expected arguments (then excluding letin's) *)
-let instantiate_indrec_scheme sort =
+let modify_sort_scheme sort =
let rec drec npar elim =
match kind_of_term elim with
- | Lambda (n,t,c) ->
- if npar = 0 then
+ | Lambda (n,t,c) ->
+ if npar = 0 then
mkLambda (n, change_sort_arity sort t, c)
- else
+ else
mkLambda (n, t, drec (npar-1) c)
| LetIn (n,b,t,c) -> mkLetIn (n,b,t,drec npar c)
- | _ -> anomaly "instantiate_indrec_scheme: wrong elimination type"
+ | _ -> anomaly "modify_sort_scheme: wrong elimination type"
in
drec
(* Change the sort in the type of an inductive definition, builds the
corresponding eta-expanded term *)
-let instantiate_type_indrec_scheme sort npars term =
+let weaken_sort_scheme sort npars term =
let rec drec np elim =
match kind_of_term elim with
- | Prod (n,t,c) ->
- if np = 0 then
+ | Prod (n,t,c) ->
+ if np = 0 then
let t' = change_sort_arity sort t in
mkProd (n, t', c),
mkLambda (n, t', mkApp(term,Termops.rel_vect 0 (npars+1)))
- else
+ else
let c',term' = drec (np-1) c in
mkProd (n, t, c'), mkLambda (n, t, term')
| LetIn (n,b,t,c) -> let c',term' = drec np c in
- mkLetIn (n,b,t,c'), mkLetIn (n,b,t,term')
- | _ -> anomaly "instantiate_type_indrec_scheme: wrong elimination type"
+ mkLetIn (n,b,t,c'), mkLetIn (n,b,t,term')
+ | _ -> anomaly "weaken_sort_scheme: wrong elimination type"
in
drec npars
(**********************************************************************)
(* Interface to build complex Scheme *)
-(* Check inductive types only occurs once
+(* Check inductive types only occurs once
(otherwise we obtain a meaning less scheme) *)
-let check_arities listdepkind =
+let check_arities listdepkind =
let _ = List.fold_left
- (fun ln ((_,ni as mind),mibi,mipi,dep,kind) ->
+ (fun ln ((_,ni as mind),mibi,mipi,dep,kind) ->
let kelim = elim_sorts (mibi,mipi) in
if not (List.exists ((=) kind) kelim) then raise
(RecursionSchemeError
@@ -510,56 +513,29 @@ let check_arities listdepkind =
[] listdepkind
in true
-let build_mutual_indrec env sigma = function
- | (mind,mib,mip,dep,s)::lrecspec ->
+let build_mutual_induction_scheme env sigma = function
+ | (mind,dep,s)::lrecspec ->
+ let (mib,mip) = Global.lookup_inductive mind in
let (sp,tyi) = mind in
- let listdepkind =
- (mind,mib,mip, dep,s)::
+ let listdepkind =
+ (mind,mib,mip,dep,s)::
(List.map
- (function (mind',mibi',mipi',dep',s') ->
+ (function (mind',dep',s') ->
let (sp',_) = mind' in
if sp=sp' then
let (mibi',mipi') = lookup_mind_specif env mind' in
(mind',mibi',mipi',dep',s')
else
- raise (RecursionSchemeError (NotMutualInScheme (mind,mind'))))
+ raise (RecursionSchemeError (NotMutualInScheme (mind,mind'))))
lrecspec)
in
- let _ = check_arities listdepkind in
+ let _ = check_arities listdepkind in
mis_make_indrec env sigma listdepkind mib
- | _ -> anomaly "build_indrec expects a non empty list of inductive types"
+ | _ -> anomaly "build_induction_scheme expects a non empty list of inductive types"
-let build_indrec env sigma ind =
+let build_induction_scheme env sigma ind dep kind =
let (mib,mip) = lookup_mind_specif env ind in
- let kind = inductive_sort_family mip in
- let dep = kind <> InProp in
- List.hd (mis_make_indrec env sigma [(ind,mib,mip,dep,kind)] mib)
-
-(**********************************************************************)
-(* To handle old Case/Match syntax in Pretyping *)
-
-(*****************************************)
-(* To interpret Case and Match operators *)
-(* Expects a dependent predicate *)
-
-let type_rec_branches recursive env sigma indt p c =
- let IndType (indf,realargs) = indt in
- let (ind,params) = dest_ind_family indf in
- let (mib,mip) = lookup_mind_specif env ind in
- let recargs = mip.mind_recargs in
- let tyi = snd ind in
- let init_depPvec i = if i = tyi then Some(true,p) else None in
- let depPvec = Array.init mib.mind_ntypes init_depPvec in
- let constructors = get_constructors env indf in
- let lft =
- array_map2
- (type_rec_branch recursive true env sigma (params,depPvec,0) tyi)
- constructors (dest_subterms recargs) in
- (lft,Reduction.beta_appvect p (Array.of_list (realargs@[c])))
-(* Non recursive case. Pb: does not deal with unification
- let (p,ra,_) = type_case_branches env (ind,params@realargs) pj c in
- (p,ra)
-*)
+ List.hd (mis_make_indrec env sigma [(ind,mib,mip,dep,kind)] mib)
(*s Eliminations. *)
@@ -568,51 +544,32 @@ let elimination_suffix = function
| InSet -> "_rec"
| InType -> "_rect"
+let case_suffix = "_case"
+
let make_elimination_ident id s = add_suffix id (elimination_suffix s)
(* Look up function for the default elimination constant *)
let lookup_eliminator ind_sp s =
let kn,i = ind_sp in
- let mp,dp,l = repr_kn kn in
+ let mp,dp,l = repr_mind kn in
let ind_id = (Global.lookup_mind kn).mind_packets.(i).mind_typename in
let id = add_suffix ind_id (elimination_suffix s) in
(* Try first to get an eliminator defined in the same section as the *)
(* inductive type *)
- let ref = ConstRef (make_con mp dp (label_of_id id)) in
- try
- let _ = sp_of_global ref in
- constr_of_global ref
+ try
+ let cst =Global.constant_of_delta
+ (make_con mp dp (label_of_id id)) in
+ let _ = Global.lookup_constant cst in
+ mkConst cst
with Not_found ->
(* Then try to get a user-defined eliminator in some other places *)
(* using short name (e.g. for "eq_rec") *)
- try constr_of_global (Nametab.locate (make_short_qualid id))
+ try constr_of_global (Nametab.locate (qualid_of_ident id))
with Not_found ->
errorlabstrm "default_elim"
(strbrk "Cannot find the elimination combinator " ++
pr_id id ++ strbrk ", the elimination of the inductive definition " ++
- pr_global_env Idset.empty (IndRef ind_sp) ++
+ pr_global_env Idset.empty (IndRef ind_sp) ++
strbrk " on sort " ++ pr_sort_family s ++
strbrk " is probably not allowed.")
-
-
-(* let env = Global.env() in
- let path = sp_of_global None (IndRef ind_sp) in
- let dir, base = repr_path path in
- let id = add_suffix base (elimination_suffix s) in
- (* Try first to get an eliminator defined in the same section as the *)
- (* inductive type *)
- try construct_absolute_reference (Names.make_path dir id)
- with Not_found ->
- (* Then try to get a user-defined eliminator in some other places *)
- (* using short name (e.g. for "eq_rec") *)
- try constr_of_global (Nametab.locate (make_short_qualid id))
- with Not_found ->
- errorlabstrm "default_elim"
- (str "Cannot find the elimination combinator " ++
- pr_id id ++ spc () ++
- str "The elimination of the inductive definition " ++
- pr_id base ++ spc () ++ str "on sort " ++
- spc () ++ pr_sort_family s ++
- str " is probably not allowed")
-*)