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

inherit
  VTUPLE [G]
  redefine
    emitter, reverse_emitter,
    cyclic_emitter, reverse_cyclic_emitter
end
    -- The emitters need to be redefined simply to
    -- get the correct type for `place.'  There was
    -- some difficulty compiling the reverse emitters
    -- which may be a SmallEiffel inadequacy.

creation
  make

creation {PROTECTED}
 make_protecting

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

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


  emitter: DLIST_EMITTER [G] is
      -- only change is the inherited type.  This is
      -- a type anchor, so the change passes to the other
      -- emitters.
    do
      !! Result . make ( Current, false )
    end

  reverse_emitter: like emitter is
    do
      !! Result . make ( Current, true )
    end

  cyclic_emitter (start_place: like first_place): like emitter is
    do
      !! Result . make_cyclic ( Current, false, start_place )
    end

  reverse_cyclic_emitter (start_place: like first_place): like emitter is
    do
      !! Result . make_cyclic ( Current, true, start_place )
    end


  has_place ( p: PLACE ) : BOOLEAN is
    local
      pp : like first_place
    do
      pp ?= p
        -- `has_place' is not restricted
        -- to arguments of type 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 : DLIST_PLACE [G] is 
    do
      Result := myfirst
    end

  last_place : like first_place is
    do
      Result := mylast
    end

  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 VTUPLE:

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

  wipe_out is
    do
      myfirst := Void
      mylast := Void
      !! uf_marker . make
      count := 0
    end

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

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

      if mylast = Void then
        mylast := myfirst
      end
      count := count + 1
    end

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

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

      mylast := q
      if myfirst = Void then
        myfirst := 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 is
    -- First_place is removed from tuple.
    local
      q : like first_place
    do
      q := myfirst . succ
      count := count - 1
      myfirst . reset_uf_marker ( Void )
      myfirst := q

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

    end

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

      if q = Void then
        myfirst := 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
        pop
      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
	  myfirst := otherfirst
	  mylast := otherlast
        else
	  oldfirst := myfirst
	  myfirst := 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
	  myfirst := otherfirst
	  mylast := otherlast
        else
	  oldlast := mylast
	  mylast := 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: BOX [ like Current ] ) is
    local
      subt: like Current
      oldfirst, oldlast : like first_place
    do
      if not place_lesseq ( p , q ) then
        oldfirst:= myfirst
        oldlast:= mylast
        if q . succ = p then
          myfirst := Void
          mylast := Void
        else
          q . succ . set_pred ( Void )
          myfirst := q . succ
          p . pred . set_succ ( Void )
          mylast := p . pred
        end
	oldfirst . set_pred ( oldlast )
	oldlast . set_succ ( oldfirst )
	p . set_pred ( Void )
	q . set_succ ( Void )
      else
        if p = myfirst and q = mylast then
          myfirst := Void
          mylast := Void
        elseif p = myfirst then
          q . succ . set_pred ( Void )
          myfirst := q . succ
        elseif q = mylast then
          p . pred . set_succ ( Void )
          mylast := 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 {DLIST}
  uf_marker : UF_ELEMENT

feature {NONE}
  myfirst, mylast : like first_place

  make is
    do
      !! uf_marker . make
    end

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

  make_sublist ( protectorate: 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
      myfirst := p
      mylast := q
      myfirst . set_pred ( Void )
      mylast . set_succ ( Void )
      from
        r := myfirst
      until
        finished
      loop
        count := count + 1
        r . reset_uf_marker ( uf_marker )
        finished := r = mylast
        r := r . succ
      end
      
    ensure
      p_first: p = first_place
      q_last : q = last_place
      protecting: protecting = protectorate
    end

invariant
  count = 0 implies myfirst = Void
  myfirst = Void implies mylast = Void
  mylast = Void implies count = 0
  myfirst /= Void implies myfirst . pred = Void
  mylast /= Void implies mylast . succ = Void
end -- class DLIST [G]