/*If you comment out the dispose instruction in list_remove
  then an error will be flaged, because it is a memory leak*/


hd,tl;

list_traverse(x) [list(x)] {
  t = x;
  /* listseg(x,t) should be framed */
  while(t != NULL) [listseg(x,t) * list(t)] {
    t = t->tl;
  }
} [list(x)]


listseg_traverse(x,y) [listseg(x,y)] {
  local t;
  t = x;
  if(t != y) {
    t = t->tl;
    listseg_traverse(t,y);
  } else {}
} [listseg(x,y)]

list_reverse(o,i) [list(i)] {
  o = NULL;
  while (i != NULL) [list(i) * list(o)] {
    t = i->tl;
    i->tl = o;
    o = i;
    i = t;
  }
} [list(o)]

list_deallocate(x) [listseg(x,0)] {
  while(x != NULL) [listseg(x,0)] {
    t = x;
    x = x->tl;
    dispose t;
  }
} [emp]

list_append(x,y) [list(x) * list(y)] {
  if (x == NULL) {
    x = y;
  } else {
    t = x;
    n = t->tl;
    /* list(y) is framed */
    while (n != NULL) [listseg(x,t) * t |-> n * list(n)] {
      t = n;
      n = t->tl;
    }
    t->tl = y;
  } /* listseg(x,t) * t |-> y * list(y) */
} [list(x)]

list_insert(l;x) [x|-> * list(l)] {
  local s, t, u;
  if(l==NULL) {
    x->tl = NULL;
    l = x;
  } else {
    s = x->hd;
    t = l->hd;
    if(s>t) {
      u = l->tl;
      list_insert(u;x);
      l->tl = u;
    } else {
      x->tl = l;
      l = x;
    }
  }
} [list(l)]

list_remove(l;x) [list(l)] {
  local t;
  if(l!=NULL) {
    if(l==x) {
      l = l->tl;
      dispose(x);
    } else {
      t = l->tl;
      list_remove(t;x);
      l->tl = t;
    }
  }
} [list(l)]