ATSLIB/prelude/reference

A reference is just a persistent array of size 1. It is persistent in the sense that the memory associated with a reference is heap-allocated and can only be reclaimed by GC. While it is allowed to store linear values in references, doing so demands caution as resources contained in references may be inadvertently leaked.

ref_get_ptr

ref_get_viewptr

ref

ref_get_ptr

Synopsis

castfn ref_get_ptr
  {a:vt0p} (r: ref a):<> [l:agz] ptr (l)

Description

This cast function (castfn) returns the pointer associated with a given reference. Note that the returned pointer is guaranteed to be non-null.

ref_get_viewptr

Synopsis

castfn ref_get_viewptr
  {a:vt0p} (r: ref a):<> [l:agz] (vbox (a @ l) | ptr l)

Description

This cast function (castfn) returns the boxed at-view and pointer associated with a given reference. If the value stored in a reference is linear, then it is not allowed for the value be taken out from the reference. Instead, ref_get_viewptr can be called on the reference to allow that the value be processed in situ.

Example

The following function ref_exch_at exchanges the contents of a reference and a variable:

fun{a:vt0p}
ref_exch_at (
  r: ref (a), x: &a >> a
) : void = let
  val (
    vbox pf | p
  ) = ref_get_viewptr (r)
  val tmp = !p
in
  !p := x; x := tmp
end // end of [ref_exch_at]

Note that the type for the contents of r and x can be linear.

ref

Synopsis

fun{a:vt0p} ref(x: a):<!wrt> ref(a)

Description

This function creates a reference initialized with its given argument.

ref_make_elt

Synopsis

fun{a:vt0p} ref_make_elt(x: a):<!wrt> ref(a)

Description

This function does the same as ref.

ref_make_viewptr

Synopsis

castfn
ref_make_viewptr
  {a:vt0p}{l:addr} (pf: a @ l | p: ptr l):<> ref(a)

Description

This cast function (castfn) turns a pointer with a proof of at-view into a reference.

Example

The following code implements a counter:

local

var __count: int = 0 // it is statically allocated
val theCount =
  ref_make_viewptr {int} (view@(__count) | addr@(__count))
// end of [val]

in (* in of [local] *)

fun theCount_get (): int = !theCount

fun theCount_inc (): void = !theCount := !theCount + 1

fun theCount_getinc
  (): int = let
  val n = !theCount; val () = !theCount := n + 1 in n
end // end of [theCount_getind]

fun theCount_reset (): void = !theCount := 0

end // end of [local]

The specialty of this implementation is that it does not make use of any dynamic memory allocation. This is a style often necessary for low-level embedded systems programming.

ref_get_elt

Synopsis

fun{a:t0p} ref_get_elt (r: ref a):<!ref> a

Description

This function returns the value stored in a given reference. Note that the type of the value is nonlinear.

ref_set_elt

Synopsis

fun{a:t0p} ref_set_elt (r: ref a, x: a):<!refwrt> void

Description

This function stores a value (the second argument) into a given reference (the first argument). Note that the type of the value is nonlinear.

ref_exch_elt

Synopsis

fun{a:vt0p} ref_exch_elt (r: ref a, x: &a>>a):<!refwrt> void

Description

This function exchanges the value in a given reference (the first argument) with the value in a variable (the second argument). Note that the type of these values can be linear.

ref_app_fun

Synopsis

fun{}
ref_app_fun{a:vt0p}
(
  r: ref a, f: (&(a)>>_) -<0,!wrt> void
) :<!refwrt> void // end of [ref_app_fun]

ref_app_funenv

Synopsis

fun{}
ref_app_funenv{a:vt0p}
  {v:view}{vt:viewtype}
(
  pfv: !v
| r: ref a, f: (!v | &(a)>>_, !vt) -<0,!wrt> void, env: !vt
) :<!refwrt> void // end of [ref_app_funenv]

ref_vtakeout

Synopsis

fun{}
ref_vtakeout
  {a:vt0p}
(
  ref: ref (a)
) :<!ref> [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 to which a given reference points. 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.