UGraph
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_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
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 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 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.
module Bound : sig ... end
val add_universe : Univ.Level.t -> lbound:Bound.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
val check_subtype : UVars.AbstractContext.t check_function
check_subtype univ ctx1 ctx2
checks whether ctx2
is an instance of ctx1
.
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
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