Module UnivFlex
type t
Flexible universe data. A level is flexible if
UnivFlex.mem
returnstrue
on it. Flexible levels may have a definition, this induces a universe substitution.Only some flexible levels may be defined as algebraic universes.
val empty : t
val is_empty : t -> bool
val domain : t -> Univ.Level.Set.t
Contains both defined and undefined flexible levels.
val fold : (Univ.Level.t -> is_defined:bool -> 'a -> 'a) -> t -> 'a -> 'a
For universe minimization.
val mem : Univ.Level.t -> t -> bool
Returns
true
for both defined and undefined flexible levels.
val is_algebraic : Univ.Level.t -> t -> bool
Is the level allowed to be defined by an algebraic universe?
val make_nonalgebraic_variable : t -> Univ.Level.t -> t
Make the level non algebraic. Undefined behaviour on already-defined algebraics.
val make_all_undefined_nonalgebraic : t -> t
Turn all undefined flexible algebraic variables into simply flexible ones. Can be used in case the variables might appear in universe instances (typically for polymorphic program obligations).
val fix_undefined_variables : t -> t
Make all undefined flexible levels into rigid levels, ie remove them.
val add : Univ.Level.t -> algebraic:bool -> t -> t
MAkes a level flexible with no definition. It must not already be flexible.
val add_levels : Univ.Level.Set.t -> algebraic:bool -> t -> t
Make the levels flexible with no definitions. They must not already be flexible.
val define : Univ.Level.t -> Univ.Universe.t -> t -> t
Define the level to the given universe. The level must already be flexible and must be undefined.
val constrain_variables : Univ.Level.Set.t -> t -> Univ.ContextSet.t -> Univ.ContextSet.t * t
constrain_variables diff subst ctx
removes bindingsl := l'
from the substitution wherel
is indiff
andl'
is a level, and addsl, l = l'
toctx
.
val biased_union : t -> t -> t
biased_union x y
favors the bindings of the first map that are defined, otherwise takes the second's bindings.
val normalize_univ_variables : t -> t * Univ.Level.Set.t * UnivSubst.universe_subst_fn
As
normalize
and also returns the set of defined variables and a function which is equivalent to callingnormalize_univ_variable
on the substitution but may be faster.
val normalize_univ_variable : t -> UnivSubst.universe_subst_fn
Apply the substitution to a variable.
val normalize_universe : t -> Univ.Universe.t -> Univ.Universe.t
Apply the substitution to an algebraic universe.
val pr : (Univ.Level.t -> Pp.t) -> t -> Pp.t
"Show Universes"-style printing.