expanded class
	REAL_NUMBER_IMPL

inherit
	REAL_NUMBER
		redefine
			default_create,
			complex_anchor,
			real_anchor
		end

create
	default_create,
	make,
	make_from_normalized_value,
	make_from_real,
	make_from_native_integer,
	make_from_integer,
	make_opposite

convert
	make ({REAL}),
	make_from_real ({REAL_NUMBER}),
	make_from_native_integer ({INTEGER}),
	make_from_integer ({INTEGER_NUMBER}),
	value: {REAL, REAL_REF, NUMERIC, COMPARABLE, HASHABLE},
	as_complex: {COMPLEX_NUMBER_IMPL}

feature {NONE} -- Initialization

	default_create
			-- <Precursor>
		do
			value := 0
		ensure then
			value: value = 0
		end

	make (v: REAL)
			-- Create a real number with `value' = `normalized_value' (`v').
		do
			value := normalized_value (v)
		ensure
			value: value = normalized_value (v)
		end

	make_from_normalized_value (v: REAL)
			-- Create a real number with `value' = `v'.
		require
			normalized_value: v = normalized_value (v)
		do
			value := v
		ensure
			value: value = v
		end

	make_from_real (x: REAL_NUMBER)
			-- Create a real number with `value' = `x'.`value'
		do
				check
					normalized_value: x.value = normalized_value (x.value)
						-- {REAL_NUMBER} invariant
				end
			make_from_normalized_value (x.value)
		ensure
			value: value = x.value
		end

	make_from_native_integer (v: INTEGER)
			-- Create a real number with `value' = `normalized_value' (`v'.`to_real').
		do
			make (v)
		ensure
			value: value = normalized_value (v)
		end

	make_from_integer (i: INTEGER_NUMBER)
			-- Create a real number with `value' = `normalized_value' (`i'.`value'.`to_real').
		do
			make_from_native_integer (i.value)
		ensure
			value: value = normalized_value (i.value)
		end

	make_opposite (x: REAL_NUMBER_IMPL)
			-- Create a real number with value -`x'.`value'
		do
				check
					normalized_value: - x.value = normalized_value (- x.value)
						-- `normalized_value' definition
				end
			make_from_normalized_value (- x.value)
		ensure
			value: value = - x.value
		end

feature -- Primitive

	value: REAL
			-- <Precursor>

feature -- Access

	Zero: INTEGER_NUMBER_IMPL
			-- <Precursor>
		once
		end

	Min_value: REAL = - 14.0
			-- Minimum value representable by this kind of real number.

	Max_value: REAL = 14.0 -- 2 ^ `greatest_exponent' * (1 + `greatest_mantissa' * `mantissa_unit')
			-- Maximum value representable by this kind of real number.

	Machine_epsilon: REAL = 0.25 -- 2 ^ 0 * (1 + 1 * `mantissa_unit') - 1 -- todo: fix it.
			-- The difference between 1 and the least value greater than
			-- 1 that is representable by this kind of real number.

	Epsilon: REAL = 0.3125 -- 2 ^ `least_normal_exponent' * (1 + 1 * `mantissa_unit')
			-- Minimum normalized positive number representable by this kind of real number

feature -- Quality

	is_nan: BOOLEAN
			-- Is current the representation of `nan'?
		do
			Result := value.is_nan
		ensure
			definition: Result = value.is_nan
		end

	is_negative_infinity: BOOLEAN
			-- Is current the representation of `negative_infinity'?
		do
			Result := value.is_negative_infinity
		ensure
			definition: Result = value.is_negative_infinity
		end

	is_positive_infinity: BOOLEAN
			-- Is current the representation of `positive_infinity'?
		do
			Result := value.is_positive_infinity
		ensure
			definition: Result = value.is_positive_infinity
		end

feature -- Operation

	opposite alias "-": like real_anchor
			-- <Precursor>
		do
			create Result.make_opposite (Current)
		end

	complex_product (z: COMPLEX_NUMBER): like complex_anchor
			-- <Precursor>
		do
			Result := as_complex * z
		end

feature -- Conversion

	as_complex: like complex_anchor
			-- This real number represented as a complex number
		do
			create Result.make_from_real (Current)
		ensure
			real: Result.a ≍ Current
			Imaginary: Result.b ≍ Zero
		end

feature -- Factory

	normalized_value (v: REAL): REAL
			-- <Precursor>
			--| The normalized values range as if they were encoded by a 6-bit, base 2,
			--| IEEE 754-like, floating point number with the following parameters:
			--| sign bit: 1 bit;
			--| exponent width: 3 bits;
			--| significand (mantissa) precision: 3 bits (2 explicitly stored).
			--| Conceptual normalized value layout: s_eee_mm
		local
			s, e: INTEGER
			f, exp, m: NATURAL
		do
			if v.is_nan then
				Result := v
			elseif v > Max_value then
				Result := {REAL}.positive_infinity
			elseif v < Min_value then
				Result := {REAL}.negative_infinity
			else
				s := v.sign
				f := real_bit_pattern (v)
				exp := f |>> Native_mantissa_width
				exp := exp & Native_exponent_mask
				m := f |>> (Native_mantissa_width - Mantissa_width)
				m := m & Mantissa_mask
				e := exp.as_integer_32 - Native_exponent_bias
				if Least_normal_exponent <= e then
					Result := s * (2 ^ e).truncated_to_real * (1 + m * Mantissa_unit)
				elseif Least_subnormal_exponent <= e then
					m := m | Mantissa_scale
					m := m |>> (Least_normal_exponent - e)
					Result := s * (2 ^ Least_normal_exponent).truncated_to_real * m * Mantissa_unit
				else
					Result := s * 0
				end
			end
		ensure then
			class
			Nan: v.is_nan implies Result.is_nan
			Positive_infinity: not v.is_nan and v > Max_value implies Result.is_positive_infinity
			Negative_infinity: not v.is_nan and v < Min_value implies Result.is_negative_infinity
			el_s: attached v.sign as el_s
			el_f: attached real_bit_pattern (v) as el_f
			el_exp: attached ((el_f |>> Native_mantissa_width) & Native_exponent_mask) as el_exp
			el_m: attached
				((el_f |>> (Native_mantissa_width - Mantissa_width)) & Mantissa_mask) as el_m
			el_e: attached (el_exp.as_integer_32 - Native_exponent_bias) as el_e
			normal_value: not v.is_nan and Min_value <= v and v <= Max_value and
				Least_normal_exponent <= el_e implies
				Result = el_s * (2 ^ el_e).truncated_to_real * (1 + el_m * Mantissa_unit)
			subnormal_value: not v.is_nan and Min_value <= v and v <= Max_value and
				Least_subnormal_exponent <= el_e and el_e < Least_normal_exponent implies
				attached
					((el_m | Mantissa_scale) |>> (Least_normal_exponent - el_e)) as el_subm and then
				Result = el_s *
					(2 ^ Least_normal_exponent).truncated_to_real *
					(el_subm * Mantissa_unit)
			Zero: not v.is_nan and Min_value <= v and v <= Max_value and
				el_e < Least_subnormal_exponent implies Result = el_s * 0
		end

feature -- Anchor

	complex_anchor: COMPLEX_NUMBER_IMPL
			-- <Precursor>
		do
			Result := Current
		end

	real_anchor: REAL_NUMBER_IMPL
			-- <Precursor>
		do
			Result := Current
		end

	integer_anchor: INTEGER_NUMBER_IMPL
			-- <Precursor>
		do
			Result := 0
		end

feature  -- Implementation

	native_exponent_width: INTEGER = 8
			-- How many bits a native real number uses to represent its exponent

	native_exponent_mask: NATURAL = 0b1111_1111 -- 2 ^ `native_exponent_width' - 1
			-- Binary mask for the exponent of a native real number

	greatest_native_biased_exponent: INTEGER = 0b1111_1111 -- 2 ^ `native_exponent_width' - 1
			-- Maximum biased value for the exponent of a native real number

	native_exponent_bias: INTEGER = 0b0111_1111 -- (`greatest_native_biased_exponent' - 1) // 2
			-- Bias value for the exponent of a native real number

	native_mantissa_width: INTEGER = 23
			-- How many bits a native real number uses to represent its mantissa

	exponent_width: INTEGER = 3
			-- How many bits a real number uses to represent its exponent

	exponent_mask: NATURAL = 0b111 -- 2 ^ `exponent_width' - 1
			-- Binary mask for the exponent of a real number

	greatest_biased_exponent: INTEGER = 0b111 -- 2 ^ `exponent_width' - 1
			-- Maximum biased value for the exponent of a real number

	exponent_bias, -- (`greatest_biased_exponent' - 1) // 2
			-- Bias value for the exponent of a real number
	greatest_exponent: INTEGER = 0b011 -- `greatest_biased_exponent' - 1 - `exponent_bias'
			-- Maximum unbiased value for the exponent of a real number

	least_normal_exponent: INTEGER = - 2 -- 1 - `exponent_bias'
			-- Minimum unbiased value for the exponent of a normal real number

	least_subnormal_exponent: INTEGER = - 4 -- `least_normal_exponent' - `mantissa_width'
			-- Minimum unbiased value for the exponent of a subnormal real number

	mantissa_width: INTEGER = 2
			-- How many bits a real number uses to represent its mantissa

	mantissa_mask,
			-- Binary mask for the exponent of a real number
	greatest_mantissa: NATURAL = 0b11 -- 2 ^ `mantissa_width' - 1
			-- Maximum value for the mantissa of a real number

	mantissa_scale: NATURAL = 0b100 -- 2 ^ `mantissa_width'
			-- Reference against wich the units of the mantissa of a real number are measured

	mantissa_unit: REAL = 0.25 -- 1 / `mantissa_scale'
			-- Numerical value of a unit in the mantissa of a real number

	real_bit_pattern (r: REAL): NATURAL
			-- The bit pattern of `r' encoded as a {NATURAL} value
			--| Assumptions:
			--| `Result' is encoded as a 32-bit value;
			--| `r' is encoded as a 32-bit, base 2, IEEE 754, floating point number with the
			--| following parameters:
			--| sign bit: 1 bit;
			--| exponent width: 8 bits;
			--| significand (mantissa) precision: 24 bits (23 explicitly stored).
			--| `r' layout: s_eeee_eeee_mmm_mmmm_mmmm_mmmm_mmmm_mmmm
		external
			"C inline"
		alias
			"{
				union {
					EIF_REAL r;
					EIF_NATURAL n;
					} rn;
				rn.r = $r;
				return rn.n;
				}"
		ensure
			class
		end

invariant
	Min_value: not is_nan and not is_negative_infinity implies Min_value <= value
	Max_value: not is_nan and not is_positive_infinity implies value <= Max_value
	Min_value_definition: Min_value = - Max_value
	Max_value_definition:
		Max_value = 2 ^ Greatest_exponent * (1 + Greatest_mantissa * Mantissa_unit)
	Machine_epsilon: Machine_epsilon = 2 ^ 0 * (1 + 1 * Mantissa_unit) - 1
	Epsilon: Epsilon = 2 ^ Least_normal_exponent * (1 + 1 * Mantissa_unit)
	native_real_width: 1+ Native_exponent_width + Native_mantissa_width = {PLATFORM}.Real_32_bits
	Native_exponent_mask:
		Native_exponent_mask = (2 ^ Native_exponent_width - 1).truncated_to_integer.as_natural_32
	Greatest_native_biased_exponent:
		Greatest_native_biased_exponent = Native_exponent_mask.as_integer_32
	Native_exponent_bias: Native_exponent_bias = (Greatest_native_biased_exponent - 1) // 2
	real_width: 1 + Exponent_width + Mantissa_width = 6
	Exponent_mask: Exponent_mask = (2 ^ Exponent_width - 1).truncated_to_integer.as_natural_32
	Greatest_biased_exponent: Greatest_biased_exponent = Exponent_mask.as_integer_32
	Exponent_bias: Exponent_bias = (Greatest_biased_exponent - 1) // 2
	Greatest_exponent: Greatest_exponent = Exponent_bias
	Least_normal_exponent: Least_normal_exponent = 1 - Exponent_bias
	Least_subnormal_exponent: Least_subnormal_exponent = Least_normal_exponent - Mantissa_width
	Mantissa_mask: Mantissa_mask = (2 ^ Mantissa_width - 1).truncated_to_integer.as_natural_32
	Greatest_mantissa: Greatest_mantissa = Mantissa_mask
	Mantissa_scale: Mantissa_scale = (2 ^ Mantissa_width).truncated_to_integer.as_natural_32
	Mantissa_unit: Mantissa_unit = 1 / Mantissa_scale

end
