ATSLIB/prelude/arrayref

This package contains functions for creating and manipulating persistent arrays.

Given a type T, the type arrayref(T, N) is for a plain array containing N cells in which elements of the type T are stored. Array-subscripting on an arrayref-value requires static verification that the subscripting index is within the bounds of the subscripted array. Note that the type T can be linear. However, it is somewhat unwieldy in practice to make use of an arrayref-value containing linear elements.

Given a type T, the type arrszref(T) is for an array paired with its own size in which elements of the type T are stored. Array-subscripting on an arrszref-value is internally combined with array-bounds checking at run-time to prevent the use of illegal array-indexes (at the expense of raising probably unattended exceptions).

In safe programming languages such as Java and ML, plain and ungarnished arrays cannot be safely supported due to the limitation of the underlying type systems. Instead, arrszref-values (or something similar) are used to represent arrays so that array-bounds checking can be performed at run-time.


  • arrayref
  • arrayref_vt0ype_int_type
  • arrayptr_refize
  • arrayref_get_viewptr
  • arrayref_make_elt
  • arrayref_get_at
  • arrayref_get_at_gint
  • arrayref_get_at_guint
  • arrayref_set_at
  • arrayref_set_at_gint
  • arrayref_set_at_guint
  • arrayref_exch_at
  • arrayref_exch_at_gint
  • arrayref_exch_at_guint
  • fprint_arrayref
  • fprint_arrayref_sep
  • arrayref_copy
  • arrayref_tabulate
  • arrszref
  • arrszref_vt0ype_type
  • arrszref_make_arrpsz
  • arrszref_make_arrayref
  • arrszref_get_ref
  • arrszref_get_size
  • arrszref_get_refsize
  • arrszref_make_elt
  • arrszref_get_at
  • arrszref_get_at_gint
  • arrszref_get_at_guint
  • arrszref_set_at
  • arrszref_set_at_gint
  • arrszref_set_at_guint
  • arrszref_exch_at
  • arrszref_exch_at_gint
  • arrszref_exch_at_guint
  • fprint_arrszref
  • fprint_arrszref_sep
  • arrszref_tabulate
  • Overloaded Symbols
  • []
  • .size
  • .head
  • .tail
  • ptrcast
  • fprint

  • arrayref

    Synopsis

    stadef arrayref = arrayref_vt0ype_int_type
    overload arrayref with arrayref_make_arrpsz

    Description

    Given a type T and an integer N, the type arrayref(T, N) is for persistent arrays of size N in which each element is of the type T.

    arrayref_vt0ype_int_type

    Synopsis

    abstype
    arrayref_vt0ype_int_type
      (a: vt@ype(*elt*), n: int(*size*)) = ptr

    arrayptr_refize

    Synopsis

    castfn
    arrayptr_refize
      {a:vt0p}
      {l:addr}
      {n:int} (
      A: arrayptr (INV(a), l, n)
    ) :<!wrt> arrayref (a, n) // end of [arrayptr_refize]

    arrayref_get_viewptr

    Synopsis

    castfn
    arrayref_get_viewptr
      {a:vt0p}
      {n:int} (
      A: arrayref (a, n)
    ) :<> [l:addr] (vbox (array_v (a, l, n)) | ptr l)

    arrayref_make_elt

    Synopsis

    fun{a:t0p}
    arrayref_make_elt
      {n:int} (asz: size_t n, x: a):<!wrt> arrayref (a, n)

    arrayref_get_at

    Synopsis

    overload arrayref_get_at with arrayref_get_at_gint of 0
    overload arrayref_get_at with arrayref_get_at_guint of 0

    arrayref_get_at_gint

    Synopsis

    fun{
    a:t0p}{tk:tk
    } arrayref_get_at_gint
      {n:int}{i:nat | i < n}
    (
      A: arrayref(a, n), i: g1int(tk, i)
    ) :<!ref> a // end of [arrayref_get_at_gint]

    arrayref_get_at_guint

    Synopsis

    fun{
    a:t0p}{tk:tk
    } arrayref_get_at_guint
      {n:int}{i:nat | i < n}
    (
      A: arrayref(a, n), i: g1uint(tk, i)
    ) :<!ref> a // end of [arrayref_get_at_guint]

    arrayref_set_at

    Synopsis

    overload arrayref_set_at with arrayref_set_at_gint of 0
    overload arrayref_set_at with arrayref_set_at_guint of 0

    arrayref_set_at_gint

    Synopsis

    fun{
    a:t0p}{tk:tk
    } arrayref_set_at_gint
      {n:int}{i:nat | i < n} (
      A: arrayref (a, n), i: g1int (tk, i), x: a
    ) :<!refwrt> void // end of [arrayref_set_at_gint]

    arrayref_set_at_guint

    Synopsis

    fun{
    a:t0p}{tk:tk
    } arrayref_set_at_guint
      {n:int}{i:nat | i < n} (
      A: arrayref (a, n), i: g1uint (tk, i), x: a
    ) :<!refwrt> void // end of [arrayref_set_at_guint]

    arrayref_exch_at

    Synopsis

    overload arrayref_exch_at with arrayref_exch_at_gint of 0
    overload arrayref_exch_at with arrayref_exch_at_guint of 0

    arrayref_exch_at_gint

    Synopsis

    fun{
    a:vt0p}{tk:tk
    } arrayref_exch_at_gint
      {n:int}{i:nat | i < n} (
      A: arrayref (a, n), i: g1int (tk, i), x: &a >> _
    ) :<!refwrt> void // end of [arrayref_exch_at_gint]

    arrayref_exch_at_guint

    Synopsis

    fun{
    a:vt0p}{tk:tk
    } arrayref_exch_at_guint
      {n:int}{i:nat | i < n} (
      A: arrayref (a, n), i: g1uint (tk, i), x: &a >> _
    ) :<!refwrt> void // end of [arrayref_exch_at_guint]

    fprint_arrayref

    Synopsis

    fun{a:vt0p}
    fprint_arrayref
      {n:int} (
      out: FILEref, A: arrayref (INV(a), n), n: size_t n
    ) : void // end of [fprint_arrayref]

    fprint_arrayref_sep

    Synopsis

    fun{a:vt0p}
    fprint_arrayref_sep
      {n:int} (
      out: FILEref
    , A: arrayref (a, n), asz: size_t n, sep: NSH(string)
    ) : void // end of [fprint_arrayref_sep]

    Description

    This function prints the elements in a given array to the output channel provided as its first argument, interspersing the string sep between the printed array elements. Note that printing each array element is handled by calling the function fprint_ref.

    arrayref_copy

    Synopsis

    fun{a:t0p}
    arrayref_copy{n:int}
      (A: arrayref (a, n), n: size_t (n)): arrayptr (a, n)

    arrayref_tabulate

    Synopsis

    fun{a:vt0p}
    arrayref_tabulate
      {n:int} (asz: size_t n): arrayref (a, n)

    arrszref

    Synopsis

    stadef arrszref = arrszref_vt0ype_type
    overload arrszref with arrszref_make_arrpsz

    arrszref_vt0ype_type

    Synopsis

    abstype
    arrszref_vt0ype_type (a: vt@ype) = ptr

    arrszref_make_arrpsz

    Synopsis

    fun{}
    arrszref_make_arrpsz
      {a:vt0p}{n:int}
      (arrpsz (INV(a), n)):<!wrt> arrszref(a)

    arrszref_make_arrayref

    Synopsis

    fun{}
    arrszref_make_arrayref
      {a:vt0p}{n:int}
      (A: SHR(arrayref(a, n)), n: size_t n):<!wrt> arrszref (a)

    Description

    This function combines an arrayref-value and its size into an arrszref-value.

    arrszref_get_ref

    Synopsis

    fun{
    } arrszref_get_ref{a:vt0p} (A: arrszref (a)):<> Ptr1

    Description

    This function returns the pointer to the arrayref-value inside a given arrszref-value.

    arrszref_get_size

    Synopsis

    fun{
    } arrszref_get_size{a:vt0p} (A: arrszref (a)):<> size_t

    Description

    This function returns the size of a given arrszref-value.

    arrszref_get_refsize

    Synopsis

    fun{}
    arrszref_get_refsize{a:vt0p}
      (A: arrszref (a), asz: &size_t? >> size_t n):<!wrt> #[n:nat] arrayref (a, n)

    Description

    This function obtains the arrayref-value and its size in a given arrszref-value.

    arrszref_make_elt

    Synopsis

    fun{a:t0p}
    arrszref_make_elt (asz: size_t, x: a):<!wrt> arrszref (a)

    arrszref_get_at

    Synopsis

    overload arrszref_get_at with arrszref_get_at_gint of 0
    overload arrszref_get_at with arrszref_get_at_guint of 0

    arrszref_get_at_gint

    Synopsis

    fun{
    a:t0p}{tk:tk
    } arrszref_get_at_gint
      (A: arrszref (a), i: g0int (tk)):<!exnref> a

    arrszref_get_at_guint

    Synopsis

    fun{
    a:t0p}{tk:tk
    } arrszref_get_at_guint
      (A: arrszref (a), i: g0uint (tk)):<!exnref> a

    arrszref_set_at

    Synopsis

    overload arrszref_set_at with arrszref_set_at_gint of 0
    overload arrszref_set_at with arrszref_set_at_guint of 0

    arrszref_set_at_gint

    Synopsis

    fun{
    a:t0p}{tk:tk
    } arrszref_set_at_gint
      (A: arrszref (a), i: g0int (tk), x: a):<!exnrefwrt> void

    arrszref_set_at_guint

    Synopsis

    fun{
    a:t0p}{tk:tk
    } arrszref_set_at_guint
      (A: arrszref (a), i: g0uint (tk), x: a):<!exnrefwrt> void

    arrszref_exch_at

    Synopsis

    overload arrszref_exch_at with arrszref_exch_at_gint of 0
    overload arrszref_exch_at with arrszref_exch_at_guint of 0

    arrszref_exch_at_gint

    Synopsis

    fun{
    a:vt0p}{tk:tk
    } arrszref_exch_at_gint
      (A: arrszref (a), i: g0int (tk), x: &a >> _):<!exnrefwrt> void

    arrszref_exch_at_guint

    Synopsis

    fun{
    a:vt0p}{tk:tk
    } arrszref_exch_at_guint
      (A: arrszref (a), i: g0uint (tk), x: &a >> _):<!exnrefwrt> void

    fprint_arrszref

    Synopsis

    fun{a:vt0p}
    fprint_arrszref
      (out: FILEref, A: arrszref (a)): void

    fprint_arrszref_sep

    Synopsis

    fun{a:vt0p}
    fprint_arrszref_sep (
      out: FILEref, A: arrszref (a), sep: NSH(string)
    ) : void // end of [fprint_arrszref_sep]

    arrszref_tabulate

    Synopsis

    fun{a:vt0p}
    arrszref_tabulate (asz: size_t): arrszref (a)

    Overloaded Symbols


    []

    Synopsis

    overload [] with arrayref_get_at_gint of 0
    overload [] with arrayref_get_at_guint of 0
    overload [] with arrayref_set_at_gint of 0
    overload [] with arrayref_set_at_guint of 0
    overload [] with arrszref_get_at_gint of 0
    overload [] with arrszref_get_at_guint of 0
    overload [] with arrszref_set_at_gint of 0
    overload [] with arrszref_set_at_guint of 0

    .size

    Synopsis

    overload .size with arrszref_get_size

    .head

    Synopsis

    overload .head with arrayref_head

    .tail

    Synopsis

    overload .tail with arrayref_tail

    ptrcast

    Synopsis

    overload ptrcast with arrayref2ptr

    fprint

    Synopsis

    overload fprint with fprint_arrayref
    overload fprint with fprint_arrayref_sep
    overload fprint with fprint_arrszref
    overload fprint with fprint_arrszref_sep

    This page is created with ATS by Hongwei Xi and also maintained by Hongwei Xi. SourceForge.net Logo