class BTLIST [G]
  -- Vtuples realised by binary trees

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.'

creation
  make

creation {PROTECTED}
 make_protecting

creation {BTLIST}
  make_with_root

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

  count : INTEGER is
    do
      if root /= Void then
	Result := root . size
      end
    end
	

  emitter: BTLIST_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 BTLIST_NODE
      if pp = Void or else root = Void then
        Result := false
      else
	from
	until
	  pp . parent = Void
	loop
	  pp := pp . parent
	end
	Result := pp = root
      end
    end

  place_lesseq ( p, q : like first_place ) : BOOLEAN is
    local
      p1, q1 : like first_place
      panc, qanc : ARRAY [ like first_place ]
      ip, iq : INTEGER
    do

      if p = q then
	Result := true
      else
	from
	  !! panc . make ( 1, 50 )
	  p1 := p
	until
	  p1 = Void
	loop
	  ip := ip + 1
	  panc . force ( p1, ip )
	  p1 := p1 . parent
	end

	from
	  !! qanc . make ( 1, 50 )
	  q1 := q
	until
	  q1 = Void
	loop
	  iq := iq + 1
	  qanc . force ( q1, iq )
	  q1 := q1 . parent
	end

	from
	until
	  ip = 0 or else iq = 0 or else
	    panc . item ( ip ) /= qanc . item ( iq )
	loop
	  ip := ip - 1
	  iq := iq - 1
	end
		-- p/=q, so ip > 0 or iq > 0

	if ip = 0 then
		-- p ancesor of q
	  Result := qanc . item ( iq ) = p . rchild
	elseif iq = 0 then
		-- q ancesor of p
	  Result := panc . item ( ip ) = q . lchild
	else
		-- independent
	  p1 := panc . item ( ip )
	  Result := p1 = p1 . parent . lchild
		-- so qanc . item ( iq ) must be the rchild
	end

      end
    end

  first_place : BTLIST_NODE [G] is 
    do
      if root = Void then
	Result := Void
      else
	Result := leftmost_descendant ( root )
      end
    end

  last_place : like first_place is
    do
      if root = Void then
	Result := Void
      else
	Result := rightmost_descendant ( root )
      end
    end

  rank ( p : like first_place ) : INTEGER is
    local
      q, r : like first_place
    do
      from
	q := p
	r := p . parent
	if p . lchild /= Void then
	  Result := p . lchild . size + 1
	else
	  Result := 1
	end
      until
	r = Void
      loop
	Result := Result + 1
	if q = r . rchild and r . lchild /= Void then
	    Result := Result + r . lchild . size
	end
	q := r
	r := q . parent
      end
    end

  nth_after ( n: INTEGER; p : like first_place ) : like first_place is
    local
      r : INTEGER
    do
      r := 1 + ( rank ( p ) + n - 1 ) \\ count
      Result := nth_place ( r )
    end

  nth_before ( n: INTEGER; p : like first_place ) : like first_place is
    local
      r : INTEGER
    do
      r := 1 + ( rank ( p ) - n - 1 ) \\ count
      Result := nth_place ( r )
    end

  nth_place ( n : INTEGER ) : like first_place is
    local
      p : like first_place
      acc : INTEGER
    do
      from
	p := root
      until
	p = Void
      loop
	if p . lchild /= Void and then 
		acc + p . lchild . size >= n then
	  p := p . lchild
	else
	  if p . lchild /= Void then
	    acc := acc + p . lchild . size
	  end
	  acc := acc + 1
	  if acc = n then
	    Result := p
	    p := Void
	  else
	    p := p . rchild
	  end
	end
      end
    end

  succ ( p: like first_place ) : like first_place is
	-- inorder successor
    local
      q : like first_place
    do
      if p . rchild /= Void then
	Result := leftmost_descendant ( p . rchild )
      else
	from
	  q := p
	  Result := p . parent
	until
	  Result = Void or else q = Result . lchild
	loop
	  q := Result
	  Result := Result . parent
	end
      end
    end
      
  pred ( p: like first_place ) : like first_place is
	-- inorder predecessor
    local
      q : like first_place
    do
      if p . lchild /= Void then
	Result := rightmost_descendant ( p . lchild )
      else
	from
	  q := p
	  Result := p . parent
	until
	  Result = Void or else q = Result . rchild
	loop
	  q := Result
	  Result := Result . parent
	end
      end
    end
      

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

-- deferred features inherited from VTUPLE:

  replica: like Current is
    do
      !! Result . make_with_root ( isomorphic_subtree ( root ),
		protecting )
    end

  wipe_out is
    do
      root := Void
    end

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

      if root = Void then
        root := q
      else
	p := first_place
	q . set_parent ( p )
	p . set_lchild ( q )
	from
	until
	  p = Void
	loop
	  p . set_size ( p . size + 1 )
	  p := p . parent
	end
      end
    end

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

      if root = Void then
        root := q
      else
	p := last_place
	q . set_parent ( p )
	p . set_rchild ( q )
	from
	until
	  p = Void
	loop
	  p . set_size ( p . size + 1 )
	  p := p . parent
	end
      end
    end


  add_after ( x: G; p: like first_place ) is
    local
      q,r : like first_place
    do
      if p = Void then
        push ( x )
      elseif succ ( p ) = Void then
        add_last ( x )
      else
	!! q . make ( x )
	if p . rchild = Void then
	  p . set_rchild ( q )
	  q . set_parent ( p )
	else
	  from
	    r := p . rchild
	  until
	    r . lchild = Void
	  loop
	    r := r . lchild
	  end
	  r . set_lchild ( q )
	  q . set_parent ( r )
	end
	from
	  r := q . parent
	  until
	  r = Void
	loop
	  r . set_size ( r . size + 1 )
	  r := r . parent
	end
      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 pred ( p ) = Void then
        push ( x )
      else
	!! q . make ( x )
	if p . lchild = Void then
	  p . set_lchild ( q )
	  q . set_parent ( p )
	else
	  from
	    r := p . lchild
	  until
	    r . rchild = Void
	  loop
	    r := r . rchild
	  end
	  r . set_rchild ( q )
	  q . set_parent ( r )
	end
	from
	  r := q . parent
	  until
	  r = Void
	loop
	  r . set_size ( r . size + 1 )
	  r := r . parent
	end
      end
    end

  pop is
    local
      q : like  first_place 
    do
      q := first_place
      if q = root then
	root := q . rchild
	if root /= Void then
	  root . set_parent ( Void )
	end
	q . unlink
      else
        prune ( q )
      end
    end

  remove_last is
    local
      q : like  first_place
    do
      q := last_place
      if q = root then
	root := q . lchild
	if root /= Void then
	  root . set_parent ( Void )
	end
	q . unlink
      else
        prune ( q )
      end
    end

  remove ( p: like first_place ) is
    local
      q,r : like first_place
    do
      if p . lchild = Void then
	q := p . rchild
	prune ( p )
	if p = root then
	  root := q
	  if root /= Void then
	    root . set_parent ( Void )
	  end
	end
      elseif p . rchild = Void then
	q := p . lchild
	prune ( p )
	if p = root then
	  root := q
	  if root /= Void then
	    root . set_parent ( Void )
	  end
	end
      else
	q := succ ( p )
	prune ( q )
	q . set_item ( p . item )
	q . set_parent ( p . parent )
	if q . parent /= Void then
	  if q = q . parent . lchild then
	    q . parent . set_lchild ( q )
	  else
	    q . parent . set_rchild ( q )
	  end
	else
	  root := q
	end
	q .set_lchild ( p . lchild )
	if q . lchild /= Void then
	  q . lchild . set_parent ( q )
	end
	q .set_rchild ( p . rchild )
	if q . rchild /= Void then
	  q . rchild . set_parent ( q )
	end
      end

	p . unlink
   end

  absorb_prefix ( other : like Current ) is
    local
      newsize: INTEGER
      oldroot, otherroot, p : like first_place
      temp : BOX [ like first_place ]
    do
      if is_empty then
	root := other . root
	other . wipe_out
      elseif not other . is_empty then
	!! temp . make
	oldroot := root
	otherroot := other . root
	wipe_out
	other . wipe_out
	join2 ( otherroot, oldroot, temp )
	root := temp . item
      end
    end

  absorb_suffix ( other : like Current ) is
    local
      newsize: INTEGER
      otherroot, oldroot, p : like first_place
      temp : BOX [ like first_place ]
    do
      if is_empty then
	root := other . root
	other . wipe_out
      elseif not other . is_empty then
	!! temp . make
	oldroot := root
	otherroot := other . root
	other . wipe_out
	wipe_out
	join2 ( oldroot, otherroot, temp )
	root := temp . item
      end
    end

  absorb_before ( other: like Current; p: like first_place ) is
    local
      before, after : BOX [ like first_place ]
      otherroot : like first_place
      newsize : INTEGER
      temp : BOX [ like first_place ]
    do
      if is_empty then
	root := other . root
	other . wipe_out
      elseif p = Void then
	absorb_suffix ( other )
      elseif p = first_place then
	absorb_prefix ( other )
      else
	!! temp . make
	newsize := 1
	otherroot := other . root
	other . wipe_out
	!! before . make
	!! after . make
	split ( p, before, after )
	join2 ( before . item, otherroot , temp )
	p . set_lchild ( temp . item )
	if p . lchild /= Void then
	  newsize := 1 + p . lchild . size
	  p . lchild . set_parent ( p )
	end
	p . set_rchild ( after . item )
	if p . rchild /= Void then
	  newsize := newsize + p . rchild . size
	  p . rchild . set_parent ( p )
	end
	root := p
	root . set_size ( newsize )
	root . set_parent ( Void )
      end
    end

  absorb_after ( other: like Current; p: like first_place ) is
    local
      before, after : BOX [ like first_place ]
      otherroot : like first_place
      newsize : INTEGER
      temp : BOX [ like first_place ]
    do
      if is_empty then
	root := other . root
	other . wipe_out
      elseif p = Void then
	absorb_prefix ( other )
      elseif p = last_place then
	absorb_suffix ( other )
      else
	!! temp . make
	newsize := 1
	otherroot := other . root
	other . wipe_out
	!! before . make
	!! after . make
	split ( p, before, after )
	join2 ( otherroot, after . item, temp )
	p . set_rchild ( temp . item )
	if p . rchild /= Void then
	  newsize := 1 + p . rchild . size
	  p . rchild . set_parent ( p )
	end
	p . set_lchild ( before . item )
	if p . lchild /= Void then
	  newsize := newsize + p . lchild . size
	  p . lchild . set_parent ( p )
	end
	root := p
	root . set_size ( newsize )
	root . set_parent ( Void )
      end
    end

  cyclic_remove ( p, q: like first_place;
      subtuple: BOX [ like Current ] ) is
    local
      subtree, ptree, qtree : like Current
      temp, box1, box2, box3 : BOX [ like first_place ]
inspector : BTREE_INSPECTOR [ G ]
    do
!! inspector
      !! box1 . make
      !! box2 . make
      !! box3 . make
      !! temp . make
io . put_string ( "cyclic remove: p . item " + p . item . out +
	" q . item " + q . item . out + "%N" )

      if p = q then
	remove ( p )
	!! subtree . make_with_root ( p, protecting )
	if subtuple /= Void then
	  subtuple . put ( subtree )
	end
      elseif p = succ ( q ) or else p = first_place and then q = last_place
      then
	!! subtree . make_with_root ( root, protecting )
	if subtuple /= Void then
	  subtuple . put ( subtree )
	end
	wipe_out
      elseif p = first_place then
	split ( q, box1, box2 )
	!! subtree . make_with_root ( box1.item, protecting )
	!! qtree . make_with_root ( q, protecting )
	subtree . absorb_suffix ( qtree )
	if subtuple /= Void then
	  subtuple . put ( subtree )
	end
	root := box2.item
	if root /= Void then
	  root . set_parent ( Void )
	end
      elseif q = last_place then
	split ( p , box1, box2 )
	!! subtree . make_with_root ( box2.item, protecting )
	!! ptree . make_with_root ( p, protecting )
	subtree . absorb_prefix ( ptree )
	if subtuple /= Void then
	  subtuple . put ( subtree )
	end
	root := box1.item
	if root /= Void then
	  root . set_parent ( Void )
	end
      elseif place_lesseq ( p, q) then
	split ( p, box1, box2 )
	split ( q, box2, box3 )
	!! subtree . make_with_root ( box2.item, protecting )
	!! ptree . make_with_root ( p, protecting )
	subtree . absorb_prefix ( ptree )
	!! qtree . make_with_root ( q, protecting )
	subtree . absorb_suffix ( qtree )
	if subtuple /= Void then
	  subtuple . put ( subtree )
	end
	join2 ( box2 . item , box3 . item, temp )
	root := temp . item
      else
	split ( q, box1, box2 )
	split ( p, box2, box3 )
	join2 ( box3 . item, box1 . item, temp )
	!! subtree . make_with_root ( temp . item,
		protecting )
	!! ptree . make_with_root ( p, protecting )
	subtree . absorb_prefix ( ptree )
	!! qtree . make_with_root ( q, protecting )
	subtree . absorb_suffix ( qtree )
	if subtuple /= Void then
	  subtuple . put ( subtree )
	end
	root := box2.item
      end
io . put_string ( "cyclic remove: removed.. and remainder%N" )
if subtuple /= Void then
  inspector . show_subtree ( subtuple . item . root )
  inspector . local_size_check ( subtuple . item . root )
else
  io . put_string ("removed discarded%N" )
end
inspector . show_subtree ( root )
inspector . local_size_check ( root )
    end

feature {BTLIST, BTREE_INSPECTOR}

  root: like first_place


feature {NONE}

  reset_sizes ( p : like first_place ) is
    local
      q : like first_place
      temp_int : INTEGER
    do
      from
	q := p
      until
	q = Void
      loop
	if q . lchild /= Void then
	  temp_int := 1 + q . lchild . size
	else
	  temp_int := 1
	end
	if q . rchild /= Void then
	  temp_int := temp_int + q . rchild . size
	end
	q . set_size ( temp_int )
	q := q . parent
      end
    end


  leftmost_descendant ( p : like first_place ) : like first_place is
    do
      from
	Result := p
      until
	Result . lchild = Void
      loop
	Result := Result . lchild
      end
    end

  rightmost_descendant ( p : like first_place ) : like first_place is
    do
      from
	Result := p
      until
	Result . rchild = Void
      loop
	Result := Result . rchild
      end
    end

  prune ( p : like first_place ) is
    require
      nonvoid : p /= Void
      one_child : p . lchild = Void or p . rchild = Void
    local
      r : like first_place
inspector : BTREE_INSPECTOR [ G ]
    do
      r := p . parent
      if r /= Void then
	if p = r . lchild then
	  if p . lchild /= Void then
	    r . set_lchild ( p . lchild )
	  else
	    r . set_lchild ( p . rchild )
	  end
	  if r . lchild /= Void then
	    r . lchild . set_parent ( r )
	  end
	else
	  if p . lchild /= Void then
	    r . set_rchild ( p . lchild )
	  else
	    r . set_rchild ( p . rchild )
	  end
	  if r . rchild /= Void then
	    r . rchild . set_parent ( r )
	  end
	end

	from
	until
	  r = Void
	loop
	  r . set_size ( r . size - 1 )
	  r := r . parent
	end
      elseif p . lchild /= Void then
	root := p . lchild
      else
	root := p . rchild
      end

	p . unlink
    end


  isomorphic_subtree ( p : like first_place ) : like first_place is
    require
      p = Void or else has_place ( p )
    do
      if p /= Void then
	!! Result . make ( p . item )
	Result . set_size ( p . size )
	if p . lchild /= Void then
	  Result . set_lchild ( isomorphic_subtree ( p . lchild ) )
	  Result . lchild . set_parent ( Result )
	end
	if p . rchild /= Void then
	  Result . set_rchild ( isomorphic_subtree ( p . rchild ) )
	  Result . rchild . set_parent ( Result )
	end
      end
    end

  join3 ( left, mid, right : like first_place ) is
    require
      mid_nonvoid : mid /= Void
      mid_linkless : mid . parent = Void and mid . lchild = Void and
		mid . rchild = Void
      left_ne_mid : left /= mid
      left_orphan : left = Void or else left . parent = Void
      right_ne_mid : right /= mid
      right_orphan : right = Void or else right . parent = Void
      left_ne_right : left = Void or left /= right
    local
      newsize : INTEGER
    do
      newsize := 1
      mid . set_lchild ( left )
      if left /= Void then
	newsize := newsize + left . size
	left . set_parent ( mid )
      end
      mid . set_rchild ( right )
      if right /= Void then
	newsize := newsize + right . size
	right . set_parent ( mid )
      end
      mid . set_size ( newsize )
    end
      
  join2 ( p, q : like first_place; answer : BOX [ like first_place ] ) is
    require
      answer_nonvoid : answer /= Void
      p_orphan : p = Void or else p . parent = Void
      q_orphan : q = Void or else q . parent = Void
      different : p = Void or p /= q
    local
      r : like first_place
inspector : BTREE_INSPECTOR [ G ]
    do
!! inspector
io . put_string ( "join2: subtrees p, q...%N" )
inspector . show_subtree ( p )
inspector . show_subtree ( q )


      if p = Void then
	answer . put ( q )
io . put_string ( "p void, answer = q%N" )
      elseif q = Void then
	answer . put ( p )
io . put_string ( "q void, answer = p%N" )
      elseif p . size < q . size then
		-- heuristic, attempts
		-- to keep a rough balance
	r := leftmost_descendant ( q )
io . put_string ( "r = leftmost desc. of q%N" )
	if r = q then
	  q . set_lchild ( p )
	  p . set_parent ( q )
	  q . set_size ( q . size + p . size )
	  answer . put ( q )
io . put_string ( "r = q, answer = q%N" )
	else
	  prune ( r )
	  join3 ( p, r, q )
	  answer . put ( r )
io . put_string ( "r /= q, answer = r after  join3 p, r, q%N" )
	end
      else
	r := rightmost_descendant ( p )
io . put_string ( "r = rightmost desc. of p%N" )
	if r = p then
	  p . set_rchild ( q )
	  q . set_parent ( p )
	  p . set_size ( q . size + p . size )
	  answer . put ( p )
io . put_string ( "r = p, answer = p%N" )
	else
	  prune ( r )
	  join3 ( p, r, q )
	  answer . put ( r )
io . put_string ( "r /= q, answer = r after  join3 p, r, q%N" )
	end
io . put_string ( "joined tree is%N" )
inspector . show_subtree ( answer . item )
      end
    ensure
      answer . item . parent = Void
    end

  split ( p : like first_place;
	  before, after : BOX [ like first_place ] ) is
    require
      has_p : has_place ( p )
      nonvoid : before /= Void and after /= Void
    local
      q, r, preds, succs : like first_place
      preds_low, succs_low : like first_place
      temp_int : INTEGER
inspector : BTREE_INSPECTOR [ G ]
    do
!! inspector
io . put_string ( "split; size check before split%N" )
inspector . local_size_check ( root )
      from
	preds := p . lchild
	succs := p . rchild
	q := p
	r := q . parent
      until
	r = Void
      loop
	if q = r . lchild then
	  r . set_lchild ( succs )
	  if succs /= Void then
	    succs . set_parent ( r )
	  end
	  succs := r
	  if succs_low = Void then
	    succs_low := r
	  end
	else
	  r . set_rchild ( preds )
	  if preds /= Void then
	    preds . set_parent ( r )
	  end
	  preds := r
	  if preds_low = Void then
	    preds_low := r
	  end
	end
	q := r
	r := q . parent
      end

      if preds /= Void then
	preds . set_parent ( Void )
	reset_sizes ( preds_low )
      end

      if succs /= Void then
	succs . set_parent ( Void )
	reset_sizes ( succs_low )
      end

      p . unlink

      before . put ( preds )
      after . put ( succs )
!! inspector
io . put_string ( "After split on " + p . item . out + "%N" )
inspector . show_subtree ( before . item )
inspector . local_size_check ( before . item )
inspector . show_subtree ( after . item )
inspector . local_size_check ( after . item )
      root := Void
    end

  make is
    do
    end

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

  make_with_root ( p : like first_place; protectorate: PROTECTED ) is
    do
      root := p
      if root /= Void then
	root . set_parent ( Void )
      end
      protecting := protectorate
    end


invariant
  count = 0 implies root = Void
  root = Void implies count = 0
  root /= Void implies root . parent = Void
end -- class BTLIST [G]