module Data.HSet.TypeLevel
       ( Nat(..)
       , Elem
       , Index
       , MayIndexGo
       , MayIndex
       , MayFstIndexSnd
       , TEq
       , Length
       , Append
       , XReverse
       , Reverse
       , Delete
       , And
       , HSubset
       ) where

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)

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)

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)