(original) (raw)

{-# 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](#local-6989586621679185156). [ShowType](GHC.TypeLits.html#ShowType) [t](#local-6989586621679185156)
                         

                       | [ErrorMessage](GHC.TypeLits.html#ErrorMessage) [:<>:](GHC.TypeLits.html#%3A%3C%3E%3A) [ErrorMessage](GHC.TypeLits.html#ErrorMessage)
                         

                       | [ErrorMessage](GHC.TypeLits.html#ErrorMessage) [:$$:](GHC.TypeLits.html#%3A%24%24%3A) [ErrorMessage](GHC.TypeLits.html#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