{-# 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 #-}

{-| This module is an internal GHC module.  It declares the constants used
in the implementation of type-level natural numbers.  The programmer interface
for working with type-level naturals should be defined in a separate library.

@since 4.10.0.0
-}

module GHC.TypeNats
  ( -- * Nat Kind
    Nat -- declared in GHC.Types in package ghc-prim

    -- * Linking type and value level
  , KnownNat, natVal, natVal'
  , SomeNat(..)
  , someNatVal
  , sameNat

    -- * Functions on type literals
  , 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)

--------------------------------------------------------------------------------

-- | This class gives the integer associated with a type-level natural.
-- There are instances of the class for every concrete literal: 0, 1, 2, etc.
--
-- @since 4.7.0.0
class KnownNat (n :: Nat) where
  natSing :: SNat n

-- | @since 4.10.0.0
natVal :: forall n proxy. KnownNat n => proxy n -> Natural
natVal :: proxy n -> Natural
natVal _ = case SNat n
forall (n :: Nat). KnownNat n => SNat n
natSing :: SNat n of
             SNat x :: Natural
x -> Natural
x

-- | @since 4.10.0.0
natVal' :: forall n. KnownNat n => Proxy# n -> Natural
natVal' :: Proxy# n -> Natural
natVal' _ = case SNat n
forall (n :: Nat). KnownNat n => SNat n
natSing :: SNat n of
             SNat x :: Natural
x -> Natural
x

-- | This type represents unknown type-level natural numbers.
--
-- @since 4.10.0.0
data SomeNat    = forall n. KnownNat n    => SomeNat    (Proxy n)

-- | Convert an integer into an unknown type-level natural.
--
-- @since 4.10.0.0
someNatVal :: Natural -> SomeNat
someNatVal :: Natural -> SomeNat
someNatVal n :: Natural
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 (Natural -> SNat Any
forall (n :: Nat). Natural -> SNat n
SNat Natural
n) Proxy Any
forall k (t :: k). Proxy t
Proxy

-- | @since 4.7.0.0
instance Eq SomeNat where
  SomeNat x :: Proxy n
x == :: SomeNat -> SomeNat -> Bool
== SomeNat y :: Proxy n
y = Proxy n -> Natural
forall (n :: Nat) (proxy :: Nat -> Type).
KnownNat n =>
proxy n -> Natural
natVal Proxy n
x Natural -> Natural -> Bool
forall a. Eq a => a -> a -> Bool
== Proxy n -> Natural
forall (n :: Nat) (proxy :: Nat -> Type).
KnownNat n =>
proxy n -> Natural
natVal Proxy n
y

-- | @since 4.7.0.0
instance Ord SomeNat where
  compare :: SomeNat -> SomeNat -> Ordering
compare (SomeNat x :: Proxy n
x) (SomeNat y :: Proxy n
y) = Natural -> Natural -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (Proxy n -> Natural
forall (n :: Nat) (proxy :: Nat -> Type).
KnownNat n =>
proxy n -> Natural
natVal Proxy n
x) (Proxy n -> Natural
forall (n :: Nat) (proxy :: Nat -> Type).
KnownNat n =>
proxy n -> Natural
natVal Proxy n
y)

-- | @since 4.7.0.0
instance Show SomeNat where
  showsPrec :: Int -> SomeNat -> ShowS
showsPrec p :: Int
p (SomeNat x :: Proxy n
x) = Int -> Natural -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
p (Proxy n -> Natural
forall (n :: Nat) (proxy :: Nat -> Type).
KnownNat n =>
proxy n -> Natural
natVal Proxy n
x)

-- | @since 4.7.0.0
instance Read SomeNat where
  readsPrec :: Int -> ReadS SomeNat
readsPrec p :: Int
p xs :: String
xs = do (a :: Natural
a,ys :: String
ys) <- Int -> ReadS Natural
forall a. Read a => Int -> ReadS a
readsPrec Int
p String
xs
                      [(Natural -> SomeNat
someNatVal Natural
a, String
ys)]

--------------------------------------------------------------------------------

infix  4 <=?, <=
infixl 6 +, -
infixl 7 *, `Div`, `Mod`
infixr 8 ^

-- | Comparison of type-level naturals, as a constraint.
--
-- @since 4.7.0.0
type x <= y = (x <=? y) ~ 'True

-- | Comparison of type-level naturals, as a function.
--
-- @since 4.7.0.0
type family CmpNat    (m :: Nat)    (n :: Nat)    :: Ordering

{- | Comparison of type-level naturals, as a function.
NOTE: The functionality for this function should be subsumed
by 'CmpNat', so this might go away in the future.
Please let us know, if you encounter discrepancies between the two. -}
type family (m :: Nat) <=? (n :: Nat) :: Bool

-- | Addition of type-level naturals.
--
-- @since 4.7.0.0
type family (m :: Nat) + (n :: Nat) :: Nat

-- | Multiplication of type-level naturals.
--
-- @since 4.7.0.0
type family (m :: Nat) * (n :: Nat) :: Nat

-- | Exponentiation of type-level naturals.
--
-- @since 4.7.0.0
type family (m :: Nat) ^ (n :: Nat) :: Nat

-- | Subtraction of type-level naturals.
--
-- @since 4.7.0.0
type family (m :: Nat) - (n :: Nat) :: Nat

-- | Division (round down) of natural numbers.
-- @Div x 0@ is undefined (i.e., it cannot be reduced).
--
-- @since 4.11.0.0
type family Div (m :: Nat) (n :: Nat) :: Nat

-- | Modulus of natural numbers.
-- @Mod x 0@ is undefined (i.e., it cannot be reduced).
--
-- @since 4.11.0.0
type family Mod (m :: Nat) (n :: Nat) :: Nat

-- | Log base 2 (round down) of natural numbers.
-- @Log 0@ is undefined (i.e., it cannot be reduced).
--
-- @since 4.11.0.0
type family Log2 (m :: Nat) :: Nat

--------------------------------------------------------------------------------

-- | We either get evidence that this function was instantiated with the
-- same type-level numbers, or 'Nothing'.
--
-- @since 4.7.0.0
sameNat :: (KnownNat a, KnownNat b) =>
           Proxy a -> Proxy b -> Maybe (a :~: b)
sameNat :: Proxy a -> Proxy b -> Maybe (a :~: b)
sameNat x :: Proxy a
x y :: Proxy b
y
  | Proxy a -> Natural
forall (n :: Nat) (proxy :: Nat -> Type).
KnownNat n =>
proxy n -> Natural
natVal Proxy a
x Natural -> Natural -> Bool
forall a. Eq a => a -> a -> Bool
== Proxy b -> Natural
forall (n :: Nat) (proxy :: Nat -> Type).
KnownNat n =>
proxy n -> Natural
natVal Proxy 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

--------------------------------------------------------------------------------
-- PRIVATE:

newtype SNat    (n :: Nat)    = SNat    Natural

data WrapN a b = WrapN (KnownNat    a => Proxy a -> b)

-- See Note [magicDictId magic] in "basicType/MkId.hs"
withSNat :: (KnownNat a => Proxy a -> b)
         -> SNat a      -> Proxy a -> b
withSNat :: (KnownNat a => Proxy a -> b) -> SNat a -> Proxy a -> b
withSNat f :: KnownNat a => Proxy a -> b
f x :: SNat a
x y :: 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