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

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

#ifndef CT_LIST_PUT_TO_1
#define CT_LIST_PUT_TO_1 1

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

#include "AT/General/Put_To.h"
/*!
    #include "AT/List/Kernel.h"
!*/
   
///------------------------------------------------------------------------
/// Interface -------------------------------------------------------------
///------------------------------------------------------------------------

concrete_template <
	concrete_instance class Item,
	/*!
	    implements
		abstract_instance General_Put_To <Item>
	!*/
	concrete_instance class List_Base
	/*!
	    implements
		abstract_instance List_Kernel<Item>
	!*/
    >
class List_Put_To_1 :
    extends
	concrete_instance List_Base,
    implements
	abstract_instance General_Put_To <List_Base>
{
public:
    
    procedure_body Put_To (
	    alters Character_OStream& outs
	)
    {
	object Integer original_left_length = self.Left_Length ();

	self.Move_To_Start ();

	outs.Open_Scope ("(");
	outs.Open_Scope ("<");

	// Put left string of original
    
	while (self.Left_Length () < original_left_length)
	/*!
	    alters self
	    preserves original_left_length
	    maintains
		self.left * self.right = #self.left * #self.right  and
		|self.left| <= original_left_length  and
		[items in self.left have been output already]
	    decreases
		|self.right|
	!*/
	{
	    outs.New_Line ();
	    outs << self[current];
	    self.Advance ();
	}

	outs.Close_Scope (">");
	outs.Open_Scope ("<");

	// Put right string of original
    
	while (self.Right_Length () > 0)
	/*!
	    alters self
	    maintains
		self.left * self.right = #self.left * #self.right  and
		[items in self.left have been output already]
	    decreases
		|self.right|
	!*/
	{
	    outs.New_Line ();
	    outs << self[current];
	    self.Advance ();
	}

	outs.Close_Scope (">");
	outs.Close_Scope (")");

	// Restore the fence position
    
	self.Move_To_Start ();
	while (self.Left_Length () < original_left_length)
	/*!
	    alters self
	    preserves original_left_length
	    maintains
		self.left * self.right = #self.left * #self.right  and
		|self.left| <= original_left_length
	    decreases
		|self.right|
	!*/
	{
	    self.Advance ();
	}
    }

};

#endif // CT_LIST_PUT_TO_1