{-# OPTIONS_HADDOCK hide, prune     #-}
{-# LANGUAGE DataKinds              #-}
{-# LANGUAGE FlexibleContexts       #-}
{-# LANGUAGE FlexibleInstances      #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE PolyKinds              #-}
{-# LANGUAGE TypeFamilyDependencies #-}
{-# LANGUAGE TypeOperators          #-}
{-# LANGUAGE UndecidableInstances   #-}
module Data.Type.List.Families
  ( Head, Tail
  , Snoc, Init, Last, Reverse
  , StripSuffix, StripPrefix, Concat
    -- * Internals
  , List (..), RunList, Snoc', Reverse'
  ) where


-- | Extract the first element of a list, which must be non-empty.
type family Head (xs :: [k]) :: k where
    Head (x ': _)     = x

-- | Extract the elements after the head of a list, which must be non-empty.
type family Tail (xs :: [k]) :: [k] where
    Tail (_ ': xs)    = xs

-- | Extract the last element of a list, which must be non-empty.
type family Last (xs :: [k]) :: k where
    Last '[x]         = x
    Last (_ ': xs)    = Last xs

-- | Extract all but last elements of a list, which must be non-empty.
type family Init (xs :: [k]) = (ys :: [k]) | ys -> k where
    Init ('[x] :: [k]) = ('[] :: [k])
    Init (x ': xs)     = x ': Init xs

-- | Appending a list on the other side (injective).
type Snoc (xs :: [k]) (x :: k) = (RunList (Snoc' xs x :: List k) :: [k])

-- | Reverse elements of a list (injective).
type Reverse (xs :: [k]) = (RunList (Reverse' xs :: List k) :: [k])

-- | A helper data type that makes possible injective `Snoc` and `Reverse` families.
--
--   It assures GHC type checker that the `Snoc` operation on a non-empty list
--   yields a list that contains at least two elements.
data List k
  = Empty
  | Single k
  | TwoOrMore [k]
    -- ^ An important invariant: the argument list contains at least two elements.

type family RunList (xs :: List k) = (ys :: [k]) | ys -> k xs where
    RunList ('Empty :: List k)          = ('[] :: [k])
    RunList ('Single x)                 = '[x]
    RunList ('TwoOrMore (x ': y ': xs)) = x ': y ': xs

type family Snoc' (xs :: [k]) (x :: k) = (ys :: List k) | ys -> k xs x where
    Snoc' '[]       y = 'Single y
    Snoc' (x ': xs) y = 'TwoOrMore (x ': RunList (Snoc' xs y))

type family Reverse' (xs :: [k]) = (ys :: List k) | ys -> k xs where
    Reverse' ('[] :: [k])   = ('Empty :: List k)
    Reverse' '[x]           = 'Single x
    Reverse' (y ': x ': xs) = 'TwoOrMore (Snoc (RunList (Reverse' (x ': xs))) y)


-- | Append two lists.
type family Concat (as :: [k]) (bs :: [k]) :: [k] where
    Concat  as       '[]       = as -- "incoherent instance"
    Concat '[]        bs       = bs
    Concat (a ': as)  bs       = a ': Concat as bs

-- | Remove prefix @as@ from a list @asbs@ if @as@ is a prefix; fail otherwise.
type family StripPrefix (as :: [k]) (asbs :: [k]) :: [k] where
    StripPrefix  as        as         = '[] -- "incoherent instance"
    StripPrefix '[]        bs         = bs
    StripPrefix (a ': as) (a ': asbs) = StripPrefix as asbs

-- | Remove suffix @bs@ from a list @asbs@ if @bs@ is a suffix; fail otherwise.
type family StripSuffix (bs :: [k]) (asbs :: [k]) :: [k] where
    StripSuffix '[]        as         = as -- "incoherent instance"
    StripSuffix  bs        bs         = '[]
    StripSuffix  bs       (a ': asbs) = a ': StripSuffix bs asbs