diff options
35 files changed, 65 insertions, 281 deletions
diff --git a/API/API.mli b/API/API.mli index 4d9904b5f..f2324bb44 100644 --- a/API/API.mli +++ b/API/API.mli @@ -1185,8 +1185,6 @@ sig | RegularArity of 'a | TemplateArity of 'b - type constant_type = (Constr.types, Context.Rel.t * template_arity) declaration_arity - type constant_universes = | Monomorphic_const of Univ.universe_context | Polymorphic_const of Univ.abstract_universe_context @@ -1208,7 +1206,7 @@ sig type constant_body = { const_hyps : Context.Named.t; const_body : constant_def; - const_type : constant_type; + const_type : Term.types; const_body_code : Cemitcodes.to_patch_substituted option; const_universes : constant_universes; const_proj : projection_body option; @@ -1586,7 +1584,6 @@ end module Typeops : sig val infer_type : Environ.env -> Term.types -> Environ.unsafe_type_judgment - val type_of_constant_type : Environ.env -> Declarations.constant_type -> Term.types val type_of_constant_in : Environ.env -> Term.pconstant -> Term.types end diff --git a/checker/cic.mli b/checker/cic.mli index 14fa7c774..59dd5bc4d 100644 --- a/checker/cic.mli +++ b/checker/cic.mli @@ -182,8 +182,6 @@ type ('a, 'b) declaration_arity = | RegularArity of 'a | TemplateArity of 'b -type constant_type = (constr, rel_context * template_arity) declaration_arity - (** Inlining level of parameters at functor applications. This is ignored by the checker. *) @@ -226,7 +224,7 @@ type typing_flags = { type constant_body = { const_hyps : section_context; (** New: younger hyp at top *) const_body : constant_def; - const_type : constant_type; + const_type : constr; const_body_code : to_patch_substituted; const_universes : constant_universes; const_proj : projection_body option; diff --git a/checker/declarations.ml b/checker/declarations.ml index 2eefe4781..093d999a3 100644 --- a/checker/declarations.ml +++ b/checker/declarations.ml @@ -515,12 +515,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_arity sub s = subst_decl_arity subst_mps subst_template_cst_arity sub s - let constant_is_polymorphic cb = match cb.const_universes with | Monomorphic_const _ -> false @@ -531,7 +525,7 @@ let constant_is_polymorphic cb = let subst_const_body sub cb = { cb with const_body = subst_constant_def sub cb.const_body; - const_type = subst_arity sub cb.const_type } + const_type = subst_mps sub cb.const_type } let subst_regular_ind_arity sub s = diff --git a/checker/environ.ml b/checker/environ.ml index d3f393c65..a0818012c 100644 --- a/checker/environ.ml +++ b/checker/environ.ml @@ -124,12 +124,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 @@ -137,7 +131,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) exception NotEvaluableConst of const_evaluation_result diff --git a/checker/environ.mli b/checker/environ.mli index 754c295d2..8e8d0fd49 100644 --- a/checker/environ.mli +++ b/checker/environ.mli @@ -46,7 +46,7 @@ val check_constraints : Univ.constraints -> env -> bool (* Constants *) val lookup_constant : constant -> env -> Cic.constant_body val add_constant : constant -> Cic.constant_body -> env -> env -val constant_type : env -> constant puniverses -> constant_type Univ.constrained +val constant_type : env -> constant puniverses -> constr Univ.constrained type const_evaluation_result = NoBody | Opaque | IsProj exception NotEvaluableConst of const_evaluation_result val constant_value : env -> constant puniverses -> constr diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml index 4948f6008..b6816dd48 100644 --- a/checker/mod_checking.ml +++ b/checker/mod_checking.ml @@ -35,15 +35,11 @@ let check_constant_declaration env kn cb = push_context ~strict:false ctx env in let envty, ty = - match cb.const_type with - RegularArity ty -> - let ty', cu = refresh_arity ty in - let envty = push_context_set cu env' in - let _ = infer_type envty ty' in envty, ty - | TemplateArity(ctxt,par) -> - let _ = check_ctxt env' ctxt in - check_polymorphic_arity env' ctxt par; - env', it_mkProd_or_LetIn (Sort(Type par.template_level)) ctxt + let ty = cb.const_type in + let ty', cu = refresh_arity ty in + let envty = push_context_set cu env' in + let _ = infer_type envty ty' in + envty, ty in let () = match body_of_constant cb with diff --git a/checker/subtyping.ml b/checker/subtyping.ml index 3097c3a0b..68a467bea 100644 --- a/checker/subtyping.ml +++ b/checker/subtyping.ml @@ -294,8 +294,8 @@ let check_constant env mp1 l info1 cb2 spec2 subst1 subst2 = let cb1 = subst_const_body subst1 cb1 in let cb2 = subst_const_body subst2 cb2 in (*Start by checking 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 check_type env typ1 typ2; (* Now we check the bodies: - A transparent constant can only be implemented by a compatible diff --git a/checker/typeops.ml b/checker/typeops.ml index f2cbfec7d..9f39d588a 100644 --- a/checker/typeops.ml +++ b/checker/typeops.ml @@ -69,35 +69,16 @@ let judge_of_relative env n = (* 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 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_knowing_parameters env (kn,u as cst) paramstyp = +let judge_of_constant env (kn,u as cst) = let _cb = try lookup_constant kn env with Not_found -> failwith ("Cannot find constant: "^Constant.to_string kn) in - let ty, cu = type_of_constant_knowing_parameters env cst paramstyp in + let ty, cu = constant_type env cst in let () = check_constraints cu env in ty -let judge_of_constant env cst = - judge_of_constant_knowing_parameters env cst [||] - (* Type of an application. *) let judge_of_apply env (f,funj) argjv = @@ -276,8 +257,6 @@ let rec execute env cstr = match f with | Ind ind -> judge_of_inductive_knowing_parameters env ind jl - | Const cst -> - judge_of_constant_knowing_parameters env cst jl | _ -> (* No template polymorphism *) execute env f diff --git a/checker/typeops.mli b/checker/typeops.mli index 2be461b05..d9f2915a3 100644 --- a/checker/typeops.mli +++ b/checker/typeops.mli @@ -18,6 +18,3 @@ val infer_type : env -> constr -> sorts val check_ctxt : env -> rel_context -> env val check_polymorphic_arity : env -> rel_context -> template_arity -> unit - -val type_of_constant_type : env -> constant_type -> constr - diff --git a/checker/values.ml b/checker/values.ml index e13430e98..c95c3f1b2 100644 --- a/checker/values.ml +++ b/checker/values.ml @@ -13,7 +13,7 @@ To ensure this file is up-to-date, 'make' now compares the md5 of cic.mli with a copy we maintain here: -MD5 67309b04a86b247431fd3e580ecbb50d checker/cic.mli +MD5 c802f941f368bedd96e931cda0559d67 checker/cic.mli *) @@ -201,9 +201,6 @@ let v_engagement = v_impredicative_set let v_pol_arity = v_tuple "polymorphic_arity" [|List(Opt v_level);v_univ|] -let v_cst_type = - v_sum "constant_type" 0 [|[|v_constr|]; [|v_pair v_rctxt v_pol_arity|]|] - let v_cst_def = v_sum "constant_def" 0 [|[|Opt Int|]; [|v_cstr_subst|]; [|v_lazy_constr|]|] @@ -222,7 +219,7 @@ let v_const_univs = v_sum "constant_universes" 0 [|[|v_context|]; [|v_abs_contex let v_cb = v_tuple "constant_body" [|v_section_ctxt; v_cst_def; - v_cst_type; + v_constr; Any; v_const_univs; Opt v_projbody; diff --git a/engine/termops.ml b/engine/termops.ml index 1aba2bbdd..cf7c0cc20 100644 --- a/engine/termops.ml +++ b/engine/termops.ml @@ -1145,9 +1145,6 @@ let is_template_polymorphic env sigma f = | Ind (ind, u) -> if not (EConstr.EInstance.is_empty u) then false else Environ.template_polymorphic_ind ind env - | Const (cst, u) -> - if not (EConstr.EInstance.is_empty u) then false - else Environ.template_polymorphic_constant cst env | _ -> false let base_sort_cmp pb s0 s1 = diff --git a/engine/universes.ml b/engine/universes.ml index 08461a218..719af43ed 100644 --- a/engine/universes.ml +++ b/engine/universes.ml @@ -419,7 +419,7 @@ 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 + let ty = cb.const_type in begin match cb.const_universes with | Monomorphic_const _ -> ty, ContextSet.empty diff --git a/interp/impargs.ml b/interp/impargs.ml index b7125fc85..d8241c044 100644 --- a/interp/impargs.ml +++ b/interp/impargs.ml @@ -414,7 +414,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 = Typeops.type_of_constant_type env cb.const_type in + let ty = cb.const_type in let impls = compute_semi_auto_implicits env flags manual ty in impls diff --git a/kernel/cooking.ml b/kernel/cooking.ml index 63614e20f..80d41847c 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 f386fd936..6d1b776c0 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 f35438dfc..9697b0b8b 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 efce21982..85dd1e66d 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 b01b65200..d2c737ab0 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 cd7a9d279..377c61de2 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 c7f3e5c51..0888ccc10 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 bd82dd465..b311165f1 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 43c099712..3f42c348f 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 b814deb6e..044877e82 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 24521070e..a8f7fba9a 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 diff --git a/library/global.ml b/library/global.ml index 00a3a4986..963c97741 100644 --- a/library/global.ml +++ b/library/global.ml @@ -199,8 +199,7 @@ let type_of_global_in_context env r = | ConstRef c -> let cb = Environ.lookup_constant c env in let univs = Declareops.constant_polymorphic_context cb in - let env = Environ.push_context ~strict:false (Univ.AUContext.repr univs) env in - Typeops.type_of_constant_type env cb.Declarations.const_type, univs + cb.Declarations.const_type, univs | IndRef ind -> let (mib, oib as specif) = Inductive.lookup_mind_specif env ind in let univs = Declareops.inductive_polymorphic_context mib in @@ -255,7 +254,7 @@ let is_template_polymorphic r = let env = env() in match r with | VarRef id -> false - | ConstRef c -> Environ.template_polymorphic_constant c env + | ConstRef c -> false | IndRef ind -> Environ.template_polymorphic_ind ind env | ConstructRef cstr -> Environ.template_polymorphic_ind (inductive_of_constructor cstr) env diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml index 39826d744..89c2a0ae3 100644 --- a/plugins/extraction/extract_env.ml +++ b/plugins/extraction/extract_env.ml @@ -132,7 +132,7 @@ let rec add_labels mp = function exception Impossible let check_arity env cb = - let t = Typeops.type_of_constant_type env cb.const_type in + let t = 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 3661faada..661842790 100644 --- a/plugins/extraction/extraction.ml +++ b/plugins/extraction/extraction.ml @@ -518,7 +518,7 @@ and mlt_env env r = match r with match lookup_typedef kn cb with | Some _ as o -> o | None -> - let typ = Typeops.type_of_constant_type env cb.const_type + let typ = cb.const_type (* FIXME not sure if we should instantiate univs here *) in match flag_of_type env typ with | Info,TypeScheme -> @@ -543,7 +543,7 @@ let record_constant_type env kn opt_typ = | Some schema -> schema | None -> let typ = match opt_typ with - | None -> Typeops.type_of_constant_type env cb.const_type + | None -> cb.const_type | Some typ -> typ in let mlt = extract_type env [] 1 typ [] in @@ -969,7 +969,7 @@ let extract_fixpoint env vkn (fi,ti,ci) = let extract_constant env kn cb = let r = ConstRef kn in - let typ = Typeops.type_of_constant_type env cb.const_type in + let typ = cb.const_type 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 @@ -1025,7 +1025,7 @@ let extract_constant env kn cb = let extract_constant_spec env kn cb = let r = ConstRef kn in - let typ = Typeops.type_of_constant_type env cb.const_type in + let typ = cb.const_type in try match flag_of_type env typ with | (Logic, TypeScheme) -> Stype (r, [], Some (Tdummy Ktype)) diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index 863c9dc8d..89537ad3f 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -857,7 +857,7 @@ let make_graph (f_ref:global_reference) = with_full_print (fun () -> (Constrextern.extern_constr false env sigma body, Constrextern.extern_type false env sigma - ((*FIXME*) Typeops.type_of_constant_type env c_body.const_type) + ((*FIXME*) c_body.const_type) ) ) () diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index 9f4829761..ef0fb8ea6 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -34,12 +34,6 @@ let get_polymorphic_positions sigma f = (match oib.mind_arity with | RegularArity _ -> assert false | TemplateArity templ -> templ.template_param_levels) - | Const (cst, u) -> - let cb = Global.lookup_constant cst in - (match cb.const_type with - | RegularArity _ -> assert false - | TemplateArity (_, templ) -> - templ.template_param_levels) | _ -> assert false let refresh_universes ?(status=univ_rigid) ?(onlyalg=false) ?(refreshset=false) diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml index e0f9bfcb7..079524f34 100644 --- a/pretyping/retyping.ml +++ b/pretyping/retyping.ml @@ -192,11 +192,6 @@ let retype ?(polyprop=true) sigma = EConstr.of_constr (try Inductive.type_of_inductive_knowing_parameters ~polyprop env (mip, u) argtyps with Reduction.NotArity -> retype_error NotAnArity) - | Const (cst, u) -> - let u = EInstance.kind sigma u in - EConstr.of_constr (try Typeops.type_of_constant_knowing_parameters_in env (cst, u) argtyps - with Reduction.NotArity -> retype_error NotAnArity) - | Var id -> type_of_var env id | Construct (cstr, u) -> let u = EInstance.kind sigma u in EConstr.of_constr (type_of_constructor env (cstr, u)) @@ -220,7 +215,7 @@ let type_of_global_reference_knowing_conclusion env sigma c conclty = | Const (cst, u) -> let t = constant_type_in env (cst, EInstance.kind sigma u) in (* TODO *) - sigma, EConstr.of_constr (Typeops.type_of_constant_type_knowing_parameters env t [||]) + sigma, EConstr.of_constr t | Var id -> sigma, type_of_var env id | Construct (cstr, u) -> sigma, EConstr.of_constr (type_of_constructor env (cstr, EInstance.kind sigma u)) | _ -> assert false diff --git a/pretyping/typing.ml b/pretyping/typing.ml index 1bb003575..1f35fa19a 100644 --- a/pretyping/typing.ml +++ b/pretyping/typing.ml @@ -35,11 +35,6 @@ let meta_type evd mv = let ty = Evd.map_fl EConstr.of_constr ty in meta_instance evd ty -let constant_type_knowing_parameters env sigma (cst, u) jl = - let u = Unsafe.to_instance u in - let paramstyp = Array.map (fun j -> lazy (EConstr.to_constr sigma j.uj_type)) jl in - EConstr.of_constr (type_of_constant_knowing_parameters_in env (cst, u) paramstyp) - let inductive_type_knowing_parameters env sigma (ind,u) jl = let u = Unsafe.to_instance u in let mspec = lookup_mind_specif env ind in @@ -315,9 +310,6 @@ let rec execute env evdref cstr = | Ind (ind, u) when EInstance.is_empty u && Environ.template_polymorphic_ind ind env -> make_judge f (inductive_type_knowing_parameters env !evdref (ind, u) jl) - | Const (cst, u) when EInstance.is_empty u && Environ.template_polymorphic_constant cst env -> - make_judge f - (constant_type_knowing_parameters env !evdref (cst, u) jl) | _ -> (* No template polymorphism *) execute env evdref f diff --git a/printing/prettyp.ml b/printing/prettyp.ml index 827c0e458..17249262e 100644 --- a/printing/prettyp.ml +++ b/printing/prettyp.ml @@ -501,9 +501,6 @@ let print_body env evd = function let print_typed_body env evd (val_0,typ) = (print_body env evd val_0 ++ fnl () ++ str " : " ++ pr_ltype_env env evd typ) -let ungeneralized_type_of_constant_type t = - Typeops.type_of_constant_type (Global.env ()) t - let print_instance sigma cb = if Declareops.constant_is_polymorphic cb then let univs = Declareops.constant_polymorphic_context cb in @@ -515,17 +512,13 @@ let print_instance sigma cb = let print_constant with_values sep sp = let cb = Global.lookup_constant sp in let val_0 = Global.body_of_constant_body cb in - let typ = match cb.const_type with - | RegularArity t as x -> - begin match cb.const_universes with - | Monomorphic_const _ -> x + let typ = + match cb.const_universes with + | Monomorphic_const _ -> cb.const_type | Polymorphic_const univs -> let inst = Univ.AUContext.instance univs in - RegularArity (Vars.subst_instance_constr inst t) - end - | TemplateArity _ as x -> x + Vars.subst_instance_constr inst cb.const_type in - let typ = ungeneralized_type_of_constant_type typ in let univs = let otab = Global.opaque_tables () in match cb.const_body with @@ -698,7 +691,7 @@ let print_full_pure_context () = | "CONSTANT" -> let con = Global.constant_of_delta_kn kn in let cb = Global.lookup_constant con in - let typ = ungeneralized_type_of_constant_type cb.const_type in + let typ = cb.const_type in hov 0 ( match cb.const_body with | Undef _ -> diff --git a/printing/printmod.ml b/printing/printmod.ml index 5c7dcdc10..219eafda4 100644 --- a/printing/printmod.ml +++ b/printing/printmod.ml @@ -323,7 +323,7 @@ let print_body is_impl env mp (l,body) = str " :" ++ spc () ++ hov 0 (Printer.pr_ltype_env env sigma (Vars.subst_instance_constr u - (Typeops.type_of_constant_type env cb.const_type))) ++ + cb.const_type)) ++ (match cb.const_body with | Def l when is_impl -> spc () ++ diff --git a/vernac/assumptions.ml b/vernac/assumptions.ml index 86bbf46a3..6711b14da 100644 --- a/vernac/assumptions.ml +++ b/vernac/assumptions.ml @@ -311,10 +311,7 @@ let traverse current t = (** Hopefully bullet-proof function to recover the type of a constant. It just ignores all the universe stuff. There are many issues that can arise when considering terms out of any valid environment, so use with caution. *) -let type_of_constant cb = match cb.Declarations.const_type with -| Declarations.RegularArity ty -> ty -| Declarations.TemplateArity (ctx, arity) -> - Term.mkArity (ctx, Sorts.sort_of_univ arity.Declarations.template_level) +let type_of_constant cb = cb.Declarations.const_type let assumptions ?(add_opaque=false) ?(add_transparent=false) st gr t = let (idts, knst) = st in diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 9650ea19d..6b04ff00a 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -257,7 +257,7 @@ let print_namespace ns = in let print_constant k body = (* FIXME: universes *) - let t = Typeops.type_of_constant_type (Global.env ()) body.Declarations.const_type in + let t = body.Declarations.const_type in print_kn k ++ str":" ++ spc() ++ Printer.pr_type t in let matches mp = match match_modulepath ns mp with |