module Data.HSet.TypeLevel
       ( Nat(..)
       , Elem
       , Index
       , MayIndexGo
       , MayIndex
       , MayFstIndexSnd
       , TEq
       , Length
       , Append
       , AppendUniq
       , Union
       , UnionList'
       , UnionList
       , XReverse
       , Reverse
       , Delete
       , Replace
       , TagElem
       , And
       , HSubset
       ) where

import Data.Tagged

data Nat = Z | S Nat

-- | Calculates to 'True if first type argument contained in second
-- list element
type family Elem (typ :: k) (typs :: [k]) :: Bool where
    Elem typ '[]             = 'False
    Elem typ (typ ': typs)   = 'True
    Elem typ1 (typ2 ': typs) = Elem typ1 typs

-- | Calculates to Nat kinded type describing the index of first
-- argument in second argument
type family Index (typ :: k) (typs :: [k]) :: Nat where
  Index t (t ': ts) = 'Z
  Index t (tt ': ts) = 'S (Index t ts)


type family MayIndexGo (typ :: k) (typs :: [k]) (acc :: Nat) :: (Maybe Nat) where
  MayIndexGo t (t ': ts)  acc = 'Just acc
  MayIndexGo t (tt ': ts) acc = MayIndexGo t ts ('S acc)
  MayIndexGo t '[]        acc = 'Nothing

type MayIndex typ typs = MayIndexGo typ typs 'Z


type family MayFstIndexSnd (ts1 :: [k]) (ts2 :: [k]) :: (Maybe Nat) where
  MayFstIndexSnd (e ': els) x = MayIndex e x
  MayFstIndexSnd '[] x        = 'Nothing

type family TEq (t1 :: k) (t2 :: k) :: Bool where
  TEq a a = 'True
  TEq a b = 'False

-- | Type level list length
type family Length (list :: [*]) :: Nat where
  Length '[] = 'Z
  Length (x ': xs) = 'S (Length xs)

type family Append (l1 :: [*]) (l2 :: [*]) :: [*] where
  Append '[] x = x
  Append x '[] = x
  Append (x ': xs) ys = x ': (Append xs ys)

-- | Append element to type list if element is not presented in list
-- already
type family AppendUniq (typs :: [*]) (typ :: *) :: [*] where
  AppendUniq (t ': ts) t = t ': ts
  AppendUniq (t ': ts) t1 = t ': (AppendUniq ts t1)
  AppendUniq '[] t1 = '[t1]

-- | Calculates union two lists
type family Union (l1 :: [*]) (l2 :: [*]) :: [*] where
  Union l1 '[] = l1
  Union l1 (l ': ls) = Union (AppendUniq l1 l) ls

type family UnionList' (acc :: [*]) (ls :: [[*]]) :: [*] where
  UnionList' acc (e ': es) = UnionList' (Union acc e) es
  UnionList' acc '[] = acc

-- | Union list of lists of elements. Return just unique elements of
-- each nested list
type UnionList l = UnionList' '[] l

type family XReverse (acc :: [*]) (l :: [*]) :: [*] where
  XReverse acc '[] = acc
  XReverse acc (e ': els) = XReverse (e ': acc) els

-- | Reverse list of elements
type Reverse a = XReverse '[] a

-- | Delete element from type list
type family Delete (typ :: *) (typs :: [*]) :: [*] where
  Delete x '[] = '[]
  Delete x (x ': ys) = Delete x ys
  Delete x (y ': ys) = y ': (Delete x ys)

-- | Replace first arbitrary element 'typ1' in type list with 'typ2'
type family Replace (typ1 :: *) (typ2 :: *) (typs :: [*]) :: [*] where
  Replace a b (a ': xs) = (b ': xs)
  Replace a b (x ': xs) = x ': (Replace a b xs)

-- | Wrap first element with __Tagged tag__
type TagElem (tag :: k) (typ :: *) (typs :: [*])
  = Replace typ (Tagged tag typ) typs

type family And (a :: Bool) (b :: Bool) where
  And 'False x      = 'False
  And x      'False = 'False
  And x      y      = 'True

-- | Checks if the former subset included in the latter one.
type family HSubset (h1 :: [k]) (h2 :: [k]) where
  HSubset '[]         x   = 'True
  HSubset x           '[] = 'False
  HSubset (h1 ': tl2) h2  = And (Elem h1 h2) (HSubset tl2 h2)