{-# 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
  , 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', mostly 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).
-- Contrary to "Prelude"'s 'P.Integer', "KindInteger"'s 'Integer' preserves
-- the internal distinction between @'P' 0@ and @'N' 0@, this is why functions
-- such as 'fromSInteger' prefer to use "KindInteger"'s 'Integer' rather
-- than "Prelude"'s 'P.Integer'.
data Integer
  = P_ Natural
  | N_ Natural

-- | Note that @'P' 0 '==' 'N' 0@.
instance Eq Integer where
  a == b = toPrelude a P.== toPrelude b

instance Ord Integer where
  compare a b = compare (toPrelude a) (toPrelude b)
  a <= b = toPrelude a <= toPrelude b

-- | Same as "Prelude" 'P.Integer'.
instance Show Integer where
  showsPrec p = showsPrec p . toPrelude

-- | Same as "Prelude" 'P.Integer'.
instance Read Integer where
  readsPrec p xs = do (a, ys) <- readsPrec p xs
                      [(fromPrelude a, 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 p i = showParen (p > appPrec) $ case i of
  P_ x -> showString "P " . shows x
  N_ x -> showString "N " . shows 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 (P_ n) = toInteger n
toPrelude (N_ n) = negate (toInteger 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 i = if i >= 0 then P_ (fromInteger i)
                          else N_ (fromInteger (negate 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 = UnsafeSInteger (P_ (fromInteger (L.natVal (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 = UnsafeSInteger (N_ (fromInteger (L.natVal (Proxy @x))))

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

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

-- | Convert a term-level "KindInteger" 'Integer' into an unknown
-- type-level 'Integer'.
someIntegerVal :: Integer -> SomeInteger
someIntegerVal i = withSomeSInteger i $ \(si :: SInteger i) ->
                   withKnownInteger si (SomeInteger @i Proxy)

-- | Note that @'P' 0 '==' 'N' 0@.
instance Eq SomeInteger where
  SomeInteger x == SomeInteger y = integerVal x P.== integerVal y

instance Ord SomeInteger where
  compare (SomeInteger x) (SomeInteger y) =
    compare (integerVal x) (integerVal y)

instance Show SomeInteger where
  showsPrec p (SomeInteger x) = showsPrec p (integerVal x)

instance Read SomeInteger where
  readsPrec p xs = do (a, ys) <- readsPrec p xs
                      [(someIntegerVal a, 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 _ _ = testEquality (integerSing @a) (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 x y = case compare (integerVal x) (integerVal y) of
  EQ -> case unsafeCoerce Refl :: CmpInteger a b :~: 'EQ of
    Refl -> case unsafeCoerce Refl :: a :~: b of
      Refl -> EQI
  LT -> case unsafeCoerce Refl :: (CmpInteger a b :~: 'LT) of
    Refl -> LTI
  GT -> case unsafeCoerce Refl :: (CmpInteger a b :~: 'GT) of
    Refl -> 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 SInteger <- (knownIntegerInstance -> KnownIntegeregerInstance)
  where SInteger = 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 si = withKnownInteger si KnownIntegeregerInstance

instance Show (SInteger i) where
  showsPrec p (UnsafeSInteger i) = showParen (p > appPrec) $
    showString "SInteger @" . showsPrecTypeLit appPrec1 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 = 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 = decideCoercion
  {-# INLINE testCoercion #-}

-- | Return the term-level "KindInteger" 'Integer' number corresponding to @i@
-- in a @'SInteger' i@ value.
fromSInteger :: SInteger i -> Integer
fromSInteger (UnsafeSInteger i) = 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 (N_ l) (N_ r) = l P.== r
eqIntegerRep (P_ l) (P_ r) = l P.== r
eqIntegerRep _      _      = 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 = withDict @(KnownInteger i)

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

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

type instance Sing = SInteger

instance KnownInteger i => SingI (i :: Integer) where
  sing = integerSing
  {-# INLINE sing #-}

-- | 'Demote' refers to "KindInteger"'s 'Integer' rather than "Prelude"'s
-- 'Integer' so that the 'SInteger''s internal representation is preserved.
-- Use 'toPrelude' and 'fromPrelude' as necessary.
instance SingKind Integer where
  type Demote Integer = Integer
  fromSing = fromSInteger
  {-# INLINE fromSing #-}
  toSing i = withSomeSInteger i SomeSing
  {-# INLINE toSing #-}

-- | 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 l %~ UnsafeSInteger r =
    case eqIntegerRep l r of
      True  -> Proved (unsafeCoerce Refl)
      False -> Disproved (\Refl -> error "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 (Eq, Ord, Show, Read, Enum, 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 r a b = fst (divRem r a 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 r a b = snd (divRem r a 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 RoundZero = \a (errDiv0 -> b) -> P.quotRem a b
divRem RoundDown = \a (errDiv0 -> b) -> P.divMod a b
divRem RoundUp = \a (errDiv0 -> b) -> _divRemRoundUpNoCheck a b
divRem RoundAway = \a (errDiv0 -> b) ->
  if xor (a < 0) (b < 0)
     then P.divMod a b
     else _divRemRoundUpNoCheck a b
divRem RoundHalfUp = _divRemHalf $ \_ _ up -> up
divRem RoundHalfDown = _divRemHalf $ \_ down _ -> down
divRem RoundHalfZero = _divRemHalf $ \neg down up ->
  if neg then up else down
divRem RoundHalfAway = _divRemHalf $ \neg down up ->
  if neg then down else up
divRem RoundHalfEven = _divRemHalf $ \_ down up ->
  if even (fst down) then down else up
divRem RoundHalfOdd = _divRemHalf $ \_ down up ->
  if odd (fst down) then down else up

_divRemRoundUpNoCheck :: P.Integer -> P.Integer -> (P.Integer, P.Integer)
_divRemRoundUpNoCheck a b =
  let q = negate (P.div (negate a) b)
  in (q, a - b * 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 f = \a (errDiv0 -> b) ->
  let neg  = xor (a < 0) (b < 0)
      down = P.divMod a b
      up   = _divRemRoundUpNoCheck a b
  in  case compare (a P.% b - toRational (fst down)) (1 P.:% 2) of
        LT -> down
        GT -> up
        EQ -> f neg down 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 0 = Ex.throw Ex.DivideByZero
errDiv0 i = i