Class DS_ARRAYED_LIST_CURSOR |

    indexing

>     description:

>         "Cursors for arrayed list traversals"

>     library:    "Gobo Eiffel Structure Library"
>     author:     "Eric Bezault <ericb@gobosoft.com>"
>     copyright:  "Copyright (c) 1999, Eric Bezault and others"
>     license:    "Eiffel Forum License v2 (see forum.txt)"

    class interface

>     DS_ARRAYED_LIST_CURSOR [G]

    inherit

>     DS_LIST_CURSOR [G]
>         DS_BILINEAR_CURSOR [G]
>             DS_LINEAR_CURSOR [G]
>                 DS_CURSOR [G]
>         DS_DYNAMIC_CURSOR [G]
>             DS_CURSOR [G]
>         DS_INDEXED_CURSOR [G]
>             DS_CURSOR [G]

    creation

>     make (a_list: like container)
>             -- Create a new cursor for a_list.
>         require
>             a_list_not_void: a_list /= Void
>         ensure
>             container_set: container = a_list
>             before: before

    feature -- Access

>     item: G
>             -- Item at cursor position
>             -- (Performance: O(1).)
>             -- (From DS_CURSOR.)
>         require
>             not_off: not off

>     index: INTEGER
>             -- Index of current position
>             -- (Performance: O(1).)
>             -- (From DS_INDEXED_CURSOR.)
>         ensure
>             valid_index: valid_index (Result)

>     container: DS_ARRAYED_LIST [G]
>             -- List traversed
>             -- (From DS_CURSOR.)

    feature -- Status report

>     is_first: BOOLEAN
>             -- Is cursor on first item?
>             -- (From DS_LINEAR_CURSOR.)
>         ensure
>             not_empty: Result implies not container.is_empty
>             not_off: Result implies not off
>             definition: Result implies (item = container.first)

>     is_last: BOOLEAN
>             -- Is cursor on last item?
>             -- (From DS_BILINEAR_CURSOR.)
>         ensure
>             not_empty: Result implies not container.is_empty
>             not_off: Result implies not off
>             definition: Result implies (item = container.last)

>     after: BOOLEAN
>             -- Is there no valid position to right of cursor?
>             -- (From DS_LINEAR_CURSOR.)

>     before: BOOLEAN
>             -- Is there no valid position to left of cursor?
>             -- (From DS_BILINEAR_CURSOR.)

>     off: BOOLEAN
>             -- Is there no item at cursor position?
>             -- (From DS_CURSOR.)

>     same_position (other: like Current): BOOLEAN
>             -- Is current cursor at same position as other?
>             -- (From DS_CURSOR.)
>         require
>             other_not_void: other /= Void

>     valid_index (i: INTEGER): BOOLEAN
>             -- Is i a valid index value?
>             -- (From DS_INDEXED_CURSOR.)
>         ensure
>             definition: Result = (0 <= i and i <= (container.count + 1))

    feature -- Cursor movement

>     start
>             -- Move cursor to first position.
>             -- (Performance: O(1).)
>             -- (From DS_LINEAR_CURSOR.)
>         ensure
>             empty_behavior: container.is_empty implies after
>             not_empty_behavior: not container.is_empty implies is_first

>     finish
>             -- Move cursor to last position.
>             -- (Performance: O(1).)
>             -- (From DS_BILINEAR_CURSOR.)
>         ensure
>             empty_behavior: container.is_empty implies before
>             not_empty_behavior: not container.is_empty implies is_last

>     forth
>             -- Move cursor to next position.
>             -- (Performance: O(1).)
>             -- (From DS_LINEAR_CURSOR.)
>         require
>             not_after: not after

>     back
>             -- Move cursor to previous position.
>             -- (Performance: O(1).)
>             -- (From DS_BILINEAR_CURSOR.)
>         require
>             not_before: not before

>     search_forth (v: G)
>             -- Move to first position at or after current
>             -- position where item and v are equal.
>             -- (Use equality_tester's criterion from container
>             -- if not void, use `=' criterion otherwise.)
>             -- Move after if not found.
>             -- (From DS_LINEAR_CURSOR.)
>         require
>             not_off: not off or after

>     search_back (v: G)
>             -- Move to first position at or before current
>             -- position where item and v are equal.
>             -- (Use equality_tester's criterion from container
>             -- if not void, use `=' criterion otherwise.)
>             -- Move before if not found.
>             -- (From DS_BILINEAR_CURSOR.)
>         require
>             not_off: not off or before

>     go_after
>             -- Move cursor to after position.
>             -- (Performance: O(1).)
>             -- (From DS_LINEAR_CURSOR.)
>         ensure
>             after: after

>     go_before
>             -- Move cursor to before position.
>             -- (Performance: O(1).)
>             -- (From DS_BILINEAR_CURSOR.)
>         ensure
>             before: before

>     go_to (other: like Current)
>             -- Move cursor to other's position.
>             -- (Performance: O(1).)
>             -- (From DS_CURSOR.)
>         require
>             other_not_void: other /= Void
>             valid_cursor: container.valid_cursor (other)
>         ensure
>             same_position: same_position (other)

>     go_i_th (i: INTEGER)
>             -- Move cursor to i-th position.
>             -- (Performance: O(1).)
>             -- (From DS_INDEXED_CURSOR.)
>         require
>             valid_index: valid_index (i)
>         ensure
>             moved: index = i

    feature -- Comparison

>     is_equal (other: like Current): BOOLEAN
>             -- Are other and current cursor at the same position?
>             -- (From GENERAL.)
>         require
>             other_not_void: other /= Void
>         ensure
>             consistent: standard_is_equal (other) implies Result
>             same_type: Result implies same_type (other)
>             symmetric: Result implies other.is_equal (Current)

    feature -- Duplication

>     copy (other: like Current)
>             -- Copy other to current cursor.
>             -- (From GENERAL.)
>         require
>             other_not_void: other /= Void
>             type_identity: same_type (other)
>         ensure
>             is_equal: is_equal (other)

    feature -- Element change

>     put_left (v: G)
>             -- Add v to left of cursor position.
>             -- Do not move cursors.
>             -- (Performance: O(container.count-index).)
>             -- (From DS_LIST_CURSOR.)
>         require
>             extendible: container.extendible (1)
>             not_before: not before
>         ensure
>             one_more: container.count = old (container.count) + 1

>     put_right (v: G)
>             -- Add v to right of cursor position.
>             -- Do not move cursors.
>             -- (Performance: O(container.count-index).)
>             -- (From DS_LIST_CURSOR.)
>         require
>             extendible: container.extendible (1)
>             not_after: not after
>         ensure
>             one_more: container.count = old (container.count) + 1

>     force_left (v: G)
>             -- Add v to left of cursor position.
>             -- Do not move cursors.
>             -- (Performance: O(container.count-index)[+resizing].)
>             -- (From DS_LIST_CURSOR.)
>         require
>             not_before: not before
>         ensure
>             one_more: container.count = old (container.count) + 1

>     force_right (v: G)
>             -- Add v to right of cursor position.
>             -- Do not move cursors.
>             -- (Performance: O(container.count-index)[+resizing].)
>             -- (From DS_LIST_CURSOR.)
>         require
>             not_after: not after
>         ensure
>             one_more: container.count = old (container.count) + 1

>     replace (v: G)
>             -- Replace item at cursor position by v.
>             -- (Performance: O(1).)
>             -- (From DS_DYNAMIC_CURSOR.)
>         require
>             not_off: not off
>         ensure
>             replaced: item = v

>     swap (other: DS_DYNAMIC_CURSOR [G])
>             -- Exchange items at current and other's positions.
>             -- Note: cursors may reference two different containers.
>             -- (From DS_DYNAMIC_CURSOR.)
>         require
>             not_off: not off
>             other_not_void: other /= Void
>             other_not_off: not other.off
>         ensure
>             new_item: item = old (other.item)
>             new_other: other.item = old item

>     extend_left (other: DS_LINEAR [G])
>             -- Add items of other to left of cursor position.
>             -- Keep items of other in the same order.
>             -- Do not move cursors.
>             -- (Performance: O(container.count-index+other.count).)
>             -- (From DS_LIST_CURSOR.)
>         require
>             other_not_void: other /= Void
>             extendible: container.extendible (other.count)
>             not_before: not before
>         ensure
>             new_count: container.count = old (container.count) + other.count

>     extend_right (other: DS_LINEAR [G])
>             -- Add items of other to right of cursor position.
>             -- Keep items of other in the same order.
>             -- Do not move cursors.
>             -- (Performance: O(container.count-index+other.count).)
>             -- (From DS_LIST_CURSOR.)
>         require
>             other_not_void: other /= Void
>             extendible: container.extendible (other.count)
>             not_after: not after
>         ensure
>             new_count: container.count = old (container.count) + other.count

>     append_left (other: DS_LINEAR [G])
>             -- Add items of other to left of cursor position.
>             -- Keep items of other in the same order.
>             -- Do not move cursors.
>             -- (Performance: O(container.count-index+other.count)[+resizing].)
>             -- (From DS_LIST_CURSOR.)
>         require
>             other_not_void: other /= Void
>             not_before: not before
>         ensure
>             new_count: container.count = old (container.count) + other.count

>     append_right (other: DS_LINEAR [G])
>             -- Add items of other to right of cursor position.
>             -- Keep items of other in the same order.
>             -- Do not move cursors.
>             -- (Performance: O(container.count-index+other.count)[+resizing].)
>             -- (From DS_LIST_CURSOR.)
>         require
>             other_not_void: other /= Void
>             not_after: not after
>         ensure
>             new_count: container.count = old (container.count) + other.count

    feature -- Removal

>     remove
>             -- Remove item at cursor position.
>             -- Move any cursors at this position forth.
>             -- (Performance: O(container.count-index).)
>             -- (From DS_LIST_CURSOR.)
>         require
>             not_off: not off
>         ensure
>             one_less: container.count = old (container.count) - 1

>     remove_left
>             -- Remove item to left of cursor position.
>             -- Move any cursors at this position forth.
>             -- (Performance: O(container.count-index).)
>             -- (From DS_LIST_CURSOR.)
>         require
>             not_empty: not container.is_empty
>             not_before: not before
>             not_first: not is_first
>         ensure
>             one_less: container.count = old (container.count) - 1

>     remove_right
>             -- Remove item to right of cursor position.
>             -- Move any cursors at this position forth.
>             -- (Performance: O(container.count-index).)
>             -- (From DS_LIST_CURSOR.)
>         require
>             not_empty: not container.is_empty
>             not_after: not after
>             not_last: not is_last
>         ensure
>             one_less: container.count = old (container.count) - 1

>     prune_left (n: INTEGER)
>             -- Remove n items to left of cursor position.
>             -- Move all cursors off.
>             -- (Performance: O(container.count-index).)
>             -- (From DS_LIST_CURSOR.)
>         require
>             valid_n: 0 <= n and n < index
>         ensure
>             new_count: container.count = old (container.count) - n

>     prune_right (n: INTEGER)
>             -- Remove n items to right of cursor position.
>             -- Move all cursors off.
>             -- (Performance: O(container.count-index-n).)
>             -- (From DS_LIST_CURSOR.)
>         require
>             valid_n: 0 <= n and n <= (container.count - index)
>         ensure
>             new_count: container.count = old (container.count) - n

    invariant

>     container_not_void: container /= Void
>     empty_constraint: container.is_empty implies off
>         -- (From DS_CURSOR.)

>     after_constraint: after implies off
>         -- (From DS_LINEAR_CURSOR.)

>     not_both: not (after and before)
>     before_constraint: before implies off
>         -- (From DS_BILINEAR_CURSOR.)

    end -- class DS_ARRAYED_LIST_CURSOR