aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
-rw-r--r--kernel/cooking.ml29
-rw-r--r--kernel/declarations.mli23
-rw-r--r--kernel/declareops.ml130
-rw-r--r--kernel/declareops.mli5
-rw-r--r--kernel/environ.ml17
-rw-r--r--kernel/environ.mli8
-rw-r--r--kernel/fast_typeops.ml33
-rw-r--r--kernel/indtypes.ml22
-rw-r--r--kernel/inductive.ml79
-rw-r--r--kernel/inductive.mli3
-rw-r--r--kernel/subtyping.ml8
-rw-r--r--kernel/term_typing.ml38
-rw-r--r--kernel/typeops.ml56
-rw-r--r--kernel/typeops.mli20
-rw-r--r--library/assumptions.ml2
-rw-r--r--library/declare.ml3
-rw-r--r--library/global.ml18
-rw-r--r--library/impargs.ml2
-rw-r--r--library/universes.ml14
-rw-r--r--plugins/Derive/g_derive.ml42
-rw-r--r--plugins/extraction/extract_env.ml2
-rw-r--r--plugins/extraction/extraction.ml29
-rw-r--r--plugins/extraction/table.ml2
-rw-r--r--plugins/funind/functional_principles_proofs.ml2
-rw-r--r--plugins/funind/indfun.ml2
-rw-r--r--plugins/funind/merge.ml2
-rw-r--r--plugins/xml/xmlcommand.ml2
-rw-r--r--pretyping/inductiveops.ml41
-rw-r--r--pretyping/inductiveops.mli2
-rw-r--r--pretyping/retyping.ml10
-rw-r--r--pretyping/retyping.mli2
-rw-r--r--pretyping/typing.ml2
-rw-r--r--pretyping/vnorm.ml3
-rw-r--r--printing/prettyp.ml3
-rw-r--r--printing/printer.ml6
-rw-r--r--printing/printmod.ml3
-rw-r--r--proofs/logic.ml7
-rw-r--r--toplevel/discharge.ml27
-rw-r--r--toplevel/search.ml7
-rw-r--r--toplevel/vernacentries.ml3
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