class interface P_SHRINK_STRING

creation
   make (a_string: STRING)
      --  Setup virtual string.

      require
         not_void: a_string /= Void

feature(s) from P_SHRINK_STRING
   --  Conversion

   to_string: STRING
      --  String (non mutable, may be original) corresponding to the 
      --  correspondingly shrinked string.


feature(s) from P_SHRINK_STRING
   --  General

   is_equal (s_string: like Current): BOOLEAN
      --  Equality.

      require
         other_not_void: s_string /= Void
      ensure
         consistent: standard_is_equal(s_string) implies Result;
         symmetric: Result implies s_string.is_equal(Current)

   is_start (other: P_SHRINK_STRING): BOOLEAN
      --  Is current start of other?

      require
         not_void: other /= Void

   is_first_one_of (some_chars: STRING): BOOLEAN
      --  Is first character a character from some_chars?

      require
         has_first: count > 0;
         chars_not_void: some_chars /= Void

   duplicate: P_SHRINK_STRING
      --  New shrink string equal to this one.


feature(s) from P_SHRINK_STRING
   --  Operation(s)

   remove_first
      --  Remove a character at start

      require
         has_char: count > 0
      ensure
         done: count = old count - 1

   remove_start (n: INTEGER)
      --  Remove 'n' characters at start.

      require
         has_chars: count >= n
      ensure
         done: count = old count - n

   remove_last
      --  Remove character at end.

      require
         has_char: count > 0
      ensure
         done: count = old count - 1

   remove_end (n: INTEGER)
      --  Remove 'n' characters at end.

      require
         has_chars: count >= n
      ensure
         done: count = old count - n

   skip_character (a_char: CHARACTER)
      --  Remove all occurences of character at start of virtual string. 

      ensure
         skipped: is_empty or else first /= a_char;
         shrinked: count <= old count

   skip_characters (some_chars: STRING)
      --  Remove all occurences of characters in 'some_chars' at start of virtual string. 

      require
         not_void: some_chars /= Void;
         not_empty: not some_chars.empty
      ensure
         shrinked: count <= old count

   count: INTEGER
      --  Number of characters in virtual string.

      ensure
         positive: count >= 0

   is_empty: BOOLEAN
      --  Empty virtual string?


   item (an_index: INTEGER): CHARACTER
      --  Characters in virtual string.

      require
         low_index: an_index >= 1;
         up_index: an_index <= count

   first: CHARACTER
      --  First character of string.

      require
         has_char: count > 0

   last: CHARACTER
      --  Last character of string.

      require
         has_char: count > 0

invariant
   string_is: string /= Void;
   dead_max: dead_start + dead_end <= string.count;

end of P_SHRINK_STRING