diff options
Diffstat (limited to 'pretyping/indrec.ml')
| -rw-r--r-- | pretyping/indrec.ml | 553 |
1 files changed, 553 insertions, 0 deletions
diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml new file mode 100644 index 00000000..0b9283ae --- /dev/null +++ b/pretyping/indrec.ml @@ -0,0 +1,553 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* $Id: indrec.ml,v 1.20.2.3 2004/07/16 19:30:44 herbelin Exp $ *) + +open Pp +open Util +open Names +open Libnames +open Nameops +open Term +open Termops +open Declarations +open Entries +open Inductive +open Inductiveops +open Instantiate +open Environ +open Reductionops +open Typeops +open Type_errors +open Indtypes (* pour les erreurs *) +open Safe_typing +open Nametab + +let make_prod_dep dep env = if dep then prod_name env else mkProd +let mkLambda_string s t c = mkLambda (Name (id_of_string s), t, c) + +(*******************************************) +(* Building curryfied elimination *) +(*******************************************) + +(**********************************************************************) +(* 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 *) + +let mis_make_case_com depopt env sigma (ind,mib,mip) kind = + let lnamespar = mip.mind_params_ctxt in + let dep = match depopt with + | None -> mip.mind_sort <> (Prop Null) + | Some d -> d + in + if not (List.exists ((=) kind) mip.mind_kelim) then + raise + (InductiveError + (NotAllowedCaseAnalysis + (dep,(new_sort_in_family kind),ind))); + + let nbargsprod = mip.mind_nrealargs + 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) *) + let env' = push_rel_context lnamespar env in + + 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 = + if k = Array.length mip.mind_consnames then + let nbprod = k+1 in + let indf = make_ind_family(ind,extended_rel_list nbprod lnamespar) in + let lnamesar,_ = get_arity env indf in + let ci = make_default_case_info env RegularStyle ind in + let depind = build_dependent_inductive env indf in + let deparsign = (Anonymous,None,depind)::lnamesar in + let p = + it_mkLambda_or_LetIn_name env' + (appvect + (mkRel ((if dep then nbargsprod else mip.mind_nrealargs) + nbprod), + if dep then extended_rel_vect 0 deparsign + else extended_rel_vect 0 lnamesar)) + (if dep then deparsign else lnamesar) in + it_mkLambda_or_LetIn_name env' + (mkCase (ci, lift nbargsprod p, + mkRel 1, + rel_vect nbargsprod k)) + deparsign + else + let cs = lift_constructor (k+1) constrs.(k) in + let t = build_branch_type env dep (mkRel (k+1)) cs in + mkLambda_string "f" t + (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 + (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 *) + +(* + * 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 + * the case operation + * 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 make_prod = make_prod_dep dep in + let nparams = List.length vargs in + let process_pos env depK pk = + let rec prec env i sign 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 + make_prod env (n,t,prec (push_rel d env) (i+1) (d::sign) 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::sign) c) + | Ind (_,_) -> + let realargs = list_skipn nparams largs in + let base = applist (lift i pk,realargs) in + if depK then + Reduction.beta_appvect + base [|applist (mkRel (i+1),extended_rel_list 0 sign)|] + else + base + | _ -> 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 + | Prod (n,t,c_0) -> + let (optionpos,rest) = + match recargs with + | [] -> None,[] + | ra::rest -> + (match dest_recarg ra with + | Mrec j when is_rec -> (depPvect.(j),rest) + | Imbr _ -> + Options.if_verbose warning "Ignoring recursive call"; + (None,rest) + | _ -> (None, rest)) + 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) -> + 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 + make_prod_dep (dep or dep') env + (n,t, + mkArrow t_0 + (process_constr + (push_rel (Anonymous,None,t_0) env') + (i+2) (lift 1 c_0) rest (nhyps-1) (i::li)))) + | LetIn (n,b,t,c_0) -> + mkLetIn (n,b,t, + process_constr + (push_rel (n,Some b,t) env) + (i+1) c_0 recargs (nhyps-1) li) + | _ -> assert false + else + if dep then + let realargs = List.map (fun k -> mkRel (i-k)) (List.rev li) in + let params = List.map (lift i) vargs in + let co = applist (mkConstruct cs.cs_cstr,params@realargs) in + Reduction.beta_appvect c [|co|] + else c + in + let nhyps = List.length cs.cs_args in + 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 (nparams,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) + | 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 _ -> + let realargs = list_skipn nparams largs + and arg = appvect (mkRel (i+1),extended_rel_vect 0 hyps) in + applist(lift i fk,realargs@[arg]) + | _ -> assert false + in + prec env 0 [] + 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 + | Norec -> None + | Imbr _ -> None + | Mrec i -> fvect.(i) + in + (match optionpos with + | None -> + lambda_name env + (n,t,process_constr (push_rel d env) (i+1) + (whd_beta (applist (lift 1 f, [(mkRel 1)]))) + (cprest,rest)) + | 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 + (n,t,process_constr env' (i+1) + (whd_beta (applist (lift 1 f, [(mkRel 1); arg]))) + (cprest,rest))) + | (n,Some c,t as d)::cprest, rest -> + mkLetIn + (n,c,t, + process_constr (push_rel d env) (i+1) (lift 1 f) + (cprest,rest)) + | [],[] -> f + | _,[] | [],_ -> anomaly "process_constr" + + in + process_constr env 0 f (List.rev cstr.cs_args, recargs) + +(* Main function *) +let mis_make_indrec env sigma listdepkind (ind,mib,mip) = + let nparams = mip.mind_nparams in + let lnamespar = mip.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 + | [] -> () + | (indi,mibi,mipi,dep,_)::rest -> + (Array.set depPvec (snd indi) (Some(dep,mkRel k)); + assign (k-1) rest) + in + assign nrec listdepkind in + let recargsvec = + Array.map (fun mip -> mip.mind_recargs) mib.mind_packets in + let make_one_rec p = + let makefix nbconstruct = + let rec mrec i ln ltyp ldef = function + | (indi,mibi,mipi,dep,_)::rest -> + 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) lnamespar in + let indf = make_ind_family(indi,args) in + let lnames,_ = get_arity env indf in + + let nar = mipi.mind_nrealargs in + let dect = nar+nrec+nbconstruct in + + let branches = + (* 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+1) lnamespar in + let indf' = make_ind_family(indi,args') in + let constrs = get_constructors env indf' in + let vecfi = rel_vect (dect+1-i-nctyi) nctyi in + array_map3 + (make_rec_branch_arg env sigma (nparams,depPvec,nar+1)) + vecfi constrs (dest_subterms recargsvec.(tyi)) in + let j = (match depPvec.(tyi) with + | Some (_,c) when isRel c -> destRel c + | _ -> assert false) in + let deftyi = + let ci = make_default_case_info env RegularStyle indi in + let indf' = lift_inductive_family nrec indf in + let depind = build_dependent_inductive env indf' in + let lnames' = Termops.lift_rel_context nrec lnames in + let p = + let arsign = + if dep then (Anonymous,None,depind)::lnames' else lnames' in + it_mkLambda_or_LetIn_name env + (appvect + (mkRel ((if dep then 1 else 0) + dect + j), + extended_rel_vect 0 arsign)) arsign + in + it_mkLambda_or_LetIn_name env + (lambda_create env + (depind,mkCase (ci, lift (nar+1) p, mkRel 1, branches))) + lnames' + in + let typtyi = + let ind = build_dependent_inductive env indf in + it_mkProd_or_LetIn_name env + (prod_create env + (ind, + (if dep then + let ext_lnames = (Anonymous,None,ind)::lnames in + let args = extended_rel_list 0 ext_lnames in + applist (mkRel (nbconstruct+nar+j+1), args) + else + let args = extended_rel_list 1 lnames in + applist (mkRel (nbconstruct+nar+j+1), args)))) + 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 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 + | (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 recarg = (dest_subterms recargsvec.(tyi)).(j) in + let vargs = extended_rel_list (nrec+i+j) lnamespar in + let indf = (indi, vargs) in + let cs = get_constructor (indi,mibi,mipi,vargs) (j+1) in + let p_0 = + type_rec_branch + true dep env sigma (vargs,depPvec,i+j) tyi cs recarg + 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 indf = make_ind_family (indi,extended_rel_list i lnamespar) 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 + in + let (indi,mibi,mipi,dep,kind) = List.nth listdepkind p in + let env' = push_rel_context lnamespar env in + if mis_is_recursive_subset + (List.map (fun (indi,_,_,_,_) -> snd indi) listdepkind) + mipi.mind_recargs + then + it_mkLambda_or_LetIn_name env (put_arity env' 0 listdepkind) lnamespar + else + mis_make_case_com (Some dep) env sigma (indi,mibi,mipi) kind + in + 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 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 + + +(**********************************************************************) +(* [instanciate_indrec_scheme s rec] replace the sort of the scheme + [rec] by [s] *) + +let change_sort_arity sort = + let rec drec a = match kind_of_term a with + | Cast (c,t) -> drec c + | Prod (n,t,c) -> mkProd (n, t, drec c) + | Sort _ -> mkSort sort + | _ -> assert false + in + drec + +(* [npar] is the number of expected arguments (then excluding letin's) *) +let instanciate_indrec_scheme sort = + let rec drec npar elim = + match kind_of_term elim with + | Lambda (n,t,c) -> + if npar = 0 then + mkLambda (n, change_sort_arity sort t, c) + else + mkLambda (n, t, drec (npar-1) c) + | LetIn (n,b,t,c) -> mkLetIn (n,b,t,drec npar c) + | _ -> anomaly "instanciate_indrec_scheme: wrong elimination type" + in + drec + +(* Change the sort in the type of an inductive definition, builds the + corresponding eta-expanded term *) +let instanciate_type_indrec_scheme sort npars term = + let rec drec np elim = + match kind_of_term elim with + | 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 + 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 "instanciate_type_indrec_scheme: wrong elimination type" + in + drec npars + +(**********************************************************************) +(* Interface to build complex Scheme *) + +let check_arities listdepkind = + List.iter + (function (indi,mibi,mipi,dep,kind) -> + let id = mipi.mind_typename in + let kelim = mipi.mind_kelim in + if not (List.exists ((=) kind) kelim) then + raise + (InductiveError (BadInduction (dep, id, new_sort_in_family kind)))) + listdepkind + +let build_mutual_indrec env sigma = function + | (mind,mib,mip,dep,s)::lrecspec -> + let (sp,tyi) = mind in + let listdepkind = + (mind,mib,mip, dep,s):: + (List.map + (function (mind',mibi',mipi',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 (InductiveError NotMutualInScheme)) + lrecspec) + in + let _ = check_arities listdepkind in + mis_make_indrec env sigma listdepkind (mind,mib,mip) + | _ -> anomaly "build_indrec expects a non empty list of inductive types" + +let build_indrec env sigma ind = + let (mib,mip) = lookup_mind_specif env ind in + let kind = family_of_sort mip.mind_sort in + let dep = kind <> InProp in + List.hd (mis_make_indrec env sigma [(ind,mib,mip,dep,kind)] (ind,mib,mip)) + +(**********************************************************************) +(* 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 vargs = Array.of_list params 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) +*) + +(*s Eliminations. *) + +let elimination_suffix = function + | InProp -> "_ind" + | InSet -> "_rec" + | InType -> "_rect" + +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 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_kn mp dp (label_of_id id)) in + try + let _ = sp_of_global ref in + constr_of_reference ref + 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_reference (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 id ++ spc () ++ str "on sort " ++ + spc () ++ print_sort_family s ++ + str " 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_reference (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 () ++ print_sort_family s ++ + str " is probably not allowed") +*) |