class interface NUMBER_FRACTION
   --
   -- To implement NUMBER (do not use this class, see NUMBER).
   --

creation
   make (n, d: ABSTRACT_INTEGER; s: BOOLEAN)
      -- Create a simplified large_fraction

      require
         n.is_positive;
         d.is_positive;
         not ((n \\ d) @= 0)

   make_simply (n, d: ABSTRACT_INTEGER; s: BOOLEAN)
      -- create a large_fraction without simplify it

      require
         n.is_positive;
         d.is_positive;
         not ((n \\ d) @= 0)

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
      -- Difference of Current and other.

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

   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

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 ?


   is_one: BOOLEAN
      -- Is it 1 ?


   is_positive: BOOLEAN
      -- Is Current greater or equal zero ?

      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_string: STRING
      -- Convert the NUMBER into a new allocated STRING.
      -- Note: see also append_in to save memory.


   append_in (string: 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
         string /= 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
      -- Difference of Current and other.

      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?

      require
         other /= minimum_integer
      ensure
         Result = not (Current @>= other)

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

      require
         other /= minimum_integer
      ensure
         Result = not (Current @> other)

   infix "@>" (other: INTEGER): BOOLEAN
      -- Is Current strictly greater than other?

      require
         other /= minimum_integer
      ensure
         Result = not (Current @<= other)

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

      require
         other /= minimum_integer
      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.


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


invariant
   not (numerator.is_small_integer and denominator.is_small_integer);

end of NUMBER_FRACTION