package coq

  1. Overview
  2. Docs
package coq
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

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:

  • 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 lazy_val
Sourceval build_lazy_val : lazy_val -> (Vmvalues.values * Names.Id.Set.t) -> unit
Sourceval force_lazy_val : lazy_val -> (Vmvalues.values * Names.Id.Set.t) option
Sourceval dummy_lazy_val : unit -> lazy_val

Linking information for the native compiler

Sourcetype key = int CEphemeron.key option ref
Sourcemodule Globals : sig ... end
Sourcetype stratification = {
  1. env_universes : UGraph.t;
  2. env_sprop_allowed : bool;
  3. env_universes_lbound : UGraph.Bound.t;
  4. env_engagement : Declarations.engagement;
}
Sourcetype named_context_val = private {
  1. env_named_ctx : Constr.named_context;
  2. env_named_map : (Constr.named_declaration * lazy_val) Names.Id.Map.t;
    (*

    Identifier-indexed version of env_named_ctx

    *)
  3. env_named_var : Constr.t list;
    (*

    List of identifiers in env_named_ctx, in the same order, including let-ins. This is not used in the kernel, but is critical to preserve sharing of evar instances in the proof engine.

    *)
}
Sourcetype rel_context_val = private {
  1. env_rel_ctx : Constr.rel_context;
  2. env_rel_map : (Constr.rel_declaration * lazy_val) 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_stratification : stratification;
  6. env_typing_flags : Declarations.typing_flags;
  7. retroknowledge : Retroknowledge.retroknowledge;
  8. indirect_pterms : Opaqueproof.opaquetab;
}
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_univ : env -> Univ.Universe.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 lookup_rel_val : int -> env -> lazy_val
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 lookup_named_val : Names.variable -> env -> lazy_val
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 * lazy_val * 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 -> Opaqueproof.opaque 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 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 Univ.Instance.t * CPrimitives.t
Sourceexception NotEvaluableConst of const_evaluation_result

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

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

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

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

Sourceval get_projection : env -> Names.inductive -> proj_arg:int -> Names.Projection.Repr.t option
Sourceval 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

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

Sourceval 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 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.Constraint.t -> env -> env

Add universe constraints to the environment.

  • raises UniverseInconsistency.
Sourceval check_constraints : Univ.Constraint.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.

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_engagement : Declarations.engagement -> env -> env
Sourceval set_typing_flags : Declarations.typing_flags -> 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 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.AUContext.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 punsafe_type_judgment = {
  1. utj_val : 'types;
  2. utj_type : Sorts.t;
}
Sourcetype unsafe_type_judgment = Constr.types 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

Native compiler

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

Primitives

OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct