indexing
	description: "Command history implemented as arrayed circular buffers"
	representation: array
	access: cursor
	size: fixed
	author: "Patrick Schoenbach"

class interface
	ARRAYED_HISTORY [G -> COMMAND_HISTORY_ENTRY]

create 

	make (n: INTEGER)
		require
			number_of_elements_positive: n > 0

feature -- Access

	after_index: INTEGER
			-- Index of after sentinel
			-- (from ARRAYED_CIRCULAR_BUFFER)

	before_index: INTEGER
			-- Index of before sentinel
			-- (from ARRAYED_CIRCULAR_BUFFER)

	first: INTEGER
			-- Index of first item
			-- (from ARRAYED_CIRCULAR_BUFFER)

	i_th (i: INTEGER): like item
			-- Item at index i
			-- (from ARRAYED_CIRCULAR_BUFFER)
		require -- from SEQUENCIAL_CONTAINER
			valid_index: valid_index (i)

	index: INTEGER
			-- Current item
			-- (from ARRAYED_CIRCULAR_BUFFER)

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

	last: INTEGER
			-- Index of last item
			-- (from ARRAYED_CIRCULAR_BUFFER)

	Sentinels: INTEGER is 2
			-- (from ARRAYED_CIRCULAR_BUFFER)

	infix "@" (i: INTEGER): G
			-- i-th item
	
feature -- Measurement

	capacity: INTEGER
			-- Capacity of buffer
			-- (from ARRAYED_CIRCULAR_BUFFER)
		ensure then -- from ARRAYED_CIRCULAR_BUFFER
			non_negative: Result >= 0
		ensure then -- from ARRAYED_CIRCULAR_BUFFER
			non_negative: Result >= 0

	count: INTEGER
			-- (from ARRAYED_CIRCULAR_BUFFER)
	
feature -- Status report

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

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

	empty: BOOLEAN
			-- Is buffer empty?
			-- (from ARRAYED_CIRCULAR_BUFFER)

	full: BOOLEAN
			-- Is buffer entirely filled?
			-- (from ARRAYED_CIRCULAR_BUFFER)

	Insertable: BOOLEAN is false
			-- Can elements be inserted in the middle? (Answer: No)
			-- (from ARRAYED_CIRCULAR_BUFFER)

	is_executed: BOOLEAN
			-- Has current item been executed?

	isfirst: BOOLEAN
			-- Is cursor on first item?
			-- (from ARRAYED_CIRCULAR_BUFFER)

	islast: BOOLEAN
			-- Is cursor on last item?
			-- (from ARRAYED_CIRCULAR_BUFFER)

	next (i: INTEGER): INTEGER
			-- Index next to i
			-- (from ARRAYED_CIRCULAR_BUFFER)
		require -- from CIRCULAR_CONTAINER
			valid_index: valid_index (i)

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

	previous (i: INTEGER): INTEGER
			-- Index previous to i
			-- (from ARRAYED_CIRCULAR_BUFFER)
		require -- from CIRCULAR_CONTAINER
			valid_index: valid_index (i)

	Prunable: BOOLEAN is true
			-- Is container prunable? (Answer: Yes)
			-- (from ARRAYED_CIRCULAR_BUFFER)

	redoable_item: BOOLEAN
			-- Is there a redoable item?

	Resizable: BOOLEAN is true
			-- Is container resizable? (Answer: yes)
			-- (from ARRAYED_CIRCULAR_BUFFER)

	undoable_item: BOOLEAN
			-- Is there an undoable item?

	valid_index (i: INTEGER): BOOLEAN
			-- Is index i valid?
			-- (from ARRAYED_CIRCULAR_BUFFER)

feature -- Cursor movement

	back
			-- Move cursor to previous item.
			-- (from ARRAYED_CIRCULAR_BUFFER)
		require -- CIRCULAR_CONTAINER
			precursor: True
		require -- from TWO_WAY_SEQUENCIAL_CONTAINER
			not_before: not before
		ensure then -- from CIRCULAR_CONTAINER
			previous_position: index = previous (old index)

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

	forth
			-- Move cursor to next item.
			-- (from ARRAYED_CIRCULAR_BUFFER)
		require -- CIRCULAR_CONTAINER
			precursor: True
		require -- from SEQUENCIAL_CONTAINER
			not_after: not after
		ensure then -- from CIRCULAR_CONTAINER
			next_position: index = next (old index)

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

	start
			-- Move cursor to first item.
			-- (from ARRAYED_CIRCULAR_BUFFER)
		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 the end of buffer.
			-- Remove all elements between cursor and end, if cursor not at
			-- end.
			-- (from ARRAYED_CIRCULAR_BUFFER)
		require -- CIRCULAR_CONTAINER
			precursor: True
		require else -- from ARRAYED_CIRCULAR_BUFFER
			always_extendable: full or not full
		require -- from SEQUENCIAL_CONTAINER
			not_full: not full
		require else -- from ARRAYED_CIRCULAR_BUFFER
			always_extendable: full or not full
		ensure then -- from CIRCULAR_CONTAINER
			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
		ensure then -- from ARRAYED_CIRCULAR_BUFFER
			cursor_advanced: not old full implies index = next (old index)
		ensure then -- from ARRAYED_CIRCULAR_BUFFER
			cursor_advanced: not old full implies index = next (old index)

	put (v: like item)
			-- Replace current item with v,
			-- (from ARRAYED_CIRCULAR_BUFFER)
		require -- CIRCULAR_CONTAINER
			precursor: True
		require -- from SEQUENCIAL_CONTAINER
			not_off: not off
		ensure then -- from CIRCULAR_CONTAINER
			capacity_unchanged: capacity = old capacity

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

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

	remove
			-- Remove last item.
			-- (from ARRAYED_CIRCULAR_BUFFER)
		require -- CIRCULAR_CONTAINER
			precursor: True
		require -- from SEQUENCIAL_CONTAINER
			prunable: prunable;
			not_empty: not empty;
			not_off: not off
		ensure then -- from CIRCULAR_CONTAINER
			count_decreased: count = old count - 1;
			cursor_unchanged: not old islast implies index = old index;
			capacity_unchanged: capacity = old capacity

	wipe_out
			-- Clear entire buffer.
			-- (from ARRAYED_CIRCULAR_BUFFER)
		ensure then -- from CIRCULAR_CONTAINER
			capacity_unchanged: capacity = old capacity
		ensure -- from SEQUENCIAL_CONTAINER
			empty: empty
	
feature -- Resizing

	resize (n: INTEGER)
			-- Resize buffer.
			-- (from ARRAYED_CIRCULAR_BUFFER)
		require -- from SEQUENCIAL_CONTAINER
			resizable: resizable;
			size_increasing: n > capacity
		ensure -- from SEQUENCIAL_CONTAINER
			resized: capacity = n
	
feature -- Basic operations

	redo
			-- Redo current item.

	undo
			-- Undo current item.
	
invariant

		-- from GENERAL
	reflexive_equality: standard_is_equal (Current);
	reflexive_conformance: conforms_to (Current);
		-- from HISTORY_CONTAINER
	current_command_executed: not off implies item.is_executed;
		-- 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;
		-- from ARRAYED_CIRCULAR_BUFFER
after_definition: after = not empty implies (index = after_index);
	after_index_constraint: not empty implies after_index = next (last);
	before_definition: after = not empty implies (index = before_index);
	before_index_constraint: not empty implies before_index = previous (first);
	after_sentinel_empty: not empty implies i_th (after_index) = void;
	before_sentinel_empty: not empty implies i_th (before_index) = void;
		-- from CIRCULAR_CONTAINER
	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));

end -- class ARRAYED_HISTORY