note
	description: "Cells that can be linked to two neighbour cells."
	author: "Nadia Polikarpova"
	revised_by: "Alexander Kogtenkov"
	model: item, left, right

frozen class
	V_DOUBLY_LINKABLE [G]

inherit
	V_CELL [G]

create
	put

feature -- Access

	right: detachable V_DOUBLY_LINKABLE [G]
			-- Next cell.
		note
			guard: not_right
		attribute
		end

	left: detachable V_DOUBLY_LINKABLE [G]
			-- Previous cell.
		note
			guard: not_left
		attribute
		end

feature -- Replacement

	connect_right (cell: V_DOUBLY_LINKABLE [G])
			-- Connect current list segment to the segment beginning with `cell'.
		note
			explicit: contracts
		require
			different: cell /= Current
			wrapped: is_wrapped
			cell_wrapped: cell.is_wrapped
			segment_end: right = Void
			segment_start: cell.left = Void
		do
			cell.unwrap
			put_right (cell)
			cell.put_left (Current)
			cell.wrap
		ensure
			wrapped: is_wrapped
			cell_wrapped: cell.is_wrapped
			connected: right = cell
			modify_model (["right", "subjects", "observers"], Current)
			modify_model (["left", "subjects", "observers"], cell)
		end

	insert_right (front, back: V_DOUBLY_LINKABLE [G])
			-- Insert a list segment `front'-`back' to the right of current cell.
		note
			explicit: contracts, wrapping
		require
			wrapped: is_wrapped
			front_wrapped: front.is_wrapped
			back_wrapped: back.is_wrapped
			right_wrapped: right.is_wrapped
			segment_start: front.left = Void
			segment_end: back.right = Void
		do
			unwrap_all (create {MML_SET [ANY]} & Current & right & front & back)
			back.put_right (right)
			right.put_left (back)
			put_right (front)
			front.put_left (Current)
			wrap_all (create {MML_SET [ANY]} & Current & back.right & front & back)
		ensure
			front_connected: right = front
			back_connected: back.right = old right
			wrapped: is_wrapped
			front_wrapped: front.is_wrapped
			back_wrapped: back.is_wrapped
			right_wrapped: (old right).is_wrapped
			modify_model (["right", "subjects", "observers"], [Current, back])
			modify_model (["left", "subjects", "observers"], [right, front])
		end

	remove_right
			-- Remove the cell to the right of current cell.
		note
			explicit: contracts, wrapping
		require
			wrapped: is_wrapped
			right_wrapped: right.is_wrapped
			right_wrapped: attached right as x and then x.is_wrapped
			next_wrapped: right.right.is_wrapped
		do
			unwrap_all (create {MML_SET [ANY]} & Current & right & right.right)
			put_right (right.right)
			right.put_left (Current)
			wrap_all (create {MML_SET [ANY]} & Current & right)
		ensure
			right_set: right = old right.right
			wrapped: is_wrapped
			right_wrapped: right.is_wrapped
			modify_model (["right", "subjects", "observers"], Current)
			modify_model (["left", "subjects", "observers"], right.right)
			modify (right)
		end

feature {V_DOUBLY_LINKABLE, V_DOUBLY_LINKED_LIST} -- Replacement

	put_right (cell: detachable V_DOUBLY_LINKABLE [G])
			-- Replace `right' with `cell'.
		require
			open: is_open
			right_open: attached right as r implies r.is_open
			inv_only ("subjects_definition", "observers_definition")
		do
			right := cell
			set_subjects
				(if attached left as c then create {MML_SET [ANY]}.singleton (c) else create {MML_SET [ANY]} end +
				if attached right as c then create {MML_SET [ANY]}.singleton (c) else create {MML_SET [ANY]} end)
			set_observers (subjects)
		ensure
			right_effect: right = cell
			inv_only ("subjects_definition", "observers_definition")
			modify_field (["right", "subjects", "observers"], Current)
		end

	put_left (cell: detachable V_DOUBLY_LINKABLE [G])
			-- Replace `left' with `cell'.
		require
			open: is_open
			left_open: attached left as l implies l.is_open
			inv_only ("subjects_definition", "observers_definition")
		do
			left := cell
			set_subjects
				(if attached left as c then create {MML_SET [ANY]}.singleton (c) else create {MML_SET [ANY]} end +
				if attached right as c then create {MML_SET [ANY]}.singleton (c) else create {MML_SET [ANY]} end)
			set_observers (subjects)
		ensure
			left_effect: left = cell
			inv_only ("subjects_definition", "observers_definition")
			modify_field (["left", "subjects", "observers"], Current)
		end

feature -- Specification

	not_left (new_left: V_DOUBLY_LINKABLE [G]; o: ANY): BOOLEAN
			-- Is `o' different from `left'?
		note
			status: functional, ghost
		do
			Result := o /= left
		end

	not_right (new_right: V_DOUBLY_LINKABLE [G]; o: ANY): BOOLEAN
			-- Is `o' different from `right'?
		note
			status: functional, ghost
		do
			Result := o /= right
		end

invariant
	subjects_definition: subjects =
		if attached left as c then create {MML_SET [ANY]}.singleton (c) else create {MML_SET [ANY]} end +
		if attached right as c then create {MML_SET [ANY]}.singleton (c) else create {MML_SET [ANY]} end
	observers_definition: observers = subjects
	left_consistent: attached left as l implies l.right = Current
	right_consistent: attached right as r implies r.left = Current

note
	explicit: subjects, observers
	copyright: "Copyright (c) 1984-2018, 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