#pragma once
#include <stdio.h> // REMOVE THIS AFTER DEBUGGING


struct Colable {
	struct Colable * next;										// next node in the list
	// invariant: (next != 0) <=> listed()
};
#ifdef __cforall
static inline {
	// PUBLIC

	void ?{}( Colable & co ) with( co ) {
		next = 0p;
	} // post: ! listed()

	// return true iff *this is an element of a collection
	bool listed( Colable & co ) with( co ) {			// pre: this != 0
		return next != 0p;
	}

	Colable & getNext( Colable & co ) with( co ) {
		return *next;
	}

	// PRIVATE

	Colable *& Next( Colable * cp ) {
		return cp->next;
	}

	// // wrappers to make Collection have T
	// forall( T & ) {
	// 	T *& Next( T * n ) {
	// 		return (T *)Next( (Colable *)n );
	// 	}
	// } // distribution
} // distribution

forall( T & | { T *& Next ( T * ); } ) {
	bool listed( T * n ) {
		return Next( n ) != 0p;
	}
}

struct Collection {
	void * root;										// pointer to root element of list
};

static inline {
	// class invariant: root == 0 & empty() | *root in *this
	void ?{}( Collection &, const Collection & ) = void; // no copy
	Collection & ?=?( const Collection & ) = void;		// no assignment

	void ?{}( Collection & collection ) with( collection ) {	
		root = 0p;
	} // post: empty()

	bool empty( Collection & collection ) with( collection ) { // 0 <=> *this contains no elements
		return root == 0p;
	}

	void * head( Collection & collection ) with( collection ) {
		return root;
	} // post: empty() & head() == 0 | !empty() & head() in *this
} // distribution


struct ColIter {
	void * curr;										// element returned by |
};

static inline {
	void ?{}( ColIter & colIter ) with( colIter ) {
		curr = 0p;
	} // post: elts = null

	forall( T & ) {
		T * Curr( ColIter & ci ) with( ci ) {
			return (T *)curr;
		}
	} // distribution
} // distribution
#endif