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.
stadef arrayref = arrayref_vt0ype_int_type
overload
arrayref with arrayref_make_arrpsz
abstype
arrayref_vt0ype_int_type
(a: vt@ype(*elt*), n: int(*size*)) = ptr
castfn
arrayptr_refize
{a:vt0p}
{l:addr}{n:int}
(
A0:
arrayptr(INV(a), l, n)
) :<!wrt> arrayref(a, n)
castfn arrayref_get_viewptr {a:vt0p}{n:int} ( A0: arrayref(a, n) ) :<> [ l:addr ] ( vbox(array_v(a, l, n)) | ptr(l) ) (* end of [arrayref_get_viewptr] *)
fun
{a:t0p}
arrayref_make_elt
{n:int}
(
asz: size_t(n), x0: a
) :<!wrt> arrayref(a, n)
overload
arrayref_get_at with arrayref_get_at_gint of 0
overload
arrayref_get_at with arrayref_get_at_guint of 0
fun{ a:t0p}{tk:tk } arrayref_get_at_gint {n:int}{i:nat | i < n} ( A0: arrayref(a, n), i: g1int(tk, i) ) :<!ref> (a) // arrayref_get_at_gint
fun{ a:t0p}{tk:tk } arrayref_get_at_guint {n:int}{i:nat | i < n} ( A0: arrayref(a, n), i: g1uint(tk, i) ) :<!ref> (a) // arrayref_get_at_guint
overload
arrayref_set_at with arrayref_set_at_gint of 0
overload
arrayref_set_at with arrayref_set_at_guint of 0
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]
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]
overload
arrayref_exch_at with arrayref_exch_at_gint of 0
overload
arrayref_exch_at with arrayref_exch_at_guint of 0
fun{ a:vt0p}{tk:tk } arrayref_exch_at_gint {n:int}{i:nat | i < n} ( A0: arrayref(a, n), i: g1int(tk, i), x: &a >> _ ) :<!refwrt> void // arrayref_exch_at_gint
fun{ a:vt0p}{tk:tk } arrayref_exch_at_guint {n:int}{i:nat | i < n} ( A0: arrayref(a, n), i: g1uint(tk, i), x: &a >> _ ) :<!refwrt> void // arrayref_exch_at_guint
fun{a:vt0p} fprint_arrayref {n:int} ( FILEref , arrayref(a, n), asz: size_t(n) ) : void // end of [fprint_arrayref]
fun{a:vt0p} fprint_arrayref_sep {n:int} ( FILEref , arrayref(a, n), asz: size_t(n), sep: NSH(string) ) : void // end of [fprint_arrayref_sep]
fun{a:t0p}
arrayref_copy{n:int}
(A: arrayref(a, n), n: size_t(n)): arrayptr(a, n)
fun{a:vt0p}
arrayref_tabulate
{n:int}(asz: size_t(n)): arrayref(a, n)
stadef arrszref = arrszref_vt0ype_type
overload arrszref with arrszref_make_arrpsz
abstype
arrszref_vt0ype_type (a: vt@ype) = ptr
fun{}
arrszref_make_arrpsz
{a:vt0p}{n:int}
(arrpsz (INV(a), n)):<!wrt> arrszref(a)
fun{}
arrszref_make_arrayref
{a:vt0p}{n:int}
(A: SHR(arrayref(a, n)), n: size_t(n)):<!wrt> arrszref(a)
fun{
} arrszref_get_ref{a:vt0p} (A: arrszref(a)):<> Ptr1
fun{
} arrszref_get_size{a:vt0p} (A: arrszref(a)):<> size_t
fun{} arrszref_get_refsize{a:vt0p} ( A: arrszref(a), asz: &size_t? >> size_t(n) ) :<!wrt> #[n:nat] arrayref(a, n) // end-of-fun
fun{a:t0p}
arrszref_make_elt(asz: size_t, x: a):<!wrt> arrszref(a)
overload
arrszref_get_at with arrszref_get_at_gint of 0
overload
arrszref_get_at with arrszref_get_at_guint of 0
fun{
a:t0p}{tk:tk
} arrszref_get_at_gint
(A: arrszref(a), i: g0int(tk)):<!exnref> a
fun{
a:t0p}{tk:tk
} arrszref_get_at_guint
(A: arrszref(a), i: g0uint(tk)):<!exnref> a
overload
arrszref_set_at with arrszref_set_at_gint of 0
overload
arrszref_set_at with arrszref_set_at_guint of 0
fun{
a:t0p}{tk:tk
} arrszref_set_at_gint
(A: arrszref(a), i: g0int(tk), x: a):<!exnrefwrt> void
fun{
a:t0p}{tk:tk
} arrszref_set_at_guint
(A: arrszref(a), i: g0uint(tk), x: a):<!exnrefwrt> void
overload
arrszref_exch_at with arrszref_exch_at_gint of 0
overload
arrszref_exch_at with arrszref_exch_at_guint of 0
fun{ a:vt0p }{tk:tk} arrszref_exch_at_gint ( A0: arrszref(a), i: g0int(tk), x: &a >> _ ) :<!exnrefwrt> void // end-of-function
fun{ a:vt0p }{tk:tk} arrszref_exch_at_guint ( A0: arrszref(a), i: g0uint(tk), x: &a >> _ ) :<!exnrefwrt> void // end-of-function
fun{a:vt0p}
fprint_arrszref
(out: FILEref, A: arrszref(a)): void
fun{a:vt0p} fprint_arrszref_sep ( out: FILEref, A: arrszref(a), sep: NSH(string) ) : void // end of [fprint_arrszref_sep]
fun{a:vt0p}
arrszref_tabulate(asz: size_t): arrszref(a)
overload [] with arrayref_get_at_gint of 0
overload [] with arrayref_set_at_gint of 0
overload [] with arrszref_get_at_gint of 0
overload [] with arrszref_set_at_gint of 0
overload [] with arrayref_get_at_guint of 0
overload [] with arrayref_set_at_guint of 0
overload [] with arrszref_get_at_guint of 0
overload [] with arrszref_set_at_guint of 0
overload .size with arrszref_get_size
overload .head with arrayref_head
overload .tail with arrayref_tail
overload ptrcast with arrayref2ptr
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. |
|