Module QGraph

Graphs of quality elimination constraints.
module ElimTable : sig ... end
type t
val set_ignore_constraints : bool -> t -> t
val ignore_constraints : t -> bool

When ignore_constraints, functions adding sort constraints do not fail and may instead ignore inconsistent constraints. Breaks the system.

Checking functions such as elim_to always return true.

type path_explanation
type explanation =
| Path of path_explanation
| Other of Pp.t
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 mem : Sorts.Quality.t -> 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.printer -> t -> Pp.t
val explain_quality_inconsistency : Sorts.Quality.printer -> explanation option -> Pp.t
val explain_elimination_error : Sorts.Quality.printer -> elimination_error -> Pp.t