ATSLIB/libats/refcount
This package implements reference-counted values.
Note that this implementation is only good for use in
sequential programs.
Synopsis
stadef refcnt = refcnt_vt0ype_vtype
fun
{a:vt0p}
refcnt(x0: a): refcnt(a)
Description
Given a viewtype VT, refcnt(VT) is for a reference-counted
value that wraps around a value of the type VT with a ref-count.
Synopsis
absvtype
refcnt_vt0ype_vtype(a:vt@ype) = ptr
Synopsis
Synopsis for [refcnt_make] is unavailable.
Description
Given a value, which is usually linear, this function returns a
reference-counted value that wraps around the given value with a ref-count
equal to 1.
Synopsis
fun{a:vt0p}
refcnt_get_count(!refcnt(a)): intGte(1)
Description
This function returns the ref-count of a given reference-counted value.
Note that the returned ref-count must be positive.
Synopsis
fun{a:vt0p}
refcnt_incref (!refcnt(a)): refcnt(a)
Description
This function increases the ref-count of a given reference-counted value.
Synopsis
fun{a:vt0p}
refcnt_decref
(
rfc: refcnt(a), x: &a? >> opt(a, b)
) : #[b:bool] bool(b)
Description
This function decreases the ref-count of a given reference-counted
value. If the ref-count reaches 0, then the value contained in the
reference-counted value is put into the second argument of the function and
the memory holding the reference-counted value is freed. The returned
boolean indicates whether the given reference-counted value has been freed.
Synopsis
fun{a:vt0p}
refcnt_decref_opt (rfc: refcnt(a)): Option_vt(a)
Description
This function is just a slight variant of the function refcnt_decref.
Synopsis
fun{a:vt0p}
refcnt_vtakeout
(rfc: !refcnt(a))
: [l:addr] (a @ l, a @ l -<lin,prf> void | ptr l)
Description
This function is called to borrow a proof of at-view for the value
contained in a given reference-counted value. Note that borrowing of
this style is fundamentally unsafe but can be of great convenience
in practice.