ATSLIB/prelude/array

The type for a plain ungarnished array containing N elements of type T is denoted by the special syntax @[T][N]. The size of this array-type is N times the size of T and its linearity coincides with the linearity of T, that is, the type @[T][N] is linear if and only if T is linear. It should be noted that a value of this form of array-type can be passed to a function call only as a call-by-reference parameter (unless certain special arrangement is made for it to be passed as a call-by-value parameter).

Please see array.sats and array.dats (plus array_bsearch.dats, array_quicksort.dats) for the SATS file and DATS files in ATSLIB where the functions in this package are declared and implemented.

array_v

ArraySubscriptExn

array_initize_list_vt

array_initize_rlist_vt

array_uninitize

array_uninitize$clear

array_quicksort_stdlib

array_permute$randint

Overloaded Symbols

[]

array_v

Synopsis

viewtypedef array_v (a: viewt@ype, l:addr, n: int) = @[a][n] @ l

Description

Given a type T, an address L and an integer N, the view array_v(T, L, N) means that a value of the type @[T][N] is stored at the location L. An equivalent definition of array_v can be given as follows:

dataview array_v
  (a:vt@ype+, l:addr, int) =
  | array_v_nil (a, l, 0) of ((*none*))
  | {n:nat}
    array_v_cons (a, l, n+1) of (a @ l, array_v (a, l+sizeof(a), n))
// end of [array_v]

where array_v is (recursively) defined as a dataview.

ArraySubscriptExn

Synopsis

exception
ArraySubscriptExn of ()

Description

By convention, this exception is raised to indicate a situation where the index involved in array subscripting is out-of-bounds.

lemma_array_param

Synopsis

praxi
lemma_array_param
  {a:vt0p}{l:addr}{n:int}
  (A: &(@[INV(a)][n])): [n >= 0] void

Description

This proof function establishes that the integer n in any array-type @[T][n] is a natural number.

lemma_array_v_param

Synopsis

praxi
lemma_array_v_param
  {a:vt0p}{l:addr}{n:int}
  (pf: !array_v (INV(a), l, n)): [n >= 0] void

Description

This proof function establishes that the integer n in any array-view array_v(T, l, n) is a natural number.

array_v_nil

Synopsis

praxi
array_v_nil :
  {a:vt0p}{l:addr} () -<prf> array_v (a, l, 0)

Description

This proof function generates a proof of empty array-view.

array_v_unnil

Synopsis

praxi
array_v_unnil :
  {a:vt0p}{l:addr} array_v (a, l, 0) -<prf> void

Description

This proof function consumes a proof of empty array-view.

array_v_unnil_nil

Synopsis

prfun
array_v_unnil_nil :
  {a1,a2:vt0p}{l:addr} array_v (a1, l, 0) -<prf> array_v (a2, l, 0)

Description

This proof function consumes a proof of empty array-view and then generates a proof of empty array-view. It is a combination of array_v_unnil and array_v_nil.

array_v_cons

Synopsis

praxi
array_v_cons :
{a:vt0p}{l:addr}{n:int}
(a @ l, array_v (INV(a), l+sizeof(a), n)) -<prf> array_v (a, l, n+1)

Description

This proof function composes a proof of at-view and a proof of array-view of size n to form a proof of array-view of size n+1.

array_v_uncons

Synopsis

praxi
array_v_uncons :
{a:vt0p}{l:addr}{n:int | n > 0}
array_v (INV(a), l, n) -<prf> (a @ l, array_v (a, l+sizeof(a), n-1))

Description

This proof function is the inverse of array_v_cons: It decomposes a proof of array-view of size n into a proof of at-view and a proof of array-view of size n-1, where n is positive.

array_v_sing

Synopsis

prfun
array_v_sing
  {a:vt0p}{l:addr} (pf: INV(a) @ l): array_v (a, l, 1)

Description

This proof function turns a proof of at-view into a proof of array-view of size 1.

array_v_unsing

Synopsis

prfun
array_v_unsing
  {a:vt0p}{l:addr} (pf: array_v (INV(a), l, 1)): a @ l

Description

This proof function is the inverse of array_v_sing: It turns a proof of array-view of size 1 into a proof of at-view.

array_getref_at

Synopsis

fun
{a:vt0p}
array_getref_at
  {n:int} (A: &RD(@[INV(a)][n]), i: sizeLt n):<> cPtr1(a)

Description

This function returns the pointer to array-cell i of the given array A, that is, the pointer equal to addr@(A)+i*sizeof<a>, where addr@(A) refers to the starting address of A.

Example

A typical use of array_getref_at is given in the following example:

//
staload UN = "prelude/SATS/unsafe.sats"
//
fun{a:t0p}
array_get_at{n:int}
(
  A: &(@[a][n]), i: sizeLt n
) : a = let
  val p = array_getref_at<a> (A, i) in $UN.cptr_get (p)
end // end of [array_get_at]

fun{a:t0p}
array_set_at{n:int}
(
  A: &(@[a][n]), i: sizeLt n, x: a
) : void = let
  val p = array_getref_at<a> (A, i) in $UN.cptr_set (p, x)
end // end of [array_set_at]

Note that unsafe functions cptr_get and cptr_set are called here to read from and write through the pointer p.

array_get_at

Synopsis

overload array_get_at with array_get_at_gint of 0

overload array_get_at with array_get_at_guint of 0

array_get_at_gint

Synopsis

fun{
a:t0p}{tk:tk
} array_get_at_gint
  {n:int}
  (A: &RD(@[INV(a)][n]), i: g1intLt(tk, n)):<> a

Description

This function, which overloads the symbol [], returns the value stored in array-cell i of the given array A. Note that the type for values stored in A is nonlinear.

Example

The following code computes the sum of the doubles stored in a given array:

fn tally{n:nat}
(
  A: &(@[double][n]), n: int n
) :<(*none*)> double = let
//
fun loop
  {i:nat | i <= n} .<n-i>.
(
  A: &(@[double][n]), n: int n, i: int i, res: double
) :<(*none*)> double =
  if n > i then loop (A, n, i+1, res + A[i]) else res
//
in
  loop (A, n, 0(*i*), 0.0(*res*))
end // end of [tally]

array_get_at_guint

Synopsis

fun{
a:t0p}{tk:tk
} array_get_at_guint
  {n:int}
  (A: &RD(@[INV(a)][n]), i: g1uintLt(tk, n)):<> a

Description

This function, which overloads the symbol [], is like array_get_at_gint except that the index is unsigned.

array_set_at

Synopsis

overload array_set_at with array_set_at_gint of 0

overload array_set_at with array_set_at_guint of 0

array_set_at_gint

Synopsis

fun{
a:t0p}{tk:tk
} array_set_at_gint
  {n:int}
  (A: &(@[INV(a)][n]), i: g1intLt(tk, n), x: a):<!wrt> void

Description

This function, which overloads the symbol [], stores a value into array-cell i of the given array A, overwriting the original value. Note that the type of values stored in A is nonlinear.

Example

The following code doubles the integer value of each array-cell in a given array:

fn doubling{n:nat}
(
  A: &(@[int][n]), n: int n
) :<!wrt> void = let
//
fun loop
  {i:nat | i <= n} .<n-i>.
(
  A: &(@[int][n]), n: int n, i: int i
) :<!wrt> void =
  if n > i then (A[i] := 2 * A[i]; loop (A, n, i+1)) else ()
//
in
  loop (A, n, 0)
end // end of [doubling]

array_set_at_guint

Synopsis

fun{
a:t0p}{tk:tk
} array_set_at_guint
  {n:int}
  (A: &(@[INV(a)][n]), i: g1uintLt(tk, n), x: a):<!wrt> void

Description

This function, which overloads the symbol [], is like array_set_at_gint except that the index is unsigned.

array_exch_at

Synopsis

overload array_exch_at with array_exch_at_gint of 0

overload array_exch_at with array_exch_at_guint of 0

array_exch_at_gint

Synopsis

fun{
a:vt0p}{tk:tk
} array_exch_at_gint{n:int}
(
  A: &(@[INV(a)][n]), i: g1intLt (tk, n), x: &a >> _
) :<!wrt> void

Description

This function exchanges the value in array-cell i of the given array A and the value in its second argument. Note that the type of these values can be linear.

array_exch_at_guint

Synopsis

fun{
a:vt0p}{tk:tk
} array_exch_at_guint{n:int}
(
  A: &(@[INV(a)][n]), i: g1uintLt (tk, n), x: &a >> _
) :<!wrt> void

Description

This function, which is like array_exch_at_gint except that the index is unsigned.

array_interchange

Synopsis

fun
{a:vt0p}
array_interchange
  {n:int}
(
  A: &(@[INV(a)][n]), i: sizeLt (n), j: sizeLt (n)
) :<!wrt> void // end of [array_interchange]

Description

Given an array and two valid indices i and j, this function interchanges the values in array-cell i and array-cell j. Note that the type of these values can be linear.

Example

The following code implements the standard insertion sort:

fn{a:t0p}
insertion_sort
  {n:int} (
  A: &(@[a][n]), n: size_t n
) :<!wrt> void = let
//
fun loop1
  {i:nat | i < n} .<i>.
(
  A: &(@[a][n]), i: size_t i
) :<!wrt> void =
  if i > 0 then let
    val i1 = pred (i)
    val sgn = gcompare_ref<a> (A.[i1], A.[i])
  in
    if sgn > 0 then
    (
      array_interchange (A, i1, i); loop1 (A, i1)
    ) // end of [if]
  end else () // end of [if]
//
fun loop2
  {i:nat | i <= n} .<n-i>.
(
  A: &(@[a][n]), n: size_t n, i: size_t i
) :<!wrt> void =
  if i < n then (loop1 (A, i); loop2 (A, n, succ(i)))
//
in
//
  if n >= 2 then loop2 (A, n, g1i2u(1)) else ((*exit*))
//
end // end of [insertion_sort]

array_subcirculate

Synopsis

fun
{a:vt0p}
array_subcirculate
  {n:int}
(
  A: &(@[INV(a)][n]), i: sizeLt (n), j: sizeLt (n)
) :<!wrt> void // end of [array_subcirculate]

Description

Given an array A and two valid indices i and j, this function circulates the values stored in array-cells between cell i and cell j, inclusive. If i is less than j, then A[k] moves into A[k+1] for k ranging from i up to j-1 and A[j] moves into A[i]. If i is greater than j, then A[k] moves into A[k-1] for k ranging from i down to j+1, and A[j] moves into A[i].

array_ptr_alloc

Synopsis

fun
{a:vt0p}
array_ptr_alloc
  {n:int}
(
  asz: size_t n
) :<!wrt> [l:agz]
(
  array_v (a?, l, n), mfree_gc_v (l) | ptr l
) (* end of [array_ptr_alloc] *)

array_ptr_free

Synopsis

fun
{(*void*)}
array_ptr_free
  {a:vt0p}{l:addr}{n:int}
(
  array_v (a?, l, n), mfree_gc_v (l) | ptr l
) :<!wrt> void // end-of-function

array_ptr_tabulate

Synopsis

fun
{a:vt0p}
array_ptr_tabulate
  {n:int}
(
  asz: size_t(n)
) : [l:addr] (array_v(a, l, n), mfree_gc_v(l) | ptr(l))

array_tabulate$fopr

Synopsis

fun
{a:vt0p}
array_tabulate$fopr(i: size_t): (a)

fprint_array

Synopsis

overload fprint_array with fprint_array_int

overload fprint_array with fprint_array_size

Description

This function prints the elements in a given array to the output channel provided as its first argument, and it calls the function fprint_array$sep before printing an element as long as the element is not the first one. Note that printing each array element is handled by calling the function fprint_ref.

fprint_array$sep

Synopsis

fun
{(*void*)}
fprint_array$sep (out: FILEref): void

fprint_array_sep

Synopsis

fun
{a:vt0p}
fprint_array_sep{n:int}
(
  out: FILEref
, A: &RD(@[INV(a)][n]), n: size_t n, sep: NSH(string)
) : void // end of [fprint_array_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.

array_foreach

Synopsis

fun{
a:vt0p
} array_foreach{n:int}
(
  A: &(@[INV(a)][n]) >> @[a][n], asz: size_t(n)
) : sizeLte(n) // end of [array_foreach]

Description

This function traverses a given array from left to right, applying to each encountered array-cell the function implemented by array_foreach$fwork. The traversal stops if the function implemented by array_foreach$cont returns false, and the return value of array_foreach indicates the number of processed array-cells.

Example

The following code implements a function that searches for the index of the first array-cell in a given array that contains an element satisfing the predicate provided as the third argument of the function:

fun{a:t@ype}
array_find{n:int}
(
  A: &(@[a][n]) >> @[a][n], n: size_t n, p: (a) -> bool
) : Option_vt (sizeLt(n)) = let
//
implement(env)
array_foreach$cont<a><env> (x, env) = ~p(x)
implement(env)
array_foreach$fwork<a><env> (x, env) = ((*nothing*))
val i = array_foreach (A, n)
//
in
  if n > i then Some_vt (i) else None_vt ()
end // end of [array_find]

array_foreach_env

Synopsis

fun{
a:vt0p}{env:vt0p
} array_foreach_env{n:int}
(
  A: &(@[INV(a)][n]) >> @[a][n], asz: size_t(n), env: &(env) >> _
) : sizeLte(n) // end of [array_foreach_env]

Description

This function does essentially the same as array_foreach except for taking an additional argument that serves as an environment.

Example

The following code implements the standard fold-from-left operation on a given array:

fun{
a:t0p}{res:t0p
} array_foldleft{n:int}
(
  A: &(@[a][n])
, asz: size_t n, ini: res, f: (res, a) -> res
) : res = let
//
var env: res = ini
//
implement
array_foreach$fwork<a><res> (x, env) = env := f (env, x)
//
val _(*asz*) = array_foreach_env (A, asz, env)
//
in
  env
end // end of [array_foldleft]

array_foreach$cont

Synopsis

fun{
a:vt0p}{env:vt0p
} array_foreach$cont (x: &a, env: &env): bool

Description

The default implementation of this function always returns true.

array_foreach$fwork

Synopsis

fun{
a:vt0p}{env:vt0p
} array_foreach$fwork (x: &a >> _, env: &(env) >> _): void

array_foreach_funenv

Synopsis

fun
{a:vt0p}
array_foreach_funenv
  {v:view}
  {vt:vtype}
  {n:int}
  {fe:eff}
(
  pfv: !v
| A: &(@[INV(a)][n]) >> @[a][n]
, asz: size_t n
, f: (!v | &a >> _, !vt) -<fun,fe> void
, env: !vt
) :<fe> void

Description

This function is like array_foreach except that the function to be applied to each array-cell is provided as an argument.

array_foreach_fun

Synopsis

fun
{a:vt0p}
array_foreach_fun
  {n:int}{fe:eff}
(
  &(@[INV(a)][n]) >> @[a][n]
, size_t (n), (&a >> _) -<fun,fe> void
) :<fe> void // end of [array_foreach_fun]

Description

This function is a special case of array_foreach_funenv in that the provided function does not take an argument as its environment.

array_foreach2

Synopsis

fun{
a1,a2:vt0p
} array_foreach2
  {n:int}
(
  A1: &(@[INV(a1)][n]) >> @[a1][n]
, A2: &(@[INV(a2)][n]) >> @[a2][n]
, asz: size_t (n)
) : sizeLte(n) // end of [array_foreach2]

array_foreach2_env

Synopsis

fun{
a1,a2:vt0p}{env:vt0p
} array_foreach2_env
  {n:int}
(
  A1: &(@[INV(a1)][n]) >> @[a1][n]
, A2: &(@[INV(a2)][n]) >> @[a2][n]
, asz:size_t (n)
, env: &(env) >> env
) : sizeLte(n) // end of [array_foreach2_env]

array_foreach2$cont

Synopsis

fun{
a1,a2:vt0p}{env:vt0p
} array_foreach2$cont
  (x1: &a1, x2: &a2, env: &env): bool

Description

The default implementation of this function always returns true.

array_foreach2$fwork

Synopsis

fun{
a1,a2:vt0p}{env:vt0p
} array_foreach2$fwork
  (x1: &a1 >> _, x2: &a2 >> _, env: &(env) >> _): void

array_rforeach

Synopsis

fun{
a:vt0p
} array_rforeach{n:int}
(
  A: &(@[INV(a)][n]) >> @[a][n], asz: size_t(n)
) : sizeLte(n) // end of [array_rforeach]

Description

This function traverses a given array from right to left, applying to each encountered array-cell the function implemented by array_rforeach$fwork. The traversal stops is the function implemented by array_rforeach$cont returns false, and the return value of array_rforeach indicates the number of processed array-cells.

Example

The following code implements a function that searches for the index of the last array-cell in a given array that contains an element satisfing the predicate provided as the third argument of the function:

fun{a:t@ype}
array_rfind{n:int}
(
  A: &(@[a][n]) >> @[a][n], n: size_t n, p: (a) -> bool
) : Option_vt (sizeLt(n)) = let
//
implement(env)
array_rforeach$cont<a><env> (x, env) = ~p(x)
implement(env)
array_rforeach$fwork<a><env> (x, env) = ((*nothing*))
val i = array_rforeach (A, n)
//
in
  if n > i then Some_vt (pred(n)-i) else None_vt ()
end // end of [array_rfind]

array_rforeach_env

Synopsis

fun{
a:vt0p}{env:vt0p
} array_rforeach_env{n:int}
(
  A: &(@[INV(a)][n]) >> @[a][n], asz: size_t(n), env: &(env) >> _
) : sizeLte(n) // end of [array_rforeach_env]

Description

This function does essentially the same as array_rforeach except for taking an additional argument that serves as an environment.

Example

The following code implements the standard fold-from-right operation on a given array:

fun{
a:t0p}{res:t0p
} array_foldright{n:int}
(
  A: &(@[a][n])
, asz: size_t n, f: (a, res) -> res, snk: res
) : res = let
//
var env: res = snk
//
implement
array_rforeach$fwork<a><res>
  (x, env) = env := f (x, env)
//
val _(*asz*) = array_rforeach_env<a><env> (A, asz, env)
//
in
  env
end // end of [array_foldright]

Please note that array_rforeach_env is given a tail-recursive implementation in ATSLIB.

array_rforeach$cont

Synopsis

fun{
a:vt0p}{env:vt0p
} array_rforeach$cont(x: &a, env: &env): bool

Description

The default implementation of this function always returns true.

array_rforeach$fwork

Synopsis

fun{
a:vt0p}{env:vt0p
} array_rforeach$fwork(x: &a >> _, env: &(env) >> _): void

array_initize

Synopsis

fun{a:vt0p}
array_initize{n:int}
(
  A: &(@[a?][n]) >> @[a][n], asz: size_t(n)
) : void // end of [array_initize]

array_initize$init

Synopsis

fun{a:vt0p}
array_initize$init (i: size_t, x: &a? >> a): void

array_initize_elt

Synopsis

fun{a:t0p}
array_initize_elt{n:int}
(
  A: &(@[a?][n]) >> @[a][n], asz: size_t n, elt: (a)
) :<!wrt> void // end of [array_initize_elt]

array_initize_list

Synopsis

fun{a:t0p}
array_initize_list{n:int}
(
  A: &(@[a?][n]) >> @[a][n], asz: int n, xs: list(INV(a), n)
) :<!wrt> void // end of [array_initize_list]

array_initize_rlist

Synopsis

fun{a:t0p}
array_initize_rlist{n:int}
(
  A: &(@[a?][n]) >> @[a][n], asz: int n, xs: list(INV(a), n)
) :<!wrt> void // end of [array_initize_rlist]

array_initize_list_vt

Synopsis

fun{a:vt0p}
array_initize_list_vt{n:int}
(
  A: &(@[a?][n]) >> @[a][n], asz: int n, xs: list_vt(INV(a), n)
) :<!wrt> void // end of [array_initize_list_vt]

array_initize_rlist_vt

Synopsis

fun{a:vt0p}
array_initize_rlist_vt{n:int}
(
  A: &(@[a?][n]) >> @[a][n], asz: int n, xs: list_vt(INV(a), n)
) :<!wrt> void // end of [array_initize_rlist_vt]

array_uninitize

Synopsis

fun
{a:vt0p}
array_uninitize
  {n:int}
(
  A: &(@[INV(a)][n]) >> @[a?][n], asz: size_t n
) : void // end of [array_uninitize]

array_uninitize$clear

Synopsis

fun{a:vt0p}
array_uninitize$clear(i: size_t, x: &a >> a?): void

array_bsearch

Synopsis

fun
{a:vt0p}
array_bsearch
  {n:int}
  (A: &RD(@[a][n]), n: size_t(n)):<> sizeLte(n)

array_bsearch$ford

Synopsis

fun{a:vt0p}
array_bsearch$ford (x: &RD(a)):<> int

array_bsearch_stdlib

Synopsis

fun
{a:vt0p}
array_bsearch_stdlib
  {n:int}
(
  A: &RD(@[a][n]), asz: size_t (n), key: &RD(a), cmp: cmpref(a)
) :<> Ptr0 (* found/~found : ~null/null *)

Description

This function is a wrapper around the function bsearch declared in stdlib.h of libc.

array_quicksort

Synopsis

fun
{a:vt0p}
array_quicksort
  {n:int}
(
  A: &(@[INV(a)][n]) >> @[a][n], n: size_t n
) :<!wrt> void // end-of-function

array_quicksort$cmp

Synopsis

fun{a:vt0p}
array_quicksort$cmp(x1: &RD(a), x2: &RD(a)):<> int(*sgn*)

Description

This function is called in the implementation of array_quicksort to perform comparison test on array elements, and its default implementation is based on gcompare_ref:

implement{a}
array_quicksort$cmp (x, y) = gcompare_ref<a> (x, y)

array_quicksort_stdlib

Synopsis

fun
{a:vt0p}
array_quicksort_stdlib
  {n:int}
(
  A: &(@[INV(a)][n]) >> @[a][n], n: size_t(n), cmp: cmpref(a)
) :<!wrt> void // end of [array_quicksort_stdlib]

Description

This function is a wrapper around the function qsort declared in stdlib.h of libc.

array_mapto

Synopsis

fun{
a:vt0p}{b:vt0p
} array_mapto{n:int}
(
  A: &array(INV(a), n)
, B: &array(b?, n) >> array (b, n)
, n: size_t (n)
) : void // end of [array_mapto]

array_mapto$fwork

Synopsis

fun{
a:vt0p}{b:vt0p
} array_mapto$fwork(x: &a, y: &b? >> b): void

array_map2to

Synopsis

fun{
a,b:vt0p}{c:vt0p
} array_map2to{n:int}
(
  A: &array(INV(a), n)
, B: &array(INV(b), n)
, C: &array(c?, n) >> array (c, n)
, n: size_t (n)
) : void // end of [array_map2to]

array_map2to$fwork

Synopsis

fun{
a,b:vt0p}{c:vt0p
} array_map2to$fwork(x: &a, y: &b, z: &c? >> c): void

array_permute

Synopsis

fun{a:vt0p}
array_permute{n:int}
  (A: &(@[INV(a)][n]) >> @[a][n], n: size_t(n)): void

Description

This function permutes the contents of a given array according to the random number generator implemented by array_permute$randint.

Example

The following code creates an array of integers 1, 2, 3, 4, and 5, and then permutes the array contents to obtain an array of integers 5, 1, 2, 3, and 4:

implement
main0 () = {
//
#define N 5
val asz = g1i2u (N)
val out = stdout_ref
//
val (pf, pfgc | p) = array_ptr_alloc<int> (asz)
//
implement
array_initize$init<int> (i, x) = x := g0u2i(i)+1
val () = array_initize<int> (!p, asz) // array: 1, 2, ..., N-1, N
//
val (
) = fprint_array_sep (out, !p, asz, ",")
val () = fprint_newline (out)
//
implement
array_permute$randint<> (n) = pred(n) // this is not random
val () = array_permute<int> (!p, asz) // array: N, 1, 2, ..., N-1
//
val (
) = fprint_array_sep (out, !p, asz, ",")
val () = fprint_newline (out)
//
val () = array_ptr_free (pf, pfgc | p)
//
} // end of [main0]

Note that the created array is properly freed before the code exits.

array_permute$randint

Synopsis

fun{(*void*)}
array_permute$randint{n:int | n > 0}(size_t(n)): sizeLt(n)

Overloaded Symbols

[]

Synopsis

overload [] with array_get_at_gint of 0

overload [] with array_get_at_guint of 0

overload [] with array_set_at_gint of 0

overload [] with array_set_at_guint of 0

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