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

#ifndef CT_STACK_REVERSE_1
#define CT_STACK_REVERSE_1 1

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

#include "AT/Stack/Reverse.h"
/*!
    #include "AT/Stack/Kernel.h"
!*/
  
///------------------------------------------------------------------------
/// Interface -------------------------------------------------------------
///------------------------------------------------------------------------

concrete_template <
	concrete_instance class Item,
	concrete_instance class Stack_Base
	/*!
	    implements
		abstract_instance Stack_Kernel <Item>
	!*/
    >
class Stack_Reverse_1 :
    extends
	concrete_instance Stack_Base,
    implements
	abstract_instance Stack_Reverse <Item>
{
public:
    
    procedure_body Reverse ()
    {
	object Stack_Reverse_1 temp;

	while (self.Length () > 0)
	/*!
	    alters self, temp
	    maintains
		reverse (temp) * self = reverse (#temp) * #self 
	    decreases
		|self|
	!*/
	{
	    object catalyst Item x;

	    self.Pop (x);
	    temp.Push (x);
	}

	self &= temp;
    }

};

#endif // CT_STACK_REVERSE_1