From 7c7726a798caa6b506a727703de24d2bb5bb3956 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Tue, 7 Jul 2015 17:04:45 +0200 Subject: Univs: bug fix. Missing universe substitutions of mind_params_ctxt when typechecking cases, which appeared only when let-ins were used. --- kernel/inductive.ml | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) (limited to 'kernel/inductive.ml') diff --git a/kernel/inductive.ml b/kernel/inductive.ml index 4c1614bac1..35b29e73a6 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -96,11 +96,11 @@ let full_inductive_instantiate mib u params sign = let ar = fst (destArity (instantiate_params true t params mib.mind_params_ctxt)) in Vars.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) 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 params + (Vars.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. --- kernel/inductive.ml | 76 +++++++++++++++++++++++++++++++---------------------- 1 file changed, 45 insertions(+), 31 deletions(-) (limited to 'kernel/inductive.ml') diff --git a/kernel/inductive.ml b/kernel/inductive.ml index 35b29e73a6..84084718f0 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -134,46 +134,60 @@ let sort_as_univ = function (* Template polymorphism *) +(* 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 + 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 (Lazy.force 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 (Lazy.force 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/ --- kernel/inductive.ml | 11 +++++------ 1 file changed, 5 insertions(+), 6 deletions(-) (limited to 'kernel/inductive.ml') diff --git a/kernel/inductive.ml b/kernel/inductive.ml index 84084718f0..00d14a25e2 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -73,7 +73,7 @@ let constructor_instantiate mind u mib c = let s = ind_subst mind mib u in substl s (subst_instance_constr u c) -let instantiate_params full t args sign = +let instantiate_params full t u args sign = let fail () = anomaly ~label:"instantiate_params" (Pp.str "type, ctxt and args mismatch") in let (rem_args, subs, ty) = @@ -81,7 +81,8 @@ let instantiate_params full t args sign = (fun (_,copt,_) (largs,subs,ty) -> match (copt, largs, kind_of_term ty) with | (None, a::args, Prod(_,_,t)) -> (args, a::subs, t) - | (Some b,_,LetIn(_,_,_,t)) -> (largs, (substl subs b)::subs, t) + | (Some b,_,LetIn(_,_,_,t)) -> + (largs, (substl subs (subst_instance_constr u b))::subs, t) | (_,[],_) -> if full then fail() else ([], subs, ty) | _ -> fail ()) sign @@ -93,13 +94,11 @@ let instantiate_params full t args sign = let full_inductive_instantiate mib u params sign = let dummy = prop_sort in let t = mkArity (sign,dummy) in - let ar = fst (destArity (instantiate_params true t params mib.mind_params_ctxt)) in - Vars.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 params - (Vars.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. --- kernel/inductive.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'kernel/inductive.ml') diff --git a/kernel/inductive.ml b/kernel/inductive.ml index 00d14a25e2..cf4177c50b 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -153,7 +153,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 @@ -166,7 +166,7 @@ let rec make_subst env = (* a useless extra constraint *) let s = sort_as_univ (snd (dest_arity env (Lazy.force 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. --- kernel/inductive.ml | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'kernel/inductive.ml') diff --git a/kernel/inductive.ml b/kernel/inductive.ml index cf4177c50b..87c139f48d 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -93,7 +93,7 @@ let instantiate_params full t u args sign = let full_inductive_instantiate mib u params sign = let dummy = prop_sort in - let t = mkArity (sign,dummy) in + let t = mkArity (Vars.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 = @@ -344,13 +344,13 @@ let is_correct_arity env c pj ind specif params = | Prod (na1,a1,a2), [] -> (* whnf of t was not needed here! *) let env' = push_rel (na1,None,a1) env in let ksort = match kind_of_term (whd_betadeltaiota env' a2) with - | Sort s -> family_of_sort s - | _ -> raise (LocalArity None) in + | Sort s -> family_of_sort s + | _ -> raise (LocalArity None) in let dep_ind = build_dependent_inductive ind specif params in let _ = try conv env a1 dep_ind with NotConvertible -> raise (LocalArity None) in - check_allowed_sort ksort specif + check_allowed_sort ksort specif | _, (_,Some _,_ as d)::ar' -> srec (push_rel d env) (lift 1 pt') ar' | _ -> -- cgit v1.2.3