deferred class RO_VTUPLE [G]

-- This class has all the read-only properties of a tuple. An
-- object of this type can inspect and traverse the tuple, but
-- not alter it.

inherit PROTECTED
  redefine
     logon, logoff, is_protected
  end

feature {ANY}
  count : INTEGER is
    deferred
  end

  is_empty : BOOLEAN is 
    do
      Result:= count = 0
    end

  has_place ( p: PLACE ) : BOOLEAN is
    deferred
    end

  first_place: PLACE is
    deferred
    ensure
      void_if_empty : is_empty implies Result = Void
      empty_if_void : Result = Void implies is_empty
    end

  last_place : like first_place is
    deferred
    ensure
      void_if_empty : is_empty implies Result = Void
      empty_if_void : Result = Void implies is_empty
    end

  rank ( p : like first_place ) : INTEGER is
    require
      has_p : has_place ( p )
    deferred
    ensure
      in_range : 1 <= Result and Result <= count
    end

  nth_after ( n: INTEGER; p : like first_place ) : like first_place is
	-- 0 <= n <= count; the n-th place following p
	-- in cyclic order, p itself if n=0.
    require
      has_p : has_place ( p )
      n_nonnegative: n >= 0
      n_inrange: n <= count - 1
    deferred
    ensure
      ranks: rank ( Result ) - rank ( p ) - n \\ count = 0
    end

  nth_before ( n: INTEGER; p : like first_place ) : like first_place is
	-- 0 <= n <= count; the n-th place preceding p
	-- in cyclic order, p itself if n=0.
    require
      has_p : has_place ( p )
      n_nonnegative: n >= 0
      n_inrange: n <= count - 1
    deferred
    ensure
      ranks: rank ( Result ) - rank ( p ) + n \\ count = 0
    end

  nth_place ( n: INTEGER ) : like first_place is
    require
      n_positive: n > 0
      inrange: n <= count
    deferred
    ensure
      rank : rank ( Result ) = n
    end

  pred ( p: like first_place ): like first_place is 
    require
      has_p: has_place ( p )
    deferred
    end

  succ ( p: like first_place ): like first_place is 
    require
      has_p: has_place ( p )
    deferred
    end

  cyclic_pred ( p: like first_place ): like first_place is 
    require
      has_p: has_place ( p )
    do
      if p = first_place then
        Result := last_place
      else
        Result := pred ( p )
      end
    end

  cyclic_succ ( p: like first_place ): like first_place is 
    require
      has_p: has_place ( p )
    do
      if p = last_place then
        Result := first_place
      else
        Result := succ ( p )
      end
    end

  place_lesseq ( p, q : like first_place ) : BOOLEAN is
    require
      has_p: has_place (p)
      has_q: has_place (q)
    deferred
    end

  item, infix "@" ( p: like first_place ) : G is
    require
      has_p: has_place (p)
    deferred
    end

  top, first_item: G is
    require
      nonempty: not is_empty
    do
      Result := item ( first_place )
    end

  last_item: G is
    require
      nonempty: not is_empty
    do
      Result := item ( last_place )
    end

  protecting: PROTECTED

  emitter: VTUPLE_EMITTER [ G ] is
    do
      !! Result . make ( Current, false )
    ensure
      protection: Result.finished or else is_protected
    end

  reverse_emitter: like emitter is
    do
      !! Result . make ( Current, true )
    ensure
      protection: Result.finished or else is_protected
    end

  cyclic_emitter (start_at, stop_after: like first_place): like emitter is
    require
      has_start_place: has_place ( start_at )
      has_stop_place: has_place ( stop_after )
    do
      !! Result . make_cyclic ( Current, false, start_at, stop_after )
    ensure
      protection: is_protected and not Result . finished
    end

  reverse_cyclic_emitter (start_at, stop_after: like first_place):
		like emitter is
    require
      has_start_place: has_place ( start_at )
      has_stop_place: has_place ( stop_after )
    do
      !! Result . make_cyclic ( Current, true, start_at, stop_after )
    ensure
      protection: is_protected and not Result . finished
    end

  printout (f: OUTPUT_STREAM) is
    require
      nonvoid: f /= Void
      is_connected: f.is_connected
    local
      p : like first_place
      str : STRING
      length : INTEGER
      newline : BOOLEAN
    do
      from
	p := first_place
      until
	p = Void
      loop
	if newline then
	  str := "%N"+item(p).out
	  length := str.count-1
	else
	  str := " "+item(p).out
	  length := length + 1 + str.count
	end
	if length > 70 then
	  newline := true
	end
	f . put_string ( str )
	p := succ (p)
      end
      f.put_new_line
    end

  is_protected : BOOLEAN is
    do
      check
         protecting /= Current
      end

      if protecting /= Void then
        Result := protecting . is_protected
      else
        Result := emitter_count > 0
      end
    end
 
  feature {VTUPLE_EMITTER}

    logon is
      do
        emitter_count := emitter_count + 1
      -- ensure
      --    is_protected
      end

    logoff is
      -- require
      --    is_protected
      do
        emitter_count := emitter_count - 1
      end

end --- deferred class RO_VTUPLE [G]