ATSLIB/libats/gflist_vt
This package contains various functions for manipulating generic linear
lists that are assigned the fully indexed list type.
Synopsis
fun{a:vt0p}
gflist_vt_length
{xs:ilist}
(xs: !gflist_vt (INV(a), xs)):<> [n:nat] (LENGTH (xs, n) | int n)
Description
This function computes the length of a given list.
Synopsis
fun{a:vt0p}
gflist_vt_append
{xs1,xs2:ilist}
(
xs1: gflist_vt (INV(a), xs1), xs2: gflist_vt (a, xs2)
) :<!wrt> [res:ilist] (APPEND (xs1, xs2, res) | gflist_vt (a, res))
Description
Given two lists xs1 and xs2, this function returns a list that is the
concatenation of xs1 and xs2. Note that there is no involvement of memory
allocation/deallocation in the implementation of
gflist_vt_append.
Synopsis
fun{a:vt0p}
gflist_vt_revapp
{xs1,xs2:ilist}
(
xs1: gflist_vt (INV(a), xs1), xs2: gflist_vt (a, xs2)
) :<!wrt> [res:ilist] (REVAPP (xs1, xs2, res) | gflist_vt (a, res))
Description
Given two lists xs1 and xs2, this function returns a list that is the
concatenation of rxs1 and xs2, where rxs1 is the reverse of xs1. Note that
there is no involvement of memory allocation/deallocation in the
implementation of gflist_vt_revapp.
Synopsis
fun{a:vt0p}
gflist_vt_reverse
{xs:ilist} (
xs: gflist_vt (INV(a), xs)
) :<!wrt> [ys:ilist] (REVERSE (xs, ys) | gflist_vt (a, ys))
Description
This function reverses a given list. It is just a special case of
gflist_vt_revapp where the first argument is taken to be empty.
Synopsis
fun{a:vt0p}
gflist_vt_mergesort
{xs:ilist}
(
xs: gflist_vt (INV(a), xs)
) : [ys:ilist] (SORT (xs, ys) | gflist_vt (a, ys))
Description
This function applies mergesort to a given list. Note that there is no
involvement of memory allocation/deallocation in the implementation of
gflist_vt_mergesort and the returned list is constructed
precisely of the nodes in the original given list.
Synopsis
fun{a:vt0p}
gflist_vt_mergesort$cmp
{x1,x2:int}
(x1: &stamped_vt (a, x1), x2: &stamped_vt (a, x2)): int(sgn(x1-x2))
Description
This function is employed by gflist_vt_mergesort for comparing
elements in a given list during sorting.