#if __GLASGOW_HASKELL__ < 800
#endif
module Basement.Nat
( Nat
, KnownNat
, natVal
, type (<=), type (<=?), type (+), type (*), type (^), type ()
, CmpNat
, natValNatural
, natValInt
, natValInt8
, natValInt16
, natValInt32
, natValInt64
, natValWord
, natValWord8
, natValWord16
, natValWord32
, natValWord64
, NatNumMaxBound
, NatInBoundOf
, NatWithinBound
) where
#include "MachDeps.h"
import GHC.TypeLits
import Basement.Compat.Base
import Basement.Compat.Natural
import Data.Int (Int8, Int16, Int32, Int64)
import Data.Word (Word8, Word16, Word32, Word64)
import qualified Prelude (fromIntegral)
#if __GLASGOW_HASKELL__ >= 800
import Data.Type.Bool
#endif
natValNatural :: forall n proxy . KnownNat n => proxy n -> Natural
natValNatural n = Prelude.fromIntegral (natVal n)
natValInt :: forall n proxy . (KnownNat n, NatWithinBound Int n) => proxy n -> Int
natValInt n = Prelude.fromIntegral (natVal n)
natValInt64 :: forall n proxy . (KnownNat n, NatWithinBound Int64 n) => proxy n -> Int64
natValInt64 n = Prelude.fromIntegral (natVal n)
natValInt32 :: forall n proxy . (KnownNat n, NatWithinBound Int32 n) => proxy n -> Int32
natValInt32 n = Prelude.fromIntegral (natVal n)
natValInt16 :: forall n proxy . (KnownNat n, NatWithinBound Int16 n) => proxy n -> Int16
natValInt16 n = Prelude.fromIntegral (natVal n)
natValInt8 :: forall n proxy . (KnownNat n, NatWithinBound Int8 n) => proxy n -> Int8
natValInt8 n = Prelude.fromIntegral (natVal n)
natValWord :: forall n proxy . (KnownNat n, NatWithinBound Word n) => proxy n -> Word
natValWord n = Prelude.fromIntegral (natVal n)
natValWord64 :: forall n proxy . (KnownNat n, NatWithinBound Word64 n) => proxy n -> Word64
natValWord64 n = Prelude.fromIntegral (natVal n)
natValWord32 :: forall n proxy . (KnownNat n, NatWithinBound Word32 n) => proxy n -> Word32
natValWord32 n = Prelude.fromIntegral (natVal n)
natValWord16 :: forall n proxy . (KnownNat n, NatWithinBound Word16 n) => proxy n -> Word16
natValWord16 n = Prelude.fromIntegral (natVal n)
natValWord8 :: forall n proxy . (KnownNat n, NatWithinBound Word8 n) => proxy n -> Word8
natValWord8 n = Prelude.fromIntegral (natVal n)
type family NatNumMaxBound ty where
NatNumMaxBound Int64 = 0x7fffffffffffffff
NatNumMaxBound Int32 = 0x7fffffff
NatNumMaxBound Int16 = 0x7fff
NatNumMaxBound Int8 = 0x7f
NatNumMaxBound Word64 = 0xffffffffffffffff
NatNumMaxBound Word32 = 0xffffffff
NatNumMaxBound Word16 = 0xffff
NatNumMaxBound Word8 = 0xff
#if WORD_SIZE_IN_BITS == 64
NatNumMaxBound Int = NatNumMaxBound Int64
NatNumMaxBound Word = NatNumMaxBound Word64
#else
NatNumMaxBound Int = NatNumMaxBound Int32
NatNumMaxBound Word = NatNumMaxBound Word32
#endif
type family NatInBoundOf ty n where
NatInBoundOf Integer n = 'True
NatInBoundOf Natural n = 'True
NatInBoundOf ty n = n <=? NatNumMaxBound ty
#if __GLASGOW_HASKELL__ >= 800
type family NatWithinBound ty (n :: Nat) where
NatWithinBound ty n = If (NatInBoundOf ty n)
(() ~ ())
(TypeError ('Text "Natural " ':<>: 'ShowType n ':<>: 'Text " is out of bounds for " ':<>: 'ShowType ty))
#else
type NatWithinBound ty n = NatInBoundOf ty n ~ 'True
#endif