Module UState

This file defines universe unification states which are part of evarmaps. Most of the API below is reexported in Evd. Consider using higher-level primitives when needed.

exception UniversesDiffer
type t

Type of universe unification states. They allow the incremental building of universe constraints during an interactive proof.

Constructors
val empty : t
val make : lbound:Univ.Level.t -> UGraph.t -> t
val make_with_initial_binders : lbound:Univ.Level.t -> UGraph.t -> Names.lident list -> t
val is_empty : t -> bool
val union : t -> t -> t
val of_context_set : Univ.ContextSet.t -> t
val of_binders : UnivNames.universe_binders -> t
val universe_binders : t -> UnivNames.universe_binders
Projections
val context_set : t -> Univ.ContextSet.t

The local context of the state, i.e. a set of bound variables together with their associated constraints.

val subst : t -> UnivSubst.universe_opt_subst

The local universes that are unification variables

val ugraph : t -> UGraph.t

The current graph extended with the local constraints

val initial_graph : t -> UGraph.t

The initial graph with just the declarations of new universes.

val algebraics : t -> Univ.LSet.t

The subset of unification variables that can be instantiated with algebraic universes as they appear in inferred types only.

val constraints : t -> Univ.Constraint.t

Shorthand for context_set composed with ContextSet.constraints.

val context : t -> Univ.UContext.t

Shorthand for context_set with Context_set.to_context.

val univ_entry : poly:bool -> t -> Entries.universes_entry

Pick from context or context_set based on poly.

val const_univ_entry : poly:bool -> t -> Entries.universes_entry
Constraints handling
val drop_weak_constraints : bool Stdlib.ref
val add_constraints : t -> Univ.Constraint.t -> t
raises UniversesDiffer

when universes differ

val add_universe_constraints : t -> UnivProblem.Set.t -> t
raises UniversesDiffer

when universes differ

Names
val universe_of_name : t -> Names.Id.t -> Univ.Level.t

Retrieve the universe associated to the name.

Unification
val restrict_universe_context : lbound:Univ.Level.t -> Univ.ContextSet.t -> Univ.LSet.t -> Univ.ContextSet.t

restrict_universe_context lbound (univs,csts) keep restricts univs to the universes in keep. The constraints csts are adjusted so that transitive constraints between remaining universes (those in keep and those not in univs) are preserved.

val restrict : t -> Univ.LSet.t -> t

restrict uctx ctx restricts the local universes of uctx to ctx extended by local named universes and side effect universes (from demote_seff_univs). Transitive constraints between retained universes are preserved.

val demote_seff_univs : Safe_typing.private_constants Entries.definition_entry -> t -> t
type rigid =
| UnivRigid
| UnivFlexible of bool

Is substitution by an algebraic ok?

val univ_rigid : rigid
val univ_flexible : rigid
val univ_flexible_alg : rigid
val merge : ?⁠loc:Loc.t -> sideff:bool -> extend:bool -> rigid -> t -> Univ.ContextSet.t -> t
val merge_subst : t -> UnivSubst.universe_opt_subst -> t
val emit_side_effects : Safe_typing.private_constants -> t -> t
val new_univ_variable : ?⁠loc:Loc.t -> rigid -> Names.Id.t option -> t -> t * Univ.Level.t
val add_global_univ : t -> Univ.Level.t -> t
val make_flexible_variable : t -> algebraic:bool -> Univ.Level.t -> t

make_flexible_variable g algebraic l

Turn the variable l flexible, and algebraic if algebraic is true and l can be. That is if there are no strict upper constraints on l and and it does not appear in the instance of any non-algebraic universe. Otherwise the variable is just made flexible.

If l is already algebraic it will remain so even with algebraic:false.

val make_nonalgebraic_variable : t -> Univ.Level.t -> t

Make the level non algebraic. Undefined behaviour on already-defined algebraics.

val make_flexible_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 is_sort_variable : t -> Sorts.t -> Univ.Level.t option
val normalize_variables : t -> Univ.universe_subst * t
val constrain_variables : Univ.LSet.t -> t -> t
val abstract_undefined_variables : t -> t
val fix_undefined_variables : t -> t
val refresh_undefined_univ_variables : t -> t * Univ.universe_level_subst
val minimize : t -> t

Universe minimization

type ('a, 'b) gen_universe_decl = {
univdecl_instance : 'a;
univdecl_extensible_instance : bool;
univdecl_constraints : 'b;
univdecl_extensible_constraints : bool;
}
type universe_decl = (Names.lident list, Univ.Constraint.t) gen_universe_decl
val default_univ_decl : universe_decl
val check_univ_decl : poly:bool -> t -> universe_decl -> Entries.universes_entry

check_univ_decl ctx decl

If non extensible in decl, check that the local universes (resp. universe constraints) in ctx are implied by decl.

Return a Entries.constant_universes_entry containing the local universes of ctx and their constraints.

When polymorphic, the universes corresponding to decl.univdecl_instance come first in the order defined by that list.

val check_mono_univ_decl : t -> universe_decl -> Univ.ContextSet.t
TODO: Document me
val update_sigma_env : t -> Environ.env -> t
Pretty-printing
val pr_uctx_level : t -> Univ.Level.t -> Pp.t
val qualid_of_level : t -> Univ.Level.t -> Libnames.qualid option
val pr_weak : (Univ.Level.t -> Pp.t) -> t -> Pp.t