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

#ifndef CT_WORD_OCCURRENCE_KERNEL_1
#define CT_WORD_OCCURRENCE_KERNEL_1 1

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

#include "AT/Word_Occurrence/Kernel.h"
#include "RESOLVE_Foundation.h"
#include "AT/General/Is_Equal_To.h"
#include "CI/Text/Are_In_Order_1.h"
#include "CT/Queue/Kernel_1a.h"

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

concrete_template <
    concrete_instance class Item,
	/*!
	    implements
		abstract_instance General_Is_Equal_To <Item, Item>
	!*/
        concrete_instance class Item_Pair =
            Record <
		    Item, 
		    Integer
                >,
        concrete_instance class Queue_Of_Item_Pair =
            Queue_Kernel_1a <Item_Pair>,
	concrete_instance class Rep =
            Representation <
                    Queue_Of_Item_Pair,
		    Integer
                >
    >
class Word_Occurrence_Kernel_1 :
    implements
	abstract_instance Word_Occurrence_Kernel <Item>,
    encapsulates
	concrete_instance Rep
{
private:

    rep_field_name (Rep, 0, Queue_Of_Item_Pair, word_queue);
    rep_field_name (Rep, 1, Integer, total);

    field_name (Item_Pair, 0, Item, word);
    field_name (Item_Pair, 1, Integer, count);
    
    /*!
	convention
	    for all d1, d2: Item, r1, r2: Integer,
		a, b, c: string of (Item, Integer)
		    where (self.word_queue =
			       a * <(d1,r1)> * b * <(d2,r2)> * c)
		(d1 /= d2)
		
	correspondence
	    self = elements (self.word_queue)
    !*/

    local_procedure_body Move_To_Front (
	    alters Queue_Of_Item_Pair& q,
	    preserves Item& d
	)
    /*!
	ensures
	    q is permutation of #q  and
	    (if IS_DEFINED_IN (elements (q), d)
	     then there exists r: Integer (<(d,r)> is prefix of q)
    !*/
    {
	object Integer words_left_to_check = q.Length ();

	while (words_left_to_check > 0)
	/*!
	    alters q, words_left_to_check
	    maintains
		q is permutation of #q  and
		there exists a, b: string of (Item, Integer)
		    (q = a * b  and
		     |a| = words_left_to_check  and
		     not IS_DEFINED_IN (elements (b), d))
	    decreases
	        words_left_to_check
	!*/
	{
	    if (d.Is_Equal_To (q[current][word]))
	    {
		return;
	    }
	    else
	    {
		object catalyst Item_Pair temp;

		q.Dequeue (temp);
		q.Enqueue (temp);
		words_left_to_check--;
	    }
	}
    }

public:

    standard_concrete_operations (Word_Occurrence_Kernel_1);

    procedure_body Add (
	    consumes Item& d
	)
    {
	object Integer r = 1;
	object Item_Pair temp;
	if( self[word_queue].Is_Defined(d))
	{
	    self[word_queue][current][count]++;
	}
	else
	{
	    temp[word] &= d;
	    temp[count] &= r;
	    self[word_queue].Enqueue (temp);
	}
	self[total]++;
    }

    procedure_body Remove (
            preserves Item& d,
	    produces Item& d_copy,
            produces Integer& r
	)
    {
	object Item_Pair temp;
	Move_To_Front(self[word_queue], d);
	self[word_queue].Dequeue(temp);
	temp[word] &= d_copy;
	temp[count] &= r;
    }

    procedure_body Remove_Any (
	    produces Item& d,
	    produces Integer& r
	)
    {
	object Item_Pair temp;
	self[word_queue].Dequeue(temp);
	temp[word] &= d;
	temp[count] &= r;
    }

    function_body Boolean Is_Defined (
	    preserves Item& d
	)
    {
	if (self[word_queue].Length () == 0)
	{
	    return false;
	}
	else
	{
	    Move_To_Front (self[word_queue], d);
	    return (d.Is_Equal_To (self[word_queue][current][word]));
	}
    }

    function_body Integer& operator [] (
	    preserves Item& d
	)
    {
	Move_To_Front (self[word_queue], d);
	return self[word_queue][current][count];
    }

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

    function_body Integer Total()
    {
	return self[total];
    }

};

#endif // CT_WORD_OCCURRENCE_KERNEL_1