{-# LANGUAGE DataKinds #-}
{-# LANGUAGE NoStarIsType #-}
{-# LANGUAGE TypeOperators #-}
module GHC.TypeLits.Experimental (
    appendSSymbol,
    consSSymbol,
    sCharToSNat,
    sNatToSChar,
) where

import GHC.Internal.TypeLits
import Data.Char (ord, chr)

appendSSymbol :: SSymbol a -> SSymbol b -> SSymbol (AppendSymbol a b)
appendSSymbol :: forall (a :: Symbol) (b :: Symbol).
SSymbol a -> SSymbol b -> SSymbol (AppendSymbol a b)
appendSSymbol (UnsafeSSymbol String
a) (UnsafeSSymbol String
b) = String -> SSymbol (AppendSymbol a b)
forall (s :: Symbol). String -> SSymbol s
UnsafeSSymbol (String
a String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
b)

consSSymbol :: SChar a -> SSymbol b -> SSymbol (ConsSymbol a b)
consSSymbol :: forall (a :: Char) (b :: Symbol).
SChar a -> SSymbol b -> SSymbol (ConsSymbol a b)
consSSymbol (UnsafeSChar Char
a) (UnsafeSSymbol String
b) = String -> SSymbol (ConsSymbol a b)
forall (s :: Symbol). String -> SSymbol s
UnsafeSSymbol (Char
a Char -> String -> String
forall a. a -> [a] -> [a]
: String
b)

sCharToSNat :: SChar a -> SNat (CharToNat a)
sCharToSNat :: forall (a :: Char). SChar a -> SNat (CharToNat a)
sCharToSNat (UnsafeSChar Char
a) = Natural -> SNat (CharToNat a)
forall (n :: Natural). Natural -> SNat n
UnsafeSNat (Int -> Natural
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Char -> Int
ord Char
a))

sNatToSChar :: (n <= 1114111) => SNat n -> SChar (NatToChar n)
sNatToSChar :: forall (n :: Natural).
(n <= 1114111) =>
SNat n -> SChar (NatToChar n)
sNatToSChar (UnsafeSNat Natural
n) = Char -> SChar (NatToChar n)
forall (c :: Char). Char -> SChar c
UnsafeSChar (Int -> Char
chr (Natural -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Natural
n))