diff options
40 files changed, 445 insertions, 224 deletions
diff --git a/kernel/cooking.ml b/kernel/cooking.ml index 4bae6de66..3d580d713 100644 --- a/kernel/cooking.ml +++ b/kernel/cooking.ml @@ -183,21 +183,17 @@ let cook_constant env { from = cb; info = { Opaqueproof.modlist; abstract } } = Context.fold_named_context (fun (h,_,_) hyps -> List.filter (fun (id,_,_) -> not (Id.equal id h)) hyps) hyps ~init:cb.const_hyps in - - (* let typ = match cb.const_type with *) - (* | NonPolymorphicType t -> *) - (* let typ = *) - (* abstract_constant_type (expmod_constr cache r.d_modlist t) hyps in *) - (* NonPolymorphicType typ *) - (* | PolymorphicArity (ctx,s) -> *) - (* let t = mkArity (ctx,Type s.poly_level) in *) - (* let typ = *) - (* abstract_constant_type (expmod_constr cache r.d_modlist t) hyps in *) - (* let j = make_judge (constr_of_def body) typ in *) - (* Typeops.make_polymorphic_if_constant_for_ind env j *) - (* in *) - let typ = - abstract_constant_type (expmod_constr cache modlist cb.const_type) hyps + let typ = match cb.const_type with + | RegularArity t -> + let typ = + abstract_constant_type (expmod_constr cache modlist t) hyps in + RegularArity typ + | TemplateArity (ctx,s) -> + let t = mkArity (ctx,Type s.template_level) in + let typ = + abstract_constant_type (expmod_constr cache modlist t) hyps in + let j = make_judge (constr_of_def body) typ in + Typeops.make_polymorphic_if_constant_for_ind env j in let projection pb = let c' = abstract_constant_body (expmod_constr cache modlist pb.proj_body) hyps in @@ -210,6 +206,9 @@ let cook_constant env { from = cb; info = { Opaqueproof.modlist; abstract } } = | _ -> assert false with Not_found -> (((pb.proj_ind,0),Univ.Instance.empty), 0) in + let typ = (* By invariant, a regular arity *) + match typ with RegularArity t -> t | TemplateArity _ -> assert false + in let ctx, ty' = decompose_prod_n (n' + pb.proj_npars + 1) typ in { proj_ind = mind; proj_npars = pb.proj_npars + n'; proj_arg = pb.proj_arg; proj_type = ty'; proj_body = c' } diff --git a/kernel/declarations.mli b/kernel/declarations.mli index f3cb41f32..f269e165e 100644 --- a/kernel/declarations.mli +++ b/kernel/declarations.mli @@ -18,7 +18,24 @@ type engagement = ImpredicativeSet (** {6 Representation of constants (Definition/Axiom) } *) -type constant_type = types +(** Non-universe polymorphic mode polymorphism (Coq 8.2+): inductives + and constants hiding inductives are implicitely polymorphic when + applied to parameters, on the universes appearing in the whnf of + their parameters and their conclusion, in a template style. + + In truely universe polymorphic mode, we always use RegularArity. +*) + +type template_arity = { + template_param_levels : Univ.universe option list; + template_level : Univ.universe; +} + +type ('a, 'b) declaration_arity = + | RegularArity of 'a + | TemplateArity of 'b + +type constant_type = (types, rel_context * template_arity) declaration_arity (** Inlining level of parameters at functor applications. None means no inlining *) @@ -79,11 +96,13 @@ type wf_paths = recarg Rtree.t v} *) -type inductive_arity = { +type regular_inductive_arity = { mind_user_arity : types; mind_sort : sorts; } +type inductive_arity = (regular_inductive_arity, template_arity) declaration_arity + type one_inductive_body = { (** {8 Primitive datas } *) diff --git a/kernel/declareops.ml b/kernel/declareops.ml index 0e4b80495..be6c18810 100644 --- a/kernel/declareops.ml +++ b/kernel/declareops.ml @@ -13,6 +13,28 @@ open Util (** Operations concernings types in [Declarations] : [constant_body], [mutual_inductive_body], [module_body] ... *) +(** {6 Arities } *) + +let subst_decl_arity f g sub ar = + match ar with + | RegularArity x -> + let x' = f sub x in + if x' == x then ar + else RegularArity x' + | TemplateArity x -> + let x' = g sub x in + if x' == x then ar + else TemplateArity x' + +let map_decl_arity f g = function + | RegularArity a -> RegularArity (f a) + | TemplateArity a -> TemplateArity (g a) + +let hcons_template_arity ar = + { template_param_levels = + List.smartmap (Option.smartmap Univ.hcons_univ) ar.template_param_levels; + template_level = Univ.hcons_univ ar.template_level } + (** {6 Constants } *) let body_of_constant cb = match cb.const_body with @@ -44,14 +66,10 @@ let subst_rel_declaration sub (id,copt,t as x) = let subst_rel_context sub = List.smartmap (subst_rel_declaration sub) -(* let subst_const_type sub arity = match arity with *) -(* | NonPolymorphicType s -> *) -(* let s' = subst_mps sub s in *) -(* if s==s' then arity else NonPolymorphicType s' *) -(* | PolymorphicArity (ctx,s) -> *) -(* let ctx' = subst_rel_context sub ctx in *) -(* if ctx==ctx' then arity else PolymorphicArity (ctx',s) *) - +let subst_template_cst_arity sub (ctx,s as arity) = + let ctx' = subst_rel_context sub ctx in + if ctx==ctx' then arity else (ctx',s) + let subst_const_type sub arity = if is_empty_subst sub then arity else subst_mps sub arity @@ -73,7 +91,7 @@ let subst_const_body sub cb = if is_empty_subst sub then cb else let body' = subst_const_def sub cb.const_body in - let type' = subst_const_type sub cb.const_type in + let type' = subst_decl_arity subst_const_type subst_template_cst_arity sub cb.const_type in let proj' = Option.smartmap (subst_const_proj sub) cb.const_proj in if body' == cb.const_body && type' == cb.const_type && proj' == cb.const_proj then cb @@ -102,7 +120,13 @@ let hcons_rel_decl ((n,oc,t) as d) = let hcons_rel_context l = List.smartmap hcons_rel_decl l -let hcons_const_type t = Term.hcons_constr t +let hcons_regular_const_arity t = Term.hcons_constr t + +let hcons_template_const_arity (ctx, ar) = + (hcons_rel_context ctx, hcons_template_arity ar) + +let hcons_const_type = + map_decl_arity hcons_regular_const_arity hcons_template_const_arity let hcons_const_def = function | Undef inl -> Undef inl @@ -164,72 +188,15 @@ let subst_wf_paths sub p = Rtree.smartmap (subst_recarg sub) p (** {7 Substitution of inductive declarations } *) -(* OLD POLYMORPHISM *) -(* let subst_indarity sub ar = match ar with *) -(* | Monomorphic s -> *) -(* let uar' = subst_mps sub s.mind_user_arity in *) -(* if uar' == s.mind_user_arity then ar *) -(* else Monomorphic { mind_user_arity = uar'; mind_sort = s.mind_sort } *) -(* | Polymorphic _ -> ar *) - -(* let subst_mind_packet sub mip = *) -(* let { mind_nf_lc = nf; *) -(* mind_user_lc = user; *) -(* mind_arity_ctxt = ctxt; *) -(* mind_arity = ar; *) -(* mind_recargs = ra } = mip *) -(* in *) -(* let nf' = Array.smartmap (subst_mps sub) nf in *) -(* let user' = *) -(* (\* maintain sharing of [mind_user_lc] and [mind_nf_lc] *\) *) -(* if user==nf then nf' *) -(* else Array.smartmap (subst_mps sub) user *) -(* in *) -(* let ctxt' = subst_rel_context sub ctxt in *) -(* let ar' = subst_indarity sub ar in *) -(* let ra' = subst_wf_paths sub ra in *) -(* if nf==nf' && user==user' && ctxt==ctxt' && ar==ar' && ra==ra' *) -(* then mip *) -(* else *) -(* { mip with *) -(* mind_nf_lc = nf'; *) -(* mind_user_lc = user'; *) -(* mind_arity_ctxt = ctxt'; *) -(* mind_arity = ar'; *) -(* mind_recargs = ra' } *) - -(* let subst_mind sub mib = *) -(* assert (List.is_empty mib.mind_hyps); (\* we're outside sections *\) *) -(* if is_empty_subst sub then mib *) -(* else *) -(* let params = mib.mind_params_ctxt in *) -(* let params' = Context.map_rel_context (subst_mps sub) params in *) -(* let packets = mib.mind_packets in *) -(* let packets' = Array.smartmap (subst_mind_packet sub) packets in *) -(* if params==params' && packets==packets' then mib *) -(* else *) -(* { mib with *) -(* mind_params_ctxt = params'; *) -(* mind_packets = packets'; *) -(* mind_native_name = ref NotLinked } *) - -(* (\** {6 Hash-consing of inductive declarations } *\) *) - -(* (\** Just as for constants, this hash-consing is quite partial *\) *) - -(* let hcons_indarity = function *) -(* | Monomorphic a -> *) -(* Monomorphic *) -(* { mind_user_arity = Term.hcons_constr a.mind_user_arity; *) -(* mind_sort = Term.hcons_sorts a.mind_sort } *) -(* | Polymorphic a -> Polymorphic (hcons_polyarity a) *) +let subst_regular_ind_arity sub s = + let uar' = subst_mps sub s.mind_user_arity in + if uar' == s.mind_user_arity then s + else { mind_user_arity = uar'; mind_sort = s.mind_sort } -(** Substitution of inductive declarations *) +let subst_template_ind_arity sub s = s -let subst_indarity sub s = - { mind_user_arity = subst_mps sub s.mind_user_arity; - mind_sort = s.mind_sort; - } +let subst_ind_arity = + subst_decl_arity subst_regular_ind_arity subst_template_ind_arity let subst_mind_packet sub mbp = { mind_consnames = mbp.mind_consnames; @@ -238,7 +205,7 @@ let subst_mind_packet sub mbp = mind_typename = mbp.mind_typename; mind_nf_lc = Array.smartmap (subst_mps sub) mbp.mind_nf_lc; mind_arity_ctxt = subst_rel_context sub mbp.mind_arity_ctxt; - mind_arity = subst_indarity sub mbp.mind_arity; + mind_arity = subst_ind_arity sub mbp.mind_arity; mind_user_lc = Array.smartmap (subst_mps sub) mbp.mind_user_lc; mind_nrealargs = mbp.mind_nrealargs; mind_nrealargs_ctxt = mbp.mind_nrealargs_ctxt; @@ -261,12 +228,19 @@ let subst_mind_body sub mib = mind_polymorphic = mib.mind_polymorphic; mind_universes = mib.mind_universes } -(** Hash-consing of inductive declarations *) +(** {6 Hash-consing of inductive declarations } *) -let hcons_indarity a = +let hcons_regular_ind_arity a = { mind_user_arity = Term.hcons_constr a.mind_user_arity; mind_sort = Term.hcons_sorts a.mind_sort } +(** Just as for constants, this hash-consing is quite partial *) + +let hcons_ind_arity = + map_decl_arity hcons_regular_ind_arity hcons_template_arity + +(** Substitution of inductive declarations *) + let hcons_mind_packet oib = let user = Array.smartmap Term.hcons_types oib.mind_user_lc in let nf = Array.smartmap Term.hcons_types oib.mind_nf_lc in @@ -275,7 +249,7 @@ let hcons_mind_packet oib = { oib with mind_typename = Names.Id.hcons oib.mind_typename; mind_arity_ctxt = hcons_rel_context oib.mind_arity_ctxt; - mind_arity = hcons_indarity oib.mind_arity; + mind_arity = hcons_ind_arity oib.mind_arity; mind_consnames = Array.smartmap Names.Id.hcons oib.mind_consnames; mind_user_lc = user; mind_nf_lc = nf } diff --git a/kernel/declareops.mli b/kernel/declareops.mli index 0c5f3584e..9f5197668 100644 --- a/kernel/declareops.mli +++ b/kernel/declareops.mli @@ -12,6 +12,11 @@ open Mod_subst (** Operations concerning types in [Declarations] : [constant_body], [mutual_inductive_body], [module_body] ... *) +(** {6 Arities} *) + +val map_decl_arity : ('a -> 'c) -> ('b -> 'd) -> + ('a, 'b) declaration_arity -> ('c, 'd) declaration_arity + (** {6 Constants} *) val subst_const_body : substitution -> constant_body -> constant_body diff --git a/kernel/environ.ml b/kernel/environ.ml index 323d6fcea..1f29fd67a 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -214,12 +214,22 @@ let universes_and_subst_of cb u = let subst = Univ.make_universe_subst u univs in subst, Univ.instantiate_univ_context subst univs +let get_regular_arity = function + | RegularArity a -> a + | TemplateArity _ -> assert false + +let map_regular_arity f = function + | RegularArity a as ar -> + let a' = f a in + if a' == a then ar else RegularArity a' + | TemplateArity _ -> assert false + (* constant_type gives the type of a constant *) let constant_type env (kn,u) = let cb = lookup_constant kn env in if cb.const_polymorphic then let subst, csts = universes_and_subst_of cb u in - (subst_univs_constr subst cb.const_type, csts) + (map_regular_arity (subst_univs_constr subst) cb.const_type, csts) else cb.const_type, Univ.Constraint.empty let constant_type_in_ctx env kn = @@ -260,7 +270,8 @@ let constant_value_and_type env (kn, u) = | Def l_body -> Some (subst_univs_constr subst (Mod_subst.force_constr l_body)) | OpaqueDef _ -> None | Undef _ -> None - in b', subst_univs_constr subst cb.const_type, cst + in + b', map_regular_arity (subst_univs_constr subst) cb.const_type, cst else let b' = match cb.const_body with | Def l_body -> Some (Mod_subst.force_constr l_body) @@ -277,7 +288,7 @@ let constant_type_in env (kn,u) = let cb = lookup_constant kn env in if cb.const_polymorphic then let subst = Univ.make_universe_subst u (Future.force cb.const_universes) in - subst_univs_constr subst cb.const_type + map_regular_arity (subst_univs_constr subst) cb.const_type else cb.const_type let constant_value_in env (kn,u) = diff --git a/kernel/environ.mli b/kernel/environ.mli index fb5d79718..330d9c277 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -140,12 +140,12 @@ type const_evaluation_result = NoBody | Opaque | IsProj exception NotEvaluableConst of const_evaluation_result val constant_value : env -> constant puniverses -> constr constrained -val constant_type : env -> constant puniverses -> types constrained -val constant_type_in_ctx : env -> constant -> types Univ.in_universe_context +val constant_type : env -> constant puniverses -> constant_type constrained +val constant_type_in_ctx : env -> constant -> constant_type Univ.in_universe_context val constant_opt_value : env -> constant puniverses -> (constr * Univ.constraints) option val constant_value_and_type : env -> constant puniverses -> - types option * constr * Univ.constraints + constr option * constant_type * Univ.constraints (** The universe context associated to the constant, empty if not polymorphic *) val constant_context : env -> constant -> Univ.universe_context @@ -154,7 +154,7 @@ val constant_context : env -> constant -> Univ.universe_context already contains the constraints corresponding to the constant application. *) val constant_value_in : env -> constant puniverses -> constr -val constant_type_in : env -> constant puniverses -> types +val constant_type_in : env -> constant puniverses -> constant_type val constant_opt_value_in : env -> constant puniverses -> constr option diff --git a/kernel/fast_typeops.ml b/kernel/fast_typeops.ml index b441e02a3..8b7230c3b 100644 --- a/kernel/fast_typeops.ml +++ b/kernel/fast_typeops.ml @@ -109,17 +109,40 @@ let check_hyps_inclusion env f c sign = (* Type of constants *) -let type_of_constant env cst = constant_type env cst -let type_of_constant_in env cst = constant_type_in env cst -let type_of_constant_knowing_parameters env t _ = t -let judge_of_constant env (kn,u as cst) = +let type_of_constant_knowing_parameters_arity env t paramtyps = + match t with + | RegularArity t -> t + | TemplateArity (sign,ar) -> + let ctx = List.rev sign in + let ctx,s = instantiate_universes env ctx ar paramtyps in + mkArity (List.rev ctx,s) + +let type_of_constant_knowing_parameters env cst paramtyps = + let ty, cu = constant_type env cst in + type_of_constant_knowing_parameters_arity env ty paramtyps, cu + +let type_of_constant_type env t = + type_of_constant_knowing_parameters_arity env t [||] + +let type_of_constant env cst = + type_of_constant_knowing_parameters env cst [||] + +let type_of_constant_in env cst = + let ar = constant_type_in env cst in + type_of_constant_knowing_parameters_arity env ar [||] + +let judge_of_constant_knowing_parameters env (kn,u as cst) jl = let cb = lookup_constant kn env in let () = check_hyps_inclusion env mkConstU cst cb.const_hyps in - let ty, cu = type_of_constant env cst in + let paramstyp = Array.map (fun j -> lazy j.uj_type) jl in + let ty, cu = type_of_constant_knowing_parameters env cst paramstyp in let () = check_constraints cu env in ty +let judge_of_constant env cst = + judge_of_constant_knowing_parameters env cst [||] + let type_of_projection env (cst,u) = let cb = lookup_constant cst env in match cb.const_proj with diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index 0ac6a4e4a..e89bbf0d9 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -300,7 +300,7 @@ let typecheck_inductive env ctx mie = Universe.pr defu ++ Pp.str " declared for inductive type, inferred level is " ++ Universe.pr infu) in - (id,cn,lc,(sign,(not is_natural,full_arity,defu)))) + (id,cn,lc,(sign,RegularArity (not is_natural,full_arity,defu)))) inds in (env_arities, params, inds) @@ -615,9 +615,13 @@ let allowed_sorts is_smashed s = (* - all_sorts in case of small, unitary Prop (not smashed) *) (* - logical_sorts in case of large, unitary Prop (smashed) *) +let arity_conclusion = function + | RegularArity (_, c, _) -> c + | TemplateArity s -> mkType s.template_level + let fold_inductive_blocks f = Array.fold_left (fun acc (_,_,lc,(arsign,ar)) -> - f (Array.fold_left f acc lc) (it_mkProd_or_LetIn (pi2 ar) arsign)) + f (Array.fold_left f acc lc) (it_mkProd_or_LetIn (arity_conclusion ar) arsign)) let used_section_variables env inds = let ids = fold_inductive_blocks @@ -675,12 +679,14 @@ let build_inductive env p ctx env_ar params kn isrecord isfinite inds nmr recarg splayed_lc in (* Elimination sorts *) let arkind,kelim = - let (info,ar,defs) = ar_kind in - let s = sort_of_univ defs in - let kelim = allowed_sorts info s in - { mind_user_arity = ar; - mind_sort = s; - }, kelim in + match ar_kind with + | TemplateArity ar -> TemplateArity ar, all_sorts + | RegularArity (info,ar,defs) -> + let s = sort_of_univ defs in + let kelim = allowed_sorts info s in + let ar = RegularArity + { mind_user_arity = ar; mind_sort = s; } in + ar, kelim in (* Assigning VM tags to constructors *) let nconst, nblock = ref 0, ref 0 in let transf num = diff --git a/kernel/inductive.ml b/kernel/inductive.ml index e57b0b4ad..9862ffd3e 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -152,30 +152,93 @@ let sort_as_univ = function | Prop Null -> Universe.type0m | Prop Pos -> Universe.type0 +(* Template polymorphism *) + let cons_subst u su subst = try (u, Universe.sup su (List.assoc_f Universe.eq u subst)) :: List.remove_assoc_f Universe.eq u subst with Not_found -> (u, su) :: subst +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 (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,[] + | [], _, _ -> + assert false + 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 level = subst_large_constraints subst ar.template_level in + let ty = + (* Singleton type not containing types are interpretable in Prop *) + if is_type0m_univ level then prop_sort + (* Non singleton type not containing types are interpretable in Set *) + else if is_type0_univ level then set_sort + (* This is a Type with constraints *) + else Type level + in + (ctx, ty) + (* Type of an inductive type *) -let type_of_inductive_gen env ((mib,mip),u) = - let subst = make_inductive_subst mib u in - (subst_univs_constr subst mip.mind_arity.mind_user_arity, subst) +let type_of_inductive_gen ?(polyprop=true) env ((mib,mip),u) paramtyps = + match mip.mind_arity with + | RegularArity a -> + let subst = make_inductive_subst mib u in + (subst_univs_constr subst a.mind_user_arity, subst) + | TemplateArity ar -> + let ctx = List.rev mip.mind_arity_ctxt in + let ctx,s = instantiate_universes env ctx ar paramtyps in + (* The Ocaml extraction cannot handle (yet?) "Prop-polymorphism", i.e. + the situation where a non-Prop singleton inductive becomes Prop + when applied to Prop params *) + if not polyprop && not (is_type0m_univ ar.template_level) && is_prop_sort s + then raise (SingletonInductiveBecomesProp mip.mind_typename); + mkArity (List.rev ctx,s), Univ.LMap.empty let type_of_inductive env pind = - fst (type_of_inductive_gen env pind) + fst (type_of_inductive_gen env pind [||]) let constrained_type_of_inductive env ((mib,mip),u as pind) = - let ty, subst = type_of_inductive_gen env pind in + let ty, subst = type_of_inductive_gen env pind [||] in let cst = instantiate_inductive_constraints mib subst in (ty, cst) let type_of_inductive_knowing_parameters env ?(polyprop=false) mip args = - type_of_inductive env mip + fst (type_of_inductive_gen env mip args) (* The max of an array of universes *) @@ -248,7 +311,9 @@ let local_rels ctxt = (* Get type of inductive, with parameters instantiated *) let inductive_sort_family mip = - family_of_sort mip.mind_arity.mind_sort + match mip.mind_arity with + | RegularArity s -> family_of_sort s.mind_sort + | TemplateArity _ -> InType let mind_arity mip = mip.mind_arity_ctxt, inductive_sort_family mip diff --git a/kernel/inductive.mli b/kernel/inductive.mli index c4a7452f0..a403003e2 100644 --- a/kernel/inductive.mli +++ b/kernel/inductive.mli @@ -109,6 +109,9 @@ exception SingletonInductiveBecomesProp of Id.t val max_inductive_sort : sorts array -> universe +val instantiate_universes : env -> rel_context -> + template_arity -> constr Lazy.t array -> rel_context * sorts + (** {6 Debug} *) type size = Large | Strict diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml index 2c093939a..56e94ba0d 100644 --- a/kernel/subtyping.ml +++ b/kernel/subtyping.ml @@ -277,8 +277,8 @@ let check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2 = let cb1 = Declareops.subst_const_body subst1 cb1 in let cb2 = Declareops.subst_const_body subst2 cb2 in (* Start by checking types*) - let typ1 = cb1.const_type in - let typ2 = cb2.const_type in + let typ1 = Typeops.type_of_constant_type env cb1.const_type in + let typ2 = Typeops.type_of_constant_type env cb2.const_type in let cst = check_type cst env typ1 typ2 in (* Now we check the bodies: - A transparent constant can only be implemented by a compatible @@ -309,7 +309,7 @@ let check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2 = let arity1,cst1 = constrained_type_of_inductive env ((mind1,mind1.mind_packets.(i)),u1) in let cst2 = UContext.constraints (Future.force cb2.const_universes) in - let typ2 = cb2.const_type in + let typ2 = Typeops.type_of_constant_type env cb2.const_type in let cst = Constraint.union cst (Constraint.union cst1 cst2) in let error = NotConvertibleTypeField (env, arity1, typ2) in check_conv error cst infer_conv_leq env arity1 typ2 @@ -324,7 +324,7 @@ let check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2 = let u1 = inductive_instance mind1 in let ty1,cst1 = constrained_type_of_constructor (cstr,u1) (mind1,mind1.mind_packets.(i)) in let cst2 = UContext.constraints (Future.force cb2.const_universes) in - let ty2 = cb2.const_type in + let ty2 = Typeops.type_of_constant_type env cb2.const_type in let cst = Constraint.union cst (Constraint.union cst1 cst2) in let error = NotConvertibleTypeField (env, ty1, ty2) in check_conv error cst infer_conv env ty1 ty2 diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index a7f2125a7..c655e2f33 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -29,17 +29,20 @@ let prerr_endline = if debug then prerr_endline else fun _ -> () let constrain_type env j poly = function - | `None -> j.uj_type + | `None -> + if not poly then (* Old-style polymorphism *) + make_polymorphic_if_constant_for_ind env j + else RegularArity j.uj_type | `Some t -> let tj = infer_type env t in let _ = judge_of_cast env j DEFAULTcast tj in assert (eq_constr t tj.utj_val); - t + RegularArity t | `SomeWJ (t, tj) -> let tj = infer_type env t in let _ = judge_of_cast env j DEFAULTcast tj in assert (eq_constr t tj.utj_val); - t + RegularArity t let map_option_typ = function None -> `None | Some x -> `Some x @@ -72,12 +75,12 @@ let handle_side_effects env body side_eff = | Undef _ -> assert false | Def b -> let b = Mod_subst.force_constr b in - let b_ty = cb.const_type in + let b_ty = Typeops.type_of_constant_type env cb.const_type in let t = sub c 1 (Vars.lift 1 t) in mkLetIn (cname c, b, b_ty, t) | OpaqueDef b -> let b = Opaqueproof.force_proof b in - let b_ty = cb.const_type in + let b_ty = Typeops.type_of_constant_type env cb.const_type in let t = sub c 1 (Vars.lift 1 t) in mkApp (mkLambda (cname c, b_ty, t), [|b|]) in List.fold_right fix_body cbl t @@ -98,7 +101,7 @@ let infer_declaration env kn dcl = let env = push_context uctx env in let j = infer env t in let t = hcons_constr (Typeops.assumption_of_judgment env j) in - Undef nl, t, None, poly, Future.from_val uctx, false, ctx + Undef nl, RegularArity t, None, poly, Future.from_val uctx, false, ctx | DefinitionEntry ({ const_entry_type = Some typ; const_entry_opaque = true } as c) -> let env = push_context (Future.join c.const_entry_universes) env in (* FIXME *) @@ -113,7 +116,7 @@ let infer_declaration env kn dcl = feedback_completion_typecheck feedback_id; j.uj_val, Univ.empty_constraint) in let def = OpaqueDef (Opaqueproof.create proofterm) in - def, typ, None, c.const_entry_polymorphic, c.const_entry_universes, + def, RegularArity typ, None, c.const_entry_polymorphic, c.const_entry_universes, c.const_entry_inline_code, c.const_entry_secctx | DefinitionEntry c -> let env = push_context (Future.join c.const_entry_universes) env in (* FIXME *) @@ -129,13 +132,13 @@ let infer_declaration env kn dcl = def, typ, None, c.const_entry_polymorphic, c.const_entry_universes, c.const_entry_inline_code, c.const_entry_secctx -(* let global_vars_set_constant_type env = function *) -(* | NonPolymorphicType t -> global_vars_set env t *) -(* | PolymorphicArity (ctx,_) -> *) -(* Context.fold_rel_context *) -(* (fold_rel_declaration *) -(* (fun t c -> Id.Set.union (global_vars_set env t) c)) *) -(* ctx ~init:Id.Set.empty *) +let global_vars_set_constant_type env = function + | RegularArity t -> global_vars_set env t + | TemplateArity (ctx,_) -> + Context.fold_rel_context + (fold_rel_declaration + (fun t c -> Id.Set.union (global_vars_set env t) c)) + ctx ~init:Id.Set.empty let record_aux env s1 s2 = let v = @@ -162,7 +165,7 @@ let build_constant_declaration kn env (def,typ,proj,poly,univs,inline_code,ctx) | None when not (List.is_empty context_ids) -> (* No declared section vars, and non-empty section context: we must look at the body NOW, if any *) - let ids_typ = global_vars_set env typ in + let ids_typ = global_vars_set_constant_type env typ in let ids_def = match def with | Undef _ -> Idset.empty | Def cs -> global_vars_set env (Mod_subst.force_constr cs) @@ -186,14 +189,14 @@ let build_constant_declaration kn env (def,typ,proj,poly,univs,inline_code,ctx) match def with | Undef _ as x -> x (* nothing to check *) | Def cs as x -> - let ids_typ = global_vars_set env typ in + let ids_typ = global_vars_set_constant_type env typ in let ids_def = global_vars_set env (Mod_subst.force_constr cs) in let inferred = keep_hyps env (Idset.union ids_typ ids_def) in check declared inferred; x | OpaqueDef lc -> (* In this case we can postpone the check *) OpaqueDef (Opaqueproof.iter_direct_opaque (fun c -> - let ids_typ = global_vars_set env typ in + let ids_typ = global_vars_set_constant_type env typ in let ids_def = global_vars_set env c in let inferred = keep_hyps env (Idset.union ids_typ ids_def) in check declared inferred) lc) in @@ -229,6 +232,7 @@ let translate_recipe env kn r = let translate_local_def env id centry = let def,typ,proj,poly,univs,inline_code,ctx = infer_declaration env None (DefinitionEntry centry) in + let typ = type_of_constant_type env typ in def, typ, univs (* Insertion of inductive types. *) diff --git a/kernel/typeops.ml b/kernel/typeops.ml index 09fd4cc7f..09e2fb1d5 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -113,20 +113,62 @@ let check_hyps_inclusion env c sign = (* Make a type polymorphic if an arity *) +let extract_level env p = + let _,c = dest_prod_assum env p in + match kind_of_term c with Sort (Type u) -> Some u | _ -> None + +let extract_context_levels env l = + let fold l (_, b, p) = match b with + | None -> extract_level env p :: l + | _ -> l + in + List.fold_left fold [] l + +let make_polymorphic_if_constant_for_ind env {uj_val = c; uj_type = t} = + let params, ccl = dest_prod_assum env t in + match kind_of_term ccl with + | Sort (Type u) when isInd (fst (decompose_app (whd_betadeltaiota env c))) -> + let param_ccls = extract_context_levels env params in + let s = { template_param_levels = param_ccls; template_level = u} in + TemplateArity (params,s) + | _ -> + RegularArity t + (* Type of constants *) -let type_of_constant env cst = constant_type env cst -let type_of_constant_in env cst = constant_type_in env cst -let type_of_constant_knowing_parameters env t _ = t -let type_of_constant_type env cst = cst +let type_of_constant_type_knowing_parameters env t paramtyps = + match t with + | RegularArity t -> t + | TemplateArity (sign,ar) -> + let ctx = List.rev sign in + let ctx,s = instantiate_universes env ctx ar paramtyps in + mkArity (List.rev ctx,s) + +let type_of_constant_knowing_parameters env cst paramtyps = + let ty, cu = constant_type env cst in + type_of_constant_type_knowing_parameters env ty paramtyps, cu + +let type_of_constant_type env t = + type_of_constant_type_knowing_parameters env t [||] -let judge_of_constant env (kn,u as cst) = +let type_of_constant env cst = + type_of_constant_knowing_parameters env cst [||] + +let type_of_constant_in env cst = + let ar = constant_type_in env cst in + type_of_constant_type_knowing_parameters env ar [||] + +let judge_of_constant_knowing_parameters env (kn,u as cst) jl = let c = mkConstU cst in let cb = lookup_constant kn env in let _ = check_hyps_inclusion env c cb.const_hyps in - let ty, cu = type_of_constant env cst in + let paramstyp = Array.map (fun j -> lazy j.uj_type) jl in + let ty, cu = type_of_constant_knowing_parameters env cst paramstyp in let _ = Environ.check_constraints cu env in - (make_judge c ty) + make_judge c ty + +let judge_of_constant env cst = + judge_of_constant_knowing_parameters env cst [||] let type_of_projection env (cst,u) = let cb = lookup_constant cst env in diff --git a/kernel/typeops.mli b/kernel/typeops.mli index 6bc1ce496..9747dbe83 100644 --- a/kernel/typeops.mli +++ b/kernel/typeops.mli @@ -51,10 +51,13 @@ val judge_of_relative : env -> int -> unsafe_judgment val judge_of_variable : env -> variable -> unsafe_judgment (** {6 type of a constant } *) -val judge_of_constant : env -> constant puniverses -> unsafe_judgment -(* val judge_of_constant_knowing_parameters : *) -(* env -> constant -> unsafe_judgment array -> unsafe_judgment *) +val judge_of_constant : env -> pconstant -> unsafe_judgment + +val judge_of_constant_knowing_parameters : + env -> pconstant -> unsafe_judgment array -> unsafe_judgment + +(** {6 type of an applied projection } *) val judge_of_projection : env -> Names.projection -> unsafe_judgment -> unsafe_judgment @@ -103,15 +106,20 @@ val judge_of_case : env -> case_info val type_fixpoint : env -> Name.t array -> types array -> unsafe_judgment array -> unit -val type_of_constant : env -> constant puniverses -> types constrained +val type_of_constant : env -> pconstant -> types constrained val type_of_constant_type : env -> constant_type -> types val type_of_projection : env -> Names.projection puniverses -> types -val type_of_constant_in : env -> constant puniverses -> types +val type_of_constant_in : env -> pconstant -> types -val type_of_constant_knowing_parameters : +val type_of_constant_type_knowing_parameters : env -> constant_type -> types Lazy.t array -> types +val type_of_constant_knowing_parameters : + env -> pconstant -> types Lazy.t array -> types constrained +(** Make a type polymorphic if an arity *) +val make_polymorphic_if_constant_for_ind : env -> unsafe_judgment -> + constant_type diff --git a/library/assumptions.ml b/library/assumptions.ml index 9cfe531ce..37585caa4 100644 --- a/library/assumptions.ml +++ b/library/assumptions.ml @@ -222,7 +222,7 @@ let assumptions ?(add_opaque=false) ?(add_transparent=false) st (* t *) = and add_kn kn s acc = let cb = lookup_constant kn in let do_type cst = - let ctype = cb.Declarations.const_type in + let ctype = Global.type_of_global_unsafe (Globnames.ConstRef kn) in (s,ContextObjectMap.add cst ctype acc) in let (s,acc) = diff --git a/library/declare.ml b/library/declare.ml index 820e72369..45015ac65 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -222,7 +222,8 @@ let declare_sideff se = in let ty_of cb = match cb.Declarations.const_type with - | (* Declarations.NonPolymorphicType *)t -> Some t in + | Declarations.RegularArity t -> Some t + | Declarations.TemplateArity _ -> None in let cst_of cb = let pt, opaque = pt_opaque_of cb in let ty = ty_of cb in diff --git a/library/global.ml b/library/global.ml index 16b07db25..fbba81b51 100644 --- a/library/global.ml +++ b/library/global.ml @@ -151,10 +151,16 @@ let type_of_global_unsafe r = match r with | VarRef id -> Environ.named_type id env | ConstRef c -> - let cb = Environ.lookup_constant c env in cb.Declarations.const_type + let cb = Environ.lookup_constant c env in + Typeops.type_of_constant_type env cb.Declarations.const_type | IndRef ind -> - let (mib, oib) = Inductive.lookup_mind_specif env ind in - oib.Declarations.mind_arity.Declarations.mind_user_arity + let (mib, oib as specif) = Inductive.lookup_mind_specif env ind in + let inst = + if mib.Declarations.mind_polymorphic then + Univ.UContext.instance mib.Declarations.mind_universes + else Univ.Instance.empty + in + Inductive.type_of_inductive env (specif, inst) | ConstructRef cstr -> let (mib,oib as specif) = Inductive.lookup_mind_specif env (inductive_of_constructor cstr) in let inst = Univ.UContext.instance mib.Declarations.mind_universes in @@ -169,13 +175,13 @@ let type_of_global_in_context env r = let univs = if cb.const_polymorphic then Future.force cb.const_universes else Univ.UContext.empty - in cb.Declarations.const_type, univs + in Typeops.type_of_constant_type env cb.Declarations.const_type, univs | IndRef ind -> - let (mib, oib) = Inductive.lookup_mind_specif env ind in + let (mib, oib as specif) = Inductive.lookup_mind_specif env ind in let univs = if mib.mind_polymorphic then mib.mind_universes else Univ.UContext.empty - in oib.Declarations.mind_arity.Declarations.mind_user_arity, univs + in Inductive.type_of_inductive env (specif, Univ.UContext.instance univs), univs | ConstructRef cstr -> let (mib,oib as specif) = Inductive.lookup_mind_specif env (inductive_of_constructor cstr) in let univs = diff --git a/library/impargs.ml b/library/impargs.ml index 5a44b5bdb..f0292762f 100644 --- a/library/impargs.ml +++ b/library/impargs.ml @@ -403,7 +403,7 @@ let compute_semi_auto_implicits env f manual t = let compute_constant_implicits flags manual cst = let env = Global.env () in let cb = Environ.lookup_constant cst env in - let ty = cb.const_type in + let ty = Typeops.type_of_constant_type env cb.const_type in let impls = compute_semi_auto_implicits env flags manual ty in impls (* match cb.const_proj with *) diff --git a/library/universes.ml b/library/universes.ml index c7009b400..73a0b2b1c 100644 --- a/library/universes.ml +++ b/library/universes.ml @@ -144,17 +144,21 @@ let type_of_reference env r = | VarRef id -> Environ.named_type id env, ContextSet.empty | ConstRef c -> let cb = Environ.lookup_constant c env in + let ty = Typeops.type_of_constant_type env cb.const_type in if cb.const_polymorphic then let (inst, subst), ctx = fresh_instance_from (Future.force cb.const_universes) in - Vars.subst_univs_constr subst cb.const_type, ctx - else cb.const_type, ContextSet.empty + Vars.subst_univs_constr subst ty, ctx + else ty, ContextSet.empty | IndRef ind -> - let (mib, oib) = Inductive.lookup_mind_specif env ind in + let (mib, oib as specif) = Inductive.lookup_mind_specif env ind in if mib.mind_polymorphic then let (inst, subst), ctx = fresh_instance_from mib.mind_universes in - Vars.subst_univs_constr subst oib.mind_arity.mind_user_arity, ctx - else oib.mind_arity.mind_user_arity, ContextSet.empty + let ty = Inductive.type_of_inductive env (specif, inst) in + ty, ctx + else + let ty = Inductive.type_of_inductive env (specif, Univ.Instance.empty) in + ty, ContextSet.empty | ConstructRef cstr -> let (mib,oib as specif) = Inductive.lookup_mind_specif env (inductive_of_constructor cstr) in if mib.mind_polymorphic then diff --git a/plugins/Derive/g_derive.ml4 b/plugins/Derive/g_derive.ml4 index 9137c3d28..c7db26fb8 100644 --- a/plugins/Derive/g_derive.ml4 +++ b/plugins/Derive/g_derive.ml4 @@ -8,7 +8,7 @@ (*i camlp4deps: "grammar/grammar.cma" i*) -let classify_derive_command _ = Vernacexpr.(VtStartProof ("Classic",Doesn'tGuaranteeOpacity,[]),VtLater) +let classify_derive_command _ = Vernacexpr.(VtStartProof ("Classic",Doesn'tGuaranteeOpacity,[], false),VtLater) VERNAC COMMAND EXTEND Derive CLASSIFIED BY classify_derive_command | [ "Derive" ident(f) "From" constr(init) "Upto" constr(r) "As" ident(lemma) ] -> diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml index 74de31368..791294902 100644 --- a/plugins/extraction/extract_env.ml +++ b/plugins/extraction/extract_env.ml @@ -131,7 +131,7 @@ end exception Impossible let check_arity env cb = - let t = cb.const_type in + let t = Typeops.type_of_constant_type env cb.const_type in if Reduction.is_arity env t then raise Impossible let check_fix env cb i = diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml index 5b79f6d78..f7b677a1e 100644 --- a/plugins/extraction/extraction.ml +++ b/plugins/extraction/extraction.ml @@ -202,17 +202,15 @@ let parse_ind_args si args relmax = let oib_equal o1 o2 = Id.equal o1.mind_typename o2.mind_typename && List.equal eq_rel_declaration o1.mind_arity_ctxt o2.mind_arity_ctxt && - begin match o1.mind_arity, o2.mind_arity with - (* | Monomorphic {mind_user_arity=c1; mind_sort=s1}, *) - (* Monomorphic {mind_user_arity=c2; mind_sort=s2} -> *) - (* eq_constr c1 c2 && Sorts.equal s1 s2 *) - (* | ma1, ma2 -> Pervasives.(=) ma1 ma2 (\** FIXME: this one is surely wrong *\) end && *) - (* Array.equal Id.equal o1.mind_consnames o2.mind_consnames *) - | {mind_user_arity=c1; mind_sort=s1}, - {mind_user_arity=c2; mind_sort=s2} -> - eq_constr c1 c2 && Sorts.equal s1 s2 - end && - Array.equal Id.equal o1.mind_consnames o2.mind_consnames + begin + match o1.mind_arity, o2.mind_arity with + | RegularArity {mind_user_arity=c1; mind_sort=s1}, RegularArity {mind_user_arity=c2; mind_sort=s2} -> + eq_constr c1 c2 && Sorts.equal s1 s2 + | {mind_user_arity=c1; mind_sort=s1}, + {mind_user_arity=c2; mind_sort=s2} -> + eq_constr c1 c2 && Sorts.equal s1 s2 + end && + Array.equal Id.equal o1.mind_consnames o2.mind_consnames let mib_equal m1 m2 = Array.equal oib_equal m1.mind_packets m1.mind_packets && @@ -525,7 +523,8 @@ and mlt_env env r = match r with | _ -> None with Not_found -> let cb = Environ.lookup_constant kn env in - let typ = cb.const_type (* FIXME not sure if we should instantiate univs here *) in + let typ = Typeops.type_of_constant_type env cb.const_type + (* FIXME not sure if we should instantiate univs here *) in match cb.const_body with | Undef _ | OpaqueDef _ -> None | Def l_body -> @@ -553,7 +552,7 @@ let record_constant_type env kn opt_typ = lookup_type kn with Not_found -> let typ = match opt_typ with - | None -> (lookup_constant kn env).const_type + | None -> Typeops.type_of_constant_type env (lookup_constant kn env).const_type | Some typ -> typ in let mlt = extract_type env [] 1 typ [] in let schema = (type_maxvar mlt, mlt) @@ -976,7 +975,7 @@ let extract_fixpoint env vkn (fi,ti,ci) = let extract_constant env kn cb = let r = ConstRef kn in - let typ = cb.const_type in + let typ = Global.type_of_global_unsafe r in let warn_info () = if not (is_custom r) then add_info_axiom r in let warn_log () = if not (constant_has_body cb) then add_log_axiom r in @@ -1023,7 +1022,7 @@ let extract_constant env kn cb = let extract_constant_spec env kn cb = let r = ConstRef kn in - let typ = cb.const_type in + let typ = Global.type_of_global_unsafe r in match flag_of_type env typ with | (Logic, TypeScheme) -> Stype (r, [], Some (Tdummy Ktype)) | (Logic, Default) -> Sval (r, Tdummy Kother) diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml index 133f4ada9..c48873c80 100644 --- a/plugins/extraction/table.ml +++ b/plugins/extraction/table.ml @@ -816,7 +816,7 @@ let extract_constant_inline inline r ids s = match g with | ConstRef kn -> let env = Global.env () in - let typ = (Environ.lookup_constant kn env).const_type in + let typ = Global.type_of_global_unsafe (ConstRef kn) in let typ = Reduction.whd_betadeltaiota env typ in if Reduction.is_arity env typ then begin diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index a3af23dcd..f0c7b5a7f 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -964,7 +964,7 @@ let generate_equation_lemma fnames f fun_num nb_params nb_args rec_args_num = let eq_rhs = nf_betaiotazeta (mkApp(compose_lam params f_body_with_params_and_other_fun,Array.init (nb_params + nb_args) (fun i -> mkRel(nb_params + nb_args - i)))) in (* observe (str "eq_rhs " ++ pr_lconstr eq_rhs); *) let type_ctxt,type_of_f = decompose_prod_n_assum (nb_params + nb_args) - ((*FIXME*)f_def.const_type) in + (Typeops.type_of_constant_type (Global.env ()) (*FIXME*)f_def.const_type) in let eqn = mkApp(Lazy.force eq,[|type_of_f;eq_lhs;eq_rhs|]) in let lemma_type = it_mkProd_or_LetIn eqn type_ctxt in let f_id = Label.to_id (con_label (fst (destConst f))) in diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index d6ad5575b..49f833590 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -771,7 +771,7 @@ let make_graph (f_ref:global_reference) = with_full_print (fun () -> (Constrextern.extern_constr false env body, Constrextern.extern_type false env - ((*FIXNE*) c_body.const_type) + ((*FIXNE*) Typeops.type_of_constant_type env c_body.const_type) ) ) () diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml index d0497f6f6..2e524a35f 100644 --- a/plugins/funind/merge.ml +++ b/plugins/funind/merge.ml @@ -139,7 +139,7 @@ let showind (id:Id.t) = print_string (string_of_name nm^":"); prconstr tp; print_string "\n") ib1.mind_arity_ctxt; - Printf.printf "arity :"; prconstr ib1.mind_arity.mind_user_arity; + Printf.printf "arity :"; prconstr (Inductiveops.type_of_inductive (Global.env ()) ind1); Array.iteri (fun i x -> Printf.printf"type constr %d :" i ; prconstr x) ib1.mind_user_lc diff --git a/plugins/xml/xmlcommand.ml b/plugins/xml/xmlcommand.ml index 3d655920b..8f47859da 100644 --- a/plugins/xml/xmlcommand.ml +++ b/plugins/xml/xmlcommand.ml @@ -380,7 +380,7 @@ let print internal glob_ref kind xml_library_root = let val0 = Declareops.body_of_constant cb in let typ = cb.Declarations.const_type in let hyps = cb.Declarations.const_hyps in - let typ = (* Typeops.type_of_constant_type (Global.env()) *) typ in + let typ = Typeops.type_of_constant_type (Global.env()) typ in Cic2acic.Constant kn,mk_constant_obj id val0 typ variables hyps | Globnames.IndRef (kn,_) -> let mib = Global.lookup_mind kn in diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index 7e4d37b2e..0b7cd89f2 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -451,9 +451,44 @@ let arity_of_case_predicate env (ind,params) dep k = (* Inferring the sort of parameters of a polymorphic inductive type knowing the sort of the conclusion *) -let type_of_inductive_knowing_conclusion env ((mib,mip),u) conclty = - let subst = Inductive.make_inductive_subst mib u in - subst_univs_constr subst mip.mind_arity.mind_user_arity + +(* Compute the inductive argument types: replace the sorts + that appear in the type of the inductive by the sort of the + conclusion, and the other ones by fresh universes. *) +let rec instantiate_universes env evdref scl is = function + | (_,Some _,_ as d)::sign, exp -> + d :: instantiate_universes env evdref scl is (sign, exp) + | d::sign, None::exp -> + d :: instantiate_universes env evdref scl is (sign, exp) + | (na,None,ty)::sign, Some u::exp -> + let ctx,_ = Reduction.dest_arity env ty in + let s = + (* Does the sort of parameter [u] appear in (or equal) + the sort of inductive [is] ? *) + if univ_depends u is then + scl (* constrained sort: replace by scl *) + else + (* unconstriained sort: replace by fresh universe *) + let evm, s = Evd.new_sort_variable Evd.univ_flexible !evdref in + evdref := evm; s + in + (na,None,mkArity(ctx,s)):: instantiate_universes env evdref scl is (sign, exp) + | sign, [] -> sign (* Uniform parameters are exhausted *) + | [], _ -> assert false + +let type_of_inductive_knowing_conclusion env sigma ((mib,mip),u) conclty = + match mip.mind_arity with + | RegularArity s -> + let subst = Inductive.make_inductive_subst mib u in + sigma, subst_univs_constr subst s.mind_user_arity + | TemplateArity ar -> + let _,scl = Reduction.dest_arity env conclty in + let ctx = List.rev mip.mind_arity_ctxt in + let evdref = ref sigma in + let ctx = + instantiate_universes + env evdref scl ar.template_level (ctx,ar.template_param_levels) in + !evdref, mkArity (List.rev ctx,scl) (***********************************************) (* Guard condition *) diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli index 39451ec05..34ddce72b 100644 --- a/pretyping/inductiveops.mli +++ b/pretyping/inductiveops.mli @@ -142,7 +142,7 @@ i*) (********************) val type_of_inductive_knowing_conclusion : - env -> Inductive.mind_specif puniverses -> types -> types + env -> evar_map -> Inductive.mind_specif puniverses -> types -> evar_map * types (********************) val control_only_guard : env -> types -> unit diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml index 31487125a..ccb9420fd 100644 --- a/pretyping/retyping.ml +++ b/pretyping/retyping.ml @@ -190,7 +190,7 @@ let retype ?(polyprop=true) sigma = with Reduction.NotArity -> retype_error NotAnArity) | Const cst -> let t = constant_type_in env cst in - (try Typeops.type_of_constant_knowing_parameters env t argtyps + (try Typeops.type_of_constant_type_knowing_parameters env t argtyps with Reduction.NotArity -> retype_error NotAnArity) | Var id -> type_of_var env id | Construct cstr -> type_of_constructor env cstr @@ -211,13 +211,13 @@ let type_of_global_reference_knowing_conclusion env sigma c conclty = match kind_of_term c with | Ind (ind,u) -> let spec = Inductive.lookup_mind_specif env ind in - type_of_inductive_knowing_conclusion env (spec,u) conclty + type_of_inductive_knowing_conclusion env sigma (spec,u) conclty | Const cst -> let t = constant_type_in env cst in (* TODO *) - Typeops.type_of_constant_knowing_parameters env t [||] - | Var id -> type_of_var env id - | Construct cstr -> type_of_constructor env cstr + sigma, Typeops.type_of_constant_type_knowing_parameters env t [||] + | Var id -> sigma, type_of_var env id + | Construct cstr -> sigma, type_of_constructor env cstr | _ -> assert false (* Profiling *) diff --git a/pretyping/retyping.mli b/pretyping/retyping.mli index fc1dd3564..b8b458555 100644 --- a/pretyping/retyping.mli +++ b/pretyping/retyping.mli @@ -41,4 +41,4 @@ val type_of_global_reference_knowing_parameters : env -> evar_map -> constr -> constr array -> types val type_of_global_reference_knowing_conclusion : - env -> evar_map -> constr -> types -> types + env -> evar_map -> constr -> types -> evar_map * types diff --git a/pretyping/typing.ml b/pretyping/typing.ml index bd559ddd5..cc473bd86 100644 --- a/pretyping/typing.ml +++ b/pretyping/typing.ml @@ -27,7 +27,7 @@ let meta_type evd mv = let constant_type_knowing_parameters env cst jl = let paramstyp = Array.map (fun j -> lazy j.uj_type) jl in - type_of_constant_knowing_parameters env (constant_type_in env cst) paramstyp + type_of_constant_type_knowing_parameters env (constant_type_in env cst) paramstyp let inductive_type_knowing_parameters env (ind,u) jl = let mspec = lookup_mind_specif env ind in diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml index 16eeaa293..2cf730f11 100644 --- a/pretyping/vnorm.ml +++ b/pretyping/vnorm.ml @@ -98,7 +98,8 @@ let construct_of_constr_block = construct_of_constr false let constr_type_of_idkey env idkey = match idkey with | ConstKey cst -> - mkConst cst, (Environ.lookup_constant cst env).const_type + let const_type = (Environ.lookup_constant cst env).const_type in + mkConst cst, Typeops.type_of_constant_type env const_type | VarKey id -> let (_,_,ty) = lookup_named id env in mkVar id, ty diff --git a/printing/prettyp.ml b/printing/prettyp.ml index e885f5978..87d7e0980 100644 --- a/printing/prettyp.ml +++ b/printing/prettyp.ml @@ -371,7 +371,8 @@ let print_body = function let print_typed_body (val_0,typ) = (print_body val_0 ++ fnl () ++ str " : " ++ pr_ltype typ) -let ungeneralized_type_of_constant_type t = t +let ungeneralized_type_of_constant_type t = + Typeops.type_of_constant_type (Global.env ()) t let print_constant with_values sep sp = let cb = Global.lookup_constant sp in diff --git a/printing/printer.ml b/printing/printer.ml index 91156e21f..cb10f9661 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -755,16 +755,16 @@ let print_constructors envpar names types = hv 0 (str " " ++ pc) let build_ind_type env mip = - mip.mind_arity.mind_user_arity + Inductive.type_of_inductive env mip let print_one_inductive env mib ((_,i) as ind) = let mip = mib.mind_packets.(i) in let params = mib.mind_params_ctxt in let args = extended_rel_list 0 params in - let arity = hnf_prod_applist env (build_ind_type env mip) args in let u = if mib.mind_polymorphic then Univ.UContext.instance mib.mind_universes else Univ.Instance.empty in + let arity = hnf_prod_applist env (build_ind_type env ((mib,mip),u)) args in let cstrtypes = Inductive.type_of_constructors (ind,u) (mib,mip) in let cstrtypes = Array.map (fun c -> hnf_prod_applist env c args) cstrtypes in let envpar = push_rel_context params env in @@ -802,7 +802,7 @@ let print_record env mind mib = let u = if mib.mind_polymorphic then Univ.UContext.instance mib.mind_universes else Univ.Instance.empty in - let arity = hnf_prod_applist env (build_ind_type env mip) args in + let arity = hnf_prod_applist env (build_ind_type env ((mib,mip),u)) args in let cstrtypes = Inductive.type_of_constructors ((mind,0),u) (mib,mip) in let cstrtype = hnf_prod_applist env cstrtypes.(0) args in let fields = get_fields cstrtype in diff --git a/printing/printmod.ml b/printing/printmod.ml index da5546bac..8d05e2d6d 100644 --- a/printing/printmod.ml +++ b/printing/printmod.ml @@ -146,7 +146,8 @@ let print_body is_impl env mp (l,body) = | None -> mt () | Some env -> str " :" ++ spc () ++ - hov 0 (Printer.pr_ltype_env env cb.const_type) ++ + hov 0 (Printer.pr_ltype_env env + (Typeops.type_of_constant_type env cb.const_type)) ++ (match cb.const_body with | Def l when is_impl -> spc () ++ diff --git a/proofs/logic.ml b/proofs/logic.ml index 02f3a16d8..fb88b8754 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -382,10 +382,11 @@ let rec mk_refgoals sigma goal goalacc conclty trm = match kind_of_term f with | Ind _ | Const _ when (isInd f || has_polymorphic_type (fst (destConst f))) -> + let sigma, ty = (* Sort-polymorphism of definition and inductive types *) - goalacc, - type_of_global_reference_knowing_conclusion env sigma f conclty, - sigma, f + type_of_global_reference_knowing_conclusion env sigma f conclty + in + goalacc, ty, sigma, f | _ -> mk_hdgoals sigma goal goalacc f in diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml index 55475a378..e17038a4f 100644 --- a/toplevel/discharge.ml +++ b/toplevel/discharge.ml @@ -69,23 +69,34 @@ let abstract_inductive hyps nparams inds = in (params',ind'') let refresh_polymorphic_type_of_inductive (_,mip) = - mip.mind_arity.mind_user_arity + match mip.mind_arity with + | RegularArity s -> s.mind_user_arity, Univ.ContextSet.empty + | TemplateArity ar -> + let ctx = List.rev mip.mind_arity_ctxt in + let univ, uctx = Universes.new_global_univ () in + mkArity (List.rev ctx, Type univ), uctx let process_inductive (sechyps,abs_ctx) modlist mib = let nparams = mib.mind_nparams in + let univctx = ref Univ.ContextSet.empty in let inds = Array.map_to_list (fun mip -> - let arity = expmod_constr modlist (refresh_polymorphic_type_of_inductive (mib,mip)) in - let lc = Array.map (expmod_constr modlist) mip.mind_user_lc in - (mip.mind_typename, - arity, - Array.to_list mip.mind_consnames, - Array.to_list lc)) + let ty, uctx = refresh_polymorphic_type_of_inductive (mib,mip) in + let () = univctx := Univ.ContextSet.union uctx !univctx in + let arity = expmod_constr modlist ty in + let lc = Array.map (expmod_constr modlist) mip.mind_user_lc in + (mip.mind_typename, + arity, + Array.to_list mip.mind_consnames, + Array.to_list lc)) mib.mind_packets in let sechyps' = map_named_context (expmod_constr modlist) sechyps in let (params',inds') = abstract_inductive sechyps' nparams inds in - let univs = Univ.UContext.union abs_ctx mib.mind_universes in + let univs = Univ.UContext.union abs_ctx + (Univ.UContext.union (Univ.ContextSet.to_context !univctx) + mib.mind_universes) + in { mind_entry_record = mib.mind_record <> None; mind_entry_finite = mib.mind_finite; mind_entry_params = params'; diff --git a/toplevel/search.ml b/toplevel/search.ml index 1535ae617..37403504d 100644 --- a/toplevel/search.ml +++ b/toplevel/search.ml @@ -60,14 +60,15 @@ let iter_declarations (fn : global_reference -> env -> constr -> unit) = with Not_found -> (* we are in a section *) () end | "CONSTANT" -> let cst = Global.constant_of_delta_kn kn in - let typ, _ = Environ.constant_type_in_ctx env cst in - fn (ConstRef cst) env typ + let gr = ConstRef cst in + let typ = Global.type_of_global_unsafe gr in + fn gr env typ | "INDUCTIVE" -> let mind = Global.mind_of_delta_kn kn in let mib = Global.lookup_mind mind in let iter_packet i mip = let ind = (mind, i) in - let i = (ind, Univ.UContext.instance mib.mind_universes) in + let i = (ind, Inductive.inductive_instance mib) in let typ = Inductiveops.type_of_inductive env i in let () = fn (IndRef ind) env typ in let len = Array.length mip.mind_user_lc in diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 02e59a227..67ca1b666 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -252,7 +252,8 @@ let print_namespace ns = print_list pr_id qn in let print_constant k body = - let t = body.Declarations.const_type in + (* FIXME: universes *) + let t = Typeops.type_of_constant_type (Global.env ()) body.Declarations.const_type in print_kn k ++ str":" ++ spc() ++ Printer.pr_type t in let matches mp = match match_modulepath ns mp with |