package coq

  1. Overview
  2. Docs
package coq
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.

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 : lbound:UGraph.Bound.t -> UGraph.t -> t
  • deprecated Use from_env
Sourceval make_with_initial_binders : lbound:UGraph.Bound.t -> UGraph.t -> Names.lident list -> t
  • deprecated 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.

Sourceval of_context_set : Univ.ContextSet.t -> t

Main entry point when starting from the instance of a global reference, e.g. when building a scheme.

Misc

Sourceval is_empty : t -> bool
Sourceval union : t -> t -> t
Projections and other destructors
Sourceval context_set : t -> Univ.ContextSet.t

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

The local universes that are unification variables

Sourceval ugraph : t -> UGraph.t

The current graph extended with the local constraints

Sourceval initial_graph : t -> UGraph.t

The initial graph with just the declarations of new universes.

Sourceval algebraics : t -> Univ.LSet.t

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

Sourceval constraints : t -> Univ.Constraint.t

Shorthand for context_set composed with ContextSet.constraints.

Sourceval context : t -> Univ.UContext.t

Shorthand for context_set with Context_set.to_context.

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

Pick from context or context_set based on poly.

Sourceval universe_binders : t -> UnivNames.universe_binders

Return local names of universes.

Constraints handling
Sourceval add_constraints : t -> Univ.Constraint.t -> t
Sourceval add_universe_constraints : t -> UnivProblem.Set.t -> t
Names
Sourceval universe_of_name : t -> Names.Id.t -> Univ.Level.t

Retrieve the universe associated to the name.

Unification
Sourceval restrict_universe_context : lbound:UGraph.Bound.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.

Sourceval 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.

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 : ?loc:Loc.t -> sideff:bool -> rigid -> t -> Univ.ContextSet.t -> t
Sourceval merge_subst : t -> UnivSubst.universe_opt_subst -> t
Sourceval emit_side_effects : Safe_typing.private_constants -> t -> t
Sourceval demote_global_univs : Environ.env -> t -> t

Removes from the uctx_local part of the UState the universes and constraints that are present in the universe graph in the input env (supposedly the global ones)

Sourceval demote_seff_univs : Univ.LSet.t -> t -> t

Mark the universes as not local any more, because they have been globally declared by some side effect. You should be using emit_side_effects instead.

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

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

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

Sourceval 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).

Sourceval is_sort_variable : t -> Sorts.t -> Univ.Level.t option
Sourceval normalize_variables : t -> t
Sourceval constrain_variables : Univ.LSet.t -> t -> t
Sourceval abstract_undefined_variables : t -> t
Sourceval fix_undefined_variables : t -> t
Sourceval minimize : t -> t

Universe minimization

Sourcetype ('a, 'b) gen_universe_decl = {
  1. univdecl_instance : 'a;
  2. univdecl_extensible_instance : bool;
  3. univdecl_constraints : 'b;
  4. univdecl_extensible_constraints : bool;
}
Sourceval default_univ_decl : universe_decl
Sourceval 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.

Sourceval check_mono_univ_decl : t -> universe_decl -> 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 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 pr_weak : (Univ.Level.t -> Pp.t) -> t -> Pp.t
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct