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

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

#ifndef CT_SORTING_MACHINE_PUT_TO_1
#define CT_SORTING_MACHINE_PUT_TO_1 1

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

#include "AT/General/Put_To.h"
/*!
    #include "AT/Sorting_Machine/Kernel.h"
!*/

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

concrete_template <
	concrete_instance class Item,
	/*!
	    implements
		abstract_instance General_Put_To <Item>
	!*/
	concrete_instance class Sorting_Machine_Base
	/*!
	    implements
		abstract_instance Sorting_Machine_Kernel <Item>
	!*/
    >
class Sorting_Machine_Put_To_1 :
    extends
	concrete_instance Sorting_Machine_Base,
    implements
	abstract_instance General_Put_To <Sorting_Machine_Base>
{
public:
    
    procedure_body Put_To (
	    alters Character_OStream& outs
	)
    {
	object Boolean insertion_phase;
	object catalyst Sorting_Machine_Put_To_1 temp;

	insertion_phase = not self.Is_In_Extraction_Phase ();

	outs.Open_Scope ("(");

	// Display machine phase (note: model variable is "inserting")

	outs.New_Line ();
	outs << insertion_phase << ",";

	outs.Open_Scope ("{");

	// Display items in any order

	while (self.Size () > 0)
	/*!
	    alters self, temp
	    maintains
		temp multiset_union self = #temp multiset_union #self  and
		temp multiset_intersection self = empty_multiset  and
		[items in temp have been output already]
	    decreases
		|self|
	!*/
	{
	    object catalyst Item x;

	    self.Remove_Any (x);
	    outs.New_Line ();
	    outs << x;
	    if (self.Size () > 0)
	    {
		outs << ',';
	    }
	    temp.Insert (x);
	}

	outs.Close_Scope ("}");
	outs.Close_Scope (")");

	if (not insertion_phase)
	{
	    temp.Change_To_Extraction_Phase ();
	}
	self &= temp; 
    }

};

#endif // CT_SORTING_MACHINE_PUT_TO_1