Module signature for global domains used by the union-find module.
A global domain records a set of potentially correlated values for multiple variables at once. This is typically, but not necessarily, an associative mapping of variables to their own independent domain.
Note: This module signature only contains the bare minimum for interaction with the union-find module to be able to update the global domains appropriately when new terms are introduced and equivalence classes are merged. In particular, it purposefully provides no facility to access or modify the global domain to allow more flexibility in the to the implementer.
val pp : t Fmt.tPretty-printer for global domains.
val empty : tThe empty domain.
val filter_ty : Ty.t -> boolLimit the type of terms that this module cares about. Only substitutions of representatives for which filter_ty (type_info r) holds will be propagated to this module.
init r t is called when the representative r is added to the union-find, if it has a type that matches filter_ty.
Note: unlike Relation.add, this function is called even for "dynamic" representatives added by X.make or AC normalization.
exception Inconsistent of Explanation.tRaised by subst below when an inconsistency is found while merging the domains.
val subst : ex:Explanation.t -> r -> r -> t -> tsubst ~ex rr nrr t is called when the representatives rr and nrr are merged with explanation ex. nrr is the new representative; rr should no longer be tracked and the intersection of domains should be associated with nrr.
The explanation ex justifies the equality rr = nrr.
Inconsistent if the domains for rr and nrr are incompatible.