class interface P_FORMAT

feature(s) from P_FORMAT
   --  Misc character (character set independent)

   is_hexdigit (ch: CHARACTER): BOOLEAN
      --  Is this character hexadecimal? [0-9a-fA-F]


   is_digit (ch: CHARACTER): BOOLEAN
      --  Is this character a digit? [0-9]


   is_alpha (ch: CHARACTER): BOOLEAN
      --  Is this character an ASCII alphabetic character? [a-zA-Z]


   is_lower (ch: CHARACTER): BOOLEAN
      --  Is this character [a-z]?


   is_upper (ch: CHARACTER): BOOLEAN
      --  Is this character [A-Z]?


feature(s) from P_FORMAT
   --  CHARACTER -- ascii case

   to_lower (ch: CHARACTER): CHARACTER
      --  Convert ASCII character to lower case (strictly a-z).

      ensure
         done: not is_upper(Result);
         down: is_upper(ch) implies is_lower(Result);
         keep: not is_upper(ch) implies ch = Result

   to_upper (ch: CHARACTER): CHARACTER
      --  Convert ASCII character to upper case (stricly A-Z).

      ensure
         done: not is_lower(Result);
         up: is_lower(ch) implies is_upper(Result);
         keep: not is_lower(ch) implies ch = Result

feature(s) from P_FORMAT
   --  CHARACTER/INTEGER

   code_to_char (code: INTEGER): CHARACTER
      --  Convert character code (integer) to CHARACTER object.

      ensure
         done: Result.code = code

feature(s) from P_FORMAT
   --  INTEGER/STRING

   int_to_str (int: INTEGER): STRING
      --  Convert integer to string.
      --  Format: "[-](digits)+"

      ensure
         is_copy: Result /= Void

   int_to_str_min (int: INTEGER; min: INTEGER): STRING
      --  Convert integer to string, 
      --  fill with 0 to go up to 'min' digits.

      require
         min_positive: min >= 0
      ensure
         min: Result.count >= min;
         is_copy: Result /= Void

   int_to_hex (int: INTEGER): STRING
      --  Convert integer to string, hexadecimal format.

      ensure
         is_copy: Result /= Void

   int_to_hex_min (int: INTEGER; min: INTEGER): STRING
      --  Convert integer to string, hexadecimal format.
      --  fill with 0 to go up to 'min' digits.

      ensure
         min: Result.count >= min;
         is_copy: Result /= Void

   str_to_int (str: STRING): INTEGER
      --  Convert string to integer.
      --  Format: "[+|-](digits)*"

      require
         valid: str /= Void

feature(s) from P_FORMAT
   --  REAL/STRING, DOUBLE/STRING

   str_to_double (str: STRING): DOUBLE
      --  String to DOUBLE.
      --  Format: "[+|-](digits)*[.[(digits)*]][{e|E}[{+|-}](digits)*]"

      require
         valid: str /= Void

   real_to_str (r: REAL): STRING
      --  Convert REAL to string. 
      --  Format: "[-]E" 

      ensure
         is_copy: Result /= Void

   str_to_real (str: STRING): REAL
      --  Convert string to REAL.

      require
         valid: str /= Void

   double_to_str (r: DOUBLE): STRING
      --  Convert DOUBLE to string.

      ensure
         is_copy: Result /= Void

feature(s) from P_FORMAT
   --  CHARACTER/INTEGER

   char_to_int (ch: CHARACTER): INTEGER
      --  Convert digit character (0-9) to INTEGER.

      require
         valid:  --  ch should be '0'/'9', otherwise Result = 0
      ensure
         done: Result >= 0 and Result < 10

   int_to_char (int: INTEGER): CHARACTER
      --  Convert 0-9 integer to character.

      require
         valid: int >= 0 and int < 10
      ensure
         done: char_to_int(Result) = int

feature(s) from P_FORMAT
   --  hexadecimal CHARACTER/INTEGER

   hex_to_char (int: INTEGER): CHARACTER
      --  Convert hex digit to char.

      require
         hex: int >= 0 and int < 16
      ensure
         done: char_to_hex(Result) = int

   char_to_hex (ch: CHARACTER): INTEGER
      --  Convert hex char to integer.

      require
         hex:  --  ch 0-9A-Za-z
      ensure
         done: Result >= 0 and Result < 16

feature(s) from P_FORMAT
   --  Strings & characters

   index_of (str: STRING; ch: CHARACTER): INTEGER
      --  Index of first occurence of 'ch' in 'str'.
      --  Time: O(str.count)

      require
         valid: str /= Void
      ensure
         done: not has_character(str,ch) = Result = 0;
         found: Result > 0 implies str.item(Result) = ch

   index_of_last (str: STRING; ch: CHARACTER): INTEGER
      --  Index of last occurence of 'ch' in 'str'.
      --  Time: O(str.count)

      require
         valid: str /= Void
      ensure
         done: not has_character(str,ch) = Result = 0;
         found: Result > 0 implies str.item(Result) = ch

   has_character (str: STRING; ch: CHARACTER): BOOLEAN
      --  Does 'str' has 'ch'?
      --  Time: O(str.count)

      require
         valid: str /= Void

feature(s) from P_FORMAT
   --  String utilities

   tokenize (input: STRING; separators: STRING): P_LIST[STRING]
      --  Basic tokeniser for a string, returns a list of tokens 
      --  made of chars which are not in 'separators'.

      require
         valid_input: input /= Void;
         valid_separator: separators /= Void
      ensure
         not_void: Result /= Void

   start_case_equal (a, b: STRING): BOOLEAN
      --  Test case-independently if two strings have equal beginnings.

      require
         valid: a /= Void and b /= Void

   start_equal (a, b: STRING): BOOLEAN
      --  Test if two strings have equal beginnings.

      require
         valid: a /= Void and b /= Void

   case_equal (a, b: STRING): BOOLEAN
      --  Test case-independently if two strings are equal.

      require
         valid: a /= Void and b /= Void

   invert (str: STRING)
      --  Invert string.
      --  Time: O(str.count)

      require
         valid: str /= Void
      ensure
         done:  --  invert(str) = old str


end of P_FORMAT