Module UVarsSource

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

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

Sourcetype 'a quconstraint_function = 'a -> 'a -> Sorts.QUConstraints.t -> Sorts.QUConstraints.t
Sourceval enforce_eq_instances : Instance.t quconstraint_function
Sourceval enforce_eq_variance_instances : Variance.t array -> Instance.t quconstraint_function
Sourceval enforce_leq_variance_instances : Variance.t array -> Instance.t quconstraint_function
Sourcetype 'a puniverses = 'a * Instance.t
Sourceval out_punivs : 'a puniverses -> 'a
Sourceval in_punivs : 'a -> 'a puniverses
Sourceval eq_puniverses : ('a -> 'a -> bool) -> 'a puniverses -> 'a puniverses -> bool
Sourcetype 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

Sourcemodule UContext : sig ... end

A value in a universe context.

Sourcetype 'a in_universe_context = 'a * UContext.t

A value in a universe context.

Sourcemodule AbstractContext : sig ... end
Sourcetype 'a univ_abstracted = {
  1. univ_abstracted_value : 'a;
  2. univ_abstracted_binder : AbstractContext.t;
}

A value with bound universe levels.

Sourceval map_univ_abstracted : ('a -> 'b) -> 'a univ_abstracted -> 'b univ_abstracted
Substitution
Sourceval pr_quality_level_subst : (Sorts.QVar.t -> Pp.t) -> Sorts.Quality.t Sorts.QVar.Map.t -> Pp.t
Sourceval empty_sort_subst : sort_level_subst
Sourceval is_empty_sort_subst : sort_level_subst -> bool
Sourceval 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

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

Level to universe substitutions.

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

Substitution of instances

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

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

Sourceval abstract_universes : UContext.t -> Instance.t * AbstractContext.t

TODO: move universe abstraction out of the kernel

Sourceval make_abstract_instance : AbstractContext.t -> Instance.t
Pretty-printing of universes.
Sourceval pr_universe_context : (Sorts.QVar.t -> Pp.t) -> (Univ.Level.t -> Pp.t) -> ?variance:Variance.t array -> UContext.t -> Pp.t
Sourceval pr_abstract_universe_context : (Sorts.QVar.t -> Pp.t) -> (Univ.Level.t -> Pp.t) -> ?variance:Variance.t array -> AbstractContext.t -> Pp.t
Hash-consing
Sourceval hcons_universe_context : UContext.t -> UContext.t
Sourceval hcons_abstract_universe_context : AbstractContext.t -> AbstractContext.t