#pragma once

#include "bits/collection.hfa"
#include "bits/defs.hfa"

struct Seqable {
	__cfa_anonymous_object(Colable);
	struct Seqable * back;										// pointer to previous node in the list
};

#ifdef __cforall
static inline {
	// PUBLIC

	void ?{}( Seqable & sq ) with( sq ) {
		((Colable &)sq){};
		back = 0p;
	} // post: ! listed()

	Seqable & getBack( Seqable & sq ) with( sq ) {
		return *back;
	}

	// PRIVATE

	Seqable *& Back( Seqable * sq ) {
		return sq->back;
	}

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


// A Sequence(T) is a Collection(T) defining the ordering of a uStack and uQueue, and to insert and remove elements
// anywhere in the sequence. T must be a public descendant of uSeqable.

// The implementation is a typical doubly-linked list, except the next field of the last node points at the first node
// and the back field of the last node points at the first node (circular).

forall( T & | { T *& Back ( T * ); T *& Next ( T * ); } ) {
	struct Sequence {
		inline Collection;								// Plan 9 inheritance
	};

	static inline {
		// wrappers to make Collection have T
		T & head( Sequence(T) & s ) with( s ) {
			return *(T *)head( (Collection &)s );
		} // post: empty() & head() == 0 | !empty() & head() in *s

		void ?{}( Sequence(T) &, const Sequence(T) & ) = void; // no copy
		Sequence(T) & ?=?( const Sequence(T) & ) = void; // no assignment

		void ?{}( Sequence(T) & s ) with( s ) {	
			((Collection &)s){};
		}	// post: isEmpty()

		// Return a pointer to the last sequence element, without removing it.
		T & tail( Sequence(T) & s ) with( s ) {
			return root ? (T &)*Back( &head( s ) ) : *0p;
		}	// post: empty() & tail() == 0 | !empty() & tail() in *s

		// Return a pointer to the element after *n, or 0p if list empty.
		T * succ( Sequence(T) & s, T * n ) with( s ) {	// pre: *n in *s
			#ifdef __CFA_DEBUG__
			if ( ! listed( n ) ) abort( "(Sequence &)%p.succ( %p ) : Node is not on a list.", &s, n );
			#endif // __CFA_DEBUG__
			return Next( n ) == &head( s ) ? 0p : Next( n );
		} // post: n == tail() & succ(n) == 0 | n != tail() & *succ(n) in *s

		// Return a pointer to the element before *n, or 0p if list empty.
		T * pred( Sequence(T) & s, T * n ) with( s ) {	// pre: *n in *s
			#ifdef __CFA_DEBUG__
			if ( ! listed( n ) ) abort( "(Sequence &)%p.pred( %p ) : Node is not on a list.", &s, n );
			#endif // __CFA_DEBUG__
			return n == &head( s ) ? 0p : Back( n );
		} // post: n == head() & head(n) == 0 | n != head() & *pred(n) in *s


		// Insert *n into the sequence before *bef, or at the end if bef == 0p.
		T & insertBef( Sequence(T) & s, T & n, T & bef ) with( s ) { // pre: !n->listed() & *bef in *s
			#ifdef __CFA_DEBUG__
			if ( listed( &n ) ) abort( "(Sequence &)%p.insertBef( %p, %p ) : Node is already on another list.", &s, n, &bef );
			#endif // __CFA_DEBUG__
			if ( &bef == &head( s ) ) {					// must change root
				if ( root ) {
					Next( &n ) = &head( s );
					Back( &n ) = Back( &head( s ) );
					// inserted node must be consistent before it is seen
					asm( "" : : : "memory" );			// prevent code movement across barrier
					Back( &head( s ) ) = &n;
					Next( Back( &n ) ) = &n;
				} else {
					Next( &n ) = &n;
					Back( &n ) = &n;
				} // if
				// inserted node must be consistent before it is seen
				asm( "" : : : "memory" );				// prevent code movement across barrier
				root = &n;
			} else {
				if ( ! &bef ) &bef = &head( s );
				Next( &n ) = &bef;
				Back( &n ) = Back( &bef );
				// inserted node must be consistent before it is seen
				asm( "" : : : "memory" );				// prevent code movement across barrier
				Back( &bef ) = &n;
				Next( Back( &n ) ) = &n;
			} // if
			return n;
		}	// post: n->listed() & *n in *s & succ(n) == bef


		// Insert *n into the sequence after *aft, or at the beginning if aft == 0.
		T & insertAft( Sequence(T) & s, T & aft, T & n ) with( s ) {	// pre: !n->listed() & *aft in *s
			#ifdef __CFA_DEBUG__
			if ( listed( &n ) ) abort( "(Sequence &)%p.insertAft( %p, %p ) : Node is already on another list.", &s, &aft, &n );
			#endif // __CFA_DEBUG__
			if ( ! &aft ) {								// must change root
				if ( root ) {
					Next( &n ) = &head( s );
					Back( &n ) = Back( &head( s ) );
					// inserted node must be consistent before it is seen
					asm( "" : : : "memory" );			// prevent code movement across barrier
					Back( &head( s ) ) = &n;
					Next( Back( &n ) ) = &n;
				} else {
					Next( &n ) = &n;
					Back( &n ) = &n;
				} // if
				asm( "" : : : "memory" );				// prevent code movement across barrier
				root = &n;
			} else {
				Next( &n ) = Next( &aft );
				Back( &n ) = &aft;
				// inserted node must be consistent before it is seen
				asm( "" : : : "memory" );				// prevent code movement across barrier
				Back( Next( &n ) ) = &n;
				Next( &aft ) = &n;
			} // if
			return n;
		} // post: n->listed() & *n in *s & succ(n) == bef
		
		// pre: n->listed() & *n in *s
		T & remove( Sequence(T) & s, T & n ) with( s ) { // O(1)
			#ifdef __CFA_DEBUG__
			if ( ! listed( &n ) ) abort( "(Sequence &)%p.remove( %p ) : Node is not on a list.", &s, &n );
			#endif // __CFA_DEBUG__
			if ( &n == &head( s ) ) {
				if ( Next( &head( s ) ) == &head( s ) ) root = 0p;
				else root = Next( &head( s ) );
			} // if
			Back( Next( &n ) ) = Back( &n );
			Next( Back( &n ) ) = Next( &n );
			Next( &n ) = Back( &n ) = 0p;
			return n;
		} // post: !n->listed()

		// Add an element to the head of the sequence.
		T & addHead( Sequence(T) & s, T & n ) {			// pre: !n->listed(); post: n->listed() & head() == n
			return insertAft( s, *0p, n );
		}

		// Add an element to the tail of the sequence.
		T & addTail( Sequence(T) & s, T & n ) {			// pre: !n->listed(); post: n->listed() & head() == n
			return insertBef( s, n, *0p );
		}

		// Add an element to the tail of the sequence.
		T & add( Sequence(T) & s, T & n ) {				// pre: !n->listed(); post: n->listed() & head() == n
			return addTail( s, n );
		}

		// Remove and return the head element in the sequence.
		T & dropHead( Sequence(T) & s ) {
			T & n = head( s );
			return &n ? remove( s, n ), n : *0p;
		}

		// Remove and return the head element in the sequence.
		T & drop( Sequence(T) & s ) {
			return dropHead( s );
		}

		// Remove and return the tail element in the sequence.
		T & dropTail( Sequence(T) & s ) {
			T & n = tail( s );
			return &n ? remove( s, n ), n : *0p;
		}

		// Transfer the "from" list to the end of s sequence; the "from" list is empty after the transfer.
		void transfer( Sequence(T) & s, Sequence(T) & from ) with( s ) {
			if ( empty( from ) ) return;				// "from" list empty ?
			if ( empty( s ) ) {							// "to" list empty ?
				root = from.root;
			} else {									// "to" list not empty
				T * toEnd = Back( &head( s ) );
				T * fromEnd = Back( &head( from ) );
				Back( (T *)root ) = fromEnd;
				Next( fromEnd ) = &head( s );
				Back( (T *)from.root ) = toEnd;
				Next( toEnd ) = &head( from );
			} // if
			from.root = 0p;								// mark "from" list empty
		}

		// Transfer the "from" list up to node "n" to the end of s list; the "from" list becomes the sequence after node "n".
		// Node "n" must be in the "from" list.
		void split( Sequence(T) & s, Sequence(T) & from, T & n ) with( s ) {
			#ifdef __CFA_DEBUG__
			if ( ! listed( &n ) ) abort( "(Sequence &)%p.split( %p ) : Node is not on a list.", &s, &n );
			#endif // __CFA_DEBUG__
			Sequence(T) to;
			to.root = from.root;						// start of "to" list
			from.root = Next( &n );						// start of "from" list
			if ( to.root == from.root ) {				// last node in list ?
				from.root = 0p;							// mark "from" list empty
			} else {
				Back( &head( from ) ) = Back( &head( to ) ); // fix "from" list
		 		Next( Back( &head( to ) ) ) = &head( from );
				Next( &n ) = &head( to );				// fix "to" list
				Back( &head( to ) ) = &n;
			} // if
			transfer( s, to );
		}
	} // distribution
} // distribution

forall( T & | { T *& Back ( T * ); T *& Next ( T * ); } ) {
	// SeqIter(T) is used to iterate over a Sequence(T) in head-to-tail order.
	struct SeqIter {
		inline ColIter;
		// The Sequence must be passed to pred and succ to check for the end of the Sequence and return 0p. Without
		// passing the sequence, traversing would require its length. Thus the iterator needs a pointer to the sequence
		// to pass to succ/pred. Both stack and queue just encounter 0p since the lists are not circular.
		Sequence(T) * seq;								// FIX ME: cannot be reference
	};

	static inline {
		void ?{}( SeqIter(T) & si ) with( si ) {
			((ColIter &)si){};
			seq = 0p;
		} // post: elts = null

		// Create a iterator active in sequence s.
		void ?{}( SeqIter(T) & si, Sequence(T) & s ) with( si ) {
			((ColIter &)si){};
			seq = &s;
			curr = &head( s );
		} // post: elts = null

		void ?{}( SeqIter(T) & si, Sequence(T) & s, T & start ) with( si ) {
			((ColIter &)si){};
			seq = &s;
			curr = &start;
		} // post: elts = null

		// Make the iterator active in sequence s.
		void over( SeqIter(T) & si, Sequence(T) & s ) with( si ) {
			seq = &s;
			curr = &head( s );
		} // post: elts = {e in s}

		bool ?|?( SeqIter(T) & si, T && tp ) with( si ) {
			if ( curr ) {
				&tp = Curr( si );
				T * n = succ( *seq, Curr( si ) );
				curr = n == &head( *seq ) ? 0p : n;
			} else &tp = 0p;
			return &tp != 0p;
		}
	} // distribution


	// A SeqIterRev(T) is used to iterate over a Sequence(T) in tail-to-head order.
	struct SeqIterRev {
		inline ColIter;
		// See above for explanation.
		Sequence(T) * seq;								// FIX ME: cannot be reference
	};

	static inline {
		void ?{}( SeqIterRev(T) & si ) with( si ) {	
			((ColIter &)si){};
			seq = 0p;
		} // post: elts = null

		// Create a iterator active in sequence s.
		void ?{}( SeqIterRev(T) & si, Sequence(T) & s ) with( si ) {	
			((ColIter &)si){};
			seq = &s;
			curr = &tail( s );
		} // post: elts = null

		void ?{}( SeqIterRev(T) & si, Sequence(T) & s, T & start ) with( si ) {	
			((ColIter &)si){};
			seq = &s;
			curr = &start;
		} // post: elts = null

		// Make the iterator active in sequence s.
		void over( SeqIterRev(T) & si, Sequence(T) & s ) with( si ) {
			seq = &s;
			curr = &tail( s );
		} // post: elts = {e in s}

		bool ?|?( SeqIterRev(T) & si, T && tp ) with( si ) {
			if ( curr ) {
				&tp = Curr( si );
				T * n = pred( *seq, Curr( si ) );
				curr = n == &tail( *seq ) ? 0p : n;
			} else &tp = 0p;
			return &tp != 0p;
		}
	} // distribution
} // distribution

#endif