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

    , HNil(..)
    , hNil

    , HCons(..)
    , hCons

    , HExtendable(..)
    , HAppendable(..)

    , Applyable(..)
    , Applyable2(..)

    , Id(..)
    , ApplyHAppend(..)

    , HFoldrable(..)
    , HConcatable(..)
    , HMappable(..)
    , HAllable(..)

    , 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

-- HExtendable
infixr 2 :*:
infixr 2 .*.

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

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

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

-- HAppendable
infixr 1 :++:
infixr 1 .++.

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

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

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

-- Applyable
class Applyable f a where
    type Apply f a
    apply :: f -> a -> Apply f a

-- Applyable2
class Applyable2 f a b where
    type Apply2 f a b
    apply2 :: f -> a -> b -> Apply2 f a b

-- Id
data Id = Id

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

-- ApplyHAppend
data ApplyHAppend = ApplyHAppend

instance HAppendable a b => Applyable2 ApplyHAppend a b where
    type Apply2 ApplyHAppend a b = a :++: b
    apply2 _ a b = a .++. b

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

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

instance ( HFoldrable f v l
         , Applyable2 f e (HFoldr f v l)
         ) => HFoldrable 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)

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

instance HFoldrable ApplyHAppend HNil ls => HConcatable ls where
    type HConcat ls = HFoldr ApplyHAppend HNil ls
    hConcat ls = hFoldr ApplyHAppend hNil ls

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

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

instance ( Applyable f x
         , HMappable f xs
         , HList (HMap f xs)
         ) => HMappable 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)

-- HAllable
class HAllable f l where
    type HAll f l
    hAll :: f -> l -> HAll f l

instance HAllable f HNil where
    type HAll f HNil = True
    hAll _ _ = undefined :: True

instance ( IfT (Apply f x) (HAll f xs) False
         , Applyable f x
         , HAllable f xs
         ) => HAllable f (HCons x xs) where
    type HAll f (HCons x xs) = If (Apply f x)
                                 (HAll f xs)
                                 False
    hAll f (HCons x xs) = ifT (apply f x)
                                 (hAll f xs)
                                 (undefined :: False)

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