Module UVars

Support for universe polymorphism
module Variance : sig ... end
Universe instances
module Instance : sig ... end
val eq_sizes : (int * int) -> (int * int) -> bool

Convenient function to compare the result of Instance.length, UContext.size etc

type 'a pconstraints_function = 'a -> 'a -> (QPairSet.t * Univ.UnivConstraints.t) -> QPairSet.t * Univ.UnivConstraints.t
val enforce_eq_instances : Instance.t pconstraints_function
val enforce_eq_variance_instances : Variance.t array -> Instance.t pconstraints_function
val enforce_leq_variance_instances : Variance.t array -> Instance.t pconstraints_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
type bound_names = {
  1. quals : Names.Name.t array;
  2. univs : Names.Name.t array;
}
val empty_bound_names : bound_names

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

module UContext : sig ... end

A value in a universe context.

type 'a in_universe_context = 'a * UContext.t

A value in a universe context.

module AbstractContext : 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
Substitution
type universe_level_subst = Univ.Level.t Univ.Level.Map.t
val empty_level_subst : universe_level_subst
val is_empty_level_subst : universe_level_subst -> bool
val subst_univs_level_level : universe_level_subst -> Univ.Level.t -> Univ.Level.t

Substitution of universes.

val subst_univs_level_universe : universe_level_subst -> Univ.Universe.t -> Univ.Universe.t
val subst_poly_constraints : sort_level_subst -> PConstraints.t -> PConstraints.t
val pr_universe_level_subst : (Univ.Level.t -> Pp.t) -> universe_level_subst -> Pp.t
val pr_quality_level_subst : Sorts.Quality.printer -> Sorts.Quality.t Sorts.QVar.Map.t -> Pp.t
val empty_sort_subst : sort_level_subst
val is_empty_sort_subst : sort_level_subst -> bool
val subst_univs_level_abstract_universe_context : sort_level_subst -> AbstractContext.t -> AbstractContext.t

There are no constraints on qualities, so this only needs a subst for univs

val subst_sort_level_instance : sort_level_subst -> Instance.t -> Instance.t

Level to universe substitutions.

val subst_sort_level_quality : sort_level_subst -> Sorts.Quality.t -> Sorts.Quality.t
val subst_sort_level_sort : sort_level_subst -> Sorts.t -> Sorts.t
val subst_sort_level_relevance : sort_level_subst -> Sorts.relevance -> Sorts.relevance
val subst_instance_instance : Instance.t -> Instance.t -> Instance.t

Substitution of instances

val subst_instance_universe : Instance.t -> Univ.Universe.t -> Univ.Universe.t
val subst_instance_quality : Instance.t -> Sorts.Quality.t -> Sorts.Quality.t
val subst_instance_sort : Instance.t -> Sorts.t -> Sorts.t
val subst_instance_relevance : Instance.t -> Sorts.relevance -> Sorts.relevance
val subst_instance_sort_level_subst : Instance.t -> sort_level_subst -> sort_level_subst
val make_instance_subst : Instance.t -> sort_level_subst

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

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