expanded class interface INTEGER
   --
   -- 32 bits signed integer.
   --

feature(s) from HASHABLE   hash_code: INTEGER
      -- The hash-code value of Current.

      ensure
         good_hash_value: Result >= 0

feature(s) from NUMERIC   infix "+" (other: like Current): like item
      -- Sum with other (commutative).
      --      require
      --        other /= Void

      require
         no_overflow: item > 0 = (other.item > 0) implies Current #+ other > 0 = (item > 0) -- this means: if operand are of same sign, it will be sign 
 -- of the Result.
      ensure
         Result #- other.item = item

   infix "-" (other: like Current): like item
      -- Result of substracting other.
      --      require
      --         other /= Void

      require
         no_overflow: item > 0 /= (other.item > 0) implies Current #- other > 0 = (item > 0) -- this means: if operand are of different sign, sign of the 
 -- Result will be the same sign as item.
      ensure
         Result #+ other.item = item

   infix "*" (other: like Current): like item
      -- Product by other.
      --      require
      --         other /= Void

      require
         no_overflow: divisible(other) implies item #* other.item // other.item = item
      ensure
         item /= 0 and other.item /= 0 implies Result /= 0;
         Result /= 0 implies Result // other.item = item;
         Result /= 0 implies Result \\ other.item = 0

   infix "/" (other: like Current): DOUBLE
      -- Division by other.

      require
         other /= Void;
         divisible(other)

   prefix "+": like Current
      -- Unary plus of Current.


   prefix "-": like item
      -- Unary minus of Current.

      require
         not_minimum_value: item = 0 or else item |<< 1 /= 0

   divisible (other: like Current): BOOLEAN
      -- May Current be divided by other ?

      require
         other /= Void

   one: INTEGER_8
      -- Neutral element for "*" and "/".


   zero: INTEGER_8
      -- Neutral element for "+" and "-".


   sign: INTEGER_8
      -- Sign of Current (0 -1 or 1).

      ensure
         -1 <= Result;
         Result <= 1

feature(s) from COMPARABLE   is_equal (other: like Current): BOOLEAN
      -- Is other attached to an object considered equal to
      -- current object ?

      require
         other /= Void
      ensure
         generating_type = other.generating_type implies Result = other.is_equal(Current)

   infix "<" (other: like Current): BOOLEAN
      -- Is Current strictly less than other?

      require
         other_exists: other /= Void
      ensure
         asymmetric: Result implies not (other < Current)

   infix "<=" (other: like Current): BOOLEAN
      require
         other_exists: other /= Void
      ensure
         definition: Result = (Current < other or is_equal(other))

   infix ">" (other: like Current): BOOLEAN
      require
         other_exists: other /= Void
      ensure
         definition: Result = (other < Current)

   infix ">=" (other: like Current): BOOLEAN
      require
         other_exists: other /= Void
      ensure
         definition: Result = (other <= Current)

   in_range (lower, upper: like Current): BOOLEAN
      -- Return true if Current is in range [lower..upper]

      ensure
         Result = (Current >= lower and Current <= upper)

   compare (other: like Current): INTEGER
      -- If current object equal to other, 0
      -- if smaller,  -1; if greater, 1.

      require
         other_exists: other /= Void
      ensure
         equal_zero: Result = 0 = is_equal(other);
         smaller_negative: Result = -1 = (Current < other);
         greater_positive: Result = 1 = (Current > other)

   three_way_comparison (other: like Current): INTEGER
      -- If current object equal to other, 0
      -- if smaller,  -1; if greater, 1.

      require
         other_exists: other /= Void
      ensure
         equal_zero: Result = 0 = is_equal(other);
         smaller_negative: Result = -1 = (Current < other);
         greater_positive: Result = 1 = (Current > other)

   min (other: like Current): like Current
      -- Minimum of Current and other.

      require
         other /= Void
      ensure
         Result <= Current and then Result <= other;
         compare(Result) = 0 or else other.compare(Result) = 0

   max (other: like Current): like Current
      -- Maximum of Current and other.

      require
         other /= Void
      ensure
         Result >= Current and then Result >= other;
         compare(Result) = 0 or else other.compare(Result) = 0

feature(s) from INTEGER_GENERAL   item: INTEGER
      -- Access to the expanded value of Current. (The type of 
      -- item is INTEGER_8 or INTEGER_16 or INTEGER_32 or INTEGER_64.)


   infix "//" (other: like Current): like item
      -- Integer division of Current by other


   infix "\\" (other: like Current): like item
      -- Remainder of integer division of Current by other


   infix "^" (exp: like Current): INTEGER_64
      -- Integer power of Current by other

      require
         exp >= 0

   abs: like Current
      -- Absolute value of Current.

      require
         not_minimum_value: item = 0 or else item |<< 1 /= 0

   odd: BOOLEAN
      -- Is odd ?


   even: BOOLEAN
      -- Is even ?


   sqrt: DOUBLE
      -- Compute the square routine.

      require
         item >= 0

   log: DOUBLE
      -- (ANSI C log).

      require
         item > 0

   log10: DOUBLE
      -- (ANSI C log10).

      require
         item > 0

   gcd (other: like Current): like item
      -- Great Common Divisor of Current and other.

      require
         Current >= 0;
         other >= 0
      ensure
         Result.is_equal(other.gcd(Current))

feature(s) from INTEGER_GENERAL
   -- Conversions:

   to_real: REAL

   to_double: DOUBLE

   to_string: STRING
      -- Convert the decimal view of Current into a new allocated 
      -- STRING. For example, if Current is -1 the new STRING is "-1".
      -- Note: see also append_in to save memory.


   to_unicode_string: UNICODE_STRING
      -- Convert the decimal view of Current into a new allocated 
      -- UNICODE_STRING. For example, if Current is -1 the new 
      -- UNICODE_STRING is U"-1".
      -- Note: see also append_in_unicode to save memory.


   to_boolean: BOOLEAN
      -- Return false for 0, otherwise true.

      ensure
         Result = (Current.item /= 0)

   fit_integer_8: BOOLEAN
      -- Does Current fit on an INTEGER_8 ?

      ensure
         Result = Current.in_range(-128,127)

   to_integer_8: INTEGER_8
      -- Explicit conversion to INTEGER_8.

      require
         fit_integer_8
      ensure
         Current.is_equal(Result)

   fit_integer_16: BOOLEAN
      -- Does Current fit on an INTEGER_16 ?

      ensure
         Result = Current.in_range(-32768,32767)

   to_integer_16: INTEGER_16
      -- Explicit conversion to INTEGER_16.

      require
         fit_integer_16
      ensure
         Current.is_equal(Result)

   fit_integer_32: BOOLEAN
      -- Does Current fit on an INTEGER_32 ?


   fit_integer: BOOLEAN
      -- Does Current fit on an INTEGER_32 ?


   to_integer_32: INTEGER_32
      -- Explicit conversion to INTEGER_32.

      require
         fit_integer_32
      ensure
         Current.is_equal(Result)

   to_integer: INTEGER_32
      -- Explicit conversion to INTEGER_32.

      require
         fit_integer_32
      ensure
         Current.is_equal(Result)

   to_integer_64: INTEGER_64
      -- Explicit conversion to INTEGER_64.

      ensure
         Current.is_equal(Result)

   to_number: NUMBER
      ensure
         Result @= Current.to_integer

   to_bit: BIT_N integer_bits
      -- Portable BIT_N conversion.


   append_in (buffer: STRING)
      -- Append in the buffer the equivalent of to_string. No new 
      -- STRING creation during the process.

      require
         buffer /= Void

   append_in_unicode (buffer: UNICODE_STRING)
      -- Append in the buffer the equivalent of to_unicode_string. No 
      -- new UNICODE_STRING creation during the process.

      require
         buffer /= Void

   to_string_format (s: INTEGER): STRING
      -- Same as to_string but the result is on s character and the
      -- number is right aligned.
      -- Note: see append_in_format to save memory.

      require
         to_string.count <= s
      ensure
         Result.count = s

   to_unicode_string_format (s: INTEGER): UNICODE_STRING
      -- Same as to_unicode_string but the result is on s character and 
      -- the number is right aligned.
      -- Note: see append_in_unicode_format to save memory.

      require
         to_string.count <= s
      ensure
         Result.count = s

   append_in_format (str: STRING; s: INTEGER)
      -- Append the equivalent of to_string_format at the end of
      -- str. Thus you can save memory because no other
      -- STRING is allocate for the job.

      require
         to_string.count <= s
      ensure
         str.count >= old str.count + s

   append_in_unicode_format (str: UNICODE_STRING; s: INTEGER)
      -- Append the equivalent of to_unicode_string_format at the end of
      -- str. Thus you can save memory because no other
      -- UNICODE_STRING is allocate for the job.

      require
         to_string.count <= s
      ensure
         str.count >= old str.count + s

   decimal_digit: CHARACTER
      -- Gives the corresponding CHARACTER for range 0..9.

      require
         in_range(0,9)
      ensure
         (once "0123456789").has(Result);
         Current.is_equal(Result.value)

   digit: CHARACTER
      -- Gives the corresponding CHARACTER for range 0..9.

      require
         in_range(0,9)
      ensure
         (once "0123456789").has(Result);
         Current.is_equal(Result.value)

   hexadecimal_digit: CHARACTER
      -- Gives the corresponding CHARACTER for range 0..15.

      require
         in_range(0,15)
      ensure
         (once "0123456789ABCDEF").has(Result)

   to_character: CHARACTER
      -- Return the coresponding ASCII character.

      require
         Current >= 0

   to_octal_in (buffer: STRING)
      -- Append in buffer the octal view of Current. No new 
      -- STRING creation during the process.
      -- For example, if Current is -1 and if Current is a 
      -- 16 bits integer the Result is "177777".
      -- Note: see also to_hexadecimal_in to save memory.

      ensure
         buffer.count = old buffer.count + object_size * 8 // 3 + 1

   to_hexadecimal: STRING
      -- Convert the hexadecimal view of Current into a new allocated
      -- STRING. For example, if Current is -1 and if Current is a 
      -- 32 bits integer the Result is "FFFFFFFF".
      -- Note: see also to_hexadecimal_in to save memory.

      ensure
         Result.count = object_size * 2

   to_hexadecimal_in (buffer: STRING)
      -- Append in buffer the equivalent of to_hexadecimal. No new 
      -- STRING creation during the process.

      ensure
         buffer.count = old buffer.count + object_size * 2

feature(s) from INTEGER_GENERAL
   -- Bitwise Logical Operators:

   bit_test (idx: INTEGER_8): BOOLEAN
      -- The value of the idx-ith bit (the right-most bit is at 
      -- index 0).

      require
         idx >= 0

   infix "|>>" (s: INTEGER_8): like item
      -- Shift by s positions right (sign bit copied) bits falling 
      -- off the end are lost.

      require
         s >= 0

   bit_shift_right (s: INTEGER_8): like item
      -- Shift by s positions right (sign bit copied) bits falling 
      -- off the end are lost.

      require
         s >= 0

   infix "|>>>" (s: INTEGER_8): like item
      -- Shift by s positions right (sign bit not copied) bits
      -- falling off the end are lost.

      require
         s >= 0

   bit_shift_right_unsigned (s: INTEGER_8): like item
      -- Shift by s positions right (sign bit not copied) bits
      -- falling off the end are lost.

      require
         s >= 0

   infix "|<<" (s: INTEGER_8): like item
      -- Shift by s positions left bits falling off the end are lost.

      require
         s >= 0

   bit_shift_left (s: INTEGER_8): like item
      -- Shift by s positions left bits falling off the end are lost.

      require
         s >= 0

   infix "#>>" (s: INTEGER_8): like item
      -- Rotate by s positions right.

      require
         s >= 0

   bit_rotate_right (s: INTEGER_8): like item
      -- Rotate by s positions right.

      require
         s >= 0

   infix "#<<" (s: INTEGER_8): like item
      -- Rotate by s positions left.

      require
         s >= 0

   bit_rotate_left (s: INTEGER_8): like item
      -- Rotate by s positions left.

      require
         s >= 0

   bit_rotate (s: INTEGER_8): like item
      -- Rotate by s positions (positive s shifts right, negative left
      -- See also infix "#>>" and infix "#<<".


   prefix "~": like item
      -- One's complement of Current.


   bit_not: like item
      -- One's complement of Current.


   infix "&" (other: like Current): like item
      -- Bitwise logical and of Current with other.


   bit_and (other: like Current): like item
      -- Bitwise logical and of Current with other.


   infix "|" (other: like Current): like item
      -- Bitwise logical inclusive or of Current with other.


   bit_or (other: like Current): like item
      -- Bitwise logical inclusive or of Current with other.


   bit_xor (other: like Current): like item
      -- Bitwise logical exclusive or of Current with other.


   bit_shift (s: INTEGER_8): like item
      -- Shift by s positions (positive s shifts right (sign bit 
      -- copied), negative shifts left bits falling off the end are lost).
      -- See also infix "|>>" and infix "|<<".


   bit_shift_unsigned (s: INTEGER_8): like item
      -- Shift by s positions (positive s shifts right (sign bit not 
      -- copied), negative left bits falling off the end are lost).
      -- See also infix "|>>>" and infix "|<<".


feature(s) from INTEGER_GENERAL
   -- Object Printing:

   out_in_tagged_out_memory
      -- Append terse printable represention of current object
      -- in tagged_out_memory.

      ensure
         not_cleared: tagged_out_memory.count >= old tagged_out_memory.count;
         append_only: (old tagged_out_memory.twin).is_equal(tagged_out_memory.substring(1,old tagged_out_memory.count))

   fill_tagged_out_memory
      -- Append terse printable represention of current object
      -- in tagged_out_memory.


feature(s) from INTEGER_GENERAL
   -- For experts only: native operators with potential overflow

   infix "#+" (other: like Current): like item

   infix "#-" (other: like Current): like item

   infix "#*" (other: like Current): like item

feature(s) from INTEGER   low_16: INTEGER_16
      -- The 16 low bits of Current (i.e. the right-most part).


   high_16: INTEGER_16
      -- The 16 high bits of Current (i.e. the left-most part).


feature(s) from INTEGER
   -- For experts only:

   set_item (value: like item)
      ensure
         item = value



end of expanded INTEGER