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

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

#ifndef CT_SORTING_MACHINE_KERNEL_1
#define CT_SORTING_MACHINE_KERNEL_1 1

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

#include "AT/Sorting_Machine/Kernel.h"
#include "CT/Queue/Kernel_1a.h"

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

concrete_template <
	concrete_instance class Item,
	concrete_instance utility_class Item_Are_In_Order,
        /*!
            implements
                abstract_instance General_Are_In_Order <Item>
        !*/
	concrete_instance class Queue_Of_Item =
            Queue_Kernel_1a <Item>,
	concrete_instance class Rep =
            Representation <
		    Boolean,
		    Queue_Of_Item
		>
    >
class Sorting_Machine_Kernel_1 :
    implements
	abstract_instance Sorting_Machine_Kernel <Item, Item_Are_In_Order>,
    encapsulates
	concrete_instance Rep
{
private:

    rep_field_name (Rep, 0, Boolean, inserting_rep);
    rep_field_name (Rep, 1, Queue_Of_Item, contents_rep);

    /*!
	correspondence
	    self.inserting = self.inserting_rep  and
	    self.contents = multiset_elements (self.contents_rep)
    !*/

    local_procedure_body Initialize ()
    {
	self[inserting_rep] = true;
    }
    
public:

    standard_concrete_operations (Sorting_Machine_Kernel_1);

    procedure_body Insert (
	    consumes Item& x
	)
    {
	self[contents_rep].Enqueue (x);
    }

    procedure_body Change_To_Extraction_Phase ()
    {
	self[inserting_rep] = false;
    }
    
    procedure_body Remove_First (
	    produces Item& x
	)
    {
	object catalyst Queue_Of_Item temp;

	self[contents_rep].Dequeue (x);
	while (self[contents_rep].Length () > 0)
	/*!
	    alters self.contents_rep, x, temp
	    maintains
		(temp * self.contents_rep * <x>) is permutation of
		    (#temp * #self.contents_rep * <#x>)  and
		 for all y: Item
			where (y is in elements (temp))
		    (ARE_IN_ORDER (x, y))
	    decreases
	        |self.contents_rep|
	!*/	        
	{
	    object catalyst Item y;

	    self[contents_rep].Dequeue (y);
	    if (Item_Are_In_Order::Are_In_Order (y, x))
	    {
		x &= y;
	    }
	    temp.Enqueue (y);
	}
	self[contents_rep] &= temp;
    }

    procedure_body Remove_Any (
	    produces Item& x
	)
    {    
	self[contents_rep].Dequeue (x);
    }

    function_body Boolean Is_In_Extraction_Phase ()
    {
	return not (self[inserting_rep]);
    }

    function_body Integer Size ()
    {
	return (self[contents_rep].Length ());
    }

};

//----------------------------------------------------------------------

#endif // CT_SORTING_MACHINE_KERNEL_1