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/QGraph/index.html

Module QGraphSource

Graphs of quality elimination constraints.
Sourcemodule ElimTable : sig ... end
Sourcetype t
Sourcetype path_explanation
Sourcetype explanation =
  1. | Path of path_explanation
  2. | Other of Pp.t
Sourcetype quality_inconsistency = (Sorts.QVar.t -> Pp.t) option * (Sorts.ElimConstraint.kind * Sorts.Quality.t * Sorts.Quality.t * explanation option)
Sourcetype elimination_error =
  1. | IllegalConstraintFromSProp of Sorts.Quality.t
  2. | IllegalConstantConstraint of Sorts.Quality.constant * Sorts.Quality.constant
  3. | CreatesForbiddenPath of Sorts.Quality.t * Sorts.Quality.t
  4. | MultipleDominance of Sorts.Quality.t * Sorts.Quality.t * Sorts.Quality.t
  5. | QualityInconsistency of quality_inconsistency
Sourceexception EliminationError of elimination_error
Sourceexception AlreadyDeclared
Sourceval add_quality : Sorts.Quality.t -> t -> t

Always call this function on a quality before trying to enforce or check a constraint or calling eliminates_to. Forces Type to eliminate to this quality.

Sourceval merge : t -> t -> t
Sourceval merge_constraints : Sorts.ElimConstraints.t -> t -> t
Sourceval update_dominance_if_valid : t -> Sorts.ElimConstraint.t -> t option

Checks if the given constraint satisfies the dominance condition: Let q1 ~> q2 be the given constraint, with q2 a sort variable. Then q1 (or the dominant sort of q1) should be related to the dominant sort of q2, i.e., dom*(q1) ~> dom(q2) or dom(q2) ~> dom*(q1).

Returns None if the dominance *is not valid*, i.e., if the dominant sorts are not related. Otherwise, returns Some g where g is the updated graph.

Sourceval check_constraint : t -> Sorts.ElimConstraint.t -> bool
Sourceval check_constraints : Sorts.ElimConstraints.t -> t -> bool
Sourceval enforce_eliminates_to : Sorts.Quality.t -> Sorts.Quality.t -> t -> t

Set the first quality to eliminate to the second one in the graph.

If this constraint creates a cycle that violates the constraints, QualityInconsistency is raised.

Sourceval initial_graph : t

Graph with the constant quality elimination constraints found in Quality.Constants.eliminates_to.

Sourceval update_rigids : t -> t -> t
Sourceval check_rigid_paths : t -> unit
Sourceval add_rigid_path : Sorts.Quality.t -> Sorts.Quality.t -> t -> t
Sourceval is_declared : Sorts.Quality.t -> t -> bool
Sourceval eliminates_to : t -> Sorts.Quality.t -> Sorts.Quality.t -> bool
Sourceval eliminates_to_prop : t -> Sorts.Quality.t -> bool
Sourceval sort_eliminates_to : t -> Sorts.t -> Sorts.t -> bool
Sourceval qvar_domain : t -> Sorts.QVar.Set.t
Sourceval is_empty : t -> bool
Sourceval pr_qualities : (Sorts.Quality.t -> Pp.t) -> t -> Pp.t
Sourceval explain_quality_inconsistency : (Sorts.QVar.t -> Pp.t) -> explanation option -> Pp.t
Sourceval explain_elimination_error : (Sorts.QVar.t -> Pp.t) -> elimination_error -> Pp.t