Module Make.Ephemeral

include Domains_intf.EphemeralDomainMap with type key = AltErgoLib.Domains_intf.X.r and type Entry.domain = D.t
type t

The type of ephemeral domain maps, i.e. an imperative structure mapping keys to their current domain.

The type of keys in the ephemeral map.

module Entry : sig ... end
val entry : t -> key -> Entry.t

entry t k returns the entry associated with k.

There is a unique entry associated with each key k that is created on-the-fly when entry t k is called for the first time. Calling entry t k with the same key will always return the same (physical) entry.

The domain associated with the entry is initialized from the underlying persistent domain (or the default function provided to edit) the first time it is accessed, and updated with set_domain or update.

include Domains_intf.EntryNotation with type entry := Entry.t and type domain := D.t
val (!!) : Entry.t -> D.t

Return the domain associated with this entry.

val update : ex:Explanation.t -> Entry.t -> D.t -> unit

update ~ex e d updates the domain associated with e, intersecting it with d. The explanation ex is added to d.

  • raises Domain.Inconsistent

    if the domains are incompatible.

module Canon : sig ... end

The Canon module first computes the canonical representative in an Uf.t instance before accessing the ephemeral map.

val canon : Uf.t -> t -> Canon.t

Wraps the ephemeral domain map to first compute the canonical representative in the current union-find environment prior to accessing the ephemeral map.

Note: The canonical map shares the same mutable space with the original map.