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

#ifndef CT_SORTING_MACHINE_KERNEL_2
#define CT_SORTING_MACHINE_KERNEL_2 1

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

#include "AT/Sorting_Machine/Kernel.h"
#include "CT/Queue/Kernel_1a.h"
#include "CT/Array/Kernel_1.h"
#include "CT/Array/Are_In_Order_At_1.h"
#include "CT/Array/Exchange_At_1.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 Array_Of_Item =
            Array_Exchange_At_1 <
		    Item,
		    Array_Are_In_Order_At_1 <
			    Item,
			    Item_Are_In_Order,
			    Array_Kernel_1 <Item>
			>
                >,
	concrete_instance class Rep =
            Representation <
		    Boolean,
		    Queue_Of_Item,
		    Array_Of_Item,
		    Integer
		>
    >
class Sorting_Machine_Kernel_2 :
    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, queue);
    rep_field_name (Rep, 2, Array_Of_Item, array);
    rep_field_name (Rep, 3, Integer, heap_size);

    /*!
        math definition IS_ORDERED (
                s: string of Item
            ): boolean is
	    for all u, v: Item where (<u> * <v> is substring of s)
		(ARE_IN_ORDER (u, v))

        math definition LOCATIONS_OF_SUB_TREE_ELEMENTS (
		a: ARRAY_MODEL
		start: integer
		stop: integer
	    ): finite set of integer satisfies
	    if a.lb <= start <= stop <= a.ub
	    then
		LOCATIONS_OF_SUB_TREE_ELEMENTS (a,start,stop) =
		    {start} union
		    LOCATIONS_OF_SUB_TREE_ELEMENTS (a,2 * start,stop) union
		    LOCATIONS_OF_SUB_TREE_ELEMENTS (a,2 * start + 1,stop)
	    else
		LOCATIONS_OF_SUB_TREE_ELEMENTS (a,start,stop) = empty_set

        math definition SUB_TREE_ARRAY_ELEMENTS (
		a: ARRAY_MODEL
		start: integer
		stop: integer
	    ): finite multiset of Item satisfies
	    for all x: Item
		(x is in SUB_TREE_ARRAY_ELEMENTS (a, start, stop)  iff
		 there exists i: integer
		     (i is in LOCATIONS_OF_SUB_TREE_ELEMENTS (
			      a, start, stop)  and
		      (i, x) is in a.table))

	math definition SUB_TREE_IS_ORDERED (
		a: ARRAY_MODEL
		start: integer
		stop: integer
	    ): boolean satisfies
	    if a.lb <= start and 2 * start + 1 <= stop and stop <= a.ub
	    then
		for all x, y, z: Item
		where ((start, x) is in a.table  and
		       (2 * start, y) is in a.table  and
		       (2 * start + 1, z) is in a.table)
		    (SUB_TREE_IS_ORDERED (a, start, stop) =
		     SUB_TREE_IS_ORDERED (a, 2 * start, stop)  and
		     SUB_TREE_IS_ORDERED (a, 2 * start + 1, stop)  and
		     ARE_IN_ORDER (x, y)  and  ARE_IN_ORDER (x, z))
	    else if a.lb <= start and 2 * start <= stop and stop <= a.ub
	    then
		for all x, y: Item
		where ((start, x) is in a.table  and
		       (2 * start, y) is in a.table)
		    (SUB_TREE_IS_ORDERED (a, start, stop) =
		     SUB_TREE_IS_ORDERED (a, 2 * start, stop)  and
		     ARE_IN_ORDER (x, y))
	    else
		SUB_TREE_IS_ORDERED (a, start, stop) = true

	convention
	    if self.inserting_rep
	    then
		self.heap_size = 0  and
		self.array = (1, 0, empty_set)
	    else
		self.array.lb = 1  and
		0 <= self.heap_size  and
		self.heap_size <= self.array.ub  and
		SUB_TREE_IS_ORDERED (self.array, 1, self.heap_size)  and
		self.queue = empty_string

	correspondence
	    self.inserting = self.inserting_rep  and
	    if self.inserting
	    then
		self.contents = multiset_elements (self.queue)
	    else
		for all x: Item
		    (x is in self.contents  iff
		     there exists i: integer
			 (self.array.lb <= i  and
			  i <= self.heap_size  and
			  (i,x) is in self.array.table))
    !*/

    local_procedure_body Initialize ()
    {
       // Students to fill this in

	self[inserting_rep] = true;
    }

    // Add other local operations here


    local_procedure_body Arrayify (
	consumes Queue_Of_Item& queue,
	produces Array_Of_Item& array
	)
    /*!
	  requires
	      A Queue_Of_Item with .Length() > 0
	  ensures
	      There exists an Array_Of_Item with the lowest item in
	      position [1].
	      Queue_Of_Item.Length() = 0.

    !*/
    {
	object Item temp;
	object Integer count = 1;

	array.Set_Bounds (1, queue.Length());

	while (queue.Length() > 0)
	{
	    queue.Dequeue (temp);
	    array[count] &= temp;
	    count++;
	}
    }

    local_procedure_body Sift_Root_Down (
	alters Array_Of_Item& array,
	preserves Integer start,
	preserves Integer end
	)
    /*!
	  requires
	  ensures
     !*/
    {
	object Integer root = start;

	while (root * 2 <= end)
	{
	    object Integer count = (root * 2);
	    if ((count < end) and (array.Are_In_Order_At(count, count + 1)))
	    {
		count++;
	    }
	    if (array.Are_In_Order_At(root, count))
	    {
		array.Exchange_At (root, count);
		root = count;
	    }
	    else
	    {
		return;
	    }

	}
    }

    local_procedure_body Heapify (
	alters Array_Of_Item& array,
	alters Integer start
	)
    /*!
	  requires
	  ensures
     !*/
    {
	while (start > 0)
	{
	    Sift_Root_Down (array, start, self[heap_size]);
	    start--;
	}
    }



public:

    standard_concrete_operations (Sorting_Machine_Kernel_2);

    procedure_body Insert (
	    consumes Item& x
	)
    {
       // Students to fill this in

	self[queue].Enqueue(x);

    }

    procedure_body Change_To_Extraction_Phase ()
    {
       // Students to fill this in

	self[inserting_rep] = false;
	Arrayify (self[queue], self[array]);
	Heapify (self[array], self[array].Upper_Bound() / 2);
	self[heap_size] = self[array].Upper_Bound();

    }

    procedure_body Remove_First (
	    produces Item& x
	)
    {
       // Students to fill this in
	x.Clear();

	if (not self[inserting_rep])
	{
	    x &= self[array][1];
	    self[array].Exchange_At (self[array].Lower_Bound(), self[heap_size]);
	    if(self[heap_size] > 1)
	    {
		Sift_Root_Down (self[array], self[array].Lower_Bound(), self[heap_size]);
	    }
	    self[heap_size]--;
	}
    }

    procedure_body Remove_Any (
	    produces Item& x
	)
    {
       // Students to fill this in
	x.Clear();

	if (not self[inserting_rep])
	{

	    x &= self[array][self[heap_size]];
	    self[heap_size]--;
	}
	else
	{
	    self[queue].Dequeue(x);
	}
    }

    function_body Boolean Is_In_Extraction_Phase ()
    {
       // Students to fill this in

	return not self[inserting_rep];
    }

    function_body Integer Size ()
    {
       // Students to fill this in
	if (not self[inserting_rep])
	{
	    return self[heap_size];
	}
	else
	{
	    return (self[queue].Length());
	}
    }

};

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

#endif // CT_SORTING_MACHINE_KERNEL_2