From c71cff0328fa0ee640f35337278f344e0d00698a Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Wed, 8 Jul 2015 12:44:59 +0200 Subject: Checker: Report bugfixes from kernel/inductive.ml Wrong handling of mind_params_ctxt... --- checker/inductive.ml | 12 +++++++----- 1 file changed, 7 insertions(+), 5 deletions(-) (limited to 'checker/inductive.ml') diff --git a/checker/inductive.ml b/checker/inductive.ml index 59d1a645a5..1c8f570df9 100644 --- a/checker/inductive.ml +++ b/checker/inductive.ml @@ -104,12 +104,14 @@ let instantiate_params full t u args sign = let full_inductive_instantiate mib u params sign = let dummy = Prop Null in let t = mkArity (sign,dummy) in - fst (destArity (instantiate_params true t u params mib.mind_params_ctxt)) + let ar = fst (destArity (instantiate_params true t u params mib.mind_params_ctxt)) in + subst_instance_context u ar -let full_constructor_instantiate ((mind,_),u,(mib,_),params) = - let inst_ind = constructor_instantiate mind u mib in - (fun t -> - instantiate_params true (inst_ind t) u params mib.mind_params_ctxt) + +let full_constructor_instantiate ((mind,_),u,(mib,_),params) t = + let inst_ind = constructor_instantiate mind u mib t in + instantiate_params true inst_ind u params + (subst_instance_context u mib.mind_params_ctxt) (************************************************************************) (************************************************************************) -- cgit v1.2.3 From 3a6b08286ac78c674d6d3e3073b38de26a610fdc Mon Sep 17 00:00:00 2001 From: mlasson Date: Mon, 22 Jun 2015 21:14:20 +0200 Subject: Template polymorphism: A bug-fix for Bug #4258 Reviewed by M. Sozeau This commit fixes template polymorphism and makes it more precise, applying to non-linear uses of the same universe in parameters of template-polymorphic inductives. See bug report and https://github.com/coq/coq/pull/69 for full details. I also removed some deadcode in checker/inductive.ml. I do not know if it is also necessary to fix checker/indtypes.ml. --- checker/inductive.ml | 83 ++++++++++++++++++++++++++++------------------------ 1 file changed, 45 insertions(+), 38 deletions(-) (limited to 'checker/inductive.ml') diff --git a/checker/inductive.ml b/checker/inductive.ml index 1c8f570df9..5d31649737 100644 --- a/checker/inductive.ml +++ b/checker/inductive.ml @@ -144,53 +144,60 @@ let sort_as_univ = function | Prop Null -> Univ.type0m_univ | Prop Pos -> Univ.type0_univ +(* cons_subst add the mapping [u |-> su] in subst if [u] is not *) +(* in the domain or add [u |-> sup x su] if [u] is already mapped *) +(* to [x]. *) let cons_subst u su subst = - Univ.LMap.add u su subst - -let actualize_decl_level env lev t = - let sign,s = dest_arity env t in - mkArity (sign,lev) - -let polymorphism_on_non_applied_parameters = false + try + Univ.LMap.add u (Univ.sup (Univ.LMap.find u subst) su) subst + with Not_found -> Univ.LMap.add u su subst + +(* remember_subst updates the mapping [u |-> x] by [u |-> sup x u] *) +(* if it is presents and returns the substitution unchanged if not.*) +let remember_subst u subst = + try + let su = Universe.make u in + Univ.LMap.add u (Univ.sup (Univ.LMap.find u subst) su) subst + with Not_found -> subst (* Bind expected levels of parameters to actual levels *) (* Propagate the new levels in the signature *) -let rec make_subst env = function - | (_,Some _,_ as t)::sign, exp, args -> - let ctx,subst = make_subst env (sign, exp, args) in - t::ctx, subst - | d::sign, None::exp, args -> - let args = match args with _::args -> args | [] -> [] in - let ctx,subst = make_subst env (sign, exp, args) in - d::ctx, subst - | d::sign, Some u::exp, a::args -> - (* We recover the level of the argument, but we don't change the *) - (* level in the corresponding type in the arity; this level in the *) - (* arity is a global level which, at typing time, will be enforce *) - (* to be greater than the level of the argument; this is probably *) - (* a useless extra constraint *) - let s = sort_as_univ (snd (dest_arity env a)) in - let ctx,subst = make_subst env (sign, exp, args) in - d::ctx, cons_subst u s subst - | (na,None,t as d)::sign, Some u::exp, [] -> - (* No more argument here: we instantiate the type with a fresh level *) - (* which is first propagated to the corresponding premise in the arity *) - (* (actualize_decl_level), then to the conclusion of the arity (via *) - (* the substitution) *) - let ctx,subst = make_subst env (sign, exp, []) in - d::ctx, subst - | sign, [], _ -> - (* Uniform parameters are exhausted *) - sign,Univ.LMap.empty - | [], _, _ -> - assert false - +let rec make_subst env = + let rec make subst = function + | (_,Some _,_ as t)::sign, exp, args -> + make subst (sign, exp, args) + | d::sign, None::exp, args -> + let args = match args with _::args -> args | [] -> [] in + make subst (sign, exp, args) + | d::sign, Some u::exp, a::args -> + (* We recover the level of the argument, but we don't change the *) + (* level in the corresponding type in the arity; this level in the *) + (* arity is a global level which, at typing time, will be enforce *) + (* to be greater than the level of the argument; this is probably *) + (* a useless extra constraint *) + let s = sort_as_univ (snd (dest_arity env a)) in + make (cons_subst u s subst) (sign, exp, args) + | (na,None,t as d)::sign, Some u::exp, [] -> + (* No more argument here: we add the remaining universes to the *) + (* substitution (when [u] is distinct from all other universes in the *) + (* template, it is identity substitution otherwise (ie. when u is *) + (* already in the domain of the substitution) [remember_subst] will *) + (* update its image [x] by [sup x u] in order not to forget the *) + (* dependency in [u] that remains to be fullfilled. *) + make (remember_subst u subst) (sign, exp, []) + | sign, [], _ -> + (* Uniform parameters are exhausted *) + subst + | [], _, _ -> + assert false + in + make Univ.LMap.empty exception SingletonInductiveBecomesProp of Id.t let instantiate_universes env ctx ar argsorts = let args = Array.to_list argsorts in - let ctx,subst = make_subst env (ctx,ar.template_param_levels,args) in + let subst = make_subst env (ctx,ar.template_param_levels,args) in let level = Univ.subst_univs_universe (Univ.make_subst subst) ar.template_level in let ty = (* Singleton type not containing types are interpretable in Prop *) -- cgit v1.2.3 From 2c59d19ad207a6bf193e9f0c9d73258b3133d484 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Thu, 9 Jul 2015 16:58:06 +0200 Subject: Kernel/Checker: Cleanup fixes of substitutions due to let-ins. Avoid undeeded large substitutions, and add test-suite file for fixed bug 4283 in closed/ --- checker/inductive.ml | 7 ++----- 1 file changed, 2 insertions(+), 5 deletions(-) (limited to 'checker/inductive.ml') diff --git a/checker/inductive.ml b/checker/inductive.ml index 5d31649737..e3d8dd2060 100644 --- a/checker/inductive.ml +++ b/checker/inductive.ml @@ -104,14 +104,11 @@ let instantiate_params full t u args sign = let full_inductive_instantiate mib u params sign = let dummy = Prop Null in let t = mkArity (sign,dummy) in - let ar = fst (destArity (instantiate_params true t u params mib.mind_params_ctxt)) in - subst_instance_context u ar - + fst (destArity (instantiate_params true t u params mib.mind_params_ctxt)) let full_constructor_instantiate ((mind,_),u,(mib,_),params) t = let inst_ind = constructor_instantiate mind u mib t in - instantiate_params true inst_ind u params - (subst_instance_context u mib.mind_params_ctxt) + instantiate_params true inst_ind u params mib.mind_params_ctxt (************************************************************************) (************************************************************************) -- cgit v1.2.3 From 1391955c6635da17b4fb2d7c7b5cec799685e99d Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Fri, 10 Jul 2015 10:26:57 +0200 Subject: Unused variables reported by OCaml. --- checker/inductive.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'checker/inductive.ml') diff --git a/checker/inductive.ml b/checker/inductive.ml index e3d8dd2060..00d3bc8e14 100644 --- a/checker/inductive.ml +++ b/checker/inductive.ml @@ -161,7 +161,7 @@ let remember_subst u subst = (* Propagate the new levels in the signature *) let rec make_subst env = let rec make subst = function - | (_,Some _,_ as t)::sign, exp, args -> + | (_,Some _,_)::sign, exp, args -> make subst (sign, exp, args) | d::sign, None::exp, args -> let args = match args with _::args -> args | [] -> [] in @@ -174,7 +174,7 @@ let rec make_subst env = (* a useless extra constraint *) let s = sort_as_univ (snd (dest_arity env a)) in make (cons_subst u s subst) (sign, exp, args) - | (na,None,t as d)::sign, Some u::exp, [] -> + | (na,None,t)::sign, Some u::exp, [] -> (* No more argument here: we add the remaining universes to the *) (* substitution (when [u] is distinct from all other universes in the *) (* template, it is identity substitution otherwise (ie. when u is *) -- cgit v1.2.3 From c57c7edbe517851c7309112f6eb5d8297f03e000 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Wed, 15 Jul 2015 17:36:58 +0200 Subject: Univs/Inductive: fix typechecking of cases I was trying to be a bit too clever with not substituting the universe instance everywhere: the constructor type/inductive arity has to be instantiated before instantiate_params runs, which became true only for constructor types since my last commit. --- checker/inductive.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'checker/inductive.ml') diff --git a/checker/inductive.ml b/checker/inductive.ml index 00d3bc8e14..21b80f323e 100644 --- a/checker/inductive.ml +++ b/checker/inductive.ml @@ -103,7 +103,7 @@ let instantiate_params full t u args sign = let full_inductive_instantiate mib u params sign = let dummy = Prop Null in - let t = mkArity (sign,dummy) in + let t = mkArity (subst_instance_context u sign,dummy) in fst (destArity (instantiate_params true t u params mib.mind_params_ctxt)) let full_constructor_instantiate ((mind,_),u,(mib,_),params) t = -- cgit v1.2.3