{-# LANGUAGE DataKinds #-}
{-# LANGUAGE NoStarIsType #-}
{-# LANGUAGE TypeOperators #-}
module GHC.TypeNats.Experimental (
    plusSNat,
    timesSNat,
    powerSNat,
    minusSNat,
    divSNat,
    modSNat,
    log2SNat,
) where

import GHC.Internal.TypeNats
import GHC.Num.Natural (naturalLog2)

plusSNat :: SNat n -> SNat m -> SNat (n + m)
plusSNat :: forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n + m)
plusSNat (UnsafeSNat Nat
n) (UnsafeSNat Nat
m) = Nat -> SNat (n + m)
forall (n :: Nat). Nat -> SNat n
UnsafeSNat (Nat
n Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
+ Nat
m)

timesSNat :: SNat n -> SNat m -> SNat (n * m)
timesSNat :: forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n * m)
timesSNat (UnsafeSNat Nat
n) (UnsafeSNat Nat
m) = Nat -> SNat (n * m)
forall (n :: Nat). Nat -> SNat n
UnsafeSNat (Nat
n Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
* Nat
m)

powerSNat :: SNat n -> SNat m -> SNat (n ^ m)
powerSNat :: forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n ^ m)
powerSNat (UnsafeSNat Nat
n) (UnsafeSNat Nat
m) = Nat -> SNat (n ^ m)
forall (n :: Nat). Nat -> SNat n
UnsafeSNat (Nat
n Nat -> Nat -> Nat
forall a b. (Num a, Integral b) => a -> b -> a
^ Nat
m)

minusSNat :: (m <= n) => SNat n -> SNat m -> SNat (n - m)
minusSNat :: forall (m :: Nat) (n :: Nat).
(m <= n) =>
SNat n -> SNat m -> SNat (n - m)
minusSNat (UnsafeSNat Nat
n) (UnsafeSNat Nat
m) = Nat -> SNat (n - m)
forall (n :: Nat). Nat -> SNat n
UnsafeSNat (Nat
n Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
- Nat
m)

divSNat :: (1 <= m) => SNat n -> SNat m -> SNat (Div n m)
divSNat :: forall (m :: Nat) (n :: Nat).
(1 <= m) =>
SNat n -> SNat m -> SNat (Div n m)
divSNat (UnsafeSNat Nat
n) (UnsafeSNat Nat
m) = Nat -> SNat (Div n m)
forall (n :: Nat). Nat -> SNat n
UnsafeSNat (Nat -> Nat -> Nat
forall a. Integral a => a -> a -> a
div Nat
n Nat
m)

modSNat :: (1 <= m) => SNat n -> SNat m -> SNat (Mod n m)
modSNat :: forall (m :: Nat) (n :: Nat).
(1 <= m) =>
SNat n -> SNat m -> SNat (Mod n m)
modSNat (UnsafeSNat Nat
n) (UnsafeSNat Nat
m) = Nat -> SNat (Mod n m)
forall (n :: Nat). Nat -> SNat n
UnsafeSNat (Nat -> Nat -> Nat
forall a. Integral a => a -> a -> a
mod Nat
n Nat
m)

log2SNat :: (1 <= n) => SNat n -> SNat (Log2 n)
log2SNat :: forall (n :: Nat). (1 <= n) => SNat n -> SNat (Log2 n)
log2SNat (UnsafeSNat Nat
n) = Nat -> SNat (Log2 n)
forall (n :: Nat). Nat -> SNat n
UnsafeSNat (Word -> Nat
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Nat -> Word
naturalLog2 Nat
n))