AmigActive 3/AACD03.BIN/AACD/Programming/sofa/archive/SmallEiffel.lha/SmallEiffel/lib_std/string.e

Text File | 1999-06-05 | 39KB | 1,524 lines

-- This file is  free  software, which  comes  along  with  SmallEiffel. This
-- software  is  distributed  in the hope that it will be useful, but WITHOUT
-- ANY  WARRANTY;  without  even  the  implied warranty of MERCHANTABILITY or
-- FITNESS  FOR A PARTICULAR PURPOSE. You can modify it as you want, provided
-- this header is kept unaltered, and a notification of the changes is added.
-- You  are  allowed  to  redistribute  it and sell it, alone or as a part of
-- another product.
--          Copyright (C) 1994-98 LORIA - UHP - CRIN - INRIA - FRANCE
--            Dominique COLNET and Suzanne COLLIN - [e-mail]
--                       http://SmallEiffel.loria.fr
--
class STRING
   --
   -- Resizable character STRINGs.
   --

inherit
   HASHABLE;
   COMPARABLE
      redefine
         is_equal, compare, three_way_comparison, copy,
         out_in_tagged_out_memory, fill_tagged_out_memory
      end;

creation make, copy, blank, from_external, from_external_copy,
   make_from_string

feature {STRING}

   storage: NATIVE_ARRAY[CHARACTER];
         -- The place where characters are stored.

feature

   count: INTEGER;
         -- String length.

   capacity: INTEGER;
         -- Capacity of the `storage'.

feature -- Creation / Modification :

   make(needed_capacity: INTEGER) is
         -- Initialize the string to have at least `needed_capacity'
         -- characters of storage.
      require
          non_negative_size: needed_capacity >= 0;
      do
         if needed_capacity > 0 then
            if capacity < needed_capacity then
               storage := storage.calloc(needed_capacity);
               capacity := needed_capacity;
            end;
         end;
         count := 0;
      ensure
         needed_capacity <= capacity;
         empty_string: count = 0
      end;

   blank(nr_blanks: INTEGER) is
         -- Initialize string with `nr_blanks' blanks.
      require
         nr_blanks >= 0;
      do
         make(nr_blanks);
         count := nr_blanks;
         fill_with(' ');
      ensure
         count = nr_blanks;
         occurrences_of(' ') = count
      end;

feature -- Testing :

   empty: BOOLEAN is
         -- Has string length 0?
      do
         Result := (count = 0)
      end;

   item, infix "@" (index: INTEGER): CHARACTER is
         -- Character at position `index'.
      require
         valid_index(index)
      do
         Result := storage.item(index - 1);
      end;

   valid_index(index: INTEGER): BOOLEAN is
         -- True when `index' is valid (i.e., inside actual bounds).
      do
         Result := 1 <= index and then index <= count;
      ensure
         Result = (1 <= index and then index <= count)
      end;

   hash_code: INTEGER is
      local
         i: INTEGER;
      do
         i := count;
         if i > 5 then
            Result := i * item(i).code;
            i := 5;
         end;
         from until i <= 0 loop
            Result := Result + item(i).code;
            i := i - 1;
         end;
         Result := Result * count;
      end;

   infix "<" (other: like Current): BOOLEAN is
         -- Is Current less than `other' ?
      local
         i: INTEGER;
      do
         from
            i := 1;
         until
            count < i or else other.count < i
            or else item(i) /= other.item(i)
         loop
            i := i + 1;
         end;
         if count < i then
            Result := other.count >= i;
         elseif other.count < i then
            Result := false;
         else
            Result := item(i) < other.item(i);
         end;
      end;

   compare, three_way_comparison(other: like Current): INTEGER is
      local
         i: INTEGER;
      do
         from
            i := 1;
         until
            count < i or else other.count < i
            or else item(i) /= other.item(i)
         loop
            i := i + 1;
         end;
         if count < i then
            if other.count < i then
            else
               Result := -1;
            end;
         elseif other.count < i then
            Result := 1;
         elseif item(i) < other.item(i) then
            Result := -1;
         else
            Result := 1;
         end;
      end;

   same_as(other: STRING): BOOLEAN is
         -- Case insensitive `is_equal'.
      require
         other /= Void
      local
         s1, s2: like storage;
         i: INTEGER;
      do
         i := count;
         if i = other.count then
            from
               i := i - 1;
               s1 := storage;
               s2 := other.storage;
               Result := true;
            until
               i < 0
            loop
               if s1.item(i).same_as(s2.item(i)) then
                  i := i - 1;
               else
                  i := -1;
                  Result := false;
               end;
            end;
         end;
      end;

   is_equal(other: like Current): BOOLEAN is
         -- Has Current the same text as `other' ?
      do
         if count = other.count then
            Result := storage.fast_memcmp(other.storage,count);
         end;
      end;

   index_of(ch: CHARACTER): INTEGER is
         -- Gives the index of the first occurrence `ch' or
         -- `count + 1' if none.
      do
         Result := 1 + storage.fast_index_of(ch,count - 1);
      ensure
         (Result /= count + 1) implies (item(Result) = ch);
      end;

   index_of_string(other: STRING): INTEGER is
         -- Position of the first occurrence of `other'
         -- or `count + 1' if none.
      require
         not other.empty
      local
         stop: BOOLEAN;
         i1, i2, i3: INTEGER;
      do
         from
            i1 := 1;
            i2 := other.count;
            i3 := i2;
         invariant
            i3 = i2 - i1 + 1;
         variant
            count - i1 + 1
         until
            Result /= 0
         loop
            if i2 > count then
               Result := count + 1;
            else
               from
                  stop := false;
               invariant
                  i3 = i2 - i1 + 1
               variant
                  (i3 + i2)
               until
                  stop
               loop
                  if i3 = 0 then
                     stop := true;
                     Result := i1;
                  elseif other.item(i3) /= item(i2) then
                     stop := true;
                  end;
                  i3 := i3 - 1;
                  i2 := i2 - 1;
               end;
            end;
            i1 := i1 + 1;
            i3 := other.count;
            i2 := i1 + i3 - 1;
         end;
      end;

   has(ch: CHARACTER): BOOLEAN is
         -- True if `ch' is in the STRING.
      do
         Result := storage.fast_has(ch,count - 1);
      end;

   has_string(other: STRING): BOOLEAN is
         -- True if `other' is in the STRING.
      do
         Result := index_of_string(other) /= (count + 1);
      end;

   occurrences_of, occurrences(c: CHARACTER): INTEGER is
         -- Number of times character `c' appears in the string.
      do
         Result := storage.fast_nb_occurrences(c,count - 1);
      ensure
         Result >= 0
      end;

   has_suffix(s: STRING): BOOLEAN is
         -- True if suffix of Current is `s'.
      require
         s /= Void
      local
         i1, i2: INTEGER;
      do
         if s.count <= count then
            from
               i1 := count - s.count + 1;
               i2 := 1;
            until
               i1 > count or else
               i2 > s.count or else
               item(i1) /= s.item(i2)
            loop
               i1 := i1 + 1;
               i2 := i2 + 1;
            end;
            Result := i1 > count;
         end;
      end;

   has_prefix(p: STRING): BOOLEAN is
         -- True if prefix of Current is `p'.
      require
         p /= Void;
      local
         i: INTEGER;
      do
         if p.count <= count then
            from
               i := p.count;
            until
               i = 0 or else item(i) /= p.item(i)
            loop
               i := i - 1;
            end;
            Result := i = 0;
         end;
      end;

   replace_all(old_character, new_character: like item) is
         -- Replace all occurrences of the element `old_character' by
         -- `new_character'.
      do
         storage.fast_replace_all(old_character,new_character,count - 1);
      ensure
         count = old count;
         occurrences_of(old_character) = 0
      end;

   is_integer: BOOLEAN is
      -- Can contents be read as an INTEGER ?
      local
         i, state: INTEGER;
         cc: CHARACTER;
      do
         -- state 0 : nothing read.
         -- state 1 : "+" or "-" read.
         -- state 2 : in the number.
         -- state 3 : after the number.
         -- state 4 : error.
         from
            i := 1;
         until
            i > count or else state = 4
         loop
            cc := item(i);
            inspect
               state
            when 0 then
               if cc.is_separator then
               elseif cc = '+' then
                  state := 1;
               elseif cc = '-' then
                  state := 1;
               elseif cc.is_digit then
                  state := 2;
                  Result := true;
               else
                  state := 4;
                  Result := false;
               end;
            when 1 then
               if cc.is_separator then
               elseif cc.is_digit then
                  state := 2;
                  Result := true;
               else
                  state := 4;
                  Result := false;
               end;
            when 2 then
               if cc.is_digit then
               elseif cc.is_separator then
                  state := 3;
               else
                  state := 4;
                  Result := false;
               end;
            when 3 then
               if cc.is_separator then
               else
                  state := 4;
                  Result := false;
               end;
            end;
            i := i + 1;
         end;
      end;

   is_real: BOOLEAN is
         -- Contents can be read as a REAL.
      local
         d: DOUBLE;
      do
         if is_double then
            d := to_double
            if Minimum_real <= d and then d <= Maximum_real then
               Result := true
               -- This gives only approximate accuracy; the comparison
               -- is not accurate to nearly as many significant figures
               -- as are displayed for the limits.
            end
         end
      end

   is_double: BOOLEAN is
         -- Contents can be read as a DOUBLE.
      local
         i, state: INTEGER;
         cc: CHARACTER;
         begun: BOOLEAN;
      do
         -- state 0 : nothing read.
         -- state 1 : "+" or "-" read.
         -- state 2 : in the number.
         -- state 3 : decimal point read
         -- state 4 : in fractional part
         -- state 5 : read 'E' or 'e' for scientific notation
         -- state 6 : read "-" sign of exponent
         -- state 7 : in exponent
         -- state 8 : after the number.
         -- state 9 : error.
         from
            i := 1;
         until
            i > count or else state = 9
         loop
            cc := item(i);
            inspect
               state
            when 0 then
               if cc.is_separator then
               elseif cc = '+' then
                  state := 1;
               elseif cc = '-' then
                  state := 1;
               elseif cc.is_digit then
                  state := 2;
                  Result := true;
               elseif cc = '.' then
                  state := 3
               else
                  state := 9;
                  Result := false;
               end;
            when 1 then
               if cc.is_separator then
               elseif cc.is_digit then
                  state := 2;
                  Result := true;
               elseif cc = '.' then
                  state := 3
               else
                  state := 9;
                  Result := false;
               end;
            when 2 then
               if cc.is_digit then
                  begun := true
               elseif cc = '.' then
                  state := 3
               else
                  state := 9;
                  Result := false;
               end;
            when 3 then
               if cc.is_separator then
                  state := 8;
               elseif cc.is_digit then
                  state := 4
                  Result := true;
                  begun := true
               else
                  state := 9
                  Result := false
               end
            when 4 then
               if cc.is_digit then
                  begun := true
               elseif cc.is_separator then
                  state := 8;
               elseif (cc = 'e' or cc = 'E') and begun then
                  state := 5
               else
                  state := 9;
                  Result := false;
               end;
            when 5 then
               if cc = '-' then
                  state := 6
               elseif cc.is_digit then
                  state := 7
               else
                  state := 9;
                  Result := false;
               end;
            when 6 then
               if cc.is_digit then
                  state := 7
               else
                  state := 9;
                  Result := false;
               end;
            when 7 then
               if cc.is_digit then
               elseif cc.is_separator then
                  state := 8
               else
                  state := 9;
                  Result := false;
               end;
            when 8 then
               if cc.is_separator then
               else
                  state := 9;
                  Result := false;
               end;
            end;
            i := i + 1;
         end;
         if state < 3 then
            -- exclude integers
            Result := false
         end
         -- We should check the value is within the system limits, but
         -- I can't see how to do that without trying to convert it.
      end;

   is_bit: BOOLEAN is
         -- True when the contents is a sequence of bits (i.e., mixed
         -- characters `0' and characters `1').
      local
         i: INTEGER;
      do
         from
            i := count;
            Result := true;
         until
            not Result or else i = 0
         loop
            Result := item(i).is_bit;
            i := i - 1;
         end;
      ensure
         Result = (count = occurrences_of('0') + occurrences_of('1'))
      end;

feature -- Modification :

   clear, wipe_out is
         -- Clear out the current STRING.
         -- Note : internal `storage' memory is neither released nor shrunk.
      do
         count := 0;
      ensure
         count = 0;
      end;

   copy(other: like Current) is
         -- Copy `other' onto Current.
      do
         count := other.count;
         if count > 0 then
            if capacity < count then
               storage := storage.calloc(count);
               capacity := count;
            end;
            storage.copy_from(other.storage,count-1);
         end;
      ensure then
         count = other.count
      end;

   fill, fill_with(c: CHARACTER) is
         -- Replace every character with `c'.
      do
         storage.set_all_with(c,count - 1);
      ensure
         occurrences_of(c) = count
      end;

   fill_blank is
         -- Fill entire string with blanks
      do
         fill_with(' ');
      ensure
         occurrences_of(' ') = count
      end;

   append, append_string(other: STRING) is
         -- Append `other' to Current.
      require
         other /= Void
      local
         other_count, needed_capacity: INTEGER;
      do
         other_count := other.count;
         needed_capacity := count + other_count;
         if capacity < needed_capacity then
            if capacity = 0 then
               capacity := needed_capacity;
               storage := storage.calloc(capacity);
            else
               storage := storage.realloc(capacity,needed_capacity);
               capacity := needed_capacity;
            end;
         end;
         storage.copy_at(count,other.storage,other_count);
         count := needed_capacity;
      end;

   prepend(other: STRING) is
         -- Prepend `other' to Current
      require
         other /= Void
      local
         i, old_count: INTEGER;
      do
         old_count := count;
         from
            i := other.count;
         until
            i = 0
         loop
            extend(' ');
            i := i - 1;
         end;
         from
            i := count;
         until
            old_count = 0
         loop
            put(item(old_count),i);
            i := i - 1;
            old_count := old_count - 1;
         end;
         from
            i := other.count
         until
            i = 0
         loop
            put(other.item(i),i);
            i := i - 1;
         end;
      ensure
         count = other.count + old count
      end;

   infix "+" (other: STRING): STRING is
         -- Create a new STRING which is the concatenation of
         -- `Current' and `other'.
      require
         other /= Void
      do
         !!Result.make(count + other.count);
         Result.append(Current);
         Result.append(other);
      ensure
         Result.count = count + other.count
      end;

   put(ch: CHARACTER; index: INTEGER) is
         -- Put `ch' at position `index'.
      require
         valid_index(index)
      do
         storage.put(ch,index - 1);
      ensure
         item (index) = ch
      end;

   swap(i1, i2: INTEGER) is
      require
         valid_index(i1);
         valid_index(i2)
      local
         tmp: CHARACTER;
      do
         tmp := item(i1);
         put(item(i2),i1);
         put(tmp,i2);
      ensure
         item(i1) = old item(i2);
         item(i2) = old item(i1);
      end;

   insert(ch: CHARACTER; index: INTEGER) is
         -- Insert `ch' after position `index'.
      require
         0 <= index and index <= count;
      local
         i: INTEGER;
      do
         from
            i := count;
            extend(' ');
         until
            i = index
         loop
            put(item(i),i + 1);
            i := i - 1;
         end;
         put(ch,index + 1);
      ensure
         item (index + 1) = ch
      end;

   shrink(low, up: INTEGER) is
         -- Keep only the slice `low' .. `up' or nothing
         -- when the slice is empty.
      require
         1 <= low;
         low <= count;
         1 <= up;
         up <= count;
      local
         i, i2: INTEGER;
      do
         if up < low then
            clear;
         elseif low = 1 then
            count := up;
         else
            from
               i := 1;
               i2 := low;
            until
               i2 > up
            loop
               put(item(i2),i);
               i := i + 1;
               i2 := i2 + 1;
            end;
            count := i - 1;
         end;
      ensure
         up > low implies count = up - low + 1;
      end;

   remove(index: INTEGER) is
         -- Remove character at position `index'.
      require
         valid_index(index)
      do
         remove_between(index,index);
      ensure
         count = (old count) - 1
      end;

   add_first(ch: CHARACTER) is
         -- Add `ch' at first position.
      local
         i: INTEGER;
      do
         from
            extend(' ');
            i := count;
         until
            i = 1
         loop
            put(item(i - 1),i);
            i := i - 1;
         end;
         put(ch,1);
      ensure
         count = 1 + old count;
         item(1) = ch
      end;

   add_last, extend, append_character(ch: CHARACTER) is
         -- Append `ch' to string
      local
         new_capacity: INTEGER;
      do
         if capacity > count then
         elseif capacity = 0 then
            capacity := 32;
            storage := storage.calloc(capacity);
         else
            new_capacity := 2 * capacity;
            storage := storage.realloc(capacity,new_capacity);
            capacity := new_capacity;
         end;
         storage.put(ch,count);
         count := count + 1;
      ensure
         count = 1 + old count;
         item (count) = ch
      end;

   precede(ch: CHARACTER) is
         -- Prepend `ch' to string
      local
         i: INTEGER;
      do
         from
            extend(' ');
            i := count;
         until
            i = 1
         loop
            put(item(i-1),i);
            i := i - 1;
         end;
         put(ch,1);
      ensure
         item (1) = ch
      end;

   to_lower is
         -- Convert all characters to lower case.
      local
         i: INTEGER;
      do
         from
            i := count;
         until
            i = 0
         loop
            put(item(i).to_lower,i);
            i := i - 1;
         end;
      end;

   to_upper is
         -- Convert all characters to upper case.
      local
         i: INTEGER;
      do
         from
            i := count;
         until
            i = 0
         loop
            put(item(i).to_upper,i);
            i := i - 1;
         end;
      end;

   remove_first(nb: INTEGER) is
         -- Remove `nb' first characters.
      require
         nb >= 0;
         count >= nb;
      do
         if nb > 0 then
            remove_between(1, nb)
         end;
      ensure
         count = (old count) - nb
      end;

   remove_last(nb: INTEGER) is
         -- Remove `nb' last characters.
      require
         0 <= nb;
         nb <= count;
      do
         count := count - nb;
      ensure
         count = old count - nb
      end;

   remove_between(low, up : INTEGER) is
         -- Remove character between positions `low' and `up'.
      require
         valid_index(low);
         valid_index(up);
         low <= up
      local
         i : INTEGER;
      do
         from
            i := up;
         until
            i >= count
         loop
            put(item(i + 1), low + i - up);
            i := i + 1;
         end;
         count := count - (up - low + 1);
      ensure
         count = (old count) - (up - low + 1)
      end;

   remove_suffix(s: STRING) is
      -- Remove the suffix `s' of current string.
      require
         has_suffix(s);
      do
         remove_last(s.count);
      ensure
         old count = count + s.count
      end;

   remove_prefix(s: STRING) is
      -- Remove the prefix `s' of current string.
      require
         has_prefix(s);
      do
         remove_first(s.count);
      ensure
         old count = count + s.count
      end;

   left_adjust is
         -- Remove leading blanks.
      local
         i: INTEGER;
      do
         from
         until
            i + 1 > count or else item(i + 1) /= ' '
         loop
            i := i + 1;
         end;
         remove_first(i);
      ensure
         stripped: empty or else item (1) /= ' '
      end;

   right_adjust is
         -- Remove trailing blanks.
      do
         from
         until
            count = 0 or else item(count) /= ' '
         loop
            count := count - 1;
         end
      ensure
         stripped: empty or else item (count) /= ' '
      end;

feature -- Features which don't modify the string

   first: CHARACTER is
      require
         not empty
      do
         Result := storage.item(0);
      end;

   last: CHARACTER is
      require
         not empty;
      do
         Result := item(count);
      end;

feature -- Conversion :

   to_integer: INTEGER is
         -- Current must looks like an INTEGER.
      require
         is_integer
      local
         i, state: INTEGER;
         cc: CHARACTER;
         minus: BOOLEAN;
      do
         -- state 0 : nothing read.
         -- state 1 : "+" or "-" read.
         -- state 2 : in the number.
         -- state 3 : after the number.
         -- state 4 : error.
         from
            i := 1;
         until
            i > count
         loop
            cc := item(i);
            inspect
               state
            when 0 then
               if cc.is_separator then
               elseif cc = '+' then
                  state := 1;
               elseif cc = '-' then
                  minus := true;
                  state := 1;
               else
                  check
                     cc.is_digit
                  end;
                  Result := cc.value;
                  state := 2;
               end;
            when 1 then
               if cc.is_separator then
               else
                  check
                     cc.is_digit
                  end;
                  Result := cc.value;
                  state := 2;
               end;
            when 2 then
               if cc.is_digit then
                  Result := (Result * 10) + cc.value;
               else
                  check
                     cc.is_separator
                  end;
                  state := 3;
               end;
            when 3 then
               check
                  cc.is_separator
               end;
            end;
            i := i + 1;
         end;
         if minus then
            Result := - Result;
         end;
      end;

   to_real: REAL is
         -- Conversion to the corresponding REAL value.
         -- The string must looks like a REAL (or like an
         -- INTEGER because fractionnal part is optional).
      require
         is_integer or is_real
      do
         Result := to_double.to_real;
      end;

   to_double: DOUBLE is
         -- Conversion to the corresponding DOUBLE value.
         -- The string must looks like a DOUBLE, like
         -- a REAL (or like an INTEGER because fractionnal
         -- part is optional).
      require
         is_integer or is_real
      local
         negative: BOOLEAN;
         p: POINTER;
      do
         tmp_string.copy(Current);
         tmp_string.left_adjust;
         if tmp_string.first = '-' then
            negative := true;
            tmp_string.remove_first(1);
         elseif tmp_string.first = '+' then
            tmp_string.remove_first(1);
         end;
         tmp_string.left_adjust;
         p := tmp_string.to_external;
         Result := se_string2double(p);
         if negative then
            Result := -Result;
         end;
      end;

   binary_to_integer: INTEGER is
         -- Assume there is enougth space in the INTEGER to store
         -- the corresponding decimal value.
      require
         is_bit;
         count <= Integer_bits
      local
         i: INTEGER;
      do
         from
            i := 1;
         until
            i > count
         loop
            if item(i) = '1' then
               Result := (2 * Result) + 1;
            else
               Result := 2 * Result;
            end;
            i := i + 1;
         end;
      end;

   to_hexadecimal is
         -- Convert Current bit sequence into the corresponding
         -- hexadecimal notation.
      require
         is_bit
      local
         i, k, new_count: INTEGER;
         value: INTEGER;
      do
         from
            i := 1;
            k := count \\ 4;
            if k > 0 then
               new_count := 1;
            end;
         until
            k = 0
         loop
            value := value * 2 + item(i).value;
            i := i + 1;
            k := k - 1;
         end;
         if new_count > 0 then
            put(value.hexadecimal_digit,new_count);
         end;
         from
         until
            i > count
         loop
            from
               value := item(i).value;
               i := i + 1;
               k := 3;
            until
               k = 0
            loop
               value := value * 2 + item(i).value;
               i := i + 1;
               k := k - 1;
            end;
            new_count := new_count + 1;
            put(value.hexadecimal_digit,new_count);
         end;
         count := new_count;
      end;

feature -- Printing :

   out_in_tagged_out_memory is
      do
         tagged_out_memory.append(Current);
      end;

   fill_tagged_out_memory is
      do
         tagged_out_memory.append("count: ");
         count.append_in(tagged_out_memory);
         tagged_out_memory.append("capacity: ");
         capacity.append_in(tagged_out_memory);
         tagged_out_memory.append("storage: %"");
         tagged_out_memory.append(Current);
         tagged_out_memory.extend('%"');
      end;

feature -- Other features :

   substring(low, up: INTEGER): like Current is
         -- Create a new string initialized with range `low'.. `up'.
      require
         1 <= low;
         low <= up;
         up <= count;
      local
         i: INTEGER;
      do
         from
            !!Result.make(up - low + 1);
            i := low;
         until
            i > up
         loop
            Result.extend(item(i));
            i := i + 1;
         end;
      end;

   extend_multiple(c: CHARACTER; n: INTEGER) is
         -- Extend Current with `n' times character `c'.
      require
         n >= 0
      local
         i: INTEGER;
      do
         from
            i := n;
         until
            i = 0
         loop
            extend(c);
            i := i - 1;
         end;
      ensure
         count = n + old count
      end;

   precede_multiple(c: CHARACTER; n: INTEGER) is
         -- Prepend `n' times character `c' to Current.
      require
         n >= 0
      local
         old_count: INTEGER;
      do
         if n > 0 then
            old_count := count;
            if old_count = 0 then
               extend_multiple(c,n);
            else
               extend_multiple('%U',n);
               storage.move(0,old_count - 1,n);
               storage.set_all_with(c,n - 1);
            end;
         end;
      ensure
         count = n + old count
      end;

   extend_to_count(c: CHARACTER; needed_count: INTEGER) is
         -- Extend Current with `c' until `needed_count' is reached.
         -- Do nothing if `needed_count' is already greater or equal
         -- to `count'.
      require
         needed_count >= 0
      local
         offset: INTEGER;
      do
         from
            offset := needed_count - count;
         until
            offset <= 0
         loop
            extend(c);
            offset := offset - 1;
         end;
      ensure
         count >= needed_count
      end;

   precede_to_count(c: CHARACTER; needed_count: INTEGER) is
         -- Prepend `c' to Current until `needed_count' is reached.
         -- Do nothing if `needed_count' is already greater or equal
         -- to `count'.
      require
         needed_count >= 0
      local
         offset, old_count: INTEGER;
      do
         old_count := count;
         offset := needed_count - old_count;
         if offset > 0 then
            extend_to_count('%U',needed_count);
            storage.move(0,old_count - 1,offset);
            storage.set_all_with(c,offset - 1);
         end;
      ensure
         count >= needed_count
      end;

   reverse is
         -- Reverse the string.
      local
         i1, i2: INTEGER;
      do
         from
            i1 := 1;
            i2 := count;
         until
            i1 >= i2
         loop
            swap(i1,i2);
            i1 := i1 + 1;
            i2 := i2 - 1;
         end;
      end;

   remove_all_occurrences(ch: CHARACTER) is
         -- Remove all occurrences of `ch'.
      local
         i, j: INTEGER;
      do
         from
            i := 1;
            j := 1;
         until
            i > count
         loop
            if item(i) /= ch then
               put(item(i),j);
               j := j + 1;
            end;
            i := i + 1;
         end;
         count := j - 1;
      ensure
         count = old count - old occurrences_of(ch)
      end;

   substring_index(other: STRING; start: INTEGER): INTEGER is
         -- Position of first occurrence of `other' at or after
         -- `start';
         -- 0 if none.
      require
         start_large_enough: start >= 1;
         start_small_enough: start <= count;
         string_exist: other /= Void
      local
         i, s: INTEGER;
      do
         from
            s := start;
         until
            Result /= 0 or else (s + other.count - 1) > count
         loop
            from
               i := 1;
            until
               i > other.count or else item(s + i - 1) /= other.item(i)
            loop
               i := i + 1;
            end;
            if i > other.count then
               Result := s;
            else
               s := s + 1
            end;
         end;
      end;

feature -- Splitting a STRING :

   split: ARRAY[STRING] is
         -- Split the string into an array of words.
         -- Uses `is_separator' of CHARACTER to find words.
         -- Gives Void or a non empty array.
      do
         if count > 0 then
            split_buffer.clear;
            split_in(split_buffer);
            if not split_buffer.empty then
               Result := split_buffer.twin;
            end;
         end;
      ensure
         Result /= Void implies not Result.empty
      end;

   split_in(words: COLLECTION[STRING]) is
         -- Same jobs as `split' but result is appended in `words'.
      require
         words /= Void
      local
         state, i: INTEGER;
         -- state = 0 : waiting next word.
         -- state = 1 : inside a new word.
         c: CHARACTER;
      do
         if count > 0 then
            from
               i := 1;
            until
               i > count
            loop
               c := item(i);
               if state = 0 then
                  if not c.is_separator then
                     tmp_string.clear;
                     tmp_string.extend(c);
                     state := 1;
                  end;
               else
                  if not c.is_separator then
                     tmp_string.extend(c);
                  else
                     words.add_last(tmp_string.twin);
                     state := 0;
                  end;
               end;
               i := i + 1;
            end;
            if state = 1 then
               words.add_last(tmp_string.twin);
            end;
         end;
      ensure
         words.count >= old (words.count)
      end;

feature -- Other feature :

   set_last(ch: CHARACTER) is
      do
         if count = 0 or else item(count) /= ch then
            extend(ch);
         end;
      ensure
         last = ch
      end;

feature -- Interfacing with C string :

   to_external: POINTER is
         -- Gives C access to the internal `storage' (may be dangerous).
         -- To be compatible with C, a null character is added at the end
         -- of the internal `storage'. This extra null character is not
         -- part of the Eiffel STRING.
      do
         if capacity > count then
            count := count + 1;
            if item(count) /= '%U' then
               put('%U',count);
            end;
         else
            extend('%U');
         end;
         count := count - 1;
         Result := storage.to_pointer;
      ensure
         count = old count;
         Result.is_not_null
      end;

   from_external(p: POINTER) is
         -- Internal `storage' is set using `p' (may be dangerous because
         -- the external C string `p' is not duplicated).
         -- Assume `p' has a null character at the end in order to
         -- compute the Eiffel `count'. This extra null character
         -- is not part of the Eiffel STRING.
         -- Also consider `from_external_copy' to choose the most appropriate.
      require
         p.is_not_null
      do
         from
            storage := storage.from_pointer(p);
            count := 0;
         until
            storage.item(count) = '%U'
         loop
            count := count + 1;
         end;
         capacity := count + 1;
      ensure
         capacity = count + 1;
         p = to_external
      end;

   from_external_copy(p: POINTER) is
         -- Internal `storage' is set using a copy of `p'.
         -- Assume `p' has a null character at the end in order to
         -- compute the Eiffel `count'. This extra null character
         -- is not part of the Eiffel STRING.
         -- Also consider `from_external' to choose the most appropriate.
      local
         s: like storage;
      do
         from_external(p);
         s := s.calloc(capacity);
         s.copy_from(storage,capacity);
         storage := s;
      end;

feature -- Other feature here for ELKS'95 compatibility :

   make_from_string(s: STRING) is
         -- Initialize from the characters of `s'.
         -- (Useful in proper descendants of class STRING, to
         -- initialize a string-like object from a manifest string.)
      require
         s /= Void
      local
         i, sc: INTEGER;
      do
         from
            sc := s.count;
            make(sc);
         until
            i = sc
         loop
            i := i + 1;
            extend(s.item(i));
         end;
      ensure
         count = s.count
      end;

   head(n: INTEGER) is
      -- Remove all characters except fo the first `n'.
      -- Do nothing if n >= count.
      require
         n >= 0
      do
         if n < count then
            remove_last(count - n);
         end;
      ensure
         count = n.min(old count)
      end;

   tail(n: INTEGER) is
      -- Remove all characters except for the last `n'.
      -- Do nothing if n >= count.
      require
         n >= 0
      do
         if n < count then
            remove_first(count - n);
         end;
      ensure
         count = n.min(old count)
      end;

feature {STRING}

   se_string2double(number_view: POINTER):DOUBLE is
      external "SmallEiffel"
      end;

feature {NONE}

   tmp_string: STRING is
      once
         !!Result.make(256);
      end;

feature {NONE}

   split_buffer: ARRAY[STRING] is
      once
         !!Result.with_capacity(4,1);
      end;

invariant

   0 <= count;

   count <= capacity;

   capacity > 0 implies storage.is_not_null;

end -- STRING