note
	description: "[
			Singly linked lists.
			Random access takes linear time. 
			Once a position is found, inserting or removing elements to the right of it takes constant time 
			and doesn't require reallocation of other elements.
		]"
	author: "Nadia Polikarpova"
	revised_by: "Alexander Kogtenkov"
	model: sequence
	manual_inv: true
	false_guards: true

frozen class
	V_LINKED_LIST [G]

inherit
	V_LIST [G]
		redefine
			first,
			last,
			new_cursor,
			is_equal_,
			reverse
		end

feature -- Initialization

	copy_ (other: V_LIST [G])
			-- Initialize by copying all the items of `other'.
		note
			explicit: wrapping
		require
			observers_open: ∀ o: observers ¦ o.is_open
		local
			i: V_LIST_ITERATOR [G]
		do
			if other /= Current then
				wipe_out
				i := other.new_cursor
				append (i)
				other.forget_iterator (i)
			end
		ensure
			sequence_effect: sequence ~ old other.sequence
			observers_open: ∀ o: observers ¦ o.is_open
			observers_preserved: other.observers ~ old other.observers
			modify_model ("sequence", Current)
			modify_field (["observers", "closed"], other)
		end

feature -- Access

	item alias "[]" (i: INTEGER): G assign put
			-- Value at position `i'.
		do
			check inv end
			if i = count then
				Result := last
			else
				Result := cell_at (i).item
			end
		end

	first: G
			-- First element.
		do
			check inv end
			if attached first_cell as c then
				Result := c.item
			else
				check
					from_precondition: False
				then
				end
			end
		end

	last: G
			-- Last element.
		do
			check inv end
			if attached last_cell as c then
				Result := c.item
			else
				check
					from_precondition: False
				then
				end
			end
		end

feature -- Iteration

	new_cursor: like at
			-- New iterator pointing to the first position.
		note
			status: impure
		do
			create Result.make (Current)
			Result.start
		end

	at (i: INTEGER): V_LINKED_LIST_ITERATOR [G]
			-- New iterator pointing at position `i'.
		note
			status: impure
		do
			create Result.make (Current)
			check Result.inv end
			check inv_only ("lower_definition") end
			if i < 1 then
				Result.go_before
			elseif i > count then
				Result.go_after
			else
				Result.go_to (i)
			end
		end

feature -- Comparison

	is_equal_ (other: like Current): BOOLEAN
			-- Is list made of the same values in the same order as `other'?
			-- (Use reference comparison.)
		local
			c1, c2: V_LINKABLE [G]
			i_: INTEGER
		do
			check inv end
			if other = Current then
				Result := True
			elseif count = other.count then
				check
					other.inv
				end
				Result := True
				c1 := first_cell
				c2 := other.first_cell
				if attached c1 then
					if not attached c2 then
						check from_same_count_and_non_empty: False then end
					end
					from
						i_ := 1
					invariant
						1 <= i_ and i_ <= sequence.count + 1
						other.inv
						i_ <= sequence.count implies c1 = cells [i_] and c2 = other.cells [i_]
						i_ = sequence.count + 1 implies c1 = Void and c2 = Void
						if Result
							then ∀ k: 1 |..| (i_ - 1) ¦ sequence [k] = other.sequence [k]
							else sequence [i_ - 1] /= other.sequence [i_ - 1] end
					until
						c1 = Void or not Result
					loop
						if not attached c2 then
							check from_exit_condition_and_loop_invariant: False then end
						end
						Result := c1.item = c2.item
						c1 := c1.right
						c2 := c2.right
						i_ := i_ + 1
					variant
						sequence.count - i_
					end
				end
			end
		end

feature -- Replacement

	put (v: G; i: INTEGER)
			-- Associate `v' with index `i'.
		note
			explicit: wrapping
		do
			check inv end
			put_cell (v, cell_at (i), i)
		end

	reverse
			-- Reverse the order of elements.
		note
			explicit: wrapping
		local
			rest, next: V_LINKABLE [G]
			rest_cells: MML_SEQUENCE [V_LINKABLE [G]]
		do
			lemma_cells_distinct
			unwrap
			from
				last_cell := first_cell
				rest := first_cell
				rest_cells := cells
				first_cell := Void
				create cells
				create sequence
			invariant
				∀ i: 1 |..| count_ ¦ cells.old_ [i].is_wrapped
				rest_cells.count = count_ - cells.count
				inv_only ("cells_domain", "first_cell_empty", "cells_exist", "sequence_implementation", "cells_linked", "cells_first", "cells_last")

				rest_cells.non_void
				is_linked (rest_cells)
				not rest_cells.is_empty implies rest = rest_cells.first and rest_cells.last.right = Void
				rest_cells.is_empty = (rest = Void)

				cells.old_.tail (cells.count + 1) = rest_cells
				∀ i: 1 |..| cells.count ¦ cells [i] = cells.old_ [cells.count - i + 1]
				cells.range = cells.old_.front (cells.count).range

				modify_field (["first_cell", "cells", "sequence"], Current)
				modify_model ("right", cells.old_.range)
			until
				rest = Void
			loop
				next := rest.right
				rest.put_right (first_cell)
				first_cell := rest
				check cells.prepended (rest).range = cells.range & rest end
				cells := cells.prepended (rest)
				sequence := sequence.prepended (rest.item)
				rest := next
				rest_cells := rest_cells.but_first
			variant
				rest_cells.count
			end
			wrap
		end

feature -- Extension

	extend_front (v: G)
			-- Insert `v' at the front.
		local
			cell: V_LINKABLE [G]
		do
			create cell.put (v)
			if attached first_cell as f then
				cell.put_right (f)
			else
				last_cell := cell
			end
			first_cell := cell
			count_ := count_ + 1

			cells := cells.prepended (cell)
			sequence := sequence.prepended (v)
		ensure then
			cells_preserved: old cells ~ cells.but_first
		end

	extend_back (v: G)
			-- Insert `v' at the back.
		local
			cell: V_LINKABLE [G]
		do
			create cell.put (v)
			if first_cell = Void then
				first_cell := cell
			else
				if attached last_cell as l then
					l.put_right (cell)
				else
					check from_condition: False then end
				end
			end
			last_cell := cell
			count_ := count_ + 1

			cells := cells & cell
			sequence := sequence & v
		ensure then
			cells_preserved: old cells ~ cells.but_last
		end

	extend_at (v: G; i: INTEGER)
			-- Insert `v' at position `i'.
		note
			explicit: wrapping
		do
			check inv end
			if i = 1 then
				extend_front (v)
			elseif i = count + 1 then
				extend_back (v)
			else
				extend_after (create {V_LINKABLE [G]}.put (v), cell_at (i - 1), i - 1)
			end
		end

	prepend (input: V_ITERATOR [G])
			-- Prepend sequence of values, over which `input' iterates.
		note
			explicit: wrapping
		local
			it: V_LINKED_LIST_ITERATOR [G]
		do
			if not input.after then
				check input.inv end
				extend_front (input.item)
				input.forth

				from
					it := new_cursor
				invariant
					1 <= input.index_ and input.index_ <= input.sequence.count + 1
					1 <= it.index_ and it.index_ <= it.sequence.count
					it.index_ = input.index_ - input.index_.old_
					sequence ~ input.sequence.interval (input.index_.old_, input.index_ - 1) + sequence.old_
					is_wrapped
					input.is_wrapped
					it.is_wrapped
					it.target = Current
					observers = observers.old_ & it
					∀ o: observers.old_ ¦ o.is_open
					cells.old_ ~ cells.tail (it.index_ + 1)
				until
					input.after
				loop
					check it.inv_only ("no_observers", "subjects_definition", "sequence_definition") end
					it.extend_right (input.item)
					check it.inv_only ("sequence_definition") end
					it.forth
					input.forth
				variant
					input.sequence.count - input.index_
				end
				forget_iterator (it)
			end
		ensure then
			cells_preserved: old cells ~ cells.tail (input.sequence.count - old input.index_ + 2)
		end

	insert_at (input: V_ITERATOR [G]; i: INTEGER)
			-- Insert sequence of values, over which `input' iterates, starting at position `i'.
		note
			explicit: wrapping
		local
			it: V_LINKED_LIST_ITERATOR [G]
			s: like sequence
		do
			if i = 1 then
				prepend (input)
			else
				from
					it := at (i - 1)
					check input.inv_only ("subjects_definition", "index_constraint", "no_observers") end
					check inv_only ("lower_definition") end
					create s
				invariant
					1 <= input.index_ and input.index_ <= input.sequence.count + 1
					i - 1 <= it.index_
					it.index_ <= it.sequence.count
					it.index_ - i + 1 = input.index_ - input.index_.old_
					s = input.sequence.interval (input.index_.old_, input.index_ - 1)
					sequence ~ sequence.old_.front (i - 1) + s + sequence.old_.tail (i)
					is_wrapped
					input.is_wrapped
					it.is_wrapped
					it.target = Current
					observers = observers.old_ & it
					∀ o: observers.old_ ¦ o.is_open
				until
					input.after
				loop
					check it.inv_only ("no_observers", "subjects_definition", "sequence_definition") end
					it.extend_right (input.item)
					s := s & input.item
					check it.inv_only ("sequence_definition") end
					it.forth
					input.forth
				variant
					input.sequence.count - input.index_
				end
				forget_iterator (it)
			end
		end

feature -- Removal

	remove_front
			-- Remove first element.
		do
			if attached first_cell as f then
				if count_ = 1 then
					last_cell := Void
				else
					check f.right = cells [2] end
				end
				first_cell := f.right
			else
				check from_precondition: False then end
			end
			count_ := count_ - 1

			cells := cells.but_first
			sequence := sequence.but_first
		ensure then
			cells_preserved: cells ~ old cells.but_first
		end

	remove_back
			-- Remove last element.
		note
			explicit: wrapping
		do
			check inv end
			if count = 1 then
				wipe_out
				check inv_only ("cells_domain") end
			else
				remove_after (cell_at (count - 1), count - 1)
			end
		ensure then
			cells_preserved: cells ~ old cells.but_last
		end

	remove_at (i: INTEGER)
			-- Remove element at position `i'.
		note
			explicit: wrapping
		do
			check inv end
			if i = 1 then
				remove_front
			else
				remove_after (cell_at (i - 1), i - 1)
			end
		ensure then
			cells_preserved: cells ~ old cells.removed_at (i)
		end

	wipe_out
			-- Remove all elements.
		do
			first_cell := Void
			last_cell := Void
			count_ := 0
			create cells
			create sequence
		ensure then
			old_cells_wrapped: ∀ c: old owns ¦ c.is_wrapped
			cells_exist: (old cells).non_void
			cells_linked: is_linked (old cells)
			items_unchanged: ∀ i: 1 |..| old sequence.count ¦ (old sequence) [i] = (old cells) [i].item
			cells_last: old cells.count > 0 implies (attached old last_cell as c and then not attached c.right)
		end

feature {V_CONTAINER, V_ITERATOR} -- Implementation

	first_cell: detachable V_LINKABLE [G]
			-- First cell of the list.

	last_cell: detachable V_LINKABLE [G]
			-- Last cell of the list.

	cell_at (i: INTEGER): V_LINKABLE [G]
			-- Cell at position `i'.
		require
			valid_position: 1 <= i and i <= cells.count
			inv_only ("cells_domain", "cells_exist", "cells_first", "cells_linked")
		local
			j: INTEGER
		do
			from
				j := 1
				Result := first_cell
				if not attached Result then
					check from_precondition: False then end
				end
			invariant
				1 <= j and j <= i
				Result = cells [j]
			until
				j = i
			loop
				if not attached Result then
					check from_loop_invariant: False then end
				end
				Result := Result.right
				j := j + 1
			end
		ensure
			definition: Result = cells [i]
		end

	put_cell (v: G; c: V_LINKABLE [G]; index_: INTEGER)
			-- Put `v' into `c' located at `index_'.
		require
			index_in_domain: cells.domain [index_]
			c_in_list: cells [index_] = c
			wrapped: is_wrapped
			observers_open: ∀ o: observers ¦ o.is_open
		do
			lemma_cells_distinct
			unwrap
			c.put (v)
			sequence := sequence.replaced_at (index_, v)
			wrap
		ensure
			sequence ~ old sequence.replaced_at (index_, v)
			cells ~ old cells
			wrapped: is_wrapped
			modify_model ("sequence", Current)
		end

	extend_after (new, c: V_LINKABLE [G]; index_: INTEGER)
			-- Add a new cell with value `v' after `c'.
		require
			wrapped: is_wrapped
			observers_open: ∀ o: observers ¦ o.is_open
			new_is_wrapped: new.is_wrapped

			new_not_current: new /= Current
			index_in_domain: 1 <= index_ and index_ <= cells.count
			c_in_list: cells [index_] = c
			new_right_void: new.right = Void
		do
			lemma_cells_distinct
			unwrap

			check index_ < cells.count implies c.right = cells [index_ + 1] end

			if c.right = Void then
				last_cell := new
			else
				new.put_right (c.right)
			end
			c.put_right (new)
			count_ := count_ + 1

			cells := cells.extended_at (index_ + 1, new)
			sequence := sequence.extended_at (index_ + 1, new.item)
			wrap
		ensure
			sequence ~ old sequence.extended_at (index_ + 1, new.item)
			cells ~ old cells.extended_at (index_ + 1, new)
			wrapped: is_wrapped
			modify_model ("sequence", Current)
			modify_model ("right", new)
		end

	remove_after (c: V_LINKABLE [G]; index_: INTEGER)
			-- Remove the cell to the right of `c'.
		require
			valid_index: 1 <= index_ and index_ <= sequence.count - 1
			c_in_list: cells [index_] = c
			wrapped: is_wrapped
			observers_open: ∀ o: observers ¦ o.is_open
		do
			lemma_cells_distinct
			unwrap
			check c.right = cells [index_ + 1] end
			if attached c.right as r then
				check index_ + 1 < cells.count implies r.right = cells [index_ + 2] end
				c.put_right (r.right)
				if c.right = Void then
					last_cell := c
				end
			else
				check from_precondition: False then end
			end
			count_ := count_ - 1

			cells := cells.removed_at (index_ + 1)
			sequence := sequence.removed_at (index_ + 1)
			wrap
		ensure
			sequence ~ old sequence.removed_at (index_ + 1)
			cells ~ old cells.removed_at (index_ + 1)
			wrapped: is_wrapped
			modify_model ("sequence", Current)
		end

	merge_after (other: V_LINKED_LIST [G]; c: detachable V_LINKABLE [G]; index_: INTEGER)
			-- Merge `other' into `Current' after cell `c'. If `c' is `Void', merge to the front.
		require
			valid_index: 0 <= index_ and index_ <= cells.count
			c_void_if_before: (index_ = 0) = (c = Void)
			c_in_list_if_in_domain: 1 <= index_ implies cells [index_] = c
			other_not_current: other /= Current
			wrapped: is_wrapped
			other_wrapped: other.is_wrapped
			observers_open: ∀ o: observers ¦ o.is_open
			other_observers_open: ∀ o: other.observers ¦ o.is_open
		local
			other_first, other_last: V_LINKABLE [G]
			other_count: INTEGER
		do
			check other.inv_only ("count_definition", "cells_domain", "first_cell_empty", "owns_definition", "cells_first", "cells_last") end
			other_count := other.count_
			if other_count > 0 then
				lemma_cells_distinct
				other.lemma_cells_distinct

				other_first := other.first_cell
				other_last := other.last_cell
				if
					not attached other_first or else
					not attached other_last
				then
					check from_condition: False then end
				end
				other.wipe_out

				unwrap
				if c = Void then
					if attached first_cell as f then
						other_last.put_right (f)
					else
						last_cell := other_last
					end
					first_cell := other_first
				else
					check index_ < cells.count implies c.right = cells [index_ + 1] end
					if c.right = Void then
						last_cell := other_last
					else
						other_last.put_right (c.right)
					end
					c.put_right (other_first)
				end
				count_ := count_ + other_count
				cells := cells.front (index_) + other.cells.old_ + cells.tail (index_ + 1)
				sequence := sequence.front (index_) + other.sequence.old_ + sequence.tail (index_ + 1)
				wrap
			end
		ensure
			wrapped: is_wrapped
			other_wrapped: other.is_wrapped
			sequence_effect: sequence = old (sequence.front (index_) + other.sequence + sequence.tail (index_ + 1))
			other_sequence_effect: other.sequence.is_empty
			cells_effect: cells = old (cells.front (index_) + other.cells + cells.tail (index_ + 1))
			modify_model ("sequence", [Current, other])
		end

feature -- Specificaton

	cells: MML_SEQUENCE [V_LINKABLE [G]]
			-- Sequence of linakble cells.
		note
			status: ghost
		attribute
			check is_executable: False then end
		end

feature {V_CONTAINER, V_ITERATOR} -- Specificaton

	lemma_cells_distinct
			-- All cells in `cells' are distinct.
		note
			status: lemma
		require
			closed
		do
			check inv end
			if cells.count > 0 then
				lemma_cells_distinct_from (1)
			end
		ensure
			cells_distinct: cells.no_duplicates
		end

	lemma_cells_distinct_from (i: INTEGER)
			-- All cells in `cells' starting from `i' are distinct.
		note
			status: lemma
		require
			in_bounds: 1 <= i and i <= cells.count
			inv_only ("cells_domain", "cells_exist", "cells_linked", "cells_last")
			decreases (cells.count - i)
		do
			if i /= cells.count then
				lemma_cells_distinct_from (i + 1)
				check cells [i].right = cells [i + 1] end
				check ∀ j: (i + 1) |..| (cells.count - 1) ¦ cells [j].right = cells [j + 1] end
			end
		ensure
			cells_distinct: ∀ j: i |..| cells.count ¦
					∀ k: i |..| cells.count ¦
						j < k implies cells [j] /= cells [k]
		end

	is_linked (cs: like cells): BOOLEAN
			-- Are adjacent cells of `cs' liked to each other?
		note
			status: ghost, functional, static
		require
			cs.non_void
			reads_field ("right", cs)
		do
			Result := ∀ i: 1 |..| cs.count ¦
					∀ j: 1 |..| cs.count ¦
						i + 1 = j implies cs [i].right = cs [j]
		end

invariant
	cells_domain: sequence.count = cells.count
	first_cell_empty: cells.is_empty = (first_cell = Void)
	last_cell_empty: cells.is_empty = (last_cell = Void)
	owns_definition: owns = cells.range
	cells_exist: cells.non_void
	sequence_implementation: ∀ i: 1 |..| cells.count ¦ sequence [i] = cells [i].item
	cells_linked: is_linked (cells)
	cells_first: cells.count > 0 implies first_cell = cells.first
	cells_last: cells.count > 0 implies attached last_cell as l and then l = cells.last and then l.right = Void

note
	explicit: observers
	date: "$Date$"
	revision: "$Revision$"
	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