{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FlexibleInstances #-}
module Type.RBSet
(
TypeSet (..)
, Empty
, Member
, Insertable(Insert)
, InsertAll
, FromList
, Removable(Remove)
, Merge
) where
import Type.Compare
import GHC.TypeLits
data Color = R
| B
deriving (Show,Eq)
data TypeSet a = E
| N Color (TypeSet a) a (TypeSet a)
deriving (Show,Eq)
type Empty = E
type family InsertAll (es :: [k]) (t :: TypeSet k) :: TypeSet k where
InsertAll '[] t = t
InsertAll ( v ': es ) t = Insert v (InsertAll es t)
type FromList (es :: [k]) = InsertAll es Empty
class Insertable (k :: ki) (t :: TypeSet ki) where
type Insert k t :: TypeSet ki
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
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
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
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
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)
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
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
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)
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)
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)
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)
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)
instance BalanceableHelper DoNotBalance a k b where
type Balance' DoNotBalance a k b = N B a k b
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
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))
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
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)
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)
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))
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
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))
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
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)
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
instance Fuseable E (N color left k right) where
type Fuse E (N color left k right) = N color left k right
instance Fuseable (N color left k right) E where
type Fuse (N color left k right) E = N color left k right
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
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))
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
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)
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)
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)
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)
class FuseableHelper2 (fused :: TypeSet ki) (l :: TypeSet ki) (r :: TypeSet ki) where
type Fuse2 fused l r :: TypeSet ki
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)
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)
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)
class Delable (k :: ki) (t :: TypeSet ki) where
type Del k t :: TypeSet ki
class DelableL (k :: ki) (l :: TypeSet ki) (kx :: ki) (r :: TypeSet ki) where
type DelL k l kx r :: TypeSet ki
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
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
instance DelableL k E kx right where
type DelL k E kx right = N R E kx right
class DelableR (k :: ki) (l :: TypeSet ki) (kx :: ki) (r :: TypeSet ki) where
type DelR k l kx r :: TypeSet ki
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))
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))
instance DelableR k left kx E where
type DelR k left kx E = N R left kx E
instance Delable k E where
type Del k E = E
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
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
instance Fuseable left right => DelableHelper EQ k left k right where
type Del' EQ k left k right = Fuse left right
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
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)