Introduction to Programming in ATS:
Prev	Chapter 14. Dataviews as Linear Dataprops	Next

Dataview for 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
, addr(*beg*)
, addr(*end*)
, int(*length*)
) = // slseg_v
  | {l:addr}
    slseg_v_nil (a, l, l, 0) of ()
  | {l_fst:agz}{l_nxt,l_end:addr}{n:nat}
    slseg_v_cons (a, l_fst, l_end, n+1) of
      ((a, ptr l_nxt) @ l_fst, slseg_v (a, l_nxt, l_end, n))
// 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, l, l, 0)
//
slseg_v_cons :
  {a:t@ype}{l_fst:agz}{l_nxt,l_end:addr}{n:nat}
  ((a, ptr l_nxt) @ l_fst, slseg_v (a, l_nxt, l_end, n)) -> slseg_v (a, l_fst, l_end, n+1)
//

Note that agz is a subset sort for addresses that are not null. Given a type T, two addresses L1 and L2, and a natural number N, the view slseg_v(T, L1, L2, N) 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 slist_v
  (a:t@ype, l:addr, n:int) = slseg_v (a, l, null, n)
// end of [slist_v]

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

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

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

fn{a:t@ype}
slist_ptr_length
  {l:addr}{n:nat}
(
  pflst: !slist_v (a, l, n) | p: ptr l
) : int (n) = let
  fun loop
    {l:addr}{i,j:nat} .<i>.
  (
    pflst: !slist_v (a, l, i) | p: ptr l, j: int (j)
  ) : int (i+j) =
    if p > 0 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 [slist_ptr_length]

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

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

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

fn{a:t@ype}
slist_ptr_reverse
  {l:addr}{n:nat}
(
  pflst: slist_v (a, l, n) | p: ptr l
) : [l:addr] (slist_v (a, l, n) | ptr l) = let
  fun loop
    {n1,n2:nat}
    {l1,l2:addr} .<n1>. (
    pf1lst: slist_v (a, l1, n1)
  , pf2lst: slist_v (a, l2, n2)
  | p1: ptr l1, p2: ptr l2
  ) : [l:addr] (slist_v (a, l, n1+n2) | ptr l) =
    if p1 > 0 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, the_null_ptr)
end // end of [slist_ptr_reverse]

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

slist_struct*
slist_ptr_reverse
(
  slist_struct *p
) {
  slist_struct *tmp, *res = NULL ;
  while (p != NULL) {
    tmp = p->next ; p->next = res ; res = p ; p = tmp ;
  }
  return res ;
} // end of [slist_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:

slist_struct*
slist_ptr_append
  (slist_struct *p, slist_struct *q) {
  slist_struct *p1 = p ;
  if (p1 == NULL) return q ;
  while (p1->next != NULL) p1 = p1->next ; p1->next = q ;
  return p ;
} // end of [slist_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 slist_ptr_append in C can be translated directly into to the following one in ATS:

fn{a:t@ype}
slist_ptr_append
  {l1,l2:addr}{n1,n2:nat}
(
  pf1lst: slist_v (a, l1, n1)
, pf2lst: slist_v (a, l2, n2)
| p1: ptr l1, p2: ptr l2
) : [l:addr] (slist_v (a, l, n1+n2) | ptr l) = let
  fun loop
    {n1,n2:nat}
    {l1,l2:addr | l1 > null} .<n1>. (
    pf1lst: slist_v (a, l1, n1)
  , pf2lst: slist_v (a, l2, n2)
  | p1: ptr l1, p2: ptr l2
  ) : (slist_v (a, l1, n1+n2) | void) = let
    prval slseg_v_cons (pf1at, pf1lst) = pf1lst
    val p1_nxt = !p1.1
  in
    if p1_nxt > 0 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 > 0 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 [slist_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 slist_ptr_reverse in C is certainly type-correct:

/*
** This implementation is *incorrect* but type-correct:
*/
slist_struct*
slist_ptr_reverse
  (slist_struct *p)
{
  slist_struct *tmp, *res = NULL ;
  while (p != NULL) {
    tmp = p->next ; res = p ; p->next = res ; p = tmp ;
  }
  return res ;
} // end of [slist_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 also be declared in ATS, but there is really little need for it as we can declare a dataviewtype for such lists that is far more convenient to use. However, dataviews are fundamentally 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 dataviews in ATS.

Prev	Home	Next
Dataview for Linear Strings	Up	Proof Functions for View-Changes