Introduction to Programming in ATS:
<<< Previous	Dataviews as Linear Dataprops	Next >>>

Singly-Linked Lists

The following dataview slseg_v captures the notion of a singly-linked list segment:

dataview
slseg_v (
  a:t@ype+ // covariant argument
, int(*len*)
, addr(*beg*)
, addr(*end*)
) =
  | {l:addr} slseg_v_nil (a, 0, l, l) of ()
  | {n:nat} {l_fst:agz} {l_nxt,l_end:addr}
    slseg_v_cons (a, n+1, l_fst, l_end) of
      ((a, ptr l_nxt) @ l_fst, slseg_v (a, n, l_nxt, l_end))
// end of [slseg]_v

There are two proof constructors slseg_v_nil and slseg_v_cons associated with slseg_v, which are assigned the following types:

slseg_v_nil :
  {a:t@ype} {l:addr} () -> slseg_v (a, 0, l, l)
slseg_v_cons :
  {a:t@ype} {n:nat} {l_fst:agz} {l_nxt,l_end:addr}
  ((a, ptr l_nxt) @ l_fst, slseg_v (a, l_nxt, l_end)) -> slseg_v (a, n+1, l_fst, l_end)

Note that agz is a subset sort for addresses that are not null. Given a type T, a natural number N and two addresses L1 and L2, the view slseg_v (T, N, L1, L2) is for a singly-linked list segment containing N elements of the type T that starts at L1 and finishes at L2. In the case where L2 is the null pointer, then the list segment is considered a list as is formally defined below:

viewdef sllst_v
  (a:t@ype, n:int, l:addr) = slseg_v (a, n, l, null)
// end of [sllst_v]

Given a type T, a pointer pointing to L plus a proof of the view sllst_v(T, N, L) for some natural number N is essentially the same as a pointer to a struct of the following declared type sllst_struct in C:

typedef struct sllst {
  T data ; /* [T] matches the corresponding type in ATS */
  struct sllst *next ; /* pointing to the tail of the list */
} sllst_struct ;

Let us now see a simple example involving singly-linked lists:

fn{a:t@ype}
sllst_ptr_length
  {n:nat} {l:addr} (
  pflst: !sllst_v (a, n, l) | p: ptr l
) : int (n) = let
  fun loop {i,j:nat} {l:addr} .<i>. (
    pflst: !sllst_v (a, i, l) | p: ptr l, j: int (j)
  ) : int (i+j) =
    if p > null then let
      prval slseg_v_cons (pfat, pf1lst) = pflst
      val res = loop (pf1lst | !p.1, j+1) // !p.1 points to the tail
      prval () = pflst := slseg_v_cons (pfat, pf1lst)
    in
      res
    end else let // the length of a null list is 0
      prval slseg_v_nil () = pflst in pflst := slseg_v_nil (); j
    end (* end of [if] *)
  // end of [loop]
in
  loop (pflst | p, 0)
end // end of [sllst_ptr_length]

The function template sllst_ptr_length computes the length of a given singly-linked list. Note that the inner function loop is tail-recursive. The above implementation of sllst_ptr_length essentially corresponds to the following implementation in C:

int sllst_ptr_length (sllst_struct *p) {
  int res = 0 ;
  while (p != NULL) { res = res + 1 ; p = p->next ; }
  return res ;
} // end of [sllst_ptr_length]

As another example, the following function template sllst_ptr_reverse turns a given linked list into its reverse:

fn{a:t@ype}
sllst_ptr_reverse
  {n:nat} {l:addr} (
  pflst: sllst_v (a, n, l) | p: ptr l
) : [l:addr] (sllst_v (a, n, l) | ptr l) = let
  fun loop
    {n1,n2:nat}
    {l1,l2:addr} .<n1>. (
    pf1lst: sllst_v (a, n1, l1)
  , pf2lst: sllst_v (a, n2, l2)
  | p1: ptr l1, p2: ptr l2
  ) : [l:addr] (sllst_v (a, n1+n2, l) | ptr l) =
    if p1 > null then let
      prval slseg_v_cons (pf1at, pf1lst) = pf1lst
      val p1_nxt = !p1.1
      val () = !p1.1 := p2
    in
      loop (pf1lst, slseg_v_cons (pf1at, pf2lst) | p1_nxt, p1)
    end else let
      prval slseg_v_nil () = pf1lst in (pf2lst | p2)
    end // end of [if]
in
  loop (pflst, slseg_v_nil | p, null)
end // end of [sllst_ptr_reverse]

By translating the tail-recursive function loop into a while-loop, we can readily turn the implementation of sllst_ptr_reverse in ATS into the following implementation in C:

sllst_struct *sllst_ptr_reverse (sllst_struct *p) {
  sllst_struct *tmp, *res = NULL ;
  while (p != NULL) {
    tmp = p->next ; p->next = res ; res = p ; p = tmp ;
  }
  return res ;
} // end of [sllst_ptr_reverse]

Let us see yet another example. List concatenation is a common operation on lists. This time, we first give an implementation of list concatenation in C:

sllst_struct *sllst_ptr_append
  (sllst_struct *p, sllst_struct *q) {
  sllst_struct *p1 = p ;
  if (p1 == NULL) return q ;
  while (p1->next != NULL) p1 = p1->next ; p1->next = q ;
  return p ;
} // end of [sllst_ptr_append]

The algorithm is straightforward. If p is null, then q is returned. Otherwise, the last node in the list pointed to by p is first found and its field of the name next then replaced with q. This implementation of sllst_ptr_append in C can be translated directly into to following one in ATS:

fn{a:t@ype}
sllst_ptr_append
  {n1,n2:nat} {l1,l2:addr} (
  pf1lst: sllst_v (a, n1, l1)
, pf2lst: sllst_v (a, n2, l2)  
| p1: ptr l1, p2: ptr l2
) : [l:addr] (sllst_v (a, n1+n2, l) | ptr l) = let
  fun loop
    {n1,n2:nat}
    {l1,l2:addr | l1 > null} .<n1>. (
    pf1lst: sllst_v (a, n1, l1)
  , pf2lst: sllst_v (a, n2, l2)  
  | p1: ptr l1, p2: ptr l2
  ) : (sllst_v (a, n1+n2, l1) | void) = let
    prval slseg_v_cons (pf1at, pf1lst) = pf1lst
    val p1_nxt = !p1.1
  in
    if p1_nxt > null then let
      val (pflst | ()) = loop (pf1lst, pf2lst | p1_nxt, p2)
    in
      (slseg_v_cons (pf1at, pflst) | ())
    end else let
      val () = !p1.1 := p2
      prval slseg_v_nil () = pf1lst
    in
      (slseg_v_cons (pf1at, pf2lst) | ())
    end (* end of [if] *)
  end // end of [loop]
in
  if p1 > null then let
    val (pflst | ()) = loop (pf1lst, pf2lst | p1, p2)
  in
    (pflst | p1)
  end else let
    prval slseg_v_nil () = pf1lst in (pf2lst | p2)
  end (* end of [if] *)
end // end of [sllst_ptr_append]

In the above examples, it is evident that the code in ATS is a lot more verbose than its counterpart in C. However, the former is also a lot more robust than the latter in the following sense: If a minor change is made to the code in ATS (e.g., renaming identifiers, reordering function arguments), it is most likely that a type-error is to be reported when the changed code is typechecked. On the other hand, the same thing cannot be said about the code written in C. For instance, the following erroneous implementation of sllst_ptr_reverse in C is certainly type-correct:

/*
** This implementation is *incorrect* but type-correct:
*/
sllst_struct *sllst_ptr_reverse (sllst_struct *p) {
  sllst_struct *tmp, *res = NULL ;
  while (p != NULL) {
    tmp = p->next ; res = p ; p->next = res ; p = tmp ;
  }
  return res ;
} // end of [sllst_ptr_reverse]

I now point out that the dataview slseg_v is declared here in a manner that does not address the issue of allocating and freeing list nodes, and it is done so for the sake of a less involved presentation. A dataview for singly-linked lists that does handle allocation and deallocation of list nodes can be found in the libats library of ATS.

There is another method for handling singly-linked lists in ATS that is based on the notion of dataviewtype (i.e., linear datatype). When compared to the one presented above, this alternative is significantly simpler. However, dataviews are more general and flexible than dataviewtypes, and there are many common data structures (e.g. doubly-linked lists) that can only be properly handled with the former in ATS.

<<< Previous	Home	Next >>>
Linear Arrays	Up	Proof Functions for View Changes