Refinement.RefinementsRefinements collected over a whole expression: those attached to a program point, plus anonymous ones that only contribute to partitioning.
val empty : tval get : t -> Mlsem_common.Eid.t -> Mlsem_common.REnv.tThe refinement holding at a program point; the empty (trivially true) environment if none was recorded.
val get_anonymous : t -> Mlsem_common.REnv.t listval all : t -> Mlsem_common.REnv.t listEvery recorded refinement, located or not.
val add : t -> Mlsem_common.Eid.t -> Mlsem_common.REnv.t -> tRecords a refinement at a program point, intersecting it with any refinement already recorded there. Distinct program points must therefore carry distinct Eid.ts, or unrelated refinements get conflated.
val add_anonymous : t -> Mlsem_common.REnv.t -> tval map : (Mlsem_common.REnv.t -> Mlsem_common.REnv.t) -> t -> t