note description: "Unicode strings" remark: "[ Unless specified otherwise, STRING and CHARACTER are supposed to contain characters whose code follows the unicode character set. In other words characters whose code is between 128 and 255 should follow the ISO 8859-1 Latin-1 character set. ]" remark2: "[ By default UC_STRING is implemented using the UTF-8 encoding. Use UC_UTF*_STRING to specify the encoding explicitly. ]" library: "Gobo Eiffel Kernel Library" copyright: "Copyright (c) 2001-2018, Eric Bezault and others" license: "MIT License" date: "$Date: 2019-02-07 22:54:15 +0000 (Thu, 07 Feb 2019) $" revision: "$Revision: 102807 $" class UC_STRING create make, make_empty, make_from_string, make_from_utf8, make_filled, make_filled_code, make_filled_unicode, make_from_substring, make_from_utf16, make_from_utf16le, make_from_utf16be, make_from_string_general, make_from_substring_general feature -- Initialization adapt (s: STRING_8): UC_STRING -- Object of a type conforming to the type of s, -- initialized with attributes from s -- (from STRING_8) do Result := new_string (0) Result.share (s) ensure -- from STRING_8 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. -- (from STRING_8) require -- from STRING_8 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 -- from STRING_8 no_zero_byte: not has ('%U') end from_c_substring (c_string: POINTER; start_pos, end_pos: INTEGER_32) -- Reset contents of string from substring of c_string, -- between start_pos and end_pos, -- and c_string created by some C function. -- (from STRING_8) require -- from STRING_8 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 -- from STRING_8 valid_count: count = end_pos - start_pos + 1 end make (suggested_capacity: INTEGER_32) -- Create empty string, or remove all characters from -- existing string. -- (Extended from ELKS 2001 STRING) require -- from READABLE_STRING_GENERAL non_negative_size: suggested_capacity >= 0 do reset_byte_index_cache count := 0 if suggested_capacity = 0 then Precursor (1) else Precursor (suggested_capacity) end set_count (byte_capacity) old_set_count (byte_capacity) set_count (0) byte_count := 0 ensure -- from READABLE_STRING_GENERAL empty_string: count = 0 area_allocated: byte_capacity >= suggested_capacity ensure then byte_count_set: byte_count = 0 byte_capacity_set: byte_capacity >= suggested_capacity end make_from_c (c_string: POINTER) -- Initialize from contents of c_string, -- a string created by some C function. -- (from READABLE_STRING_8) require -- from READABLE_STRING_8 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', l_count + 1) count := l_count internal_hash_code := 0 internal_case_insensitive_hash_code := 0 C_string_provider.read_substring_into_character_8_area (area, 1, l_count) end make_from_c_substring (c_string: POINTER; start_pos, end_pos: INTEGER_32) -- Initialize from substring of c_string, -- between start_pos and end_pos, -- c_string created by some C function. -- (from READABLE_STRING_8) require -- from READABLE_STRING_8 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) create area.make_filled ('%U', l_count + 1) count := l_count internal_hash_code := 0 internal_case_insensitive_hash_code := 0 C_string_provider.read_substring_into_character_8_area (area, 1, l_count) end make_from_cil (a_system_string: detachable SYSTEM_STRING) -- Initialize Current with a_system_string. -- (from STRING_8) require -- from READABLE_STRING_8 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 old_set_count (l_count) Dotnet_convertor.read_system_string_into (a_system_string, Current) end end make_from_string (a_string: STRING_8) -- Initialize from the character sequence of a_string. -- (ELKS 2001 STRING) require -- from READABLE_STRING_8 string_exists: a_string /= Void do make_from_string_general (a_string) ensure -- from READABLE_STRING_8 not_shared_implementation: Current /= a_string implies not shared_with (a_string) initialized: same_string (a_string) ensure then same_unicode: same_unicode_string (a_string) end remake (n: INTEGER_32) obsolete "Use `make' instead. [2017-05-31]" -- Allocate space for at least n characters. -- (from STRING_8) require -- from STRING_8 non_negative_size: n >= 0 do make (n) ensure -- from STRING_8 empty_string: count = 0 area_allocated: byte_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 -- Create empty string. -- (ELKS 2001 STRING) do make (0) ensure -- from READABLE_STRING_GENERAL empty: count = 0 area_allocated: byte_capacity >= 0 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 (c: CHARACTER_8; n: INTEGER_32) -- Create string of length n filled with character c. -- (ELKS 2001 STRING) require -- from READABLE_STRING_8 valid_count: n >= 0 local i, nb: INTEGER_32 new_byte_count: INTEGER_32 do nb := Utf8.character_byte_count (c) new_byte_count := nb * n make (new_byte_count) set_count (n) byte_count := new_byte_count if nb = 1 then from i := 1 until i > new_byte_count loop put_byte (c, i) i := i + 1 end else from i := 1 until i > new_byte_count loop put_character_at_byte_index (c, nb, i) i := i + nb end end ensure -- from READABLE_STRING_8 count_set: count = n area_allocated: byte_capacity >= n filled: occurrences (c) = count ensure then filled_code: code_occurrences (c.code) = count end make_filled_area (a_default_value: CHARACTER_8; 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_filled_code (a_code: INTEGER_32; n: INTEGER_32) -- Create string of length n filled with unicode -- character of code a_code. require valid_code: Unicode.valid_code (a_code) valid_count: n >= 0 local i, nb: INTEGER_32 new_byte_count: INTEGER_32 do nb := Utf8.code_byte_count (a_code) new_byte_count := nb * n make (new_byte_count) set_count (n) byte_count := new_byte_count from i := 1 until i > new_byte_count loop put_code_at_byte_index (a_code, nb, i) i := i + nb end ensure count_set: count = n filled: code_occurrences (a_code) = count end make_filled_unicode (c: UC_CHARACTER; n: INTEGER_32) -- Create string of length n filled with unicode character c. require c_not_void: c /= Void valid_count: n >= 0 do make_filled_code (c.code, n) ensure count_set: count = n filled: unicode_occurrences (c) = count end make_from_c_pointer (c_string: POINTER) obsolete "Use `make_from_c' instead. [2017-05-31]" -- Create new instance from contents of c_string, -- a string created by some C function. -- (from READABLE_STRING_8) require -- from READABLE_STRING_8 c_string_exists: c_string /= default_pointer do make_from_c (c_string) end make_from_separate (other: separate READABLE_STRING_8) -- Initialize current string from other. -- (from READABLE_STRING_8) require -- from READABLE_STRING_8 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.area.item (i), i) i := i + 1 end count := nb ensure -- from READABLE_STRING_8 same_string: end make_from_string_general (a_string: STRING_GENERAL) -- Initialize from the character sequence of a_string. require a_string_not_void: a_string /= Void local l_uc_string: detachable UC_STRING do if attached {UC_STRING} a_string as l_uc_string_2 then l_uc_string := l_uc_string_2 area := l_uc_string.area if a_string /= Current then l_uc_string := Void end end if l_uc_string /= Void then area := l_uc_string.area else make_from_substring_general (a_string, 1, a_string.count) end ensure same_unicode: same_unicode_string (a_string) end make_from_substring (a_string: STRING_8; start_index, end_index: INTEGER_32) -- Initialize from the character sequence of a_string -- between start_index and end_index inclusive. require a_string_not_void: a_string /= Void valid_start_index: 1 <= start_index valid_end_index: end_index <= a_string.count meaningful_interval: start_index <= end_index + 1 do make_from_substring_general (a_string, start_index, end_index) ensure initialized: same_unicode_string (a_string.substring (start_index, end_index)) end make_from_substring_general (a_string: STRING_GENERAL; start_index, end_index: INTEGER_32) -- Initialize from the character sequence of a_string -- between start_index and end_index inclusive. require a_string_not_void: a_string /= Void valid_start_index: 1 <= start_index valid_end_index: end_index <= a_string.count meaningful_interval: start_index <= end_index + 1 local nb: INTEGER_32 str: STRING_GENERAL l_uc_string: detachable UC_STRING do if attached {UC_STRING} a_string as l_uc_string_2 then l_uc_string := l_uc_string_2 area := l_uc_string.area if a_string /= Current then l_uc_string := Void end end if l_uc_string /= Void and then start_index = 1 and then end_index = count then area := l_uc_string.area else if end_index < start_index then make (0) else if l_uc_string /= Void then str := l_uc_string.cloned_string else str := a_string end nb := Utf8.substring_byte_count (str, start_index, end_index) make (nb) set_count (end_index - start_index + 1) byte_count := nb put_substring_at_byte_index (str, start_index, end_index, nb, 1) end end ensure initialized: same_unicode_string (a_string.substring (start_index, end_index)) end make_from_utf16 (s: STRING_8) -- Initialize from the bytes sequence of s corresponding -- to the UTF-16 representation of a string. require s_not_void: s /= Void s_is_string: Any_.same_types (s, "") valid_utf16: Utf16.valid_utf16 (s) do make (s.count // 2) append_utf16 (s) end make_from_utf16be (s: STRING_8) -- Initialize from the bytes sequence of s corresponding -- to the UTF-16BE representation of a string. require s_not_void: s /= Void s_is_string: Any_.same_types (s, "") valid_utf16be: Utf16.valid_utf16be (s) do make (s.count // 2) append_utf16be (s) end make_from_utf16le (s: STRING_8) -- Initialize from the bytes sequence of s corresponding -- to the UTF-16LE representation of a string. require s_not_void: s /= Void s_is_string: Any_.same_types (s, "") valid_utf16le: Utf16.valid_utf16le (s) do make (s.count // 2) append_utf16le (s) end make_from_utf8 (s: STRING_8) -- Initialize from the bytes sequence of s corresponding -- to the UTF-8 representation of a string. require s_not_void: s /= Void s_is_string: Any_.same_types (s, "") valid_utf8: Utf8.valid_utf8 (s) do make (s.count) append_utf8 (s) end feature -- Access Any_: KL_ANY_ROUTINES -- Routines that ought to be in class ANY -- (from KL_IMPORTED_ANY_ROUTINES) once create Result ensure -- from KL_IMPORTED_ANY_ROUTINES instance_free: class any_routines_not_void: Result /= Void end at alias "@" (i: INTEGER_32): CHARACTER_8 -- Character at index i -- (ELKS 2001 STRING) require -- from READABLE_STRING_8 True require -- from TABLE valid_key: valid_index (i) require -- from TO_SPECIAL valid_index: valid_index (i) do Result := item (i) ensure then definition: Result = item (i) 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 (character_32_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 character_32_item (i: INTEGER_32): CHARACTER_32 -- Character at position i. -- (from STRING_8) require -- from READABLE_STRING_GENERAL valid_index: valid_index (i) do Result := code (i).to_character_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_8) 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 UC_STRING] -- 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 -- (ELKS 2001 STRING) require -- from HASHABLE True local i, nb: INTEGER_32 a_code: INTEGER_32 fit_in_string: BOOLEAN do nb := count if nb = byte_count then internal_hash_code := 0 Result := Precursor else fit_in_string := True nb := byte_count from i := 1 until i > nb loop a_code := item_code_at_byte_index (i) Result := 5 * Result + a_code if a_code > Platform.Maximum_character_code then fit_in_string := False end i := next_byte_index (i) end if fit_in_string then Result := string.hash_code end end if Result < 0 then Result := - (Result + 1) end ensure -- from HASHABLE good_hash_value: Result >= 0 end index_of (c: CHARACTER_8; start_index: INTEGER_32): INTEGER_32 -- Index of first occurrence of character c -- at or after start_index; 0 if none -- (ELKS 2001 STRING) require -- from READABLE_STRING_8 start_large_enough: start_index >= 1 start_small_enough: start_index <= count + 1 local i, k, nb: INTEGER_32 max_code: INTEGER_32 a_code: INTEGER_32 do nb := count if nb = byte_count then from i := start_index until i > nb loop if byte_item (i) = c then Result := i i := nb + 1 else i := i + 1 end end elseif c = '%U' then if start_index <= nb then max_code := Platform.Maximum_character_code k := byte_index (start_index) from i := start_index until i > nb loop a_code := item_code_at_byte_index (k) if a_code = 0 or a_code > max_code then Result := i i := nb + 1 else k := next_byte_index (k) i := i + 1 end end end else Result := index_of_item_code (c.code, start_index) end ensure -- from READABLE_STRING_8 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 character_32_index_of (c: like character_32_item; 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 character_32_item (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).character_32_has (c) found_if_present: substring (start_index, count).character_32_has (c) implies character_32_item (Result) = c none_before: substring (start_index, count).character_32_has (c) implies not substring (start_index, Result - 1).character_32_has (c) end index_of_item_code (a_code: INTEGER_32; start_index: INTEGER_32): INTEGER_32 -- Index of first occurrence of unicode character with -- code a_code at or after start_index; 0 if none require valid_start_index: start_index >= 1 and start_index <= count + 1 valid_code: Unicode.valid_code (a_code) local i, k, nb: INTEGER_32 do nb := count if nb = byte_count then if a_code > 127 then Result := 0 else from i := start_index until i > nb loop if byte_item (i).code = a_code then Result := i i := nb + 1 else i := i + 1 end end end elseif start_index <= nb then k := byte_index (start_index) from i := start_index until i > nb loop if item_code_at_byte_index (k) = a_code then Result := i i := nb + 1 else k := next_byte_index (k) i := i + 1 end end end ensure valid_result: Result = 0 or (start_index <= Result and Result <= count) zero_if_absent: (Result = 0) = not substring (start_index, count).has_item_code (a_code) found_if_present: substring (start_index, count).has_item_code (a_code) implies item_code (Result) = a_code none_before: substring (start_index, count).has_item_code (a_code) implies not substring (start_index, Result - 1).has_item_code (a_code) end index_of_unicode (c: UC_CHARACTER; start_index: INTEGER_32): INTEGER_32 -- Index of first occurrence of c at or after start_index; -- 0 if none require c_not_void: c /= Void valid_start_index: start_index >= 1 and start_index <= count + 1 do Result := index_of_item_code (c.code, start_index) ensure valid_result: Result = 0 or (start_index <= Result and Result <= count) zero_if_absent: (Result = 0) = not substring (start_index, count).has_unicode (c) found_if_present: substring (start_index, count).has_unicode (c) implies item_code (Result) = c.code none_before: substring (start_index, count).has_unicode (c) implies not substring (start_index, Result - 1).has_unicode (c) end Integer_: KL_INTEGER_ROUTINES -- Routines that ought to be in class INTEGER -- (from KL_IMPORTED_INTEGER_ROUTINES) once create Result ensure -- from KL_IMPORTED_INTEGER_ROUTINES instance_free: class integer_routines_not_void: Result /= Void end item (i: INTEGER_32): CHARACTER_8 -- Character at index i; -- '%U' if the unicode character at index -- i cannot fit into a CHARACTER -- (Extended from ELKS 2001 STRING) -- Note: Use item_code instead of this routine when Current -- can contain characters which may not fit into a CHARACTER. local k: INTEGER_32 do if count = byte_count then Result := byte_item (i) else k := byte_index (i) Result := character_item_at_byte_index (k) end ensure then code_small_enough: item_code (i) <= Platform.Maximum_character_code implies Result.code = item_code (i) overflow: item_code (i) > Platform.Maximum_character_code implies Result = '%U' end item_code (i: INTEGER_32): INTEGER_32 -- Code of character at index i require -- from READABLE_STRING_8 index_small_enough: i <= count index_large_enough: i > 0 local k: INTEGER_32 do if count = byte_count then Result := byte_item (i).code else k := byte_index (i) Result := item_code_at_byte_index (k) end ensure then item_code_not_negative: Result >= 0 valid_item_code: Unicode.valid_code (Result) end last_index_of (c: CHARACTER_8; start_index_from_end: INTEGER_32): INTEGER_32 -- Position of last occurrence of c, -- 0 if none. -- (from READABLE_STRING_8) require -- from READABLE_STRING_8 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_8 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 character_32_last_index_of (c: like character_32_item; 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 character_32_item (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).character_32_has (c) found_if_present: substring (1, start_index_from_end).character_32_has (c) implies character_32_item (Result) = c none_after: substring (1, start_index_from_end).character_32_has (c) implies not substring (Result + 1, start_index_from_end).character_32_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_8_ITERATION_CURSOR -- Fresh cursor associated with current structure -- (from READABLE_STRING_8) require -- from ITERABLE True do create Result.make (Current) ensure -- from ITERABLE result_attached: Result /= Void end new_empty_string (suggested_capacity: INTEGER_32): like Current -- New empty string with same dynamic type as Current require non_negative_suggested_capacity: suggested_capacity >= 0 do create Result.make (suggested_capacity) ensure new_string_not_void: Result /= Void same_type: Any_.same_types (Result, Current) new_string_empty: Result.count = 0 byte_count_set: Result.byte_count = 0 byte_capacity_set: Result.byte_capacity >= suggested_capacity end Platform: KL_PLATFORM -- Platform-dependent properties -- (from KL_SHARED_PLATFORM) once create Result ensure -- from KL_SHARED_PLATFORM instance_free: class platform_not_void: Result /= Void end plus alias "+" (other: READABLE_STRING_8): like Current -- New object which is a clone of Current extended -- by the characters of other -- (ELKS 2001 STRING) require -- from READABLE_STRING_GENERAL argument_not_void: other /= Void compatible_strings: Is_string_8 implies other.Is_valid_as_string_8 do create Result.make (byte_count + Utf8.substring_byte_count (other, 1, other.count)) Result.append_string (Current) Result.append_string (other) ensure -- from READABLE_STRING_GENERAL plus_not_void: Result /= Void new_count: Result.count = count + other.count initial: Elks_checking implies Result.substring (1, count) ~ Current final: Elks_checking implies Result.substring (count + 1, count + other.count).same_string_general (other) ensure then final_unicode: Result.substring (count + 1, count + other.count).same_unicode_string (other) end prefixed_string (other: STRING_8): like Current -- New object which is a clone of Current preceded -- by the characters of other require other_not_void: other /= Void do create Result.make (byte_count + Utf8.substring_byte_count (other, 1, other.count)) Result.append_string (other) Result.append_string (Current) ensure prefixed_string_not_void: Result /= Void prefixed_string_count: Result.count = other.count + count initial: Result.substring (1, other.count).same_unicode_string (other) final: Result.substring (other.count + 1, Result.count).is_equal (Current) end string: STRING_8 -- New STRING having the same character sequence as Current -- where characters which do not fit in a CHARACTER are -- replaced by a '%U' -- (Extended from ELKS 2001 STRING) local i, nb: INTEGER_32 a_code: INTEGER_32 do nb := count create Result.make (nb) if nb = byte_count then from i := 1 until i > nb loop Result.append_character (byte_item (i)) i := i + 1 end else nb := byte_count from i := 1 until i > nb loop a_code := item_code_at_byte_index (i) if a_code <= Platform.Maximum_character_code then Result.append_character (Integer_.to_character (a_code)) else Result.append_character ('%U') end i := next_byte_index (i) end end ensure -- from READABLE_STRING_8 string_not_void: Result /= Void string_type: Result.same_type (create {STRING_8}.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_8 -- Similar to string but only create a new object if Current is not of dynamic type STRING_8. -- (from READABLE_STRING_8) do if same_type (create {STRING_8}.make_empty) and then attached {STRING_8} Current as l_s8 then Result := l_s8 else Result := string end ensure -- from READABLE_STRING_8 result_not_void: Result /= Void correct_type: Result.same_type (create {STRING_8}.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 (start_index, end_index: INTEGER_32): like Current -- New object containing all characters -- from start_index to end_index inclusive -- (ELKS 2001 STRING) require -- from READABLE_STRING_GENERAL True do if end_index < start_index then create Result.make (0) else create Result.make_from_substring (Current, start_index, end_index) 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.character_32_item (1) = character_32_item (start_index) recurse: Result.count > 0 implies Result.substring (2, Result.count) ~ substring (start_index + 1, end_index) ensure then first_unicode_item: Result.count > 0 implies Result.item_code (1) = item_code (start_index) end substring_index (other: STRING_8; start_index: INTEGER_32): INTEGER_32 -- Index of first occurrence of other at or after start_index; -- 0 if none. other and Current are considered with their -- characters which do not fit in a CHARACTER replaced by a '%U' -- (Extended from ELKS 2001 STRING) require -- from READABLE_STRING_GENERAL other_not_void: other /= Void valid_start_index: start_index >= 1 and start_index <= count + 1 local i, j, nb: INTEGER_32 a_code, a_code2: INTEGER_32 k, z, end_index: INTEGER_32 found: BOOLEAN other_count: INTEGER_32 do if other = Current then if start_index = 1 then Result := 1 end else other_count := other.count if other_count = 0 then Result := start_index else end_index := count - other_count + 1 if start_index <= end_index then if count = byte_count then if attached {UC_STRING} other as other_unicode then nb := other_unicode.byte_count from k := start_index until k > end_index loop j := k found := True from i := 1 until i > nb loop a_code := other_unicode.item_code_at_byte_index (i) if a_code > Platform.Maximum_character_code then a_code := 0 end if byte_item (j).code /= a_code then found := False i := nb + 1 else j := j + 1 i := other_unicode.next_byte_index (i) end end if found then Result := k k := end_index + 1 else k := k + 1 end end else nb := other_count from k := start_index until k > end_index loop j := k found := True from i := 1 until i > nb loop if byte_item (j) /= other.item (i) then found := False i := nb + 1 else j := j + 1 i := i + 1 end end if found then Result := k k := end_index + 1 else k := k + 1 end end end else z := byte_index (start_index) if attached {UC_STRING} other as other_unicode then nb := other_unicode.byte_count from k := start_index until k > end_index loop j := z found := True from i := 1 until i > nb loop a_code := item_code_at_byte_index (j) if a_code > Platform.Maximum_character_code then a_code := 0 end a_code2 := other_unicode.item_code_at_byte_index (i) if a_code2 > Platform.Maximum_character_code then a_code2 := 0 end if a_code /= a_code2 then found := False i := nb + 1 else j := next_byte_index (j) i := other_unicode.next_byte_index (i) end end if found then Result := k k := end_index + 1 else z := next_byte_index (z) k := k + 1 end end else nb := other_count from k := start_index until k > end_index loop j := z found := True from i := 1 until i > nb loop a_code := item_code_at_byte_index (j) if a_code > Platform.Maximum_character_code then a_code := 0 end if a_code /= other.item (i).code then found := False i := nb + 1 else j := next_byte_index (j) i := i + 1 end end if found then Result := k k := end_index + 1 else z := next_byte_index (z) k := k + 1 end end end end end end end 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_general (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_8) 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) Unicode: UC_UNICODE_ROUTINES -- Unicode routines -- (from UC_IMPORTED_UNICODE_ROUTINES) once create Result ensure -- from UC_IMPORTED_UNICODE_ROUTINES instance_free: class unicode_not_void: Result /= Void end unicode_item (i: INTEGER_32): UC_CHARACTER -- Unicode character at index i; -- Return a new object at each call require valid_index: valid_index (i) do create Result.make_from_code (item_code (i)) ensure item_not_void: Result /= Void code_set: Result.code = item_code (i) end unicode_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 require other_not_void: other /= Void valid_start_index: start_index >= 1 and start_index <= count + 1 local i, j, nb: INTEGER_32 a_code, a_code2: INTEGER_32 k, z, end_index: INTEGER_32 found: BOOLEAN other_count: INTEGER_32 do if other = Current then if start_index = 1 then Result := 1 end else other_count := other.count if other_count = 0 then Result := start_index else end_index := count - other_count + 1 if start_index <= end_index then if count = byte_count then if attached {UC_STRING} other as other_unicode then nb := other_unicode.byte_count from k := start_index until k > end_index loop j := k found := True from i := 1 until i > nb loop a_code := other_unicode.item_code_at_byte_index (i) if byte_item (j).code /= a_code then found := False i := nb + 1 else j := j + 1 i := other_unicode.next_byte_index (i) end end if found then Result := k k := end_index + 1 else k := k + 1 end end else nb := other_count from k := start_index until k > end_index loop j := k found := True from i := 1 until i > nb loop if byte_item (j).code /= other.code (i).to_integer_32 then found := False i := nb + 1 else j := j + 1 i := i + 1 end end if found then Result := k k := end_index + 1 else k := k + 1 end end end else z := byte_index (start_index) if attached {UC_STRING} other as other_unicode then nb := other_unicode.byte_count from k := start_index until k > end_index loop j := z found := True from i := 1 until i > nb loop a_code := item_code_at_byte_index (j) a_code2 := other_unicode.item_code_at_byte_index (i) if a_code /= a_code2 then found := False i := nb + 1 else j := next_byte_index (j) i := other_unicode.next_byte_index (i) end end if found then Result := k k := end_index + 1 else z := next_byte_index (z) k := k + 1 end end else nb := other_count from k := start_index until k > end_index loop j := z found := True from i := 1 until i > nb loop a_code := item_code_at_byte_index (j) if a_code /= other.code (i).to_integer_32 then found := False i := nb + 1 else j := next_byte_index (j) i := i + 1 end end if found then Result := k k := end_index + 1 else z := next_byte_index (z) k := k + 1 end end end end end end end ensure 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_unicode_substring (other) at_this_index: Result >= start_index implies substring (Result, Result + other.count - 1).same_unicode_string (other) none_before: Result > start_index implies not substring (start_index, Result + other.count - 2).has_unicode_substring (other) end Utf16: UC_UTF16_ROUTINES -- UTF-16 encoding routines -- (from UC_IMPORTED_UTF16_ROUTINES) once create Result ensure -- from UC_IMPORTED_UTF16_ROUTINES instance_free: class utf16_not_void: Result /= Void end Utf32: UC_UTF32_ROUTINES -- UTF-32 encoding routines -- (from UC_IMPORTED_UTF32_ROUTINES) once create Result ensure -- from UC_IMPORTED_UTF32_ROUTINES instance_free: class utf32_not_void: Result /= Void end Utf8: UC_UTF8_ROUTINES -- UTF-8 encoding routines -- (from UC_IMPORTED_UTF8_ROUTINES) once create Result ensure -- from UC_IMPORTED_UTF8_ROUTINES instance_free: class utf8_not_void: Result /= Void end feature {NONE} -- Access old_item (i: INTEGER_32): CHARACTER_8 assign put -- Character at position i. -- (from STRING_8) 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 String_: KL_STRING_ROUTINES -- Routines that ought to be in class STRING -- (from KL_IMPORTED_STRING_ROUTINES) once create Result ensure -- from KL_IMPORTED_STRING_ROUTINES instance_free: class string_routines_not_void: Result /= Void end feature {STRING_8} -- Access area: SPECIAL [CHARACTER_8] -- Storage for characters. -- (from STRING_8) shared_with (other: READABLE_STRING_8): BOOLEAN -- Does string share the text of other? -- (from READABLE_STRING_8) do Result := (other /= Void) and then (area = other.area) end feature -- Measurement additional_space: INTEGER_32 -- Proposed number of additional items -- (from RESIZABLE) do Result := (byte_capacity // 2).max (Minimal_increase) ensure -- from RESIZABLE at_least_one: Result >= 1 end byte_capacity: INTEGER_32 -- Maximum number of bytes that can be put in -- internal storage require -- from READABLE_STRING_GENERAL True require -- from BOUNDED True do Result := Precursor ensure -- from READABLE_STRING_GENERAL capacity_non_negative: Result >= 0 ensure -- from BOUNDED capacity_non_negative: Result >= 0 end byte_count: INTEGER_32 -- Number of bytes in internal storage code_occurrences (a_code: INTEGER_32): INTEGER_32 -- Number of times unicode character of code -- a_code appears in the string require valid_code: Unicode.valid_code (a_code) local i, nb: INTEGER_32 do nb := count if nb = byte_count then if a_code > 127 then Result := 0 else from i := 1 until i > nb loop if byte_item (i).code = a_code then Result := Result + 1 end i := i + 1 end end else nb := byte_count from i := 1 until i > nb loop if item_code_at_byte_index (i) = a_code then Result := Result + 1 end i := next_byte_index (i) end end ensure zero_if_empty: count = 0 implies Result = 0 recurse_if_not_found_at_first_position: (count > 0 and then item_code (1) /= a_code) implies Result = substring (2, count).code_occurrences (a_code) recurse_if_found_at_first_position: (count > 0 and then item_code (1) = a_code) implies Result = 1 + substring (2, count).code_occurrences (a_code) end count: INTEGER_32 -- Number of characters -- (ELKS 2001 STRING) 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_8) Minimal_increase: INTEGER_32 = 5 -- Minimal number of additional items -- (from RESIZABLE) occurrences (c: CHARACTER_8): INTEGER_32 -- Number of times character c appears in the string -- (ELKS 2001 STRING) require -- from BAG True require -- from READABLE_STRING_8 True local i, nb: INTEGER_32 max_code: INTEGER_32 a_code: INTEGER_32 do nb := count if nb = byte_count then from i := 1 until i > nb loop if byte_item (i) = c then Result := Result + 1 end i := i + 1 end elseif c = '%U' then max_code := Platform.Maximum_character_code nb := byte_count from i := 1 until i > nb loop a_code := item_code_at_byte_index (i) if a_code = 0 or a_code > max_code then Result := Result + 1 end i := next_byte_index (i) end else Result := code_occurrences (c.code) end ensure -- from BAG non_negative_occurrences: Result >= 0 ensure then -- from READABLE_STRING_8 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 character_32_occurrences (c: CHARACTER_32): INTEGER_32 -- Number of times c appears in the string -- (from READABLE_STRING_GENERAL) local i, nb: INTEGER_32 do nb := count if nb > 0 then from i := 1 until i > nb loop if character_32_item (i) = c then Result := Result + 1 end i := i + 1 end 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 character_32_item (1) /= c) implies Result = substring (2, count).character_32_occurrences (c) recurse_if_found_at_first_position: (count > 0 and then character_32_item (1) = c) implies Result = 1 + substring (2, count).character_32_occurrences (c) end unicode_occurrences (c: UC_CHARACTER): INTEGER_32 -- Number of times c appears in the string require c_not_void: c /= Void do Result := code_occurrences (c.code) ensure zero_if_empty: count = 0 implies Result = 0 recurse_if_not_found_at_first_position: (count > 0 and then item_code (1) /= c.code) implies Result = substring (2, count).unicode_occurrences (c) recurse_if_found_at_first_position: (count > 0 and then item_code (1) = c.code) implies Result = 1 + substring (2, count).unicode_occurrences (c) end feature {NONE} -- Measurement estimated_count_of (other: ITERABLE [CHARACTER_8]): INTEGER_32 -- Estimated number of elements in other. -- (from CONTAINER) do if attached {FINITE [CHARACTER_8]} other as f then Result := f.count elseif attached {READABLE_INDEXABLE [CHARACTER_8]} 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 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 {UC_STRING} other as l_other implies (standard_is_equal (l_other) implies Result) valid_result: as_lower ~ other.as_lower implies Result end frozen is_deep_equal (other: UC_STRING): 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: like Current): BOOLEAN -- Is other attached to an object considered equal -- to current object? -- (Extended from ELKS 2001 STRING) local i, nb: INTEGER_32 do if other = Current then Result := True elseif Any_.same_types (Current, other) and then other.byte_count = byte_count then nb := byte_count Result := True from i := 1 until i > nb loop if byte_item (i) /= other.byte_item (i) then Result := False i := nb + 1 else i := i + 1 end end end ensure then unicode_definition: Result = (Any_.same_types (Current, other) and then count = other.count and then (count > 0 implies (item_code (1) = other.item_code (1) and substring (2, count).is_equal (other.substring (2, count))))) end old_is_equal (other: UC_STRING): BOOLEAN -- Is string made of same character sequence as other -- (possibly with a different capacity)? -- (from READABLE_STRING_8) 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: UC_STRING): 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 ">=" (other: UC_STRING): 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: like Current): BOOLEAN -- Is string lexicographically lower than other? -- (Extended from ELKS 2001 STRING, inherited from COMPARABLE) do Result := (three_way_comparison (other) = -1) ensure then unicode_definition: Result = (count = 0 and other.count > 0 or count > 0 and then other.count > 0 and then (item_code (1) < other.item_code (1) or item_code (1) = other.item_code (1) and substring (2, count) < other.substring (2, other.count))) end old_infix_less (other: UC_STRING): BOOLEAN -- Is string lexicographically lower than other? -- (from READABLE_STRING_8) 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 "<=" (other: UC_STRING): 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 (other: UC_STRING): UC_STRING -- 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 (other: UC_STRING): UC_STRING -- 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 (other: READABLE_STRING_8; 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_8) require -- from READABLE_STRING_8 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_area, l_other_area: like area c1, c2: CHARACTER_8 do nb := end_pos - start_pos + 1 if nb <= count - index_pos + 1 then from 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: l_area.upper - i + 1 until i = nb loop c1 := l_area.item (i) c2 := l_other_area.item (j) if c1 /= c2 and then c1.as_lower /= c2.as_lower then Result := False i := nb - 1 end i := i + 1 j := j + 1 end end ensure -- from READABLE_STRING_8 same_characters: Result = substring (index_pos, index_pos + end_pos - start_pos).is_case_insensitive_equal (other.substring (start_pos, end_pos)) 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 character_32_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 := character_32_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_characters (other: READABLE_STRING_8; 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_8) require -- from READABLE_STRING_8 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_8 same_characters: Result = substring (index_pos, index_pos + end_pos - start_pos).same_string (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 character_32_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_string (other: READABLE_STRING_8): BOOLEAN -- Do Current and other have the same character sequence? -- Current is considered with its characters which do not -- fit in a CHARACTER replaced by a '%U'. -- (Extended from ELKS 2001 STRING) require -- from READABLE_STRING_8 other_not_void: other /= Void do if other = Current then Result := True elseif other.count = count then Result := (substring_index (other.as_string_8, 1) = 1) end ensure -- from READABLE_STRING_8 definition: Result = (string ~ other.string) end same_string_general (other: READABLE_STRING_GENERAL): BOOLEAN -- Do Current and other have the same character sequence? -- Current is considered with its characters which do not -- fit in a CHARACTER replaced by a '%U'. -- (Extended from ELKS 2001 STRING) require -- from READABLE_STRING_GENERAL other_not_void: other /= Void local i, l_count: INTEGER_32 l_c, l_other_c: NATURAL_32 do if other = Current then Result := True elseif other.count = count then l_count := count from Result := True i := 1 until i > l_count loop l_c := code (i) if l_c > Platform.Maximum_character_code.to_natural_32 then l_c := 0 end l_other_c := other.code (i) if l_other_c > Platform.Maximum_character_code.to_natural_32 then l_other_c := 0 end if l_c /= l_other_c then Result := False i := l_count end i := i + 1 end end end same_unicode_string (other: READABLE_STRING_GENERAL): BOOLEAN -- Do Current and other have the same unicode character sequence? require other_not_void: other /= Void do if other = Current then Result := True elseif other.count = count then Result := (unicode_substring_index (other, 1) = 1) end ensure definition: Result = (count = other.count and then (count > 0 implies (code (1) = other.code (1) and (count >= 2 implies substring (2, count).same_unicode_string (other.substring (2, count)))))) end frozen standard_equal (a: detachable ANY; b: like arg #1): BOOLEAN -- Are a and b either both void or attached to -- field-by-field identical objects of the same type? -- Always uses default object comparison criterion. -- (from ANY) do if a = Void then Result := b = Void else Result := b /= Void and then a.standard_is_equal (b) end ensure -- from ANY instance_free: class definition: Result = (a = Void and b = Void) or else ((a /= Void and b /= Void) and then a.standard_is_equal (b)) end frozen standard_is_equal (other: UC_STRING): 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 (other: like Current): INTEGER_32 -- If current object equal to other, 0; -- if smaller, -1; if greater, 1 -- (ELKS 2001 STRING, inherited from COMPARABLE) -- Note: there is a bug in the specification of the -- contracts of three_way_comparison inherited -- from COMPARABLE. This routine cannot satisfy -- its postconditions if other is not of the -- same type as Current because the postcondition -- uses is_equal and is_equal has a postcondition -- inherited from ANY which says if it returns true -- then other has the same type as Current. require -- from COMPARABLE other_exists: other /= Void local i, nb, nb1, nb2: INTEGER_32 b1, b2: CHARACTER_8 found: BOOLEAN do if other /= Current and Any_.same_types (Current, other) then nb1 := byte_count nb2 := other.byte_count if nb1 < nb2 then nb := nb1 else nb := nb2 end from i := 1 until i > nb loop b1 := byte_item (i) b2 := other.byte_item (i) if b1 = b2 then i := i + 1 elseif b1 < b2 then found := True Result := -1 i := nb + 1 else found := True Result := 1 i := nb + 1 end end if not found then if nb1 < nb2 then Result := -1 elseif nb1 /= nb2 then Result := 1 end end end ensure -- from COMPARABLE equal_zero: (Result = 0) = (Current ~ other) smaller_negative: (Result = -1) = (Current < other) greater_positive: (Result = 1) = (Current > other) end three_way_unicode_comparison (other: STRING_8): INTEGER_32 -- If current object equal to other, 0; -- if smaller, -1; if greater, 1 -- Note: there is a bug in the specification of the -- contracts of three_way_comparison inherited -- from COMPARABLE. This routine cannot satisfy -- its postconditions if other is not of the -- same type as Current because the postcondition -- uses is_equal and is_equal has a postcondition -- inherited from ANY which says if it returns true -- then other has the same type as Current. -- three_way_unicode_comparison solves this problem -- and make the comparison polymorphically safe by -- changing the signature from 'like Current' to -- 'STRING' and by using same_unicode_string instead -- of is_equal in its postcondition. require other_not_void: other /= Void local i, nb, nb1, nb2: INTEGER_32 b1, b2: CHARACTER_8 c1, c2: INTEGER_32 found: BOOLEAN do if other = Current then Result := 0 elseif Any_.same_types (Current, other) and then attached {UC_STRING} other as uc_string then nb1 := byte_count nb2 := uc_string.byte_count if nb1 < nb2 then nb := nb1 else nb := nb2 end from i := 1 until i > nb loop b1 := byte_item (i) b2 := uc_string.byte_item (i) if b1 = b2 then i := i + 1 elseif b1 < b2 then found := True Result := -1 i := nb + 1 else found := True Result := 1 i := nb + 1 end end if not found then if nb1 < nb2 then Result := -1 elseif nb1 /= nb2 then Result := 1 end end else nb1 := count nb2 := other.count if nb1 < nb2 then nb := nb1 else nb := nb2 end from i := 1 until i > nb loop c1 := item_code (i) c2 := other.item_code (i) if c1 = c2 then i := i + 1 elseif c1 < c2 then found := True Result := -1 i := nb + 1 else found := True Result := 1 i := nb + 1 end end if not found then if nb1 < nb2 then Result := -1 elseif nb1 /= nb2 then Result := 1 end end end ensure equal_zero: (Result = 0) = same_unicode_string (other) end feature {STRING_8} -- Comparison is_case_insensitive_equal (other: READABLE_STRING_8): BOOLEAN -- Is string made of same character sequence as other regardless of casing -- (possibly with a different capacity)? -- (from READABLE_STRING_8) require -- from READABLE_STRING_8 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_8 symmetric: Result implies other.is_case_insensitive_equal (Current) consistent: attached {UC_STRING} other as l_other implies (standard_is_equal (l_other) implies Result) valid_result: as_lower.same_string (other.as_lower) implies Result end feature -- Status report Changeable_comparison_criterion: BOOLEAN = False -- May object_comparison be changed? -- (Answer: yes by default.) -- (from STRING_8) 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 old_empty: BOOLEAN obsolete "ELKS 2000: Use `is_empty' instead. [2017-05-31]" -- Is there no element? -- (from CONTAINER) do Result := old_is_empty end ends_with (s: READABLE_STRING_8): BOOLEAN -- Does string finish with s? -- (from READABLE_STRING_8) require -- from READABLE_STRING_8 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_8 definition: Result = s.same_string (substring (count - s.count + 1, count)) end Extendible: BOOLEAN = True -- May new items be added? (Answer: yes.) -- (from STRING_8) full: BOOLEAN -- Is structure full? -- (from BOUNDED) do Result := count = byte_capacity end character_32_has (c: like character_32_item): 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 (character_32_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 character_32_item (1) = c implies Result recurse: (count > 0 and then character_32_item (1) /= c) implies (Result = substring (2, count).character_32_has (c)) end has (c: CHARACTER_8): BOOLEAN -- Does Current contain character c? -- (ELKS 2001 STRING) require -- from CONTAINER True require -- from READABLE_STRING_8 True do Result := (index_of (c, 1) /= 0) ensure -- from CONTAINER not_found_in_empty: Result implies not old_is_empty ensure -- from READABLE_STRING_8 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)) end has_item_code (a_code: INTEGER_32): BOOLEAN -- Does Current contain the unicode character of code a_code? require valid_code: Unicode.valid_code (a_code) do Result := (index_of_item_code (a_code, 1) /= 0) ensure false_if_empty: count = 0 implies not Result true_if_first: count > 0 and then item_code (1) = a_code implies Result recurse: (count > 0 and then item_code (1) /= a_code) implies (Result = substring (2, count).has_item_code (a_code)) end has_substring (other: STRING_8): BOOLEAN -- Does Current contain other? -- other and Current are considered with their characters -- which do not fit in a CHARACTER replaced by a '%U'. -- (Extented from ELKS 2001 STRING) 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_general (substring (1, other.count))) implies Result recurse: (count >= other.count and then not other.same_string_general (substring (1, other.count))) implies (Result = substring (2, count).has_substring (other)) end has_unicode (c: UC_CHARACTER): BOOLEAN -- Does Current contain c? require c_not_void: c /= Void do Result := has_item_code (c.code) ensure false_if_empty: count = 0 implies not Result true_if_first: count > 0 and then item_code (1) = c.code implies Result recurse: (count > 0 and then item_code (1) /= c.code) implies (Result = substring (2, count).has_unicode (c)) end has_unicode_substring (other: READABLE_STRING_GENERAL): BOOLEAN -- Does Current contain other? require other_not_void: other /= Void do if other = Current then Result := True elseif other.count <= count then Result := (unicode_substring_index (other, 1) /= 0) end ensure false_if_too_small: count < other.count implies not Result true_if_initial: (count >= other.count and then substring (1, other.count).same_unicode_string (other)) implies Result recurse: (count >= other.count and then not substring (1, other.count).same_unicode_string (other)) implies (Result = substring (2, count).has_unicode_substring (other)) end is_ascii: BOOLEAN -- Does string contain only ASCII characters? do Result := (count = byte_count) ensure empty: count = 0 implies Result recurse: count > 0 implies Result = (unicode_item (1).is_ascii and substring (2, count).is_ascii) end is_boolean: BOOLEAN -- Does Current represent a BOOLEAN? -- (from READABLE_STRING_8) require -- from READABLE_STRING_GENERAL True local nb: INTEGER_32 l_area: like area i: INTEGER_32 do nb := count if nb = 4 then l_area := area i := area_lower Result := l_area.item (i).lower = 't' and then l_area.item (i + 1).lower = 'r' and then l_area.item (i + 2).lower = 'u' and then l_area.item (i + 3).lower = 'e' elseif nb = 5 then l_area := area i := area_lower Result := l_area.item (i).lower = 'f' and then l_area.item (i + 1).lower = 'a' and then l_area.item (i + 2).lower = 'l' and then l_area.item (i + 3).lower = 's' and then l_area.item (i + 4).lower = 'e' 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_closable: BOOLEAN -- Can current output stream be closed? -- (from KI_OUTPUT_STREAM) do Result := False ensure -- from KI_OUTPUT_STREAM is_open: Result implies is_open_write 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 string empty? -- (ELKS 2001 STRING) do Result := (count = 0) end old_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_8): 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 = False -- Is Current a sequence of CHARACTER_32? -- (from READABLE_STRING_8) Is_string_8: BOOLEAN = True -- Is Current a sequence of CHARACTER_8? -- (from READABLE_STRING_8) 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_8) 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_area: like area do from l_area := area i := area_lower + start_index - 1 n := area_lower + end_index - 1 until i > n or not l_area.item (i).is_space loop i := i + 1 end Result := i > n end Is_valid_as_string_8: BOOLEAN = True -- Is Current convertible to a sequence of CHARACTER_8 without information loss? -- (from READABLE_STRING_8) 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 STRING_8) 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_8): BOOLEAN -- Does string begin with s? -- (from READABLE_STRING_8) require -- from READABLE_STRING_8 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_8 definition: Result = s.same_string (substring (1, s.count)) 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 {STRING_8} -- Status report valid_code (v: NATURAL_32): BOOLEAN -- Is v a valid code for a CHARACTER_32? -- (from READABLE_STRING_8) require -- from READABLE_STRING_GENERAL True do Result := v <= {CHARACTER_8}.max_value.to_natural_32 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 old_left_adjust old_right_adjust ensure -- from STRING_GENERAL valid_count: count <= old count new_count_left: not old_is_empty implies not character_32_item (1).is_space new_count_right: not old_is_empty implies not character_32_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 (a_string: READABLE_STRING_8) -- Append a copy of a_string at end. -- (ELKS 2001 STRING) require -- from STRING_8 argument_not_void: a_string /= Void local nb: INTEGER_32 old_a_string_byte_count: INTEGER_32 old_a_string_count: INTEGER_32 new_byte_count: INTEGER_32 new_count: INTEGER_32 b: BOOLEAN do if Any_.same_types (a_string, Dummy_string) then nb := Utf8.substring_byte_count (a_string.as_string_8, 1, a_string.count) if nb = a_string.count then new_byte_count := byte_count + nb new_count := count + nb set_count (byte_count) old_set_count (byte_count) b := {ISE_RUNTIME}.check_assert (False) Precursor (a_string) b := {ISE_RUNTIME}.check_assert (b) set_count (byte_capacity) old_set_count (byte_capacity) set_count (new_count) byte_count := new_byte_count else gobo_append_substring (a_string.as_string_8, 1, a_string.count) end else if attached {UC_STRING} a_string as a_uc_string then if attached {UC_UTF8_STRING} a_string or Any_.same_types (a_uc_string, Dummy_uc_string) then if a_uc_string = Current then new_byte_count := 2 * byte_count new_count := 2 * count set_count (byte_count) old_set_count (byte_count) b := {ISE_RUNTIME}.check_assert (False) Precursor (a_string) b := {ISE_RUNTIME}.check_assert (b) set_count (byte_capacity) old_set_count (byte_capacity) set_count (new_count) byte_count := new_byte_count else old_a_string_count := a_uc_string.count old_a_string_byte_count := a_uc_string.byte_count new_byte_count := byte_count + old_a_string_byte_count new_count := count + old_a_string_count a_uc_string.set_count (old_a_string_byte_count) set_count (byte_count) old_set_count (byte_count) b := {ISE_RUNTIME}.check_assert (False) Precursor (a_string) b := {ISE_RUNTIME}.check_assert (b) set_count (byte_capacity) old_set_count (byte_capacity) set_count (new_count) a_uc_string.set_count (old_a_string_count) byte_count := new_byte_count end else gobo_append_substring (a_string.as_string_8, 1, a_string.count) end else gobo_append_substring (a_string.as_string_8, 1, a_string.count) end end ensure -- from STRING_8 new_count: count = old count + old a_string.count appended: Elks_checking implies same_string (old (Current + a_string)) end append_boolean (b: BOOLEAN) -- Append the string representation of b at end. -- (from STRING_8) do append (b.out) end append_character (c: CHARACTER_8) -- Append character c at end. -- (ELKS 2001 STRING) require -- from KI_OUTPUT_STREAM is_open_write: is_open_write require -- from STRING_8 True local k, nb: INTEGER_32 new_byte_count: INTEGER_32 new_count: INTEGER_32 do if c <= '%/127/' then nb := 1 else nb := Utf8.character_byte_count (c) end k := byte_count + 1 new_byte_count := byte_count + nb if new_byte_count > byte_capacity then resize_byte_storage (new_byte_count) end byte_count := new_byte_count if nb = 1 then new_count := count + 1 set_count (byte_count) old_put (c, k) set_count (new_count) else set_count (count + 1) put_character_at_byte_index (c, nb, k) end ensure then -- from STRING_8 item_inserted: item (count) = c new_count: count = old count + 1 stable_before: Elks_checking implies substring (1, count - 1) ~ (old twin) ensure then unicode_appended: item_code (count) = c.code end append_double (d: REAL_64) -- Append the string representation of d at end. -- (from STRING_8) do append (d.out) end append_integer (i: INTEGER_32) -- Append the string representation of i at end. -- (from STRING_8) local l_value: INTEGER_32 l_starting_index, l_ending_index: INTEGER_32 l_temp: CHARACTER_8 l_area: like area do if i = 0 then append_character ('0') else from l_starting_index := count if i < 0 then append_character ('-') l_starting_index := l_starting_index + 1 if i = {INTEGER_32}.min_value then append_character ('8') 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_8) 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. -- (from STRING_8) local l_value: INTEGER_16 l_starting_index, l_ending_index: INTEGER_32 l_temp: CHARACTER_8 l_area: like area do if i = 0 then append_character ('0') else from l_starting_index := count if i < 0 then append_character ('-') l_starting_index := l_starting_index + 1 if i = {INTEGER_16}.min_value then append_character ('8') 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_8) 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. -- (from STRING_8) local l_value: INTEGER_64 l_starting_index, l_ending_index: INTEGER_32 l_temp: CHARACTER_8 l_area: like area do if i = 0 then append_character ('0') else from l_starting_index := count if i < 0 then append_character ('-') l_starting_index := l_starting_index + 1 if i = {INTEGER_64}.min_value then append_character ('8') 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_8) 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. -- (from STRING_8) local l_value: INTEGER_8 l_starting_index, l_ending_index: INTEGER_32 l_temp: CHARACTER_8 l_area: like area do if i = 0 then append_character ('0') else from l_starting_index := count if i < 0 then append_character ('-') l_starting_index := l_starting_index + 1 if i = {INTEGER_8}.min_value then append_character ('8') 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_8) 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_item_code (a_code: INTEGER_32) -- Append unicode character of code a_code at end. require valid_item_code: Unicode.valid_code (a_code) local k, nb: INTEGER_32 new_byte_count: INTEGER_32 do nb := Utf8.code_byte_count (a_code) k := byte_count + 1 new_byte_count := byte_count + nb if new_byte_count > byte_capacity then resize_byte_storage (new_byte_count) end byte_count := new_byte_count set_count (count + 1) put_code_at_byte_index (a_code, nb, k) ensure new_count: count = old count + 1 appended: item_code (count) = a_code stable_before: substring (1, count - 1).is_equal (old cloned_string) end append_natural_16 (i: NATURAL_16) -- Append the string representation of i at end. -- (from STRING_8) local l_value: NATURAL_16 l_starting_index, l_ending_index: INTEGER_32 l_temp: CHARACTER_8 l_area: like area do if i = 0 then append_character ('0') else from l_starting_index := count l_value := i until l_value = 0 loop append_character (((l_value \\ 10) + 48).to_character_8) 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. -- (from STRING_8) local l_value: NATURAL_32 l_starting_index, l_ending_index: INTEGER_32 l_temp: CHARACTER_8 l_area: like area do if i = 0 then append_character ('0') else from l_starting_index := count l_value := i until l_value = 0 loop append_character (((l_value \\ 10) + 48).to_character_8) 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. -- (from STRING_8) local l_value: NATURAL_64 l_starting_index, l_ending_index: INTEGER_32 l_temp: CHARACTER_8 l_area: like area do if i = 0 then append_character ('0') else from l_starting_index := count l_value := i until l_value = 0 loop append_character (((l_value \\ 10) + 48).to_character_8) 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. -- (from STRING_8) local l_value: NATURAL_8 l_starting_index, l_ending_index: INTEGER_32 l_temp: CHARACTER_8 l_area: like area do if i = 0 then append_character ('0') else from l_starting_index := count l_value := i until l_value = 0 loop append_character (((l_value \\ 10) + 48).to_character_8) 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. -- (from STRING_8) do append (r.out) end append_string (s: detachable READABLE_STRING_8) -- Append a copy of s at end. do if s /= Void then append (s) end ensure -- from STRING_8 appended: s /= Void implies (Elks_checking implies Current ~ (old twin + old s.twin)) end append_string_general (s: READABLE_STRING_GENERAL) -- Append a copy 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 {STRING_8} s as ls then append (ls) else Precursor (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)) 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 > byte_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 old_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))) end append_substring (s: READABLE_STRING_8; start_index, end_index: INTEGER_32) -- Append characters of s.substring (start_index, end_index) at end. -- (from STRING_8) require -- from STRING_8 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 > byte_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 -- from STRING_8 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 append_unicode_character (c: UC_CHARACTER) -- Append unicode character c at end. require c_not_void: c /= Void do append_item_code (c.code) ensure new_count: count = old count + 1 appended: item_code (count) = c.code stable_before: substring (1, count - 1).is_equal (old cloned_string) end append_utf16 (s: STRING_8) -- Append UTF-16 encoded string s at end of current string. require s_not_void: s /= Void s_is_string: Any_.same_types (s, "") valid_utf16: Utf16.valid_utf16 (s) local msb_first: BOOLEAN i, nb: INTEGER_32 a_most, a_least: INTEGER_32 a_low_most, a_low_least: INTEGER_32 do i := 1 nb := s.count msb_first := True if nb >= 2 then if Utf16.is_endian_detection_character_most_first (s.item_code (1), s.item_code (2)) then check msb_first_set: msb_first end i := 3 elseif Utf16.is_endian_detection_character_least_first (s.item_code (1), s.item_code (2)) then msb_first := False i := 3 end end from until i > nb loop if msb_first then a_most := s.item_code (i) a_least := s.item_code (i + 1) else a_least := s.item_code (i) a_most := s.item_code (i + 1) end if Utf16.is_surrogate (a_most) then check valid_pre_implies_high: Utf16.is_high_surrogate (a_most) end check valid_pre_implies_size: i + 2 < nb end i := i + 2 if msb_first then a_low_most := s.item_code (i) a_low_least := s.item_code (i + 1) else a_low_least := s.item_code (i) a_low_most := s.item_code (i + 1) end check valid_pre_implies_low: Utf16.is_low_surrogate (a_low_most) end append_item_code (Utf16.surrogate_from_bytes (a_most, a_least, a_low_most, a_low_least)) else append_item_code (a_most * 256 + a_least) end i := i + 2 end end append_utf16be (s: STRING_8) -- Append UTF-16BE encoded string s at end of current string. require s_not_void: s /= Void s_is_string: Any_.same_types (s, "") valid_utf16be: Utf16.valid_utf16be (s) local i, nb: INTEGER_32 a_most, a_least: INTEGER_32 a_low_most, a_low_least: INTEGER_32 do i := 1 nb := s.count from until i > nb loop a_most := s.item_code (i) a_least := s.item_code (i + 1) if Utf16.is_surrogate (a_most) then check valid_pre_implies_high: Utf16.is_high_surrogate (a_most) end check valid_pre_implies_size: i + 2 < nb end i := i + 2 a_low_most := s.item_code (i) a_low_least := s.item_code (i + 1) check valid_pre_implies_low: Utf16.is_low_surrogate (a_low_most) end append_item_code (Utf16.surrogate_from_bytes (a_most, a_least, a_low_most, a_low_least)) else append_item_code (a_most * 256 + a_least) end i := i + 2 end end append_utf16le (s: STRING_8) -- Append UTF-16LE encoded string s at end of current string. require s_not_void: s /= Void s_is_string: Any_.same_types (s, "") valid_utf16le: Utf16.valid_utf16le (s) local i, nb: INTEGER_32 a_most, a_least: INTEGER_32 a_low_most, a_low_least: INTEGER_32 do i := 1 nb := s.count from until i > nb loop a_least := s.item_code (i) a_most := s.item_code (i + 1) if Utf16.is_surrogate (a_most) then check valid_pre_implies_high: Utf16.is_high_surrogate (a_most) end check valid_pre_implies_size: i + 2 < nb end i := i + 2 a_low_least := s.item_code (i) a_low_most := s.item_code (i + 1) check valid_pre_implies_low: Utf16.is_low_surrogate (a_low_most) end append_item_code (Utf16.surrogate_from_bytes (a_most, a_least, a_low_most, a_low_least)) else append_item_code (a_most * 256 + a_least) end i := i + 2 end end append_utf8 (s: STRING_8) -- Append UTF-8 encoded string s at end of current string. require s_not_void: s /= Void s_is_string: Any_.same_types (s, "") valid_utf8: Utf8.valid_utf8 (s) local i, k, nb: INTEGER_32 a_byte: CHARACTER_8 j, nb2: INTEGER_32 a_count: INTEGER_32 new_byte_count: INTEGER_32 do nb := s.count new_byte_count := byte_count + nb if new_byte_count > byte_capacity then resize_byte_storage (new_byte_count) end k := byte_count + 1 byte_count := new_byte_count from i := 1 until i > nb loop from a_count := a_count + 1 a_byte := s.item (i) put_byte (a_byte, k) i := i + 1 k := k + 1 nb2 := Utf8.encoded_byte_count (a_byte) j := 1 until j >= nb2 loop put_byte (s.item (i), k) i := i + 1 k := k + 1 j := j + 1 end end set_count (count + a_count) end extend (c: CHARACTER_8) -- Append c at end. -- Was declared in STRING_8 as synonym of append_character. -- (from STRING_8) require -- from COLLECTION extendible: Extendible local current_count: INTEGER_32 do current_count := count if current_count = byte_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 -- from STRING_8 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_8]) -- 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_8] 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. -- (from STRING_8) do fill_character (' ') ensure -- from STRING_8 filled: full same_size: (count = byte_capacity) and (byte_capacity = old byte_capacity) end fill_character (c: CHARACTER_8) -- Fill with capacity characters all equal to c. -- (from READABLE_STRING_8) local l_cap: like byte_capacity do l_cap := byte_capacity if l_cap /= 0 then area.fill_with (c, 0, l_cap - 1) count := l_cap internal_hash_code := 0 internal_case_insensitive_hash_code := 0 end ensure -- from READABLE_STRING_8 filled: count = byte_capacity same_size: byte_capacity = old byte_capacity end fill_with (c: CHARACTER_8) -- Replace every character with character c. -- (ELKS 2001 STRING) require -- from STRING_8 True local i, nb: INTEGER_32 new_byte_count: INTEGER_32 do reset_byte_index_cache nb := Utf8.character_byte_count (c) new_byte_count := nb * count if new_byte_count > byte_capacity then resize_byte_storage (new_byte_count) end byte_count := new_byte_count if nb = 1 then from i := 1 until i > new_byte_count loop put_byte (c, i) i := i + 1 end else from i := 1 until i > new_byte_count loop put_character_at_byte_index (c, nb, i) i := i + nb end end ensure -- from STRING_8 same_count: (count = old count) and (byte_capacity = old byte_capacity) filled: Elks_checking implies occurrences (c) = count ensure then all_code: code_occurrences (c.code) = count end fill_with_code (a_code: INTEGER_32) -- Replace every character with unicode character of code a_code. require valid_code: Unicode.valid_code (a_code) local i, nb: INTEGER_32 new_byte_count: INTEGER_32 do reset_byte_index_cache nb := Utf8.code_byte_count (a_code) new_byte_count := nb * count if new_byte_count > byte_capacity then resize_byte_storage (new_byte_count) end byte_count := new_byte_count from i := 1 until i > new_byte_count loop put_code_at_byte_index (a_code, nb, i) i := i + nb end ensure same_count: old count = count filled: code_occurrences (a_code) = count end fill_with_unicode (c: UC_CHARACTER) -- Replace every character with unicode character c. require c_not_void: c /= Void do fill_with_code (c.code) ensure same_count: old count = count filled: unicode_occurrences (c) = count end gobo_append_substring (a_string: STRING_8; s, e: INTEGER_32) -- Append substring of a_string between indexes -- s and e at end of current string. require a_string_not_void: a_string /= Void s_large_enough: s >= 1 e_small_enough: e <= a_string.count valid_interval: s <= e + 1 local a_substring_count: INTEGER_32 k, nb: INTEGER_32 new_byte_count: INTEGER_32 str: STRING_8 do a_substring_count := e - s + 1 if a_substring_count /= 0 then if a_string = Current then str := cloned_string else str := a_string end nb := Utf8.substring_byte_count (str, s, e) k := byte_count + 1 new_byte_count := byte_count + nb if new_byte_count > byte_capacity then resize_byte_storage (new_byte_count) end byte_count := new_byte_count set_count (count + a_substring_count) put_substring_at_byte_index (str, s, e, nb, k) end ensure then appended: is_equal (old cloned_string + old a_string.substring (s, e)) end insert (s: STRING_8; i: INTEGER_32) obsolete "ELKS 2001: use `insert_string' instead. [2017-04-09]" -- Add s to left of position i in current string. require -- from STRING_8 string_exists: s /= Void index_small_enough: i <= count + 1 index_large_enough: i > 0 do insert_string (s, i) ensure -- from STRING_8 inserted: Elks_checking implies (Current ~ (old substring (1, i - 1) + old (s.twin) + old substring (i, count))) end insert_character (c: CHARACTER_8; i: INTEGER_32) -- Insert character c at index i, shifting -- characters between ranks i and count rightwards. -- (ELKS 2001 STRING) require -- from STRING_8 valid_insertion_index: 1 <= i and i <= count + 1 local k, nb: INTEGER_32 new_byte_count: INTEGER_32 do if i = count + 1 then append_character (c) else if count = byte_count then k := i else k := byte_index (i) end nb := Utf8.character_byte_count (c) new_byte_count := byte_count + nb if new_byte_count > byte_capacity then resize_byte_storage (new_byte_count) end set_count (count + 1) move_bytes_right (k, nb) put_character_at_byte_index (c, nb, k) end ensure -- from STRING_8 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)) ensure then code_inserted: item_code (i) = c.code end insert_code (a_code: INTEGER_32; i: INTEGER_32) -- Insert unicode character of code a_code -- at index i, shifting characters between -- ranks i and count rightwards. require valid_code: Unicode.valid_code (a_code) valid_insertion_index: 1 <= i and i <= count + 1 local k, nb: INTEGER_32 new_byte_count: INTEGER_32 do if i = count + 1 then append_item_code (a_code) else if count = byte_count then k := i else k := byte_index (i) end nb := Utf8.code_byte_count (a_code) new_byte_count := byte_count + nb if new_byte_count > byte_capacity then resize_byte_storage (new_byte_count) end set_count (count + 1) move_bytes_right (k, nb) put_code_at_byte_index (a_code, nb, k) end ensure one_more_character: count = old count + 1 inserted: item_code (i) = a_code stable_before_i: substring (1, i - 1).is_equal (old substring (1, i - 1)) stable_after_i: substring (i + 1, count).is_equal (old substring (i, count)) end insert_string (a_string: READABLE_STRING_8; i: INTEGER_32) -- Insert a_string at index i, shifting characters between ranks -- i and count rightwards. -- (ELKS 2001 STRING) require -- from STRING_8 string_exists: a_string /= Void valid_insertion_index: 1 <= i and i <= count + 1 require else string_not_void: a_string /= Void valid_insertion_index: 1 <= i and i <= count + 1 local a_string_count: INTEGER_32 k, nb: INTEGER_32 new_byte_count: INTEGER_32 str: STRING_8 do a_string_count := a_string.count if a_string_count /= 0 then if i = count + 1 then append_string (a_string) else if a_string = Current then str := cloned_string else str := a_string.as_string_8 end if count = byte_count then k := i else k := byte_index (i) end nb := Utf8.substring_byte_count (str, 1, a_string_count) new_byte_count := byte_count + nb if new_byte_count > byte_capacity then resize_byte_storage (new_byte_count) end move_bytes_right (k, nb) set_count (count + a_string_count) put_substring_at_byte_index (str, 1, a_string_count, nb, k) end end ensure -- from STRING_8 inserted: Elks_checking implies (Current ~ (old substring (1, i - 1) + old (a_string.twin) + old substring (i, count))) end insert_unicode_character (c: UC_CHARACTER; i: INTEGER_32) -- Insert unicode character c at index i, shifting -- characters between ranks i and count rightwards. require c_not_void: c /= Void valid_insertion_index: 1 <= i and i <= count + 1 do insert_code (c.code, i) ensure one_more_character: count = old count + 1 inserted: item_code (i) = c.code stable_before_i: substring (1, i - 1).is_equal (old substring (1, i - 1)) stable_after_i: substring (i + 1, count).is_equal (old substring (i, count)) end precede (c: CHARACTER_8) -- Add c at front. -- Was declared in STRING_8 as synonym of prepend_character. -- (from STRING_8) local l_area: like area do if count = byte_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 -- from STRING_8 new_count: count = old count + 1 end prepend (s: READABLE_STRING_8) -- Prepend a copy of s at front. require -- from STRING_8 argument_not_void: s /= Void do insert_string (s, 1) ensure -- from STRING_8 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. -- (from STRING_8) do prepend (b.out) end prepend_character (c: CHARACTER_8) -- Add c at front. -- Was declared in STRING_8 as synonym of precede. -- (from STRING_8) local l_area: like area do if count = byte_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 -- from STRING_8 new_count: count = old count + 1 end prepend_double (d: REAL_64) -- Prepend the string representation of d at front. -- (from STRING_8) do prepend (d.out) end prepend_integer (i: INTEGER_32) -- Prepend the string representation of i at front. -- (from STRING_8) do prepend (i.out) end prepend_real (r: REAL_32) -- Prepend the string representation of r at front. -- (from STRING_8) do prepend (r.out) end prepend_string (s: detachable STRING_8) -- Prepend a copy 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. -- (from STRING_8) 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_8} s as l_s8 then prepend (l_s8) 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)) 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 > byte_capacity then resize (l_new_size) end old_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)) end prepend_substring (s: READABLE_STRING_8; start_index, end_index: INTEGER_32) -- Prepend characters of s.substring (start_index, end_index) at front. -- (from STRING_8) require -- from STRING_8 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 > byte_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 -- from STRING_8 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 put (c: CHARACTER_8; i: INTEGER_32) -- Replace unicode character at index i by character c. -- (ELKS 2001 STRING) local k, nb: INTEGER_32 a_byte: CHARACTER_8 old_count, new_count: INTEGER_32 new_byte_count: INTEGER_32 do if count = byte_count then k := i old_count := 1 else k := byte_index (i) a_byte := byte_item (k) old_count := Utf8.encoded_byte_count (a_byte) end new_count := Utf8.character_byte_count (c) if new_count = old_count then elseif new_count < old_count then move_bytes_left (k + old_count, old_count - new_count) else nb := new_count - old_count new_byte_count := byte_count + nb if new_byte_count > byte_capacity then resize_byte_storage (new_byte_count) end move_bytes_right (k + old_count, nb) end put_character_at_byte_index (c, new_count, k) ensure then unicode_replaced: item_code (i) = c.code end put_item_code (a_code: INTEGER_32; i: INTEGER_32) -- Replace unicode character at index i -- by unicode character of code a_code. require valid_index: valid_index (i) valid_item_code: Unicode.valid_code (a_code) local k, nb: INTEGER_32 old_count, new_count: INTEGER_32 new_byte_count: INTEGER_32 a_byte: CHARACTER_8 do if count = byte_count then k := i old_count := 1 else k := byte_index (i) a_byte := byte_item (k) old_count := Utf8.encoded_byte_count (a_byte) end new_count := Utf8.code_byte_count (a_code) if new_count = old_count then elseif new_count < old_count then move_bytes_left (k + old_count, old_count - new_count) else nb := new_count - old_count new_byte_count := byte_count + nb if new_byte_count > byte_capacity then resize_byte_storage (new_byte_count) end move_bytes_right (k + old_count, nb) end put_code_at_byte_index (a_code, new_count, k) ensure stable_count: count = old count replaced: item_code (i) = a_code stable_before_i: substring (1, i - 1).is_equal (old substring (1, i - 1)) stable_after_i: substring (i + 1, count).is_equal (old substring (i + 1, count)) end put_string (a_string: STRING_8) -- Write a_string to output stream. require -- from KI_CHARACTER_OUTPUT_STREAM is_open_write: is_open_write a_string_not_void: a_string /= Void do append (a_string) end put_substring (a_string: STRING_8; s, e: INTEGER_32) -- Write substring of a_string between indexes -- s and e to output stream. require -- from KI_CHARACTER_OUTPUT_STREAM is_open_write: is_open_write a_string_not_void: a_string /= Void s_large_enough: s >= 1 e_small_enough: e <= a_string.count valid_interval: s <= e + 1 do gobo_append_substring (a_string, s, e) end put_unicode (c: UC_CHARACTER; i: INTEGER_32) -- Replace unicode character at index i by c. require valid_index: valid_index (i) c_not_void: c /= Void do put_item_code (c.code, i) ensure stable_count: count = old count replaced: item_code (i) = c.code stable_before_i: substring (1, i - 1).is_equal (old substring (1, i - 1)) stable_after_i: substring (i + 1, count).is_equal (old substring (i + 1, count)) end replace_blank -- Replace all current characters with blanks. -- (from STRING_8) do fill_with (' ') ensure -- from STRING_8 same_size: (count = old count) and (byte_capacity = old byte_capacity) all_blank: Elks_checking implies occurrences (' ') = count end replace_character (c: CHARACTER_8) obsolete "ELKS 2001: use `fill_with' instead'. [2017-05-31]" -- Replace every character with c. -- (from STRING_8) do fill_with (c) ensure -- from STRING_8 same_count: (count = old count) and (byte_capacity = old byte_capacity) filled: Elks_checking implies occurrences (c) = count end replace_substring (a_string: STRING_8; start_index, end_index: INTEGER_32) -- Replace the substring from start_index to end_index, -- inclusive, with a_string. -- (ELKS 2001 STRING) require -- from STRING_8 string_not_void: a_string /= Void valid_start_index: 1 <= start_index valid_end_index: end_index <= count meaningfull_interval: start_index <= end_index + 1 do replace_substring_by_string (a_string, start_index, end_index) ensure -- from STRING_8 new_count: count = old count + old a_string.count - end_index + start_index - 1 replaced: Elks_checking implies (Current ~ (old (substring (1, start_index - 1) + a_string + substring (end_index + 1, count)))) end replace_substring_all (original, new: like Current) -- Replace every occurrence of original with new. require -- from STRING_8 original_exists: original /= Void new_exists: new /= Void original_not_empty: not original.old_is_empty local l_byte_count, l_original_byte_count, l_new_byte_count: INTEGER_32 l_bytes, l_original_bytes: SPECIAL [CHARACTER_8] i, nb, l_diff: INTEGER_32 do if not is_empty then from i := 1 l_byte_count := byte_count l_original_byte_count := original.byte_count l_new_byte_count := new.byte_count l_bytes := area l_original_bytes := original.area until i + l_original_byte_count - 1 > l_byte_count loop if l_bytes.same_items (l_original_bytes, 0, i - 1, l_original_byte_count) then if l_new_byte_count = l_original_byte_count then elseif l_new_byte_count < l_original_byte_count then move_bytes_left (i + l_original_byte_count, l_original_byte_count - l_new_byte_count) else l_diff := l_new_byte_count - l_original_byte_count nb := l_byte_count + l_diff if nb > byte_capacity then resize_byte_storage (nb) l_bytes := area end move_bytes_right (i + l_original_byte_count, l_diff) end l_byte_count := byte_count l_bytes.copy_data (new.area, 0, i - 1, l_new_byte_count) set_count (count - original.count + new.count) i := i + l_new_byte_count else i := next_byte_index (i) end end end end replace_substring_by_string (a_string: STRING_8; start_index, end_index: INTEGER_32) -- Replace the substring from start_index to end_index, -- inclusive, with a_string. require a_string_not_void: a_string /= Void local a_string_count: INTEGER_32 k, nb: INTEGER_32 a_range: INTEGER_32 old_count, new_count: INTEGER_32 new_byte_count: INTEGER_32 str: STRING_8 do a_string_count := a_string.count if a_string_count = 0 then remove_substring (start_index, end_index) else if start_index = count + 1 then append_string (a_string) else if a_string = Current then str := cloned_string else str := a_string end a_range := end_index - start_index + 1 if count = byte_count then k := start_index old_count := a_range else k := byte_index (start_index) if end_index < start_index then old_count := 0 elseif end_index = count then old_count := byte_count - k + 1 else old_count := shifted_byte_index (k, a_range) - k end end new_count := Utf8.substring_byte_count (str, 1, a_string_count) if new_count = old_count then elseif new_count < old_count then move_bytes_left (k + old_count, old_count - new_count) else nb := new_count - old_count new_byte_count := byte_count + nb if new_byte_count > byte_capacity then resize_byte_storage (new_byte_count) end move_bytes_right (k + old_count, nb) end set_count (count + a_string_count - a_range) put_substring_at_byte_index (str, 1, a_string_count, new_count, k) end end end set (t: READABLE_STRING_8; n1, n2: INTEGER_32) -- Set current string to substring of t from indices n1 -- to n2, or to empty string if no such substring. -- (from STRING_8) require -- from STRING_8 argument_not_void: t /= Void local s: READABLE_STRING_8 do s := t.substring (n1, n2) area := s.area count := s.count reset_hash_codes ensure -- from STRING_8 is_substring: same_string (t.substring (n1, n2)) end subcopy (other: READABLE_STRING_8; 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. -- (from STRING_8) require -- from STRING_8 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 -- from STRING_8 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 {STRING_8} -- Element change share (other: STRING_8) -- Make current string share the text of other. -- Subsequent changes to the characters of current string -- will also affect other, and conversely. -- (from STRING_8) require -- from STRING_8 argument_not_void: other /= Void do area := other.area count := other.count reset_hash_codes ensure -- from STRING_8 shared_count: other.count = count shared_area: other.area = area end feature {NONE} -- Element change old_put (c: CHARACTER_8; i: INTEGER_32) -- Replace character at position i by c. -- (from STRING_8) 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 -- from STRING_8 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 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 keep_head (n: INTEGER_32) -- Remove all the characters except for the first n; -- if n > count, do nothing. -- (ELKS 2001 STRING) require -- from STRING_GENERAL non_negative_argument: n >= 0 do if n = 0 then byte_count := 0 set_count (0) elseif n < count then if count = byte_count then byte_count := n else byte_count := byte_index (n + 1) - 1 end set_count (n) 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 the characters except for the last n; -- if n > count, do nothing. -- (ELKS 2001 STRING) require -- from STRING_GENERAL non_negative_argument: n >= 0 local removed_byte_count: INTEGER_32 do if n = 0 then byte_count := 0 set_count (0) elseif n < count then if count = byte_count then removed_byte_count := byte_count - n else removed_byte_count := byte_index (count - n + 1) - 1 end move_bytes_left (removed_byte_count + 1, removed_byte_count) set_count (n) 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 prune (c: CHARACTER_8) -- Remove first occurrence of c, if any. -- (from STRING_8) require -- from COLLECTION prunable: prunable require else -- from STRING_8 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_8) -- Remove all occurrences of c. -- (from STRING_8) require -- from COLLECTION prunable: prunable require else -- from STRING_8 True local i, j, nb: INTEGER_32 l_area: like area l_char: CHARACTER_8 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 -- from STRING_8 changed_count: count = (old count) - (old occurrences (c)) end prune_all_leading (c: CHARACTER_8) -- Remove all leading occurrences of c. -- (from STRING_8) do from until old_is_empty or else item (1) /= c loop remove (1) end end prune_all_trailing (c: CHARACTER_8) -- Remove all trailing occurrences of c. -- (from STRING_8) do from until old_is_empty or else item (count) /= c loop remove (count) end end remove (i: INTEGER_32) -- Remove i-th character, shifting characters between -- ranks i + 1 and count leftwards. -- (ELKS 2001 STRING) require -- from STRING_GENERAL valid_index: valid_index (i) local k, nb: INTEGER_32 do if count = byte_count then k := i nb := 1 else k := byte_index (i) nb := Utf8.encoded_byte_count (byte_item (k)) end move_bytes_left (k + nb, nb) set_count (count - 1) 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 the first n characters; -- if n > count, remove all. -- (ELKS 2001 STRING) require -- from STRING_GENERAL n_non_negative: n >= 0 do if n >= count then wipe_out elseif n /= 0 then 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. -- (ELKS 2001 STRING) require -- from STRING_GENERAL valid_start_index: 1 <= start_index valid_end_index: end_index <= count meaningful_interval: start_index <= end_index + 1 local k, nb: INTEGER_32 s: INTEGER_32 a_count: INTEGER_32 do if start_index = end_index then remove (start_index) elseif start_index < end_index then a_count := end_index - start_index + 1 if count = byte_count then k := end_index + 1 nb := a_count else s := byte_index (start_index) if end_index = count then k := byte_count + 1 else k := shifted_byte_index (s, a_count) end nb := k - s end move_bytes_left (k, nb) set_count (count - a_count) end ensure -- from STRING_GENERAL removed: Elks_checking implies Current ~ (old substring (1, start_index - 1) + old substring (end_index + 1, count)) end remove_tail (n: INTEGER_32) -- Remove the last n characters; -- if n > count, remove all. -- (ELKS 2001 STRING) require -- from STRING_GENERAL n_non_negative: n >= 0 do if n >= count then wipe_out elseif n /= 0 then keep_head (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. -- (ELKS 2001 STRING) do byte_count := 0 set_count (0) end feature -- Resizing adapt_size -- Adapt the size to accommodate count characters. -- (from STRING_8) 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 (byte_capacity + additional_space) ensure -- from RESIZABLE increased_capacity: byte_capacity >= old byte_capacity + old additional_space end grow (newsize: INTEGER_32) -- Ensure that the capacity is at least newsize. -- (from STRING_8) require -- from RESIZABLE resizable: resizable do if newsize > byte_capacity then resize (newsize) end ensure -- from RESIZABLE new_capacity: byte_capacity >= newsize end resize (newsize: INTEGER_32) -- Rearrange string so that it can accommodate -- at least newsize characters. -- (from STRING_8) require -- from STRING_GENERAL new_size_large_enough: newsize >= count do area := area.aliased_resized_area_with_default ('%U', newsize + 1) ensure -- from STRING_GENERAL same_count: count = old count capacity_large_enough: byte_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. -- (from STRING_8) require -- from RESIZABLE True local n: like count do n := count if n < byte_capacity then area := area.aliased_resized_area (n + 1) end ensure -- from RESIZABLE same_count: count = old count minimal_capacity: byte_capacity = count ensure then -- from STRING_8 same_string: same_string (old twin) end feature -- Transformation correct_mismatch -- Attempt to correct object mismatch during retrieve using Mismatch_information. -- (from STRING_8) do end feature -- Conversion as_lower: like Current -- New object with all letters in lower case -- (Extended from ELKS 2001 STRING) require -- from READABLE_STRING_GENERAL True do Result := cloned_string Result.to_lower ensure -- from READABLE_STRING_GENERAL as_lower_attached: Result /= Void length: Result.count = count anchor: count > 0 implies Result.character_32_item (1) = character_32_item (1).as_lower recurse: count > 1 implies Result.substring (2, count) ~ substring (2, count).as_lower ensure then unicode_anchor: count > 0 implies Result.unicode_item (1).is_equal (unicode_item (1).as_lower) unicode_recurse: count > 1 implies Result.substring (2, count).is_equal (substring (2, count).as_lower) end as_readable_string_32: READABLE_STRING_32 obsolete "Use explicit conversion `to_string_32' instead. [2017-05-31]" -- (from READABLE_STRING_GENERAL) do Result := as_string_32 end as_readable_string_8: READABLE_STRING_8 obsolete "Use explicit conversion `to_string_8' instead. [2017-05-31]" -- (from READABLE_STRING_GENERAL) do Result := as_string_8 end as_string: STRING_8 -- STRING version of current string; -- Return the UTF8 representation if it is encoded -- with UTF8, the UTF16 representation if it is -- encoded with UTF16, etc. do Result := to_utf8 ensure as_string_not_void: Result /= Void string_type: Any_.same_types (Result, "") 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 -- 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 -- (Extended from ELKS 2001 STRING) require -- from READABLE_STRING_GENERAL True do Result := cloned_string Result.to_upper ensure -- from READABLE_STRING_GENERAL as_upper_attached: Result /= Void length: Result.count = count anchor: count > 0 implies Result.character_32_item (1) = character_32_item (1).as_upper recurse: count > 1 implies Result.substring (2, count) ~ substring (2, count).as_upper ensure then unicode_anchor: count > 0 implies Result.unicode_item (1).is_equal (unicode_item (1).as_upper) unicode_recurse: count > 1 implies Result.substring (2, count).is_equal (substring (2, count).as_upper) end center_justify -- Center justify Current using count as width. -- (from STRING_8) local i, nb, l_offset: INTEGER_32 left_nb_space, right_nb_space: INTEGER_32 l_area: like area do from nb := count l_area := area until left_nb_space = nb or else not l_area.item (left_nb_space).is_space loop left_nb_space := left_nb_space + 1 end from i := nb - 1 l_area := area until i = -1 or else not l_area.item (i).is_space 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 (' ', left_nb_space, left_nb_space - l_offset - 1) else l_area.fill_with (' ', nb - right_nb_space - l_offset, nb - 1) end reset_hash_codes end end character_justify (pivot: CHARACTER_8; 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. -- (from STRING_8) require -- from STRING_8 valid_position: position <= byte_capacity positive_position: position >= 1 pivot_not_space: pivot /= ' ' not_empty: not old_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 (' ', 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 (' ', count - l_index_of_pivot + position, count - 1) end reset_hash_codes end end left_justify -- Left justify Current using count as witdth. -- (from STRING_8) local i, nb: INTEGER_32 l_area: like area do nb := count old_left_adjust i := count if i < nb then from l_area := area until i = nb loop l_area.put (' ', i) i := i + 1 end count := nb reset_hash_codes end end linear_representation: LINEAR [CHARACTER_8] -- Representation as a linear structure -- (from STRING_8) local temp: ARRAYED_LIST [CHARACTER_8] i: INTEGER_32 do create temp.make (byte_capacity) from i := 1 until i > count loop temp.extend (item (i)) i := i + 1 end Result := temp end mirrored: UC_STRING -- Mirror image of string; -- Result for "Hello world" is "dlrow olleH". -- (from STRING_8) do Result := twin if count > 0 then Result.mirror end ensure -- from READABLE_STRING_8 same_count: Result.count = count end right_justify -- Right justify Current using count as width. -- (from STRING_8) local i, nb: INTEGER_32 nb_space: INTEGER_32 l_area: like area do nb := count old_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 (' ', nb_space) end count := nb reset_hash_codes end ensure -- from STRING_8 same_count: count = old count end split (a_separator: CHARACTER_32): LIST [UC_STRING] -- Split on a_separator. -- (from READABLE_STRING_GENERAL) local l_list: ARRAYED_LIST [UC_STRING] 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 := character_32_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: character_32_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 = character_32_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. -- (from STRING_8) require -- from STRING_8 not_is_dotnet: not {PLATFORM}.is_dotnet local l_area: like area do l_area := area l_area.put ('%U', 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 all letters to lower case. -- (ELKS 2001 STRING) local i, nb: INTEGER_32 old_count, new_count: INTEGER_32 new_byte_count: INTEGER_32 a_code, new_code: INTEGER_32 do nb := byte_count from i := 1 until i > nb loop a_code := item_code_at_byte_index (i) new_code := Unicode.lower_code (a_code) if new_code /= a_code then old_count := Utf8.code_byte_count (a_code) new_count := Utf8.code_byte_count (new_code) if new_count = old_count then elseif new_count < old_count then move_bytes_left (i + old_count, old_count - new_count) else nb := new_count - old_count new_byte_count := byte_count + nb if new_byte_count > byte_capacity then resize_byte_storage (new_byte_count) end move_bytes_right (i + old_count, nb) end put_code_at_byte_index (new_code, new_count, i) end i := next_byte_index (i) end ensure -- from STRING_8 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_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 do Result := as_string_8 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 all letters to upper case. -- (ELKS 2001 STRING) local i, nb: INTEGER_32 old_count, new_count: INTEGER_32 new_byte_count: INTEGER_32 a_code, new_code: INTEGER_32 do nb := byte_count from i := 1 until i > nb loop a_code := item_code_at_byte_index (i) new_code := Unicode.upper_code (a_code) if new_code /= a_code then old_count := Utf8.code_byte_count (a_code) new_count := Utf8.code_byte_count (new_code) if new_count = old_count then elseif new_count < old_count then move_bytes_left (i + old_count, old_count - new_count) else nb := new_count - old_count new_byte_count := byte_count + nb if new_byte_count > byte_capacity then resize_byte_storage (new_byte_count) end move_bytes_right (i + old_count, nb) end put_code_at_byte_index (new_code, new_count, i) end i := next_byte_index (i) end ensure -- from STRING_8 length_and_content: Elks_checking implies Current ~ (old as_upper) end to_utf16_be: STRING_8 -- New STRING made up of bytes corresponding to -- the UTF-16BE representation of current string local i, nb, a_code, a_high, a_low, a_surrogate: INTEGER_32 do nb := byte_count create Result.make (nb) from i := 1 until i > nb loop a_code := item_code_at_byte_index (i) if Unicode.is_bmp_code (a_code) then a_high := a_code // 256 a_low := a_code \\ 256 Result.append_character (Integer_.to_character (a_high)) Result.append_character (Integer_.to_character (a_low)) else a_surrogate := Utf16.supplementary_to_high_surrogate (a_code) a_high := a_surrogate // 256 a_low := a_surrogate \\ 256 Result.append_character (Integer_.to_character (a_high)) Result.append_character (Integer_.to_character (a_low)) a_surrogate := Utf16.supplementary_to_low_surrogate (a_code) a_high := a_surrogate // 256 a_low := a_surrogate \\ 256 Result.append_character (Integer_.to_character (a_high)) Result.append_character (Integer_.to_character (a_low)) end i := next_byte_index (i) end ensure to_utf16_be_not_void: Result /= Void string_type: Any_.same_types (Result, "") valid_utf16: Utf16.valid_utf16 (Result) end to_utf16_le: STRING_8 -- New STRING made up of bytes corresponding to -- the UTF-16LE representation of current string local i, nb, a_code, a_high, a_low, a_surrogate: INTEGER_32 do nb := byte_count create Result.make (nb) from i := 1 until i > nb loop a_code := item_code_at_byte_index (i) if Unicode.is_bmp_code (a_code) then a_high := a_code // 256 a_low := a_code \\ 256 Result.append_character (Integer_.to_character (a_low)) Result.append_character (Integer_.to_character (a_high)) else a_surrogate := Utf16.supplementary_to_high_surrogate (a_code) a_high := a_surrogate // 256 a_low := a_surrogate \\ 256 Result.append_character (Integer_.to_character (a_low)) Result.append_character (Integer_.to_character (a_high)) a_surrogate := Utf16.supplementary_to_low_surrogate (a_code) a_high := a_surrogate // 256 a_low := a_surrogate \\ 256 Result.append_character (Integer_.to_character (a_low)) Result.append_character (Integer_.to_character (a_high)) end i := next_byte_index (i) end ensure to_utf16_le_not_void: Result /= Void string_type: Any_.same_types (Result, "") valid_utf16: Utf16.valid_utf16 (Utf16.Bom_le + Result) end to_utf32_be: STRING_8 -- New STRING made up of bytes corresponding to -- the UTF-32BE representation of current string local i, j, k, l, m, nb, a_code: INTEGER_32 do nb := byte_count create Result.make (4 * count) from i := 1 until i > nb loop a_code := item_code_at_byte_index (i) m := a_code \\ 256 a_code := a_code // 256 l := a_code \\ 256 a_code := a_code // 256 j := a_code // 256 k := a_code \\ 256 Result.append_character (Integer_.to_character (j)) Result.append_character (Integer_.to_character (k)) Result.append_character (Integer_.to_character (l)) Result.append_character (Integer_.to_character (m)) i := next_byte_index (i) end ensure to_utf32_be_not_void: Result /= Void string_type: Any_.same_types (Result, "") valid_utf32: Utf32.valid_utf32 (Result) end to_utf32_le: STRING_8 -- New STRING made up of bytes corresponding to -- the UTF-32LE representation of current string local i, j, k, l, m, nb, a_code: INTEGER_32 do nb := byte_count create Result.make (4 * count) from i := 1 until i > nb loop a_code := item_code_at_byte_index (i) m := a_code \\ 256 a_code := a_code // 256 l := a_code \\ 256 a_code := a_code // 256 j := a_code // 256 k := a_code \\ 256 Result.append_character (Integer_.to_character (m)) Result.append_character (Integer_.to_character (l)) Result.append_character (Integer_.to_character (k)) Result.append_character (Integer_.to_character (j)) i := next_byte_index (i) end ensure to_utf32_le_not_void: Result /= Void string_type: Any_.same_types (Result, "") valid_utf32: Utf32.valid_utf32 (Utf32.Bom_le + Result) end to_utf8: STRING_8 -- New STRING made up of bytes corresponding to -- the UTF-8 representation of current string local i, nb: INTEGER_32 do nb := byte_count create Result.make (nb) from i := 1 until i > nb loop Result.append_character (byte_item (i)) i := i + 1 end ensure to_utf8_not_void: Result /= Void string_type: Any_.same_types (Result, "") valid_utf8: Utf8.valid_utf8 (Result) end feature {STRING_8} -- Conversion mirror -- Reverse the order of characters. -- "Hello world" -> "dlrow olleH". -- (from STRING_8) local a: like area c: CHARACTER_8 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 -- from STRING_8 same_count: count = old count 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 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 cloned_string: like Current -- New object equal to Current do Result := twin ensure twin_not_void: Result /= Void is_equal: Result.is_equal (Current) end copy (other: like Current) -- Reinitialize by copying the characters of other. -- (This is also used by clone.) -- (ELKS 2001 STRING) require -- from ANY other_not_void: other /= Void type_identity: same_type (other) local other_count: INTEGER_32 do if other /= Current then other_count := other.count other.set_count (other.byte_count) Precursor {KL_STRING} (other) set_count (other_count) other.set_count (other_count) end ensure -- from ANY is_equal: Current ~ other ensure then -- from READABLE_STRING_8 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: UC_STRING) -- 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: UC_STRING -- 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): UC_STRING -- 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" -- (from STRING_8) require -- from STRING_8 meaningful_multiplier: n >= 1 local s: UC_STRING 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: UC_STRING) -- 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: UC_STRING -- 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 tail (n: INTEGER_32): UC_STRING -- 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: UC_STRING -- 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 UC_STRING 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 close -- Try to close output stream if it is closable. Set -- is_open_write to false if operation was successful. -- (from KI_OUTPUT_STREAM) require -- from KI_OUTPUT_STREAM is_closable: is_closable do end frozen default: detachable UC_STRING -- Default value of object's type -- (from ANY) do end frozen default_pointer: POINTER -- Default value of type POINTER -- (Avoid the need to write p.default for -- some p of type POINTER.) -- (from ANY) do ensure -- from ANY instance_free: class end default_rescue -- Process exception for routines with no Rescue clause. -- (Default: do nothing.) -- (from ANY) do end frozen do_nothing -- Execute a null action. -- (from ANY) do ensure -- from ANY instance_free: class end feature {NONE} -- Inapplicable bag_put (v: CHARACTER_8) -- Ensure that structure includes v. -- (from TABLE) require -- from COLLECTION extendible: Extendible do ensure -- from COLLECTION item_inserted: is_inserted (v) end old_clear_all -- Remove all characters. do wipe_out ensure -- from STRING_8 is_empty: count = 0 same_capacity: byte_capacity = old byte_capacity end old_wipe_out -- Remove all characters. -- (ELKS 2001 STRING) require -- from STRING_GENERAL True require -- from COLLECTION prunable: prunable do count := 0 Precursor wipe_out ensure -- from STRING_GENERAL is_empty: count = 0 same_capacity: byte_capacity = old byte_capacity ensure -- from COLLECTION wiped_out: old_is_empty end feature {UC_STRING} -- Inapplicable append_code (c: like code) -- Append c at end. require -- from STRING_GENERAL valid_code: valid_code (c) do append_item_code (c.as_integer_32) 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 code (i: INTEGER_32): NATURAL_32 -- Code at position i require -- from READABLE_STRING_GENERAL valid_index: valid_index (i) do Result := item_code (i).as_natural_32 end has_code (c: like code): BOOLEAN -- Does string include c? do Result := has_item_code (c.as_integer_32) 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 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. require -- from READABLE_STRING_GENERAL start_large_enough: start_index >= 1 start_small_enough: start_index <= count + 1 do Result := index_of_item_code (c.as_integer_32, start_index) 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 old_left_adjust -- Remove leading whitespace. require -- from STRING_GENERAL True local i, nb: INTEGER_32 do nb := count from i := 1 until i > nb loop inspect item (i) when ' ', '%T', '%R', '%N' then i := i + 1 else nb := 0 end end remove_head (i - 1) ensure -- from STRING_GENERAL valid_count: count <= old count new_count: not old_is_empty implies not character_32_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 old_right_adjust -- Remove trailing whitespace. require -- from STRING_GENERAL True local i, nb: INTEGER_32 do nb := count from i := 1 until i > nb loop inspect item (nb) when ' ', '%T', '%R', '%N' then nb := nb - 1 else i := nb + 1 end end keep_head (nb) ensure -- from STRING_GENERAL valid_count: count <= old count new_count: not old_is_empty implies not character_32_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 put_code (v: like code; i: INTEGER_32) -- Put code v at position i. require -- from STRING_GENERAL valid_code: valid_code (v) valid_index: valid_index (i) do put_item_code (v.as_integer_32, i) 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 feature -- Implementation current_string: STRING_8 -- Current string do Result := Current end feature {UC_STRING_HANDLER} -- Implementation byte_item (i: INTEGER_32): CHARACTER_8 -- Byte at index i require i_large_enough: i >= 1 i_small_enough: i <= byte_count local old_count: INTEGER_32 do old_count := count set_count (byte_count) Result := old_item (i) set_count (old_count) end move_bytes_left (i, offset: INTEGER_32) -- Move bytes at and after position i -- by offset positions to the left. require valid_index: 1 <= i and i <= byte_count + 1 positive_offset: offset >= 0 constraint: offset < i local j, nb: INTEGER_32 old_count: INTEGER_32 do if last_byte_index_result > i - offset then reset_byte_index_cache end from j := i nb := byte_count old_count := count set_count (byte_count) until j > nb loop old_put (old_item (j), j - offset) j := j + 1 end set_count (old_count) byte_count := byte_count - offset ensure byte_count_set: byte_count = old byte_count - offset end move_bytes_right (i, offset: INTEGER_32) -- Move bytes at and after position i -- by offset positions to the right. require valid_index: 1 <= i and i <= byte_count + 1 positive_offset: offset >= 0 offset_small_enough: offset <= (byte_capacity - byte_count) local j, nb: INTEGER_32 old_count: INTEGER_32 do if last_byte_index_result > i then reset_byte_index_cache end from j := byte_count nb := i byte_count := byte_count + offset old_count := count set_count (byte_count) until j < nb loop old_put (old_item (j), j + offset) j := j - 1 end set_count (old_count) ensure byte_count_set: byte_count = old byte_count + offset end put_byte (c: CHARACTER_8; i: INTEGER_32) -- Replace byte at index i by c. require i_large_enough: i >= 1 i_small_enough: i <= byte_count local old_count: INTEGER_32 do old_count := count set_count (byte_count) old_put (c, i) set_count (old_count) end resize_byte_storage (n: INTEGER_32) -- Resize space for n bytes. -- Do not lose previously stored bytes. require n_large_enough: n >= byte_capacity local old_count: INTEGER_32 do if n > byte_capacity then resize (n) old_count := count set_count (n) old_set_count (n) set_count (old_count) end ensure byte_capacity_set: byte_capacity = n end set_byte_count (nb: INTEGER_32) -- Set byte_count to nb. require nb_large_enough: nb >= 0 nb_small_enough: nb <= byte_capacity do if last_byte_index_result > nb then reset_byte_index_cache end byte_count := nb ensure byte_count_set: byte_count = nb end set_count (nb: INTEGER_32) -- Set count to nb. require nb_positive: nb >= 0 do if last_byte_index_input > nb then reset_byte_index_cache end count := nb ensure count_set: count = nb 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 Dummy_string: STRING_8 = "" -- Dummy string Dummy_uc_string: UC_STRING -- Dummy Unicode string once create Result.make_empty ensure instance_free: class dummy_uc_string_not_void: Result /= Void end empty_area: SPECIAL [CHARACTER_8] obsolete "Simply create `area' directly. [2017-05-31]" -- Empty area to avoid useless creation of empty areas when wiping out a STRING. -- (from STRING_8) do create Result.make_empty (1) Result.extend ('%U') ensure -- from STRING_8 empty_area_not_void: Result /= Void end Stream_false_constant: STRING_8 = "False" -- String representation of boolean value 'False' -- (from KI_CHARACTER_OUTPUT_STREAM) 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_8) require -- from READABLE_STRING_8 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_8 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): UC_STRING -- New instance of current with space for at least n characters. -- (from STRING_8) 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.old_is_empty new_string_area_big_enough: Result.byte_capacity >= n end put_character_at_byte_index (c: CHARACTER_8; b: INTEGER_32; i: INTEGER_32) -- Put character c at byte index i. -- b is the number of bytes necessary to encode c. require i_large_enough: i >= 1 enough_space: (i + b - 1) <= byte_count local a_byte: CHARACTER_8 a_code: INTEGER_32 do check valid_utf8: b = Utf8.character_byte_count (c) end inspect b when 1 then put_byte (c, i) when 2 then a_code := c.code a_byte := Integer_.to_character ((a_code // 64) + 192) put_byte (a_byte, i) a_byte := Integer_.to_character ((a_code \\ 64) + 128) put_byte (a_byte, i + 1) else put_code_at_byte_index (c.code, b, i) end end put_code_at_byte_index (a_code: INTEGER_32; b: INTEGER_32; i: INTEGER_32) -- Put unicode character of code a_code -- at byte index i. b is the number of -- bytes necessary to encode this character. require i_large_enough: i >= 1 enough_space: (i + b - 1) <= byte_count valid_code: Unicode.valid_code (a_code) local j: INTEGER_32 a_byte: CHARACTER_8 c: INTEGER_32 do check valid_utf8: b = Utf8.code_byte_count (a_code) end from c := a_code j := i + b - 1 until j = i loop a_byte := Integer_.to_character ((c \\ 64) + 128) put_byte (a_byte, j) c := c // 64 j := j - 1 end inspect b when 1 then a_byte := Integer_.to_character (c) when 2 then a_byte := Integer_.to_character (c + 192) when 3 then a_byte := Integer_.to_character (c + 224) when 4 then a_byte := Integer_.to_character (c + 240) when 5 then a_byte := Integer_.to_character (c + 248) when 6 then a_byte := Integer_.to_character (c + 252) end put_byte (a_byte, i) end put_substring_at_byte_index (a_string: STRING_GENERAL; start_index, end_index, b: INTEGER_32; i: INTEGER_32) -- Put characters of a_string between start_index -- and end_index at byte index i. b is the number -- of bytes necessary to encode these characters. require a_string_not_void: a_string /= Void a_string_not_current: a_string /= Current valid_start_index: 1 <= start_index valid_end_index: end_index <= a_string.count meaningful_interval: start_index <= end_index + 1 i_large_enough: i >= 1 enough_space: (i + b - 1) <= byte_count local j, nb: INTEGER_32 k, z: INTEGER_32 c: CHARACTER_8 a_code: INTEGER_32 do check valid_utf8: b = Utf8.substring_byte_count (a_string, start_index, end_index) end if b > 0 then if attached {STRING_8} a_string as l_string_8 and then Any_.same_types (a_string, Dummy_string) then nb := end_index - start_index + 1 if nb = b then k := i from j := start_index until j > end_index loop put_byte (l_string_8.item (j), k) k := k + 1 j := j + 1 end else k := i from j := start_index until j > end_index loop c := l_string_8.item (j) z := Utf8.character_byte_count (c) put_character_at_byte_index (c, z, k) k := k + z j := j + 1 end end elseif Any_.same_types (a_string, Current) and attached {UC_STRING} a_string as a_uc_string then k := i j := a_uc_string.byte_index (start_index) nb := j + b - 1 from until j > nb loop put_byte (a_uc_string.byte_item (j), k) k := k + 1 j := j + 1 end elseif attached {UC_UTF8_STRING} a_string as a_utf8_string then k := i j := a_utf8_string.byte_index (start_index) nb := j + b - 1 from until j > nb loop put_byte (a_utf8_string.byte_item (j), k) k := k + 1 j := j + 1 end elseif attached {UC_STRING} a_string as a_uc_string then k := i j := a_uc_string.byte_index (start_index) nb := j + b - 1 from until j > nb loop a_code := a_uc_string.item_code_at_byte_index (j) z := Utf8.code_byte_count (a_code) put_code_at_byte_index (a_code, z, k) k := k + z j := a_uc_string.next_byte_index (j) end else k := i from j := start_index until j > end_index loop a_code := a_string.code (j).to_integer_32 z := Utf8.code_byte_count (a_code) put_code_at_byte_index (a_code, z, k) k := k + z j := j + 1 end end end 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_8) require -- from READABLE_STRING_8 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_8_SEARCHER -- String searcher specialized for READABLE_STRING_8 instances. -- (from READABLE_STRING_8) 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. -- (from READABLE_STRING_8) require -- from READABLE_STRING_8 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 do from i := start_index until i > end_index loop a.put (a.item (i).lower, i) 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. -- (from READABLE_STRING_8) require -- from READABLE_STRING_8 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 do from i := start_index until i > end_index loop a.put (a.item (i).upper, i) i := i + 1 end end Stream_true_constant: STRING_8 = "True" -- String representation of boolean value 'True' -- (from KI_CHARACTER_OUTPUT_STREAM) feature {STRING_HANDLER} -- Implementation frozen old_set_count (number: INTEGER_32) -- Set count to number of characters. -- (from STRING_8) require -- from STRING_GENERAL valid_count: 0 <= number and number <= byte_capacity do count := number reset_hash_codes ensure -- from STRING_GENERAL new_count: count = number 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_8_ITERATION_CURSOR} -- Implementation area_lower: INTEGER_32 -- Minimum index. -- (from READABLE_STRING_8) do ensure -- from READABLE_STRING_8 area_lower_non_negative: Result >= 0 area_lower_valid: Result <= area.upper end area_upper: INTEGER_32 -- Maximum index. -- (from READABLE_STRING_8) do Result := area_lower + count - 1 ensure -- from READABLE_STRING_8 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 {UC_STRING} -- Byte index cache last_byte_index_input: INTEGER_32 -- Last byte_index requested -- (Cache for 'i := i + 1' iterations and similar) last_byte_index_result: INTEGER_32 -- Last byte_index Result -- (Cache for 'i := i + 1' iterations and similar) reset_byte_index_cache -- Reset byte index (after write operation for example). do last_byte_index_input := 1 last_byte_index_result := 1 end feature -- Correction Mismatch_information: MISMATCH_INFORMATION -- Original attribute values of mismatched object -- (from MISMATCH_CORRECTOR) once create Result end feature -- Output append_stream (an_input_stream: KI_INPUT_STREAM [CHARACTER_8]) -- Read items of an_input_stream until the end -- of input is reached, and write these items to -- current output stream. -- (from KI_CHARACTER_OUTPUT_STREAM) require -- from KI_OUTPUT_STREAM is_open_write: is_open_write an_input_stream_not_void: an_input_stream /= Void an_input_stream_open_read: an_input_stream.is_open_read do if attached {KI_CHARACTER_INPUT_STREAM} an_input_stream as a_character_input then from if not a_character_input.end_of_input then a_character_input.read_string (512) end until a_character_input.end_of_input loop put_string (a_character_input.last_string) a_character_input.read_string (512) end else Precursor (an_input_stream) end ensure -- from KI_OUTPUT_STREAM end_of_input: an_input_stream.end_of_input end debug_output: STRING_8 -- String that should be displayed in debugger to represent Current. do Result := out ensure -- from DEBUG_OUTPUT result_not_void: Result /= Void end Io: STD_FILES -- Handle to standard file setup -- (from ANY) once create Result Result.set_output_default ensure -- from ANY instance_free: class io_not_void: Result /= Void end out: STRING_8 -- New STRING containing terse printable representation -- of current object; Non-ascii characters are represented -- with the %/code/ convention. -- (ELKS 2001 STRING) require -- from ANY True local i, nb: INTEGER_32 a_code: INTEGER_32 c: CHARACTER_8 max_ascii_char: CHARACTER_8 max_ascii_code: INTEGER_32 do nb := count create Result.make (nb) if nb = byte_count then max_ascii_char := Unicode.Maximum_ascii_character from i := 1 until i > nb loop c := byte_item (i) if c <= max_ascii_char then Result.append_character (c) else Result.append_character ('%%') Result.append_character ('/') Result.append_string (c.code.out) Result.append_character ('/') end i := i + 1 end else nb := byte_count max_ascii_code := Unicode.Maximum_ascii_character_code from i := 1 until i > nb loop a_code := item_code_at_byte_index (i) if a_code <= max_ascii_code then Result.append_character (Integer_.to_character (a_code)) else Result.append_character ('%%') Result.append_character ('/') Result.append_string (a_code.out) Result.append_character ('/') end i := next_byte_index (i) end end ensure -- from ANY out_not_void: Result /= Void ensure then -- from READABLE_STRING_8 out_not_void: Result /= Void same_items: same_type ("") implies Result.same_string (Current) end print (o: detachable ANY) -- Write terse external representation of o -- on standard output. -- (from ANY) do if o /= Void then Io.put_string (o.out) end ensure -- from ANY instance_free: class end put_boolean (b: BOOLEAN) -- Write "True" to output stream if -- b is true, "False" otherwise. -- (from KI_CHARACTER_OUTPUT_STREAM) require -- from KI_CHARACTER_OUTPUT_STREAM is_open_write: is_open_write do if b then put_string (Stream_true_constant) else put_string (Stream_false_constant) end end put_integer (i: INTEGER_32) -- Write decimal representation -- of i to output stream. -- Regexp: 0|(-?[1-9][0-9]*) -- (from KI_CHARACTER_OUTPUT_STREAM) require -- from KI_CHARACTER_OUTPUT_STREAM is_open_write: is_open_write do put_integer_64 (i.to_integer_64) end put_integer_16 (i: INTEGER_16) -- Write decimal representation -- of i to output stream. -- Regexp: 0|(-?[1-9][0-9]*) -- (from KI_CHARACTER_OUTPUT_STREAM) require -- from KI_CHARACTER_OUTPUT_STREAM is_open_write: is_open_write do put_integer_64 (i.to_integer_64) end put_integer_32 (i: INTEGER_32) -- Write decimal representation -- of i to output stream. -- Regexp: 0|(-?[1-9][0-9]*) -- (from KI_CHARACTER_OUTPUT_STREAM) require -- from KI_CHARACTER_OUTPUT_STREAM is_open_write: is_open_write do put_integer_64 (i.to_integer_64) end put_integer_64 (i: INTEGER_64) -- Write decimal representation -- of i to output stream. -- Regexp: 0|(-?[1-9][0-9]*) -- (from KI_CHARACTER_OUTPUT_STREAM) require -- from KI_CHARACTER_OUTPUT_STREAM is_open_write: is_open_write local k, j: INTEGER_64 do if i = 0 then append_character ('0') elseif i < 0 then append_character ('-') k := - (i + 1) j := k // 10 inspect k \\ 10 when 0 then if j /= 0 then put_integer_64 (j) end append_character ('1') when 1 then if j /= 0 then put_integer_64 (j) end append_character ('2') when 2 then if j /= 0 then put_integer_64 (j) end append_character ('3') when 3 then if j /= 0 then put_integer_64 (j) end append_character ('4') when 4 then if j /= 0 then put_integer_64 (j) end append_character ('5') when 5 then if j /= 0 then put_integer_64 (j) end append_character ('6') when 6 then if j /= 0 then put_integer_64 (j) end append_character ('7') when 7 then if j /= 0 then put_integer_64 (j) end append_character ('8') when 8 then if j /= 0 then put_integer_64 (j) end append_character ('9') when 9 then put_integer_64 (j + 1) append_character ('0') end else k := i j := k // 10 if j /= 0 then put_integer_64 (j) end inspect k \\ 10 when 0 then append_character ('0') when 1 then append_character ('1') when 2 then append_character ('2') when 3 then append_character ('3') when 4 then append_character ('4') when 5 then append_character ('5') when 6 then append_character ('6') when 7 then append_character ('7') when 8 then append_character ('8') when 9 then append_character ('9') end end end put_integer_8 (i: INTEGER_8) -- Write decimal representation -- of i to output stream. -- Regexp: 0|(-?[1-9][0-9]*) -- (from KI_CHARACTER_OUTPUT_STREAM) require -- from KI_CHARACTER_OUTPUT_STREAM is_open_write: is_open_write do put_integer_64 (i.to_integer_64) end put_line (a_string: STRING_8) -- Write a_string to output stream -- followed by a line separator. -- (from KI_TEXT_OUTPUT_STREAM) require -- from KI_TEXT_OUTPUT_STREAM is_open_write: is_open_write a_string_not_void: a_string /= Void do put_string (a_string) put_new_line end put_natural_16 (i: NATURAL_16) -- Write decimal representation -- of i to output stream. -- Regexp: 0|([1-9][0-9]*) -- (from KI_CHARACTER_OUTPUT_STREAM) require -- from KI_CHARACTER_OUTPUT_STREAM is_open_write: is_open_write do put_natural_64 (i.to_natural_64) end put_natural_32 (i: NATURAL_32) -- Write decimal representation -- of i to output stream. -- Regexp: 0|([1-9][0-9]*) -- (from KI_CHARACTER_OUTPUT_STREAM) require -- from KI_CHARACTER_OUTPUT_STREAM is_open_write: is_open_write do put_natural_64 (i.to_natural_64) end put_natural_64 (i: NATURAL_64) -- Write decimal representation -- of i to output stream. -- Regexp: 0|([1-9][0-9]*) -- (from KI_CHARACTER_OUTPUT_STREAM) require -- from KI_CHARACTER_OUTPUT_STREAM is_open_write: is_open_write local k, j: NATURAL_64 do if i = 0 then append_character ('0') else k := i j := k // 10 if j /= 0 then put_natural_64 (j) end inspect k \\ 10 when 0 then append_character ('0') when 1 then append_character ('1') when 2 then append_character ('2') when 3 then append_character ('3') when 4 then append_character ('4') when 5 then append_character ('5') when 6 then append_character ('6') when 7 then append_character ('7') when 8 then append_character ('8') when 9 then append_character ('9') end end end put_natural_8 (i: NATURAL_8) -- Write decimal representation -- of i to output stream. -- Regexp: 0|([1-9][0-9]*) -- (from KI_CHARACTER_OUTPUT_STREAM) require -- from KI_CHARACTER_OUTPUT_STREAM is_open_write: is_open_write do put_natural_64 (i.to_natural_64) end put_new_line -- Write a line separator to output stream. -- (from KI_TEXT_OUTPUT_STREAM) require -- from KI_TEXT_OUTPUT_STREAM is_open_write: is_open_write do put_string (Eol) 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 -- Output stream Eol: STRING_8 = "%N" -- Line separator flush -- Do nothing (operation does not apply to string). require -- from KI_CHARACTER_OUTPUT_STREAM is_open_write: is_open_write do end is_open_write: BOOLEAN -- Can characters be written to output stream? do Result := True end Name: STRING_8 = "UC_STRING" -- Name of output stream 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_8 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: ") create l_exc l_msg.append (generating_type.name) 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 feature -- Traversal byte_index (i: INTEGER_32): INTEGER_32 -- Byte index of character at index i require valid_index: valid_index (i) local j: INTEGER_32 a_byte: CHARACTER_8 do if byte_count = count then Result := i else from if i < last_byte_index_input then j := 1 Result := 1 else j := last_byte_index_input Result := last_byte_index_result end invariant j <= i until j = i loop a_byte := byte_item (Result) Result := Result + Utf8.encoded_byte_count (a_byte) j := j + 1 end end last_byte_index_input := i last_byte_index_result := Result ensure byte_index_large_enough: Result >= 1 byte_index_small_enough: Result <= byte_count is_encoded_first_byte: is_encoded_first_byte (Result) end character_item_at_byte_index (i: INTEGER_32): CHARACTER_8 -- Character at byte_index i; -- '%U' is the unicode character at byte index -- i cannot fit into a CHARACTER require i_large_enough: i >= 1 i_small_enough: i <= byte_count is_encoded_first_byte: is_encoded_first_byte (i) local a_byte: CHARACTER_8 a_code: INTEGER_32 do a_byte := byte_item (i) inspect Utf8.encoded_byte_count (a_byte) when 1 then Result := a_byte when 2 then a_code := Utf8.encoded_first_value (a_byte) a_byte := byte_item (i + 1) a_code := a_code * 64 + Utf8.encoded_next_value (a_byte) if a_code <= Platform.Maximum_character_code then Result := Integer_.to_character (a_code) else Result := '%U' end else a_code := item_code_at_byte_index (i) if a_code <= Platform.Maximum_character_code then Result := Integer_.to_character (a_code) else Result := '%U' end end ensure code_small_enough: item_code_at_byte_index (i) <= Platform.Maximum_character_code implies Result.code = item_code_at_byte_index (i) overflow: item_code_at_byte_index (i) > Platform.Maximum_character_code implies Result = '%U' end is_encoded_first_byte (i: INTEGER_32): BOOLEAN -- Is byte at index i the first byte of an encoded unicode character? require i_large_enough: i >= 1 i_small_enough: i <= byte_count do Result := Utf8.is_encoded_first_byte (byte_item (i)) end item_code_at_byte_index (i: INTEGER_32): INTEGER_32 -- Code of character at byte index i require i_large_enough: i >= 1 i_small_enough: i <= byte_count is_encoded_first_byte: is_encoded_first_byte (i) local k, nb: INTEGER_32 a_byte: CHARACTER_8 do k := i a_byte := byte_item (k) Result := Utf8.encoded_first_value (a_byte) nb := k + Utf8.encoded_byte_count (a_byte) - 1 from k := k + 1 until k > nb loop a_byte := byte_item (k) Result := Result * 64 + Utf8.encoded_next_value (a_byte) k := k + 1 end ensure valid_item_code: Unicode.valid_code (Result) end next_byte_index (i: INTEGER_32): INTEGER_32 -- Byte index of unicode character after character -- at byte index i; Return 'byte_count + 1' if -- character at byte index i is the last character -- in the string require i_large_enough: i >= 1 i_small_enough: i <= byte_count is_encoded_first_byte: is_encoded_first_byte (i) do Result := i + Utf8.encoded_byte_count (byte_item (i)) ensure next_byte_index_large_enough: Result > i next_byte_index_small_enough: Result <= byte_count + 1 end shifted_byte_index (i: INTEGER_32; n: INTEGER_32): INTEGER_32 -- Byte index of unicode character n positions after -- character at byte index i; Return 'byte_count + 1' -- if no such character in the string require i_large_enough: i >= 1 i_small_enough: i <= byte_count is_encoded_first_byte: is_encoded_first_byte (i) n_positive: n >= 0 local j: INTEGER_32 do Result := i from j := 1 until j > n loop Result := Result + Utf8.encoded_byte_count (byte_item (Result)) if Result > byte_count then j := n + 1 else j := j + 1 end end ensure next_byte_index_large_enough: Result >= i next_byte_index_small_enough: Result <= byte_count + 1 end invariant non_negative_byte_count: byte_count >= 0 byte_count_small_enough: byte_count <= byte_capacity count_small_enough: count <= byte_count -- from ANY reflexive_equality: standard_is_equal (Current) reflexive_conformance: conforms_to (Current) -- from STRING_8 extendible: Extendible compare_character: not object_comparison -- from READABLE_STRING_8 area_not_void: area /= Void -- from COMPARABLE irreflexive_comparison: not (Current < 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 <= byte_capacity full_definition: full = (count = byte_capacity) -- from FINITE empty_definition: old_is_empty = (count = 0) end -- class UC_STRING
Generated by ISE EiffelStudio