indexing
	description: "Hash tables, used to store items identified by hashable keys"
	legal: "See notice at end of class."
	instructions: "[
				Several procedures are provided for inserting an item
				with a given key.
		
				Here is how to choose between them:
		
					- Use put if you want to do an insertion only if
					  there was no item with the given key, doing nothing
					  otherwise. (You can find out on return if there was one,
					  and what it was.)
		
					- Use force if you always want to insert the item;
					  if there was one for the given key it will be removed,
					  (and you can find out on return what it was).
		
					- Use extend if you are sure there is no item with
					  the given key, enabling faster insertion (but
					  unpredictable behavior if this assumption is not true).
		
					- Use replace if you want to replace an already present
					  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:
		
					your_table.search (your_key)
					if your_table.found then
						what_you_where_looking_for := your_table.found_item
						... Do whatever is needed to `what_you_were_looking_for' ...
					else
						... No item was present for `your_key' ...
					end
	]"
	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.
	]"
	status: "See notice at end of class."
	date: "$Date: 2006-09-28 17:53:09 -0700 (Thu, 28 Sep 2006) $"
	revision: "$Revision: 63977 $"

class interface
	HASH_TABLE [G, H -> HASHABLE]

create 
	make (n: INTEGER_32)
			-- 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 < capacity * initial_occupation
			minimum_space: minimum_capacity < capacity * initial_occupation
			more_than_minimum: capacity >= minimum_capacity
			no_status: not special_status

feature -- Initialization

	accommodate (n: INTEGER_32)
			-- 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 < capacity * initial_occupation

	make (n: INTEGER_32)
			-- 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 < capacity * initial_occupation
			minimum_space: minimum_capacity < capacity * initial_occupation
			more_than_minimum: capacity >= minimum_capacity
			no_status: not special_status
	
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

	generating_type: STRING_8
			-- Name of current object's generating type
			-- (type of which it is a direct instance)
			-- (from ANY)

	generator: STRING_8
			-- Name of current object's generating class
			-- (base class of the type of which it is a direct instance)
			-- (from ANY)

	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 is_empty

	item alias "[]" (key: H): G assign put
			-- Item associated with `key', if present
			-- otherwise default value of type `G'
			-- Was declared in HASH_TABLE as synonym of infix "@".
		require -- from TABLE
			valid_key: valid_key (key)
		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 assign put
			-- Item associated with `key', if present
			-- otherwise default value of type `G'
			-- Was declared in HASH_TABLE as synonym of item.
		require -- from TABLE
			valid_key: valid_key (key)
		ensure then
			default_value_if_not_present: (not (has (key))) implies (Result = computed_default_value)
	
feature -- Measurement

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

	count: INTEGER_32
			-- Number of items in table

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

	frozen deep_equal (some: ANY; other: like arg #1): BOOLEAN
			-- Are `some' and `other' either both void
			-- or attached to isomorphic object structures?
			-- (from ANY)
		ensure -- from ANY
			shallow_implies_deep: standard_equal (some, other) implies Result
			both_or_none_void: (some = Void) implies (Result = (other = Void))
			same_type: (Result and (some /= Void)) implies some.same_type (other)
			symmetric: Result implies deep_equal (other, some)

	frozen equal (some: ANY; other: like arg #1): BOOLEAN
			-- Are `some' and `other' either both void or attached
			-- to objects considered equal?
			-- (from ANY)
		ensure -- from ANY
			definition: Result = (some = Void and other = Void) or else ((some /= Void and other /= Void) and then some.is_equal (other))

	is_equal (other: like Current): BOOLEAN
			-- Does table contain the same information as `other'?
		require -- from ANY
			other_not_void: other /= Void
		ensure -- from ANY
			symmetric: Result implies other.is_equal (Current)
			consistent: standard_is_equal (other) implies Result

	frozen standard_equal (some: ANY; other: like arg #1): BOOLEAN
			-- Are `some' and `other' either both void or attached to
			-- field-by-field identical objects of the same type?
			-- Always uses default object comparison criterion.
			-- (from ANY)
		ensure -- from ANY
			definition: Result = (some = Void and other = Void) or else ((some /= Void and other /= Void) and then some.standard_is_equal (other))

	frozen standard_is_equal (other: like Current): BOOLEAN
			-- Is `other' attached to an object of the same type
			-- as current object, and field-by-field identical to it?
			-- (from ANY)
		require -- from ANY
			other_not_void: other /= Void
		ensure -- from ANY
			same_type: Result implies same_type (other)
			symmetric: Result implies other.standard_is_equal (Current)
	
feature -- Status report

	after: BOOLEAN
			-- Is cursor past last item?
			-- Was declared in HASH_TABLE as synonym of 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?

	conforms_to (other: ANY): BOOLEAN
			-- Does type of current object conform to type
			-- of `other' (as per Eiffel: The Language, chapter 13)?
			-- (from ANY)
		require -- from ANY
			other_not_void: other /= Void

	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?

	is_empty: BOOLEAN
			-- Is structure empty?
			-- (from FINITE)
		require -- from  CONTAINER
			True

	is_inserted (v: G): BOOLEAN
			-- Has `v' been inserted by the most recent insertion?
			-- (By default, the value returned is equivalent to calling 
			-- `has (v)'. However, descendants might be able to provide more
			-- efficient implementations.)
			-- (from COLLECTION)

	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.
		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?

	same_type (other: ANY): BOOLEAN
			-- Is type of current object identical to type of `other'?
			-- (from ANY)
		require -- from ANY
			other_not_void: other /= Void
		ensure -- from ANY
			definition: Result = (conforms_to (other) and other.conforms_to (Current))

	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)
		require -- from  TABLE
			True
		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: 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: 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: 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_if_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)))

	merge (other: HASH_TABLE [G, H])
			-- Merge `other' into Current. If `other' has some elements
			-- with same key as in `Current', replace them by one from
			-- `other'.
		require
			other_not_void: other /= Void
		ensure
			inserted: other.current_keys.linear_representation.for_all (agent has)

	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 (key)
		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)
			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
			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_implies_no_old_key: not_found implies 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: prunable
		ensure -- from COLLECTION
			wiped_out: is_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
			no_status: not special_status

	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.
			-- Reset found_item to its default value if removed.
		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
		require -- from  CONTAINER
			True
		ensure then
			result_exists: Result /= Void
			good_count: Result.count = count
	
feature -- Duplication

	copy (other: like Current)
			-- Re-initialize from `other'.
		require -- from ANY
			other_not_void: other /= Void
			type_identity: same_type (other)
		ensure -- from ANY
			is_equal: is_equal (other)

	frozen deep_copy (other: like Current)
			-- Effect equivalent to that of:
			--		copy (`other' . deep_twin)
			-- (from ANY)
		require -- from ANY
			other_not_void: other /= Void
		ensure -- from ANY
			deep_equal: deep_equal (Current, other)

	frozen deep_twin: like Current
			-- New object structure recursively duplicated from Current.
			-- (from ANY)
		ensure -- from ANY
			deep_equal: deep_equal (Current, Result)

	frozen standard_copy (other: like Current)
			-- Copy every field of `other' onto corresponding field
			-- of current object.
			-- (from ANY)
		require -- from ANY
			other_not_void: other /= Void
			type_identity: same_type (other)
		ensure -- from ANY
			is_standard_equal: standard_is_equal (other)

	frozen standard_twin: like Current
			-- New object field-by-field identical to `other'.
			-- Always uses default copying semantics.
			-- (from ANY)
		ensure -- from ANY
			standard_twin_not_void: Result /= Void
			equal: standard_equal (Result, Current)

	frozen twin: like Current
			-- New object equal to `Current'
			-- twin calls copy; to change copying/twining semantics, redefine copy.
			-- (from ANY)
		ensure -- from ANY
			twin_not_void: Result /= Void
			is_equal: Result.is_equal (Current)
	
feature -- Basic operations

	frozen default: like Current
			-- Default value of object's type
			-- (from ANY)

	frozen default_pointer: POINTER
			-- Default value of type `POINTER'
			-- (Avoid the need to write `p'.default for
			-- some `p' of type `POINTER'.)
			-- (from ANY)

	default_rescue
			-- Process exception for routines with no Rescue clause.
			-- (Default: do nothing.)
			-- (from ANY)

	frozen do_nothing
			-- Execute a null action.
			-- (from ANY)
	
feature -- Output

	io: STD_FILES
			-- Handle to standard file setup
			-- (from ANY)

	out: STRING_8
			-- New string containing terse printable representation
			-- of current object
			-- Was declared in ANY as synonym of tagged_out.
			-- (from ANY)

	print (some: ANY)
			-- Write terse external representation of `some'
			-- on standard output.
			-- (from ANY)

	frozen tagged_out: STRING_8
			-- New string containing terse printable representation
			-- of current object
			-- Was declared in ANY as synonym of out.
			-- (from ANY)
	
feature -- Platform

	operating_environment: OPERATING_ENVIRONMENT
			-- Objects available from the operating system
			-- (from ANY)
	
invariant
	keys_not_void: keys /= Void
	content_not_void: content /= Void
	deleted_marks_not_void: deleted_marks /= 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 + 1
	valid_iteration_position: off or truly_occupied (iteration_position)
	control_non_negative: control >= 0
	special_status: special_status = (conflict or inserted or replaced or removed or found or not_found)
	max_occupation_meaningful: (max_occupation > 0) and (max_occupation < 1)
	initial_occupation_meaningful: (initial_occupation > 0) and (initial_occupation < 1)
	sized_generously_enough: initial_occupation < max_occupation
	count_big_enough: 0 <= count
	count_small_enough: count <= capacity
	breathing_space: count <= 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

		-- from FINITE
	empty_definition: is_empty = (count = 0)
	non_negative_count: count >= 0

		-- from ANY
	reflexive_equality: standard_is_equal (Current)
	reflexive_conformance: conforms_to (Current)

indexing
	library: "EiffelBase: Library of reusable components for Eiffel."
	copyright: "Copyright (c) 1984-2006, Eiffel Software and others"
	license: "Eiffel Forum License v2 (see http://www.eiffel.com/licensing/forum.txt)"
	source: "[
		Eiffel Software
		356 Storke Road, Goleta, CA 93117 USA
		Telephone 805-685-1006, Fax 805-685-6869
		Website http://www.eiffel.com
		Customer support http://support.eiffel.com
	]"

end -- class HASH_TABLE