diff options
Diffstat (limited to 'kernel/indtypes.ml')
| -rw-r--r-- | kernel/indtypes.ml | 130 |
1 files changed, 85 insertions, 45 deletions
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index 49e858315..a8625009c 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -12,7 +12,6 @@ open Names open Univ open Term open Vars -open Context open Declarations open Declareops open Inductive @@ -30,8 +29,13 @@ 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 @@ -284,7 +288,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,7 +314,7 @@ 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 " ++ @@ -336,7 +340,7 @@ let typecheck_inductive env mie = type ill_formed_ind = | LocalNonPos of int | LocalNotEnoughArgs of int - | LocalNotConstructor of rel_context * int + | LocalNotConstructor of Context.Rel.t * int | LocalNonPar of int * int * int exception IllFormedInd of ill_formed_ind @@ -356,7 +360,7 @@ let explain_ind_err id ntyp env nbpar c err = raise (InductiveError (NotEnoughArgs (env,c',mkRel (kt+nbpar)))) | LocalNotConstructor (paramsctxt,nargs)-> - let nparams = rel_context_nhyps paramsctxt in + let nparams = Context.Rel.nhyps paramsctxt in raise (InductiveError (NotConstructor (env,id,c',mkRel (ntyp+nbpar),nparams,nargs))) | LocalNonPar (n,i,l) -> @@ -378,7 +382,7 @@ let failwith_non_pos_list n ntypes l = (* 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 nparams = Context.Rel.nhyps hyps in let largs = Array.of_list largs in if Array.length largs < nparams then raise (IllFormedInd (LocalNotEnoughArgs l)); @@ -450,17 +454,30 @@ 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 *) +(** [check_positivity_one ienv hyps (mind,i) nargs 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). *) 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] *) + let lparams = Context.Rel.length hyps in + let nmr = Context.Rel.nhyps hyps 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 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] | Some b -> @@ -473,21 +490,35 @@ let check_positivity_one (env,_,ntypes,_ as ienv) hyps (_,i as ind) nargs lcname Mrec _ -> compute_rec_par ienv hyps nmr largs | _ -> nmr) in + (** 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 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 an inductive of the mutually inductive block + appears in any other way, then the positivy check gives + up. *) if 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 @@ -496,12 +527,13 @@ let check_positivity_one (env,_,ntypes,_ as ienv) hyps (_,i as ind) nargs lcname let (lpar,auxlargs) = try List.chop auxnpar largs with Failure _ -> raise (IllFormedInd (LocalNonPos n)) in - (* If the inductive appears in the args (non params) then the - definition is not positive. *) + (** 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 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 *) + (* 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 *) @@ -512,8 +544,11 @@ let check_positivity_one (env,_,ntypes,_ as ienv) hyps (_,i as ind) nargs lcname (* Parameters expressed in env' *) let lpar' = List.map (lift auxntyp) lpar 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 @@ -527,10 +562,14 @@ 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 @@ -570,17 +609,19 @@ let check_positivity_one (env,_,ntypes,_ as ienv) hyps (_,i as ind) nargs lcname and nmr' = array_min nmr irecargs_nmr in (nmr', mk_paths (Mrec ind) irecargs) +(** [check_positivity kn env_ar params] checks that the mutually + inductive block [inds] is strictly positive. *) let check_positivity kn env_ar params inds = let ntypes = Array.length inds 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 lparams = Context.Rel.length params in + let nmr = Context.Rel.nhyps params 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 + let nargs = Context.Rel.nhyps sign - nmr in check_positivity_one ienv params (kn,i) nargs lcnames lc in let irecargs_nmr = Array.mapi check_one inds in @@ -638,6 +679,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 @@ -652,23 +694,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; @@ -741,8 +781,8 @@ let build_inductive env p prv ctx env_ar params kn isrecord isfinite inds nmr re 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 params in + let nparamdecls = Context.Rel.length params in let subst, ctx = Univ.abstract_universes p ctx in let params = Vars.subst_univs_level_context subst params in let env_ar = @@ -757,10 +797,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 - Context.Rel.length params) 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 - Context.Rel.nhyps params) splayed_lc in (* Elimination sorts *) let arkind,kelim = @@ -793,8 +833,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 - nparamdecls; mind_kelim = kelim; mind_consnames = Array.of_list cnames; mind_consnrealdecls = consnrealdecls; |