ATSLIB/libats/funralist_nested
This package implements 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_type
typedef ralist (a:t0p) = [n:int] ralist (a, n)
Synopsis
abstype
ralist_type (a:t@ype+, n:int) = ptr
Synopsis
typedef Ralist (a:t0p) = [n:int] ralist (a, n)
Synopsis
prfun lemma_ralist_param
{a:t0p}{n:int} (xs: ralist (INV(a), n)): [n >= 0] void
Synopsis
fun{}
funralist_nil{a:t0p}():<> ralist (a, 0)
Description
This function forms an empty list.
Synopsis
fun{a:t0p}
funralist_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:t0p}
funralist_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{
} funralist_is_nil
{a:t0p}{n:int} (xs: ralist (INV(a), n)):<> bool(n==0)
Description
This function tests whether a given list is empty.
Synopsis
fun{
} funralist_is_cons
{a:t0p}{n:int} (xs: ralist (INV(a), n)):<> bool(n > 0)
Description
This function tests whether a given list is non-empty.
Synopsis
fun{
} funralist_length
{a:t0p}{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}
funralist_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}
funralist_tail
{n:pos} (xs: ralist (INV(a), n)):<> ralist (a, n-1)
Description
This function returns the tail of a given non-empty list.
Synopsis
fun{a:t0p}
funralist_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}
funralist_lookup{n:int}
(xs: ralist (INV(a), n), i: natLt n):<> a
Description
This function is an alias of funralist_get_at.
Synopsis
fun{a:t0p}
funralist_set_at{n:int}
(
xs: ralist (INV(a), n), i: natLt n, x0: a
) :<> ralist (a, n)
Description
Given a list xs of length n, a natural number i less than n and an element
x0, this function returns a list obtained from replacing element i in xs
with x0. The time-complexity of the function is O(log(i)).
Synopsis
fun{a:t0p}
funralist_update{n:int}
(
xs: ralist (INV(a), n), i: natLt n, x0: a
) :<> ralist (a, n)
Description
This function is an alias of funralist_set_at.
Synopsis
Synopsis for [funralist_foreach$cont] is unavailable.
Synopsis
fun{a:t0p}{env:vt0p}
funralist_foreach$fwork (x: a, env: &(env) >> _): void
Synopsis
fun{a:t0p}
funralist_foreach (xs: Ralist (INV(a))): void
Synopsis
fun{a:t0p}{env:vt0p}
funralist_foreach_env (xs: Ralist (INV(a)), env: &(env)>>env): void
Synopsis
fun{a:t0p}
funralist_listize
{n:int} (xs: ralist (INV(a), n)):<!wrt> list_vt (a, n)