Resolve/C++ Catalog
CT/Queue/Kernel_1.h
Copyright © 2010, Reusable Software Research Group, The Ohio State University

//  /*----------------------------------------------------------------*\
//  |   Concrete Template : Queue_Kernel_1
//  \*----------------------------------------------------------------*/

#ifndef CT_QUEUE_KERNEL_1
#define CT_QUEUE_KERNEL_1 1

///---------------------------------------------------------------------
/// Global Context -----------------------------------------------------
///---------------------------------------------------------------------

#include "AT/Queue/Kernel.h"

///---------------------------------------------------------------------
/// Interface ----------------------------------------------------------
///---------------------------------------------------------------------

concrete_template <
	concrete_instance class Item,
	concrete_instance class Node,
	/*!
	    implements
		abstract_instance Record <
			Item,
			Pointer_C <Node>
		    >
	!*/
	concrete_instance class Rep =
            Representation <
		    Pointer_C <Node>,
		    Pointer_C <Node>,
		    Integer
		>    
    >
class Queue_Kernel_1 :
    implements
	abstract_instance Queue_Kernel <Item>,
    encapsulates
	concrete_instance Rep
{
private:

    rep_field_name (Rep, 0, Pointer_C <Node>, pre_front);
    rep_field_name (Rep, 1, Pointer_C <Node>, rear);
    rep_field_name (Rep, 2, Integer, length);

    field_name (Node, 0, Item, data);
    field_name (Node, 1, Pointer_C <Node>, next);
    
    /*!
	convention
	    self.pre_front /= NULL  and
	    self.rear /= NULL  and
	    self.length >= 0  and
	    [self.pre_front points to the first node of a
	     singly linked list containing self.length+1
	     Node nodes]  and
	    [self.rear points to the last node in that
	     singly linked list of nodes]
	     
	correspondence
	    if self.length = 0
		then self = empty_string
	    else if self.length = 1
		then self = <self.pre_front.next.data>
	    else if self.length = 2
		then self =
		    <self.pre_front.next.data> *
		    <self.rear.data>
	    else [self = 
		<self.pre_front.next.data> *
		<self.pre_front.next.next.data> *
		... *
		<self.rear.data>]
    !*/

    local_procedure_body Initialize ()
    {
	New (self[pre_front]);
	self[rear] = self[pre_front];
    }

    local_procedure_body Finalize ()
    {
	object Pointer_C <Node> p = self[pre_front];
	
	while (p != self[rear])
	{
	    self[pre_front] = (*p)[next];
	    Delete (p);
	    p = self[pre_front];
	}
	Delete (p);
    }

public:

    standard_concrete_operations (Queue_Kernel_1);

    procedure_body Enqueue (
	    consumes Item& x
	)
    {
	object Pointer_C <Node> p, q = self[rear];

	New (p);
	
	x &= (*p)[data];
	(*q)[next] = p;
	self[rear] = p;

	self[length]++;
    }

    procedure_body Dequeue (
	    produces Item& x
	)
    {
	object Pointer_C <Node> p = self[pre_front], q = (*p)[next];

	x &= (*q)[data];
	self[pre_front] = q;
	Delete (p);

	self[length]--;
    }

    function_body Item& operator [] (
	    preserves Accessor_Position& current
	)
    {
	object Pointer_C <Node> p = self[pre_front], q = (*p)[next];

	return (*q)[data];
    }

    function_body Integer Length ()
    {
	return self[length];
    }

};

#endif // CT_QUEUE_KERNEL_1