ATSLIB/libats/deqarray

This package implements array-based linear double-ended queues (deques).

deqarray

Synopsis

stadef deqarray = deqarray_vtype

vtypedef
deqarray(a:vt0p) =
  [m,n:int] deqarray_vtype (a, m, n)

deqarray_vtype

Synopsis

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

lemma_deqarray_param

Synopsis

praxi
lemma_deqarray_param
  {a:vt0p}{m,n:int}
  (!deqarray(INV(a), m, n)): [m >= n; n >= 0] void

deqarray_make_cap

Synopsis

fun{a:vt0p}
deqarray_make_cap
  {m:int} (cap: size_t(m)):<!wrt> deqarray(a, m, 0)

deqarray_make_ngc__tsz

Synopsis

fun
deqarray_make_ngc__tsz
  {a:vt0p}
  {l:addr}{m:int}
(
  deqarray_tsize? @ l
| ptr(l), arrayptr(a?, m+1), size_t(m), sizeof_t(a)
) :<!wrt> (mfree_ngc_v (l) | deqarray(a, m, 0)) = "mac#%"

deqarray_free_nil

Synopsis

fun
deqarray_free_nil
  {a:vt0p}{m:int}
  (deq: deqarray(a, m, 0)):<!wrt> void = "mac#%"

deqarray_get_size

Synopsis

fun
{a:vt0p}
deqarray_get_size
  {m,n:int}
  (deq: !deqarray(INV(a), m, n)):<> size_t(n)

deqarray_get_capacity

Synopsis

fun
{a:vt0p}
deqarray_get_capacity
  {m,n:int}
  (deq: !deqarray(INV(a), m, n)):<> size_t(m)

deqarray_insert_atbeg

Synopsis

fun{a:vt0p}
deqarray_insert_atbeg
  {m,n:int | m > n}
(
  deq: !deqarray(INV(a),m,n) >> deqarray(a,m,n+1), x0: a
) :<!wrt> void // endfun

deqarray_insert_atbeg_opt

Synopsis

fun{a:vt0p}
deqarray_insert_atbeg_opt
  (deq: !deqarray(INV(a)) >> _, x0: a):<!wrt> Option_vt(a)

deqarray_insert_atend

Synopsis

fun
{a:vt0p}
deqarray_insert_atend
  {m,n:int | m > n}
(
  deq: !deqarray(INV(a),m,n) >> deqarray(a,m,n+1), x0: a
) :<!wrt> void // end-of-fun

deqarray_insert_atend_opt

Synopsis

fun
{a:vt0p}
deqarray_insert_atend_opt
  (deq: !deqarray(INV(a)) >> _, x0: a):<!wrt> Option_vt(a)

deqarray_takeout_atbeg

Synopsis

fun
{a:vt0p}
deqarray_takeout_atbeg
  {m,n:int | n > 0}
(
  deq: !deqarray(INV(a),m,n) >> deqarray(a,m,n-1)
) :<!wrt> (a) // end-of-fun

deqarray_takeout_atbeg_opt

Synopsis

fun
{a:vt0p}
deqarray_takeout_atbeg_opt
  (deq: !deqarray(INV(a)) >> _):<!wrt> Option_vt(a)

deqarray_takeout_atend

Synopsis

fun
{a:vt0p}
deqarray_takeout_atend
  {m,n:int | n > 0}
(
  deq: !deqarray(INV(a),m,n) >> deqarray(a,m,n-1)
) :<!wrt> (a) // end-of-fun

deqarray_takeout_atend_opt

Synopsis

fun
{a:vt0p}
deqarray_takeout_atend_opt
  (deq: !deqarray(INV(a)) >> _):<!wrt> Option_vt(a)

deqarray_getref_at

Synopsis

fun
{a:vt0p}
deqarray_getref_at
  {m,n:int}
  (deq: !deqarray(INV(a), m, n), i: sizeLt(n)):<> cPtr1(a)

deqarray_getref_at_int

Synopsis

Synopsis for [deqarray_getref_at_int] is unavailable.

deqarray_getref_at_size

Synopsis

Synopsis for [deqarray_getref_at_size] is unavailable.

deqarray_foreach

Synopsis

fun{
a:vt0p
} deqarray_foreach{m,n:int}
  (deq: !deqarray(INV(a), m, n)): void

deqarray_foreach_env

Synopsis

fun{
a:vt0p}{env:vt0p
} deqarray_foreach_env{m,n:int}
  (deq: !deqarray(INV(a), m, n), env: &(env) >> _): void

deqarray_foreach$cont

Synopsis

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

deqarray_foreach$fwork

Synopsis

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

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