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 =
| IllegalConstraintFromSProp of Sorts.Quality.t
| IllegalConstantConstraint of Sorts.Quality.constant * Sorts.Quality.constant
| 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.

val merge : t -> t -> t
val merge_constraints : 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 : 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.

val initial_graph : t

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

val update_rigids : t -> t -> t
val check_rigid_paths : t -> unit
val add_rigid_path : Sorts.Quality.t -> Sorts.Quality.t -> t -> t
val is_declared : Sorts.Quality.t -> t -> bool
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 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