{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE UndecidableInstances #-}
-- | List utilities at the type-level.
module Language.Symantic.Helper.Data.Type.List where

import GHC.Exts (Constraint)

import Language.Symantic.Helper.Data.Type.Peano

-- ** Type 'Index'
-- | Return the position of a type within a list of them.
-- This is useful to work around @OverlappingInstances@.
type family Index xs x where
	Index (x     ': xs) x = Zero
	Index (not_x ': xs) x = Succ (Index xs x)

-- * Type family @(++)@
type family (++) xs ys where
	'[] ++ ys = ys
	(x ': xs) ++ ys = x ': xs ++ ys
infixr 5 ++

-- * Type family 'Concat'
type family Concat (xs::[[k]]) :: [k] where
	Concat '[] = '[]
	Concat (x ': xs) = x ++ Concat xs

-- * Type family 'Concat_Constraints'
type family Concat_Constraints (cs::[Constraint]) :: Constraint where
	Concat_Constraints '[] = ()
	Concat_Constraints (c ': cs) = (c, Concat_Constraints cs)

-- * Type family 'DeleteAll'
type family DeleteAll (x::k) (xs::[k]) :: [k] where
	DeleteAll x '[] = '[]
	DeleteAll x (x ': xs) = DeleteAll x xs
	DeleteAll x (y ': xs) = y ': DeleteAll x xs

-- * Type family 'Head'
type family Head (xs::[k]) :: k where
	Head (x ': _xs) = x

-- * Type family 'Tail'
type family Tail (xs::[k]) :: [k] where
	Tail (_x ': xs) = xs

-- * Type family 'Map'
type family Map (f::a -> b) (cs::[a]) :: [b] where
	Map f '[] = '[]
	Map f (c ': cs) = f c ': Map f cs

-- * Type family 'Nub'
type family Nub (xs::[k]) :: [k] where
	Nub '[] = '[]
	Nub (x ': xs) = x ': Nub (DeleteAll x xs)