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
  • lemma_array_param
  • lemma_array_v_param
  • array_v_nil
  • array_v_unnil
  • array_v_unnil_nil
  • array_v_cons
  • array_v_uncons
  • array_v_sing
  • array_v_unsing
  • array_getref_at
  • array_get_at
  • array_get_at_gint
  • array_get_at_guint
  • array_set_at
  • array_set_at_gint
  • array_set_at_guint
  • array_exch_at
  • array_exch_at_gint
  • array_exch_at_guint
  • array_interchange
  • array_subcirculate
  • array_ptr_alloc
  • array_ptr_free
  • array_ptr_tabulate
  • array_tabulate$fopr
  • fprint_array
  • fprint_array$sep
  • fprint_array_sep
  • array_foreach
  • array_foreach_env
  • array_foreach$cont
  • array_foreach$fwork
  • array_foreach_funenv
  • array_foreach_fun
  • array_foreach2
  • array_foreach2_env
  • array_foreach2$cont
  • array_foreach2$fwork
  • array_rforeach
  • array_rforeach_env
  • array_rforeach$cont
  • array_rforeach$fwork
  • array_initize
  • array_initize$init
  • array_initize_elt
  • array_initize_list
  • array_initize_rlist
  • array_initize_list_vt
  • array_initize_rlist_vt
  • array_uninitize
  • array_uninitize$clear
  • array_bsearch
  • array_bsearch$ford
  • array_bsearch_stdlib
  • array_quicksort
  • array_quicksort$cmp
  • array_quicksort_stdlib
  • array_mapto
  • array_mapto$fwork
  • array_map2to
  • array_map2to$fwork
  • array_permute
  • 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{}
    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{}
    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{}
    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. SourceForge.net Logo