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

    , Nil(..)
    , hNil

    , Cons(..)
    , hCons

    , ExtendT(..)
    , AppendT(..)

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

    , Id(..)
    , AppendA(..)

    , FoldrT(..)
    , ConcatT(..)
    , MapT(..)

    , All
    , Length

    , Fail
    , TypeFound
    , TypeNotFound
    , OccursMany(..)
    , OccursMany1(..)
    , OccursOpt(..)
    , Occurs(..)
    , OccursNot

    , NoDuplicates
    )
    where

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


-- List
class List l

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

instance List Nil

hNil :: Nil
hNil = Nil

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

instance List l => List (Cons e l)

hCons :: List l => e -> l -> Cons e l
hCons = Cons

-- ExtendT
infixr 2 :&:
infixr 2 .&.

class ExtendT e l where
    type e :&: l
    (.&.) :: e -> l -> e :&: l

instance ExtendT e Nil where
    type e :&: Nil = Cons e Nil
    e .&. nil = hCons e nil

instance List l => ExtendT e (Cons e' l) where
    type e :&: Cons e' l = Cons e (Cons e' l)
    e .&. Cons e' l = hCons e (hCons e' l)

-- AppendT
infixr 1 :++:
infixr 1 .++.

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

instance List l => AppendT Nil l where
    type Nil :++: l = l
    _ .++. l = l

instance ( List (l :++: l')
         , AppendT l l'
         ) => AppendT (Cons e l) l' where
    type Cons e l :++: l' = Cons e (l :++: l')
    (Cons 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

-- AppendA
data AppendA = AppendA

instance AppendT a b => Apply2T AppendA a b where
    type Apply2 AppendA a b = a :++: b
    apply2 _ a b = a .++. b

-- FoldrT
class FoldrT f v l where
    type Foldr f v l
    hFoldr :: f -> v -> l -> Foldr f v l

instance FoldrT f v Nil where
    type Foldr f v Nil = v
    hFoldr _ v _ = v

instance ( FoldrT f v l
         , Apply2T f e (Foldr f v l)
         ) => FoldrT f v (Cons e l) where
    type Foldr f v (Cons e l) = Apply2 f e (Foldr f v l)
    hFoldr f v (Cons e l) = apply2 f e (hFoldr f v l)

-- ConcatT
class ConcatT ls where
    type Concat ls
    hConcat :: ls -> Concat ls

instance FoldrT AppendA Nil ls => ConcatT ls where
    type Concat ls = Foldr AppendA Nil ls
    hConcat ls = hFoldr AppendA hNil ls

-- MapT
class MapT f l where
    type Map f l
    hMap :: f -> l -> Map f l

instance MapT f Nil where
    type Map f Nil = Nil
    hMap _ _ = hNil

instance ( ApplyT f x
         , MapT f xs
         , List (Map f xs)
         ) => MapT f (Cons x xs) where
    type Map f (Cons x xs) = Cons (Apply f x) (Map f xs)
    hMap f (Cons x xs) = hCons (apply f x) (hMap f xs)

-- All
type family All f l
type instance All f Nil         = True
type instance All f (Cons x xs) = If (Apply f x) (All f xs) False

-- Length
type family Length l
type instance Length Nil        = D0
type instance Length (Cons e l) = Succ (Length l)

-- Fail
class Fail a

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

instance OccursMany e Nil where
    hOccursMany _ = []

instance ( List l
         , OccursMany e l
         )
    => OccursMany e (Cons e l)
    where
      hOccursMany (Cons e l) = e : hOccursMany l

instance ( List l
         , OccursMany e l
         )
    => OccursMany e (Cons e' l)
    where
      hOccursMany (Cons _ l) = hOccursMany l

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

instance Fail (TypeNotFound e) => OccursMany1 e Nil where
    hOccursMany1 _ = undefined

instance ( List l
         , OccursMany e l
         )
    => OccursMany1 e (Cons e l)
    where
      hOccursMany1 (Cons e l) = e : hOccursMany l

instance ( List l
         , OccursMany1 e l
         )
    => OccursMany1 e (Cons e' l)
    where
      hOccursMany1 (Cons _ l) = hOccursMany1 l

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

instance OccursOpt e Nil where
    hOccursOpt _ = Nothing

instance OccursNot e l => OccursOpt e (Cons e l) where
    hOccursOpt (Cons e _) = Just e

instance OccursOpt e l => OccursOpt e (Cons e' l) where
    hOccursOpt (Cons _ l) = hOccursOpt l

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

data TypeNotFound e

instance Fail (TypeNotFound e) => Occurs e Nil
    where
      hOccurs = undefined

instance ( List l
         , OccursNot e l
         )
    => Occurs e (Cons e l)
    where
      hOccurs (Cons e _) = e

instance ( List l
         , Occurs e l
         )
    => Occurs e (Cons e' l)
    where
      hOccurs (Cons _ l) = hOccurs l

-- OccursNot (zero)
data     TypeFound e
class    OccursNot e l
instance OccursNot e Nil
instance Fail (TypeFound e) => OccursNot e (Cons e  l)
instance OccursNot e l     => OccursNot e (Cons e' l)

-- NoDuplicates
class    NoDuplicates l
instance NoDuplicates Nil
instance OccursNot e l => NoDuplicates (Cons 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
-}