#include <vcc.h>

#include "xListMap.h" 


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

void setItemValue(xListItem *li, unsigned value)
{
	_(unwrap li )
	li->xItemValue = value;
	_(wrap li) 
}
unsigned getItemValue(xListItem *li)
{
	unsigned value;
	value = li->xItemValue;
	return value;
}
unsigned listIsEmpty(xMap *xList)
{
	return (xList->length==0) ? 1 : 0;
}

unsigned currentLength(xMap *xList)
{
	return xList->length;
}
TCB *getOwnerOfFirstEntry(xMap *xList)
{
	TCB *result;
	_(assume result == xList->list[0]->pvOwner )
	return result;
}
void rotateLeft(xMap *xList)
{
	_(unwrap xList)
	_(ghost xList->list = \lambda unsigned i; 
		(i<xList->length)	
			?	( (i!=xList->length-1)	
					?	xList->list[i+1]	
					:	xList->list[0] 
				)
			:	(xListItem *) NULL
	 )
	_(ghost xList->position = \lambda xListItem *li; 
		( li \in xList->\owns )	
			?	( ( li==\old(xList->list[0]) )	
					?	xList->length-1		
					:	xList->position[li]-1 
				)
			:	(unsigned) maxNumVal
	 )
	_(wrap xList)
}
TCB* getOwnerOfNextEntry(xMap *xList)
{	
	TCB *result;
	_(unwrap xList)
	_(assume result == xList->list[1]->pvOwner )
	_(ghost xList->list = \lambda unsigned i; 
		(i<xList->length)	
			?	( (i!=xList->length-1)	
					?	xList->list[i+1]	
					:	xList->list[0] 
				)
			:	(xListItem *) NULL
	 )
	_(ghost xList->position = \lambda xListItem *li; 
		( li \in xList->\owns )	
			?	( ( li==\old(xList->list[0]) )	
					?	xList->length-1		
					:	xList->position[li]-1 
				)
			:	(unsigned) maxNumVal
	 )
	_(wrap xList)
	return result;
}
TCB *getOwnerOfHeadEntry(xMap *xList)
{
	TCB *result;
	_(assume result == xList->list[0]->pvOwner )
	return result;
}
unsigned containedWithin( xMap *xList, xListItem *li )
{
	unsigned result;
	_(assume result ==
		(	( li \in xList->\owns )
		)
	 )
	return result;
}
void listInitialise( xMap *xList 
		_(ghost enum xListType type) )
{
	//xList->length = 0;
	_(ghost xList->\owns={} )
	_(ghost xList->type=type )
	_(ghost xList->list = \lambda unsigned i; 
								(xListItem *)NULL )
	_(ghost xList->position = 
			\lambda xListItem *li; (unsigned) maxNumVal )
	_(wrap xList)
}
void listInsertEnd(xMap *xList, xListItem *li)
{
	
	_(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++;
	_(wrap xList)
}
void listInsert(xMap *xList, xListItem *li)
{
	unsigned index,xValue;
	_(assume index<=xList->length )
	_(assume \forall unsigned i; 
		(	( ( i < index ) && ( i<xList->length ) ) ==> 
			( xList->list[i]->xItemValue <= li->xItemValue ) 
		)  
	 )
	_(assume \forall unsigned i; 
		(	(	( i >= index ) && 
				( i<xList->length ) 
			) ==> ( xList->list[i]->xItemValue > li->xItemValue ) 
		)  
	 )
	_(unwrapping xList)
	{	
		_(ghost xList->list = \lambda unsigned i; 
				( i<=xList->length ) 
					? (		( i < index ) 
								?	xList->list[i] 
								: ( ( i == index ) 
									?	li 
									: xList->list[i-1] 
								  ) 
					  ) 
					: (xListItem*) NULL
		 )
		_(unwrap li )
			li->pvContainer = xList;
			xList->length++;
		_(wrap li )
		
		_(ghost xList->\owns += li )
		_(ghost xList->position = \lambda xListItem *xli;
				( xli \in xList->\owns ) 
					?	(	( xli == li ) 
								?	index
								:	( (	xList->position[xli] < index ) 
										?	xList->position[xli] 
										:	xList->position[xli]+1 
									) 
						)
					:  (unsigned) maxNumVal 
		 )
		 
	}
}
void listRemove(xMap *xList, xListItem *li)
{
	_(ghost unsigned index=xList->position[li] )
	_(unwrap xList)
	_(ghost xList->list = \lambda unsigned i; 
				(i<xList->length) 
					?	( ( i < index ) 
							?	xList->list[i] 
							: xList->list[i+1] 
						)
					: (xListItem *) NULL
	 )
	_(ghost xList->\owns -= li )
	_(unwrap li)
	li->pvContainer=NULL;
	_(wrap li)
	_(ghost xList->position = \lambda xListItem *xli; 
		( xli \in xList->\owns ) 
			?	(	( xList->position[xli] < index ) 
					?	xList->position[xli] 
					:	xList->position[xli]-1 
				)
			: (unsigned) maxNumVal
	 )
	xList->length--;
	_(wrap xList)
}