{-# LANGUAGE UndecidableInstances #-}

module Singleraeh.List where

import Data.Kind ( Type )
import Singleraeh.Demote

-- | Singleton list.
type SList :: (a -> Type) -> [a] -> Type
data SList sa as where
    SCons :: sa a -> SList sa as -> SList sa (a : as)
    SNil  ::                        SList sa '[]

demoteSList
    :: forall da sa as
    .  (forall a. sa a -> da)
    -> SList sa as
    -> [da]
demoteSList :: forall {a} da (sa :: a -> Type) (as :: [a]).
(forall (a :: a). sa a -> da) -> SList sa as -> [da]
demoteSList forall (a :: a). sa a -> da
demoteSA = \case
  SCons sa a
sa SList sa as
sas -> sa a -> da
forall (a :: a). sa a -> da
demoteSA sa a
sa da -> [da] -> [da]
forall a. a -> [a] -> [a]
: (forall (a :: a). sa a -> da) -> SList sa as -> [da]
forall {a} da (sa :: a -> Type) (as :: [a]).
(forall (a :: a). sa a -> da) -> SList sa as -> [da]
demoteSList sa a -> da
forall (a :: a). sa a -> da
demoteSA SList sa as
sas
  SList sa as
SNil         -> []

instance Demotable sa => Demotable (SList sa) where
    type Demote (SList sa) = [Demote sa]
    demote :: forall (k1 :: [a]). SList sa k1 -> Demote (SList sa)
demote = (forall (a :: a). sa a -> Demote sa) -> SList sa k1 -> [Demote sa]
forall {a} da (sa :: a -> Type) (as :: [a]).
(forall (a :: a). sa a -> da) -> SList sa as -> [da]
demoteSList sa a -> Demote sa
forall (a :: a). sa a -> Demote sa
forall k (sk :: k -> Type) (k1 :: k).
Demotable sk =>
sk k1 -> Demote sk
demote

-- | Reverse a type level list.
type Reverse as = Reverse' '[] as
type family Reverse' (acc :: [k]) (as :: [k]) :: [k] where
  Reverse' acc (a : as) = Reverse' (a : acc) as
  Reverse' acc '[]      = acc

sReverse :: SList sa as -> SList sa (Reverse as)
sReverse :: forall {k} (sa :: k -> Type) (as :: [k]).
SList sa as -> SList sa (Reverse as)
sReverse SList sa as
as = SList sa '[] -> SList sa as -> SList sa (Reverse' '[] as)
forall {k} (sa :: k -> Type) (acc :: [k]) (as :: [k]).
SList sa acc -> SList sa as -> SList sa (Reverse' acc as)
sReverse' SList sa '[]
forall {a} (sa :: a -> Type). SList sa '[]
SNil SList sa as
as

sReverse' :: SList sa acc -> SList sa as -> SList sa (Reverse' acc as)
sReverse' :: forall {k} (sa :: k -> Type) (acc :: [k]) (as :: [k]).
SList sa acc -> SList sa as -> SList sa (Reverse' acc as)
sReverse' SList sa acc
acc = \case
  SCons sa a
a SList sa as
as -> SList sa (a : acc)
-> SList sa as -> SList sa (Reverse' (a : acc) as)
forall {k} (sa :: k -> Type) (acc :: [k]) (as :: [k]).
SList sa acc -> SList sa as -> SList sa (Reverse' acc as)
sReverse' (sa a -> SList sa acc -> SList sa (a : acc)
forall {a} (sa :: a -> Type) (a :: a) (as :: [a]).
sa a -> SList sa as -> SList sa (a : as)
SCons sa a
a SList sa acc
acc) SList sa as
as
  SList sa as
SNil       -> SList sa acc
SList sa (Reverse' acc as)
acc