diff options
Diffstat (limited to 'kernel/environ.mli')
| -rw-r--r-- | kernel/environ.mli | 98 |
1 files changed, 49 insertions, 49 deletions
diff --git a/kernel/environ.mli b/kernel/environ.mli index 6ac00088..fdd84b25 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -1,15 +1,17 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Names -open Term -open Declarations +open Constr open Univ +open Declarations (** Unsafe environments. We define here a datatype for environments. Since typing is not yet defined, it is not possible to check the @@ -80,6 +82,7 @@ val fold_rel_context : val named_context_of_val : named_context_val -> Context.Named.t val val_of_named_context : Context.Named.t -> named_context_val val empty_named_context_val : named_context_val +val ids_of_named_context_val : named_context_val -> Id.Set.t (** [map_named_val f ctxt] apply [f] to the body and the type of @@ -125,23 +128,19 @@ val pop_rel_context : int -> env -> env (** {5 Global constants } {6 Add entries to global environment } *) -val add_constant : constant -> constant_body -> env -> env -val add_constant_key : constant -> constant_body -> Pre_env.link_info -> +val add_constant : Constant.t -> constant_body -> env -> env +val add_constant_key : Constant.t -> constant_body -> Pre_env.link_info -> env -> env (** Looks up in the context of global constant names raises [Not_found] if the required path is not found *) -val lookup_constant : constant -> env -> constant_body -val evaluable_constant : constant -> env -> bool +val lookup_constant : Constant.t -> env -> constant_body +val evaluable_constant : Constant.t -> env -> bool (** New-style polymorphism *) -val polymorphic_constant : constant -> env -> bool +val polymorphic_constant : Constant.t -> 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 +val type_in_type_constant : Constant.t -> env -> bool (** {6 ... } *) (** [constant_value env c] raises [NotEvaluableConst Opaque] if @@ -149,38 +148,36 @@ val template_polymorphic_pconstant : pconstant -> env -> bool body and [NotEvaluableConst IsProj] if [c] is a projection and [Not_found] if it does not exist in [env] *) -type const_evaluation_result = NoBody | Opaque | IsProj +type const_evaluation_result = NoBody | Opaque 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.t 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 +val constant_value_and_type : env -> Constant.t puniverses -> + constr option * types * Univ.Constraint.t (** The universe context associated to the constant, empty if not polymorphic *) -val constant_context : env -> constant -> Univ.universe_context +val constant_context : env -> Constant.t -> Univ.AUContext.t (* These functions should be called under the invariant that [env] 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_opt_value_in : env -> constant puniverses -> constr option +val constant_value_in : env -> Constant.t puniverses -> constr +val constant_type_in : env -> Constant.t puniverses -> types +val constant_opt_value_in : env -> Constant.t puniverses -> constr option (** {6 Primitive projections} *) -val lookup_projection : Names.projection -> env -> projection_body -val is_projection : constant -> env -> bool +val lookup_projection : Names.Projection.t -> env -> projection_body +val is_projection : Constant.t -> env -> bool (** {5 Inductive types } *) -val add_mind_key : mutual_inductive -> Pre_env.mind_key -> env -> env -val add_mind : mutual_inductive -> mutual_inductive_body -> env -> env +val add_mind_key : MutInd.t -> Pre_env.mind_key -> env -> env +val add_mind : MutInd.t -> mutual_inductive_body -> env -> env (** Looks up in the context of global inductive names raises [Not_found] if the required path is not found *) -val lookup_mind : mutual_inductive -> env -> mutual_inductive_body +val lookup_mind : MutInd.t -> env -> mutual_inductive_body (** New-style polymorphism *) val polymorphic_ind : inductive -> env -> bool @@ -198,20 +195,20 @@ val add_modtype : module_type_body -> env -> env (** [shallow_add_module] does not add module components *) val shallow_add_module : module_body -> env -> env -val lookup_module : module_path -> env -> module_body -val lookup_modtype : module_path -> env -> module_type_body +val lookup_module : ModPath.t -> env -> module_body +val lookup_modtype : ModPath.t -> env -> module_type_body (** {5 Universe constraints } *) (** Add universe constraints to the environment. - @raises UniverseInconsistency + @raise UniverseInconsistency . *) -val add_constraints : Univ.constraints -> env -> env +val add_constraints : Univ.Constraint.t -> env -> env (** Check constraints are satifiable in the environment. *) -val check_constraints : Univ.constraints -> env -> bool -val push_context : ?strict:bool -> Univ.universe_context -> env -> env -val push_context_set : ?strict:bool -> Univ.universe_context_set -> env -> env +val check_constraints : Univ.Constraint.t -> env -> bool +val push_context : ?strict:bool -> Univ.UContext.t -> env -> env +val push_context_set : ?strict:bool -> Univ.ContextSet.t -> env -> env val push_constraints_to_env : 'a Univ.constrained -> env -> env val set_engagement : engagement -> env -> env @@ -231,29 +228,32 @@ val vars_of_global : env -> constr -> Id.Set.t val really_needed : env -> Id.Set.t -> Id.Set.t (** like [really_needed] but computes a well ordered named context *) -val keep_hyps : env -> Id.Set.t -> Context.section_context +val keep_hyps : env -> Id.Set.t -> Context.Named.t (** {5 Unsafe judgments. } We introduce here the pre-type of judgments, which is actually only a datatype to store a term with its type and the type of its type. *) -type unsafe_judgment = { - uj_val : constr; - uj_type : types } +type ('constr, 'types) punsafe_judgment = { + uj_val : 'constr; + uj_type : 'types } + +type unsafe_judgment = (constr, types) punsafe_judgment -val make_judge : constr -> types -> unsafe_judgment -val j_val : unsafe_judgment -> constr -val j_type : unsafe_judgment -> types +val make_judge : 'constr -> 'types -> ('constr, 'types) punsafe_judgment +val j_val : ('constr, 'types) punsafe_judgment -> 'constr +val j_type : ('constr, 'types) punsafe_judgment -> 'types -type unsafe_type_judgment = { - utj_val : constr; - utj_type : sorts } +type 'types punsafe_type_judgment = { + utj_val : 'types; + utj_type : Sorts.t } +type unsafe_type_judgment = types punsafe_type_judgment (** {6 Compilation of global declaration } *) -val compile_constant_body : env -> constant_universes option -> constant_def -> Cemitcodes.body_code option +val compile_constant_body : env -> constant_universes -> constant_def -> Cemitcodes.body_code option exception Hyp_not_found |