class interface MUTABLE_BIG_INTEGER
   --
   -- WARNING: THIS CLASS IS NOT YET FINISHED. DO NOT USE.
   --
   -- A class used to represent multiprecision integers that makes efficient
   -- use of allocated space by allowing a number to occupy only part of
   -- an array so that the arrays do not have to be reallocated as often.
   -- When performing an operation with many iterations the array used to
   -- hold a number is only reallocated when necessary and does not have to
   -- be the same size as the number it represents. A mutable number allows
   -- calculations to occur on the same number without having to create
   -- a new number for every step of the calculation as occurs with NUMBERs.
   --

creation
   from_integer (value: INTEGER)
      -- Create or set Current using value as an initializer.
      -- directly allocate a storage of 4 INTEGER cause it's non-sense to use
      -- mutable_big_integer to perform calculation that could fit in an 
      -- INTEGER_64

      ensure
         to_integer = value

   from_integer_64 (value: INTEGER_64)
      -- Create or set Current using value as an initializer.
      -- directly allocate a storage of 4 INTEGER cause it's non-sense to use
      -- mutable_big_integer to perform calculation that could fit in an INTEGER_64

      ensure
         to_integer_64 = value

   copy (other: like Current)
      -- Update current object using fields of object attached
      -- to other, so as to yield equal objects.
      -- Note: you can't copy object from a different dynamic type.

      require
         same_dynamic_type(other)
      ensure
         is_equal(other)

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);
         trichotomy: Result = (not (Current < other) and not (other < 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
      -- Is Current less than or equal other?

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

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

      require
         other_exists: other /= Void
      ensure
         definition: Result = (other < Current)

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

      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 HASHABLE   hash_code: INTEGER
      -- The hash-code value of Current.

      ensure
         good_hash_value: Result >= 0

feature(s) from MUTABLE_BIG_INTEGER
   -- Creation/initialization from INTEGER_32 or INTEGER_64:

   from_integer (value: INTEGER)
      -- Create or set Current using value as an initializer.
      -- directly allocate a storage of 4 INTEGER cause it's non-sense to use
      -- mutable_big_integer to perform calculation that could fit in an 
      -- INTEGER_64

      ensure
         to_integer = value

   is_integer: BOOLEAN
      -- Do Current fit on an INTEGER_32?

      ensure
         Result implies is_integer_64

   to_integer: INTEGER
      -- Convert Current as a 32 bit INTEGER.

      require
         is_integer

   from_integer_64 (value: INTEGER_64)
      -- Create or set Current using value as an initializer.
      -- directly allocate a storage of 4 INTEGER cause it's non-sense to use
      -- mutable_big_integer to perform calculation that could fit in an INTEGER_64

      ensure
         to_integer_64 = value

   is_integer_64: BOOLEAN
      -- Do Current fit on an INTEGER_64?

      ensure
         not Result implies not is_integer

   to_integer_64: INTEGER_64
      -- Convert Current as a INTEGER_64.

      require
         is_integer_64

feature(s) from MUTABLE_BIG_INTEGER
   -- Addition:

   add (other: like Current)
      -- Add other into Current.

      require
         other /= Void

   add_integer (other: INTEGER_32)
      -- Add other into Current.


   add_integer_64 (other: INTEGER_64)
      -- Add other into Current.


   add_natural (other: like Current)
      -- Same behavior as add, but this one works only when Current 
      -- and other are both positive numbers and are both greater than 
      -- zero. The only one advantage of using add_natural instead of the 
      -- general add is the gain of efficiency.

      require
         not is_zero and not is_negative;
         not other.is_zero and not other.is_negative

feature(s) from MUTABLE_BIG_INTEGER
   -- Subtract:

   subtract (other: like Current)
      -- Subtract other from Current.

      require
         other /= Void

   subtract_integer (other: INTEGER_32)

feature(s) from MUTABLE_BIG_INTEGER
   -- To divide:

   divide (other, quotient, remainder: like Current)
      -- Calculates the quotient and remainder of Current 
      -- divided by other. (The contents of Current and other are 
      -- not changed.)
      --
      -- Note: Uses Algorithm D in Knuth section 4.3.1. Many 
      -- optimizations to that algorithm have been adapted from the Colin
      -- Plumb C library. It special cases one word divisors for speed.

      require
         not other.is_zero

   left_shift (n: INTEGER_32)
      -- If there is enough storage space in storage already
      -- the available space will be used. Space to the right of the used
      -- ints in the storage array is faster to utilize, so the extra
      -- space will be taken from the right if possible.


   right_shift (n: INTEGER_32)
      -- Right shift Current n bits. (Current is left in normal form.)

      require
         n > 0

feature(s) from MUTABLE_BIG_INTEGER
   -- To multiply:

   multiply (other, res: like Current)
      -- Multiply the contents of Current and other and place the 
      -- result  in res. (Current and other are not modified.)

      require
         other /= Void;
         res /= Void

   multiply_integer (other: INTEGER; res: like Current)
      -- Multiply the contents of Current and other and place the 
      -- result  in res. (Current is not modified.)

      require
         other /= Void;
         res /= Void

feature(s) from MUTABLE_BIG_INTEGER
   -- Comparison:

   is_zero: BOOLEAN
      -- Is it 0?

      ensure
         Result implies not is_negative

   is_one: BOOLEAN
      -- Is it 1?

      ensure
         Result implies not is_negative

   is_one_negative: BOOLEAN
      -- Is it -1?

      ensure
         Result implies is_negative

   is_negative: BOOLEAN
      -- Is Current negative integer?


   is_even: BOOLEAN
      -- Is Current even?

      ensure
         Result = not Current.is_odd

   is_odd: BOOLEAN
      -- Is Current odd?

      ensure
         Result = not Current.is_even

   abs_compare (other: like Current): INTEGER
      -- Compare the magnitude of Current and other. Returns -1, 0 or 1
      -- as this MutableBigInteger is numerically less than, equal to, or
      -- greater than other. 


feature(s) from MUTABLE_BIG_INTEGER
   -- Printing:

   to_string: STRING
      -- Create a decimal view of the Current big integer.
      -- Note: see also append_in to save memory.


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


   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 MUTABLE_BIG_INTEGER
   -- Miscellaneous:

   negate
      -- Negate the sign of Current.

      ensure
         is_zero implies not is_negative

   set_with_zero
      ensure
         is_zero

   copy (other: like Current)
      -- Update current object using fields of object attached
      -- to other, so as to yield equal objects.
      -- Note: you can't copy object from a different dynamic type.

      require
         same_dynamic_type(other)
      ensure
         is_equal(other)

   swap_with (other: like Current)
      -- Swap the value of Current with the value of other.



invariant
   capacity > 0 = storage.is_not_null;
   integer_length.in_range(0,capacity);
   integer_length /= 0 implies offset.in_range(0,capacity - 1);
   integer_length /= 0 implies item(offset) /= 0;
   integer_length = 0 implies not negative;

end of MUTABLE_BIG_INTEGER