diff options
Diffstat (limited to 'kernel/indtypes.ml')
-rw-r--r-- | kernel/indtypes.ml | 383 |
1 files changed, 232 insertions, 151 deletions
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index f9c2a7b0..de97268b 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -6,13 +6,12 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Errors +open CErrors open Util open Names open Univ open Term open Vars -open Context open Declarations open Declareops open Inductive @@ -21,6 +20,17 @@ open Reduction open Typeops open Entries open Pp +open Context.Rel.Declaration + +(* Terminology: +paramdecls (ou paramsctxt?) +args = params + realargs (called vargs when an array, largs when a list) +params = recparams + nonrecparams +nonrecargs = nonrecparams + realargs +env_ar = initial env + declaration of inductive types +env_ar_par = env_ar + declaration of parameters +nmr = ongoing computation of recursive parameters +*) (* Tell if indices (aka real arguments) contribute to size of inductive type *) (* If yes, this is compatible with the univalent model *) @@ -30,12 +40,17 @@ let indices_matter = ref false let enforce_indices_matter () = indices_matter := true let is_indices_matter () = !indices_matter -(* Same as noccur_between but may perform reductions. - Could be refined more... *) +(* [weaker_noccur_between env n nvars t] (defined above), checks that + no de Bruijn indices between [n] and [n+nvars] occur in [t]. If + some such occurrences are found, then reduction is performed + (lazily for efficiency purposes) in order to determine whether + these occurrences are occurrences in the normal form. If the + occurrences are eliminated a witness reduct [Some t'] of [t] is + returned otherwise [None] is returned. *) let weaker_noccur_between env x nvars t = if noccur_between x nvars t then Some t else - let t' = whd_betadeltaiota env t in + let t' = whd_all env t in if noccur_between x nvars t' then Some t' else None @@ -114,11 +129,11 @@ let is_unit constrsinfos = let infos_and_sort env t = let rec aux env t max = - let t = whd_betadeltaiota env t in + let t = whd_all env t in match kind_of_term t with | Prod (name,c1,c2) -> let varj = infer_type env c1 in - let env1 = Environ.push_rel (name,None,varj.utj_val) env in + let env1 = Environ.push_rel (LocalAssum (name,varj.utj_val)) env in let max = Universe.sup max (univ_of_sort varj.utj_type) in aux env1 c2 max | _ when is_constructor_head t -> max @@ -164,12 +179,14 @@ let infer_constructor_packet env_ar_par params lc = (* If indices matter *) let cumulate_arity_large_levels env sign = fst (List.fold_right - (fun (_,b,t as d) (lev,env) -> - if Option.is_empty b then + (fun d (lev,env) -> + match d with + | LocalAssum (_,t) -> let tj = infer_type env t in let u = univ_of_sort tj.utj_type in (Universe.sup u lev, push_rel d env) - else lev, push_rel d env) + | LocalDef _ -> + lev, push_rel d env) sign (Universe.type0m,env)) let is_impredicative env u = @@ -179,15 +196,16 @@ let is_impredicative env u = polymorphism. The elements x_k is None if the k-th parameter (starting from the most recent and ignoring let-definitions) is not contributing or is Some u_k if its level is u_k and is contributing. *) -let param_ccls params = - let fold acc = function (_, None, p) -> +let param_ccls paramsctxt = + let fold acc = function + | (LocalAssum (_, p)) -> (let c = strip_prod_assum p in match kind_of_term c with | Sort (Type u) -> Univ.Universe.level u | _ -> None) :: acc - | _ -> acc + | LocalDef _ -> acc in - List.fold_left fold [] params + List.fold_left fold [] paramsctxt (* Type-check an inductive definition. Does not check positivity conditions. *) @@ -203,7 +221,7 @@ let typecheck_inductive env mie = mind_check_names mie; (* Params are typed-checked here *) let env' = push_context mie.mind_entry_universes env in - let (env_params, params) = infer_local_decls env' mie.mind_entry_params in + let (env_params,paramsctxt) = infer_local_decls env' mie.mind_entry_params in (* We first type arity of each inductive definition *) (* This allows building the environment of arities and to share *) (* the set of constraints *) @@ -242,26 +260,26 @@ let typecheck_inductive env mie = later, after the validation of the inductive definition, full_arity is used as argument or subject to cast, an upper universe will be generated *) - let full_arity = it_mkProd_or_LetIn arity params in + let full_arity = it_mkProd_or_LetIn arity paramsctxt in let id = ind.mind_entry_typename in let env_ar' = - push_rel (Name id, None, full_arity) env_ar in + push_rel (LocalAssum (Name id, full_arity)) env_ar in (* (add_constraints cst2 env_ar) in *) - (env_ar', (id,full_arity,sign @ params,expltype,deflev,inflev)::l)) + (env_ar', (id,full_arity,sign @ paramsctxt,expltype,deflev,inflev)::l)) (env',[]) mie.mind_entry_inds in let arity_list = List.rev rev_arity_list in (* builds the typing context "Gamma, I1:A1, ... In:An, params" *) - let env_ar_par = push_rel_context params env_arities in + let env_ar_par = push_rel_context paramsctxt env_arities in (* Now, we type the constructors (without params) *) let inds = List.fold_right2 (fun ind arity_data inds -> let (lc',cstrs_univ) = - infer_constructor_packet env_ar_par params ind.mind_entry_lc in + infer_constructor_packet env_ar_par paramsctxt ind.mind_entry_lc in let consnames = ind.mind_entry_consnames in let ind' = (arity_data,consnames,lc',cstrs_univ) in ind'::inds) @@ -284,7 +302,7 @@ let typecheck_inductive env mie = let full_polymorphic () = let defu = Term.univ_of_sort def_level in let is_natural = - type_in_type env || (check_leq (universes env') infu defu) + type_in_type env || (UGraph.check_leq (universes env') infu defu) in let _ = (** Impredicative sort, always allow *) @@ -310,14 +328,14 @@ let typecheck_inductive env mie = (* conclusions of the parameters *) (* We enforce [u >= lev] in case [lev] has a strict upper *) (* constraints over [u] *) - let b = type_in_type env || check_leq (universes env') infu u in + let b = type_in_type env || UGraph.check_leq (universes env') infu u in if not b then anomaly ~label:"check_inductive" (Pp.str"Incorrect universe " ++ Universe.pr u ++ Pp.str " declared for inductive type, inferred level is " ++ Universe.pr clev) else - TemplateArity (param_ccls params, infu) + TemplateArity (param_ccls paramsctxt, infu) | _ (* Not an explicit occurrence of Type *) -> full_polymorphic () in @@ -327,7 +345,7 @@ let typecheck_inductive env mie = in (id,cn,lc,(sign,arity))) inds - in (env_arities, env_ar_par, params, inds) + in (env_arities, env_ar_par, paramsctxt, inds) (************************************************************************) (************************************************************************) @@ -336,7 +354,7 @@ let typecheck_inductive env mie = type ill_formed_ind = | LocalNonPos of int | LocalNotEnoughArgs of int - | LocalNotConstructor of rel_context * constr list + | LocalNotConstructor of Context.Rel.t * int | LocalNonPar of int * int * int exception IllFormedInd of ill_formed_ind @@ -347,22 +365,22 @@ exception IllFormedInd of ill_formed_ind let mind_extract_params = decompose_prod_n_assum -let explain_ind_err id ntyp env nbpar c err = - let (lpar,c') = mind_extract_params nbpar c in +let explain_ind_err id ntyp env nparamsctxt c err = + let (lparams,c') = mind_extract_params nparamsctxt c in match err with | LocalNonPos kt -> - raise (InductiveError (NonPos (env,c',mkRel (kt+nbpar)))) + raise (InductiveError (NonPos (env,c',mkRel (kt+nparamsctxt)))) | LocalNotEnoughArgs kt -> raise (InductiveError - (NotEnoughArgs (env,c',mkRel (kt+nbpar)))) - | LocalNotConstructor (paramsctxt,args)-> - let nparams = rel_context_nhyps paramsctxt in + (NotEnoughArgs (env,c',mkRel (kt+nparamsctxt)))) + | LocalNotConstructor (paramsctxt,nargs)-> + let nparams = Context.Rel.nhyps paramsctxt in raise (InductiveError - (NotConstructor (env,id,c',mkRel (ntyp+nbpar),nparams, - List.length args - nparams))) + (NotConstructor (env,id,c',mkRel (ntyp+nparamsctxt), + nparams,nargs))) | LocalNonPar (n,i,l) -> raise (InductiveError - (NonPar (env,c',n,mkRel i, mkRel (l+nbpar)))) + (NonPar (env,c',n,mkRel i,mkRel (l+nparamsctxt)))) let failwith_non_pos n ntypes c = for k = n to n + ntypes - 1 do @@ -378,43 +396,50 @@ let failwith_non_pos_list n ntypes l = anomaly ~label:"failwith_non_pos_list" (Pp.str "some k in [n;n+ntypes-1] should occur") (* Check the inductive type is called with the expected parameters *) -let check_correct_par (env,n,ntypes,_) hyps l largs = - let nparams = rel_context_nhyps hyps in - let largs = Array.of_list largs in - if Array.length largs < nparams then - raise (IllFormedInd (LocalNotEnoughArgs l)); - let (lpar,largs') = Array.chop nparams largs in - let nhyps = List.length hyps in - let rec check k index = function +(* [n] is the index of the last inductive type in [env] *) +let check_correct_par (env,n,ntypes,_) paramdecls ind_index args = + let nparams = Context.Rel.nhyps paramdecls in + let args = Array.of_list args in + if Array.length args < nparams then + raise (IllFormedInd (LocalNotEnoughArgs ind_index)); + let (params,realargs) = Array.chop nparams args in + let nparamdecls = List.length paramdecls in + let rec check param_index paramdecl_index = function | [] -> () - | (_,Some _,_)::hyps -> check k (index+1) hyps - | _::hyps -> - match kind_of_term (whd_betadeltaiota env lpar.(k)) with - | Rel w when Int.equal w index -> check (k-1) (index+1) hyps - | _ -> raise (IllFormedInd (LocalNonPar (k+1, index-n+nhyps+1, l))) - in check (nparams-1) (n-nhyps) hyps; - if not (Array.for_all (noccur_between n ntypes) largs') then - failwith_non_pos_vect n ntypes largs' - -(* Computes the maximum number of recursive parameters : - the first parameters which are constant in recursive arguments - n is the current depth, nmr is the maximum number of possible - recursive parameters *) - -let compute_rec_par (env,n,_,_) hyps nmr largs = + | LocalDef _ :: paramdecls -> + check param_index (paramdecl_index+1) paramdecls + | _::paramdecls -> + match kind_of_term (whd_all env params.(param_index)) with + | Rel w when Int.equal w paramdecl_index -> + check (param_index-1) (paramdecl_index+1) paramdecls + | _ -> + let paramdecl_index_in_env = paramdecl_index-n+nparamdecls+1 in + let err = + LocalNonPar (param_index+1, paramdecl_index_in_env, ind_index) in + raise (IllFormedInd err) + in check (nparams-1) (n-nparamdecls) paramdecls; + if not (Array.for_all (noccur_between n ntypes) realargs) then + failwith_non_pos_vect n ntypes realargs + +(* Computes the maximum number of recursive parameters: + the first parameters which are constant in recursive arguments + [n] is the current depth, [nmr] is the maximum number of possible + recursive parameters *) + +let compute_rec_par (env,n,_,_) paramsctxt nmr largs = if Int.equal nmr 0 then 0 else -(* start from 0, hyps will be in reverse order *) +(* start from 0, params will be in reverse order *) let (lpar,_) = List.chop nmr largs in let rec find k index = function ([],_) -> nmr - | (_,[]) -> assert false (* |hyps|>=nmr *) - | (lp,(_,Some _,_)::hyps) -> find k (index-1) (lp,hyps) - | (p::lp,_::hyps) -> - ( match kind_of_term (whd_betadeltaiota env p) with - | Rel w when Int.equal w index -> find (k+1) (index-1) (lp,hyps) + | (_,[]) -> assert false (* |paramsctxt|>=nmr *) + | (lp, LocalDef _ :: paramsctxt) -> find k (index-1) (lp,paramsctxt) + | (p::lp,_::paramsctxt) -> + ( match kind_of_term (whd_all env p) with + | Rel w when Int.equal w index -> find (k+1) (index-1) (lp,paramsctxt) | _ -> k) - in find 0 (n-1) (lpar,List.rev hyps) + in find 0 (n-1) (lpar,List.rev paramsctxt) (* [env] is the typing environment [n] is the dB of the last inductive type @@ -423,15 +448,15 @@ if Int.equal nmr 0 then 0 else [lra] is the list of recursive tree of each variable *) let ienv_push_var (env, n, ntypes, lra) (x,a,ra) = - (push_rel (x,None,a) env, n+1, ntypes, (Norec,ra)::lra) + (push_rel (LocalAssum (x,a)) env, n+1, ntypes, (Norec,ra)::lra) -let ienv_push_inductive (env, n, ntypes, ra_env) ((mi,u),lpar) = +let ienv_push_inductive (env, n, ntypes, ra_env) ((mi,u),lrecparams) = let auxntyp = 1 in let specif = (lookup_mind_specif env mi, u) in let ty = type_of_inductive env specif in let env' = - push_rel (Anonymous,None, - hnf_prod_applist env ty lpar) env in + let decl = LocalAssum (Anonymous, hnf_prod_applist env ty lrecparams) in + push_rel decl env in let ra_env' = (Imbr mi,(Rtree.mk_rec_calls 1).(0)) :: List.map (fun (r,t) -> (r,Rtree.lift 1 t)) ra_env in @@ -441,7 +466,7 @@ let ienv_push_inductive (env, n, ntypes, ra_env) ((mi,u),lpar) = let rec ienv_decompose_prod (env,_,_,_ as ienv) n c = if Int.equal n 0 then (ienv,c) else - let c' = whd_betadeltaiota env c in + let c' = whd_all env c in match kind_of_term c' with Prod(na,a,b) -> let ienv' = ienv_push_var ienv (na,a,mk_norec) in @@ -451,75 +476,115 @@ let rec ienv_decompose_prod (env,_,_,_ as ienv) n c = let array_min nmr a = if Int.equal nmr 0 then 0 else Array.fold_left (fun k (nmri,_) -> min k nmri) nmr a -(* The recursive function that checks positivity and builds the list - of recursive arguments *) -let check_positivity_one (env,_,ntypes,_ as ienv) hyps (_,i as ind) nargs lcnames indlc = - let lparams = rel_context_length hyps in - let nmr = rel_context_nhyps hyps in - (* Checking the (strict) positivity of a constructor argument type [c] *) +(** [check_positivity_one ienv paramsctxt (mind,i) nnonrecargs lcnames indlc] + checks the positivity of the [i]-th member of the mutually + inductive definition [mind]. It returns an [Rtree.t] which + represents the position of the recursive calls of inductive in [i] + for use by the guard condition (terms at these positions are + considered sub-terms) as well as the number of of non-uniform + arguments (used to generate induction schemes, so a priori less + relevant to the kernel). + + If [chkpos] is [false] then positivity is assumed, and + [check_positivity_one] computes the subterms occurrences in a + best-effort fashion. *) +let check_positivity_one ~chkpos recursive (env,_,ntypes,_ as ienv) paramsctxt (_,i as ind) nnonrecargs lcnames indlc = + let nparamsctxt = Context.Rel.length paramsctxt in + let nmr = Context.Rel.nhyps paramsctxt in + (** Positivity of one argument [c] of a constructor (i.e. the + constructor [cn] has a type of the shape [… -> c … -> P], where, + more generally, the arrows may be dependent). *) let rec check_pos (env, n, ntypes, ra_env as ienv) nmr c = - let x,largs = decompose_app (whd_betadeltaiota env c) in + let x,largs = decompose_app (whd_all env c) in match kind_of_term x with | Prod (na,b,d) -> let () = assert (List.is_empty largs) in + (** If one of the inductives of the mutually inductive + block occurs in the left-hand side of a product, then + such an occurrence is a non-strictly-positive + recursive call. Occurrences in the right-hand side of + the product must be strictly positive.*) (match weaker_noccur_between env n ntypes b with - None -> failwith_non_pos_list n ntypes [b] + | None when chkpos -> + failwith_non_pos_list n ntypes [b] + | None -> + check_pos (ienv_push_var ienv (na, b, mk_norec)) nmr d | Some b -> - check_pos (ienv_push_var ienv (na, b, mk_norec)) nmr d) + check_pos (ienv_push_var ienv (na, b, mk_norec)) nmr d) | Rel k -> (try let (ra,rarg) = List.nth ra_env (k-1) in - let largs = List.map (whd_betadeltaiota env) largs in + let largs = List.map (whd_all env) largs in let nmr1 = (match ra with - Mrec _ -> compute_rec_par ienv hyps nmr largs + Mrec _ -> compute_rec_par ienv paramsctxt nmr largs | _ -> nmr) in - if not (List.for_all (noccur_between n ntypes) largs) + (** The case where one of the inductives of the mutually + inductive block occurs as an argument of another is not + known to be safe. So Coq rejects it. *) + if chkpos && + not (List.for_all (noccur_between n ntypes) largs) then failwith_non_pos_list n ntypes largs else (nmr1,rarg) with Failure _ | Invalid_argument _ -> (nmr,mk_norec)) | Ind ind_kn -> - (* If the inductive type being defined appears in a - parameter, then we have a nested indtype *) + (** If one of the inductives of the mutually inductive + block being defined appears in a parameter, then we + have a nested inductive type. The positivity is then + discharged to the [check_positive_nested] function. *) if List.for_all (noccur_between n ntypes) largs then (nmr,mk_norec) else check_positive_nested ienv nmr (ind_kn, largs) | err -> - if noccur_between n ntypes x && - List.for_all (noccur_between n ntypes) largs + (** If an inductive of the mutually inductive block + appears in any other way, then the positivy check gives + up. *) + if not chkpos || + (noccur_between n ntypes x && + List.for_all (noccur_between n ntypes) largs) then (nmr,mk_norec) else failwith_non_pos_list n ntypes (x::largs) + (** [check_positive_nested] handles the case of nested inductive + calls, that is, when an inductive types from the mutually + inductive block is called as an argument of an inductive types + (for the moment, this inductive type must be a previously + defined types, not one of the types of the mutually inductive + block being defined). *) (* accesses to the environment are not factorised, but is it worth? *) and check_positive_nested (env,n,ntypes,ra_env as ienv) nmr ((mi,u), largs) = let (mib,mip) = lookup_mind_specif env mi in - let auxnpar = mib.mind_nparams_rec in - let nonrecpar = mib.mind_nparams - auxnpar in - let (lpar,auxlargs) = - try List.chop auxnpar largs + let auxnrecpar = mib.mind_nparams_rec in + let auxnnonrecpar = mib.mind_nparams - auxnrecpar in + let (auxrecparams,auxnonrecargs) = + try List.chop auxnrecpar largs with Failure _ -> raise (IllFormedInd (LocalNonPos n)) in - (* If the inductive appears in the args (non params) then the - definition is not positive. *) - if not (List.for_all (noccur_between n ntypes) auxlargs) then - failwith_non_pos_list n ntypes auxlargs; - (* We do not deal with imbricated mutual inductive types *) + (** Inductives of the inductive block being defined are only + allowed to appear nested in the parameters of another inductive + type. Not in the proper indices. *) + if chkpos && not (List.for_all (noccur_between n ntypes) auxnonrecargs) then + failwith_non_pos_list n ntypes auxnonrecargs; + (* Nested mutual inductive types are not supported *) let auxntyp = mib.mind_ntypes in if not (Int.equal auxntyp 1) then raise (IllFormedInd (LocalNonPos n)); (* The nested inductive type with parameters removed *) - let auxlcvect = abstract_mind_lc auxntyp auxnpar mip.mind_nf_lc in + let auxlcvect = abstract_mind_lc auxntyp auxnrecpar mip.mind_nf_lc in (* Extends the environment with a variable corresponding to the inductive def *) - let (env',_,_,_ as ienv') = ienv_push_inductive ienv ((mi,u),lpar) in + let (env',_,_,_ as ienv') = ienv_push_inductive ienv ((mi,u),auxrecparams) in (* Parameters expressed in env' *) - let lpar' = List.map (lift auxntyp) lpar in + let auxrecparams' = List.map (lift auxntyp) auxrecparams in let irecargs_nmr = - (* fails if the inductive type occurs non positively *) - (* with recursive parameters substituted *) + (** Checks that the "nesting" inductive type is covariant in + the relevant parameters. In other words, that the + (nested) parameters which are instantiated with + inductives of the mutually inductive block occur + positively in the types of the nested constructors. *) Array.map (function c -> - let c' = hnf_prod_applist env' c lpar' in + let c' = hnf_prod_applist env' c auxrecparams' in (* skip non-recursive parameters *) - let (ienv',c') = ienv_decompose_prod ienv' nonrecpar c' in + let (ienv',c') = ienv_decompose_prod ienv' auxnnonrecpar c' in check_constructors ienv' false nmr c') auxlcvect in @@ -528,17 +593,23 @@ let check_positivity_one (env,_,ntypes,_ as ienv) hyps (_,i as ind) nargs lcname in (nmr',(Rtree.mk_rec [|mk_paths (Imbr mi) irecargs|]).(0)) - (* check the inductive types occur positively in the products of C, if - check_head=true, also check the head corresponds to a constructor of - the ith type *) - + (** [check_constructors ienv check_head nmr c] checks the positivity + condition in the type [c] of a constructor (i.e. that recursive + calls to the inductives of the mutually inductive definition + appear strictly positively in each of the arguments of the + constructor, see also [check_pos]). If [check_head] is [true], + then the type of the fully applied constructor (the "head" of + the type [c]) is checked to be the right (properly applied) + inductive type. *) and check_constructors ienv check_head nmr c = let rec check_constr_rec (env,n,ntypes,ra_env as ienv) nmr lrec c = - let x,largs = decompose_app (whd_betadeltaiota env c) in + let x,largs = decompose_app (whd_all env c) in match kind_of_term x with | Prod (na,b,d) -> let () = assert (List.is_empty largs) in + if not recursive && not (noccur_between n ntypes b) then + raise (InductiveError BadEntry); let nmr',recarg = check_pos ienv nmr b in let ienv' = ienv_push_var ienv (na,b,mk_norec) in check_constr_rec ienv' nmr' (recarg::lrec) d @@ -547,11 +618,12 @@ let check_positivity_one (env,_,ntypes,_ as ienv) hyps (_,i as ind) nargs lcname if check_head then begin match hd with | Rel j when Int.equal j (n + ntypes - i - 1) -> - check_correct_par ienv hyps (ntypes - i) largs - | _ -> raise (IllFormedInd (LocalNotConstructor(hyps,largs))) + check_correct_par ienv paramsctxt (ntypes - i) largs + | _ -> raise (IllFormedInd (LocalNotConstructor(paramsctxt,nnonrecargs))) end else - if not (List.for_all (noccur_between n ntypes) largs) + if chkpos && + not (List.for_all (noccur_between n ntypes) largs) then failwith_non_pos_list n ntypes largs in (nmr, List.rev lrec) @@ -560,29 +632,36 @@ let check_positivity_one (env,_,ntypes,_ as ienv) hyps (_,i as ind) nargs lcname let irecargs_nmr = Array.map2 (fun id c -> - let _,rawc = mind_extract_params lparams c in + let _,rawc = mind_extract_params nparamsctxt c in try check_constructors ienv true nmr rawc with IllFormedInd err -> - explain_ind_err id (ntypes-i) env lparams c err) + explain_ind_err id (ntypes-i) env nparamsctxt c err) (Array.of_list lcnames) indlc in let irecargs = Array.map snd irecargs_nmr and nmr' = array_min nmr irecargs_nmr in (nmr', mk_paths (Mrec ind) irecargs) -let check_positivity kn env_ar params inds = +(** [check_positivity ~chkpos kn env_ar paramsctxt inds] checks that the mutually + inductive block [inds] is strictly positive. + + If [chkpos] is [false] then positivity is assumed, and + [check_positivity_one] computes the subterms occurrences in a + best-effort fashion. *) +let check_positivity ~chkpos kn env_ar_par paramsctxt finite inds = let ntypes = Array.length inds in + let recursive = finite != Decl_kinds.BiFinite in let rc = Array.mapi (fun j t -> (Mrec (kn,j),t)) (Rtree.mk_rec_calls ntypes) in - let lra_ind = Array.rev_to_list rc in - let lparams = rel_context_length params in - let nmr = rel_context_nhyps params in + let ra_env_ar = Array.rev_to_list rc in + let nparamsctxt = Context.Rel.length paramsctxt in + let nmr = Context.Rel.nhyps paramsctxt in let check_one i (_,lcnames,lc,(sign,_)) = - let ra_env = - List.init lparams (fun _ -> (Norec,mk_norec)) @ lra_ind in - let ienv = (env_ar, 1+lparams, ntypes, ra_env) in - let nargs = rel_context_nhyps sign - nmr in - check_positivity_one ienv params (kn,i) nargs lcnames lc + let ra_env_ar_par = + List.init nparamsctxt (fun _ -> (Norec,mk_norec)) @ ra_env_ar in + let ienv = (env_ar_par, 1+nparamsctxt, ntypes, ra_env_ar_par) in + let nnonrecargs = Context.Rel.nhyps sign - nmr in + check_positivity_one ~chkpos recursive ienv paramsctxt (kn,i) nnonrecargs lcnames lc in let irecargs_nmr = Array.mapi check_one inds in let irecargs = Array.map snd irecargs_nmr @@ -639,6 +718,7 @@ let used_section_variables env inds = keep_hyps env ids let rel_vect n m = Array.init m (fun i -> mkRel(n+m-i)) +let rel_list n m = Array.to_list (rel_vect n m) exception UndefinableExpansion @@ -653,23 +733,21 @@ let compute_projections ((kn, _ as ind), u as indu) n x nparamargs params that typechecking projections requires just a substitution and not matching with a parameter context. *) let indty, paramsletsubst = - let _, _, subst, inst = - List.fold_right - (fun (na, b, t) (i, j, subst, inst) -> - match b with - | None -> (i-1, j-1, mkRel i :: subst, mkRel j :: inst) - | Some b -> (i, j-1, substl subst b :: subst, inst)) - paramslet (nparamargs, List.length paramslet, [], []) - in + (* [ty] = [Ind inst] is typed in context [params] *) + let inst = Context.Rel.to_extended_vect 0 paramslet in + let ty = mkApp (mkIndU indu, inst) in + (* [Ind inst] is typed in context [params-wo-let] *) + let inst' = rel_list 0 nparamargs in + (* {params-wo-let |- subst:params] *) + let subst = subst_of_rel_context_instance paramslet inst' in + (* {params-wo-let, x:Ind inst' |- subst':(params,x:Ind inst)] *) let subst = (* For the record parameter: *) - mkRel 1 :: List.map (lift 1) subst - in - let ty = mkApp (mkIndU indu, CArray.rev_of_list inst) in + mkRel 1 :: List.map (lift 1) subst in ty, subst in let ci = let print_info = - { ind_tags = []; cstr_tags = [|rel_context_tags ctx|]; style = LetStyle } in + { ind_tags = []; cstr_tags = [|Context.Rel.to_tags ctx|]; style = LetStyle } in { ci_ind = ind; ci_npar = nparamargs; ci_cstr_ndecls = mind_consnrealdecls; @@ -687,9 +765,9 @@ let compute_projections ((kn, _ as ind), u as indu) n x nparamargs params let body = mkCase (ci, p, mkRel 1, [|lift 1 branch|]) in it_mkLambda_or_LetIn (mkLambda (x,indty,body)) params in - let projections (na, b, t) (i, j, kns, pbs, subst, letsubst) = - match b with - | Some c -> + let projections decl (i, j, kns, pbs, subst, letsubst) = + match decl with + | LocalDef (na,c,t) -> (* From [params, field1,..,fieldj |- c(params,field1,..,fieldj)] to [params, x:I, field1,..,fieldj |- c(params,field1,..,fieldj)] *) let c = liftn 1 j c in @@ -707,7 +785,7 @@ let compute_projections ((kn, _ as ind), u as indu) n x nparamargs params to [params-wo-let, x:I |- subst:(params, x:I, field1,..,fieldj+1)] *) let letsubst = c2 :: letsubst in (i, j+1, kns, pbs, subst, letsubst) - | None -> + | LocalAssum (na,t) -> match na with | Name id -> let kn = Constant.make1 (KerName.make mp dp (Label.of_id id)) in @@ -738,14 +816,14 @@ let compute_projections ((kn, _ as ind), u as indu) n x nparamargs params Array.of_list (List.rev kns), Array.of_list (List.rev pbs) -let build_inductive env p prv ctx env_ar params kn isrecord isfinite inds nmr recargs = +let build_inductive env p prv ctx env_ar paramsctxt kn isrecord isfinite inds nmr recargs = let ntypes = Array.length inds in (* Compute the set of used section variables *) let hyps = used_section_variables env inds in - let nparamargs = rel_context_nhyps params in - let nparamdecls = rel_context_length params in + let nparamargs = Context.Rel.nhyps paramsctxt in + let nparamsctxt = Context.Rel.length paramsctxt in let subst, ctx = Univ.abstract_universes p ctx in - let params = Vars.subst_univs_level_context subst params in + let paramsctxt = Vars.subst_univs_level_context subst paramsctxt in let env_ar = let ctx = Environ.rel_context env_ar in let ctx' = Vars.subst_univs_level_context subst ctx in @@ -758,10 +836,10 @@ let build_inductive env p prv ctx env_ar params kn isrecord isfinite inds nmr re let splayed_lc = Array.map (dest_prod_assum env_ar) lc in let nf_lc = Array.map (fun (d,b) -> it_mkProd_or_LetIn b d) splayed_lc in let consnrealdecls = - Array.map (fun (d,_) -> rel_context_length d - rel_context_length params) + Array.map (fun (d,_) -> Context.Rel.length d - nparamsctxt) splayed_lc in let consnrealargs = - Array.map (fun (d,_) -> rel_context_nhyps d - rel_context_nhyps params) + Array.map (fun (d,_) -> Context.Rel.nhyps d - nparamargs) splayed_lc in (* Elimination sorts *) let arkind,kelim = @@ -794,8 +872,8 @@ let build_inductive env p prv ctx env_ar params kn isrecord isfinite inds nmr re { mind_typename = id; mind_arity = arkind; mind_arity_ctxt = Vars.subst_univs_level_context subst ar_sign; - mind_nrealargs = rel_context_nhyps ar_sign - nparamargs; - mind_nrealdecls = rel_context_length ar_sign - nparamdecls; + mind_nrealargs = Context.Rel.nhyps ar_sign - nparamargs; + mind_nrealdecls = Context.Rel.length ar_sign - nparamsctxt; mind_kelim = kelim; mind_consnames = Array.of_list cnames; mind_consnrealdecls = consnrealdecls; @@ -808,10 +886,11 @@ let build_inductive env p prv ctx env_ar params kn isrecord isfinite inds nmr re mind_reloc_tbl = rtbl; } in let packets = Array.map2 build_one_packet inds recargs in - let pkt = packets.(0) in + let pkt = packets.(0) in let isrecord = match isrecord with - | Some (Some rid) when pkt.mind_kelim == all_sorts && Array.length pkt.mind_consnames == 1 + | Some (Some rid) when pkt.mind_kelim == all_sorts + && Array.length pkt.mind_consnames == 1 && pkt.mind_consnrealargs.(0) > 0 -> (** The elimination criterion ensures that all projections can be defined. *) let u = @@ -824,7 +903,7 @@ let build_inductive env p prv ctx env_ar params kn isrecord isfinite inds nmr re (try let fields, paramslet = List.chop pkt.mind_consnrealdecls.(0) rctx in let kns, projs = - compute_projections indsp pkt.mind_typename rid nparamargs params + compute_projections indsp pkt.mind_typename rid nparamargs paramsctxt pkt.mind_consnrealdecls pkt.mind_consnrealargs paramslet fields in Some (Some (rid, kns, projs)) with UndefinableExpansion -> Some None) @@ -838,11 +917,12 @@ let build_inductive env p prv ctx env_ar params kn isrecord isfinite inds nmr re mind_hyps = hyps; mind_nparams = nparamargs; mind_nparams_rec = nmr; - mind_params_ctxt = params; + mind_params_ctxt = paramsctxt; mind_packets = packets; mind_polymorphic = p; mind_universes = ctx; mind_private = prv; + mind_typing_flags = Environ.typing_flags env; } (************************************************************************) @@ -850,11 +930,12 @@ let build_inductive env p prv ctx env_ar params kn isrecord isfinite inds nmr re let check_inductive env kn mie = (* First type-check the inductive definition *) - let (env_ar, env_ar_par, params, inds) = typecheck_inductive env mie in + let (env_ar, env_ar_par, paramsctxt, inds) = typecheck_inductive env mie in (* Then check positivity conditions *) - let (nmr,recargs) = check_positivity kn env_ar_par params inds in + let chkpos = (Environ.typing_flags env).check_guarded in + let (nmr,recargs) = check_positivity ~chkpos kn env_ar_par paramsctxt mie.mind_entry_finite inds in (* Build the inductive packets *) build_inductive env mie.mind_entry_polymorphic mie.mind_entry_private mie.mind_entry_universes - env_ar params kn mie.mind_entry_record mie.mind_entry_finite + env_ar paramsctxt kn mie.mind_entry_record mie.mind_entry_finite inds nmr recargs |