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_make_elt
  • ref_make_viewptr
  • ref_get_elt
  • ref_set_elt
  • ref_exch_elt
  • ref_app_fun
  • ref_app_funenv
  • ref_vtakeout

  • 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. SourceForge.net Logo