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