Module Stdlib.Weak

The type of arrays of weak pointers (weak arrays). A weak pointer is a value that the garbage collector may erase whenever the value is not used any more (through normal pointers) by the program. Note that finalisation functions are run before the weak pointers are erased, because the finalisation functions can make values alive again (before 4.03 the finalisation functions were run after).

A weak pointer is said to be full if it points to a value, empty if the value was erased by the GC.

Notes:

• Integers are not allocated and cannot be stored in weak arrays.
• Weak arrays cannot be marshaled using output_value nor the functions of the Marshal module.

Weak.create n returns a new weak array of length n. All the pointers are initially empty.

Weak.length ar returns the length (number of elements) of ar.

Weak.set ar n (Some el) sets the nth cell of ar to be a (full) pointer to el; Weak.set ar n None sets the nth cell of ar to empty.

Weak.get ar n returns None if the nth cell of ar is empty, Some x (where x is the value) if it is full.

Weak.get_copy ar n returns None if the nth cell of ar is empty, Some x (where x is a (shallow) copy of the value) if it is full. In addition to pitfalls with mutable values, the interesting difference with get is that get_copy does not prevent the incremental GC from erasing the value in its current cycle (get may delay the erasure to the next GC cycle).

Weak.check ar n returns true if the nth cell of ar is full, false if it is empty. Note that even if Weak.check ar n returns true, a subsequent Weak.get ar n can return None.

Weak.fill ar ofs len el sets to el all pointers of ar from ofs to ofs + len - 1.

Weak.blit ar1 off1 ar2 off2 len copies len weak pointers from ar1 (starting at off1) to ar2 (starting at off2). It works correctly even if ar1 and ar2 are the same.