Module Univ

module Level : sig ... end

Universes.

module LSet : sig ... end
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

val type0_univ : Universe.t
val type1_univ : Universe.t
val is_type0_univ : Universe.t -> bool
val is_type0m_univ : Universe.t -> bool
val is_univ_variable : Universe.t -> bool
val is_small_univ : Universe.t -> bool
val sup : Universe.t -> Universe.t -> Universe.t
val super : Universe.t -> Universe.t
val universe_level : Universe.t -> Level.t option
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
module Constraint : sig ... end
val empty_constraint : Constraints.t
val union_constraint : Constraints.t -> Constraints.t -> Constraints.t
val eq_constraint : Constraints.t -> Constraints.t -> bool
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 : Universe.t constraint_function
val enforce_leq : Universe.t constraint_function
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...

type univ_inconsistency = constraint_type * Universe.t * Universe.t * explanation Stdlib.Lazy.t option
exception UniverseInconsistency of univ_inconsistency
Support for universe polymorphism
module LMap : sig ... end
type 'a universe_map = 'a Level.Map.t
Substitution
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

type universe_level_subst = Level.t universe_map
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
module AUContext : 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
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 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 : 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 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
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