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 quconstraint_function = 'a -> 'a -> Sorts.QUConstraints.t -> Sorts.QUConstraints.t
val enforce_eq_instances : Instance.t quconstraint_function
val enforce_eq_variance_instances : Variance.t array -> Instance.t quconstraint_function
val enforce_leq_variance_instances : Variance.t array -> Instance.t quconstraint_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 = Names.Name.t array * Names.Name.t array

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

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 = {
univ_abstracted_value : 'a;
univ_abstracted_binder : AbstractContext.t;
}

A value with bound universe levels.

val map_univ_abstracted : ('a -> 'b) -> 'a univ_abstracted -> 'b univ_abstracted
Substitution
val pr_quality_level_subst : (Sorts.QVar.t -> Pp.t) -> 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 : Univ.universe_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
Pretty-printing of universes.
val pr_universe_context : (Sorts.QVar.t -> Pp.t) -> (Univ.Level.t -> Pp.t) -> ?variance:Variance.t array -> UContext.t -> Pp.t
val pr_abstract_universe_context : (Sorts.QVar.t -> Pp.t) -> (Univ.Level.t -> Pp.t) -> ?variance:Variance.t array -> AbstractContext.t -> Pp.t
Hash-consing
val hcons_universe_context : UContext.t -> UContext.t
val hcons_abstract_universe_context : AbstractContext.t -> AbstractContext.t