{-# LANGUAGE PolyKinds, TypeFamilies, DataKinds, KindSignatures,
    TypeOperators, UndecidableInstances #-}

{-# LANGUAGE RankNTypes, LiberalTypeSynonyms, EmptyDataDecls #-}

-- | A prelude for type-level programming with type families

module Prelude.Type.Families ( 
  module Prelude,
  module Prelude.Type.Families,
  module GHC.TypeLits,
  module Prelude.Type.Integer,
  module Prelude.Type.Value
  ) where

import Prelude.Type.Value
import Prelude.Type.Integer
import GHC.TypeLits (Symbol, Nat)
import Prelude (
  Bool(False, True),
  Maybe(Nothing, Just),
  Either(Left, Right),
  Ordering(LT, GT, EQ)
  )

-- | If

-- >>> T :: T (If (I 3 < I 2) "a" "b")
-- "b"
type family If (p :: Bool) (a :: k) (b :: k) :: k
type instance If True a b = a
type instance If False a b = b

-- * Type Classes

-- ** Show

type Show a = Shows a '[]

type family Shows (a :: k) (t :: [Symbol]) :: [Symbol]

-- TODO: ShowsPrec

-- ** Kind

-- | Get kind of a type

type family Kind (a :: k) :: *

-- ** Eq

type family (a :: k) == (b :: k) :: Bool

type a /= b = Not (a == b)

-- ** Ord

type family Compare (a :: k) (b :: k) :: Ordering

type a < b = FromOrdering True False False (Compare a b)

type a <= b = FromOrdering True True False (Compare a b)

type a >= b = FromOrdering False True True (Compare a b)

type a > b = FromOrdering False False True (Compare a b)

type Max a b = FromOrdering b a a (Compare a b)

type Min a b = FromOrdering a a b  (Compare a b)

-- ** Enum
          
type family ToEnum (i :: Integer) :: k

type family FromEnum (a :: k) :: Integer

type Succ a = ToEnum (I 1 + FromEnum a)

type Pred a = ToEnum (FromEnum a `Minus` I 1)

-- TODO : test
type EnumFromTo a b = EnumFromTo_1 (FromEnum a < FromEnum b) a b
type family EnumFromTo_1 (lt :: Bool) (a :: k) (b :: k) :: [k]
type instance EnumFromTo_1 True a b = a ': EnumFromTo (Succ a) b
type instance EnumFromTo_1 False a b = '[]

-- TODO: EnumFromThenTo

-- ** Bounded

type family MinBound :: k

type family MaxBound :: k

-- * Primitive kinds

-- ** Unit

type instance Shows '() x = "()" ': x

type instance ToEnum Zeros = '()
type instance FromEnum '() = Zeros

type instance Kind (a :: ()) = ()

type instance ((a :: ()) == b) = True

type instance MinBound = '()
type instance MaxBound = '()

type instance Compare '() '() = EQ

-- ** Maybe

type instance Shows Nothing x = "Nothing" ': x
type instance Shows (Just a) x = "Just" ': Shows a x

type instance FromEnum Nothing = Zeros
type instance FromEnum (Just x) = I 1 + FromEnum x

type instance ToEnum Zeros = Nothing
type instance ToEnum (One i) = Just (ToEnum (IntegerCons False i))
type instance ToEnum (Zero i) = Just (ToEnum (Zero i `Minus` I 1))

type instance Compare Nothing Nothing = EQ
type instance Compare Nothing (Just a) = LT
type instance Compare (Just a) Nothing = GT
type instance Compare (Just a) (Just b) = Compare a b

type instance Kind (a :: Maybe k) = Maybe (Kind (Undefined :: k))

type instance Nothing == Nothing = True
type instance Just a  == Nothing = False
type instance Nothing == Just b  = False
type instance Just a  == Just b  = a == b

type instance MinBound = Nothing
type instance MaxBound = Just MaxBound

-- ** Bool

type instance Shows True  x = "True"  ': x
type instance Shows False x = "False" ': x

type instance FromEnum False = I 0
type instance FromEnum True  = I 1

type instance ToEnum Zeros       = False
type instance ToEnum (One Zeros) = True

type instance Compare True True = EQ
type instance Compare False False = EQ
type instance Compare True False = GT
type instance Compare False True = LT

type instance Kind (a :: Bool) = Bool

type instance True  == True  = True
type instance True  == False = False
type instance False == True  = False
type instance False == False = True

type instance MinBound = False
type instance MaxBound = True

type family Not (a :: Bool) :: Bool
type instance Not True = False
type instance Not False = True

type family ((a :: Bool) || (b :: Bool)) :: Bool
type instance False || a = a
type instance True  || a = True

type family ((a :: Bool) && (b :: Bool)) :: Bool
type instance True  && a = a
type instance False && a = False

-- ** Ordering

type family FromOrdering (lt :: k) (eq :: k) (gt :: k) (o :: Ordering) :: k
type instance FromOrdering a b c LT = a
type instance FromOrdering a b c EQ = b
type instance FromOrdering a b c GT = c

type instance Shows LT x = "LT" ': x
type instance Shows EQ x = "EQ" ': x
type instance Shows GT x = "GT" ': x

type instance FromEnum LT = I 0
type instance FromEnum EQ = I 1
type instance FromEnum GT = I 2

type instance ToEnum Zeros              = LT
type instance ToEnum (One Zeros)        = EQ
type instance ToEnum (Zero (One Zeros)) = GT

type instance Compare EQ EQ = EQ
type instance Compare LT LT = EQ
type instance Compare GT GT = EQ
type instance Compare LT EQ = LT
type instance Compare LT GT = LT
type instance Compare EQ GT = LT
type instance Compare GT EQ = GT
type instance Compare GT LT = GT
type instance Compare EQ LT = GT

type instance Kind (a :: Ordering) = Ordering

type instance MinBound = LT
type instance MaxBound = GT

type family CombineOrdering (a :: Ordering) (b :: Ordering) :: Ordering
type instance CombineOrdering LT a = LT
type instance CombineOrdering EQ a = a
type instance CombineOrdering GT a = GT

-- ** Either

type instance Shows (Left  a) x = "Left" ': Shows a x
type instance Shows (Right a) x = "Right" ': Shows a x

type instance Compare (Left a) (Right b) = LT
type instance Compare (Right a) (Left b) = GT
type instance Compare (Right a) (Right b) = Compare a b
type instance Compare (Left a) (Left b) = Compare a b

type instance Kind (a :: Either k1 k2) = Either (Kind (Undefined :: k1)) (Kind (Undefined :: k2))

type instance Left  a == Left  b = a == b
type instance Right a == Right b = a == b
type instance Left  a == Right b = False
type instance Right a == Left  b = False

type instance MinBound = Left MinBound
type instance MaxBound = Right MaxBound

-- ** Tuples

type instance Shows '(a, b)       x = "(" ': Shows a ("," ': Shows b (")" ': x))
type instance Shows '(a, b, c)    x = "(" ': Shows a ("," ': Shows b ("," ': Shows c (")" ': x)))
type instance Shows '(a, b, c, d) x = "(" ': Shows a ("," ': Shows b ("," ': Shows c ("," ': Shows d (")" ': x))))

type instance Compare '(a, b)       '(e, f)       = CombineOrdering (Compare a e) (Compare b f)
type instance Compare '(a, b, c)    '(e, f, g)    = CombineOrdering (Compare a e) (Compare '(b, c) '(f, g))
type instance Compare '(a, b, c, d) '(e, f, g, h) = CombineOrdering (Compare a e) (Compare '(b, c, d) '(f, g, h))

type instance Kind '(a, b) = (Kind a, Kind b)
type instance Kind '(a, b, c) = (Kind a, Kind b, Kind c)
type instance Kind '(a, b, c, d) = (Kind a, Kind b, Kind c, Kind d)

type instance '(a, b) == '(e, f) = (a == e) && (b == f)
type instance '(a, b, c) == '(e, f, g) = (a == e) && (b == f) && (c == g)
type instance '(a, b, c, d) == '(e, f, g, h) = (a == e) && (b == f) && (c == g) && (d == h)

type instance MinBound = '(MinBound, MinBound)
type instance MinBound = '(MinBound, MinBound, MinBound)
type instance MinBound = '(MinBound, MinBound, MinBound, MinBound)

type instance MaxBound = '(MaxBound, MaxBound)
type instance MaxBound = '(MaxBound, MaxBound, MaxBound)
type instance MaxBound = '(MaxBound, MaxBound, MaxBound, MaxBound)

type family Fst (p :: (a, b)) :: a
type instance Fst '(a, b) = a

type family Snd (p :: (a, b)) :: b
type instance Snd '(a, b) = b

-- ** Type Literals

type instance Kind (a :: Nat) = Nat
type instance Kind (a :: Symbol) = Symbol

type instance MinBound = 0

-- ** Star

-- | The Kind *

data StarKind

type instance Kind (a :: *) = StarKind

-- * Predicates/Constraints

type Compose f g a = f (g a)

type family (a :: x) $ (b :: y) :: k
type instance a $ b = a b

type Id a = a

type Flip f a b = f a b

-- ** Lists

type instance Shows '[] r = "[]" ': r
type instance Shows (x ': xs) r = "(" ': Shows x ("," ': (ShowsTail xs r))
type family ShowsTail (a :: [k]) (x :: [Symbol]) :: [Symbol]
type instance ShowsTail '[] r = "]" ': r 
type instance ShowsTail (x ': xs) r = "," ': Shows x (ShowsTail xs r)

type instance Compare '[] '[] = EQ
type instance Compare '[] (x ': xs) = LT
type instance Compare (x ': xs) '[] = GT
type instance Compare (x ': xs) (y ': ys) = CombineOrdering (Compare x y) (Compare xs ys)

type instance Kind (a :: [k]) = [Kind (Undefined :: k)]

type instance '[]       == '[]       = True
type instance '[]       == (x ': xs) = False
type instance (x ': xs) == '[]       = False
type instance (x ': xs) == (y ': ys) = (x == y) && (xs == ys)

type instance MinBound = '[]
                      
type family Head (l :: [k]) :: k
type instance Head '[] = Error "Head_: empty list"
type instance Head (x ': xs) = x

type family Tail (l :: [k]) :: [k]
type instance Tail '[] = Error "Tail_: empty list"
type instance Tail (x ': xs) = xs
               
type family Last (a :: [k]) :: k
type instance Last '[] = Error "Last_: empty list"
type instance Last (x ': y ': xs) = Last (y ': xs)
type instance Last (x ': '[]) = x

type family Init (a :: [k]) :: [k]
type instance Init '[] = Error "Init_: empty list"
type instance Init (x ': y ': xs) = x ': Init (y ': xs)
type instance Init (x ': '[]) = '[]

type family Null (a :: [k]) :: Bool
type instance Null '[] = True
type instance Null (x ': xs) = False

type family Length (a :: [k]) :: Integer
type instance Length '[] = I 0
type instance Length (x ': xs) = I 1 + Length xs

type family (a :: [k]) !! (i :: Integer) :: k
type instance '[] !! i = Error "(!!\\): index too large"
type instance (x ': xs) !! i = At_1 x xs (IsZero i) i
type family At_1 (a :: k) (b :: [k]) (c :: Bool) (d :: Integer) :: k
type instance At_1 x xs True i = x
type instance At_1 x xs False i = xs !! (i `Minus` I 1)

-- >>> T :: T (Drop (I 7) '[1,2,3,4,5,6,7,8,9,10,11,12])
-- [8,9,10,11,12]
type family Drop (i :: Integer) (a :: [k]) :: [k]
type instance Drop i '[] = '[]
type instance Drop Zeros (x ': xs) = (x ': xs)
type instance Drop Ones (x ': xs) = Error "Drop_: negative count" 
type instance Drop (One i) (x ': xs) = Drop i (Drop i xs)
type instance Drop (Zero i) (x ': xs) = Drop i (Drop i (x ': xs))

type family (a :: [k]) ++ (b :: [k]) :: [k]
type instance '[] ++ l = l
type instance (x ': xs) ++ l = x ': (xs ++ l)

type family Concat (a :: [[k]]) :: [k]
type instance Concat '[] = '[]
type instance Concat (x ': xs) = x ++ Concat xs

type Replicate i a = Replicate_1 (IsZero i) i a
type family Replicate_1 (z :: Bool) (i :: Integer) (a :: k) :: [k]
type instance Replicate_1 True  i a = '[]
type instance Replicate_1 False i a = a ': Replicate (i `Minus` I 1) a

type family And (a :: [Bool]) :: Bool
type instance And '[] = True
type instance And (x ': xs) = x && And xs

type family Or (a :: [Bool]) :: Bool
type instance Or '[] = False
type instance Or (x ': xs) = x || Or xs

type family Elem (a :: k) (b :: [k]) :: Bool
type instance Elem a '[] = False
type instance Elem a (x ': xs) = Elem_1 (a == x) a xs
type family Elem_1 (p :: Bool) (a :: k) (b :: [k]) :: Bool
type instance Elem_1 True a xs = True
type instance Elem_1 False a xs = Elem a xs

type NotElem a b = Not (Elem a b)

-- TODO: Maximum
-- TODO: minimum zip zip3 zipWith zipWith3 unzip unzip3
-- TODO: filter

-- * Integer

-- >>> T :: (Shows (I 15) '[]) ~ s => T s
-- ["1","5"]
-- TODO: case for 0 is wrong
type instance Shows i x = ShowsInteger_2 (IsZero i) i x
type family ShowsInteger_2 (z :: Bool) (i :: Integer) (x :: [Symbol]) :: [Symbol]
type instance ShowsInteger_2 True  i x = x
type instance ShowsInteger_2 False i x =
      (Shows (Quot i (I 10)) (Digit (Rem i (I 10)) ': x))

type family IsZero (i :: Integer) :: Bool
type instance IsZero Zeros = True
type instance IsZero (Zero i) = IsZero i
type instance IsZero Ones = False
type instance IsZero (One i) = False

type family Digit (i :: Integer) :: Symbol
type instance Digit Zeros = "0"
type instance Digit (One Zeros) = "1"
type instance Digit (Zero (One Zeros)) = "2"
type instance Digit (One (One Zeros)) = "3"
type instance Digit (Zero (Zero (One Zeros))) = "4"
type instance Digit (One (Zero (One Zeros))) = "5"
type instance Digit (Zero (One (One Zeros))) = "6"
type instance Digit (One (One (One Zeros))) = "7"
type instance Digit (Zero (Zero (Zero (One Zeros)))) = "8"
type instance Digit (One (Zero (Zero (One Zeros)))) = "9"

type instance i == j = IntegerEqual (IntegerEnd2 i j) i j
type family IntegerEqual (p :: Bool) (i :: Integer) (j :: Integer) :: Bool
type instance IntegerEqual True i j = IntegerHead i == IntegerHead j
type instance IntegerEqual False i j = (IntegerHead i == IntegerHead j) && (IntegerTail i == IntegerTail j)

type instance FromEnum i = i
type instance ToEnum i = i

type instance Kind (a :: Integer) = Integer

type family IntegerEnd (i :: Integer) :: Bool
type instance IntegerEnd Zeros = True
type instance IntegerEnd Ones = True
type instance IntegerEnd (One i) = False
type instance IntegerEnd (Zero i) = False

type IntegerEnd2 i j = IntegerEnd i && IntegerEnd j

type family ((a :: k) + (b :: k)) :: k
type instance a + b = AddWithCarry False a b

-- >>> T :: T (AddWithCarry False (I 4) (I 7))
-- 11
-- >>> T :: T (I 14 * I 15)
-- 210
type AddWithCarry c i j = AddWithCarry_2 (IntegerEnd2 i j) c i j
type family AddWithCarry_2 (end :: Bool) (a :: Bool) (b :: Integer) (c :: Integer) :: Integer
type instance AddWithCarry_2 True False Zeros i = i
type instance AddWithCarry_2 True False Ones  Ones = Zeros
type instance AddWithCarry_2 True False Ones  Zeros = Ones
type instance AddWithCarry_2 True True Zeros Zeros = One Zeros
type instance AddWithCarry_2 True True Zeros Ones = Zeros
type instance AddWithCarry_2 True True Ones  Ones = Ones
type instance AddWithCarry_2 True True Ones  Zeros = Zeros
type instance AddWithCarry_2 False c i j =
  AddWithCarry_3 (Add3 c (IntegerHead i) (IntegerHead j))
                 (IntegerTail i) (IntegerTail j)
type family AddWithCarry_3 (h :: (Bool, Bool)) (i :: Integer) (j :: Integer) :: Integer
type instance AddWithCarry_3 '(s, c) i j = IntegerCons s (AddWithCarry c i j)

-- | Two bit sum of three bits
-- Add3 a b c ~ '(sum, carry)
type family Add3 (a :: Bool) (b :: Bool) (c :: Bool) :: (Bool, Bool)
type instance Add3 True True True = '(True, True)
type instance Add3 False True True = '(False, True)
type instance Add3 True False True = '(False, True)
type instance Add3 True True False = '(False, True)
type instance Add3 False False True = '(True, False)
type instance Add3 True False False = '(True, False)
type instance Add3 False True False = '(True, False)
type instance Add3 False False False = '(False, False)
    
-- >>> T :: T ((I 4) `Minus` (I 7))
-- -3
type family (a :: k) `Minus` (b :: k) :: k
type instance a `Minus` b = a + Negate b

type family Negate (a :: k) :: k
type instance Negate a = Complement a + I 1
          
type family   (a :: k) * (b :: k) :: k
type instance Zeros    * j = Zeros
type instance Ones     * j = Negate j
type instance (Zero i) * j = IntegerCons False (i * j)
type instance (One i)  * j = j + IntegerCons False (i * j)

type Signum a = FromOrdering Ones Zeros (One Zeros) (Compare0 a)

type Abs a = FromOrdering (Negate a) a a (Compare0 a)

type Subtract a b = b `Minus` a

type Even i = IntegerHead i

type Odd i = Not (Even i)

-- >>> T :: T (Gcd (I 14) (I 6))
-- 2
type family   Gcd_1 (zs :: Bool) (a :: Integer) (b :: Integer) :: Integer
type family   Gcd_3 (z :: Bool) (a :: Integer) (b :: Integer) :: Integer
type          Gcd        a b = Gcd_1 (IsZero a && IsZero b) a b
type instance Gcd_1 True  a b = Error "Gcd 0 0 is undefined"
type instance Gcd_1 False a b = Gcd_2 (Abs a) (Abs b)
type          Gcd_2       a b = Gcd_3 (IsZero b) a b
type instance Gcd_3 True  a b = a
type instance Gcd_3 False a b = Gcd_2 b (Rem a b)

-- TODO: lcm, (^), (^^), 

-- Ord Integer

type instance Compare (i :: Integer) j = Compare0 (i `Minus` j)

type family Compare0 (i :: Integer) :: Ordering
type instance Compare0 Zeros    = EQ
type instance Compare0 Ones     = LT
type instance Compare0 (One i)  = FromOrdering LT GT GT (Compare0 i)
type instance Compare0 (Zero i) = Compare0 i
                                     
-- * Misc functions from the Prelude

type Undefined = Error "undefined"

type family Error (a :: k1) :: k2
type instance Error (a :: k1) = ERROR a
type family ERROR (a :: k1) :: k2

type family AsKindOf (a :: k) (b :: k) :: k
type instance AsKindOf a b = a

-- * Bits

type family Xor (a :: k) (b :: k) :: k

type instance Xor True True = False
type instance Xor True False = True
type instance Xor False True = True
type instance Xor False False = False

type instance Xor i j = Xor_2 (IntegerEnd2 i j) i j
type family Xor_2 (end :: Bool) (a :: k) (b :: k) :: k
type instance Xor_2 True Zeros Zeros = Zeros
type instance Xor_2 True Ones Ones = Zeros
type instance Xor_2 True Zeros Ones = Ones
type instance Xor_2 True Ones Zeros = Ones
type instance Xor_2 False i j =
  IntegerCons (Xor (IntegerHead i) (IntegerHead j))
              (Xor (IntegerTail i) (IntegerTail j))

type family ((a ::  k) .&. (b :: k)) :: k
type instance (True .&. True) = True
type instance (True .&. False) = False
type instance (False .&. True) = False
type instance (False .&. False) = False

type instance i .&. j = BitwiseAnd_2 (IntegerEnd2 i j) i j
type family BitwiseAnd_2 (end :: Bool) (a :: k) (b :: k) :: k
type instance BitwiseAnd_2 True Zeros Zeros = Zeros
type instance BitwiseAnd_2 True Ones Ones = Ones
type instance BitwiseAnd_2 True Zeros Ones = Zeros
type instance BitwiseAnd_2 True Ones Zeros = Zeros
type instance BitwiseAnd_2 False i j =
  IntegerCons (IntegerHead i .&. IntegerHead j)
              (IntegerTail i .&. IntegerTail j)

type family Complement (a :: k) :: k

type instance Complement True = False
type instance Complement False = True

type instance Complement Zeros = Ones
type instance Complement Ones = Zeros
type instance Complement (One i) = IntegerCons False (Complement i)
type instance Complement (Zero i) = IntegerCons True (Complement i)

-- * Integral

-- >>> T :: T (QuotRem (I 13) (I 7))
-- (1,6)
type QuotRem a b = '(
  (Signum a * Signum b * Fst (QuotRem' (Abs a) (Abs b))),
  (Signum a * Snd (QuotRem' (Abs a) (Abs b))))

type family QuotRem'_2 (p :: Bool) (a :: Integer) (b :: Integer) :: (Integer, Integer)
type family QuotRem'_3 (b :: Integer) (qr :: (Integer, Integer)) :: (Integer, Integer)
type family QuotRem'_4 (p :: Bool) (a :: Integer) (b :: Integer) (c :: Integer) :: (Integer, Integer)
type          QuotRem'        a b   = QuotRem'_2 (a < b) a b
type instance QuotRem'_2 True  a b   = '(I 0, a)
type instance QuotRem'_2 False a b   = QuotRem'_3 b (QuotRem' a (IntegerCons False b))
type instance QuotRem'_3 b '(q', r') = QuotRem'_4 (r' >= b) b q' r'
type instance QuotRem'_4 True b q' r' = '(IntegerCons True q', r' `Minus` b)
type instance QuotRem'_4 False b q' r' = '(IntegerCons False q', r')

type Rem a b = Snd (QuotRem a b)
 
type Quot a b = Fst (QuotRem a b)

-- TODO: quot, div, mod, quotRem, divMod, toInteger