    {-# LANGUAGE CPP                       #-}
    {-# LANGUAGE KindSignatures            #-}
    {-# LANGUAGE DataKinds                 #-}
    {-# LANGUAGE GADTs                     #-}
    {-# LANGUAGE TypeOperators             #-}
    {-# LANGUAGE TypeFamilies              #-}
    {-# LANGUAGE ExistentialQuantification #-}
    {-# LANGUAGE ScopedTypeVariables       #-}
    {-# LANGUAGE UndecidableInstances      #-}
    {-# LANGUAGE ConstraintKinds           #-}
    #if __GLASGOW_HASKELL__ >= 806
    {-# LANGUAGE NoStarIsType              #-}
    #endif
    module Basement.Nat
        ( Nat
        , KnownNat
        , natVal
        , type (<=), type (<=?), type (+), type (*), type (^), type (-)
        , CmpNat
        -- * Nat convertion
        , natValNatural
        , natValInt
        , natValInt8
        , natValInt16
        , natValInt32
        , natValInt64
        , natValWord
        , natValWord8
        , natValWord16
        , natValWord32
        , natValWord64
        -- * Maximum bounds
        , NatNumMaxBound
        -- * Constraint
        , NatInBoundOf
        , NatWithinBound
        ) where

    #include "MachDeps.h"

    import           GHC.TypeLits
    import           Basement.Compat.Base
    import           Basement.Compat.Natural
    import           Basement.Types.Char7 (Char7)
    import           Basement.Types.Word128 (Word128)
    import           Basement.Types.Word256 (Word256)
    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 :: forall (n :: Nat) (proxy :: Nat -> Type).
    KnownNat n =>
    proxy n -> Nat
    natValNatural proxy n
    n = Integer -> Nat
    forall a b. (Integral a, Num b) => a -> b
    Prelude.fromIntegral (proxy n -> Integer
    forall (n :: Nat) (proxy :: Nat -> Type).
    KnownNat n =>
    proxy n -> Integer
    natVal proxy n
    n)

    natValInt :: forall n proxy . (KnownNat n, NatWithinBound Int n) => proxy n -> Int
    natValInt :: forall (n :: Nat) (proxy :: Nat -> Type).
    (KnownNat n, NatWithinBound Int n) =>
    proxy n -> Int
    natValInt proxy n
    n = Integer -> Int
    forall a b. (Integral a, Num b) => a -> b
    Prelude.fromIntegral (proxy n -> Integer
    forall (n :: Nat) (proxy :: Nat -> Type).
    KnownNat n =>
    proxy n -> Integer
    natVal proxy n
    n)

    natValInt64 :: forall n proxy . (KnownNat n, NatWithinBound Int64 n) => proxy n -> Int64
    natValInt64 :: forall (n :: Nat) (proxy :: Nat -> Type).
    (KnownNat n, NatWithinBound Int64 n) =>
    proxy n -> Int64
    natValInt64 proxy n
    n = Integer -> Int64
    forall a b. (Integral a, Num b) => a -> b
    Prelude.fromIntegral (proxy n -> Integer
    forall (n :: Nat) (proxy :: Nat -> Type).
    KnownNat n =>
    proxy n -> Integer
    natVal proxy n
    n)

    natValInt32 :: forall n proxy . (KnownNat n, NatWithinBound Int32 n) => proxy n -> Int32
    natValInt32 :: forall (n :: Nat) (proxy :: Nat -> Type).
    (KnownNat n, NatWithinBound Int32 n) =>
    proxy n -> Int32
    natValInt32 proxy n
    n = Integer -> Int32
    forall a b. (Integral a, Num b) => a -> b
    Prelude.fromIntegral (proxy n -> Integer
    forall (n :: Nat) (proxy :: Nat -> Type).
    KnownNat n =>
    proxy n -> Integer
    natVal proxy n
    n)

    natValInt16 :: forall n proxy . (KnownNat n, NatWithinBound Int16 n) => proxy n -> Int16
    natValInt16 :: forall (n :: Nat) (proxy :: Nat -> Type).
    (KnownNat n, NatWithinBound Int16 n) =>
    proxy n -> Int16
    natValInt16 proxy n
    n = Integer -> Int16
    forall a b. (Integral a, Num b) => a -> b
    Prelude.fromIntegral (proxy n -> Integer
    forall (n :: Nat) (proxy :: Nat -> Type).
    KnownNat n =>
    proxy n -> Integer
    natVal proxy n
    n)

    natValInt8 :: forall n proxy . (KnownNat n, NatWithinBound Int8 n) => proxy n -> Int8
    natValInt8 :: forall (n :: Nat) (proxy :: Nat -> Type).
    (KnownNat n, NatWithinBound Int8 n) =>
    proxy n -> Int8
    natValInt8 proxy n
    n = Integer -> Int8
    forall a b. (Integral a, Num b) => a -> b
    Prelude.fromIntegral (proxy n -> Integer
    forall (n :: Nat) (proxy :: Nat -> Type).
    KnownNat n =>
    proxy n -> Integer
    natVal proxy n
    n)

    natValWord :: forall n proxy . (KnownNat n, NatWithinBound Word n) => proxy n -> Word
    natValWord :: forall (n :: Nat) (proxy :: Nat -> Type).
    (KnownNat n, NatWithinBound Word n) =>
    proxy n -> Word
    natValWord proxy n
    n = Integer -> Word
    forall a b. (Integral a, Num b) => a -> b
    Prelude.fromIntegral (proxy n -> Integer
    forall (n :: Nat) (proxy :: Nat -> Type).
    KnownNat n =>
    proxy n -> Integer
    natVal proxy n
    n)

    natValWord64 :: forall n proxy . (KnownNat n, NatWithinBound Word64 n) => proxy n -> Word64
    natValWord64 :: forall (n :: Nat) (proxy :: Nat -> Type).
    (KnownNat n, NatWithinBound Word64 n) =>
    proxy n -> Word64
    natValWord64 proxy n
    n = Integer -> Word64
    forall a b. (Integral a, Num b) => a -> b
    Prelude.fromIntegral (proxy n -> Integer
    forall (n :: Nat) (proxy :: Nat -> Type).
    KnownNat n =>
    proxy n -> Integer
    natVal proxy n
    n)

    natValWord32 :: forall n proxy . (KnownNat n, NatWithinBound Word32 n) => proxy n -> Word32
    natValWord32 :: forall (n :: Nat) (proxy :: Nat -> Type).
    (KnownNat n, NatWithinBound Word32 n) =>
    proxy n -> Word32
    natValWord32 proxy n
    n = Integer -> Word32
    forall a b. (Integral a, Num b) => a -> b
    Prelude.fromIntegral (proxy n -> Integer
    forall (n :: Nat) (proxy :: Nat -> Type).
    KnownNat n =>
    proxy n -> Integer
    natVal proxy n
    n)

    natValWord16 :: forall n proxy . (KnownNat n, NatWithinBound Word16 n) => proxy n -> Word16
    natValWord16 :: forall (n :: Nat) (proxy :: Nat -> Type).
    (KnownNat n, NatWithinBound Word16 n) =>
    proxy n -> Word16
    natValWord16 proxy n
    n = Integer -> Word16
    forall a b. (Integral a, Num b) => a -> b
    Prelude.fromIntegral (proxy n -> Integer
    forall (n :: Nat) (proxy :: Nat -> Type).
    KnownNat n =>
    proxy n -> Integer
    natVal proxy n
    n)

    natValWord8 :: forall n proxy . (KnownNat n, NatWithinBound Word8 n) => proxy n -> Word8
    natValWord8 :: forall (n :: Nat) (proxy :: Nat -> Type).
    (KnownNat n, NatWithinBound Word8 n) =>
    proxy n -> Word8
    natValWord8 proxy n
    n = Integer -> Word8
    forall a b. (Integral a, Num b) => a -> b
    Prelude.fromIntegral (proxy n -> Integer
    forall (n :: Nat) (proxy :: Nat -> Type).
    KnownNat n =>
    proxy n -> Integer
    natVal proxy n
    n)

    -- | Get Maximum bounds of different Integral / Natural types related to Nat
    type family NatNumMaxBound ty :: Nat

    type instance NatNumMaxBound Char   = 0x10ffff
    type instance NatNumMaxBound Char7  = 0x7f
    type instance NatNumMaxBound Int64  = 0x7fffffffffffffff
    type instance NatNumMaxBound Int32  = 0x7fffffff
    type instance NatNumMaxBound Int16  = 0x7fff
    type instance NatNumMaxBound Int8   = 0x7f
    type instance NatNumMaxBound Word256 = 0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff
    type instance NatNumMaxBound Word128 = 0xffffffffffffffffffffffffffffffff
    type instance NatNumMaxBound Word64 = 0xffffffffffffffff
    type instance NatNumMaxBound Word32 = 0xffffffff
    type instance NatNumMaxBound Word16 = 0xffff
    type instance NatNumMaxBound Word8  = 0xff
    #if WORD_SIZE_IN_BITS == 64
    type instance NatNumMaxBound Int    = NatNumMaxBound Int64
    type instance NatNumMaxBound Word   = NatNumMaxBound Word64
    #else
    type instance NatNumMaxBound Int    = NatNumMaxBound Int32
    type instance NatNumMaxBound Word   = NatNumMaxBound Word32
    #endif

    -- | Check if a Nat is in bounds of another integral / natural types
    type family NatInBoundOf ty n where
        NatInBoundOf Integer n = 'True
        NatInBoundOf Natural n = 'True
        NatInBoundOf ty      n = n <=? NatNumMaxBound ty

    -- | Constraint to check if a natural is within a specific bounds of a type.
    --
    -- i.e. given a Nat `n`, is it possible to convert it to `ty` without losing information
    #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