Module QGraph

Graphs of quality elimination constraints.
module ElimTable : sig ... end
type t
type path_explanation
type explanation =
| Path of path_explanation
| Other of Pp.t
type quality_inconsistency = (Sorts.QVar.t -> Pp.t) option * (Sorts.ElimConstraint.kind * Sorts.Quality.t * Sorts.Quality.t * explanation option)
type elimination_error =
| IllegalConstraint
| CreatesForbiddenPath of Sorts.Quality.t * Sorts.Quality.t
| MultipleDominance of Sorts.Quality.t * Sorts.Quality.t * Sorts.Quality.t
| QualityInconsistency of quality_inconsistency
exception EliminationError of elimination_error
exception AlreadyDeclared
val 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.

type constraint_source =
| Internal
| Rigid
| Static
val merge : t -> t -> t
val merge_constraints : constraint_source -> Sorts.ElimConstraints.t -> t -> t
val 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.

val check_constraint : t -> Sorts.ElimConstraint.t -> bool
val check_constraints : Sorts.ElimConstraints.t -> t -> bool
val enforce_eliminates_to : constraint_source -> 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. On an Internal enforcement, it also 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.

val enforce_eq : Sorts.Quality.t -> Sorts.Quality.t -> t -> t

Set the first quality equal to the second one in the graph. If it's impossible, raise QualityInconsistency.

val initial_graph : t

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

val update_rigids : t -> t -> t
val eliminates_to : t -> Sorts.Quality.t -> Sorts.Quality.t -> bool
val eliminates_to_prop : t -> Sorts.Quality.t -> bool
val sort_eliminates_to : t -> Sorts.t -> Sorts.t -> bool
val check_eq : t -> Sorts.Quality.t -> Sorts.Quality.t -> bool
val check_eq_sort : t -> Sorts.t -> Sorts.t -> bool
val domain : t -> Sorts.Quality.Set.t
val qvar_domain : t -> Sorts.QVar.Set.t
val is_empty : t -> bool
val pr_qualities : (Sorts.Quality.t -> Pp.t) -> t -> Pp.t
val explain_quality_inconsistency : (Sorts.QVar.t -> Pp.t) -> explanation option -> Pp.t
val explain_elimination_error : (Sorts.QVar.t -> Pp.t) -> elimination_error -> Pp.t