{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE Trustworthy #-}
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)
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))