Module `Environ`Source

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:

a context for de Bruijn variables
a context for de Bruijn variables vm values
a context for section variables and goal assumptions
a context for section variables and goal assumptions vm values
a context for global constants and axioms
a context for inductive definitions
a set of universe constraints
a flag telling if Set is, can be, or cannot be set impredicative

Sourcetype link_info =

| Linked of string
| NotLinked

Linking information for the native compiler

Sourcetype key = int CEphemeron.key option ref

Sourcetype constant_key = Declarations.constant_body * (link_info ref * key)

Sourcetype mind_key = Declarations.mutual_inductive_body * link_info ref

Sourcemodule Globals : sig ... end

Sourcetype 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.
*)

}

Sourcetype rel_context_val = private {

env_rel_ctx : Constr.rel_context;
env_rel_map : Constr.rel_declaration Range.t;

}

Sourcetype 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;
indirect_pterms : Opaqueproof.opaquetab;

}

Sourceval oracle : env -> Conv_oracle.oracle

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 universes_lbound : env -> UGraph.Bound.t

Sourceval set_universes_lbound : env -> UGraph.Bound.t -> env

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 opaque_tables : env -> Opaqueproof.opaquetab

Sourceval set_opaque_tables : env -> Opaqueproof.opaquetab -> 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 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`

Source

val 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

Source

val map_named_val : 
  (Constr.named_declaration -> Constr.named_declaration) ->
  named_context_val ->
  named_context_val

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

Source

val push_named_context_val : 
  Constr.named_declaration ->
  named_context_val ->
  named_context_val

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

Sourceval lookup_named : Names.variable -> env -> Constr.named_declaration

Source

val lookup_named_ctxt : 
  Names.variable ->
  named_context_val ->
  Constr.named_declaration

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

Source

val fold_named_context : 
  (env -> Constr.named_declaration -> 'a -> 'a) ->
  env ->
  init:'a ->
  'a

Source

val match_named_context_val : 
  named_context_val ->
  (Constr.named_declaration * named_context_val) option

Source

val 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

Source

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

Useful for printing

Source

val fold_inductives : 
  (Names.MutInd.t -> Declarations.mutual_inductive_body -> 'a -> 'a) ->
  env ->
  'a ->
  'a

Global constants

Add entries to global environment

Sourceval add_constant : Names.Constant.t -> Declarations.constant_body -> env -> env

Source

val add_constant_key : 
  Names.Constant.t ->
  Declarations.constant_body ->
  link_info ->
  env ->
  env

Sourceval lookup_constant_key : Names.Constant.t -> env -> constant_key

Sourceval 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

Sourceval evaluable_constant : Names.Constant.t -> env -> bool

Sourceval mem_constant : Names.Constant.t -> env -> bool

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 =

| NoBody
| Opaque
| IsPrimitive of Univ.Instance.t * CPrimitives.t

Sourceexception NotEvaluableConst of const_evaluation_result

Source

val constant_type : 
  env ->
  Names.Constant.t Univ.puniverses ->
  Constr.types Univ.constrained

Source

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

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

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

Source

val constant_value_in : 
  env ->
  Names.Constant.t Univ.puniverses ->
  Constr.constr

Sourceval constant_type_in : env -> Names.Constant.t Univ.puniverses -> Constr.types

Source

val constant_opt_value_in : 
  env ->
  Names.Constant.t Univ.puniverses ->
  Constr.constr option

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_primitive_type : env -> Names.Constant.t -> bool

Primitive projections

Sourceval lookup_projection : Names.Projection.t -> env -> Constr.types

Checks that the number of parameters is correct.

Source

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

Anomaly when not a primitive record or invalid proj_arg.

Source

val get_projections : 
  env ->
  Names.inductive ->
  Names.Projection.Repr.t 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

Source

val add_mind : 
  Names.MutInd.t ->
  Declarations.mutual_inductive_body ->
  env ->
  env

Sourceval lookup_mind : Names.MutInd.t -> env -> Declarations.mutual_inductive_body

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

Sourceval mind_context : env -> Names.MutInd.t -> Univ.AbstractContext.t

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

Source

val template_polymorphic_variables : 
  Names.inductive ->
  env ->
  Univ.Level.t list

Sourceval template_polymorphic_pind : Constr.pinductive -> env -> bool

Name quotients

Sourcemodule type QNameS = sig ... end

Sourcemodule QConstant : QNameS with type t = Names.Constant.t

Sourcemodule QMutInd : QNameS with type t = Names.MutInd.t

Sourcemodule QInd : QNameS with type t = Names.Ind.t

Sourcemodule QConstruct : QNameS with type t = Names.Construct.t

Sourcemodule QProjection : sig ... end

Sourcemodule QGlobRef : QNameS with type t = Names.GlobRef.t

Modules

Sourceval add_modtype : Declarations.module_type_body -> env -> env

Sourceval shallow_add_module : Declarations.module_body -> env -> env

shallow_add_module does not add module components

Sourceval lookup_module : Names.ModPath.t -> env -> Declarations.module_body

Sourceval lookup_modtype : Names.ModPath.t -> env -> Declarations.module_type_body

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

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_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_cumulative_sprop : bool -> env -> env

Sourceval set_type_in_type : bool -> env -> env

Sourceval set_allow_sprop : bool -> env -> env

Sourceval sprop_allowed : env -> bool

Sourceval same_flags : Declarations.typing_flags -> Declarations.typing_flags -> 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 -> 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

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

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

Sourcetype ('constr, 'types) punsafe_judgment = {

uj_val : 'constr;
uj_type : 'types;

}

Source

val on_judgment : 
  ('a -> 'b) ->
  ('a, 'a) punsafe_judgment ->
  ('b, 'b) punsafe_judgment

Source

val on_judgment_value : 
  ('c -> 'c) ->
  ('c, 't) punsafe_judgment ->
  ('c, 't) punsafe_judgment

Source

val on_judgment_type : 
  ('t -> 't) ->
  ('c, 't) punsafe_judgment ->
  ('c, 't) punsafe_judgment

Sourcetype unsafe_judgment = (Constr.constr, Constr.types) 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 punsafe_type_judgment = {

utj_val : 'types;
utj_type : Sorts.t;

}

Sourcetype unsafe_type_judgment = Constr.types punsafe_type_judgment

Sourceexception Hyp_not_found

Source

val apply_to_hyp : 
  named_context_val ->
  Names.variable ->
  (Constr.named_context ->
    Constr.named_declaration ->
    Constr.named_context ->
    Constr.named_declaration) ->
  named_context_val

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

Source

val remove_hyps : 
  Names.Id.Set.t ->
  (Constr.named_declaration -> Constr.named_declaration) ->
  named_context_val ->
  named_context_val

Sourceval is_polymorphic : env -> Names.GlobRef.t -> bool

Sourceval is_template_polymorphic : env -> Names.GlobRef.t -> bool

Source

val get_template_polymorphic_variables : 
  env ->
  Names.GlobRef.t ->
  Univ.Level.t list

Sourceval is_type_in_type : env -> Names.GlobRef.t -> bool

Sourceval no_link_info : link_info

Native compiler

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

Primitives

Install

Dune Dependency

Authors

Maintainers

Sources

doc/coq-core.kernel/Environ/index.html

Module `Environ`Source

Context of de Bruijn variables (`rel_context`)

Recurrence on `rel_context`

Context of variables (section variables and goal assumptions)

Recurrence on `named_context`: older declarations processed first

Global constants

Add entries to global environment

...

Primitive projections

Name quotients

Modules

Universe constraints

Sets of referred section variables

Unsafe judgments.

package coq-core

Install

Dune Dependency

Authors

Maintainers

Sources

doc/coq-core.kernel/Environ/index.html

Module EnvironSource

Context of de Bruijn variables (rel_context)

Recurrence on rel_context

Context of variables (section variables and goal assumptions)

Recurrence on named_context: older declarations processed first

Global constants

Add entries to global environment

...

Primitive projections

Name quotients

Modules

Universe constraints

Sets of referred section variables

Unsafe judgments.

Module `Environ`Source

Context of de Bruijn variables (`rel_context`)

Recurrence on `rel_context`

Recurrence on `named_context`: older declarations processed first