{-# 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
  , 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
  , eqIntegerRep

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

import Control.Exception qualified as Ex
import Data.Bits
import Data.Proxy
import Data.Singletons
import Data.Singletons.Decide
import Data.Type.Bool (If)
import Data.Type.Coercion
import Data.Type.Equality (TestEquality(..))
import Data.Type.Ord
import GHC.Base (WithDict(..))
import GHC.Exts (TYPE, Constraint)
import GHC.Real qualified as P
import GHC.Show (appPrec, appPrec1)
import GHC.TypeLits qualified as L
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 (Natural -> Integer
P_ (Integer -> Natural
forall a. Num a => Integer -> a
fromInteger (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.
--
-- Implementation note: Notice that @'N' 0@ will not be 'Normalize'd to
-- @'P' 0@. This is so that 'SDecide', 'TestEquality' and 'TestCoercion'
-- behave as expected. If you want a 'Normalize'd 'SInteger', then use
-- @'integerSing' \@('Normalize' i)@.
instance L.KnownNat x => KnownInteger (N x) where
  integerSing :: SInteger (N x)
integerSing = Integer -> SInteger (N x)
forall (i :: Integer). Integer -> SInteger i
UnsafeSInteger (Natural -> Integer
N_ (Integer -> Natural
forall a. Num a => Integer -> a
fromInteger (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 -> Integer
toPrelude 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 Integer
type role SInteger representational

-- | 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
showsPrecTypeLit Int
appPrec1 Integer
i

-- | Note that this checks for type equality. That is, @'P' 0@ and @'N' 0@
-- are not equal types, even if they are treated equally elsewhere in
-- "KindInteger".
instance TestEquality SInteger where
  testEquality :: forall (a :: Integer) (b :: Integer).
SInteger a -> SInteger b -> Maybe (a :~: b)
testEquality = Sing a -> Sing b -> Maybe (a :~: b)
SInteger a -> SInteger b -> Maybe (a :~: b)
forall k (a :: k) (b :: k).
SDecide k =>
Sing a -> Sing b -> Maybe (a :~: b)
decideEquality
  {-# INLINE testEquality #-}

-- | Note that this checks for type equality. That is, @'P' 0@ and @'N' 0@
-- are not equal types, even if they are treated equally elsewhere in
-- "KindInteger".
instance TestCoercion SInteger where
  testCoercion :: forall (a :: Integer) (b :: Integer).
SInteger a -> SInteger b -> Maybe (Coercion a b)
testCoercion = Sing a -> Sing b -> Maybe (Coercion a b)
SInteger a -> SInteger b -> Maybe (Coercion a b)
forall k (a :: k) (b :: k).
SDecide k =>
Sing a -> Sing b -> Maybe (Coercion a b)
decideCoercion
  {-# INLINE testCoercion #-}

-- | Return the term-level "Prelude" '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 -> Integer
toPrelude Integer
i
{-# INLINE fromSInteger #-}

-- | Return the term-level "KindInteger" 'Integer' number corresponding to @i@
-- in a @'SInteger' i@ value.
fromSInteger' :: SInteger i -> Integer
fromSInteger' :: forall (i :: Integer). SInteger i -> Integer
fromSInteger' (UnsafeSInteger Integer
i) = Integer
i
{-# INLINE fromSInteger' #-}

-- | Whether the internal representation of the 'Integer's are equal.
--
-- Note that this is not the same as '(P.==)'. Use '(P.==)' unless you
-- know what you are doing.
eqIntegerRep :: Integer -> Integer -> Bool
eqIntegerRep :: Integer -> Integer -> Bool
eqIntegerRep (N_ Natural
l) (N_ Natural
r) = Natural
l Natural -> Natural -> Bool
forall a. Eq a => a -> a -> Bool
P.== Natural
r
eqIntegerRep (P_ Natural
l) (P_ Natural
r) = Natural
l Natural -> Natural -> Bool
forall a. Eq a => a -> a -> Bool
P.== Natural
r
eqIntegerRep Integer
_      Integer
_      = Bool
False
{-# INLINE eqIntegerRep #-}

-- | 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 -> Integer
fromPrelude Integer
n))
-- It's very important to keep this NOINLINE! See the docs at "GHC.TypeNats"
{-# NOINLINE withSomeSInteger #-}

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

type instance Sing = SInteger

-- | Note that this checks for type equality. That is, @'P' 0@ and @'N' 0@
-- are not equal types, even if they are treated equally elsewhere in
-- "KindInteger".
instance SDecide Integer where
  UnsafeSInteger Integer
l %~ :: forall (a :: Integer) (b :: Integer).
Sing a -> Sing b -> Decision (a :~: b)
%~ UnsafeSInteger Integer
r =
    case Integer -> Integer -> Bool
eqIntegerRep Integer
l Integer
r of
      Bool
True  -> (a :~: b) -> Decision (a :~: b)
forall a. a -> Decision a
Proved ((Any :~: Any) -> a :~: b
forall a b. a -> b
unsafeCoerce Any :~: Any
forall {k} (a :: k). a :~: a
Refl)
      Bool
False -> Refuted (a :~: b) -> Decision (a :~: b)
forall a. Refuted a -> Decision a
Disproved (\a :~: b
Refl -> String -> Void
forall a. HasCallStack => String -> a
error String
"SDecide.Integer")

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

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