Module type Uf.GlobalDomain

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.

type t

The type of global domains.

val pp : t Fmt.t

Pretty-printer for global domains.

type id +=
  1. | Id : t id
    (*

    Unique identifier for this module. Used for dispatch by the union-find.

    Warning: This identifier must be unique; do not re-export the Id from another module (e.g. through include).

    *)
val empty : t

The empty domain.

val filter_ty : Ty.t -> bool

Limit 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.

val init : r -> t -> t

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.t

Raised by subst below when an inconsistency is found while merging the domains.

val subst : ex:Explanation.t -> r -> r -> t -> t

subst ~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.

  • raises Inconsistent

    if the domains for rr and nrr are incompatible.