{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE UndecidableInstances #-}
-- | List utilities at the type-level.
module Language.Symantic.Typing.List where

import GHC.Exts (Constraint)

import Language.Symantic.Typing.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
        -- xs  ++ '[] = xs
        (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)

{-
-- * Type family 'L'
type family L (xs::[k]) :: Nat where
	L '[] = 'Z
	L (x ': xs) = 'S (L xs)

-- ** Class 'LInj'
class LInj (as::[k]) where
	lInj :: SNat (L as)
instance LInj '[] where
	lInj = SNatZ
instance LInj as => LInj (a ': as) where
	lInj = SNatS (lInj @_ @as)
-}

-- * Type 'Len'
data Len (xs::[k]) where
        LenZ :: Len '[]
        LenS :: Len xs -> Len (x ': xs)

instance Show (Len vs) where
        showsPrec _p = showsPrec 10 . intLen

addLen :: Len a -> Len b -> Len (a ++ b)
addLen LenZ     b = b
addLen (LenS a) b = LenS $ addLen a b

shiftLen ::
 forall t b a.
 Len a ->
 Len (a ++      b) ->
 Len (a ++ t ': b)
shiftLen LenZ b = LenS b
shiftLen (LenS a) (LenS b) = LenS $ shiftLen @t @b a b

intLen :: Len xs -> Int
intLen = go 0
        where
        go :: Int -> Len xs -> Int
        go i LenZ     = i
        go i (LenS l) = go (1 + i) l

-- ** Class 'LenInj'
class LenInj (vs::[k]) where
        lenInj :: Len vs
instance LenInj '[] where
        lenInj = LenZ
instance LenInj as => LenInj (a ': as) where
        lenInj = LenS lenInj