{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -Wno-orphans #-}

-----------------------------------------------------------------------------

-- |

-- Module      :  GHC.TypeLits.Singletons

-- Copyright   :  (C) 2014 Richard Eisenberg

-- License     :  BSD-style (see LICENSE)

-- Maintainer  :  Ryan Scott

-- Stability   :  experimental

-- Portability :  non-portable

--

-- Defines and exports singletons useful for the Natural, Symbol, and Char

-- kinds.

--

----------------------------------------------------------------------------


module GHC.TypeLits.Singletons (
  Natural, Symbol, Char,
  Sing,
  SNat, pattern SNat,
  SSymbol, pattern SSymbol, pattern SSym,
  SChar, pattern SChar,
  withKnownNat, withKnownSymbol, withKnownChar,
  Error, sError,
  ErrorWithoutStackTrace, sErrorWithoutStackTrace,
  Undefined, sUndefined,
  KnownNat, natVal,
  KnownSymbol, symbolVal,
  KnownChar, charVal,

  type (^), (%^),
  type (<=?), (%<=?),

  TN.Log2, sLog2,
  Div, sDiv, Mod, sMod, DivMod, sDivMod,
  Quot, sQuot, Rem, sRem, QuotRem, sQuotRem,

  consSymbol, ConsSymbol, sConsSymbol,
  unconsSymbol, UnconsSymbol, sUnconsSymbol,
  charToNat, CharToNat, sCharToNat,
  natToChar, NatToChar, sNatToChar,

  -- * Defunctionalization symbols

  ErrorSym0, ErrorSym1,
  ErrorWithoutStackTraceSym0, ErrorWithoutStackTraceSym1,
  UndefinedSym0,
  KnownNatSym0, KnownNatSym1,
  KnownSymbolSym0, KnownSymbolSym1,
  KnownCharSym0, KnownCharSym1,
  type (^@#@$), type (^@#@$$), type (^@#@$$$),
  type (<=?@#@$), type (<=?@#@$$), type (<=?@#@$$$),
  Log2Sym0, Log2Sym1,
  DivSym0, DivSym1, DivSym2,
  ModSym0, ModSym1, ModSym2,
  DivModSym0, DivModSym1, DivModSym2,
  QuotSym0, QuotSym1, QuotSym2,
  RemSym0, RemSym1, RemSym2,
  QuotRemSym0, QuotRemSym1, QuotRemSym2,
  ConsSymbolSym0, ConsSymbolSym1, ConsSymbolSym2,
  UnconsSymbolSym0, UnconsSymbolSym1,
  CharToNatSym0, CharToNatSym1,
  NatToCharSym0, NatToCharSym1
  ) where

import Data.Char (chr, ord)
import qualified Data.List as L (uncons)
import Data.Singletons
import Data.Singletons.TH
import Data.String (IsString(..))
import qualified Data.Text as T
import Data.Tuple.Singletons
import GHC.TypeLits ( CharToNat, ConsSymbol, NatToChar, UnconsSymbol
                    , withSomeSChar, withSomeSSymbol )
import GHC.TypeLits.Singletons.Internal
import qualified GHC.TypeNats as TN
import GHC.TypeNats (Div, Mod)
import Unsafe.Coerce

-- | This bogus instance is helpful for people who want to define

-- functions over Symbols that will only be used at the type level or

-- as singletons.

instance Eq Symbol where
  == :: Symbol -> Symbol -> Bool
(==)        = Symbol -> Symbol -> Bool
forall a. a
no_term_level_syms

instance Ord Symbol where
  compare :: Symbol -> Symbol -> Ordering
compare     = Symbol -> Symbol -> Ordering
forall a. a
no_term_level_syms

instance IsString Symbol where
  fromString :: String -> Symbol
fromString  = String -> Symbol
forall a. a
no_term_level_syms

instance Semigroup Symbol where
  <> :: Symbol -> Symbol -> Symbol
(<>) = Symbol -> Symbol -> Symbol
forall a. a
no_term_level_syms

instance Monoid Symbol where
  mempty :: Symbol
mempty = Symbol
forall a. a
no_term_level_syms

instance Show Symbol where
  showsPrec :: Int -> Symbol -> ShowS
showsPrec = Int -> Symbol -> ShowS
forall a. a
no_term_level_syms

no_term_level_syms :: a
no_term_level_syms :: forall a. a
no_term_level_syms = String -> a
forall a. HasCallStack => String -> a
error String
"The kind `Symbol` may not be used at the term level."

-- These are often useful in TypeLits-heavy code

$(genDefunSymbols [''KnownNat, ''KnownSymbol, ''KnownChar])

------------------------------------------------------------

-- Log2, Div, Mod, DivMod, and friends

------------------------------------------------------------


{- | Adapted from GHC's source code.

Compute the logarithm of a number in the given base, rounded down to the
closest integer. -}
genLog2 :: Natural -> Natural
genLog2 :: Natural -> Natural
genLog2 Natural
x = Natural -> Natural -> Natural
forall {t} {t}. (Num t, Integral t) => t -> t -> t
exactLoop Natural
0 Natural
x
  where
  exactLoop :: t -> t -> t
exactLoop t
s t
i
    | t
i t -> t -> Bool
forall a. Eq a => a -> a -> Bool
== t
1     = t
s
    | t
i t -> t -> Bool
forall a. Ord a => a -> a -> Bool
< t
2      = t
s
    | Bool
otherwise  =
        let s1 :: t
s1 = t
s t -> t -> t
forall a. Num a => a -> a -> a
+ t
1
        in t
s1 t -> t -> t
forall a b. a -> b -> b
`seq` case t -> t -> (t, t)
forall a. Integral a => a -> a -> (a, a)
divMod t
i t
2 of
                      (t
j,t
r)
                        | t
r t -> t -> Bool
forall a. Eq a => a -> a -> Bool
== t
0    -> t -> t -> t
exactLoop t
s1 t
j
                        | Bool
otherwise -> t -> t -> t
forall {t} {t}. (Num t, Integral t) => t -> t -> t
underLoop t
s1 t
j

  underLoop :: t -> t -> t
underLoop t
s t
i
    | t
i t -> t -> Bool
forall a. Ord a => a -> a -> Bool
< t
2  = t
s
    | Bool
otherwise = let s1 :: t
s1 = t
s t -> t -> t
forall a. Num a => a -> a -> a
+ t
1 in t
s1 t -> t -> t
forall a b. a -> b -> b
`seq` t -> t -> t
underLoop t
s1 (t -> t -> t
forall a. Integral a => a -> a -> a
div t
i t
2)


sLog2 :: Sing x -> Sing (TN.Log2 x)
sLog2 :: forall (x :: Natural). Sing x -> Sing (Log2 x)
sLog2 Sing x
sx =
    let x :: Demote Natural
x = Sing x -> Demote Natural
forall (a :: Natural). Sing a -> Demote Natural
forall k (a :: k). SingKind k => Sing a -> Demote k
fromSing Sing x
sx
    in case Demote Natural
x of
         Demote Natural
0 -> String -> SNat (Log2 x)
forall a. HasCallStack => String -> a
error String
"log2 of 0"
         Demote Natural
_ -> Natural
-> (forall (n :: Natural). SNat n -> SNat (Log2 x))
-> SNat (Log2 x)
forall r. Natural -> (forall (n :: Natural). SNat n -> r) -> r
TN.withSomeSNat (Natural -> Natural
genLog2 Natural
Demote Natural
x) SNat n -> SNat (Log2 x)
forall (n :: Natural). SNat n -> SNat (Log2 x)
forall a b. a -> b
unsafeCoerce
$(genDefunSymbols [''TN.Log2])
instance SingI Log2Sym0 where
  sing :: Sing Log2Sym0
sing = SingFunction1 Log2Sym0 -> Sing Log2Sym0
forall {a1} {b} (f :: a1 ~> b). SingFunction1 f -> Sing f
singFun1 Sing t -> Sing (Log2 t)
Sing t -> Sing (Apply Log2Sym0 t)
forall (x :: Natural). Sing x -> Sing (Log2 x)
SingFunction1 Log2Sym0
sLog2

sDiv :: Sing x -> Sing y -> Sing (Div x y)
sDiv :: forall (x :: Natural) (y :: Natural).
Sing x -> Sing y -> Sing (Div x y)
sDiv Sing x
sx Sing y
sy =
    let x :: Demote Natural
x = Sing x -> Demote Natural
forall (a :: Natural). Sing a -> Demote Natural
forall k (a :: k). SingKind k => Sing a -> Demote k
fromSing Sing x
sx
        y :: Demote Natural
y = Sing y -> Demote Natural
forall (a :: Natural). Sing a -> Demote Natural
forall k (a :: k). SingKind k => Sing a -> Demote k
fromSing Sing y
sy
    in Natural
-> (forall (n :: Natural). SNat n -> SNat (Div x y))
-> SNat (Div x y)
forall r. Natural -> (forall (n :: Natural). SNat n -> r) -> r
TN.withSomeSNat (Natural
Demote Natural
x Natural -> Natural -> Natural
forall a. Integral a => a -> a -> a
`div` Natural
Demote Natural
y) SNat n -> SNat (Div x y)
forall (n :: Natural). SNat n -> SNat (Div x y)
forall a b. a -> b
unsafeCoerce
infixl 7 `sDiv`
$(genDefunSymbols [''Div])
instance SingI DivSym0 where
  sing :: Sing DivSym0
sing = SingFunction2 DivSym0 -> Sing DivSym0
forall {a1} {a2} {b} (f :: a1 ~> (a2 ~> b)).
SingFunction2 f -> Sing f
singFun2 Sing t1 -> Sing t2 -> Sing (Div t1 t2)
Sing t1 -> Sing t2 -> Sing (Apply (Apply DivSym0 t1) t2)
forall (x :: Natural) (y :: Natural).
Sing x -> Sing y -> Sing (Div x y)
SingFunction2 DivSym0
sDiv
instance SingI x => SingI (DivSym1 x) where
  sing :: Sing (DivSym1 x)
sing = SingFunction1 (DivSym1 x) -> Sing (DivSym1 x)
forall {a1} {b} (f :: a1 ~> b). SingFunction1 f -> Sing f
singFun1 (SingFunction1 (DivSym1 x) -> Sing (DivSym1 x))
-> SingFunction1 (DivSym1 x) -> Sing (DivSym1 x)
forall a b. (a -> b) -> a -> b
$ Sing x -> Sing t -> Sing (Div x t)
forall (x :: Natural) (y :: Natural).
Sing x -> Sing y -> Sing (Div x y)
sDiv (forall (a :: Natural). SingI a => Sing a
forall {k} (a :: k). SingI a => Sing a
sing @x)
instance SingI1 DivSym1 where
  liftSing :: forall (x :: Natural). Sing x -> Sing (DivSym1 x)
liftSing Sing x
s = SingFunction1 (DivSym1 x) -> Sing (DivSym1 x)
forall {a1} {b} (f :: a1 ~> b). SingFunction1 f -> Sing f
singFun1 (SingFunction1 (DivSym1 x) -> Sing (DivSym1 x))
-> SingFunction1 (DivSym1 x) -> Sing (DivSym1 x)
forall a b. (a -> b) -> a -> b
$ Sing x -> Sing t -> Sing (Div x t)
forall (x :: Natural) (y :: Natural).
Sing x -> Sing y -> Sing (Div x y)
sDiv Sing x
s

sMod :: Sing x -> Sing y -> Sing (Mod x y)
sMod :: forall (x :: Natural) (y :: Natural).
Sing x -> Sing y -> Sing (Mod x y)
sMod Sing x
sx Sing y
sy =
    let x :: Demote Natural
x = Sing x -> Demote Natural
forall (a :: Natural). Sing a -> Demote Natural
forall k (a :: k). SingKind k => Sing a -> Demote k
fromSing Sing x
sx
        y :: Demote Natural
y = Sing y -> Demote Natural
forall (a :: Natural). Sing a -> Demote Natural
forall k (a :: k). SingKind k => Sing a -> Demote k
fromSing Sing y
sy
    in Natural
-> (forall (n :: Natural). SNat n -> SNat (Mod x y))
-> SNat (Mod x y)
forall r. Natural -> (forall (n :: Natural). SNat n -> r) -> r
TN.withSomeSNat (Natural
Demote Natural
x Natural -> Natural -> Natural
forall a. Integral a => a -> a -> a
`mod` Natural
Demote Natural
y) SNat n -> SNat (Mod x y)
forall (n :: Natural). SNat n -> SNat (Mod x y)
forall a b. a -> b
unsafeCoerce
infixl 7 `sMod`
$(genDefunSymbols [''Mod])
instance SingI ModSym0 where
  sing :: Sing ModSym0
sing = SingFunction2 ModSym0 -> Sing ModSym0
forall {a1} {a2} {b} (f :: a1 ~> (a2 ~> b)).
SingFunction2 f -> Sing f
singFun2 Sing t1 -> Sing t2 -> Sing (Mod t1 t2)
Sing t1 -> Sing t2 -> Sing (Apply (Apply ModSym0 t1) t2)
forall (x :: Natural) (y :: Natural).
Sing x -> Sing y -> Sing (Mod x y)
SingFunction2 ModSym0
sMod
instance SingI x => SingI (ModSym1 x) where
  sing :: Sing (ModSym1 x)
sing = SingFunction1 (ModSym1 x) -> Sing (ModSym1 x)
forall {a1} {b} (f :: a1 ~> b). SingFunction1 f -> Sing f
singFun1 (SingFunction1 (ModSym1 x) -> Sing (ModSym1 x))
-> SingFunction1 (ModSym1 x) -> Sing (ModSym1 x)
forall a b. (a -> b) -> a -> b
$ Sing x -> Sing t -> Sing (Mod x t)
forall (x :: Natural) (y :: Natural).
Sing x -> Sing y -> Sing (Mod x y)
sMod (Sing x -> Sing t -> Sing (Mod x t))
-> Sing x -> Sing t -> Sing (Mod x t)
forall a b. (a -> b) -> a -> b
$ forall (a :: Natural). SingI a => Sing a
forall {k} (a :: k). SingI a => Sing a
sing @x
instance SingI1 ModSym1 where
  liftSing :: forall (x :: Natural). Sing x -> Sing (ModSym1 x)
liftSing Sing x
s = SingFunction1 (ModSym1 x) -> Sing (ModSym1 x)
forall {a1} {b} (f :: a1 ~> b). SingFunction1 f -> Sing f
singFun1 (SingFunction1 (ModSym1 x) -> Sing (ModSym1 x))
-> SingFunction1 (ModSym1 x) -> Sing (ModSym1 x)
forall a b. (a -> b) -> a -> b
$ Sing x -> Sing t -> Sing (Mod x t)
forall (x :: Natural) (y :: Natural).
Sing x -> Sing y -> Sing (Mod x y)
sMod Sing x
s

$(promoteOnly [d|
  divMod :: Natural -> Natural -> (Natural, Natural)
  divMod x y = (div x y, mod x y)

  quotRem :: Natural -> Natural -> (Natural, Natural)
  quotRem = divMod

  quot :: Natural -> Natural -> Natural
  quot = div
  infixl 7 `quot`

  rem :: Natural -> Natural -> Natural
  rem = mod
  infixl 7 `rem`
  |])

sDivMod :: Sing x -> Sing y -> Sing (DivMod x y)
sDivMod :: forall (x :: Natural) (y :: Natural).
Sing x -> Sing y -> Sing (DivMod x y)
sDivMod Sing x
sx Sing y
sy =
    let x :: Demote Natural
x     = Sing x -> Demote Natural
forall (a :: Natural). Sing a -> Demote Natural
forall k (a :: k). SingKind k => Sing a -> Demote k
fromSing Sing x
sx
        y :: Demote Natural
y     = Sing y -> Demote Natural
forall (a :: Natural). Sing a -> Demote Natural
forall k (a :: k). SingKind k => Sing a -> Demote k
fromSing Sing y
sy
        (Natural
q,Natural
r) = Natural
Demote Natural
x Natural -> Natural -> (Natural, Natural)
forall a. Integral a => a -> a -> (a, a)
`divMod` Natural
Demote Natural
y
    in Natural
-> (forall {n :: Natural}. SNat n -> Sing (DivMod x y))
-> Sing (DivMod x y)
forall r. Natural -> (forall (n :: Natural). SNat n -> r) -> r
TN.withSomeSNat Natural
q ((forall {n :: Natural}. SNat n -> Sing (DivMod x y))
 -> Sing (DivMod x y))
-> (forall {n :: Natural}. SNat n -> Sing (DivMod x y))
-> Sing (DivMod x y)
forall a b. (a -> b) -> a -> b
$ \SNat n
sq ->
       Natural
-> (forall {n :: Natural}. SNat n -> Sing (DivMod x y))
-> Sing (DivMod x y)
forall r. Natural -> (forall (n :: Natural). SNat n -> r) -> r
TN.withSomeSNat Natural
r ((forall {n :: Natural}. SNat n -> Sing (DivMod x y))
 -> Sing (DivMod x y))
-> (forall {n :: Natural}. SNat n -> Sing (DivMod x y))
-> Sing (DivMod x y)
forall a b. (a -> b) -> a -> b
$ \SNat n
sr ->
       STuple2 '(n, n) -> STuple2 '(Div x y, Mod x y)
forall a b. a -> b
unsafeCoerce (Sing n -> Sing n -> STuple2 '(n, n)
forall a b (n1 :: a) (n2 :: b).
Sing n1 -> Sing n2 -> STuple2 '(n1, n2)
STuple2 Sing n
SNat n
sq Sing n
SNat n
sr)

sQuotRem :: Sing x -> Sing y -> Sing (QuotRem x y)
sQuotRem :: forall (x :: Natural) (y :: Natural).
Sing x -> Sing y -> Sing (QuotRem x y)
sQuotRem = Sing x -> Sing y -> Sing (DivMod x y)
Sing x -> Sing y -> Sing (QuotRem x y)
forall (x :: Natural) (y :: Natural).
Sing x -> Sing y -> Sing (DivMod x y)
sDivMod

sQuot :: Sing x -> Sing y -> Sing (Quot x y)
sQuot :: forall (x :: Natural) (y :: Natural).
Sing x -> Sing y -> Sing (Quot x y)
sQuot = Sing x -> Sing y -> Sing (Div x y)
Sing x -> Sing y -> Sing (Quot x y)
forall (x :: Natural) (y :: Natural).
Sing x -> Sing y -> Sing (Div x y)
sDiv
infixl 7 `sQuot`

sRem :: Sing x -> Sing y -> Sing (Rem x y)
sRem :: forall (x :: Natural) (y :: Natural).
Sing x -> Sing y -> Sing (Rem x y)
sRem = Sing x -> Sing y -> Sing (Mod x y)
Sing x -> Sing y -> Sing (Rem x y)
forall (x :: Natural) (y :: Natural).
Sing x -> Sing y -> Sing (Mod x y)
sMod
infixl 7 `sRem`

consSymbol :: Char -> String -> String
consSymbol :: Char -> ShowS
consSymbol = (:)

sConsSymbol :: Sing x -> Sing y -> Sing (ConsSymbol x y)
sConsSymbol :: forall (x :: Char) (y :: Symbol).
Sing x -> Sing y -> Sing (ConsSymbol x y)
sConsSymbol Sing x
sx Sing y
sy =
    let x :: Demote Char
x = Sing x -> Demote Char
forall (a :: Char). Sing a -> Demote Char
forall k (a :: k). SingKind k => Sing a -> Demote k
fromSing Sing x
sx
        y :: String
y = Text -> String
T.unpack (Sing y -> Demote Symbol
forall k (a :: k). SingKind k => Sing a -> Demote k
forall (a :: Symbol). Sing a -> Demote Symbol
fromSing Sing y
sy)
    in String
-> (forall (s :: Symbol). SSymbol s -> SSymbol (ConsSymbol x y))
-> SSymbol (ConsSymbol x y)
forall r. String -> (forall (s :: Symbol). SSymbol s -> r) -> r
withSomeSSymbol (Char -> ShowS
consSymbol Char
Demote Char
x String
y) SSymbol s -> SSymbol (ConsSymbol x y)
forall a b. a -> b
forall (s :: Symbol). SSymbol s -> SSymbol (ConsSymbol x y)
unsafeCoerce
$(genDefunSymbols [''ConsSymbol])
instance SingI ConsSymbolSym0 where
  sing :: Sing ConsSymbolSym0
sing = SingFunction2 ConsSymbolSym0 -> Sing ConsSymbolSym0
forall {a1} {a2} {b} (f :: a1 ~> (a2 ~> b)).
SingFunction2 f -> Sing f
singFun2 Sing t1 -> Sing t2 -> Sing (ConsSymbol t1 t2)
Sing t1 -> Sing t2 -> Sing (Apply (Apply ConsSymbolSym0 t1) t2)
forall (x :: Char) (y :: Symbol).
Sing x -> Sing y -> Sing (ConsSymbol x y)
SingFunction2 ConsSymbolSym0
sConsSymbol
instance SingI x => SingI (ConsSymbolSym1 x) where
  sing :: Sing (ConsSymbolSym1 x)
sing = SingFunction1 (ConsSymbolSym1 x) -> Sing (ConsSymbolSym1 x)
forall {a1} {b} (f :: a1 ~> b). SingFunction1 f -> Sing f
singFun1 (SingFunction1 (ConsSymbolSym1 x) -> Sing (ConsSymbolSym1 x))
-> SingFunction1 (ConsSymbolSym1 x) -> Sing (ConsSymbolSym1 x)
forall a b. (a -> b) -> a -> b
$ Sing x -> Sing t -> Sing (ConsSymbol x t)
forall (x :: Char) (y :: Symbol).
Sing x -> Sing y -> Sing (ConsSymbol x y)
sConsSymbol (Sing x -> Sing t -> Sing (ConsSymbol x t))
-> Sing x -> Sing t -> Sing (ConsSymbol x t)
forall a b. (a -> b) -> a -> b
$ forall (a :: Char). SingI a => Sing a
forall {k} (a :: k). SingI a => Sing a
sing @x
instance SingI1 ConsSymbolSym1 where
  liftSing :: forall (x :: Char). Sing x -> Sing (ConsSymbolSym1 x)
liftSing Sing x
s = SingFunction1 (ConsSymbolSym1 x) -> Sing (ConsSymbolSym1 x)
forall {a1} {b} (f :: a1 ~> b). SingFunction1 f -> Sing f
singFun1 (SingFunction1 (ConsSymbolSym1 x) -> Sing (ConsSymbolSym1 x))
-> SingFunction1 (ConsSymbolSym1 x) -> Sing (ConsSymbolSym1 x)
forall a b. (a -> b) -> a -> b
$ Sing x -> Sing t -> Sing (ConsSymbol x t)
forall (x :: Char) (y :: Symbol).
Sing x -> Sing y -> Sing (ConsSymbol x y)
sConsSymbol Sing x
s

unconsSymbol :: String -> Maybe (Char, String)
unconsSymbol :: String -> Maybe (Char, String)
unconsSymbol = String -> Maybe (Char, String)
forall a. [a] -> Maybe (a, [a])
L.uncons

sUnconsSymbol :: Sing x -> Sing (UnconsSymbol x)
sUnconsSymbol :: forall (x :: Symbol). Sing x -> Sing (UnconsSymbol x)
sUnconsSymbol Sing x
sx =
    let x :: String
x   = Text -> String
T.unpack (Sing x -> Demote Symbol
forall k (a :: k). SingKind k => Sing a -> Demote k
forall (a :: Symbol). Sing a -> Demote Symbol
fromSing Sing x
sx)
        res :: SomeSing (Maybe (Char, String))
res = Demote (Maybe (Char, String)) -> SomeSing (Maybe (Char, String))
forall k. SingKind k => Demote k -> SomeSing k
toSing (String -> Maybe (Char, String)
unconsSymbol String
x)
    in case SomeSing (Maybe (Char, String))
res of
         SomeSing Sing a
s -> SMaybe a -> SMaybe (UnconsSymbol x)
forall a b. a -> b
unsafeCoerce Sing a
SMaybe a
s
$(genDefunSymbols [''UnconsSymbol])
instance SingI UnconsSymbolSym0 where
  sing :: Sing UnconsSymbolSym0
sing = SingFunction1 UnconsSymbolSym0 -> Sing UnconsSymbolSym0
forall {a1} {b} (f :: a1 ~> b). SingFunction1 f -> Sing f
singFun1 Sing t -> Sing (UnconsSymbol t)
Sing t -> Sing (Apply UnconsSymbolSym0 t)
forall (x :: Symbol). Sing x -> Sing (UnconsSymbol x)
SingFunction1 UnconsSymbolSym0
sUnconsSymbol

charToNat :: Char -> Natural
charToNat :: Char -> Natural
charToNat = Int -> Natural
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int -> Natural) -> (Char -> Int) -> Char -> Natural
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Char -> Int
ord

sCharToNat :: Sing x -> Sing (CharToNat x)
sCharToNat :: forall (x :: Char). Sing x -> Sing (CharToNat x)
sCharToNat Sing x
sx =
    let x :: Demote Char
x = Sing x -> Demote Char
forall (a :: Char). Sing a -> Demote Char
forall k (a :: k). SingKind k => Sing a -> Demote k
fromSing Sing x
sx
    in Natural
-> (forall (n :: Natural). SNat n -> SNat (CharToNat x))
-> SNat (CharToNat x)
forall r. Natural -> (forall (n :: Natural). SNat n -> r) -> r
TN.withSomeSNat (Char -> Natural
charToNat Char
Demote Char
x) SNat n -> SNat (CharToNat x)
forall (n :: Natural). SNat n -> SNat (CharToNat x)
forall a b. a -> b
unsafeCoerce
$(genDefunSymbols [''CharToNat])
instance SingI CharToNatSym0 where
  sing :: Sing CharToNatSym0
sing = SingFunction1 CharToNatSym0 -> Sing CharToNatSym0
forall {a1} {b} (f :: a1 ~> b). SingFunction1 f -> Sing f
singFun1 Sing t -> Sing (CharToNat t)
Sing t -> Sing (Apply CharToNatSym0 t)
forall (x :: Char). Sing x -> Sing (CharToNat x)
SingFunction1 CharToNatSym0
sCharToNat

natToChar :: Natural -> Char
natToChar :: Natural -> Char
natToChar = Int -> Char
chr (Int -> Char) -> (Natural -> Int) -> Natural -> Char
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Natural -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral

sNatToChar :: Sing x -> Sing (NatToChar x)
sNatToChar :: forall (x :: Natural). Sing x -> Sing (NatToChar x)
sNatToChar Sing x
sx =
    let x :: Demote Natural
x = Sing x -> Demote Natural
forall (a :: Natural). Sing a -> Demote Natural
forall k (a :: k). SingKind k => Sing a -> Demote k
fromSing Sing x
sx
    in Char
-> (forall (c :: Char). SChar c -> SChar (NatToChar x))
-> SChar (NatToChar x)
forall r. Char -> (forall (c :: Char). SChar c -> r) -> r
withSomeSChar (Natural -> Char
natToChar Natural
Demote Natural
x) SChar c -> SChar (NatToChar x)
forall (c :: Char). SChar c -> SChar (NatToChar x)
forall a b. a -> b
unsafeCoerce
$(genDefunSymbols [''NatToChar])
instance SingI NatToCharSym0 where
  sing :: Sing NatToCharSym0
sing = SingFunction1 NatToCharSym0 -> Sing NatToCharSym0
forall {a1} {b} (f :: a1 ~> b). SingFunction1 f -> Sing f
singFun1 Sing t -> Sing (NatToChar t)
Sing t -> Sing (Apply NatToCharSym0 t)
forall (x :: Natural). Sing x -> Sing (NatToChar x)
SingFunction1 NatToCharSym0
sNatToChar