Module UGraph

type t

Graphs of universes.

val set_type_in_type : bool -> t -> t
val type_in_type : t -> bool

When type_in_type, functions adding constraints do not fail and may instead ignore inconsistent constraints.

Checking functions such as check_leq always return true.

type 'a check_function = t -> 'a -> 'a -> bool
val check_eq_level : Univ.Level.t check_function
val initial_universes : t

The initial graph of universes: Prop < Set

val initial_universes_with : t -> t

Initial universes, but keeping options such as type in type from the argument.

val check_eq_instances : UVars.Instance.t check_function

Check equality of instances w.r.t. a universe graph

...

Merge of constraints in a universes graph. The function merge_constraints merges a set of constraints in a given universes graph. It raises the exception UniverseInconsistency if the constraints are not satisfiable.

type path_explanation
type explanation =
| Path of path_explanation
| Other of Pp.t
type univ_variable_printers = (Sorts.QVar.t -> Pp.t) * (Univ.Level.t -> Pp.t)
type univ_inconsistency = univ_variable_printers option * (Univ.constraint_type * Sorts.t * Sorts.t * explanation option)
exception UniverseInconsistency of univ_inconsistency
val enforce_constraint : Univ.univ_constraint -> t -> t
val merge_constraints : Univ.Constraints.t -> t -> t
val check_constraint : t -> Univ.univ_constraint -> bool
val check_constraints : Univ.Constraints.t -> t -> bool
val check_eq_sort : QGraph.t -> t -> Sorts.t -> Sorts.t -> bool

Checks whether (i) the first quality is equal to the second and (ii) that the universe of the first one is equal to the universe of the second one. When type_in_type, only checks relevance.

val check_leq_sort : QGraph.t -> t -> Sorts.t -> Sorts.t -> bool

Checks whether (i) the second quality eliminates into the first and (ii) that the universe of the first one is below the universe of the second one. When type_in_type, only checks relevance.

val enforce_leq_alg : Univ.Universe.t -> Univ.Universe.t -> t -> Univ.Constraints.t * t

Adds a universe to the graph, ensuring it is >= or > Set.

exception AlreadyDeclared
val add_universe : Univ.Level.t -> strict:bool -> t -> t
val check_declared_universes : t -> Univ.Level.Set.t -> (unit, Univ.Level.Set.t) Stdlib.result

Check that the universe levels are declared.

val empty_universes : t

The empty graph of universes

val constraints_of_universes : t -> Univ.Constraints.t * Univ.Level.Set.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.Level.Set.t -> t -> Univ.Constraints.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.Level.Set.t

Known universes

check_subtype univ ctx1 ctx2 checks whether ctx2 is an instance of ctx1.

Dumping
type node =
| Alias of Univ.Level.t
| Node of bool Univ.Level.Map.t(*

Nodes v s.t. u < v (true) or u <= v (false)

*)
val repr : t -> node Univ.Level.Map.t
Pretty-printing of universes.
val pr_universes : (Univ.Level.t -> Pp.t) -> node Univ.Level.Map.t -> Pp.t
val explain_universe_inconsistency : (Sorts.QVar.t -> Pp.t) -> (Univ.Level.t -> Pp.t) -> univ_inconsistency -> Pp.t
val check_universes_invariants : t -> unit

Debugging

module Internal : sig ... end