{-|
Copyright  :  (C) 2015-2016, University of Twente,
                  2017-2018, QBayLogic B.V.
License    :  BSD2 (see the file LICENSE)
Maintainer :  Christiaan Baaij <christiaan.baaij@gmail.com>

Additional type-level operations on 'GHC.TypeLits.Nat':

  * 'Max': type-level 'max'

  * 'Min': type-level 'min'

  * 'Div': type-level 'div'

  * 'Mod': type-level 'mod'

  * 'FLog': type-level equivalent of <https://hackage.haskell.org/package/base-4.17.0.0/docs/GHC-Integer-Logarithms.html#v:integerLogBase-35- integerLogBase#>
    .i.e. the exact integer equivalent to "@'floor' ('logBase' x y)@"

  * 'CLog': type-level equivalent of /the ceiling of/ <https://hackage.haskell.org/package/base-4.17.0.0/docs/GHC-Integer-Logarithms.html#v:integerLogBase-35- integerLogBase#>
    .i.e. the exact integer equivalent to "@'ceiling' ('logBase' x y)@"

  * 'Log': type-level equivalent of <https://hackage.haskell.org/package/base-4.17.0.0/docs/GHC-Integer-Logarithms.html#v:integerLogBase-35- integerLogBase#>
     where the operation only reduces when "@'floor' ('logBase' b x) ~ 'ceiling' ('logBase' b x)@"

  * 'GCD': a type-level 'gcd'

  * 'LCM': a type-level 'lcm'

A custom solver for the above operations defined is defined in
"GHC.TypeLits.Extra.Solver" as a GHC type-checker plugin. To use the plugin,
add the

@
{\-\# OPTIONS_GHC -fplugin GHC.TypeLits.Extra.Solver \#-\}
@

pragma to the header of your file.
-}

{-# LANGUAGE CPP                   #-}
{-# LANGUAGE DataKinds             #-}
{-# LANGUAGE FlexibleInstances     #-}
{-# LANGUAGE GADTs                 #-}
{-# LANGUAGE MagicHash             #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE ScopedTypeVariables   #-}
{-# LANGUAGE TemplateHaskell       #-}
{-# LANGUAGE TypeApplications      #-}
{-# LANGUAGE TypeFamilies          #-}
{-# LANGUAGE TypeOperators         #-}
{-# LANGUAGE UndecidableInstances  #-}

{-# OPTIONS_HADDOCK show-extensions #-}
{-# OPTIONS_GHC -Wno-orphans #-}

{-# LANGUAGE Trustworthy #-}

module GHC.TypeLits.Extra
  ( -- * Type-level operations on `Nat`
    -- ** Ord
    Max
  , Min
    -- ** Integral
  , Div
  , Mod
  , DivMod
    -- *** Variants
  , DivRU
    -- ** Logarithm
  , FLog
  , CLog
    -- *** Exact logarithm
  , Log
    -- Numeric
  , GCD
  , LCM
  )
where

import Data.Proxy             (Proxy (..))
import Data.Type.Bool         (If)
import GHC.Base               (Int#,isTrue#,(==#),(+#))
#if MIN_VERSION_ghc(9,4,0)
import GHC.Base               (Constraint)
#endif
import GHC.Integer.Logarithms (integerLogBase#)
#if MIN_VERSION_ghc(8,2,0)
import GHC.Magic              (noinline)
#endif
#if MIN_VERSION_ghc(8,2,0)
import qualified GHC.TypeNats as N
import GHC.Natural
import GHC.Prim               (int2Word#)
import GHC.TypeLits
#else
import GHC.Integer            (smallInteger)
import GHC.TypeLits           as N
#endif
  (KnownNat, Nat, type (+), type (-), type (<=), type (<=?), natVal)
#if MIN_VERSION_ghc(8,4,0)
import GHC.TypeLits           (Div, Mod)
#endif
import GHC.TypeLits.KnownNat  (KnownNat2 (..), SNatKn (..), nameToSymbol)

#if MIN_VERSION_ghc(8,2,0)
intToNumber :: Int# -> Natural
intToNumber :: Int# -> Natural
intToNumber Int#
x = Word# -> Natural
NatS# (Int# -> Word#
int2Word# Int#
x)
#else
intToNumber :: Int# -> Integer
intToNumber x = smallInteger x
#endif
{-# INLINE intToNumber #-}

-- | Type-level 'max'
type family Max (x :: Nat) (y :: Nat) :: Nat where
  Max n n = n
  Max x y = If (x <=? y) y x

instance (KnownNat x, KnownNat y) => KnownNat2 $(nameToSymbol ''Max) x y where
  natSing2 :: SNatKn "GHC.TypeLits.Extra.Max"
natSing2 = forall (f :: Symbol). Natural -> SNatKn f
SNatKn (forall a. Ord a => a -> a -> a
max (forall (n :: Natural) (proxy :: Natural -> *).
KnownNat n =>
proxy n -> Natural
N.natVal (forall {k} (t :: k). Proxy t
Proxy @x)) (forall (n :: Natural) (proxy :: Natural -> *).
KnownNat n =>
proxy n -> Natural
N.natVal (forall {k} (t :: k). Proxy t
Proxy @y)))

-- | Type-level 'min'
type family Min (x :: Nat) (y :: Nat) :: Nat where
  Min n n = n
  Min x y = If (x <=? y) x y

instance (KnownNat x, KnownNat y) => KnownNat2 $(nameToSymbol ''Min) x y where
  natSing2 :: SNatKn "GHC.TypeLits.Extra.Min"
natSing2 = forall (f :: Symbol). Natural -> SNatKn f
SNatKn (forall a. Ord a => a -> a -> a
min (forall (n :: Natural) (proxy :: Natural -> *).
KnownNat n =>
proxy n -> Natural
N.natVal (forall {k} (t :: k). Proxy t
Proxy @x)) (forall (n :: Natural) (proxy :: Natural -> *).
KnownNat n =>
proxy n -> Natural
N.natVal (forall {k} (t :: k). Proxy t
Proxy @y)))

#if !MIN_VERSION_ghc(8,4,0)
-- | Type-level 'div'
--
-- Note that additional equations are provided by the type-checker plugin solver
-- "GHC.TypeLits.Extra.Solver".
type family Div (dividend :: Nat) (divisor :: Nat) :: Nat where
  Div x 1 = x

instance (KnownNat x, KnownNat y, 1 <= y) => KnownNat2 $(nameToSymbol ''Div) x y where
  natSing2 = SNatKn (quot (N.natVal (Proxy @x)) (N.natVal (Proxy @y)))
#endif

-- | A variant of 'Div' that rounds up instead of down
type DivRU n d = Div (n + (d - 1)) d

#if !MIN_VERSION_ghc(8,4,0)
-- | Type-level 'mod'
--
-- Note that additional equations are provided by the type-checker plugin solver
-- "GHC.TypeLits.Extra.Solver".
type family Mod (x :: Nat) (y :: Nat) :: Nat where
  Mod x 1 = 0

instance (KnownNat x, KnownNat y, 1 <= y) => KnownNat2 $(nameToSymbol ''Mod) x y where
  natSing2 = SNatKn (rem (N.natVal (Proxy @x)) (N.natVal (Proxy @y)))
#endif

-- | Type-level `divMod`
type DivMod n d = '(Div n d, Mod n d)

-- | Type-level equivalent of <https://hackage.haskell.org/package/base-4.17.0.0/docs/GHC-Integer-Logarithms.html#v:integerLogBase-35- integerLogBase#>
-- .i.e. the exact integer equivalent to "@'floor' ('logBase' base value)@"
--
-- Note that additional equations are provided by the type-checker plugin solver
-- "GHC.TypeLits.Extra.Solver".
type family FLog (base :: Nat) (value :: Nat) :: Nat where
  FLog 2 1 = 0 -- Additional equations are provided by the custom solver

instance (KnownNat x, KnownNat y, 2 <= x, 1 <= y) => KnownNat2 $(nameToSymbol ''FLog) x y where
#if MIN_VERSION_ghc (8,2,0)
  natSing2 :: SNatKn "GHC.TypeLits.Extra.FLog"
natSing2 = forall (f :: Symbol). Natural -> SNatKn f
SNatKn (Int# -> Natural
intToNumber (Integer -> Integer -> Int#
integerLogBase# (forall (n :: Natural) (proxy :: Natural -> *).
KnownNat n =>
proxy n -> Integer
natVal (forall {k} (t :: k). Proxy t
Proxy @x)) (forall (n :: Natural) (proxy :: Natural -> *).
KnownNat n =>
proxy n -> Integer
natVal (forall {k} (t :: k). Proxy t
Proxy @y))))
#else
  natSing2 = SNatKn (intToNumber (integerLogBase# (natVal (Proxy @x)) (natVal (Proxy @y))))
#endif

-- | Type-level equivalent of /the ceiling of/ <https://hackage.haskell.org/package/base-4.17.0.0/docs/GHC-Integer-Logarithms.html#v:integerLogBase-35- integerLogBase#>
-- .i.e. the exact integer equivalent to "@'ceiling' ('logBase' base value)@"
--
-- Note that additional equations are provided by the type-checker plugin solver
-- "GHC.TypeLits.Extra.Solver".
type family CLog (base :: Nat) (value :: Nat) :: Nat where
  CLog 2 1 = 0 -- Additional equations are provided by the custom solver

#if MIN_VERSION_ghc(9,4,0)
instance (KnownNat x, KnownNat y, (2 <= x) ~ (() :: Constraint), 1 <= y) => KnownNat2 $(nameToSymbol ''CLog) x y where
#else
instance (KnownNat x, KnownNat y, 2 <= x, 1 <= y) => KnownNat2 $(nameToSymbol ''CLog) x y where
#endif
  natSing2 :: SNatKn "GHC.TypeLits.Extra.CLog"
natSing2 = let x :: Integer
x  = forall (n :: Natural) (proxy :: Natural -> *).
KnownNat n =>
proxy n -> Integer
natVal (forall {k} (t :: k). Proxy t
Proxy @x)
                 y :: Integer
y  = forall (n :: Natural) (proxy :: Natural -> *).
KnownNat n =>
proxy n -> Integer
natVal (forall {k} (t :: k). Proxy t
Proxy @y)
                 z1 :: Int#
z1 = Integer -> Integer -> Int#
integerLogBase# Integer
x Integer
y
                 z2 :: Int#
z2 = Integer -> Integer -> Int#
integerLogBase# Integer
x (Integer
yforall a. Num a => a -> a -> a
-Integer
1)
             in  case Integer
y of
                    Integer
1 -> forall (f :: Symbol). Natural -> SNatKn f
SNatKn Natural
0
                    Integer
_ | Int# -> Bool
isTrue# (Int#
z1 Int# -> Int# -> Int#
==# Int#
z2) -> forall (f :: Symbol). Natural -> SNatKn f
SNatKn (Int# -> Natural
intToNumber (Int#
z1 Int# -> Int# -> Int#
+# Int#
1#))
                      | Bool
otherwise           -> forall (f :: Symbol). Natural -> SNatKn f
SNatKn (Int# -> Natural
intToNumber Int#
z1)

-- | Type-level equivalent of <https://hackage.haskell.org/package/base-4.17.0.0/docs/GHC-Integer-Logarithms.html#v:integerLogBase-35- integerLogBase#>
-- where the operation only reduces when:
--
-- @
-- 'FLog' base value ~ 'CLog' base value
-- @
--
-- Additionally, the following property holds for 'Log':
--
-- > (base ^ (Log base value)) ~ value
--
-- Note that additional equations are provided by the type-checker plugin solver
-- "GHC.TypeLits.Extra.Solver".
type family Log (base :: Nat) (value :: Nat) :: Nat where
  Log 2 1 = 0 -- Additional equations are provided by the custom solver

instance (KnownNat x, KnownNat y, FLog x y ~ CLog x y) => KnownNat2 $(nameToSymbol ''Log) x y where
  natSing2 :: SNatKn "GHC.TypeLits.Extra.Log"
natSing2 = forall (f :: Symbol). Natural -> SNatKn f
SNatKn (Int# -> Natural
intToNumber (Integer -> Integer -> Int#
integerLogBase# (forall (n :: Natural) (proxy :: Natural -> *).
KnownNat n =>
proxy n -> Integer
natVal (forall {k} (t :: k). Proxy t
Proxy @x)) (forall (n :: Natural) (proxy :: Natural -> *).
KnownNat n =>
proxy n -> Integer
natVal (forall {k} (t :: k). Proxy t
Proxy @y))))

-- | Type-level greatest common denominator (GCD).
--
-- Note that additional equations are provided by the type-checker plugin solver
-- "GHC.TypeLits.Extra.Solver".
type family GCD (x :: Nat) (y :: Nat) :: Nat where
  GCD 0 x = x
  GCD x 0 = x
  GCD 1 x = 1
  GCD x 1 = 1
  GCD x x = x
  -- Additional equations are provided by the custom solver

instance (KnownNat x, KnownNat y) => KnownNat2 $(nameToSymbol ''GCD) x y where
  natSing2 :: SNatKn "GHC.TypeLits.Extra.GCD"
natSing2 = forall (f :: Symbol). Natural -> SNatKn f
SNatKn (
#if MIN_VERSION_ghc(8,2,0)
    forall a. a -> a
noinline
#endif
      forall a. Integral a => a -> a -> a
gcd (forall (n :: Natural) (proxy :: Natural -> *).
KnownNat n =>
proxy n -> Natural
N.natVal (forall {k} (t :: k). Proxy t
Proxy @x)) (forall (n :: Natural) (proxy :: Natural -> *).
KnownNat n =>
proxy n -> Natural
N.natVal (forall {k} (t :: k). Proxy t
Proxy @y)))

-- | Type-level least common multiple (LCM).
--
-- Note that additional equations are provided by the type-checker plugin solver
-- "GHC.TypeLits.Extra.Solver".
type family LCM (x :: Nat) (y :: Nat) :: Nat where
  LCM 0 x = 0
  LCM x 0 = 0
  LCM 1 x = x
  LCM x 1 = x
  LCM x x = x
  -- Additional equations are provided by the custom solver

instance (KnownNat x, KnownNat y) => KnownNat2 $(nameToSymbol ''LCM) x y where
  natSing2 :: SNatKn "GHC.TypeLits.Extra.LCM"
natSing2 = forall (f :: Symbol). Natural -> SNatKn f
SNatKn (
#if MIN_VERSION_ghc(8,2,0)
    forall a. a -> a
noinline
#endif
      forall a. Integral a => a -> a -> a
lcm (forall (n :: Natural) (proxy :: Natural -> *).
KnownNat n =>
proxy n -> Natural
N.natVal (forall {k} (t :: k). Proxy t
Proxy @x)) (forall (n :: Natural) (proxy :: Natural -> *).
KnownNat n =>
proxy n -> Natural
N.natVal (forall {k} (t :: k). Proxy t
Proxy @y)))