ATSLIB/libats/lindeque_dllist
This package implements linear deques (double-ended queues) based on the
circular doubly-linked list structure.
Synopsis
stadef deque = deque_vtype
vtypedef deque (a:vt0p, n:int) = deque_vtype (a, n)
Description
The type constructor deque is a shorthand for
deque_vtype.
Synopsis
absvtype
deque_vtype (a:vt@ype+, n:int) = ptr
Description
Given a type T and an integer N, the abstract viewtype
deque_vtype(K, T) is for a deque storing N elements of the type
T. Note that deque_vtype is co-variant in its first argument.
Synopsis
fun{} lindeque_nil{a:vt0p} ():<> deque (a, 0)
Description
This function creates an empty deque.
Synopsis
fun{} lindeque_is_nil
{a:vt0p}{n:int} (dq: !deque (INV(a), n)):<> bool (n==0)
Description
This function tests whether a given deque is empty.
Synopsis
fun{} lindeque_isnot_nil
{a:vt0p}{n:int} (dq: !deque (INV(a), n)):<> bool (n > 0)
Description
This function tests whether a given deque is non-empty.
Synopsis
fun{a:vt0p}
lindeque_length {n:int} (dq: !deque (INV(a), n)):<> int (n)
Description
This function computes the length of a given deque,
Synopsis
fun{a:vt0p}
lindeque_insert_atbeg{n:int}
(dq: &deque (INV(a), n) >> deque (a, n+1), x: a): void
Description
This function inserts an element at the beginning of a given deque.
Synopsis
fun{a:vt0p}
lindeque_insert_atend{n:int}
(dq: &deque (INV(a), n) >> deque (a, n+1), x: a): void
Description
This function inserts an element at the end of a given deque.
Synopsis
fun{a:vt0p}
lindeque_takeout_atbeg{n:pos}
(dq: &deque (INV(a), n) >> deque (a, n-1)): (a)
Description
This function takes out the element at the beginning of a given deque.
Synopsis
fun{a:vt0p}
lindeque_takeout_atend{n:pos}
(dq: &deque (INV(a), n) >> deque (a, n-1)): (a)
Description
This function takes out the element at the end of a given deque.
Synopsis
fun{a:vt0p}
lindeque2dllist{n:int} (dq: deque (INV(a), n)):<!wrt> dllist (a, 0, n)
Description
This function turns a given deque into a doubly-linked list. Note that it
is a specific function for this particular dllist-based implementation of
deques.