
Data Structure

This illustrates a data structure, a means of storing data within a program.

You may see other such structures in the Data Structures category.
 Illustration of FIFO behavior
Task

Implement a FIFO queue.

Elements are added at one side and popped from the other in the order of insertion.



Operations:

   push   (aka enqueue)    - add element
   pop     (aka dequeue)    - pop first element
   empty                             - return truth value when empty


Errors:

   handle the error of trying to pop from an empty queue (behavior depends on the language and platform)


See

   Queue/Usage   for the built-in FIFO or queue of your language or standard library.


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


(*------------------------------------------------------------------*)
 
#define ATS_DYNLOADFLAG 0
 
#include "share/atspre_staload.hats"
 
staload UN = "prelude/SATS/unsafe.sats"
 
(*------------------------------------------------------------------*)
 
vtypedef queue_vt (vt : vt@ype+, n : int) =
  (* A list that forms the queue, and a pointer to its last node. *)
  @(list_vt (vt, n), ptr)
 
#define NIL list_vt_nil ()
#define :: list_vt_cons
 
fn {}
queue_vt_nil {vt : vt@ype}
            () :
    queue_vt (vt, 0) =
  @(NIL, the_null_ptr)
 
fn {}
queue_vt_is_empty
          {n  : int}
          {vt : vt@ype}
          (q  : !queue_vt (vt, n)) :
    [is_empty : bool | is_empty == (n == 0)]
    bool is_empty =
  case+ q.0 of
  | NIL => true
  | _ :: _ => false
 
fn {vt : vt@ype}
queue_vt_enqueue
          {n : int}
          (q : queue_vt (vt, n),
           x : vt) :
    (* Returns the new queue. *)
    [m : int | 1 <= m; m == n + 1]
    queue_vt (vt, m) =
  let
    val @(lst, tail_ptr) = q
    prval _ = lemma_list_vt_param lst
  in
    case+ lst of
    | ~ NIL =>
      let
        val lst = x :: NIL
        val tail_ptr = $UN.castvwtp1{ptr} lst
      in
        @(lst, tail_ptr)
      end
    | _ :: _ =>
      let
        val old_tail = $UN.castvwtp0{list_vt (vt, 1)} tail_ptr
        val+ @ (hd :: tl) = old_tail
 
        (* Extend the list by one node, at its tail end. *)
        val new_tail : list_vt (vt, 1) = x :: NIL
        val tail_ptr = $UN.castvwtp1{ptr} new_tail
        prval _ = $UN.castvwtp0{void} tl
        val _ = tl := new_tail
 
        prval _ = fold@ old_tail
        prval _ = $UN.castvwtp0{void} old_tail
 
        (* Let us cheat and simply *assert* (rather than prove) that
           the list has grown by one node. *)
        val lst = $UN.castvwtp0{list_vt (vt, n + 1)} lst
      in
        @(lst, tail_ptr)
      end
  end
 
(* The dequeue routine simply CANNOT BE CALLED with an empty queue.
   It requires a queue of type queue_vt (vt, n) where n is positive. *)
fn {vt : vt@ype}
queue_vt_dequeue
          {n : int | 1 <= n}
          (q : queue_vt (vt, n)) :
    (* Returns a tuple: the dequeued element and the new queue. *)
    [m : int | 0 <= m; m == n - 1]
    @(vt, queue_vt (vt, m)) =
  case+ q.0 of
  | ~ (x :: lst) => @(x, @(lst, q.1))
 
(* queue_vt is a linear type that must be freed. *)
extern fun {vt : vt@ype}
queue_vt$element_free : vt -> void
fn {vt : vt@ype}
queue_vt_free {n : int}
              (q : queue_vt (vt, n)) :
    void =
  let
    fun
    loop {n : nat} .<n>. (lst : list_vt (vt, n)) : void =
      case+ lst of
      | ~ NIL => begin end
      | ~ (hd :: tl) =>
        begin
          queue_vt$element_free<vt> hd;
          loop tl
        end
    prval _ = lemma_list_vt_param (q.0)
  in
    loop (q.0)
  end
 
(*------------------------------------------------------------------*)
(* An example: a queue of nonlinear strings. *)
 
vtypedef strq_vt (n : int) = queue_vt (string, n)
 
fn {}                  (* A parameterless template, for efficiency. *)
strq_vt_nil () : strq_vt 0 =
  queue_vt_nil ()
 
fn {}                  (* A parameterless template, for efficiency. *)
strq_vt_is_empty {n : int} (q : !strq_vt n) :
    [is_empty : bool | is_empty == (n == 0)] bool is_empty =
  queue_vt_is_empty<> q
 
fn
strq_vt_enqueue {n : int} (q : strq_vt n, x : string) :
    [m : int | 1 <= m; m == n + 1] strq_vt m =
  queue_vt_enqueue<string> (q, x)
 
fn (* Impossible to...     VVVVVV   ...call with an empty queue. *)
strq_vt_dequeue {n : int | 1 <= n} (q : strq_vt n) :
    [m : int | 0 <= m; m == n - 1] @(string, strq_vt m) =
  queue_vt_dequeue<string> q
 
fn
strq_vt_free {n : int} (q : strq_vt n) : void =
  let
    implement
    queue_vt$element_free<string> x =
      (* A nonlinear string will be allowed to leak. (It might be
         collected as garbage, however.) *)
      begin end
  in
    queue_vt_free<string> q
  end
 
macdef qnil = strq_vt_nil ()
overload iseqz with strq_vt_is_empty
overload << with strq_vt_enqueue
overload pop with strq_vt_dequeue
overload free with strq_vt_free
 
implement
main0 () =
  {
    val q = qnil
    val _ = println! ("val q = qnil")
    val _ = println! ("iseqz q = ", iseqz q)
    val _ = println! ("val q = q << \"one\" << \"two\" << \"three\"")
    val q = q << "one" << "two" << "three"
    val _ = println! ("iseqz q = ", iseqz q)
    val _ = println! ("val (x, q) = pop q")
    val (x, q) = pop q
    val _ = println! ("x = ", x)
    val _ = println! ("val (x, q) = pop q")
    val (x, q) = pop q
    val _ = println! ("x = ", x)
    val _ = println! ("val q = q << \"four\"")
    val q = q << "four"
    val _ = println! ("val (x, q) = pop q")
    val (x, q) = pop q
    val _ = println! ("x = ", x)
    val _ = println! ("val (x, q) = pop q")
    val (x, q) = pop q
    val _ = println! ("x = ", x)
    val _ = println! ("iseqz q = ", iseqz q)
    //val (x, q) = pop q  // If you uncomment this you cannot compile!
    val _ = free q
  }
 
(*------------------------------------------------------------------*)