ATSLIB/libats/ML/array0
The functions declared in this package are primarily for supporting
ML-style processing of persisten arrays. Note that a plain array (as is in
C) is not available in languages such as Java and ML due to the need for
performing array-bounds checking at run-time. Instead, arrays in these
languages are always bundled together with their sizes. In ATS, the type
array0(T) is for an array paired with its size in which
elements of the type T are stored.
Synopsis
stadef array0 = array0_vt0ype_type
overload array0 with array0_make_arrpsz
overload array0 with array0_make_arrayref
Synopsis
abstype
array0_vt0ype_type
(a: vt@ype) = ptr
Synopsis
fun{}
array0_of_arrszref
{a:vt0p}(arrszref(a)):<> array0(a)
Synopsis
fun{}
arrszref_of_array0
{a:vt0p}(A: array0(a)):<> arrszref(a)
Synopsis
fun{}
array0_make_arrpsz
{a:vt0p}{n:int}
(psz: arrpsz(INV(a), n)):<!wrt> array0(a)
Example
The following code builds an array of digits and then print them out:
staload "libats/ML/SATS/array0.sats"
implement
main0 () =
{
val xs =
(array0)$arrpsz{int}(0, 1, 2, 3, 4, 5, 6, 7, 8, 9)
val () = array0_foreach<int> (xs, lam (x) => print_int (x))
val () = print_newline ()
}
Synopsis
fun{}
array0_get_ref
{a:vt0p}(A: array0(a)):<> Ptr1
Description
Tis function returns a pointer to the beginning of the array associated
with a given array0-value.
Synopsis
overload .size with array0_get_size
Synopsis
fun{}
array0_get_size
{a:vt0p}(A: array0(a)):<> size_t
Description
This function returns the size of the array associated with a given
array0-value.
Synopsis
fun{}
array0_get_refsize
{a:vt0p}
(
A : array0(a)
) :<> [n:nat] (arrayref(a, n), size_t(n))
Description
This function returns a pair that are essentially obtained by calling
array0_get_ref and array0_get_size.
Synopsis
overload
array0_make_elt with array0_make_elt_int
overload
array0_make_elt with array0_make_elt_size
Description
This function creates an array0-value of a given size (1st argument) in
which each array-cell is initialized with a given value (2nd argument).
Synopsis
fun{a:t0p}
array0_make_list
(xs: list0(INV(a))):<!wrt> array0(a)
Description
Given a list xs of length n, this function returns an array0-value A of the
same size such that A[i] equals xs[i] for i ranging from 0 until n-1,
inclusive.
Example
Given a file handle, the following function returns an array containing
all of the chars stored in the file referred to by the file handle:
staload
UN = "prelude/SATS/unsafe.sats"
staload "libats/ML/SATS/basis.sats"
staload "libats/ML/SATS/array0.sats"
fun
array0_make_fileref
(
inp: FILEref
) : array0 (char) = A0 where
{
val cs =
fileref_get_file_charlst (inp)
val A0 = array0_make_list ($UN.castvwtp1{list0(char)}(cs))
val () = list_vt_free (cs)
}
Synopsis
fun{a:t0p}
array0_make_rlist
(xs: list0(INV(a))):<!wrt> array0(a)
Description
Given a list xs of length n, this function returns an array0-value A of the
same size such that A[i] equals xs[n-i-1] for i ranging from 0 until n-1,
inclusive.
Synopsis
fun{a:t0p}
array0_make_subarray
( A: array0(a)
, st: size_t, ln: size_t):<!wrt> array0(a)
Description
Given an array0-value A of size n and two non-negative integers st and ln,
this function returns another array0-value A2 of size ln2 such that the
value in each A2[i] equals the value in A[st2+i], where st2 and ln2 equal
min(st,n) and min(ln,n-st2), respectively, and i ranges from 0 until ln2-1,
inclusive. Please note that the returned array0-value A2 is of size 0 if st
is greater than or equal to n.
Synopsis
overload
array0_get_at with array0_get_at_gint
overload
array0_get_at with array0_get_at_guint
Synopsis
fun
{a:t0p}{tk:tk}
array0_get_at_gint
(A: array0(a), i: g0int(tk)):<!exnref> (a)
Description
Given an array0-value A of size n and an index i, this function returns
A[i] if i is valid (that is, 0 <= i < n), or it raises the exception
ArraySubscriptExn.
Synopsis
fun
{a:t0p}{tk:tk}
array0_get_at_guint
(A: array0(a), i: g0uint(tk)):<!exnref> (a)
Description
This function is like array0_get_at_gint except for the given
index being an unsigned integer.
Synopsis
overload
array0_set_at with array0_set_at_gint
overload
array0_set_at with array0_set_at_guint
Synopsis
fun
{a:t0p}{tk:tk}
array0_set_at_gint
( A: array0(a)
, i: g0int(tk), x: a):<!exnrefwrt> void
Description
Given an array0-value A of size n, an index i and a value x, this function
assigns x to A[i] if i is valid (that is, 0 <= i < n), or it raises the
exception ArraySubscriptExn.
Synopsis
fun
{a:t0p}{tk:tk}
array0_set_at_guint
( A: array0(a)
, i: g0uint(tk), x: a):<!exnrefwrt> void
Description
This function is like array0_set_at_gint except for the given
index being an unsigned integer.
Synopsis
overload
array0_exch_at with array0_exch_at_gint
overload
array0_exch_at with array0_exch_at_guint
Synopsis
fun
{a:vt0p}{tk:tk}
array0_exch_at_gint
( A: array0(a)
, i: g0int(tk), x: &a >> _):<!exnrefwrt> void
Description
Given an array0-value A of size n, an index i and a reference x, this
function exchanges the values of A[i] and x if i is valid (that is, 0 <= i < n),
or it raises the exception ArraySubscriptExn.
Synopsis
fun
{a:vt0p}{tk:tk}
array0_exch_at_guint
( A: array0(a)
, i: g0uint(tk), x: &a >> _):<!exnrefwrt> void
Description
This function is like array0_exch_at_gint except for the given
index being an unsigned integer.
Synopsis
fun{a:t0p}
array0_copy(array0(a)):<!refwrt> array0(a)
Description
Given an array0-value A of size n, this function returns another
array0-value B such that each B[i] is initialized with A[i], where i ranges
from i until n-1, inclusive.
Synopsis
fun{a:t0p}
array0_append
(array0(a), array0(a)):<!refwrt> array0(a)
Description
Given two array0-values A1 and A2, this function returns another
array0-value B that contains the concatenation of the elements in A1 and
A2.
Synopsis
fun
{a:vt0p}
{b:vt0p}
array0_map
(
A0: array0(a), fopr: (&a) -<cloref1> b
) : array0(b)
Description
Given an array0-value A of size n and a function f, this function returns
another array0-value B of the same size such that each B[i] is initialized
with the value returned by f(A[i]), where i ranges from 0 until n-1,
inclusive.
Synopsis
Synopsis for [array0_mapopt] is unavailable.
Description
Given an array0-value A of size n and a function f, this function returns
another array0-value B that collects precisely every x whenever
Some0(x) is returned by f(A[i]), where i ranges from 0 until
n-1, inclusive.
Synopsis
fun
{a:vt0p}
array0_tabulate
{n:int}
(
asz: size_t(n), fopr: (sizeLt(n)) -<cloref1> a
) : array0(a)
Description
Given a size asz and a function f, this function returns an array0-value A
of size asz such that each A[i] is initialized with the value returned by f(i),
where i ranges from 0 until asz-1, inclusive.
Synopsis
Synopsis for [array0_tabulate_opt] is unavailable.
Description
Given an integer asz and a function f, this function returns an array0-value
that collects precisely every x whenever Some0(x) is returned
by f(i), where i ranges from 0 until asz-1, inclusive.
Synopsis
fun
{a:vt0p}
array0_find_exn
(
xs: array0(a), pred: (&a) -<cloref1> bool
) : size_t
Description
This function returns the index of the first array-cell in a given array
that contains an element satisfiing a given predicate. If there is no such
an element, then the function raises an exception (NotFoundExn).
Synopsis
fun
{a:vt0p}
array0_find_opt
(
xs: array0(a), pred: (&a) -<cloref1> bool
) : Option_vt(size_t)
Description
This function is just the optional version of array0_find_exn.
Synopsis
fun
{a:vt0p}
array0_foreach
(
A0: array0(a)
, fwork: (&a >> _) -<cloref1> void
) : void
Description
Given an array0-value A of size n and a function f, this function applies f
to each A[i], where i ranges from 0 until n-1, inclusive.
Synopsis
fun
{a:vt0p}
array0_iforeach
(
A0: array0(a)
, fwork: (size_t, &a >> _) -<cloref1> void
) : void
Description
Given an array0-value A of size n and a function f, this function applies f
to each pair (i, A[i]), where i ranges from 0 until n-1, inclusive.
Synopsis
fun{
res:vt0p}{a:vt0p
} array0_foldleft
( A0: array0(a)
, ini: res, fopr: (res, &a) -<cloref1> res
) : res
Synopsis
fun{
res:vt0p}{a:vt0p
} array0_ifoldleft
( A0: array0(a), ini: res
, fopr: (res, size_t, &a) -<cloref1> res
) : res
Synopsis
fun
{a:vt0p}
array0_rforeach
( A0: array0(a)
, fwork: (&a >> _) -<cloref1> void
) : void
Description
Given an array0-value A of size n and a function f, this function applies f
to each A[n-i-1], where i ranges from 0 until n-1, inclusive.
Synopsis
fun{
a:vt0p}{res:vt0p
} array0_foldright
(
A0: array0(a)
, fopr: (&a, res) -<cloref1> res, snk: res
) : res
Synopsis
overload
[] with array0_get_at_gint
overload
[] with array0_set_at_gint
overload
[] with array0_get_at_guint
overload
[] with array0_set_at_guint
Synopsis
overload .size with array0_get_size
Synopsis
overload fprint with fprint_array0
overload fprint with fprint_array0_sep