class GBN_DLIST [G]
  -- Vtuples realised by doubly-linked lists

inherit
  GBN_TUPLE [G]
  redefine
    iterator, reverse_iterator,
    	cyclic_iterator, reverse_cyclic_iterator
end
    -- The iterators need to be redefined simply to
    -- get the correct type for `place.'  There was
    -- some difficulty compiling the reverse iterators
    -- which may be a SmallEiffel inadequacy.

creation
  make

creation {GBN_PROTECTED}
 make_protecting

creation {GBN_DLIST}
  make_sublist
    -- to be used only in cyclic_remove

feature {ANY}
  -- deferred features inherited from GBN_ROTUPLE:

  count : INTEGER

  iterator: GBN_DLIST_ITERATOR [G] is
      -- only change is the inherited type.  This is
      -- a type anchor, so the change passes to the other
      -- iterators.
      -- OOPS no it doesn't. Why?
    do
      !! Result . make ( Current, false )
    end

  reverse_iterator: like iterator is
    do
      !! Result . make ( Current, true )
    end

  cyclic_iterator (start_at, stop_after: like first_place): like iterator is
    do
      !! Result . make_cyclic ( Current, false, start_at, stop_after )
    end

  reverse_cyclic_iterator (start_at, stop_after: like first_place):
		like iterator is
    do
      !! Result . make_cyclic ( Current, true, start_at, stop_after )
    end

  has_place ( p: GBN_PLACE ) : BOOLEAN is
    local
      pp : like first_place
    do
      pp ?= p
        -- `has_place' is not restricted
        -- to arguments of type GBN_DLIST_PLACE
      if pp = Void or else pp.uf_marker = Void then
        Result := false
      else
        Result := pp.uf_marker.find = uf_marker.find
      end
    end

  first_place : GBN_DLIST_PLACE [G]
  last_place : like first_place

  rank ( p : like first_place ) : INTEGER is
    local
      q : like first_place
    do
      from
	q := p
	Result := 1
      until
	q = first_place
      loop
	q := q . pred
	Result := Result + 1
      end
    end

  nth_after ( n: INTEGER; p : like first_place ) : like first_place is
    local
      i : INTEGER
      q : like first_place
    do
      from
        i := 0
        q := p
      until
        i = n
      loop
        i := i + 1
        q := cyclic_succ ( q )
      end
      Result := q
    end

  nth_before ( n: INTEGER; p : like first_place ) : like first_place is
    local
      i : INTEGER
      q : like first_place
    do
      from
        i := 0
        q := p
      until
        i = n
      loop
        i := i + 1
        q := cyclic_pred ( q )
      end
      Result := q
    end

  nth_place ( n : INTEGER ) : like first_place is
    do
      Result := nth_after ( n-1, first_place )
    end

  succ ( p: like first_place ) : like first_place is
    do
      Result := p.succ
    end

  pred ( p: like first_place ) : like first_place is
    do
      Result := p.pred
    end

  place_lesseq ( p, q : like first_place ) : BOOLEAN is
    local
      r : like first_place
    do
      from
        r := p
      until
        r = q or r = Void
      loop
        r := r.succ
      end
      Result := r = q
    end

  item, infix "@" ( p: like first_place ) : G is
    do
      Result := p . item
    end

-- deferred features inherited from GBN_TUPLE:

  replica: like Current is
    local
      em: like iterator
    do
      from
        !! Result . make
        em := iterator
      until
        em . finished
      loop
        Result . add_last ( em . item )
        em . forth
      end
    end

  wipe_out is
    do
      first_place := Void
      last_place := Void
      !! uf_marker . make
      count := 0
    end

  push, add_first ( x: G ) is
    local
      q: like first_place
    do
      !! q . make ( x, uf_marker )
      q . set_succ ( first_place )

      if first_place /= Void
      then
        first_place . set_pred ( q )
      end
      first_place := q

      if last_place = Void then
        last_place := first_place
      end
      count := count + 1
    end

  add_last ( x: G ) is
    local
      q: like first_place
    do
      !! q . make ( x, uf_marker )
      q . set_pred ( last_place )

      if last_place /= Void
      then
        last_place . set_succ ( q )
      end

      last_place := q
      if first_place = Void then
        first_place := q
      end
      count := count + 1
    end

  add_after ( x: G; p: like first_place ) is
    local
      q,r : like first_place
    do
      if p = Void then
        push ( x )
      elseif p . succ = Void then
        add_last ( x )
      else
        r := p . succ
        !! q . make ( x, uf_marker )
        r . set_pred ( q )
        q . set_succ ( r )
        q . set_pred ( p )
        p . set_succ ( q )
        count := count + 1
      end
    end


  add_before ( x: G; p: like first_place ) is
    local
      q,r : like first_place
    do
      if p = Void then
        add_last ( x )
      elseif p . pred = Void then
        push ( x )
      else
        q := p . pred
        !! r . make ( x, uf_marker )
        r . set_succ ( p )
        p . set_pred ( r )
        r . set_pred ( q )
        q . set_succ ( r )
        count := count + 1
      end
    end

  pop, remove_first is
    -- First_place is removed from tuple.
    local
      q : like first_place
    do
      q := first_place . succ
      count := count - 1
      first_place . reset_uf_marker ( Void )
      first_place := q

      if q = Void then
        last_place := Void
      else
        q . set_pred ( Void )
      end

    end

  remove_last is
    local
      q : like first_place
    do
      q := last_place . pred
      count := count - 1
      last_place . reset_uf_marker ( Void )
      last_place := q

      if q = Void then
        first_place := Void
      else
        q . set_succ ( Void )
      end

    end

  remove ( p: like first_place ) is
    local
      q,r : like first_place
    do
      q := p . pred
      r := p . succ
      if q = Void then
        remove_first
      elseif r = Void then
        remove_last
      else
        q . set_succ ( r )
        r . set_pred ( q )
        p . reset_uf_marker ( Void )
        count := count - 1
      end
    end

  absorb_prefix ( other: like Current ) is
    local
      oldfirst, otherfirst, otherlast : like first_place
      othercount : INTEGER

    do
      if not other . is_empty then
	otherfirst := other . first_place
	otherlast := other . last_place
	othercount := other . count
        uf_marker . unite ( other . uf_marker )
	other . wipe_out

	if is_empty then
	  first_place := otherfirst
	  last_place := otherlast
        else
	  oldfirst := first_place
	  first_place := otherfirst
	  otherlast .  set_succ ( oldfirst )
	  oldfirst . set_pred ( otherlast )
        end
        count := count + othercount

      end
    end


  absorb_suffix ( other: like Current ) is
    local
      oldlast, otherfirst, otherlast : like first_place
      othercount : INTEGER

    do
      if not other . is_empty then
	otherfirst := other . first_place
	otherlast := other . last_place
	othercount := other . count
        uf_marker . unite ( other . uf_marker )
	other . wipe_out

	if is_empty then
	  first_place := otherfirst
	  last_place := otherlast
        else
	  oldlast := last_place
	  last_place := otherlast
	  otherfirst .  set_pred ( oldlast )
	  oldlast . set_succ ( otherfirst )
        end
        count := count + othercount

      end
    end

  absorb_before ( other: like Current; p: like first_place ) is
    local
      otherfirst, otherlast : like first_place
      othercount : INTEGER

    do
      if not other . is_empty then
	if p = Void then
	  absorb_suffix ( other )
	elseif p = first_place then
	  absorb_prefix ( other )
	else
	  otherfirst := other . first_place
	  otherlast := other . last_place
	  othercount := other . count
          uf_marker . unite ( other . uf_marker )
	  other . wipe_out

	  otherlast . set_succ ( p )
	  otherfirst . set_pred ( p . pred )
	  p . pred . set_succ ( otherfirst )
          p . set_pred ( otherlast )
        end
        count := count + othercount
      end
    end

  absorb_after ( other: like Current; p: like first_place ) is
    local
      otherlast, otherfirst : like first_place
      othercount : INTEGER
    do
      if not other . is_empty then
	if p = Void then
	  absorb_prefix ( other )
	elseif p = last_place then
	  absorb_suffix ( other )
	else
	  otherfirst := other . first_place
	  otherlast := other . last_place
	  othercount := other . count
          uf_marker . unite ( other . uf_marker )
	  other . wipe_out

	  otherfirst . set_pred ( p )
	  otherlast . set_succ ( p . succ )
	  p . succ . set_pred ( otherlast )
	  p . set_succ ( otherfirst )
        end
        count := count + othercount
      end
    end


  cyclic_remove ( p, q: like first_place;
      subtuple: GBN_BOX [ like Current ] ) is
    local
      subt: like Current
      oldfirst, oldlast : like first_place
    do
      if not place_lesseq ( p , q ) then
        oldfirst:= first_place
        oldlast:= last_place
        if q . succ = p then
          first_place := Void
          last_place := Void
        else
          q . succ . set_pred ( Void )
          first_place := q . succ
          p . pred . set_succ ( Void )
          last_place := p . pred
        end
	oldfirst . set_pred ( oldlast )
	oldlast . set_succ ( oldfirst )
	p . set_pred ( Void )
	q . set_succ ( Void )
      else
        if p = first_place and q = last_place then
          first_place := Void
          last_place := Void
        elseif p = first_place then
          q . succ . set_pred ( Void )
          first_place := q . succ
        elseif q = last_place then
          p . pred . set_succ ( Void )
          last_place := p . pred
        else
          p . pred . set_succ ( q . succ )
          q . succ . set_pred ( p . pred )
        end
      end
      p . set_pred ( Void )
      q . set_succ ( Void )
      !!subt . make_sublist ( protecting, p, q )
          -- the sublist must be processed even if
          -- subtuple is Void, to count the number of
          -- places removed and to alter their uf_marker
          -- field.
      count := count - subt . count

      if subtuple /= Void then
        subtuple . put ( subt )
      end
    end

feature {GBN_DLIST}
  uf_marker : GBN_UF_ELEMENT

feature {NONE}

  make is
    do
      !! uf_marker . make
    end

  make_protecting (protectorate: GBN_PROTECTED) is
    require
      nonvoid: protectorate /= Void
      different: protectorate /= Current
    do
      !! uf_marker . make
      protecting := protectorate
    ensure
      protecting: protecting = protectorate
    end

  make_sublist ( protectorate: GBN_PROTECTED; p,q : like first_place ) is
    require
      p_nonvoid : p /= Void
      q_nonvoid : q /= Void
    local
      r: like first_place
      finished : BOOLEAN
    do
      !! uf_marker . make
      protecting := protectorate
      first_place := p
      last_place := q
      first_place . set_pred ( Void )
      last_place . set_succ ( Void )
      from
        r := first_place
      until
        finished
      loop
        count := count + 1
        r . reset_uf_marker ( uf_marker )
        finished := r = last_place
        r := r . succ
      end
      
    ensure
      p_first: p = first_place
      q_last : q = last_place
      protecting: protecting = protectorate
    end

invariant
  count = 0 implies first_place = Void
  first_place = Void implies last_place = Void
  last_place = Void implies count = 0
  first_place /= Void implies first_place . pred = Void
  last_place /= Void implies last_place . succ = Void
end -- class GBN_DLIST [G]