{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE NoStarIsType #-}
{-# OPTIONS_HADDOCK prune not-home #-}
module System.TmpProc.TypeLevel.Sort (
SortSymbols,
Take,
Drop,
LengthOf,
HalfOf,
) where
import GHC.TypeLits (
CmpNat,
CmpSymbol,
Nat,
Symbol,
type (*),
type (+),
type (-),
)
type family Take (xs :: [k]) (n :: Nat) :: [k] where
Take '[] n = '[]
Take xs 0 = '[]
Take (x ': xs) n = (x ': Take xs (n - 1))
type family Drop (xs :: [k]) (n :: Nat) :: [k] where
Drop '[] n = '[]
Drop xs 0 = xs
Drop (x ': xs) n = Drop xs (n - 1)
type family LengthOf (xs :: [k]) :: Nat where
LengthOf '[] = 0
LengthOf (x ': xs) = 1 + LengthOf xs
type family HalfOf (n :: Nat) :: Nat where
HalfOf 0 = 0
HalfOf 1 = 1
HalfOf 2 = 1
HalfOf 3 = 1
HalfOf 4 = 2
HalfOf 5 = 2
HalfOf 6 = 3
HalfOf 7 = 3
HalfOf n = HalfOfImpl n 0 n 'LT
type family HalfOfImpl (n :: Nat) (i :: Nat) (dist :: Nat) (o :: Ordering) :: Nat where
HalfOfImpl n m dist 'GT = m - 1
HalfOfImpl n m dist 'EQ = m
HalfOfImpl n m 1 'LT = m
HalfOfImpl n m dist 'LT = HalfOfImpl n (m + 2) (n - ((m + 2) * 2)) (CmpNat ((m + 2) * 2) n)
type family SortSymbols (xs :: [Symbol]) :: [Symbol] where
SortSymbols '[] = '[]
SortSymbols '[x] = '[x]
SortSymbols '[x, y] = MergeSymbols '[x] '[y]
SortSymbols xs = SortSymbolsStep xs (HalfOf (LengthOf xs))
type family SortSymbolsStep (xs :: [Symbol]) (halfLen :: Nat) :: [Symbol] where
SortSymbolsStep xs halfLen =
MergeSymbols
(SortSymbols (Take xs halfLen))
(SortSymbols (Drop xs halfLen))
type family MergeSymbols (xs :: [Symbol]) (ys :: [Symbol]) :: [Symbol] where
MergeSymbols xs '[] = xs
MergeSymbols '[] ys = ys
MergeSymbols (x ': xs) (y ': ys) = MergeSymbolsImpl (x ': xs) (y ': ys) (CmpSymbol x y)
type family MergeSymbolsImpl (xs :: [Symbol]) (ys :: [Symbol]) (o :: Ordering) :: [Symbol] where
MergeSymbolsImpl (x ': xs) (y ': ys) 'GT = y ': MergeSymbols (x ': xs) ys
MergeSymbolsImpl (x ': xs) (y ': ys) leq = x ': MergeSymbols xs (y ': ys)