{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE CPP #-}
-- | Utilities for working with 'KnownChar' constraints.
--
-- This module is only available on GHC 9.2 or later.
module Data.Constraint.Char
  ( CharToNat
  , NatToChar
  , charToNat
  , natToChar
  ) where

import Data.Char
import Data.Constraint
import Data.Proxy
import GHC.TypeLits
#if MIN_VERSION_base(4,18,0)
import Data.Constraint.Unsafe
import qualified GHC.TypeNats as TN
#else
import Unsafe.Coerce
#endif

-- implementation details

#if !MIN_VERSION_base(4,18,0)
newtype Magic c = Magic (KnownChar c => Dict (KnownChar c))
#endif

magicCN :: forall c n. (Char -> Int) -> KnownChar c :- KnownNat n
#if MIN_VERSION_base(4,18,0)
magicCN :: forall (c :: Char) (n :: Nat).
(Char -> Int) -> KnownChar c :- KnownNat n
magicCN Char -> Int
f = (KnownChar c => Dict (KnownNat n)) -> KnownChar c :- KnownNat n
forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
Sub ((KnownChar c => Dict (KnownNat n)) -> KnownChar c :- KnownNat n)
-> (KnownChar c => Dict (KnownNat n)) -> KnownChar c :- KnownNat n
forall a b. (a -> b) -> a -> b
$ SNat n -> (KnownNat n => Dict (KnownNat n)) -> Dict (KnownNat n)
forall (n :: Nat) r. SNat n -> (KnownNat n => r) -> r
TN.withKnownNat (forall (n :: Nat). Nat -> SNat n
unsafeSNat @n (Int -> Nat
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Char -> Int
f (Proxy c -> Char
forall (n :: Char) (proxy :: Char -> *).
KnownChar n =>
proxy n -> Char
charVal (forall (t :: Char). Proxy t
forall {k} (t :: k). Proxy t
Proxy @c))))) Dict (KnownNat n)
KnownNat n => Dict (KnownNat n)
forall (a :: Constraint). a => Dict a
Dict
#else
magicCN f = Sub $ unsafeCoerce (Magic Dict) (fromIntegral @Int @Natural (f (charVal (Proxy @c))))
#endif

magicNC :: forall n c. (Int -> Char) -> KnownNat n :- KnownChar c
#if MIN_VERSION_base(4,18,0)
magicNC :: forall (n :: Nat) (c :: Char).
(Int -> Char) -> KnownNat n :- KnownChar c
magicNC Int -> Char
f = (KnownNat n => Dict (KnownChar c)) -> KnownNat n :- KnownChar c
forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
Sub ((KnownNat n => Dict (KnownChar c)) -> KnownNat n :- KnownChar c)
-> (KnownNat n => Dict (KnownChar c)) -> KnownNat n :- KnownChar c
forall a b. (a -> b) -> a -> b
$ SChar c
-> (KnownChar c => Dict (KnownChar c)) -> Dict (KnownChar c)
forall (c :: Char) r. SChar c -> (KnownChar c => r) -> r
withKnownChar (forall (c :: Char). Char -> SChar c
unsafeSChar @c (Int -> Char
f (Integer -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Proxy n -> Integer
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
natVal (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @n))))) Dict (KnownChar c)
KnownChar c => Dict (KnownChar c)
forall (a :: Constraint). a => Dict a
Dict
#else
magicNC f = Sub $ unsafeCoerce (Magic Dict) (f (fromIntegral (natVal (Proxy @n))))
#endif

-- operations

charToNat :: forall c. KnownChar c :- KnownNat (CharToNat c)
charToNat :: forall (c :: Char). KnownChar c :- KnownNat (CharToNat c)
charToNat = (Char -> Int) -> KnownChar c :- KnownNat (CharToNat c)
forall (c :: Char) (n :: Nat).
(Char -> Int) -> KnownChar c :- KnownNat n
magicCN Char -> Int
ord

-- NB: 0x10FFFF the maximum value for a Unicode code point. Calling `chr` on
-- anything greater will throw an exception.
natToChar :: forall n. (n <= 0x10FFFF, KnownNat n) :- KnownChar (NatToChar n)
natToChar :: forall (n :: Nat).
(n <= 1114111, KnownNat n) :- KnownChar (NatToChar n)
natToChar = ((n <= 1114111, KnownNat n) => Dict (KnownChar (NatToChar n)))
-> (n <= 1114111, KnownNat n) :- KnownChar (NatToChar n)
forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
Sub (((n <= 1114111, KnownNat n) => Dict (KnownChar (NatToChar n)))
 -> (n <= 1114111, KnownNat n) :- KnownChar (NatToChar n))
-> ((n <= 1114111, KnownNat n) => Dict (KnownChar (NatToChar n)))
-> (n <= 1114111, KnownNat n) :- KnownChar (NatToChar n)
forall a b. (a -> b) -> a -> b
$ case forall (n :: Nat) (c :: Char).
(Int -> Char) -> KnownNat n :- KnownChar c
magicNC @n @(NatToChar n) Int -> Char
chr of Sub KnownNat n => Dict (KnownChar (NatToChar n))
r -> Dict (KnownChar (NatToChar n))
KnownNat n => Dict (KnownChar (NatToChar n))
r