(original) (raw)

{-# LANGUAGE Trustworthy #-} {-# LANGUAGE DataKinds #-} {-# LANGUAGE KindSignatures #-} {-# 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 ( 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](GHC.TypeNats.html#Div), [Mod](GHC.TypeNats.html#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