package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
module Level : sig ... end

Universes.

module LSet : sig ... end
module Universe : sig ... end

Alias name.

val pr_uni : Universe.t -> Pp.t
val type0m_univ : Universe.t

The universes hierarchy: Type 0- = Prop <= Type 0 = Set <= Type 1 <= ... Typing of universes: Type 0-, Type 0 : Type 1; Type i : Type (i+1) if i>0

val type0_univ : Universe.t
val type1_univ : Universe.t
val is_type0_univ : Universe.t -> bool
val is_type0m_univ : Universe.t -> bool
val is_univ_variable : Universe.t -> bool
val is_small_univ : Universe.t -> bool
val super : Universe.t -> Universe.t
val universe_level : Universe.t -> Level.t option

univ_level_mem l u Is l is mentioned in u ?

val univ_level_mem : Level.t -> Universe.t -> bool

univ_level_rem u v min removes u from v, resulting in min if v was exactly u.

val univ_level_rem : Level.t -> Universe.t -> Universe.t -> Universe.t
Constraints.
type constraint_type = AcyclicGraph.constraint_type =
  1. | Lt
  2. | Le
  3. | Eq
type univ_constraint = Level.t * constraint_type * Level.t
module Constraints : sig ... end
module Constraint : sig ... end
val empty_constraint : Constraints.t
val union_constraint : Constraints.t -> Constraints.t -> Constraints.t
val eq_constraint : Constraints.t -> Constraints.t -> bool
type 'a constrained = 'a * Constraints.t

A value with universe Constraints.t.

val constraints_of : 'a constrained -> Constraints.t

Constrained

type 'a constraint_function = 'a -> 'a -> Constraints.t -> Constraints.t

Enforcing Constraints.t.

val enforce_eq_level : Level.t constraint_function
val enforce_leq_level : Level.t constraint_function
type explanation = (constraint_type * Level.t) list

Type explanation is used to decorate error messages to provide useful explanation why a given constraint is rejected. It is composed of a path of universes and relation kinds (r1,u1);..;(rn,un) means .. <(r1) u1 <(r2) ... <(rn) un (where <(ri) is the relation symbol denoted by ri, currently only < and <=). The lowest end of the chain is supposed known (see UniverseInconsistency exn). The upper end may differ from the second univ of UniverseInconsistency because all universes in the path are canonical. Note that each step does not necessarily correspond to an actual constraint, but reflect how the system stores the graph and may result from combination of several Constraints.t...

type univ_inconsistency = constraint_type * Universe.t * Universe.t * explanation Lazy.t option
exception UniverseInconsistency of univ_inconsistency
Support for universe polymorphism
module LMap : sig ... end
type 'a universe_map = 'a Level.Map.t
Substitution
type universe_subst_fn = Level.t -> Universe.t
type universe_level_subst_fn = Level.t -> Level.t
type universe_subst = Universe.t universe_map

A full substitution, might involve algebraic universes

type universe_level_subst = Level.t universe_map
module Variance : sig ... end
Universe instances
module Instance : sig ... end
val enforce_eq_instances : Instance.t constraint_function
val enforce_eq_variance_instances : Variance.t array -> Instance.t constraint_function
val enforce_leq_variance_instances : Variance.t array -> Instance.t constraint_function
type 'a puniverses = 'a * Instance.t
val out_punivs : 'a puniverses -> 'a
val in_punivs : 'a -> 'a puniverses
val eq_puniverses : ('a -> 'a -> bool) -> 'a puniverses -> 'a puniverses -> bool

A vector of universe levels with universe Constraints.t, representing local universe variables and associated Constraints.t; the names are user-facing names for printing

module UContext : sig ... end
module AbstractContext : sig ... end
module AUContext : sig ... end
type 'a univ_abstracted = {
  1. univ_abstracted_value : 'a;
  2. univ_abstracted_binder : AbstractContext.t;
}

A value with bound universe levels.

val map_univ_abstracted : ('a -> 'b) -> 'a univ_abstracted -> 'b univ_abstracted

Universe contexts (as sets)

A set of universes with universe Constraints.t. We linearize the set to a list after typechecking. Beware, representation could change.

module ContextSet : sig ... end
type 'a in_universe_context = 'a * UContext.t

A value in a universe context (resp. context set).

type 'a in_universe_context_set = 'a * ContextSet.t
val extend_in_context_set : 'a in_universe_context_set -> ContextSet.t -> 'a in_universe_context_set
val empty_level_subst : universe_level_subst
val is_empty_level_subst : universe_level_subst -> bool
val subst_univs_level_level : universe_level_subst -> Level.t -> Level.t

Substitution of universes.

val subst_univs_level_universe : universe_level_subst -> Universe.t -> Universe.t
val subst_univs_level_constraints : universe_level_subst -> Constraints.t -> Constraints.t
val subst_univs_level_abstract_universe_context : universe_level_subst -> AbstractContext.t -> AbstractContext.t
val subst_univs_level_instance : universe_level_subst -> Instance.t -> Instance.t

Level to universe substitutions.

val make_subst : universe_subst -> universe_subst_fn
val subst_univs_universe : universe_subst_fn -> Universe.t -> Universe.t

Only user in the kernel is template polymorphism. Ideally we get rid of this code if it goes away.

val subst_instance_instance : Instance.t -> Instance.t -> Instance.t

Substitution of instances

val subst_instance_universe : Instance.t -> Universe.t -> Universe.t
val make_instance_subst : Instance.t -> universe_level_subst

Creates u(0) ↦ 0; ...; u(n-1) ↦ n - 1 out of u(0); ...; u(n - 1)

val make_inverse_instance_subst : Instance.t -> universe_level_subst
val abstract_universes : UContext.t -> Instance.t * AbstractContext.t

TODO: move universe abstraction out of the kernel

val make_abstract_instance : AbstractContext.t -> Instance.t
val compact_univ : Universe.t -> Universe.t * int list

compact_univ u remaps local variables in u such that their indices become consecutive. It returns the new universe and the mapping. Example: compact_univ (Var 0, i); (Prop, 0); (Var 2; j)) = (Var 0,i); (Prop, 0); (Var 1; j), 0; 2

Pretty-printing of universes.
val pr_constraint_type : constraint_type -> Pp.t
val pr_constraints : (Level.t -> Pp.t) -> Constraints.t -> Pp.t
val pr_universe_context : (Level.t -> Pp.t) -> ?variance:Variance.t array -> UContext.t -> Pp.t
val pr_abstract_universe_context : (Level.t -> Pp.t) -> ?variance:Variance.t array -> AbstractContext.t -> Pp.t
val pr_universe_context_set : (Level.t -> Pp.t) -> ContextSet.t -> Pp.t
val explain_universe_inconsistency : (Level.t -> Pp.t) -> univ_inconsistency -> Pp.t
val pr_universe_level_subst : universe_level_subst -> Pp.t
val pr_universe_subst : universe_subst -> Pp.t
Hash-consing
val hcons_univ : Universe.t -> Universe.t
val hcons_constraints : Constraints.t -> Constraints.t
val hcons_universe_set : Level.Set.t -> Level.Set.t
val hcons_universe_context : UContext.t -> UContext.t
val hcons_abstract_universe_context : AbstractContext.t -> AbstractContext.t
val hcons_universe_context_set : ContextSet.t -> ContextSet.t