ATSLIB/prelude/arrayptr

This package contains some common functions for creating/freeing and manipulating arrayptr-values.

  • arrayptr
  • arrayptr_vt0ype_addr_int_vtype
  • arrayptrout
  • arrayptrout_vt0ype_addr_int_vtype
  • arrayptr_encode
  • arrayptr2ptr
  • arrayptrout2ptr
  • arrayptr_takeout
  • arrayptr_addback
  • arrayptr_make_elt
  • arrayptr_make_intrange
  • arrayptr_make_arrpsz
  • arrayptr_make_list
  • arrayptr_make_rlist
  • arrayptr_make_subarray
  • arrayptr_make_list_vt
  • arrayptr_make_uninitized
  • arrayptr_imake_list
  • arrayptr_free
  • arrayptr_get_at
  • arrayptr_get_at_gint
  • arrayptr_get_at_guint
  • arrayptr_set_at
  • arrayptr_set_at_gint
  • arrayptr_set_at_guint
  • arrayptr_exch_at
  • arrayptr_exch_at_gint
  • arrayptr_exch_at_guint
  • fprint_arrayptr
  • fprint_arrayptr_sep
  • arrayptr_foreach
  • arrayptr_foreach_env
  • arrayptr_foreach_funenv
  • arrayptr_foreach_fun
  • arrayptr_rforeach
  • arrayptr_rforeach_env
  • arrayptr_initize
  • arrayptr_uninitize
  • arrayptr_freelin
  • arrayptr_tabulate
  • Overloaded Symbols
  • []
  • ptrcast
  • free
  • fprint
    •

    arrayptr

    Synopsis

    stadef
arrayptr = arrayptr_vt0ype_addr_int_vtype
    vtypedef
arrayptr
  (a:vt0p, n:int) = [l:addr] arrayptr(a, l, n)
    overload arrayptr with arrayptr_make_arrpsz

    Description

    Given a type T, an address L and an integer N, the type arrayptr(T, L, N) is for a linear array located at L that stores N elements of the type T.

    arrayptr_vt0ype_addr_int_vtype

    Synopsis

    absvtype
arrayptr_vt0ype_addr_int_vtype
  (a:vt0ype+, l: addr, n: int) = ptr(l)

    arrayptrout

    Synopsis

    stadef
arrayptrout = arrayptrout_vt0ype_addr_int_vtype

    Description

    Given a type T, an address L and an integer N, the type arrayptrout(T, L, N) essentially means arrayptr(T, L, N) minus the array-view array_v(T, L, N).

    arrayptrout_vt0ype_addr_int_vtype

    Synopsis

    absvtype
arrayptrout_vt0ype_addr_int_vtype
  (a:t@ype, l: addr, n: int) = ptr(l)

    arrayptr_encode

    Synopsis

    castfn
arrayptr_encode :
  {a:vt0p}{l:addr}{n:int}
  (array_v(INV(a), l, n), mfree_gc_v(l) | ptr(l)) -<0> arrayptr(a, l, n)

    arrayptr2ptr

    Synopsis

    castfn
arrayptr2ptr
  {a:vt0p}
  {l:addr}{n:int}
  (A: !arrayptr(INV(a), l, n)):<> ptr(l)

    arrayptrout2ptr

    Synopsis

    castfn
arrayptrout2ptr
  {a:t0p}{l:addr}{n:int}
  (A: !arrayptrout(INV(a), l, n)):<> ptr(l)

    arrayptr_takeout

    Synopsis

    praxi
arrayptr_takeout
  {a:vt0p}{l:addr}{n:int}
(
  A: !arrayptr(INV(a), l, n) >> arrayptrout(a?, l, n)
) : array_v(a, l, n) // end of [arrayptr_takeout]

    arrayptr_addback

    Synopsis

    praxi
arrayptr_addback
  {a:vt0p}{l:addr}{n:int}
(
  pf: array_v(INV(a), l, n) | A: !arrayptrout(a?, l, n) >> arrayptr(a, l, n)
) : void // end of [arrayptr_addback]

    arrayptr_make_elt

    Synopsis

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

    Description

    This function creates an arrayptr-value of a given size (first argument) and then initializes it with a given value (second argument) of some non-linear type.

    arrayptr_make_intrange

    Synopsis

    fun{}
arrayptr_make_intrange
  {l,r:int | l <= r}
  (l: int l, r: int r):<!wrt> arrayptr(intBtw(l, r), r-l)

    Description

    This function creates an arrayptr-value of size r-l that contains the integers from l until r-1, inclusive.

    arrayptr_make_arrpsz

    Synopsis

    fun
arrayptr_make_arrpsz
  {a:vt0p}{n:int}
  (psz: arrpsz(INV(a), n)):<> arrayptr(a, n) = "mac#%"

    Description

    This function, which overloads the symbol arrayptr, turns an arrpsz-value (arrayptr-with-size) into an arrayptr-value. It can be conveniently called to build an array of fixed size.

    Example

    The following code builds an array of digits, prints them out and then frees the array: 
    implement
main () = 0 where {
  val out = stdout_ref
  val A = (arrayptr)$arrpsz{int} (0, 1, 2, 3, 4, 5, 6, 7, 8, 9)
  val () = fprint_arrayptr_sep<int> (out, A, g1int2uint(10), ", ")
  val () = arrayptr_free (A)
  val () = fprint_newline (out)
} // end of [main]

    arrayptr_make_list

    Synopsis

    fun
{a:t0p}
arrayptr_make_list{n:int}
  (asz: int n, xs: list(INV(a), n)):<!wrt> arrayptr(a, n)

    Description

    This function creates an arrayptr-value of a given size n (first argument) and then initializes it with a given list (second argument) of length n.

    arrayptr_make_rlist

    Synopsis

    fun
{a:t0p}
arrayptr_make_rlist{n:int}
  (asz: int n, xs: list(INV(a), n)):<!wrt> arrayptr(a, n)

    Description

    This function creates an arrayptr-value of a given size n (first argument) and then initializes it with the reverse of a given list (second argument) of length n.

    arrayptr_make_subarray

    Synopsis

    fun{a:t0p}
arrayptr_make_subarray
  {n:int}{st,ln:int | st+ln <= n}
  (A: RD(arrayref(a, n)), size_t(st), size_t(ln)): arrayptr(a, ln)

    Description

    Given a non-linear array A of size n and two non-negative integers st and ln satisfying st+ln <= n, this function returns a linear array A2 of size ln such that the value in each A2[i] equals the value in A[st+i], where i ranges from 0 until ln-1, inclusive.

    arrayptr_make_list_vt

    Synopsis

    fun
{a:vt0p}
arrayptr_make_list_vt{n:int}
  (asz: int n, xs: list_vt (INV(a), n)):<!wrt> arrayptr(a, n)

    Description

    This function creates an arrayptr-value of a given size n (first argument) and then initializes it with the reverse of a given linear list (second argument) of length n. Note that the linear list is consumed after the function returns.

    arrayptr_make_uninitized

    Synopsis

    fun
{a:vt0p}
arrayptr_make_uninitized
  {n:int} (asz: size_t(n)):<!wrt> arrayptr(a?, n)

    Description

    This function creates an uninitialized arrayptr-value of a given size.

    arrayptr_imake_list

    Synopsis

    fun
{a:vt0p}
arrayptr_imake_list{n:int}
(
  A: !arrayptr(INV(a), n) >> arrayptr(a?!, n), n: size_t(n)
) : list_vt (a, n) // end of [arrayptr_imake_list]

    Description

    This function copies out the elements in a given arrayptr-value to form a linear list. In the case where the elements are linear, the array becomes uninitialized after the function returns. Note that the name imake is a shorthand for inverse-make in the sense that the function may alternatively be named list_make_arrayptr.

    arrayptr_free

    Synopsis

    fun
arrayptr_free
  {a:t0p}{l:addr}{n:int}
  (A: arrayptr(INV(a), l, n)):<!wrt> void = "mac#%"

    Description

    This function, which overloads the symbol free, frees the memory occupied by a given arrayptr-value that contains only non-linear elements. If there are linear elements involved, please try to use the function arrayptr_freelin.

    arrayptr_get_at

    Synopsis

    overload arrayptr_get_at with arrayptr_get_at_gint
    overload arrayptr_get_at with arrayptr_get_at_guint

    arrayptr_get_at_gint

    Synopsis

    fun{
a:t0p}{tk:tk
} arrayptr_get_at_gint
  {n:int}{i:nat | i < n}
  (A: !arrayptr(INV(a), n), i: g1int (tk, i)):<> (a)

    Description

    This function reads out the non-linear value stored at cell i of the array associated with its first argument.

    arrayptr_get_at_guint

    Synopsis

    fun{
a:t0p}{tk:tk
} arrayptr_get_at_guint
  {n:int}{i:nat | i < n}
  (A: !arrayptr(INV(a), n), i: g1uint (tk, i)):<> (a)

    Description

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

    arrayptr_set_at

    Synopsis

    overload arrayptr_set_at with arrayptr_set_at_gint of 0
    overload arrayptr_set_at with arrayptr_set_at_guint of 0

    arrayptr_set_at_gint

    Synopsis

    fun{
a:t0p}{tk:tk
} arrayptr_set_at_gint
  {n:int}{i:nat | i < n}
  (A: !arrayptr(INV(a), n), i: g1int (tk, i), x: a):<!wrt> void

    Description

    This function writes a non-linear value x to cell i of the array associated with its first argument.

    arrayptr_set_at_guint

    Synopsis

    fun{
a:t0p}{tk:tk
} arrayptr_set_at_guint
  {n:int}{i:nat | i < n}
  (A: !arrayptr(INV(a), n), i: g1uint (tk, i), x: a):<!wrt> void

    Description

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

    arrayptr_exch_at

    Synopsis

    overload arrayptr_exch_at with arrayptr_exch_at_gint of 0
    overload arrayptr_exch_at with arrayptr_exch_at_guint of 0

    arrayptr_exch_at_gint

    Synopsis

    fun{
a:vt0p}{tk:tk
} arrayptr_exch_at_gint
  {n:int}{i:nat | i < n}
  (A: !arrayptr(INV(a), n), i: g1int (tk, i), x: &a >> _):<!wrt> void

    Description

    This function exchanges the content of cell i of the array associated with its first argument and that of the variable x (its third argument). Note that the type for these contents can be linear.

    arrayptr_exch_at_guint

    Synopsis

    fun{
a:vt0p}{tk:tk
} arrayptr_exch_at_guint
  {n:int}{i:nat | i < n}
  (A: !arrayptr(INV(a), n), i: g1uint (tk, i), x: &a >> _):<!wrt> void

    Description

    This function is like arrayptr_exch_at_gint except that the index is unsigned.

    fprint_arrayptr

    Synopsis

    fun{a:vt0p}
fprint_arrayptr
  {l:addr}{n:int}
(
  out: FILEref, A: !arrayptr(INV(a), l, n), n: size_t(n)
) : void // end of [fprint_arrayptr]

    fprint_arrayptr_sep

    Synopsis

    fun{a:vt0p}
fprint_arrayptr_sep
  {l:addr}{n:int}
(
  out: FILEref
, A: !arrayptr(INV(a), l, n), n: size_t(n), sep: NSH(string)
) : void // end of [fprint_arrayptr_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.

    arrayptr_foreach

    Synopsis

    fun{
a:vt0p
} arrayptr_foreach{n:int}
(
  A: !arrayptr(INV(a), n), asz: size_t(n)
) : sizeLte(n) // end of [arrayptr_foreach]

    Description

    This function traverses the array associated with a given arrayptr-value from left to right, applying the function implemented by arrayptr_foreach$fwork to each cell in the array.

    arrayptr_foreach_env

    Synopsis

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

    Description

    This function does essentially the same as arrayptr_foreach except for taking an additional argument that serves as an environment (for recording changes).

    Example

    The following code creates an array of integers, computes the sum of the integers in the created array and then frees it. 
    implement
main () = let
//
val N = 10
val asz = g1int2uint (N)
val A = arrayptr_make_intrange (0, N)
//
typedef a = int
typedef tenv = int
var ans: tenv = 0
implement
array_foreach$fwork<a><tenv> (x, env) = env := env + x
val _(*ignored*) = arrayptr_foreach_env<a><tenv> (A, asz, ans)
//
val () = arrayptr_free (A)
//
val () = assertloc (ans = N*(N-1)/2)
//
in
  0(*normal*)
end // end of [main]

    arrayptr_foreach_funenv

    Synopsis

    fun
{a:vt0p}
arrayptr_foreach_funenv
  {v:view}
  {vt:vtype}
  {n:int}
  {fe:eff}
(
  pfv: !v
| A: !arrayptr(INV(a), n)
, asz: size_t(n)
, fop: (!v | &a, !vt) -<fun,fe> void
, env: !vt
) :<fe> void

    Description

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

    arrayptr_foreach_fun

    Synopsis

    fun
{a:vt0p}
arrayptr_foreach_fun
  {n:int}{fe:eff}
(
  A: !arrayptr(INV(a), n), asz: size_t(n), fwork: (&a) -<fun,fe> void
) :<fe> void // end of [arrayptr_foreach_fun]

    Description

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

    arrayptr_rforeach

    Synopsis

    fun{
a:vt0p
} arrayptr_rforeach{n:int}
(
  A: !arrayptr(INV(a), n), asz: size_t(n)
) : sizeLte(n) // end of [arrayptr_rforeach]

    arrayptr_rforeach_env

    Synopsis

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

    Description

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

    arrayptr_initize

    Synopsis

    fun{a:vt0p}
arrayptr_initize
  {l:addr}{n:int}
(
  A: !arrayptr(a?, l, n) >> arrayptr(a, l, n), asz: size_t(n)
) : void // end of [arrayptr_initize]

    arrayptr_uninitize

    Synopsis

    fun{a:vt0p}
arrayptr_uninitize
  {l:addr}{n:int}
(
  A: !arrayptr(INV(a), l, n) >> arrayptr(a?, l, n), asz: size_t(n)
) : void // end of [arrayptr_uninitize]

    arrayptr_freelin

    Synopsis

    fun{a:vt0p}
arrayptr_freelin
  {l:addr}{n:int}
  (A: arrayptr(INV(a), l, n), asz: size_t(n)): void

    Description

    This function first uninitializes a given arrayptr-value and then frees the memory occupied by it. In other words, arrayptr_freelin combines arrayptr_uninitize with arrayptr_free.

    arrayptr_tabulate

    Synopsis

    fun{a:vt0p}
arrayptr_tabulate
  {n:int} (asz: size_t(n)): arrayptr(a, n)

    Description

    Given a non-negative integer n, this function returns a linear array A of size n such that A is initialized from left to right by storing into A[i] the value returned from a call to array_tabulate$fopr on i, where i ranges from 0 until n-1, inclusive.

    Overloaded Symbols

    []

    Synopsis

    overload [] with arrayptr_get_at_gint of 0
    overload [] with arrayptr_set_at_gint of 0
    overload [] with arrayptr_get_at_guint of 0
    overload [] with arrayptr_set_at_guint of 0

    ptrcast

    Synopsis

    overload ptrcast with arrayptr2ptr
    overload ptrcast with arrayptrout2ptr

    free

    Synopsis

    overload free with arrayptr_free

    fprint

    Synopsis

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