{-# 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.TypeNats
(
Nat
, KnownNat, natVal, natVal'
, SomeNat(..)
, someNatVal
, sameNat
, type (<=), type (<=?), type (+), type (*), type (^), type (-)
, CmpNat
, Div, Mod, Log2
) where
import GHC.Base(Eq(..), Ord(..), Bool(True), Ordering(..), otherwise)
import GHC.Types( Nat )
import GHC.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 Unsafe.Coerce(unsafeCoerce)
class KnownNat (n :: Nat) where
natSing :: SNat n
natVal :: forall n proxy. KnownNat n => proxy n -> Natural
natVal _ = case natSing :: SNat n of
SNat x -> x
natVal' :: forall n. KnownNat n => Proxy# n -> Natural
natVal' _ = case natSing :: SNat n of
SNat x -> x
data SomeNat = forall n. KnownNat n => SomeNat (Proxy n)
someNatVal :: Natural -> SomeNat
someNatVal n = withSNat SomeNat (SNat n) Proxy
instance Eq SomeNat where
SomeNat x == SomeNat y = natVal x == natVal y
instance Ord SomeNat where
compare (SomeNat x) (SomeNat y) = compare (natVal x) (natVal y)
instance Show SomeNat where
showsPrec p (SomeNat x) = showsPrec p (natVal x)
instance Read SomeNat where
readsPrec p xs = do (a,ys) <- readsPrec p xs
[(someNatVal a, ys)]
infix 4 <=?, <=
infixl 6 +, -
infixl 7 *, `Div`, `Mod`
infixr 8 ^
type x <= y = (x <=? y) ~ 'True
type family CmpNat (m :: Nat) (n :: Nat) :: Ordering
type family (m :: Nat) <=? (n :: Nat) :: Bool
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) =>
Proxy a -> Proxy b -> Maybe (a :~: b)
sameNat x y
| natVal x == natVal y = Just (unsafeCoerce Refl)
| otherwise = Nothing
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 f x y = magicDict (WrapN f) x y