content: {-# 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
      -- some optimizations for faster compilation
      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
      -- the general case
      HalfOf n = HalfOfHelper n 0 n 'LT -- usually (CmpNat 0 n), but 0 ist already handled!
  
  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))
  
  -- | Sort a list of fields using merge sort
  type family FieldListSort (xs :: [Type]) :: [Type] where
      FieldListSort '[] = '[]
      FieldListSort '[x] = '[x]
      FieldListSort '[x, y] = FieldListMerge '[x] '[y] -- not needed, just an optimization
      FieldListSort xs =
          ListSortStep xs (HalfOf (LengthOf xs))
  
  -- Some type level tests. These will produce an "overlapping patterns" warning when failing
  
  _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
  