class interface P_INTEGER_DECODER

creation
   make (new_base: INTEGER)
      require
         ok: new_base > 2

feature(s) from P_INTEGER_DECODER
   --  Creation

   make (new_base: INTEGER)
      require
         ok: new_base > 2

feature(s) from P_INTEGER_DECODER
   --  Base

   base: INTEGER

feature(s) from P_INTEGER_DECODER
   --  Integer

   extend (digit: CHARACTER)
      --  Add right digit.

      require
         base: is_digit(digit)
      ensure
         done_integer: value = old value * base + char_to_int(digit);
         done_digits: digits = old digits + 1

   reset
      ensure
         ok: value = 0 and digits = 0

   value: INTEGER
      --  Current integer.


   digits: INTEGER
      --  Number of converted digits (not including sign).


feature(s) from P_INTEGER_DECODER
   --  String to integer

   from_string (str: STRING)
      require
         ok: str /= Void

feature(s) from P_INTEGER_DECODER
   --  Digit level

   int_to_char (digit: INTEGER): CHARACTER
      --  Integer to character digit.

      require
         ok: digit >= 0 and digit < base
      ensure
         good_base: is_digit(Result);
         done: char_to_int(Result) = digit

   char_to_int (c: CHARACTER): INTEGER
      --  Character to integer.

      require
         is_intchar: is_digit(c)
      ensure
         good_base: Result >= 0 and Result < base; --  (case sensitive) int_to_char(Result) = c
         done: 

   is_digit (c: CHARACTER): BOOLEAN
      --  Is this character a valid digit?


feature(s) from P_INTEGER_DECODER
   --  Encode

   value_to_string (int: INTEGER): STRING
      --  Encode character.

      ensure
         is_copy: Result /= Void;
         done: Result.count > 0

invariant
   base_ok: base >= 2 and base <= digit_table.count;

end of P_INTEGER_DECODER