{-# LANGUAGE DataKinds             #-}
{-# LANGUAGE PolyKinds             #-}
{-# LANGUAGE TypeFamilies          #-}
{-# LANGUAGE TypeOperators         #-}
{-# LANGUAGE UndecidableInstances  #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FlexibleInstances     #-}

-- | See <https://www.cs.kent.ac.uk/people/staff/smk/redblack/rb.html here> for
-- the original term-level code by Stefan Kahrs.
--
-- @since 0.1.1.0
module Type.RBSet
  ( -- * Core type
    TypeSet (..)
  , Empty
    -- * Set operations
  , Member
  , Insertable(Insert)
  , InsertAll
  , FromList
  , Removable(Remove)
  , Merge
  ) where

import Type.Compare
import GHC.TypeLits

-- | The color of a node.
data Color = R
           | B
    deriving (Show,Eq)

-- | A Red-Black tree.
--
-- @since 0.1.1.0
data TypeSet a = E
               | N Color (TypeSet a) a (TypeSet a)
    deriving (Show,Eq)

-- | A map without entries.
type Empty = E

--
--
-- Insertion

{- | Insert a list of type level key / value pairs into a type-level map.
-}
type family InsertAll (es :: [k]) (t :: TypeSet k) :: TypeSet k where
    InsertAll '[] t = t
    InsertAll ( v ': es ) t = Insert v (InsertAll es t)

{- | Build a type-level map out of a list of type level key / value pairs.
-}
type FromList (es :: [k]) = InsertAll es Empty

{- | The associated type family 'Insert' produces the resulting map.

 -}
class Insertable (k :: ki) (t :: TypeSet ki) where
    type Insert k t :: TypeSet ki

-- insert x s =
--  T B a z b
--  where
--  T _ a z b = ins s
instance (InsertableHelper1 k t, Insert1 k t ~ inserted, CanMakeBlack inserted) => Insertable k t where
    type Insert k t = MakeBlack (Insert1 k t)

class CanMakeBlack (t :: TypeSet ki) where
    type MakeBlack t :: TypeSet ki

instance CanMakeBlack (N color left k right) where
    type MakeBlack (N color left k right) = N B left k right

instance CanMakeBlack E where
    type MakeBlack E = E

class InsertableHelper1 (k :: ki)
                        (t :: TypeSet ki) where
    type Insert1 k t :: TypeSet ki

instance InsertableHelper1 k E where
    type Insert1 k E = N R E k E

instance (CmpType k k' ~ ordering,
          InsertableHelper2 ordering k color left k' right
         )
         => InsertableHelper1 k (N color left k' right) where
    -- FIXME possible duplicate work with CmpType: both in constraint and in associated type family.
    -- Is that bad? How to avoid it?
    type Insert1 k (N color left k' right) = Insert2 (CmpType k k') k color left k' right

class InsertableHelper2 (ordering :: Ordering)
                        (k :: ki)
                        (color :: Color)
                        (left :: TypeSet ki)
                        (k' :: ki)
                        (right :: TypeSet ki) where
    type Insert2 ordering k color left k' right :: TypeSet ki

--  ins s@(T B a y b)
--      | x<y = balance (ins a) y b
instance (InsertableHelper1 k left, Insert1 k left ~ inserted,
          Balanceable inserted k' right
         )
         => InsertableHelper2 LT k B left k' right where
    type Insert2              LT k B left k' right = Balance (Insert1 k left) k' right

--  ins s@(T B a y b)
--      | x<y = balance (ins a) y b
instance (InsertableHelper1 k left, Insert1 k left ~ inserted,
          Balanceable inserted k' right
         )
         => InsertableHelper2 LT k R left k' right where
    type Insert2              LT k R left k' right = N R (Insert1 k left) k' right


instance InsertableHelper2 EQ k color left k right where
    type Insert2           EQ k color left k right = N color left k right

--  ins s@(T B a y b)
--      | ...
--      | x>y = balance a y (ins b)
instance (InsertableHelper1 k right, Insert1 k right ~ inserted,
          Balanceable left  k' inserted
         )
         => InsertableHelper2 GT k B left k' right where
    type Insert2              GT k B left k' right = Balance left  k' (Insert1 k right)

--  ins s@(T R a y b)
--      | ...
--      | x>y = T R a y (ins b)
instance (InsertableHelper1 k right, Insert1 k right ~ inserted,
          Balanceable left  k' inserted
         )
         => InsertableHelper2 GT k R left k' right where
    type Insert2              GT k R left k' right = N R left k' (Insert1 k right)

data BalanceAction = BalanceSpecial
                   | BalanceLL
                   | BalanceLR
                   | BalanceRL
                   | BalanceRR
                   | DoNotBalance
                   deriving Show

type family ShouldBalance (left :: TypeSet ki) (right :: TypeSet ki) :: BalanceAction where
    ShouldBalance (N R _ _ _) (N R _ _ _) = BalanceSpecial
    ShouldBalance (N R (N R _ _ _) _ _) _ = BalanceLL
    ShouldBalance (N R _ _ (N R _ _ _)) _ = BalanceLR
    ShouldBalance _ (N R (N R _ _ _) _ _) = BalanceRL
    ShouldBalance _ (N R _ _ (N R _ _ _)) = BalanceRR
    ShouldBalance _ _                     = DoNotBalance

class Balanceable (left :: TypeSet ki) (k :: ki) (right :: TypeSet ki) where
    type Balance left k right :: TypeSet ki

instance (ShouldBalance left right ~ action,
          BalanceableHelper action left k right
         )
         => Balanceable left k right where
    -- FIXME possible duplicate work with ShouldBalance: both in constraint and in associated type family.
    -- Is that bad? How to avoid it?
    type Balance left k right = Balance' (ShouldBalance left right) left k right

class BalanceableHelper (action :: BalanceAction)
                        (left :: TypeSet ki)
                        (k :: ki)
                        (right :: TypeSet ki) where
    type Balance' action left k right :: TypeSet ki

-- balance (T R a x b) y (T R c z d) = T R (T B a x b) y (T B c z d)
instance BalanceableHelper BalanceSpecial (N R left1 k1 right1) kx (N R left2 k2 right2) where
    type Balance'          BalanceSpecial (N R left1 k1 right1) kx (N R left2 k2 right2) =
                                      N R (N B left1 k1 right1) kx (N B left2 k2 right2)

-- balance (T R (T R a x b) y c) z d = T R (T B a x b) y (T B c z d)
instance BalanceableHelper BalanceLL (N R (N R a k1 b) k2 c) k3 d where
    type Balance'          BalanceLL (N R (N R a k1 b) k2 c) k3 d =
                                 N R (N B a k1 b) k2 (N B c k3 d)

-- balance (T R a x (T R b y c)) z d = T R (T B a x b) y (T B c z d)
instance BalanceableHelper BalanceLR (N R a k1 (N R b k2 c)) k3 d where
    type Balance'          BalanceLR (N R a k1 (N R b k2 c)) k3 d =
                                 N R (N B a k1 b) k2 (N B c k3 d)

-- balance a x (T R (T R b y c) z d) = T R (T B a x b) y (T B c z d)
instance BalanceableHelper BalanceRL a k1 (N R (N R b k2 c) k3 d) where
    type Balance'          BalanceRL a k1 (N R (N R b k2 c) k3 d) =
                                 N R (N B a k1 b) k2 (N B c k3 d)


-- balance a x (T R b y (T R c z d)) = T R (T B a x b) y (T B c z d)
instance BalanceableHelper BalanceRR a k1(N R b k2 (N R c k3 d)) where
    type Balance'          BalanceRR a k1(N R b k2 (N R c k3 d)) =
                                 N R (N B a k1 b) k2 (N B c k3 d)

-- balance a x b = T B a x b
instance BalanceableHelper DoNotBalance a k b where
    type Balance'          DoNotBalance a k b = N B a k b


--- Member
---
---
------------------------------------------------------------------------------
-- | /O(log n)/. Determine membership in the 'TypeSet.'
type family Member (t :: k) (bst :: TypeSet k)  :: Bool where
  Member t 'E = 'False
  Member t ('N _ lbst a rbst) = MemberImpl (CmpType t a) t lbst rbst

type family MemberImpl (ord :: Ordering)
                       (t :: k)
                       (lbst :: TypeSet k)
                       (rbst :: TypeSet k) :: Bool where
  MemberImpl 'EQ t lbst rbst = 'True
  MemberImpl 'LT t lbst rbst = Member t lbst
  MemberImpl 'GT t lbst rbst = Member t rbst

------------------------------------------------------------------------------
-- | /O(m log n)/ for @Merge m n@; put your smaller set on the left side. Merge
-- two 'TypeSet's together.
type family Merge (small :: TypeSet k) (big :: TypeSet k) :: TypeSet k where
  Merge Empty big   = big
  Merge small Empty = small
  Merge ('N _ lbst a rbst) big = Merge rbst (Merge lbst (Insert a big))


--
--
--
-- deletion
--
--
--

type family DiscriminateBalL (l :: TypeSet ki) (r :: TypeSet ki) :: Bool where
    DiscriminateBalL (N R _ _ _) _ = False
    DiscriminateBalL _           _ = True

class BalanceableL (l :: TypeSet ki) (k :: ki) (r :: TypeSet ki) where
    type BalL l k r :: TypeSet ki

class BalanceableHelperL (b :: Bool) (l :: TypeSet ki) (k :: ki) (r :: TypeSet ki) where
    type BalL' b l k r :: TypeSet ki

instance (DiscriminateBalL l r ~ b, BalanceableHelperL b l k r) => BalanceableL l k r where
    type BalL l k r = BalL' (DiscriminateBalL l r) l k r

-- balleft :: RB a -> a -> RB a -> RB a
-- balleft (T R a x b) y c = T R (T B a x b) y c
instance BalanceableHelperL False (N R left1 k1 right1) k2 right2 where
    type BalL'              False (N R left1 k1 right1) k2 right2 =
                             (N R (N B left1 k1 right1) k2 right2)

-- balleft bl x (T B a y b) = balance bl x (T R a y b)
-- the @(N B in the call to balance tree is misleading, as it is ingored...
instance (N R t2 z t3 ~ g, BalanceableHelper (ShouldBalance t1 g) t1 y g) =>
    BalanceableHelperL True t1 y (N B t2 z t3) where
    type BalL'         True t1 y (N B t2 z t3)
                 =  Balance t1 y (N R t2 z t3)

-- balleft bl x (T R (T B a y b) z c) = T R (T B bl x a) y (balance b z (sub1 c))
instance (N R l k r ~ g, BalanceableHelper    (ShouldBalance t3 g) t3 z g) =>
    BalanceableHelperL True t1 y (N R (N B t2 u t3) z (N B l k r)) where
    type BalL'         True t1 y (N R (N B t2 u t3) z (N B l k r)) =
                             N R (N B t1 y t2) u (Balance t3 z (N R l k r))


-- balright :: RB a -> a -> RB a -> RB a
-- balright a x (T R b y c) = T R a x (T B b y c)
-- balright (T B a x b) y bl = balance (T R a x b) y bl
-- balright (T R a x (T B b y c)) z bl = T R (balance (sub1 a) x b) y (T B c z bl)
type family DiscriminateBalR (l :: TypeSet ki) (r :: TypeSet ki) :: Bool where
    DiscriminateBalR _ (N R _ _ _) = False
    DiscriminateBalR _ _           = True

class BalanceableR (l :: TypeSet ki) (k :: ki) (r :: TypeSet ki) where
    type BalR l k r :: TypeSet ki

class BalanceableHelperR (b :: Bool) (l :: TypeSet ki) (k :: ki) (r :: TypeSet ki) where
    type BalR' b l k r :: TypeSet ki

instance (DiscriminateBalR l r ~ b, BalanceableHelperR b l k r) => BalanceableR l k r where
    type BalR l k r = BalR' (DiscriminateBalR l r) l k r

-- balright :: RB a -> a -> RB a -> RB a
-- balright a x (T R b y c) = T R a x (T B b y c)
instance BalanceableHelperR False right2 k2 (N R left1 k1 right1) where
    type BalR'              False right2 k2 (N R left1 k1 right1) =
                                  (N R right2 k2 (N B left1 k1 right1))

-- balright (T B a x b) y bl = balance (T R a x b) y bl
instance (N R t2 z t3 ~ g, ShouldBalance g t1 ~ shouldbalance, BalanceableHelper shouldbalance g y t1) =>
    BalanceableHelperR True (N B t2 z t3) y t1 where
    type BalR'         True (N B t2 z t3) y t1
             =  Balance (N R t2 z t3) y t1

-- balright (T R a x (T B b y c)) z bl = T R (balance (sub1 a) x b) y (T B c z bl)
instance (N R t2 u t3 ~ g, ShouldBalance g l ~ shouldbalance, BalanceableHelper shouldbalance g z l) =>
    BalanceableHelperR True (N R (N B t2 u t3) z (N B l k r)) y t1 where
    type BalR'         True (N R (N B t2 u t3) z (N B l k r)) y t1 =
                             N R (Balance (N R t2 u t3) z l) k (N B r y t1)
-- app :: RB a -> RB a -> RB a
-- app E x = x
-- app x E = x
-- app (T R a x b) (T R c y d) =
--  case app b c of
--      T R b' z c' -> T R(T R a x b') z (T R c' y d)
--      bc -> T R a x (T R bc y d)
-- app (T B a x b) (T B c y d) =
--  case app b c of
--      T R b' z c' -> T R(T B a x b') z (T B c' y d)
--      bc -> balleft a x (T B bc y d)
-- app a (T R b x c) = T R (app a b) x c
-- app (T R a x b) c = T R a x (app b c)


class Fuseable (l :: TypeSet ki) (r :: TypeSet ki) where
    type Fuse l r :: TypeSet ki

instance Fuseable E E where
    type Fuse E E = E

-- app E x = x
instance Fuseable E (N color left k right) where
    type Fuse E (N color left k right) = N color left k right

-- app x E = x
instance Fuseable (N color left k right) E where
    type Fuse (N color left k right) E = N color left k right

-- app a (T R b x c) = T R (app a b) x c
instance Fuseable (N B left1 k1 right1) left2
    => Fuseable (N B left1 k1 right1) (N R left2 k2 right2) where
    type Fuse   (N B left1 k1 right1) (N R left2 k2 right2) = N R (Fuse (N B left1 k1 right1) left2) k2 right2


-- app (T R a x b) c = T R a x (app b c)
instance Fuseable right1 (N B left2 k2 right2)
    => Fuseable (N R left1 k1 right1) (N B left2 k2 right2) where
    type Fuse   (N R left1 k1 right1) (N B left2 k2 right2) = N R left1 k1 (Fuse right1 (N B left2 k2 right2))


-- app (T R a x b) (T R c y d) =
instance (Fuseable right1 left2, Fuse right1 left2 ~ fused, FuseableHelper1 fused (N R left1 k1 right1) (N R left2 k2 right2))
    => Fuseable (N R left1 k1 right1) (N R left2 k2 right2) where
    type Fuse   (N R left1 k1 right1) (N R left2 k2 right2) = Fuse1 (Fuse right1 left2) (N R left1 k1 right1) (N R left2 k2 right2)

class FuseableHelper1 (fused :: TypeSet ki) (l :: TypeSet ki) (r :: TypeSet ki) where
    type Fuse1 fused l r :: TypeSet ki

-- app (T R a x b) (T R c y d) =
--  case app b c of
--      T R b' z c' -> T R (T R a x b') z (T R c' y d)
-- FIXME: The Fuseable constraint is repeated from avobe :(
instance (Fuseable right1 left2, Fuse right1 left2 ~ N R s1 z s2)
    => FuseableHelper1 (N R s1 z s2) (N R left1 k1 right1) (N R left2 k2 right2) where
    type Fuse1         (N R s1 z s2) (N R left1 k1 right1) (N R left2 k2 right2) = N R (N R left1 k1 s1) z (N R s2 k2 right2)


-- app (T R a x b) (T R c y d) =
--  case app b c of
--      ...
--      bc -> T R a x (T R bc y d)
-- FIXME: The Fuseable constraint is repeated from above :(
instance (Fuseable right1 left2, Fuse right1 left2 ~ N B s1 z s2)
    => FuseableHelper1 (N B s1 z s2) (N R left1 k1 right1) (N R left2 k2 right2) where
    type Fuse1         (N B s1 z s2) (N R left1 k1 right1) (N R left2 k2 right2) = N R left1 k1 (N R (N B s1 z s2) k2 right2)

-- app (T R a x b) (T R c y d) =
--  case app b c of
--      ...
--      bc -> T R a x (T R bc y d)
instance FuseableHelper1 E (N R left1 k1 E) (N R E k2 right2) where
    type Fuse1           E (N R left1 k1 E) (N R E k2 right2) = N R left1 k1 (N R E k2 right2)

-- app (T B a x b) (T B c y d) =
instance (Fuseable right1 left2, Fuse right1 left2 ~ fused, FuseableHelper2 fused (N B left1 k1 right1) (N B left2 k2 right2))
    => Fuseable (N B left1 k1 right1) (N B left2 k2 right2) where
    type Fuse   (N B left1 k1 right1) (N B left2 k2 right2) = Fuse2 (Fuse right1 left2) (N B left1 k1 right1) (N B left2 k2 right2)

-- could FuseableHelper1 and FuseableHelper2 be, well... fused?
class FuseableHelper2 (fused :: TypeSet ki) (l :: TypeSet ki) (r :: TypeSet ki) where
    type Fuse2 fused l r :: TypeSet ki

-- app (T B a x b) (T B c y d) =
--  case app b c of
--      T R b' z c' -> T R (T B a x b') z (T B c' y d)
instance (Fuseable right1 left2, Fuse right1 left2 ~ N R s1 z s2)
    => FuseableHelper2 (N R s1 z s2) (N B left1 k1 right1) (N B left2 k2 right2) where
    type Fuse2         (N R s1 z s2) (N B left1 k1 right1) (N B left2 k2 right2) = N R (N B left1 k1 s1) z (N B s2 k2 right2)

-- app (T B a x b) (T B c y d) =
--  case app b c of
--      ...
--      bc -> balleft a x (T B bc y d)
instance (Fuseable right1 left2, Fuse right1 left2 ~ N B s1 z s2, BalanceableL left1 k1 (N B (N B s1 z s2) k2 right2))
    => FuseableHelper2 (N B s1 z s2) (N B left1 k1 right1) (N B left2 k2 right2) where
    type Fuse2         (N B s1 z s2) (N B left1 k1 right1) (N B left2 k2 right2) = BalL left1 k1 (N B (N B s1 z s2) k2 right2)

-- app (T B a x b) (T B c y d) =
--  case app b c of
--      ...
--      bc -> balleft a x (T B bc y d)
instance (BalanceableL left1 k1 (N B E k2 right2))
    => FuseableHelper2 E (N B left1 k1 E) (N B E k2 right2) where
    type Fuse2         E (N B left1 k1 E) (N B E k2 right2) = BalL left1 k1 (N B E k2 right2)


--  del E = E
--  del (T _ a y b)
--      | x<y = delformLeft a y b
--      | x>y = delformRight a y b
--      | otherwise = app a b
class Delable (k :: ki) (t :: TypeSet ki) where
    type Del k t :: TypeSet ki

--  delformLeft a@(T B _ _ _) y b = balleft (del a) y b
--  delformLeft a y b = T R (del a) y b
--  In the term-level code, the k to delete is already on the environment.
class DelableL (k :: ki) (l :: TypeSet ki) (kx :: ki)  (r :: TypeSet ki) where
    type DelL k l kx r :: TypeSet ki

--  delformLeft a@(T B _ _ _) y b = balleft (del a) y b
instance (N B leftz kz rightz ~ g, Delable k g, Del k g ~ deleted, BalanceableL deleted kx right)
    => DelableL k (N B leftz kz rightz) kx right where
    type DelL   k (N B leftz kz rightz) kx right = BalL (Del k (N B leftz kz rightz)) kx right

--  delformLeft a y b = T R (del a) y b
instance (Delable k (N R leftz kz rightz))
    => DelableL k (N R leftz kz rightz) kx right where
    type DelL   k (N R leftz kz rightz) kx right = N R (Del k (N R leftz kz rightz)) kx right

--  delformLeft a y b = T R (del a) y b
instance DelableL k E kx right where
    type DelL     k E kx right = N R E kx right

--  delformRight a y b@(T B _ _ _) = balright a y (del b)
--  delformRight a y b = T R a y (del b)
class DelableR (k :: ki) (l :: TypeSet ki) (kx :: ki) (r :: TypeSet ki) where
    type DelR k l kx r :: TypeSet ki

--  delformRight a y b@(T B _ _ _) = balright a y (del b)
instance (N B leftz kz rightz ~ g, Delable k g, Del k g ~ deleted, BalanceableR left kx deleted)
    => DelableR k left kx (N B leftz kz rightz) where
    type DelR   k left kx (N B leftz kz rightz) = BalR left kx (Del k (N B leftz kz rightz))


--  delformRight a y b = T R a y (del b)
instance (Delable k (N R leftz kz rightz))
    => DelableR k left kx (N R leftz kz rightz) where
    type   DelR k left kx (N R leftz kz rightz) = N R left kx (Del k (N R leftz kz rightz))

--  delformRight a y b = T R a y (del b)
instance DelableR k left kx E where
    type DelR     k left kx E = N R left kx E

--  del E = E
instance Delable k E where
    type Del     k E = E

-- the color is discarded
--  del (T _ a y b)
--      | x<y = delformLeft a y b
--      | x>y = delformRight a y b
--      | otherwise = app a b
instance (CmpType kx k ~ ordering, DelableHelper ordering k left kx right) => Delable k (N color left kx right) where
    type Del k (N color left kx right) = Del' (CmpType kx k) k left kx right

class DelableHelper (ordering :: Ordering) (k :: ki) (l :: TypeSet ki) (kx :: ki) (r :: TypeSet ki) where
    type Del' ordering k l kx r :: TypeSet ki

--      | x<y = delformLeft a y b
instance DelableL k left kx right => DelableHelper GT k left kx right where
    type Del'                                      GT k left kx right = DelL k left kx right

--      | otherwise = app a b
instance Fuseable left right => DelableHelper EQ k left k right where
    type Del'                                 EQ k left k right = Fuse left right

--      | x>y = delformRight a y b
instance DelableR k left kx right => DelableHelper LT k left kx right where
    type Del'                                      LT k left kx right = DelR k left kx right

{- | The associated type family 'Remove' produces the resulting map.

 -}
class Removable (k :: ki) (t :: TypeSet ki) where
    type Remove k t :: TypeSet ki

instance (Delable k t, Del k t ~ deleted, CanMakeBlack deleted) => Removable k t where
    type Remove k t = MakeBlack (Del k t)



-- The original term-level code, taken from:
-- https://www.cs.kent.ac.uk/people/staff/smk/redblack/rb.html
--
-- {- Version 1, 'untyped' -}
-- data Color = R | B deriving Show
-- data RB a = E | T Color (RB a) a (RB a) deriving Show
--
-- {- Insertion and membership test as by Okasaki -}
-- insert :: Ord a => a -> RB a -> RB a
-- insert x s =
--  T B a z b
--  where
--  T _ a z b = ins s
--  ins E = T R E x E
--  ins s@(T B a y b)
--      | x<y = balance (ins a) y b
--      | x>y = balance a y (ins b)
--      | otherwise = s
--  ins s@(T R a y b)
--      | x<y = T R (ins a) y b
--      | x>y = T R a y (ins b)
--      | otherwise = s
--
--
-- {- balance: first equation is new,
--    to make it work with a weaker invariant -}
-- balance :: RB a -> a -> RB a -> RB a
-- balance (T R a x b) y (T R c z d) = T R (T B a x b) y (T B c z d)
-- balance (T R (T R a x b) y c) z d = T R (T B a x b) y (T B c z d)
-- balance (T R a x (T R b y c)) z d = T R (T B a x b) y (T B c z d)
-- balance a x (T R b y (T R c z d)) = T R (T B a x b) y (T B c z d)
-- balance a x (T R (T R b y c) z d) = T R (T B a x b) y (T B c z d)
-- balance a x b = T B a x b
--
-- member :: Ord a => a -> RB a -> Bool
-- member x E = False
-- member x (T _ a y b)
--  | x<y = member x a
--  | x>y = member x b
--  | otherwise = True
--
-- {- deletion a la SMK -}
-- delete :: Ord a => a -> RB a -> RB a
-- delete x t =
--  case del t of {T _ a y b -> T B a y b; _ -> E}
--  where
--  del E = E
--  del (T _ a y b)
--      | x<y = delformLeft a y b
--      | x>y = delformRight a y b
--             | otherwise = app a b
--  delformLeft a@(T B _ _ _) y b = balleft (del a) y b
--  delformLeft a y b = T R (del a) y b
--
--  delformRight a y b@(T B _ _ _) = balright a y (del b)
--  delformRight a y b = T R a y (del b)
--
-- balleft :: RB a -> a -> RB a -> RB a
-- balleft (T R a x b) y c = T R (T B a x b) y c
-- balleft bl x (T B a y b) = balance bl x (T R a y b)
-- balleft bl x (T R (T B a y b) z c) = T R (T B bl x a) y (balance b z (sub1 c))
--
-- balright :: RB a -> a -> RB a -> RB a
-- balright a x (T R b y c) = T R a x (T B b y c)
-- balright (T B a x b) y bl = balance (T R a x b) y bl
-- balright (T R a x (T B b y c)) z bl = T R (balance (sub1 a) x b) y (T B c z bl)
--
-- sub1 :: RB a -> RB a
-- sub1 (T B a x b) = T R a x b
-- sub1 _ = error "invariance violation"
--
-- app :: RB a -> RB a -> RB a
-- app E x = x
-- app x E = x
-- app (T R a x b) (T R c y d) =
--  case app b c of
--      T R b' z c' -> T R (T R a x b') z (T R c' y d)
--      bc -> T R a x (T R bc y d)
-- app (T B a x b) (T B c y d) =
--  case app b c of
--      T R b' z c' -> T R(T B a x b') z (T B c' y d)
--      bc -> balleft a x (T B bc y d)
-- app a (T R b x c) = T R (app a b) x c
-- app (T R a x b) c = T R a x (app b c)