Module EnvironSource

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

Sourcetype key = int CEphemeron.key option ref
Sourcemodule Globals : sig ... end
Sourcetype named_context_val = private {
  1. env_named_ctx : Constr.named_context;
  2. env_named_map : Constr.named_declaration Names.Id.Map.t;
    (*

    Identifier-indexed version of env_named_ctx

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

    Same as env_named_ctx but with a fast-access list.

    *)
}
Sourcetype rel_context_val = private {
  1. env_rel_ctx : Constr.rel_context;
  2. env_rel_map : Constr.rel_declaration Range.t;
}
Sourcetype env = private {
  1. env_globals : Globals.t;
  2. env_named_context : named_context_val;
  3. env_rel_context : rel_context_val;
  4. env_nb_rel : int;
  5. env_universes : UGraph.t;
  6. env_qualities : Sorts.QVar.Set.t;
  7. irr_constants : Sorts.relevance Names.Cmap_env.t;
    (*

    irr_constants is a cache of the relevances which are not Relevant. In other words, const_relevance == Option.default Relevant (find_opt con irr_constants).

    *)
  8. irr_inds : Sorts.relevance Names.Indmap_env.t;
    (*

    irr_inds is a cache of the relevances which are not Relevant. cf irr_constants.

    *)
  9. symb_pats : Declarations.rewrite_rule list Names.Cmap_env.t;
  10. env_typing_flags : Declarations.typing_flags;
  11. vm_library : Vmlibrary.t;
  12. retroknowledge : Retroknowledge.retroknowledge;
  13. rewrite_rules_allowed : bool;
    (*

    Allow rewrite rules (breaks e.g. SR)

    *)
}
Sourcetype rewrule_not_allowed =
  1. | Symb
  2. | Rule
Sourceexception RewriteRulesNotAllowed of rewrule_not_allowed
Sourceval set_oracle : env -> Conv_oracle.oracle -> env
Sourceval eq_named_context_val : named_context_val -> named_context_val -> bool
Sourceval empty_env : env
Sourceval universes : env -> UGraph.t
Sourceval rel_context : env -> Constr.rel_context
Sourceval named_context : env -> Constr.named_context
Sourceval named_context_val : env -> named_context_val
Sourceval set_universes : UGraph.t -> env -> env
Sourceval typing_flags : env -> Declarations.typing_flags
Sourceval is_impredicative_set : env -> bool
Sourceval type_in_type : env -> bool
Sourceval deactivated_guard : env -> bool
Sourceval indices_matter : env -> bool
Sourceval is_impredicative_sort : env -> Sorts.t -> bool
Sourceval is_impredicative_family : env -> Sorts.family -> bool
Sourceval empty_context : env -> bool

is the local context empty

Context of de Bruijn variables (rel_context)
Sourceval nb_rel : env -> int
Sourceval push_rel : Constr.rel_declaration -> env -> env
Sourceval push_rel_context : Constr.rel_context -> env -> env
Sourceval push_rec_types : Constr.rec_declaration -> env -> env
Sourceval set_rel_context_val : rel_context_val -> env -> env
Sourceval empty_rel_context_val : rel_context_val
Sourceval 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

Sourceval evaluable_rel : int -> env -> bool
Sourceval env_of_rel : int -> env -> env
Recurrence on rel_context
Sourceval fold_rel_context : (env -> Constr.rel_declaration -> 'a -> 'a) -> env -> init:'a -> 'a
Context of variables (section variables and goal assumptions)
Sourceval named_context_of_val : named_context_val -> Constr.named_context
Sourceval val_of_named_context : Constr.named_context -> named_context_val
Sourceval empty_named_context_val : named_context_val
Sourceval 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

Sourceval push_named : Constr.named_declaration -> env -> env
Sourceval 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

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

Recurrence on named_context starting from younger decl

Sourceval reset_context : env -> env

This forgets named and rel contexts

Sourceval reset_with_named_context : named_context_val -> env -> env

This forgets rel context and sets a new named context

Sourceval pop_rel_context : int -> env -> env

This removes the n last declarations from the rel context

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

Useful for printing

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

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

Sourceval evaluable_constant : Names.Constant.t -> env -> bool
Sourceval mem_constant : Names.Constant.t -> env -> bool
Sourceval add_rewrite_rules : (Names.Constant.t * Declarations.rewrite_rule) list -> env -> env
Sourceval polymorphic_constant : Names.Constant.t -> env -> bool

New-style polymorphism

Sourceval polymorphic_pconstant : Constr.pconstant -> env -> bool
Sourceval 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

Sourcetype const_evaluation_result =
  1. | NoBody
  2. | Opaque
  3. | IsPrimitive of UVars.Instance.t * CPrimitives.t
  4. | HasRules of UVars.Instance.t * bool * Declarations.rewrite_rule list
Sourceexception NotEvaluableConst of const_evaluation_result

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

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

Sourceval constant_opt_value_in : env -> Names.Constant.t UVars.puniverses -> Constr.constr option
Sourceval is_symbol : env -> Names.Constant.t -> bool
Sourceval is_primitive : env -> Names.Constant.t -> bool
Sourceval get_primitive : env -> Names.Constant.t -> CPrimitives.t option
Sourceval is_array_type : env -> Names.Constant.t -> bool
Sourceval is_int63_type : env -> Names.Constant.t -> bool
Sourceval is_float64_type : env -> Names.Constant.t -> bool
Sourceval is_string_type : env -> Names.Constant.t -> bool
Sourceval is_primitive_type : env -> Names.Constant.t -> bool
Primitive projections

Checks that the number of parameters is correct.

Sourceval get_projection : env -> Names.inductive -> proj_arg:int -> Names.Projection.Repr.t * Sorts.relevance

Anomaly when not a primitive record or invalid proj_arg.

Sourceval get_projections : env -> Names.inductive -> (Names.Projection.Repr.t * Sorts.relevance) array option
Sourceval lookup_mind_key : Names.MutInd.t -> env -> mind_key

Inductive types

Sourceval 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

Sourceval mem_mind : Names.MutInd.t -> env -> bool

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

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

New-style polymorphism

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

Old-style polymorphism

Sourceval template_polymorphic_variables : Names.inductive -> env -> Univ.Level.t list
Sourceval template_polymorphic_pind : Constr.pinductive -> env -> bool
Changes of representation of Case nodes

Given an inductive type and its parameters, builds the context of the return clause, including the inductive being eliminated. The additional binder array is only used to set the names of the context variables, we use the less general type to make it easy to use this function on Case nodes.

Sourceval expand_branch_contexts : Declarations.mind_specif -> UVars.Instance.t -> Constr.constr array -> (Names.Name.t Constr.binder_annot array * 'a) array -> Constr.rel_context array

Given an inductive type and its parameters, builds the context of the return clause, including the inductive being eliminated. The additional binder array is only used to set the names of the context variables, we use the less general type to make it easy to use this function on Case nodes.

instantiate_context u subst nas ctx applies both u and subst to ctx while replacing names using nas (order reversed). In particular, assumes that ctx and nas have the same length.

Name quotients
Sourcemodule type QNameS = sig ... end
Sourcemodule QMutInd : QNameS with type t = Names.MutInd.t
Sourcemodule QInd : QNameS with type t = Names.Ind.t
Sourcemodule QProjection : sig ... end
Sourcemodule QGlobRef : QNameS with type t = Names.GlobRef.t
Modules
Sourceval shallow_add_module : Declarations.module_body -> env -> env

shallow_add_module does not add module components

Universe constraints
Sourceval add_constraints : Univ.Constraints.t -> env -> env

Add universe constraints to the environment.

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

Check constraints are satifiable in the environment.

Sourceval push_context : ?strict:bool -> UVars.UContext.t -> env -> env

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

Sourceval 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.

Sourceval push_floating_context_set : Univ.ContextSet.t -> env -> env

Same as above but keep the universes floating for template. Do not use.

Sourceval 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.

Sourceval set_typing_flags : Declarations.typing_flags -> env -> env
Sourceval set_impredicative_set : bool -> env -> env
Sourceval set_type_in_type : bool -> env -> env
Sourceval set_allow_sprop : bool -> env -> env
Sourceval sprop_allowed : env -> bool
Sourceval allow_rewrite_rules : env -> env
Sourceval rewrite_rules_allowed : env -> bool
Sourceval update_typing_flags : ?typing_flags:Declarations.typing_flags -> env -> env

update_typing_flags ?typing_flags may update env with optional typing flags

Sourceval universes_of_global : env -> Names.GlobRef.t -> UVars.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

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

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

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.

Sourcetype ('constr, 'types) punsafe_judgment = {
  1. uj_val : 'constr;
  2. uj_type : 'types;
}
Sourceval on_judgment : ('a -> 'b) -> ('a, 'a) punsafe_judgment -> ('b, 'b) punsafe_judgment
Sourceval on_judgment_value : ('c -> 'c) -> ('c, 't) punsafe_judgment -> ('c, 't) punsafe_judgment
Sourceval on_judgment_type : ('t -> 't) -> ('c, 't) punsafe_judgment -> ('c, 't) punsafe_judgment
Sourceval make_judge : 'constr -> 'types -> ('constr, 'types) punsafe_judgment
Sourceval j_val : ('constr, 'types) punsafe_judgment -> 'constr
Sourceval j_type : ('constr, 'types) punsafe_judgment -> 'types
Sourcetype ('types, 'sorts) punsafe_type_judgment = {
  1. utj_val : 'types;
  2. utj_type : 'sorts;
}
Sourcetype unsafe_type_judgment = (Constr.types, Sorts.t) punsafe_type_judgment
Sourceexception 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

Sourceval is_polymorphic : env -> Names.GlobRef.t -> bool
Sourceval is_template_polymorphic : env -> Names.GlobRef.t -> bool
Sourceval get_template_polymorphic_variables : env -> Names.GlobRef.t -> Univ.Level.t list
Sourceval is_type_in_type : env -> Names.GlobRef.t -> bool
VM and native
Sourceval vm_library : env -> Vmlibrary.t
Sourceval set_vm_library : Vmlibrary.t -> env -> env

Native compiler

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

Primitives