#include <vcc.h>
#include "xListJoint.h"

void listInitialiseItem(xListItem *li)
{
	CHECK_PRECONDITION();

	_(unwrap li)
	li->pvContainer = NULL;
	_(wrap li)
}
void setItemOwner(xListItem *li, TCB *task)
{
	CHECK_PRECONDITION();

	_(unwrap li)
	li->pvOwner = task;
	li->ownersPriority = task->uxPriority;
	_(wrap li)
}

void setItemValue(xListItem *li, unsigned value)
{
	CHECK_PRECONDITION();

	_(unwrap li )
	li->xItemValue = value;
	_(wrap li) 
}
unsigned getItemValue(xListItem *li)
{
	CHECK_PRECONDITION();

	unsigned value;
	value = li->xItemValue;
	return value;
}
unsigned listIsEmpty(xMap *xList)
{
	CHECK_PRECONDITION();

	return (xList->length==0) ? 1 : 0;
}

unsigned currentLength(xMap *xList)
{
	CHECK_PRECONDITION();

	return xList->length;
}
TCB *getOwnerOfFirstEntry(xMap *xList)
{
	CHECK_PRECONDITION();

	TCB *result;
	_(assume result == xList->list[0]->pvOwner )
	return result;
}
void rotateLeft(xMap *xList)
{
	CHECK_PRECONDITION();

	_(unwrap xList)
	_(assert xList->list[ZERO] \in xList->\owns) //HELPS PROVER

	_(ghost{ //GHOST BLOCK STARTS HERE

		xListItem *firstElement = xList->list[ZERO]; // HELPS PROVER
		
		xList->list = (\lambda unsigned i;				( i >= xList->length )	
													?	( xList->list[i] ) 
													:	( 
															(i == xList->length - 1)
														?	( firstElement )
														:	( xList->list[i + 1] )
														)
													);
		
		xList->position = (\lambda xListItem *xli;		( xList->position[ xli ] >= xList->length )	
													?	( xList->position[ xli ] ) 
													:	(
															(xli == firstElement)
														?	(xList->length - 1)
														:	(xList->position[ xli ] - 1) 
														)
													);

	}) //GHOST BLOCK ENDS HERE

	xMap * const pxConstList = xList;
	pxConstList->pxIndex = pxConstList->pxIndex->pxNext;
	if( pxConstList->pxIndex == (&(pxConstList->xListEnd)) )
	{
		pxConstList->pxIndex = (pxConstList->pxIndex)->pxNext;
	}
	_(assert pxConstList->pxIndex \in pxConstList->\owns)
	_(wrap xList)
}

TCB* getOwnerOfNextEntry(xMap *xList)
{
	CHECK_PRECONDITION();

	TCB *result;
	_(ghost TCB *ghost_result) 
	
	_(assume result == xList->list[1]->pvOwner )
	_(assert xList->list[ZERO] \in xList->\owns) //HELPS PROVER

	_(unwrap xList)
	_(ghost{ //GHOST BLOCK STARTS HERE
		_(assert \forall xListItem *A; 
			( (A \in xList->\owns) && (A != &(xList->xListEnd))) ==> (xList->list[xList->position[A]] == A)
		)

		xListItem *firstElement = xList->list[ZERO]; // HELPS PROVER

		xList->list = (\lambda unsigned i;				( i >= xList->length )	
													?	( xList->list[i] ) 
													:	( 
															(i == xList->length - 1)
														?	( firstElement )
														:	( xList->list[i + 1] )
														)
													);
		
		xList->position = (\lambda xListItem *xli;		( xList->position[ xli ] >= xList->length )	
													?	( xList->position[ xli ] ) 
													:	(
															(xli == firstElement)
														?	(xList->length - 1)
														:	(xList->position[ xli ] - 1) 
														)
													);
	}) //GHOST BLOCK ENDS HERE

	xMap * const pxConstList = xList;
	pxConstList->pxIndex = pxConstList->pxIndex->pxNext;
	if( pxConstList->pxIndex == (&(pxConstList->xListEnd)) )
	{
		pxConstList->pxIndex = (pxConstList->pxIndex)->pxNext;
	}
	_(assert pxConstList->pxIndex \in pxConstList->\owns)
	_(wrap xList)
	return result;
}
TCB *getOwnerOfHeadEntry(xMap *xList)
{
	CHECK_PRECONDITION();

	TCB *result;
	_(assume result == xList->list[0]->pvOwner )
	return result;
}
unsigned containedWithin( xMap *xList, xListItem *li )
{
	CHECK_PRECONDITION();

	unsigned result;
	_(assume result ==
		(	( li \in xList->\owns )
		)
	 )
	return result;
}
void listInitialise( xMap *xList _(ghost enum xListType type) )
{
	CHECK_PRECONDITION();

	_(ghost xList->\owns={} )
	_(ghost xList->type=type )
	_(ghost xList->list = \lambda unsigned i; 
								(xListItem *)NULL )
	_(ghost xList->position = \lambda xListItem *li; (unsigned) maxNumVal )

	/* The concrete method that is taken from xlist implementation */
	_(unwrap (&(xList->xListEnd)))
		xList->pxIndex = (xListItem *)&( xList->xListEnd );
		xList->xListEnd.xItemValue = maxNumVal;
		xList->xListEnd.pxNext = (xListItem *)&( xList->xListEnd );
		xList->xListEnd.pxPrevious = (xListItem *)&( xList->xListEnd );

		xList->uxNumberOfItems = 0;

		xList->xListEnd.pvOwner = NULL;
		xList->xListEnd.pvContainer = xList;
		xList->xListEnd.ownersPriority = ZERO;
	_(wrap (&(xList->xListEnd)))
	_(ghost {
		
		xList->\owns = {xList->pxIndex};
		xList->index[(xListItem *)&xList->xListEnd] = 0;
	})

	_(wrap xList)
}
void listInsertEnd(xMap *xList, xListItem *li)
{
	CHECK_PRECONDITION();
	_(unwrap xList )
		_(ghost xList->list[xList->length] = li )
		_(unwrap li )
			li->pvContainer = xList;
		_(wrap li )
		_(ghost xList->\owns += li )
		_(ghost xList->position[li] =  xList->length )	
		xList->length++;



		xListItem *pxIndex;
		pxIndex = xList->pxIndex;
		_(assert pxIndex->pxNext \in xList->\owns)
		_(assert pxIndex->pxPrevious \in xList->\owns)
		_(unwrapping li ){
		li->pxNext = pxIndex->pxNext;
		li->pxPrevious = xList->pxIndex;
		}
		_(unwrapping pxIndex->pxNext){
			(pxIndex->pxNext)->pxPrevious = li;
		}
		_(unwrapping pxIndex){
			pxIndex->pxNext = li;
		}
		_(unwrapping li ){
			li->pvContainer = xList;
		}
		xList->pxIndex = li;
		(xList->uxNumberOfItems)++;

		_(ghost{
			//xList->\owns += li;
			//#ANIRUDH: Commenting above statement as we have already added to the set
			if(li->pxPrevious == (&xList->xListEnd)){
				xList->index = (\lambda xListItem *p; (p == li)? 0:(xList->index[p] + 1 ));
			}else{
				xList->index = (\lambda xListItem *p; (p == li)? (xList->index[pxIndex]+1):
					( (xList->index[p] <= xList->index[pxIndex]) ? (xList->index[p]) : (xList->index[p] + 1))	
					);
			}
		})


	_(wrap xList)
}
void listInsert(xMap *xList, xListItem *li)
{
	CHECK_PRECONDITION();
	
	/* FIND THE CORRECT POSITION FOR THE XMAP BEFORE UNWRAPPING XLIST*/
	_(assert !(li \in xList->\owns))
	_(ghost unsigned index)
	_(ghost{
		index = ZERO;
		if(xList->length == ZERO){
			index = ZERO;
		}else{
			if (li->xItemValue == maxNumVal){
				index = xList->length;
			}else{
				for( index = ZERO; index < xList->length ; index++)
					_(invariant \wrapped( xList ))
					_(invariant (index < xList->length) ==> (xList->list[index] \in xList->\owns) )
					_(invariant index <= xList->length )
					_(invariant (xList->type == PQ) ==>(\forall unsigned i; ( (i < index) ==> (xList->list[i]->xItemValue <= li->xItemValue))))
				{
					unsigned value;
					_(assume value == xList->list[index]->xItemValue)
						if(value > li->xItemValue){
							_(assert (xList->type == PQ) ==> ( \forall unsigned i ; ((i >= index) && (i < xList->length) )
								==> ( (xList->list[i] \in xList->\owns) && (xList->list[i]->xItemValue > li->xItemValue) ) )
								)
								break;
						}
				}
			}
		}

	})

	/* FIND THE CORRECT POSITION USING THE XLIST METHOD */
	xListItem *pxIterator;
	unsigned xValueOfInsertion;
	xValueOfInsertion = li->xItemValue;
	_(assert ( (&xList->xListEnd) \in xList->\owns))

	/*FIND THE CORRECT ITEM TO INSERT AFTER*/
	if( xValueOfInsertion >= maxNumVal )
	{
		pxIterator = xList->xListEnd.pxPrevious;
		_(assert (pxIterator \in xList->\owns))
	}
	else
	{	
		for(pxIterator = ( xListItem * )&(xList->xListEnd);pxIterator->pxNext->xItemValue <= xValueOfInsertion ; pxIterator = ( xListItem * )pxIterator->pxNext )	
			_(invariant pxIterator \in xList->\owns)
			_(invariant pxIterator->pxNext \in xList->\owns)
			_(invariant \wrapped(xList))
			_(invariant (pxIterator->xItemValue > xValueOfInsertion ) ==> ( pxIterator == (&(xList->xListEnd))))
			_(invariant (pxIterator == (&(xList->xListEnd)) || (pxIterator->xItemValue <= xValueOfInsertion )) )
		{
		}

	}



	
	_(unwrap xList)
		_(assert xList->position[&(xList->xListEnd)] == maxNumVal)
		_(assert index <= xList->length)
		_(ghost{
			xList->list = ( \lambda unsigned i;		( (i > index) && (i <= xList->length))
												?	( xList->list[i-1] )
												:	(
														( i == index )
													?	( li )
													:	( xList->list[i] )
													)
							);

			xList->position = (\lambda xListItem *xli;	( (xList->position[ xli ] >= index) && ( xList->position[xli] < xList->length))
													?	( xList->position[ xli ] + 1 )
													:	(
															( xli == li )
														?	( index )
														:	( xList->position[ xli ] )
														)
							  );

			xList->\owns += li;
		})
		_(assert xList->position[li] == index)
		_(unwrapping li ){
			li->pvContainer = xList;
		}	
		xList->length++;

		/* XLIST METHOD CODE */

		_(assert pxIterator \in xList->\owns)
		_(assert pxIterator->pxNext \in xList->\owns)

		_(unwrapping li){
			li->pxNext = pxIterator->pxNext;
		}
		_(unwrapping li->pxNext){
			li->pxNext->pxPrevious = li;
		}
		_(unwrapping li){
		li->pxPrevious = pxIterator;
		}
		_(unwrapping pxIterator){
			pxIterator->pxNext =  li;
		}
		_(unwrapping li){
		li->pvContainer =  xList;
		}
		
		( xList->uxNumberOfItems )++;

		_(ghost {
			//xlist->\owns += xli; //ALREADY DONE BY ABOVE CODE
			if(pxIterator != (&xList->xListEnd)){
				xList->index = (\lambda xListItem *p; (p == li)? (xList->index[pxIterator]+1):
					( (xList->index[p] <= xList->index[pxIterator]) ? (xList->index[p]) : (xList->index[p] + 1))	
					);
			}else{
				xList->index = (\lambda xListItem *p; (p == li)? 0:(xList->index[p] + 1));
			}
		})
	_(wrap xList)
}
void listRemove(xMap *xList, xListItem *li)
{
	CHECK_PRECONDITION();

	_(assert li \in xList->\owns )
	_(assert li->pxNext \in xList->\owns)
	_(assert li->pxPrevious \in xList->\owns)
	_(assert xList->position[ &xList->xListEnd ] == maxNumVal) 
	_(assert li != &xList->xListEnd)
	
	_(unwrap xList)
	_(ghost{
		unsigned index=xList->position[li];
		xList->list =(\lambda unsigned i;	(i<xList->length) 
											?	( 
													(i < index) 
												?	xList->list[i] 
												:	xList->list[i+1] 
												)

											:	NULL
		);
		
		xList->\owns -= li;
		
		xList->position = (\lambda xListItem *xli;		( ( xli \in xList->\owns ) && (xli != &(xList->xListEnd)))
													?	(	
															( xList->position[xli] < index ) 
														?	xList->position[xli] 
														:	xList->position[xli]-1 
														)

													:	(unsigned) maxNumVal
		);
	
	})//GHOST BLOCK ENDS HERE
	_(unwrap li)
		li->pvContainer=NULL;
	_(wrap li)
	xList->length--;



	/* xlist original code*/
	
	_(unwrapping li->pxNext){
		li->pxNext->pxPrevious = li->pxPrevious;
	}
	_(unwrapping li->pxPrevious){
		li->pxPrevious->pxNext = li->pxNext;	
	}
	(xList->uxNumberOfItems)--;
	if( xList->pxIndex == li ){
		xList->pxIndex = li->pxPrevious;
	}
	_(unwrapping li){
		li->pvContainer = NULL;
	}
	_(ghost {
		xList->index = (\lambda xListItem *p; 
						(xList->index[p] < xList->index[li] 
					?	(xList->index[p]) 
					:	(xList->index[p] - 1))
		);

	})

	_(wrap xList)
}


void sanityCheckFunction(xMap *list)
	_(requires \wrapped(list))
{
	CHECK_PRECONDITION();
}