{-# LANGUAGE Trustworthy #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE NoImplicitPrelude #-}
{-# LANGUAGE MagicHash #-}
{-# LANGUAGE TypeApplications #-}
module GHC.TypeLits
(
N.Natural, N.Nat, Symbol
, N.KnownNat, natVal, natVal'
, KnownSymbol, symbolVal, symbolVal'
, KnownChar, charVal, charVal'
, N.SomeNat(..), SomeSymbol(..), SomeChar(..)
, someNatVal, someSymbolVal, someCharVal
, N.sameNat, sameSymbol, sameChar
, OrderingI(..)
, N.cmpNat, cmpSymbol, cmpChar
, type (N.<=), type (N.<=?), type (N.+), type (N.*), type (N.^), type (N.-)
, type N.Div, type N.Mod, type N.Log2
, AppendSymbol
, N.CmpNat, CmpSymbol, CmpChar
, ConsSymbol, UnconsSymbol
, CharToNat, NatToChar
, TypeError
, ErrorMessage(..)
) where
import GHC.Base(Eq(..), Ord(..), Ordering(..), String, otherwise, withDict)
import GHC.Types(Symbol, Char)
import GHC.TypeError(ErrorMessage(..), TypeError)
import GHC.Num(Integer, fromInteger)
import GHC.Show(Show(..))
import GHC.Read(Read(..))
import GHC.Real(toInteger)
import GHC.Prim(Proxy#)
import Data.Maybe(Maybe(..))
import Data.Proxy (Proxy(..))
import Data.Type.Equality((:~:)(Refl))
import Data.Type.Ord(OrderingI(..))
import Unsafe.Coerce(unsafeCoerce)
import GHC.TypeLits.Internal(CmpSymbol, CmpChar)
import qualified GHC.TypeNats as N
class KnownSymbol (n :: Symbol) where
symbolSing :: SSymbol n
natVal :: forall n proxy. N.KnownNat n => proxy n -> Integer
natVal :: forall (n :: Natural) (proxy :: Natural -> *).
KnownNat n =>
proxy n -> Integer
natVal proxy n
p = Natural -> Integer
forall a. Integral a => a -> Integer
toInteger (proxy n -> Natural
forall (n :: Natural) (proxy :: Natural -> *).
KnownNat n =>
proxy n -> Natural
N.natVal proxy n
p)
symbolVal :: forall n proxy. KnownSymbol n => proxy n -> String
symbolVal :: forall (n :: Symbol) (proxy :: Symbol -> *).
KnownSymbol n =>
proxy n -> String
symbolVal proxy n
_ = case SSymbol n
forall (n :: Symbol). KnownSymbol n => SSymbol n
symbolSing :: SSymbol n of
SSymbol String
x -> String
x
natVal' :: forall n. N.KnownNat n => Proxy# n -> Integer
natVal' :: forall (n :: Natural). KnownNat n => Proxy# n -> Integer
natVal' Proxy# n
p = Natural -> Integer
forall a. Integral a => a -> Integer
toInteger (Proxy# n -> Natural
forall (n :: Natural). KnownNat n => Proxy# n -> Natural
N.natVal' Proxy# n
p)
symbolVal' :: forall n. KnownSymbol n => Proxy# n -> String
symbolVal' :: forall (n :: Symbol). KnownSymbol n => Proxy# n -> String
symbolVal' Proxy# n
_ = case SSymbol n
forall (n :: Symbol). KnownSymbol n => SSymbol n
symbolSing :: SSymbol n of
SSymbol String
x -> String
x
data SomeSymbol = forall n. KnownSymbol n => SomeSymbol (Proxy n)
class KnownChar (n :: Char) where
charSing :: SChar n
charVal :: forall n proxy. KnownChar n => proxy n -> Char
charVal :: forall (n :: Char) (proxy :: Char -> *).
KnownChar n =>
proxy n -> Char
charVal proxy n
_ = case SChar n
forall (n :: Char). KnownChar n => SChar n
charSing :: SChar n of
SChar Char
x -> Char
x
charVal' :: forall n. KnownChar n => Proxy# n -> Char
charVal' :: forall (n :: Char). KnownChar n => Proxy# n -> Char
charVal' Proxy# n
_ = case SChar n
forall (n :: Char). KnownChar n => SChar n
charSing :: SChar n of
SChar Char
x -> Char
x
data SomeChar = forall n. KnownChar n => SomeChar (Proxy n)
someNatVal :: Integer -> Maybe N.SomeNat
someNatVal :: Integer -> Maybe SomeNat
someNatVal Integer
n
| Integer
n Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer
0 = SomeNat -> Maybe SomeNat
forall a. a -> Maybe a
Just (Natural -> SomeNat
N.someNatVal (Integer -> Natural
forall a. Num a => Integer -> a
fromInteger Integer
n))
| Bool
otherwise = Maybe SomeNat
forall a. Maybe a
Nothing
someSymbolVal :: String -> SomeSymbol
someSymbolVal :: String -> SomeSymbol
someSymbolVal String
n = (KnownSymbol Any => Proxy Any -> SomeSymbol)
-> SSymbol Any -> Proxy Any -> SomeSymbol
forall (a :: Symbol) b.
(KnownSymbol a => Proxy a -> b) -> SSymbol a -> Proxy a -> b
withSSymbol KnownSymbol Any => Proxy Any -> SomeSymbol
Proxy Any -> SomeSymbol
forall (n :: Symbol). KnownSymbol n => Proxy n -> SomeSymbol
SomeSymbol (String -> SSymbol Any
forall (s :: Symbol). String -> SSymbol s
SSymbol String
n) Proxy Any
forall {k} (t :: k). Proxy t
Proxy
{-# NOINLINE someSymbolVal #-}
instance Eq SomeSymbol where
SomeSymbol Proxy n
x == :: SomeSymbol -> SomeSymbol -> Bool
== SomeSymbol Proxy n
y = Proxy n -> String
forall (n :: Symbol) (proxy :: Symbol -> *).
KnownSymbol n =>
proxy n -> String
symbolVal Proxy n
x String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== Proxy n -> String
forall (n :: Symbol) (proxy :: Symbol -> *).
KnownSymbol n =>
proxy n -> String
symbolVal Proxy n
y
instance Ord SomeSymbol where
compare :: SomeSymbol -> SomeSymbol -> Ordering
compare (SomeSymbol Proxy n
x) (SomeSymbol Proxy n
y) = String -> String -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (Proxy n -> String
forall (n :: Symbol) (proxy :: Symbol -> *).
KnownSymbol n =>
proxy n -> String
symbolVal Proxy n
x) (Proxy n -> String
forall (n :: Symbol) (proxy :: Symbol -> *).
KnownSymbol n =>
proxy n -> String
symbolVal Proxy n
y)
instance Show SomeSymbol where
showsPrec :: Int -> SomeSymbol -> ShowS
showsPrec Int
p (SomeSymbol Proxy n
x) = Int -> String -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
p (Proxy n -> String
forall (n :: Symbol) (proxy :: Symbol -> *).
KnownSymbol n =>
proxy n -> String
symbolVal Proxy n
x)
instance Read SomeSymbol where
readsPrec :: Int -> ReadS SomeSymbol
readsPrec Int
p String
xs = [ (String -> SomeSymbol
someSymbolVal String
a, String
ys) | (String
a,String
ys) <- Int -> ReadS String
forall a. Read a => Int -> ReadS a
readsPrec Int
p String
xs ]
someCharVal :: Char -> SomeChar
someCharVal :: Char -> SomeChar
someCharVal Char
n = (KnownChar Any => Proxy Any -> SomeChar)
-> SChar Any -> Proxy Any -> SomeChar
forall (a :: Char) b.
(KnownChar a => Proxy a -> b) -> SChar a -> Proxy a -> b
withSChar KnownChar Any => Proxy Any -> SomeChar
Proxy Any -> SomeChar
forall (n :: Char). KnownChar n => Proxy n -> SomeChar
SomeChar (Char -> SChar Any
forall (s :: Char). Char -> SChar s
SChar Char
n) Proxy Any
forall {k} (t :: k). Proxy t
Proxy
{-# NOINLINE someCharVal #-}
instance Eq SomeChar where
SomeChar Proxy n
x == :: SomeChar -> SomeChar -> Bool
== SomeChar Proxy n
y = Proxy n -> Char
forall (n :: Char) (proxy :: Char -> *).
KnownChar n =>
proxy n -> Char
charVal Proxy n
x Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Proxy n -> Char
forall (n :: Char) (proxy :: Char -> *).
KnownChar n =>
proxy n -> Char
charVal Proxy n
y
instance Ord SomeChar where
compare :: SomeChar -> SomeChar -> Ordering
compare (SomeChar Proxy n
x) (SomeChar Proxy n
y) = Char -> Char -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (Proxy n -> Char
forall (n :: Char) (proxy :: Char -> *).
KnownChar n =>
proxy n -> Char
charVal Proxy n
x) (Proxy n -> Char
forall (n :: Char) (proxy :: Char -> *).
KnownChar n =>
proxy n -> Char
charVal Proxy n
y)
instance Show SomeChar where
showsPrec :: Int -> SomeChar -> ShowS
showsPrec Int
p (SomeChar Proxy n
x) = Int -> Char -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
p (Proxy n -> Char
forall (n :: Char) (proxy :: Char -> *).
KnownChar n =>
proxy n -> Char
charVal Proxy n
x)
instance Read SomeChar where
readsPrec :: Int -> ReadS SomeChar
readsPrec Int
p String
xs = [ (Char -> SomeChar
someCharVal Char
a, String
ys) | (Char
a,String
ys) <- Int -> ReadS Char
forall a. Read a => Int -> ReadS a
readsPrec Int
p String
xs ]
type family AppendSymbol (m ::Symbol) (n :: Symbol) :: Symbol
type family ConsSymbol (a :: Char) (b :: Symbol) :: Symbol
type family UnconsSymbol (a :: Symbol) :: Maybe (Char, Symbol)
type family CharToNat (c :: Char) :: N.Nat
type family NatToChar (n :: N.Nat) :: Char
sameSymbol :: (KnownSymbol a, KnownSymbol b) =>
proxy1 a -> proxy2 b -> Maybe (a :~: b)
sameSymbol :: forall (a :: Symbol) (b :: Symbol) (proxy1 :: Symbol -> *)
(proxy2 :: Symbol -> *).
(KnownSymbol a, KnownSymbol b) =>
proxy1 a -> proxy2 b -> Maybe (a :~: b)
sameSymbol proxy1 a
x proxy2 b
y
| proxy1 a -> String
forall (n :: Symbol) (proxy :: Symbol -> *).
KnownSymbol n =>
proxy n -> String
symbolVal proxy1 a
x String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== proxy2 b -> String
forall (n :: Symbol) (proxy :: Symbol -> *).
KnownSymbol n =>
proxy n -> String
symbolVal proxy2 b
y = (a :~: b) -> Maybe (a :~: b)
forall a. a -> Maybe a
Just ((Any :~: Any) -> a :~: b
forall a b. a -> b
unsafeCoerce Any :~: Any
forall {k} (a :: k). a :~: a
Refl)
| Bool
otherwise = Maybe (a :~: b)
forall a. Maybe a
Nothing
sameChar :: (KnownChar a, KnownChar b) =>
proxy1 a -> proxy2 b -> Maybe (a :~: b)
sameChar :: forall (a :: Char) (b :: Char) (proxy1 :: Char -> *)
(proxy2 :: Char -> *).
(KnownChar a, KnownChar b) =>
proxy1 a -> proxy2 b -> Maybe (a :~: b)
sameChar proxy1 a
x proxy2 b
y
| proxy1 a -> Char
forall (n :: Char) (proxy :: Char -> *).
KnownChar n =>
proxy n -> Char
charVal proxy1 a
x Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== proxy2 b -> Char
forall (n :: Char) (proxy :: Char -> *).
KnownChar n =>
proxy n -> Char
charVal proxy2 b
y = (a :~: b) -> Maybe (a :~: b)
forall a. a -> Maybe a
Just ((Any :~: Any) -> a :~: b
forall a b. a -> b
unsafeCoerce Any :~: Any
forall {k} (a :: k). a :~: a
Refl)
| Bool
otherwise = Maybe (a :~: b)
forall a. Maybe a
Nothing
cmpSymbol :: forall a b proxy1 proxy2. (KnownSymbol a, KnownSymbol b)
=> proxy1 a -> proxy2 b -> OrderingI a b
cmpSymbol :: forall (a :: Symbol) (b :: Symbol) (proxy1 :: Symbol -> *)
(proxy2 :: Symbol -> *).
(KnownSymbol a, KnownSymbol b) =>
proxy1 a -> proxy2 b -> OrderingI a b
cmpSymbol proxy1 a
x proxy2 b
y = case String -> String -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (proxy1 a -> String
forall (n :: Symbol) (proxy :: Symbol -> *).
KnownSymbol n =>
proxy n -> String
symbolVal proxy1 a
x) (proxy2 b -> String
forall (n :: Symbol) (proxy :: Symbol -> *).
KnownSymbol n =>
proxy n -> String
symbolVal proxy2 b
y) of
Ordering
EQ -> case (Any :~: Any, Any :~: Any) -> (CmpSymbol a b :~: 'EQ, a :~: b)
forall a b. a -> b
unsafeCoerce (Any :~: Any
forall {k} (a :: k). a :~: a
Refl, Any :~: Any
forall {k} (a :: k). a :~: a
Refl) :: (CmpSymbol a b :~: 'EQ, a :~: b) of
(CmpSymbol a b :~: 'EQ
Refl, a :~: b
Refl) -> OrderingI a a
OrderingI a b
forall {k} (a :: k). (Compare a a ~ 'EQ) => OrderingI a a
EQI
Ordering
LT -> case (Any :~: Any) -> CmpSymbol a b :~: 'LT
forall a b. a -> b
unsafeCoerce Any :~: Any
forall {k} (a :: k). a :~: a
Refl :: (CmpSymbol a b :~: 'LT) of
CmpSymbol a b :~: 'LT
Refl -> OrderingI a b
forall {k} (a :: k) (b :: k). (Compare a b ~ 'LT) => OrderingI a b
LTI
Ordering
GT -> case (Any :~: Any) -> CmpSymbol a b :~: 'GT
forall a b. a -> b
unsafeCoerce Any :~: Any
forall {k} (a :: k). a :~: a
Refl :: (CmpSymbol a b :~: 'GT) of
CmpSymbol a b :~: 'GT
Refl -> OrderingI a b
forall {k} (a :: k) (b :: k). (Compare a b ~ 'GT) => OrderingI a b
GTI
cmpChar :: forall a b proxy1 proxy2. (KnownChar a, KnownChar b)
=> proxy1 a -> proxy2 b -> OrderingI a b
cmpChar :: forall (a :: Char) (b :: Char) (proxy1 :: Char -> *)
(proxy2 :: Char -> *).
(KnownChar a, KnownChar b) =>
proxy1 a -> proxy2 b -> OrderingI a b
cmpChar proxy1 a
x proxy2 b
y = case Char -> Char -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (proxy1 a -> Char
forall (n :: Char) (proxy :: Char -> *).
KnownChar n =>
proxy n -> Char
charVal proxy1 a
x) (proxy2 b -> Char
forall (n :: Char) (proxy :: Char -> *).
KnownChar n =>
proxy n -> Char
charVal proxy2 b
y) of
Ordering
EQ -> case (Any :~: Any, Any :~: Any) -> (CmpChar a b :~: 'EQ, a :~: b)
forall a b. a -> b
unsafeCoerce (Any :~: Any
forall {k} (a :: k). a :~: a
Refl, Any :~: Any
forall {k} (a :: k). a :~: a
Refl) :: (CmpChar a b :~: 'EQ, a :~: b) of
(CmpChar a b :~: 'EQ
Refl, a :~: b
Refl) -> OrderingI a a
OrderingI a b
forall {k} (a :: k). (Compare a a ~ 'EQ) => OrderingI a a
EQI
Ordering
LT -> case (Any :~: Any) -> CmpChar a b :~: 'LT
forall a b. a -> b
unsafeCoerce Any :~: Any
forall {k} (a :: k). a :~: a
Refl :: (CmpChar a b :~: 'LT) of
CmpChar a b :~: 'LT
Refl -> OrderingI a b
forall {k} (a :: k) (b :: k). (Compare a b ~ 'LT) => OrderingI a b
LTI
Ordering
GT -> case (Any :~: Any) -> CmpChar a b :~: 'GT
forall a b. a -> b
unsafeCoerce Any :~: Any
forall {k} (a :: k). a :~: a
Refl :: (CmpChar a b :~: 'GT) of
CmpChar a b :~: 'GT
Refl -> OrderingI a b
forall {k} (a :: k) (b :: k). (Compare a b ~ 'GT) => OrderingI a b
GTI
newtype SSymbol (s :: Symbol) = SSymbol String
withSSymbol :: forall a b.
(KnownSymbol a => Proxy a -> b)
-> SSymbol a -> Proxy a -> b
withSSymbol :: forall (a :: Symbol) b.
(KnownSymbol a => Proxy a -> b) -> SSymbol a -> Proxy a -> b
withSSymbol KnownSymbol a => Proxy a -> b
f SSymbol a
x Proxy a
y = forall (cls :: Constraint) meth r.
WithDict cls meth =>
meth -> (cls => r) -> r
withDict @(KnownSymbol a) SSymbol a
x KnownSymbol a => Proxy a -> b
Proxy a -> b
f Proxy a
y
newtype SChar (s :: Char) = SChar Char
withSChar :: forall a b.
(KnownChar a => Proxy a -> b)
-> SChar a -> Proxy a -> b
withSChar :: forall (a :: Char) b.
(KnownChar a => Proxy a -> b) -> SChar a -> Proxy a -> b
withSChar KnownChar a => Proxy a -> b
f SChar a
x Proxy a
y = forall (cls :: Constraint) meth r.
WithDict cls meth =>
meth -> (cls => r) -> r
withDict @(KnownChar a) SChar a
x KnownChar a => Proxy a -> b
Proxy a -> b
f Proxy a
y