This package contains a variety of common functions for creating/freeing and manipulating singly-linked linear lists.
The type for a singly-linked linear list containing N elements of type T is denoted by sllist(T, N), where T can be linear and N indicates that there are N elements in the list. Note that the type constructor sllist is co-variant in its first argument, that is, sllist(T1, N) is a subtype of sllist(T2, N) if T1 is a subtype of T2. The low-level representation for sllist is the same as that for a standard singly-linked list in C, and it is fairly straightforward to implement functions in C that can directly manipulate singly-linked linear lists in ATS and vice versa.
stadef sllist = sllist_vtype // HX: shorthand
absvtype
sllist_vtype (a:viewt@ype+, n:int) = ptr
praxi
lemma_sllist_param {a:vt0p}
{n:int} (xs: !sllist (INV(a), n)): [n >= 0] void
fun{}
sllist_nil {a:vt0p} ():<> sllist (a, 0)
praxi
sllist_free_nil
{a:vt0p} (xs: sllist (INV(a), 0)): void
fun{a:vt0p}
sllist_sing (x: a):<!wrt> sllist (a, 1)
fun{a:vt0p}
sllist_cons{n:int}
(x: a, xs: sllist (INV(a), n)):<!wrt> sllist (a, n+1)
fun{a:vt0p}
sllist_uncons{n:int | n > 0}
(xs: &sllist (INV(a), n) >> sllist (a, n-1)):<!wrt> (a)
fun{a:vt0p}
sllist_snoc{n:int}
(xs: sllist (INV(a), n), x: a):<!wrt> sllist (a, n+1)
fun{a:vt0p}
sllist_unsnoc{n:int | n > 0}
(xs: &sllist (INV(a), n) >> sllist (a, n-1)):<!wrt> (a)
fun{
} sllist_is_nil
{a:vt0p}{n:int} (xs: !sllist (INV(a), n)):<> bool (n==0)
fun{
} sllist_is_cons
{a:vt0p}{n:int} (xs: !sllist (INV(a), n)):<> bool (n > 0)
fun{a:vt0p}
sllist_length
{n:int} (xs: !sllist (INV(a), n)):<> int (n)
fun{a:t0p}
sllist_get_elt (xs: !Sllist1 (INV(a))): (a)
fun{a:t0p}
sllist_set_elt (xs: !Sllist1 (INV(a)), x0: a): void
fun{a:vt0p}
sllist_getref_elt (xs: !Sllist1 (INV(a))):<> cPtr1 (a)
fun{a:vt0p}
sllist_getref_next (xs: !Sllist1 (INV(a))):<> Ptr1
fun{a:t0p}
sllist_get_elt_at {n:int}
(xs: !sllist (INV(a), n), i: natLt(n)):<> (a)
fun{a:t0p}
sllist_set_elt_at {n:int}
(xs: !sllist (INV(a), n), i: natLt(n), x0: a):<!wrt> void
fun{a:vt0p}
sllist_getref_elt_at {n:int}
(xs: !sllist (INV(a), n), i: natLt(n)):<> cPtr1 (a)
fun{a:vt0p}
sllist_insert_at {n:int}
(xs: sllist (INV(a), n), i: natLte(n), x0: a):<!wrt> sllist (a, n+1)
fun{a:vt0p}
sllist_takeout_at {n:int}
(xs: &sllist (INV(a), n) >> sllist (a, n-1), i: natLt(n)):<!wrt> (a)
fun{a:vt0p} sllist_append {n1,n2:int} ( xs1: sllist (INV(a), n1), xs2: sllist (a, n2) ) :<!wrt> sllist (a, n1+n2) // end of [sllist_append]
fun{a:vt0p}
sllist_reverse
{n:int} (xs: sllist (INV(a), n)):<!wrt> sllist (a, n)
fun{a:t0p}
sllist_free (xs: Sllist (INV(a))):<!wrt> void
fun{a:vt0p}
sllist_freelin$clear (x: &a >> a?):<!wrt> void
fun{a:vt0p}
sllist_freelin (xs: Sllist (INV(a))):<!wrt> void
fun{
a:vt0p}{b:vt0p
} sllist_map {n:int} (xs: !sllist (a, n)): sllist (b, n)
fun{
a:vt0p}{b:vt0p
} sllist_map$fopr (x: &a): b
fun{a:vt0p}
sllist_foreach (xs: !Sllist (INV(a))): void
fun{
a:vt0p}{env:vt0p
} sllist_foreach_env
(xs: !Sllist (INV(a)), env: &env >> _): void
fun{
a:vt0p}{env:vt0p
} sllist_foreach$cont (x: &a, env: &env): bool
fun{
a:vt0p}{env:vt0p
} sllist_foreach$fwork (x: &a, env: &env >> _): void
stadef mytkind = $extkind"libats_sllist"
typedef g2node0 (a:vt0p) = gnode0 (mytkind, a)
typedef g2node1 (a:vt0p) = gnode1 (mytkind, a)
fun{a:vt0p}
sllist_cons_ngc{n:int}
(nx: g2node1(a), xs: sllist(INV(a), n)):<!wrt> sllist (a, n+1)
fun{a:vt0p}
sllist_uncons_ngc{n:pos}
(xs: &sllist (INV(a), n) >> sllist (a, n-1)):<!wrt> g2node1 (a)
fun{a:vt0p}
sllist_snoc_ngc{n:int}
(xs: sllist(INV(a), n), nx: g2node1(a)):<!wrt> sllist (a, n+1)
fun{a:vt0p}
sllist_unsnoc_ngc{n:pos}
(xs: &sllist (INV(a), n) >> sllist (a, n-1)):<!wrt> g2node1 (a)
overload iseqz with sllist_is_nil
overload isneqz with sllist_is_cons
overload [] with sllist_get_elt_at
overload [] with sllist_set_elt_at
overload fprint with fprint_sllist
| This page is created with ATS by Hongwei Xi and also maintained by Hongwei Xi. |
|