Module `Univ`

module Universe : sig ... end

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

type constraint_type = AcyclicGraph.constraint_type = | Lt | Le | Eq
type univ_constraint = Level.t * constraint_type * Level.t

module Constraint : sig ... end

type 'a constrained = 'a * Constraint.t: A value with universe Constraint.t.

type 'a constraint_function = 'a -> 'a -> Constraint.t -> Constraint.t: Enforcing Constraint.t.

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 Constraint.t...

type univ_inconsistency = constraint_type * Universe.t * Universe.t * explanation Stdlib.Lazy.t option

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

module Variance : sig ... end

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

val out_punivs : 'a puniverses -> 'a
val in_punivs : 'a -> 'a puniverses
val eq_puniverses : ('a -> 'a -> bool) -> 'a puniverses -> 'a puniverses -> bool

module UContext : sig ... end

module AUContext : sig ... end

type 'a univ_abstracted = { univ_abstracted_value : 'a; univ_abstracted_binder : AUContext.t; }: A value with bound universe levels.

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

module ContextSet : sig ... end

type 'a in_universe_context = 'a * UContext.t: A value in a universe context (resp. context set).

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 -> Constraint.t -> Constraint.t
val subst_univs_level_abstract_universe_context : universe_level_subst -> AUContext.t -> AUContext.t
val subst_univs_level_instance : universe_level_subst -> Instance.t -> Instance.t

val empty_subst : universe_subst
val is_empty_subst : universe_subst -> bool
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 : Names.Name.t array -> UContext.t -> Instance.t * AUContext.t: TODO: move universe abstraction out of the kernel

val make_abstract_instance : AUContext.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

val pr_constraint_type : constraint_type -> Pp.t
val pr_constraints : (Level.t -> Pp.t) -> Constraint.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 -> AUContext.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