[gobo-eiffel-develop] ST_STRING_BUILDER

[Colin P. A. <co...@co...>]

indexing

	description:

		"[
        Objects for constructing XPath UTF-32 strings.
        Usage pattern is:
        1) Create builder.
        2) Call appending features.
        3) Call `set_built' followed by `new_string'.
        4) Call `reuse' and loop to (2).
       ]"

	library: "Gobo Eiffel String Library"
	copyright: "Copyright (c) 2008, Colin Adams and others"
	license: "MIT License"
	date: "$Date:  $"
	revision: "$Revision:  $"

class ST_STRING_BUILDER

inherit
	
	ANY

	ST_STRING_ROUTINES
		export {NONE} all end

	ST_SHARED_STRINGS
		export {NONE} all end

create

	make

feature {NONE} -- Initialization

	make (a_capacity: INTEGER) is
			-- Initialize for a string of expected size `a_capacity'.
		require
			a_capacity_non_negative: a_capacity >= 0
		do
			create array.make (1, a_capacity)
			count := 0
			is_building := True
		ensure
			correct_capacity: array.count = a_capacity
			empty: count = 0
			ready_to_build: is_building
		end

feature -- Initialization

	reuse (a_capacity: INTEGER) is
			-- Prepare to reuse `Current' for a string of expected size `a_capacity'.
		require
			a_capacity_non_negative: a_capacity >= 0
			not_ready: not is_building
		do
			array.conservative_resize (1, a_capacity)
			count := 0
			is_building := True
		ensure
			correct_capacity: array.capacity >= a_capacity
			empty: count = 0
			ready_to_build: is_building
		end

feature -- Access

	new_string: ST_STRING is
			-- Newly constructed string
		require
			built: not is_building
		do
			if count = 0 then
				Result := shared_empty_string
			else
				create Result.make_from_codepoints (array.subarray (1, count.as_integer_32))
			end
		ensure
			new_string_not_void: Result /= Void
		end
	
	index_of_code (a_code: NATURAL_32): INTEGER is
			-- Index of first built character matching `a_code';
			-- Result = 0 = no match
		require
			ready_to_build: is_building
		local
			l_finished: BOOLEAN
		do
			from
				Result := 1 
			until
				l_finished
			loop
				if Result > count then
					Result := 0
					l_finished := True
				elseif array.item (Result) = a_code then
					l_finished := True
				else
					Result := Result + 1
				end
			end
		ensure
			index_of_code_in_range: Result >= 0 and Result <= count
		end
	
	code (a_index: INTEGER): NATURAL_32 is
			-- code at `a_index'
		require
			ready_to_build: is_building
			good_index: a_index > 0 and a_index <= count
		do
			Result := array.item (a_index)
		end

feature -- Measurement

	count: INTEGER
			-- Number of characters added to `Current' since last call to `reuse'
	
	is_empty: BOOLEAN is
			-- Have any characters been added?
		do
			Result := count = 0
		ensure
			definition: Result = (count = 0)
		end
			
feature -- Status report

	is_building: BOOLEAN
			-- Is `Current' ready for receiving characters?

feature -- Status setting

	set_built is
			-- Set `is_building' to `False'.
		do
			is_building := False
		ensure
			not_ready: not is_building
		end

feature -- Basic operations

	append_character (a_character: CHARACTER_8) is
			-- Add `a_character' at end of `Current'.
		require
			ready_to_build: is_building
		do
			array.conservative_resize (1, 1 + count)
			array.put (a_character.code.as_natural_32, count + 1)
			count := count + 1
		ensure
			correct_count: count = old count + 1
			correct_character_appended: array.item (count) = a_character.code.as_natural_32
		end
	
	append_code (a_character: NATURAL_32) is
			-- Add `a_character' at end of `Current'.
		require
			ready_to_build: is_building
		do
			array.conservative_resize (1, 1 + count)
			array.put (a_character, count + 1)
			count := count + 1
		ensure
			correct_count: count = old count + 1
			correct_character_appended: array.item (count) = a_character
		end
	
	append_code_multiple (a_character: NATURAL_32; a_count: INTEGER) is
			-- Add `a_character' at end of `Current' `a_count' times.
		require
			ready_to_build: is_building
			strictly_positive_count: a_count > 0
		local
			i: INTEGER
		do
			array.conservative_resize (1, a_count + count)
			from
				i := 1
			until
				i > a_count
			loop
				array.put (a_character, count + 1)
				count := count + 1
				i := i + 1
			end
		ensure
			correct_count: count = old count + a_count
			correct_character_appended: array.subarray (old count + 1, count).for_all (agent matches_code (?, a_character))
		end

	replace_code (a_character: NATURAL_32; a_index: INTEGER) is
			-- Replace `a_character' at `a_index'
		require
			ready_to_build: is_building
			a_index_valid: a_index > 0 and a_index <= count
		do
			array.put (a_character, a_index)
		ensure
			count_unchanged: count = old count
			correct_character_replaced: array.item (a_index) = a_character
		end

	append_string (a_string: READABLE_STRING_GENERAL) is
			-- Add all characters from `a_string' at end of `Current'.
		require
			a_string_not_void: a_string /= Void
			ready_to_build: is_building
		local
			i, l_count, l_new_count: INTEGER
		do
			l_count := a_string.count
			if l_count > 0 then
				l_new_count := count + l_count
				array.conservative_resize (1, l_new_count)
				from
					i := 1
				until
					i > l_count
				loop
					array.put (a_string.code (i), count + i)
					i := i + 1
				end
				count := l_new_count
			end
		ensure
			correct_count: count = old count + a_string.count
			correct_characters_appended: not a_string.is_empty implies characters_match (a_string, old count + 1, count)
		end

	append_strings (a_strings: ARRAY [READABLE_STRING_GENERAL]) is
			-- Add all characters from all of `a_strings' at end of `Current'.
		require
			a_strings_not_void: a_strings /= Void
			all_strings_not_void: not a_strings.has (Void)
			ready_to_build: is_building
		local
			j, k: INTEGER
			i, l_count, l_new_count: INTEGER
			l_string: READABLE_STRING_GENERAL
		do
			l_count := string_sums (a_strings)
			l_new_count := count + l_count
			if l_new_count > 0 then
				array.conservative_resize (1, l_new_count)
				from
					j := 1
					i := 1
				until
					j > a_strings.count
				loop
					from
						l_string := a_strings.item (j)
						k := 1
					until
						k > l_string.count
					loop
						array.put (l_string.code (k), count + i)
						i := i + 1
						k := k + 1
					end
					j := j + 1
				end
				check
					correct_i: i = l_new_count + 1 - count
					-- `i' is incremented on every inner loop
				end
			end
			count := l_new_count
		ensure
			correct_count: count = old count + string_sums (a_strings)
			correct_characters_appended: True -- TODO
		end
	
feature -- Removal

	remove_tail (a_n: INTEGER) is
			-- Remove final `a_n' characters from `Current'.
			-- If `a_n' > `count' remove all characters.
		require
			a_n_non_negative: a_n >= 0
		do
			if a_n > count then
				count := 0
			else
				count := count - a_n
			end
		ensure
			zero_characters_if_a_n_larger_than_count: a_n > old count implies count = 0
			correct_count: a_n <= old count implies count = old count - a_n
		end

feature {NONE} -- Implementation	

	array: ARRAY [NATURAL_32]
			-- Character buffer

	characters_match (a_string: READABLE_STRING_GENERAL; a_start, a_end: INTEGER): BOOLEAN is
			-- Does character sequence of `a_string' match `array.subarray (a_start, a_end)'?
		require
			a_string_not_void: a_string /= Void
			a_start_strictly_positive: a_start > 0
			a_end_greater_than_a_start: a_end > a_start
			a_end_small_enough: a_end <= count
			correct_string_count: a_string.count = (a_end - a_start + 1)
		local
			i, j: INTEGER
		do
			from
				Result := True
				i := a_start
				j := 1
			until
				not Result or i > a_end
			loop
				Result := a_string.code (j) = array.item (i)
				i := i + 1
				j := j + 1
			end
		end
	
	matches_code (a_code, a_other: NATURAL_32): BOOLEAN is
			-- Does `a_code' equal `a_other'?
		do
			Result := a_code = a_other
		ensure
			definition: Result = (a_code = a_other)
		end

invariant

	array_not_void: array /= Void
	count_non_negative: count >= 0

end

-- 
Colin Adams
Preston Lancashire