deferred class interface NUMBER
   --
   -- This abstract definition of a NUMBER is intended to be the unique
   -- view of the client (do not use sub-classes names at all in the
   -- client code). In order to create NUMBERs without using concrete
   -- class name, the client code can inherit NUMBER_TOOLS. (See directory
   -- ${SmartEiffel}/tutorial/number for example.)
   --

feature(s) from HASHABLE
   hash_code: INTEGER
      -- The hash-code value of Current.
      ensure
         good_hash_value: Result >= 0

feature(s) from NUMBER
   -- Binary operators for two NUMBERs:

   infix "+" (other: NUMBER): NUMBER
      -- Sum of Current and other.
      require
         other /= Void
      ensure
         (Result - other).is_equal(Current)

   infix "-" (other: NUMBER): NUMBER
      -- Difference of Current and other.
      require
         other /= Void
      ensure
         (Result + other).is_equal(Current)

   infix "*" (other: NUMBER): NUMBER
      -- Product of Current and other.
      require
         other /= Void
      ensure
         Result /= Void

   infix "/" (other: NUMBER): NUMBER
      -- Quotient of Current and other.
      require
         not (other @= 0);
         divisible(other)
      ensure
         Result /= Void

   infix "//" (other: NUMBER): NUMBER
      -- Divide Current by other (Integer division).
      require
         is_abstract_integer;
         other.is_abstract_integer;
         divisible(other)
      ensure
         Result.is_abstract_integer

   infix "\\" (other: NUMBER): NUMBER
      -- Remainder of division of Current by other.
      require
         is_abstract_integer;
         other.is_abstract_integer;
         divisible(other)
      ensure
         Result.is_abstract_integer

   infix "^" (exp: NUMBER): NUMBER
      -- Current raised to exp-th power.
      require
         exp.is_abstract_integer;
         exp.is_positive;
         not (is_zero and then exp.is_zero)
      ensure
         Result /= Void;
         exp.is_zero implies Result.is_one

   infix "<" (other: NUMBER): BOOLEAN
      -- Is Current strictly less than other?
      require
         other_exists: other /= Void
      ensure
         asymmetric: Result implies not (other <= Current)

   infix "<=" (other: NUMBER): BOOLEAN
      -- Is Current less or equal than other?
      require
         other_exists: other /= Void
      ensure
         definition: Result = (Current < other) or is_equal(other)

   infix ">" (other: NUMBER): BOOLEAN
      -- Is Current strictly greater than other?
      require
         other_exists: other /= Void
      ensure
         definition: Result = (other < Current)

   infix ">=" (other: NUMBER): BOOLEAN
      -- Is Current greater or equal than other?
      require
         other_exists: other /= Void
      ensure
         definition: Result = (other <= Current)

   gcd (other: NUMBER): ABSTRACT_INTEGER
      -- Great Common Divisor of Current and other.
      require
         other.is_abstract_integer;
         is_abstract_integer;
         is_positive;
         other.is_positive

feature(s) from NUMBER
   -- Unary operators for two NUMBERs:

   prefix "+": NUMBER
      -- Unary plus of Current.
      ensure
         Result = Current

   prefix "-": NUMBER
      -- Opposite of Current.
      ensure
         Result /= Void

feature(s) from NUMBER
   -- To know more about a NUMBER:

   in_range (lower, upper: NUMBER): BOOLEAN
      -- Return true if Current is in range [lower..upper]
      ensure
         Result = (Current >= lower and Current <= upper)

   compare (other: NUMBER): INTEGER
      -- Compare Current with other.
      -- <  <==> Result < 0
      -- >  <==> Result > 0
      -- Otherwise Result = 0.
      require
         other /= Void
      ensure
         Result < 0 = (Current < other);
         Result = 0 = not (Current < other or Current > other);
         Result > 0 = (Current > other)

   min (other: NUMBER): NUMBER
      -- 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: NUMBER): NUMBER
      -- Maximum of Current and other.
      require
         other /= Void
      ensure
         Result >= Current and then Result >= other;
         compare(Result) = 0 or else other.compare(Result) = 0

   is_zero: BOOLEAN
      -- Is it 0 ?
      ensure
         Result = Current @= 0

   is_one: BOOLEAN
      -- Is it 1 ?
      ensure
         Result = Current @= 1

   is_positive: BOOLEAN
      -- Is Current greater or equal zero ?
      ensure
         Result = Current @>= 0

   is_negative: BOOLEAN
      -- Is Current < 0 ?
      ensure
         Result = Current @< 0

   is_odd: BOOLEAN
      -- Is odd ?
      require
         is_abstract_integer

   odd: BOOLEAN
      -- Is odd ?
      require
         is_abstract_integer

   is_even: BOOLEAN
      -- Is even ?
      require
         is_abstract_integer

   even: BOOLEAN
      -- Is even ?
      require
         is_abstract_integer

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

   is_abstract_integer: BOOLEAN

   is_abstract_fraction: BOOLEAN

   is_integer: BOOLEAN
      -- Does Current value fit on an INTEGER ?
      ensure
         Result implies is_abstract_integer

   is_double: BOOLEAN

feature(s) from NUMBER
   -- Conversions and printing:

   to_integer: INTEGER
      -- Conversion of Current in an INTEGER.
      require
         is_integer

   to_double: DOUBLE
      -- Conversion of Current in a DOUBLE.
      require
         is_double

   to_string: STRING
      -- Convert the NUMBER into a new allocated STRING.
      -- Note: see also append_in to save memory.

   append_in (buffer: STRING)
      -- Append the equivalent of to_string at the end of buffer. 
      -- Thus you can save memory because no other STRING is allocated 
      -- for the job.
      require
         buffer /= Void

   to_decimal (digits: INTEGER; all_digits: BOOLEAN): STRING
      -- Convert Current into its decimal view. A maximum of decimal 
      -- digits places will be used for the decimal part. If the 
      -- all_digits flag is true insignificant digits will be included 
      -- as well. (See also decimal_in to save memory.)
      require
         non_negative_digits: digits >= 0
      ensure
         not Result.is_empty

   append_decimal_in (buffer: STRING; digits: INTEGER; all_digits: BOOLEAN)
      -- Append the equivalent of to_decimal at the end of buffer. Thus 
      -- you can save memory because no other STRING is allocated.
      require
         non_negative_digits: digits >= 0

   digit: CHARACTER
      -- Gives the corresponding CHARACTER for range 0..9.
      require
         to_integer.in_range(0,9)
      ensure
         (once "0123456789").has(Result);
         Current @= Result.value

feature(s) from NUMBER
   -- To mimic NUMERIC:

   divisible (other: NUMBER): BOOLEAN
      -- Is other a valid divisor for Current ?
      require
         other /= Void

   one: NUMBER
      -- The neutral element of multiplication.
      ensure
         neutral_element:  -- Result is the neutral element of
 -- multiplication.

   zero: NUMBER
      -- The neutral element of addition.
      ensure
         neutral_element:  -- Result is the neutral element of
 -- addition.

   sign: INTEGER

   sqrt: DOUBLE
      -- Compute the square routine.
      require
         is_double

   log: DOUBLE
      require
         is_double

   abs: NUMBER

feature(s) from NUMBER
   -- To mix NUMBER and INTEGER:

   infix "@+" (other: INTEGER): NUMBER
      -- Sum of Current and other.
      ensure
         Result /= Void

   infix "@-" (other: INTEGER): NUMBER
      -- Difference of Current and other.
      ensure
         Result /= Void

   infix "@*" (other: INTEGER): NUMBER
      require
         other /= Void
      ensure
         Result /= Void

   infix "@/" (other: INTEGER): NUMBER
      -- Quotient of Current and other.
      require
         other /= 0
      ensure
         Result /= Void

   infix "@//" (other: INTEGER): NUMBER
      -- Divide Current by other (Integer division).
      require
         is_abstract_integer;
         other /= 0
      ensure
         Result.is_abstract_integer

   infix "@\\" (other: INTEGER): NUMBER
      -- Remainder of division of Current by other.
      require
         is_abstract_integer;
         other /= 0
      ensure
         Result.is_abstract_integer

   infix "@^" (exp: INTEGER): NUMBER
      require
         exp > 0 or else not is_zero
      ensure
         Result /= Void;
         Result /= Current implies exp /= 1 or else not is_zero

   infix "@=" (other: INTEGER): BOOLEAN
      -- Is Current equal other ?

   infix "@<" (other: INTEGER): BOOLEAN
      -- Is Current strictly less than other?
      ensure
         Result = not (Current @>= other)

   infix "@<=" (other: INTEGER): BOOLEAN
      -- Is Current less or equal other?
      ensure
         Result = not (Current @> other)

   infix "@>" (other: INTEGER): BOOLEAN
      -- Is Current strictly greater than other?
      ensure
         Result = not (Current @<= other)

   infix "@>=" (other: INTEGER): BOOLEAN
      -- Is Current greater or equal than other?
      ensure
         Result = not (Current @< other)

feature(s) from NUMBER
   -- To mix NUMBER and DOUBLE:

   infix "#=" (other: DOUBLE): BOOLEAN
      -- Is Current equal other?

   infix "#<" (other: DOUBLE): BOOLEAN
      -- Is Current strictly less than other?
      ensure
         Result implies not (Current #>= other)

   infix "#<=" (other: DOUBLE): BOOLEAN
      -- Is Current less or equal other?
      ensure
         Result = not (Current #> other)

   infix "#>" (other: DOUBLE): BOOLEAN
      -- Is Current strictly greater than other?
      ensure
         Result = not (Current #<= other)

   infix "#>=" (other: DOUBLE): BOOLEAN
      -- Is Current greater or equal than other?
      ensure
         Result = not (Current #< other)

feature(s) from NUMBER
   -- Misc:

   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.

   inverse: NUMBER
      require
         divisible(Current)
      ensure
         Result /= Void

   factorial: NUMBER
      require
         is_abstract_integer;
         is_positive
      ensure
         Result.is_abstract_integer;
         Result.is_positive



end of deferred NUMBER