note description: "[ Lists implemented as sequences of arrays, the last of which may be non-full. No limit on size (a new array is allocated if list outgrows its initial allocation). ]" library: "Free implementation of ELKS library" legal: "See notice at end of class." status: "See notice at end of class." names: list, sequence representation: array, linked access: index, cursor, membership contents: generic date: "$Date: 2018-12-15 18:06:16 +0000 (Sat, 15 Dec 2018) $" revision: "$Revision: 102608 $" class MULTI_ARRAY_LIST [G] create make feature {NONE} -- Initialization default_create -- Process instances of classes with no creation clause. -- (Default: do nothing.) -- (from ANY) do end make (b: INTEGER_32) -- Create an empty list, setting block_size to b do block_size := b first_element := new_cell (create {ARRAYED_LIST [G]}.make (b)) last_element := first_element active := first_element end feature -- Access at alias "@" (i: INTEGER_32): like item assign put_i_th -- Item at i-th position -- Was declared in CHAIN as synonym of i_th. -- (from CHAIN) require -- from TABLE valid_key: valid_index (i) local pos: CURSOR do pos := cursor go_i_th (i) Result := item go_to (pos) end block_size: INTEGER_32 cursor: MULTAR_LIST_CURSOR [G] -- Current cursor position do create Result.make (active, active.item.index, index) ensure -- from CURSOR_STRUCTURE cursor_not_void: Result /= Void end first: like item -- Item at first position require -- from CHAIN not_empty: not is_empty do Result := first_element.item.first end first_element: BI_LINKABLE [ARRAYED_LIST [G]] -- First array_sequence element of the list generating_type: TYPE [detachable MULTI_ARRAY_LIST [G]] -- Type of current object -- (type of which it is a direct instance) -- (from ANY) external "built_in" ensure -- from ANY generating_type_not_void: Result /= Void end generator: STRING_8 -- Name of current object's generating class -- (base class of the type of which it is a direct instance) -- (from ANY) external "built_in" ensure -- from ANY generator_not_void: Result /= Void generator_not_empty: not Result.is_empty end sequential_has (v: like item): BOOLEAN -- Does structure include an occurrence of v? -- (Reference or object equality, -- based on object_comparison.) -- (from LINEAR) require -- from CONTAINER True do start if not off then search (v) end Result := not exhausted ensure -- from CONTAINER not_found_in_empty: Result implies not is_empty end has (v: like item): BOOLEAN -- Does list include v? -- (Reference or object equality, -- based on object_comparison.) local pos: CURSOR do if not is_empty then pos := cursor start search (v) Result := not after go_to (pos) end end i_th alias "[]" (i: INTEGER_32): like item assign put_i_th -- Item at i-th position -- Was declared in CHAIN as synonym of at. -- (from CHAIN) require -- from TABLE valid_key: valid_index (i) require -- from READABLE_INDEXABLE valid_index: valid_index (i) local pos: CURSOR do pos := cursor go_i_th (i) Result := item go_to (pos) end index: INTEGER_32 -- Current cursor index sequential_index_of (v: like item; i: INTEGER_32): INTEGER_32 -- Index of i-th occurrence of v. -- 0 if none. -- (Reference or object equality, -- based on object_comparison.) -- (from LINEAR) require -- from LINEAR positive_occurrences: i > 0 local occur, pos: INTEGER_32 do if object_comparison and v /= Void then from start pos := 1 until exhausted or (occur = i) loop if item ~ v then occur := occur + 1 end forth pos := pos + 1 end else from start pos := 1 until exhausted or (occur = i) loop if item = v then occur := occur + 1 end forth pos := pos + 1 end end if occur = i then Result := pos - 1 end ensure -- from LINEAR non_negative_result: Result >= 0 end index_of (v: like item; i: INTEGER_32): INTEGER_32 -- Index of i-th occurrence of item identical to v. -- (Reference or object equality, -- based on object_comparison.) -- 0 if none. -- (from CHAIN) local pos: CURSOR do pos := cursor Result := sequential_index_of (v, i) go_to (pos) end item: G -- Item at cursor position require -- from ACTIVE readable: readable require -- from TRAVERSABLE not_off: not off do Result := active.item.item end item_for_iteration: G -- Item at current position -- (from LINEAR) require -- from LINEAR not_off: not off do Result := item end last: like item -- Item at last position require -- from CHAIN not_empty: not is_empty do Result := last_element.item.last end last_element: BI_LINKABLE [ARRAYED_LIST [G]] -- Last array_sequence element of the list new_cursor: INDEXABLE_ITERATION_CURSOR [G] -- Fresh cursor associated with current structure -- (from READABLE_INDEXABLE) require -- from ITERABLE True do create {READABLE_INDEXABLE_ITERATION_CURSOR [G]} Result.make (Current); Result.start ensure -- from ITERABLE result_attached: Result /= Void end sequential_occurrences (v: like item): INTEGER_32 -- Number of times v appears. -- (Reference or object equality, -- based on object_comparison.) -- (from LINEAR) require -- from BAG True do from start search (v) until exhausted loop Result := Result + 1 forth search (v) end ensure -- from BAG non_negative_occurrences: Result >= 0 end feature -- Measurement count: INTEGER_32 -- Number of items index_set: INTEGER_INTERVAL obsolete "Use `lower' and `upper' instead. [2017-05-31]" -- Range of acceptable indexes. -- (from READABLE_INDEXABLE) do create Result.make (Lower, count) ensure -- from READABLE_INDEXABLE not_void: Result /= Void empty_if_not_in_order: (Lower > count) implies Result.is_empty same_lower_if_not_empty: (Lower <= count) implies Result.lower = Lower same_upper_if_not_empty: (Lower <= count) implies Result.upper = count end Lower: INTEGER_32 = 1 -- Minimum index. -- (from CHAIN) occurrences (v: like item): INTEGER_32 -- Number of times v appears. -- (Reference or object equality, -- based on object_comparison.) -- (from CHAIN) local pos: CURSOR do pos := cursor Result := sequential_occurrences (v) go_to (pos) end feature {NONE} -- Measurement estimated_count_of (other: ITERABLE [G]): INTEGER_32 -- Estimated number of elements in other. -- (from CONTAINER) do if attached {FINITE [G]} other as f then Result := f.count elseif attached {READABLE_INDEXABLE [G]} other as r then Result := r.upper - r.lower + 1 end ensure -- from CONTAINER instance_free: class non_negative_result: Result >= 0 end feature -- Comparison frozen deep_equal (a: detachable ANY; b: like arg #1): BOOLEAN -- Are a and b either both void -- or attached to isomorphic object structures? -- (from ANY) do if a = Void then Result := b = Void else Result := b /= Void and then a.is_deep_equal (b) end ensure -- from ANY instance_free: class shallow_implies_deep: standard_equal (a, b) implies Result both_or_none_void: (a = Void) implies (Result = (b = Void)) same_type: (Result and (a /= Void)) implies (b /= Void and then a.same_type (b)) symmetric: Result implies deep_equal (b, a) end frozen equal (a: detachable ANY; b: like arg #1): BOOLEAN -- Are a and b either both void or attached -- to objects considered equal? -- (from ANY) do if a = Void then Result := b = Void else Result := b /= Void and then a.is_equal (b) end ensure -- from ANY instance_free: class definition: Result = (a = Void and b = Void) or else ((a /= Void and b /= Void) and then a.is_equal (b)) end frozen is_deep_equal alias "≡≡≡" (other: MULTI_ARRAY_LIST [G]): BOOLEAN -- Are Current and other attached to isomorphic object structures? -- (from ANY) require -- from ANY other_not_void: other /= Void external "built_in" ensure -- from ANY shallow_implies_deep: standard_is_equal (other) implies Result same_type: Result implies same_type (other) symmetric: Result implies other.is_deep_equal (Current) end is_equal (other: MULTI_ARRAY_LIST [G]): BOOLEAN -- Does other contain the same elements? -- (from LIST) require -- from ANY other_not_void: other /= Void do if Current = other then Result := True else Result := (is_empty = other.is_empty) and (object_comparison = other.object_comparison) and (count = other.count) if Result and not is_empty then if attached cursor as c1 and then attached other.cursor as c2 then from start; other.start until after or not Result loop if object_comparison then Result := item ~ other.item else Result := item = other.item end forth; other.forth end go_to (c1); other.go_to (c2) else check cursors_exist: False end end elseif is_empty and other.is_empty and object_comparison = other.object_comparison then Result := True end end ensure -- from ANY symmetric: Result implies other ~ Current consistent: standard_is_equal (other) implies Result ensure then -- from LIST indices_unchanged: index = old index and other.index = old other.index true_implies_same_size: Result implies count = other.count end frozen standard_equal (a: detachable ANY; b: like arg #1): BOOLEAN -- Are a and b either both void or attached to -- field-by-field identical objects of the same type? -- Always uses default object comparison criterion. -- (from ANY) do if a = Void then Result := b = Void else Result := b /= Void and then a.standard_is_equal (b) end ensure -- from ANY instance_free: class definition: Result = (a = Void and b = Void) or else ((a /= Void and b /= Void) and then a.standard_is_equal (b)) end frozen standard_is_equal alias "≜" (other: MULTI_ARRAY_LIST [G]): BOOLEAN -- Is other attached to an object of the same type -- as current object, and field-by-field identical to it? -- (from ANY) require -- from ANY other_not_void: other /= Void external "built_in" ensure -- from ANY same_type: Result implies same_type (other) symmetric: Result implies other.standard_is_equal (Current) end feature -- Status report after: BOOLEAN -- Is there no valid cursor position to the right of cursor? -- (from LIST) require -- from LINEAR True do Result := index = count + 1 end before: BOOLEAN -- Is there no valid cursor position to the left of cursor? -- (from LIST) require -- from BILINEAR True do Result := index = 0 end changeable_comparison_criterion: BOOLEAN -- May object_comparison be changed? -- (Answer: yes by default.) -- (from CONTAINER) do Result := True end conforms_to (other: ANY): BOOLEAN -- Does type of current object conform to type -- of other (as per Eiffel: The Language, chapter 13)? -- (from ANY) require -- from ANY other_not_void: other /= Void external "built_in" end empty: BOOLEAN obsolete "ELKS 2000: Use `is_empty' instead. [2017-05-31]" -- Is there no element? -- (from CONTAINER) do Result := is_empty end exhausted: BOOLEAN -- Has structure been completely explored? -- (from LINEAR) do Result := off ensure -- from LINEAR exhausted_when_off: off implies Result end extendible: BOOLEAN -- May new items be added? (Answer: yes.) -- (from DYNAMIC_CHAIN) require -- from COLLECTION True do Result := True end full: BOOLEAN -- Is structure filled to capacity? do Result := False end is_empty: BOOLEAN -- Is structure empty? -- (from FINITE) require -- from CONTAINER True do Result := count = 0 end is_inserted (v: G): BOOLEAN -- Has v been inserted by the most recent insertion? -- (By default, the value returned is equivalent to calling -- has (v). However, descendants might be able to provide more -- efficient implementations.) -- (from COLLECTION) do Result := has (v) end isfirst: BOOLEAN -- Is cursor at first position? -- (from CHAIN) do Result := not is_empty and (index = 1) ensure -- from CHAIN valid_position: Result implies not is_empty end islast: BOOLEAN -- Is cursor at last position? -- (from CHAIN) do Result := not is_empty and (index = count) ensure -- from CHAIN valid_position: Result implies not is_empty end object_comparison: BOOLEAN -- Must search operations use equal rather than = -- for comparing references? (Default: no, use =.) -- (from CONTAINER) off: BOOLEAN -- Is there no current item? -- (from CHAIN) require -- from TRAVERSABLE True do Result := (index = 0) or (index = count + 1) end prunable: BOOLEAN -- May items be removed? (Answer: yes.) -- (from DYNAMIC_TABLE) require -- from COLLECTION True do Result := True end readable: BOOLEAN -- Is there a current item that may be read? -- (from SEQUENCE) require -- from ACTIVE True do Result := not off end replaceable: BOOLEAN -- Can current item be replaced? -- (from ACTIVE) do Result := True end same_type (other: ANY): BOOLEAN -- Is type of current object identical to type of other? -- (from ANY) require -- from ANY other_not_void: other /= Void external "built_in" ensure -- from ANY definition: Result = (conforms_to (other) and other.conforms_to (Current)) end valid_cursor (p: CURSOR): BOOLEAN -- Can the cursor be moved to position p? do if attached {MULTAR_LIST_CURSOR [G]} p as al_c then Result := (al_c /= Void) and then valid_cursor_index (al_c.index) and then al_c.active.item.valid_cursor_index (al_c.active_index) end end valid_cursor_index (i: INTEGER_32): BOOLEAN -- Is i correctly bounded for cursor movement? -- (from CHAIN) do Result := (i >= 0) and (i <= count + 1) ensure -- from CHAIN valid_cursor_index_definition: Result = ((i >= 0) and (i <= count + 1)) end valid_index (i: INTEGER_32): BOOLEAN -- Is i within allowable bounds? -- (from CHAIN) require -- from READABLE_INDEXABLE True require -- from TABLE True do Result := (i >= 1) and (i <= count) ensure -- from READABLE_INDEXABLE only_if_in_index_set: Result implies (Lower <= i and i <= count) ensure then -- from CHAIN valid_index_definition: Result = ((i >= 1) and (i <= count)) end writable: BOOLEAN -- Is there a current item that may be modified? -- (from SEQUENCE) require -- from ACTIVE True do Result := not off end feature -- Status setting compare_objects -- Ensure that future search operations will use equal -- rather than = for comparing references. -- (from CONTAINER) require -- from CONTAINER changeable_comparison_criterion: changeable_comparison_criterion do object_comparison := True ensure -- from CONTAINER object_comparison end compare_references -- Ensure that future search operations will use = -- rather than equal for comparing references. -- (from CONTAINER) require -- from CONTAINER changeable_comparison_criterion: changeable_comparison_criterion do object_comparison := False ensure -- from CONTAINER reference_comparison: not object_comparison end feature -- Cursor movement back -- Move cursor to previous position, if any. require -- from BILINEAR not_before: not before local current_array: ARRAYED_LIST [G] a: detachable like active do if not is_empty then current_array := active.item; current_array.back if current_array.before and then active /= first_element then a := active.left if a /= Void then active := a end; active.item.finish end end index := index - 1 end finish -- Move cursor to last position. -- (No effect if empty) require -- from LINEAR True do active := last_element; active.item.finish index := count ensure then -- from CHAIN at_last: not is_empty implies islast end forth -- Move cursor to next position, if any. require -- from LINEAR not_after: not after local current_array: ARRAYED_LIST [G] a: detachable like active do if not is_empty then current_array := active.item; current_array.forth if current_array.after and then active /= last_element then a := active.right if a /= Void then active := a end; active.item.start end end index := index + 1 ensure then -- from LIST moved_forth: index = old index + 1 end go_i_th (i: INTEGER_32) -- Move cursor to i-th position. -- (from CHAIN) require -- from CHAIN valid_cursor_index: valid_cursor_index (i) do move (i - index) ensure -- from CHAIN position_expected: index = i end go_to (p: CURSOR) -- Move cursor to position p require -- from CURSOR_STRUCTURE cursor_position_valid: valid_cursor (p) do if attached {MULTAR_LIST_CURSOR [G]} p as al_c then active := al_c.active; active.item.go_i_th (al_c.active_index) index := al_c.index end end move (i: INTEGER_32) -- Move cursor i positions. The cursor -- may end up off if the offset is too big. local counter: INTEGER_32 cell: detachable like active current_array: ARRAYED_LIST [G] do cell := active current_array := cell.item if i > 0 then from counter := i + active.item.index until counter <= current_array.count or cell = Void loop counter := counter - current_array.count cell := cell.right if cell /= Void then current_array := cell.item end end if cell = Void then current_array.finish; current_array.forth else active := cell; current_array.go_i_th (counter) end elseif i < 0 then from counter := current_array.count - current_array.index - i until counter <= current_array.count or cell = Void loop counter := counter - current_array.count cell := cell.left if cell /= Void then current_array := cell.item end end if counter = current_array.count then counter := 0 if cell /= Void then cell := cell.left if cell /= Void then current_array := cell.item end end end if cell = Void then current_array.go_i_th (0) else active := cell; current_array.go_i_th (current_array.count - counter) end end if i /= 0 then if current_array.before then index := 0 elseif current_array.after then index := count + 1 else index := index + i end end ensure -- from CHAIN too_far_right: (old index + i > count) implies exhausted too_far_left: (old index + i < 1) implies exhausted expected_index: (not exhausted) implies (index = old index + i) end search (v: like item) -- Move cursor to first position (at or after current -- cursor position) where item and v are equal. -- (Reference or object equality, -- based on object_comparison.) require -- from LINEAR True local current_array: ARRAYED_LIST [G] old_index: INTEGER_32 cell: detachable like active do cell := active current_array := cell.item old_index := current_array.index if object_comparison then current_array.compare_objects else current_array.compare_references end; current_array.search (v) if current_array.after then cell := cell.right index := index + current_array.count - old_index + 1 else index := index + current_array.index - old_index end from invariant index <= count + 1 until not current_array.after or else cell = Void loop current_array := cell.item if object_comparison then current_array.compare_objects else current_array.compare_references end; current_array.start; current_array.search (v) if current_array.after then cell := cell.right index := index + current_array.count else index := index + current_array.index - 1 end end if cell /= Void then active := cell else active := last_element end ensure -- from LINEAR object_found: (not exhausted and object_comparison) implies v ~ item item_found: (not exhausted and not object_comparison) implies v = item end start -- Move cursor to first position. -- (No effect if empty) require -- from TRAVERSABLE True do active := first_element; active.item.start index := 1 ensure then -- from CHAIN at_first: not is_empty implies isfirst end feature -- Element change append (s: SEQUENCE [G]) -- Append a copy of s. -- (from CHAIN) require -- from SEQUENCE argument_not_void: s /= Void local l: SEQUENCE [G] l_cursor: CURSOR do l := s if s = Current then l := twin end from l_cursor := cursor; l.start until l.exhausted loop extend (l.item) finish; l.forth end go_to (l_cursor) ensure -- from SEQUENCE new_count: count >= old count end extend (v: like item) -- Add v to end. require -- from COLLECTION extendible: extendible local current_array: ARRAYED_LIST [G] n: like new_cell do current_array := last_element.item if current_array.count = block_size then create current_array.make (block_size) n := new_cell (current_array); last_element.put_right (n) last_element := n end; current_array.extend (v) count := count + 1 ensure -- from COLLECTION item_inserted: is_inserted (v) end fill (other: CONTAINER [G]) -- Fill with as many items of other as possible. -- The representations of other and current structure -- need not be the same. -- (from CHAIN) require -- from COLLECTION other_not_void: other /= Void extendible: extendible local lin_rep: LINEAR [G] l_cursor: CURSOR do lin_rep := other.linear_representation from l_cursor := cursor; lin_rep.start until not extendible or else lin_rep.off loop extend (lin_rep.item) finish; lin_rep.forth end go_to (l_cursor) end force (v: like item) -- Add v to end. -- (from SEQUENCE) require -- from SEQUENCE extendible: extendible do extend (v) ensure then -- from SEQUENCE new_count: count = old count + 1 item_inserted: has (v) end merge_left (other: MULTI_ARRAY_LIST [G]) -- Merge other into current structure before cursor -- position. Do not move cursor. Empty other. -- (from DYNAMIC_LIST) require -- from DYNAMIC_CHAIN extendible: extendible not_before: not before other_exists: other /= Void not_current: other /= Current do from other.start until other.is_empty loop put_left (other.item); other.remove end ensure -- from DYNAMIC_CHAIN new_count: count = old count + old other.count new_index: index = old index + old other.count other_is_empty: other.is_empty end merge_right (other: MULTI_ARRAY_LIST [G]) -- Merge other into current structure after cursor -- position. Do not move cursor. Empty other. -- (from DYNAMIC_LIST) require -- from DYNAMIC_CHAIN extendible: extendible not_after: not after other_exists: other /= Void not_current: other /= Current do from other.finish until other.is_empty loop put_right (other.item); other.back; other.remove_right end ensure -- from DYNAMIC_CHAIN new_count: count = old count + old other.count same_index: index = old index other_is_empty: other.is_empty end put (v: like item) -- Replace current item by v. -- (Synonym for replace) -- (from CHAIN) require -- from CHAIN writeable: writable replaceable: replaceable do replace (v) ensure -- from CHAIN same_count: count = old count is_inserted: is_inserted (v) end sequence_put (v: like item) -- Add v to end. -- (from SEQUENCE) require -- from COLLECTION extendible: extendible do extend (v) ensure -- from COLLECTION item_inserted: is_inserted (v) ensure then -- from SEQUENCE new_count: count = old count + 1 end put_front (v: like item) -- Add v at the beginning. -- Do not move cursor. require -- from DYNAMIC_CHAIN extendible: extendible local first_array: ARRAYED_LIST [G] pos: INTEGER_32 do first_array := first_element.item if active = first_element then pos := first_array.index else pos := -1 end; first_array.start put_left (v) if pos > 0 then first_array.go_i_th (pos + 1) elseif pos = 0 then first_array.go_i_th (0) end if not before then index := index + 1 end ensure -- from DYNAMIC_CHAIN new_count: count = old count + 1 item_inserted: first = v end put_i_th (v: like item; i: INTEGER_32) -- Put v at i-th position. -- (from CHAIN) require -- from TABLE valid_key: valid_index (i) require -- from TABLE valid_key: valid_index (i) local pos: CURSOR do pos := cursor go_i_th (i) replace (v) go_to (pos) ensure -- from TABLE inserted: i_th (i) = v end put_left (v: like item) -- Add v to the left of current position. -- Do not move cursor. require -- from DYNAMIC_CHAIN extendible: extendible not_before: not before local cell: like first_element current_array: ARRAYED_LIST [G] new_array: ARRAYED_LIST [G] pos, cut: INTEGER_32 l: detachable like first_element i, n: like {ARRAYED_LIST [G]}.count do current_array := active_array check is_empty implies after end if after then extend (v) else if active /= first_element then l := active.left end if l /= Void and then not l.item.full then l.item.extend (v) elseif current_array.count <= block_size then current_array.put_left (v) else pos := current_array.index; current_array.go_i_th (block_size // 2 + 1) cut := index from i := current_array.index n := if current_array.after then 0 else count.min (current_array.count - i + 1) end create new_array.make (n) until n <= 0 loop new_array.extend (current_array [i]) i := i + 1 n := n - 1 end cell := new_cell (new_array); cell.put_right (active.right); cell.put_left (active) if last_element = active then last_element := cell end if pos < cut then current_array.go_i_th (pos); current_array.put_left (v) elseif pos = cut then current_array.extend (v) active := cell; active.item.start else active := cell current_array := cell.item; current_array.go_i_th (pos - cut + 1); current_array.put_left (v) end end end index := index + 1 count := count + 1 ensure -- from DYNAMIC_CHAIN new_count: count = old count + 1 new_index: index = old index + 1 end put_right (v: like item) -- Add v to the left of current position. -- Do not move cursor. require -- from DYNAMIC_CHAIN extendible: extendible not_after: not after do forth put_left (v) back back ensure -- from DYNAMIC_CHAIN new_count: count = old count + 1 same_index: index = old index end replace (v: like item) -- Replace current item by v. require -- from ACTIVE writable: writable replaceable: replaceable do active.item.replace (v) ensure -- from ACTIVE item_replaced: item = v end feature -- Removal prune (v: like item) -- Remove first occurrence of v, if any, -- after cursor position. -- If found, move cursor to right neighbor; -- if not, make structure exhausted. -- (from DYNAMIC_CHAIN) require -- from COLLECTION prunable: prunable do search (v) if not exhausted then remove end end prune_all (v: like item) -- Remove all occurrences of v. -- (Reference or object equality, -- based on object_comparison.) -- Leave structure exhausted. require -- from COLLECTION prunable: prunable local cell: detachable like active new_active: like active array: ARRAYED_LIST [G] do from cell := first_element until cell = Void loop array := cell.item if object_comparison then array.compare_objects else array.compare_references end count := count - array.count; array.prune_all (v) count := count + array.count if array.is_empty then if cell = first_element then if cell = last_element then cell := Void else if attached cell.right as e then first_element := e end cell := first_element; cell.forget_left end elseif cell = last_element then if attached cell.left as e then last_element := e end; last_element.forget_right cell := Void else new_active := cell.right if attached new_active and then attached cell.left as e then new_active.put_left (e) end cell := new_active end else cell := cell.right end end active := last_element index := count + 1 ensure -- from COLLECTION no_more_occurrences: not has (v) ensure then -- from DYNAMIC_CHAIN is_exhausted: exhausted end remove -- Remove current item require -- from ACTIVE prunable: prunable writable: writable local current_array: ARRAYED_LIST [G] new_active: detachable like active e: detachable like first_element do current_array := active.item; current_array.remove if current_array.is_empty then if active = first_element then if active /= last_element then e := active.right if e /= Void then first_element := e; e.forget_left end active := first_element; active.item.start end elseif active = last_element then e := active.left if e /= Void then last_element := e; e.forget_right end active := last_element; active.item.finish else new_active := active.right if new_active /= Void then e := active.left if e /= Void then new_active.put_left (e) end active := new_active end; active.item.start end elseif current_array.after then if active /= last_element then e := active.right if e /= Void then active := e end; active.item.start end end count := count - 1 ensure then -- from DYNAMIC_LIST after_when_empty: is_empty implies after end remove_i_th (i: INTEGER_32) -- Remove item at index i. -- Move cursor to next neighbor (or after if no next neighbor) if it is at i-th position. -- Do not change cursor otherwise. -- (from DYNAMIC_CHAIN) require -- from DYNAMIC_TABLE prunable: prunable valid_key: valid_index (i) local new_index: like index do new_index := index if new_index > i then new_index := new_index - 1 end go_i_th (i) remove go_i_th (new_index) ensure then -- from DYNAMIC_CHAIN new_count: count = old count - 1 same_index_if_below: index <= i implies index = old index new_index_if_above: index > i implies index = old index - 1 same_leading_items: across old twin as c all c.target_index < i implies c.item = i_th (c.target_index) end same_trailing_items: across old twin as c all c.target_index > i implies c.item = i_th (c.target_index - 1) end end remove_left -- Remove item to the left of cursor position. -- Do not move cursor. require -- from DYNAMIC_CHAIN left_exists: index > 1 do back remove ensure -- from DYNAMIC_CHAIN new_count: count = old count - 1 new_index: index = old index - 1 end remove_right -- Remove item to the right of cursor position. -- Do not move cursor. require -- from DYNAMIC_CHAIN right_exists: index < count do forth remove back ensure -- from DYNAMIC_CHAIN new_count: count = old count - 1 same_index: index = old index end wipe_out -- Remove all items. do count := 0 index := 0; first_element.item.wipe_out; first_element.forget_right active := first_element last_element := first_element ensure then -- from DYNAMIC_LIST is_before: before end chain_wipe_out -- Remove all items. -- (from DYNAMIC_CHAIN) require -- from COLLECTION prunable: prunable do from start until is_empty loop remove end ensure -- from COLLECTION wiped_out: is_empty end feature -- Transformation swap (i: INTEGER_32) -- Exchange item at i-th position with item -- at cursor position. -- (from CHAIN) require -- from CHAIN not_off: not off valid_index: valid_index (i) local old_item, new_item: like item pos: CURSOR do pos := cursor old_item := item go_i_th (i) new_item := item replace (old_item) go_to (pos) replace (new_item) ensure -- from CHAIN swapped_to_item: item = old i_th (i) swapped_from_item: i_th (i) = old item end feature -- Conversion linear_representation: LINEAR [G] -- Representation as a linear structure -- (from LINEAR) require -- from CONTAINER True do Result := Current end feature -- Duplication frozen clone (other: detachable ANY): like other obsolete "Use `twin' instead. [2017-05-31]" -- Void if other is void; otherwise new object -- equal to other -- -- For non-void other, clone calls copy; -- to change copying/cloning semantics, redefine copy. -- (from ANY) do if other /= Void then Result := other.twin end ensure -- from ANY instance_free: class equal: Result ~ other end copy (other: MULTI_ARRAY_LIST [G]) -- Update current object using fields of object attached -- to other, so as to yield equal objects. -- (from ANY) require -- from ANY other_not_void: other /= Void type_identity: same_type (other) external "built_in" ensure -- from ANY is_equal: Current ~ other end frozen deep_clone (other: detachable ANY): like other obsolete "Use `deep_twin' instead. [2017-05-31]" -- Void if other is void: otherwise, new object structure -- recursively duplicated from the one attached to other -- (from ANY) do if other /= Void then Result := other.deep_twin end ensure -- from ANY instance_free: class deep_equal: deep_equal (other, Result) end frozen deep_copy (other: MULTI_ARRAY_LIST [G]) -- Effect equivalent to that of: -- copy (other . deep_twin) -- (from ANY) require -- from ANY other_not_void: other /= Void do copy (other.deep_twin) ensure -- from ANY deep_equal: deep_equal (Current, other) end frozen deep_twin: MULTI_ARRAY_LIST [G] -- New object structure recursively duplicated from Current. -- (from ANY) external "built_in" ensure -- from ANY deep_twin_not_void: Result /= Void deep_equal: deep_equal (Current, Result) end duplicate (n: INTEGER_32): like Current obsolete "[ Create a new container explicitly using `make_from_iterable` if available. Otherwise, replace a call to the feature with code that creates and initializes container. [2018-11-30] ]" -- Copy of sub-list beginning at cursor position -- and having min (n, count - index + 1) items require -- from CHAIN not_off_unless_after: off implies after valid_subchain: n >= 0 local pos: CURSOR counter: INTEGER_32 do from pos := cursor Result := new_chain until (counter = n) or exhausted loop Result.extend (item) forth counter := counter + 1 end go_to (pos) end frozen standard_clone (other: detachable ANY): like other obsolete "Use `standard_twin' instead. [2017-05-31]" -- Void if other is void; otherwise new object -- field-by-field identical to other. -- Always uses default copying semantics. -- (from ANY) do if other /= Void then Result := other.standard_twin end ensure -- from ANY instance_free: class equal: standard_equal (Result, other) end frozen standard_copy (other: MULTI_ARRAY_LIST [G]) -- Copy every field of other onto corresponding field -- of current object. -- (from ANY) require -- from ANY other_not_void: other /= Void type_identity: same_type (other) external "built_in" ensure -- from ANY is_standard_equal: standard_is_equal (other) end frozen standard_twin: MULTI_ARRAY_LIST [G] -- New object field-by-field identical to other. -- Always uses default copying semantics. -- (from ANY) external "built_in" ensure -- from ANY standard_twin_not_void: Result /= Void equal: standard_equal (Result, Current) end frozen twin: MULTI_ARRAY_LIST [G] -- New object equal to Current -- twin calls copy; to change copying/twinning semantics, redefine copy. -- (from ANY) external "built_in" ensure -- from ANY twin_not_void: Result /= Void is_equal: Result ~ Current end feature -- Basic operations frozen as_attached: attached MULTI_ARRAY_LIST [G] obsolete "Remove calls to this feature. [2017-05-31]" -- Attached version of Current. -- (Can be used during transitional period to convert -- non-void-safe classes to void-safe ones.) -- (from ANY) do Result := Current end frozen default: detachable MULTI_ARRAY_LIST [G] -- Default value of object's type -- (from ANY) do end frozen default_pointer: POINTER -- Default value of type POINTER -- (Avoid the need to write p.default for -- some p of type POINTER.) -- (from ANY) do ensure -- from ANY instance_free: class end default_rescue -- Process exception for routines with no Rescue clause. -- (Default: do nothing.) -- (from ANY) do end frozen do_nothing -- Execute a null action. -- (from ANY) do ensure -- from ANY instance_free: class end feature {MULTI_ARRAY_LIST}{DYNAMIC_CHAIN} -- Implementation new_chain: like Current obsolete "Use explicit creation instead. See also explanations for `duplicate`. [2018-11-30]" -- A newly created instance of the same type. -- This feature may be redefined in descendants so as to -- produce an adequately allocated and initialized object. do create Result.make (block_size) ensure -- from DYNAMIC_CHAIN result_exists: Result /= Void end feature {MULTI_ARRAY_LIST} -- Implementation active: like first_element -- Element at cursor position active_array: ARRAYED_LIST [G] -- Array_sequence at cursor position require active_exists: active /= Void not_off: not off do Result := active.item end feature {NONE} -- Implementation new_cell (a: ARRAYED_LIST [G]): like first_element do create Result.put (a) end feature -- Iteration do_all (action: PROCEDURE [G]) -- Apply action to every item. -- Semantics not guaranteed if action changes the structure; -- in such a case, apply iterator to clone of structure instead. -- (from LINEAR) require -- from TRAVERSABLE action_exists: action /= Void local c: detachable CURSOR cs: detachable CURSOR_STRUCTURE [G] do if attached {CURSOR_STRUCTURE [G]} Current as acs then cs := acs c := acs.cursor end from start until after loop action.call ([item]) forth end if cs /= Void and c /= Void then cs.go_to (c) end end do_if (action: PROCEDURE [G]; test: FUNCTION [G, BOOLEAN]) -- Apply action to every item that satisfies test. -- Semantics not guaranteed if action or test changes the structure; -- in such a case, apply iterator to clone of structure instead. -- (from LINEAR) require -- from TRAVERSABLE action_exists: action /= Void test_exists: test /= Void local c: detachable CURSOR cs: detachable CURSOR_STRUCTURE [G] do if attached {CURSOR_STRUCTURE [G]} Current as acs then cs := acs c := acs.cursor end from start until after loop if test.item ([item]) then action.call ([item]) end forth end if cs /= Void and c /= Void then cs.go_to (c) end end for_all (test: FUNCTION [G, BOOLEAN]): BOOLEAN -- Is test true for all items? -- Semantics not guaranteed if test changes the structure; -- in such a case, apply iterator to clone of structure instead. -- (from LINEAR) require -- from TRAVERSABLE test_exists: test /= Void local c: detachable CURSOR cs: detachable CURSOR_STRUCTURE [G] do if attached {CURSOR_STRUCTURE [G]} Current as acs then cs := acs c := acs.cursor end from start Result := True until after or not Result loop Result := test.item ([item]) forth end if cs /= Void and c /= Void then cs.go_to (c) end ensure then -- from LINEAR empty: is_empty implies Result end there_exists (test: FUNCTION [G, BOOLEAN]): BOOLEAN -- Is test true for at least one item? -- Semantics not guaranteed if test changes the structure; -- in such a case, apply iterator to clone of structure instead. -- (from LINEAR) require -- from TRAVERSABLE test_exists: test /= Void local c: detachable CURSOR cs: detachable CURSOR_STRUCTURE [G] do if attached {CURSOR_STRUCTURE [G]} Current as acs then cs := acs c := acs.cursor end from start until after or Result loop Result := test.item ([item]) forth end if cs /= Void and c /= Void then cs.go_to (c) end end feature -- Output Io: STD_FILES -- Handle to standard file setup -- (from ANY) once create Result; Result.set_output_default ensure -- from ANY instance_free: class io_not_void: Result /= Void end out: STRING_8 -- New string containing terse printable representation -- of current object -- (from ANY) do Result := tagged_out ensure -- from ANY out_not_void: Result /= Void end print (o: detachable ANY) -- Write terse external representation of o -- on standard output. -- (from ANY) local s: READABLE_STRING_8 do if attached o then s := o.out if attached {READABLE_STRING_32} s as s32 then Io.put_string_32 (s32) elseif attached {READABLE_STRING_8} s as s8 then Io.put_string (s8) else Io.put_string_32 (s.as_string_32) end end ensure -- from ANY instance_free: class end frozen tagged_out: STRING_8 -- New string containing terse printable representation -- of current object -- (from ANY) external "built_in" ensure -- from ANY tagged_out_not_void: Result /= Void end feature -- Platform Operating_environment: OPERATING_ENVIRONMENT -- Objects available from the operating system -- (from ANY) once create Result ensure -- from ANY instance_free: class operating_environment_not_void: Result /= Void end feature {NONE} -- Retrieval frozen internal_correct_mismatch -- Called from runtime to perform a proper dynamic dispatch on correct_mismatch -- from MISMATCH_CORRECTOR. -- (from ANY) local l_msg: STRING_32 l_exc: EXCEPTIONS do if attached {MISMATCH_CORRECTOR} Current as l_corrector then l_corrector.correct_mismatch else create l_msg.make_from_string ("Mismatch: ".as_string_32) create l_exc; l_msg.append (generating_type.name_32); l_exc.raise_retrieval_exception (l_msg) end end invariant writable_definition: writable = not off readable_definition: readable = not off extendible_definition: extendible -- from LIST before_definition: before = (index = 0) after_definition: after = (index = count + 1) -- from CHAIN non_negative_index: index >= 0 index_small_enough: index <= count + 1 off_definition: off = ((index = 0) or (index = count + 1)) isfirst_definition: isfirst = ((not is_empty) and (index = 1)) islast_definition: islast = ((not is_empty) and (index = count)) item_corresponds_to_index: (not off) implies (item = i_th (index)) -- from ACTIVE writable_constraint: writable implies readable empty_constraint: is_empty implies (not readable) and (not writable) -- from ANY reflexive_equality: standard_is_equal (Current) reflexive_conformance: conforms_to (Current) -- from READABLE_INDEXABLE consistent_boundaries: Lower <= count or else Lower = count + 1 -- from BILINEAR not_both: not (after and before) before_constraint: before implies off -- from LINEAR after_constraint: after implies off -- from TRAVERSABLE empty_constraint: is_empty implies off -- from FINITE empty_definition: is_empty = (count = 0) note 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 -- class MULTI_ARRAY_LIST
Generated by ISE EiffelStudio