indexing
	description: "Circular containers"
	names: circular_buffer, buffer, circular
	access: cursor
	author: "Patrick Schoenbach"

deferred class interface
	CIRCULAR_CONTAINER [G]

feature -- Access

	first: INTEGER
			-- Index of first element

	i_th (i: INTEGER): G
			-- i-th item
			-- (from SEQUENCIAL_CONTAINER)
		require -- from SEQUENCIAL_CONTAINER
			valid_index: valid_index (i)

	index: INTEGER
			-- Current index
			-- (from SEQUENCIAL_CONTAINER)

	item: G
			-- Current item
			-- (from SEQUENCIAL_CONTAINER)
		require -- from SEQUENCIAL_CONTAINER
			not_off: not off

	last: INTEGER
			-- Index of last element

	sentinels: INTEGER
			-- Number of sentinel items
		ensure
			sentinels_non_negative: Result >= 0
	
feature -- Measurement

	capacity: INTEGER
			-- Size of container
			-- (from SEQUENCIAL_CONTAINER)

	count: INTEGER
			-- Number of elements
			-- (from SEQUENCIAL_CONTAINER)
	
feature -- Status report

	after: BOOLEAN
			-- Is there no valid cursor position to the right of cursor?
			-- (from SEQUENCIAL_CONTAINER)

	before: BOOLEAN
			-- Is there no valid cursor position to the left of cursor?
			-- (from TWO_WAY_SEQUENCIAL_CONTAINER)

	empty: BOOLEAN
			-- Is container empty?
			-- (from SEQUENCIAL_CONTAINER)

	full: BOOLEAN
			-- Is container full?
			-- (from SEQUENCIAL_CONTAINER)

	insertable: BOOLEAN
			-- Can elements be inserted in the middle?
			-- (from SEQUENCIAL_CONTAINER)

	isfirst: BOOLEAN
			-- Is cursor on first element?
			-- (from SEQUENCIAL_CONTAINER)

	islast: BOOLEAN
			-- Is cursor on last element?
			-- (from SEQUENCIAL_CONTAINER)

	next (i: INTEGER): INTEGER
			-- Index of next item
		require
			valid_index: valid_index (i)

	off: BOOLEAN
			-- Is there no current item?
			-- (from SEQUENCIAL_CONTAINER)

	previous (i: INTEGER): INTEGER
			-- Index of previous item
		require
			valid_index: valid_index (i)

	prunable: BOOLEAN
			-- Is container prunable?
			-- (from SEQUENCIAL_CONTAINER)

	resizable: BOOLEAN
			-- Is container resizable?
			-- (from SEQUENCIAL_CONTAINER)

	valid_index (i: INTEGER): BOOLEAN
			-- Is index i valid?
			-- (from SEQUENCIAL_CONTAINER)
	
feature -- Cursor movement

	back
			-- Move cursor backwards.
		require -- from TWO_WAY_SEQUENCIAL_CONTAINER
			not_before: not before
		ensure then
			previous_position: index = previous (old index)

	finish
			-- Move cursor to last element.
			-- (from TWO_WAY_SEQUENCIAL_CONTAINER)
		require -- from TWO_WAY_SEQUENCIAL_CONTAINER
			not_empty: not empty
		ensure -- from TWO_WAY_SEQUENCIAL_CONTAINER
			cursor_at_end: islast

	forth
			-- Move cursor forwards.
		require -- from SEQUENCIAL_CONTAINER
			not_after: not after
		ensure then
			next_position: index = next (old index)

	go_i_th (i: INTEGER)
			-- Move cursor to the i-th position.
			-- (from SEQUENCIAL_CONTAINER)
		require -- from SEQUENCIAL_CONTAINER
			valid_index: valid_index (i)
		ensure -- from SEQUENCIAL_CONTAINER
			i_th_position: index = i

	start
			-- Move cursor to first element.
			-- (from SEQUENCIAL_CONTAINER)
		require -- from SEQUENCIAL_CONTAINER
			not_empty: not empty
		ensure -- from SEQUENCIAL_CONTAINER
			cursor_at_start: isfirst
	
feature -- Element change

	extend (v: like item)
			-- Add v to end of buffer.
			-- Remove newer items if cursor not at end.
		require -- from SEQUENCIAL_CONTAINER
			not_full: not full
		ensure then
			extended: i_th (last) = v;
			add_item_if_not_full: (old index = old last and not full) implies count = old count + 1;
			capacity_unchanged: capacity = old capacity

	put (v: like item)
			-- Replace current item with v.
		require -- from SEQUENCIAL_CONTAINER
			not_off: not off
		ensure then
			capacity_unchanged: capacity = old capacity

	put_left (v: G)
			-- Insert v to the right of cursor.
			-- (from SEQUENCIAL_CONTAINER)
		require -- from SEQUENCIAL_CONTAINER
			insertable: insertable;
			not_full: not full;
			not_before: not before

	put_right (v: G)
			-- Insert v to the right of cursor.
			-- (from SEQUENCIAL_CONTAINER)
		require -- from SEQUENCIAL_CONTAINER
			insertable: insertable;
			not_full: not full;
			not_after: not after
	
feature -- Removal

	remove
			-- Remove current item.
		require -- from SEQUENCIAL_CONTAINER
			prunable: prunable;
			not_empty: not empty;
			not_off: not off
		ensure then
			count_decreased: count = old count - 1;
			cursor_unchanged: not old islast implies index = old index;
			capacity_unchanged: capacity = old capacity

	wipe_out
			-- Empty container.
		ensure -- from SEQUENCIAL_CONTAINER
			empty: empty
		ensure then
			capacity_unchanged: capacity = old capacity
	
feature -- Resizing

	resize (n: INTEGER)
			-- Resize container to n elements.
			-- (from SEQUENCIAL_CONTAINER)
		require -- from SEQUENCIAL_CONTAINER
			resizable: resizable;
			size_increasing: n > capacity
		ensure -- from SEQUENCIAL_CONTAINER
			resized: capacity = n
	
invariant

		-- from GENERAL
	reflexive_equality: standard_is_equal (Current);
	reflexive_conformance: conforms_to (Current);
	not_off_yields_existing_item: not off implies item /= void;
	empty_definition: empty = (count = 0);
	full_definition: full = (count = capacity);
	count_in_range: count >= 0 and count <= capacity;
	isfirst_definition: isfirst = (not empty and then (index = first));
	islast_definition: islast = (not empty and then (index = last));
		-- from TWO_WAY_SEQUENCIAL_CONTAINER
	off_definition: off = (before or after);
		-- from SEQUENCIAL_CONTAINER
	empty_definition: empty = (count = 0);
	off_definition: off = (before or after);
	empty_constraint: empty implies off;
	count_range: 0 <= count and count <= capacity;

end -- class CIRCULAR_CONTAINER