{-# LANGUAGE CPP #-}
{- | Description: sorting

Benchmarks for these functions can be found at
<http://code.haskell.org/~aavogt/HList-nodup/Run.html>.

See <Data-HList-CommonMain.html#v:hSort>
for the public interface.

-}
module Data.HList.HSort where

import Data.HList.HList
import Data.HList.FakePrelude
import Data.HList.Label3

#if __GLASGOW_HASKELL__ > 707
import GHC.TypeLits (type (<=?), CmpSymbol)
-- | only in ghc >= 7.7
instance ((x <=? y) ~ b) => HEqBy HLeFn x y b
-- | only in ghc >= 7.7

{- |

>>> let b1 = Proxy :: HEqBy HLeFn "x" "y" b => Proxy b
>>> :t b1
b1 :: Proxy 'True

>>> let b2 = Proxy :: HEqBy HLeFn "x" "x" b => Proxy b
>>> :t b2
b2 :: Proxy 'True

>>> let b3 = Proxy :: HEqBy HLeFn "y" "x" b => Proxy b
>>> :t b3
b3 :: Proxy 'False

-}
instance (HEq (CmpSymbol x y) GT nb, HNot nb ~ b) => HEqBy HLeFn x y b
#endif

-- | the \"standard\" '<=' for types. Reuses 'HEqBy'
--
-- Note that ghc-7.6 is missing instances for Symbol and Nat, so that
-- sorting only works 'HNat' (as used by "Data.HList.Label3").
data HLeFn

instance HEqByFn HLeFn

instance (HLe x y ~ b) => HEqBy HLeFn x y b
instance HEqBy HLeFn x y b => HEqBy HLeFn (Tagged x v) (Tagged y w) b
instance HEqBy HLeFn x y b => HEqBy HLeFn (Label x) (Label y) b
instance HEqBy HLeFn x y b => HEqBy HLeFn (Proxy x) (Proxy y) b

-- | Data.HList.Label3 labels can only be compared if they belong
-- to the same namespace.
instance (HEqBy HLeFn n m b, ns ~ ns')
     => HEqBy HLeFn (Lbl n ns desc) (Lbl m ns' desc') b


-- | analogous to 'Data.Ord.Down'
data HDown a
instance HEqByFn a => HEqByFn (HDown a)
instance HEqBy f y x b => HEqBy (HDown f) x y b

-- | The HEqBy instances for @HNeq HLeFn@ gives '<'
data HNeq le
instance HEqByFn a => HEqByFn (HNeq a)
instance (HEqBy le y x b1, HNot b1 ~ b2) => HEqBy (HNeq le) x y b2

{- | @HIsAscList le xs b@ is analogous to

> b = all (\(x,y) -> x `le` y) (xs `zip` tail xs)

-}
class HEqByFn le => HIsAscList le (xs :: [*]) (b :: Bool) | le xs -> b

instance HEqByFn le => HIsAscList le '[x] True
instance HEqByFn le => HIsAscList le '[] True
instance (HEqBy le x y b1,
         HIsAscList le (y ': ys) b2,
         HAnd b1 b2 ~ b3)  => HIsAscList le (x ': y ': ys) b3


-- | quick sort with a special case for sorted lists
class (SameLength a b, HEqByFn le) => HSortBy le (a :: [*]) (b :: [*]) | le a -> b where
    hSortBy :: Proxy le -> HList a -> HList b

type HSort x y = HSortBy HLeFn x y

hSort :: HSort x y => HList x -> HList y
hSort :: forall (x :: [*]) (y :: [*]). HSort x y => HList x -> HList y
hSort HList x
xs = forall {k} (le :: k) (a :: [*]) (b :: [*]).
HSortBy le a b =>
Proxy le -> HList a -> HList b
hSortBy (forall {k} (t :: k). Proxy t
Proxy :: Proxy HLeFn) HList x
xs

instance (SameLength a b,
          HIsAscList le a ok,
          HSortBy1 ok le a b,
          HEqByFn le) => HSortBy le a b where
    hSortBy :: Proxy le -> HList a -> HList b
hSortBy = forall {k} {k} (ok :: k) (le :: k) (a :: [*]) (b :: [*]).
HSortBy1 ok le a b =>
Proxy ok -> Proxy le -> HList a -> HList b
hSortBy1 (forall {k} (t :: k). Proxy t
Proxy :: Proxy ok)

instance HSortBy1 True le a a where
    hSortBy1 :: Proxy 'True -> Proxy le -> HList a -> HList a
hSortBy1 Proxy 'True
_ Proxy le
_ HList a
a = HList a
a -- already sorted

instance HQSortBy le a b => HSortBy1 False le a b where
    hSortBy1 :: Proxy 'False -> Proxy le -> HList a -> HList b
hSortBy1 Proxy 'False
_ = forall {k} (le :: k) (a :: [*]) (b :: [*]).
HQSortBy le a b =>
Proxy le -> HList a -> HList b
hQSortBy

class HSortBy1 ok le (a :: [*]) (b :: [*]) | ok le a -> b where
    hSortBy1 :: Proxy ok -> Proxy le -> HList a -> HList b

-- * Merge Sort

{- | HMSortBy is roughly a transcription of this merge sort

> msort [] = []
> msort [x] = [x]
> msort [x,y] = hSort2 x y
> msort xs = case splitAt (length xs `div` 2) xs of
>              (a,b) -> msort a `merge` msort b

> hSort2 x y
>     | x <= y    = [x,y]
>     | otherwise = [y,x]

> merge (x : xs) (y : ys)
>   | x > y     = y : merge (x : xs) ys
>   | otherwise = x : merge xs (y : ys)

-}
class HEqByFn le => HMSortBy le (a :: [*]) (b :: [*]) | le a -> b where
    hMSortBy :: Proxy le -> HList a -> HList b


instance HEqByFn le => HMSortBy le '[] '[] where hMSortBy :: Proxy le -> HList '[] -> HList '[]
hMSortBy Proxy le
_ HList '[]
x = HList '[]
x
instance HEqByFn le => HMSortBy le '[x] '[x] where hMSortBy :: Proxy le -> HList '[x] -> HList '[x]
hMSortBy Proxy le
_ HList '[x]
x = HList '[x]
x
instance (HSort2 b x y ab, HEqBy le x y b, HEqByFn le) =>
    HMSortBy le '[x,y] ab where
      hMSortBy :: Proxy le -> HList '[x, y] -> HList ab
hMSortBy Proxy le
_ (x
a `HCons` y
b `HCons` HList '[]
R:HList[]
HNil) = forall {k} (b :: k) x y (ab :: [*]).
HSort2 b x y ab =>
Proxy b -> x -> y -> HList ab
hSort2 (forall {k} (t :: k). Proxy t
Proxy :: Proxy b) x
a y
b

class HSort2 b x y ab | b x y -> ab where
    hSort2 :: Proxy b -> x -> y -> HList ab

instance HSort2 True x y '[x,y] where
    hSort2 :: Proxy 'True -> x -> y -> HList '[x, y]
hSort2 Proxy 'True
_ x
x y
y = x
x forall x (xs :: [*]). x -> HList xs -> HList (x : xs)
`HCons` y
y forall x (xs :: [*]). x -> HList xs -> HList (x : xs)
`HCons` HList '[]
HNil

instance HSort2 False x y '[y,x] where
    hSort2 :: Proxy 'False -> x -> y -> HList '[y, x]
hSort2 Proxy 'False
_ x
x y
y = y
y forall x (xs :: [*]). x -> HList xs -> HList (x : xs)
`HCons` x
x forall x (xs :: [*]). x -> HList xs -> HList (x : xs)
`HCons` HList '[]
HNil

instance (HMerge le xs' ys' sorted,
          HMSortBy le ys ys',
          HMSortBy le xs xs',
          HLengthEq (a ': b ': c ': cs) n2,
          HDiv2 n2 ~ n,
          HSplitAt n (a ': b ': c ': cs) xs ys)
  => HMSortBy le (a ': b ': c ': cs) sorted where
  hMSortBy :: Proxy le -> HList (a : b : c : cs) -> HList sorted
hMSortBy Proxy le
le HList (a : b : c : cs)
abbs = case forall (n :: HNat) (xsys :: [*]) (xs :: [*]) (ys :: [*]).
HSplitAt n xsys xs ys =>
Proxy n -> HList xsys -> (HList xs, HList ys)
hSplitAt (forall {k} (t :: k). Proxy t
Proxy :: Proxy n) HList (a : b : c : cs)
abbs of
      (HList xs
xs, HList ys
ys) -> forall {k} (le :: k) (x :: [*]) (y :: [*]) (xy :: [*]).
HMerge le x y xy =>
Proxy le -> HList x -> HList y -> HList xy
hMerge Proxy le
le (forall {k} (le :: k) (a :: [*]) (b :: [*]).
HMSortBy le a b =>
Proxy le -> HList a -> HList b
hMSortBy Proxy le
le HList xs
xs) (forall {k} (le :: k) (a :: [*]) (b :: [*]).
HMSortBy le a b =>
Proxy le -> HList a -> HList b
hMSortBy Proxy le
le HList ys
ys)


class HMerge le x y xy | le x y -> xy where
    hMerge :: Proxy le -> HList x -> HList y -> HList xy

instance HMerge le '[] '[] '[] where hMerge :: Proxy le -> HList '[] -> HList '[] -> HList '[]
hMerge Proxy le
_ HList '[]
_ HList '[]
_ = HList '[]
HNil
instance HMerge le (x ': xs) '[] (x ': xs) where hMerge :: Proxy le -> HList (x : xs) -> HList '[] -> HList (x : xs)
hMerge Proxy le
_ HList (x : xs)
x HList '[]
_ = HList (x : xs)
x
instance HMerge le '[] (x ': xs) (x ': xs) where hMerge :: Proxy le -> HList '[] -> HList (x : xs) -> HList (x : xs)
hMerge Proxy le
_ HList '[]
_ HList (x : xs)
x = HList (x : xs)
x

instance (HEqBy le x y b,
          HMerge1 b (x ': xs) (y ': ys) (l ': ls) hhs,
          HMerge le ls hhs srt)
    => HMerge le (x ': xs) (y ': ys) (l ': srt) where
  hMerge :: Proxy le -> HList (x : xs) -> HList (y : ys) -> HList (l : srt)
hMerge Proxy le
le HList (x : xs)
xxs HList (y : ys)
yys = case forall {t :: Bool} {y} {x} {a} {b}.
(HCond t y x a, HCond t x y b) =>
Proxy t -> y -> x -> (a, b)
hMerge1 (forall {k} (t :: k). Proxy t
Proxy :: Proxy b) HList (x : xs)
xxs HList (y : ys)
yys of
        (HCons l
l HList ls
ls, HList hhs
hhs) -> l
l forall x (xs :: [*]). x -> HList xs -> HList (x : xs)
`HCons` forall {k} (le :: k) (x :: [*]) (y :: [*]) (xy :: [*]).
HMerge le x y xy =>
Proxy le -> HList x -> HList y -> HList xy
hMerge Proxy le
le HList ls
ls HList hhs
hhs

type HMerge1 b x y min max = (HCond b (HList x) (HList y) (HList min),
                              HCond b (HList y) (HList x) (HList max))
hMerge1 :: Proxy t -> y -> x -> (a, b)
hMerge1 Proxy t
b y
x x
y = (forall (t :: Bool) x y z. HCond t x y z => Proxy t -> x -> y -> z
hCond Proxy t
b y
x x
y, forall (t :: Bool) x y z. HCond t x y z => Proxy t -> x -> y -> z
hCond Proxy t
b x
y y
x)

-- * Quick sort
{- | HQSortBy is this algorithm

> qsort (x : xs @ (_ : _)) = case partition (<= x) xs of
>                  (le, gt) -> qsort le ++ x : qsort gt
> qsort xs = xs

on random inputs that are not pathological (ie. not already sorted or reverse
sorted) this turns out to be faster than HMSortBy, so it is used by default.

-}
class HQSortBy le (a :: [*]) (b :: [*]) | le a -> b where
    hQSortBy :: Proxy le -> HList a -> HList b

instance HQSortBy le '[] '[] where hQSortBy :: Proxy le -> HList '[] -> HList '[]
hQSortBy Proxy le
_ HList '[]
x = HList '[]
x
instance HQSortBy le '[x] '[x] where hQSortBy :: Proxy le -> HList '[x] -> HList '[x]
hQSortBy Proxy le
_ HList '[x]
x = HList '[x]
x
instance (HPartitionEq le a (b ': bs) bGeq bLt,
        HQSortBy le bLt  sortedLt,
        HQSortBy le bGeq sortedGeq,
        HAppendListR sortedLt (a ': sortedGeq) ~ sorted,
        HAppendList sortedLt (a ': sortedGeq)) =>
    HQSortBy le (a ': b ': bs) sorted where
    hQSortBy :: Proxy le -> HList (a : b : bs) -> HList sorted
hQSortBy Proxy le
le (a
a `HCons` HList (b : bs)
xs) = case forall {k} {k1} (f :: k) (x1 :: k1) (xs :: [*]) (xi :: [*])
       (xo :: [*]).
HPartitionEq f x1 xs xi xo =>
Proxy f -> Proxy x1 -> HList xs -> (HList xi, HList xo)
hPartitionEq Proxy le
le (forall {k} (t :: k). Proxy t
Proxy :: Proxy a) HList (b : bs)
xs of
                      (HList bGeq
g,HList bLt
l) -> forall {k} (le :: k) (a :: [*]) (b :: [*]).
HQSortBy le a b =>
Proxy le -> HList a -> HList b
hQSortBy Proxy le
le HList bLt
l forall (l1 :: [*]) (l2 :: [*]).
HAppendList l1 l2 =>
HList l1 -> HList l2 -> HList (HAppendListR l1 l2)
`hAppendList` (a
a forall x (xs :: [*]). x -> HList xs -> HList (x : xs)
`HCons` forall {k} (le :: k) (a :: [*]) (b :: [*]).
HQSortBy le a b =>
Proxy le -> HList a -> HList b
hQSortBy Proxy le
le HList bGeq
g)




-- * More efficient HRLabelSet / HLabelSet
{- | Provided the labels involved have an appropriate instance of HEqByFn,
it would be possible to use the following definitions:

> type HRLabelSet = HSet
> type HLabelSet  = HSet

-}
class HEqByFn lt => HSetBy lt (ps :: [*])
instance (HEqByFn lt, HSortBy lt ps ps', HAscList lt ps') => HSetBy lt ps

class HSetBy (HNeq HLeFn) ps => HSet (ps :: [*])
instance HSetBy (HNeq HLeFn) ps => HSet ps

{- |

>>> let xx = Proxy :: HIsSet [Label "x", Label "x"] b => Proxy b
>>> :t xx
xx :: Proxy 'False

>>> let xy = Proxy :: HIsSet [Label "x", Label "y"] b => Proxy b
>>> :t xy
xy :: Proxy 'True

-}
class HIsSet (ps :: [*]) (b :: Bool) | ps -> b
instance HIsSetBy (HNeq HLeFn) ps b => HIsSet ps b

class HEqByFn lt => HIsSetBy lt (ps :: [*]) (b :: Bool) | lt ps -> b
instance (HEqByFn lt, HSortBy lt ps ps', HIsAscList lt ps' b) => HIsSetBy lt ps b


-- | @HAscList le xs@ confirms that xs is in ascending order,
-- and reports which element is duplicated otherwise.
class HEqByFn le => HAscList le (ps :: [*])

instance (HEqByFn le, HAscList0 le ps ps) => HAscList le ps

class HEqByFn le => HAscList0 le (ps :: [*]) (ps0 :: [*])

class HEqByFn le => HAscList1 le (b :: Bool) (ps :: [*]) (ps0 :: [*])
instance (HAscList1 le b (y ': ys) ps0, HEqBy le x y b)
  => HAscList0 le (x ': y ': ys) ps0
instance HEqByFn le => HAscList0 le '[] ps0
instance HEqByFn le => HAscList0 le '[x] ps0

instance ( Fail '("Duplicated element", y, "using le", le, "in", ys0), HEqByFn le )
    => HAscList1 le False (y ': ys) ys0
instance HAscList0 le ys ys0 => HAscList1 le True ys ys0

{- $setup

>>> import Data.HList.TypeEqO

-}