{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE Trustworthy #-}
{-|
Module:      Data.Eliminator.TypeLits
Copyright:   (C) 2022 Ryan Scott
License:     BSD-style (see the file LICENSE)
Maintainer:  Ryan Scott
Stability:   Experimental
Portability: GHC

Crude imitations of eliminator functions for 'GHC.TypeLits.Nat' and
'GHC.TypeLits.Symbol'.
-}
module Data.Eliminator.TypeLits
  ( elimNat
  , elimSymbol
  ) where

import Data.Eliminator.TypeNats
import Data.Kind (Type)
import Data.Singletons
import qualified Data.Text as T

import GHC.TypeLits.Singletons ()
import GHC.TypeLits

import Unsafe.Coerce (unsafeCoerce)

-- | Although 'Nat' is not actually an inductive data type in GHC, we can
-- (crudely) pretend that it is using this eliminator.
elimSymbol :: forall (p :: Symbol ~> Type) (s :: Symbol).
              Sing s
           -> Apply p ""
           -> (forall (c :: Char) (ss :: Symbol).
                 Sing c -> Sing ss -> Apply p ss ->
                 Apply p (ConsSymbol c ss))
           -> Apply p s
elimSymbol :: forall (p :: Symbol ~> *) (s :: Symbol).
Sing s
-> Apply p ""
-> (forall (c :: Char) (ss :: Symbol).
    Sing c -> Sing ss -> Apply p ss -> Apply p (ConsSymbol c ss))
-> Apply p s
elimSymbol Sing s
ssym Apply p ""
pNil forall (c :: Char) (ss :: Symbol).
Sing c -> Sing ss -> Apply p ss -> Apply p (ConsSymbol c ss)
pCons = forall (s' :: Symbol). Sing s' -> Apply p s'
go @s Sing s
ssym
  where
    go :: forall (s' :: Symbol). Sing s' -> Apply p s'
    go :: forall (s' :: Symbol). Sing s' -> Apply p s'
go Sing s'
ssym' =
      case Text -> Maybe (Char, Text)
T.uncons (Sing s' -> Demote Symbol
forall k (a :: k). SingKind k => Sing a -> Demote k
forall (a :: Symbol). Sing a -> Demote Symbol
fromSing Sing s'
ssym') of
        Maybe (Char, Text)
Nothing      -> Apply p "" -> Apply p s'
forall a b. a -> b
unsafeCoerce Apply p ""
pNil
        Just (Char
c, Text
ss) -> Demote Char
-> (forall (a :: Char). Sing a -> Apply p s') -> Apply p s'
forall k r.
SingKind k =>
Demote k -> (forall (a :: k). Sing a -> r) -> r
withSomeSing Char
Demote Char
c  ((forall (a :: Char). Sing a -> Apply p s') -> Apply p s')
-> (forall (a :: Char). Sing a -> Apply p s') -> Apply p s'
forall a b. (a -> b) -> a -> b
$ \(Sing a
sc  :: Sing c)  ->
                        Demote Symbol
-> (forall (a :: Symbol). Sing a -> Apply p s') -> Apply p s'
forall k r.
SingKind k =>
Demote k -> (forall (a :: k). Sing a -> r) -> r
withSomeSing Demote Symbol
Text
ss ((forall (a :: Symbol). Sing a -> Apply p s') -> Apply p s')
-> (forall (a :: Symbol). Sing a -> Apply p s') -> Apply p s'
forall a b. (a -> b) -> a -> b
$ \(Sing a
sss :: Sing ss) ->
                          Apply p (ConsSymbol a a) -> Apply p s'
forall a b. a -> b
unsafeCoerce (Sing a -> Sing a -> Apply p a -> Apply p (ConsSymbol a a)
forall (c :: Char) (ss :: Symbol).
Sing c -> Sing ss -> Apply p ss -> Apply p (ConsSymbol c ss)
pCons Sing a
sc Sing a
sss (forall (s' :: Symbol). Sing s' -> Apply p s'
go @ss Sing a
sss))