Define the data structure for a complete Doubly Linked List.

 The structure should support adding elements to the head, tail and middle of the list. 
 The structure should not allow circular loops


See also

 Array
 Associative array: Creation, Iteration
 Collections
 Compound data type
 Doubly-linked list: Definition, Element definition, Element insertion, List Traversal, Element Removal
 Linked list
 Queue: Definition, Usage
 Set
 Singly-linked list: Element definition, Element insertion, List Traversal, Element Removal
 Stack


(********************************************************************)
(* The public interface                                             *)
 
abstype dllist_t (t : t@ype+, is_root : bool) (* An abstract type. *)
typedef dllist_t (t : t@ype+) = [b : bool] dllist_t (t, b)
 
(* Make a new dllist_t, consisting of a root node. *)
fun {t : t@ype}
dllist_t_make () : dllist_t (t, true)
 
(* Is this the root node, with no element stored? *)
fun {t : t@ype}
dllist_t_is_root
          {is_root : bool}
          (dl : dllist_t (t, is_root)) :
    [b : bool | b == is_root]
    bool b
 
(* Is this a non-root node, with an element stored? *)
fun {t : t@ype}
dllist_t_isnot_root
          {is_root : bool}
          (dl : dllist_t (t, is_root)) :
    [b : bool | b == ~is_root]
    bool b
 
(* Return the root node of the list. *)
fun {t : t@ype}
dllist_t_root (dl : dllist_t t) : dllist_t (t, true)
 
(* Return the previous node. *)
fun {t : t@ype}
dllist_t_previous (dl : dllist_t t) : dllist_t t
 
(* Return the next node. *)
fun {t : t@ype}
dllist_t_next (dl : dllist_t t) : dllist_t t
 
(* Insert an element before the given node. *)
fun {t : t@ype}
dllist_t_insert_before (dl : dllist_t t, elem : t) : void
 
(* Insert an element after the given node. *)
fun {t : t@ype}
dllist_t_insert_after (dl : dllist_t t, elem : t) : void
 
(* Remove the given node. It is an error to call this on the root
   node. *)
fun {t : t@ype}
dllist_t_remove (dl : dllist_t t) : void
 
(* Return a copy of the stored element. It is an error to call this on
   the root node. *)
fun {t : t@ype}
dllist_t_element (dl: dllist_t t) : t
 
fun {t : t@ype}
dllist_t_make_generator (dl: dllist_t t, direction : int) :
    () -<cloref1> Option t
 
fun {t : t@ype}
dllist_t_to_list
          (dl : dllist_t t) : [n : nat] list (t, n)
 
fun {t : t@ype}
list_to_dllist_t
          {n : int}
          (dl : list (t, n)) : dllist_t t
 
(********************************************************************)