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

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

#ifndef CT_SET_KERNEL_3
#define CT_SET_KERNEL_3 1
 
///---------------------------------------------------------------------
/// Global Context -----------------------------------------------------
///---------------------------------------------------------------------

#include "AT/Set/Kernel.h"
/*!
    #include "AT/General/Is_Equal_To.h"
!*/
#include "CT/Partial_Map/Kernel_1.h"

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

concrete_template <
	concrete_instance class Item,
        /*!
            implements
                abstract_instance General_Is_Equal_To <Item>
        !*/
        concrete_instance class Item_Character_Partial_Map =
            Partial_Map_Kernel_1 <Item,
			          Character>,
	concrete_instance class Rep =
            Representation <Item_Character_Partial_Map>
    >
class Set_Kernel_3 :
    implements
	abstract_instance Set_Kernel <Item>,
    encapsulates
	concrete_instance Rep
{
private:

    rep_field_name (Rep, 0, Item_Character_Partial_Map, contents);

    /*!
	correspondence
	    self = {x: Item where
	    (there exists c: Character ((x, c) is in self[contents]))}
    !*/

public:

    standard_concrete_operations (Set_Kernel_3);

    procedure_body Add (
	    consumes Item& x
	)
    {
	object Character ch;
	self[contents].Define (x, ch);
    }

    procedure_body Remove (
	    preserves Item& x,
	    produces Item& x_copy
	)
    {
	object Character ch;
	self[contents].Undefine (x, x_copy, ch);
    }


    procedure_body Remove_Any (
	    produces Item& x
	)
    {
	object Character ch;
	self[contents].Undefine_Any (x, ch);
    }

    function_body Boolean Is_Member (
	    preserves Item& x
	)
    {
	return self[contents].Is_Defined (x);
    }

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

};

#endif // CT_SET_KERNEL_3