ATSLIB/libats/gflist
This package contains various functions for manipulating generic functional
lists that are assigned the fully indexed list type.
Synopsis
datatype
gflist (
a:t@ype+, ilist
) =
| gflist_nil
(a, ilist_nil) of ()
| {x:int}
{xs:ilist}
gflist_cons
(a, ilist_cons (x, xs)) of (stamped_t (a, x), gflist (a, xs))
Synopsis
datavtype
gflist_vt (
a:vt@ype+, ilist
) =
| gflist_vt_nil
(a, ilist_nil) of ()
| {x:int}
{xs:ilist}
gflist_vt_cons
(a, ilist_cons (x, xs)) of (stamped_vt (a, x), gflist_vt (a, xs))
Synopsis
fun{a:t0p}
gflist_length
{xs:ilist}
(
xs: gflist(INV(a), xs)
) :<> [n:nat] (LENGTH (xs, n) | int n)
Description
Given a list, this function returns a proof and an integer such that the
proof attests to the integer being the length of the list.
Synopsis
fun{a:t0p}
gflist_append
{xs1,xs2:ilist}
(
xs1: gflist (INV(a), xs1), xs2: gflist (a, xs2)
) :<> [res:ilist] (APPEND (xs1, xs2, res) | gflist (a, res))
Description
Given two lists xs1 and xs2, this function returns a proof and a list res
such that the proof attests to res being the result of appending xs1 to
xs2. The implementation given for gflist_append is
tail-recursive.
Synopsis
fun{a:t0p}
gflist_revapp
{xs1,xs2:ilist}
(
xs1: gflist (INV(a), xs1), xs2: gflist (a, xs2)
) :<> [res:ilist] (REVAPP (xs1, xs2, res) | gflist (a, res))
Description
Given two lists xs1 and xs2, this function returns a proof and a list res
such that the proof attests to res being the result of appending the reverse of
xs1 to xs2.
Synopsis
fun{a:t0p}
gflist_reverse
{xs:ilist}
(
xs: gflist (INV(a), xs)
) :<> [ys:ilist] (REVERSE (xs, ys) | gflist_vt (a, ys))
Description
Given a list xs, this function returns a proof and another list ys such
that the proof attests to ys being the reverse of xs.
Synopsis
fun{a:t0p}
gflist_mergesort
{xs:ilist}
(
xs: gflist (INV(a), xs)
) : [ys:ilist] (SORT (xs, ys) | gflist_vt (a, ys))
Description
Given a list xs, this function returns a proof and another list ys such
that the proof attests to ys being an ordered permutation of xs.
Synopsis
fun{a:t0p}
gflist_mergesort$cmp
{x1,x2:int}
(x1: stamped_t (a, x1), x2: stamped_t (a, x2)): int(sgn(x1-x2))
Description
This function is employed by gflist_mergesort for comparing
elements in a given list during sorting.