From e759333a8b5c11247c4cc134fdde8c1bd85a6e17 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Fri, 11 Sep 2015 18:07:39 +0200 Subject: Universes: enforce Set <= i for all Type occurrences. --- kernel/indtypes.ml | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) (limited to 'kernel/indtypes.ml') diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index 8c89abe940..9c065101a3 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -286,7 +286,10 @@ let typecheck_inductive env mie = let defu = Term.univ_of_sort def_level in let is_natural = type_in_type env || (check_leq (universes env') infu defu && - not (is_type0m_univ defu && not is_unit)) + not (is_type0m_univ defu && not is_unit) + (* (~ is_type0m_univ defu \/ is_unit) (\* infu <= defu && not prop or unital *\) *) + + ) in let _ = (** Impredicative sort, always allow *) -- cgit v1.2.3 From 84add29c036735ceacde73ea98a9a5a454a5e3a0 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 6 Oct 2015 19:09:10 +0200 Subject: Splitting kernel universe code in two modules. 1. The Univ module now only cares about definitions about universes. 2. The UGraph module contains the algorithm responsible for aciclicity. --- kernel/indtypes.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'kernel/indtypes.ml') diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index 5a234d09b9..155ad79879 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -290,7 +290,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 && not (is_type0m_univ defu && not is_unit) (* (~ is_type0m_univ defu \/ is_unit) (\* infu <= defu && not prop or unital *\) *) @@ -320,7 +320,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 " ++ -- cgit v1.2.3 From 5b67ba8e1bbd92d4ef7e2adab13bd05e7b55bfd7 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Wed, 14 Oct 2015 15:57:19 +0200 Subject: Univs: inductives, remove unneeded test --- kernel/indtypes.ml | 6 +----- 1 file changed, 1 insertion(+), 5 deletions(-) (limited to 'kernel/indtypes.ml') diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index 9c065101a3..5d7a0bbf00 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -285,11 +285,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 && - not (is_type0m_univ defu && not is_unit) - (* (~ is_type0m_univ defu \/ is_unit) (\* infu <= defu && not prop or unital *\) *) - - ) + type_in_type env || (check_leq (universes env') infu defu) in let _ = (** Impredicative sort, always allow *) -- cgit v1.2.3 From 273005ac85e9ae0c23328e243edeadfc8dcaf8bb Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Thu, 22 Oct 2015 22:25:35 +0200 Subject: Fixing a bug in reporting ill-formed inductive. Was introduced in b06d3badb (15 Jul 2015). --- kernel/indtypes.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'kernel/indtypes.ml') diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index 5d7a0bbf00..8b03df64c6 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -390,7 +390,7 @@ let check_correct_par (env,n,ntypes,_) hyps l largs = | _::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, l))) + | _ -> 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' -- cgit v1.2.3 From bde12b7066d7d1f3849d529428b2be3343a27787 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Fri, 6 Nov 2015 17:37:42 +0100 Subject: Fixing a bug in reporting ill-formed constructor. For instance, Inductive a (x:=1) := C : a -> True. was wrongly reporting Error: The type of constructor C is not valid; its conclusion must be "a" applied to its parameter. Also "simplifying" explain_ind_err. --- kernel/indtypes.ml | 14 ++++++++------ 1 file changed, 8 insertions(+), 6 deletions(-) (limited to 'kernel/indtypes.ml') diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index 8b03df64c6..5e899d07be 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -337,7 +337,7 @@ let typecheck_inductive env mie = type ill_formed_ind = | LocalNonPos of int | LocalNotEnoughArgs of int - | LocalNotConstructor + | LocalNotConstructor of rel_context * constr list | LocalNonPar of int * int * int exception IllFormedInd of ill_formed_ind @@ -348,7 +348,7 @@ exception IllFormedInd of ill_formed_ind let mind_extract_params = decompose_prod_n_assum -let explain_ind_err id ntyp env nbpar c nargs err = +let explain_ind_err id ntyp env nbpar c err = let (lpar,c') = mind_extract_params nbpar c in match err with | LocalNonPos kt -> @@ -356,9 +356,11 @@ let explain_ind_err id ntyp env nbpar c nargs err = | LocalNotEnoughArgs kt -> raise (InductiveError (NotEnoughArgs (env,c',mkRel (kt+nbpar)))) - | LocalNotConstructor -> + | LocalNotConstructor (paramsctxt,args)-> + let nparams = rel_context_nhyps paramsctxt in raise (InductiveError - (NotConstructor (env,id,c',mkRel (ntyp+nbpar),nbpar,nargs))) + (NotConstructor (env,id,c',mkRel (ntyp+nbpar),nparams, + List.length args - nparams))) | LocalNonPar (n,i,l) -> raise (InductiveError (NonPar (env,c',n,mkRel i, mkRel (l+nbpar)))) @@ -547,7 +549,7 @@ let check_positivity_one (env,_,ntypes,_ as ienv) hyps (_,i as ind) nargs lcname 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) + | _ -> raise (IllFormedInd (LocalNotConstructor(hyps,largs))) end else if not (List.for_all (noccur_between n ntypes) largs) @@ -563,7 +565,7 @@ let check_positivity_one (env,_,ntypes,_ as ienv) hyps (_,i as ind) nargs lcname try check_constructors ienv true nmr rawc with IllFormedInd err -> - explain_ind_err id (ntypes-i) env lparams c nargs err) + explain_ind_err id (ntypes-i) env lparams c err) (Array.of_list lcnames) indlc in let irecargs = Array.map snd irecargs_nmr -- cgit v1.2.3 From ab1d8792143a05370a1efe3d19469c25b82d7097 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Fri, 6 Nov 2015 16:33:29 +0100 Subject: Dead code from the commit having introduced primitive projections (a4043608). --- kernel/indtypes.ml | 15 +++++++-------- 1 file changed, 7 insertions(+), 8 deletions(-) (limited to 'kernel/indtypes.ml') diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index 5e899d07be..351de9ee88 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -112,18 +112,18 @@ let is_unit constrsinfos = | [] -> (* type without constructors *) true | _ -> false -let infos_and_sort env ctx t = - let rec aux env ctx t max = +let infos_and_sort env t = + let rec aux env t max = let t = whd_betadeltaiota 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 max = Universe.sup max (univ_of_sort varj.utj_type) in - aux env1 ctx c2 max + aux env1 c2 max | _ when is_constructor_head t -> max | _ -> (* don't fail if not positive, it is tested later *) max - in aux env ctx t Universe.type0m + in aux env t Universe.type0m (* Computing the levels of polymorphic inductive types @@ -148,14 +148,14 @@ let infos_and_sort env ctx t = (* This (re)computes informations relevant to extraction and the sort of an arity or type constructor; we do not to recompute universes constraints *) -let infer_constructor_packet env_ar_par ctx params lc = +let infer_constructor_packet env_ar_par params lc = (* type-check the constructors *) let jlc = List.map (infer_type env_ar_par) lc in let jlc = Array.of_list jlc in (* generalize the constructor over the parameters *) let lc'' = Array.map (fun j -> it_mkProd_or_LetIn j.utj_val params) jlc in (* compute the max of the sorts of the products of the constructors types *) - let levels = List.map (infos_and_sort env_ar_par ctx) lc in + let levels = List.map (infos_and_sort env_ar_par) lc in let isunit = is_unit levels in let min = if Array.length jlc > 1 then Universe.type0 else Universe.type0m in let level = List.fold_left (fun max l -> Universe.sup max l) min levels in @@ -261,8 +261,7 @@ let typecheck_inductive env mie = List.fold_right2 (fun ind arity_data inds -> let (lc',cstrs_univ) = - infer_constructor_packet env_ar_par ContextSet.empty - params ind.mind_entry_lc in + infer_constructor_packet env_ar_par params ind.mind_entry_lc in let consnames = ind.mind_entry_consnames in let ind' = (arity_data,consnames,lc',cstrs_univ) in ind'::inds) -- cgit v1.2.3 From c71aa6bd368b801bb17d4da69d1ab1e2bd7cbf39 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sat, 7 Nov 2015 07:20:34 +0100 Subject: Fixing logical bugs in the presence of let-ins in computiong primitive projections. - lift accounting for the record missing in computing the subst from fields to projections of the record - substitution for parameters should not lift the local definitions - typo in building the latter (subst -> letsubst) --- kernel/indtypes.ml | 17 +++++++++-------- 1 file changed, 9 insertions(+), 8 deletions(-) (limited to 'kernel/indtypes.ml') diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index 351de9ee88..f08f0b7bbb 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -654,13 +654,12 @@ let compute_projections ((kn, _ as ind), u as indu) n x nparamargs params matching with a parameter context. *) let indty, paramsletsubst = let subst, inst = - List.fold_right - (fun (na, b, t) (subst, inst) -> + List.fold_right_i + (fun i (na, b, t) (subst, inst) -> match b with - | None -> (mkRel 1 :: List.map (lift 1) subst, - mkRel 1 :: List.map (lift 1) inst) - | Some b -> (substl subst b) :: subst, List.map (lift 1) inst) - paramslet ([], []) + | None -> (mkRel i :: subst, mkRel i :: inst) + | Some b -> (substl subst b) :: subst, inst) + 1 paramslet ([], []) in let subst = (* For the record parameter: *) mkRel 1 :: List.map (lift 1) subst @@ -690,8 +689,10 @@ let compute_projections ((kn, _ as ind), u as indu) n x nparamargs params in let projections (na, b, t) (i, j, kns, pbs, subst, letsubst) = match b with - | Some c -> (i, j+1, kns, pbs, substl subst c :: subst, - substl letsubst c :: subst) + | Some c -> + let c = liftn 1 j c in + (i, j+1, kns, pbs, substl subst c :: subst, + substl letsubst c :: letsubst) | None -> match na with | Name id -> -- cgit v1.2.3 From df04191b48350b76a7650cccc68c9dfc60447787 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sat, 7 Nov 2015 07:33:55 +0100 Subject: Slightly documenting code for building primitive projections. --- kernel/indtypes.ml | 29 +++++++++++++++++++++++++---- 1 file changed, 25 insertions(+), 4 deletions(-) (limited to 'kernel/indtypes.ml') diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index f08f0b7bbb..6c32626ad9 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -690,15 +690,36 @@ let compute_projections ((kn, _ as ind), u as indu) n x nparamargs params let projections (na, b, t) (i, j, kns, pbs, subst, letsubst) = match b with | Some c -> + (* 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 - (i, j+1, kns, pbs, substl subst c :: subst, - substl letsubst c :: letsubst) + (* From [params, x:I, field1,..,fieldj |- c(params,field1,..,fieldj)] + to [params, x:I |- c(params,proj1 x,..,projj x)] *) + let c1 = substl subst c in + (* From [params, x:I |- subst:field1,..,fieldj] + to [params, x:I |- subst:field1,..,fieldj+1] where [subst] + is represented with instance of field1 last *) + let subst = c1 :: subst in + (* From [params, x:I, field1,..,fieldj |- c(params,field1,..,fieldj)] + to [params-wo-let, x:I |- c(params,proj1 x,..,projj x)] *) + let c2 = substl letsubst c in + (* From [params-wo-let, x:I |- subst:(params, x:I, field1,..,fieldj)] + 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 -> match na with | Name id -> let kn = Constant.make1 (KerName.make mp dp (Label.of_id id)) in - let projty = substl letsubst (liftn 1 j t) in - let ty = substl subst (liftn 1 j t) in + (* from [params, field1,..,fieldj |- t(params,field1,..,fieldj)] + to [params, x:I, field1,..,fieldj |- t(params,field1,..,fieldj] *) + let t = liftn 1 j t in + (* from [params, x:I, field1,..,fieldj |- t(params,field1,..,fieldj)] + to [params-wo-let, x:I |- t(params,proj1 x,..,projj x)] *) + let projty = substl letsubst t in + (* from [params, x:I, field1,..,fieldj |- t(field1,..,fieldj)] + to [params, x:I |- t(proj1 x,..,projj x)] *) + let ty = substl subst t in let term = mkProj (Projection.make kn true, mkRel 1) in let fterm = mkProj (Projection.make kn false, mkRel 1) in let compat = compat_body ty (j - 1) in -- cgit v1.2.3 From 6ababf42b3f03926c30cfbd209436ec83a21769e Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Wed, 18 Nov 2015 17:04:12 +0100 Subject: Fixing fix c71aa6b to primitive projections. - Introduced an error: fold was counting in the wrong direction and I did not test it. Sorry. - Substitution from params-with-let to params-without-let was still not correct. Hopefully everything ok now. Eventually, we should use canonical combinators for that: extended_rel_context to built the instance and and a combinator apparently yet to define for building a substitution contracting the let-ins. --- kernel/indtypes.ml | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) (limited to 'kernel/indtypes.ml') diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index 6c32626ad9..a46c33bf03 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -653,13 +653,13 @@ 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_i - (fun i (na, b, t) (subst, inst) -> + let _, _, subst, inst = + List.fold_right + (fun (na, b, t) (i, j, subst, inst) -> match b with - | None -> (mkRel i :: subst, mkRel i :: inst) - | Some b -> (substl subst b) :: subst, inst) - 1 paramslet ([], []) + | 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 let subst = (* For the record parameter: *) mkRel 1 :: List.map (lift 1) subst -- cgit v1.2.3 From e3cefca41b568b1e517313051a111b0416cd2594 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sat, 21 Nov 2015 00:16:34 +0100 Subject: Slight simplification of the code of primitive projection (in relation to c71aa6b and 6ababf) so as to rely on generic functions rather than re-doing the de Bruijn indices cooking locally. --- kernel/indtypes.ml | 12 +++--------- 1 file changed, 3 insertions(+), 9 deletions(-) (limited to 'kernel/indtypes.ml') diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index 21d1e71344..a649ec81e8 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -695,18 +695,12 @@ 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 + let inst = extended_rel_list 0 paramslet in + let subst = subst_of_rel_context_instance paramslet inst in 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 + let ty = mkApp (mkIndU indu, Array.of_list inst) in ty, subst in let ci = -- cgit v1.2.3 From 7fa49442f30dceb7e403fb5dab660002dda7f6e9 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Tue, 15 Dec 2015 15:25:30 +0100 Subject: Fixing e3cefca41b about supposingly simplifying primitive projections typing. Had built the instance for substitution in the wrong context. --- kernel/indtypes.ml | 15 ++++++++++----- 1 file changed, 10 insertions(+), 5 deletions(-) (limited to 'kernel/indtypes.ml') diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index a649ec81e8..11df40caf3 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -681,6 +681,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 @@ -695,12 +696,16 @@ 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 inst = extended_rel_list 0 paramslet in - let subst = subst_of_rel_context_instance paramslet inst in + (* [ty] = [Ind inst] is typed in context [params] *) + let inst = extended_rel_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, Array.of_list inst) in + mkRel 1 :: List.map (lift 1) subst in ty, subst in let ci = -- cgit v1.2.3 From 9d991d36c07efbb6428e277573bd43f6d56788fc Mon Sep 17 00:00:00 2001 From: Matej Kosik Date: Fri, 8 Jan 2016 10:00:21 +0100 Subject: CLEANUP: kernel/context.ml{,i} The structure of the Context module was refined in such a way that: - Types and functions related to rel-context declarations were put into the Context.Rel.Declaration module. - Types and functions related to rel-context were put into the Context.Rel module. - Types and functions related to named-context declarations were put into the Context.Named.Declaration module. - Types and functions related to named-context were put into the Context.Named module. - Types and functions related to named-list-context declarations were put into Context.NamedList.Declaration module. - Types and functions related to named-list-context were put into Context.NamedList module. Some missing comments were added to the *.mli file. The output of ocamldoc was checked whether it looks in a reasonable way. "TODO: cleanup" was removed The order in which are exported functions listed in the *.mli file was changed. (as in a mature modules, this order usually is not random) The order of exported functions in Context.{Rel,Named} modules is now consistent. (as there is no special reason why that order should be different) The order in which are functions defined in the *.ml file is the same as the order in which they are listed in the *.mli file. (as there is no special reason to define them in a different order) The name of the original fold_{rel,named}_context{,_reverse} functions was changed to better indicate what those functions do. (Now they are called Context.{Rel,Named}.fold_{inside,outside}) The original comments originally attached to the fold_{rel,named}_context{,_reverse} did not full make sense so they were updated. Thrown exceptions are now documented. Naming of formal parameters was made more consistent across different functions. Comments of similar functions in different modules are now consistent. Comments from *.mli files were copied to *.ml file. (We need that information in *.mli files because that is were ocamldoc needs it. It is nice to have it also in *.ml files because when we are using Merlin and jump to the definion of the function, we can see the comments also there and do not need to open a different file if we want to see it.) When we invoke ocamldoc, we instruct it to generate UTF-8 HTML instead of (default) ISO-8859-1. (UTF-8 characters are used in our ocamldoc markup) "open Context" was removed from all *.mli and *.ml files. (Originally, it was OK to do that. Now it is not.) An entry to dev/doc/changes.txt file was added that describes how the names of types and functions have changed. --- kernel/indtypes.ml | 33 ++++++++++++++++----------------- 1 file changed, 16 insertions(+), 17 deletions(-) (limited to 'kernel/indtypes.ml') diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index 11df40caf3..da2d213ff1 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 @@ -341,7 +340,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 * constr list | LocalNonPar of int * int * int exception IllFormedInd of ill_formed_ind @@ -361,7 +360,7 @@ let explain_ind_err id ntyp env nbpar c err = raise (InductiveError (NotEnoughArgs (env,c',mkRel (kt+nbpar)))) | LocalNotConstructor (paramsctxt,args)-> - let nparams = rel_context_nhyps paramsctxt in + let nparams = Context.Rel.nhyps paramsctxt in raise (InductiveError (NotConstructor (env,id,c',mkRel (ntyp+nbpar),nparams, List.length args - nparams))) @@ -384,7 +383,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)); @@ -465,8 +464,8 @@ let array_min nmr a = if Int.equal nmr 0 then 0 else 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 + 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). *) @@ -617,13 +616,13 @@ 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 @@ -697,7 +696,7 @@ let compute_projections ((kn, _ as ind), u as indu) n x nparamargs params matching with a parameter context. *) let indty, paramsletsubst = (* [ty] = [Ind inst] is typed in context [params] *) - let inst = extended_rel_vect 0 paramslet in + 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 @@ -710,7 +709,7 @@ let compute_projections ((kn, _ as ind), u as indu) n x nparamargs params 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; @@ -783,8 +782,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 = @@ -799,10 +798,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 = @@ -835,8 +834,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; -- cgit v1.2.3 From 86f5c0cbfa64c5d0949365369529c5b607878ef8 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Wed, 20 Jan 2016 17:25:10 +0100 Subject: Update copyright headers. --- kernel/indtypes.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'kernel/indtypes.ml') diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index a46c33bf03..f9c2a7b0d5 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* nat -> Prop := C : forall z, let '(x,y) := z in x + y = 0. the computation of the number of arguments to I was made wrong in bde12b70. --- kernel/indtypes.ml | 9 ++++----- 1 file changed, 4 insertions(+), 5 deletions(-) (limited to 'kernel/indtypes.ml') diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index f9c2a7b0d5..49e8583158 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -336,7 +336,7 @@ let typecheck_inductive env mie = type ill_formed_ind = | LocalNonPos of int | LocalNotEnoughArgs of int - | LocalNotConstructor of rel_context * constr list + | LocalNotConstructor of rel_context * int | LocalNonPar of int * int * int exception IllFormedInd of ill_formed_ind @@ -355,11 +355,10 @@ let explain_ind_err id ntyp env nbpar c err = | LocalNotEnoughArgs kt -> raise (InductiveError (NotEnoughArgs (env,c',mkRel (kt+nbpar)))) - | LocalNotConstructor (paramsctxt,args)-> + | LocalNotConstructor (paramsctxt,nargs)-> let nparams = rel_context_nhyps paramsctxt in raise (InductiveError - (NotConstructor (env,id,c',mkRel (ntyp+nbpar),nparams, - List.length args - nparams))) + (NotConstructor (env,id,c',mkRel (ntyp+nbpar),nparams,nargs))) | LocalNonPar (n,i,l) -> raise (InductiveError (NonPar (env,c',n,mkRel i, mkRel (l+nbpar)))) @@ -548,7 +547,7 @@ let check_positivity_one (env,_,ntypes,_ as ienv) hyps (_,i as ind) nargs lcname 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))) + | _ -> raise (IllFormedInd (LocalNotConstructor(hyps,nargs))) end else if not (List.for_all (noccur_between n ntypes) largs) -- cgit v1.2.3 From 34ef02fac1110673ae74c41c185c228ff7876de2 Mon Sep 17 00:00:00 2001 From: Matej Kosik Date: Fri, 29 Jan 2016 10:13:12 +0100 Subject: CLEANUP: Context.{Rel,Named}.Declaration.t Originally, rel-context was represented as: Context.rel_context = Names.Name.t * Constr.t option * Constr.t Now it is represented as: Context.Rel.t = LocalAssum of Names.Name.t * Constr.t | LocalDef of Names.Name.t * Constr.t * Constr.t Originally, named-context was represented as: Context.named_context = Names.Id.t * Constr.t option * Constr.t Now it is represented as: Context.Named.t = LocalAssum of Names.Id.t * Constr.t | LocalDef of Names.Id.t * Constr.t * Constr.t Motivation: (1) In "tactics/hipattern.ml4" file we define "test_strict_disjunction" function which looked like this: let test_strict_disjunction n lc = Array.for_all_i (fun i c -> match (prod_assum (snd (decompose_prod_n_assum n c))) with | [_,None,c] -> isRel c && Int.equal (destRel c) (n - i) | _ -> false) 0 lc Suppose that you do not know about rel-context and named-context. (that is the case of people who just started to read the source code) Merlin would tell you that the type of the value you are destructing by "match" is: 'a * 'b option * Constr.t (* worst-case scenario *) or Named.Name.t * Constr.t option * Constr.t (* best-case scenario (?) *) To me, this is akin to wearing an opaque veil. It is hard to figure out the meaning of the values you are looking at. In particular, it is hard to discover the connection between the value we are destructing above and the datatypes and functions defined in the "kernel/context.ml" file. In this case, the connection is there, but it is not visible (between the function above and the "Context" module). ------------------------------------------------------------------------ Now consider, what happens when the reader see the same function presented in the following form: let test_strict_disjunction n lc = Array.for_all_i (fun i c -> match (prod_assum (snd (decompose_prod_n_assum n c))) with | [LocalAssum (_,c)] -> isRel c && Int.equal (destRel c) (n - i) | _ -> false) 0 lc If the reader haven't seen "LocalAssum" before, (s)he can use Merlin to jump to the corresponding definition and learn more. In this case, the connection is there, and it is directly visible (between the function above and the "Context" module). (2) Also, if we already have the concepts such as: - local declaration - local assumption - local definition and we describe these notions meticulously in the Reference Manual, then it is a real pity not to reinforce the connection of the actual code with the abstract description we published. --- kernel/indtypes.ml | 35 +++++++++++++++++++---------------- 1 file changed, 19 insertions(+), 16 deletions(-) (limited to 'kernel/indtypes.ml') diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index a8625009ce..4834f95d15 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -20,6 +20,7 @@ open Reduction open Typeops open Entries open Pp +open Context.Rel.Declaration (* Tell if indices (aka real arguments) contribute to size of inductive type *) (* If yes, this is compatible with the univalent model *) @@ -122,7 +123,7 @@ let infos_and_sort env t = 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 @@ -168,12 +169,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 = @@ -184,12 +187,12 @@ let is_impredicative env u = 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 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 @@ -249,7 +252,7 @@ let typecheck_inductive env mie = let full_arity = it_mkProd_or_LetIn arity params 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',[]) @@ -390,7 +393,7 @@ let check_correct_par (env,n,ntypes,_) hyps l largs = let nhyps = List.length hyps in let rec check k index = function | [] -> () - | (_,Some _,_)::hyps -> check k (index+1) hyps + | LocalDef _ :: 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 @@ -412,7 +415,7 @@ if Int.equal nmr 0 then 0 else function ([],_) -> nmr | (_,[]) -> assert false (* |hyps|>=nmr *) - | (lp,(_,Some _,_)::hyps) -> find k (index-1) (lp,hyps) + | (lp, LocalDef _ :: 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) @@ -426,15 +429,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 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 lpar) 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 @@ -726,9 +729,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 @@ -746,7 +749,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 -- cgit v1.2.3 From 4341f37cf3c51ed82c23f05846c8e6e8823d3cd6 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Thu, 10 Mar 2016 19:02:16 +0100 Subject: Primitive projections: protect kernel from erroneous definitions. E.g., Inductive foo := mkFoo { bla : foo } allowed to define recursive records with eta for which conversion is incomplete. - Eta-conversion only applies to BiFinite inductives - Finiteness information is now checked by the kernel (the constructor types must be strictly non recursive for BiFinite declarations). --- kernel/indtypes.ml | 19 ++++++++++++------- 1 file changed, 12 insertions(+), 7 deletions(-) (limited to 'kernel/indtypes.ml') diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index 49e8583158..acf5ab17d3 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -452,7 +452,7 @@ let array_min nmr a = if Int.equal nmr 0 then 0 else (* 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 check_positivity_one recursive (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] *) @@ -538,6 +538,8 @@ let check_positivity_one (env,_,ntypes,_ as ienv) hyps (_,i as ind) nargs lcname | 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 @@ -570,9 +572,11 @@ 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) -let check_positivity kn env_ar params inds = +let check_positivity kn env_ar params finite 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 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 @@ -581,7 +585,7 @@ let check_positivity kn env_ar params inds = 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 + check_positivity_one recursive ienv params (kn,i) nargs lcnames lc in let irecargs_nmr = Array.mapi check_one inds in let irecargs = Array.map snd irecargs_nmr @@ -807,10 +811,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 = @@ -851,7 +856,7 @@ 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 (* Then check positivity conditions *) - let (nmr,recargs) = check_positivity kn env_ar_par params inds in + let (nmr,recargs) = check_positivity kn env_ar_par params 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 -- cgit v1.2.3 From a88f5f162272ced5fb2b8ea555756b8fc51b939a Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Thu, 22 Oct 2015 18:22:26 +0200 Subject: This is an attempt to clarify terminology in choosing variable names in file indtypes.ml so that it is easier to follow what the code is doing. This is a purely alpha-renaming commit (if no mistakes). Note: was submitted as pull request #116. --- kernel/indtypes.ml | 200 +++++++++++++++++++++++++++++------------------------ 1 file changed, 109 insertions(+), 91 deletions(-) (limited to 'kernel/indtypes.ml') diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index 33abfe5b76..edb758f078 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -22,6 +22,16 @@ 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 *) @@ -186,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 (LocalAssum (_, 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 | LocalDef _ -> acc in - List.fold_left fold [] params + List.fold_left fold [] paramsctxt (* Type-check an inductive definition. Does not check positivity conditions. *) @@ -210,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 *) @@ -249,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 (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) @@ -324,7 +335,7 @@ let typecheck_inductive env mie = 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 @@ -334,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) (************************************************************************) (************************************************************************) @@ -354,21 +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)))) + (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,nargs))) + (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 @@ -384,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 = Context.Rel.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 | [] -> () - | LocalDef _ :: 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_betadeltaiota 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, LocalDef _ :: hyps) -> find k (index-1) (lp,hyps) - | (p::lp,_::hyps) -> + | (_,[]) -> assert false (* |paramsctxt|>=nmr *) + | (lp, LocalDef _ :: paramsctxt) -> find k (index-1) (lp,paramsctxt) + | (p::lp,_::paramsctxt) -> ( match kind_of_term (whd_betadeltaiota env p) with - | Rel w when Int.equal w index -> find (k+1) (index-1) (lp,hyps) + | 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 @@ -431,12 +450,12 @@ if Int.equal nmr 0 then 0 else let ienv_push_var (env, n, ntypes, lra) (x,a,ra) = (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' = - let decl = LocalAssum (Anonymous, hnf_prod_applist env ty lpar) 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)) :: @@ -457,7 +476,7 @@ 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 -(** [check_positivity_one ienv hyps (mind,i) nargs lcnames indlc] +(** [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] @@ -465,9 +484,9 @@ let array_min nmr a = if Int.equal nmr 0 then 0 else 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 recursive (env,_,ntypes,_ as ienv) hyps (_,i as ind) nargs lcnames indlc = - let lparams = Context.Rel.length hyps in - let nmr = Context.Rel.nhyps hyps in +let check_positivity_one 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). *) @@ -490,7 +509,7 @@ let check_positivity_one recursive (env,_,ntypes,_ as ienv) hyps (_,i as ind) na let largs = List.map (whd_betadeltaiota 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 (** The case where one of the inductives of the mutually @@ -525,27 +544,27 @@ let check_positivity_one recursive (env,_,ntypes,_ as ienv) hyps (_,i as ind) na (* 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 (** 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; + if 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 = (** Checks that the "nesting" inductive type is covariant in the relevant parameters. In other words, that the @@ -554,9 +573,9 @@ let check_positivity_one recursive (env,_,ntypes,_ as ienv) hyps (_,i as ind) na 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 @@ -590,8 +609,8 @@ let check_positivity_one recursive (env,_,ntypes,_ as ienv) hyps (_,i as ind) na 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,nargs))) + 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) @@ -603,33 +622,32 @@ let check_positivity_one recursive (env,_,ntypes,_ as ienv) hyps (_,i as ind) na 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) -(** [check_positivity kn env_ar params] checks that the mutually +(** [check_positivity kn env_ar paramsctxt inds] checks that the mutually inductive block [inds] is strictly positive. *) -let check_positivity kn env_ar params finite inds = +let check_positivity 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 = Context.Rel.length params in - let nmr = Context.Rel.nhyps params in + let rc = Array.mapi (fun j t -> (Mrec (kn,j),t)) (Rtree.mk_rec_calls ntypes) 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 = Context.Rel.nhyps sign - nmr in - check_positivity_one recursive 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 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 @@ -784,14 +802,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 = Context.Rel.nhyps params in - let nparamdecls = Context.Rel.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 @@ -804,10 +822,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,_) -> Context.Rel.length d - Context.Rel.length params) + Array.map (fun (d,_) -> Context.Rel.length d - nparamsctxt) splayed_lc in let consnrealargs = - Array.map (fun (d,_) -> Context.Rel.nhyps d - Context.Rel.nhyps params) + Array.map (fun (d,_) -> Context.Rel.nhyps d - nparamargs) splayed_lc in (* Elimination sorts *) let arkind,kelim = @@ -841,7 +859,7 @@ let build_inductive env p prv ctx env_ar params kn isrecord isfinite inds nmr re mind_arity = arkind; mind_arity_ctxt = Vars.subst_univs_level_context subst ar_sign; mind_nrealargs = Context.Rel.nhyps ar_sign - nparamargs; - mind_nrealdecls = Context.Rel.length ar_sign - nparamdecls; + mind_nrealdecls = Context.Rel.length ar_sign - nparamsctxt; mind_kelim = kelim; mind_consnames = Array.of_list cnames; mind_consnrealdecls = consnrealdecls; @@ -871,7 +889,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) @@ -885,7 +903,7 @@ 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; @@ -897,11 +915,11 @@ 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 mie.mind_entry_finite inds in + let (nmr,recargs) = check_positivity 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 -- cgit v1.2.3