class interface BIT_STRING
   --
   -- Long and very long bit sequences.
   -- As for the primitive expanded BIT_N type, an INTEGER index can be
   -- used to access each bit of the sequence.
   -- As for BIT_N class, the leftmost bit has index 1 and the
   -- rightmost bit has index count.
   --
   -- For short bit sequences (less or equal to 32 or 64), also
   -- consider to use basic BIT_N type.
   --

creation
   make (n: INTEGER)
      -- Make bit sequence of n bits.
      -- All bits are set to false.

      require
         n > 0
      ensure
         count = n;
         all_default

   from_string (model: STRING)
      -- Create or set Current using model which is supposed
      -- to be a sequence of mixed 0 or 1 characters.

      require
         model.is_bit

feature(s) from BIT_STRING   count: INTEGER
      --  Number of bits in the sequence.


   make (n: INTEGER)
      -- Make bit sequence of n bits.
      -- All bits are set to false.

      require
         n > 0
      ensure
         count = n;
         all_default

   from_string (model: STRING)
      -- Create or set Current using model which is supposed
      -- to be a sequence of mixed 0 or 1 characters.

      require
         model.is_bit

   valid_index (idx: INTEGER): BOOLEAN
      -- True when index is valid (ie. inside actual
      -- bounds of the bit sequence).

      ensure
         Result = idx.in_range(1,count)

   item (idx: INTEGER): BOOLEAN
      --  True if idx-th bit is 1, false otherwise.

      require
         valid_index(idx)

   put (value: BOOLEAN; idx: INTEGER)
      --  Set bit idx to 1 if value is true, 0 otherwise.

      require
         valid_index(idx)
      ensure
         value = item(idx)

   put_1 (idx: INTEGER)
      --  Set bit idx to 1.

      require
         valid_index(idx)
      ensure
         item(idx)

   put_0 (idx: INTEGER)
      --  Set bit idx to 0.

      require
         valid_index(idx)
      ensure
         not item(idx)

feature(s) from BIT_STRING
   --  Rotating and shifting:

   shift_by (n: INTEGER)
      -- Shift n-bits.
      --  n > 0 : shift right,
      --  n < 0 : shift left,
      --  n = 0 : do nothing.
      -- Falling bits are lost and entering bits are 0.


   shift_left_by (n: INTEGER)
      -- Shift left by n bits.
      -- Falling bits are lost and entering bits are 0.

      require
         n >= 0

   shift_right_by (n: INTEGER)
      -- Shift right by n bits.
      -- Falling bits are lost and entering bits are 0.

      require
         n >= 0

   rotate_by (n: INTEGER)
      -- Rotate by n bits.
      --  n > 0 : Rotate right,
      --  n < 0 : Rotate left,
      --  n = 0 : do nothing.


   rotate_left_by (n: INTEGER)
      --  Rotate left by n bits.

      require
         n >= 0

   rotate_right_by (n: INTEGER)
      -- Rotate right by n bits.

      require
         n >= 0

   infix "^" (s: INTEGER): like Current
      -- Sequence shifted by s positions (positive s shifts
      -- right, negative left; bits falling off the sequence's
      -- bounds are lost).
      -- See also infix "|>>" and infix "|<<".

      require
         s.abs < count

   infix "|>>" (s: INTEGER): like Current
      -- Sequence shifted right by s positions.
      -- Same as infix "^" when s is positive (may run a little
      -- bit faster).

      require
         s > 0

   infix "|<<" (s: INTEGER): like Current
      -- Sequence shifted left by s positions.
      -- Same as infix "^" when s is negative (may run a little
      -- bit faster.

      require
         s > 0

   infix "#" (s: INTEGER): like Current
      -- Sequence rotated by s positions (positive right,
      -- negative left).

      require
         s.abs < count

   infix "#>>" (s: INTEGER): like Current
      -- Sequence rotated by s positions right.

      require
         s >= 0;
         s < count

   infix "#<<" (s: INTEGER): like Current
      -- Sequence rotated by s positions left.

      require
         s >= 0;
         s < count

feature(s) from BIT_STRING
   --  Bitwise Logical Operators:

   infix "and" (other: like Current): like Current
      --  Bitwise and of Current with other

      require
         count = other.count
      ensure
         Result.count = Current.count

   infix "implies" (other: like Current): like Current
      -- Bitwise implication of Current with other

      require
         count = other.count

   prefix "not": like Current
      -- Bitwise not of Current.

      ensure
         Result.count = Current.count

   infix "or" (other: like Current): like Current
      -- Bitwise or of Current with other.

      require
         other /= Void;
         count = other.count
      ensure
         Result.count = Current.count

   infix "xor" (other: like Current): like Current
      -- Bitwise xor of Current with other

      require
         other /= Void;
         count = other.count
      ensure
         Result.count = Current.count

   and_mask (other: like Current)
      -- Apply bitwise and mask of other onto Current.

      require
         count = other.count

   implies_mask (other: like Current)
      -- Aply bitwise implies mask of other.

      require
         count = other.count

   or_mask (other: like Current)
      -- Apply bitwise or mask of other onto Current.

      require
         count = other.count

   xor_mask (other: like Current)
      -- Apply bitwise xor mask of other onto Current

      require
         count = other.count

   invert
      -- Invert Current bit-per-bit.


feature(s) from BIT_STRING
   -- Conversions:

   to_string: STRING
      -- String representation of bit sequence.
      -- A zero bit is mapped to '0', a one bit to '1'.
      -- Leftmost bit is at index 1 in the returned string.
      --
      --  Note: see append_in to save memory.

      ensure
         Result.count = count

   to_integer: INTEGER
      -- The corresponding INTEGER value when count <= Integer_bits.
      -- No sign-extension when count < Integer_bits.

      require
         count <= integer_bits

feature(s) from BIT_STRING
   -- Others:

   all_cleared: BOOLEAN
      --  Are all bits set to 0 ?


   all_default: BOOLEAN
      --  Are all bits set to 0 ?


   clear_all
      -- Set all bits to 0

      ensure
         all_default

   all_set: BOOLEAN
      --  Are all bits set to 1 ?


   set_all
      -- Set all bits to 1

      ensure
         all_set

   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)

   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)

   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))

   append_in (str: STRING)
      -- Append in str a viewable representation of Current.


   set_from_string (model: STRING; offset: INTEGER)
      -- Use the whole contents of model to reset range
      -- offset .. offset + model.count - 1 of Current.
      -- Assume all characters of model are 0 or 1.

      require
         model.is_bit;
         valid_index(offset);
         valid_index(offset + model.count - 1)
      ensure
         count = old count


invariant
   count >= 1;
   not storage.is_empty;

end of BIT_STRING