module Data.HSet.TypeLevel
       ( Nat(..)
       , Elem
       , Index
       , TEq
       , Length
       , Append
       , Delete
       , FirstEQ
       , FirstContains
       , 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 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)

-- | 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)

-- | First elements of two lists are equal?
type family FirstEQ (list1 :: [*]) (list2 :: [*]) :: Bool where
  FirstEQ '[] '[]             = 'False
  FirstEQ '[] x               = 'False
  FirstEQ x '[]               = 'False
  FirstEQ (x ': xs) (x ': ys) = 'True
  FirstEQ (x ': xs) (y ': ys) = 'False

type family FirstContains (list1 :: [*]) (list2 :: [*]) :: Bool where
  FirstContains '[] x         = 'False
  FirstContains x '[]         = 'False
  FirstContains (x ': xs) els = Elem x els

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)