Make.Ephemeral
include Domains_intf.EphemeralDomainMap
with type key = AltErgoLib.Domains_intf.X.r
and type Entry.domain = D.t
The type of ephemeral domain maps, i.e. an imperative structure mapping keys to their current domain.
type key = AltErgoLib.Domains_intf.X.r
The type of keys in the ephemeral map.
module Entry : sig ... end
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 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
.
module Canon : sig ... end
The Canon
module first computes the canonical representative in an Uf.t
instance before accessing the ephemeral map.