ATSLIB/libats/deqarray

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


  • deqarray
  • deqarray_vtype
  • lemma_deqarray_param
  • deqarray_make_cap
  • deqarray_make_ngc__tsz
  • deqarray_free_nil
  • deqarray_get_size
  • deqarray_get_capacity
  • deqarray_insert_atbeg
  • deqarray_insert_atbeg_opt
  • deqarray_insert_atend
  • deqarray_insert_atend_opt
  • deqarray_takeout_atbeg
  • deqarray_takeout_atbeg_opt
  • deqarray_takeout_atend
  • deqarray_takeout_atend_opt
  • deqarray_getref_at
  • deqarray_getref_at_int
  • deqarray_getref_at_size
  • deqarray_foreach
  • deqarray_foreach_env
  • deqarray_foreach$cont
  • deqarray_foreach$fwork

  • 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. SourceForge.net Logo