Module Univ

module UGlobal : sig ... end

Qualified global universe level

module Level : sig ... end

Universes.

module Universe : sig ... end
val univ_level_mem : Level.t -> Universe.t -> bool
val univ_level_rem : Level.t -> Universe.t -> Universe.t -> Universe.t
Constraints.
type constraint_type = AcyclicGraph.constraint_type =
| Lt
| Le
| Eq
type univ_constraint = Level.t * constraint_type * Level.t
module Constraints : sig ... end
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...

Support for universe polymorphism
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
module UContext : sig ... end
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
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
Substitution
type universe_level_subst = Level.t 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 -> 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
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 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 pr_universe_level_subst : universe_level_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