{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE CPP #-}
#if MIN_VERSION_base(4, 12, 0)
{-# LANGUAGE NoStarIsType #-}
#endif
module SuperRecord.Sort
( FieldListSort
)
where
import SuperRecord.Field
import Data.Kind (Type)
import Data.Proxy
import GHC.TypeLits
type family HalfOfHelper (n :: Nat) (i :: Nat) (dist :: Nat) (o :: Ordering) :: Nat where
HalfOfHelper n m dist 'GT = m - 1
HalfOfHelper n m dist 'EQ = m
HalfOfHelper n m 1 'LT = m
HalfOfHelper n m dist 'LT = HalfOfHelper n (m + 2) (n - ((m + 2) * 2)) (CmpNat ((m + 2) * 2) n)
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 8 = 4
HalfOf 9 = 4
HalfOf 10 = 5
HalfOf n = HalfOfHelper n 0 n 'LT
type family LengthOf (xs :: [k]) :: Nat where
LengthOf '[] = 0
LengthOf (x ': xs) = 1 + LengthOf xs
type family ListTake (xs :: [k]) (n :: Nat) :: [k] where
ListTake '[] n = '[]
ListTake xs 0 = '[]
ListTake (x ': xs) n = (x ': ListTake xs (n - 1))
type family ListDrop (xs :: [k]) (n :: Nat) :: [k] where
ListDrop '[] n = '[]
ListDrop xs 0 = xs
ListDrop (x ': xs) n = ListDrop xs (n - 1)
type family FieldListMergeHelper (xs :: [Type]) (ys :: [Type]) (o :: Ordering) :: [Type] where
FieldListMergeHelper (x := xv ': xs) (y := yv ': ys) 'GT =
(y := yv) ': FieldListMerge (x := xv ': xs) ys
FieldListMergeHelper (x := xv ': xs) (y := yv ': ys) leq =
(x := xv) ': FieldListMerge xs (y := yv ': ys)
type family FieldListMerge (xs :: [Type]) (ys :: [Type]) :: [Type] where
FieldListMerge xs '[] = xs
FieldListMerge '[] ys = ys
FieldListMerge (x := xv ': xs) (y := yv ': ys) =
FieldListMergeHelper (x := xv ': xs) (y := yv ': ys) (CmpSymbol x y)
type family ListSortStep (xs :: [Type]) (halfLen :: Nat) :: [Type] where
ListSortStep xs halfLen =
FieldListMerge
(FieldListSort (ListTake xs halfLen))
(FieldListSort (ListDrop xs halfLen))
type family FieldListSort (xs :: [Type]) :: [Type] where
FieldListSort '[] = '[]
FieldListSort '[x] = '[x]
FieldListSort '[x, y] = FieldListMerge '[x] '[y]
FieldListSort xs =
ListSortStep xs (HalfOf (LengthOf xs))
_testDrop2 :: ( ListDrop '[1, 2, 3, 4] 2 ~ x, x ~ '[3, 4] ) => Proxy x
_testDrop2 = Proxy
_testLengthOf :: ( LengthOf '[1, 2, 3, 4] ~ x, x ~ 4 ) => Proxy x
_testLengthOf = Proxy
_testHalfOf :: ( HalfOf 0 ~ x, x ~ 0 ) => Proxy x
_testHalfOf = Proxy
_testHalfOf1 :: ( HalfOf 1 ~ x, x ~ 1 ) => Proxy x
_testHalfOf1 = Proxy
_testHalfOf2 :: ( HalfOf 2 ~ x, x ~ 1 ) => Proxy x
_testHalfOf2 = Proxy
_testHalfOf3 :: ( HalfOf 3 ~ x, x ~ 1 ) => Proxy x
_testHalfOf3 = Proxy
_testHalfOf4 :: ( HalfOf 4 ~ x, x ~ 2 ) => Proxy x
_testHalfOf4 = Proxy
_testHalfOf99 :: ( HalfOf 99 ~ x, x ~ 49 ) => Proxy x
_testHalfOf99 = Proxy
_testHalfOf100 :: ( HalfOf 100 ~ x, x ~ 50 ) => Proxy x
_testHalfOf100 = Proxy
_testHalfOf101 :: ( HalfOf 101 ~ x, x ~ 50 ) => Proxy x
_testHalfOf101 = Proxy
_testHalfOf200 :: ( HalfOf 200 ~ x, x ~ 100 ) => Proxy x
_testHalfOf200 = Proxy
_testHalfOf400 :: ( HalfOf 400 ~ x, x ~ 200 ) => Proxy x
_testHalfOf400 = Proxy
_testHalfOf401 :: ( HalfOf 401 ~ x, x ~ 200 ) => Proxy x
_testHalfOf401 = Proxy
_testHalfOf793 :: ( HalfOf 793 ~ x, x ~ 396 ) => Proxy x
_testHalfOf793 = Proxy
_testSort0 ::
( FieldListSort '[] ~ x
, x ~ '[]
) => Proxy x
_testSort0 = Proxy
_testSort1 ::
( FieldListSort '["test" := Int] ~ x
, x ~ '["test" := Int]
) => Proxy x
_testSort1 = Proxy
_testSort2 ::
( FieldListSort '["test" := Int, "abc" := String] ~ x
, x ~ '["abc" := String, "test" := Int]
) => Proxy x
_testSort2 = Proxy
_testSort3 ::
( FieldListSort '["test" := Int, "abc" := String, "def" := String] ~ x
, x ~ '["abc" := String, "def" := String, "test" := Int]
) => Proxy x
_testSort3 = Proxy