note
	description: "[
			Hash sets with hash function provided by HASHABLE and object equality.
			Implementation uses hash tables.
			Search, extension and removal are amortized constant time.
		]"
	author: "Nadia Polikarpova"
	revised_by: "Alexander Kogtenkov"
	model: set, lock
	manual_inv: true
	false_guards: true

frozen class
	V_HASH_SET [G -> V_HASHABLE]

inherit
	V_SET [G]
		redefine
			is_equal_,
			lock,
			forget_iterator
		end

create
	make

feature {NONE} -- Initialization

	make (l: V_HASH_LOCK [G])
			-- Create an empty set with lock `l'.
		note
			status: creator
		require
			l_wrapped: l.is_wrapped
		do
			create table.make (l)
			l.add_client (Current)
		ensure then
			set_empty: set.is_empty
			lock_set: lock = l
			lock_observers_effect: l.observers = old l.observers & table & Current
			table.is_empty
			is_empty
			observers_empty: observers.is_empty
			modify (Current)
			modify_model ("observers", l)
		end

feature -- Initialization

	copy_ (other: V_HASH_SET [G])
			-- Initialize by copying all the items of `other'.
		note
			explicit: wrapping
		require
			lock_wrapped: lock.is_wrapped
			same_lock: lock = other.lock
			no_iterators: observers.is_empty
		do
			if other /= Current then
				unwrap
				other.unwrap
				table.copy_ (other.table)
				other.wrap
				wrap
			end
		ensure
			set_effect: set ~ old other.set
			observers_restored: observers ~ old observers
			other_observers_restored: other.observers ~ old other.observers
			modify_model ("set", Current)
			modify_model ("observers", [Current, other])
		end

feature -- Measurement

	count: INTEGER
			-- Number of elements.
		do
			check inv end
			Result := table.count
		end

feature -- Search

	has (v: G): BOOLEAN
			-- Is `v' contained?
			-- (Uses object equality.)
		do
			check inv end
			Result := table.has_key (v)
		end

	item (v: G): G
			-- Element of `set' equivalent to `v' according to object equality.
		do
			check inv end
			Result := table.key (v)
		end

feature -- Iteration

	new_cursor: V_HASH_SET_ITERATOR [G]
			-- New iterator pointing to a position in the set, from which it can traverse all elements by going `forth'.
		note
			status: impure
		do
			create Result.make (Current)
			Result.start
		end

	at (v: G): V_HASH_SET_ITERATOR [G]
			-- New iterator over `Current' pointing at element `v' if it exists and `after' otherwise.
		note
			status: impure
		do
			create Result.make (Current)
			Result.search (v)
		end

feature -- Comparison

	is_equal_ (other: like Current): BOOLEAN
			-- Is the abstract state of Current equal to that of `other'?
		do
			check inv; other.inv end
			check table.inv_only ("subjects_definition"); other.table.inv_only ("subjects_definition") end
			Result := table.is_equal_ (other.table)
		end

feature -- Extension

	extend (v: G)
			-- Add `v' to the set.
		do
			check table.inv_only ("items_locked", "locked_definition") end
			check lock.inv_only ("owns_definition") end
			table.force (Void, v)
			check table.inv_only ("locked_definition", "no_duplicates") end
			if not table.domain_has (v).old_ then
				check table.map.domain [v] end
			else
				check table.map.domain = table.map.domain.old_ end
			end
		end

feature -- Removal

	wipe_out
			-- Remove all elements.
		do
			table.lemma_domain
			table.wipe_out
		end

feature -- Implementation

	table: V_HASH_TABLE [G, detachable ANY]
			-- Hash table that stores set elements as keys.

feature -- Specification

	lock: V_HASH_LOCK [G]
			-- Helper object for keeping items consistent.
		note
			status: ghost
		attribute
			check is_executable: False then end
		end

	forget_iterator (it: V_ITERATOR [G])
			-- Remove `it' from `observers'.
		note
			status: ghost
			explicit: contracts
		do
			check it.inv_only ("subjects_definition", "A2") end
			check attached {V_HASH_SET_ITERATOR [G]} it as hsit then
				hsit.unwrap
				set_observers (observers / hsit)
				check hsit.iterator.inv_only ("subjects_definition", "A2") end
				table.lemma_domain
				check hsit.iterator.inv_only ("owns_definition"); hsit.iterator.list_iterator.inv_only ("default_owns") end
				table.forget_iterator (hsit.iterator)
			end
		end

invariant
	table_exists: table /= Void
	owns_definition: owns ~ create {MML_SET [ANY]}.singleton (table)
	set_implementation: set = table.map.domain
	table_values_definition: ∀ x: set ¦ table.map [x] = Void
	same_lock: lock = table.lock
	observers_type: ∀ o: observers ¦ attached {V_HASH_SET_ITERATOR [G]} o
	observers_correspond: table.observers.count <= observers.count

note
	copyright: "Copyright (c) 1984-2021, Eiffel Software and others"
	license: "Eiffel Forum License v2 (see http://www.eiffel.com/licensing/forum.txt)"
	source: "[
			Eiffel Software
			5949 Hollister Ave., Goleta, CA 93117 USA
			Telephone 805-685-1006, Fax 805-685-6869
			Website http://www.eiffel.com
			Customer support http://support.eiffel.com
		]"

end