module NF : Domains_intf.NormalFormmodule D :
Domains_intf.Domain
with type var = NF.Composite.t
and type atom = NF.Atom.t
and type constant = NF.constantmodule W : Domains_intf.OrderedTypeinclude Uf.GlobalDomainval 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 -> Uf.r -> Uf.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.
val get : AltErgoLib.Domains_intf.X.r -> t -> D.tget r t returns the domain associated with semantic value r.
val watch : W.t -> AltErgoLib.Domains_intf.X.r -> t -> twatch w r t associated the watch w with the domain of semantic value r. The watch w is triggered whenever the domain associated with r changes, and is preserved across substitutions (i.e. if r becomes nr, w will be transfered to nr).
Note: The watch w is also immediately triggered for a first propagation.
unwatch w removes w from all watch lists. It will no longer be triggered.
Note: If w has already been triggered, it is not removed from the triggered list.
val needs_propagation : t -> boolReturns true if the domains needs propagation, i.e. if any variable's domain has changed.
Returns the set of atomic variables that are currently being tracked.
Returns a map from atomic variables to all the composite variables that contain them and are currently being tracked.
module Ephemeral : sig ... endval edit :
events:(NF.Atom.t, NF.Composite.t, W.t) Domains_intf.events ->
t ->
Ephemeral.tedit ~events t returns an ephemeral copy of the domains for edition.
The events argument is used to notify the caller about domain changes and watches being triggered.
Note: Any domain that has changed or watches that have been triggered through the persistent API (e.g. due to substitutions) are immediately notified through the appropriare events callback.
val snapshot : Ephemeral.t -> tConverts back an ephemeral domain into a persistent one.