From c5e8c731ede28ba4f734bbd143c7d7e5a05c365a Mon Sep 17 00:00:00 2001 From: herbelin Date: Fri, 27 Oct 2006 17:32:45 +0000 Subject: Correction de 2 bugs critiques du polymorphisme d'univers git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9301 85f007b7-540e-0410-9357-904b9bb8a0f7 --- kernel/indtypes.ml | 6 +++- kernel/inductive.ml | 95 ++++++++++++++++++++++++++++++++--------------------- 2 files changed, 62 insertions(+), 39 deletions(-) diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index 41ca4e661..a41cc53be 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -163,9 +163,13 @@ let small_unit constrsinfos = w1,w2,w3 <= u3 *) +let extract_level (_,_,_,lc,lev) = + (* Enforce that the level is not in Prop if more than two constructors *) + if Array.length lc >= 2 then sup base_univ lev else lev + let inductive_levels arities inds = let levels = Array.map pi3 arities in - let cstrs_levels = Array.map (fun (_,_,_,_,lev) -> lev) inds in + let cstrs_levels = Array.map extract_level inds in (* Take the transitive closure of the system of constructors *) (* level constraints and remove the recursive dependencies *) solve_constraints_system levels cstrs_levels diff --git a/kernel/inductive.ml b/kernel/inductive.ml index d62af2e5e..bce14dc27 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -139,44 +139,61 @@ let cons_subst u su subst = try (u, sup su (List.assoc u subst)) :: List.remove_assoc u subst with Not_found -> (u, su) :: subst -let rec make_subst env exp act = - match exp, act with - (* Bind expected levels of parameters to actual levels *) - | None :: exp, _ :: act -> - make_subst env exp act - | Some u :: exp, t :: act -> - let su = sort_as_univ (snd (dest_arity env t)) in - cons_subst u su (make_subst env exp act) - (* Not enough parameters, create a fresh univ *) - | Some u :: exp, [] -> - let su = fresh_local_univ () in - cons_subst u su (make_subst env exp []) - | None :: exp, [] -> - make_subst env exp [] - (* Uniform parameters are exhausted *) - | [], _ -> [] - -let sort_of_instantiated_universe mip subst level = - let level = subst_large_constraints subst level in - let nci = number_of_constructors mip in - if nci = 0 then mk_Prop - else - if is_empty_univ level then if nci = 1 then mk_Prop else mk_Set - else if is_base_univ level then mk_Set - else Type level - -let instantiate_inductive_with_param_levels env ar mip paramtyps = - let args = Array.to_list paramtyps in - let subst = make_subst env ar.mind_param_levels args in - sort_of_instantiated_universe mip subst ar.mind_level +let actualize_decl_level env lev t = + let sign,s = dest_arity env t in + mkArity (sign,lev) + +(* 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)::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 s = fresh_local_univ () in + let t = actualize_decl_level env (Type s) t in + let ctx,subst = make_subst env (sign, exp, []) in + (na,None,t)::ctx, cons_subst u s subst + | sign, [], _ -> + (* Uniform parameters are exhausted *) + sign,[] + | [], _, _ -> + assert false + +let instantiate_universes env ctx mip ar argsorts = + let args = Array.to_list argsorts in + let ctx,subst = make_subst env (ctx,ar.mind_param_levels,args) in + let level = subst_large_constraints subst ar.mind_level in + ctx, + if is_empty_univ level then mk_Prop + else if is_base_univ level then mk_Set + else Type level let type_of_inductive_knowing_parameters env mip paramtyps = match mip.mind_arity with | Monomorphic s -> s.mind_user_arity | Polymorphic ar -> - let s = instantiate_inductive_with_param_levels env ar mip paramtyps in - mkArity (mip.mind_arity_ctxt,s) + let ctx = List.rev mip.mind_arity_ctxt in + let ctx,s = instantiate_universes env ctx mip ar paramtyps in + mkArity (List.rev ctx,s) (* The max of an array of universes *) @@ -190,15 +207,17 @@ let max_inductive_sort = (* Type of a (non applied) inductive type *) -let type_of_inductive (_,mip) = +let type_of_inductive (mib,mip) = match mip.mind_arity with | Monomorphic s -> s.mind_user_arity | Polymorphic s -> - let subst = map_succeed (function - | Some u -> (u, fresh_local_univ ()) - | None -> failwith "") s.mind_param_levels in - let s = mkSort (sort_of_instantiated_universe mip subst s.mind_level) in - it_mkProd_or_LetIn s mip.mind_arity_ctxt + let s = + if mib.mind_nparams = 0 then + if is_empty_univ s.mind_level then mk_Prop + else if is_base_univ s.mind_level then mk_Set + else Type s.mind_level + else Type s.mind_level in + mkArity (mip.mind_arity_ctxt,s) (************************************************************************) (* Type of a constructor *) -- cgit v1.2.3