/* in-place list reversal */

#include "list.h"

/*@ requires is_list(p0)
  @ ensures \forall plist l0; \old(llist(p0, l0)) => llist(\result, rev(l0))
  @*/
list rev(list p0) {
  list r = p0;
  list p = NULL;
  /*@ invariant 
        \exists plist lp; \exists plist lr;
          llist(p, lp) && llist(r, lr) && disjoint(lp, lr) &&
          \forall plist l; 
            \old(llist(p0, l)) => app(rev(lr), lp) == rev(l)
    @ variant length(r) for length_order */
  while (r != NULL) {
    list q = r;
    r = r->tl;
    q->tl = p;
    p = q;
  }
  return p;
}

/* test */

#if 0
#include <stdio.h>

void print(list l) {
  if (l == NULL) 
    printf("NULL\n");
  else {
    printf("%d :: ", l->hd);
    print(l->tl);
  }
}

int main() {
  /* 1::2::3::NULL */
  struct struct_list l[3];
  list r;
  l[0].hd = 1;
  l[0].tl = &l[1];
  l[1].hd = 2;
  l[1].tl = &l[2];
  l[2].hd = 3;
  l[2].tl = NULL;
  print(l);
  r = rev(l);
  print(r);
}
#endif