{-# LANGUAGE UndecidableInstances #-}

-- | This module provides a type-level representation for term-level
-- 'P.Integer's. This type-level representation is also named 'P.Integer',
-- So import this module qualified to avoid name conflicts.
--
-- @
-- import "KindInteger" qualified as KI
-- @
--
-- The implementation details are the same as the ones for type-level 'Natural's
-- in "GHC.TypeNats" as of @base-4.18@, and it will continue to evolve together
-- with @base@, trying to follow its API as much as possible until the day
-- @base@ provides its own type-level integer, making this module redundant.
module KindInteger {--}
  ( -- * Integer kind
    Integer
  , type P
  , type N
  , Normalize

    -- * Prelude support
  , toPrelude
  , fromPrelude
  , showsPrecTypeLit

    -- * Types ⇔ Terms
  , KnownInteger(integerSing), integerVal
  , SomeInteger(..)
  , someIntegerVal
  , sameInteger

    -- * Singletons
  , SInteger
  , pattern SInteger
  , fromSInteger
  , withSomeSInteger
  , withKnownInteger

    -- * Arithmethic
  , type (+), type (*), type (^), type (-)
  , Odd, Even, Abs, Sign, Negate, GCD, LCM, Log2

    -- ** Division
  , Div
  , Rem
  , DivRem
  , Round(..)
    -- *** Term-level
  , div
  , rem
  , divRem

    -- * Comparisons
  , CmpInteger
  , cmpInteger

    -- * Extra
  , type (==?), type (==), type (/=?), type (/=)
  ) --}
  where

import Control.Exception qualified as Ex
import Data.Bits
import Data.Proxy
import Data.Type.Bool (If)
import Data.Type.Coercion
import Data.Type.Equality (TestEquality(..), (:~:)(..))
import Data.Type.Ord
import GHC.Base (WithDict(..))
import GHC.Real qualified as P
import GHC.Show (appPrec, appPrec1)
import GHC.TypeLits qualified as L
import GHC.Types (TYPE, Constraint)
import Numeric.Natural (Natural)
import Prelude hiding (Integer, (==), (/=), div, rem)
import Prelude qualified as P
import Unsafe.Coerce(unsafeCoerce)

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

-- | Type-level version of 'P.Integer', only ever used as a /kind/
-- for 'P' and 'N'
--
-- * A positive number /+x/ is represented as @'P' x@.
--
-- * A negative number /-x/ is represented as @'N' x@.
--
-- * /Zero/ can be represented as @'P' 0@ or @'N' 0@. For consistency, all
-- /zero/ outputs from type families in this "KindInteger" module use the
-- @'P' 0@, but don't assume that this will be the case elsewhere. So, if you
-- need to treat /zero/ specially in some situation, be sure to handle both the
-- @'P' 0@ and @'N' 0@ cases.
--
-- __NB__: 'Integer' is mostly used as a kind, with its types constructed
-- using 'P' and 'N'.  However, it might also be used as type, with its terms
-- constructed using 'fromPrelude'. One reason why you may want a 'Integer'
-- at the term-level is so that you embed it in larger data-types (for example,
-- the "KindRational" module from the
-- [@kind-rational@](https://hackage.haskell.org/package/kind-rational)
-- library embeds this 'I.Integer' in its 'KindRational.Rational' type)
data Integer
  = P_ Natural
  | N_ Natural

instance Eq Integer where
  Integer
a == :: Integer -> Integer -> Bool
== Integer
b = Integer -> Integer
toPrelude Integer
a Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
P.== Integer -> Integer
toPrelude Integer
b

instance Ord Integer where
  compare :: Integer -> Integer -> Ordering
compare Integer
a Integer
b = Integer -> Integer -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (Integer -> Integer
toPrelude Integer
a) (Integer -> Integer
toPrelude Integer
b)
  Integer
a <= :: Integer -> Integer -> Bool
<= Integer
b = Integer -> Integer
toPrelude Integer
a Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= Integer -> Integer
toPrelude Integer
b

-- | Same as "Prelude" 'P.Integer'.
instance Show Integer where
  showsPrec :: Int -> Integer -> ShowS
showsPrec Int
p = Int -> Integer -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
p (Integer -> ShowS) -> (Integer -> Integer) -> Integer -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> Integer
toPrelude

-- | Same as "Prelude" 'P.Integer'.
instance Read Integer where
  readsPrec :: Int -> ReadS Integer
readsPrec Int
p String
xs = do (Integer
a, String
ys) <- Int -> ReadS Integer
forall a. Read a => Int -> ReadS a
readsPrec Int
p String
xs
                      [(Integer -> Integer
fromPrelude Integer
a, String
ys)]

-- | Shows the 'Integer' as it appears literally at the type-level.
--
-- This is different from normal 'show' for 'Integer', which shows
-- the term-level value.
--
-- @
-- 'shows'            0 ('fromPrelude' 8) \"z\" == \"8z\"
-- 'showsPrecTypeLit' 0 ('fromPrelude' 8) \"z\" == \"P 8z\"
-- @
showsPrecTypeLit :: Int -> Integer -> ShowS
showsPrecTypeLit :: Int -> Integer -> ShowS
showsPrecTypeLit Int
p Integer
i = Bool -> ShowS -> ShowS
showParen (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
appPrec) (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ case Integer
i of
  P_ Natural
x -> String -> ShowS
showString String
"P " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Natural -> ShowS
forall a. Show a => a -> ShowS
shows Natural
x
  N_ Natural
x -> String -> ShowS
showString String
"N " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Natural -> ShowS
forall a. Show a => a -> ShowS
shows Natural
x

-- | * A positive number /+x/ is represented as @'P' x@.
--
-- * /Zero/ can be represented as @'P' 0@ (see notes at 'Integer').
type P (x :: Natural) = 'P_ x :: Integer

-- | * A negative number /-x/ is represented as @'N' x@.
--
-- * /Zero/ can be represented as @'N' 0@ (but often isn't, see notes at 'Integer').
type N (x :: Natural) = 'N_ x :: Integer

-- | Convert a term-level "KindInteger" 'Integer' into a term-level
-- "Prelude" 'P.Integer'.
--
-- @
-- 'fromPrelude' . 'toPrelude' == 'id'
-- 'toPrelude' . 'fromPrelude' == 'id'
-- @
toPrelude :: Integer -> P.Integer
toPrelude :: Integer -> Integer
toPrelude (P_ Natural
n) = Natural -> Integer
forall a. Integral a => a -> Integer
toInteger Natural
n
toPrelude (N_ Natural
n) = Integer -> Integer
forall a. Num a => a -> a
negate (Natural -> Integer
forall a. Integral a => a -> Integer
toInteger Natural
n)

-- | Obtain a term-level "KindInteger" 'Integer' from a term-level
-- "Prelude" 'P.Integer'. This can fail if the "Prelude" 'P.Integer' is
-- infinite, or if it is so big that it would exhaust system resources.
--
-- @
-- 'fromPrelude' . 'toPrelude' == 'id'
-- 'toPrelude' . 'fromPrelude' == 'id'
-- @
--
-- This function can be handy if you are passing "KindInteger"'s 'Integer'
-- around for some reason. But, other than this, "KindInteger" doesn't offer
-- any tool to deal with the internals of its 'Integer'.
fromPrelude :: P.Integer -> Integer
fromPrelude :: Integer -> Integer
fromPrelude Integer
i = if Integer
i Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer
0 then Natural -> Integer
P_ (Integer -> Natural
forall a. Num a => Integer -> a
fromInteger Integer
i)
                          else Natural -> Integer
N_ (Integer -> Natural
forall a. Num a => Integer -> a
fromInteger (Integer -> Integer
forall a. Num a => a -> a
negate Integer
i))

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

-- | This class gives the integer associated with a type-level integer.
-- There are instances of the class for every integer.
class KnownInteger (i :: Integer) where
  integerSing :: SInteger i

-- | Positive numbers and zero.
instance L.KnownNat x => KnownInteger (P x) where
  integerSing :: SInteger (P x)
integerSing = Integer -> SInteger (P x)
forall (i :: Integer). Integer -> SInteger i
UnsafeSInteger (Proxy x -> Integer
forall (n :: Natural) (proxy :: Natural -> Type).
KnownNat n =>
proxy n -> Integer
L.natVal (forall (t :: Natural). Proxy t
forall {k} (t :: k). Proxy t
Proxy @x))

-- | Negative numbers and zero.
instance L.KnownNat x => KnownInteger (N x) where
  integerSing :: SInteger (N x)
integerSing = Integer -> SInteger (N x)
forall (i :: Integer). Integer -> SInteger i
UnsafeSInteger (Integer -> Integer
forall a. Num a => a -> a
negate (Proxy x -> Integer
forall (n :: Natural) (proxy :: Natural -> Type).
KnownNat n =>
proxy n -> Integer
L.natVal (forall (t :: Natural). Proxy t
forall {k} (t :: k). Proxy t
Proxy @x)))

-- | Term-level 'P.Integer' representation of the type-level 'Integer' @i@.
integerVal :: forall i proxy. KnownInteger i => proxy i -> P.Integer
integerVal :: forall (i :: Integer) (proxy :: Integer -> Type).
KnownInteger i =>
proxy i -> Integer
integerVal proxy i
_ = case SInteger i
forall (i :: Integer). KnownInteger i => SInteger i
integerSing :: SInteger i of UnsafeSInteger Integer
x -> Integer
x

-- | This type represents unknown type-level 'Integer'.
data SomeInteger = forall n. KnownInteger n => SomeInteger (Proxy n)

-- | Convert a term-level 'P.Integer' into an unknown type-level 'Integer'.
someIntegerVal :: P.Integer -> SomeInteger
someIntegerVal :: Integer -> SomeInteger
someIntegerVal Integer
i = Integer
-> (forall (n :: Integer). SInteger n -> SomeInteger)
-> SomeInteger
forall r. Integer -> (forall (n :: Integer). SInteger n -> r) -> r
withSomeSInteger Integer
i (\(SInteger n
si :: SInteger i) ->
                   SInteger n -> (KnownInteger n => SomeInteger) -> SomeInteger
forall (i :: Integer) r. SInteger i -> (KnownInteger i => r) -> r
withKnownInteger SInteger n
si (forall (n :: Integer). KnownInteger n => Proxy n -> SomeInteger
SomeInteger @i Proxy n
forall {k} (t :: k). Proxy t
Proxy))

instance Eq SomeInteger where
  SomeInteger Proxy n
x == :: SomeInteger -> SomeInteger -> Bool
== SomeInteger Proxy n
y = Proxy n -> Integer
forall (i :: Integer) (proxy :: Integer -> Type).
KnownInteger i =>
proxy i -> Integer
integerVal Proxy n
x Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
P.== Proxy n -> Integer
forall (i :: Integer) (proxy :: Integer -> Type).
KnownInteger i =>
proxy i -> Integer
integerVal Proxy n
y

instance Ord SomeInteger where
  compare :: SomeInteger -> SomeInteger -> Ordering
compare (SomeInteger Proxy n
x) (SomeInteger Proxy n
y) =
    Integer -> Integer -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (Proxy n -> Integer
forall (i :: Integer) (proxy :: Integer -> Type).
KnownInteger i =>
proxy i -> Integer
integerVal Proxy n
x) (Proxy n -> Integer
forall (i :: Integer) (proxy :: Integer -> Type).
KnownInteger i =>
proxy i -> Integer
integerVal Proxy n
y)

instance Show SomeInteger where
  showsPrec :: Int -> SomeInteger -> ShowS
showsPrec Int
p (SomeInteger Proxy n
x) = Int -> Integer -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
p (Proxy n -> Integer
forall (i :: Integer) (proxy :: Integer -> Type).
KnownInteger i =>
proxy i -> Integer
integerVal Proxy n
x)

instance Read SomeInteger where
  readsPrec :: Int -> ReadS SomeInteger
readsPrec Int
p String
xs = do (Integer
a, String
ys) <- Int -> ReadS Integer
forall a. Read a => Int -> ReadS a
readsPrec Int
p String
xs
                      [(Integer -> SomeInteger
someIntegerVal Integer
a, String
ys)]

--------------------------------------------------------------------------------
-- Within this module, we use these “normalization” tools to make sure that
-- /zero/ is always represented as @'P' 0@. We don't export any of these
-- normalization tools to end-users because it seems like we can't make them
-- reliable enough so as to offer a decent user experience. So, we just tell
-- users to deal with the fact that both @'P' 0@ and @'N' 0@ mean /zero/.

-- | Make sure /zero/ is represented as @'P' 0@, not as @'N' 0@
--
-- Notice that all the tools in the "KindInteger" can readily handle
-- non-'Normalize'd inputs. This 'Normalize' type-family is offered offered
-- only as a convenience in case you want to simplify /your/ dealing with
-- /zeros/.
type family Normalize (i :: Integer) :: Integer where
  Normalize (N 0) = P 0
  Normalize i     = i

-- | Construct a 'Normalize'd 'N'egative type-level 'Integer'.
--
-- To be used for producing all negative outputs in this module.
type NN (a :: Natural) = Normalize (N a) :: Integer

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

infixl 6 +, -
infixl 7 *, `Div`, `Rem`
infixr 8 ^

-- | Whether a type-level 'Natural' is odd. /Zero/ is not considered odd.
type Odd (x :: Integer) = L.Mod (Abs x) 2 ==? 1 :: Bool

-- | Whether a type-level 'Natural' is even. /Zero/ is considered even.
type Even (x :: Integer) = L.Mod (Abs x) 2 ==? 0 :: Bool

-- | Negation of type-level 'Integer's.
type family Negate (x :: Integer) :: Integer where
  Negate (P 0) = P 0
  Negate (P x) = N x
  Negate (N x) = P x

-- | Sign of type-level 'Integer's.
--
-- * @'P' 0@ if zero.
--
-- * @'P' 1@ if positive.
--
-- * @'N' 1@ if negative.
type family Sign (x :: Integer) :: Integer where
  Sign (P 0) = P 0
  Sign (N 0) = P 0
  Sign (P _) = P 1
  Sign (N _) = N 1

-- | Absolute value of a type-level 'Integer', as a type-level 'Natural'.
type family Abs (x :: Integer) :: Natural where
  Abs (P x) = x
  Abs (N x) = x

-- | Addition of type-level 'Integer's.
type (a :: Integer) + (b :: Integer) = Add_ (Normalize a) (Normalize b) :: Integer
type family Add_ (a :: Integer) (b :: Integer) :: Integer where
  Add_ (P a) (P b) = P (a L.+ b)
  Add_ (N a) (N b) = NN (a L.+ b)
  Add_ (P a) (N b) = If (b <=? a) (P (a L.- b)) (NN (b L.- a))
  Add_ (N a) (P b) = Add_ (P b) (N a)

-- | Multiplication of type-level 'Integer's.
type (a :: Integer) * (b :: Integer) = Mul_ (Normalize a) (Normalize b) :: Integer
type family Mul_ (a :: Integer) (b :: Integer) :: Integer where
  Mul_ (P a) (P b) = P (a L.* b)
  Mul_ (N a) (N b) = Mul_ (P a) (P b)
  Mul_ (P a) (N b) = NN (a L.* b)
  Mul_ (N a) (P b) = Mul_ (P a) (N b)

-- | Exponentiation of type-level 'Integer's.
--
-- * Exponentiation by negative 'Integer' doesn't type-check.
type (a :: Integer) ^ (b :: Integer) = Pow_ (Normalize a) (Normalize b) :: Integer
type family Pow_ (a :: Integer) (b :: Integer) :: Integer where
  Pow_ (P a) (P b) = P (a L.^ b)
  Pow_ (N a) (P b) = NN (a L.^ b)
  Pow_ _     (N _) = L.TypeError ('L.Text "KindInteger.(^): Negative exponent")

-- | Subtraction of type-level 'Integer's.
type (a :: Integer) - (b :: Integer) = a + Negate b :: Integer

-- | Get both the quotient and the 'Rem'ainder of the 'Div'ision of
-- type-level 'Integer's @a@ and @b@ using the specified 'Round'ing @r@.
--
-- @
-- forall (r :: 'Round') (a :: 'Integer') (b :: 'Integer').
--   (b '/=' 0) =>
--     'DivRem' r a b '=='  '('Div' r a b, 'Rem' r a b)
-- @
type DivRem (r :: Round) (a :: Integer) (b :: Integer) =
  '( Div r a b, Rem r a b ) :: (Integer, Integer)

-- | 'Rem'ainder of the division of type-level 'Integer' @a@ by @b@,
-- using the specified 'Round'ing @r@.
--
-- @
-- forall (r :: 'Round') (a :: 'Integer') (b :: 'Integer').
--   (b '/=' 0) =>
--     'Rem' r a b  '=='  a '-' b '*' 'Div' r a b
-- @
--
-- * Division by /zero/ doesn't type-check.
type Rem (r :: Round) (a :: Integer) (b :: Integer) =
  a - b * Div r a b :: Integer

-- | Divide of type-level 'Integer' @a@ by @b@,
-- using the specified 'Round'ing @r@.
--
-- * Division by /zero/ doesn't type-check.
type Div (r :: Round) (a :: Integer) (b :: Integer) =
  Div_ r (Normalize a) (Normalize b) :: Integer

type family Div_ (r :: Round) (a :: Integer) (b :: Integer) :: Integer where
  Div_ r (P a) (P b) = Div__ r (P a) b
  Div_ r (N a) (N b) = Div__ r (P a) b
  Div_ r (P a) (N b) = Div__ r (N a) b
  Div_ r (N a) (P b) = Div__ r (N a) b

type family Div__ (r :: Round) (a :: Integer) (b :: Natural) :: Integer where
  Div__ _ _ 0 = L.TypeError ('L.Text "KindInteger.Div: Division by zero")
  Div__ _ (P 0) _ = P 0
  Div__ _ (N 0) _ = P 0

  Div__ 'RoundDown (P a) b = P (L.Div a b)
  Div__ 'RoundDown (N a) b = NN (If (b L.* L.Div a b ==? a)
                                    (L.Div a b)
                                    (L.Div a b L.+ 1))

  Div__ 'RoundUp a b = Negate (Div__ 'RoundDown (Negate a) b)

  Div__ 'RoundZero (P a) b = Div__ 'RoundDown (P a) b
  Div__ 'RoundZero (N a) b = Negate (Div__ 'RoundDown (P a) b)

  Div__ 'RoundAway (P a) b = Div__ 'RoundUp (P a) b
  Div__ 'RoundAway (N a) b = Div__ 'RoundDown (N a) b

  Div__ 'RoundHalfDown a b = If (HalfLT (R a b) (Div__ 'RoundUp a b))
                                (Div__ 'RoundUp a b)
                                (Div__ 'RoundDown a b)

  Div__ 'RoundHalfUp a b = If (HalfLT (R a b) (Div__ 'RoundDown a b))
                              (Div__ 'RoundDown a b)
                              (Div__ 'RoundUp a b)

  Div__ 'RoundHalfEven a b = If (HalfLT (R a b) (Div__ 'RoundDown a b))
                                (Div__ 'RoundDown a b)
                                (If (HalfLT (R a b) (Div__ 'RoundUp a b))
                                    (Div__ 'RoundUp a b)
                                    (If (Even (Div__ 'RoundDown a b))
                                        (Div__ 'RoundDown a b)
                                        (Div__ 'RoundUp a b)))

  Div__ 'RoundHalfOdd a b = If (HalfLT (R a b) (Div__ 'RoundDown a b))
                               (Div__ 'RoundDown a b)
                               (If (HalfLT (R a b) (Div__ 'RoundUp a b))
                                   (Div__ 'RoundUp a b)
                                   (If (Odd (Div__ 'RoundDown a b))
                                       (Div__ 'RoundDown a b)
                                       (Div__ 'RoundUp a b)))

  Div__ 'RoundHalfZero a b = If (HalfLT (R a b) (Div__ 'RoundDown a b))
                                (Div__ 'RoundDown a b)
                                (If (HalfLT (R a b) (Div__ 'RoundUp a b))
                                    (Div__ 'RoundUp a b)
                                    (Div__ 'RoundZero a b))

  Div__ 'RoundHalfAway (P a) b = Div__ 'RoundHalfUp   (P a) b
  Div__ 'RoundHalfAway (N a) b = Div__ 'RoundHalfDown (N a) b


-- | Log base 2 ('floor'ed) of type-level 'Integer's.
--
-- * Logarithm of /zero/ doesn't type-check.
--
-- * Logarithm of negative number doesn't type-check.
type Log2 (a :: Integer) = Log2_ (Normalize a) :: Integer
type family Log2_ (a :: Integer) :: Integer where
  Log2_ (P 0) = L.TypeError ('L.Text "KindInteger.Log2: Logarithm of zero")
  Log2_ (P a) = P (L.Log2 a)
  Log2_ (N a) = L.TypeError ('L.Text "KindInteger.Log2: Logarithm of negative number")

-- | Greatest Common Divisor of type-level 'Integer' numbers @a@ and @b@.
--
-- Returns a 'Natural', since the Greatest Common Divisor is always positive.
type GCD (a :: Integer) (b :: Integer) = NatGCD (Abs a) (Abs b) :: Natural

-- | Greatest Common Divisor of type-level 'Natural's @a@ and @b@.
type family NatGCD (a :: Natural) (b :: Natural) :: Natural where
  NatGCD a 0 = a
  NatGCD a b = NatGCD b (L.Mod a b)

-- | Least Common Multiple of type-level 'Integer' numbers @a@ and @b@.
--
-- Returns a 'Natural', since the Least Common Multiple is always positive.
type LCM (a :: Integer) (b :: Integer) = NatLCM (Abs a) (Abs b) :: Natural

-- | Least Common Multiple of type-level 'Natural's @a@ and @b@.
type NatLCM (a :: Natural) (b :: Natural) =
  L.Div a (NatGCD a b) L.* b :: Natural

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

-- | Comparison of type-level 'Integer's, as a function.
type CmpInteger (a :: Integer) (b :: Integer) =
  CmpInteger_ (Normalize a) (Normalize b) :: Ordering
type family CmpInteger_ (a :: Integer) (b :: Integer) :: Ordering where
  CmpInteger_ a a = 'EQ
  CmpInteger_ (P a) (P b) = Compare a b
  CmpInteger_ (N a) (N b) = Compare b a
  CmpInteger_ (N _) (P _) = 'LT
  CmpInteger_ (P _) (N _) = 'GT

-- | "Data.Type.Ord" support for type-level 'Integer's.
type instance Compare (a :: Integer) (b :: Integer) =
  CmpInteger a b :: Ordering

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

-- | We either get evidence that this function was instantiated with the
-- same type-level 'Integer's, or 'Nothing'.
sameInteger
  :: forall a b proxy1 proxy2
  .  (KnownInteger a, KnownInteger b)
  => proxy1 a
  -> proxy2 b
  -> Maybe (a :~: b)
sameInteger :: forall (a :: Integer) (b :: Integer) (proxy1 :: Integer -> Type)
       (proxy2 :: Integer -> Type).
(KnownInteger a, KnownInteger b) =>
proxy1 a -> proxy2 b -> Maybe (a :~: b)
sameInteger proxy1 a
_ proxy2 b
_ = SInteger a -> SInteger b -> Maybe (a :~: b)
forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
forall (a :: Integer) (b :: Integer).
SInteger a -> SInteger b -> Maybe (a :~: b)
testEquality (forall (i :: Integer). KnownInteger i => SInteger i
integerSing @a) (forall (i :: Integer). KnownInteger i => SInteger i
integerSing @b)

-- | Like 'sameInteger', but if the type-level 'Integer's aren't equal, this
-- additionally provides proof of 'LT' or 'GT'.
cmpInteger
  :: forall a b proxy1 proxy2
  .  (KnownInteger a, KnownInteger b)
  => proxy1 a
  -> proxy2 b
  -> OrderingI a b
cmpInteger :: forall (a :: Integer) (b :: Integer) (proxy1 :: Integer -> Type)
       (proxy2 :: Integer -> Type).
(KnownInteger a, KnownInteger b) =>
proxy1 a -> proxy2 b -> OrderingI a b
cmpInteger proxy1 a
x proxy2 b
y = case Integer -> Integer -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (proxy1 a -> Integer
forall (i :: Integer) (proxy :: Integer -> Type).
KnownInteger i =>
proxy i -> Integer
integerVal proxy1 a
x) (proxy2 b -> Integer
forall (i :: Integer) (proxy :: Integer -> Type).
KnownInteger i =>
proxy i -> Integer
integerVal proxy2 b
y) of
  Ordering
EQ -> case (Any :~: Any) -> CmpInteger_ (Normalize a) (Normalize b) :~: 'EQ
forall a b. a -> b
unsafeCoerce Any :~: Any
forall {k} (a :: k). a :~: a
Refl :: CmpInteger a b :~: 'EQ of
    CmpInteger_ (Normalize a) (Normalize b) :~: 'EQ
Refl -> case (Any :~: Any) -> a :~: b
forall a b. a -> b
unsafeCoerce Any :~: Any
forall {k} (a :: k). a :~: a
Refl :: a :~: b of
      a :~: b
Refl -> OrderingI a a
OrderingI a b
forall {k} (a :: k). (Compare a a ~ 'EQ) => OrderingI a a
EQI
  Ordering
LT -> case (Any :~: Any) -> CmpInteger_ (Normalize a) (Normalize b) :~: 'LT
forall a b. a -> b
unsafeCoerce Any :~: Any
forall {k} (a :: k). a :~: a
Refl :: (CmpInteger a b :~: 'LT) of
    CmpInteger_ (Normalize a) (Normalize b) :~: 'LT
Refl -> OrderingI a b
forall {k} (a :: k) (b :: k). (Compare a b ~ 'LT) => OrderingI a b
LTI
  Ordering
GT -> case (Any :~: Any) -> CmpInteger_ (Normalize a) (Normalize b) :~: 'GT
forall a b. a -> b
unsafeCoerce Any :~: Any
forall {k} (a :: k). a :~: a
Refl :: (CmpInteger a b :~: 'GT) of
    CmpInteger_ (Normalize a) (Normalize b) :~: 'GT
Refl -> OrderingI a b
forall {k} (a :: k) (b :: k). (Compare a b ~ 'GT) => OrderingI a b
GTI

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

-- | Singleton type for a type-level 'Integer' @i@.
newtype SInteger (i :: Integer) = UnsafeSInteger P.Integer

-- | A explicitly bidirectional pattern synonym relating an 'SInteger' to a
-- 'KnownInteger' constraint.
--
-- As an __expression__: Constructs an explicit @'SInteger' i@ value from an
-- implicit @'KnownInteger' i@ constraint:
--
-- @
-- 'SInteger' @i :: 'KnownInteger' i => 'SInteger' i
-- @
--
-- As a __pattern__: Matches on an explicit @'SInteger' i@ value bringing
-- an implicit @'KnownInteger' i@ constraint into scope:
--
-- @
-- f :: 'SInteger' i -> ..
-- f SInteger = {- SInteger i in scope -}
-- @
pattern SInteger :: forall i. () => KnownInteger i => SInteger i
pattern $mSInteger :: forall {r} {i :: Integer}.
SInteger i -> (KnownInteger i => r) -> ((# #) -> r) -> r
$bSInteger :: forall (i :: Integer). KnownInteger i => SInteger i
SInteger <- (knownIntegerInstance -> KnownIntegeregerInstance)
  where SInteger = SInteger i
forall (i :: Integer). KnownInteger i => SInteger i
integerSing

-- | An internal data type that is only used for defining the 'SInteger' pattern
-- synonym.
data KnownIntegeregerInstance (i :: Integer) where
  KnownIntegeregerInstance :: KnownInteger i => KnownIntegeregerInstance i

-- | An internal function that is only used for defining the 'SInteger' pattern
-- synonym.
knownIntegerInstance :: SInteger i -> KnownIntegeregerInstance i
knownIntegerInstance :: forall (i :: Integer). SInteger i -> KnownIntegeregerInstance i
knownIntegerInstance SInteger i
si = SInteger i
-> (KnownInteger i => KnownIntegeregerInstance i)
-> KnownIntegeregerInstance i
forall (i :: Integer) r. SInteger i -> (KnownInteger i => r) -> r
withKnownInteger SInteger i
si KnownIntegeregerInstance i
KnownInteger i => KnownIntegeregerInstance i
forall (i :: Integer). KnownInteger i => KnownIntegeregerInstance i
KnownIntegeregerInstance

instance Show (SInteger i) where
  showsPrec :: Int -> SInteger i -> ShowS
showsPrec Int
p (UnsafeSInteger Integer
i) = Bool -> ShowS -> ShowS
showParen (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
appPrec) (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$
    String -> ShowS
showString String
"SInteger @" ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
    Int -> Integer -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
appPrec1 (Integer -> Integer
fromPrelude Integer
i)

instance TestEquality SInteger where
  testEquality :: forall (a :: Integer) (b :: Integer).
SInteger a -> SInteger b -> Maybe (a :~: b)
testEquality (UnsafeSInteger Integer
x) (UnsafeSInteger Integer
y)
    | Integer
x Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
P.== Integer
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

instance TestCoercion SInteger where
  testCoercion :: forall (a :: Integer) (b :: Integer).
SInteger a -> SInteger b -> Maybe (Coercion a b)
testCoercion SInteger a
x SInteger b
y = ((a :~: b) -> Coercion a b)
-> Maybe (a :~: b) -> Maybe (Coercion a b)
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap (\a :~: b
Refl -> Coercion a b
forall {k} (a :: k) (b :: k). Coercible a b => Coercion a b
Coercion) (SInteger a -> SInteger b -> Maybe (a :~: b)
forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
forall (a :: Integer) (b :: Integer).
SInteger a -> SInteger b -> Maybe (a :~: b)
testEquality SInteger a
x SInteger b
y)

-- | Return the term-level 'P.Integer' number corresponding to @i@ in
-- a @'SInteger' i@ value.
fromSInteger :: SInteger i -> P.Integer
fromSInteger :: forall (i :: Integer). SInteger i -> Integer
fromSInteger (UnsafeSInteger Integer
i) = Integer
i

-- | Convert an explicit @'SInteger' i@ value into an implicit
-- @'KnownInteger' i@ constraint.
withKnownInteger
  :: forall i rep (r :: TYPE rep). SInteger i -> (KnownInteger i => r) -> r
withKnownInteger :: forall (i :: Integer) r. SInteger i -> (KnownInteger i => r) -> r
withKnownInteger = forall (cls :: Constraint) meth r.
WithDict cls meth =>
meth -> (cls => r) -> r
withDict @(KnownInteger i)

-- | Convert a 'P.Integer' number into an @'SInteger' n@ value, where @n@ is a
-- fresh type-level 'Integer'.
withSomeSInteger
  :: forall rep (r :: TYPE rep). P.Integer -> (forall n. SInteger n -> r) -> r
withSomeSInteger :: forall r. Integer -> (forall (n :: Integer). SInteger n -> r) -> r
withSomeSInteger Integer
n forall (n :: Integer). SInteger n -> r
k = SInteger Any -> r
forall (n :: Integer). SInteger n -> r
k (Integer -> SInteger Any
forall (i :: Integer). Integer -> SInteger i
UnsafeSInteger Integer
n)
-- It's very important to keep this NOINLINE! See the docs at "GHC.TypeNats"
{-# NOINLINE withSomeSInteger #-}

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

data Round
  = RoundUp
  -- ^ Round __up__ towards positive infinity.
  | RoundDown
  -- ^ Round __down__ towards negative infinity.  Also known as "Prelude"'s
  -- 'P.floor'. This is the type of rounding used by "Prelude"'s 'P.div',
  -- 'P.mod', 'P.divMod', 'L.Div', 'L.Mod'.
  | RoundZero
  -- ^ Round towards __zero__.  Also known as "Prelude"'s 'P.truncate'. This is
  -- the type of rounding used by "Prelude"'s 'P.quot', 'P.rem', 'P.quotRem'.
  | RoundAway
  -- ^ Round __away__ from zero.
  | RoundHalfUp
  -- ^ Round towards the closest integer. If __half__way between two integers,
  -- round __up__ towards positive infinity.
  | RoundHalfDown
  -- ^ Round towards the closest integer. If __half__way between two integers,
  -- round __down__ towards negative infinity.
  | RoundHalfZero
  -- ^ Round towards the closest integer. If __half__way between two integers,
  -- round towards __zero__.
  | RoundHalfAway
  -- ^ Round towards the closest integer. If __half__way between two integers,
  -- round __away__ from zero.
  | RoundHalfEven
  -- ^ Round towards the closest integer. If __half__way between two integers,
  -- round towards the closest __even__ integer. Also known as "Prelude"'s
  -- 'P.round'.
  | RoundHalfOdd
  -- ^ Round towards the closest integer. If __half__way between two integers,
  -- round towards the closest __odd__ integer.
  deriving (Round -> Round -> Bool
(Round -> Round -> Bool) -> (Round -> Round -> Bool) -> Eq Round
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Round -> Round -> Bool
== :: Round -> Round -> Bool
$c/= :: Round -> Round -> Bool
/= :: Round -> Round -> Bool
Eq, Eq Round
Eq Round
-> (Round -> Round -> Ordering)
-> (Round -> Round -> Bool)
-> (Round -> Round -> Bool)
-> (Round -> Round -> Bool)
-> (Round -> Round -> Bool)
-> (Round -> Round -> Round)
-> (Round -> Round -> Round)
-> Ord Round
Round -> Round -> Bool
Round -> Round -> Ordering
Round -> Round -> Round
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: Round -> Round -> Ordering
compare :: Round -> Round -> Ordering
$c< :: Round -> Round -> Bool
< :: Round -> Round -> Bool
$c<= :: Round -> Round -> Bool
<= :: Round -> Round -> Bool
$c> :: Round -> Round -> Bool
> :: Round -> Round -> Bool
$c>= :: Round -> Round -> Bool
>= :: Round -> Round -> Bool
$cmax :: Round -> Round -> Round
max :: Round -> Round -> Round
$cmin :: Round -> Round -> Round
min :: Round -> Round -> Round
Ord, Int -> Round -> ShowS
[Round] -> ShowS
Round -> String
(Int -> Round -> ShowS)
-> (Round -> String) -> ([Round] -> ShowS) -> Show Round
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Round -> ShowS
showsPrec :: Int -> Round -> ShowS
$cshow :: Round -> String
show :: Round -> String
$cshowList :: [Round] -> ShowS
showList :: [Round] -> ShowS
Show, ReadPrec [Round]
ReadPrec Round
Int -> ReadS Round
ReadS [Round]
(Int -> ReadS Round)
-> ReadS [Round]
-> ReadPrec Round
-> ReadPrec [Round]
-> Read Round
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
$creadsPrec :: Int -> ReadS Round
readsPrec :: Int -> ReadS Round
$creadList :: ReadS [Round]
readList :: ReadS [Round]
$creadPrec :: ReadPrec Round
readPrec :: ReadPrec Round
$creadListPrec :: ReadPrec [Round]
readListPrec :: ReadPrec [Round]
Read, Int -> Round
Round -> Int
Round -> [Round]
Round -> Round
Round -> Round -> [Round]
Round -> Round -> Round -> [Round]
(Round -> Round)
-> (Round -> Round)
-> (Int -> Round)
-> (Round -> Int)
-> (Round -> [Round])
-> (Round -> Round -> [Round])
-> (Round -> Round -> [Round])
-> (Round -> Round -> Round -> [Round])
-> Enum Round
forall a.
(a -> a)
-> (a -> a)
-> (Int -> a)
-> (a -> Int)
-> (a -> [a])
-> (a -> a -> [a])
-> (a -> a -> [a])
-> (a -> a -> a -> [a])
-> Enum a
$csucc :: Round -> Round
succ :: Round -> Round
$cpred :: Round -> Round
pred :: Round -> Round
$ctoEnum :: Int -> Round
toEnum :: Int -> Round
$cfromEnum :: Round -> Int
fromEnum :: Round -> Int
$cenumFrom :: Round -> [Round]
enumFrom :: Round -> [Round]
$cenumFromThen :: Round -> Round -> [Round]
enumFromThen :: Round -> Round -> [Round]
$cenumFromTo :: Round -> Round -> [Round]
enumFromTo :: Round -> Round -> [Round]
$cenumFromThenTo :: Round -> Round -> Round -> [Round]
enumFromThenTo :: Round -> Round -> Round -> [Round]
Enum, Round
Round -> Round -> Bounded Round
forall a. a -> a -> Bounded a
$cminBound :: Round
minBound :: Round
$cmaxBound :: Round
maxBound :: Round
Bounded)


-- | Divide @a@ by @a@ using the specified 'Round'ing.
-- Return the quotient @q@. See 'divRem'.
div :: Round
    -> P.Integer  -- ^ Dividend @a@.
    -> P.Integer  -- ^ Divisor @b@.
    -> P.Integer  -- ^ Quotient @q@.
div :: Round -> Integer -> Integer -> Integer
div Round
r Integer
a Integer
b = (Integer, Integer) -> Integer
forall a b. (a, b) -> a
fst (Round -> Integer -> Integer -> (Integer, Integer)
divRem Round
r Integer
a Integer
b)

-- | Divide @a@ by @a@ using the specified 'Round'ing.
-- Return the remainder @m@. See 'divRem'.
rem :: Round
    -> P.Integer  -- ^ Dividend @a@.
    -> P.Integer  -- ^ Divisor @b@.
    -> P.Integer  -- ^ Remainder @m@.
rem :: Round -> Integer -> Integer -> Integer
rem Round
r Integer
a Integer
b = (Integer, Integer) -> Integer
forall a b. (a, b) -> b
snd (Round -> Integer -> Integer -> (Integer, Integer)
divRem Round
r Integer
a Integer
b)

-- | Divide @a@ by @a@ using the specified 'Round'ing.
-- Return the quotient @q@ and the remainder @m@.
--
-- @
-- forall (r :: 'Round') (a :: 'P.Integer') (b :: 'P.Integer').
--   (b 'P./=' 0) =>
--     case 'divRem' r a b of
--       (q, m) -> m 'P.==' a 'P.-' b 'P.*' q
-- @
divRem
  :: Round
  -> P.Integer  -- ^ Dividend @a@.
  -> P.Integer  -- ^ Divisor @b@.
  -> (P.Integer, P.Integer)  -- ^ Quotient @q@ and remainder @m@.
{-# NOINLINE divRem #-}
divRem :: Round -> Integer -> Integer -> (Integer, Integer)
divRem Round
RoundZero = \Integer
a (Integer -> Integer
errDiv0 -> Integer
b) -> Integer -> Integer -> (Integer, Integer)
forall a. Integral a => a -> a -> (a, a)
P.quotRem Integer
a Integer
b
divRem Round
RoundDown = \Integer
a (Integer -> Integer
errDiv0 -> Integer
b) -> Integer -> Integer -> (Integer, Integer)
forall a. Integral a => a -> a -> (a, a)
P.divMod Integer
a Integer
b
divRem Round
RoundUp = \Integer
a (Integer -> Integer
errDiv0 -> Integer
b) -> Integer -> Integer -> (Integer, Integer)
_divRemRoundUpNoCheck Integer
a Integer
b
divRem Round
RoundAway = \Integer
a (Integer -> Integer
errDiv0 -> Integer
b) ->
  if Bool -> Bool -> Bool
forall a. Bits a => a -> a -> a
xor (Integer
a Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
0) (Integer
b Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
0)
     then Integer -> Integer -> (Integer, Integer)
forall a. Integral a => a -> a -> (a, a)
P.divMod Integer
a Integer
b
     else Integer -> Integer -> (Integer, Integer)
_divRemRoundUpNoCheck Integer
a Integer
b
divRem Round
RoundHalfUp = (Bool
 -> (Integer, Integer) -> (Integer, Integer) -> (Integer, Integer))
-> Integer -> Integer -> (Integer, Integer)
_divRemHalf ((Bool
  -> (Integer, Integer) -> (Integer, Integer) -> (Integer, Integer))
 -> Integer -> Integer -> (Integer, Integer))
-> (Bool
    -> (Integer, Integer) -> (Integer, Integer) -> (Integer, Integer))
-> Integer
-> Integer
-> (Integer, Integer)
forall a b. (a -> b) -> a -> b
$ \Bool
_ (Integer, Integer)
_ (Integer, Integer)
up -> (Integer, Integer)
up
divRem Round
RoundHalfDown = (Bool
 -> (Integer, Integer) -> (Integer, Integer) -> (Integer, Integer))
-> Integer -> Integer -> (Integer, Integer)
_divRemHalf ((Bool
  -> (Integer, Integer) -> (Integer, Integer) -> (Integer, Integer))
 -> Integer -> Integer -> (Integer, Integer))
-> (Bool
    -> (Integer, Integer) -> (Integer, Integer) -> (Integer, Integer))
-> Integer
-> Integer
-> (Integer, Integer)
forall a b. (a -> b) -> a -> b
$ \Bool
_ (Integer, Integer)
down (Integer, Integer)
_ -> (Integer, Integer)
down
divRem Round
RoundHalfZero = (Bool
 -> (Integer, Integer) -> (Integer, Integer) -> (Integer, Integer))
-> Integer -> Integer -> (Integer, Integer)
_divRemHalf ((Bool
  -> (Integer, Integer) -> (Integer, Integer) -> (Integer, Integer))
 -> Integer -> Integer -> (Integer, Integer))
-> (Bool
    -> (Integer, Integer) -> (Integer, Integer) -> (Integer, Integer))
-> Integer
-> Integer
-> (Integer, Integer)
forall a b. (a -> b) -> a -> b
$ \Bool
neg (Integer, Integer)
down (Integer, Integer)
up ->
  if Bool
neg then (Integer, Integer)
up else (Integer, Integer)
down
divRem Round
RoundHalfAway = (Bool
 -> (Integer, Integer) -> (Integer, Integer) -> (Integer, Integer))
-> Integer -> Integer -> (Integer, Integer)
_divRemHalf ((Bool
  -> (Integer, Integer) -> (Integer, Integer) -> (Integer, Integer))
 -> Integer -> Integer -> (Integer, Integer))
-> (Bool
    -> (Integer, Integer) -> (Integer, Integer) -> (Integer, Integer))
-> Integer
-> Integer
-> (Integer, Integer)
forall a b. (a -> b) -> a -> b
$ \Bool
neg (Integer, Integer)
down (Integer, Integer)
up ->
  if Bool
neg then (Integer, Integer)
down else (Integer, Integer)
up
divRem Round
RoundHalfEven = (Bool
 -> (Integer, Integer) -> (Integer, Integer) -> (Integer, Integer))
-> Integer -> Integer -> (Integer, Integer)
_divRemHalf ((Bool
  -> (Integer, Integer) -> (Integer, Integer) -> (Integer, Integer))
 -> Integer -> Integer -> (Integer, Integer))
-> (Bool
    -> (Integer, Integer) -> (Integer, Integer) -> (Integer, Integer))
-> Integer
-> Integer
-> (Integer, Integer)
forall a b. (a -> b) -> a -> b
$ \Bool
_ (Integer, Integer)
down (Integer, Integer)
up ->
  if Integer -> Bool
forall a. Integral a => a -> Bool
even ((Integer, Integer) -> Integer
forall a b. (a, b) -> a
fst (Integer, Integer)
down) then (Integer, Integer)
down else (Integer, Integer)
up
divRem Round
RoundHalfOdd = (Bool
 -> (Integer, Integer) -> (Integer, Integer) -> (Integer, Integer))
-> Integer -> Integer -> (Integer, Integer)
_divRemHalf ((Bool
  -> (Integer, Integer) -> (Integer, Integer) -> (Integer, Integer))
 -> Integer -> Integer -> (Integer, Integer))
-> (Bool
    -> (Integer, Integer) -> (Integer, Integer) -> (Integer, Integer))
-> Integer
-> Integer
-> (Integer, Integer)
forall a b. (a -> b) -> a -> b
$ \Bool
_ (Integer, Integer)
down (Integer, Integer)
up ->
  if Integer -> Bool
forall a. Integral a => a -> Bool
odd ((Integer, Integer) -> Integer
forall a b. (a, b) -> a
fst (Integer, Integer)
down) then (Integer, Integer)
down else (Integer, Integer)
up

_divRemRoundUpNoCheck :: P.Integer -> P.Integer -> (P.Integer, P.Integer)
_divRemRoundUpNoCheck :: Integer -> Integer -> (Integer, Integer)
_divRemRoundUpNoCheck Integer
a Integer
b =
  let q :: Integer
q = Integer -> Integer
forall a. Num a => a -> a
negate (Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
P.div (Integer -> Integer
forall a. Num a => a -> a
negate Integer
a) Integer
b)
  in (Integer
q, Integer
a Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
b Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Integer
q)
{-# INLINE _divRemRoundUpNoCheck #-}

_divRemHalf
  :: (Bool ->
      (P.Integer, P.Integer) ->
      (P.Integer, P.Integer) ->
      (P.Integer, P.Integer))
  -- ^ Negative -> divRem RoundDown -> divRem RoundDown -> Result
  -> P.Integer  -- ^ Dividend
  -> P.Integer  -- ^ Divisor
  -> (P.Integer, P.Integer)
_divRemHalf :: (Bool
 -> (Integer, Integer) -> (Integer, Integer) -> (Integer, Integer))
-> Integer -> Integer -> (Integer, Integer)
_divRemHalf Bool
-> (Integer, Integer) -> (Integer, Integer) -> (Integer, Integer)
f = \Integer
a (Integer -> Integer
errDiv0 -> Integer
b) ->
  let neg :: Bool
neg  = Bool -> Bool -> Bool
forall a. Bits a => a -> a -> a
xor (Integer
a Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
0) (Integer
b Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
0)
      down :: (Integer, Integer)
down = Integer -> Integer -> (Integer, Integer)
forall a. Integral a => a -> a -> (a, a)
P.divMod Integer
a Integer
b
      up :: (Integer, Integer)
up   = Integer -> Integer -> (Integer, Integer)
_divRemRoundUpNoCheck Integer
a Integer
b
  in  case Ratio Integer -> Ratio Integer -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (Integer
a Integer -> Integer -> Ratio Integer
forall a. Integral a => a -> a -> Ratio a
P.% Integer
b Ratio Integer -> Ratio Integer -> Ratio Integer
forall a. Num a => a -> a -> a
- Integer -> Ratio Integer
forall a. Real a => a -> Ratio Integer
toRational ((Integer, Integer) -> Integer
forall a b. (a, b) -> a
fst (Integer, Integer)
down)) (Integer
1 Integer -> Integer -> Ratio Integer
forall a. a -> a -> Ratio a
P.:% Integer
2) of
        Ordering
LT -> (Integer, Integer)
down
        Ordering
GT -> (Integer, Integer)
up
        Ordering
EQ -> Bool
-> (Integer, Integer) -> (Integer, Integer) -> (Integer, Integer)
f Bool
neg (Integer, Integer)
down (Integer, Integer)
up
{-# INLINE _divRemHalf #-}

--------------------------------------------------------------------------------
-- Extras

infixr 4 /=, /=?, ==, ==?

-- | This should be exported by "Data.Type.Ord".
type (a :: k) ==? (b :: k) = OrdCond (Compare a b) 'False 'True 'False :: Bool

-- | This should be exported by "Data.Type.Ord".
type (a :: k) == (b :: k) = (a ==? b) ~ 'True :: Constraint

-- | This should be exported by "Data.Type.Ord".
type (a :: k) /=? (b :: k) = OrdCond (Compare a b) 'True 'False 'True :: Bool

-- | This should be exported by "Data.Type.Ord".
type (a :: k) /= (b :: k) = (a /=? b) ~ 'True :: Constraint

--------------------------------------------------------------------------------
-- Rational tools

data Rat = Rat Integer Natural

type family R (n :: Integer) (d :: Natural) :: Rat where
  R (P n) d = RatNormalize ('Rat (P n) d)
  R (N n) d = RatNormalize ('Rat (N n) d)

type family RatNormalize (r :: Rat) :: Rat where
  RatNormalize ('Rat _ 0) =
    L.TypeError ('L.Text "KindInteger: Denominator is 0")
  RatNormalize ('Rat (P 0) _) = 'Rat (P 0) 1
  RatNormalize ('Rat (N 0) _) = 'Rat (P 0) 1
  RatNormalize ('Rat (P n) d) = 'Rat (P (L.Div n (NatGCD n d)))
                                     (L.Div d (NatGCD n d))
  RatNormalize ('Rat (N n) d) = 'Rat (N (L.Div n (NatGCD n d)))
                                     (L.Div d (NatGCD n d))

type family RatAbs (a :: Rat) :: Rat where
  RatAbs ('Rat n d) = RatNormalize ('Rat (P (Abs n)) d)

type RatAdd (a :: Rat) (b :: Rat) =
  RatNormalize (RatAdd_ (RatNormalize a) (RatNormalize b)) :: Rat
type family RatAdd_ (a :: Rat) (b :: Rat) :: Rat where
  RatAdd_ ('Rat an ad) ('Rat bn bd) = 'Rat (an * P bd + bn * P ad) (ad L.* bd)

type family RatNegate (a :: Rat) :: Rat where
  RatNegate ('Rat n d) = RatNormalize ('Rat (Negate n) d)

type RatMinus (a :: Rat) (b :: Rat) = RatAdd a (RatNegate b)

type instance Compare (a :: Rat) (b :: Rat) = RatCmp a b
type RatCmp (a :: Rat) (b :: Rat) =
  RatCmp_ (RatNormalize a) (RatNormalize b) :: Ordering
type family RatCmp_ (a :: Rat) (b :: Rat) :: Ordering where
  RatCmp_ a a = 'EQ
  RatCmp_ ('Rat an ad) ('Rat bn bd) = CmpInteger (an * P bd) (bn * P ad)

-- | ''True' if the distance between @a@ and @b@ is less than /0.5/.
type HalfLT (a :: Rat) (b :: Integer) =
  (RatAbs (RatMinus a ('Rat b 1))) <? ('Rat (P 1) 2) :: Bool

errDiv0 :: P.Integer -> P.Integer
errDiv0 :: Integer -> Integer
errDiv0 Integer
0 = ArithException -> Integer
forall a e. Exception e => e -> a
Ex.throw ArithException
Ex.DivideByZero
errDiv0 Integer
i = Integer
i