indexing
	description: "Simple single-linked lists"
	author: "Patrick Schoenbach"
	access: cursor
	representation: linked
	contents: generic

class interface
	SIMPLE_LIST [G]

create 

	make
		require
			empty: empty

feature -- Access

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

	i_th (i: INTEGER): G
			-- Item at index i
			-- Was declared in DS_LINKED_LIST as synonym of @ and item.
			-- (from DS_LINKED_LIST)
		require -- from SEQUENCIAL_CONTAINER
			valid_index: valid_index (i)
		require -- from DS_TABLE
			valid_entry: valid_entry (k)

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

	capacity: INTEGER
			-- Capacity of list
			-- (from LIST_ADAPTER)

	count: INTEGER
			-- Number of items in list
			-- (from DS_LINKED_LIST)
	
feature -- Comparison

	is_equal (other: like Current): BOOLEAN
			-- Is list equal to other?
			-- (from DS_LINKED_LIST)
		require -- DS_CONTAINER
			precursor: True
		require -- from GENERAL
			other_not_void: other /= void
		ensure then -- from DS_CONTAINER
			same_count: Result implies count = other.count
		ensure -- from GENERAL
			symmetric: Result implies other.is_equal (Current);
			consistent: standard_is_equal (other) implies Result
	
feature -- Status report

	after: BOOLEAN
			-- Is there no valid item to the left of cursor?
			-- (from LIST_ADAPTER)

	before: BOOLEAN
			-- Is there no valid item to the right of cursor?
			-- (from LIST_ADAPTER)

	Full: BOOLEAN is false
			-- Is container full? (Answer: no)
			-- (from LIST_ADAPTER)

	Insertable: BOOLEAN is true
			-- Can items be inserted in the middle of container? (Answer: yes)
			-- (from LIST_ADAPTER)

	empty: BOOLEAN
			-- Is structure empty?
			-- (from DS_CONTAINER)

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

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

	off: BOOLEAN
			-- Is cursor off the list?
			-- (from LIST_ADAPTER)

	Prunable: BOOLEAN is true
			-- Can items be removed from container? (Answer: yes)
			-- (from LIST_ADAPTER)

	Resizable: BOOLEAN is false
			-- Can container be resized? (Answer: no)
			-- (from LIST_ADAPTER)

	valid_index (i: INTEGER): BOOLEAN
			-- Is i a valid index?
			-- (from DS_INDEXABLE)
		ensure then -- from DS_INDEXABLE
			definition: Result = (1 <= i and i <= count + 1)
		ensure then -- from DS_INDEXABLE
			definition: Result = (1 <= i and i <= count + 1)
	
feature -- Cursor movement

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

	go_i_th (i: INTEGER)
			-- Move cursor to i-th item.
			-- (from LIST_ADAPTER)
		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 LIST_ADAPTER)
		require -- from SEQUENCIAL_CONTAINER
			not_empty: not empty
		ensure -- from SEQUENCIAL_CONTAINER
			cursor_at_start: isfirst
	
feature -- Element change

	extend (v: G)
			-- Add v to end of container.
			-- (from LIST_ADAPTER)
		require -- from SEQUENCIAL_CONTAINER
			not_full: not full
		ensure then -- from LINEAR_CONTAINER
			extended: i_th (count) = v;
			count_increased: count = old count + 1;
			index_unchanged: not old empty implies index = old index

	put (v: G)
			-- Replace current item with v.
			-- (from LIST_ADAPTER)
		require -- from SEQUENCIAL_CONTAINER
			not_off: not off
		ensure then -- from LINEAR_CONTAINER
			replaced: item = v;
			count_unchanged: count = old count;
			index_unchanged: index = old index

	put_left (v: G)
			-- Insert v to the left of current position.
			-- (from LIST_ADAPTER)
		require -- from SEQUENCIAL_CONTAINER
			insertable: insertable;
			not_full: not full;
			not_before: not before
		ensure then -- from LINEAR_CONTAINER
			inserted: i_th (index - 1) = v;
			count_increased: count = old count + 1;
			index_increased: index = old index + 1

	put_right (v: G)
			-- Insert v to the right of current position.
			-- (from LIST_ADAPTER)
		require -- from SEQUENCIAL_CONTAINER
			insertable: insertable;
			not_full: not full;
			not_after: not after
		ensure then -- from LINEAR_CONTAINER
			inserted: i_th (index + 1) = v;
			count_increased: count = old count + 1;
			index_unchanged: index = old index
	
feature -- Removal

	remove
			-- Remove current item.
			-- (from LIST_ADAPTER)
		require -- from SEQUENCIAL_CONTAINER
			prunable: prunable;
			not_empty: not empty;
			not_off: not off
		ensure then -- from LINEAR_CONTAINER
			count_decreased: count = old count - 1;
			index_unchanged: not off implies index = old index

	wipe_out
			-- Empty container.
		ensure -- from SEQUENCIAL_CONTAINER
			empty: empty
		ensure -- from DS_CONTAINER
			wipe_out: empty
	
feature -- Resizing

	resize (n: INTEGER)
			-- Resize history to n items.
			-- (from LIST_ADAPTER)
		require -- from SEQUENCIAL_CONTAINER
			resizable: resizable;
			size_increasing: n > capacity
		ensure -- from SEQUENCIAL_CONTAINER
			resized: capacity = n
	
feature -- Duplication

	copy (other: like Current)
			-- Copy other to list.
			-- (from DS_LINKED_LIST)
		require -- from GENERAL
			other_not_void: other /= void;
			type_identity: same_type (other)
		ensure -- from GENERAL
			is_equal: is_equal (other)
	
invariant

		-- from GENERAL
	reflexive_equality: standard_is_equal (Current);
	reflexive_conformance: conforms_to (Current);
		-- from LINEAR_CONTAINER
	after_definition: after = (index = count + 1);
	before_definition: before = (index = 0);
	isfirst_definition: isfirst = (not empty and then (index = 1));
	islast_definition: islast = (not empty and then (index = count));
		-- 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 DS_CONTAINER
	positive_count: count >= 0;
	empty_definition: empty = (count = 0);

end -- class SIMPLE_LIST