aboutsummaryrefslogtreecommitdiff
path: root/kernel
diff options
context:
space:
mode:
Diffstat (limited to 'kernel')
-rw-r--r--kernel/cooking.ml23
-rw-r--r--kernel/cooking.mli2
-rw-r--r--kernel/declarations.ml4
-rw-r--r--kernel/declareops.ml16
-rw-r--r--kernel/environ.ml21
-rw-r--r--kernel/environ.mli10
-rw-r--r--kernel/mod_typing.ml4
-rw-r--r--kernel/subtyping.ml4
-rw-r--r--kernel/term_typing.ml34
-rw-r--r--kernel/typeops.ml61
-rw-r--r--kernel/typeops.mli16
11 files changed, 30 insertions, 165 deletions
diff --git a/kernel/cooking.ml b/kernel/cooking.ml
index 63614e20f7..80d41847cd 100644
--- a/kernel/cooking.ml
+++ b/kernel/cooking.ml
@@ -18,7 +18,6 @@ open Util
open Names
open Term
open Declarations
-open Environ
open Univ
module NamedDecl = Context.Named.Declaration
@@ -153,7 +152,7 @@ type inline = bool
type result = {
cook_body : constant_def;
- cook_type : constant_type;
+ cook_type : types;
cook_proj : projection_body option;
cook_universes : constant_universes;
cook_inline : inline;
@@ -167,11 +166,6 @@ let on_body ml hy f = function
OpaqueDef (Opaqueproof.discharge_direct_opaque ~cook_constr:f
{ Opaqueproof.modlist = ml; abstract = hy } o)
-let constr_of_def otab = function
- | Undef _ -> assert false
- | Def cs -> Mod_subst.force_constr cs
- | OpaqueDef lc -> Opaqueproof.force_proof otab lc
-
let expmod_constr_subst cache modlist subst c =
let c = expmod_constr cache modlist c in
Vars.subst_univs_level_constr subst c
@@ -220,17 +214,7 @@ let cook_constant ~hcons env { from = cb; info } =
List.filter (fun decl' -> not (Id.equal (NamedDecl.get_id decl) (NamedDecl.get_id decl')))
hyps)
hyps ~init:cb.const_hyps in
- let typ = match cb.const_type with
- | RegularArity t ->
- let typ =
- abstract_constant_type (expmod t) hyps in
- RegularArity typ
- | TemplateArity (ctx,s) ->
- let t = mkArity (ctx,Type s.template_level) in
- let typ = abstract_constant_type (expmod t) hyps in
- let j = make_judge (constr_of_def (opaque_tables env) body) typ in
- Typeops.make_polymorphic_if_constant_for_ind env j
- in
+ let typ = abstract_constant_type (expmod cb.const_type) hyps in
let projection pb =
let c' = abstract_constant_body (expmod pb.proj_body) hyps in
let etab = abstract_constant_body (expmod (fst pb.proj_eta)) hyps in
@@ -244,9 +228,6 @@ let cook_constant ~hcons env { from = cb; info } =
| _ -> 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_eta = etab, etat;
diff --git a/kernel/cooking.mli b/kernel/cooking.mli
index f386fd9362..6d1b776c05 100644
--- a/kernel/cooking.mli
+++ b/kernel/cooking.mli
@@ -18,7 +18,7 @@ type inline = bool
type result = {
cook_body : constant_def;
- cook_type : constant_type;
+ cook_type : types;
cook_proj : projection_body option;
cook_universes : constant_universes;
cook_inline : inline;
diff --git a/kernel/declarations.ml b/kernel/declarations.ml
index f35438dfc4..9697b0b8b2 100644
--- a/kernel/declarations.ml
+++ b/kernel/declarations.ml
@@ -36,8 +36,6 @@ type ('a, 'b) declaration_arity =
| RegularArity of 'a
| TemplateArity of 'b
-type constant_type = (types, Context.Rel.t * template_arity) declaration_arity
-
(** Inlining level of parameters at functor applications.
None means no inlining *)
@@ -83,7 +81,7 @@ type typing_flags = {
type constant_body = {
const_hyps : Context.Named.t; (** New: younger hyp at top *)
const_body : constant_def;
- const_type : constant_type;
+ const_type : types;
const_body_code : Cemitcodes.to_patch_substituted option;
const_universes : constant_universes;
const_proj : projection_body option;
diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index efce219826..85dd1e66db 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -69,10 +69,6 @@ let subst_rel_declaration sub =
let subst_rel_context sub = List.smartmap (subst_rel_declaration sub)
-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
@@ -94,7 +90,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_decl_arity subst_const_type subst_template_cst_arity sub cb.const_type in
+ let type' = subst_const_type 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
@@ -120,14 +116,6 @@ let hcons_rel_decl =
let hcons_rel_context l = List.smartmap hcons_rel_decl l
-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
| Def l_constr ->
@@ -145,7 +133,7 @@ let hcons_const_universes cbu =
let hcons_const_body cb =
{ cb with
const_body = hcons_const_def cb.const_body;
- const_type = hcons_const_type cb.const_type;
+ const_type = Term.hcons_constr cb.const_type;
const_universes = hcons_const_universes cb.const_universes }
(** {6 Inductive types } *)
diff --git a/kernel/environ.ml b/kernel/environ.ml
index b01b652001..d2c737ab0c 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -232,12 +232,6 @@ let constraints_of cb u =
| Monomorphic_const _ -> Univ.Constraint.empty
| Polymorphic_const ctx -> Univ.AUContext.instantiate u ctx
-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
@@ -245,7 +239,7 @@ let constant_type env (kn,u) =
| Monomorphic_const _ -> cb.const_type, Univ.Constraint.empty
| Polymorphic_const ctx ->
let csts = constraints_of cb u in
- (map_regular_arity (subst_instance_constr u) cb.const_type, csts)
+ (subst_instance_constr u cb.const_type, csts)
let constant_context env kn =
let cb = lookup_constant kn env in
@@ -287,7 +281,7 @@ let constant_value_and_type env (kn, u) =
| OpaqueDef _ -> None
| Undef _ -> None
in
- b', map_regular_arity (subst_instance_constr u) cb.const_type, cst
+ b', subst_instance_constr u cb.const_type, cst
else
let b' = match cb.const_body with
| Def l_body -> Some (Mod_subst.force_constr l_body)
@@ -303,7 +297,7 @@ let constant_value_and_type env (kn, u) =
let constant_type_in env (kn,u) =
let cb = lookup_constant kn env in
if Declareops.constant_is_polymorphic cb then
- map_regular_arity (subst_instance_constr u) cb.const_type
+ subst_instance_constr u cb.const_type
else cb.const_type
let constant_value_in env (kn,u) =
@@ -337,15 +331,6 @@ let polymorphic_pconstant (cst,u) env =
let type_in_type_constant cst env =
not (lookup_constant cst env).const_typing_flags.check_universes
-let template_polymorphic_constant cst env =
- match (lookup_constant cst env).const_type with
- | TemplateArity _ -> true
- | RegularArity _ -> false
-
-let template_polymorphic_pconstant (cst,u) env =
- if not (Univ.Instance.is_empty u) then false
- else template_polymorphic_constant cst env
-
let lookup_projection cst env =
match (lookup_constant (Projection.constant cst) env).const_proj with
| Some pb -> pb
diff --git a/kernel/environ.mli b/kernel/environ.mli
index cd7a9d2791..377c61de2c 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -139,10 +139,6 @@ val polymorphic_constant : constant -> env -> bool
val polymorphic_pconstant : pconstant -> env -> bool
val type_in_type_constant : constant -> env -> bool
-(** Old-style polymorphism *)
-val template_polymorphic_constant : constant -> env -> bool
-val template_polymorphic_pconstant : pconstant -> env -> bool
-
(** {6 ... } *)
(** [constant_value env c] raises [NotEvaluableConst Opaque] if
[c] is opaque and [NotEvaluableConst NoBody] if it has no
@@ -153,11 +149,11 @@ 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 -> constant_type constrained
+val constant_type : env -> constant puniverses -> types constrained
val constant_opt_value : env -> constant puniverses -> (constr * Univ.constraints) option
val constant_value_and_type : env -> constant puniverses ->
- constr option * constant_type * Univ.constraints
+ constr option * types * Univ.constraints
(** The universe context associated to the constant, empty if not
polymorphic *)
val constant_context : env -> constant -> Univ.abstract_universe_context
@@ -166,7 +162,7 @@ val constant_context : env -> constant -> Univ.abstract_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 -> constant_type
+val constant_type_in : env -> constant puniverses -> types
val constant_opt_value_in : env -> constant puniverses -> constr option
(** {6 Primitive projections} *)
diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml
index c7f3e5c51b..0888ccc109 100644
--- a/kernel/mod_typing.ml
+++ b/kernel/mod_typing.ml
@@ -83,7 +83,7 @@ let rec check_with_def env struc (idl,(c,ctx)) mp equiv =
let c',cst = match cb.const_body with
| Undef _ | OpaqueDef _ ->
let j = Typeops.infer env' c in
- let typ = Typeops.type_of_constant_type env' cb.const_type in
+ let typ = cb.const_type in
let cst' = Reduction.infer_conv_leq env' (Environ.universes env')
j.uj_type typ in
j.uj_val, cst'
@@ -103,7 +103,7 @@ let rec check_with_def env struc (idl,(c,ctx)) mp equiv =
let cst = match cb.const_body with
| Undef _ | OpaqueDef _ ->
let j = Typeops.infer env' c in
- let typ = Typeops.type_of_constant_type env' cb.const_type in
+ let typ = cb.const_type in
let cst' = Reduction.infer_conv_leq env' (Environ.universes env')
j.uj_type typ in
cst'
diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml
index bd82dd465b..b311165f10 100644
--- a/kernel/subtyping.ml
+++ b/kernel/subtyping.ml
@@ -313,8 +313,8 @@ let check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2 =
error (PolymorphicStatusExpected false)
in
(* Now check types *)
- 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 typ1 = cb1.const_type in
+ let typ2 = cb2.const_type in
let cst = check_type poly cst env typ1 typ2 in
(* Now we check the bodies:
- A transparent constant can only be implemented by a compatible
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index 43c099712a..3f42c348fc 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -21,7 +21,6 @@ open Environ
open Entries
open Typeops
-module RelDecl = Context.Rel.Declaration
module NamedDecl = Context.Named.Declaration
(* Insertion of constants and parameters in environment. *)
@@ -128,7 +127,7 @@ let inline_side_effects env body ctx side_eff =
match cb.const_universes with
| Monomorphic_const cnstctx ->
(** Abstract over the term at the top of the proof *)
- let ty = Typeops.type_of_constant_type env cb.const_type in
+ let ty = cb.const_type in
let subst = Cmap_env.add c (Inr var) subst in
let univs = Univ.ContextSet.of_context cnstctx in
let ctx = Univ.ContextSet.union ctx univs in
@@ -249,7 +248,7 @@ let infer_declaration (type a) ~(trust : a trust) env kn (dcl : a constant_entry
let t = hcons_constr (Vars.subst_univs_level_constr usubst c) in
{
Cooking.cook_body = Undef nl;
- cook_type = RegularArity t;
+ cook_type = t;
cook_proj = None;
cook_universes = univs;
cook_inline = false;
@@ -290,7 +289,7 @@ let infer_declaration (type a) ~(trust : a trust) env kn (dcl : a constant_entry
let def = OpaqueDef (Opaqueproof.create proofterm) in
{
Cooking.cook_body = def;
- cook_type = RegularArity typ;
+ cook_type = typ;
cook_proj = None;
cook_universes = Monomorphic_const univs;
cook_inline = c.const_entry_inline_code;
@@ -320,13 +319,11 @@ let infer_declaration (type a) ~(trust : a trust) env kn (dcl : a constant_entry
let j = infer env body in
let typ = match typ with
| None ->
- if not poly then (* Old-style polymorphism *)
- make_polymorphic_if_constant_for_ind env j
- else RegularArity (Vars.subst_univs_level_constr usubst j.uj_type)
+ Vars.subst_univs_level_constr usubst j.uj_type
| Some t ->
let tj = infer_type env t in
let _ = judge_of_cast env j DEFAULTcast tj in
- RegularArity (Vars.subst_univs_level_constr usubst t)
+ Vars.subst_univs_level_constr usubst t
in
let def = hcons_constr (Vars.subst_univs_level_constr usubst j.uj_val) in
let def =
@@ -363,21 +360,13 @@ let infer_declaration (type a) ~(trust : a trust) env kn (dcl : a constant_entry
let term, typ = pb.proj_eta in
{
Cooking.cook_body = Def (Mod_subst.from_val (hcons_constr term));
- cook_type = RegularArity typ;
+ cook_type = typ;
cook_proj = Some pb;
cook_universes = univs;
cook_inline = false;
cook_context = None;
}
-let global_vars_set_constant_type env = function
- | RegularArity t -> global_vars_set env t
- | TemplateArity (ctx,_) ->
- Context.Rel.fold_outside
- (RelDecl.fold_constr
- (fun t c -> Id.Set.union (global_vars_set env t) c))
- ctx ~init:Id.Set.empty
-
let record_aux env s_ty s_bo suggested_expr =
let in_ty = keep_hyps env s_ty in
let v =
@@ -426,7 +415,7 @@ let build_constant_declaration kn env result =
| 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_constant_type env typ in
+ let ids_typ = global_vars_set env typ in
let ids_def = match def with
| Undef _ -> Idset.empty
| Def cs -> global_vars_set env (Mod_subst.force_constr cs)
@@ -454,14 +443,14 @@ let build_constant_declaration kn env result =
match def with
| Undef _ as x -> x (* nothing to check *)
| Def cs as x ->
- let ids_typ = global_vars_set_constant_type env typ in
+ let ids_typ = global_vars_set 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_constant_type env typ in
+ let ids_typ = global_vars_set 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
@@ -524,8 +513,7 @@ let constant_entry_of_side_effect cb u =
const_entry_body = Future.from_val (pt, ());
const_entry_secctx = None;
const_entry_feedback = None;
- const_entry_type =
- (match cb.const_type with RegularArity t -> Some t | _ -> None);
+ const_entry_type = Some cb.const_type;
const_entry_universes = univs;
const_entry_opaque = Declareops.is_opaque cb;
const_entry_inline_code = cb.const_inline_code }
@@ -625,7 +613,7 @@ let translate_recipe env kn r =
let translate_local_def mb env id centry =
let open Cooking in
let decl = infer_declaration ~trust:mb env None (DefinitionEntry centry) in
- let typ = type_of_constant_type env decl.cook_type in
+ let typ = decl.cook_type in
if Option.is_empty decl.cook_context && !Flags.compilation_mode = Flags.BuildVo then begin
match decl.cook_body with
| Undef _ -> ()
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index b814deb6eb..044877e82a 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -111,36 +111,17 @@ let check_hyps_inclusion env f c sign =
(* Type of constants *)
-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 (kn,u as cst) args =
+let type_of_constant env (kn,u as cst) =
let cb = lookup_constant kn env in
let () = check_hyps_inclusion env mkConstU cst cb.const_hyps in
let ty, cu = constant_type env cst in
- let ty = type_of_constant_type_knowing_parameters env ty args in
let () = check_constraints cu env in
ty
-let type_of_constant_knowing_parameters_in env (kn,u as cst) args =
+let type_of_constant_in env (kn,u as cst) =
let cb = lookup_constant kn env in
let () = check_hyps_inclusion env mkConstU cst cb.const_hyps in
- let ty = constant_type_in env cst in
- type_of_constant_type_knowing_parameters env ty args
-
-let type_of_constant env cst =
- type_of_constant_knowing_parameters env cst [||]
-
-let type_of_constant_in env cst =
- type_of_constant_knowing_parameters_in env cst [||]
-
-let type_of_constant_type env t =
- type_of_constant_type_knowing_parameters env t [||]
+ constant_type_in env cst
(* Type of a lambda-abstraction. *)
@@ -369,9 +350,6 @@ let rec execute env cstr =
| Ind ind when Environ.template_polymorphic_pind ind env ->
let args = Array.map (fun t -> lazy t) argst in
type_of_inductive_knowing_parameters env ind args
- | Const cst when Environ.template_polymorphic_pconstant cst env ->
- let args = Array.map (fun t -> lazy t) argst in
- type_of_constant_knowing_parameters env cst args
| _ ->
(* No template polymorphism *)
execute env f
@@ -509,8 +487,6 @@ let judge_of_relative env k = make_judge (mkRel k) (type_of_relative env k)
let judge_of_variable env x = make_judge (mkVar x) (type_of_variable env x)
let judge_of_constant env cst = make_judge (mkConstU cst) (type_of_constant env cst)
-let judge_of_constant_knowing_parameters env cst args =
- make_judge (mkConstU cst) (type_of_constant_knowing_parameters env cst args)
let judge_of_projection env p cj =
make_judge (mkProj (p,cj.uj_val)) (type_of_projection env p cj.uj_val cj.uj_type)
@@ -559,34 +535,3 @@ let type_of_projection_constant env (p,u) =
Vars.subst_instance_constr u pb.proj_type
else pb.proj_type
| None -> raise (Invalid_argument "type_of_projection: not a projection")
-
-(* Instantiation of terms on real arguments. *)
-
-(* 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) -> Univ.Universe.level u | _ -> None
-
-let extract_context_levels env l =
- let fold l = function
- | RelDecl.LocalAssum (_,p) -> extract_level env p :: l
- | RelDecl.LocalDef _ -> 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) ->
- let ind, l = decompose_app (whd_all env c) in
- if isInd ind && List.is_empty l then
- let mis = lookup_mind_specif env (fst (destInd ind)) in
- let nparams = Inductive.inductive_params mis in
- let paramsl = CList.lastn nparams params in
- let param_ccls = extract_context_levels env paramsl in
- let s = { template_param_levels = param_ccls; template_level = u} in
- TemplateArity (params,s)
- else RegularArity t
- | _ ->
- RegularArity t
diff --git a/kernel/typeops.mli b/kernel/typeops.mli
index 24521070e2..a8f7fba9a0 100644
--- a/kernel/typeops.mli
+++ b/kernel/typeops.mli
@@ -11,7 +11,6 @@ open Univ
open Term
open Environ
open Entries
-open Declarations
(** {6 Typing functions (not yet tagged as safe) }
@@ -53,9 +52,6 @@ val judge_of_variable : env -> variable -> unsafe_judgment
val judge_of_constant : env -> pconstant -> unsafe_judgment
-val judge_of_constant_knowing_parameters :
- env -> pconstant -> types Lazy.t array -> unsafe_judgment
-
(** {6 type of an applied projection } *)
val judge_of_projection : env -> Names.projection -> unsafe_judgment -> unsafe_judgment
@@ -98,21 +94,9 @@ val judge_of_case : env -> case_info
-> unsafe_judgment -> unsafe_judgment -> unsafe_judgment array
-> unsafe_judgment
-val type_of_constant_type : env -> constant_type -> types
-
val type_of_projection_constant : env -> Names.projection puniverses -> types
val type_of_constant_in : env -> pconstant -> types
-val type_of_constant_type_knowing_parameters :
- env -> constant_type -> types Lazy.t array -> types
-
-val type_of_constant_knowing_parameters_in :
- env -> pconstant -> types Lazy.t array -> types
-
-(** Make a type polymorphic if an arity *)
-val make_polymorphic_if_constant_for_ind : env -> unsafe_judgment ->
- constant_type
-
(** Check that hyps are included in env and fails with error otherwise *)
val check_hyps_inclusion : env -> ('a -> constr) -> 'a -> Context.Named.t -> unit
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 16:27:03 +0000