ATSLIB/libats/dllist

This package contains a variety of common functions for creating/freeing and manipulating doubly-linked linear lists.

The type for a doubly-linked linear list containing N elements of type T is denoted by dllist(T, F, R), where T can be linear, and F and R (satisfying F+R=N) indicate that there are F and R elements before and after the current pointer, respectively. Note that the type constructor dllist is co-variant in its first argument, that is, dllist(T1, F, R) is a subtype of dllist(T2, F, R) if T1 is a subtype of T2. The low-level representation for dllist is the same as that for a standard doubly-linked list in C, and it is fairly straightforward to implement functions in C that can directly manipulate doubly linked linear lists in ATS and vice versa.

dllist

dllist_vtype

dllist

Synopsis

stadef dllist = dllist_vtype

dllist_vtype

Synopsis

absvtype
dllist_vtype
  (a: viewt@ype+, f: int, r: int) = ptr // HX: f: front; r: rear

lemma1_dllist_param

Synopsis

praxi
lemma1_dllist_param {a:vt0p}
  {f,r:int} (xs: !dllist (INV(a), f, r)): [f >= 0;r >= 0] void

lemma2_dllist_param

Synopsis

praxi
lemma2_dllist_param
  {a:vt0p} {f,r:int | f > 0} (xs: !dllist (INV(a), f, r)): [r > 0] void

lemma3_dllist_param

Synopsis

praxi
lemma3_dllist_param
  {a:vt0p} {f,r:int | r <= 0} (xs: !dllist (INV(a), f, r)): [f == 0] void

dllist_nil

Synopsis

fun{}
dllist_nil {a:vt0p} ():<> dllist (a, 0, 0)

dllist_free_nil

Synopsis

praxi
dllist_free_nil
  {a:vt0p}{f:int} (xs: dllist (INV(a), f, 0)): void

dllist_sing

Synopsis

fun{a:vt0p}
dllist_sing (x: a):<!wrt> dllist (a, 0, 1)

Description

Given a value, this function returns a singleton list containing the value.

dllist_cons

Synopsis

fun{a:vt0p}
dllist_cons{r:int}
  (x: a, xs: dllist (INV(a), 0, r)):<!wrt> dllist (a, 0, r+1)

dllist_uncons

Synopsis

fun{a:vt0p}
dllist_uncons{r:int | r > 0}
  (xs: &dllist (INV(a), 0, r) >> dllist (a, 0, r-1)):<!wrt> (a)

dllist_snoc

Synopsis

fun{a:vt0p}
dllist_snoc{f:int}
  (xs: dllist (INV(a), f, 1), x: a):<!wrt> dllist (a, f+1, 1)

dllist_unsnoc

Synopsis

fun{a:vt0p}
dllist_unsnoc{f:int | f > 0}
  (xs: &dllist (INV(a), f, 1) >> dllist (a, f-1, 1)):<!wrt> (a)

dllist_is_nil

Synopsis

fun{
} dllist_is_nil
  {a:vt0p}{f,r:int} (xs: !dllist (INV(a), f, r)):<> bool (r==0)

Description

This function tests whether a given list is empty.

dllist_is_cons

Synopsis

fun{
} dllist_is_cons
  {a:vt0p}{f,r:int} (xs: !dllist (INV(a), f, r)):<> bool (r > 0)

Description

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

dllist_is_atbeg

Synopsis

fun{a:vt0p}
dllist_is_atbeg
  {f,r:int}
  (xs: !dllist (INV(a), f, r)):<> bool (f==0)

Description

This function tests whether the segment before the current pointer of a given list is empty.

dllist_is_atend

Synopsis

fun{a:vt0p}
dllist_is_atend
  {f,r:int | r > 0}
  (xs: !dllist (INV(a), f, r)):<> bool (r==1)

Description

This function tests whether the segment after the current pointer of a given list is singleton.

rdllist_is_atbeg

Synopsis

fun{a:vt0p}
rdllist_is_atbeg
  {f,r:int | r > 0}
  (xs: !dllist (INV(a), f, r)):<> bool (r==1)

rdllist_is_atend

Synopsis

fun{a:vt0p}
rdllist_is_atend
  {f,r:int}
  (xs: !dllist (INV(a), f, r)):<> bool (f==0)

dllist_getref_elt

Synopsis

fun{a:vt0p}
dllist_getref_elt (xs: !Dllist1 (INV(a))):<> cPtr1 (a)

dllist_getref_next

Synopsis

fun{a:vt0p}
dllist_getref_next (xs: !Dllist1 (INV(a))):<> Ptr1

dllist_getref_prev

Synopsis

fun{a:vt0p}
dllist_getref_prev (xs: !Dllist1 (INV(a))):<> Ptr1

dllist_get_elt

Synopsis

fun{a:t0p}
dllist_get_elt (xs: !Dllist1 (INV(a))): a

dllist_set_elt

Synopsis

fun{a:t0p}
dllist_set_elt (xs: !Dllist1 (INV(a)), x0: a): void

dllist_length

Synopsis

fun{a:vt0p}
dllist_length
  {f,r:int} (xs: !dllist (INV(a), f, r)):<> int (r)

rdllist_length

Synopsis

fun{a:vt0p}
rdllist_length
  {f,r:int} (xs: !dllist (INV(a), f, r)):<> int (f)

dllist_move

Synopsis

fun{a:vt0p}
dllist_move
  {f,r:int | r > 1}
  (xs: dllist (INV(a), f, r)):<> dllist (a, f+1, r-1)

dllist_move_all

Synopsis

fun{a:vt0p}
dllist_move_all
  {f,r:int | r > 0}
  (xs: dllist (INV(a), f, r)):<> dllist (a, f+r-1, 1)

rdllist_move

Synopsis

fun{a:vt0p}
rdllist_move
  {f,r:int | f > 0}
  (xs: dllist (INV(a), f, r)):<> dllist (a, f-1, r+1)

rdllist_move_all

Synopsis

fun{a:vt0p}
rdllist_move_all
  {f,r:int | r >= 0}
  (xs: dllist (INV(a), f, r)):<> dllist (a, 0(*front*), f+r)

dllist_insert_next

Synopsis

fun{a:vt0p}
dllist_insert_next
  {f,r:int | r > 0}
  (xs: dllist (INV(a), f, r), x0: a):<!wrt> dllist (a, f, r+1)

Description

This function inserts a node into a given list immediately after the current node (to which the current pointer points).

dllist_insert_prev

Synopsis

fun{a:vt0p}
dllist_insert_prev
  {f,r:int | r > 0}
  (xs: dllist (INV(a), f, r), x0: a):<!wrt> dllist (a, f, r+1)

Description

This function inserts a node into a given list immediately before the current node (to which the current pointer points).

dllist_takeout

Synopsis

fun{a:vt0p}
dllist_takeout
  {f,r:int | r > 1}
  (xs: &dllist (INV(a), f, r) >> dllist (a, f, r-1)):<!wrt> (a)

dllist_takeout_next

Synopsis

fun{a:vt0p}
dllist_takeout_next
  {f,r:int | r > 1}
  (xs: &dllist (INV(a), f, r) >> dllist (a, f, r-1)):<!wrt> (a)

rdllist_insert

Synopsis

fun{a:vt0p}
rdllist_insert
  {f,r:int | r > 0}
  (xs: dllist (INV(a), f, r), x0: a):<!wrt> dllist (a, f+1, r)

rdllist_takeout

Synopsis

fun{a:vt0p}
rdllist_takeout
  {f,r:int | f > 0}
  (xs: &dllist (INV(a), f, r) >> dllist (a, f-1, r)):<!wrt> (a)

dllist_append

Synopsis

fun{a:vt0p}
dllist_append
  {f1,r1:int}{f2,r2:int} (
  xs1: dllist (INV(a), f1, r1), xs2: dllist (a, f2, r2)
) :<!wrt> dllist (a, f1, r1+f2+r2) // end of [dllist_append]

rdllist_append

Synopsis

fun{a:vt0p}
rdllist_append
  {f1,r1:int}{f2,r2:int | r2 > 0} (
  xs1: dllist (INV(a), f1, r1), xs2: dllist (a, f2, r2)
) :<!wrt> dllist (a, f1+r1+f2, r2) // end of [rdllist_append]

dllist_reverse

Synopsis

fun{a:vt0p}
dllist_reverse
  {f,r:int} (xs: dllist (INV(a), f, r)):<!wrt> dllist (a, f, r)

rdllist_reverse

Synopsis

fun{a:vt0p}
rdllist_reverse
  {f,r:int} (xs: dllist (INV(a), f, r)):<!wrt> dllist (a, f, r)

dllist_free

Synopsis

fun{a:t0p}
dllist_free
  {r:int} (xs: dllist (INV(a), 0, r)):<!wrt> void

dllist_freelin$clear

Synopsis

fun{a:vt0p}
dllist_freelin$clear (x: &a >> a?):<!wrt> void

dllist_freelin

Synopsis

fun{a:vt0p}
dllist_freelin {r:int} (xs: dllist (INV(a), 0, r)):<!wrt> void

dllist_foreach

Synopsis

fun{a:vt0p}
dllist_foreach (xs: !Dllist (INV(a))): void

dllist_foreach_env

Synopsis

fun{
a:vt0p}{env:vt0p
} dllist_foreach_env
  (xs: !Dllist (INV(a)), env: &env >> _): void

rdllist_foreach

Synopsis

fun{a:vt0p}
rdllist_foreach (xs: !Dllist (INV(a))): void

rdllist_foreach_env

Synopsis

fun{
a:vt0p}{env:vt0p
} rdllist_foreach_env
  (xs: !Dllist (INV(a)), env: &env >> _): void

Overloaded Symbols

fprint

Synopsis

overload fprint with fprint_dllist

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