diff options
Diffstat (limited to 'pretyping/indrec.ml')
| -rw-r--r-- | pretyping/indrec.ml | 583 |
1 files changed, 583 insertions, 0 deletions
diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml new file mode 100644 index 000000000..3c5e17b09 --- /dev/null +++ b/pretyping/indrec.ml @@ -0,0 +1,583 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) + +(* $Id$ *) + +open Pp +open Util +open Names +open Nameops +open Term +open Termops +open Declarations +open Inductive +open Inductiveops +open Instantiate +open Environ +open Reductionops +open Typeops +open Type_errors +open Indtypes (* pour les erreurs *) +open Declare +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 nparams = mip.mind_nparams 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 = (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 = (ind,extended_rel_list nbprod lnamespar) in + let lnamesar,_ = get_arity env indf in + let ci = make_default_case_info env ind in + it_mkLambda_or_LetIn_name env' + (lambda_create env' + (build_dependent_inductive env indf, + mkCase (ci, + mkRel (nbprod+nbargsprod), + mkRel 1, + rel_vect nbargsprod k))) + lnamesar + 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 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_chop nparams largs in + let base = applist (lift i pk,realargs) in + if depK then + mkApp (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,[] + | 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 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 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 (n,None,t) + (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 + mkApp (c, [|co|]) + else c +(* + let c', largs = whd_stack c in + match kind_of_term c' with + | Prod (n,t,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 env + (n,t, + process_constr (push_rel (n,None,t) env) (i+1) c_0 rest + (mkApp (lift 1 co, [|mkRel 1|]))) + | Some(dep',p) -> + let nP = lift (i+1+decP) p 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 (n,None,t) + (push_rel (Anonymous,None,t_0) env)) + (i+2) (lift 1 c_0) rest + (mkApp (lift 2 co, [|mkRel 2|]))))) + | LetIn (n,b,t,c_0) -> + mkLetIn (n,b,t, + process_constr + (push_rel (n,Some b,t) env) + (i+1) c_0 recargs (lift 1 co)) + + | Ind ((_,tyi),_) -> + let nP = match depPvect.(tyi) with + | Some(_,p) -> lift (i+decP) p + | _ -> assert false in + let (_,realargs) = list_chop nparams largs in + let base = applist (nP,realargs) in + if dep then mkApp (base, [|co|]) else base + | _ -> assert false +*) + 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_chop 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 recarg with + | Param i -> None + | 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 arg = process_pos env nF (lift 1 (body_of_type t)) in + lambda_name env + (n,t,process_constr (push_rel d 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_listrec) 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 P1..P_nrec f1..f_nbconstruct *) + let args = extended_rel_list (nrec+nbconstruct) lnamespar in + let indf = (indi,args) in + let lnames,_ = get_arity env indf in + + let nar = mipi.mind_nrealargs 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 args = extended_rel_list (decf+1) lnamespar in + let constrs = get_constructors env (indi,args) in + let branches = + array_map3 + (make_rec_branch_arg env sigma (nparams,depPvec,nar+1)) + vecfi constrs recargsvec.(tyi) in + let j = (match depPvec.(tyi) with + | Some (_,c) when isRel c -> destRel c + | _ -> assert false) in + let args = extended_rel_list (nrec+nbconstruct) lnamespar in + let indf = (indi,args) in + let deftyi = + it_mkLambda_or_LetIn_name env + (lambda_create env + (build_dependent_inductive env + (lift_inductive_family nrec indf), + mkCase (make_default_case_info env indi, + mkRel (dect+j+1), mkRel 1, branches))) + (Termops.lift_rel_context nrec lnames) + in + let ind = build_dependent_inductive env indf in + let typtyi = + 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 = 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 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 + 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 + +(**********************************************************************) +(* 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 the Match operator *) + +(* TODO: check that we can drop universe constraints ? *) +let type_mutind_rec env sigma (IndType (indf,realargs) as indt) pj c = + let p = pj.uj_val in + let (ind,params) = dest_ind_family indf in + let tyi = snd ind in + let (mib,mip) = lookup_mind_specif env ind in + if mis_is_recursive_subset [tyi] mip then + let (dep,_) = find_case_dep_nparams env (c,pj) indf in + let init_depPvec i = if i = tyi then Some(dep,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 recargs = mip.mind_listrec in + let lft = array_map2 (type_rec_branch dep env sigma (params,depPvec,0) tyi) + constructors recargs in + (lft, + if dep then applist(p,realargs@[c]) + else applist(p,realargs) ) + else + let (p,ra,_) = type_case_branches env (ind,params@realargs) pj c in + (p,ra) + +let type_rec_branches recursive env sigma indt pj c = + if recursive then + type_mutind_rec env sigma indt pj c + else + let IndType((ind,params),rargs) = indt in + let (p,ra,_) = type_case_branches env (ind,params@rargs) pj c in + (p,ra) + + +(*s Eliminations. *) + +let eliminations = + [ (InProp,"_ind") ; (InSet,"_rec") ; (InType,"_rect") ] + +let elimination_suffix = function + | InProp -> "_ind" + | InSet -> "_rec" + | InType -> "_rect" + +let make_elimination_ident id s = add_suffix id (elimination_suffix s) + +let declare_one_elimination ind = + let (mib,mip) = Global.lookup_inductive ind in + let mindstr = string_of_id mip.mind_typename in + let declare na c = + let _ = Declare.declare_constant (id_of_string na) + (ConstantEntry + { const_entry_body = c; + const_entry_type = None; + const_entry_opaque = false }, + NeverDischarge) in + Options.if_verbose pPNL [< 'sTR na; 'sTR " is defined" >] + in + let env = Global.env () in + let sigma = Evd.empty in + let elim_scheme = build_indrec env sigma ind in + let npars = mip.mind_nparams in + let make_elim s = instanciate_indrec_scheme s npars elim_scheme in + let kelim = mip.mind_kelim in + List.iter + (fun (sort,suff) -> + if List.mem sort kelim then + declare (mindstr^suff) (make_elim (new_sort_in_family sort))) + eliminations + +let declare_eliminations sp = + let mib = Global.lookup_mind sp in +(* + let ids = ids_of_named_context mib.mind_hyps in + if not (list_subset ids (ids_of_named_context (Global.named_context ()))) then error ("Declarations of elimination scheme outside the section "^ + "of the inductive definition is not implemented"); +*) + if mib.mind_finite then + for i = 0 to Array.length mib.mind_packets - 1 do + declare_one_elimination (sp,i) + done + +(* Look up function for the default elimination constant *) + +let lookup_eliminator ind_sp s = + let env = Global.env() in + let path = sp_of_global env (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 construct_reference env 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 (new_sort_in_family s) ; + 'sTR " is probably not allowed" >] |