{-# 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 :: proxy n -> Integer
natVal p :: proxy n
p = Natural -> Integer
forall a. Integral a => a -> Integer
toInteger (proxy n -> Natural
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Natural
N.natVal proxy n
p)
symbolVal :: forall n proxy. KnownSymbol n => proxy n -> String
symbolVal :: proxy n -> String
symbolVal _ = case SSymbol n
forall (n :: Symbol). KnownSymbol n => SSymbol n
symbolSing :: SSymbol n of
SSymbol x :: String
x -> String
x
natVal' :: forall n. KnownNat n => Proxy# n -> Integer
natVal' :: Proxy# n -> Integer
natVal' p :: Proxy# n
p = Natural -> Integer
forall a. Integral a => a -> Integer
toInteger (Proxy# n -> Natural
forall (n :: Nat). KnownNat n => Proxy# n -> Natural
N.natVal' Proxy# n
p)
symbolVal' :: forall n. KnownSymbol n => Proxy# n -> String
symbolVal' :: Proxy# n -> String
symbolVal' _ = case SSymbol n
forall (n :: Symbol). KnownSymbol n => SSymbol n
symbolSing :: SSymbol n of
SSymbol x :: String
x -> String
x
data SomeSymbol = forall n. KnownSymbol n => SomeSymbol (Proxy n)
someNatVal :: Integer -> Maybe N.SomeNat
someNatVal :: Integer -> Maybe SomeNat
someNatVal n :: Integer
n
| Integer
n Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= 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 n :: 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
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 x :: Proxy n
x == :: SomeSymbol -> SomeSymbol -> Bool
== SomeSymbol y :: 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 x :: Proxy n
x) (SomeSymbol y :: 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 p :: Int
p (SomeSymbol x :: 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 p :: Int
p xs :: String
xs = [ (String -> SomeSymbol
someSymbolVal String
a, String
ys) | (a :: String
a,ys :: String
ys) <- Int -> ReadS String
forall a. Read a => Int -> ReadS a
readsPrec Int
p String
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 :: Proxy a -> Proxy b -> Maybe (a :~: b)
sameSymbol x :: Proxy a
x y :: Proxy b
y
| Proxy a -> String
forall (n :: Symbol) (proxy :: Symbol -> *).
KnownSymbol n =>
proxy n -> String
symbolVal Proxy a
x String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== Proxy b -> String
forall (n :: Symbol) (proxy :: Symbol -> *).
KnownSymbol n =>
proxy n -> String
symbolVal Proxy 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
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 :: (KnownSymbol a => Proxy a -> b) -> SSymbol a -> Proxy a -> b
withSSymbol f :: KnownSymbol a => Proxy a -> b
f x :: SSymbol a
x y :: Proxy a
y = WrapS a b -> SSymbol a -> Proxy a -> b
forall a. a
magicDict ((KnownSymbol a => Proxy a -> b) -> WrapS a b
forall (a :: Symbol) b.
(KnownSymbol a => Proxy a -> b) -> WrapS a b
WrapS KnownSymbol a => Proxy a -> b
f) SSymbol a
x Proxy a
y