package rocq-runtime

  1. Overview
  2. Docs
The Rocq Prover -- Core Binaries and Tools

Install 

dune-project
 Dependency

rocq-prover.org Readme Edit opam file Versions (5)

Authors

  1. T
    The Rocq development team, INRIA, CNRS, and contributors

Maintainers

  1. T
    The Rocq development team <rocq+rocq-development@discoursemail.com>

Sources

rocq-9.2.0.tar.gz
sha256=a45280ab4fbaac7540b136a6b073b4a6db15739ec1e149bded43fa6f4fc25f20

doc/rocq-runtime.kernel/UGraph/index.html

Module UGraphSource

Sourcetype t

Graphs of universes.

Sourceval set_type_in_type : bool -> t -> t
Sourceval 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.

Sourcetype 'a check_function = t -> 'a -> 'a -> bool
Sourceval check_eq_level : Univ.Level.t check_function
Sourceval initial_universes : t

The initial graph of universes: Prop < Set

Sourceval initial_universes_with : t -> t

Initial universes, but keeping options such as type in type from the argument.

Sourceval check_eq_instances : (Sorts.Quality.t -> Sorts.Quality.t -> bool) -> t -> UVars.Instance.t -> UVars.Instance.t -> bool

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.

Sourcetype path_explanation
Sourcetype explanation =
  1. | Path of path_explanation
  2. | Other of Pp.t
Sourcetype univ_variable_printers = (Sorts.QVar.t -> Pp.t) * (Univ.Level.t -> Pp.t)
Sourcetype univ_inconsistency = univ_variable_printers option * (Univ.UnivConstraint.kind * Sorts.t * Sorts.t * explanation option)
Sourceexception UniverseInconsistency of univ_inconsistency
Sourceval enforce_constraint : Univ.UnivConstraint.t -> t -> t
Sourceval merge_constraints : Univ.UnivConstraints.t -> t -> t
Sourceval check_constraint : t -> Univ.UnivConstraint.t -> bool
Sourceval check_constraints : Univ.UnivConstraints.t -> t -> bool
Sourceval check_eq_sort : (Sorts.Quality.t -> Sorts.Quality.t -> bool) -> t -> Sorts.t -> Sorts.t -> bool

Checks whether (i) the first quality is equal to the second and (ii) that the universe of the first one is equal to the universe of the second one. When type_in_type, only checks relevance.

Sourceval check_leq_sort : (Sorts.Quality.t -> Sorts.Quality.t -> bool) -> t -> Sorts.t -> Sorts.t -> bool

Checks whether (i) the second quality eliminates into the first and (ii) that the universe of the first one is below the universe of the second one. When type_in_type, only checks relevance.

Adds a universe to the graph, ensuring it is >= or > Set.

Sourceexception AlreadyDeclared
Sourceval add_universe : Univ.Level.t -> strict:bool -> t -> t
Sourceval check_declared_universes : t -> Univ.Level.Set.t -> (unit, Univ.Level.Set.t) result

Check that the universe levels are declared.

Sourceval empty_universes : t

The empty graph of universes

Sourceval constraints_of_universes : t -> Univ.UnivConstraints.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.

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

Sourceval constraints_for : kept:Univ.Level.Set.t -> t -> Univ.UnivConstraints.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.

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

Known universes

Dumping
Sourcetype node =
  1. | Alias of Univ.Level.t
  2. | Node of bool Univ.Level.Map.t
    (*

    Nodes v s.t. u < v (true) or u <= v (false)

    *)
Pretty-printing of universes.
Sourceval pr_universes : (Univ.Level.t -> Pp.t) -> node Univ.Level.Map.t -> Pp.t
Sourceval explain_universe_inconsistency : (Sorts.QVar.t -> Pp.t) -> (Univ.Level.t -> Pp.t) -> univ_inconsistency -> Pp.t
Sourceval check_universes_invariants : t -> unit

Debugging

Sourcemodule Internal : sig ... end