ATSLIB/libats/qlist

This package implements linear queues based on the singly-linked list structure. Such queues, often referred to as qlist-objects, can be employed to accumulate items that need to be returned in a list in which the items appear in the same order as they are accumulated.

qlist

qlist_vtype

qlist0

qlist

Synopsis

vtypedef
qlist(a:vt0p, n:int) = qlist_vtype(a, n)

vtypedef
qlist(a:vt0p) = [n:int] qlist_vtype(a, n)

qlist_vtype

Synopsis

absvtype
qlist_vtype(a:vt@ype+, n:int) = ptr

qlist0

Synopsis

vtypedef
qlist0(a:vt0p) = [n:int | n >= 0] qlist(a, n)

qlist1

Synopsis

Synopsis for [qlist1] is unavailable.

qlist_make_nil

Synopsis

fun{}
qlist_make_nil{a:vt0p}():<!wrt> qlist(a, 0)

qlist_free_nil

Synopsis

fun{}
qlist_free_nil{a:vt0p}(qlist(a, 0)):<!wrt> void

qlist_is_nil

Synopsis

fun{a:vt0p}
qlist_is_nil
  {n:int} (q0: !qlist(a, n)):<> bool (n == 0)

Description

This function tests whether a given queue is empty.

qlist_isnot_nil

Synopsis

fun{a:vt0p}
qlist_isnot_nil
  {n:int} (q0: !qlist(INV(a), n)):<> bool (n > 0)

Description

This function tests whether a given queue is non-empty.

qlist_length

Synopsis

fun
{a:vt0p}
qlist_length
  {n:int}(q0: !qlist(INV(a), n)):<> int(n)

Description

This function computes the length of a given queue.

qlist_insert

Synopsis

fun{a:vt0p}
qlist_insert{n:int}
(
  q0: !qlist(INV(a), n) >> qlist(a, n+1), x: a
) :<!wrt> void // end of [qlist_insert]

Description

This function inserts an element at the end of a given queue.

qlist_takeout

Synopsis

fun{a:vt0p}
qlist_takeout{n:pos}
(
  q0: !qlist(INV(a), n) >> qlist(a, n-1)
) :<!wrt> (a) // end-of-function

Description

This function takes out the element at the front of a given queue if the queue is not empty, and returns true. Otherwise, it returns false.

qlist_takeout_opt

Synopsis

fun{a:vt0p}
qlist_takeout_opt
  (q0: !qlist(INV(a)) >> _):<!wrt> Option_vt(a)

Description

This function is the optional version of qlist_takeout.

qlist_takeout_list

Synopsis

fun{}
qlist_takeout_list
  {a:vt0p}{n:int}
  (q0: !qlist(INV(a), n) >> qlist(a, 0)):<!wrt> list_vt(a, n)

Description

This function takes out all of the elements in a given queue. Note that the complexity of the funtion is O(1).

Example

The following code demonstrates a typical use of a qlist as a FIFO accumulator:

//
staload "libats/SATS/qlist.sats"
//
fun{
a:t0p
} list_copy
  {n:int}
(
  xs: list (a, n)
) : list_vt (a, n) = let
//
fun loop
  {i,j:int}
(
  xs: list (a, i), pq: qlist (a, j)
) : list_vt (a, i+j) = let
in
//
case+ xs of
| list_cons
    (x, xs) => let
    val () = qlist_insert (pq, x)
  in
    loop (xs, pq)
  end // end of [list_cons]
| list_nil () => let
    val res = qlist_takeout_list (pq)
    val () = qlist_free_nil (pq)
  in
     res
  end // end of [list_nil]
//
end // end of [loop]
//
in
  loop (xs, qlist_make_nil ())
end // end of [list_copy]

qlist_foreach$cont

Synopsis

fun
{a:vt0p}
{env:vt0p}
qlist_foreach$cont (x: &a, env: &env): bool

qlist_foreach$fwork

Synopsis

fun
{a:vt0p}
{env:vt0p}
qlist_foreach$fwork (x: &a >> _, env: &(env) >> _): void

qlist_foreach

Synopsis

fun
{a:vt0p}
qlist_foreach (q: !qlist(INV(a))): void

qlist_foreach_env

Synopsis

fun
{a:vt0p}
{env:vt0p}
qlist_foreach_env
  (q: !qlist(INV(a)), env: &(env) >> _): void

qstruct

Synopsis

abst@ype
qstruct_tsize =
  $extype"atslib_qlist_qstruct"
stadef qstruct = qstruct_tsize
absvt@ype
qstruct_vt0ype (a:vt@ype+, n:int) = qstruct_tsize
stadef qstruct = qstruct_vt0ype

Description

The abstract type qstruct_tsize is primarily needed for allocating a variable in the calling frame of a function to store a qstruct-value.

Given a type T and an integer N, the abstract type qstruct_vt0ype(T, N) is for an unboxed queue containing N elements of type T.

qstruct_initize

Synopsis

fun{}
qstruct_initize
  {a:vt0p}
  (q0: &qstruct? >> qstruct(a, 0)):<!wrt> void

qstruct_uninitize

Synopsis

praxi
qstruct_uninitize
  {a:vt0p}
  ( q0: &qstruct(a, 0) >> qstruct? ):<prf> void

qstruct_objfize

Synopsis

praxi
qstruct_objfize
  {a:vt0p}
  {l:addr}{n:int}
(
  pf: qstruct(INV(a), n) @ l | p: !ptrlin l >> qlist(a, n)
) :<prf> mfree_ngc_v (l) // endfun

qstruct_unobjfize

Synopsis

praxi
qstruct_unobjfize
  {a:vt0p}
  {l:addr}{n:int}
(
  pf: mfree_ngc_v(l) | p: ptr l, q: !qlist(INV(a), n) >> ptrlin l
) :<prf> qstruct(a, n) @ l // endfun

qstruct_insert

Synopsis

fun{a:vt0p}
qstruct_insert{n:int}
  (q: &qstruct(INV(a), n) >> qstruct(a, n+1), x: a):<!wrt> void

Description

This function is a variant of qlist_insert.

qstruct_takeout

Synopsis

fun{a:vt0p}
qstruct_takeout{n:pos}
  (q: &qstruct(INV(a), n) >> qstruct(a, n-1)):<!wrt> (a)

Description

This function is a variant of qlist_takeout.

qstruct_takeout_list

Synopsis

fun{}
qstruct_takeout_list
  {a:vt0p}{n:int}
  (q: &qstruct(INV(a), n) >> qstruct(a, 0)):<!wrt> list_vt(a, n)

Description

This function is a variant of qlist_takeout_list.

qlist_node_vtype

Synopsis

absvtype
qlist_node_vtype(a:vt@ype+, l:addr) = ptr

Description

This abstract viewtype is for the list-nodes in a qlist-object.

mynode

Synopsis

stadef
mynode = qlist_node_vtype

vtypedef
mynode(a) = [l:addr] mynode(a, l)

mynode0

Synopsis

vtypedef
mynode0(a) = [l:addr | l >= null] mynode(a, l)

mynode1

Synopsis

vtypedef
mynode1(a) = [l:addr | l >  null] mynode(a, l)

mynode2ptr

Synopsis

castfn
mynode2ptr
  {a:vt0p}
  {l:addr}
  (nx: !mynode(INV(a), l)):<> ptr(l)

mynode_free_null

Synopsis

praxi
mynode_free_null{a:vt0p}(nx: mynode(a, null)): void

mynode_make_elt

Synopsis

fun{a:vt0p}
mynode_make_elt(x: a):<!wrt> mynode1(a)

mynode_getref_elt

Synopsis

fun{a:vt0p}
mynode_getref_elt(nx: !mynode1(INV(a))):<> cPtr1(a)

mynode_free_elt

Synopsis

fun{a:vt0p}
mynode_free_elt
  (nx: mynode1(INV(a)), res: &(a?) >> a):<!wrt> void

mynode_getfree_elt

Synopsis

fun{a:vt0p}
mynode_getfree_elt(node: mynode1(INV(a))):<!wrt> (a)

qlist_insert_ngc

Synopsis

fun{a:vt0p}
qlist_insert_ngc (*last*)
  {n:int}
(
  q0: !qlist(INV(a), n) >> qlist(a, n+1), nx: mynode1(a)
) :<!wrt> void // end of [qlist_insert_ngc]

qlist_takeout_ngc

Synopsis

fun{a:vt0p}
qlist_takeout_ngc (*first*)
  {n:int | n > 0}
  (q0: !qlist(INV(a), n) >> qlist(a, n-1)):<!wrt> mynode1(a)

Overloaded Symbols

iseqz

Synopsis

overload iseqz with qlist_is_nil

isneqz

Synopsis

overload isneqz with qlist_isnot_nil

length

Synopsis

overload length with qlist_length

fprint

Synopsis

overload fprint with fprint_qlist

overload fprint with fprint_qlist_sep

This page is created with ATS by Hongwei Xi and also maintained by Hongwei Xi.