{-# LANGUAGE Trustworthy #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE NoImplicitPrelude #-}
{-# LANGUAGE MagicHash #-}
{-# LANGUAGE PolyKinds #-}
module GHC.TypeLits
(
Nat, Symbol
, N.KnownNat, natVal, natVal'
, KnownSymbol, symbolVal, symbolVal'
, N.SomeNat(..), SomeSymbol(..)
, someNatVal, someSymbolVal
, N.sameNat, sameSymbol
, 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
, TypeError
, ErrorMessage(..)
) where
import GHC.Base(Eq(..), Ord(..), Ordering(..), otherwise)
import GHC.Types( Nat, Symbol )
import GHC.Num(Integer, fromInteger)
import GHC.Base(String)
import GHC.Show(Show(..))
import GHC.Read(Read(..))
import GHC.Real(toInteger)
import GHC.Prim(magicDict, Proxy#)
import Data.Maybe(Maybe(..))
import Data.Proxy (Proxy(..))
import Data.Type.Equality((:~:)(Refl))
import Unsafe.Coerce(unsafeCoerce)
import GHC.TypeNats (KnownNat)
import qualified GHC.TypeNats as N
class KnownSymbol (n :: Symbol) where
symbolSing :: SSymbol n
natVal :: forall n proxy. KnownNat n => proxy n -> Integer
natVal p = toInteger (N.natVal p)
symbolVal :: forall n proxy. KnownSymbol n => proxy n -> String
symbolVal _ = case symbolSing :: SSymbol n of
SSymbol x -> x
natVal' :: forall n. KnownNat n => Proxy# n -> Integer
natVal' p = toInteger (N.natVal' p)
symbolVal' :: forall n. KnownSymbol n => Proxy# n -> String
symbolVal' _ = case symbolSing :: SSymbol n of
SSymbol x -> x
data SomeSymbol = forall n. KnownSymbol n => SomeSymbol (Proxy n)
someNatVal :: Integer -> Maybe N.SomeNat
someNatVal n
| n >= 0 = Just (N.someNatVal (fromInteger n))
| otherwise = Nothing
someSymbolVal :: String -> SomeSymbol
someSymbolVal n = withSSymbol SomeSymbol (SSymbol n) Proxy
instance Eq SomeSymbol where
SomeSymbol x == SomeSymbol y = symbolVal x == symbolVal y
instance Ord SomeSymbol where
compare (SomeSymbol x) (SomeSymbol y) = compare (symbolVal x) (symbolVal y)
instance Show SomeSymbol where
showsPrec p (SomeSymbol x) = showsPrec p (symbolVal x)
instance Read SomeSymbol where
readsPrec p xs = [ (someSymbolVal a, ys) | (a,ys) <- readsPrec p xs ]
type family CmpSymbol (m :: Symbol) (n :: Symbol) :: Ordering
type family AppendSymbol (m ::Symbol) (n :: Symbol) :: Symbol
data ErrorMessage = Text Symbol
| forall t. ShowType t
| ErrorMessage :<>: ErrorMessage
| ErrorMessage :$$: ErrorMessage
infixl 5 :$$:
infixl 6 :<>:
type family TypeError (a :: ErrorMessage) :: b where
sameSymbol :: (KnownSymbol a, KnownSymbol b) =>
Proxy a -> Proxy b -> Maybe (a :~: b)
sameSymbol x y
| symbolVal x == symbolVal y = Just (unsafeCoerce Refl)
| otherwise = Nothing
newtype SSymbol (s :: Symbol) = SSymbol String
data WrapS a b = WrapS (KnownSymbol a => Proxy a -> b)
withSSymbol :: (KnownSymbol a => Proxy a -> b)
-> SSymbol a -> Proxy a -> b
withSSymbol f x y = magicDict (WrapS f) x y