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

//  /*-------------------------------------------------------------------*\
//  |   Concrete Instance : Partial_Map_Is_Equal_To_1
//  \*-------------------------------------------------------------------*/

#ifndef CT_PARTIAL_MAP_IS_EQUAL_TO_1
#define CT_PARTIAL_MAP_IS_EQUAL_TO_1 1

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

#include "AT/General/Is_Equal_To.h"
/*!
    #include "AT/Partial_Map/Kernel.h"
!*/
    
///------------------------------------------------------------------------
/// Interface -------------------------------------------------------------
///------------------------------------------------------------------------
    
concrete_template <
	concrete_instance class D_Item,
	/*!
	    implements
		abstract_instance Is_Equal_To <D_Item>
        !*/
        concrete_instance class R_Item,
	/*!
	    implements
		abstract_instance Is_Equal_To <R_Item>
        !*/
	concrete_instance class Partial_Map_Base
	/*!
	    implements
		abstract_instance Partial_Map_Kernel <D_Item,R_Item>
        !*/
    >
class Partial_Map_Is_Equal_To_1 :
    implements
	abstract_instance General_Is_Equal_To <Partial_Map_Base>,
    extends
	concrete_instance Partial_Map_Base
{
public:

    function_body Boolean Is_Equal_To (
	    preserves General_Is_Equal_To <Partial_Map_Base>& m	    
	)
    {
       if (self.Size () != m.Size ())
       {
	   return false;
       }
       else
       {
	   object Partial_Map_Is_Equal_To_1 temp;
	   object Boolean equal_so_far = true;

	   while ((self.Size () > 0) and equal_so_far)
	   /*!
	       alters self, temp, equal_so_far
	       preserves m
	       maintains
	           for all d: D_Item where (IS_DEFINED_IN (self, d))
		       (not IS_DEFINED_IN (temp, d))  and
		   self union temp = #self union #temp  and
		   equal_so_far = (temp is subset of m)
	       decreases
		   |self|
	   !*/
	   {
	       object catalyst D_Item d;
	       object catalyst R_Item r;
	       
	       self.Undefine_Any (d, r);

	       if (not m.Is_Defined (d))
	       {
		   equal_so_far = false;
	       }
	       else
	       {
		   equal_so_far = r.Is_Equal_To(m[d]);
	       }

	       temp.Define (d, r);
	   }

	   // Put self back together as efficiently as possible
	   
	   if (self.Size () < temp.Size ())
	   {
	       self &= temp;
	   }

	   while (temp.Size () > 0)
	   /*!
	       alters self, temp
	       maintains
	           for all d: D_Item where (IS_DEFINED_IN (temp, d))
		       (not IS_DEFINED_IN (self, d))  and
		   self union temp = #self union #temp
	       decreases
		   |temp|
	   !*/
	   {
	       object catalyst D_Item d;
	       object catalyst R_Item r;

	       temp.Undefine_Any (d, r);
	       self.Define (d, r);
	   }

	   return equal_so_far;
       }
    }

};

#endif // CT_PARTIAL_MAP_IS_EQUAL_TO_1