ATSLIB/libats/dynarray
This package implements dynamic arrays. Given a dynamic array DA, its size
is the current number of elements stored in DA, and its capacity is the
number of cells (either occupied or unoccupied) in DA. In contrast to an
array of fixed size, a dynamic array can grow its capacity at run-time when
there is no cell available for adding a new element.
Synopsis
vtypedef
dynarray(a:vt0p) = dynarray_vtype(a)
Synopsis
absvtype
dynarray_vtype(a:vt@ype+) = ptr
Synopsis
fun{}
dynarray$recapacitize (): int
Description
The value returned by this function determines whether the capacity of a
dynamic array is allowed to be expanded automatically if needed.
Synopsis
fun{a:vt0p}
dynarray_make_nil(cap: sizeGte(1)): dynarray(a)
Description
Given a size m, this function returns a dynamic array of capacity m and
size 0.
Synopsis
fun{}
dynarray_free
{a:t0p} (DA: dynarray(INV(a))):<!wrt> void
Synopsis
fun{}
dynarray_get_size
{a:vt0p}(DA: !RD(dynarray(INV(a)))): size_t
Description
This function returns the current size of a given dynamic array.
Synopsis
fun{}
dynarray_get_capacity
{a:vt0p}(DA: !RD(dynarray(INV(a)))): size_t
Description
This function returns the current capacity of a given dynamic array.
Synopsis
fun{}
dynarray_get_array{a:vt0p}
(
DA: !dynarray(INV(a)), n: &size_t? >> size_t(n)
) :<!wrt> #[l:addr;n:int]
(
array_v (a, l, n), array_v (a, l, n) -<lin,prf> void | ptr l
)
Description
Given a dynamic array DA, this function returns a pointer plus some
proofs of views for accessing the array contained in DA.
Synopsis
fun{}
dynarray_getfree_arrayptr
{a:vt0p}
(
DA: dynarray(INV(a)), n: &size_t? >> size_t(n)
) :<!wrt> #[n:nat] arrayptr (a, n)
Description
Given a dynamic array DA, this function returns the arrayptr-value inside
DA and then frees DA.
Synopsis
fun{a:vt0p}
dynarray_getref_at
(DA: !RD(dynarray(INV(a))), i: size_t):<> cPtr0(a)
Description
Given a dynamic array DA and an index i, this function returns the address
of cell i in DA if i is valid. Otherwise, it returns the null pointer.
Synopsis
fun{a:t0p}
dynarray_get_at_exn
(DA: !dynarray(INV(a)), i: size_t):<!exn> a
Description
Given a dynamic array DA and an index i, this function returns the content
of cell i in DA if i is valid. Otherwise, it raises an exception
(ArraySubscriptExn). Note that the type of the content is
non-linear.
Synopsis
fun{a:t0p}
dynarray_set_at_exn
(DA: !dynarray(INV(a)), i: size_t, x: a):<!exnwrt> void
Description
Given a dynamic array DA, an index i and a value x, this function updates
the content of cell i in DA with x if i is valid. Otherwise, it raises an
exception (ArraySubscriptExn). Note that the type of the
content is non-linear.
Synopsis
fun{a:vt0p}
dynarray_insert_at
(
DA: !dynarray(INV(a)), i: size_t, x: a, res: &a? >> opt(a, b)
) : #[b:bool] bool (b)
Description
Given a dynamic array DA, an index i and a value x, this function inserts x
into cell i in DA if i is valid, that is, i is less than or equal to the
current size of DA. Otherwise, there is no insertion. If insertion
happens, then false is returned. Otherwise, true is
returned. If DA is not allowed to reset its capacity, then insertion may
not happen even if the index i is valid. The time-complexity of this
function is O(n), where n is the current size of DA.
Synopsis
fun{a:vt0p}
dynarray_insert_at_opt
(DA: !dynarray(INV(a)), i: size_t, x: a): Option_vt(a)
Description
This function is the optional variant of dynarray_insert_at.
Synopsis
fun{a:vt0p}
dynarray_insert_atbeg_opt
(DA: !dynarray(INV(a)), x: a): Option_vt(a)
Description
This function is a special case of dynarray_insert_at_opt where
the index i equals 0.
Synopsis
fun{a:vt0p}
dynarray_insert_atend_opt
(DA: !dynarray(INV(a)), x: a): Option_vt(a)
Description
This function is a special case of dynarray_insert_at_opt where
the index i equals the current size of the dynamic array.
Synopsis
fun{a:vt0p}
dynarray_insertseq_at
{n2:int}
(
DA: !dynarray(INV(a)), i: size_t
, xs: &array(a, n2) >> arrayopt(a, n2, b), n2: size_t(n2)
) : #[b:bool] bool(b)
Description
This function is for inserting an array of elements into a given dynamic
array. If the operation is actually performed, then false is
returned. Otherwise, true is returned.
Synopsis
fun{a:vt0p}
dynarray_takeout_at
(
DA: !dynarray(INV(a)), i: size_t, res: &a? >> opt(a, b)
) : #[b:bool] bool(b)
Description
Given a dynamic array DA, an index i, this function takes out the content
of cell i in DA if i is valid, that is, it is less than the current size of
DA. If the content is taken out, then true is
returned. Otherwise, false is returned. The time-complexity of
this function is O(n), where n is the current size of DA.
Synopsis
fun{a:vt0p}
dynarray_takeout_at_opt
(DA: !dynarray(INV(a)), i: size_t): Option_vt(a)
Description
This function is the optional variant of dynarray_takeout_at.
Synopsis
fun{a:vt0p}
dynarray_takeout_atbeg_opt (DA: !dynarray(INV(a))): Option_vt(a)
Description
This function is a special case of dynarray_takeout_at_opt where
the index i equals 0.
Synopsis
fun{a:vt0p}
dynarray_takeout_atend_opt (DA: !dynarray(INV(a))): Option_vt(a)
Description
This function is a special case of dynarray_takeout_at_opt
where the index i equals the current size of DA minus 1.
Synopsis
fun{a:vt0p}
dynarray_takeoutseq_at
{n2:int}
(
DA: !dynarray(INV(a)), i: size_t
, xs: &array(a?, n2) >> arrayopt(a, n2, b), n2: size_t (n2)
) : #[b:bool] bool(b)
Description
This function is for taking out an array of elements from a given dynamic
array. If the operation is actually performed, then true is
returned. Otherwise, false is returned.
Synopsis
fun{a:t@ype}
dynarray_removeseq_at
(DA: !dynarray(INV(a)), st: size_t, ln: size_t):<!wrt> size_t
Description
Given a dynamic array DA and two sizes st and ln,
this function removes the segment in DA of length ln that starts at index
st. The return value of the function indicates the actual number of
elements removed.
Synopsis
fun{a:vt0p}
dynarray_reset_capacity
(DA: !dynarray(INV(a)), m2: sizeGte(1)):<!wrt> bool
Description
Given a dynamic array DA and a size m2, this function resets the capacity
of DA to m2 if m2 is great than or equal to the current size of DA. If the
capacity is reset, then true is returned. Otherwise,
false is returned.
Synopsis
fun{a:vt0p}
dynarray_quicksort (DA: !dynarray(INV(a))): void
Synopsis
fun{a:vt0p}
dynarray_quicksort$cmp
(x1: &RD(a), x2: &RD(a)):<> int
Description
This function is called in the implementation of
dynarray_quicksort to perform comparison test on array
elements, and its default implementation is based on
gcompare_ref:
staload "libats/SATS/dynarray.sats"
implement{a}
dynarray_quicksort$cmp (x, y) = gcompare_ref<a> (x, y)