module Type.BST.List (
List(Nil, Cons), (.:.)
, Length
, MergeableL(MergeL, mergeL, MergeEL, mergeEL)
, Sortable(Sort, sort)
) where
import GHC.TypeLits
import Type.BST.Proxy
import Type.BST.Item
import Type.BST.Compare
data family List (as :: [*])
data instance List '[] = Nil
data instance List (a ': as) = Cons a (List as)
(.:.) :: a -> List as -> List (a ': as)
(.:.) = Cons
infixr 5 `Cons`, .:.
instance Show (List '[]) where
show _ = "[]"
instance (Show a, Showlist (List as)) => Show (List (a ': as)) where
show (x `Cons` xs) = "[" ++ show x ++ showlist xs
class Showlist (a :: *) where
showlist :: a -> String
instance Showlist (List '[]) where
showlist _ = "]"
instance (Show a, Showlist (List as)) => Showlist (List (a ': as)) where
showlist (x `Cons` xs) = "," ++ show x ++ showlist xs
data family ListList (ass :: [[*]])
data instance ListList (as ': ass) = ConsCons (List as) (ListList ass)
data instance ListList '[] = NilNil
(.::.) :: List as -> ListList ass -> ListList (as ': ass)
(.::.) = ConsCons
infixr 5 `ConsCons`, .::.
type family Length (as :: [*]) :: Nat
type instance Length '[] = 0
type instance Length (_' ': as) = 1 + Length as
class MergeableL (as :: [*]) (bs :: [*]) where
type MergeL as bs :: [*]
mergeL :: List as -> List bs -> List (MergeL as bs)
type MergeEL as bs :: [*]
mergeEL :: List as -> List bs -> List (MergeEL as bs)
instance MergeableL '[] bs where
type MergeL '[] bs = bs
mergeL _ ys = ys
type MergeEL '[] bs = bs
mergeEL _ ys = ys
instance MergeableL (a ': as) '[] where
type MergeL (a ': as) '[] = a ': as
mergeL xs _ = xs
type MergeEL (a ': as) '[] = a ': as
mergeEL xs _ = xs
instance MergeableL' (Compare a b) (a ': as) (b ': bs) => MergeableL (a ': as) (b ': bs) where
type MergeL (a ': as) (b ': bs) = MergeL' (Compare a b) (a ': as) (b ': bs)
mergeL = mergeL' (Proxy :: Proxy (Compare a b))
type MergeEL (a ': as) (b ': bs) = MergeEL' (Compare a b) (a ': as) (b ': bs)
mergeEL = mergeEL' (Proxy :: Proxy (Compare a b))
class MergeableL' (o :: Ordering) (as :: [*]) (bs :: [*]) where
type MergeL' o as bs :: [*]
mergeL' :: Proxy o -> List as -> List bs -> List (MergeL' o as bs)
type MergeEL' o as bs :: [*]
mergeEL' :: Proxy o -> List as -> List bs -> List (MergeEL' o as bs)
instance MergeableL as bs => MergeableL' EQ (Item key a ': as) (Item key b ': bs) where
type MergeL' EQ (Item key a ': as) (Item key b ': bs) = Item key a ': MergeL as bs
mergeL' _ (Cons x xs) (Cons _ ys) = Cons x (mergeL xs ys)
type MergeEL' EQ (Item key a ': as) (Item key b ': bs) = Item key (a, b) ': MergeEL as bs
mergeEL' _ (Cons (Item x) xs) (Cons (Item y) ys) = Cons ((Item :: With key) (x, y)) (mergeEL xs ys)
instance MergeableL as bs => MergeableL' LT (a ': as) bs where
type MergeL' LT (a ': as) bs = a ': MergeL as bs
mergeL' _ (Cons x xs) ys = Cons x (mergeL xs ys)
type MergeEL' LT (a ': as) bs = a ': MergeEL as bs
mergeEL' _ (Cons x xs) ys = Cons x (mergeEL xs ys)
instance MergeableL as bs => MergeableL' GT as (b ': bs) where
type MergeL' GT as (b ': bs) = b ': MergeL as bs
mergeL' _ xs (Cons y ys) = Cons y (mergeL xs ys)
type MergeEL' GT as (b ': bs) = b ': MergeEL as bs
mergeEL' _ xs (Cons y ys) = Cons y (mergeEL xs ys)
class Revappable (as :: [*]) (bs :: [*]) where
type Revapp as bs :: [*]
revapp :: List as -> List bs -> List (Revapp as bs)
instance Revappable '[] bs where
type Revapp '[] bs = bs
revapp _ ys = ys
instance Revappable as (a ': bs) => Revappable (a ': as) bs where
type Revapp (a ': as) bs = Revapp as (a ': bs)
revapp (Cons x xs) ys = revapp xs (x .:. ys)
class Sortable (as :: [*]) where
type Sort as :: [*]
sort :: Sortable as => List as -> List (Sort as)
instance (Sequencesable as, Mergeallable (Sequences as)) => Sortable as where
type Sort as = Mergeall (Sequences as)
sort = mergeall . sequences
class Sequencesable (as :: [*]) where
type Sequences as :: [[*]]
sequences :: List as -> ListList (Sequences as)
instance Sequencesable '[] where
type Sequences '[] = '[ '[] ]
sequences xs = xs .::. NilNil
instance Sequencesable '[a] where
type Sequences '[a] = '[ '[a] ]
sequences xs = xs .::. NilNil
instance Sequencesable' (Compare a b) (a ': b ': cs) => Sequencesable (a ': b ': cs) where
type Sequences (a ': b ': cs) = Sequences' (Compare a b) (a ': b ': cs)
sequences xs = sequences' (Proxy :: Proxy (Compare a b)) xs
class Sequencesable' (o :: Ordering) (as :: [*]) where
type Sequences' o as :: [[*]]
sequences' :: Proxy o -> List as -> ListList (Sequences' o as)
instance Sequencesable (a ': cs) => Sequencesable' EQ (a ': _' ': cs) where
type Sequences' EQ (a ': _' ': cs) = Sequences (a ': cs)
sequences' _ (x `Cons` _ `Cons` zs) = sequences (x .:. zs)
instance Ascendingable b '[a] cs => Sequencesable' LT (a ': b ': cs) where
type Sequences' LT (a ': b ': cs) = Ascending b '[a] cs
sequences' _ (x `Cons` y `Cons` zs) = ascending y (x .:. Nil) zs
instance Descendingable b '[a] cs => Sequencesable' GT (a ': b ': cs) where
type Sequences' GT (a ': b ': cs) = Descending b '[a] cs
sequences' _ (x `Cons` y `Cons` zs) = descending y (x .:. Nil) zs
class Descendingable (a :: *) (as :: [*]) (bs :: [*]) where
type Descending a as bs :: [[*]]
descending :: a -> List as -> List bs -> ListList (Descending a as bs)
instance Revappable as '[a] => Descendingable a as '[] where
type Descending a as '[] = (a ': as) ': Sequences '[]
descending x xs ys = (x .:. xs) .::. sequences ys
instance Descendingable' (Compare a b) a as (b ': bs) => Descendingable a as (b ': bs) where
type Descending a as (b ': bs) = Descending' (Compare a b) a as (b ': bs)
descending x xs ys = descending' (Proxy :: Proxy (Compare a b)) x xs ys
class Descendingable' (o :: Ordering) (a :: *) (as :: [*]) (bs :: [*]) where
type Descending' o a as bs :: [[*]]
descending' :: Proxy o -> a -> List as -> List bs -> ListList (Descending' o a as bs)
instance Descendingable a as bs => Descendingable' EQ a as (_' ': bs) where
type Descending' EQ a as (_' ': bs) = Descending a as bs
descending' _ x xs (Cons _ ys) = descending x xs ys
instance Sequencesable bs => Descendingable' LT a as bs where
type Descending' LT a as bs = (a ': as) ': Sequences bs
descending' _ x xs ys = (x .:. xs) .::. sequences ys
instance Descendingable b (a ': as) bs => Descendingable' GT a as (b ': bs) where
type Descending' GT a as (b ': bs) = Descending b (a ': as) bs
descending' _ x xs (Cons y ys) = descending y (x .:. xs) ys
class Ascendingable (a :: *) (as :: [*]) (bs :: [*]) where
type Ascending a as bs :: [[*]]
ascending :: a -> List as -> List bs -> ListList (Ascending a as bs)
instance Revappable as '[a] => Ascendingable a as '[] where
type Ascending a as '[] = Revapp as '[a] ': Sequences '[]
ascending x xs ys = revapp xs (x .:. Nil) .::. sequences ys
instance Ascendingable' (Compare a b) a as (b ': bs) => Ascendingable a as (b ': bs) where
type Ascending a as (b ': bs) = Ascending' (Compare a b) a as (b ': bs)
ascending x xs ys = ascending' (Proxy :: Proxy (Compare a b)) x xs ys
class Ascendingable' (o :: Ordering) (a :: *) (as :: [*]) (bs :: [*]) where
type Ascending' o a as bs :: [[*]]
ascending' :: Proxy o -> a -> List as -> List bs -> ListList (Ascending' o a as bs)
instance Ascendingable b (a ': as) bs => Ascendingable' LT a as (b ': bs) where
type Ascending' LT a as (b ': bs) = Ascending b (a ': as) bs
ascending' _ x xs (Cons y ys) = ascending y (x .:. xs) ys
instance Ascendingable a as bs => Ascendingable' EQ a as (_' ': bs) where
type Ascending' EQ a as (_' ': bs) = Ascending a as bs
ascending' _ x xs (Cons _ ys) = ascending x xs ys
instance (Revappable as '[a], Sequencesable bs) => Ascendingable' GT a as bs where
type Ascending' GT a as bs = Revapp as '[a] ': Sequences bs
ascending' _ x xs ys = revapp xs (x .:. Nil) .::. sequences ys
class Mergeallable (ass :: [[*]]) where
type Mergeall ass :: [*]
mergeall :: ListList ass -> List (Mergeall ass)
instance Mergeallable '[as] where
type Mergeall '[as] = as
mergeall (ConsCons xs _) = xs
instance (Mergepairsable (as ': bs ': css), Mergeallable (Mergepairs (as ': bs ': css))) => Mergeallable (as ': bs ': css) where
type Mergeall (as ': bs ': css) = Mergeall (Mergepairs (as ': bs ': css))
mergeall xss = mergeall (mergepairs xss)
class Mergepairsable ass where
type Mergepairs ass :: [[*]]
mergepairs :: ListList ass -> ListList (Mergepairs ass)
instance Mergepairsable '[] where
type Mergepairs '[] = '[]
mergepairs xss = xss
instance Mergepairsable '[as] where
type Mergepairs '[as] = '[as]
mergepairs xss = xss
instance (MergeableL as bs, Mergepairsable css) => Mergepairsable (as ': bs ': css) where
type Mergepairs (as ': bs ': css) = MergeL as bs ': Mergepairs css
mergepairs (xs `ConsCons` ys `ConsCons` zss) = mergeL xs ys .::. mergepairs zss