indexing
	description: "Hash tables, used to store items identified by hashable keys"
	instructions: "Several procedures are provided for inserting an item with a given key. Here is how to choose between them: %T- Use `put%' if you want to do an insertion only if %T  there was no item with the given key, doing nothing %T  otherwise. (You can find out on return if there was one, %T  and what it was.) %T- Use `force%' if you always want to insert the item; %T  if there was one for the given key it will be removed, %T  (and you can find out on return what it was). %T- Use `extend%' if you are sure there is no item with %T  the given key, enabling faster insertion (but %T  unpredictable behavior if this assumption is not true). %T- Use `replace%' if you want to replace an already present %T  item with the given key, and do nothing if there is none. In addition you can use `replace_key%' to change the key of an already present item, identified by its previous key, or do nothing if there is nothing for that previous key. You can find out on return."
	instructions: "To find out whether a key appears in the table, use `has%'. To find out the item, if any, associated with a certain key, use `item%'. Both of these routines perform a search. If you need both pieces of information (does a key appear? And, if so, what is the associated item?), you can avoid performing two redundant traversals by using instead the combination of `search%', `found%' and `found_item%' as follows:  %Tyour_table.search (your_key) %Tif your_table.found then %T%Twhat_you_where_looking_for := your_table.found_item %T%T... Do whatever is needed to `what_you_were_looking_for%' ...  %Telse %T%T... No item was present for `your_key%' ... %Tend"
	compatibility: "This version of the class accepts any value of type H as key. Previous versions did not accept the default value as a key; this restriction no longer applies. Most clients of the old version should work correctly with this one; a client that explicitly relied on the default value not being hashable should use the old version available in the EiffelBase 3.3 compatibility cluster. Also, `force%' now sets either `found%' or `not_found%'. (Previously it would always set `inserted%'.)"
	storable_compatibility: "Persistent instances of the old version of this class will not be  retrievable with the present version."
	warning: "Modifying an object used as a key by an item present in a table will cause incorrect behavior. If you will be modifying key objects, pass a clone, not the object itself, as key argument to `put%' and `replace_key%'."

class interface
	HASH_TABLE [G, H -> HASHABLE]

create 

	make (n: INTEGER)
			-- Allocate hash table for at least n items.
			-- The table will be resized automatically
			-- if more than n items are inserted.
		ensure
			breathing_space: n * 100 < capacity * initial_occupation;
			minimum_space: minimum_capacity * 100 < capacity * initial_occupation;
			more_than_minimum: capacity >= minimum_capacity;

feature -- Initialization

			-- Reallocate table with enough space for n items;
			-- keep all current items.
		require
			n >= 0
		ensure
			count_not_changed: count = old count;
			slot_count_same_as_count: used_slot_count = count;
			breathing_space: count * 100 < capacity * initial_occupation

	make (n: INTEGER)
			-- Allocate hash table for at least n items.
			-- The table will be resized automatically
			-- if more than n items are inserted.
		ensure
			breathing_space: n * 100 < capacity * initial_occupation;
			minimum_space: minimum_capacity * 100 < capacity * initial_occupation;
			more_than_minimum: capacity >= minimum_capacity;
	
feature -- Access

	current_keys: ARRAY [H]
			-- New array containing actually used keys, from 1 to count
		ensure
			good_count: Result.count = count

	cursor: CURSOR
			-- Current cursor position
		ensure
			cursor_not_void: Result /= void

	found_item: G
			-- Item, if any, yielded by last search operation

	has (key: H): BOOLEAN
			-- Is there an item in the table with key key?
		ensure then
			default_case: (key = computed_default_key) implies (Result = has_default)

	has_item (v: G): BOOLEAN
			-- Does structure include v?
			-- (Reference or object equality,
			-- based on object_comparison.)
		ensure -- from CONTAINER
			not_found_in_empty: Result implies not empty

	item (key: H): G
			-- Item associated with key, if present
			-- otherwise default value of type G
			-- Was declared in HASH_TABLE as synonym of item and @.
		require -- from TABLE
			valid_key: valid_key (k)
		ensure then
			default_value_if_not_present: (not (has (key))) implies (Result = computed_default_value)

	item_for_iteration: G
			-- Element at current iteration position
		require
			not_off: not off

	key_for_iteration: H
			-- Key at current iteration position
		require
			not_off: not off
		ensure
			at_iteration_position: Result = key_at (iteration_position)

	infix "@" (key: H): G
			-- Item associated with key, if present
			-- otherwise default value of type G
			-- Was declared in HASH_TABLE as synonym of item and @.
		require -- from TABLE
			valid_key: valid_key (k)
		ensure then
			default_value_if_not_present: (not (has (key))) implies (Result = computed_default_value)
	
feature -- Measurement

	capacity: INTEGER
			-- Number of items that may be stored.

	count: INTEGER
			-- Number of items in table

	occurrences (v: G): INTEGER
			-- Number of table items equal to v.
		ensure -- from BAG
			non_negative_occurrences: Result >= 0
	
feature -- Comparison

	is_equal (other: like Current): BOOLEAN
			-- Does table contain the same information as other?
		require -- from GENERAL
			other_not_void: other /= void
		ensure -- from GENERAL
			symmetric: Result implies other.is_equal (Current);
			consistent: standard_is_equal (other) implies Result
	
feature -- Status report

	after: BOOLEAN
			-- Is cursor past last item?
			-- Was declared in HASH_TABLE as synonym of after and off.
		ensure
			definition: Result = ((not has_default and (iteration_position >= capacity)) or (has_default and (iteration_position = (capacity + 1))))

	changeable_comparison_criterion: BOOLEAN
			-- May object_comparison be changed?
			-- (Answer: yes by default.)
			-- (from CONTAINER)

	conflict: BOOLEAN
			-- Did last operation cause a conflict?

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

	Extendible: BOOLEAN is true
			-- May new items be added? (Answer: yes.)

	found: BOOLEAN
			-- Did last operation find the item sought?

	Full: BOOLEAN is false
			-- Is structure filled to capacity? (Answer: no.)

	inserted: BOOLEAN
			-- Did last operation insert an item?

	not_found: BOOLEAN
			-- Did last operation fail to find the item sought?

	object_comparison: BOOLEAN
			-- Must search operations use equal rather than =
			-- for comparing references? (Default: no, use =.)
			-- (from CONTAINER)

	off: BOOLEAN
			-- Is cursor past last item?
			-- Was declared in HASH_TABLE as synonym of after and off.
		ensure
			definition: Result = ((not has_default and (iteration_position >= capacity)) or (has_default and (iteration_position = (capacity + 1))))

	prunable: BOOLEAN
			-- May items be removed? (Answer: yes.)

	removed: BOOLEAN
			-- Did last operation remove an item?

	replaced: BOOLEAN
			-- Did last operation replace an item?

	valid_cursor (c: CURSOR): BOOLEAN
			-- Can cursor be moved to position c?
		require
			c_not_void: c /= void

	valid_key (k: H): BOOLEAN
			-- Is k a valid key?
			-- (Answer: always yes for hash tables in this version)
		ensure then
			Result
	
feature -- Status setting

	compare_objects
			-- Ensure that future search operations will use equal
			-- rather than = for comparing references.
			-- (from CONTAINER)
		require -- from CONTAINER
			changeable_comparison_criterion
		ensure -- from CONTAINER
			object_comparison

	compare_references
			-- Ensure that future search operations will use =
			-- rather than equal for comparing references.
			-- (from CONTAINER)
		require -- from CONTAINER
			changeable_comparison_criterion
		ensure -- from CONTAINER
			reference_comparison: not object_comparison
	
feature -- Cursor movement

	forth
			-- Advance cursor to next occupied position,
			-- or off if no such position remains.
		require
			not_off: not off

	go_to (c: CURSOR)
			-- Move to position c.
		require
			c_not_void: c /= void;
			valid_cursor: valid_cursor (c)

	search (key: H)
			-- Search for item of key key.
			-- If found, set found to true, and set
			-- found_item to item associated with key.
		ensure
			found_or_not_found: found or not_found;
			item_if_found: found implies (found_item = content.item (position))

	start
			-- Bring cursor to first position.
	
feature -- Element change

	extend (new: G; key: H)
			-- Assuming there is no item of key key,
			-- insert new with key.
			-- Set inserted.
			--
			-- To choose between various insert/replace procedures,
			-- see instructions in the Indexing clause.
		require
			not_present: not has (key)
		ensure
			inserted: inserted;
			insertion_done: item (key) = new;
			one_more: count = old count + 1;
			same_slot_count_or_one_more_unless_reallocated: (used_slot_count = old used_slot_count) or (used_slot_count = old used_slot_count + 1) or (used_slot_count = count);
			default_property: has_default = ((key = computed_default_key) or (old has_default))

	fill (other: CONTAINER [G])
			-- Fill with as many items of other as possible.
			-- The representations of other and current structure
			-- need not be the same.
			-- (from COLLECTION)
		require -- from COLLECTION
			other_not_void: other /= void;
			extendible

	force (new: G; key: H)
			-- Update table so that new will be the item associated
			-- with key.
			-- If there was an item for that key, set found
			-- and set found_item to that item.
			-- If there was none, set not_found and set
			-- found_item to the default value.
			--
			-- To choose between various insert/replace procedures,
			-- see instructions in the Indexing clause.
		require else
			true
		ensure then
			insertion_done: item (key) = new;
			now_present: has (key);
			found_or_not_found: found or not_found;
			not_found_iff_was_not_present: not_found = not (old has (key));
			same_count_or_one_more: (count = old count) or (count = old count + 1);
			same_slot_count_or_one_more_unless_reallocated: (used_slot_count = old used_slot_count) or (used_slot_count = old used_slot_count + 1) or (used_slot_count = count);
			found_item_is_old_item: found implies (found_item = old (item (key)));
			default_value_if_not_found: not_found implies (found_item = computed_default_value);
			default_property: has_default = ((key = computed_default_key) or ((key /= computed_default_key) and (old has_default)))

	put (new: G; key: H)
			-- Insert new with key if there is no other item
			-- associated with the same key.
			-- Set inserted if and only if an insertion has
			-- been made (i.e. key was not present).
			-- If so, set position to the insertion position.
			-- If not, set conflict.
			-- In either case, set found_item to the item
			-- now associated with key (previous item if
			-- there was one, new otherwise).
			--
			-- To choose between various insert/replace procedures,
			-- see instructions in the Indexing clause.
		require -- from TABLE
			valid_key: valid_key (k)
		ensure then
			conflict_or_inserted: conflict or inserted;
			insertion_done: inserted implies item (key) = new;
			now_present: inserted implies has (key);
			one_more_if_inserted: inserted implies (count = old count + 1);
			one_more_slot_if_inserted_unless_reallocated: inserted implies ((used_slot_count = old used_slot_count + 1) or (used_slot_count = count));
			unchanged_if_conflict: conflict implies (count = old count);
			same_item_if_conflict: conflict implies (item (key) = old (item (key)));
			slot_count_unchanged_if_conflict: conflict implies (used_slot_count = old used_slot_count);
			found_item_associated_with_key: found_item = item (key);
			new_item_if_inserted: inserted implies (found_item = new);
			old_item_if_conflict: conflict implies (found_item = old (item (key)));
			default_property: has_default = ((inserted and (key = computed_default_key)) or ((conflict or (key /= computed_default_key)) and (old has_default)))

	replace (new: G; key: H)
			-- Replace item at key, if present,
			-- with new; do not change associated key.
			-- Set replaced if and only if a replacement has been made
			-- (i.e. key was present); otherwise set not_found.
			-- Set found_item to the item previously associated
			-- with key (default value if there was none).
			--
			-- To choose between various insert/replace procedures,
			-- see instructions in the Indexing clause.
		ensure
			replaced_or_not_found: replaced or not_found;
			insertion_done: replaced implies item (key) = new;
			no_change_if_not_found: not_found implies item (key) = old (item (key));
			found_item_is_old_item: found_item = old (item (key))

	replace_key (new_key: H; old_key: H)
			-- If there is an item of key old_key and no item of key
			-- new_key, replace the former's key by new_key,
			-- set replaced, and set found_item to the item
			-- previously associated with old_key.
			-- Otherwise set not_found or conflict respectively.
			-- If conflict, set found_item to the item previously
			-- associated with new_key.
			--
			-- To choose between various insert/replace procedures,
			-- see instructions in the Indexing clause.
		ensure
			same_count: count = old count;
			same_slot_count: used_slot_count = old used_slot_count;
			replaced_or_conflict_or_not_found: replaced or conflict or not_found;
			old_absent: (replaced and not equal (new_key, old_key)) implies (not has (old_key));
			new_present: (replaced or conflict) = has (new_key);
			new_item: replaced implies (item (new_key) = old (item (old_key)));
			not_found_iff_no_old_key: not_found = old (not has (old_key));
			conflict_iff_already_present: conflict = old (has (new_key));
			not_inserted_if_conflict: conflict implies (item (new_key) = old (item (new_key)));
			default_property: has_default = ((new_key = computed_default_key) or ((new_key /= computed_default_key) and (old has_default)))
	
feature -- Removal

	clear_all
			-- Reset all items to default values; reset status.
		require -- from COLLECTION
			prunable
		ensure -- from COLLECTION
			wiped_out: empty
		ensure then
			position_equal_to_zero: position = 0;
			count_equal_to_zero: count = 0;
			used_slot_count_equal_to_zero: used_slot_count = 0;
			has_default_set: not has_default;

	remove (key: H)
			-- Remove item associated with key, if present.
			-- Set removed if and only if an item has been
			-- removed (i.e. key was present);
			-- if so, set position to index of removed element.
			-- If not, set not_found.
		ensure
			removed_or_not_found: removed or not_found;
			not_present: not has (key);
			one_less: found implies (count = old count - 1);
			same_slot_count: used_slot_count = old used_slot_count;
			default_case: (key = computed_default_key) implies (not has_default);
			non_default_case: (key /= computed_default_key) implies (has_default = old has_default)
	
feature -- Conversion

	linear_representation: ARRAYED_LIST [G]
			-- Representation as a linear structure
		ensure then
			result_exists: Result /= void;
			good_count: Result.count = count
	
feature -- Duplication

	copy (other: like Current)
			-- Re-initialize from other.
		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);
	keys_not_void: keys /= void;
	content_not_void: content /= void;
	keys_same_capacity_plus_one: keys.count = capacity + 1;
	content_same_capacity_plus_one: content.count = capacity + 1;
	deleted_same_capacity: deleted_marks.count = capacity;
	keys_starts_at_zero: keys.lower = 0;
	content_starts_at_zero: content.lower = 0;
	deleted_starts_at_zero: deleted_marks.lower = 0;
	valid_iteration_position: off or truly_occupied (iteration_position);
	control_non_negative: control >= 0;
	max_occupation_meaningful: (max_occupation > 0) and (max_occupation < 100);
	initial_occupation_meaningful: (initial_occupation > 0) and (initial_occupation < 100);
	sized_generously_enough: initial_occupation < max_occupation;
	count_big_enough: 0 <= count;
	count_small_enough: count <= capacity;
	breathing_space: count * 100 <= capacity * max_occupation;
	count_no_more_than_slot_count: count <= used_slot_count;
	slot_count_big_enough: 0 <= count;
	slot_count_small_enough: used_slot_count <= capacity;
	extra_space_non_negative: extra_space >= 0;
		-- from FINITE
	empty_definition: empty = (count = 0);
	non_negative_count: count >= 0;

end -- class HASH_TABLE