{- -*- coding: utf-8 -*- -}
{-# LANGUAGE
  DeriveDataTypeable,
  EmptyDataDecls,
  FlexibleContexts,
  FlexibleInstances,
  FunctionalDependencies,
  MultiParamTypeClasses,
  OverlappingInstances,
  TypeFamilies,
  TypeOperators,
  UndecidableInstances
  #-}
module Data.HList.Prelude
    ( HList

    , HNil(..)
    , hNil

    , HCons(..)
    , hCons

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

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

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

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

    , HAll
    , HLength

    , Fail
    , TypeFound
    , TypeNotFound
    , HOccursMany(..)
    , HOccursMany1(..)
    , HOccursOpt(..)
    , HOccurs(..)
    , HOccursNot(..)
    )
    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)

-- Fail
class Fail a

-- HOccursMany (zero or more)
class HOccursMany e l where
    hOccursMany :: l -> [e]

instance HOccursMany e HNil where
    hOccursMany _ = []

instance ( HList l
         , HOccursMany e l
         )
    => HOccursMany e (HCons e l)
    where
      hOccursMany (HCons e l) = e : hOccursMany l

instance ( HList l
         , HOccursMany e l
         )
    => HOccursMany e (HCons e' l)
    where
      hOccursMany (HCons _ l) = hOccursMany l

-- HOccursMany1 (one or more)
class HOccursMany1 e l where
    hOccursMany1 :: l -> [e]

instance Fail (TypeNotFound e) => HOccursMany1 e HNil where
    hOccursMany1 _ = undefined

instance ( HList l
         , HOccursMany e l
         )
    => HOccursMany1 e (HCons e l)
    where
      hOccursMany1 (HCons e l) = e : hOccursMany l

instance ( HList l
         , HOccursMany1 e l
         )
    => HOccursMany1 e (HCons e' l)
    where
      hOccursMany1 (HCons _ l) = hOccursMany1 l

-- HOccursOpt (zero or one)
class HOccursOpt e l where
    hOccursOpt :: l -> Maybe e

instance HOccursOpt e HNil where
    hOccursOpt _ = Nothing

instance HOccursNot e l => HOccursOpt e (HCons e l) where
    hOccursOpt (HCons e _) = Just e

instance HOccursOpt e l => HOccursOpt e (HCons e' l) where
    hOccursOpt (HCons _ l) = hOccursOpt l

-- HOccurs (one)
class HOccurs e l where
    hOccurs :: l -> e

data TypeNotFound e

instance Fail (TypeNotFound e) => HOccurs e HNil
    where
      hOccurs = undefined

instance ( HList l
         , HOccursNot e l
         )
    => HOccurs e (HCons e l)
    where
      hOccurs (HCons e _) = e

instance ( HList l
         , HOccurs e l
         )
    => HOccurs e (HCons e' l)
    where
      hOccurs (HCons _ l) = hOccurs l

-- HOccursNot (zero)
data     TypeFound e
class    HOccursNot e l
instance HOccursNot e HNil
instance Fail (TypeFound e) => HOccursNot e (HCons e  l)
instance HOccursNot e l     => HOccursNot e (HCons e' l)

{-
{-
"Strongly Typed Heterogeneous Collections"
   — August 26, 2004
       Oleg Kiselyov
       Ralf Lämmel
       Keean Schupke
==========================
9 By chance or by design? 

We will now discuss the issues surrounding the definition of type
equality, inequality, and unification — and give implementations
differing in simplicity, genericity, and portability.

We define the class TypeEq x y b for type equality. The class relates
two types x and y to the type HTrue in case the two types are equal;
otherwise, the types are related to HFalse. We should point out
however groundness issues. If TypeEq is to return HTrue, the types
must be ground; TypeEq can return HFalse even for unground types,
provided they are instantiated enough to determine that they are not
equal. So, TypeEq is total for ground types, and partial for unground
types. We also define the class TypeCast x y: a constraint that holds
only if the two types x and y are unifiable. Regarding groundness of x
and y, the class TypeCast is less restricted than TypeEq. That is,
TypeCast x y succeeds even for unground types x and y in case they can
be made equal through unification. TypeEq and TypeCast are related to
each other as fol- lows. Whenever TypeEq succeeds with HTrue, TypeCast
succeeds as well. Whenever TypeEq succeeds with HFalse, TypeCast
fails.  But for unground types, when TypeCast succeeds, TypeEq might
fail. So the two complement each other for unground types. Also,
TypeEq is a partial predicate, while TypeCast is a relation. That’s
why both are useful.
 -}
class    TypeEq x y b | x y -> b
instance TypeEq x x True
instance TypeCast False b =>
         TypeEq x y b

class TypeCast a b | a -> b, b -> a
    where
      typeCast :: a -> b

class TypeCast' t a b | t a -> b, t b -> a
    where
      typeCast' :: t -> a -> b

class TypeCast'' t a b | t a -> b, t b -> a
    where
      typeCast'' :: t -> a -> b

instance TypeCast' () a b => TypeCast a b
    where
      typeCast x = typeCast' () x

instance TypeCast'' t a b => TypeCast' t a b
    where
      typeCast' = typeCast''

instance TypeCast'' () a a
    where
      typeCast'' _ x = x
-}