diff options
| -rw-r--r-- | library/declare.ml | 2 | ||||
| -rw-r--r-- | library/global.ml | 39 | ||||
| -rw-r--r-- | library/global.mli | 12 | ||||
| -rw-r--r-- | library/indrec.ml | 670 | ||||
| -rw-r--r-- | library/indrec.mli | 45 |
5 files changed, 767 insertions, 1 deletions
diff --git a/library/declare.ml b/library/declare.ml index f92cc43a8..2220632c6 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -132,7 +132,7 @@ let declare_mind mie = Global.add_mind sp mie; push_inductive_names sp mie; declare_inductive_implicits sp - + (***TODO: declare_eliminations ***) (* Global references. *) diff --git a/library/global.ml b/library/global.ml index 5e11a3652..63efdbe4d 100644 --- a/library/global.ml +++ b/library/global.ml @@ -1,6 +1,10 @@ (* $Id$ *) +open Generic +open Term +open Instantiate +open Sign open Typing open Summary @@ -39,3 +43,38 @@ let lookup_mind_specif c = lookup_mind_specif c !global_env let export s = export !global_env s let import cenv = global_env := import cenv !global_env + +(* Re-exported functions of [Inductive], composed with [lookup_mind_specif]. *) + +open Inductive + +let mind_is_recursive = Util.compose mis_is_recursive lookup_mind_specif +let mind_nconstr = Util.compose mis_nconstr lookup_mind_specif +let mind_nparams = Util.compose mis_nparams lookup_mind_specif + +let mis_arity' mis = + let idhyps = ids_of_sign mis.mis_mib.mind_hyps + and largs = Array.to_list mis.mis_args in + { body = instantiate_constr idhyps mis.mis_mip.mind_arity.body largs; + typ = mis.mis_mip.mind_arity.typ } + +let mis_arity mispec = + let { body = b; typ = t } = mis_arity' mispec in + DOP2 (Cast, b, DOP0 (Sort t)) + +let mind_arity = Util.compose mis_arity lookup_mind_specif + +let mis_lc mis = + instantiate_constr (ids_of_sign mis.mis_mib.mind_hyps) + mis.mis_mip.mind_lc (Array.to_list mis.mis_args) + +let mis_lc_without_abstractions mis = + let rec strip_DLAM = function + | (DLAM (n,c1)) -> strip_DLAM c1 + | (DLAMV (n,v)) -> v + | _ -> assert false + in + strip_DLAM (mis_lc mis) + +let mind_lc_without_abstractions = + Util.compose mis_lc_without_abstractions lookup_mind_specif diff --git a/library/global.mli b/library/global.mli index f29276667..5a788f1f9 100644 --- a/library/global.mli +++ b/library/global.mli @@ -37,3 +37,15 @@ val lookup_mind_specif : constr -> mind_specif val export : string -> compiled_env val import : compiled_env -> unit + +(*s Re-exported functions of [Inductive], composed with + [lookup_mind_specif]. *) + +val mind_is_recursive : constr -> bool +val mind_nconstr : constr -> int +val mind_nparams : constr -> int +val mind_arity : constr -> constr + +val mind_lc_without_abstractions : constr -> constr array + + diff --git a/library/indrec.ml b/library/indrec.ml new file mode 100644 index 000000000..788e405f9 --- /dev/null +++ b/library/indrec.ml @@ -0,0 +1,670 @@ + +(* $Id$ *) + +open Pp +open Util +open Names +open Generic +open Term +open Inductive +open Environ +open Reduction +open Typing + +let whd_betadeltaiota_empty env = whd_betadeltaiota env Evd.empty + +let make_lambda_string s t c = DOP2(Lambda,t,DLAM(Name(id_of_string s),c)) + +let make_prod_string s t c = DOP2(Prod,t,DLAM(Name(id_of_string s),c)) + +let lift_context n l = + let k = List.length l in + list_map_i (fun i (name,c) -> (name,liftn n (k-i) c)) 0 l + +(*******************************************) +(* Building curryfied elimination *) +(*******************************************) + +(*********************************************) +(* lc is the list of the constructors of ind *) +(*********************************************) + +let mis_make_case_com depopt sigma mispec kinds = + let sp = mispec.mis_sp in + let tyi = mispec.mis_tyi in + let cl = mispec.mis_args in + let nparams = mis_nparams mispec in + let mip = mispec.mis_mip in + let mind = DOPN(MutInd(sp,tyi),cl) in + let kd = mis_kd mispec in + let kn = mis_kn mispec in + let t = mis_arity mispec in + let (lc,lct) = mis_type_mconstructs mispec in + let lnames,sort = splay_prod sigma t in + let nconstr = Array.length lc in + let dep = match depopt with + | None -> (sort<>DOP0(Sort(Prop Null))) + | Some d -> d + in + let _ = + if dep then begin + if not (List.exists (sort_cmp CONV_X kinds) kd) then + let pm = pTERM mind in + let ps = pTERM (DOP0(Sort kinds)) in + errorlabstrm "Case analysis" + [< 'sTR "Dependent case analysis on sort: "; ps; 'fNL; + 'sTR "is not allowed for inductive definition: "; pm >] + end else if not (List.exists (sort_cmp CONV_X kinds) kn) then + let pm = pTERM mind in + let ps = pTERM (DOP0(Sort kinds)) in + errorlabstrm "Case analysis" + [< 'sTR "Non Dependent case analysis on sort: "; ps; 'fNL; + 'sTR "is not allowed for inductive definition: "; pm >] + in + let lnamesar,lnamespar = chop_list (List.length lnames - nparams) lnames in + let lgar = List.length lnamesar in + let ar = hnf_prod_appvect sigma "make_case_dep" t (rel_vect 0 nparams) in + let typP = + if dep then + make_arity_dep (DOP0(Sort kinds)) ar + (appvect (mind,rel_vect 0 nparams)) + else + make_arity_nodep (DOP0(Sort kinds)) ar + in + let rec add_branch k = + if k = nconstr then + it_lambda_name + (lambda_create + (appvect (mind, + (Array.append (rel_vect (nconstr+lgar+1) nparams) + (rel_vect 0 lgar))), + mkMutCaseA (ci_of_mind mind) + (Rel (nconstr+lgar+2)) + (Rel 1) + (* (appvect (mind, + (Array.append (rel_vect (nconstr+lgar+2) nparams) + (rel_vect 1 lgar)))) *) + (rel_vect (lgar+1) nconstr))) + (lift_context (nconstr+1) lnamesar) + else + make_lambda_string "f" + (if dep then + type_one_branch_dep + (sigma,nparams,(rel_list (k+1) nparams),Rel (k+1)) lc.(k) lct.(k) + else + type_one_branch_nodep + (sigma,nparams,(rel_list (k+1) nparams),Rel (k+1)) lct.(k)) + (add_branch (k+1)) + in + it_lambda_name (make_lambda_string "P" typP (add_branch 0)) lnamespar + +let make_case_com depopt sigma mind kinds = + let ity = mrectype_spec sigma mind in + let (sp,tyi,cl) = destMutInd ity in + let mispec = mind_specif_of_mind ity in + mis_make_case_com depopt sigma mispec kinds + +let make_case_dep sigma = make_case_com (Some true) sigma +let make_case_nodep sigma = make_case_com (Some false) sigma +let make_case_gen sigma = make_case_com None sigma + + +(* check if the type depends recursively on one of the inductive scheme *) + +(* Building the recursive elimination *) + + +(*********************************************************************** +* t is the type of the constructor co and recargs is the information on +* the recursive calls. +* 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 +* the case operation +* FPvect gives for each inductive definition if we want an elimination +* on it with which predicate and which recursive function. +************************************************************************) + +let simple_prod (n,t,c) = DOP2(Prod,t,DLAM(n,c)) +let make_prod_dep dep = if dep then prod_name else simple_prod + +let type_rec_branch dep (sigma,vargs,depPvect,decP) co t recargs = + let make_prod = make_prod_dep dep in + let nparams = Array.length vargs in + let st = hnf_prod_appvect sigma "type_rec_branch" t vargs in + let process_pos depK pk = + let rec prec i p = + match whd_betadeltaiota_stack sigma p [] with + | (DOP2(Prod,t,DLAM(n,c))),[] -> make_prod (n,t,prec (i+1) c) + | (DOPN(MutInd _,_),largs) -> + let (_,realargs) = chop_list nparams largs in + let base = applist (lift i pk,realargs) in + if depK then + mkAppList base [appvect (Rel (i+1),rel_vect 0 i)] + else + base + | _ -> assert false + in + prec 0 + in + let rec process_constr i c recargs co = + match whd_betadeltaiota_stack sigma c [] with + | (DOP2(Prod,t,DLAM(n,c_0)),[]) -> + let (optionpos,rest) = + match recargs with + | [] -> None,[] + | (Param(_)::rest) -> (None,rest) + | (Norec::rest) -> (None,rest) + | (Imbr _::rest) -> + warning "Ignoring recursive call"; (None,rest) + |(Mrec j::rest) -> (depPvect.(j),rest) + in + (match optionpos with + | None -> + make_prod (n,t,process_constr (i+1) c_0 rest + (mkAppList (lift 1 co) [Rel 1])) + | Some(dep',p) -> + let nP = lift (i+1+decP) p in + let t_0 = process_pos dep' nP (lift 1 t) in + make_prod_dep (dep or dep') + (n,t,mkArrow t_0 (process_constr (i+2) (lift 1 c_0) rest + (mkAppList (lift 2 co) [Rel 2])))) + | (DOPN(MutInd(_,tyi),_),largs) -> + let nP = match depPvect.(tyi) with + | Some(_,p) -> lift (i+decP) p + | _ -> assert false in + let (_,realargs) = chop_list nparams largs in + let base = applist (nP,realargs) in + if dep then mkAppList base [co] else base + | _ -> assert false + in + process_constr 0 st recargs (appvect(co,vargs)) + +let rec_branch_arg (sigma,vargs,fvect,decF) f t recargs = + let nparams = Array.length vargs in + let st = hnf_prod_appvect sigma "type_rec_branch" t vargs in + let process_pos fk = + let rec prec i p = + (match whd_betadeltaiota_stack sigma p [] with + | (DOP2(Prod,t,DLAM(n,c))),[] -> lambda_name (n,t,prec (i+1) c) + | (DOPN(MutInd _,_),largs) -> + let (_,realargs) = chop_list nparams largs + and arg = appvect (Rel (i+1),rel_vect 0 i) in + applist(lift i fk,realargs@[arg]) + | _ -> assert false) + in + prec 0 + in + let rec process_constr i c f recargs = + match whd_betadeltaiota_stack sigma c [] with + | (DOP2(Prod,t,DLAM(n,c_0)),[]) -> + let (optionpos,rest) = + match recargs with + | [] -> None,[] + | (Param(i)::rest) -> None,rest + | (Norec::rest) -> None,rest + | (Imbr _::rest) -> None,rest + | (Mrec i::rest) -> fvect.(i),rest + in + (match optionpos with + | None -> + lambda_name + (n,t,process_constr (i+1) c_0 + (applist(whd_beta_stack (lift 1 f) [(Rel 1)])) rest) + | Some(_,f_0) -> + let nF = lift (i+1+decF) f_0 in + let arg = process_pos nF (lift 1 t) in + lambda_name + (n,t,process_constr (i+1) c_0 + (applist(whd_beta_stack (lift 1 f) [(Rel 1); arg])) + rest)) + | (DOPN(MutInd(_,tyi),_),largs) -> f + | _ -> assert false + in + process_constr 0 st f recargs + +let mis_make_indrec sigma listdepkind mispec = + let nparams = mis_nparams mispec in + let recargsvec = mis_recargs mispec in + let ntypes = mis_ntypes mispec in + let mind_arity = mis_arity mispec in + let (lnames, ckind) = splay_prod sigma mind_arity in + let kind = destSort ckind in + let lnamespar = lastn nparams lnames in + let listdepkind = + if listdepkind = [] then + let dep = kind <> Prop Null in [(mispec,dep,kind)] + else + listdepkind + in + let nrec = List.length listdepkind in + let depPvec = Array.create ntypes (None : (bool * constr) option) in + let _ = + let rec + assign k = function + | [] -> () + | (mispeci,dep,_)::rest -> + (Array.set depPvec mispeci.tyi (Some(dep,Rel k)); + assign (k-1) rest) + in + assign nrec listdepkind + in + let make_one_rec p = + let makefix nbconstruct = + let rec mrec i ln ltyp ldef = function + | (mispeci,dep,_)::rest -> + let tyi = mispeci.tyi in + let mind = DOPN(MutInd (mispeci.sp,tyi),mispeci.args) in + let (_,lct) = mis_type_mconstructs mispeci in + let nctyi = Array.length lct in (* nb constructeurs du type *) + let realar = hnf_prod_appvect sigma "make_branch" + (mis_arity mispeci) + (rel_vect (nrec+nbconstruct) nparams) in + (* arity in the contexte P1..Prec f1..f_nbconstruct *) + let lnames,_ = splay_prod sigma realar in + let nar = List.length lnames in + let decf = nar+nrec+nbconstruct+nrec in + let dect = nar+nrec+nbconstruct in + let vecfi = rel_vect (dect+1-i-nctyi) nctyi in + let branches = + map3_vect + (rec_branch_arg (sigma,rel_vect (decf+1) nparams, + depPvec,nar+1)) + vecfi lct recargsvec.(tyi) in + let j = (match depPvec.(tyi) with + | Some (_,Rel j) -> j + | _ -> assert false) in + let deftyi = + it_lambda_name + (lambda_create + (appvect (mind,(Array.append (rel_vect decf nparams) + (rel_vect 0 nar))), + mkMutCaseA (ci_of_mind mind) + (Rel (decf-nrec+j+1)) (Rel 1) branches)) + (lift_context nrec lnames) + in + let typtyi = + it_prod_name + (prod_create + (appvect (mind,(Array.append (rel_vect dect nparams) + (rel_vect 0 nar))), + (if dep then + appvect (Rel (dect-nrec+j+1), rel_vect 0 (nar+1)) + else + appvect (Rel (dect-nrec+j+1),rel_vect 1 nar)))) + lnames + in + mrec (i+nctyi) (nar::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 makefixdef = + put_DLAMSV + (tabulate_list (fun _ -> Name(id_of_string "F")) nrec) fixdef + in + let fixspec = Array.append fixtyi [|makefixdef|] in + DOPN(Fix(fixn,p),fixspec) + in + mrec 0 [] [] [] + in + let rec make_branch i = function + | (mispeci,dep,_)::rest -> + let tyi = mispeci.tyi in + let (lc,lct) = mis_type_mconstructs mispeci in + let rec onerec j = + if j = Array.length lc then + make_branch (i+j) rest + else + let co = lc.(j) in + let t = lct.(j) in + let recarg = recargsvec.(tyi).(j) in + let vargs = rel_vect (nrec+i+j) nparams in + let p_0 = + type_rec_branch dep (sigma,vargs,depPvec,i+j) co t recarg + in + DOP2(Lambda,p_0,DLAM(Name (id_of_string "f"),onerec (j+1))) + in onerec 0 + | [] -> + makefix i listdepkind + in + let rec put_arity i = function + | ((mispeci,dep,kinds)::rest) -> + let mind = DOPN(MutInd (mispeci.sp,mispeci.tyi),mispeci.args) in + let arity = mis_arity mispeci in + let ar = + hnf_prod_appvect sigma "put_arity" arity (rel_vect i nparams) + in + let typP = + if dep then + make_arity_dep (DOP0(Sort kinds)) ar + (appvect (mind,rel_vect i nparams)) + else + make_arity_nodep (DOP0(Sort kinds)) ar + in + DOP2(Lambda,typP,DLAM(Name(id_of_string "P"),put_arity (i+1) rest)) + | [] -> + make_branch 0 listdepkind + in + let (mispeci,dep,kind) = List.nth listdepkind p in + if is_recursive (List.map (fun (mispec,_,_) -> mispec.tyi) listdepkind) + recargsvec.(mispeci.tyi) then + it_lambda_name (put_arity 0 listdepkind) lnamespar + else + mis_make_case_com (Some dep) sigma mispeci kind + in + tabulate_vect make_one_rec nrec + +let make_indrec sigma listdepkind mind = + let ity = minductype_spec sigma mind in + let (sp,tyi,largs) = destMutInd ity in + let mispec = mind_specif_of_mind ity in + mis_make_indrec sigma listdepkind mispec + +let change_sort_arity sort = + let rec drec = function + | (DOP2(Cast,c,t)) -> drec c + | (DOP2(Prod,t,DLAM(n,c))) -> DOP2(Prod,t,DLAM(n,drec c)) + | (DOP0(Sort(_))) -> DOP0(Sort(sort)) + | _ -> assert false + in + drec + +let instanciate_indrec_scheme sort = + let rec drec npar elim = + let (n,t,c) = destLambda (strip_outer_cast elim) in + if npar = 0 then + mkLambda n (change_sort_arity sort t) c + else + mkLambda n t (drec (npar-1) c) + in + drec + +let check_arities listdepkind = + List.iter + (function (mispeci,dep,kinds) -> + let mip = mispeci.mip in + if dep then + let kd = mis_kd mispeci in + if List.exists (sort_cmp CONV_X kinds) kd then + () + else + errorlabstrm "Bad Induction" + [<'sTR "Dependent induction for type "; + print_id mip.mINDTYPENAME; + 'sTR " and sort "; pTERM (DOP0(Sort kinds)); + 'sTR "is not allowed">] + else + let kn = mis_kn mispeci in + if List.exists (sort_cmp CONV_X kinds) kn then + () + else + errorlabstrm "Bad Induction" + [<'sTR "Non dependent induction for type "; + print_id mip.mINDTYPENAME; + 'sTR " and sort "; pTERM (DOP0(Sort kinds)); + 'sTR "is not allowed">]) + listdepkind + +let build_indrec sigma = function + | ((mind,dep,s)::lrecspec) -> + let redind = minductype_spec sigma mind in + let (sp,tyi,_) = destMutInd redind in + let listdepkind = + (mind_specif_of_mind redind, dep,s):: + (List.map (function (mind',dep',s') -> + let redind' = minductype_spec sigma mind' in + let (sp',_,_) = destMutInd redind' in + if sp=sp' then + (mind_specif_of_mind redind',dep',s') + else + error + "Induction schemes concern mutually inductive types") + lrecspec) + in + let _ = check_arities listdepkind in + make_indrec sigma listdepkind mind + | _ -> assert false + + +(* In order to interpret the Match operator *) + +let type_mutind_rec env sigma ct pt p c = + let (mI,largs as mind) = find_minductype sigma ct in + let mispec = mind_specif_of_mind mI in + let recargs = mis_recarg mispec in + if is_recursive [mispec.tyi] recargs then + let dep = find_case_dep_mis env sigma mispec (c,p) mind pt in + let ntypes = mis_nconstr mispec + and tyi = mispec.tyi + and nparams = mis_nparams mispec in + let depPvec = Array.create ntypes (None : (bool * constr) option) in + let _ = Array.set depPvec mispec.tyi (Some(dep,p)) in + let (pargs,realargs) = chop_list nparams largs in + let vargs = Array.of_list pargs in + let (constrvec,typeconstrvec) = mis_type_mconstructs mispec in + let lft = map3_vect (type_rec_branch dep (sigma,vargs,depPvec,0)) + constrvec typeconstrvec recargs in + (mI, lft, + if dep then applist(p,realargs@[c]) + else applist(p,realargs) ) + else + type_case_branches env sigma ct pt p c + +let is_mutind sigma ct = + try let _ = find_minductype sigma ct in true with Induc -> false + +let type_rec_branches recursive sigma env ct pt p c = + match whd_betadeltaiota_stack sigma ct [] with + | (DOPN(MutInd _,_),_) -> + if recursive then + type_mutind_rec env sigma ct pt p c + else + type_case_branches env sigma ct pt p c + | _ -> error"Elimination on a non-inductive type 1" + +(* Awful special reduction function which skips abstraction on Xtra in order to + be safe for Program ... *) + +let stacklamxtra recfun = + let rec lamrec sigma p_0 p_1 = match p_0,p_1 with + | (stack, (DOP2(Lambda,DOP1(XTRA("COMMENT",[]),_),DLAM(_,c)) as t)) -> + recfun stack (substl sigma t) + | ((h::t), (DOP2(Lambda,_,DLAM(_,c)))) -> lamrec (h::sigma) t c + | (stack, t) -> recfun stack (substl sigma t) + in + lamrec + +let rec whrec x stack = + match x with + | DOP2(Lambda,DOP1(XTRA("COMMENT",[]),c),DLAM(name,t)) -> + let t' = applist (whrec t (List.map (lift 1) stack)) in + DOP2(Lambda,DOP1(XTRA("COMMENT",[]),c),DLAM(name,t')),[] + | DOP2(Lambda,c1,DLAM(name,c2)) -> + (match stack with + | [] -> (DOP2(Lambda,c1,DLAM(name,whd_betaxtra c2)),[]) + | a1::rest -> stacklamxtra (fun l x -> whrec x l) [a1] rest c2) + | DOPN(AppL,cl) -> whrec (hd_vect cl) (app_tl_vect cl stack) + | DOP2(Cast,c,_) -> whrec c stack + | x -> x,stack + +and whd_betaxtra x = applist(whrec x []) + +let transform_rec env sigma cl (ct,pt) = + let (mI,largs as mind) = find_minductype sigma ct in + let p = cl.(0) + and c = cl.(1) + and lf = Array.sub cl 2 ((Array.length cl) - 2) in + let mispec = mind_specif_of_mind mI in + let recargs = mis_recarg mispec in + let expn = Array.length recargs in + if Array.length lf <> expn then error_number_branches CCI env c ct expn; + if is_recursive [mispec.tyi] recargs then + let dep = find_case_dep_mis env sigma mispec (c,p) mind pt in + let ntypes = mis_nconstr mispec + and tyi = mispec.tyi + and nparams = mis_nparams mispec in + let depFvec = Array.create ntypes (None : (bool * constr) option) in + let _ = Array.set depFvec mispec.tyi (Some(dep,Rel 1)) in + let (pargs,realargs) = chop_list nparams largs in + let vargs = Array.of_list pargs in + let (_,typeconstrvec) = mis_type_mconstructs mispec in + (* build now the fixpoint *) + let realar = + hnf_prod_appvect sigma "make_branch" (mis_arity mispec) vargs in + let lnames,_ = splay_prod sigma realar in + let nar = List.length lnames in + let branches = + map3_vect + (fun f t reca -> + whd_betaxtra + (rec_branch_arg + (sigma,(Array.map (lift (nar+2)) vargs),depFvec,nar+1) + f t reca)) + (Array.map (lift (nar+2)) lf) typeconstrvec recargs + in + let deffix = + it_lambda_name + (lambda_create + (appvect (mI,Array.append (Array.map (lift (nar+1)) vargs) + (rel_vect 0 nar)), + mkMutCaseA (ci_of_mind mI) + (lift (nar+2) p) (Rel 1) branches)) + (lift_context 1 lnames) + in + if noccurn 1 deffix then + whd_beta (applist (pop deffix,realargs@[c])) + else + let typPfix = + it_prod_name + (prod_create (appvect (mI,(Array.append + (Array.map (lift nar) vargs) + (rel_vect 0 nar))), + (if dep then applist (whd_beta_stack (lift (nar+1) p) + (rel_list 0 (nar+1))) + else applist (whd_beta_stack (lift (nar+1) p) + (rel_list 1 nar))))) + lnames + in + let fix = DOPN(Fix([|nar|],0), + [|typPfix; + DLAMV(Name(id_of_string "F"),[|deffix|])|]) + in + applist (fix,realargs@[c]) + else + mkMutCaseA (ci_of_mind mI) p c lf + +(*** Building ML like case expressions without types ***) + +let concl_n sigma = + let rec decrec m c = if m = 0 then c else + match whd_betadeltaiota sigma c with + | DOP2(Prod,_,DLAM(n,c_0)) -> decrec (m-1) c_0 + | _ -> failwith "Typing.concl_n" + in + decrec + +let count_rec_arg j = + let rec crec i = function + | [] -> i + | (Mrec k::l) -> crec (if k=j then (i+1) else i) l + | (_::l) -> crec i l + in + crec 0 + +let norec_branch_scheme sigma typc = + let rec crec typc = match whd_betadeltaiota sigma typc with + | DOP2(Prod,c,DLAM(name,t)) -> DOP2(Prod,c,DLAM(name,crec t)) + | _ -> mkExistential + in + crec typc + +let rec_branch_scheme sigma j typc recargs = + let rec crec (typc,recargs) = + match whd_betadeltaiota sigma typc, recargs with + | (DOP2(Prod,c,DLAM(name,t)),(ra::reca)) -> + DOP2(Prod,c, + match ra with + | Mrec k -> + if k=j then + DLAM(name,mkArrow mkExistential + (crec (lift 1 t,reca))) + else + DLAM(name,crec (t,reca)) + | _ -> DLAM(name,crec (t,reca))) + | (_,_) -> mkExistential + in + crec (typc,recargs) + +let branch_scheme sigma isrec i mind = + let typc = type_inst_construct sigma i mind in + if isrec then + let (mI,_) = find_mrectype sigma mind in + let (_,j,_) = destMutInd mI in + let mispec = mind_specif_of_mind mI in + let recarg = (mis_recarg mispec).(i-1) in + rec_branch_scheme sigma j typc recarg + else + norec_branch_scheme sigma typc + +(* if arity of mispec is (p_bar:P_bar)(a_bar:A_bar)s where p_bar are the + * K parameters. Then then build_notdep builds the predicate + * [a_bar:A'_bar](lift k pred) + * where A'_bar = A_bar[p_bar <- globargs] *) + +let build_notdep_pred mispec nparams globargs pred = + let arity = mis_arity mispec in + let lamarity = to_lambda nparams arity in + let inst_arity = whd_beta (appvect (lamarity,Array.of_list globargs)) in + let k = nb_prod inst_arity in + let env,_,npredlist = push_and_liftl k [] inst_arity [insert_lifted pred] in + let npred = (match npredlist with [npred] -> npred + | _ -> anomaly "push_and_lift should not behave this way") in + let _,finalpred,_ = lam_and_popl k env (extract_lifted npred) [] + in + finalpred + +let pred_case_ml_fail sigma isrec ct (i,ft) = + try + let (mI,largs) = find_mrectype sigma ct in + let (_,j,_) = destMutInd mI in + let mispec = mind_specif_of_mind mI in + let nparams = mis_nparams mispec in + let (globargs,la) = chop_list nparams largs in + let pred = + let recargs = (mis_recarg mispec) in + assert (Array.length recargs <> 0); + let recargi = recargs.(i-1) in + let nbrec = if isrec then count_rec_arg j recargi else 0 in + let nb_arg = List.length (recargs.(i-1)) + nbrec in + let pred = concl_n sigma nb_arg ft in + if noccur_bet 1 nb_arg pred then + lift (-nb_arg) pred + else + failwith "Dependent" + in + if la = [] then + pred + else (* we try with [_:T1]..[_:Tn](lift n pred) *) + build_notdep_pred mispec nparams globargs pred + with Induc -> + failwith "Inductive" + +let pred_case_ml env sigma isrec (c,ct) lf (i,ft) = + try + pred_case_ml_fail sigma isrec ct (i,ft) + with Failure mes -> + error_ml_case mes env c ct lf.(i-1) ft + +(* similar to pred_case_ml but does not expect the list lf of braches *) +let pred_case_ml_onebranch env sigma isrec (c,ct) (i,f,ft) = + try + pred_case_ml_fail sigma isrec ct (i,ft) + with Failure mes -> + error_ml_case mes env c ct f ft + +let make_case_ml isrec pred c ci lf = + if isrec then + DOPN(XTRA("REC",[]),Array.append [|pred;c|] lf) + else + mkMutCaseA ci pred c lf diff --git a/library/indrec.mli b/library/indrec.mli new file mode 100644 index 000000000..408c97e39 --- /dev/null +++ b/library/indrec.mli @@ -0,0 +1,45 @@ + +(* $Id$ *) + +(*i*) +open Names +open Term +open Inductive +open Environ +open Evd +(*i*) + +(* Eliminations. *) + +val make_case_dep : 'c evar_map -> constr -> sorts -> constr +val make_case_nodep : 'c evar_map -> constr -> sorts -> constr +val make_case_gen : 'c evar_map -> constr -> sorts -> constr + +val make_indrec : 'c evar_map -> (mind_specif * bool * sorts) list + -> constr -> constr array + +val mis_make_indrec : 'c evar_map -> (mind_specif * bool * sorts) list + -> mind_specif -> constr array + +val instanciate_indrec_scheme : sorts -> int -> constr -> constr + +val build_indrec : 'c evar_map -> (constr * bool * sorts) list -> constr array + +val type_rec_branches : bool -> unsafe_env -> 'c evar_map -> constr + -> constr -> constr -> constr -> constr * constr array * constr + +val transform_rec : unsafe_env -> 'c evar_map -> (constr array) + -> (constr * constr) -> constr + +val is_mutind : 'c evar_map -> constr -> bool + +val branch_scheme : 'c evar_map -> bool -> int -> constr -> constr + +val pred_case_ml : unsafe_env -> 'c evar_map -> bool -> (constr * constr) + -> constr array -> (int*constr) ->constr + +val pred_case_ml_onebranch : unsafe_env ->'c evar_map -> bool -> + constr * constr ->int * constr * constr -> constr + +val make_case_ml : + bool -> constr -> constr -> case_info -> constr array -> constr |