{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE NoMonomorphismRestriction #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleInstances #-}

module HListExtras where
import Data.HList.CommonMain


data FApply = FApply
instance (ApplyAB f a b, ab ~ (a -> b)) =>  ApplyAB FApply f ab where
    applyAB _ = applyAB

class HReplicate2 (n ::HNat) e l | n e -> l, l -> n
    where hReplicate2 :: Proxy n -> e -> HList l
instance HReplicate2 HZero e '[] where
    hReplicate2 _ _ = HNil
instance (HReplicate2 n e es') => HReplicate2 (HSucc n) e (e ': es') where
    hReplicate2 n e = e `HCons` hReplicate2 (hPred n) e

-- hReplicateApp :: HReplicate2 (HLength r) e r' => e -> HList r
hReplicateApp e = let r = hMap FApply (hReplicate2 (hLength r) e) in r

-- | splitAt
hSplitAt n xs = hSplitAtAux n xs HNil

class HSplitAtAux (n :: HNat) l a0 a b | n -> l a0 a b where
    hSplitAtAux :: Proxy n -> HList l -> HList a0 -> (HList a, HList b)

instance (l ~ b, a ~ HRevApp a0 '[]) => HSplitAtAux HZero l a0 a b where
    hSplitAtAux _ l acc = (hReverse acc, l)

instance  (  (x ': xs) ~ ls, acc' ~ (x ': acc),
    HSplitAtAux n xs acc' a b) => HSplitAtAux (HSucc n) ls acc a b where
    hSplitAtAux n (HCons x xs) acc = hSplitAtAux (hPred n) xs (HCons x acc)


hEnumFromTo :: Proxy a -> Proxy b -> Proxy (HEnumFromTo a b)
hEnumFromTo a b = proxy

-- |  [n1 .. n1 + n2]

type family HEnumFromTo (from::HNat) (to::HNat) :: [HNat]
type instance HEnumFromTo a HZero = '[a]
type instance HEnumFromTo a (HSucc b) = a ': HEnumFromTo (HSucc a) b


-- this doesn't work any better... want ghc to be able to simplify
-- that (hReverse (hReverse x) `asTypeOf` x)
class (SameLength a b, SameLength b a) => HReverse2 a b | a -> b, b -> a where
    hReverse2 :: HList a -> HList b

instance (SameLength a b, SameLength b a, HRevApp a '[] ~ b, HRevApp b '[] ~ a) =>  HReverse2 a b where
    hReverse2 = hReverse


class HMap1 f a b where hMap1 :: f -> HList a -> HList b

instance (a ~ '[]) => HMap1  f a '[] where
    hMap1 _ _ = HNil

instance (ApplyAB f a b, (a ': as) ~ aas, HMap1 f as bs) =>
    HMap1 f aas (b ': bs) where
    hMap1 f (HCons a as) = HCons (applyAB f a) (hMap1 f as)


class HMap2 f a b where hMap2 :: f -> HList a -> HList b

instance (a ~ '[]) => HMap2  f '[] a where
    hMap2 _ _ = HNil

instance (ApplyAB f a b, (b ': bs) ~ bbs, HMap2 f as bs) =>
    HMap2 f (a ': as) bbs where
    hMap2 f (HCons a as) = HCons (applyAB f a) (hMap2 f as)