{-# LANGUAGE DataKinds,
             TypeOperators,
             ConstraintKinds,
             PolyKinds,
             TypeFamilies,
             GADTs,
             MultiParamTypeClasses,
             FunctionalDependencies,
             FlexibleInstances,
             FlexibleContexts,
             UndecidableInstances,
             UndecidableSuperClasses,
             TypeApplications,
             ScopedTypeVariables,
             AllowAmbiguousTypes,
             ExplicitForAll,
             RankNTypes, 
             DefaultSignatures,
             PartialTypeSignatures,
             LambdaCase,
             EmptyCase 
#-}
{-#  OPTIONS_GHC -Wno-partial-type-signatures  #-}

module Data.RBR.Demoted where

import Data.RBR.Internal

import           Data.Proxy
import           Data.Kind
import           Data.Typeable
import           GHC.TypeLits

emptyMap :: Map String TypeRep
emptyMap :: Map String TypeRep
emptyMap = Map String TypeRep
forall symbol q. Map symbol q
E

class DemotableColor (c :: Color) where
    demoteColor :: Proxy c -> Color

instance DemotableColor R where
    demoteColor :: Proxy 'R -> Color
demoteColor Proxy 'R
_ = Color
R

instance DemotableColor B where
    demoteColor :: Proxy 'B -> Color
demoteColor Proxy 'B
_ = Color
B

class DemotableMap (t :: Map Symbol Type) where
    demoteMap :: Proxy t -> Map String TypeRep

instance DemotableMap E where
    demoteMap :: Proxy 'E -> Map String TypeRep
demoteMap Proxy 'E
_ = Map String TypeRep
forall symbol q. Map symbol q
E

instance (DemotableColor c,
          KnownSymbol s,
          Typeable ty,
          DemotableMap l,
          DemotableMap r) 
          => DemotableMap (N c l s ty r) where
    demoteMap :: Proxy ('N c l s ty r) -> Map String TypeRep
demoteMap Proxy ('N c l s ty r)
_ = Color
-> Map String TypeRep
-> String
-> TypeRep
-> Map String TypeRep
-> Map String TypeRep
forall symbol q.
Color
-> Map symbol q -> symbol -> q -> Map symbol q -> Map symbol q
N (Proxy c -> Color
forall (c :: Color). DemotableColor c => Proxy c -> Color
demoteColor (forall {k} (t :: k). Proxy t
forall (t :: Color). Proxy t
Proxy @c)) 
                    (Proxy l -> Map String TypeRep
forall (t :: Map Symbol (*)).
DemotableMap t =>
Proxy t -> Map String TypeRep
demoteMap (forall {k} (t :: k). Proxy t
forall (t :: Map Symbol (*)). Proxy t
Proxy @l)) 
                    (Proxy s -> String
forall (n :: Symbol) (proxy :: Symbol -> *).
KnownSymbol n =>
proxy n -> String
symbolVal (forall {k} (t :: k). Proxy t
forall (t :: Symbol). Proxy t
Proxy @s)) 
                    (Proxy ty -> TypeRep
forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @ty)) 
                    (Proxy r -> Map String TypeRep
forall (t :: Map Symbol (*)).
DemotableMap t =>
Proxy t -> Map String TypeRep
demoteMap (forall {k} (t :: k). Proxy t
forall (t :: Map Symbol (*)). Proxy t
Proxy @r))

t_insert :: Ord a => a -> v -> Map a v -> Map a v
t_insert :: forall a v. Ord a => a -> v -> Map a v -> Map a v
t_insert a
x v
val Map a v
s =
    Color -> Map a v -> a -> v -> Map a v -> Map a v
forall symbol q.
Color
-> Map symbol q -> symbol -> q -> Map symbol q -> Map symbol q
N Color
B Map a v
a a
v v
z Map a v
b
    where
    N Color
_ Map a v
a a
v v
z Map a v
b = Map a v -> Map a v
ins Map a v
s
    ins :: Map a v -> Map a v
ins Map a v
E = Color -> Map a v -> a -> v -> Map a v -> Map a v
forall symbol q.
Color
-> Map symbol q -> symbol -> q -> Map symbol q -> Map symbol q
N Color
R Map a v
forall symbol q. Map symbol q
E a
x v
val Map a v
forall symbol q. Map symbol q
E
    ins s :: Map a v
s@(N Color
B Map a v
a a
y v
val' Map a v
b)
        | a
xa -> a -> Bool
forall a. Ord a => a -> a -> Bool
<a
y = Map a v -> a -> v -> Map a v -> Map a v
forall a v. Map a v -> a -> v -> Map a v -> Map a v
t_balance (Map a v -> Map a v
ins Map a v
a) a
y v
val' Map a v
b
        | a
xa -> a -> Bool
forall a. Ord a => a -> a -> Bool
>a
y = Map a v -> a -> v -> Map a v -> Map a v
forall a v. Map a v -> a -> v -> Map a v -> Map a v
t_balance Map a v
a a
y v
val' (Map a v -> Map a v
ins Map a v
b)
        | Bool
otherwise = Map a v
s
    ins s :: Map a v
s@(N Color
R Map a v
a a
y v
val' Map a v
b)
        | a
xa -> a -> Bool
forall a. Ord a => a -> a -> Bool
<a
y = Color -> Map a v -> a -> v -> Map a v -> Map a v
forall symbol q.
Color
-> Map symbol q -> symbol -> q -> Map symbol q -> Map symbol q
N Color
R (Map a v -> Map a v
ins Map a v
a) a
y v
val' Map a v
b
        | a
xa -> a -> Bool
forall a. Ord a => a -> a -> Bool
>a
y = Color -> Map a v -> a -> v -> Map a v -> Map a v
forall symbol q.
Color
-> Map symbol q -> symbol -> q -> Map symbol q -> Map symbol q
N Color
R Map a v
a a
y v
val' (Map a v -> Map a v
ins Map a v
b)
        | Bool
otherwise = Map a v
s

t_balance :: Map a v -> a -> v -> Map a v -> Map a v
t_balance :: forall a v. Map a v -> a -> v -> Map a v -> Map a v
t_balance (N Color
R Map a v
a a
x v
xv Map a v
b) a
y v
yv (N Color
R Map a v
c a
z v
zv Map a v
d) = Color -> Map a v -> a -> v -> Map a v -> Map a v
forall symbol q.
Color
-> Map symbol q -> symbol -> q -> Map symbol q -> Map symbol q
N Color
R (Color -> Map a v -> a -> v -> Map a v -> Map a v
forall symbol q.
Color
-> Map symbol q -> symbol -> q -> Map symbol q -> Map symbol q
N Color
B Map a v
a a
x v
xv Map a v
b) a
y v
yv (Color -> Map a v -> a -> v -> Map a v -> Map a v
forall symbol q.
Color
-> Map symbol q -> symbol -> q -> Map symbol q -> Map symbol q
N Color
B Map a v
c a
z v
zv Map a v
d)
t_balance (N Color
R (N Color
R Map a v
a a
x v
xv Map a v
b) a
y v
yv Map a v
c) a
z v
zv Map a v
d = Color -> Map a v -> a -> v -> Map a v -> Map a v
forall symbol q.
Color
-> Map symbol q -> symbol -> q -> Map symbol q -> Map symbol q
N Color
R (Color -> Map a v -> a -> v -> Map a v -> Map a v
forall symbol q.
Color
-> Map symbol q -> symbol -> q -> Map symbol q -> Map symbol q
N Color
B Map a v
a a
x v
xv Map a v
b) a
y v
yv (Color -> Map a v -> a -> v -> Map a v -> Map a v
forall symbol q.
Color
-> Map symbol q -> symbol -> q -> Map symbol q -> Map symbol q
N Color
B Map a v
c a
z v
zv Map a v
d)
t_balance (N Color
R Map a v
a a
x v
xv (N Color
R Map a v
b a
y v
yv Map a v
c)) a
z v
zv Map a v
d = Color -> Map a v -> a -> v -> Map a v -> Map a v
forall symbol q.
Color
-> Map symbol q -> symbol -> q -> Map symbol q -> Map symbol q
N Color
R (Color -> Map a v -> a -> v -> Map a v -> Map a v
forall symbol q.
Color
-> Map symbol q -> symbol -> q -> Map symbol q -> Map symbol q
N Color
B Map a v
a a
x v
xv Map a v
b) a
y v
yv (Color -> Map a v -> a -> v -> Map a v -> Map a v
forall symbol q.
Color
-> Map symbol q -> symbol -> q -> Map symbol q -> Map symbol q
N Color
B Map a v
c a
z v
zv Map a v
d)
t_balance Map a v
a a
x v
xv (N Color
R Map a v
b a
y v
yv (N Color
R Map a v
c a
z v
zv Map a v
d)) = Color -> Map a v -> a -> v -> Map a v -> Map a v
forall symbol q.
Color
-> Map symbol q -> symbol -> q -> Map symbol q -> Map symbol q
N Color
R (Color -> Map a v -> a -> v -> Map a v -> Map a v
forall symbol q.
Color
-> Map symbol q -> symbol -> q -> Map symbol q -> Map symbol q
N Color
B Map a v
a a
x v
xv Map a v
b) a
y v
yv (Color -> Map a v -> a -> v -> Map a v -> Map a v
forall symbol q.
Color
-> Map symbol q -> symbol -> q -> Map symbol q -> Map symbol q
N Color
B Map a v
c a
z v
zv Map a v
d)
t_balance Map a v
a a
x v
xv (N Color
R (N Color
R Map a v
b a
y v
yv Map a v
c) a
z v
zv Map a v
d) = Color -> Map a v -> a -> v -> Map a v -> Map a v
forall symbol q.
Color
-> Map symbol q -> symbol -> q -> Map symbol q -> Map symbol q
N Color
R (Color -> Map a v -> a -> v -> Map a v -> Map a v
forall symbol q.
Color
-> Map symbol q -> symbol -> q -> Map symbol q -> Map symbol q
N Color
B Map a v
a a
x v
xv Map a v
b) a
y v
yv (Color -> Map a v -> a -> v -> Map a v -> Map a v
forall symbol q.
Color
-> Map symbol q -> symbol -> q -> Map symbol q -> Map symbol q
N Color
B Map a v
c a
z v
zv Map a v
d)
t_balance Map a v
a a
x v
xv Map a v
b = Color -> Map a v -> a -> v -> Map a v -> Map a v
forall symbol q.
Color
-> Map symbol q -> symbol -> q -> Map symbol q -> Map symbol q
N Color
B Map a v
a a
x v
xv Map a v
b


t_delete :: Ord a => a -> Map a v -> Map a v
t_delete :: forall a v. Ord a => a -> Map a v -> Map a v
t_delete a
x Map a v
t =
 case Map a v -> Map a v
del Map a v
t of {N Color
_ Map a v
a a
y v
yv Map a v
b -> Color -> Map a v -> a -> v -> Map a v -> Map a v
forall symbol q.
Color
-> Map symbol q -> symbol -> q -> Map symbol q -> Map symbol q
N Color
B Map a v
a a
y v
yv Map a v
b; Map a v
_ -> Map a v
forall symbol q. Map symbol q
E}
 where
 del :: Map a v -> Map a v
del Map a v
E = Map a v
forall symbol q. Map symbol q
E
 del (N Color
_ Map a v
a a
y v
yv Map a v
b)
     | a
xa -> a -> Bool
forall a. Ord a => a -> a -> Bool
<a
y = Map a v -> a -> v -> Map a v -> Map a v
delformLeft Map a v
a a
y v
yv Map a v
b
     | a
xa -> a -> Bool
forall a. Ord a => a -> a -> Bool
>a
y = Map a v -> a -> v -> Map a v -> Map a v
delformRight Map a v
a a
y v
yv Map a v
b
     | Bool
otherwise = Map a v -> Map a v -> Map a v
forall a v. Map a v -> Map a v -> Map a v
t_app Map a v
a Map a v
b
 delformLeft :: Map a v -> a -> v -> Map a v -> Map a v
delformLeft a :: Map a v
a@(N Color
B Map a v
_ a
_ v
_ Map a v
_) a
y v
yv Map a v
b = Map a v -> a -> v -> Map a v -> Map a v
forall a v. Map a v -> a -> v -> Map a v -> Map a v
t_balleft (Map a v -> Map a v
del Map a v
a) a
y v
yv Map a v
b
 delformLeft Map a v
a a
y v
yv Map a v
b = Color -> Map a v -> a -> v -> Map a v -> Map a v
forall symbol q.
Color
-> Map symbol q -> symbol -> q -> Map symbol q -> Map symbol q
N Color
R (Map a v -> Map a v
del Map a v
a) a
y v
yv Map a v
b

 delformRight :: Map a v -> a -> v -> Map a v -> Map a v
delformRight Map a v
a a
y v
yv b :: Map a v
b@(N Color
B Map a v
_ a
_ v
_ Map a v
_) = Map a v -> a -> v -> Map a v -> Map a v
forall a v. Map a v -> a -> v -> Map a v -> Map a v
t_balright Map a v
a a
y v
yv (Map a v -> Map a v
del Map a v
b)
 delformRight Map a v
a a
y v
yv Map a v
b = Color -> Map a v -> a -> v -> Map a v -> Map a v
forall symbol q.
Color
-> Map symbol q -> symbol -> q -> Map symbol q -> Map symbol q
N Color
R Map a v
a a
y v
yv (Map a v -> Map a v
del Map a v
b)

t_balleft :: Map a v -> a -> v -> Map a v -> Map a v
t_balleft :: forall a v. Map a v -> a -> v -> Map a v -> Map a v
t_balleft (N Color
R Map a v
a a
x v
xv Map a v
b) a
y v
yv Map a v
c = Color -> Map a v -> a -> v -> Map a v -> Map a v
forall symbol q.
Color
-> Map symbol q -> symbol -> q -> Map symbol q -> Map symbol q
N Color
R (Color -> Map a v -> a -> v -> Map a v -> Map a v
forall symbol q.
Color
-> Map symbol q -> symbol -> q -> Map symbol q -> Map symbol q
N Color
B Map a v
a a
x v
xv Map a v
b) a
y v
yv Map a v
c
t_balleft Map a v
bl a
x v
xv (N Color
B Map a v
a a
y v
yv Map a v
b) = Map a v -> a -> v -> Map a v -> Map a v
forall a v. Map a v -> a -> v -> Map a v -> Map a v
t_balance Map a v
bl a
x v
xv (Color -> Map a v -> a -> v -> Map a v -> Map a v
forall symbol q.
Color
-> Map symbol q -> symbol -> q -> Map symbol q -> Map symbol q
N Color
R Map a v
a a
y v
yv Map a v
b)
t_balleft Map a v
bl a
x v
xv (N Color
R (N Color
B Map a v
a a
y v
yv Map a v
b) a
z v
zv Map a v
c) = Color -> Map a v -> a -> v -> Map a v -> Map a v
forall symbol q.
Color
-> Map symbol q -> symbol -> q -> Map symbol q -> Map symbol q
N Color
R (Color -> Map a v -> a -> v -> Map a v -> Map a v
forall symbol q.
Color
-> Map symbol q -> symbol -> q -> Map symbol q -> Map symbol q
N Color
B Map a v
bl a
x v
xv Map a v
a) a
y v
yv (Map a v -> a -> v -> Map a v -> Map a v
forall a v. Map a v -> a -> v -> Map a v -> Map a v
t_balance Map a v
b a
z v
zv (Map a v -> Map a v
forall a v. Map a v -> Map a v
t_sub1 Map a v
c))

t_balright :: Map a v -> a -> v -> Map a v -> Map a v
t_balright :: forall a v. Map a v -> a -> v -> Map a v -> Map a v
t_balright Map a v
a a
x v
xv (N Color
R Map a v
b a
y v
yv Map a v
c) = Color -> Map a v -> a -> v -> Map a v -> Map a v
forall symbol q.
Color
-> Map symbol q -> symbol -> q -> Map symbol q -> Map symbol q
N Color
R Map a v
a a
x v
xv (Color -> Map a v -> a -> v -> Map a v -> Map a v
forall symbol q.
Color
-> Map symbol q -> symbol -> q -> Map symbol q -> Map symbol q
N Color
B Map a v
b a
y v
yv Map a v
c)
t_balright (N Color
B Map a v
a a
x v
xv Map a v
b) a
y v
yv Map a v
bl = Map a v -> a -> v -> Map a v -> Map a v
forall a v. Map a v -> a -> v -> Map a v -> Map a v
t_balance (Color -> Map a v -> a -> v -> Map a v -> Map a v
forall symbol q.
Color
-> Map symbol q -> symbol -> q -> Map symbol q -> Map symbol q
N Color
R Map a v
a a
x v
xv Map a v
b) a
y v
yv Map a v
bl
t_balright (N Color
R Map a v
a a
x v
xv (N Color
B Map a v
b a
y v
yv Map a v
c)) a
z v
zv Map a v
bl = Color -> Map a v -> a -> v -> Map a v -> Map a v
forall symbol q.
Color
-> Map symbol q -> symbol -> q -> Map symbol q -> Map symbol q
N Color
R (Map a v -> a -> v -> Map a v -> Map a v
forall a v. Map a v -> a -> v -> Map a v -> Map a v
t_balance (Map a v -> Map a v
forall a v. Map a v -> Map a v
t_sub1 Map a v
a) a
x v
xv Map a v
b) a
y v
yv (Color -> Map a v -> a -> v -> Map a v -> Map a v
forall symbol q.
Color
-> Map symbol q -> symbol -> q -> Map symbol q -> Map symbol q
N Color
B Map a v
c a
z v
zv Map a v
bl)

t_sub1 :: Map a v -> Map a v
t_sub1 :: forall a v. Map a v -> Map a v
t_sub1 (N Color
B Map a v
a a
x v
xv Map a v
b) = Color -> Map a v -> a -> v -> Map a v -> Map a v
forall symbol q.
Color
-> Map symbol q -> symbol -> q -> Map symbol q -> Map symbol q
N Color
R Map a v
a a
x v
xv Map a v
b
t_sub1 Map a v
_ = String -> Map a v
forall a. HasCallStack => String -> a
error String
"invariance violation"

t_app :: Map a v -> Map a v -> Map a v
t_app :: forall a v. Map a v -> Map a v -> Map a v
t_app Map a v
E Map a v
x = Map a v
x
t_app Map a v
x Map a v
E = Map a v
x
t_app (N Color
R Map a v
a a
x v
xv Map a v
b) (N Color
R Map a v
c a
y v
yv Map a v
d) =
 case Map a v -> Map a v -> Map a v
forall a v. Map a v -> Map a v -> Map a v
t_app Map a v
b Map a v
c of
     N Color
R Map a v
b' a
z v
zv Map a v
c' -> Color -> Map a v -> a -> v -> Map a v -> Map a v
forall symbol q.
Color
-> Map symbol q -> symbol -> q -> Map symbol q -> Map symbol q
N Color
R (Color -> Map a v -> a -> v -> Map a v -> Map a v
forall symbol q.
Color
-> Map symbol q -> symbol -> q -> Map symbol q -> Map symbol q
N Color
R Map a v
a a
x v
xv Map a v
b') a
z v
zv (Color -> Map a v -> a -> v -> Map a v -> Map a v
forall symbol q.
Color
-> Map symbol q -> symbol -> q -> Map symbol q -> Map symbol q
N Color
R Map a v
c' a
y v
yv Map a v
d)
     Map a v
bc -> Color -> Map a v -> a -> v -> Map a v -> Map a v
forall symbol q.
Color
-> Map symbol q -> symbol -> q -> Map symbol q -> Map symbol q
N Color
R Map a v
a a
x v
xv (Color -> Map a v -> a -> v -> Map a v -> Map a v
forall symbol q.
Color
-> Map symbol q -> symbol -> q -> Map symbol q -> Map symbol q
N Color
R Map a v
bc a
y v
yv Map a v
d)
t_app (N Color
B Map a v
a a
x v
xv Map a v
b) (N Color
B Map a v
c a
y v
yv Map a v
d) = 
 case Map a v -> Map a v -> Map a v
forall a v. Map a v -> Map a v -> Map a v
t_app Map a v
b Map a v
c of
     N Color
R Map a v
b' a
z v
zv Map a v
c' -> Color -> Map a v -> a -> v -> Map a v -> Map a v
forall symbol q.
Color
-> Map symbol q -> symbol -> q -> Map symbol q -> Map symbol q
N Color
R (Color -> Map a v -> a -> v -> Map a v -> Map a v
forall symbol q.
Color
-> Map symbol q -> symbol -> q -> Map symbol q -> Map symbol q
N Color
B Map a v
a a
x v
xv Map a v
b') a
z v
zv (Color -> Map a v -> a -> v -> Map a v -> Map a v
forall symbol q.
Color
-> Map symbol q -> symbol -> q -> Map symbol q -> Map symbol q
N Color
B Map a v
c' a
y v
yv Map a v
d)
     Map a v
bc -> Map a v -> a -> v -> Map a v -> Map a v
forall a v. Map a v -> a -> v -> Map a v -> Map a v
t_balleft Map a v
a a
x v
xv (Color -> Map a v -> a -> v -> Map a v -> Map a v
forall symbol q.
Color
-> Map symbol q -> symbol -> q -> Map symbol q -> Map symbol q
N Color
B Map a v
bc a
y v
yv Map a v
d)
t_app Map a v
a (N Color
R Map a v
b a
x v
xv Map a v
c) = Color -> Map a v -> a -> v -> Map a v -> Map a v
forall symbol q.
Color
-> Map symbol q -> symbol -> q -> Map symbol q -> Map symbol q
N Color
R (Map a v -> Map a v -> Map a v
forall a v. Map a v -> Map a v -> Map a v
t_app Map a v
a Map a v
b) a
x v
xv Map a v
c
t_app (N Color
R Map a v
a a
x v
xv Map a v
b) Map a v
c = Color -> Map a v -> a -> v -> Map a v -> Map a v
forall symbol q.
Color
-> Map symbol q -> symbol -> q -> Map symbol q -> Map symbol q
N Color
R Map a v
a a
x v
xv (Map a v -> Map a v -> Map a v
forall a v. Map a v -> Map a v -> Map a v
t_app Map a v
b Map a v
c)

-- 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)