Module `UGraph`

type t: Graphs of universes.

val make_sprop_cumulative : t -> t: Don't use this in the kernel, it makes the system incomplete.

type 'a check_function = t -> 'a -> 'a -> bool

val check_leq : Univ.Universe.t check_function
val check_eq : Univ.Universe.t check_function
val check_eq_level : Univ.Level.t check_function
val initial_universes : t: The initial graph of universes: Prop < Set

val check_eq_instances : Univ.Instance.t check_function: Check equality of instances w.r.t. a universe graph

...

val enforce_constraint : Univ.univ_constraint -> t -> t
val merge_constraints : Univ.Constraint.t -> t -> t
val check_constraint : t -> Univ.univ_constraint -> bool
val check_constraints : Univ.Constraint.t -> t -> bool
val enforce_leq_alg : Univ.Universe.t -> Univ.Universe.t -> t -> Univ.Constraint.t * t: Picks an arbitrary set of constraints sufficient to ensure u <= v.

exception AlreadyDeclared

val add_universe : Univ.Level.t -> lbound:Univ.Level.t -> strict:bool -> t -> t
val add_universe_unconstrained : Univ.Level.t -> t -> t: Add a universe without (Prop,Set) <= u

exception UndeclaredLevel of Univ.Level.t

Check that the universe levels are declared. Otherwise

raises UndeclaredLevel: l for the first undeclared level found.

val check_declared_universes : t -> Univ.LSet.t -> unit

Pretty-printing of universes.

val pr_universes : (Univ.Level.t -> Pp.t) -> t -> Pp.t
val empty_universes : t: The empty graph of universes

val sort_universes : t -> t
val constraints_of_universes : t -> Univ.Constraint.t * Univ.LSet.t list: constraints_of_universes g returns csts and partition where csts are the non-Eq constraints and partition is the partition of the universes into equivalence classes.

val choose : (Univ.Level.t -> bool) -> t -> Univ.Level.t -> Univ.Level.t option: choose p g u picks a universe verifying p and equal to u in g.

val constraints_for : kept:Univ.LSet.t -> t -> Univ.Constraint.t

constraints_for ~kept g returns the constraints about the universes kept in g up to transitivity.

eg if g is a <= b <= c then constraints_for ~kept:{a, c} g is a <= c.

val domain : t -> Univ.LSet.t: Known universes

val check_subtype : lbound:Univ.Level.t -> Univ.AUContext.t check_function: check_subtype univ ctx1 ctx2 checks whether ctx2 is an instance of ctx1.

Dumping to a file

val dump_universes : (Univ.constraint_type -> Univ.Level.t -> Univ.Level.t -> unit) -> t -> unit
val check_universes_invariants : t -> unit: Debugging