#line 976 "/home/travis/build/felix-lang/felix/src/packages/lists.fdoc"
  class DList[T]
  {
    typedef dnode_t=
    (
      data: T,
      next: cptr[dnode_t], // possibly NULL
      prev: cptr[dnode_t]  // possibly NULL
    );
    typedef dlist_t = (first:cptr[dnode_t], last:cptr[dnode_t]);
      // invariant: if first is null, so is last!
  
    ctor dlist_t () => (first=nullptr[dnode_t],last=nullptr[dnode_t]);
  
  #line 991 "/home/travis/build/felix-lang/felix/src/packages/lists.fdoc"
    fun len (x:dlist_t) = {
      var n = 0;
      var first : cptr[dnode_t] = x.first;
    again:>
      match first do
      | #nullptr => return n;
      | Ptr p => ++n; first = p*.next;
      done
      goto again;
    }
  
  #line 1004 "/home/travis/build/felix-lang/felix/src/packages/lists.fdoc"
    fun peek_front (dl:dlist_t) : opt[T] =>
      match dl.first with
      | #nullptr => None[T]
      | Ptr p => Some p*.data
      endmatch
    ;
  
    fun peek_back (dl:dlist_t) : opt[T] =>
      match dl.last with
      | #nullptr => None[T]
      | Ptr p => Some p*.data
      endmatch
    ;
  
  #line 1020 "/home/travis/build/felix-lang/felix/src/packages/lists.fdoc"
    proc push_front (dl:&dlist_t, v:T) {
      var oldfirst = dl*.first;
      var node = new (data=v, next=oldfirst, prev=nullptr[dnode_t]);
      dl.first <- Ptr node;
      match oldfirst with
      | #nullptr => dl.last
      | Ptr p => p.prev
      endmatch <- Ptr node;
    }
  
    proc push_back (dl:&dlist_t, v:T) {
      var oldlast = dl*.last;
      var node = new (data=v, next=nullptr[dnode_t], prev=oldlast);
      dl.last <- Ptr node;
      match oldlast with
      | #nullptr => dl.first
      | Ptr p => p.next
      endmatch <- Ptr node;
    }
  
  #line 1042 "/home/travis/build/felix-lang/felix/src/packages/lists.fdoc"
  
    gen pop_front (dl:&dlist_t): opt[T] = {
      match dl*.first do
      | #nullptr => return None[T];
      | Ptr p =>
        match p*.next do
        | #nullptr =>
          dl.first <- nullptr[dnode_t];
          dl.last <- nullptr[dnode_t];
        | _ =>
          dl.first <- p*.next;
        done
        return Some p*.data;
      done
    }
  
    gen pop_back (dl:&dlist_t): opt[T] = {
      match dl*.last do
      | #nullptr => return None[T];
      | Ptr p =>
        match p*.prev do
        | #nullptr =>
          dl.first <- nullptr[dnode_t];
          dl.last <- nullptr[dnode_t];
        | _ =>
          dl.last <- p*.prev;
        done
        return Some p*.data;
      done
    }
  
  #line 1077 "/home/travis/build/felix-lang/felix/src/packages/lists.fdoc"
    typedef queue_t = dlist_t;
    proc enqueue (q:&queue_t) (v:T) => push_front (q,v);
    gen dequeue (q:&queue_t) :opt[T] => pop_back q;
    ctor queue_t () => dlist_t ();
  #line 1084 "/home/travis/build/felix-lang/felix/src/packages/lists.fdoc"
    gen iterator (q:&queue_t) () => dequeue q;
  }