note description: "[ Sets whose items may be compared according to a partial order relation implemented as sorted two-way lists. ]" library: "Free implementation of ELKS library" legal: "See notice at end of class." status: "See notice at end of class." names: sorted_set, set, two_way_list representation: linked access: membership, min, max contents: generic date: "$Date: 2019-07-05 15:26:16 +0000 (Fri, 05 Jul 2019) $" revision: "$Revision: 103325 $" class PART_SORTED_SET [G -> PART_COMPARABLE] create make, make_from_iterable create {PART_SORTED_SET} make_sublist feature {NONE} -- Initialization default_create -- Process instances of classes with no creation clause. -- (Default: do nothing.) -- (from ANY) do end make -- Create an empty list. -- (from LINKED_LIST) do before := True ensure -- from LINKED_LIST is_before: before 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 cursor: TWO_WAY_LIST_CURSOR [G] -- Current cursor position -- (from TWO_WAY_LIST) require -- from CURSOR_STRUCTURE True do create Result.make (active, after, before) ensure -- from CURSOR_STRUCTURE cursor_not_void: Result /= Void end first: like item -- Item at first position -- (from LINKED_LIST) require -- from CHAIN not_empty: not is_empty do check attached first_element as f then Result := f.item end end first_element: detachable like new_cell -- Head of list -- (Anchor redefinition) -- (from TWO_WAY_LIST) generating_type: TYPE [detachable PART_SORTED_SET [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: G): BOOLEAN -- Does structure include v? -- (Reference or object equality, -- based on object_comparison.) -- (from PART_SORTED_LIST) require -- from CONTAINER True local pos: CURSOR do if not is_empty then pos := cursor start search (v) Result := not after go_to (pos) end ensure -- from CONTAINER not_found_in_empty: Result implies not is_empty 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 -- Index of current position -- (from LINKED_LIST) require -- from LINEAR True require -- from LINEAR_SUBSET True local l_active, l_active_iterator: like active do if after then Result := count + 1 elseif not before then from Result := 1 l_active := active l_active_iterator := first_element until l_active_iterator = l_active or else l_active_iterator = Void loop l_active_iterator := l_active_iterator.right Result := Result + 1 end end 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 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 item: G -- Current item -- (from LINKED_LIST) require -- from ACTIVE readable: readable require -- from TRAVERSABLE not_off: not off require -- from TRAVERSABLE_SUBSET not_off: not off do check attached active as a then Result := a.item end 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 -- (from LINKED_LIST) require -- from CHAIN not_empty: not is_empty do check attached last_element as l then Result := l.item end end last_element: like first_element -- Tail of the list -- (from TWO_WAY_LIST) new_cursor: TWO_WAY_LIST_ITERATION_CURSOR [G] -- Fresh cursor associated with current structure -- (from TWO_WAY_LIST) require -- from ITERABLE True do create 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 search_after (v: like item) -- Go to first position with item greater -- than or equal to v. -- (from PART_SORTED_LIST) do from start until after or else v <= item loop forth end ensure -- from PART_SORTED_LIST argument_less_than_item: (not after) implies (v <= item) end search_before (v: like item) -- Go to last position with item less -- than or equal to v. -- (from PART_SORTED_LIST) do from finish until before or else v >= item loop back end ensure -- from PART_SORTED_LIST (not off) implies (item <= v) end sublist: detachable PART_SORTED_SET [G] -- Result produced by last split -- (from TWO_WAY_LIST) 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 -- Measurement count: INTEGER_32 -- Number of items -- (from LINKED_LIST) 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 -- 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 disjoint (other: TRAVERSABLE_SUBSET [G]): BOOLEAN -- Do current set and other have no -- items in common? -- (from TRAVERSABLE_SUBSET) require -- from SUBSET set_exists: other /= Void same_rule: object_comparison = other.object_comparison do if not is_empty and not other.is_empty then Result := subset_strategy (other).disjoint (Current, other) else Result := True end 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: PART_SORTED_SET [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: PART_SORTED_SET [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 is_subset alias "⊆" (other: TRAVERSABLE_SUBSET [G]): BOOLEAN -- Is current set a subset of other? -- (from TRAVERSABLE_SUBSET) require -- from SUBSET set_exists: other /= Void same_rule: object_comparison = other.object_comparison do if not other.is_empty and then count <= other.count then from start until off or else not (other ∋ item) loop forth end if off then Result := True end elseif is_empty then Result := True end end is_superset alias "⊇" (other: SUBSET [G]): BOOLEAN -- Is current set a superset of other? -- (from SUBSET) require -- from SUBSET set_exists: other /= Void same_rule: object_comparison = other.object_comparison do Result := other ⊆ Current 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: PART_SORTED_SET [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 LINKED_LIST) before: BOOLEAN -- Is there no valid cursor position to the left of cursor? -- (from LINKED_LIST) changeable_comparison_criterion: BOOLEAN -- May object_comparison be changed? -- (Answer: yes by default.) -- (from CONTAINER) do Result := True ensure then -- from SET only_on_empty: Result = is_empty 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 = False -- Is structured filled to capacity? (Answer: no.) -- (from LINKED_LIST) 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 LINKED_LIST) require -- from CHAIN True do Result := not after and not before and (active = first_element) ensure -- from CHAIN valid_position: Result implies not is_empty end islast: BOOLEAN -- Is cursor at last position? -- (from TWO_WAY_LIST) require -- from CHAIN True require -- from LINEAR_SUBSET True do Result := (active = last_element) and then not after and then not before 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 LINKED_LIST) require -- from TRAVERSABLE True require -- from TRAVERSABLE_SUBSET True do Result := after or before 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 LINKED_LIST) 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 sorted: BOOLEAN -- is the structures topologically sorted -- i.e i < j implies not i_th (i) > i_th (j) -- (from PART_SORTED_TWO_WAY_LIST) local c: CURSOR prev: like item do Result := True if count > 1 then from c := cursor start check not off end prev := item forth until after or not Result loop Result := prev <= item prev := item forth end go_to (c) end end valid_cursor (p: CURSOR): BOOLEAN -- Can the cursor be moved to position p? -- (from LINKED_LIST) require -- from CURSOR_STRUCTURE True local temp, sought: like first_element do if attached {like cursor} p as ll_c then from temp := first_element sought := ll_c.active Result := ll_c.after or else ll_c.before until Result or else temp = Void loop Result := temp = sought temp := temp.right end 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 require -- from LINEAR_SUBSET 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 -- from LINEAR_SUBSET index_valid: 0 <= i and i <= count + 1 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. -- (from TWO_WAY_LIST) require -- from BILINEAR not_before: not before local a: like active do if after then after := False if is_empty then before := True end else a := active if a /= Void then a := a.left if a = Void then active := first_element before := True else active := a end end end end finish -- Move cursor to last position. -- (Go before if empty) -- (from TWO_WAY_LIST) require -- from LINEAR True do if not is_empty then active := last_element after := False before := False else after := False before := True end ensure then -- from CHAIN at_last: not is_empty implies islast ensure then -- from LINKED_LIST empty_convention: is_empty implies before ensure then -- from TWO_WAY_LIST not_after: not after end forth -- Move cursor to next position, if any. -- (from TWO_WAY_LIST) require -- from LINEAR not_after: not after require -- from TRAVERSABLE_SUBSET not_after: not after local a: like active do if before then before := False if is_empty then after := True end else a := active if a /= Void then a := a.right if a = Void then active := last_element after := True else active := a end end end ensure then -- from LIST moved_forth: index = old index + 1 end go_i_th (i: INTEGER_32) -- Move cursor to i-th position. -- (from LINKED_LIST) require -- from CHAIN valid_cursor_index: valid_cursor_index (i) require -- from LINEAR_SUBSET valid_index: valid_index (i) do if i = 0 then before := True after := False active := first_element elseif i = count + 1 then before := False after := True active := last_element else move (i - index) end ensure -- from CHAIN position_expected: index = i ensure -- from LINEAR_SUBSET cursor_moved: index = i end go_to (p: CURSOR) -- Move cursor to position p. -- (from LINKED_LIST) require -- from CURSOR_STRUCTURE cursor_position_valid: valid_cursor (p) do if attached {like cursor} p as ll_c then after := ll_c.after before := ll_c.before if before then active := first_element elseif after then active := last_element else active := ll_c.active end else check correct_cursor_type: False end end end move (i: INTEGER_32) -- Move cursor i positions. The cursor -- may end up off if the offset is to big. -- (from TWO_WAY_LIST) require -- from CHAIN True local counter: INTEGER_32 p: like first_element do if i > 0 then ll_move (i) elseif i < 0 then if after then after := False counter := -1 end from p := active until (counter = i) or else (p = Void) loop p := p.left counter := counter - 1 end if p = Void then before := True active := first_element else active := p 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 ll_move (i: INTEGER_32) -- Move cursor i positions. The cursor -- may end up off if the offset is too big. -- (from LINKED_LIST) require -- from CHAIN True local counter, new_index: INTEGER_32 p: like first_element do if i > 0 then if before then before := False counter := 1 end from p := active until (counter = i) or else (p = Void) loop active := p p := p.right counter := counter + 1 end if p = Void then after := True else active := p end elseif i < 0 then new_index := index + i before := True after := False active := first_element if new_index > 0 then move (new_index) 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) ensure then -- from LINKED_LIST moved_if_inbounds: ((old index + i) >= 0 and (old index + i) <= (count + 1)) implies index = (old index + i) before_set: (old index + i) <= 0 implies before after_set: (old index + i) >= (count + 1) implies after end search (v: like item) -- Move to first position (at or after current -- position) where item and v are equal. -- If structure does not include v ensure that -- exhausted will be true. -- (Reference or object equality, -- based on object_comparison.) -- (from BILINEAR) require -- from LINEAR True do if before and not is_empty then forth end Precursor (v) 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. -- (from LINKED_LIST) require -- from TRAVERSABLE True require -- from TRAVERSABLE_SUBSET True do if first_element /= Void then active := first_element after := False else after := True end before := False ensure then -- from CHAIN at_first: not is_empty implies isfirst ensure then -- from LINKED_LIST empty_convention: is_empty implies after 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: G) -- Ensure that structure includes v. -- Was declared in PART_SORTED_SET as synonym of put. do search_after (v) if after or else v /~ item then put_left (v) end end pstwl_extend (v: like item) -- Put v at proper position in list. -- The cursor ends up on the newly inserted -- item. -- (from PART_SORTED_TWO_WAY_LIST) require -- from COLLECTION extendible: extendible do search_after (v) put_left (v) back ensure -- from COLLECTION item_inserted: is_inserted (v) ensure then -- from PART_SORTED_LIST remains_sorted: (old sorted) implies sorted item_inserted: item = 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 pstwl_merge (other: LINEAR [G]) -- Add all items from other at their proper positions. -- (from PART_SORTED_LIST) do from other.start until other.off loop extend (other.item); other.forth end ensure then -- from PART_SORTED_LIST remains_sorted: (old sorted) implies sorted end merge (other: TRAVERSABLE_SUBSET [G]) -- Add all items of other. require -- from SUBSET set_exists: other /= Void same_rule: object_comparison = other.object_comparison local i: like item o: like item do from start; other.start until other.after or else after loop i := item o := other.item if i /= Void and then o /= Void then if i < o then forth elseif i ~ o then forth; other.forth else put_left (o); other.forth end end end if after then from until other.after loop put_left (other.item); other.forth end end end merge_left (other: PART_SORTED_SET [G]) -- Merge other into current structure before cursor -- position. Do not move cursor. Empty other. -- (from TWO_WAY_LIST) require -- from DYNAMIC_CHAIN extendible: extendible not_before: not before other_exists: other /= Void not_current: other /= Current local other_count: INTEGER_32 do if not other.is_empty then other_count := other.count check attached other.first_element as other_first_element attached other.last_element as other_last_element then other.wipe_out if is_empty then last_element := other_last_element first_element := other_first_element if before then active := first_element else active := last_element end elseif isfirst then other_last_element.put_right (first_element) first_element := other_first_element elseif after then other_first_element.put_left (last_element) last_element := other_last_element active := last_element elseif attached active as a then other_first_element.put_left (a.left); a.put_left (other_last_element) end end count := count + other_count 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 ll_merge_right (other: PART_SORTED_SET [G]) -- Merge other into current structure after cursor -- position. Do not move cursor. Empty other. -- (from LINKED_LIST) require -- from DYNAMIC_CHAIN extendible: extendible not_after: not after other_exists: other /= Void not_current: other /= Current local other_first_element: like first_element other_count: INTEGER_32 a: like active do if attached other.last_element as other_last_element then other_first_element := other.first_element other_count := other.count; other.wipe_out check other_first_element /= Void end a := active if a = Void then first_element := other_first_element active := first_element else if not islast then other_last_element.put_right (a.right) end; a.put_right (other_first_element) end count := count + other_count 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 merge_right (other: PART_SORTED_SET [G]) -- Merge other into current structure after cursor -- position. Do not move cursor. Empty other. -- (from TWO_WAY_LIST) do if is_empty or else islast then last_element := other.last_element end ll_merge_right (other) end move_item (v: G) -- Move v to the left of cursor. -- (from LINEAR_SUBSET) require -- from LINEAR_SUBSET item_exists: v /= Void item_in_set: has (v) local idx: INTEGER_32 found: BOOLEAN do idx := index from start until found or after loop if object_comparison then found := v ~ item else found := v = item end if not found then forth end end check found: found and not after end remove go_i_th (idx) put_left (v) end put (v: G) -- Ensure that structure includes v. -- Was declared in PART_SORTED_SET as synonym of extend. do search_after (v) if after or else v /~ item then put_left (v) end end pstwl_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 to beginning. -- Do not move cursor. -- (from TWO_WAY_LIST) do ll_put_front (v) if count = 1 then last_element := first_element end end ll_put_front (v: like item) -- Add v to beginning. -- Do not move cursor. -- (from LINKED_LIST) require -- from DYNAMIC_CHAIN extendible: extendible local p: like new_cell do p := new_cell (v); p.put_right (first_element) first_element := p if before or is_empty then active := p end count := count + 1 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 cursor position. -- Do not move cursor. -- (from TWO_WAY_LIST) require -- from DYNAMIC_CHAIN extendible: extendible not_before: not before require -- from LINEAR_SUBSET item_exists: v /= Void not_before: not before local p: like first_element a: like active do p := new_cell (v) if is_empty then first_element := p last_element := p active := p before := False elseif after then p.put_left (last_element) last_element := p active := p elseif isfirst then p.put_right (active) first_element := p else a := active if a /= Void then p.put_left (a.left) end; p.put_right (active) end count := count + 1 ensure -- from DYNAMIC_CHAIN new_count: count = old count + 1 new_index: index = old index + 1 ensure then -- from LINKED_LIST previous_exists: previous /= Void item_inserted: attached previous as q and then q.item = v ensure -- from LINEAR_SUBSET cursor_position_unchanged: index = old index + 1 end put_right (v: like item) -- Add v to the right of cursor position. -- Do not move cursor. -- (from TWO_WAY_LIST) local was_last: BOOLEAN a: like active do was_last := islast ll_put_right (v) if count = 1 then last_element := active elseif was_last then a := active if a /= Void then last_element := a.right end end end ll_put_right (v: like item) -- Add v to the right of cursor position. -- Do not move cursor. -- (from LINKED_LIST) require -- from DYNAMIC_CHAIN extendible: extendible not_after: not after local p: like new_cell a: like active do p := new_cell (v) check is_empty implies before end if before then p.put_right (first_element) first_element := p active := p else a := active if a /= Void then p.put_right (a.right); a.put_right (p) end end count := count + 1 ensure -- from DYNAMIC_CHAIN new_count: count = old count + 1 same_index: index = old index ensure then -- from LINKED_LIST next_exists: next /= Void item_inserted: not old before implies (attached next as n and then n.item = v) item_inserted_before: old before implies (attached active as c and then c.item = v) end replace (v: like item) -- Replace current item by v. -- (from LINKED_LIST) require -- from ACTIVE writable: writable replaceable: replaceable local a: like active do a := active if a /= Void then a.put (v) end ensure -- from ACTIVE item_replaced: item = v end feature -- Removal prune (v: like item) -- Remove v if present. do start pstwl_prune (v) end pstwl_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 items identical to v. -- (Reference or object equality, -- based on object_comparison.) -- Leave cursor off. -- (from PART_SORTED_TWO_WAY_LIST) require -- from COLLECTION prunable: prunable do from start search (v) until off or else v < item loop remove end if not off then finish forth end ensure -- from COLLECTION no_more_occurrences: not has (v) ensure then -- from DYNAMIC_CHAIN is_exhausted: exhausted end remove -- Remove current item. -- Move cursor to right neighbor -- (or after if no right neighbor). -- (from TWO_WAY_LIST) require -- from ACTIVE prunable: prunable writable: writable require -- from TRAVERSABLE_SUBSET not_off: not off local succ, pred, removed: like first_element a: like active do removed := active if isfirst then a := first_element if a /= Void then active := a.right; a.forget_right end first_element := active if count = 1 then check no_active: active = Void end after := True last_element := Void end elseif islast then a := last_element if a /= Void then active := a.left; a.forget_left end last_element := active after := True else a := active if a /= Void then pred := a.left succ := a.right end if pred /= Void and then succ /= Void then pred.forget_right; succ.forget_left; pred.put_right (succ) end active := succ end count := count - 1 cleanup_after_remove (removed) 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. -- (from TWO_WAY_LIST) 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. -- (from TWO_WAY_LIST) 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 remove_sublist -- (from TWO_WAY_LIST) do sublist := Void end split (n: INTEGER_32) -- Remove from current list -- min (n, count - index - 1) items -- starting at cursor position. -- Move cursor right one position. -- Make extracted sublist accessible -- through attribute sublist. -- (from TWO_WAY_LIST) require -- from TWO_WAY_LIST not_off: not off valid_sublist: n >= 0 local actual_number, active_index: INTEGER_32 p_elem, s_elem, e_elem, n_elem: like first_element do if n = 0 then create sublist.make else active_index := index if active_index + n > count + 1 then actual_number := count + 1 - active_index else actual_number := n end s_elem := active p_elem := previous move (actual_number - 1) e_elem := active n_elem := next if s_elem /= Void then s_elem.forget_left end if e_elem /= Void then e_elem.forget_right end create sublist.make_sublist (s_elem, e_elem, actual_number) count := count - actual_number if p_elem /= Void then p_elem.put_right (n_elem) else first_element := n_elem end if n_elem /= Void then active := n_elem else last_element := p_elem active := p_elem after := True end end end wipe_out -- Remove all items. -- (from TWO_WAY_LIST) require -- from COLLECTION prunable: prunable do ll_wipe_out last_element := Void ensure -- from COLLECTION wiped_out: is_empty end ll_wipe_out -- Remove all items. -- (from LINKED_LIST) do internal_wipe_out 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 sort -- sort the list -- Has O(count * log (count)) complexity. -- (from PART_SORTED_TWO_WAY_LIST) local no_change: BOOLEAN gap: INTEGER_32 left_cell, cell: like first_element left_cell_item, cell_item: like item do if not is_empty then from gap := count * 10 // 13 until gap = 0 loop from no_change := False go_i_th (1 + gap) until no_change loop no_change := True from left_cell := first_element cell := active until cell = Void loop if left_cell /= Void then left_cell_item := left_cell.item cell_item := cell.item if cell_item < left_cell_item then no_change := False; cell.put (left_cell_item); left_cell.put (cell_item) end left_cell := left_cell.right end cell := cell.right end end gap := gap * 10 // 13 end end end 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: PART_SORTED_SET [G]) -- Update current object using fields of object attached -- to other, so as to yield equal objects. -- (from LINKED_LIST) require -- from ANY other_not_void: other /= Void type_identity: same_type (other) local cur: LINKED_LIST_CURSOR [G] do if other /= Current then standard_copy (other) if not other.is_empty then internal_wipe_out cur := other.cursor from other.start until other.off loop extend (other.item) finish; other.forth end if cur /= Void then other.go_to (cur) end end end 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: PART_SORTED_SET [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: PART_SORTED_SET [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-set 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 require -- from SUBSET non_negative: n >= 0 local pos: CURSOR counter: INTEGER_32 do pos := cursor Result := new_chain; Result.finish from until (counter = n) or else after loop Result.put_left (item) forth counter := counter + 1 end go_to (pos) ensure -- from SUBSET correct_count_1: n <= count implies Result.count = n correct_count_2: n >= count implies Result.count = count 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: PART_SORTED_SET [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: PART_SORTED_SET [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: PART_SORTED_SET [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 PART_SORTED_SET [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 PART_SORTED_SET [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 intersect (other: TRAVERSABLE_SUBSET [G]) -- Remove all items not in other. -- No effect if other is_empty. -- (from TRAVERSABLE_SUBSET) require -- from SUBSET set_exists: other /= Void same_rule: object_comparison = other.object_comparison do if not other.is_empty then from start; other.start until off loop if other ∋ item then forth else remove end end else wipe_out end ensure -- from SUBSET is_subset_other: is_subset (other) end subtract (other: TRAVERSABLE_SUBSET [G]) -- Remove all items also in other. -- (from TRAVERSABLE_SUBSET) require -- from SUBSET set_exists: other /= Void same_rule: object_comparison = other.object_comparison do if not (other.is_empty or is_empty) then from start; other.start until off loop if other ∋ item then remove else forth end end end ensure -- from SUBSET is_disjoint: disjoint (other) end symdif (other: TRAVERSABLE_SUBSET [G]) -- Remove all items also in other, and add all -- items of other not already present. -- (from TRAVERSABLE_SUBSET) require -- from SUBSET set_exists: other /= Void same_rule: object_comparison = other.object_comparison do if not other.is_empty then if is_empty then from other.start until other.after loop extend (other.item) end else subset_strategy (other).symdif (Current, other) end end end feature {NONE} -- Implementation frozen internal_wipe_out -- Remove all items. -- (from LINKED_LIST) require -- from LINKED_LIST prunable do active := Void first_element := Void before := True after := False count := 0 ensure -- from LINKED_LIST wiped_out: is_empty is_before: before end subset_strategy (other: TRAVERSABLE_SUBSET [G]): SUBSET_STRATEGY [G] -- Subset strategy suitable for the type of the contained elements. -- (from TRAVERSABLE_SUBSET) require -- from TRAVERSABLE_SUBSET not_empty: not is_empty do start check not_off: not off end Result := subset_strategy_selection (item, other) end subset_strategy_selection (v: G; other: TRAVERSABLE_SUBSET [G]): SUBSET_STRATEGY [G] -- Strategy to calculate several subset features selected depending -- on the dynamic type of v and other -- (from LINEAR_SUBSET) require -- from TRAVERSABLE_SUBSET item_exists: v /= Void other_exists: other /= Void do if attached {HASHABLE} v as h then create {SUBSET_STRATEGY_HASHABLE [G]} Result else create {SUBSET_STRATEGY_GENERIC [G]} Result end ensure -- from TRAVERSABLE_SUBSET strategy_set: Result /= Void end feature {PART_SORTED_TWO_WAY_LIST}{TWO_WAY_LIST}{LINKED_LIST}{DYNAMIC_CHAIN} -- Implementation new_chain: PART_SORTED_SET [G] 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. -- (from PART_SORTED_TWO_WAY_LIST) require -- from DYNAMIC_CHAIN True do create Result.make ensure -- from DYNAMIC_CHAIN result_exists: Result /= Void end feature {TWO_WAY_LIST} -- Implementation make_sublist (first_item, last_item: like first_element; n: INTEGER_32) -- Create sublist -- (from TWO_WAY_LIST) do make first_element := first_item last_element := last_item active := first_element count := n end feature {TWO_WAY_LIST}{LINKED_LIST} -- Implementation new_cell (v: like item): BI_LINKABLE [G] -- A newly created instance of the type of first_element. -- (from TWO_WAY_LIST) do create Result.put (v) ensure -- from LINKED_LIST result_exists: Result /= Void end previous: like first_element -- Element left of cursor -- (from TWO_WAY_LIST) local a: like active do if after then Result := active else a := active if a /= Void then Result := a.left end end end feature {LINKED_LIST} -- Implementation active: like first_element -- Element at cursor position -- (from LINKED_LIST) cleanup_after_remove (v: like first_element) -- Clean-up a just removed cell. -- (from LINKED_LIST) require -- from LINKED_LIST non_void_cell: v /= Void do end next: like first_element -- Element right of cursor -- (from LINKED_LIST) local a: like active do if before then Result := active else a := active if a /= Void then Result := a.right end end end feature {NONE} -- Creation make_from_iterable (other: ITERABLE [G]) -- Create a set with all items obtained from other. do make across other as o loop extend (o.item) end 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 -- from LINEAR_SUBSET before_definition: before = (index = 0) -- from TRAVERSABLE_SUBSET empty_definition: is_empty = (count = 0) count_range: count >= 0 -- from ANY reflexive_equality: standard_is_equal (Current) reflexive_conformance: conforms_to (Current) -- from TWO_WAY_LIST non_empty_list_has_two_endpoints: not is_empty implies (first_element /= Void and last_element /= Void) empty_list_has_no_endpoints: is_empty implies last_element = Void first_element_constraint: attached first_element as f implies f.left = Void last_element_constraint: attached last_element as l implies l.right = Void -- from LINKED_LIST prunable: prunable empty_constraint: is_empty implies ((first_element = Void) and (active = Void)) not_void_unless_empty: (active = Void) implies is_empty before_constraint: before implies (active = first_element) after_constraint: after implies (active = last_element) -- 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 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-2019, 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 PART_SORTED_SET
Generated by ISE EiffelStudio