Typeops (rocq-runtime.Typeops)

Typing functions (not yet tagged as safe)

They return unsafe judgments that are "in context" of a set of (local) universe variables (the ones that appear in the term) and associated constraints. In case of polymorphic definitions, these variables and constraints will be generalized.

When typechecking a term it may be updated to fix relevance marks. Do not discard the result.

val infer : Environ.env -> Constr.constr -> Environ.unsafe_judgment

val infer_hconstr : Environ.env -> HConstr.t -> Environ.unsafe_judgment

val infer_type : Environ.env -> Constr.types -> Environ.unsafe_type_judgment

val check_context : 
  Environ.env ->
  Constr.rel_context ->
  Environ.env * Constr.rel_context

Basic operations of the typing machine.

If j is the judgement $ c:t $ , then assumption_of_judgement env j returns the type $ c $ , checking that $ t $ is a sort.

val assumption_of_judgment : 
  Environ.env ->
  Environ.unsafe_judgment ->
  Sorts.relevance

val type1 : Constr.types

Type of sorts.

val type_of_sort : Sorts.t -> Constr.types

val type_of_relative : Environ.env -> int -> Constr.types

Type of a bound variable.

val type_of_variable : Environ.env -> Names.variable -> Constr.types

Type of variables

val type_of_constant_in : Environ.env -> Constr.pconstant -> Constr.types

type of a constant

val type_of_projection : 
  Environ.env ->
  Names.Projection.t ->
  Constr.constr ->
  Constr.types ->
  Sorts.relevance * Constr.types

type of an applied projection

val sort_of_product : Environ.env -> Sorts.t -> Sorts.t -> Sorts.t

Type of a product.

val check_cast : 
  Environ.env ->
  Environ.unsafe_judgment ->
  Constr.cast_kind ->
  Environ.unsafe_type_judgment ->
  unit

Type of a cast.

Type of global references.

val type_of_global_in_context : 
  Environ.env ->
  Names.GlobRef.t ->
  Constr.types * UVars.AbstractContext.t

Returns the type of the global reference, by creating a fresh instance of polymorphic references and computing their instantiated universe context. The type should not be used without pushing it's universe context in the environmnent of usage. For non-universe-polymorphic constants, it does not matter.

Miscellaneous.

Types for primitives

val type_of_int : Environ.env -> Constr.types

val type_of_float : Environ.env -> Constr.types

val type_of_string : Environ.env -> Constr.types

val type_of_array : Environ.env -> UVars.Instance.t -> Constr.types

val type_of_prim_type : 
  Environ.env ->
  UVars.Instance.t ->
  'a CPrimitives.prim_type ->
  Constr.types

val type_of_prim : 
  Environ.env ->
  UVars.Instance.t ->
  CPrimitives.t ->
  Constr.types

val type_of_prim_or_type : 
  Environ.env ->
  UVars.Instance.t ->
  CPrimitives.op_or_type ->
  Constr.types

val should_invert_case : 
  Environ.env ->
  Sorts.relevance ->
  Constr.case_info ->
  bool

Matches must be annotated with the indices when going from SProp to non SProp (implies 1 or 0 constructors).