ATSLIB/libats/fundeque_fngtree
This package implements a functional deque (double-ended queue) based on
the so-called finger-tree structure.
Synopsis
stadef deque = deque_type
typedef deque(a:t0p) = [n:int] deque(a, n)
Synopsis
abstype
deque_type
(elt:t@ype+, n:int) = ptr
Synopsis
typedef Deque(a:t0p) = [n:int] deque(a, n)
Synopsis
prfun
lemma_deque_param
{a:t0p}{n:int} (xs: deque(INV(a), n)): [n >= 0] void
Synopsis
fun{}
fundeque_nil{a:t0p} ():<> deque(a, 0)
Description
This function creates an empty deque.
Synopsis
fun
{a:t0p}
fundeque_cons{n:int}
(x: a, xs: deque(INV(a), n)):<> deque(a, n+1)
Description
This function adds an element to the front-end of a given deque.
Synopsis
fun
{a:t0p}
fundeque_uncons{n:pos}
(xs: &deque(INV(a), n) >> deque(a, n-1)):<!wrt> (a)
Description
This function does the opposite of what fundeque_cons does.
Synopsis
fun
{a:t0p}
fundeque_snoc{n:int}
(xs: deque(INV(a), n), x: a):<> deque(a, n+1)
Description
This function adds an element to the rear-end of a given deque.
Synopsis
fun
{a:t0p}
fundeque_unsnoc{n:pos}
(xs: &deque(INV(a), n) >> deque(a, n-1)):<!wrt> (a)
Description
This function does the opposite of what fundeque_unsnoc does.
Synopsis
fun{}
fundeque_is_nil
{a:t0p}{n:int}(xs: deque(INV(a), n)):<> bool(n==0)
Description
This function test whether a given dequen is empty.
Synopsis
fun{}
fundeque_is_cons
{a:t0p}{n:int}(xs: deque(INV(a), n)):<> bool(n > 0)
Description
This function test whether a given dequen is non-empty.
Synopsis
fun
{a:t0p}
fundeque_size
{n:int}(xs: deque(INV(a), n)):<> size_t(n)
Description
This function returns the number of elements contained in a given deque.
Synopsis
fun
{a:t0p}
fundeque_get_atbeg{n:pos}(xs: deque(INV(a), n)):<> (a)
Description
This function returns the first element of a given non-empty deque.
Synopsis
fun
{a:t0p}
fundeque_get_atend{n:pos}(xs: deque(INV(a), n)):<> (a)
Description
This function returns the last element of a given non-empty deque.
Synopsis
fun
{a:t0p}
fundeque_append
{n1,n2:int}
(deque(INV(a), n1), deque(a, n2)):<> deque(a, n1+n2)
Synopsis
fun{a:t0p}
fprint_fundeque
(out: FILEref, xs: Deque(INV(a))): void
Synopsis
fun{}
fprint_fundeque$sep(out: FILEref): void
Synopsis
fun
{a:t0p}
{env:vt0p}
fundeque_foreach$fwork(x: a, env: &env>>_): void
Synopsis
fun
{a:t0p}
fundeque_foreach(xs: Deque(INV(a))): void
Synopsis
fun
{a:t0p}
{env:vt0p}
fundeque_foreach_env(xs: Deque(INV(a)), env: &(env)>>_): void
Synopsis
fun
{a:t0p}
{env:vt0p}
fundeque_rforeach$fwork(x: a, env: &env>>_): void
Synopsis
fun
{a:t0p}
fundeque_rforeach(xs: Deque(INV(a))): void
Synopsis
fun
{a:t0p}
{env:vt0p}
fundeque_rforeach_env(xs: Deque(INV(a)), env: &(env)>>_): void