Module Environ

Unsafe environments. We define here a datatype for environments. Since typing is not yet defined, it is not possible to check the informations added in environments, and that is why we speak here of ``unsafe'' environments.

Environments have the following components:

Linking information for the native compiler

type key = int CEphemeron.key option Stdlib.ref
type constant_key = Declarations.constant_body * (link_info Stdlib.ref * key)
type mind_key = Declarations.mutual_inductive_body * link_info Stdlib.ref
module Globals : sig ... end
type named_context_val = private {
env_named_ctx : Constr.named_context;
env_named_map : Constr.named_declaration Names.Id.Map.t;(*

Identifier-indexed version of env_named_ctx

*)
env_named_idx : Constr.named_declaration Range.t;(*

Same as env_named_ctx but with a fast-access list.

*)
}
type rel_context_val = private {
env_rel_ctx : Constr.rel_context;
env_rel_map : Constr.rel_declaration Range.t;
}
type env = private {
env_globals : Globals.t;
env_named_context : named_context_val;
env_rel_context : rel_context_val;
env_nb_rel : int;
env_universes : UGraph.t;
env_universes_lbound : UGraph.Bound.t;
irr_constants : Names.Cset_env.t;
irr_inds : Names.Indset_env.t;
env_typing_flags : Declarations.typing_flags;
retroknowledge : Retroknowledge.retroknowledge;
}
val oracle : env -> Conv_oracle.oracle
val set_oracle : env -> Conv_oracle.oracle -> env
val eq_named_context_val : named_context_val -> named_context_val -> bool
val empty_env : env
val universes : env -> UGraph.t
val universes_lbound : env -> UGraph.Bound.t
val set_universes_lbound : env -> UGraph.Bound.t -> env
val rel_context : env -> Constr.rel_context
val named_context : env -> Constr.named_context
val named_context_val : env -> named_context_val
val set_universes : UGraph.t -> env -> env
val typing_flags : env -> Declarations.typing_flags
val is_impredicative_set : env -> bool
val type_in_type : env -> bool
val deactivated_guard : env -> bool
val indices_matter : env -> bool
val is_impredicative_sort : env -> Sorts.t -> bool
val is_impredicative_family : env -> Sorts.family -> bool
val empty_context : env -> bool

is the local context empty

Context of de Bruijn variables (rel_context)
val nb_rel : env -> int
val push_rel : Constr.rel_declaration -> env -> env
val push_rel_context : Constr.rel_context -> env -> env
val push_rec_types : Constr.rec_declaration -> env -> env
val push_rel_context_val : Constr.rel_declaration -> rel_context_val -> rel_context_val
val set_rel_context_val : rel_context_val -> env -> env
val empty_rel_context_val : rel_context_val
val lookup_rel : int -> env -> Constr.rel_declaration

Looks up in the context of local vars referred by indice (rel_context) raises Not_found if the index points out of the context

val evaluable_rel : int -> env -> bool
val env_of_rel : int -> env -> env
Recurrence on rel_context
val fold_rel_context : ( env -> Constr.rel_declaration -> 'a -> 'a ) -> env -> init:'a -> 'a
Context of variables (section variables and goal assumptions)
val named_context_of_val : named_context_val -> Constr.named_context
val val_of_named_context : Constr.named_context -> named_context_val
val empty_named_context_val : named_context_val
val ids_of_named_context_val : named_context_val -> Names.Id.Set.t

map_named_val f ctxt apply f to the body and the type of each declarations. *** /!\ *** f t should be convertible with t, and preserve the name

val push_named : Constr.named_declaration -> env -> env
val push_named_context : Constr.named_context -> env -> env

Looks up in the context of local vars referred by names (named_context) raises Not_found if the Id.t is not found

val evaluable_named : Names.variable -> env -> bool
val named_type : Names.variable -> env -> Constr.types
val named_body : Names.variable -> env -> Constr.constr option
Recurrence on named_context: older declarations processed first
val fold_named_context : ( env -> Constr.named_declaration -> 'a -> 'a ) -> env -> init:'a -> 'a
val match_named_context_val : named_context_val -> (Constr.named_declaration * named_context_val) option
val fold_named_context_reverse : ( 'a -> Constr.named_declaration -> 'a ) -> init:'a -> env -> 'a

Recurrence on named_context starting from younger decl

val reset_context : env -> env

This forgets named and rel contexts

val reset_with_named_context : named_context_val -> env -> env

This forgets rel context and sets a new named context

val pop_rel_context : int -> env -> env

This removes the n last declarations from the rel context

val fold_constants : ( Names.Constant.t -> Declarations.constant_body -> 'a -> 'a ) -> env -> 'a -> 'a

Useful for printing

val fold_inductives : ( Names.MutInd.t -> Declarations.mutual_inductive_body -> 'a -> 'a ) -> env -> 'a -> 'a
Global constants
Add entries to global environment
val add_constant_key : Names.Constant.t -> Declarations.constant_body -> link_info -> env -> env
val lookup_constant_key : Names.Constant.t -> env -> constant_key
val lookup_constant : Names.Constant.t -> env -> Declarations.constant_body

Looks up in the context of global constant names raises an anomaly if the required path is not found

val evaluable_constant : Names.Constant.t -> env -> bool
val mem_constant : Names.Constant.t -> env -> bool
val polymorphic_constant : Names.Constant.t -> env -> bool

New-style polymorphism

val polymorphic_pconstant : Constr.pconstant -> env -> bool
val type_in_type_constant : Names.Constant.t -> env -> bool
...

constant_value env c raises NotEvaluableConst Opaque if c is opaque, NotEvaluableConst NoBody if it has no body, NotEvaluableConst IsProj if c is a projection, NotEvaluableConst (IsPrimitive p) if c is primitive p and an anomaly if it does not exist in env

type const_evaluation_result =
| NoBody
| Opaque
| IsPrimitive of Univ.Instance.t * CPrimitives.t
exception NotEvaluableConst of const_evaluation_result
val constant_value_and_type : env -> Names.Constant.t Univ.puniverses -> Constr.constr option * Constr.types * Univ.Constraints.t

The universe context associated to the constant, empty if not polymorphic

val constant_context : env -> Names.Constant.t -> Univ.AbstractContext.t

The universe context associated to the constant, empty if not polymorphic

val constant_value_in : env -> Names.Constant.t Univ.puniverses -> Constr.constr
val constant_type_in : env -> Names.Constant.t Univ.puniverses -> Constr.types
val constant_opt_value_in : env -> Names.Constant.t Univ.puniverses -> Constr.constr option
val is_primitive : env -> Names.Constant.t -> bool
val get_primitive : env -> Names.Constant.t -> CPrimitives.t option
val is_array_type : env -> Names.Constant.t -> bool
val is_int63_type : env -> Names.Constant.t -> bool
val is_float64_type : env -> Names.Constant.t -> bool
val is_primitive_type : env -> Names.Constant.t -> bool
Primitive projections
val lookup_projection : Names.Projection.t -> env -> Constr.types

Checks that the number of parameters is correct.

val get_projection : env -> Names.inductive -> proj_arg:int -> Names.Projection.Repr.t

Anomaly when not a primitive record or invalid proj_arg.

val get_projections : env -> Names.inductive -> Names.Projection.Repr.t array option
val lookup_mind_key : Names.MutInd.t -> env -> mind_key

Inductive types

val add_mind_key : Names.MutInd.t -> mind_key -> env -> env

Looks up in the context of global inductive names raises an anomaly if the required path is not found

val mem_mind : Names.MutInd.t -> env -> bool
val mind_context : env -> Names.MutInd.t -> Univ.AbstractContext.t

The universe context associated to the inductive, empty if not polymorphic

val polymorphic_ind : Names.inductive -> env -> bool

New-style polymorphism

val polymorphic_pind : Constr.pinductive -> env -> bool
val type_in_type_ind : Names.inductive -> env -> bool
val template_polymorphic_ind : Names.inductive -> env -> bool

Old-style polymorphism

val template_polymorphic_variables : Names.inductive -> env -> Univ.Level.t list
val template_polymorphic_pind : Constr.pinductive -> env -> bool
Name quotients
module type QNameS = sig ... end
module QConstant : QNameS with type t = Names.Constant.t
module QMutInd : QNameS with type t = Names.MutInd.t
module QInd : QNameS with type t = Names.Ind.t
module QConstruct : QNameS with type t = Names.Construct.t
module QProjection : sig ... end
module QGlobRef : QNameS with type t = Names.GlobRef.t
Modules
val add_modtype : Declarations.module_type_body -> env -> env
val shallow_add_module : Declarations.module_body -> env -> env

shallow_add_module does not add module components

val lookup_module : Names.ModPath.t -> env -> Declarations.module_body
Universe constraints
val add_constraints : Univ.Constraints.t -> env -> env

Add universe constraints to the environment.

  • raises UniverseInconsistency.
val check_constraints : Univ.Constraints.t -> env -> bool

Check constraints are satifiable in the environment.

val push_context : ?strict:bool -> Univ.UContext.t -> env -> env

push_context ?(strict=false) ctx env pushes the universe context to the environment.

  • raises UGraph.AlreadyDeclared

    if one of the universes is already declared.

val push_context_set : ?strict:bool -> Univ.ContextSet.t -> env -> env

push_context_set ?(strict=false) ctx env pushes the universe context set to the environment. It does not fail even if one of the universes is already declared.

val push_subgraph : Univ.ContextSet.t -> env -> env

push_subgraph univs env adds the universes and constraints in univs to env as push_context_set ~strict:false univs env, and also checks that they do not imply new transitive constraints between pre-existing universes in env.

val set_typing_flags : Declarations.typing_flags -> env -> env
val set_impredicative_set : bool -> env -> env
val set_type_in_type : bool -> env -> env
val set_allow_sprop : bool -> env -> env
val sprop_allowed : env -> bool
val update_typing_flags : ?typing_flags:Declarations.typing_flags -> env -> env

update_typing_flags ?typing_flags may update env with optional typing flags

val universes_of_global : env -> Names.GlobRef.t -> Univ.AbstractContext.t
Sets of referred section variables

global_vars_set env c returns the list of id's occurring either directly as Var id in c or indirectly as a section variable dependent in a global reference occurring in c

val global_vars_set : env -> Constr.constr -> Names.Id.Set.t
val vars_of_global : env -> Names.GlobRef.t -> Names.Id.Set.t
val really_needed : env -> Names.Id.Set.t -> Names.Id.Set.t

closure of the input id set w.r.t. dependency

val keep_hyps : env -> Names.Id.Set.t -> Constr.named_context

like really_needed but computes a well ordered named context

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 ('constr, 'types) punsafe_judgment = {
uj_val : 'constr;
uj_type : 'types;
}
val on_judgment : ( 'a -> 'b ) -> ( 'a, 'a ) punsafe_judgment -> ( 'b, 'b ) punsafe_judgment
val on_judgment_value : ( 'c -> 'c ) -> ( 'c, 't ) punsafe_judgment -> ( 'c, 't ) punsafe_judgment
val on_judgment_type : ( 't -> 't ) -> ( 'c, 't ) punsafe_judgment -> ( 'c, 't ) punsafe_judgment
type unsafe_judgment = ( Constr.constr, Constr.types ) punsafe_judgment
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 ('types, 'sorts) punsafe_type_judgment = {
utj_val : 'types;
utj_type : 'sorts;
}
type unsafe_type_judgment = ( Constr.types, Sorts.t ) punsafe_type_judgment
exception Hyp_not_found

apply_to_hyp sign id f split sign into tail::(id,_,_)::head and return tail::(f head (id,_,_) (rev tail))::head. the value associated to id should not change

val is_polymorphic : env -> Names.GlobRef.t -> bool
val is_template_polymorphic : env -> Names.GlobRef.t -> bool
val get_template_polymorphic_variables : env -> Names.GlobRef.t -> Univ.Level.t list
val is_type_in_type : env -> Names.GlobRef.t -> bool

Native compiler

val set_retroknowledge : env -> Retroknowledge.retroknowledge -> env

Primitives