note description: "[ Sequences of 32-bit characters, accessible through integer indices in a contiguous range. ]" library: "Free implementation of ELKS library" status: "See notice at end of class." legal: "See notice at end of class." date: "$Date: 2020-05-19 14:21:28 +0000 (Tue, 19 May 2020) $" revision: "$Revision: 104256 $" class STRING_32 create make, make_empty, make_filled, make_from_string, make_from_string_general, make_from_c, make_from_c_pointer, make_from_c_byte_array, make_from_cil, make_from_separate convert to_cil: {SYSTEM_STRING}, make_from_cil ({SYSTEM_STRING}), as_string_8: {READABLE_STRING_8, STRING_8} feature -- Initialization adapt (s: STRING_32): like Current -- Object of a type conforming to the type of s, -- initialized with attributes from s do Result := new_string (0); Result.share (s) ensure adapt_not_void: Result /= Void shared_implementation: Result.shared_with (s) end from_c (c_string: POINTER) -- Reset contents of string from contents of c_string, -- a string created by some C function. require c_string_exists: c_string /= default_pointer local l_count: INTEGER_32 do C_string_provider.set_shared_from_pointer (c_string) l_count := C_string_provider.count grow (l_count + 1) count := l_count reset_hash_codes; C_string_provider.read_string_into (Current) ensure no_zero_byte: not has ('%U'.to_character_32) end from_c_substring (c_string: POINTER; start_pos, end_pos: INTEGER_32) -- Reset contents of string from substring of c_string, -- a string created by some C function. require c_string_exists: c_string /= default_pointer start_position_big_enough: start_pos >= 1 end_position_big_enough: start_pos <= end_pos + 1 local l_count: INTEGER_32 do l_count := end_pos - start_pos + 1; C_string_provider.set_shared_from_pointer_and_count (c_string + (start_pos - 1), l_count) grow (l_count + 1) count := l_count reset_hash_codes; C_string_provider.read_substring_into (Current, 1, l_count) ensure valid_count: count = end_pos - start_pos + 1 end make (n: INTEGER_32) -- Allocate space for at least n characters. -- (from READABLE_STRING_32) require -- from READABLE_STRING_GENERAL non_negative_size: n >= 0 do count := 0 internal_hash_code := 0 create area.make_filled ('%U'.to_character_32, n + 1) ensure -- from READABLE_STRING_GENERAL empty_string: count = 0 area_allocated: capacity >= n end make_empty -- Create empty string. -- (from READABLE_STRING_GENERAL) do make (0) ensure -- from READABLE_STRING_GENERAL empty: count = 0 area_allocated: capacity >= 0 end make_filled (c: CHARACTER_32; n: INTEGER_32) -- Create string of length n filled with c. -- (from READABLE_STRING_32) require -- from READABLE_STRING_32 valid_count: n >= 0 do make (n) fill_character (c) ensure -- from READABLE_STRING_32 count_set: count = n area_allocated: capacity >= n filled: occurrences (c) = count end make_from_c (c_string: POINTER) -- Initialize from contents of c_string, -- a string created by some C function. -- (from READABLE_STRING_32) require -- from READABLE_STRING_32 c_string_exists: c_string /= default_pointer local l_count: INTEGER_32 do C_string_provider.set_shared_from_pointer (c_string) l_count := C_string_provider.count create area.make_filled ('%U'.to_character_32, l_count + 1) count := l_count internal_hash_code := 0; C_string_provider.read_substring_into_character_32_area (area, 1, l_count) end make_from_cil (a_system_string: detachable SYSTEM_STRING) -- Initialize Current with a_system_string. require -- from READABLE_STRING_32 is_dotnet: {PLATFORM}.is_dotnet local l_count: INTEGER_32 do if a_system_string /= Void then l_count := a_system_string.length + Dotnet_convertor.escape_count (a_system_string) end make (l_count) if l_count > 0 and then a_system_string /= Void then set_count (l_count); Dotnet_convertor.read_system_string_into (a_system_string, Current) end end make_from_string (s: READABLE_STRING_32) -- Initialize from the characters of s. -- (from READABLE_STRING_32) require -- from READABLE_STRING_32 string_exists: s /= Void do area := s.area count := s.count internal_hash_code := 0 if Current /= s then create area.make_empty (count + 1); area.copy_data (s.area, s.area_lower, 0, count + 1) end ensure -- from READABLE_STRING_32 not_shared_implementation: Current /= s implies not shared_with (s) initialized: same_string (s) end make_from_string_general (s: READABLE_STRING_GENERAL) -- Initialize from the characters of s. require -- from READABLE_STRING_32 string_exists: s /= Void do if attached {READABLE_STRING_32} s as s32 then make_from_string (s32) else make (s.count) append_string_general (s) end ensure -- from READABLE_STRING_32 not_shared_implementation: Current /= s initialized: same_string_general (s) end remake (n: INTEGER_32) obsolete "Use `make' instead. [2017-05-31]" -- Allocate space for at least n characters. require non_negative_size: n >= 0 do make (n) ensure empty_string: count = 0 area_allocated: capacity >= n end feature {NONE} -- Initialization default_create -- Process instances of classes with no creation clause. -- (Default: do nothing.) -- (from ANY) do end make_empty_area (n: INTEGER_32) -- Creates a special object for n entries. -- (from TO_SPECIAL) require -- from TO_SPECIAL non_negative_argument: n >= 0 do create area.make_empty (n) ensure -- from TO_SPECIAL area_allocated: area /= Void capacity_set: area.capacity = n count_set: area.count = 0 end make_filled_area (a_default_value: CHARACTER_32; n: INTEGER_32) -- Creates a special object for n entries. -- (from TO_SPECIAL) require -- from TO_SPECIAL non_negative_argument: n >= 0 do create area.make_filled (a_default_value, n) ensure -- from TO_SPECIAL area_allocated: area /= Void capacity_set: area.capacity = n count_set: area.count = n area_filled: area.filled_with (a_default_value, 0, n - 1) end make_from_c_byte_array (a_byte_array: POINTER; a_character_count: INTEGER_32) -- Initialize from contents of a_byte_array for a length of a_character_count, -- given that each character is encoded in 4 bytes (little endian). -- ex: (char*) "a\000\000\000b\000\000\000c\000\000\000" for unicode STRING_32 "abc" -- (from READABLE_STRING_32) require -- from READABLE_STRING_32 a_byte_array_exists: not a_byte_array.is_default_pointer do C_string_provider.set_shared_from_pointer_and_count (a_byte_array, 4 * a_character_count) create area.make_filled ('%U'.to_character_32, 4 * a_character_count + 1) count := a_character_count internal_hash_code := 0; C_string_provider.read_unicode_substring_into_character_32_area (area, 1, 4 * a_character_count) end make_from_c_pointer (c_string: POINTER) obsolete "Use `make_from_c'. [2017-05-31]" -- Create new instance from contents of c_string, -- a string created by some C function. -- (from READABLE_STRING_32) require -- from READABLE_STRING_32 c_string_exists: c_string /= default_pointer do make_from_c (c_string) end make_from_separate (other: separate READABLE_STRING_GENERAL) -- Initialize current string from other. -- (from READABLE_STRING_32) require -- from READABLE_STRING_32 other_not_void: other /= Void local i, nb: INTEGER_32 l_area: like area do nb := other.count make (nb) from l_area := area i := 0 until i = nb loop l_area.put (other.item (i + 1), i) i := i + 1 end count := nb ensure -- from READABLE_STRING_32 same_string: end feature -- Access area: SPECIAL [CHARACTER_32] -- Storage for characters at alias "@" (i: INTEGER_32): CHARACTER_32 assign put -- Character at position i -- Was declared in STRING_32 as synonym of item. require -- from READABLE_STRING_32 True require -- from TABLE valid_key: valid_index (i) require -- from TO_SPECIAL valid_index: valid_index (i) do Result := area.item (i - 1) end case_insensitive_hash_code: INTEGER_32 -- Hash code value of the lower case version of Current. -- (from READABLE_STRING_GENERAL) local l_props: like Character_properties i, nb: INTEGER_32 do Result := internal_case_insensitive_hash_code if Result = 0 then from i := 1 nb := count l_props := Character_properties until i > nb loop Result := ((Result \\ 8388593) |<< 8) + l_props.to_lower (item (i)).code i := i + 1 end internal_case_insensitive_hash_code := Result end ensure -- from READABLE_STRING_GENERAL consistent: Result = as_lower.case_insensitive_hash_code end code (i: INTEGER_32): NATURAL_32 -- Character at position i require -- from READABLE_STRING_GENERAL valid_index: valid_index (i) do Result := area.item (i - 1).code.to_natural_32 end False_constant: STRING_8 = "false" -- Constant string "false" -- (from READABLE_STRING_GENERAL) fuzzy_index (other: READABLE_STRING_GENERAL; start: INTEGER_32; fuzz: INTEGER_32): INTEGER_32 -- Position of first occurrence of other at or after start -- with 0..fuzz mismatches between the string and other. -- 0 if there are no fuzzy matches -- (from READABLE_STRING_32) require -- from READABLE_STRING_GENERAL other_exists: other /= Void other_not_empty: not other.is_empty start_large_enough: start >= 1 start_small_enough: start <= count acceptable_fuzzy: fuzz <= other.count do Result := String_searcher.fuzzy_index (Current, other, start, count, fuzz) end generating_type: TYPE [detachable STRING_32] -- 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 hash_code: INTEGER_32 -- Hash code value -- (from READABLE_STRING_GENERAL) local i, nb: INTEGER_32 do Result := internal_hash_code if Result = 0 then from i := 1 nb := count until i > nb loop Result := ((Result \\ 8388593) |<< 8) + item (i).code i := i + 1 end internal_hash_code := Result end ensure -- from HASHABLE good_hash_value: Result >= 0 end index_of (c: CHARACTER_32; start_index: INTEGER_32): INTEGER_32 -- Position of first occurrence of c at or after start_index; -- 0 if none. -- (from READABLE_STRING_32) require -- from READABLE_STRING_GENERAL start_large_enough: start_index >= 1 start_small_enough: start_index <= count + 1 local a: like area i, nb, l_lower_area: INTEGER_32 do nb := count if start_index <= nb then from l_lower_area := area_lower i := start_index - 1 + l_lower_area nb := nb + l_lower_area a := area until i = nb or else a.item (i) = c loop i := i + 1 end if i < nb then Result := i + 1 - l_lower_area end end ensure -- from READABLE_STRING_GENERAL valid_result: Result = 0 or (start_index <= Result and Result <= count) zero_if_absent: (Result = 0) = not substring (start_index, count).has (c) found_if_present: substring (start_index, count).has (c) implies item (Result) = c none_before: substring (start_index, count).has (c) implies not substring (start_index, Result - 1).has (c) end index_of_code (c: like code; start_index: INTEGER_32): INTEGER_32 -- Position of first occurrence of c at or after start_index; -- 0 if none. -- (from READABLE_STRING_GENERAL) require -- from READABLE_STRING_GENERAL start_large_enough: start_index >= 1 start_small_enough: start_index <= count + 1 local i, nb: INTEGER_32 do nb := count if start_index <= nb then from i := start_index until i > nb or else code (i) = c loop i := i + 1 end if i <= nb then Result := i end end ensure -- from READABLE_STRING_GENERAL valid_result: Result = 0 or (start_index <= Result and Result <= count) zero_if_absent: (Result = 0) = not substring (start_index, count).has_code (c) found_if_present: substring (start_index, count).has_code (c) implies code (Result) = c none_before: substring (start_index, count).has_code (c) implies not substring (start_index, Result - 1).has_code (c) end item alias "[]" (i: INTEGER_32): CHARACTER_32 assign put -- Character at position i -- Was declared in STRING_32 as synonym of at. require -- from READABLE_STRING_GENERAL valid_index: valid_index (i) require -- from READABLE_INDEXABLE valid_index: valid_index (i) require -- from TABLE valid_key: valid_index (i) require -- from TO_SPECIAL valid_index: valid_index (i) do Result := area.item (i - 1) end item_code (i: INTEGER_32): INTEGER_32 obsolete "Due to potential truncation it is recommended to use `code (i)' instead. [2017-05-31]" -- Character at position i require -- from READABLE_STRING_32 index_small_enough: i <= count index_large_enough: i > 0 do Result := area.item (i - 1).natural_32_code.as_integer_32 end last_index_of (c: CHARACTER_32; start_index_from_end: INTEGER_32): INTEGER_32 -- Position of last occurrence of c. -- 0 if none. -- (from READABLE_STRING_32) require -- from READABLE_STRING_GENERAL start_index_small_enough: start_index_from_end <= count start_index_large_enough: start_index_from_end >= 1 local a: like area i, l_lower_area: INTEGER_32 do from l_lower_area := area_lower i := start_index_from_end - 1 + l_lower_area a := area until i < l_lower_area or else a.item (i) = c loop i := i - 1 end Result := i + 1 - l_lower_area ensure -- from READABLE_STRING_GENERAL valid_result: 0 <= Result and Result <= start_index_from_end zero_if_absent: (Result = 0) = not substring (1, start_index_from_end).has (c) found_if_present: substring (1, start_index_from_end).has (c) implies item (Result) = c none_after: substring (1, start_index_from_end).has (c) implies not substring (Result + 1, start_index_from_end).has (c) end last_index_of_code (c: like code; start_index_from_end: INTEGER_32): INTEGER_32 -- Position of last occurrence of c. -- 0 if none. -- (from READABLE_STRING_GENERAL) require -- from READABLE_STRING_GENERAL start_index_small_enough: start_index_from_end <= count start_index_large_enough: start_index_from_end >= 1 do from Result := start_index_from_end until Result <= 0 or else code (Result) = c loop Result := Result - 1 end ensure -- from READABLE_STRING_GENERAL valid_result: 0 <= Result and Result <= start_index_from_end zero_if_absent: (Result = 0) = not substring (1, start_index_from_end).has_code (c) found_if_present: substring (1, start_index_from_end).has_code (c) implies code (Result) = c none_after: substring (1, start_index_from_end).has_code (c) implies not substring (Result + 1, start_index_from_end).has_code (c) end new_cursor: STRING_32_ITERATION_CURSOR -- Fresh cursor associated with current structure -- (from READABLE_STRING_32) require -- from ITERABLE True do create Result.make (Current) ensure -- from ITERABLE result_attached: Result /= Void end shared_with (other: READABLE_STRING_32): BOOLEAN -- Does string share the text of other? -- (from READABLE_STRING_32) do Result := (other /= Void) and then (area = other.area) end string: STRING_32 -- New STRING_32 having same character sequence as Current. -- (from READABLE_STRING_32) do create Result.make_from_string (Current) ensure -- from READABLE_STRING_32 string_not_void: Result /= Void string_type: Result.same_type (create {STRING_32}.make_empty) first_item: count > 0 implies Result.item (1) = item (1) recurse: count > 1 implies Result.substring (2, count) ~ substring (2, count).string end string_representation: STRING_32 -- Similar to string but only create a new object if Current is not of dynamic type STRING_32. -- (from READABLE_STRING_32) do if same_type (create {STRING_32}.make_empty) and then attached {STRING_32} Current as l_s32 then Result := l_s32 else Result := string end ensure -- from READABLE_STRING_32 result_not_void: Result /= Void correct_type: Result.same_type (create {STRING_32}.make_empty) first_item: count > 0 implies Result.item (1) = item (1) recurse: count > 1 implies Result.substring (2, count) ~ substring (2, count).string end substring_index (other: READABLE_STRING_GENERAL; start_index: INTEGER_32): INTEGER_32 -- Index of first occurrence of other at or after start_index; -- 0 if none -- (from READABLE_STRING_32) require -- from READABLE_STRING_GENERAL other_not_void: other /= Void valid_start_index: start_index >= 1 and start_index <= count + 1 do Result := String_searcher.substring_index (Current, other, start_index, count) ensure -- from READABLE_STRING_GENERAL valid_result: Result = 0 or else (start_index <= Result and Result <= count - other.count + 1) zero_if_absent: (Result = 0) = not substring (start_index, count).has_substring (other) at_this_index: Result >= start_index implies other.same_string (substring (Result, Result + other.count - 1)) none_before: Result > start_index implies not substring (start_index, Result + other.count - 2).has_substring (other) end substring_index_in_bounds (other: READABLE_STRING_GENERAL; start_pos, end_pos: INTEGER_32): INTEGER_32 -- Position of first occurrence of other at or after start_pos -- and to or before end_pos; -- 0 if none. -- (from READABLE_STRING_32) require -- from READABLE_STRING_GENERAL other_nonvoid: other /= Void other_notempty: not other.is_empty start_pos_large_enough: start_pos >= 1 start_pos_small_enough: start_pos <= count end_pos_large_enough: end_pos >= start_pos end_pos_small_enough: end_pos <= count do Result := String_searcher.substring_index (Current, other, start_pos, end_pos) ensure -- from READABLE_STRING_GENERAL correct_place: Result > 0 implies other.same_string (substring (Result, Result + other.count - 1)) end True_constant: STRING_8 = "true" -- Constant string "true" -- (from READABLE_STRING_GENERAL) feature -- Measurement additional_space: INTEGER_32 -- Proposed number of additional items -- (from RESIZABLE) do Result := (capacity // 2).max (Minimal_increase) ensure -- from RESIZABLE at_least_one: Result >= 1 end capacity: INTEGER_32 -- Number of characters allocated in Current -- (from READABLE_STRING_32) require -- from READABLE_STRING_GENERAL True require -- from BOUNDED True do Result := area.count - 1 ensure -- from READABLE_STRING_GENERAL capacity_non_negative: Result >= 0 ensure -- from BOUNDED capacity_non_negative: Result >= 0 end count: INTEGER_32 -- Actual number of characters making up the string. -- (from READABLE_STRING_32) Growth_percentage: INTEGER_32 = 50 -- Percentage by which structure will grow automatically -- (from RESIZABLE) 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 READABLE_STRING_32) Minimal_increase: INTEGER_32 = 5 -- Minimal number of additional items -- (from RESIZABLE) occurrences (c: CHARACTER_32): INTEGER_32 -- Number of times c appears in the string -- (from READABLE_STRING_32) require -- from READABLE_STRING_GENERAL True require -- from BAG True local i, nb: INTEGER_32 a: SPECIAL [CHARACTER_32] do from i := area_lower nb := count + i a := area until i = nb loop if a.item (i) = c then Result := Result + 1 end i := i + 1 end ensure then -- from READABLE_STRING_GENERAL zero_if_empty: count = 0 implies Result = 0 recurse_if_not_found_at_first_position: (count > 0 and then item (1) /= c) implies Result = substring (2, count).occurrences (c) recurse_if_found_at_first_position: (count > 0 and then item (1) = c) implies Result = 1 + substring (2, count).occurrences (c) ensure -- from BAG non_negative_occurrences: Result >= 0 ensure then -- from READABLE_STRING_32 zero_if_empty: count = 0 implies Result = 0 recurse_if_not_found_at_first_position: (count > 0 and then item (1) /= c) implies Result = substring (2, count).occurrences (c) recurse_if_found_at_first_position: (count > 0 and then item (1) = c) implies Result = 1 + substring (2, count).occurrences (c) end feature {NONE} -- Measurement estimated_count_of (other: ITERABLE [CHARACTER_32]): INTEGER_32 -- Estimated number of elements in other. -- (from CONTAINER) do if attached {FINITE [CHARACTER_32]} other as f then Result := f.count elseif attached {READABLE_INDEXABLE [CHARACTER_32]} 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 ends_with_general (s: READABLE_STRING_GENERAL): BOOLEAN -- Does string finish with s? -- (from READABLE_STRING_GENERAL) require -- from READABLE_STRING_GENERAL argument_not_void: s /= Void local i, j: INTEGER_32 do if Current = s then Result := True else i := s.count j := count if i <= j then from Result := True until i = 0 loop if code (j) /= s.code (i) then Result := False i := 1 end i := i - 1 j := j - 1 end end end ensure -- from READABLE_STRING_GENERAL definition: Result = s.same_string (substring (count - s.count + 1, count)) 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 has_substring (other: READABLE_STRING_GENERAL): BOOLEAN -- Does Current contain other? -- (from READABLE_STRING_GENERAL) require -- from READABLE_STRING_GENERAL other_not_void: other /= Void do if other = Current then Result := True elseif other.count <= count then Result := substring_index (other, 1) > 0 end ensure -- from READABLE_STRING_GENERAL false_if_too_small: count < other.count implies not Result true_if_initial: (count >= other.count and then other.same_string (substring (1, other.count))) implies Result recurse: (count >= other.count and then not other.same_string (substring (1, other.count))) implies (Result = substring (2, count).has_substring (other)) end is_case_insensitive_equal_general (other: READABLE_STRING_GENERAL): BOOLEAN -- Is string made of same character sequence as other regardless of casing -- (possibly with a different capacity)? -- (from READABLE_STRING_GENERAL) local nb: INTEGER_32 do if other = Current then Result := True else nb := count if nb = other.count then Result := nb = 0 or else same_caseless_characters_general (other, 1, nb, 1) end end ensure -- from READABLE_STRING_GENERAL symmetric: Result implies other.is_case_insensitive_equal (Current) consistent: attached {STRING_32} other as l_other implies (standard_is_equal (l_other) implies Result) valid_result: as_lower ~ other.as_lower implies Result end is_case_insensitive_equal (other: READABLE_STRING_32): BOOLEAN -- Is string made of same character sequence as other regardless of casing -- (possibly with a different capacity)? -- (from READABLE_STRING_32) require -- from READABLE_STRING_32 other_not_void: other /= Void local nb: INTEGER_32 do if other = Current then Result := True else nb := count if nb = other.count then Result := nb = 0 or else same_caseless_characters (other, 1, nb, 1) end end ensure -- from READABLE_STRING_32 symmetric: Result implies other.is_case_insensitive_equal (Current) consistent: attached {STRING_32} other as l_other implies (standard_is_equal (l_other) implies Result) valid_result: as_lower.same_string (other.as_lower) implies Result end frozen is_deep_equal alias "≡≡≡" (other: STRING_32): 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: STRING_32): BOOLEAN -- Is string made of same character sequence as other -- (possibly with a different capacity)? -- (from READABLE_STRING_32) require -- from ANY other_not_void: other /= Void local nb: INTEGER_32 l_hash, l_other_hash: like internal_hash_code do if other = Current then Result := True else nb := count if nb = other.count then l_hash := internal_hash_code l_other_hash := other.internal_hash_code if l_hash = 0 or else l_other_hash = 0 or else l_hash = l_other_hash then Result := area.same_items (other.area, other.area_lower, area_lower, nb) end end end ensure -- from ANY symmetric: Result implies other ~ Current consistent: standard_is_equal (other) implies Result ensure then -- from COMPARABLE trichotomy: Result = (not (Current < other) and not (other < Current)) end is_greater alias ">" (other: STRING_32): BOOLEAN -- Is current object greater than other? -- (from COMPARABLE) require -- from PART_COMPARABLE other_exists: other /= Void do Result := other < Current ensure then -- from COMPARABLE definition: Result = (other < Current) end is_greater_equal alias ">=" alias "≥" (other: STRING_32): BOOLEAN -- Is current object greater than or equal to other? -- (from COMPARABLE) require -- from PART_COMPARABLE other_exists: other /= Void do Result := not (Current < other) ensure then -- from COMPARABLE definition: Result = (other <= Current) end is_less alias "<" (other: STRING_32): BOOLEAN -- Is string lexicographically lower than other? -- (from READABLE_STRING_32) require -- from PART_COMPARABLE other_exists: other /= Void local other_count: INTEGER_32 current_count: INTEGER_32 do if other /= Current then other_count := other.count current_count := count if other_count = current_count then Result := str_strict_cmp (other.area, area, other.area_lower, area_lower, other_count) > 0 else if current_count < other_count then Result := str_strict_cmp (other.area, area, other.area_lower, area_lower, current_count) >= 0 else Result := str_strict_cmp (other.area, area, other.area_lower, area_lower, other_count) > 0 end end end ensure then -- from COMPARABLE asymmetric: Result implies not (other < Current) end is_less_equal alias "<=" alias "≤" (other: STRING_32): BOOLEAN -- Is current object less than or equal to other? -- (from COMPARABLE) require -- from PART_COMPARABLE other_exists: other /= Void do Result := not (other < Current) ensure then -- from COMPARABLE definition: Result = ((Current < other) or (Current ~ other)) end max alias "∨" (other: STRING_32): STRING_32 -- The greater of current object and other -- (from COMPARABLE) require -- from COMPARABLE other_exists: other /= Void do if Current >= other then Result := Current else Result := other end ensure -- from COMPARABLE current_if_not_smaller: Current >= other implies Result = Current other_if_smaller: Current < other implies Result = other end min alias "∧" (other: STRING_32): STRING_32 -- The smaller of current object and other -- (from COMPARABLE) require -- from COMPARABLE other_exists: other /= Void do if Current <= other then Result := Current else Result := other end ensure -- from COMPARABLE current_if_not_greater: Current <= other implies Result = Current other_if_greater: Current > other implies Result = other end same_caseless_characters_general (other: READABLE_STRING_GENERAL; start_pos, end_pos, index_pos: INTEGER_32): BOOLEAN -- Are characters of other within bounds start_pos and end_pos -- caseless identical to characters of current string starting at index index_pos. -- (from READABLE_STRING_GENERAL) require -- from READABLE_STRING_GENERAL other_not_void: other /= Void valid_start_pos: other.valid_index (start_pos) valid_end_pos: other.valid_index (end_pos) valid_bounds: (start_pos <= end_pos) or (start_pos = end_pos + 1) valid_index_pos: valid_index (index_pos) local i, j, nb: INTEGER_32 l_prop: like Character_properties c1, c2: like item do nb := end_pos - start_pos + 1 if nb <= count - index_pos + 1 then from l_prop := Character_properties Result := True i := index_pos j := start_pos nb := nb + i variant increasing_index: nb - i + 1 until i = nb loop c1 := item (i) c2 := other.item (j) if c1 /= c2 and then l_prop.to_lower (c1) /= l_prop.to_lower (c2) then Result := False i := nb - 1 end i := i + 1 j := j + 1 end end ensure -- from READABLE_STRING_GENERAL same_characters: Result = substring (index_pos, index_pos + end_pos - start_pos).is_case_insensitive_equal_general (other.substring (start_pos, end_pos)) end same_caseless_characters (other: READABLE_STRING_32; start_pos, end_pos, index_pos: INTEGER_32): BOOLEAN -- Are characters of other within bounds start_pos and end_pos -- caseless identical to characters of current string starting at index index_pos. -- (from READABLE_STRING_32) require -- from READABLE_STRING_32 other_not_void: other /= Void valid_start_pos: other.valid_index (start_pos) valid_end_pos: other.valid_index (end_pos) valid_bounds: (start_pos <= end_pos) or (start_pos = end_pos + 1) valid_index_pos: valid_index (index_pos) local i, j, nb: INTEGER_32 l_prop: like Character_properties l_area, l_other_area: like area c1, c2: CHARACTER_32 do nb := end_pos - start_pos + 1 if nb <= count - index_pos + 1 then from l_prop := Character_properties l_area := area l_other_area := other.area Result := True i := area_lower + index_pos - 1 j := other.area_lower + start_pos - 1 nb := nb + i variant increasing_index: nb - i + 1 until i = nb loop c1 := l_area.item (i) c2 := l_other_area.item (j) if c1 /= c2 and then l_prop.to_lower (c1) /= l_prop.to_lower (c2) then Result := False i := nb - 1 end i := i + 1 j := j + 1 end end ensure -- from READABLE_STRING_32 same_characters: Result = substring (index_pos, index_pos + end_pos - start_pos).is_case_insensitive_equal (other.substring (start_pos, end_pos)) end same_characters_general (other: READABLE_STRING_GENERAL; start_pos, end_pos, index_pos: INTEGER_32): BOOLEAN -- Are characters of other within bounds start_pos and end_pos -- identical to characters of current string starting at index index_pos. -- (from READABLE_STRING_GENERAL) require -- from READABLE_STRING_GENERAL other_not_void: other /= Void valid_start_pos: other.valid_index (start_pos) valid_end_pos: other.valid_index (end_pos) valid_bounds: (start_pos <= end_pos) or (start_pos = end_pos + 1) valid_index_pos: valid_index (index_pos) local i, j, nb: INTEGER_32 do nb := end_pos - start_pos + 1 if nb <= count - index_pos + 1 then from Result := True i := index_pos j := start_pos nb := nb + i variant increasing_index: nb - i + 1 until i = nb loop if item (i) /= other.item (j) then Result := False i := nb - 1 end i := i + 1 j := j + 1 end end ensure -- from READABLE_STRING_GENERAL same_characters: Result = substring (index_pos, index_pos + end_pos - start_pos).same_string_general (other.substring (start_pos, end_pos)) end same_characters (other: READABLE_STRING_32; start_pos, end_pos, index_pos: INTEGER_32): BOOLEAN -- Are characters of other within bounds start_pos and end_pos -- identical to characters of current string starting at index index_pos. -- (from READABLE_STRING_32) require -- from READABLE_STRING_32 other_not_void: other /= Void valid_start_pos: other.valid_index (start_pos) valid_end_pos: other.valid_index (end_pos) valid_bounds: (start_pos <= end_pos) or (start_pos = end_pos + 1) valid_index_pos: valid_index (index_pos) local nb: INTEGER_32 do nb := end_pos - start_pos + 1 if nb <= count - index_pos + 1 then Result := area.same_items (other.area, other.area_lower + start_pos - 1, area_lower + index_pos - 1, nb) end ensure -- from READABLE_STRING_32 same_characters: Result = substring (index_pos, index_pos + end_pos - start_pos).same_string (other.substring (start_pos, end_pos)) end same_string (other: READABLE_STRING_32): BOOLEAN -- Do Current and other have same character sequence? -- (from READABLE_STRING_32) require -- from READABLE_STRING_32 other_not_void: other /= Void local nb: INTEGER_32 do if other = Current then Result := True else nb := count if nb = other.count then Result := nb = 0 or else same_characters (other, 1, nb, 1) end end ensure -- from READABLE_STRING_32 definition: Result = (string ~ other.string) end same_string_general (other: READABLE_STRING_GENERAL): BOOLEAN -- Does other represent the same string as Current? -- (from READABLE_STRING_GENERAL) require -- from READABLE_STRING_GENERAL other_not_void: other /= Void local nb: INTEGER_32 do if other = Current then Result := True else nb := count if nb = other.count then Result := nb = 0 or else same_characters_general (other, 1, nb, 1) end end 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: STRING_32): 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 starts_with_general (s: READABLE_STRING_GENERAL): BOOLEAN -- Does string begin with s? -- (from READABLE_STRING_GENERAL) require -- from READABLE_STRING_GENERAL argument_not_void: s /= Void local i: INTEGER_32 do if Current = s then Result := True else i := s.count if i <= count then from Result := True until i = 0 loop if code (i) /= s.code (i) then Result := False i := 1 end i := i - 1 end end end ensure -- from READABLE_STRING_GENERAL definition: Result = s.same_string (substring (1, s.count)) end three_way_comparison alias "⋚" (other: STRING_32): INTEGER_32 -- If current object equal to other, 0; -- if smaller, -1; if greater, 1 -- (from COMPARABLE) require -- from COMPARABLE other_exists: other /= Void do if Current < other then Result := -1 elseif other < Current then Result := 1 end ensure -- from COMPARABLE equal_zero: (Result = 0) = (Current ~ other) smaller_negative: (Result = -1) = (Current < other) greater_positive: (Result = 1) = (Current > other) end feature -- Status report Changeable_comparison_criterion: BOOLEAN = False -- May object_comparison be changed? -- (Answer: yes by default.) 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 ends_with (s: READABLE_STRING_32): BOOLEAN -- Does string finish with s? -- (from READABLE_STRING_32) require -- from READABLE_STRING_32 argument_not_void: s /= Void local i, j, nb: INTEGER_32 l_area, l_s_area: like area do if Current = s then Result := True else i := s.count j := count if i <= j then from l_area := area l_s_area := s.area j := area_upper + 1 i := s.area_upper + 1 nb := s.area_lower Result := True until i = nb loop i := i - 1 j := j - 1 if l_area.item (j) /= l_s_area.item (i) then Result := False i := nb end end end end ensure -- from READABLE_STRING_32 definition: Result = s.same_string (substring (count - s.count + 1, count)) end Extendible: BOOLEAN = True -- May new items be added? (Answer: yes.) full: BOOLEAN -- Is structure full? -- (from BOUNDED) do Result := count = capacity end has (c: CHARACTER_32): BOOLEAN -- Does string include c? -- (from READABLE_STRING_32) require -- from READABLE_STRING_GENERAL True require -- from CONTAINER True local i, nb: INTEGER_32 l_area: like area do nb := count if nb > 0 then from i := area_lower l_area := area nb := nb + i until i = nb or else l_area.item (i) = c loop i := i + 1 end Result := i < nb end ensure then -- from READABLE_STRING_GENERAL false_if_empty: count = 0 implies not Result true_if_first: count > 0 and then item (1) = c implies Result recurse: (count > 0 and then item (1) /= c) implies (Result = substring (2, count).has (c)) ensure -- from CONTAINER not_found_in_empty: Result implies not is_empty end has_code (c: like code): BOOLEAN -- Does string include c? -- (from READABLE_STRING_GENERAL) local i, nb: INTEGER_32 do nb := count if nb > 0 then from i := 1 until i > nb or else (code (i) = c) loop i := i + 1 end Result := i <= nb end ensure then -- from READABLE_STRING_GENERAL false_if_empty: count = 0 implies not Result true_if_first: count > 0 and then code (1) = c implies Result recurse: (count > 0 and then code (1) /= c) implies (Result = substring (2, count).has_code (c)) end is_boolean: BOOLEAN -- Does Current represent a BOOLEAN? -- (from READABLE_STRING_32) require -- from READABLE_STRING_GENERAL True local nb: INTEGER_32 do nb := count if nb = 4 then Result := is_case_insensitive_equal_general (True_constant) elseif nb = 5 then Result := is_case_insensitive_equal_general (False_constant) end ensure -- from READABLE_STRING_GENERAL is_boolean: Result = (True_constant.same_string_general (as_lower) or False_constant.same_string_general (as_lower)) end is_double: BOOLEAN -- Does Current represent a REAL_64? -- Was declared in READABLE_STRING_GENERAL as synonym of is_real_64. -- (from READABLE_STRING_GENERAL) local l_convertor: like Ctor_convertor do l_convertor := Ctor_convertor; l_convertor.parse_string_with_type (Current, {NUMERIC_INFORMATION}.type_double) Result := l_convertor.is_integral_double end is_empty: BOOLEAN -- Is structure empty? -- (from FINITE) require -- from CONTAINER True require -- from READABLE_STRING_GENERAL True do Result := count = 0 end is_hashable: BOOLEAN -- May current object be hashed? -- (True by default.) -- (from HASHABLE) do Result := True end is_immutable: BOOLEAN -- Can the character sequence of Current be not changed? -- (from READABLE_STRING_GENERAL) do Result := False end is_inserted (v: CHARACTER_32): 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 is_integer: BOOLEAN -- Does Current represent an INTEGER_32? -- Was declared in READABLE_STRING_GENERAL as synonym of is_integer_32. -- (from READABLE_STRING_GENERAL) do Result := is_valid_integer_or_natural ({NUMERIC_INFORMATION}.type_integer_32) end is_integer_16: BOOLEAN -- Does Current represent an INTEGER_16? -- (from READABLE_STRING_GENERAL) do Result := is_valid_integer_or_natural ({NUMERIC_INFORMATION}.type_integer_16) end is_integer_32: BOOLEAN -- Does Current represent an INTEGER_32? -- Was declared in READABLE_STRING_GENERAL as synonym of is_integer. -- (from READABLE_STRING_GENERAL) do Result := is_valid_integer_or_natural ({NUMERIC_INFORMATION}.type_integer_32) end is_integer_64: BOOLEAN -- Does Current represent an INTEGER_64? -- (from READABLE_STRING_GENERAL) do Result := is_valid_integer_or_natural ({NUMERIC_INFORMATION}.type_integer_64) end is_integer_8: BOOLEAN -- Does Current represent an INTEGER_8? -- (from READABLE_STRING_GENERAL) do Result := is_valid_integer_or_natural ({NUMERIC_INFORMATION}.type_integer_8) end is_natural: BOOLEAN -- Does Current represent a NATURAL_32? -- Was declared in READABLE_STRING_GENERAL as synonym of is_natural_32. -- (from READABLE_STRING_GENERAL) do Result := is_valid_integer_or_natural ({NUMERIC_INFORMATION}.type_natural_32) end is_natural_16: BOOLEAN -- Does Current represent a NATURAL_16? -- (from READABLE_STRING_GENERAL) do Result := is_valid_integer_or_natural ({NUMERIC_INFORMATION}.type_natural_16) end is_natural_32: BOOLEAN -- Does Current represent a NATURAL_32? -- Was declared in READABLE_STRING_GENERAL as synonym of is_natural. -- (from READABLE_STRING_GENERAL) do Result := is_valid_integer_or_natural ({NUMERIC_INFORMATION}.type_natural_32) end is_natural_64: BOOLEAN -- Does Current represent a NATURAL_64? -- (from READABLE_STRING_GENERAL) do Result := is_valid_integer_or_natural ({NUMERIC_INFORMATION}.type_natural_64) end is_natural_8: BOOLEAN -- Does Current represent a NATURAL_8? -- (from READABLE_STRING_GENERAL) do Result := is_valid_integer_or_natural ({NUMERIC_INFORMATION}.type_natural_8) end is_number_sequence: BOOLEAN -- Does Current represent a number sequence? -- (from READABLE_STRING_GENERAL) do Result := is_valid_integer_or_natural ({NUMERIC_INFORMATION}.type_no_limitation) end is_real: BOOLEAN -- Does Current represent a REAL_32? -- Was declared in READABLE_STRING_GENERAL as synonym of is_real_32. -- (from READABLE_STRING_GENERAL) local l_convertor: like Ctor_convertor do l_convertor := Ctor_convertor; l_convertor.parse_string_with_type (Current, {NUMERIC_INFORMATION}.type_real) Result := l_convertor.is_integral_real end is_real_32: BOOLEAN -- Does Current represent a REAL_32? -- Was declared in READABLE_STRING_GENERAL as synonym of is_real. -- (from READABLE_STRING_GENERAL) local l_convertor: like Ctor_convertor do l_convertor := Ctor_convertor; l_convertor.parse_string_with_type (Current, {NUMERIC_INFORMATION}.type_real) Result := l_convertor.is_integral_real end is_real_64: BOOLEAN -- Does Current represent a REAL_64? -- Was declared in READABLE_STRING_GENERAL as synonym of is_double. -- (from READABLE_STRING_GENERAL) local l_convertor: like Ctor_convertor do l_convertor := Ctor_convertor; l_convertor.parse_string_with_type (Current, {NUMERIC_INFORMATION}.type_double) Result := l_convertor.is_integral_double end is_real_sequence: BOOLEAN -- Does Current represent a real sequence? -- (from READABLE_STRING_GENERAL) local l_convertor: like Ctor_convertor do l_convertor := Ctor_convertor; l_convertor.parse_string_with_type (Current, {NUMERIC_INFORMATION}.type_no_limitation) Result := l_convertor.is_integral_double end Is_string_32: BOOLEAN = True -- Is Current a sequence of CHARACTER_32? -- (from READABLE_STRING_32) Is_string_8: BOOLEAN = False -- Is Current a sequence of CHARACTER_8? -- (from READABLE_STRING_32) is_substring_whitespace (start_index, end_index: INTEGER_32): BOOLEAN -- Is substring between start_index and end_index containing only whitespace characters? -- (from READABLE_STRING_32) require -- from READABLE_STRING_GENERAL start_index_big_enough: 1 <= start_index end_index_small_enough: end_index <= count consistent_indexes: start_index - 1 <= end_index local i, n: INTEGER_32 l_prop: like Character_properties l_area: like area do from l_area := area i := area_lower + start_index - 1 n := area_lower + end_index - 1 l_prop := Character_properties until i > n or not l_prop.is_space (l_area.item (i)) loop i := i + 1 end Result := i > n end is_valid_as_string_8: BOOLEAN -- Is Current convertible to a sequence of CHARACTER_8 without information loss? -- (from READABLE_STRING_32) require -- from READABLE_STRING_GENERAL True local i, nb: INTEGER_32 l_area: like area do from Result := True i := area_lower nb := count + i l_area := area until i = nb or not Result loop Result := l_area.item (i).code <= {CHARACTER_8}.max_value i := i + 1 end end is_whitespace: BOOLEAN -- Is structure containing only whitespace characters? -- (from READABLE_STRING_GENERAL) do Result := is_substring_whitespace (1, count) end object_comparison: BOOLEAN -- Must search operations use equal rather than = -- for comparing references? (Default: no, use =.) -- (from CONTAINER) prunable: BOOLEAN -- May items be removed? (Answer: yes.) -- (from DYNAMIC_TABLE) require -- from COLLECTION True do Result := True end resizable: BOOLEAN -- May capacity be changed? (Answer: yes.) -- (from RESIZABLE) 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 starts_with (s: READABLE_STRING_32): BOOLEAN -- Does string begin with s? -- (from READABLE_STRING_32) require -- from READABLE_STRING_32 argument_not_void: s /= Void local i, j, nb: INTEGER_32 l_area, l_s_area: like area do if Current = s then Result := True else i := s.count if i <= count then from l_area := area l_s_area := s.area j := area_lower + i i := s.area_upper + 1 nb := s.area_lower Result := True until i = nb loop i := i - 1 j := j - 1 if l_area.item (j) /= l_s_area.item (i) then Result := False i := nb end end end end ensure -- from READABLE_STRING_32 definition: Result = s.same_string (substring (1, s.count)) end valid_code (v: NATURAL_32): BOOLEAN -- Is v a valid code for a CHARACTER_32? -- (from READABLE_STRING_32) require -- from READABLE_STRING_GENERAL True do Result := True end valid_index (i: INTEGER_32): BOOLEAN -- Is i within the bounds of the string? -- (from READABLE_STRING_GENERAL) require -- from READABLE_INDEXABLE True require -- from TABLE True require -- from TO_SPECIAL True do Result := (i > 0) and (i <= count) ensure -- from READABLE_INDEXABLE only_if_in_index_set: Result implies (Lower <= i and i <= count) ensure -- from READABLE_STRING_GENERAL definition: Result = (1 <= i and i <= count) 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 -- Element change adjust -- Remove leading and/or trailing whitespace. -- (from STRING_GENERAL) do left_adjust right_adjust ensure -- from STRING_GENERAL valid_count: count <= old count new_count_left: not is_empty implies not item (1).is_space new_count_right: not is_empty implies not item (count).is_space kept: Elks_checking implies (old twin).has_substring (Current) only_spaces_removed_before: Elks_checking implies (old twin).is_substring_whitespace (1, (old twin).substring_index (Current, 1) - 1) only_spaces_removed_after: Elks_checking implies (old twin).is_substring_whitespace ((old twin).substring_index (Current, 1) + count, old count) end append (s: READABLE_STRING_32) -- Append characters of s at end. require argument_not_void: s /= Void local l_count, l_s_count, l_new_size: INTEGER_32 do l_s_count := s.count if l_s_count > 0 then l_count := count l_new_size := l_s_count + l_count if l_new_size > capacity then resize (l_new_size + additional_space) end; area.copy_data (s.area, s.area_lower, l_count, l_s_count) count := l_new_size reset_hash_codes end ensure new_count: count = old count + old s.count appended: Elks_checking implies same_string (old (Current + s)) end append_boolean (b: BOOLEAN) -- Append the string representation of b at end. do append_string_general (b.out) end append_character (c: CHARACTER_32) -- Append c at end. -- Was declared in STRING_32 as synonym of extend. local current_count: INTEGER_32 do current_count := count if current_count = capacity then resize (current_count + additional_space) end; area.put (c, current_count) count := current_count + 1 reset_hash_codes ensure then item_inserted: item (count) = c new_count: count = old count + 1 stable_before: Elks_checking implies substring (1, count - 1) ~ (old twin) end append_code (c: like code) -- Append c at end. -- (from STRING_GENERAL) require -- from STRING_GENERAL valid_code: valid_code (c) local current_count: INTEGER_32 do current_count := count + 1 if current_count > capacity then resize (current_count) end set_count (current_count) put_code (c, current_count) ensure then -- from STRING_GENERAL item_inserted: code (count) = c new_count: count = old count + 1 stable_before: Elks_checking implies substring (1, count - 1) ~ (old twin) end append_double (d: REAL_64) -- Append the string representation of d at end. do append_string_general (d.out) end append_integer (i: INTEGER_32) -- Append the string representation of i at end. local l_value: INTEGER_32 l_starting_index, l_ending_index: INTEGER_32 l_temp: CHARACTER_32 l_area: like area do if i = 0 then append_character ('0'.to_character_32) else from l_starting_index := count if i < 0 then append_character ('-'.to_character_32) l_starting_index := l_starting_index + 1 if i = {INTEGER_32}.min_value then append_character ('8'.to_character_32) l_value := - (i // 10) else l_value := - i end else l_value := i end until l_value = 0 loop append_character ((l_value \\ 10 + 48).to_character_32) l_value := l_value // 10 end from l_ending_index := count - 1 l_area := area until l_starting_index >= l_ending_index loop l_temp := l_area.item (l_starting_index); l_area.put (l_area.item (l_ending_index), l_starting_index); l_area.put (l_temp, l_ending_index) l_ending_index := l_ending_index - 1 l_starting_index := l_starting_index + 1 end end end append_integer_16 (i: INTEGER_16) -- Append the string representation of i at end. local l_value: INTEGER_16 l_starting_index, l_ending_index: INTEGER_32 l_temp: CHARACTER_32 l_area: like area do if i = 0 then append_character ('0'.to_character_32) else from l_starting_index := count if i < 0 then append_character ('-'.to_character_32) l_starting_index := l_starting_index + 1 if i = {INTEGER_16}.min_value then append_character ('8'.to_character_32) l_value := - (i // 10) else l_value := - i end else l_value := i end until l_value = 0 loop append_character ((l_value \\ 10 + 48).to_character_32) l_value := l_value // 10 end from l_ending_index := count - 1 l_area := area until l_starting_index >= l_ending_index loop l_temp := l_area.item (l_starting_index); l_area.put (l_area.item (l_ending_index), l_starting_index); l_area.put (l_temp, l_ending_index) l_ending_index := l_ending_index - 1 l_starting_index := l_starting_index + 1 end end end append_integer_64 (i: INTEGER_64) -- Append the string representation of i at end. local l_value: INTEGER_64 l_starting_index, l_ending_index: INTEGER_32 l_temp: CHARACTER_32 l_area: like area do if i = 0 then append_character ('0'.to_character_32) else from l_starting_index := count if i < 0 then append_character ('-'.to_character_32) l_starting_index := l_starting_index + 1 if i = {INTEGER_64}.min_value then append_character ('8'.to_character_32) l_value := - (i // 10) else l_value := - i end else l_value := i end until l_value = 0 loop append_character ((l_value \\ 10 + 48).to_character_32) l_value := l_value // 10 end from l_ending_index := count - 1 l_area := area until l_starting_index >= l_ending_index loop l_temp := l_area.item (l_starting_index); l_area.put (l_area.item (l_ending_index), l_starting_index); l_area.put (l_temp, l_ending_index) l_ending_index := l_ending_index - 1 l_starting_index := l_starting_index + 1 end end end append_integer_8 (i: INTEGER_8) -- Append the string representation of i at end. local l_value: INTEGER_8 l_starting_index, l_ending_index: INTEGER_32 l_temp: CHARACTER_32 l_area: like area do if i = 0 then append_character ('0'.to_character_32) else from l_starting_index := count if i < 0 then append_character ('-'.to_character_32) l_starting_index := l_starting_index + 1 if i = {INTEGER_8}.min_value then append_character ('8'.to_character_32) l_value := - (i // 10) else l_value := - i end else l_value := i end until l_value = 0 loop append_character ((l_value \\ 10 + 48).to_character_32) l_value := l_value // 10 end from l_ending_index := count - 1 l_area := area until l_starting_index >= l_ending_index loop l_temp := l_area.item (l_starting_index); l_area.put (l_area.item (l_ending_index), l_starting_index); l_area.put (l_temp, l_ending_index) l_ending_index := l_ending_index - 1 l_starting_index := l_starting_index + 1 end end end append_natural_16 (i: NATURAL_16) -- Append the string representation of i at end. local l_value: NATURAL_16 l_starting_index, l_ending_index: INTEGER_32 l_temp: CHARACTER_32 l_area: like area do if i = 0 then append_character ('0'.to_character_32) else from l_starting_index := count l_value := i until l_value = 0 loop append_character ((l_value \\ 10 + 48).to_character_32) l_value := l_value // 10 end from l_ending_index := count - 1 l_area := area until l_starting_index >= l_ending_index loop l_temp := l_area.item (l_starting_index); l_area.put (l_area.item (l_ending_index), l_starting_index); l_area.put (l_temp, l_ending_index) l_ending_index := l_ending_index - 1 l_starting_index := l_starting_index + 1 end end end append_natural_32 (i: NATURAL_32) -- Append the string representation of i at end. local l_value: NATURAL_32 l_starting_index, l_ending_index: INTEGER_32 l_temp: CHARACTER_32 l_area: like area do if i = 0 then append_character ('0'.to_character_32) else from l_starting_index := count l_value := i until l_value = 0 loop append_character ((l_value \\ 10 + 48).to_character_32) l_value := l_value // 10 end from l_ending_index := count - 1 l_area := area until l_starting_index >= l_ending_index loop l_temp := l_area.item (l_starting_index); l_area.put (l_area.item (l_ending_index), l_starting_index); l_area.put (l_temp, l_ending_index) l_ending_index := l_ending_index - 1 l_starting_index := l_starting_index + 1 end end end append_natural_64 (i: NATURAL_64) -- Append the string representation of i at end. local l_value: NATURAL_64 l_starting_index, l_ending_index: INTEGER_32 l_temp: CHARACTER_32 l_area: like area do if i = 0 then append_character ('0'.to_character_32) else from l_starting_index := count l_value := i until l_value = 0 loop append_character ((l_value \\ 10 + 48).to_character_32) l_value := l_value // 10 end from l_ending_index := count - 1 l_area := area until l_starting_index >= l_ending_index loop l_temp := l_area.item (l_starting_index); l_area.put (l_area.item (l_ending_index), l_starting_index); l_area.put (l_temp, l_ending_index) l_ending_index := l_ending_index - 1 l_starting_index := l_starting_index + 1 end end end append_natural_8 (i: NATURAL_8) -- Append the string representation of i at end. local l_value: NATURAL_8 l_starting_index, l_ending_index: INTEGER_32 l_temp: CHARACTER_32 l_area: like area do if i = 0 then append_character ('0'.to_character_32) else from l_starting_index := count l_value := i until l_value = 0 loop append_character ((l_value \\ 10 + 48).to_character_32) l_value := l_value // 10 end from l_ending_index := count - 1 l_area := area until l_starting_index >= l_ending_index loop l_temp := l_area.item (l_starting_index); l_area.put (l_area.item (l_ending_index), l_starting_index); l_area.put (l_temp, l_ending_index) l_ending_index := l_ending_index - 1 l_starting_index := l_starting_index + 1 end end end append_real (r: REAL_32) -- Append the string representation of r at end. do append_string_general (r.out) end append_string (s: detachable READABLE_STRING_32) -- Append a copy of s, if not void, at end. do if s /= Void then append (s) end ensure appended: s /= Void implies (Elks_checking implies Current ~ (old twin + old s.twin)) end append_string_general (s: READABLE_STRING_GENERAL) -- Append characters of s at end. require -- from STRING_GENERAL argument_not_void: s /= Void compatible_strings: Is_string_8 implies s.is_valid_as_string_8 do if attached {READABLE_STRING_32} s as l_s32 then append (l_s32) else Precursor {STRING_GENERAL} (s) end ensure -- from STRING_GENERAL new_count: count = old count + old s.count appended: Elks_checking implies same_string_general (old (to_string_32 + s.as_string_32)) end append_substring_general (s: READABLE_STRING_GENERAL; start_index, end_index: INTEGER_32) -- Append characters of s.substring (start_index, end_index) at end. -- (from STRING_GENERAL) require -- from STRING_GENERAL argument_not_void: s /= Void compatible_strings: Is_string_8 implies s.is_valid_as_string_8 start_index_valid: start_index >= 1 end_index_valid: end_index <= s.count valid_bounds: start_index <= end_index + 1 local l_s_count, l_new_size: INTEGER_32 i: INTEGER_32 do l_s_count := end_index - start_index + 1 if l_s_count > 0 then l_new_size := l_s_count + count if l_new_size > capacity then resize (l_new_size) end from i := start_index until i > end_index loop append_code (s.code (i)) i := i + 1 end set_count (l_new_size) reset_hash_codes end ensure -- from STRING_GENERAL new_count: count = old count + end_index - start_index + 1 appended: Elks_checking implies same_string_general (old (to_string_32 + s.substring (start_index, end_index).as_string_32)) end append_substring (s: READABLE_STRING_32; start_index, end_index: INTEGER_32) -- Append characters of s.substring (start_index, end_index) at end. require argument_not_void: s /= Void start_index_valid: start_index >= 1 end_index_valid: end_index <= s.count valid_bounds: start_index <= end_index + 1 local l_count, l_s_count, l_new_size: INTEGER_32 do l_s_count := end_index - start_index + 1 if l_s_count > 0 then l_count := count l_new_size := l_s_count + l_count if l_new_size > capacity then resize (l_new_size + additional_space) end; area.copy_data (s.area, s.area_lower + start_index - 1, l_count, l_s_count) count := l_new_size reset_hash_codes end ensure new_count: count = old count + (end_index - start_index + 1) appended: Elks_checking implies same_string (old (Current + s.substring (start_index, end_index))) end extend (c: CHARACTER_32) -- Append c at end. -- Was declared in STRING_32 as synonym of append_character. require -- from COLLECTION extendible: Extendible local current_count: INTEGER_32 do current_count := count if current_count = capacity then resize (current_count + additional_space) end; area.put (c, current_count) count := current_count + 1 reset_hash_codes ensure -- from COLLECTION item_inserted: is_inserted (c) ensure then item_inserted: item (count) = c new_count: count = old count + 1 stable_before: Elks_checking implies substring (1, count - 1) ~ (old twin) end fill (other: CONTAINER [CHARACTER_32]) -- Fill with as many items of other as possible. -- The representations of other and current structure -- need not be the same. -- (from COLLECTION) require -- from COLLECTION other_not_void: other /= Void extendible: Extendible local lin_rep: LINEAR [CHARACTER_32] do lin_rep := other.linear_representation from lin_rep.start until not Extendible or else lin_rep.off loop extend (lin_rep.item); lin_rep.forth end end fill_blank -- Fill with capacity blank characters. do fill_character (' '.to_character_32) ensure filled: full same_size: (count = capacity) and (capacity = old capacity) end fill_character (c: CHARACTER_32) -- Fill with capacity characters all equal to c. -- (from READABLE_STRING_32) local l_cap: like capacity do l_cap := capacity if l_cap /= 0 then area.fill_with (c, 0, l_cap - 1) count := l_cap internal_hash_code := 0 end ensure -- from READABLE_STRING_32 filled: count = capacity same_size: capacity = old capacity end fill_with (c: CHARACTER_32) -- Replace every character with c. local l_count: INTEGER_32 do l_count := count if l_count /= 0 then area.fill_with (c, 0, l_count - 1) reset_hash_codes end ensure same_count: (count = old count) and (capacity = old capacity) filled: Elks_checking implies occurrences (c) = count end insert (s: READABLE_STRING_32; i: INTEGER_32) obsolete "ELKS 2001: use `insert_string' instead. [2017-05-31]" -- Add s to left of position i in current string. require string_exists: s /= Void index_small_enough: i <= count + 1 index_large_enough: i > 0 do insert_string (s, i) ensure inserted: Elks_checking implies (Current ~ (old substring (1, i - 1) + old (s.twin) + old substring (i, count))) end insert_character (c: CHARACTER_32; i: INTEGER_32) -- Insert c at index i, shifting characters between ranks -- i and count rightwards. require valid_insertion_index: 1 <= i and i <= count + 1 local pos, new_size: INTEGER_32 l_area: like area do new_size := 1 + count if new_size > capacity then resize (new_size + additional_space) end pos := i - 1 l_area := area; l_area.overlapping_move (pos, pos + 1, count - pos); l_area.put (c, pos) count := new_size reset_hash_codes ensure one_more_character: count = old count + 1 inserted: item (i) = c stable_before_i: Elks_checking implies substring (1, i - 1) ~ (old substring (1, i - 1)) stable_after_i: Elks_checking implies substring (i + 1, count) ~ (old substring (i, count)) end insert_string (s: READABLE_STRING_32; i: INTEGER_32) -- Insert s at index i, shifting characters between ranks -- i and count rightwards. require string_exists: s /= Void valid_insertion_index: 1 <= i and i <= count + 1 local pos, new_size: INTEGER_32 l_s_count: INTEGER_32 l_area: like area do l_s_count := s.count if l_s_count /= 0 then new_size := l_s_count + count if new_size > capacity then resize (new_size + additional_space) end l_area := area pos := i - 1; l_area.overlapping_move (pos, pos + l_s_count, count - pos); l_area.copy_data (s.area, s.area_lower, pos, l_s_count) count := new_size reset_hash_codes end ensure inserted: Elks_checking implies (Current ~ (old substring (1, i - 1) + old (s.twin) + old substring (i, count))) end keep_head (n: INTEGER_32) -- Remove all characters except for the first n; -- do nothing if n >= count. require -- from STRING_GENERAL non_negative_argument: n >= 0 do if n < count then count := n reset_hash_codes end ensure -- from STRING_GENERAL new_count: count = n.min (old count) kept: Elks_checking implies Current ~ (old substring (1, n.min (count))) end keep_tail (n: INTEGER_32) -- Remove all characters except for the last n; -- do nothing if n >= count. require -- from STRING_GENERAL non_negative_argument: n >= 0 local nb: like count do nb := count if n < nb then area.overlapping_move (nb - n, 0, n) count := n reset_hash_codes end ensure -- from STRING_GENERAL new_count: count = n.min (old count) kept: Elks_checking implies Current ~ (old substring (count - n.min (count) + 1, count)) end left_adjust -- Remove leading whitespace. local nb, nb_space: INTEGER_32 l_area: like area l_prop: like Character_properties do l_prop := Character_properties from nb := count - 1 l_area := area until nb_space > nb or else not l_prop.is_space (l_area.item (nb_space)) loop nb_space := nb_space + 1 end if nb_space > 0 then nb := nb + 1 - nb_space; l_area.overlapping_move (nb_space, 0, nb) count := nb reset_hash_codes end ensure -- from STRING_GENERAL valid_count: count <= old count new_count: not is_empty implies not item (1).is_space kept: Elks_checking implies Current ~ (old twin).substring (old count - count + 1, old count) only_spaces_removed_before: Elks_checking implies (old twin).is_substring_whitespace (1, (old twin).substring_index (Current, 1) - 1) end precede (c: CHARACTER_32) -- Add c at front. -- Was declared in STRING_32 as synonym of prepend_character. local l_area: like area do if count = capacity then resize (count + additional_space) end l_area := area; l_area.overlapping_move (0, 1, count); l_area.put (c, 0) count := count + 1 reset_hash_codes ensure new_count: count = old count + 1 end prepend (s: READABLE_STRING_32) -- Prepend characters of s at front. require argument_not_void: s /= Void do insert_string (s, 1) ensure new_count: count = old (count + s.count) inserted: Elks_checking implies same_string (old (s + Current)) end prepend_boolean (b: BOOLEAN) -- Prepend the string representation of b at front. do prepend_string_general (b.out) end prepend_character (c: CHARACTER_32) -- Add c at front. -- Was declared in STRING_32 as synonym of precede. local l_area: like area do if count = capacity then resize (count + additional_space) end l_area := area; l_area.overlapping_move (0, 1, count); l_area.put (c, 0) count := count + 1 reset_hash_codes ensure new_count: count = old count + 1 end prepend_double (d: REAL_64) -- Prepend the string representation of d at front. do prepend_string_general (d.out) end prepend_integer (i: INTEGER_32) -- Prepend the string representation of i at front. do prepend_string_general (i.out) end prepend_real (r: REAL_32) -- Prepend the string representation of r at front. do prepend_string_general (r.out) end prepend_string (s: detachable READABLE_STRING_32) -- Prepend characters of s, if not void, at front. do if s /= Void then prepend (s) end end prepend_string_general (s: READABLE_STRING_GENERAL) -- Prepend characters of s at front. require -- from STRING_GENERAL argument_not_void: s /= Void compatible_strings: Is_string_8 implies s.is_valid_as_string_8 do if attached {READABLE_STRING_32} s as l_s32 then prepend (l_s32) else Precursor {STRING_GENERAL} (s) end ensure -- from STRING_GENERAL new_count: count = old (count + s.count) inserted: Elks_checking implies same_string_general (old (s.to_string_32 + Current.as_string_32)) end prepend_substring (s: READABLE_STRING_32; start_index, end_index: INTEGER_32) -- Prepend characters of s.substring (start_index, end_index) at front. require argument_not_void: s /= Void start_index_valid: start_index >= 1 end_index_valid: end_index <= s.count valid_bounds: start_index <= end_index + 1 local new_size: INTEGER_32 l_s_count: INTEGER_32 l_area: like area do l_s_count := end_index - start_index + 1 if l_s_count > 0 then new_size := l_s_count + count if new_size > capacity then resize (new_size + additional_space) end l_area := area; l_area.overlapping_move (0, l_s_count, count); l_area.copy_data (s.area, s.area_lower + start_index - 1, 0, l_s_count) count := new_size reset_hash_codes end ensure new_count: count = old count + end_index - start_index + 1 inserted: Elks_checking implies same_string (old (s.substring (start_index, end_index) + Current)) end prepend_substring_general (s: READABLE_STRING_GENERAL; start_index, end_index: INTEGER_32) -- Prepend characters of s.substring (start_index, end_index) at front. -- (from STRING_GENERAL) require -- from STRING_GENERAL argument_not_void: s /= Void compatible_strings: Is_string_8 implies s.is_valid_as_string_8 start_index_valid: start_index >= 1 end_index_valid: end_index <= s.count valid_bounds: start_index <= end_index + 1 local l_count, l_s_count, l_new_size: INTEGER_32 i, j: INTEGER_32 do l_s_count := end_index - start_index + 1 if l_s_count > 0 then l_count := count l_new_size := l_s_count + l_count if l_new_size > capacity then resize (l_new_size) end set_count (l_new_size) from i := l_count until i = 0 loop put_code (code (i), i + l_s_count) i := i - 1 end from i := start_index j := 1 until i > end_index loop put_code (s.code (i), j) i := i + 1 j := j + 1 end reset_hash_codes end ensure -- from STRING_GENERAL new_count: count = old count + end_index - start_index + 1 inserted: Elks_checking implies same_string_general (old (s.substring (start_index, end_index).to_string_32 + Current.as_string_32)) end put (c: CHARACTER_32; i: INTEGER_32) -- Replace character at position i by c. require -- from TABLE valid_key: valid_index (i) require -- from TABLE valid_key: valid_index (i) require -- from TO_SPECIAL valid_index: valid_index (i) do area.put (c, i - 1) reset_hash_codes ensure -- from TABLE inserted: item (i) = c ensure -- from TO_SPECIAL inserted: item (i) = c ensure then stable_count: count = old count stable_before_i: Elks_checking implies substring (1, i - 1) ~ (old substring (1, i - 1)) stable_after_i: Elks_checking implies substring (i + 1, count) ~ (old substring (i + 1, count)) end put_code (v: NATURAL_32; i: INTEGER_32) -- Replace character at position i by character of code v. require -- from STRING_GENERAL valid_code: valid_code (v) valid_index: valid_index (i) do area.put (v.to_character_32, i - 1) reset_hash_codes ensure -- from STRING_GENERAL inserted: code (i) = v stable_count: count = old count stable_before_i: Elks_checking implies substring (1, i - 1) ~ (old substring (1, i - 1)) stable_after_i: Elks_checking implies substring (i + 1, count) ~ (old substring (i + 1, count)) end replace_blank -- Replace all current characters with blanks. do fill_with (' '.to_character_32) ensure same_size: (count = old count) and (capacity = old capacity) all_blank: Elks_checking implies occurrences (' '.to_character_32) = count end replace_character (c: CHARACTER_32) obsolete "ELKS 2001: use `fill_with' instead'. [2017-05-31]" -- Replace every character with c. do fill_with (c) ensure same_count: (count = old count) and (capacity = old capacity) filled: Elks_checking implies occurrences (c) = count end replace_substring (s: READABLE_STRING_32; start_index, end_index: INTEGER_32) -- Replace characters from start_index to end_index with s. require string_not_void: s /= Void valid_start_index: 1 <= start_index valid_end_index: end_index <= count meaningfull_interval: start_index <= end_index + 1 local new_size: INTEGER_32 diff: INTEGER_32 l_area: like area s_count: INTEGER_32 old_count: INTEGER_32 do s_count := s.count old_count := count diff := s_count - (end_index - start_index + 1) new_size := diff + old_count if diff > 0 then grow (new_size) end l_area := area if diff /= 0 then l_area.overlapping_move (end_index, end_index + diff, old_count - end_index) end set_count (new_size); l_area.copy_data (s.area, s.area_lower, start_index - 1, s_count) ensure new_count: count = old count + old s.count - end_index + start_index - 1 replaced: Elks_checking implies (Current ~ (old (substring (1, start_index - 1) + s + substring (end_index + 1, count)))) end replace_substring_all (original, new: READABLE_STRING_32) -- Replace every occurrence of original with new. require original_exists: original /= Void new_exists: new /= Void original_not_empty: not original.is_empty local l_first_pos, l_next_pos: INTEGER_32 l_orig_count, l_new_count, l_new_lower, l_count, i, l_index_count: INTEGER_32 l_src_index, l_dest_index, l_prev_index, l_copy_delta: INTEGER_32 l_area, l_new_area: like area l_offset: INTEGER_32 l_string_searcher: like String_searcher l_index_list: SPECIAL [INTEGER_32] do if not is_empty then l_count := count l_string_searcher := String_searcher; l_string_searcher.initialize_deltas (original) l_orig_count := original.count l_new_count := new.count if l_orig_count >= l_new_count then l_first_pos := l_string_searcher.substring_index_with_deltas (Current, original, 1, l_count) if l_first_pos > 0 then if l_orig_count = l_new_count then from l_area := area l_new_area := new.area l_new_lower := new.area_lower until l_first_pos = 0 loop l_area.copy_data (l_new_area, l_new_lower, l_first_pos - 1, l_new_count) if l_first_pos + l_new_count <= l_count then l_first_pos := l_string_searcher.substring_index_with_deltas (Current, original, l_first_pos + l_new_count, l_count) else l_first_pos := 0 end end elseif l_orig_count > l_new_count then from l_next_pos := l_string_searcher.substring_index_with_deltas (Current, original, l_first_pos + l_orig_count, l_count) l_area := area l_new_area := new.area l_new_lower := new.area_lower until l_next_pos = 0 loop l_area.copy_data (l_new_area, l_new_lower, l_first_pos - 1 - l_offset, l_new_count); l_area.overlapping_move (l_first_pos + l_orig_count - 1, l_first_pos + l_new_count - 1 - l_offset, l_next_pos - l_first_pos - l_orig_count) l_first_pos := l_next_pos l_offset := l_offset + (l_orig_count - l_new_count) if l_first_pos + l_new_count <= l_count then l_next_pos := l_string_searcher.substring_index_with_deltas (Current, original, l_first_pos + l_orig_count, l_count) else l_next_pos := 0 end end; l_area.copy_data (l_new_area, l_new_lower, l_first_pos - 1 - l_offset, l_new_count); l_area.overlapping_move (l_first_pos + l_orig_count - 1, l_first_pos + l_new_count - 1 - l_offset, l_count + 1 - l_first_pos - l_orig_count) l_offset := l_offset + (l_orig_count - l_new_count) set_count (l_count - l_offset) end reset_hash_codes end elseif attached l_string_searcher.substring_index_list_with_deltas (Current, original, 1, l_count) as l_list then l_index_list := l_list.area l_index_count := l_index_list.count l_prev_index := l_count l_copy_delta := l_new_count - l_orig_count l_count := l_count + (l_index_count * l_copy_delta) l_area := area.resized_area_with_default ('%U'.to_character_32, l_count + 1) area := l_area from i := l_index_count l_new_lower := new.area_lower l_new_area := new.area until i = 0 loop i := i - 1 l_src_index := l_index_list.item (i) l_dest_index := l_src_index + i * l_copy_delta; l_area.overlapping_move (l_src_index + l_orig_count - 1, l_dest_index + l_new_count - 1, l_prev_index - l_src_index - l_orig_count + 1) l_prev_index := l_src_index - 1; l_area.copy_data (l_new_area, l_new_lower, l_dest_index - 1, l_new_count) end set_count (l_count) end end end right_adjust -- Remove trailing whitespace. local i, nb: INTEGER_32 nb_space: INTEGER_32 l_area: like area c: CHARACTER_32 l_prop: like Character_properties do l_prop := Character_properties from nb := count - 1 i := nb l_area := area until i < 0 loop c := l_area.item (i) if not l_prop.is_space (c) then i := -1 else nb_space := nb_space + 1 i := i - 1 end end if nb_space > 0 then count := nb + 1 - nb_space reset_hash_codes end ensure -- from STRING_GENERAL valid_count: count <= old count new_count: not is_empty implies not item (count).is_space kept: Elks_checking implies Current ~ (old twin).substring (1, count) only_spaces_removed_after: Elks_checking implies (old twin).is_substring_whitespace ((old twin).substring_index (Current, 1) + count, old count) end set (t: READABLE_STRING_32; n1, n2: INTEGER_32) -- Set current string to substring of t from indices n1 -- to n2, or to empty string if no such substring. require argument_not_void: t /= Void local s: READABLE_STRING_32 do s := t.substring (n1, n2) area := s.area count := s.count reset_hash_codes ensure is_substring: same_string (t.substring (n1, n2)) end share (other: STRING_32) -- Make current string share the text of other. -- Subsequent changes to the characters of current string -- will also affect other, and conversely. require argument_not_void: other /= Void do area := other.area count := other.count reset_hash_codes ensure shared_count: other.count = count shared_area: other.area = area end subcopy (other: READABLE_STRING_32; start_pos, end_pos, index_pos: INTEGER_32) -- Copy characters of other within bounds start_pos and -- end_pos to current string starting at index index_pos. require other_not_void: other /= Void valid_start_pos: other.valid_index (start_pos) valid_end_pos: other.valid_index (end_pos) valid_bounds: start_pos <= end_pos or start_pos = end_pos + 1 valid_index_pos: valid_index (index_pos) enough_space: count - index_pos >= end_pos - start_pos local l_other_area, l_area: like area do if end_pos >= start_pos then l_other_area := other.area l_area := area if l_area = l_other_area then l_area.overlapping_move (start_pos - 1, index_pos - 1, end_pos - start_pos + 1) else l_area.copy_data (l_other_area, start_pos - 1, index_pos - 1, end_pos - start_pos + 1) end reset_hash_codes end ensure same_count: count = old count copied: Elks_checking implies (Current ~ (old substring (1, index_pos - 1) + old other.substring (start_pos, end_pos) + old substring (index_pos + (end_pos - start_pos + 1), count))) end feature {NONE} -- Element change set_area (other: like area) -- Make other the new area. -- (from TO_SPECIAL) do area := other ensure -- from TO_SPECIAL area_set: area = other end feature -- Removal clear_all obsolete "Use `wipe_out' instead. [2017-05-31]" -- Reset all characters. do count := 0 reset_hash_codes ensure is_empty: count = 0 same_capacity: capacity = old capacity end prune (c: CHARACTER_32) -- Remove first occurrence of c, if any. require -- from COLLECTION prunable: prunable require else True local counter: INTEGER_32 do from counter := 1 until counter > count or else (item (counter) = c) loop counter := counter + 1 end if counter <= count then remove (counter) end end prune_all (c: CHARACTER_32) -- Remove all occurrences of c. require -- from COLLECTION prunable: prunable require else True local i, j, nb: INTEGER_32 l_area: like area l_char: CHARACTER_32 do from l_area := area nb := count until i = nb loop l_char := l_area.item (i) if l_char /= c then l_area.put (l_char, j) j := j + 1 end i := i + 1 end count := j reset_hash_codes ensure -- from COLLECTION no_more_occurrences: not has (c) ensure then changed_count: count = (old count) - (old occurrences (c)) end prune_all_leading (c: CHARACTER_32) -- Remove all leading occurrences of c. do from until is_empty or else item (1) /= c loop remove (1) end end prune_all_trailing (c: CHARACTER_32) -- Remove all trailing occurrences of c. do from until is_empty or else item (count) /= c loop remove (count) end end remove (i: INTEGER_32) -- Remove i-th character. require -- from STRING_GENERAL valid_index: valid_index (i) require -- from DYNAMIC_TABLE prunable: prunable valid_key: valid_index (i) local l_count: INTEGER_32 do l_count := count; area.overlapping_move (i, i - 1, l_count - i) count := l_count - 1 reset_hash_codes ensure -- from STRING_GENERAL new_count: count = old count - 1 removed: Elks_checking implies to_string_32 ~ (old substring (1, i - 1).to_string_32 + old substring (i + 1, count).to_string_32) end remove_head (n: INTEGER_32) -- Remove first n characters; -- if n > count, remove all. require -- from STRING_GENERAL n_non_negative: n >= 0 do if n > count then count := 0 reset_hash_codes else keep_tail (count - n) end ensure -- from STRING_GENERAL removed: Elks_checking implies Current ~ (old substring (n.min (count) + 1, count)) end remove_substring (start_index, end_index: INTEGER_32) -- Remove all characters from start_index -- to end_index inclusive. require -- from STRING_GENERAL valid_start_index: 1 <= start_index valid_end_index: end_index <= count meaningful_interval: start_index <= end_index + 1 local l_count, nb_removed: INTEGER_32 do nb_removed := end_index - start_index + 1 if nb_removed > 0 then l_count := count; area.overlapping_move (start_index + nb_removed - 1, start_index - 1, l_count - end_index) count := l_count - nb_removed reset_hash_codes end ensure -- from STRING_GENERAL removed: Elks_checking implies Current.as_string_32 ~ (old substring (1, start_index - 1).as_string_32 + old substring (end_index + 1, count).as_string_32) end remove_tail (n: INTEGER_32) -- Remove last n characters; -- if n > count, remove all. require -- from STRING_GENERAL n_non_negative: n >= 0 local l_count: INTEGER_32 do l_count := count if n > l_count then count := 0 reset_hash_codes else keep_head (l_count - n) end ensure -- from STRING_GENERAL removed: Elks_checking implies Current ~ (old substring (1, count - n.min (count))) end wipe_out -- Remove all characters. require -- from STRING_GENERAL True require -- from COLLECTION prunable: prunable do count := 0 reset_hash_codes ensure -- from STRING_GENERAL is_empty: count = 0 same_capacity: capacity = old capacity ensure -- from COLLECTION wiped_out: is_empty end feature -- Resizing adapt_size -- Adapt the size to accommodate count characters. do resize (count) end automatic_grow -- Change the capacity to accommodate at least -- Growth_percentage more items. -- (from RESIZABLE) require -- from RESIZABLE resizable: resizable do grow (capacity + additional_space) ensure -- from RESIZABLE increased_capacity: capacity >= old capacity + old additional_space end grow (newsize: INTEGER_32) -- Ensure that the capacity is at least newsize. require -- from RESIZABLE resizable: resizable do if newsize > capacity then resize (newsize) end ensure -- from RESIZABLE new_capacity: capacity >= newsize end resize (newsize: INTEGER_32) -- Rearrange string so that it can accommodate -- at least newsize characters. -- Do not lose any previously entered character. require -- from STRING_GENERAL new_size_large_enough: newsize >= count do area := area.aliased_resized_area_with_default ('%U'.to_character_32, newsize + 1) ensure -- from STRING_GENERAL same_count: count = old count capacity_large_enough: capacity >= newsize same_content: Elks_checking implies same_string_general (old twin) end trim -- Decrease capacity to the minimum value. -- Apply to reduce allocated storage. require -- from RESIZABLE True local n: like count do n := count if n < capacity then area := area.aliased_resized_area (n + 1) end ensure -- from RESIZABLE same_count: count = old count minimal_capacity: capacity = count ensure then same_string: same_string (old twin) end feature -- Transformation correct_mismatch -- Attempt to correct object mismatch during retrieve using Mismatch_information. do if area = Void and then attached {like area} Mismatch_information.item ("area") as l_area then area := l_area end end feature -- Conversion as_lower: like Current -- New object with all letters in lower case. do Result := twin; Result.to_lower ensure -- from READABLE_STRING_GENERAL as_lower_attached: Result /= Void length: Result.count = count anchor: count > 0 implies Result.item (1) = item (1).as_lower recurse: count > 1 implies Result.substring (2, count) ~ substring (2, count).as_lower end as_readable_string_32: READABLE_STRING_32 obsolete "Use explicit conversion `to_string_32`, or, better use READABLE_STRING_32 and descendants instead. [2017-05-31]" -- Equivalent to as_string_32 with a different name. -- (from READABLE_STRING_GENERAL) do Result := as_string_32 end as_readable_string_8: READABLE_STRING_8 obsolete "Use explicit conversion `to_string_8' with a test that the string is made of ASCII characters only. [2017-05-31]" -- Convert Current as a READABLE_STRING_8. If a code of Current is -- not a valid code for a READABLE_STRING_8 it is replaced with the null -- character. -- (from READABLE_STRING_GENERAL) do Result := as_string_8 end as_string_32: STRING_32 -- Convert Current as a STRING_32. -- Was declared in READABLE_STRING_GENERAL as synonym of to_string_32. -- (from READABLE_STRING_GENERAL) local i, nb: INTEGER_32 do if attached {STRING_32} Current as l_result then Result := l_result else nb := count create Result.make (nb); Result.set_count (nb) from i := 1 until i > nb loop Result.put_code (code (i), i) i := i + 1 end end ensure -- from READABLE_STRING_GENERAL as_string_32_not_void: Result /= Void identity: (conforms_to (create {STRING_32}.make_empty) and Result = Current) or (not conforms_to (create {STRING_32}.make_empty) and Result /= Current) end as_string_32_conversion: STRING_32 obsolete "Update target of call to use READABLE_STRING_32 and descendants instead. [2017-05-31]" -- Equivalent to as_string_32 with a different name. -- To be used for migrating existing code to Unicode -- when you get a compiler error but cannot or do not have -- the time yet to address the source of the string to be -- a READABLE_STRING_32 or descendants. -- (from READABLE_STRING_GENERAL) do Result := as_string_32 end as_string_8: STRING_8 obsolete "[ For 32-bit strings: - use explicit conversion `to_string_8` with a test that the string is made of ASCII characters only. For 8-bit strings: - consider changing the type of reattachmanet target to READABLE_STRING_8 or - use explicit conversion `to_string_8` to avoid implicit performance penalty. [2019-11-30] ]" -- Convert Current as a STRING_8. If a code of Current is -- not a valid code for a STRING_8 it is replaced with the null -- character. -- (from READABLE_STRING_GENERAL) local i, nb: INTEGER_32 l_code: like code do if attached {STRING_8} Current as l_result then Result := l_result else nb := count create Result.make (nb); Result.set_count (nb) from i := 1 until i > nb loop l_code := code (i) if Result.valid_code (l_code) then Result.put_code (l_code, i) else Result.put_code (0, i) end i := i + 1 end end ensure -- from READABLE_STRING_GENERAL as_string_8_not_void: Result /= Void identity: (conforms_to ("") and Result = Current) or (not conforms_to ("") and Result /= Current) end as_string_8_conversion: STRING_8 obsolete "Update recipient of call to use READABLE_STRING_32 and descendants instead. [2017-05-31]" -- Equivalent to as_string_8 with a different name. -- To be used for migrating existing code to Unicode -- when you get a compiler error but cannot or do not have -- the time yet to address the target recipient of the string to be -- a READABLE_STRING_32 or descendants. -- (from READABLE_STRING_GENERAL) do Result := as_string_8 end as_upper: like Current -- New object with all letters in upper case do Result := twin; Result.to_upper ensure -- from READABLE_STRING_GENERAL as_upper_attached: Result /= Void length: Result.count = count anchor: count > 0 implies Result.item (1) = item (1).as_upper recurse: count > 1 implies Result.substring (2, count) ~ substring (2, count).as_upper end center_justify -- Center justify Current using count as width. local i, nb, l_offset: INTEGER_32 left_nb_space, right_nb_space: INTEGER_32 l_area: like area l_prop: like Character_properties do l_prop := Character_properties from nb := count l_area := area until left_nb_space = nb or else not l_prop.is_space (l_area.item (left_nb_space)) loop left_nb_space := left_nb_space + 1 end from i := nb - 1 l_area := area until i = -1 or else not l_prop.is_space (l_area.item (i)) loop right_nb_space := right_nb_space + 1 i := i - 1 end l_offset := left_nb_space + right_nb_space if l_offset \\ 2 = 0 then l_offset := left_nb_space - l_offset // 2 else l_offset := left_nb_space - l_offset // 2 - 1 end if l_offset /= 0 then l_area.move_data (left_nb_space, left_nb_space - l_offset, nb - left_nb_space - right_nb_space) if l_offset < 0 then l_area.fill_with (' '.to_character_32, left_nb_space, left_nb_space - l_offset - 1) else l_area.fill_with (' '.to_character_32, nb - right_nb_space - l_offset, nb - 1) end reset_hash_codes end end character_justify (pivot: CHARACTER_32; position: INTEGER_32) -- Justify a string based on a pivot -- and the position it needs to be in -- the final string. -- This will grow the string if necessary -- to get the pivot in the correct place. require valid_position: position <= capacity positive_position: position >= 1 pivot_not_space: pivot /= ' '.to_character_32 not_empty: not is_empty local l_index_of_pivot, l_new_size: INTEGER_32 l_area: like area do l_index_of_pivot := index_of (pivot, 1) if l_index_of_pivot /= 0 then if l_index_of_pivot < position then l_new_size := count + position - l_index_of_pivot grow (l_new_size) l_area := area; l_area.move_data (0, position - l_index_of_pivot, count); l_area.fill_with (' '.to_character_32, 0, position - l_index_of_pivot - 1) count := l_new_size else l_area := area; l_area.move_data (l_index_of_pivot - position, 0, count - l_index_of_pivot + position); l_area.fill_with (' '.to_character_32, count - l_index_of_pivot + position, count - 1) end reset_hash_codes end end left_justify -- Left justify Current using count as witdth. local i, nb: INTEGER_32 l_area: like area do nb := count left_adjust i := count if i < nb then from l_area := area until i = nb loop l_area.put (' '.to_character_32, i) i := i + 1 end count := nb reset_hash_codes end end linear_representation: LINEAR [CHARACTER_32] -- Representation as a linear structure local temp: ARRAYED_LIST [CHARACTER_32] i: INTEGER_32 do create temp.make (capacity) from i := 1 until i > count loop temp.extend (item (i)) i := i + 1 end Result := temp end mirror -- Reverse the order of characters. -- "Hello world" -> "dlrow olleH". local a: like area c: CHARACTER_32 i, j: INTEGER_32 do if count > 0 then from i := count - 1 a := area until i <= j loop c := a.item (i); a.put (a.item (j), i); a.put (c, j) i := i - 1 j := j + 1 end reset_hash_codes end ensure same_count: count = old count end mirrored: like Current -- Mirror image of string; -- Result for "Hello world" is "dlrow olleH". do Result := twin if count > 0 then Result.mirror end ensure -- from READABLE_STRING_32 same_count: Result.count = count end right_justify -- Right justify Current using count as width. local i, nb: INTEGER_32 nb_space: INTEGER_32 l_area: like area do nb := count right_adjust i := count nb_space := nb - i if nb_space > 0 then from l_area := area variant i + 1 until i = 0 loop i := i - 1; l_area.put (l_area.item (i), i + nb_space) end from variant nb_space + 1 until nb_space = 0 loop nb_space := nb_space - 1; l_area.put (' '.to_character_32, nb_space) end count := nb reset_hash_codes end ensure same_count: count = old count end split (a_separator: CHARACTER_32): LIST [STRING_32] -- Split on a_separator. -- (from READABLE_STRING_GENERAL) local l_list: ARRAYED_LIST [STRING_32] i, j, c: INTEGER_32 do c := count create l_list.make (c + 1) if c > 0 then from i := 1 until i > c loop j := index_of (a_separator, i) if j = 0 then j := c + 1 end; l_list.extend (substring (i, j - 1)) i := j + 1 end if j = c then check last_character_is_a_separator: item (j) = a_separator end; l_list.extend (new_string (0)) end else l_list.extend (new_string (0)) end Result := l_list check l_list.count = occurrences (a_separator) + 1 end ensure -- from READABLE_STRING_GENERAL Result /= Void end to_boolean: BOOLEAN -- Boolean value; -- "True" yields True, "False" yields False -- (case-insensitive) -- (from READABLE_STRING_GENERAL) require -- from READABLE_STRING_GENERAL is_boolean: is_boolean do check True_constant.count = 4 end if count = 4 then Result := True end ensure -- from READABLE_STRING_GENERAL to_boolean: (Result = as_lower.same_string_general (True_constant)) or (not Result = as_lower.same_string_general (False_constant)) end frozen to_c: ANY -- A reference to a C form of current string. -- Useful only for interfacing with C software. require not_is_dotnet: not {PLATFORM}.is_dotnet local l_area: like area do l_area := area; l_area.put ('%U'.to_character_32, count) Result := l_area end frozen to_cil: SYSTEM_STRING -- Create an instance of SYSTEM_STRING using characters -- of Current between indices 1 and count. -- (from READABLE_STRING_GENERAL) require -- from READABLE_STRING_GENERAL is_dotnet: {PLATFORM}.is_dotnet do Result := Dotnet_convertor.from_string_to_system_string (Current) ensure -- from READABLE_STRING_GENERAL to_cil_not_void: Result /= Void end to_double: REAL_64 -- "Double" value; -- for example, when applied to "123.0", will yield 123.0 (double) -- Was declared in READABLE_STRING_GENERAL as synonym of to_real_64. -- (from READABLE_STRING_GENERAL) require -- from READABLE_STRING_GENERAL represents_a_double: is_double local l_convertor: like Ctor_convertor do l_convertor := Ctor_convertor; l_convertor.parse_string_with_type (Current, {NUMERIC_INFORMATION}.type_no_limitation) Result := l_convertor.parsed_double end to_integer: INTEGER_32 -- 32-bit integer value -- Was declared in READABLE_STRING_GENERAL as synonym of to_integer_32. -- (from READABLE_STRING_GENERAL) require -- from READABLE_STRING_GENERAL is_integer: is_integer_32 local l_convertor: like Ctoi_convertor do l_convertor := Ctoi_convertor; l_convertor.parse_string_with_type (Current, {NUMERIC_INFORMATION}.type_no_limitation) Result := l_convertor.parsed_integer end to_integer_16: INTEGER_16 -- 16-bit integer value -- (from READABLE_STRING_GENERAL) require -- from READABLE_STRING_GENERAL is_integer_16: is_integer_16 local l_convertor: like Ctoi_convertor do l_convertor := Ctoi_convertor; l_convertor.parse_string_with_type (Current, {NUMERIC_INFORMATION}.type_no_limitation) Result := l_convertor.parsed_integer_16 end to_integer_32: INTEGER_32 -- 32-bit integer value -- Was declared in READABLE_STRING_GENERAL as synonym of to_integer. -- (from READABLE_STRING_GENERAL) require -- from READABLE_STRING_GENERAL is_integer: is_integer_32 local l_convertor: like Ctoi_convertor do l_convertor := Ctoi_convertor; l_convertor.parse_string_with_type (Current, {NUMERIC_INFORMATION}.type_no_limitation) Result := l_convertor.parsed_integer end to_integer_64: INTEGER_64 -- 64-bit integer value -- (from READABLE_STRING_GENERAL) require -- from READABLE_STRING_GENERAL is_integer_64: is_integer_64 local l_convertor: like Ctoi_convertor do l_convertor := Ctoi_convertor; l_convertor.parse_string_with_type (Current, {NUMERIC_INFORMATION}.type_no_limitation) Result := l_convertor.parsed_integer_64 end to_integer_8: INTEGER_8 -- 8-bit integer value -- (from READABLE_STRING_GENERAL) require -- from READABLE_STRING_GENERAL is_integer_8: is_integer_8 local l_convertor: like Ctoi_convertor do l_convertor := Ctoi_convertor; l_convertor.parse_string_with_type (Current, {NUMERIC_INFORMATION}.type_no_limitation) Result := l_convertor.parsed_integer_8 end to_lower -- Convert to lower case. do to_lower_area (area, 0, count - 1) reset_hash_codes ensure length_and_content: Elks_checking implies Current ~ (old as_lower) end to_natural: NATURAL_32 -- 32-bit natural value -- Was declared in READABLE_STRING_GENERAL as synonym of to_natural_32. -- (from READABLE_STRING_GENERAL) require -- from READABLE_STRING_GENERAL is_natural: is_natural_32 local l_convertor: like Ctoi_convertor do l_convertor := Ctoi_convertor; l_convertor.parse_string_with_type (Current, {NUMERIC_INFORMATION}.type_no_limitation) Result := l_convertor.parsed_natural_32 end to_natural_16: NATURAL_16 -- 16-bit natural value -- (from READABLE_STRING_GENERAL) require -- from READABLE_STRING_GENERAL is_natural_16: is_natural_16 local l_convertor: like Ctoi_convertor do l_convertor := Ctoi_convertor; l_convertor.parse_string_with_type (Current, {NUMERIC_INFORMATION}.type_no_limitation) Result := l_convertor.parsed_natural_16 end to_natural_32: NATURAL_32 -- 32-bit natural value -- Was declared in READABLE_STRING_GENERAL as synonym of to_natural. -- (from READABLE_STRING_GENERAL) require -- from READABLE_STRING_GENERAL is_natural: is_natural_32 local l_convertor: like Ctoi_convertor do l_convertor := Ctoi_convertor; l_convertor.parse_string_with_type (Current, {NUMERIC_INFORMATION}.type_no_limitation) Result := l_convertor.parsed_natural_32 end to_natural_64: NATURAL_64 -- 64-bit natural value -- (from READABLE_STRING_GENERAL) require -- from READABLE_STRING_GENERAL is_natural_64: is_natural_64 local l_convertor: like Ctoi_convertor do l_convertor := Ctoi_convertor; l_convertor.parse_string_with_type (Current, {NUMERIC_INFORMATION}.type_no_limitation) Result := l_convertor.parsed_natural_64 end to_natural_8: NATURAL_8 -- 8-bit natural value -- (from READABLE_STRING_GENERAL) require -- from READABLE_STRING_GENERAL is_natural_8: is_natural_8 local l_convertor: like Ctoi_convertor do l_convertor := Ctoi_convertor; l_convertor.parse_string_with_type (Current, {NUMERIC_INFORMATION}.type_no_limitation) Result := l_convertor.parsed_natural_8 end to_real: REAL_32 -- Real value; -- for example, when applied to "123.0", will yield 123.0 -- Was declared in READABLE_STRING_GENERAL as synonym of to_real_32. -- (from READABLE_STRING_GENERAL) require -- from READABLE_STRING_GENERAL represents_a_real: is_real do Result := to_double.truncated_to_real end to_real_32: REAL_32 -- Real value; -- for example, when applied to "123.0", will yield 123.0 -- Was declared in READABLE_STRING_GENERAL as synonym of to_real. -- (from READABLE_STRING_GENERAL) require -- from READABLE_STRING_GENERAL represents_a_real: is_real do Result := to_double.truncated_to_real end to_real_64: REAL_64 -- "Double" value; -- for example, when applied to "123.0", will yield 123.0 (double) -- Was declared in READABLE_STRING_GENERAL as synonym of to_double. -- (from READABLE_STRING_GENERAL) require -- from READABLE_STRING_GENERAL represents_a_double: is_double local l_convertor: like Ctor_convertor do l_convertor := Ctor_convertor; l_convertor.parse_string_with_type (Current, {NUMERIC_INFORMATION}.type_no_limitation) Result := l_convertor.parsed_double end to_string_32: STRING_32 -- Convert Current as a STRING_32. -- Was declared in READABLE_STRING_GENERAL as synonym of as_string_32. -- (from READABLE_STRING_GENERAL) local i, nb: INTEGER_32 do if attached {STRING_32} Current as l_result then Result := l_result else nb := count create Result.make (nb); Result.set_count (nb) from i := 1 until i > nb loop Result.put_code (code (i), i) i := i + 1 end end ensure -- from READABLE_STRING_GENERAL as_string_32_not_void: Result /= Void identity: (conforms_to (create {STRING_32}.make_empty) and Result = Current) or (not conforms_to (create {STRING_32}.make_empty) and Result /= Current) end to_string_8: STRING_8 -- Convert Current as a STRING_8. -- (from READABLE_STRING_GENERAL) require -- from READABLE_STRING_GENERAL is_valid_as_string_8: is_valid_as_string_8 local i, nb: INTEGER_32 do if attached {STRING_8} Current as s then Result := s else nb := count create Result.make (nb); Result.set_count (nb) from i := 1 until i > nb loop check from_precondition: Result.valid_code (code (i)) end; Result.put_code (code (i), i) i := i + 1 end end ensure -- from READABLE_STRING_GENERAL as_string_8_not_void: Result /= Void identity: (conforms_to ("") and Result = Current) or (not conforms_to ("") and Result /= Current) end to_upper -- Convert to upper case. do to_upper_area (area, 0, count - 1) reset_hash_codes ensure length_and_content: Elks_checking implies Current ~ (old as_upper) 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: STRING_32) -- Reinitialize by copying the characters of other. -- (This is also used by twin.) -- (from READABLE_STRING_32) require -- from ANY other_not_void: other /= Void type_identity: same_type (other) local old_area: like area do if other /= Current then old_area := area standard_copy (other) if old_area = Void or else old_area = other.area or else old_area.count <= count then area := area.resized_area (count + 1) else old_area.copy_data (area, 0, 0, count) area := old_area end internal_hash_code := 0 end ensure -- from ANY is_equal: Current ~ other ensure then -- from READABLE_STRING_32 new_result_count: count = other.count 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: STRING_32) -- 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: STRING_32 -- 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 head (n: INTEGER_32): STRING_32 -- Prefix, retaining first n characters (or as many as available). -- (from READABLE_STRING_GENERAL) require -- from READABLE_STRING_GENERAL non_negative_argument: n >= 0 do if n > count then Result := twin else Result := substring (1, n) end ensure -- from READABLE_STRING_GENERAL same_count: count = old count new_count: Result.count = n.min (count) end multiply (n: INTEGER_32) -- Duplicate a string within itself -- ("hello").multiply(3) => "hellohellohello" require meaningful_multiplier: n >= 1 local s: like Current i: INTEGER_32 do s := twin grow (n * count) from i := n until i = 1 loop append (s) i := i - 1 end 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: STRING_32) -- 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: STRING_32 -- 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 substring (start_index, end_index: INTEGER_32): like Current -- Copy of substring containing all characters at indices -- between start_index and end_index require -- from READABLE_STRING_GENERAL True do if (1 <= start_index) and (start_index <= end_index) and (end_index <= count) then Result := new_string (end_index - start_index + 1); Result.area.copy_data (area, start_index - 1, 0, end_index - start_index + 1); Result.set_count (end_index - start_index + 1) else Result := new_string (0) end ensure -- from READABLE_STRING_GENERAL substring_not_void: Result /= Void substring_count: Result.count = end_index - start_index + 1 or Result.count = 0 first_code: Result.count > 0 implies Result.item (1) = item (start_index) recurse: Result.count > 0 implies Result.substring (2, Result.count) ~ substring (start_index + 1, end_index) end tail (n: INTEGER_32): STRING_32 -- Suffix, retaining last n characters (or as many as available). -- (from READABLE_STRING_GENERAL) require -- from READABLE_STRING_GENERAL non_negative_argument: n >= 0 do if n > count then Result := twin else Result := substring (count - n + 1, count) end ensure -- from READABLE_STRING_GENERAL same_count: count = old count new_count: Result.count = n.min (count) end frozen twin: STRING_32 -- 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 STRING_32 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 STRING_32 -- 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 plus alias "+" (s: READABLE_STRING_32): like Current -- Concatenation with s. require -- from READABLE_STRING_32 argument_attached: attached s do Result := new_string (count + s.count); Result.append (Current); Result.append (s) ensure -- from READABLE_STRING_32 plus_attached: attached Result new_count: Result.count = count + s.count initial: Elks_checking implies Result.substring (1, count) ~ Current final: Elks_checking implies Result.substring (count + 1, count + s.count).same_string (s) end plus_general (s: READABLE_STRING_GENERAL): like Current -- Concatenation of the current string with s. require -- from READABLE_STRING_GENERAL argument_not_void: s /= Void compatible_strings: Is_string_8 implies s.is_valid_as_string_8 do Result := new_string (count + s.count); Result.append (Current); Result.append_string_general (s) ensure -- from READABLE_STRING_GENERAL plus_not_void: Result /= Void new_count: Result.count = count + s.count initial: Elks_checking implies Result.substring (1, count) ~ Current final: Elks_checking implies Result.substring (count + 1, count + s.count).same_string_general (s) end feature -- Inapplicable bag_put (v: CHARACTER_32) -- Ensure that structure includes v. -- (from TABLE) require -- from COLLECTION extendible: Extendible do ensure -- from COLLECTION item_inserted: is_inserted (v) end feature {STRING_HANDLER}{STRING_HANDLER} -- Implementation frozen set_count (number: INTEGER_32) -- Set count to number of characters. require -- from STRING_GENERAL valid_count: 0 <= number and number <= capacity do count := number reset_hash_codes ensure -- from STRING_GENERAL new_count: count = number end feature {NONE} -- Implementation C_string_provider: C_STRING -- To create Eiffel strings from C string. -- (from READABLE_STRING_GENERAL) once create Result.make_empty (0) ensure -- from READABLE_STRING_GENERAL c_string_provider_not_void: Result /= Void end Character_properties: CHARACTER_PROPERTY -- Access to Unicode character properties -- (from READABLE_STRING_GENERAL) once create Result.make end Ctoi_convertor: STRING_TO_INTEGER_CONVERTOR -- Convertor used to convert string to integer or natural -- (from READABLE_STRING_GENERAL) once create Result.make; Result.set_leading_separators (" "); Result.set_trailing_separators (" "); Result.set_leading_separators_acceptable (True); Result.set_trailing_separators_acceptable (True) ensure -- from READABLE_STRING_GENERAL ctoi_convertor_not_void: Result /= Void end Ctor_convertor: STRING_TO_REAL_CONVERTOR -- Convertor used to convert string to real or double -- (from READABLE_STRING_GENERAL) once create Result.make; Result.set_leading_separators (" "); Result.set_trailing_separators (" "); Result.set_leading_separators_acceptable (True); Result.set_trailing_separators_acceptable (True) ensure -- from READABLE_STRING_GENERAL ctor_convertor_not_void: Result /= Void end Dotnet_convertor: SYSTEM_STRING_FACTORY -- Convertor used to convert from and to SYSTEM_STRING. -- (from READABLE_STRING_GENERAL) once create Result ensure -- from READABLE_STRING_GENERAL dotnet_convertor_not_void: Result /= Void end is_valid_integer_or_natural (type: INTEGER_32): BOOLEAN -- Is Current a valid number according to given type? -- (from READABLE_STRING_GENERAL) local l_convertor: like Ctoi_convertor do l_convertor := Ctoi_convertor; l_convertor.reset (type); l_convertor.parse_string_with_type (Current, type) Result := l_convertor.is_integral_integer end mirror_area (a: like area; start_index, end_index: INTEGER_32) -- Mirror all characters in a between start_index and end_index. -- (from READABLE_STRING_32) require -- from READABLE_STRING_32 a_not_void: a /= Void start_index_non_negative: start_index >= 0 start_index_not_too_big: start_index <= end_index + 1 end_index_valid: end_index < a.count local c: CHARACTER_32 i, j: INTEGER_32 do from i := end_index until i <= j loop c := a.item (i); a.put (a.item (j), i); a.put (c, j) i := i - 1 j := j + 1 end end new_string (n: INTEGER_32): like Current -- New instance of current with space for at least n characters. require -- from READABLE_STRING_GENERAL n_non_negative: n >= 0 do create Result.make (n) ensure -- from READABLE_STRING_GENERAL new_string_not_void: Result /= Void new_string_empty: Result.is_empty new_string_area_big_enough: Result.capacity >= n end str_strict_cmp (this, other: like area; this_index, other_index, n: INTEGER_32): INTEGER_32 -- Compare n characters from this starting at this_index with -- n characters from and other starting at other_index. -- 0 if equal, < 0 if this < other, -- > 0 if this > other -- (from READABLE_STRING_32) require -- from READABLE_STRING_32 this_not_void: this /= Void other_not_void: other /= Void n_non_negative: n >= 0 n_valid: n <= (this.upper - this_index + 1) and n <= (other.upper - other_index + 1) local i, j, nb, l_current_code, l_other_code: INTEGER_32 do from i := this_index nb := i + n j := other_index until i = nb loop l_current_code := this.item (i).code l_other_code := other.item (j).code if l_current_code /= l_other_code then Result := l_current_code - l_other_code i := nb - 1 end i := i + 1 j := j + 1 end end String_searcher: STRING_32_SEARCHER -- String searcher specialized for READABLE_STRING_32 instances. -- (from READABLE_STRING_32) require -- from READABLE_STRING_GENERAL True once create Result.make ensure -- from READABLE_STRING_GENERAL string_searcher_not_void: Result /= Void end to_lower_area (a: like area; start_index, end_index: INTEGER_32) -- Replace all characters in a between start_index and end_index -- with their lower version when available. -- (from READABLE_STRING_32) require -- from READABLE_STRING_32 a_not_void: a /= Void start_index_non_negative: start_index >= 0 start_index_not_too_big: start_index <= end_index + 1 end_index_valid: end_index < a.count local i: INTEGER_32 c1, c2: CHARACTER_32 l_prop: like Character_properties do from i := start_index l_prop := Character_properties until i > end_index loop c1 := a.item (i) c2 := l_prop.to_lower (c1) if c1 /= c2 then a.put (c2, i) end i := i + 1 end end to_upper_area (a: like area; start_index, end_index: INTEGER_32) -- Replace all characters in a between start_index and end_index -- with their upper version when available. -- (from READABLE_STRING_32) require -- from READABLE_STRING_32 a_not_void: a /= Void start_index_non_negative: start_index >= 0 start_index_not_too_big: start_index <= end_index + 1 end_index_valid: end_index < a.count local i: INTEGER_32 c1, c2: CHARACTER_32 l_prop: like Character_properties do from i := start_index l_prop := Character_properties until i > end_index loop c1 := a.item (i) c2 := l_prop.to_upper (c1) if c1 /= c2 then a.put (c2, i) end i := i + 1 end end feature {READABLE_STRING_8, READABLE_STRING_32, STRING_8_SEARCHER, STRING_32_SEARCHER, HEXADECIMAL_STRING_TO_INTEGER_CONVERTER, STRING_TO_INTEGER_CONVERTOR, STRING_TO_REAL_CONVERTOR, STRING_32_ITERATION_CURSOR} -- Implementation area_lower: INTEGER_32 -- Minimum index. -- (from READABLE_STRING_32) do ensure -- from READABLE_STRING_32 area_lower_non_negative: Result >= 0 area_lower_valid: Result <= area.upper end area_upper: INTEGER_32 -- Maximum index. -- (from READABLE_STRING_32) do Result := area_lower + count - 1 ensure -- from READABLE_STRING_32 area_upper_valid: Result <= area.upper area_upper_in_bound: area_lower <= Result + 1 end feature {READABLE_STRING_GENERAL} -- Implementation internal_case_insensitive_hash_code: INTEGER_32 -- Cash for case_insensitive_hash_code. -- (from READABLE_STRING_GENERAL) internal_hash_code: INTEGER_32 -- Cache for hash_code. -- (from READABLE_STRING_GENERAL) feature -- Access: Cursor new_character_32_cursor: STRING_ITERATION_CURSOR -- Fresh cursor for this string that iterates over code points (see code) -- exposed as CHARACTER_32. -- (from READABLE_STRING_GENERAL) do create Result.make (Current); Result.start end feature {NONE} -- Assertion helper Elks_checking: BOOLEAN = False -- Are ELKS checkings verified? Must be True when changing implementation of STRING_GENERAL or descendant. -- (from READABLE_STRING_GENERAL) feature -- Correction Mismatch_information: MISMATCH_INFORMATION -- Original attribute values of mismatched object -- (from MISMATCH_CORRECTOR) once create Result 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 -- Printable representation. -- (from READABLE_STRING_32) require -- from ANY True do Result := {UTF_CONVERTER}.string_32_to_utf_8_string_8 (Current) ensure -- from ANY out_not_void: Result /= Void ensure then -- from READABLE_STRING_32 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 feature {STRING_HANDLER} -- Settings reset_hash_codes -- Reset all hash codes of Current string. -- (from STRING_GENERAL) do internal_hash_code := 0 internal_case_insensitive_hash_code := 0 end set_internal_hash_code (v: like internal_hash_code) obsolete "Use `reset_hash_codes` instead. [2017-05-31]" -- Set internal_hash_code with v. -- (from STRING_GENERAL) require -- from STRING_GENERAL v_nonnegative: v >= 0 do internal_hash_code := v ensure -- from STRING_GENERAL internal_hash_code_set: internal_hash_code = v end invariant extendible: Extendible compare_character: not object_comparison -- from READABLE_STRING_32 area_not_void: area /= Void -- from COMPARABLE irreflexive_comparison: not (Current < Current) -- 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 STRING_GENERAL mutable: not is_immutable -- from RESIZABLE increase_by_at_least_one: Minimal_increase >= 1 -- from BOUNDED valid_count: count <= capacity full_definition: full = (count = capacity) -- from FINITE empty_definition: is_empty = (count = 0) note copyright: "Copyright (c) 1984-2020, 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 STRING_32
Generated by ISE EiffelStudio