{-# LANGUAGE CPP #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE ExplicitForAll #-}
{-# LANGUAGE ExplicitNamespaces #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeFamilyDependencies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
#if __GLASGOW_HASKELL__ >= 806
{-# LANGUAGE NoStarIsType #-}
#endif
module Data.Type.Lits
(
TN.Nat, TL.Symbol
, KindOf, KindOfEl
, TN.KnownNat, TN.natVal, TN.natVal'
, TL.KnownSymbol, TL.symbolVal, TL.symbolVal'
, TN.SomeNat(..), TL.SomeSymbol(..)
, TN.someNatVal, TL.someSymbolVal
, TN.sameNat, TL.sameSymbol
, type (+), type (*), type (^), type (-)
, type TN.Div, type TN.Mod, type TN.Log2
, type Min, type Max
, TL.AppendSymbol, ShowNat
, TN.CmpNat, TL.CmpSymbol, type (<=)
, SOrdering (..), cmpNat, cmpSymbol
, TL.TypeError
, TL.ErrorMessage(..)
) where
import Data.Kind (Constraint, Type)
import qualified GHC.TypeLits as TL
import GHC.TypeNats (type (*), type (+), type (-), type (^))
import qualified GHC.TypeNats as TN
import Unsafe.Coerce (unsafeCoerce)
type family ShowNat (n :: TN.Nat) :: TL.Symbol where
ShowNat 0 = "0"
ShowNat 1 = "1"
ShowNat 2 = "2"
ShowNat 3 = "3"
ShowNat 4 = "4"
ShowNat 5 = "5"
ShowNat 6 = "6"
ShowNat 7 = "7"
ShowNat 8 = "8"
ShowNat 9 = "9"
ShowNat d = TL.AppendSymbol (ShowNat (TN.Div d 10)) (ShowNat (TN.Mod d 10))
data SOrdering :: Ordering -> Type where
SLT :: SOrdering 'LT
SEQ :: SOrdering 'EQ
SGT :: SOrdering 'GT
cmpNat :: forall (a :: TN.Nat) (b :: TN.Nat) (proxy :: TN.Nat -> Type)
. (TN.KnownNat a, TN.KnownNat b)
=> proxy a -> proxy b -> SOrdering (TN.CmpNat a b)
cmpNat a b
= case compare (TN.natVal a) (TN.natVal b) of
LT -> unsafeCoerce SLT
EQ -> unsafeCoerce SEQ
GT -> unsafeCoerce SGT
{-# INLINE cmpNat #-}
cmpSymbol :: forall (a :: TL.Symbol) (b :: TL.Symbol) (proxy :: TL.Symbol -> Type)
. (TL.KnownSymbol a, TL.KnownSymbol b)
=> proxy a -> proxy b -> SOrdering (TL.CmpSymbol a b)
cmpSymbol a b
= case compare (TL.symbolVal a) (TL.symbolVal b) of
LT -> unsafeCoerce SLT
EQ -> unsafeCoerce SEQ
GT -> unsafeCoerce SGT
{-# INLINE cmpSymbol #-}
type Min (a :: TN.Nat) (b :: TN.Nat) = Min' a b (TN.CmpNat a b)
type Max (a :: TN.Nat) (b :: TN.Nat) = Min' a b (TN.CmpNat a b)
type family Min' (a :: TN.Nat) (b :: TN.Nat) (r :: Ordering) :: TN.Nat where
Min' a _ 'LT = a
Min' a _ 'EQ = a
Min' _ b 'GT = b
type family Max' (a :: TN.Nat) (b :: TN.Nat) (r :: Ordering) :: TN.Nat where
Max' _ b 'LT = b
Max' _ b 'EQ = b
Max' a _ 'GT = a
type (<=) (a :: TN.Nat) (b :: TN.Nat) = LE a b (TN.CmpNat a b)
type family LE (a :: TN.Nat) (b :: TN.Nat) (r :: Ordering)
= (y :: Constraint) | y -> r where
LE a b 'LT = ('LT ~ TN.CmpNat a b)
LE a b 'EQ = ('EQ ~ TN.CmpNat a b)
LE a b 'GT = ('GT ~ TL.TypeError
('TL.Text "Cannot deduce type-level Nat relation: "
'TL.:<>: 'TL.ShowType a
'TL.:<>: 'TL.Text " <= "
'TL.:<>: 'TL.ShowType b
))
type KindOf (t :: k) = k
type KindOfEl (ts :: [k]) = k