ATSLIB/libats/linralist_nested
This package implements linear random-access lists based on an interesting
structure due to Chris Okasaki. Unlike Okasaki's original formulation,
which involves a nested datatype, the formulation of the structure in ATS
makes only use of regular datatypes. This package is largely for
educational purpose, demonstrating a convincing case of employing dependent
types in practical programming.
Synopsis
stadef ralist = ralist_vtype
vtypedef ralist (a:vt0p) = [n:int] ralist (a, n)
Synopsis
absvtype
ralist_vtype (a:vt@ype+, n:int)
Synopsis
vtypedef Ralist (a:vt0p) = [n:int] ralist (a, n)
Synopsis
prfun lemma_ralist_param
{a:vt0p}{n:int} (xs: !ralist (INV(a), n)): [n >= 0] void
Synopsis
fun{}
linralist_nil{a:vt0p}():<> ralist (a, 0)
Description
This function forms an empty list.
Synopsis
fun{a:vt0p}
linralist_cons {n:int}
(x: a, xs: ralist (INV(a), n)):<> ralist (a, n+1)
Description
Given x and xs, this function forms a list whose head and tail are x ans
xs, respectively.
Synopsis
fun{a:vt0p}
linralist_uncons {n:pos}
(xs: &ralist (INV(a), n) >> ralist (a, n-1)):<!wrt> a
Description
Given a non-empty list, this function returns the head of the list while
storing the tail of the list into its (call-by-reference) argument.
Synopsis
fun{}
linralist_is_nil{a:vt0p}
{n:int} (xs: !ralist (INV(a), n)):<> bool(n==0)
Description
This function tests whether a given list is empty.
Synopsis
fun{}
linralist_is_cons{a:vt0p}
{n:int} (xs: !ralist (INV(a), n)):<> bool(n > 0)
Description
This function tests whether a given list is non-empty.
Synopsis
fun
linralist_length{a:vt0p}
{n:nat} (xs: !ralist (INV(a), n)):<> int (n)
Description
This function returns the length of a given list. Its time-complexity is
O(log(n)).
Synopsis
fun{a:t0p}
linralist_head
{n:pos} (xs: !ralist (INV(a), n)):<> a
Description
This function returns the head of a given non-empty list.
Synopsis
fun{a:t0p}
linralist_tail
{n:pos} (xs: ralist (INV(a), n)):<!wrt> ralist (a, n-1)
Description
This function returns the tail of a given non-empty list.
Synopsis
fun{a:vt0p}
linralist_getref_at{n:int}
(xs: !ralist (INV(a), n), i: natLt n):<> cPtr1 (a)
Synopsis
fun{a:t0p}
linralist_get_at{n:int}
(xs: !ralist (INV(a), n), i: natLt n):<> a
Description
Given a list xs of length n and a natural number i less than n, this
function returns xs[i], that is, element i in the list xs. The
time-complexity of the function is O(log(i)).
Synopsis
fun{a:t0p}
linralist_set_at{n:int}
(xs: !ralist (INV(a), n), i: natLt n, x: a):<!wrt> void
Description
Given a list xs of length n, a natural number i less than n and an element
x0, this function replaces element i in xs with x0. The time-complexity of
the function is O(log(i)).
Synopsis
fun{a:t0p}
linralist_listize
{n:int} (xs: !ralist (INV(a), n)):<!wrt> list_vt (a, n)
Synopsis
fun{a:vt0p}
linralist_listize_free
{n:int} (xs: ralist (INV(a), n)):<!wrt> list_vt (a, n)