aboutsummaryrefslogtreecommitdiff
path: root/kernel
diff options
context:
space:
mode:
Diffstat (limited to 'kernel')
-rw-r--r--kernel/cbytecodes.mli6
-rw-r--r--kernel/cooking.ml43
-rw-r--r--kernel/cooking.mli11
-rw-r--r--kernel/declarations.ml4
-rw-r--r--kernel/declareops.ml16
-rw-r--r--kernel/entries.ml7
-rw-r--r--kernel/environ.ml21
-rw-r--r--kernel/environ.mli10
-rw-r--r--kernel/mod_subst.mli4
-rw-r--r--kernel/mod_typing.ml4
-rw-r--r--kernel/names.mli30
-rw-r--r--kernel/safe_typing.ml46
-rw-r--r--kernel/safe_typing.mli17
-rw-r--r--kernel/subtyping.ml4
-rw-r--r--kernel/term_typing.ml172
-rw-r--r--kernel/term_typing.mli23
-rw-r--r--kernel/typeops.ml61
-rw-r--r--kernel/typeops.mli16
-rw-r--r--kernel/uGraph.mli2
-rw-r--r--kernel/univ.ml2
-rw-r--r--kernel/univ.mli38
-rw-r--r--kernel/vm.mli6
22 files changed, 245 insertions, 298 deletions
diff --git a/kernel/cbytecodes.mli b/kernel/cbytecodes.mli
index 8f38e9d34e..718917ab35 100644
--- a/kernel/cbytecodes.mli
+++ b/kernel/cbytecodes.mli
@@ -34,7 +34,7 @@ type structured_constant =
| Const_univ_level of Univ.universe_level
| Const_type of Univ.universe
-val pp_struct_const : structured_constant -> Pp.std_ppcmds
+val pp_struct_const : structured_constant -> Pp.t
type reloc_table = (tag * int) array
@@ -163,8 +163,8 @@ type comp_env = {
in_env : vm_env ref (** the variables that are accessed *)
}
-val pp_bytecodes : bytecodes -> Pp.std_ppcmds
-val pp_fv_elem : fv_elem -> Pp.std_ppcmds
+val pp_bytecodes : bytecodes -> Pp.t
+val pp_fv_elem : fv_elem -> Pp.t
(*spiwack: moved this here because I needed it for retroknowledge *)
type block =
diff --git a/kernel/cooking.ml b/kernel/cooking.ml
index 95822fac68..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
@@ -151,9 +150,14 @@ let abstract_constant_body =
type recipe = { from : constant_body; info : Opaqueproof.cooking_info }
type inline = bool
-type result =
- constant_def * constant_type * projection_body option *
- constant_universes * inline * Context.Named.t option
+type result = {
+ cook_body : constant_def;
+ cook_type : types;
+ cook_proj : projection_body option;
+ cook_universes : constant_universes;
+ cook_inline : inline;
+ cook_context : Context.Named.t option;
+}
let on_body ml hy f = function
| Undef _ as x -> x
@@ -162,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
@@ -215,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
@@ -239,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;
@@ -254,9 +240,14 @@ let cook_constant ~hcons env { from = cb; info } =
| Polymorphic_const auctx ->
Polymorphic_const (AUContext.union abs_ctx auctx)
in
- (body, typ, Option.map projection cb.const_proj,
- univs, cb.const_inline_code,
- Some const_hyps)
+ {
+ cook_body = body;
+ cook_type = typ;
+ cook_proj = Option.map projection cb.const_proj;
+ cook_universes = univs;
+ cook_inline = cb.const_inline_code;
+ cook_context = Some const_hyps;
+ }
(* let cook_constant_key = Profile.declare_profile "cook_constant" *)
(* let cook_constant = Profile.profile2 cook_constant_key cook_constant *)
diff --git a/kernel/cooking.mli b/kernel/cooking.mli
index 79a028d760..6d1b776c05 100644
--- a/kernel/cooking.mli
+++ b/kernel/cooking.mli
@@ -16,9 +16,14 @@ type recipe = { from : constant_body; info : Opaqueproof.cooking_info }
type inline = bool
-type result =
- constant_def * constant_type * projection_body option *
- constant_universes * inline * Context.Named.t option
+type result = {
+ cook_body : constant_def;
+ cook_type : types;
+ cook_proj : projection_body option;
+ cook_universes : constant_universes;
+ cook_inline : inline;
+ cook_context : Context.Named.t option;
+}
val cook_constant : hcons:bool -> env -> recipe -> result
val cook_constr : Opaqueproof.cooking_info -> Term.constr -> Term.constr
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/entries.ml b/kernel/entries.ml
index 3fa25c142a..a1ccbdbc1b 100644
--- a/kernel/entries.ml
+++ b/kernel/entries.ml
@@ -64,6 +64,10 @@ type mutual_inductive_entry = {
type 'a proof_output = constr Univ.in_universe_context_set * 'a
type 'a const_entry_body = 'a proof_output Future.computation
+type constant_universes_entry =
+ | Monomorphic_const_entry of Univ.universe_context
+ | Polymorphic_const_entry of Univ.universe_context
+
type 'a definition_entry = {
const_entry_body : 'a const_entry_body;
(* List of section variables *)
@@ -71,8 +75,7 @@ type 'a definition_entry = {
(* State id on which the completion of type checking is reported *)
const_entry_feedback : Stateid.t option;
const_entry_type : types option;
- const_entry_polymorphic : bool;
- const_entry_universes : Univ.universe_context;
+ const_entry_universes : constant_universes_entry;
const_entry_opaque : bool;
const_entry_inline_code : bool }
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_subst.mli b/kernel/mod_subst.mli
index 3cd02fb9f8..f1d0e42796 100644
--- a/kernel/mod_subst.mli
+++ b/kernel/mod_subst.mli
@@ -107,9 +107,9 @@ val subst_substituted : substitution -> 'a substituted -> 'a substituted
(**/**)
(* debugging *)
val debug_string_of_subst : substitution -> string
-val debug_pr_subst : substitution -> Pp.std_ppcmds
+val debug_pr_subst : substitution -> Pp.t
val debug_string_of_delta : delta_resolver -> string
-val debug_pr_delta : delta_resolver -> Pp.std_ppcmds
+val debug_pr_delta : delta_resolver -> Pp.t
(**/**)
(** [subst_mp sub mp] guarantees that whenever the result of the
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/names.mli b/kernel/names.mli
index 74d63c0cea..d111dd3c06 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -57,7 +57,7 @@ sig
val to_string : t -> string
(** Converts a identifier into an string. *)
- val print : t -> Pp.std_ppcmds
+ val print : t -> Pp.t
(** Pretty-printer. *)
module Set : Set.S with type elt = t
@@ -105,7 +105,7 @@ sig
val hcons : t -> t
(** Hashconsing over names. *)
- val print : t -> Pp.std_ppcmds
+ val print : t -> Pp.t
(** Pretty-printer (print "_" for [Anonymous]. *)
end
@@ -187,7 +187,7 @@ sig
val to_id : t -> Id.t
(** Conversion to an identifier. *)
- val print : t -> Pp.std_ppcmds
+ val print : t -> Pp.t
(** Pretty-printer. *)
module Set : Set.S with type elt = t
@@ -286,7 +286,7 @@ sig
val debug_to_string : t -> string
(** Same as [to_string], but outputs information related to debug. *)
- val print : t -> Pp.std_ppcmds
+ val print : t -> Pp.t
(** Comparisons *)
val compare : t -> t -> int
@@ -365,9 +365,9 @@ sig
(** Displaying *)
val to_string : t -> string
- val print : t -> Pp.std_ppcmds
+ val print : t -> Pp.t
val debug_to_string : t -> string
- val debug_print : t -> Pp.std_ppcmds
+ val debug_print : t -> Pp.t
end
@@ -447,9 +447,9 @@ sig
(** Displaying *)
val to_string : t -> string
- val print : t -> Pp.std_ppcmds
+ val print : t -> Pp.t
val debug_to_string : t -> string
- val debug_print : t -> Pp.std_ppcmds
+ val debug_print : t -> Pp.t
end
@@ -609,7 +609,7 @@ val mk_label : string -> label
val string_of_label : label -> string
(** @deprecated Same as [Label.to_string]. *)
-val pr_label : label -> Pp.std_ppcmds
+val pr_label : label -> Pp.t
(** @deprecated Same as [Label.print]. *)
val label_of_id : Id.t -> label
@@ -695,7 +695,7 @@ val label : kernel_name -> Label.t
val string_of_kn : kernel_name -> string
(** @deprecated Same as [KerName.to_string]. *)
-val pr_kn : kernel_name -> Pp.std_ppcmds
+val pr_kn : kernel_name -> Pp.t
(** @deprecated Same as [KerName.print]. *)
val kn_ord : kernel_name -> kernel_name -> int
@@ -731,7 +731,7 @@ module Projection : sig
val map : (constant -> constant) -> t -> t
val to_string : t -> string
- val print : t -> Pp.std_ppcmds
+ val print : t -> Pp.t
end
@@ -776,10 +776,10 @@ val con_with_label : constant -> Label.t -> constant
val string_of_con : constant -> string
(** @deprecated Same as [Constant.to_string] *)
-val pr_con : constant -> Pp.std_ppcmds
+val pr_con : constant -> Pp.t
(** @deprecated Same as [Constant.print] *)
-val debug_pr_con : constant -> Pp.std_ppcmds
+val debug_pr_con : constant -> Pp.t
(** @deprecated Same as [Constant.debug_print] *)
val debug_string_of_con : constant -> string
@@ -826,10 +826,10 @@ val mind_modpath : mutual_inductive -> ModPath.t
val string_of_mind : mutual_inductive -> string
(** @deprecated Same as [MutInd.to_string] *)
-val pr_mind : mutual_inductive -> Pp.std_ppcmds
+val pr_mind : mutual_inductive -> Pp.t
(** @deprecated Same as [MutInd.print] *)
-val debug_pr_mind : mutual_inductive -> Pp.std_ppcmds
+val debug_pr_mind : mutual_inductive -> Pp.t
(** @deprecated Same as [MutInd.debug_print] *)
val debug_string_of_mind : mutual_inductive -> string
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index ed4c7d57ad..04051f2e23 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -382,12 +382,13 @@ let safe_push_named d env =
let push_named_def (id,de) senv =
- let c,typ,univs =
- match Term_typing.translate_local_def senv.revstruct senv.env id de with
- | c, typ, Monomorphic_const ctx -> c, typ, ctx
- | _, _, Polymorphic_const _ -> assert false
+ let open Entries in
+ let trust = Term_typing.SideEffects senv.revstruct in
+ let c,typ,univs = Term_typing.translate_local_def trust senv.env id de in
+ let poly = match de.Entries.const_entry_universes with
+ | Monomorphic_const_entry _ -> false
+ | Polymorphic_const_entry _ -> true
in
- let poly = de.Entries.const_entry_polymorphic in
let univs = Univ.ContextSet.of_context univs in
let c, univs = match c with
| Def c -> Mod_subst.force_constr c, univs
@@ -492,12 +493,16 @@ let add_field ((l,sfb) as field) gn senv =
let update_resolver f senv = { senv with modresolver = f senv.modresolver }
(** Insertion of constants and parameters in environment *)
+type 'a effect_entry =
+| EffectEntry : private_constants effect_entry
+| PureEntry : unit effect_entry
+
type global_declaration =
- | ConstantEntry of bool * private_constants Entries.constant_entry
+ | ConstantEntry : 'a effect_entry * 'a Entries.constant_entry -> global_declaration
| GlobalRecipe of Cooking.recipe
type exported_private_constant =
- constant * private_constants Entries.constant_entry * private_constant_role
+ constant * private_constant_role
let add_constant_aux no_section senv (kn, cb) =
let l = pi3 (Constant.repr3 kn) in
@@ -521,30 +526,29 @@ let add_constant_aux no_section senv (kn, cb) =
in
senv''
+let export_private_constants ~in_section ce senv =
+ let exported, ce = Term_typing.export_side_effects senv.revstruct senv.env ce in
+ let bodies = List.map (fun (kn, cb, _) -> (kn, cb)) exported in
+ let exported = List.map (fun (kn, _, r) -> (kn, r)) exported in
+ let no_section = not in_section in
+ let senv = List.fold_left (add_constant_aux no_section) senv bodies in
+ (ce, exported), senv
+
let add_constant dir l decl senv =
let kn = make_con senv.modpath dir l in
let no_section = DirPath.is_empty dir in
- let seff_to_export, decl =
- match decl with
- | ConstantEntry (true, ce) ->
- let exports, ce =
- Term_typing.export_side_effects senv.revstruct senv.env ce in
- exports, ConstantEntry (false, ce)
- | _ -> [], decl
- in
- let senv =
- List.fold_left (add_constant_aux no_section) senv
- (List.map (fun (kn,cb,_,_) -> kn, cb) seff_to_export) in
let senv =
let cb =
match decl with
- | ConstantEntry (export_seff,ce) ->
- Term_typing.translate_constant senv.revstruct senv.env kn ce
+ | ConstantEntry (EffectEntry, ce) ->
+ Term_typing.translate_constant (Term_typing.SideEffects senv.revstruct) senv.env kn ce
+ | ConstantEntry (PureEntry, ce) ->
+ Term_typing.translate_constant Term_typing.Pure senv.env kn ce
| GlobalRecipe r ->
let cb = Term_typing.translate_recipe senv.env kn r in
if no_section then Declareops.hcons_const_body cb else cb in
add_constant_aux no_section senv (kn, cb) in
- (kn, List.map (fun (kn,_,ce,r) -> kn, ce, r) seff_to_export), senv
+ kn, senv
(** Insertion of inductive types *)
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index 5bb8ceb1a5..752fdd793e 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -67,7 +67,7 @@ val mk_pure_proof : Constr.constr -> private_constants Entries.proof_output
val inline_private_constants_in_constr :
Environ.env -> Constr.constr -> private_constants -> Constr.constr
val inline_private_constants_in_definition_entry :
- Environ.env -> private_constants Entries.definition_entry -> private_constants Entries.definition_entry
+ Environ.env -> private_constants Entries.definition_entry -> unit Entries.definition_entry
val universes_of_private : private_constants -> Univ.universe_context_set list
@@ -94,19 +94,26 @@ val push_named_def :
(** Insertion of global axioms or definitions *)
+type 'a effect_entry =
+| EffectEntry : private_constants effect_entry
+| PureEntry : unit effect_entry
+
type global_declaration =
- (* bool: export private constants *)
- | ConstantEntry of bool * private_constants Entries.constant_entry
+ | ConstantEntry : 'a effect_entry * 'a Entries.constant_entry -> global_declaration
| GlobalRecipe of Cooking.recipe
type exported_private_constant =
- constant * private_constants Entries.constant_entry * private_constant_role
+ constant * private_constant_role
+
+val export_private_constants : in_section:bool ->
+ private_constants Entries.constant_entry ->
+ (unit Entries.constant_entry * exported_private_constant list) safe_transformer
(** returns the main constant plus a list of auxiliary constants (empty
unless one requires the side effects to be exported) *)
val add_constant :
DirPath.t -> Label.t -> global_declaration ->
- (constant * exported_private_constant list) safe_transformer
+ constant safe_transformer
(** Adding an inductive type *)
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 cf82d54ec1..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. *)
@@ -77,6 +76,10 @@ end
type side_effects = SideEffects.t
+type _ trust =
+| Pure : unit trust
+| SideEffects : structure_body -> side_effects trust
+
let uniq_seff_rev = SideEffects.repr
let uniq_seff l = List.rev (SideEffects.repr l)
@@ -124,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
@@ -232,7 +235,7 @@ let abstract_constant_universes abstract uctx =
let sbst, auctx = Univ.abstract_universes uctx in
sbst, Polymorphic_const auctx
-let infer_declaration ~trust env kn dcl =
+let infer_declaration (type a) ~(trust : a trust) env kn (dcl : a constant_entry) =
match dcl with
| ParameterEntry (ctx,poly,(t,uctx),nl) ->
let env = push_context ~strict:(not poly) uctx env in
@@ -243,7 +246,14 @@ let infer_declaration ~trust env kn dcl =
in
let c = Typeops.assumption_of_judgment env j in
let t = hcons_constr (Vars.subst_univs_level_constr usubst c) in
- Undef nl, RegularArity t, None, univs, false, ctx
+ {
+ Cooking.cook_body = Undef nl;
+ cook_type = t;
+ cook_proj = None;
+ cook_universes = univs;
+ cook_inline = false;
+ cook_context = ctx;
+ }
(** Definition [c] is opaque (Qed), non polymorphic and with a specified type,
so we delay the typing and hash consing of its body.
@@ -251,52 +261,69 @@ let infer_declaration ~trust env kn dcl =
delay even in the polymorphic case. *)
| DefinitionEntry ({ const_entry_type = Some typ;
const_entry_opaque = true;
- const_entry_polymorphic = false} as c) ->
- let env = push_context ~strict:true c.const_entry_universes env in
+ const_entry_universes = Monomorphic_const_entry univs } as c) ->
+ let env = push_context ~strict:true univs env in
let { const_entry_body = body; const_entry_feedback = feedback_id } = c in
let tyj = infer_type env typ in
let proofterm =
Future.chain ~pure:true body (fun ((body,uctx),side_eff) ->
- let body, uctx, signatures =
- inline_side_effects env body uctx side_eff in
- let valid_signatures = check_signatures trust signatures in
- let env = push_context_set uctx env in
- let j =
+ let j, uctx = match trust with
+ | Pure ->
+ let env = push_context_set uctx env in
+ let j = infer env body in
+ let _ = judge_of_cast env j DEFAULTcast tyj in
+ j, uctx
+ | SideEffects mb ->
+ let (body, uctx, signatures) = inline_side_effects env body uctx side_eff in
+ let valid_signatures = check_signatures mb signatures in
+ let env = push_context_set uctx env in
let body,env,ectx = skip_trusted_seff valid_signatures body env in
let j = infer env body in
- unzip ectx j in
- let _ = judge_of_cast env j DEFAULTcast tyj in
+ let j = unzip ectx j in
+ let _ = judge_of_cast env j DEFAULTcast tyj in
+ j, uctx
+ in
let c = hcons_constr j.uj_val in
feedback_completion_typecheck feedback_id;
c, uctx) in
let def = OpaqueDef (Opaqueproof.create proofterm) in
- def, RegularArity typ, None,
- (Monomorphic_const c.const_entry_universes),
- c.const_entry_inline_code, c.const_entry_secctx
+ {
+ Cooking.cook_body = def;
+ cook_type = typ;
+ cook_proj = None;
+ cook_universes = Monomorphic_const univs;
+ cook_inline = c.const_entry_inline_code;
+ cook_context = c.const_entry_secctx;
+ }
(** Other definitions have to be processed immediately. *)
| DefinitionEntry c ->
let { const_entry_type = typ; const_entry_opaque = opaque } = c in
let { const_entry_body = body; const_entry_feedback = feedback_id } = c in
let (body, ctx), side_eff = Future.join body in
- let univsctx = Univ.ContextSet.of_context c.const_entry_universes in
- let body, ctx, _ = inline_side_effects env body
- (Univ.ContextSet.union univsctx ctx) side_eff in
- let env = push_context_set ~strict:(not c.const_entry_polymorphic) ctx env in
- let abstract = c.const_entry_polymorphic && not (Option.is_empty kn) in
+ let poly, univs = match c.const_entry_universes with
+ | Monomorphic_const_entry univs -> false, univs
+ | Polymorphic_const_entry univs -> true, univs
+ in
+ let univsctx = Univ.ContextSet.of_context univs in
+ let ctx = Univ.ContextSet.union univsctx ctx in
+ let body, ctx, _ = match trust with
+ | Pure -> body, ctx, []
+ | SideEffects _ -> inline_side_effects env body ctx side_eff
+ in
+ let env = push_context_set ~strict:(not poly) ctx env in
+ let abstract = poly && not (Option.is_empty kn) in
let usubst, univs =
abstract_constant_universes abstract (Univ.ContextSet.to_context ctx)
in
let j = infer env body in
let typ = match typ with
| None ->
- if not c.const_entry_polymorphic 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 =
@@ -304,7 +331,14 @@ let infer_declaration ~trust env kn dcl =
else Def (Mod_subst.from_val def)
in
feedback_completion_typecheck feedback_id;
- def, typ, None, univs, c.const_entry_inline_code, c.const_entry_secctx
+ {
+ Cooking.cook_body = def;
+ cook_type = typ;
+ cook_proj = None;
+ cook_universes = univs;
+ cook_inline = c.const_entry_inline_code;
+ cook_context = c.const_entry_secctx;
+ }
| ProjectionEntry {proj_entry_ind = ind; proj_entry_arg = i} ->
let mib, _ = Inductive.lookup_mind_specif env (ind,0) in
@@ -324,16 +358,14 @@ let infer_declaration ~trust env kn dcl =
Polymorphic_const (Univ.ACumulativityInfo.univ_context acumi)
in
let term, typ = pb.proj_eta in
- Def (Mod_subst.from_val (hcons_constr term)), RegularArity typ, Some pb,
- univs, false, 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
+ {
+ Cooking.cook_body = Def (Mod_subst.from_val (hcons_constr term));
+ cook_type = typ;
+ cook_proj = Some pb;
+ cook_universes = univs;
+ cook_inline = false;
+ cook_context = None;
+ }
let record_aux env s_ty s_bo suggested_expr =
let in_ty = keep_hyps env s_ty in
@@ -349,7 +381,9 @@ let record_aux env s_ty s_bo suggested_expr =
let suggest_proof_using = ref (fun _ _ _ _ _ -> "")
let set_suggest_proof_using f = suggest_proof_using := f
-let build_constant_declaration kn env (def,typ,proj,univs,inline_code,ctx) =
+let build_constant_declaration kn env result =
+ let open Cooking in
+ let typ = result.cook_type in
let check declared inferred =
let mk_set l = List.fold_right Id.Set.add (List.map NamedDecl.get_id l) Id.Set.empty in
let inferred_set, declared_set = mk_set inferred, mk_set declared in
@@ -376,11 +410,12 @@ let build_constant_declaration kn env (def,typ,proj,univs,inline_code,ctx) =
(* We try to postpone the computation of used section variables *)
let hyps, def =
let context_ids = List.map NamedDecl.get_id (named_context env) in
- match ctx with
+ let def = result.cook_body in
+ match result.cook_context with
| 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)
@@ -408,20 +443,21 @@ let build_constant_declaration kn env (def,typ,proj,univs,inline_code,ctx) =
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
+ let univs = result.cook_universes in
let tps =
let res =
- match proj with
+ match result.cook_proj with
| None -> compile_constant_body env univs def
| Some pb ->
(* The compilation of primitive projections is a bit tricky, because
@@ -434,10 +470,10 @@ let build_constant_declaration kn env (def,typ,proj,univs,inline_code,ctx) =
{ const_hyps = hyps;
const_body = def;
const_type = typ;
- const_proj = proj;
+ const_proj = result.cook_proj;
const_body_code = None;
const_universes = univs;
- const_inline_code = inline_code;
+ const_inline_code = result.cook_inline;
const_typing_flags = Environ.typing_flags env;
}
in
@@ -448,10 +484,10 @@ let build_constant_declaration kn env (def,typ,proj,univs,inline_code,ctx) =
{ const_hyps = hyps;
const_body = def;
const_type = typ;
- const_proj = proj;
+ const_proj = result.cook_proj;
const_body_code = tps;
const_universes = univs;
- const_inline_code = inline_code;
+ const_inline_code = result.cook_inline;
const_typing_flags = Environ.typing_flags env }
(*s Global and local constant declaration. *)
@@ -461,11 +497,12 @@ let translate_constant mb env kn ce =
(infer_declaration ~trust:mb env (Some kn) ce)
let constant_entry_of_side_effect cb u =
- let poly, univs =
+ let univs =
match cb.const_universes with
- | Monomorphic_const ctx -> false, ctx
+ | Monomorphic_const uctx ->
+ Monomorphic_const_entry uctx
| Polymorphic_const auctx ->
- true, Univ.AUContext.repr auctx
+ Polymorphic_const_entry (Univ.AUContext.repr auctx)
in
let pt =
match cb.const_body, u with
@@ -473,12 +510,10 @@ let constant_entry_of_side_effect cb u =
| Def b, `Nothing -> Mod_subst.force_constr b, Univ.ContextSet.empty
| _ -> assert false in
DefinitionEntry {
- const_entry_body = Future.from_val (pt, empty_seff);
+ 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_polymorphic = poly;
+ 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 }
@@ -497,17 +532,18 @@ type side_effect_role =
| Schema of inductive * string
type exported_side_effect =
- constant * constant_body * side_effects constant_entry * side_effect_role
+ constant * constant_body * side_effect_role
let export_side_effects mb env ce =
match ce with
- | ParameterEntry _ | ProjectionEntry _ -> [], ce
+ | ParameterEntry e -> [], ParameterEntry e
+ | ProjectionEntry e -> [], ProjectionEntry e
| DefinitionEntry c ->
let { const_entry_body = body } = c in
let _, eff = Future.force body in
let ce = DefinitionEntry { c with
const_entry_body = Future.chain ~pure:true body
- (fun (b_ctx, _) -> b_ctx, empty_seff) } in
+ (fun (b_ctx, _) -> b_ctx, ()) } in
let not_exists (c,_,_,_) =
try ignore(Environ.lookup_constant c env); false
with Not_found -> true in
@@ -547,8 +583,8 @@ let export_side_effects mb env ce =
let env, cbs =
List.fold_left (fun (env,cbs) (kn, ocb, u, r) ->
let ce = constant_entry_of_side_effect ocb u in
- let cb = translate_constant mb env kn ce in
- (push_seff env (kn, cb,`Nothing, Subproof),(kn,cb,ce,r) :: cbs))
+ let cb = translate_constant Pure env kn ce in
+ (push_seff env (kn, cb,`Nothing, Subproof),(kn,cb,r) :: cbs))
(env,[]) cbs in
translate_seff sl rest (cbs @ acc) env
| Some sl, cbs :: rest ->
@@ -556,7 +592,7 @@ let export_side_effects mb env ce =
let cbs = List.map turn_direct cbs in
let env = List.fold_left push_seff env cbs in
let ecbs = List.map (fun (kn,cb,u,r) ->
- kn, cb, constant_entry_of_side_effect cb u, r) cbs in
+ kn, cb, r) cbs in
translate_seff (Some (sl-cbs_len)) rest (ecbs @ acc) env
in
translate_seff trusted seff [] env
@@ -575,11 +611,11 @@ let translate_recipe env kn r =
build_constant_declaration kn env (Cooking.cook_constant ~hcons env r)
let translate_local_def mb env id centry =
- let def,typ,proj,univs,inline_code,ctx =
- infer_declaration ~trust:mb env None (DefinitionEntry centry) in
- let typ = type_of_constant_type env typ in
- if ctx = None && !Flags.compilation_mode = Flags.BuildVo then begin
- match def with
+ let open Cooking in
+ let decl = infer_declaration ~trust:mb env None (DefinitionEntry centry) 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 _ -> ()
| Def _ -> ()
| OpaqueDef lc ->
@@ -592,7 +628,11 @@ let translate_local_def mb env id centry =
env ids_def ids_typ context_ids in
record_aux env ids_typ ids_def expr
end;
- def, typ, univs
+ let univs = match decl.cook_universes with
+ | Monomorphic_const ctx -> ctx
+ | Polymorphic_const _ -> assert false
+ in
+ decl.cook_body, typ, univs
(* Insertion of inductive types. *)
@@ -602,7 +642,7 @@ let inline_entry_side_effects env ce = { ce with
const_entry_body = Future.chain ~pure:true
ce.const_entry_body (fun ((body, ctx), side_eff) ->
let body, ctx',_ = inline_side_effects env body ctx side_eff in
- (body, ctx'), empty_seff);
+ (body, ctx'), ());
}
let inline_side_effects env body side_eff =
diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli
index 77d126074f..24153343e7 100644
--- a/kernel/term_typing.mli
+++ b/kernel/term_typing.mli
@@ -14,8 +14,12 @@ open Entries
type side_effects
-val translate_local_def : structure_body -> env -> Id.t -> side_effects definition_entry ->
- constant_def * types * constant_universes
+type _ trust =
+| Pure : unit trust
+| SideEffects : structure_body -> side_effects trust
+
+val translate_local_def : 'a trust -> env -> Id.t -> 'a definition_entry ->
+ constant_def * types * Univ.universe_context
val translate_local_assum : env -> types -> types
@@ -26,7 +30,7 @@ val inline_side_effects : env -> constr -> side_effects -> constr
redexes. *)
val inline_entry_side_effects :
- env -> side_effects definition_entry -> side_effects definition_entry
+ env -> side_effects definition_entry -> unit definition_entry
(** Same as {!inline_side_effects} but applied to entries. Only modifies the
{!Entries.const_entry_body} field. It is meant to get a term out of a not
yet type checked proof. *)
@@ -43,7 +47,7 @@ val uniq_seff : side_effects -> side_effect list
val equal_eff : side_effect -> side_effect -> bool
val translate_constant :
- structure_body -> env -> constant -> side_effects constant_entry ->
+ 'a trust -> env -> constant -> 'a constant_entry ->
constant_body
type side_effect_role =
@@ -51,7 +55,7 @@ type side_effect_role =
| Schema of inductive * string
type exported_side_effect =
- constant * constant_body * side_effects constant_entry * side_effect_role
+ constant * constant_body * side_effect_role
(* Given a constant entry containing side effects it exports them (either
* by re-checking them or trusting them). Returns the constant bodies to
@@ -59,10 +63,7 @@ type exported_side_effect =
* needs to be translated as usual after this step. *)
val export_side_effects :
structure_body -> env -> side_effects constant_entry ->
- exported_side_effect list * side_effects constant_entry
-
-val constant_entry_of_side_effect :
- constant_body -> seff_env -> side_effects constant_entry
+ exported_side_effect list * unit constant_entry
val translate_mind :
env -> mutual_inductive -> mutual_inductive_entry -> mutual_inductive_body
@@ -71,8 +72,8 @@ val translate_recipe : env -> constant -> Cooking.recipe -> constant_body
(** Internal functions, mentioned here for debug purpose only *)
-val infer_declaration : trust:structure_body -> env -> constant option ->
- side_effects constant_entry -> Cooking.result
+val infer_declaration : trust:'a trust -> env -> constant option ->
+ 'a constant_entry -> Cooking.result
val build_constant_declaration :
constant -> env -> Cooking.result -> constant_body
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
diff --git a/kernel/uGraph.mli b/kernel/uGraph.mli
index 4de373eb4c..2fe5550184 100644
--- a/kernel/uGraph.mli
+++ b/kernel/uGraph.mli
@@ -59,7 +59,7 @@ val check_subtype : AUContext.t check_function
(** {6 Pretty-printing of universes. } *)
-val pr_universes : (Level.t -> Pp.std_ppcmds) -> universes -> Pp.std_ppcmds
+val pr_universes : (Level.t -> Pp.t) -> universes -> Pp.t
(** {6 Dumping to a file } *)
diff --git a/kernel/univ.ml b/kernel/univ.ml
index 02b02db893..d915fb8c98 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -892,7 +892,7 @@ module Instance : sig
val subst_fn : universe_level_subst_fn -> t -> t
- val pr : (Level.t -> Pp.std_ppcmds) -> t -> Pp.std_ppcmds
+ val pr : (Level.t -> Pp.t) -> t -> Pp.t
val levels : t -> LSet.t
end =
struct
diff --git a/kernel/univ.mli b/kernel/univ.mli
index 99092a543e..a4f2e26b63 100644
--- a/kernel/univ.mli
+++ b/kernel/univ.mli
@@ -37,7 +37,7 @@ sig
(** Create a new universe level from a unique identifier and an associated
module path. *)
- val pr : t -> Pp.std_ppcmds
+ val pr : t -> Pp.t
(** Pretty-printing *)
val to_string : t -> string
@@ -56,7 +56,7 @@ module LSet :
sig
include CSig.SetS with type elt = universe_level
- val pr : (Level.t -> Pp.std_ppcmds) -> t -> Pp.std_ppcmds
+ val pr : (Level.t -> Pp.t) -> t -> Pp.t
(** Pretty-printing *)
end
@@ -86,10 +86,10 @@ sig
val make : Level.t -> t
(** Create a universe representing the given level. *)
- val pr : t -> Pp.std_ppcmds
+ val pr : t -> Pp.t
(** Pretty-printing *)
- val pr_with : (Level.t -> Pp.std_ppcmds) -> t -> Pp.std_ppcmds
+ val pr_with : (Level.t -> Pp.t) -> t -> Pp.t
val is_level : t -> bool
(** Test if the universe is a level or an algebraic universe. *)
@@ -127,7 +127,7 @@ type universe = Universe.t
(** Alias name. *)
-val pr_uni : universe -> Pp.std_ppcmds
+val pr_uni : universe -> Pp.t
(** The universes hierarchy: Type 0- = Prop <= Type 0 = Set <= Type 1 <= ...
Typing of universes: Type 0-, Type 0 : Type 1; Type i : Type (i+1) if i>0 *)
@@ -218,7 +218,7 @@ sig
(** [subst_union x y] favors the bindings of the first map that are [Some],
otherwise takes y's bindings. *)
- val pr : ('a -> Pp.std_ppcmds) -> 'a t -> Pp.std_ppcmds
+ val pr : ('a -> Pp.t) -> 'a t -> Pp.t
(** Pretty-printing *)
end
@@ -270,7 +270,7 @@ sig
val subst_fn : universe_level_subst_fn -> t -> t
(** Substitution by a level-to-level function. *)
- val pr : (Level.t -> Pp.std_ppcmds) -> t -> Pp.std_ppcmds
+ val pr : (Level.t -> Pp.t) -> t -> Pp.t
(** Pretty-printing, no comments *)
val levels : t -> LSet.t
@@ -463,18 +463,18 @@ val make_abstract_instance : abstract_universe_context -> universe_instance
(** {6 Pretty-printing of universes. } *)
-val pr_constraint_type : constraint_type -> Pp.std_ppcmds
-val pr_constraints : (Level.t -> Pp.std_ppcmds) -> constraints -> Pp.std_ppcmds
-val pr_universe_context : (Level.t -> Pp.std_ppcmds) -> universe_context -> Pp.std_ppcmds
-val pr_cumulativity_info : (Level.t -> Pp.std_ppcmds) -> cumulativity_info -> Pp.std_ppcmds
-val pr_abstract_universe_context : (Level.t -> Pp.std_ppcmds) -> abstract_universe_context -> Pp.std_ppcmds
-val pr_abstract_cumulativity_info : (Level.t -> Pp.std_ppcmds) -> abstract_cumulativity_info -> Pp.std_ppcmds
-val pr_universe_context_set : (Level.t -> Pp.std_ppcmds) -> universe_context_set -> Pp.std_ppcmds
-val explain_universe_inconsistency : (Level.t -> Pp.std_ppcmds) ->
- univ_inconsistency -> Pp.std_ppcmds
-
-val pr_universe_level_subst : universe_level_subst -> Pp.std_ppcmds
-val pr_universe_subst : universe_subst -> Pp.std_ppcmds
+val pr_constraint_type : constraint_type -> Pp.t
+val pr_constraints : (Level.t -> Pp.t) -> constraints -> Pp.t
+val pr_universe_context : (Level.t -> Pp.t) -> universe_context -> Pp.t
+val pr_cumulativity_info : (Level.t -> Pp.t) -> cumulativity_info -> Pp.t
+val pr_abstract_universe_context : (Level.t -> Pp.t) -> abstract_universe_context -> Pp.t
+val pr_abstract_cumulativity_info : (Level.t -> Pp.t) -> abstract_cumulativity_info -> Pp.t
+val pr_universe_context_set : (Level.t -> Pp.t) -> universe_context_set -> Pp.t
+val explain_universe_inconsistency : (Level.t -> Pp.t) ->
+ univ_inconsistency -> Pp.t
+
+val pr_universe_level_subst : universe_level_subst -> Pp.t
+val pr_universe_subst : universe_subst -> Pp.t
(** {6 Hash-consing } *)
diff --git a/kernel/vm.mli b/kernel/vm.mli
index 6e9579aa46..df638acc1f 100644
--- a/kernel/vm.mli
+++ b/kernel/vm.mli
@@ -50,9 +50,9 @@ type whd =
(** For debugging purposes only *)
-val pr_atom : atom -> Pp.std_ppcmds
-val pr_whd : whd -> Pp.std_ppcmds
-val pr_stack : stack -> Pp.std_ppcmds
+val pr_atom : atom -> Pp.t
+val pr_whd : whd -> Pp.t
+val pr_stack : stack -> Pp.t
(** Constructors *)
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-29 09:52:33 +0000