Module Annot.LazyIAnnot

A derivation whose construction is deferred.

Used for the cells of a partitioned Let: building the derivation of the body for every cell up-front is wasteful, since the reconstruction may never explore some of them.

Forcing is shared, but pending substitutions are not: substitute returns a new handle onto the same deferred derivation, with the substitution queued on it. So two handles obtained from a same origin force it at most once, and each then applies its own substitutions to the result.

type t
val get : t -> IAnnot.t

Forces the derivation and applies the substitutions queued on this handle.

val mk_lazy : (unit -> IAnnot.t) -> t
val mk : IAnnot.t -> t
val is_concrete : t -> bool

Whether the underlying derivation has already been forced — not whether get would be free, as this handle may still carry pending substitutions.

val substitute : Mlsem_types.Subst.t -> t -> t
val pp : Stdlib.Format.formatter -> t -> unit