note
	description: "[
		Sequences of 32-bit characters, accessible through integer indices
		in a contiguous range.
	]"
	library: "Free implementation of ELKS library"
	status: "See notice at end of class."
	legal: "See notice at end of class."
	date: "$Date: 2020-05-19 14:21:28 +0000 (Tue, 19 May 2020) $"
	revision: "$Revision: 104256 $"

class interface
	STRING_32

create 
	make,
	make_empty,
	make_filled,
	make_from_string,
	make_from_string_general,
	make_from_c,
	make_from_c_pointer,
	make_from_c_byte_array,
	make_from_cil,
	make_from_separate

convert
	to_cil: {SYSTEM_STRING},
	make_from_cil ({SYSTEM_STRING}),
	as_string_8: {READABLE_STRING_8,
		STRING_8}

feature -- Initialization

	make_from_string_general (s: READABLE_STRING_GENERAL)
			-- Initialize from the characters of s.

	make_from_cil (a_system_string: detachable SYSTEM_STRING)
			-- Initialize Current with a_system_string.

	from_c (c_string: POINTER)
			-- Reset contents of string from contents of c_string,
			-- a string created by some C function.
		require
			c_string_exists: c_string /= default_pointer
		ensure
			no_zero_byte: not has ('%U'.to_character_32)

	from_c_substring (c_string: POINTER; start_pos, end_pos: INTEGER_32)
			-- Reset contents of string from substring of c_string,
			-- a string created by some C function.
		require
			c_string_exists: c_string /= default_pointer
			start_position_big_enough: start_pos >= 1
			end_position_big_enough: start_pos <= end_pos + 1
		ensure
			valid_count: count = end_pos - start_pos + 1

	adapt (s: STRING_32): like Current
			-- Object of a type conforming to the type of s,
			-- initialized with attributes from s
		ensure
			adapt_not_void: Result /= Void
			shared_implementation: Result.shared_with (s)
	
feature -- Access

	item alias "[]" (i: INTEGER_32): CHARACTER_32 assign put
			-- Character at position i
			-- Was declared in STRING_32 as synonym of at.

	at alias "@" (i: INTEGER_32): CHARACTER_32 assign put
			-- Character at position i
			-- Was declared in STRING_32 as synonym of item.

	code (i: INTEGER_32): NATURAL_32
			-- Character at position i

	area: SPECIAL [CHARACTER_32]
			-- Storage for characters
	
feature -- Status report

	Extendible: BOOLEAN = True
			-- May new items be added? (Answer: yes.)

	Changeable_comparison_criterion: BOOLEAN = False
			-- May object_comparison be changed?
			-- (Answer: yes by default.)
	
feature -- Element change

	set (t: READABLE_STRING_32; n1, n2: INTEGER_32)
			-- Set current string to substring of t from indices n1
			-- to n2, or to empty string if no such substring.
		require
			argument_not_void: t /= Void
		ensure
			is_substring: same_string (t.substring (n1, n2))

	subcopy (other: READABLE_STRING_32; start_pos, end_pos, index_pos: INTEGER_32)
			-- Copy characters of other within bounds start_pos and
			-- end_pos to current string starting at index index_pos.
		require
			other_not_void: other /= Void
			valid_start_pos: other.valid_index (start_pos)
			valid_end_pos: other.valid_index (end_pos)
			valid_bounds: start_pos <= end_pos or start_pos = end_pos + 1
			valid_index_pos: valid_index (index_pos)
			enough_space: count - index_pos >= end_pos - start_pos
		ensure
			same_count: count = old count
			copied: Elks_checking implies (Current ~ (old substring (1, index_pos - 1) + old other.substring (start_pos, end_pos) + old substring (index_pos + (end_pos - start_pos + 1), count)))

	replace_substring (s: READABLE_STRING_32; start_index, end_index: INTEGER_32)
			-- Replace characters from start_index to end_index with s.
		require
			string_not_void: s /= Void
			valid_start_index: 1 <= start_index
			valid_end_index: end_index <= count
			meaningfull_interval: start_index <= end_index + 1
		ensure
			new_count: count = old count + old s.count - end_index + start_index - 1
			replaced: Elks_checking implies (Current ~ (old (substring (1, start_index - 1) + s + substring (end_index + 1, count))))

	replace_substring_all (original, new: READABLE_STRING_32)
			-- Replace every occurrence of original with new.
		require
			original_exists: original /= Void
			new_exists: new /= Void
			original_not_empty: not original.is_empty

	replace_blank
			-- Replace all current characters with blanks.
		ensure
			same_size: (count = old count) and (capacity = old capacity)
			all_blank: Elks_checking implies occurrences (' '.to_character_32) = count

	fill_blank
			-- Fill with capacity blank characters.
		ensure
			filled: full
			same_size: (count = capacity) and (capacity = old capacity)

	fill_with (c: CHARACTER_32)
			-- Replace every character with c.
		ensure
			same_count: (count = old count) and (capacity = old capacity)
			filled: Elks_checking implies occurrences (c) = count

	keep_head (n: INTEGER_32)
			-- Remove all characters except for the first n;
			-- do nothing if n >= count.

	keep_tail (n: INTEGER_32)
			-- Remove all characters except for the last n;
			-- do nothing if n >= count.

	left_adjust
			-- Remove leading whitespace.

	right_adjust
			-- Remove trailing whitespace.

	share (other: STRING_32)
			-- Make current string share the text of other.
			-- Subsequent changes to the characters of current string
			-- will also affect other, and conversely.
		require
			argument_not_void: other /= Void
		ensure
			shared_count: other.count = count
			shared_area: other.area = area

	put (c: CHARACTER_32; i: INTEGER_32)
			-- Replace character at position i by c.
		ensure then
			stable_count: count = old count
			stable_before_i: Elks_checking implies substring (1, i - 1) ~ (old substring (1, i - 1))
			stable_after_i: Elks_checking implies substring (i + 1, count) ~ (old substring (i + 1, count))

	put_code (v: NATURAL_32; i: INTEGER_32)
			-- Replace character at position i by character of code v.

	prepend_string_general (s: READABLE_STRING_GENERAL)
			-- Prepend characters of s at front.

	precede (c: CHARACTER_32)
			-- Add c at front.
			-- Was declared in STRING_32 as synonym of prepend_character.
		ensure
			new_count: count = old count + 1

	prepend_character (c: CHARACTER_32)
			-- Add c at front.
			-- Was declared in STRING_32 as synonym of precede.
		ensure
			new_count: count = old count + 1

	prepend (s: READABLE_STRING_32)
			-- Prepend characters of s at front.
		require
			argument_not_void: s /= Void
		ensure
			new_count: count = old (count + s.count)
			inserted: Elks_checking implies same_string (old (s + Current))

	prepend_substring (s: READABLE_STRING_32; start_index, end_index: INTEGER_32)
			-- Prepend characters of s.substring (start_index, end_index) at front.
		require
			argument_not_void: s /= Void
			start_index_valid: start_index >= 1
			end_index_valid: end_index <= s.count
			valid_bounds: start_index <= end_index + 1
		ensure
			new_count: count = old count + end_index - start_index + 1
			inserted: Elks_checking implies same_string (old (s.substring (start_index, end_index) + Current))

	prepend_boolean (b: BOOLEAN)
			-- Prepend the string representation of b at front.

	prepend_double (d: REAL_64)
			-- Prepend the string representation of d at front.

	prepend_integer (i: INTEGER_32)
			-- Prepend the string representation of i at front.

	prepend_real (r: REAL_32)
			-- Prepend the string representation of r at front.

	prepend_string (s: detachable READABLE_STRING_32)
			-- Prepend characters of s, if not void, at front.

	append_string_general (s: READABLE_STRING_GENERAL)
			-- Append characters of s at end.

	append (s: READABLE_STRING_32)
			-- Append characters of s at end.
		require
			argument_not_void: s /= Void
		ensure
			new_count: count = old count + old s.count
			appended: Elks_checking implies same_string (old (Current + s))

	append_substring (s: READABLE_STRING_32; start_index, end_index: INTEGER_32)
			-- Append characters of s.substring (start_index, end_index) at end.
		require
			argument_not_void: s /= Void
			start_index_valid: start_index >= 1
			end_index_valid: end_index <= s.count
			valid_bounds: start_index <= end_index + 1
		ensure
			new_count: count = old count + (end_index - start_index + 1)
			appended: Elks_checking implies same_string (old (Current + s.substring (start_index, end_index)))

	append_string (s: detachable READABLE_STRING_32)
			-- Append a copy of s, if not void, at end.
		ensure
			appended: s /= Void implies (Elks_checking implies Current ~ (old twin + old s.twin))

	append_integer (i: INTEGER_32)
			-- Append the string representation of i at end.

	append_integer_8 (i: INTEGER_8)
			-- Append the string representation of i at end.

	append_integer_16 (i: INTEGER_16)
			-- Append the string representation of i at end.

	append_integer_64 (i: INTEGER_64)
			-- Append the string representation of i at end.

	append_natural_8 (i: NATURAL_8)
			-- Append the string representation of i at end.

	append_natural_16 (i: NATURAL_16)
			-- Append the string representation of i at end.

	append_natural_32 (i: NATURAL_32)
			-- Append the string representation of i at end.

	append_natural_64 (i: NATURAL_64)
			-- Append the string representation of i at end.

	append_real (r: REAL_32)
			-- Append the string representation of r at end.

	append_double (d: REAL_64)
			-- Append the string representation of d at end.

	append_character (c: CHARACTER_32)
			-- Append c at end.
			-- Was declared in STRING_32 as synonym of extend.
		ensure then
			item_inserted: item (count) = c
			new_count: count = old count + 1
			stable_before: Elks_checking implies substring (1, count - 1) ~ (old twin)

	extend (c: CHARACTER_32)
			-- Append c at end.
			-- Was declared in STRING_32 as synonym of append_character.
		ensure then
			item_inserted: item (count) = c
			new_count: count = old count + 1
			stable_before: Elks_checking implies substring (1, count - 1) ~ (old twin)

	append_boolean (b: BOOLEAN)
			-- Append the string representation of b at end.

	insert_string (s: READABLE_STRING_32; i: INTEGER_32)
			-- Insert s at index i, shifting characters between ranks
			-- i and count rightwards.
		require
			string_exists: s /= Void
			valid_insertion_index: 1 <= i and i <= count + 1
		ensure
			inserted: Elks_checking implies (Current ~ (old substring (1, i - 1) + old (s.twin) + old substring (i, count)))

	insert_character (c: CHARACTER_32; i: INTEGER_32)
			-- Insert c at index i, shifting characters between ranks
			-- i and count rightwards.
		require
			valid_insertion_index: 1 <= i and i <= count + 1
		ensure
			one_more_character: count = old count + 1
			inserted: item (i) = c
			stable_before_i: Elks_checking implies substring (1, i - 1) ~ (old substring (1, i - 1))
			stable_after_i: Elks_checking implies substring (i + 1, count) ~ (old substring (i, count))
	
feature -- Basic operations

	plus alias "+" (s: READABLE_STRING_32): like Current
			-- Concatenation with s.

	plus_general (s: READABLE_STRING_GENERAL): like Current
			-- Concatenation of the current string with s.
	
feature -- Removal

	remove (i: INTEGER_32)
			-- Remove i-th character.

	remove_head (n: INTEGER_32)
			-- Remove first n characters;
			-- if n > count, remove all.

	remove_substring (start_index, end_index: INTEGER_32)
			-- Remove all characters from start_index
			-- to end_index inclusive.

	remove_tail (n: INTEGER_32)
			-- Remove last n characters;
			-- if n > count, remove all.

	prune (c: CHARACTER_32)
			-- Remove first occurrence of c, if any.
		require else
				True

	prune_all (c: CHARACTER_32)
			-- Remove all occurrences of c.
		require else
				True
		ensure then
			changed_count: count = (old count) - (old occurrences (c))

	prune_all_leading (c: CHARACTER_32)
			-- Remove all leading occurrences of c.

	prune_all_trailing (c: CHARACTER_32)
			-- Remove all trailing occurrences of c.

	wipe_out
			-- Remove all characters.
	
feature -- Resizing

	adapt_size
			-- Adapt the size to accommodate count characters.

	resize (newsize: INTEGER_32)
			-- Rearrange string so that it can accommodate
			-- at least newsize characters.
			-- Do not lose any previously entered character.

	grow (newsize: INTEGER_32)
			-- Ensure that the capacity is at least newsize.

	trim
			-- Decrease capacity to the minimum value.
			-- Apply to reduce allocated storage.
		ensure then
			same_string: same_string (old twin)
	
feature -- Conversion

	as_lower: like Current
			-- New object with all letters in lower case.

	as_upper: like Current
			-- New object with all letters in upper case

	left_justify
			-- Left justify Current using count as witdth.

	center_justify
			-- Center justify Current using count as width.

	right_justify
			-- Right justify Current using count as width.
		ensure
			same_count: count = old count

	character_justify (pivot: CHARACTER_32; position: INTEGER_32)
			-- Justify a string based on a pivot
			-- and the position it needs to be in
			-- the final string.
			-- This will grow the string if necessary
			-- to get the pivot in the correct place.
		require
			valid_position: position <= capacity
			positive_position: position >= 1
			pivot_not_space: pivot /= ' '.to_character_32
			not_empty: not is_empty

	to_lower
			-- Convert to lower case.
		ensure
			length_and_content: Elks_checking implies Current ~ (old as_lower)

	to_upper
			-- Convert to upper case.
		ensure
			length_and_content: Elks_checking implies Current ~ (old as_upper)

	linear_representation: LINEAR [CHARACTER_32]
			-- Representation as a linear structure

	frozen to_c: ANY
			-- A reference to a C form of current string.
			-- Useful only for interfacing with C software.
		require
			not_is_dotnet: not {PLATFORM}.is_dotnet

	mirrored: like Current
			-- Mirror image of string;
			-- Result for "Hello world" is "dlrow olleH".

	mirror
			-- Reverse the order of characters.
			-- "Hello world" -> "dlrow olleH".
		ensure
			same_count: count = old count
	
feature -- Duplication

	substring (start_index, end_index: INTEGER_32): like Current
			-- Copy of substring containing all characters at indices
			-- between start_index and end_index

	multiply (n: INTEGER_32)
			-- Duplicate a string within itself
			-- ("hello").multiply(3) => "hellohellohello"
		require
			meaningful_multiplier: n >= 1
	
feature -- Transformation

	correct_mismatch
			-- Attempt to correct object mismatch during retrieve using Mismatch_information.
	
invariant
	extendible: Extendible
	compare_character: not object_comparison

note
	copyright: "Copyright (c) 1984-2020, Eiffel Software and others"
	license: "Eiffel Forum License v2 (see http://www.eiffel.com/licensing/forum.txt)"
	source: "[
		Eiffel Software
		5949 Hollister Ave., Goleta, CA 93117 USA
		Telephone 805-685-1006, Fax 805-685-6869
		Website http://www.eiffel.com
		Customer support http://support.eiffel.com
	]"

end -- class STRING_32

Generated by ISE EiffelStudio