{-# LANGUAGE DeriveDataTypeable,
             FlexibleContexts,
             FlexibleInstances,
             MultiParamTypeClasses,
             TypeFamilies,
             TypeOperators,
             UndecidableInstances
  #-}
module Data.HList.Prelude
    ( HList

    , HNil(..)
    , hNil

    , HCons(..)
    , hCons

    , HExtendT(..)
    , HAppendT(..)

    , ApplyT(..)
    , Apply2T(..)

    , Id(..)
    , HAppendA(..)

    , HFoldrT(..)
    , HConcatT(..)
    , HMapT(..)

    , HAll
    , HLength
    )
    where

import Data.Typeable
import Types.Data.Bool
import Types.Data.Num hiding ((:*:))


-- HList
class HList l

-- HNil
data HNil
    = HNil
      deriving (Show, Eq, Ord, Read, Typeable)

instance HList HNil

hNil :: HNil
hNil = HNil

-- HCons
data HCons e l
    = HCons e l
      deriving (Show, Eq, Ord, Read, Typeable)

instance HList l => HList (HCons e l)

hCons :: HList l => e -> l -> HCons e l
hCons = HCons

-- HExtendT
infixr 2 :*:
infixr 2 .*.

class HExtendT e l where
    type e :*: l
    (.*.) :: e -> l -> e :*: l

instance HExtendT e HNil where
    type e :*: HNil = HCons e HNil
    e .*. nil = hCons e nil

instance HList l => HExtendT e (HCons e' l) where
    type e :*: HCons e' l = HCons e (HCons e' l)
    e .*. HCons e' l = hCons e (hCons e' l)

-- HAppendT
infixr 1 :++:
infixr 1 .++.

class HAppendT l l' where
    type l :++: l'
    (.++.) :: l -> l' -> l :++: l'

instance HList l => HAppendT HNil l where
    type HNil :++: l = l
    _ .++. l = l

instance ( HList (l :++: l')
         , HAppendT l l'
         ) => HAppendT (HCons e l) l' where
    type HCons e l :++: l' = HCons e (l :++: l')
    (HCons e l) .++. l' = hCons e (l .++. l')

-- ApplyT
class ApplyT f a where
    type Apply f a
    apply :: f -> a -> Apply f a
    apply _ _ = undefined

-- Apply2T
class Apply2T f a b where
    type Apply2 f a b
    apply2 :: f -> a -> b -> Apply2 f a b
    apply2 _ _ _ = undefined

-- Id
data Id = Id

instance ApplyT Id a where
    type Apply Id a = a
    apply _ a = a

-- HAppendA
data HAppendA = HAppendA

instance HAppendT a b => Apply2T HAppendA a b where
    type Apply2 HAppendA a b = a :++: b
    apply2 _ a b = a .++. b

-- HFoldrT
class HFoldrT f v l where
    type HFoldr f v l
    hFoldr :: f -> v -> l -> HFoldr f v l

instance HFoldrT f v HNil where
    type HFoldr f v HNil = v
    hFoldr _ v _ = v

instance ( HFoldrT f v l
         , Apply2T f e (HFoldr f v l)
         ) => HFoldrT f v (HCons e l) where
    type HFoldr f v (HCons e l) = Apply2 f e (HFoldr f v l)
    hFoldr f v (HCons e l) = apply2 f e (hFoldr f v l)

-- HConcatT
class HConcatT ls where
    type HConcat ls
    hConcat :: ls -> HConcat ls

instance HFoldrT HAppendA HNil ls => HConcatT ls where
    type HConcat ls = HFoldr HAppendA HNil ls
    hConcat ls = hFoldr HAppendA hNil ls

-- HMapT
class HMapT f l where
    type HMap f l
    hMap :: f -> l -> HMap f l

instance HMapT f HNil where
    type HMap f HNil = HNil
    hMap _ _ = hNil

instance ( ApplyT f x
         , HMapT f xs
         , HList (HMap f xs)
         ) => HMapT f (HCons x xs) where
    type HMap f (HCons x xs) = HCons (Apply f x) (HMap f xs)
    hMap f (HCons x xs) = hCons (apply f x) (hMap f xs)

-- HAll
type family HAll f l
type instance HAll f HNil         = True
type instance HAll f (HCons x xs) = If (Apply f x) (HAll f xs) False

-- HLength
type family HLength l
type instance HLength HNil        = D0
type instance HLength (HCons e l) = Succ (HLength l)