{-# 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 :: proxy a -> proxy b -> SOrdering (CmpNat a b)
cmpNat proxy a
a proxy b
b
= case Natural -> Natural -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (proxy a -> Natural
forall (n :: Nat) (proxy :: Nat -> Type).
KnownNat n =>
proxy n -> Natural
TN.natVal proxy a
a) (proxy b -> Natural
forall (n :: Nat) (proxy :: Nat -> Type).
KnownNat n =>
proxy n -> Natural
TN.natVal proxy b
b) of
Ordering
LT -> SOrdering 'LT -> SOrdering (CmpNat a b)
forall a b. a -> b
unsafeCoerce SOrdering 'LT
SLT
Ordering
EQ -> SOrdering 'EQ -> SOrdering (CmpNat a b)
forall a b. a -> b
unsafeCoerce SOrdering 'EQ
SEQ
Ordering
GT -> SOrdering 'GT -> SOrdering (CmpNat a b)
forall a b. a -> b
unsafeCoerce SOrdering 'GT
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 :: proxy a -> proxy b -> SOrdering (CmpSymbol a b)
cmpSymbol proxy a
a proxy b
b
= case String -> String -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (proxy a -> String
forall (n :: Symbol) (proxy :: Symbol -> Type).
KnownSymbol n =>
proxy n -> String
TL.symbolVal proxy a
a) (proxy b -> String
forall (n :: Symbol) (proxy :: Symbol -> Type).
KnownSymbol n =>
proxy n -> String
TL.symbolVal proxy b
b) of
Ordering
LT -> SOrdering 'LT -> SOrdering (CmpSymbol a b)
forall a b. a -> b
unsafeCoerce SOrdering 'LT
SLT
Ordering
EQ -> SOrdering 'EQ -> SOrdering (CmpSymbol a b)
forall a b. a -> b
unsafeCoerce SOrdering 'EQ
SEQ
Ordering
GT -> SOrdering 'GT -> SOrdering (CmpSymbol a b)
forall a b. a -> b
unsafeCoerce SOrdering 'GT
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) = Max' 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