{-# LANGUAGE Trustworthy #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE NoStarIsType #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE NoImplicitPrelude #-}
{-# LANGUAGE MagicHash #-}
{-# LANGUAGE PolyKinds #-}
module GHC.TypeNats
(
Natural
, Nat
, KnownNat, natVal, natVal'
, SomeNat(..)
, someNatVal
, sameNat
, type (<=), type (<=?), type (+), type (*), type (^), type (-)
, CmpNat
, cmpNat
, Div, Mod, Log2
) where
import GHC.Base(Eq(..), Ord(..), otherwise)
import GHC.Types
import GHC.Num.Natural(Natural)
import GHC.Show(Show(..))
import GHC.Read(Read(..))
import GHC.Prim(magicDict, Proxy#)
import Data.Maybe(Maybe(..))
import Data.Proxy (Proxy(..))
import Data.Type.Equality((:~:)(Refl))
import Data.Type.Ord(OrderingI(..), type (<=), type (<=?))
import Unsafe.Coerce(unsafeCoerce)
import GHC.TypeNats.Internal(CmpNat)
type Nat = Natural
class KnownNat (n :: Nat) where
natSing :: SNat n
natVal :: forall n proxy. KnownNat n => proxy n -> Natural
natVal :: forall (n :: Nat) (proxy :: Nat -> Type).
KnownNat n =>
proxy n -> Nat
natVal proxy n
_ = case SNat n
forall (n :: Nat). KnownNat n => SNat n
natSing :: SNat n of
SNat Nat
x -> Nat
x
natVal' :: forall n. KnownNat n => Proxy# n -> Natural
natVal' :: forall (n :: Nat). KnownNat n => Proxy# n -> Nat
natVal' Proxy# n
_ = case SNat n
forall (n :: Nat). KnownNat n => SNat n
natSing :: SNat n of
SNat Nat
x -> Nat
x
data SomeNat = forall n. KnownNat n => SomeNat (Proxy n)
someNatVal :: Natural -> SomeNat
someNatVal :: Nat -> SomeNat
someNatVal Nat
n = (KnownNat Any => Proxy Any -> SomeNat)
-> SNat Any -> Proxy Any -> SomeNat
forall (a :: Nat) b.
(KnownNat a => Proxy a -> b) -> SNat a -> Proxy a -> b
withSNat KnownNat Any => Proxy Any -> SomeNat
forall (n :: Nat). KnownNat n => Proxy n -> SomeNat
SomeNat (Nat -> SNat Any
forall (n :: Nat). Nat -> SNat n
SNat Nat
n) Proxy Any
forall {k} (t :: k). Proxy t
Proxy
{-# NOINLINE someNatVal #-}
instance Eq SomeNat where
SomeNat Proxy n
x == :: SomeNat -> SomeNat -> Bool
== SomeNat Proxy n
y = Proxy n -> Nat
forall (n :: Nat) (proxy :: Nat -> Type).
KnownNat n =>
proxy n -> Nat
natVal Proxy n
x Nat -> Nat -> Bool
forall a. Eq a => a -> a -> Bool
== Proxy n -> Nat
forall (n :: Nat) (proxy :: Nat -> Type).
KnownNat n =>
proxy n -> Nat
natVal Proxy n
y
instance Ord SomeNat where
compare :: SomeNat -> SomeNat -> Ordering
compare (SomeNat Proxy n
x) (SomeNat Proxy n
y) = Nat -> Nat -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (Proxy n -> Nat
forall (n :: Nat) (proxy :: Nat -> Type).
KnownNat n =>
proxy n -> Nat
natVal Proxy n
x) (Proxy n -> Nat
forall (n :: Nat) (proxy :: Nat -> Type).
KnownNat n =>
proxy n -> Nat
natVal Proxy n
y)
instance Show SomeNat where
showsPrec :: Int -> SomeNat -> ShowS
showsPrec Int
p (SomeNat Proxy n
x) = Int -> Nat -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
p (Proxy n -> Nat
forall (n :: Nat) (proxy :: Nat -> Type).
KnownNat n =>
proxy n -> Nat
natVal Proxy n
x)
instance Read SomeNat where
readsPrec :: Int -> ReadS SomeNat
readsPrec Int
p String
xs = do (Nat
a,String
ys) <- Int -> ReadS Nat
forall a. Read a => Int -> ReadS a
readsPrec Int
p String
xs
[(Nat -> SomeNat
someNatVal Nat
a, String
ys)]
infixl 6 +, -
infixl 7 *, `Div`, `Mod`
infixr 8 ^
type family (m :: Nat) + (n :: Nat) :: Nat
type family (m :: Nat) * (n :: Nat) :: Nat
type family (m :: Nat) ^ (n :: Nat) :: Nat
type family (m :: Nat) - (n :: Nat) :: Nat
type family Div (m :: Nat) (n :: Nat) :: Nat
type family Mod (m :: Nat) (n :: Nat) :: Nat
type family Log2 (m :: Nat) :: Nat
sameNat :: (KnownNat a, KnownNat b) =>
proxy1 a -> proxy2 b -> Maybe (a :~: b)
sameNat :: forall (a :: Nat) (b :: Nat) (proxy1 :: Nat -> Type)
(proxy2 :: Nat -> Type).
(KnownNat a, KnownNat b) =>
proxy1 a -> proxy2 b -> Maybe (a :~: b)
sameNat proxy1 a
x proxy2 b
y
| proxy1 a -> Nat
forall (n :: Nat) (proxy :: Nat -> Type).
KnownNat n =>
proxy n -> Nat
natVal proxy1 a
x Nat -> Nat -> Bool
forall a. Eq a => a -> a -> Bool
== proxy2 b -> Nat
forall (n :: Nat) (proxy :: Nat -> Type).
KnownNat n =>
proxy n -> Nat
natVal proxy2 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
cmpNat :: forall a b proxy1 proxy2. (KnownNat a, KnownNat b)
=> proxy1 a -> proxy2 b -> OrderingI a b
cmpNat :: forall (a :: Nat) (b :: Nat) (proxy1 :: Nat -> Type)
(proxy2 :: Nat -> Type).
(KnownNat a, KnownNat b) =>
proxy1 a -> proxy2 b -> OrderingI a b
cmpNat proxy1 a
x proxy2 b
y = case Nat -> Nat -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (proxy1 a -> Nat
forall (n :: Nat) (proxy :: Nat -> Type).
KnownNat n =>
proxy n -> Nat
natVal proxy1 a
x) (proxy2 b -> Nat
forall (n :: Nat) (proxy :: Nat -> Type).
KnownNat n =>
proxy n -> Nat
natVal proxy2 b
y) of
Ordering
EQ -> case (Any :~: Any, Any :~: Any) -> (CmpNat a b :~: 'EQ, a :~: b)
forall a b. a -> b
unsafeCoerce (Any :~: Any
forall {k} (a :: k). a :~: a
Refl, Any :~: Any
forall {k} (a :: k). a :~: a
Refl) :: (CmpNat a b :~: 'EQ, a :~: b) of
(CmpNat a b :~: 'EQ
Refl, a :~: b
Refl) -> OrderingI a b
forall {k} (a :: k). (Compare a a ~ 'EQ) => OrderingI a a
EQI
Ordering
LT -> case (Any :~: Any) -> CmpNat a b :~: 'LT
forall a b. a -> b
unsafeCoerce Any :~: Any
forall {k} (a :: k). a :~: a
Refl :: (CmpNat a b :~: 'LT) of
CmpNat a b :~: 'LT
Refl -> OrderingI a b
forall {k} (a :: k) (b :: k). (Compare a b ~ 'LT) => OrderingI a b
LTI
Ordering
GT -> case (Any :~: Any) -> CmpNat a b :~: 'GT
forall a b. a -> b
unsafeCoerce Any :~: Any
forall {k} (a :: k). a :~: a
Refl :: (CmpNat a b :~: 'GT) of
CmpNat a b :~: 'GT
Refl -> OrderingI a b
forall {k} (a :: k) (b :: k). (Compare a b ~ 'GT) => OrderingI a b
GTI
newtype SNat (n :: Nat) = SNat Natural
data WrapN a b = WrapN (KnownNat a => Proxy a -> b)
withSNat :: (KnownNat a => Proxy a -> b)
-> SNat a -> Proxy a -> b
withSNat :: forall (a :: Nat) b.
(KnownNat a => Proxy a -> b) -> SNat a -> Proxy a -> b
withSNat KnownNat a => Proxy a -> b
f SNat a
x Proxy a
y = WrapN a b -> SNat a -> Proxy a -> b
forall a. a
magicDict ((KnownNat a => Proxy a -> b) -> WrapN a b
forall (a :: Nat) b. (KnownNat a => Proxy a -> b) -> WrapN a b
WrapN KnownNat a => Proxy a -> b
f) SNat a
x Proxy a
y