indexing
	description: "Implementation of DB_SELECTION"
	legal: "See notice at end of class."
	status: "See notice at end of class."
	date: "$Date: 2007-04-16 12:45:58 -0700 (Mon, 16 Apr 2007) $"
	revision: "$Revision: 67858 $"

class interface
	DATABASE_SELECTION [G -> DATABASE create default_create end]


create 
	make (i: INTEGER_32)
			-- Create format and allocate string.
			-- (from SQL_SCAN)


create {DATABASE_SELECTION}
	string_make (n: INTEGER_32)
			-- Allocate space for at least `n' characters.
			-- (from STRING_8)
		require -- from STRING_8
			non_negative_size: n >= 0
		ensure -- from STRING_8
			empty_string: count = 0
			area_allocated: capacity >= n

feature -- Initialization

	adapt (s: STRING_8): DATABASE_SELECTION [G]
			-- Object of a type conforming to the type of `s',
			-- initialized with attributes from `s'
			-- (from STRING_8)
		ensure -- from STRING_8
			adapt_not_void: Result /= Void
			shared_implementation: Result.shared_with (s)

	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
		ensure -- from STRING_8
			no_zero_byte: not has ('%U')

	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.
			-- (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
		ensure -- from STRING_8
			valid_count: count = end_pos - start_pos + 1

	make (i: INTEGER_32)
			-- Create format and allocate string.
			-- (from SQL_SCAN)

	string_make (n: INTEGER_32)
			-- Allocate space for at least `n' characters.
			-- (from STRING_8)
		require -- from STRING_8
			non_negative_size: n >= 0
		ensure -- from STRING_8
			empty_string: count = 0
			area_allocated: capacity >= n

	format_make
			-- Create an interface object to format data.
			-- (from DB_FORMAT)

	make_empty
			-- Create empty string.
			-- (from STRING_8)
		ensure -- from STRING_8
			empty: count = 0
			area_allocated: capacity >= 0

	make_filled (c: CHARACTER_8; n: INTEGER_32)
			-- Create string of length `n' filled with `c'.
			-- (from STRING_8)
		require -- from STRING_8
			valid_count: n >= 0
		ensure -- from STRING_8
			count_set: count = n
			area_allocated: capacity >= n
			filled: occurrences (c) = count

	make_from_c (c_string: POINTER)
			-- Initialize 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

	make_from_cil (a_system_string: SYSTEM_STRING)
			-- Initialize Current with `a_system_string'.
			-- (from STRING_8)
		require -- from STRING_8
			is_dotnet: {PLATFORM}.is_dotnet

	make_from_string (s: STRING_8)
			-- Initialize from the characters of `s'.
			-- (Useful in proper descendants of class STRING,
			-- to initialize a string-like object from a manifest string.)
			-- (from STRING_8)
		require -- from STRING_8
			string_exists: s /= Void
		ensure -- from STRING_8
			not_shared_implementation: Current /= s implies not shared_with (s)
			initialized: same_string (s)
	
feature -- Access

	area: SPECIAL [CHARACTER_8]
			-- Special data zone
			-- (from TO_SPECIAL)

	bit_type: INTEGER_32 is 8
			-- (from INTERNAL)

	boolean_field (i: INTEGER_32; object: ANY): BOOLEAN
			-- Boolean value of `i'-th field of `object'
			-- (from INTERNAL)
		require -- from INTERNAL
			object_not_void: object /= Void
			index_large_enough: i >= 1
			index_small_enough: i <= field_count (object)
			boolean_field: field_type (i, object) = boolean_type

	boolean_type: INTEGER_32 is 3
			-- (from INTERNAL)

	character_32_field (i: INTEGER_32; object: ANY): CHARACTER_32
			-- CHARACTER_32 value of `i'-th field of `object'
			-- (from INTERNAL)
		require -- from INTERNAL
			object_not_void: object /= Void
			index_large_enough: i >= 1
			index_small_enough: i <= field_count (object)
			character_32_field: field_type (i, object) = character_32_type

	character_32_type: INTEGER_32 is 12
			-- Was declared in INTERNAL as synonym of Wide_character_type.
			-- (from INTERNAL)

	character_8_field (i: INTEGER_32; object: ANY): CHARACTER_8
			-- CHARACTER_8 value of `i'-th field of `object'
			-- Was declared in INTERNAL as synonym of character_field.
			-- (from INTERNAL)
		require -- from INTERNAL
			object_not_void: object /= Void
			index_large_enough: i >= 1
			index_small_enough: i <= field_count (object)
			character_8_field: field_type (i, object) = character_8_type

	character_8_type: INTEGER_32 is 2
			-- Was declared in INTERNAL as synonym of Character_type.
			-- (from INTERNAL)

	character_field (i: INTEGER_32; object: ANY): CHARACTER_8
			-- CHARACTER_8 value of `i'-th field of `object'
			-- Was declared in INTERNAL as synonym of character_8_field.
			-- (from INTERNAL)
		require -- from INTERNAL
			object_not_void: object /= Void
			index_large_enough: i >= 1
			index_small_enough: i <= field_count (object)
			character_8_field: field_type (i, object) = character_8_type

	character_type: INTEGER_32 is 2
			-- Was declared in INTERNAL as synonym of Character_8_type.
			-- (from INTERNAL)

	class_name (object: ANY): STRING_8
			-- Name of the class associated with `object'
			-- (from INTERNAL)
		require -- from INTERNAL
			object_not_void: object /= Void

	class_name_of_type (type_id: INTEGER_32): STRING_8
			-- Name of class associated with dynamic type `type_id'.
			-- (from INTERNAL)
		require -- from INTERNAL
			type_id_nonnegative: type_id >= 0

	code (i: INTEGER_32): NATURAL_32
			-- Numeric code of character at position `i'
			-- (from STRING_8)
		require -- from STRING_GENERAL
			valid_index: valid_index (i)

	db_spec: DATABASE
			-- Handle to actual database
			-- (from HANDLE_SPEC)
		ensure -- from HANDLE_SPEC
			not_void: Result /= Void

	double_field (i: INTEGER_32; object: ANY): REAL_64
			-- Double precision value of `i'-th field of `object'
			-- Was declared in INTERNAL as synonym of real_64_field.
			-- (from INTERNAL)
		require -- from INTERNAL
			object_not_void: object /= Void
			index_large_enough: i >= 1
			index_small_enough: i <= field_count (object)
			real_64_field: field_type (i, object) = real_64_type

	double_type: INTEGER_32 is 6
			-- Was declared in INTERNAL as synonym of Real_64_type.
			-- (from INTERNAL)

	dynamic_type (object: ANY): INTEGER_32
			-- Dynamic type of `object'
			-- (from INTERNAL)
		require -- from INTERNAL
			object_not_void: object /= Void
		ensure -- from INTERNAL
			dynamic_type_nonnegative: Result >= 0

	expanded_field_type (i: INTEGER_32; object: ANY): STRING_8
			-- Class name associated with the `i'-th
			-- expanded field of `object'
			-- (from INTERNAL)
		require -- from INTERNAL
			object_not_void: object /= Void
			index_large_enough: i >= 1
			index_small_enough: i <= field_count (object)
			is_expanded: field_type (i, object) = expanded_type
		ensure -- from INTERNAL
			result_exists: Result /= Void

	expanded_type: INTEGER_32 is 7
			-- (from INTERNAL)

	false_constant: STRING_8 is "false"
			-- Constant string "false"
			-- (from STRING_8)

	field (i: INTEGER_32; object: ANY): ?ANY
			-- Object attached to the `i'-th field of `object'
			-- (directly or through a reference)
			-- (from INTERNAL)
		require -- from INTERNAL
			object_not_void: object /= Void
			index_large_enough: i >= 1
			index_small_enough: i <= field_count (object)
			not_special: not is_special (object)

	field_name (i: INTEGER_32; object: ANY): STRING_8
			-- Name of `i'-th field of `object'
			-- (from INTERNAL)
		require -- from INTERNAL
			object_not_void: object /= Void
			index_large_enough: i >= 1
			index_small_enough: i <= field_count (object)
			not_special: not is_special (object)
		ensure -- from INTERNAL
			result_exists: Result /= Void

	field_name_of_type (i: INTEGER_32; type_id: INTEGER_32): STRING_8
			-- Name of `i'-th field of dynamic type `type_id'.
			-- (from INTERNAL)
		require -- from INTERNAL
			type_id_nonnegative: type_id >= 0
			index_large_enough: i >= 1
			index_small_enought: i <= field_count_of_type (type_id)

	field_offset (i: INTEGER_32; object: ANY): INTEGER_32
			-- Offset of `i'-th field of `object'
			-- (from INTERNAL)
		require -- from INTERNAL
			object_not_void: object /= Void
			index_large_enough: i >= 1
			index_small_enough: i <= field_count (object)
			not_special: not is_special (object)

	field_static_type_of_type (i: INTEGER_32; type_id: INTEGER_32): INTEGER_32
			-- Static type of declared `i'-th field of dynamic type `type_id'
			-- (from INTERNAL)
		require -- from INTERNAL
			type_id_nonnegative: type_id >= 0
			index_large_enough: i >= 1
			index_small_enough: i <= field_count_of_type (type_id)
		ensure -- from INTERNAL
			field_type_nonnegative: Result >= 0

	field_type (i: INTEGER_32; object: ANY): INTEGER_32
			-- Abstract type of `i'-th field of `object'
			-- (from INTERNAL)
		require -- from INTERNAL
			object_not_void: object /= Void
			index_large_enough: i >= 1
			index_small_enough: i <= field_count (object)
		ensure -- from INTERNAL
			field_type_nonnegative: Result >= 0

	field_type_of_type (i: INTEGER_32; type_id: INTEGER_32): INTEGER_32
			-- Abstract type of `i'-th field of dynamic type `type_id'
			-- (from INTERNAL)
		require -- from INTERNAL
			type_id_nonnegative: type_id >= 0
			index_large_enough: i >= 1
			index_small_enough: i <= field_count_of_type (type_id)
		ensure -- from INTERNAL
			field_type_nonnegative: Result >= 0

	fuzzy_index (other: STRING_8; 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 STRING_8)
		require -- from STRING_8
			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

	generating_type: STRING_8
			-- Name of current object's generating type
			-- (type of which it is a direct instance)
			-- (from ANY)
		ensure -- from ANY
			generating_type_not_void: Result /= Void
			generating_type_not_empty: not Result.is_empty

	generator: STRING_8
			-- Name of current object's generating class
			-- (base class of the type of which it is a direct instance)
			-- (from ANY)
		ensure -- from ANY
			generator_not_void: Result /= Void
			generator_not_empty: not Result.is_empty

	generic_count (obj: ANY): INTEGER_32
			-- Number of generic parameter in `obj'.
			-- (from INTERNAL)
		require -- from INTERNAL
			obj_not_void: obj /= Void

	generic_count_of_type (type_id: INTEGER_32): INTEGER_32
			-- Number of generic parameter in `type_id'.
			-- (from INTERNAL)
		require -- from INTERNAL
			type_id_nonnegative: type_id >= 0

	generic_dynamic_type (object: ANY; i: INTEGER_32): INTEGER_32
			-- Dynamic type of generic parameter of `object' at
			-- position `i'.
			-- (from INTERNAL)
		require -- from INTERNAL
			object_not_void: object /= Void
			object_generic: generic_count (object) > 0
			i_valid: i > 0 and i <= generic_count (object)
		ensure -- from INTERNAL
			dynamic_type_nonnegative: Result >= 0

	generic_dynamic_type_of_type (type_id: INTEGER_32; i: INTEGER_32): INTEGER_32
			-- Dynamic type of generic parameter of `type_id' at position `i'.
			-- (from INTERNAL)
		require -- from INTERNAL
			type_id_nonnegative: type_id >= 0
			type_id_generic: generic_count_of_type (type_id) > 0
			i_valid: i > 0 and i <= generic_count_of_type (type_id)
		ensure -- from INTERNAL
			dynamic_type_nonnegative: Result >= 0

	hash_code: INTEGER_32
			-- Hash code value
			-- (from STRING_8)
		ensure -- from HASHABLE
			good_hash_value: Result >= 0

	index_of (c: CHARACTER_8; start_index: INTEGER_32): INTEGER_32
			-- Position of first occurrence of `c' at or after `start_index';
			-- 0 if none.
			-- (from STRING_8)
		require -- from STRING_8
			start_large_enough: start_index >= 1
			start_small_enough: start_index <= count + 1
		ensure -- from 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)

	index_of_code (c: like code; start_index: INTEGER_32): INTEGER_32
			-- Position of first occurrence of `c' at or after `start_index';
			-- 0 if none.
			-- (from STRING_GENERAL)
		require -- from STRING_GENERAL
			start_large_enough: start_index >= 1
			start_small_enough: start_index <= count + 1
		ensure -- from 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)

	integer_16_field (i: INTEGER_32; object: ANY): INTEGER_16
			-- INTEGER_16 value of `i'-th field of `object'
			-- (from INTERNAL)
		require -- from INTERNAL
			object_not_void: object /= Void
			index_large_enough: i >= 1
			index_small_enough: i <= field_count (object)
			integer_16_field: field_type (i, object) = integer_16_type

	integer_16_type: INTEGER_32 is 10
			-- (from INTERNAL)

	integer_32_field (i: INTEGER_32; object: ANY): INTEGER_32
			-- INTEGER_32 value of `i'-th field of `object'
			-- Was declared in INTERNAL as synonym of integer_field.
			-- (from INTERNAL)
		require -- from INTERNAL
			object_not_void: object /= Void
			index_large_enough: i >= 1
			index_small_enough: i <= field_count (object)
			integer_32_field: field_type (i, object) = integer_32_type

	integer_32_type: INTEGER_32 is 4
			-- Was declared in INTERNAL as synonym of Integer_type.
			-- (from INTERNAL)

	integer_64_field (i: INTEGER_32; object: ANY): INTEGER_64
			-- INTEGER_64 value of `i'-th field of `object'
			-- (from INTERNAL)
		require -- from INTERNAL
			object_not_void: object /= Void
			index_large_enough: i >= 1
			index_small_enough: i <= field_count (object)
			integer_64_field: field_type (i, object) = integer_64_type

	integer_64_type: INTEGER_32 is 11
			-- (from INTERNAL)

	integer_8_field (i: INTEGER_32; object: ANY): INTEGER_8
			-- INTEGER_8 value of `i'-th field of `object'
			-- (from INTERNAL)
		require -- from INTERNAL
			object_not_void: object /= Void
			index_large_enough: i >= 1
			index_small_enough: i <= field_count (object)
			integer_8_field: field_type (i, object) = integer_8_type

	integer_8_type: INTEGER_32 is 9
			-- (from INTERNAL)

	integer_field (i: INTEGER_32; object: ANY): INTEGER_32
			-- INTEGER_32 value of `i'-th field of `object'
			-- Was declared in INTERNAL as synonym of integer_32_field.
			-- (from INTERNAL)
		require -- from INTERNAL
			object_not_void: object /= Void
			index_large_enough: i >= 1
			index_small_enough: i <= field_count (object)
			integer_32_field: field_type (i, object) = integer_32_type

	integer_type: INTEGER_32 is 4
			-- Was declared in INTERNAL as synonym of Integer_32_type.
			-- (from INTERNAL)

	item (i: INTEGER_32): CHARACTER_8 assign put
			-- Character at position `i'
			-- Was declared in STRING_8 as synonym of infix "@".
			-- (from STRING_8)
		require -- from TABLE
			valid_key: valid_index (i)
		require -- from TO_SPECIAL
			valid_index: valid_index (i)

	item_code (i: INTEGER_32): INTEGER_32
			-- Numeric code of character at position `i'
			-- (from STRING_8)
		require -- from STRING_8
			index_small_enough: i <= count
			index_large_enough: i > 0

	last_index_of (c: CHARACTER_8; start_index_from_end: INTEGER_32): INTEGER_32
			-- Position of last occurrence of `c'.
			-- 0 if none
			-- (from STRING_8)
		require -- from STRING_8
			start_index_small_enough: start_index_from_end <= count
			start_index_large_enough: start_index_from_end >= 1
		ensure -- from STRING_8
			last_index_of_non_negative: Result >= 0
			correct_place: Result > 0 implies item (Result) = c

	last_parsed_query: STRING_8
			-- Last parsed query

	max_predefined_type: INTEGER_32 is 16
			-- (from INTERNAL)

	natural_16_field (i: INTEGER_32; object: ANY): NATURAL_16
			-- NATURAL_16 value of `i'-th field of `object'
			-- (from INTERNAL)
		require -- from INTERNAL
			object_not_void: object /= Void
			index_large_enough: i >= 1
			index_small_enough: i <= field_count (object)
			natural_16_field: field_type (i, object) = natural_16_type

	natural_16_type: INTEGER_32 is 14
			-- (from INTERNAL)

	natural_32_field (i: INTEGER_32; object: ANY): NATURAL_32
			-- NATURAL_32 value of `i'-th field of `object'
			-- (from INTERNAL)
		require -- from INTERNAL
			object_not_void: object /= Void
			index_large_enough: i >= 1
			index_small_enough: i <= field_count (object)
			natural_32_field: field_type (i, object) = natural_32_type

	natural_32_type: INTEGER_32 is 15
			-- (from INTERNAL)

	natural_64_field (i: INTEGER_32; object: ANY): NATURAL_64
			-- NATURAL_64 value of `i'-th field of `object'
			-- (from INTERNAL)
		require -- from INTERNAL
			object_not_void: object /= Void
			index_large_enough: i >= 1
			index_small_enough: i <= field_count (object)
			natural_64_field: field_type (i, object) = natural_64_type

	natural_64_type: INTEGER_32 is 16
			-- (from INTERNAL)

	natural_8_field (i: INTEGER_32; object: ANY): NATURAL_8
			-- NATURAL_8 value of `i'-th field of `object'
			-- (from INTERNAL)
		require -- from INTERNAL
			object_not_void: object /= Void
			index_large_enough: i >= 1
			index_small_enough: i <= field_count (object)
			natural_8_field: field_type (i, object) = natural_8_type

	natural_8_type: INTEGER_32 is 13
			-- (from INTERNAL)

	none_type: INTEGER_32 is -2
			--