package rocq-runtime

  1. Overview
  2. Docs
package rocq-runtime
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module UStateSource

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.

Sourcetype universes_entry =
  1. | Monomorphic_entry of Univ.ContextSet.t
  2. | Polymorphic_entry of UVars.UContext.t
Sourceexception UniversesDiffer
Sourcetype t

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

Constructors

Different ways to create a new universe state

Sourceval empty : t
Sourceval make : qualities:QGraph.t -> UGraph.t -> t
  • deprecated (8.13) Use from_env
Sourceval make_with_initial_binders : qualities:QGraph.t -> UGraph.t -> Names.lident list -> t
  • deprecated (8.13) Use from_env
Sourceval from_env : ?binders:Names.lident list -> Environ.env -> t

Main entry point at the beginning of a declaration declaring the binding names as rigid universes.

Main entry point when only names matter, e.g. for printing.

Misc

Sourceval is_empty : t -> bool
Sourceval union : t -> t -> t
Projections and other destructors
Sourceval universe_context_set : t -> Univ.ContextSet.t
Sourceval sort_context_set : t -> UnivGen.sort_context_set

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

Sourcetype universe_opt_subst = UnivFlex.t
Sourceval subst : t -> UnivFlex.t

The local universes that are unification variables

Sourceval nf_universes : t -> Constr.t -> Constr.t

Apply the local substitution subst

Sourceval ugraph : t -> UGraph.t

The current graph extended with the local constraints

Sourceval elim_graph : t -> QGraph.t

The elimination graph for above prop variables

Sourceval is_above_prop : t -> Sorts.QVar.t -> bool
Sourceval is_algebraic : Univ.Level.t -> t -> bool

Can this universe be instantiated with an algebraic universe (ie it appears in inferred types only).

Sourceval constraints : t -> PConstraints.t

Shorthand for context_set composed with ContextSet.constraints.

Sourceval context : t -> UVars.UContext.t

Shorthand for context_set with Context_set.to_context.

Sourcetype named_universes_entry = universes_entry * UnivNames.universe_binders
Sourceval univ_entry : poly:PolyFlags.t -> t -> named_universes_entry

Pick from context or context_set based on poly.

Sourceval universe_binders : t -> UnivNames.universe_binders

Return local names of universes.

Sourceval compute_instance_binders : t -> UVars.Instance.t -> UVars.bound_names

Returns the normal form of the sort variable.

Sourceval nf_quality : t -> Sorts.Quality.t -> Sorts.Quality.t
Sourceval nf_instance : t -> UVars.Instance.t -> UVars.Instance.t
Sourceval nf_level : t -> Univ.Level.t -> Univ.Level.t

Must not be allowed to be algebraic

Sourceval nf_universe : t -> Univ.Universe.t -> Univ.Universe.t
Sourceval nf_sort : t -> Sorts.t -> Sorts.t

Returns the normal form of the sort.

Sourceval nf_relevance : t -> Sorts.relevance -> Sorts.relevance

Returns the normal form of the relevance.

UnivConstraints handling
Sourcetype constraint_source =
  1. | Internal
  2. | Rigid
  3. | Static
    (*

    On an Internal enforcement, checks whether a path is created between two ground/global sorts. The Rigid constraint_source should be used for constraints entered by the user. It allows to create paths between ground/global sorts, but disables path creation between two ground sorts. No additional check is performed on a Static constraint.

    *)
Sourceval add_univ_constraints : t -> Univ.UnivConstraints.t -> t
Sourceval add_poly_constraints : ?src:constraint_source -> t -> PConstraints.t -> t
Sourceval add_constraints : ?src:constraint_source -> t -> UnivProblem.Set.t -> t
Sourceval check_elim_constraints : t -> Sorts.ElimConstraints.t -> bool
Sourceval check_constraints : t -> UnivProblem.Set.t -> bool
Sourceval check_eq_quality : t -> Sorts.Quality.t -> Sorts.Quality.t -> bool
Names
Sourceval quality_of_name : t -> Names.Id.t -> Sorts.QVar.t
Sourceval universe_of_name : t -> Names.Id.t -> Univ.Level.t

Retrieve the universe associated to the name.

Sourceval name_level : Univ.Level.t -> Names.Id.t -> t -> t

Gives a name to the level (making it a binder). Asserts the name is not already used by a level

Unification
Sourceval restrict_universe_context : Univ.ContextSet.t -> Univ.Level.Set.t -> Univ.ContextSet.t

restrict_universe_context (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.

Sourceval restrict : t -> Univ.Level.Set.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.

Sourceval restrict_even_binders : t -> Univ.Level.Set.t -> t

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

Sourcetype rigid =
  1. | UnivRigid
  2. | UnivFlexible of bool
    (*

    Is substitution by an algebraic ok?

    *)
Sourceval univ_rigid : rigid
Sourceval univ_flexible : rigid
Sourceval univ_flexible_alg : rigid
Sourceval merge_sort_context : ?loc:Loc.t -> ?sort_rigid:bool -> ?src:constraint_source -> sideff:bool -> rigid -> t -> UnivGen.sort_context_set -> t
Sourceval merge_universe_context : ?loc:Loc.t -> sideff:bool -> rigid -> t -> Univ.ContextSet.t -> t
Sourceval demote_global_univs : Univ.ContextSet.t -> t -> t

After declaring global universes, call this if you want to keep using the UState.

Removes from the uctx_local part of the UState the universes that are present in the input constraint set (supposedly the global ones), and adds any new universes and constraints to the UGraph part of the UState.

Sourceval demote_global_univ_entry : universes_entry -> t -> t

After declaring a global, call this with its universe entry if you want to keep using the ustate instead of restarting it with from_env (Global.env()) or using the slow update_sigma_univs _ (Environ.universes (Global/env())).

Equivalently:

  • In the monomorphic case, call demote_global_univs on the contextset.
  • In the polymorphic case, do nothing.
Sourceval emit_side_effects : Safe_typing.private_constants -> t -> t

Calls demote_global_univs for the private constant universes.

Sourceval new_sort_variable : ?loc:Loc.t -> ?sort_rigid:bool -> ?name:Names.Id.t -> t -> t * Sorts.QVar.t

Declare a new local sort.

Sourceval new_univ_variable : ?loc:Loc.t -> rigid -> Names.Id.t option -> t -> t * Univ.Level.t

Declare a new local universe; use rigid if a global or bound universe; use flexible for a universe existential variable; use univ_flexible_alg for a universe existential variable allowed to be instantiated with an algebraic universe

Sourceval add_forgotten_univ : t -> Univ.Level.t -> t

Don't use this, it only exists for funind

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

cf UnivFlex

Sourceval make_flexible_nonalgebraic : t -> t

cf UnivFlex

Sourceval normalize_variables : t -> t
Sourceval constrain_variables : Univ.Level.Set.t -> t -> t
Sourceval fix_undefined_variables : t -> t

cf UnivFlex

Sourceval minimize : t -> t

Universe minimization

Sourceval collapse_above_prop_sort_variables : to_prop:bool -> t -> t
Sourceval collapse_sort_variables : ?except:Sorts.QVar.Set.t -> t -> t
Sourcetype ('a, 'b, 'c, 'd) gen_universe_decl = {
  1. univdecl_qualities : 'a;
  2. univdecl_extensible_qualities : bool;
  3. univdecl_elim_constraints : 'b;
  4. univdecl_instance : 'c;
  5. univdecl_extensible_instance : bool;
  6. univdecl_univ_constraints : 'd;
  7. univdecl_extensible_constraints : bool;
}
Sourceval default_univ_decl : universe_decl
Sourceval check_univ_decl : poly:PolyFlags.t -> t -> universe_decl -> named_universes_entry

check_poly_decl ctx decl

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

Return a 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.

Sourceval check_univ_decl_rev : t -> universe_decl -> t * UVars.UContext.t
Sourceval check_uctx_impl : fail:(Pp.t -> unit) -> t -> t -> unit
Sourceval check_mono_univ_decl : t -> universe_decl -> Univ.ContextSet.t
Sourceval check_template_univ_decl : t -> template_qvars:Sorts.QVar.Set.t -> universe_decl -> Univ.ContextSet.t
Sourceval check_mono_sort_constraints : t -> Univ.ContextSet.t
TODO: Document me
Sourceval update_sigma_univs : t -> UGraph.t -> t
Pretty-printing
Sourceval pr_uctx_level : t -> Univ.Level.t -> Pp.t
Sourceval pr_uctx_qvar : t -> Sorts.QVar.t -> Pp.t
Sourceval qualid_of_level : t -> Univ.Level.t -> Libnames.qualid option
Sourceval id_of_level : t -> Univ.Level.t -> Names.Id.t option

Only looks in the local names, not in the nametab.

Sourceval id_of_qvar : t -> Sorts.QVar.t -> Names.Id.t option
Sourceval is_rigid_qvar : t -> Sorts.QVar.t -> bool
Sourceval pr_weak : (Univ.Level.t -> Pp.t) -> t -> Pp.t
Sourceval pr : t -> Pp.t
Sourceval pr_sort_opt_subst : t -> Pp.t
Sourcemodule Internal : sig ... end
Sourceval add_template_default_univs : Environ.env -> Names.MutInd.t -> unit