ATSLIB/libats/refcount

This package implements reference-counted values. Note that this implementation is only good for use in sequential programs.


  • refcnt
  • refcnt_vt0ype_vtype
  • refcnt_make
  • refcnt_get_count
  • refcnt_incref
  • refcnt_decref
  • refcnt_decref_opt
  • refcnt_vtakeout

  • refcnt

    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.

    refcnt_vt0ype_vtype

    Synopsis

    absvtype // invariant
    refcnt_vt0ype_vtype(a:vt@ype) = ptr

    refcnt_make

    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.

    refcnt_get_count

    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.

    refcnt_incref

    Synopsis

    fun{a:vt0p}
    refcnt_incref (!refcnt(a)): refcnt(a)

    Description

    This function increases the ref-count of a given reference-counted value.

    refcnt_decref

    Synopsis

    fun{a:vt0p}
    refcnt_decref
    (
      rfc: refcnt(a), x: &a? >> opt(a, b)
    ) : #[b:bool] bool(b) // end-of-fun

    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.

    refcnt_decref_opt

    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.

    refcnt_vtakeout

    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.
    This page is created with ATS by Hongwei Xi and also maintained by Hongwei Xi. SourceForge.net Logo