summaryrefslogtreecommitdiff
path: root/kernel/indtypes.ml
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/indtypes.ml')
-rw-r--r--kernel/indtypes.ml383
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
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-06 10:16:50 +0000