note
	description: "Sequences where values can be updated."
	author: "Nadia Polikarpova"
	revised_by: "Alexander Kogtenkov"
	model: sequence, lower_
	manual_inv: true
	false_guards: true

deferred class
	V_MUTABLE_SEQUENCE [G]

inherit
	V_SEQUENCE [G]
		redefine
			item
		end

feature -- Access

	item alias "[]" (i: INTEGER): G assign put
			-- Value at position `i'.
		deferred
		end

feature -- Iteration

	at (i: INTEGER): V_MUTABLE_SEQUENCE_ITERATOR [G]
			-- New iterator pointing at position `i'.
		note
			status: impure
		deferred
		end

feature -- Replacement

	put (v: G; i: INTEGER)
			-- Replace value at position `i' with `v'.
		require
			has_index: has_index (i)
			observers_open: ∀ o: observers ¦ o.is_open
		deferred
		ensure
			sequence_effect: sequence ~ old sequence.replaced_at (idx (i), v)
			modify_model ("sequence", Current)
		end

	swap (i1, i2: INTEGER)
			-- Swap values at positions `i1' and `i2'.
		note
			status: nonvariant
		require
			has_index_one: has_index (i1)
			has_index_two: has_index (i2)
			observers_open: ∀ o: observers ¦ o.is_open
		local
			v: G
		do
			v := item (i1)
			put (item (i2), i1)
			put (v, i2)
		ensure
			sequence_effect: sequence ~ old sequence.replaced_at (idx (i1), sequence [idx (i2)]).replaced_at (idx (i2), sequence [idx (i1)])
			modify_model ("sequence", Current)
		end

	fill (v: G; l, u: INTEGER)
			-- Put `v' at positions [`l', `u'].
		note
			status: nonvariant
		require
			l_not_too_small: l >= lower_
			u_not_too_large: u <= upper_
			l_not_too_large: l <= u + 1
			observers_open: ∀ o: observers ¦ o.is_open
		local
			it: V_MUTABLE_SEQUENCE_ITERATOR [G]
			j: INTEGER
		do
			from
				it := at (l)
				j := l
			invariant
				is_wrapped and it.is_wrapped
				it.inv_only ("sequence_definition")
				it.index_ = idx (j)
				l <= j and j <= u + 1
				upper_ = upper_.old_
				∀ i: 1 |..| sequence.count ¦ sequence [i] = if idx (l) <= i and i < idx (j) then v else sequence.old_ [i] end
				modify_model (["index_", "sequence"], it)
				modify_model ("sequence", Current)
			until
				j > u
			loop
				it.put (v)
				it.forth
				j := j + 1
			end

			forget_iterator (it)
		ensure
			sequence_domain_effect: sequence.count = old sequence.count
			sequence_changed_effect: ∀ i: idx (l) |..| idx (u) ¦ sequence [i] = v
			sequence_front_unchanged: ∀ i: 1 |..| idx (l - 1) ¦ sequence [i] = (old sequence) [i]
			sequence_tail_unchanged: ∀ i: idx (u + 1) |..| sequence.count ¦ sequence [i] = (old sequence) [i]
			observers_restored: observers ~ old observers
			modify_model (["sequence", "observers"], Current)
		end

	clear (l, u: INTEGER)
			-- Put default value at positions [`l', `u'].
		note
			status: nonvariant
		require
			l_not_too_small: l >= lower_
			u_not_too_large: u <= upper_
			l_not_too_large: l <= u + 1
			observers_open: ∀ o: observers ¦ o.is_open
		do
			fill (({G}).default, l, u)
		ensure
			sequence_domain_effect: sequence.count = old sequence.count
			sequence_changed_effect: ∀ i: idx (l) |..| idx (u) ¦ sequence [i] = ({G}).default
			sequence_front_unchanged: ∀ i: 1 |..| idx (l - 1) ¦ sequence [i] = (old sequence) [i]
			sequence_tail_unchanged: ∀ i: idx (u + 1) |..| sequence.count ¦ sequence [i] = (old sequence) [i]
			observers_restored: observers ~ old observers
			modify_model (["sequence", "observers"], Current)
		end

	copy_range (other: V_SEQUENCE [G]; other_first, other_last, index: INTEGER)
			-- Copy items of `other' within bounds [`other_first', `other_last'] to current sequence starting at index `index'.
		note
			status: nonvariant
		require
			other_not_current: other /= Current
			other_first_not_too_small: other_first >= other.lower_
			other_last_not_too_large: other_last <= other.upper_
			other_first_not_too_large: other_first <= other_last + 1
			index_not_too_small: index >= lower_
			enough_space: upper_ - index >= other_last - other_first
			observers_open: ∀ o: observers ¦ o.is_open
		local
			other_it: V_SEQUENCE_ITERATOR [G]
			it: V_MUTABLE_SEQUENCE_ITERATOR [G]
			j, n: INTEGER
		do
			n := other_last - other_first + 1
			from
				j := 0
				other_it := other.at (other_first)
				it := at (index)
			invariant
				is_wrapped and other.is_wrapped
				it.is_wrapped and other_it.is_wrapped
				it.inv_only ("sequence_definition")
				it.index_ = idx (index + j)
				other_it.index_ = other.idx (other_first + j)
				0 <= j and j <= n
				upper_ = upper_.old_
				∀ i: 1 |..| sequence.count ¦ not (idx (index) <= i and i < idx (index + j)) implies
						sequence [i] = sequence.old_ [i]
				∀ i: 1 |..| sequence.count ¦ idx (index) <= i and i < idx (index + j) implies
						sequence [i] = other.sequence [i - idx (index) + other.idx (other_first)]
				modify_model (["index_", "sequence"], it)
				modify_model ("index_", other_it)
				modify_model ("sequence", Current)
			until
				j >= n
			loop
				it.put (other_it.item)
				other_it.forth
				it.forth
				j := j + 1
			end

			other.forget_iterator (other_it)
			forget_iterator (it)
		ensure
			sequence_domain_effect: sequence.count = old sequence.count
			sequence_effect: ∀ i: 1 |..| sequence.count ¦ if idx (index) <= i and i < idx (index + other_last - other_first + 1)
					then sequence [i] = other.sequence [i - idx (index) + other.idx (other_first)]
					else sequence [i] = (old sequence) [i] end
			observers_restored: observers ~ old observers
			other_observers_restored: other.observers ~ old other.observers
			modify_model (["sequence", "observers"], Current)
			modify_model ("observers", other)
		end

	reverse
			-- Reverse the order of elements.
		note
			status: nonvariant
		require
			observers_open: ∀ o: observers ¦ o.is_open
		local
			j, k: INTEGER
		do
			from
				j := lower
				k := upper
			invariant
				upper_ = upper_.old_
				lower_ <= j and j <= k + 1 and k <= upper_
				k = lower_ + upper_ - j
				∀ i: idx (j) |..| idx (k) ¦ sequence [i] = sequence.old_ [i]
				∀ i: 1 |..| idx (j - 1) ¦ sequence [i] = sequence.old_ [sequence.count - i + 1]
				∀ i: idx (k + 1) |..| sequence.count ¦ sequence [i] = sequence.old_ [sequence.count - i + 1]
				is_wrapped
				observers ~ observers.old_
			until
				j >= k
			loop
				swap (j, k)
				j := j + 1
				k := k - 1
			end
		ensure
			sequence_domain_effect: sequence.count = old sequence.count
			sequence_effect: ∀ i: 1 |..| sequence.count ¦ sequence [i] = (old sequence) [sequence.count - i + 1]
			modify_model (["sequence"], Current)
		end

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