{-# LANGUAGE StrictData #-}
{-# LANGUAGE TypeFamilyDependencies #-}
{-# 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 similar to the ones for type-level 'Natural's
-- as of @base-4.18@ and @singletons-base-3.1.1@, and they will continue to
-- evolve together with @base@ and @singletons-base@, trying to more or less
-- follow their API.
module KindInteger {--}
  ( -- * Integer
    Integer
  , type Z, pattern SZ
  , type N, pattern SN
  , type P, pattern SP
  , FromNatural, sFromNatural
  , Fold, sFold
    -- * SInteger
  , KnownInteger
  , Normalized
  , integerSing
  , integerVal
  , withKnownInteger
  , SomeInteger(..)
  , someIntegerVal
  , SInteger
  , pattern SInteger
  , fromSInteger
  , withSomeSInteger
    -- * Proofs
  , sNegateRefl
  , sZigZagRefl
  , sZagZigRefl

    -- * Show
    --
    -- | Besides the following /\*Lit/ tools, 'P.PShow' and 'P.SShow' can
    -- be used to display as "Prelude".'P.Integer' does.
  , ShowLit, showLit, sShowLit
  , ShowsLit, showsLit, sShowsLit
  , ShowsPrecLit, showsPrecLit, sShowsPrecLit
  , readPrecLit

    -- * Operations
    --
    -- | Additional arithmetic operations are provided through the 'P.PNum'
    -- and 'P.SNum' instances. Notably 'P.Abs', 'P.sAbs', 'P.Negate',
    -- 'P.sNegate', 'P.Signum', 'P.sSignum', 'P.+', 'P.-', 'P.*', 'P.%+',
    -- 'P.%-', 'P.%*'.
  , type (^), (%^)
  , Odd, sOdd
  , Even, sEven
  , Abs, sAbs
  , GCD, sGCD
  , LCM, sLCM
  , Log2, sLog2
  , Div, sDiv, div
  , Rem, sRem, rem
  , DivRem, sDivRem, divRem
    -- ** Rounding
  , Round(..)
  , SRound(..)

    -- * Comparisons
    --
    -- | Additional comparison tools are available at 'SDdecide',
    -- 'TestEquality', 'TestCoercion', 'P.PEq', 'P.SEq', 'P.POrd', 'P.SOrd'
    -- and 'Compare'.
  , cmpInteger
  , sameInteger

    -- * Misc
  , ZigZag, sZigZag
  , ZagZig, sZagZig

    -- * Defunctionalization
  , ZSym0
  , NSym0, NSym1
  , PSym0, PSym1
  , FromNaturalSym0, FromNaturalSym1
  , KnownIntegerSym0, KnownIntegerSym1
  , NormalizedSym0, NormalizedSym1
  , FoldSym0, FoldSym1, FoldSym2, FoldSym3, FoldSym4
  , type (^@#@$), type (^@#@$$), type (^@#@$$$)
  , OddSym0, OddSym1
  , EvenSym0, EvenSym1
  , GCDSym0, GCDSym1
  , LCMSym0, LCMSym1
  , Log2Sym0, Log2Sym1
  , DivSym0, DivSym1, DivSym2, DivSym3
  , RemSym0, RemSym1, RemSym2, RemSym3
  , DivRemSym0, DivRemSym1, DivRemSym2, DivRemSym3
  , ShowLitSym0, ShowLitSym1
  , ShowsLitSym0, ShowsLitSym1, ShowsLitSym2
  , ShowsPrecLitSym0, ShowsPrecLitSym1, ShowsPrecLitSym2, ShowsPrecLitSym3
  , RoundUpSym0
  , RoundDownSym0
  , RoundZeroSym0
  , RoundAwaySym0
  , RoundHalfUpSym0
  , RoundHalfDownSym0
  , RoundHalfZeroSym0
  , RoundHalfAwaySym0
  , RoundHalfEvenSym0
  , RoundHalfOddSym0
  ) --}
  where

import Control.Applicative
import Control.Exception qualified as Ex
import Control.Monad
import Data.Bits
import Data.Bool.Singletons (SBool(..))
import Data.Char qualified as Char
import Data.Eq.Singletons qualified as EqS
import Data.Maybe
import Data.Ord.Singletons qualified as OrdS
import Data.Proxy
import Data.Singletons
import Data.Singletons.Decide
import Data.String
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, coerce)
import GHC.Num.Integer (integerLog2)
import GHC.Real qualified as P
import GHC.Show (appPrec1)
import GHC.TypeLits qualified as L
import GHC.TypeLits.Singletons qualified as L hiding (natVal)
import Numeric.Natural (Natural)
import Prelude hiding (Show, Integer, (==), (/=), div, rem)
import Prelude qualified as P
import Prelude.Singletons qualified as P
import Text.ParserCombinators.ReadP qualified as ReadP
import Text.ParserCombinators.ReadPrec qualified as ReadPrec
import Text.Read qualified as Read
import Text.Show.Singletons (AppPrec1)
import Unsafe.Coerce (unsafeCoerce)

import KindInteger.Round

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

-- | Type-level version of 'P.Integer', only used as a /kind/.
--
-- * Zero is represented as t'Z'.
--
-- * A positive number /+x/ is represented as @t'P' x@.
--
-- * A negative number /-x/ is represented as @t'N' x@.

-- __Note__: This representation is depressing. We hate it. It's not “total”,
-- because things such as @'N' 0@ and @'P' 0@ are not “valid”, and it's not
-- efficient, because we have to pay attention to three different constructors
-- rather than just one. The reason why we use this horrible representation
-- anyway is that type errors are easier to understand, since literals like
-- @'N' 2@ or 'Z' will show up in them. @'N' 0@ and @'P' 0@ will type-check
-- just fine on their own. However, tools in this module will reject them. For
-- example, there is no 'KnownInteger' instance for them, and 'Normalized'
-- will fail to type-check. Moreover, it is not possible to construct a
-- 'SInteger' for @'N' 0@ or @'P' 0@. If we could customize the way this
-- 'Integer' gets rendered in type-errors, we'd switch to a better internal
-- representation such as ZigZag. Also note that rather than exporting the
-- constructors directly, we export type-synonyms with the same name. This is
-- mostly so that users don't need to type the annoying preceeding tick.
data Integer
  = Z         -- ^ 0.
  | N Natural -- ^ Guaranteed to be greater than 0 only after going through
              -- 'KnownInteger', 'Normalized' or 'SInteger'.
  | P Natural -- ^ Guaranteed to be greater than 0 only after going through
              -- 'KnownInteger', 'Normalized' or 'SInteger'.

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

-- | Zero is represented as t'Z'.
type Z = 'Z :: Integer

type ZSym0 :: Integer

type ZSym0 = Z

-- | A negative number /-x/ is represented as @t'N' x@.
--
-- While a standalone @t'N' 0@ type-checks, it is not considered valid,
-- so tools like 'KnownInteger' or 'Normalized' will reject it.
-- @t'N' 0@ itself is not rejected so that it can be used to pattern-match
-- against 'Integer's at the type-level if necessary.
type N (x :: Natural) = 'N x :: Integer

data NSym0 :: Natural ~> Integer
type NSym1 :: Natural -> Integer

type instance Apply NSym0 x = NSym1 x
type NSym1 x = N x

-- | A positive number /+x/ is represented as @t'P' x@.
--
-- While a standalone @t'P' 0@ type-checks, it is not considered valid,
-- so tools like 'KnownInteger' or 'Normalized' will reject it.
-- @t'P' 0@ itself is not rejected so that it can be used to pattern-match
-- against 'Integer's at the type-level if necessary.
type P (x :: Natural) = 'P x :: Integer

data PSym0 :: Natural ~> Integer
type PSym1 :: Natural -> Integer

type instance Apply PSym0 x = PSym1 x
type PSym1 x = P x

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

-- | @'SZ' == 'sing' \@Z@
pattern SZ :: SInteger Z
pattern $mSZ :: forall {r}. SInteger Z -> ((# #) -> r) -> ((# #) -> r) -> r
$bSZ :: SInteger Z
SZ <- UnsafeSInteger _
  where SZ = Integer -> SInteger Z
forall (i :: Integer). Integer -> SInteger i
UnsafeSInteger Integer
0
{-# COMPLETE SZ #-}

-- | @'SP' ('sing' \@1) == 'sing' \@(P 1)@
pattern SP :: (0 < x)
           => (KnownInteger (P x), L.KnownNat x)
           => Sing (x :: Natural)
           -> SInteger (P x)
pattern $mSP :: forall {r} {x :: Natural}.
(0 < x) =>
SInteger (P x)
-> ((KnownInteger (P x), KnownNat x) => Sing x -> r)
-> ((# #) -> r)
-> r
$bSP :: forall (x :: Natural).
(0 < x, KnownInteger (P x), KnownNat x) =>
Sing x -> SInteger (P x)
SP x <- (patternSP -> PatternSI x)
  where SP = Integer -> SInteger (P x)
forall (i :: Integer). Integer -> SInteger i
UnsafeSInteger (Integer -> SInteger (P x))
-> (SNat x -> Integer) -> SNat x -> SInteger (P x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Natural -> Integer
forall a. Integral a => a -> Integer
toInteger (Natural -> Integer) -> (SNat x -> Natural) -> SNat x -> Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SNat x -> Natural
Sing x -> Demote Natural
forall (a :: Natural). Sing a -> Demote Natural
forall k (a :: k). SingKind k => Sing a -> Demote k
fromSing
{-# COMPLETE SP #-}

-- | @'SN' ('sing' \@1) == 'sing' \@(N 1)@
pattern SN :: (0 < x)
           => (KnownInteger (N x), L.KnownNat x)
           => Sing (x :: Natural)
           -> SInteger (N x)
pattern $mSN :: forall {r} {x :: Natural}.
(0 < x) =>
SInteger (N x)
-> ((KnownInteger (N x), KnownNat x) => Sing x -> r)
-> ((# #) -> r)
-> r
$bSN :: forall (x :: Natural).
(0 < x, KnownInteger (N x), KnownNat x) =>
Sing x -> SInteger (N x)
SN x <- (patternSN -> PatternSI x)
  where SN = Integer -> SInteger (N x)
forall (i :: Integer). Integer -> SInteger i
UnsafeSInteger (Integer -> SInteger (N x))
-> (SNat x -> Integer) -> SNat x -> SInteger (N x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> Integer
forall a. Num a => a -> a
negate (Integer -> Integer) -> (SNat x -> Integer) -> SNat x -> Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Natural -> Integer
forall a. Integral a => a -> Integer
toInteger (Natural -> Integer) -> (SNat x -> Natural) -> SNat x -> Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SNat x -> Natural
Sing x -> Demote Natural
forall (a :: Natural). Sing a -> Demote Natural
forall k (a :: k). SingKind k => Sing a -> Demote k
fromSing
{-# COMPLETE SN #-}

-- | Internal. Used to implement 'SP' and 'SN'.
data PatternSI i n = (KnownInteger i, L.KnownNat n) => PatternSI (Sing n)

patternSI :: SInteger i -> PatternSI i (Abs i)
patternSI :: forall (i :: Integer). SInteger i -> PatternSI i (Abs i)
patternSI si :: SInteger i
si@SInteger i
SInteger | Sing (Abs i)
sa <- SInteger i -> Sing (Abs i)
forall (i :: Integer). SInteger i -> Sing (Abs i)
sAbs SInteger i
si = SNat (Abs i)
-> (KnownNat (Abs i) => PatternSI i (Abs i)) -> PatternSI i (Abs i)
forall (n :: Natural) r. SNat n -> (KnownNat n => r) -> r
L.withKnownNat SNat (Abs i)
Sing (Abs i)
sa (Sing (Abs i) -> PatternSI i (Abs i)
forall (i :: Integer) (n :: Natural).
(KnownInteger i, KnownNat n) =>
Sing n -> PatternSI i n
PatternSI Sing (Abs i)
sa)

patternSN :: SInteger (N x) -> PatternSI (N x) x
patternSN :: forall (x :: Natural). SInteger (N x) -> PatternSI (N x) x
patternSN = PatternSI (N x) (Fold 0 IdSym0 IdSym0 (N x)) -> PatternSI (N x) x
forall a b. a -> b
unsafeCoerce (PatternSI (N x) (Fold 0 IdSym0 IdSym0 (N x)) -> PatternSI (N x) x)
-> (SInteger (N x) -> PatternSI (N x) (Fold 0 IdSym0 IdSym0 (N x)))
-> SInteger (N x)
-> PatternSI (N x) x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SInteger (N x) -> PatternSI (N x) (Fold 0 IdSym0 IdSym0 (N x))
forall (i :: Integer). SInteger i -> PatternSI i (Abs i)
patternSI

patternSP :: SInteger (P x) -> PatternSI (P x) x
patternSP :: forall (x :: Natural). SInteger (P x) -> PatternSI (P x) x
patternSP = PatternSI (P x) (Fold 0 IdSym0 IdSym0 (P x)) -> PatternSI (P x) x
forall a b. a -> b
unsafeCoerce (PatternSI (P x) (Fold 0 IdSym0 IdSym0 (P x)) -> PatternSI (P x) x)
-> (SInteger (P x) -> PatternSI (P x) (Fold 0 IdSym0 IdSym0 (P x)))
-> SInteger (P x)
-> PatternSI (P x) x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SInteger (P x) -> PatternSI (P x) (Fold 0 IdSym0 IdSym0 (P x))
forall (i :: Integer). SInteger i -> PatternSI i (Abs i)
patternSI

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

-- | @'Fold' z n p i@ evaluates to @z@ if @i@ is zero, otherwise applies @n@ to
-- the absolute value of @i@ if negative, or @p@ to the absolute value of @i@ if
-- positive. @t'N' 0@ and @t'P' 0@ fail to type-check.
type family Fold
     (z :: k)
     (n :: Natural ~> k)
     (p :: Natural ~> k)
     (i :: Integer)
     :: k where
  Fold _ _ _ (N 0) = L.TypeError ('L.Text "Use ‘Z’ instead of ‘N 0’.")
  Fold _ _ _ (P 0) = L.TypeError ('L.Text "Use ‘Z’ instead of ‘P 0’.")
  Fold z _ _  Z    = z
  Fold _ n _ (N x) = n @@ x
  Fold _ _ p (P x) = p @@ x

data FoldSym0 :: k ~> (Natural ~> k) ~> (Natural ~> k) ~> Integer ~> k
data FoldSym1 :: k -> (Natural ~> k) ~> (Natural ~> k) ~> Integer ~> k
data FoldSym2 :: k -> (Natural ~> k) -> (Natural ~> k) ~> Integer ~> k
data FoldSym3 :: k -> (Natural ~> k) -> (Natural ~> k) -> Integer ~> k
type FoldSym4 :: k -> (Natural ~> k) -> (Natural ~> k) -> Integer -> k

type instance Apply FoldSym0 z = FoldSym1 z
type instance Apply (FoldSym1 z) n = FoldSym2 z n
type instance Apply (FoldSym2 z n) p = FoldSym3 z n p
type instance Apply (FoldSym3 z n p) i = FoldSym4 z n p i
type FoldSym4 z n p i = Fold z n p i

-- | Singleton version of 'Fold'.
sFold
  :: SingKind k
  => Sing (z :: k)
  -> Sing (n :: Natural ~> k)
  -> Sing (p :: Natural ~> k)
  -> SInteger i
  -> Sing (Fold z n p i)
sFold :: forall k (z :: k) (n :: Natural ~> k) (p :: Natural ~> k)
       (i :: Integer).
SingKind k =>
Sing z -> Sing n -> Sing p -> SInteger i -> Sing (Fold z n p i)
sFold Sing z
sz Sing n
sn Sing p
sp SInteger i
si =
  case Demote Integer -> Demote Integer -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (Sing i -> Demote Integer
forall k (a :: k). SingKind k => Sing a -> Demote k
forall (a :: Integer). Sing a -> Demote Integer
fromSing Sing i
SInteger i
si) Demote Integer
0 of
    Ordering
EQ -> Sing z -> Sing (Fold z n p i)
forall a b. a -> b
unsafeCoerce Sing z
sz
    Ordering
LT -> Sing (Apply n (Fold 0 IdSym0 IdSym0 i)) -> Sing (Fold z n p i)
forall a b. a -> b
unsafeCoerce (Sing n
sn Sing n
-> Sing (Fold 0 IdSym0 IdSym0 i)
-> Sing (Apply n (Fold 0 IdSym0 IdSym0 i))
forall k1 k2 (f :: k1 ~> k2) (t :: k1).
Sing f -> Sing t -> Sing (f @@ t)
@@ SInteger i -> Sing (Fold 0 IdSym0 IdSym0 i)
forall (i :: Integer). SInteger i -> Sing (Abs i)
sAbs SInteger i
si)
    Ordering
GT -> Sing (Apply p (Fold 0 IdSym0 IdSym0 i)) -> Sing (Fold z n p i)
forall a b. a -> b
unsafeCoerce (Sing p
sp Sing p
-> Sing (Fold 0 IdSym0 IdSym0 i)
-> Sing (Apply p (Fold 0 IdSym0 IdSym0 i))
forall k1 k2 (f :: k1 ~> k2) (t :: k1).
Sing f -> Sing t -> Sing (f @@ t)
@@ SInteger i -> Sing (Fold 0 IdSym0 IdSym0 i)
forall (i :: Integer). SInteger i -> Sing (Abs i)
sAbs SInteger i
si)

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

-- | Displays @i@ as it would show literally as a term.
--
-- @
-- 'P.Show_' ( t'N' 1) ~ \"-1\"
-- 'P.Show_'   t'Z'    ~  \"0\"
-- 'P.Show_' ( t'P' 1) ~  \"1\"
-- @
--
-- @t'N' 0@ and @t'P' 0@ fail to type-check.
instance P.PShow Integer where
  type ShowsPrec p i s = ShowsPrec_ p (Normalized i) s

type ShowsPrec_ :: Natural -> Integer -> L.Symbol -> L.Symbol
type family ShowsPrec_ p i s where
  ShowsPrec_ _  Z    s = P.Shows 0 s
  ShowsPrec_ p (N x) s =
    P.ShowParen (p P.>= AppPrec1) (P.ShowCharSym1 '-' P..@#@$$$ P.ShowsSym1 x) s
  ShowsPrec_ _ (P x) s = P.Shows x s

-- | Displays @i@ as it would show literally as a term.
--
-- @
-- 'fromSing' \@('P.sShow_' ('SN' ('sing' \@1))) == \"-1\"
-- 'fromSing' \@('P.sShow_' 'SZ')             ==  \"0\"
-- 'fromSing' \@('P.sShow_' ('SP' ('sing' \@1))) ==  \"1\"
-- @
instance P.SShow Integer where
  sShowsPrec :: forall (t1 :: Natural) (t2 :: Integer) (t3 :: Symbol).
Sing t1
-> Sing t2
-> Sing t3
-> Sing (Apply (Apply (Apply ShowsPrecSym0 t1) t2) t3)
sShowsPrec Sing t1
_ Sing t2
si Sing t3
ss =
    Demote Symbol
-> (forall (a :: Symbol).
    Sing a -> SSymbol (ShowsPrec_ t1 (Normalized t2) t3))
-> SSymbol (ShowsPrec_ t1 (Normalized t2) t3)
forall k r.
SingKind k =>
Demote k -> (forall (a :: k). Sing a -> r) -> r
withSomeSing (String -> Demote Symbol
forall a. IsString a => String -> a
fromString (Demote Integer -> String
forall a. Show a => a -> String
show (Sing t2 -> Demote Integer
forall k (a :: k). SingKind k => Sing a -> Demote k
forall (a :: Integer). Sing a -> Demote Integer
fromSing Sing t2
si)) Demote Symbol -> Demote Symbol -> Demote Symbol
forall a. Semigroup a => a -> a -> a
<> Sing t3 -> Demote Symbol
forall k (a :: k). SingKind k => Sing a -> Demote k
forall (a :: Symbol). Sing a -> Demote Symbol
fromSing Sing t3
ss) SSymbol a -> SSymbol (ShowsPrec_ t1 (Normalized t2) t3)
Sing a -> SSymbol (ShowsPrec_ t1 (Normalized t2) t3)
forall a b. a -> b
forall (a :: Symbol).
Sing a -> SSymbol (ShowsPrec_ t1 (Normalized t2) t3)
unsafeCoerce

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

-- | Displays @i@ as it would show literally as a type.
--
-- @
-- 'P.ShowLit' ( t'N' 1) ~ \"P 1\"
-- 'P.ShowLit'   t'Z'    ~ \"Z\"
-- 'P.ShowLit' ( t'P' 1) ~ \"P 1\"
-- @
--
-- @t'N' 0@ and @t'P' 0@ fail to type-check.
type ShowLit (i :: Integer) = ShowsLit i "" :: L.Symbol

data ShowLitSym0 :: Integer ~> L.Symbol
type ShowLitSym1 :: Integer -> L.Symbol

type instance Apply ShowLitSym0 i = ShowLitSym1 i
type ShowLitSym1 i = ShowLit i

-- | Displays @i@ as it would show literally as a type. See 'ShowLit.
-- Behaves like 'P.Shows'.
type ShowsLit (i :: Integer) (s :: L.Symbol) = ShowsPrecLit 0 i s :: L.Symbol

data ShowsLitSym0 :: Integer ~> L.Symbol ~> L.Symbol
data ShowsLitSym1 :: Integer -> L.Symbol ~> L.Symbol
type ShowsLitSym2 :: Integer -> L.Symbol -> L.Symbol

type instance Apply ShowsLitSym0 i = ShowsLitSym1 i
type instance Apply (ShowsLitSym1 i) s = ShowsLitSym2 i s
type ShowsLitSym2 i s = ShowsLit i s

-- | Displays @i@ as it would show literally as a type. See 'ShowLit.
-- Behaves like 'P.ShowsPrec'.
type ShowsPrecLit :: Natural -> Integer -> L.Symbol -> L.Symbol
type ShowsPrecLit p i s = ShowsPrecLit_ p (Normalized i) s

type ShowsPrecLit_ :: Natural -> Integer -> L.Symbol -> L.Symbol
type family ShowsPrecLit_ p i s where
  ShowsPrecLit_ _ Z s = P.ShowString "Z" s
  ShowsPrecLit_ p (N n) s =
    P.ShowParen (p P.>= 11) (P.ShowStringSym1 "N " P..@#@$$$ P.ShowsSym1 n) s
  ShowsPrecLit_ p (P n) s =
    P.ShowParen (p P.>= 11) (P.ShowStringSym1 "P " P..@#@$$$ P.ShowsSym1 n) s

data ShowsPrecLitSym0 :: Natural ~> Integer ~> L.Symbol ~> L.Symbol
data ShowsPrecLitSym1 :: Natural -> Integer ~> L.Symbol ~> L.Symbol
data ShowsPrecLitSym2 :: Natural -> Integer -> L.Symbol ~> L.Symbol
type ShowsPrecLitSym3 :: Natural -> Integer -> L.Symbol -> L.Symbol

type instance Apply ShowsPrecLitSym0 p = ShowsPrecLitSym1 p
type instance Apply (ShowsPrecLitSym1 p) i = ShowsPrecLitSym2 p i
type instance Apply (ShowsPrecLitSym2 p i) s = ShowsPrecLitSym3 p i s
type ShowsPrecLitSym3 p i s = ShowsPrecLit p i s

-- | Singleton version of 'ShowLit'.
--
-- @
-- 'fromSing' \@('sShowLit' ('SN' ('sing' \@1))) == \"N 1\"
-- 'fromSing' \@('sShowLit' 'SZ')             == \"Z"
-- 'fromSing' \@('sShowLit' ('SP' ('sing' \@1))) == \"P 1\"
-- @
sShowLit :: SInteger i -> Sing (ShowLit i)
sShowLit :: forall (i :: Integer). SInteger i -> Sing (ShowLit i)
sShowLit SInteger i
si = SInteger i -> Sing "" -> Sing (ShowsPrecLit_ 0 (Normalized i) "")
forall (i :: Integer) (s :: Symbol).
SInteger i -> Sing s -> Sing (ShowsLit i s)
sShowsLit SInteger i
si (forall {k} (a :: k). SingI a => Sing a
forall (a :: Symbol). SingI a => Sing a
sing @"")

-- | Demoted version of 'ShowLit'.
showLit :: P.Integer -> String
showLit :: Integer -> String
showLit Integer
i = Integer -> ShowS
showsLit Integer
i String
""

-- | Singleton version of 'ShowsLit'.
sShowsLit :: SInteger i -> Sing (s :: P.Symbol) -> Sing (ShowsLit i s)
sShowsLit :: forall (i :: Integer) (s :: Symbol).
SInteger i -> Sing s -> Sing (ShowsLit i s)
sShowsLit = Sing 0
-> SInteger i -> Sing s -> Sing (ShowsPrecLit_ 0 (Normalized i) s)
forall (p :: Natural) (i :: Integer) (s :: Symbol).
Sing p -> SInteger i -> Sing s -> Sing (ShowsPrecLit p i s)
sShowsPrecLit (forall (a :: Natural). SingI a => Sing a
forall {k} (a :: k). SingI a => Sing a
sing @0)

-- | Demoted version of 'ShowsLit'.
showsLit :: P.Integer -> ShowS
showsLit :: Integer -> ShowS
showsLit = Int -> Integer -> ShowS
showsPrecLit Int
0

-- | Singleton version of 'ShowsPrecLit'.
sShowsPrecLit
  :: Sing (p :: Natural) -> SInteger i -> Sing (s :: P.Symbol)
  -> Sing (ShowsPrecLit p i s)
sShowsPrecLit :: forall (p :: Natural) (i :: Integer) (s :: Symbol).
Sing p -> SInteger i -> Sing s -> Sing (ShowsPrecLit p i s)
sShowsPrecLit Sing p
sp SInteger i
si Sing s
ss =
  let p :: Int
p = Int -> Maybe Int -> Int
forall a. a -> Maybe a -> a
fromMaybe (String -> Int
forall a. HasCallStack => String -> a
error String
"sShowsPrecLit: invalid precedence")
                    (Demote Natural -> Maybe Int
forall a b.
(Integral a, Integral b, Bits a, Bits b) =>
a -> Maybe b
toIntegralSized (Sing p -> Demote Natural
forall (a :: Natural). Sing a -> Demote Natural
forall k (a :: k). SingKind k => Sing a -> Demote k
fromSing Sing p
sp))
      t :: Demote Symbol
t = String -> Demote Symbol
forall a. IsString a => String -> a
fromString (Int -> Integer -> ShowS
showsPrecLit Int
p (Sing i -> Demote Integer
forall k (a :: k). SingKind k => Sing a -> Demote k
forall (a :: Integer). Sing a -> Demote Integer
fromSing Sing i
SInteger i
si) String
"")
  in Demote Symbol
-> (forall (a :: Symbol).
    Sing a -> SSymbol (ShowsPrecLit_ p (Normalized i) s))
-> SSymbol (ShowsPrecLit_ p (Normalized i) s)
forall k r.
SingKind k =>
Demote k -> (forall (a :: k). Sing a -> r) -> r
withSomeSing (Demote Symbol
t Demote Symbol -> Demote Symbol -> Demote Symbol
forall a. Semigroup a => a -> a -> a
<> Sing s -> Demote Symbol
forall k (a :: k). SingKind k => Sing a -> Demote k
forall (a :: Symbol). Sing a -> Demote Symbol
fromSing Sing s
ss) SSymbol a -> SSymbol (ShowsPrecLit_ p (Normalized i) s)
Sing a -> SSymbol (ShowsPrecLit_ p (Normalized i) s)
forall a b. a -> b
forall (a :: Symbol).
Sing a -> SSymbol (ShowsPrecLit_ p (Normalized i) s)
unsafeCoerce

-- | Demoted version of 'ShowsPrecLit'.
showsPrecLit :: Int -> P.Integer -> ShowS
showsPrecLit :: Int -> Integer -> ShowS
showsPrecLit Int
p | Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
0 = String -> Integer -> ShowS
forall a. HasCallStack => String -> a
error String
"showsPrecLit: negative precedence"
showsPrecLit Int
p = \case
  Integer
0         -> Char -> ShowS
showChar Char
'Z'
  Integer
i | Integer
i Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> Integer
0 -> Bool -> ShowS -> ShowS
showParen (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
appPrec1) (String -> ShowS
showString String
"P " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> ShowS
forall a. Show a => a -> ShowS
shows Integer
i)
  Integer
i         -> Bool -> ShowS -> ShowS
showParen (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
appPrec1) (String -> ShowS
showString String
"N " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> ShowS
forall a. Show a => a -> ShowS
shows (Integer -> Integer
forall a. Num a => a -> a
abs Integer
i))

-- | Inverse of 'showsPrecLit'.
readPrecLit :: ReadPrec.ReadPrec P.Integer
readPrecLit :: ReadPrec Integer
readPrecLit = ReadPrec Integer -> ReadPrec Integer
forall a. ReadPrec a -> ReadPrec a
Read.parens (ReadPrec Integer -> ReadPrec Integer)
-> ReadPrec Integer -> ReadPrec Integer
forall a b. (a -> b) -> a -> b
$ [ReadPrec Integer] -> ReadPrec Integer
forall (t :: Type -> Type) (f :: Type -> Type) a.
(Foldable t, Alternative f) =>
t (f a) -> f a
asum
    [ Integer
0 Integer -> ReadPrec Char -> ReadPrec Integer
forall a b. a -> ReadPrec b -> ReadPrec a
forall (f :: Type -> Type) a b. Functor f => a -> f b -> f a
<$ ReadP Char -> ReadPrec Char
forall a. ReadP a -> ReadPrec a
ReadPrec.lift (Char -> ReadP Char
ReadP.char Char
'Z')
    , do ReadP () -> ReadPrec ()
forall a. ReadP a -> ReadPrec a
ReadPrec.lift (ReadP () -> ReadPrec ()) -> ReadP () -> ReadPrec ()
forall a b. (a -> b) -> a -> b
$ Char -> ReadP Char
ReadP.char Char
'N' ReadP Char -> ReadP () -> ReadP ()
forall a b. ReadP a -> ReadP b -> ReadP b
forall (m :: Type -> Type) a b. Monad m => m a -> m b -> m b
>> ReadP ()
pSkipSpaces1
         Natural
n <- ReadPrec Natural -> ReadPrec Natural
forall a. ReadPrec a -> ReadPrec a
Read.parens (ReadP Natural -> ReadPrec Natural
forall a. ReadP a -> ReadPrec a
ReadPrec.lift ReadP Natural
pNatural)
         Bool -> ReadPrec ()
forall (f :: Type -> Type). Alternative f => Bool -> f ()
guard (Natural
n Natural -> Natural -> Bool
forall a. Eq a => a -> a -> Bool
P./= Natural
0)
         Integer -> ReadPrec Integer
forall a. a -> ReadPrec a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Integer -> ReadPrec Integer) -> Integer -> ReadPrec Integer
forall a b. (a -> b) -> a -> b
$ Integer -> Integer
forall a. Num a => a -> a
negate (Integer -> Integer) -> Integer -> Integer
forall a b. (a -> b) -> a -> b
$ Natural -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral Natural
n
    , do ReadP () -> ReadPrec ()
forall a. ReadP a -> ReadPrec a
ReadPrec.lift (ReadP () -> ReadPrec ()) -> ReadP () -> ReadPrec ()
forall a b. (a -> b) -> a -> b
$ Char -> ReadP Char
ReadP.char Char
'P' ReadP Char -> ReadP () -> ReadP ()
forall a b. ReadP a -> ReadP b -> ReadP b
forall (m :: Type -> Type) a b. Monad m => m a -> m b -> m b
>> ReadP ()
pSkipSpaces1
         Natural
n <- ReadPrec Natural -> ReadPrec Natural
forall a. ReadPrec a -> ReadPrec a
Read.parens (ReadP Natural -> ReadPrec Natural
forall a. ReadP a -> ReadPrec a
ReadPrec.lift ReadP Natural
pNatural)
         Bool -> ReadPrec ()
forall (f :: Type -> Type). Alternative f => Bool -> f ()
guard (Natural
n Natural -> Natural -> Bool
forall a. Eq a => a -> a -> Bool
P./= Natural
0)
         Integer -> ReadPrec Integer
forall a. a -> ReadPrec a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Integer -> ReadPrec Integer) -> Integer -> ReadPrec Integer
forall a b. (a -> b) -> a -> b
$ Natural -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral Natural
n
    ]
  where
    pNatural :: ReadP.ReadP Natural
    pNatural :: ReadP Natural
pNatural = String -> Natural
forall a. Read a => String -> a
read (String -> Natural) -> ReadP String -> ReadP Natural
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (Char -> Bool) -> ReadP String
ReadP.munch1 (\Char
c -> Char
c Char -> Char -> Bool
forall a. Ord a => a -> a -> Bool
>= Char
'0' Bool -> Bool -> Bool
&& Char
c Char -> Char -> Bool
forall a. Ord a => a -> a -> Bool
<= Char
'9')

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

-- | This class gives the 'SInteger' associated with a type-level 'Integer'.
class KnownInteger_ (i :: Integer) where
  integerSing_ :: SInteger i

-- | Type-level 'Integer's satisfying 'KnownInteger' can be converted to
-- 'SInteger's using 'integerSing'. Every 'Integer' other than @'N' 0@ and
-- @'P' 0@ are 'KnownInteger's.

-- Note: Ideally, the constraints mentioned here would be superclasses to
-- 'KnownInteger_'. However, 'withDict' doesn't allow having a superclass
-- there, so we treat 'KnownInteger_' as internal an export 'KnownInteger' only.
-- The 'KnownNat (Abs i)' constraint is listed here as a convenience, seeing
-- as it is necessary to implement 'KnownInteger_' anyway.
type KnownInteger (i :: Integer) =
  (KnownInteger_ i, Normalized i ~ i, L.KnownNat (Abs i))

data KnownIntegerSym0 :: Integer ~> Constraint
type KnownIntegerSym1 :: Integer -> Constraint

type instance Apply KnownIntegerSym0 i = KnownIntegerSym1 i
type KnownIntegerSym1 i = KnownInteger i

-- | Convert an implicit 'KnownInteger' to an explicit 'SInteger'.
integerSing :: KnownInteger i => SInteger i
integerSing :: forall (i :: Integer). KnownInteger i => SInteger i
integerSing = SInteger i
forall (i :: Integer). KnownInteger_ i => SInteger i
integerSing_ -- The difference is in the constraint.
{-# INLINE integerSing #-}

instance KnownInteger_ Z where
  integerSing_ :: SInteger Z
integerSing_ = Integer -> SInteger Z
forall (i :: Integer). Integer -> SInteger i
UnsafeSInteger Integer
0
  {-# INLINE integerSing_ #-}

instance (KnownInteger (N n), n ~ Abs (N n)) => KnownInteger_ (N n) where
  integerSing_ :: SInteger (N n)
integerSing_ = Integer -> SInteger (N n)
forall (i :: Integer). Integer -> SInteger i
UnsafeSInteger (Integer -> SInteger (N n)) -> Integer -> SInteger (N n)
forall a b. (a -> b) -> a -> b
$! Integer -> Integer
forall a. Num a => a -> a
P.negate (Proxy n -> 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 @n))
  {-# INLINE integerSing_ #-}

instance (KnownInteger (P n), n ~ Abs (P n)) => KnownInteger_ (P n) where
  integerSing_ :: SInteger (P n)
integerSing_ = Integer -> SInteger (P n)
forall (i :: Integer). Integer -> SInteger i
UnsafeSInteger (Integer -> SInteger (P n)) -> Integer -> SInteger (P n)
forall a b. (a -> b) -> a -> b
$! Proxy n -> 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 @n)
  {-# INLINE integerSing_ #-}

-- | @'Normalized' i@ is an identity function that fails to type-check
-- if @i@ is not in normalized form. That is, /zero/ is represented with t'Z',
-- not with @t'P' 0@ or @ t'N' 0@.
type family Normalized (i :: Integer) :: Integer where
  Normalized (N 0) = L.TypeError ('L.Text "Use ‘Z’ instead of ‘N 0’.")
  Normalized (P 0) = L.TypeError ('L.Text "Use ‘Z’ instead of ‘P 0’.")
  Normalized i     = i

data NormalizedSym0 :: Integer ~> Integer
type NormalizedSym1 :: Integer -> Integer

type instance Apply NormalizedSym0 i = Normalized i
type NormalizedSym1 i = Normalized i

-- | 'SInteger' contains only 'Normalized' integers.
sNormalizedRefl :: SInteger i -> (i :~: Normalized i)
sNormalizedRefl :: forall (i :: Integer). SInteger i -> i :~: Normalized i
sNormalizedRefl !SInteger i
_ = (Any :~: Any) -> i :~: Normalized i
forall a b. a -> b
unsafeCoerce Any :~: Any
forall {k} (a :: k). a :~: a
Refl

-- | Term-level "Prelude".'P.Integer' representation of the type-level
-- 'Integer'.
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
{-# INLINE integerVal #-}

-- | Term-level representation of an existentialized 'KnownInteger'.
data SomeInteger = forall i. KnownInteger i => SomeInteger (Proxy i)

-- | Convert a term-level "Prelude".'P.Integer' into an
-- extistentialized 'KnownInteger' wrapped in 'SomeInteger'.
someIntegerVal :: P.Integer -> SomeInteger
someIntegerVal :: Integer -> SomeInteger
someIntegerVal = \Integer
i ->
  Integer
-> (forall {i :: Integer}. Sing i -> SomeInteger) -> SomeInteger
forall x. Integer -> (forall (i :: Integer). Sing i -> x) -> x
withSomeSInteger Integer
i ((forall {i :: Integer}. Sing i -> SomeInteger) -> SomeInteger)
-> (forall {i :: Integer}. Sing i -> SomeInteger) -> SomeInteger
forall a b. (a -> b) -> a -> b
$ \(SInteger i
si :: SInteger i) ->
  SInteger i -> (KnownInteger i => SomeInteger) -> SomeInteger
forall (i :: Integer) x. SInteger i -> (KnownInteger i => x) -> x
withKnownInteger SInteger i
si ((KnownInteger i => SomeInteger) -> SomeInteger)
-> (KnownInteger i => SomeInteger) -> SomeInteger
forall a b. (a -> b) -> a -> b
$ Proxy i -> SomeInteger
forall (i :: Integer). KnownInteger i => Proxy i -> SomeInteger
SomeInteger (forall {k} (t :: k). Proxy t
forall (t :: Integer). Proxy t
Proxy @i)

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

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

-- | As for "Prelude".'P.Integer'.
instance P.Show SomeInteger where
  showsPrec :: Int -> SomeInteger -> ShowS
showsPrec Int
p (SomeInteger Proxy i
i) =
    Int -> Integer -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
p (Proxy i -> Integer
forall (i :: Integer) (proxy :: Integer -> Type).
KnownInteger i =>
proxy i -> Integer
integerVal Proxy i
i)

-- | As for "Prelude".'P.Integer'.
instance Read SomeInteger where
  readPrec :: ReadPrec SomeInteger
readPrec = (Integer -> SomeInteger)
-> ReadPrec Integer -> ReadPrec SomeInteger
forall a b. (a -> b) -> ReadPrec a -> ReadPrec b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap Integer -> SomeInteger
someIntegerVal ReadPrec Integer
forall a. Read a => ReadPrec a
Read.readPrec

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

-- | Construct a type-level 'Integer' from a type-level 'Natural'.
type family FromNatural (x :: Natural) :: Integer where
  FromNatural 0 = Z
  FromNatural x = P x

data FromNaturalSym0 :: Natural ~> Integer
type FromNaturalSym1 :: Natural -> Integer

type instance Apply FromNaturalSym0 i = FromNatural i
type FromNaturalSym1 i = FromNatural i

-- | Singleton version of 'FromNatural'.
sFromNatural :: Sing (x :: Natural) -> SInteger (FromNatural x)
sFromNatural :: forall (x :: Natural). Sing x -> SInteger (FromNatural x)
sFromNatural = Integer -> SInteger (FromNatural x)
forall (i :: Integer). Integer -> SInteger i
UnsafeSInteger (Integer -> SInteger (FromNatural x))
-> (SNat x -> Integer) -> SNat x -> SInteger (FromNatural x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Natural -> Integer
forall a. Integral a => a -> Integer
toInteger (Natural -> Integer) -> (SNat x -> Natural) -> SNat x -> Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SNat x -> Natural
Sing x -> Demote Natural
forall (a :: Natural). Sing a -> Demote Natural
forall k (a :: k). SingKind k => Sing a -> Demote k
fromSing
{-# INLINE sFromNatural #-}

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

-- | Demoted version of 'ZigZag'.
zigZag :: P.Integer -> Natural
zigZag :: Integer -> Natural
zigZag Integer
0 = Natural
0
zigZag Integer
i = Integer -> Natural
forall a. Num a => Integer -> a
fromInteger (if Integer
i Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
0 then Integer -> Integer
forall a. Num a => a -> a
abs Integer
i Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Integer
2 Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
1 else Integer
i Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Integer
2)

-- | Singleton version of 'ZigZag'.
sZigZag :: SInteger i -> Sing (ZigZag i :: Natural)
sZigZag :: forall (i :: Integer). SInteger i -> Sing (ZigZag i)
sZigZag SInteger i
si = forall k r.
SingKind k =>
Demote k -> (forall (a :: k). Sing a -> r) -> r
withSomeSing @Natural (Integer -> Natural
zigZag (Sing i -> Demote Integer
forall k (a :: k). SingKind k => Sing a -> Demote k
forall (a :: Integer). Sing a -> Demote Integer
fromSing Sing i
SInteger i
si)) SNat a -> SNat (ZigZag_ (Normalized i))
Sing a -> SNat (ZigZag_ (Normalized i))
forall (a :: Natural). Sing a -> SNat (ZigZag_ (Normalized i))
forall a b. a -> b
unsafeCoerce

-- | Identity.
sZigZagRefl :: SInteger i -> (i :~: ZagZig (ZigZag i))
sZigZagRefl :: forall (i :: Integer). SInteger i -> i :~: ZagZig (ZigZag i)
sZigZagRefl !SInteger i
_ = (Any :~: Any)
-> i
   :~: If
         (DefaultEq (Mod (ZigZag i) 2) 1)
         (Fold Z PSym0 NSym0 (FromNatural (Div (ZigZag i + 1) 2)))
         (FromNatural (Div (ZigZag i) 2))
forall a b. a -> b
unsafeCoerce Any :~: Any
forall {k} (a :: k). a :~: a
Refl

-- | Demoted version of 'ZagZig'.
zagZig :: Natural -> P.Integer
zagZig :: Natural -> Integer
zagZig Natural
0 = Integer
0
zagZig Natural
n = if Natural -> Bool
forall a. Integral a => a -> Bool
odd Natural
n then Integer -> Integer
forall a. Num a => a -> a
P.negate (Natural -> Integer
forall a. Integral a => a -> Integer
P.toInteger (Natural -> Natural -> Natural
forall a. Integral a => a -> a -> a
P.div (Natural
n Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
+ Natural
1) Natural
2))
                    else Natural -> Integer
forall a. Integral a => a -> Integer
P.toInteger (Natural -> Natural -> Natural
forall a. Integral a => a -> a -> a
P.div Natural
n Natural
2)

-- | Singleton version of 'ZagZig'.
sZagZig :: Sing (n :: Natural) -> SInteger (ZagZig n)
sZagZig :: forall (n :: Natural). Sing n -> SInteger (ZagZig n)
sZagZig = Integer
-> SInteger
     (If
        (DefaultEq (Mod n 2) 1)
        (Fold Z PSym0 NSym0 (FromNatural (Div (n + 1) 2)))
        (FromNatural (Div n 2)))
forall (i :: Integer). Integer -> SInteger i
UnsafeSInteger (Integer
 -> SInteger
      (If
         (DefaultEq (Mod n 2) 1)
         (Fold Z PSym0 NSym0 (FromNatural (Div (n + 1) 2)))
         (FromNatural (Div n 2))))
-> (SNat n -> Integer)
-> SNat n
-> SInteger
     (If
        (DefaultEq (Mod n 2) 1)
        (Fold Z PSym0 NSym0 (FromNatural (Div (n + 1) 2)))
        (FromNatural (Div n 2)))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Natural -> Integer
zagZig (Natural -> Integer) -> (SNat n -> Natural) -> SNat n -> Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SNat n -> Natural
Sing n -> Demote Natural
forall (a :: Natural). Sing a -> Demote Natural
forall k (a :: k). SingKind k => Sing a -> Demote k
fromSing

-- | Identity.
sZagZigRefl :: Sing (n :: Natural) -> (n :~: ZigZag (ZagZig n))
sZagZigRefl :: forall (n :: Natural). Sing n -> n :~: ZigZag (ZagZig n)
sZagZigRefl !Sing n
_ = (Any :~: Any)
-> n
   :~: ZigZag_
         (Normalized
            (If
               (DefaultEq (Mod n 2) 1)
               (Fold Z PSym0 NSym0 (FromNatural (Div (n + 1) 2)))
               (FromNatural (Div n 2))))
forall a b. a -> b
unsafeCoerce Any :~: Any
forall {k} (a :: k). a :~: a
Refl

-- | ZigZag encoding of an 'Integer'.
--
-- * /0/ is /0/
--
-- * /-x/ is /abs(x) * 2 - 1/
--
-- * /+x/ is /x * 2/
type ZigZag :: Integer -> Natural
type ZigZag (i :: Integer) = ZigZag_ (Normalized i) :: Natural
type family ZigZag_ (i :: Integer) :: Natural where
  ZigZag_  Z    = 0
  ZigZag_ (P x) = x P.* 2
  ZigZag_ (N x) = x P.* 2 P.- 1

data ZigZagSym0 :: Integer ~> Natural
type ZigZagSym1 :: Integer -> Natural

type instance Apply ZigZagSym0 i = ZigZagSym1 i
type ZigZagSym1 i = ZigZag i

-- | Inverse of 'ZigZag'.
type ZagZig :: Natural -> Integer
type ZagZig n = If (L.Mod n 2 P.== 1)
                   (P.Negate (FromNatural (L.Div (n L.+ 1) 2)))
                   (FromNatural (L.Div n 2))

data ZagZigSym0 :: Natural ~> Integer
type ZagZigSym1 :: Natural -> Integer

type instance Apply ZagZigSym0 n = ZagZigSym1 n
type ZagZigSym1 n = ZagZig n

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


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

data OddSym0 :: Integer ~> Bool
type OddSym1 :: Integer -> Bool

type instance Apply OddSym0 i = Odd i
type OddSym1 i = Odd i

-- | Singleton version of 'Odd'.
sOdd :: SInteger i -> Sing (Odd i :: Bool)
sOdd :: forall (i :: Integer). SInteger i -> Sing (Odd i)
sOdd SInteger i
si | Demote Integer -> Bool
forall a. Integral a => a -> Bool
odd (Sing i -> Demote Integer
forall k (a :: k). SingKind k => Sing a -> Demote k
forall (a :: Integer). Sing a -> Demote Integer
fromSing Sing i
SInteger i
si) = SBool 'True -> SBool (DefaultEq (Mod (Abs i) 2) 1)
forall a b. a -> b
unsafeCoerce SBool 'True
STrue
        | Bool
otherwise         = SBool 'False -> SBool (DefaultEq (Mod (Abs i) 2) 1)
forall a b. a -> b
unsafeCoerce SBool 'False
SFalse

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

data EvenSym0 :: Integer ~> Bool
type EvenSym1 :: Integer -> Bool

type instance Apply EvenSym0 i = Even i
type EvenSym1 i = Even i

-- | Singleton version of 'Even'.
sEven :: SInteger i -> Sing (Even i :: Bool)
sEven :: forall (i :: Integer). SInteger i -> Sing (Even i)
sEven SInteger i
si | Demote Integer -> Bool
forall a. Integral a => a -> Bool
even (Sing i -> Demote Integer
forall k (a :: k). SingKind k => Sing a -> Demote k
forall (a :: Integer). Sing a -> Demote Integer
fromSing Sing i
SInteger i
si) = SBool 'True -> SBool (DefaultEq (Mod (Abs i) 2) 0)
forall a b. a -> b
unsafeCoerce SBool 'True
STrue
         | Bool
otherwise          = SBool 'False -> SBool (DefaultEq (Mod (Abs i) 2) 0)
forall a b. a -> b
unsafeCoerce SBool 'False
SFalse

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

-- | Double negation is identity.
sNegateRefl :: SInteger i -> (i :~: P.Negate (P.Negate i))
sNegateRefl :: forall (i :: Integer). SInteger i -> i :~: Negate (Negate i)
sNegateRefl !SInteger i
_ = (Any :~: Any) -> i :~: Fold Z PSym0 NSym0 (Fold Z PSym0 NSym0 i)
forall a b. a -> b
unsafeCoerce Any :~: Any
forall {k} (a :: k). a :~: a
Refl

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

-- | Absolute value of a type-level 'Integer', as a type-level 'Natural'.
type Abs (i :: Integer) = Fold 0 P.IdSym0 P.IdSym0 i :: Natural

data AbsSym0 :: Integer ~> Natural
type AbsSym1 :: Integer -> Natural

type instance Apply AbsSym0 x = AbsSym1 x
type AbsSym1 x = Abs x

-- | Singleton version of 'Abs'.
sAbs :: SInteger i -> Sing (Abs i :: Natural)
sAbs :: forall (i :: Integer). SInteger i -> Sing (Abs i)
sAbs SInteger i
si = forall k r.
SingKind k =>
Demote k -> (forall (a :: k). Sing a -> r) -> r
withSomeSing @Natural (Integer -> Natural
forall a. Num a => Integer -> a
fromInteger (Integer -> Integer
forall a. Num a => a -> a
abs (Sing i -> Demote Integer
forall k (a :: k). SingKind k => Sing a -> Demote k
forall (a :: Integer). Sing a -> Demote Integer
fromSing Sing i
SInteger i
si))) SNat a -> SNat (Fold 0 IdSym0 IdSym0 i)
Sing a -> SNat (Fold 0 IdSym0 IdSym0 i)
forall (a :: Natural). Sing a -> SNat (Fold 0 IdSym0 IdSym0 i)
forall a b. a -> b
unsafeCoerce

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

infixr 8 %^, ^, ^@#@$$$

-- | Singleton version of '^'.
(%^) :: Sing (b :: Integer) -> Sing (p :: Natural) -> Sing (b ^ p :: Integer)
Sing b
sb %^ :: forall (b :: Integer) (p :: Natural).
Sing b -> Sing p -> Sing (b ^ p)
%^ Sing p
sp = Integer -> SInteger (Pow (Normalized b) p)
forall (i :: Integer). Integer -> SInteger i
UnsafeSInteger (Sing b -> Demote Integer
forall k (a :: k). SingKind k => Sing a -> Demote k
forall (a :: Integer). Sing a -> Demote Integer
fromSing Sing b
sb Integer -> Demote Natural -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
^ Sing p -> Demote Natural
forall (a :: Natural). Sing a -> Demote Natural
forall k (a :: k). SingKind k => Sing a -> Demote k
fromSing Sing p
sp)
{-# INLINE (%^) #-}

-- | Exponentiation of type-level 'Integer's.
type (b :: Integer) ^ (p :: Natural) = Pow (Normalized b) p :: Integer

data (^@#@$) :: Integer ~> Natural ~> Integer
data (^@#@$$) :: Integer -> Natural ~> Integer
type (^@#@$$$) :: Integer -> Natural -> Integer

type instance Apply ((^@#@$$) b) p = (^@#@$$$) b p
type instance Apply (^@#@$) b = (^@#@$$) b
type (^@#@$$$) b p = b ^ p

type family Pow (b :: Integer) (p :: Natural) :: Integer where
  Pow _ 0 = P 1
  Pow Z _ = Z
  Pow (P b) p = FromNatural (b L.^ p)
  Pow (N b) p = FromNatural (b L.^ p) P.* If (Even (P p)) (P 1) (N 1)

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

infixl 7 `Div`, `Rem`, `DivRem`

-- | 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)

data DivRemSym0 :: Round ~> Integer ~> Integer ~> (Integer, Integer)
data DivRemSym1 :: Round -> Integer ~> Integer ~> (Integer, Integer)
data DivRemSym2 :: Round -> Integer -> Integer ~> (Integer, Integer)
type DivRemSym3 :: Round -> Integer -> Integer -> (Integer, Integer)

type instance Apply DivRemSym0 r = DivRemSym1 r
type instance Apply (DivRemSym1 r) a = DivRemSym2 r a
type instance Apply (DivRemSym2 r a) b = DivRemSym3 r a b
type DivRemSym3 r a b = DivRem r a b

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

-- | '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) =
  Rem_ r (Normalized a) (Normalized b) :: Integer
type Rem_ (r :: Round) (a :: Integer) (b :: Integer) =
  a P.- b P.* Div r a b :: Integer

data RemSym0 :: Round ~> Integer ~> Integer ~> Integer
data RemSym1 :: Round -> Integer ~> Integer ~> Integer
data RemSym2 :: Round -> Integer -> Integer ~> Integer
type RemSym3 :: Round -> Integer -> Integer -> Integer

type instance Apply RemSym0 r = RemSym1 r
type instance Apply (RemSym1 r) a = RemSym2 r a
type instance Apply (RemSym2 r a) b = RemSym3 r a b
type RemSym3 r a b = Rem r a b

-- | Demoted version of 'Rem'.
--
-- Throws 'Ex.DivdeByZero' where 'Div' would fail to type-check.
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)

-- | Singleton version of 'Rem'.
sRem :: SRound r
     -> SInteger a  -- ^ Dividend.
     -> SInteger b  -- ^ Divisor.
     -> SInteger (Rem r a b)
sRem :: forall (r :: Round) (a :: Integer) (b :: Integer).
SRound r -> SInteger a -> SInteger b -> SInteger (Rem r a b)
sRem SRound r
sr SInteger a
sa SInteger b
sb = (SInteger (Div_ r (Normalized a) (Normalized b)),
 SInteger
   (Add_
      (CmpInteger_
         (Fold 'EQ (ConstSym1 'LT) (ConstSym1 'GT) (Normalized a))
         'EQ
         (Fold 0 IdSym0 IdSym0 (Normalized a))
         0)
      (CmpInteger_
         (Fold
            'EQ
            (ConstSym1 'LT)
            (ConstSym1 'GT)
            (Fold
               Z
               PSym0
               NSym0
               (Mul_
                  (CmpInteger_
                     (Fold 'EQ (ConstSym1 'LT) (ConstSym1 'GT) (Normalized b))
                     'EQ
                     (Fold 0 IdSym0 IdSym0 (Normalized b))
                     0)
                  (CmpInteger_
                     (Fold
                        'EQ
                        (ConstSym1 'LT)
                        (ConstSym1 'GT)
                        (Div r (Normalized a) (Normalized b)))
                     'EQ
                     (Fold 0 IdSym0 IdSym0 (Div r (Normalized a) (Normalized b)))
                     0)
                  (Fold 0 IdSym0 IdSym0 (Normalized b))
                  (Fold 0 IdSym0 IdSym0 (Div r (Normalized a) (Normalized b))))))
         'EQ
         (Fold
            0
            IdSym0
            IdSym0
            (Fold
               Z
               PSym0
               NSym0
               (Mul_
                  (CmpInteger_
                     (Fold 'EQ (ConstSym1 'LT) (ConstSym1 'GT) (Normalized b))
                     'EQ
                     (Fold 0 IdSym0 IdSym0 (Normalized b))
                     0)
                  (CmpInteger_
                     (Fold
                        'EQ
                        (ConstSym1 'LT)
                        (ConstSym1 'GT)
                        (Div r (Normalized a) (Normalized b)))
                     'EQ
                     (Fold 0 IdSym0 IdSym0 (Div r (Normalized a) (Normalized b)))
                     0)
                  (Fold 0 IdSym0 IdSym0 (Normalized b))
                  (Fold 0 IdSym0 IdSym0 (Div r (Normalized a) (Normalized b))))))
         0)
      (Fold 0 IdSym0 IdSym0 (Normalized a))
      (Fold
         0
         IdSym0
         IdSym0
         (Fold
            Z
            PSym0
            NSym0
            (Mul_
               (CmpInteger_
                  (Fold 'EQ (ConstSym1 'LT) (ConstSym1 'GT) (Normalized b))
                  'EQ
                  (Fold 0 IdSym0 IdSym0 (Normalized b))
                  0)
               (CmpInteger_
                  (Fold
                     'EQ
                     (ConstSym1 'LT)
                     (ConstSym1 'GT)
                     (Div r (Normalized a) (Normalized b)))
                  'EQ
                  (Fold 0 IdSym0 IdSym0 (Div r (Normalized a) (Normalized b)))
                  0)
               (Fold 0 IdSym0 IdSym0 (Normalized b))
               (Fold 0 IdSym0 IdSym0 (Div r (Normalized a) (Normalized b))))))))
-> SInteger
     (Add_
        (CmpInteger_
           (Fold 'EQ (ConstSym1 'LT) (ConstSym1 'GT) (Normalized a))
           'EQ
           (Fold 0 IdSym0 IdSym0 (Normalized a))
           0)
        (CmpInteger_
           (Fold
              'EQ
              (ConstSym1 'LT)
              (ConstSym1 'GT)
              (Fold
                 Z
                 PSym0
                 NSym0
                 (Mul_
                    (CmpInteger_
                       (Fold 'EQ (ConstSym1 'LT) (ConstSym1 'GT) (Normalized b))
                       'EQ
                       (Fold 0 IdSym0 IdSym0 (Normalized b))
                       0)
                    (CmpInteger_
                       (Fold
                          'EQ
                          (ConstSym1 'LT)
                          (ConstSym1 'GT)
                          (Div r (Normalized a) (Normalized b)))
                       'EQ
                       (Fold 0 IdSym0 IdSym0 (Div r (Normalized a) (Normalized b)))
                       0)
                    (Fold 0 IdSym0 IdSym0 (Normalized b))
                    (Fold 0 IdSym0 IdSym0 (Div r (Normalized a) (Normalized b))))))
           'EQ
           (Fold
              0
              IdSym0
              IdSym0
              (Fold
                 Z
                 PSym0
                 NSym0
                 (Mul_
                    (CmpInteger_
                       (Fold 'EQ (ConstSym1 'LT) (ConstSym1 'GT) (Normalized b))
                       'EQ
                       (Fold 0 IdSym0 IdSym0 (Normalized b))
                       0)
                    (CmpInteger_
                       (Fold
                          'EQ
                          (ConstSym1 'LT)
                          (ConstSym1 'GT)
                          (Div r (Normalized a) (Normalized b)))
                       'EQ
                       (Fold 0 IdSym0 IdSym0 (Div r (Normalized a) (Normalized b)))
                       0)
                    (Fold 0 IdSym0 IdSym0 (Normalized b))
                    (Fold 0 IdSym0 IdSym0 (Div r (Normalized a) (Normalized b))))))
           0)
        (Fold 0 IdSym0 IdSym0 (Normalized a))
        (Fold
           0
           IdSym0
           IdSym0
           (Fold
              Z
              PSym0
              NSym0
              (Mul_
                 (CmpInteger_
                    (Fold 'EQ (ConstSym1 'LT) (ConstSym1 'GT) (Normalized b))
                    'EQ
                    (Fold 0 IdSym0 IdSym0 (Normalized b))
                    0)
                 (CmpInteger_
                    (Fold
                       'EQ
                       (ConstSym1 'LT)
                       (ConstSym1 'GT)
                       (Div r (Normalized a) (Normalized b)))
                    'EQ
                    (Fold 0 IdSym0 IdSym0 (Div r (Normalized a) (Normalized b)))
                    0)
                 (Fold 0 IdSym0 IdSym0 (Normalized b))
                 (Fold 0 IdSym0 IdSym0 (Div r (Normalized a) (Normalized b)))))))
forall a b. (a, b) -> b
snd (SRound r
-> SInteger a
-> SInteger b
-> (SInteger (Div_ r (Normalized a) (Normalized b)),
    SInteger
      (Normalized a
       - (Normalized b * Div r (Normalized a) (Normalized b))))
forall (r :: Round) (a :: Integer) (b :: Integer).
SRound r
-> SInteger a
-> SInteger b
-> (SInteger (Div r a b), SInteger (Rem r a b))
sDivRem SRound r
sr SInteger a
sa SInteger b
sb)

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

-- | Divide the 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 (Normalized a) (Normalized b) :: Integer
type family Div_ (r :: Round) (a :: Integer) (b :: Integer) :: Integer where
  Div_ r  Z     Z    = Div__ r Z 0
  Div_ r  Z    (P b) = Div__ r Z b
  Div_ r  Z    (N b) = Div__ r Z b
  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

data DivSym0 :: Round ~> Integer ~> Integer ~> Integer
data DivSym1 :: Round -> Integer ~> Integer ~> Integer
data DivSym2 :: Round -> Integer -> Integer ~> Integer
type DivSym3 :: Round -> Integer -> Integer -> Integer

type instance Apply DivSym0 r = DivSym1 r
type instance Apply (DivSym1 r) a = DivSym2 r a
type instance Apply (DivSym2 r a) b = DivSym3 r a b
type DivSym3 r a b = Div r a b

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

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

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

  Div__ 'RoundZero (P a) b = Div__ 'RoundDown (P a) b
  Div__ 'RoundZero (N a) b = P.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

-- | Demoted version of 'Div'.
--
-- Throws 'Ex.DivdeByZero' where 'Div' would fail to type-check.
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)

-- | Singleton version of 'Div'.
sDiv :: SRound r
     -> SInteger a  -- ^ Dividend.
     -> SInteger b  -- ^ Divisor.
     -> SInteger (Div r a b)
sDiv :: forall (r :: Round) (a :: Integer) (b :: Integer).
SRound r -> SInteger a -> SInteger b -> SInteger (Div r a b)
sDiv SRound r
sr SInteger a
sa SInteger b
sb = (SInteger (Div_ r (Normalized a) (Normalized b)),
 SInteger
   (Add_
      (CmpInteger_
         (Fold 'EQ (ConstSym1 'LT) (ConstSym1 'GT) (Normalized a))
         'EQ
         (Fold 0 IdSym0 IdSym0 (Normalized a))
         0)
      (CmpInteger_
         (Fold
            'EQ
            (ConstSym1 'LT)
            (ConstSym1 'GT)
            (Fold
               Z
               PSym0
               NSym0
               (Mul_
                  (CmpInteger_
                     (Fold 'EQ (ConstSym1 'LT) (ConstSym1 'GT) (Normalized b))
                     'EQ
                     (Fold 0 IdSym0 IdSym0 (Normalized b))
                     0)
                  (CmpInteger_
                     (Fold
                        'EQ
                        (ConstSym1 'LT)
                        (ConstSym1 'GT)
                        (Div_ r (Normalized (Normalized a)) (Normalized (Normalized b))))
                     'EQ
                     (Fold
                        0
                        IdSym0
                        IdSym0
                        (Div_ r (Normalized (Normalized a)) (Normalized (Normalized b))))
                     0)
                  (Fold 0 IdSym0 IdSym0 (Normalized b))
                  (Fold
                     0
                     IdSym0
                     IdSym0
                     (Div_
                        r (Normalized (Normalized a)) (Normalized (Normalized b)))))))
         'EQ
         (Fold
            0
            IdSym0
            IdSym0
            (Fold
               Z
               PSym0
               NSym0
               (Mul_
                  (CmpInteger_
                     (Fold 'EQ (ConstSym1 'LT) (ConstSym1 'GT) (Normalized b))
                     'EQ
                     (Fold 0 IdSym0 IdSym0 (Normalized b))
                     0)
                  (CmpInteger_
                     (Fold
                        'EQ
                        (ConstSym1 'LT)
                        (ConstSym1 'GT)
                        (Div_ r (Normalized (Normalized a)) (Normalized (Normalized b))))
                     'EQ
                     (Fold
                        0
                        IdSym0
                        IdSym0
                        (Div_ r (Normalized (Normalized a)) (Normalized (Normalized b))))
                     0)
                  (Fold 0 IdSym0 IdSym0 (Normalized b))
                  (Fold
                     0
                     IdSym0
                     IdSym0
                     (Div_
                        r (Normalized (Normalized a)) (Normalized (Normalized b)))))))
         0)
      (Fold 0 IdSym0 IdSym0 (Normalized a))
      (Fold
         0
         IdSym0
         IdSym0
         (Fold
            Z
            PSym0
            NSym0
            (Mul_
               (CmpInteger_
                  (Fold 'EQ (ConstSym1 'LT) (ConstSym1 'GT) (Normalized b))
                  'EQ
                  (Fold 0 IdSym0 IdSym0 (Normalized b))
                  0)
               (CmpInteger_
                  (Fold
                     'EQ
                     (ConstSym1 'LT)
                     (ConstSym1 'GT)
                     (Div_ r (Normalized (Normalized a)) (Normalized (Normalized b))))
                  'EQ
                  (Fold
                     0
                     IdSym0
                     IdSym0
                     (Div_ r (Normalized (Normalized a)) (Normalized (Normalized b))))
                  0)
               (Fold 0 IdSym0 IdSym0 (Normalized b))
               (Fold
                  0
                  IdSym0
                  IdSym0
                  (Div_
                     r (Normalized (Normalized a)) (Normalized (Normalized b)))))))))
-> SInteger (Div_ r (Normalized a) (Normalized b))
forall a b. (a, b) -> a
fst (SRound r
-> SInteger a
-> SInteger b
-> (SInteger (Div_ r (Normalized a) (Normalized b)),
    SInteger (Rem r a b))
forall (r :: Round) (a :: Integer) (b :: Integer).
SRound r
-> SInteger a
-> SInteger b
-> (SInteger (Div r a b), SInteger (Rem r a b))
sDivRem SRound r
sr SInteger a
sa SInteger b
sb)

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

-- | Singleton version of 'Log2'.
sLog2 :: SInteger i -> Sing (Log2 i :: Natural)
sLog2 :: forall (i :: Integer). SInteger i -> Sing (Log2 i)
sLog2 SInteger i
si = Demote Natural
-> (forall (a :: Natural).
    Sing a
    -> SNat
         (Fold (TypeError ...) (ConstSym1 (TypeError ...)) Log2Sym0 i))
-> SNat
     (Fold (TypeError ...) (ConstSym1 (TypeError ...)) Log2Sym0 i)
forall k r.
SingKind k =>
Demote k -> (forall (a :: k). Sing a -> r) -> r
withSomeSing
             (Word -> Natural
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Integer -> Word
integerLog2 (Sing i -> Demote Integer
forall k (a :: k). SingKind k => Sing a -> Demote k
forall (a :: Integer). Sing a -> Demote Integer
fromSing Sing i
SInteger i
si)) :: Natural)
             SNat a
-> SNat
     (Fold (TypeError ...) (ConstSym1 (TypeError ...)) Log2Sym0 i)
Sing a
-> SNat
     (Fold (TypeError ...) (ConstSym1 (TypeError ...)) Log2Sym0 i)
forall (a :: Natural).
Sing a
-> SNat
     (Fold (TypeError ...) (ConstSym1 (TypeError ...)) Log2Sym0 i)
forall a b. a -> b
unsafeCoerce


-- | 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) =
  Fold (L.TypeError ('L.Text "Logarithm of zero."))
       (P.ConstSym1 (L.TypeError ('L.Text "Logarithm of negative number.")))
       (L.Log2Sym0)
       a
    :: Natural

data Log2Sym0 :: Integer ~> Natural
type Log2Sym1 :: Integer -> Natural

type instance Apply Log2Sym0 a = Log2Sym1 a
type Log2Sym1 a = Log2 a

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

-- | Singleton version of 'GCD'.
sGCD :: SInteger a -> SInteger b -> Sing (GCD a b :: Natural)
sGCD :: forall (a :: Integer) (b :: Integer).
SInteger a -> SInteger b -> Sing (GCD a b)
sGCD SInteger a
sa SInteger b
sb = forall k r.
SingKind k =>
Demote k -> (forall (a :: k). Sing a -> r) -> r
withSomeSing @Natural
               (Integer -> Natural
forall a. Num a => Integer -> a
fromInteger (Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
gcd (Sing a -> Demote Integer
forall k (a :: k). SingKind k => Sing a -> Demote k
forall (a :: Integer). Sing a -> Demote Integer
fromSing Sing a
SInteger a
sa) (Sing b -> Demote Integer
forall k (a :: k). SingKind k => Sing a -> Demote k
forall (a :: Integer). Sing a -> Demote Integer
fromSing Sing b
SInteger b
sb)))
               SNat a
-> SNat (NatGCD (Fold 0 IdSym0 IdSym0 a) (Fold 0 IdSym0 IdSym0 b))
Sing a
-> SNat (NatGCD (Fold 0 IdSym0 IdSym0 a) (Fold 0 IdSym0 IdSym0 b))
forall (a :: Natural).
Sing a
-> SNat (NatGCD (Fold 0 IdSym0 IdSym0 a) (Fold 0 IdSym0 IdSym0 b))
forall a b. a -> b
unsafeCoerce

-- | 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

data GCDSym0 :: Integer ~> Integer ~> Natural
data GCDSym1 :: Integer -> Integer ~> Natural
type GCDSym2 :: Integer -> Integer -> Natural

type instance Apply GCDSym0 a = GCDSym1 a
type instance Apply (GCDSym1 a) b = GCDSym2 a b
type GCDSym2 a b = GCD a b

-- | 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)

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

-- | Singleton version of 'LCM'.
sLCM :: SInteger a -> SInteger b -> Sing (LCM a b :: Natural)
sLCM :: forall (a :: Integer) (b :: Integer).
SInteger a -> SInteger b -> Sing (LCM a b)
sLCM SInteger a
sa SInteger b
sb = forall k r.
SingKind k =>
Demote k -> (forall (a :: k). Sing a -> r) -> r
withSomeSing @Natural
               (Integer -> Natural
forall a. Num a => Integer -> a
fromInteger (Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
lcm (Sing a -> Demote Integer
forall k (a :: k). SingKind k => Sing a -> Demote k
forall (a :: Integer). Sing a -> Demote Integer
fromSing Sing a
SInteger a
sa) (Sing b -> Demote Integer
forall k (a :: k). SingKind k => Sing a -> Demote k
forall (a :: Integer). Sing a -> Demote Integer
fromSing Sing b
SInteger b
sb)))
               SNat a
-> SNat
     (Div
        (Fold 0 IdSym0 IdSym0 a)
        (NatGCD (Fold 0 IdSym0 IdSym0 a) (Fold 0 IdSym0 IdSym0 b))
      * Fold 0 IdSym0 IdSym0 b)
Sing a
-> SNat
     (Div
        (Fold 0 IdSym0 IdSym0 a)
        (NatGCD (Fold 0 IdSym0 IdSym0 a) (Fold 0 IdSym0 IdSym0 b))
      * Fold 0 IdSym0 IdSym0 b)
forall (a :: Natural).
Sing a
-> SNat
     (Div
        (Fold 0 IdSym0 IdSym0 a)
        (NatGCD (Fold 0 IdSym0 IdSym0 a) (Fold 0 IdSym0 IdSym0 b))
      * Fold 0 IdSym0 IdSym0 b)
forall a b. a -> b
unsafeCoerce

-- | 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

data LCMSym0 :: Integer ~> Integer ~> Natural
data LCMSym1 :: Integer -> Integer ~> Natural
type LCMSym2 :: Integer -> Integer -> Natural

type instance Apply LCMSym0 a = LCMSym1 a
type instance Apply (LCMSym1 a) b = LCMSym2 a b
type LCMSym2 a b = LCM a b

-- | 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

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

type Add_ :: Ordering -> Ordering ->  Natural -> Natural -> Integer
type family Add_ lc rc la ra where
  Add_ 'EQ 'EQ _ _ = Z
  Add_ 'EQ 'LT _ r = N r
  Add_ 'EQ 'GT _ r = P r
  Add_ 'LT 'EQ l _ = N l
  Add_ 'GT 'EQ l _ = P l
  Add_ 'LT 'LT l r = N (l L.+ r)
  Add_ 'LT 'GT l r = OrdCond (Compare l r) (P (r P.- l)) Z (N (l P.- r))
  Add_ 'GT 'GT l r = P (l L.+ r)
  Add_ 'GT 'LT l r = OrdCond (Compare l r) (N (r P.- l)) Z (P (l P.- r))

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

type Mul_ :: Ordering -> Ordering ->  Natural -> Natural -> Integer
type family Mul_ lc rc la ra where
  Mul_ _   'EQ _ _ = Z
  Mul_ 'EQ _   _ _ = Z
  Mul_ x   x   l r = P (l L.* r)
  Mul_ _   _   l r = N (l L.* r)

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

instance P.PNum Integer where
  type l + r = Add_ (Compare l Z) (Compare r Z) (Abs l) (Abs r)
  type l - r = l P.+ P.Negate r
  type l * r = Mul_ (Compare l Z) (Compare r Z) (Abs l) (Abs r)
  type Negate i = Fold Z PSym0 NSym0 i
  type Abs i = FromNatural (Abs i)
  type Signum i = Fold Z (P.ConstSym1 (N 1)) (P.ConstSym1 (P 1)) i
  type FromInteger i = FromNatural i

instance P.SNum Integer where
  Sing t1
l %+ :: forall (t1 :: Integer) (t2 :: Integer).
Sing t1 -> Sing t2 -> Sing (Apply (Apply (+@#@$) t1) t2)
%+ Sing t2
r = Integer
-> SInteger
     (Add_
        (CmpInteger_
           (Fold 'EQ (ConstSym1 'LT) (ConstSym1 'GT) t1)
           'EQ
           (Fold 0 IdSym0 IdSym0 t1)
           0)
        (CmpInteger_
           (Fold 'EQ (ConstSym1 'LT) (ConstSym1 'GT) t2)
           'EQ
           (Fold 0 IdSym0 IdSym0 t2)
           0)
        (Fold 0 IdSym0 IdSym0 t1)
        (Fold 0 IdSym0 IdSym0 t2))
forall (i :: Integer). Integer -> SInteger i
UnsafeSInteger (Sing t1 -> Demote Integer
forall k (a :: k). SingKind k => Sing a -> Demote k
forall (a :: Integer). Sing a -> Demote Integer
fromSing Sing t1
l Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Sing t2 -> Demote Integer
forall k (a :: k). SingKind k => Sing a -> Demote k
forall (a :: Integer). Sing a -> Demote Integer
fromSing Sing t2
r)
  Sing t1
l %- :: forall (t1 :: Integer) (t2 :: Integer).
Sing t1 -> Sing t2 -> Sing (Apply (Apply (-@#@$) t1) t2)
%- Sing t2
r = Integer
-> SInteger
     (Add_
        (CmpInteger_
           (Fold 'EQ (ConstSym1 'LT) (ConstSym1 'GT) t1)
           'EQ
           (Fold 0 IdSym0 IdSym0 t1)
           0)
        (CmpInteger_
           (Fold 'EQ (ConstSym1 'LT) (ConstSym1 'GT) (Fold Z PSym0 NSym0 t2))
           'EQ
           (Fold 0 IdSym0 IdSym0 (Fold Z PSym0 NSym0 t2))
           0)
        (Fold 0 IdSym0 IdSym0 t1)
        (Fold 0 IdSym0 IdSym0 (Fold Z PSym0 NSym0 t2)))
forall (i :: Integer). Integer -> SInteger i
UnsafeSInteger (Sing t1 -> Demote Integer
forall k (a :: k). SingKind k => Sing a -> Demote k
forall (a :: Integer). Sing a -> Demote Integer
fromSing Sing t1
l Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Sing t2 -> Demote Integer
forall k (a :: k). SingKind k => Sing a -> Demote k
forall (a :: Integer). Sing a -> Demote Integer
fromSing Sing t2
r)
  Sing t1
l %* :: forall (t1 :: Integer) (t2 :: Integer).
Sing t1 -> Sing t2 -> Sing (Apply (Apply (*@#@$) t1) t2)
%* Sing t2
r = Integer
-> SInteger
     (Mul_
        (CmpInteger_
           (Fold 'EQ (ConstSym1 'LT) (ConstSym1 'GT) t1)
           'EQ
           (Fold 0 IdSym0 IdSym0 t1)
           0)
        (CmpInteger_
           (Fold 'EQ (ConstSym1 'LT) (ConstSym1 'GT) t2)
           'EQ
           (Fold 0 IdSym0 IdSym0 t2)
           0)
        (Fold 0 IdSym0 IdSym0 t1)
        (Fold 0 IdSym0 IdSym0 t2))
forall (i :: Integer). Integer -> SInteger i
UnsafeSInteger (Sing t1 -> Demote Integer
forall k (a :: k). SingKind k => Sing a -> Demote k
forall (a :: Integer). Sing a -> Demote Integer
fromSing Sing t1
l Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Sing t2 -> Demote Integer
forall k (a :: k). SingKind k => Sing a -> Demote k
forall (a :: Integer). Sing a -> Demote Integer
fromSing Sing t2
r)
  sNegate :: forall (t :: Integer). Sing t -> Sing (Apply NegateSym0 t)
sNegate = Integer -> SInteger (Fold Z PSym0 NSym0 t)
forall (i :: Integer). Integer -> SInteger i
UnsafeSInteger (Integer -> SInteger (Fold Z PSym0 NSym0 t))
-> (SInteger t -> Integer)
-> SInteger t
-> SInteger (Fold Z PSym0 NSym0 t)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> Integer
forall a. Num a => a -> a
negate (Integer -> Integer)
-> (SInteger t -> Integer) -> SInteger t -> Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sing t -> Demote Integer
SInteger t -> Integer
forall k (a :: k). SingKind k => Sing a -> Demote k
forall (a :: Integer). Sing a -> Demote Integer
fromSing
  sAbs :: forall (t :: Integer). Sing t -> Sing (Apply AbsSym0 t)
sAbs = SNat (Fold 0 IdSym0 IdSym0 t)
-> SInteger (FromNatural (Fold 0 IdSym0 IdSym0 t))
Sing (Fold 0 IdSym0 IdSym0 t)
-> SInteger (FromNatural (Fold 0 IdSym0 IdSym0 t))
forall (x :: Natural). Sing x -> SInteger (FromNatural x)
sFromNatural (SNat (Fold 0 IdSym0 IdSym0 t)
 -> SInteger (FromNatural (Fold 0 IdSym0 IdSym0 t)))
-> (SInteger t -> SNat (Fold 0 IdSym0 IdSym0 t))
-> SInteger t
-> SInteger (FromNatural (Fold 0 IdSym0 IdSym0 t))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SInteger t -> SNat (Fold 0 IdSym0 IdSym0 t)
SInteger t -> Sing (Fold 0 IdSym0 IdSym0 t)
forall (i :: Integer). SInteger i -> Sing (Abs i)
sAbs
  sSignum :: forall (t :: Integer). Sing t -> Sing (Apply SignumSym0 t)
sSignum = Integer -> SInteger (Fold Z (ConstSym1 (N 1)) (ConstSym1 (P 1)) t)
forall (i :: Integer). Integer -> SInteger i
UnsafeSInteger (Integer
 -> SInteger (Fold Z (ConstSym1 (N 1)) (ConstSym1 (P 1)) t))
-> (SInteger t -> Integer)
-> SInteger t
-> SInteger (Fold Z (ConstSym1 (N 1)) (ConstSym1 (P 1)) t)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> Integer
forall a. Num a => a -> a
signum (Integer -> Integer)
-> (SInteger t -> Integer) -> SInteger t -> Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sing t -> Demote Integer
SInteger t -> Integer
forall k (a :: k). SingKind k => Sing a -> Demote k
forall (a :: Integer). Sing a -> Demote Integer
fromSing
  sFromInteger :: forall (t :: Natural). Sing t -> Sing (Apply FromIntegerSym0 t)
sFromInteger = Sing t -> Sing (Apply FromIntegerSym0 t)
Sing t -> SInteger (FromNatural t)
forall (x :: Natural). Sing x -> SInteger (FromNatural x)
sFromNatural

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

type instance Compare (l :: Integer) (r :: Integer) =
  CmpInteger_ (Fold 'EQ (P.ConstSym1 'LT) (P.ConstSym1 'GT) l)
              (Fold 'EQ (P.ConstSym1 'LT) (P.ConstSym1 'GT) r)
              (Abs l)
              (Abs r)

type CmpInteger_ :: Ordering -> Ordering -> Natural -> Natural -> Ordering
type family CmpInteger_ lc rc la ra where
  CmpInteger_ 'LT 'LT l r = Compare r l
  CmpInteger_ 'LT 'EQ _ _ = 'LT
  CmpInteger_ 'LT 'GT _ _ = 'LT
  CmpInteger_ 'EQ 'LT _ _ = 'GT
  CmpInteger_ 'EQ 'EQ _ _ = 'EQ
  CmpInteger_ 'EQ 'GT _ _ = 'LT
  CmpInteger_ 'GT 'LT _ _ = 'GT
  CmpInteger_ 'GT 'EQ _ _ = 'GT
  CmpInteger_ 'GT 'GT l r = Compare l r

instance OrdS.POrd Integer where
  type Compare l r = Data.Type.Ord.Compare l r

instance OrdS.SOrd Integer where
  sCompare :: forall (t1 :: Integer) (t2 :: Integer).
Sing t1 -> Sing t2 -> Sing (Apply (Apply CompareSym0 t1) t2)
sCompare Sing t1
sa Sing t2
sb =
    case Demote Integer -> Demote Integer -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (Sing t1 -> Demote Integer
forall k (a :: k). SingKind k => Sing a -> Demote k
forall (a :: Integer). Sing a -> Demote Integer
fromSing Sing t1
sa) (Sing t2 -> Demote Integer
forall k (a :: k). SingKind k => Sing a -> Demote k
forall (a :: Integer). Sing a -> Demote Integer
fromSing Sing t2
sb) of
      Ordering
LT -> SOrdering 'LT
-> SOrdering
     (CmpInteger_
        (Fold 'EQ (ConstSym1 'LT) (ConstSym1 'GT) t1)
        (Fold 'EQ (ConstSym1 'LT) (ConstSym1 'GT) t2)
        (Fold 0 IdSym0 IdSym0 t1)
        (Fold 0 IdSym0 IdSym0 t2))
forall a b. a -> b
unsafeCoerce SOrdering 'LT
OrdS.SLT
      Ordering
EQ -> SOrdering 'EQ
-> SOrdering
     (CmpInteger_
        (Fold 'EQ (ConstSym1 'LT) (ConstSym1 'GT) t1)
        (Fold 'EQ (ConstSym1 'LT) (ConstSym1 'GT) t2)
        (Fold 0 IdSym0 IdSym0 t1)
        (Fold 0 IdSym0 IdSym0 t2))
forall a b. a -> b
unsafeCoerce SOrdering 'EQ
OrdS.SEQ
      Ordering
GT -> SOrdering 'GT
-> SOrdering
     (CmpInteger_
        (Fold 'EQ (ConstSym1 'LT) (ConstSym1 'GT) t1)
        (Fold 'EQ (ConstSym1 'LT) (ConstSym1 'GT) t2)
        (Fold 0 IdSym0 IdSym0 t1)
        (Fold 0 IdSym0 IdSym0 t2))
forall a b. a -> b
unsafeCoerce SOrdering 'GT
OrdS.SGT

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

instance EqS.PEq Integer where
  type a == b = OrdCond (Compare a b) 'False 'True 'False

instance EqS.SEq Integer where
  Sing t1
sa %== :: forall (t1 :: Integer) (t2 :: Integer).
Sing t1 -> Sing t2 -> Sing (Apply (Apply (==@#@$) t1) t2)
%== Sing t2
sb = case Sing t1 -> Demote Integer
forall k (a :: k). SingKind k => Sing a -> Demote k
forall (a :: Integer). Sing a -> Demote Integer
fromSing Sing t1
sa Demote Integer -> Demote Integer -> Bool
forall a. Eq a => a -> a -> Bool
P.== Sing t2 -> Demote Integer
forall k (a :: k). SingKind k => Sing a -> Demote k
forall (a :: Integer). Sing a -> Demote Integer
fromSing Sing t2
sb of
    Bool
True  -> SBool 'True
-> SBool
     (OrdCond
        (CmpInteger_
           (Fold 'EQ (ConstSym1 'LT) (ConstSym1 'GT) t1)
           (Fold 'EQ (ConstSym1 'LT) (ConstSym1 'GT) t2)
           (Fold 0 IdSym0 IdSym0 t1)
           (Fold 0 IdSym0 IdSym0 t2))
        'False
        'True
        'False)
forall a b. a -> b
unsafeCoerce SBool 'True
STrue
    Bool
False -> SBool 'False
-> SBool
     (OrdCond
        (CmpInteger_
           (Fold 'EQ (ConstSym1 'LT) (ConstSym1 'GT) t1)
           (Fold 'EQ (ConstSym1 'LT) (ConstSym1 'GT) t2)
           (Fold 0 IdSym0 IdSym0 t1)
           (Fold 0 IdSym0 IdSym0 t2))
        'False
        'True
        'False)
forall a b. a -> b
unsafeCoerce SBool 'False
SFalse

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

-- | 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 {k} (a :: k). SingI a => Sing a
forall (a :: Integer). SingI a => Sing a
sing @a) (forall {k} (a :: k). SingI a => Sing a
forall (a :: Integer). SingI a => Sing a
sing @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
_ proxy2 b
_ = case Integer -> Integer -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (forall {k} (a :: k). (SingKind k, SingI a) => Demote k
forall (a :: Integer).
(SingKind Integer, SingI a) =>
Demote Integer
demote @a) (forall {k} (a :: k). (SingKind k, SingI a) => Demote k
forall (a :: Integer).
(SingKind Integer, SingI a) =>
Demote Integer
demote @b) of
  Ordering
EQ | a :~: b
Refl <- ((Any :~: Any) -> a :~: b
forall a b. a -> b
unsafeCoerce Any :~: Any
forall {k} (a :: k). a :~: a
Refl :: a :~: b)
     , Compare a b :~: 'EQ
Refl <- ((Any :~: Any)
-> CmpInteger_
     (Fold 'EQ (ConstSym1 'LT) (ConstSym1 'GT) a)
     (Fold 'EQ (ConstSym1 'LT) (ConstSym1 'GT) a)
     (Fold 0 IdSym0 IdSym0 a)
     (Fold 0 IdSym0 IdSym0 a)
   :~: 'EQ
forall a b. a -> b
unsafeCoerce Any :~: Any
forall {k} (a :: k). a :~: a
Refl :: Compare a b :~: 'EQ) -> OrderingI a a
OrderingI a b
forall {k} (a :: k). (Compare a a ~ 'EQ) => OrderingI a a
EQI
  Ordering
LT | Compare a b :~: 'LT
Refl <- ((Any :~: Any)
-> CmpInteger_
     (Fold 'EQ (ConstSym1 'LT) (ConstSym1 'GT) a)
     (Fold 'EQ (ConstSym1 'LT) (ConstSym1 'GT) b)
     (Fold 0 IdSym0 IdSym0 a)
     (Fold 0 IdSym0 IdSym0 b)
   :~: 'LT
forall a b. a -> b
unsafeCoerce Any :~: Any
forall {k} (a :: k). a :~: a
Refl :: Compare a b :~: 'LT) -> OrderingI a b
forall {k} (a :: k) (b :: k). (Compare a b ~ 'LT) => OrderingI a b
LTI
  Ordering
GT | Compare a b :~: 'GT
Refl <- ((Any :~: Any)
-> CmpInteger_
     (Fold 'EQ (ConstSym1 'LT) (ConstSym1 'GT) a)
     (Fold 'EQ (ConstSym1 'LT) (ConstSym1 'GT) b)
     (Fold 0 IdSym0 IdSym0 a)
     (Fold 0 IdSym0 IdSym0 b)
   :~: 'GT
forall a b. a -> b
unsafeCoerce Any :~: Any
forall {k} (a :: k). a :~: a
Refl :: Compare a b :~: 'GT) -> 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
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 si\@'SInteger' = /... both (si :: 'SInteger' i) and ('KnownInteger' 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 <- (patternSInteger -> PatternSInteger)
  where SInteger = SInteger i
forall (i :: Integer). KnownInteger i => SInteger i
integerSing
{-# COMPLETE SInteger #-}

-- | Only used for defining the 'SInteger' pattern synonym.
data PatternSInteger (i :: Integer) where
  PatternSInteger :: KnownInteger i => PatternSInteger i

-- | Only used for defining the 'SInteger' pattern synonym.
patternSInteger :: SInteger i -> PatternSInteger i
patternSInteger :: forall (i :: Integer). SInteger i -> PatternSInteger i
patternSInteger SInteger i
si = SInteger i
-> (KnownInteger i => PatternSInteger i) -> PatternSInteger i
forall (i :: Integer) x. SInteger i -> (KnownInteger i => x) -> x
withKnownInteger SInteger i
si PatternSInteger i
KnownInteger i => PatternSInteger i
forall (i :: Integer). KnownInteger i => PatternSInteger i
PatternSInteger

instance Eq (SInteger i) where
  SInteger i
_ == :: SInteger i -> SInteger i -> Bool
== SInteger i
_ = Bool
True

instance Ord (SInteger i) where
  compare :: SInteger i -> SInteger i -> Ordering
compare SInteger i
_ SInteger i
_ = Ordering
P.EQ

instance P.Show (SInteger i) where
  showsPrec :: Int -> SInteger i -> ShowS
showsPrec Int
p SInteger i
i =
    Bool -> ShowS -> ShowS
showParen (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
appPrec1) (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
showsPrecLit Int
appPrec1 (Sing i -> Demote Integer
forall k (a :: k). SingKind k => Sing a -> Demote k
forall (a :: Integer). Sing a -> Demote Integer
fromSing Sing i
SInteger i
i)

instance forall i. KnownInteger i => Read (SInteger i) where
  readPrec :: ReadPrec (SInteger i)
readPrec = ReadP (SInteger i) -> ReadPrec (SInteger i)
forall a. ReadP a -> ReadPrec a
ReadPrec.lift (ReadP (SInteger i) -> ReadPrec (SInteger i))
-> ReadP (SInteger i) -> ReadPrec (SInteger i)
forall a b. (a -> b) -> a -> b
$ do
    let si :: SInteger i
si = forall (i :: Integer). KnownInteger i => SInteger i
integerSing @i
    ()
_ <- String -> ReadP String
ReadP.string String
"SInteger" ReadP String -> ReadP () -> ReadP ()
forall a b. ReadP a -> ReadP b -> ReadP b
forall (m :: Type -> Type) a b. Monad m => m a -> m b -> m b
>> ReadP ()
pSkipSpaces1
    Char
_ <- Char -> ReadP Char
ReadP.char Char
'@'
    String
_ <- String -> ReadP String
ReadP.string (Int -> Integer -> ShowS
showsPrecLit Int
appPrec1 (Sing i -> Demote Integer
forall k (a :: k). SingKind k => Sing a -> Demote k
forall (a :: Integer). Sing a -> Demote Integer
fromSing Sing i
SInteger i
si) String
"")
    SInteger i -> ReadP (SInteger i)
forall a. a -> ReadP a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure SInteger i
si

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 #-}

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@.
fromSInteger :: SInteger i -> P.Integer
fromSInteger :: forall (i :: Integer). SInteger i -> Integer
fromSInteger = SInteger i -> Integer
forall a b. Coercible a b => a -> b
coerce
{-# INLINE fromSInteger #-}

withKnownInteger_
  :: forall i rep (x :: TYPE rep)
  .  SInteger i
  -> (KnownInteger_ i => x)
  -> x
withKnownInteger_ :: forall (i :: Integer) x. SInteger i -> (KnownInteger_ i => x) -> x
withKnownInteger_ = forall (cls :: Constraint) meth r.
WithDict cls meth =>
meth -> (cls => r) -> r
withDict @(KnownInteger_ i)

-- | Convert an explicit @'SInteger' i@ value into an implicit
-- @'KnownInteger' i@ constraint.
withKnownInteger
  :: forall i rep (x :: TYPE rep)
  .  SInteger i
  -> (KnownInteger i => x)
  -> x
withKnownInteger :: forall (i :: Integer) x. SInteger i -> (KnownInteger i => x) -> x
withKnownInteger SInteger i
si KnownInteger i => x
x
  | Sing (Fold 0 IdSym0 IdSym0 i)
sa :: Sing a <- SInteger i -> Sing (Fold 0 IdSym0 IdSym0 i)
forall (i :: Integer). SInteger i -> Sing (Abs i)
sAbs SInteger i
si
  , i :~: Normalized i
Refl <- SInteger i -> i :~: Normalized i
forall (i :: Integer). SInteger i -> i :~: Normalized i
sNormalizedRefl SInteger i
si
  = SNat (Fold 0 IdSym0 IdSym0 i)
-> (KnownNat (Fold 0 IdSym0 IdSym0 i) => x) -> x
forall (n :: Natural) r. SNat n -> (KnownNat n => r) -> r
L.withKnownNat SNat (Fold 0 IdSym0 IdSym0 i)
Sing (Fold 0 IdSym0 IdSym0 i)
sa (SInteger i -> (KnownInteger_ i => x) -> x
forall (i :: Integer) x. SInteger i -> (KnownInteger_ i => x) -> x
withKnownInteger_ SInteger i
si x
KnownInteger i => x
KnownInteger_ i => x
x)

-- | Convert a "Prelude".'P.Integer' number into an @'SInteger' n@ value,
-- where @n@ is a fresh type-level 'Integer'.
withSomeSInteger
  :: forall rep (x :: TYPE rep)
  .  P.Integer
  -> (forall (i :: Integer). Sing i -> x)
  -> x
withSomeSInteger :: forall x. Integer -> (forall (i :: Integer). Sing i -> x) -> x
withSomeSInteger Integer
i forall (i :: Integer). Sing i -> x
k = Sing Any -> x
forall (i :: Integer). Sing i -> x
k (Integer -> SInteger Any
forall (i :: Integer). Integer -> SInteger i
UnsafeSInteger Integer
i)
-- 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 :: Sing i
sing = Sing i
SInteger i
forall (i :: Integer). KnownInteger i => SInteger i
integerSing
  {-# INLINE sing #-}

instance SingKind Integer where
  type Demote Integer = P.Integer
  fromSing :: forall (a :: Integer). Sing a -> Demote Integer
fromSing = Sing a -> Demote Integer
SInteger a -> Integer
forall (i :: Integer). SInteger i -> Integer
fromSInteger
  {-# INLINE fromSing #-}
  toSing :: Demote Integer -> SomeSing Integer
toSing Demote Integer
i = Integer
-> (forall (i :: Integer). Sing i -> SomeSing Integer)
-> SomeSing Integer
forall x. Integer -> (forall (i :: Integer). Sing i -> x) -> x
withSomeSInteger Integer
Demote Integer
i Sing i -> SomeSing Integer
forall k (a :: k). Sing a -> SomeSing k
forall (i :: Integer). Sing i -> SomeSing Integer
SomeSing
  {-# INLINE toSing #-}

instance SDecide Integer where
  Sing a
l %~ :: forall (a :: Integer) (b :: Integer).
Sing a -> Sing b -> Decision (a :~: b)
%~ Sing b
r = case Sing a -> Demote Integer
forall k (a :: k). SingKind k => Sing a -> Demote k
forall (a :: Integer). Sing a -> Demote Integer
fromSing Sing a
l Demote Integer -> Demote Integer -> Bool
forall a. Eq a => a -> a -> Bool
P.== Sing b -> Demote Integer
forall k (a :: k). SingKind k => Sing a -> Demote k
forall (a :: Integer). Sing a -> Demote Integer
fromSing Sing b
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
"KindInteger.Integer: SDecide")

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

-- | Demoted version of 'DivRem'.
--
-- Throws 'Ex.DivdeByZero' where 'Div' would fail to type-check.
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 RoundUp -> 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 #-}

-- | Singleton version of 'DivRem'.
sDivRem :: SRound r
        -> SInteger a   -- ^ Dividend.
        -> SInteger b   -- ^ Divisor.
        -> (SInteger (Div r a b), SInteger (Rem r a b))
sDivRem :: forall (r :: Round) (a :: Integer) (b :: Integer).
SRound r
-> SInteger a
-> SInteger b
-> (SInteger (Div r a b), SInteger (Rem r a b))
sDivRem SRound r
sr SInteger a
sa SInteger b
sb =
  let (Integer
q, Integer
m) = Round -> Integer -> Integer -> (Integer, Integer)
divRem (Sing r -> Demote Round
forall k (a :: k). SingKind k => Sing a -> Demote k
forall (a :: Round). Sing a -> Demote Round
fromSing Sing r
SRound r
sr) (Sing a -> Demote Integer
forall k (a :: k). SingKind k => Sing a -> Demote k
forall (a :: Integer). Sing a -> Demote Integer
fromSing Sing a
SInteger a
sa) (Sing b -> Demote Integer
forall k (a :: k). SingKind k => Sing a -> Demote k
forall (a :: Integer). Sing a -> Demote Integer
fromSing Sing b
SInteger b
sb)
  in Demote Integer
-> (forall {a :: Integer}.
    Sing a -> (SInteger (Div r a b), SInteger (Rem r a b)))
-> (SInteger (Div r a b), SInteger (Rem r a b))
forall k r.
SingKind k =>
Demote k -> (forall (a :: k). Sing a -> r) -> r
withSomeSing Integer
Demote Integer
q ((forall {a :: Integer}.
  Sing a -> (SInteger (Div r a b), SInteger (Rem r a b)))
 -> (SInteger (Div r a b), SInteger (Rem r a b)))
-> (forall {a :: Integer}.
    Sing a -> (SInteger (Div r a b), SInteger (Rem r a b)))
-> (SInteger (Div r a b), SInteger (Rem r a b))
forall a b. (a -> b) -> a -> b
$ \Sing a
sq ->
     Integer
-> (forall {a :: Integer}.
    Sing a -> (SInteger (Div r a b), SInteger (Rem r a b)))
-> (SInteger (Div r a b), SInteger (Rem r a b))
forall x. Integer -> (forall (i :: Integer). Sing i -> x) -> x
withSomeSInteger Integer
m ((forall {a :: Integer}.
  Sing a -> (SInteger (Div r a b), SInteger (Rem r a b)))
 -> (SInteger (Div r a b), SInteger (Rem r a b)))
-> (forall {a :: Integer}.
    Sing a -> (SInteger (Div r a b), SInteger (Rem r a b)))
-> (SInteger (Div r a b), SInteger (Rem r a b))
forall a b. (a -> b) -> a -> b
$ \Sing i
sm ->
     (SInteger a -> SInteger (Div r a b)
forall a b. a -> b
unsafeCoerce Sing a
SInteger a
sq, SInteger i
-> SInteger
     (Add_
        (CmpInteger_
           (Fold 'EQ (ConstSym1 'LT) (ConstSym1 'GT) (Normalized a))
           'EQ
           (Fold 0 IdSym0 IdSym0 (Normalized a))
           0)
        (CmpInteger_
           (Fold
              'EQ
              (ConstSym1 'LT)
              (ConstSym1 'GT)
              (Fold
                 Z
                 PSym0
                 NSym0
                 (Mul_
                    (CmpInteger_
                       (Fold 'EQ (ConstSym1 'LT) (ConstSym1 'GT) (Normalized b))
                       'EQ
                       (Fold 0 IdSym0 IdSym0 (Normalized b))
                       0)
                    (CmpInteger_
                       (Fold
                          'EQ
                          (ConstSym1 'LT)
                          (ConstSym1 'GT)
                          (Div_ r (Normalized (Normalized a)) (Normalized (Normalized b))))
                       'EQ
                       (Fold
                          0
                          IdSym0
                          IdSym0
                          (Div_ r (Normalized (Normalized a)) (Normalized (Normalized b))))
                       0)
                    (Fold 0 IdSym0 IdSym0 (Normalized b))
                    (Fold
                       0
                       IdSym0
                       IdSym0
                       (Div_
                          r (Normalized (Normalized a)) (Normalized (Normalized b)))))))
           'EQ
           (Fold
              0
              IdSym0
              IdSym0
              (Fold
                 Z
                 PSym0
                 NSym0
                 (Mul_
                    (CmpInteger_
                       (Fold 'EQ (ConstSym1 'LT) (ConstSym1 'GT) (Normalized b))
                       'EQ
                       (Fold 0 IdSym0 IdSym0 (Normalized b))
                       0)
                    (CmpInteger_
                       (Fold
                          'EQ
                          (ConstSym1 'LT)
                          (ConstSym1 'GT)
                          (Div_ r (Normalized (Normalized a)) (Normalized (Normalized b))))
                       'EQ
                       (Fold
                          0
                          IdSym0
                          IdSym0
                          (Div_ r (Normalized (Normalized a)) (Normalized (Normalized b))))
                       0)
                    (Fold 0 IdSym0 IdSym0 (Normalized b))
                    (Fold
                       0
                       IdSym0
                       IdSym0
                       (Div_
                          r (Normalized (Normalized a)) (Normalized (Normalized b)))))))
           0)
        (Fold 0 IdSym0 IdSym0 (Normalized a))
        (Fold
           0
           IdSym0
           IdSym0
           (Fold
              Z
              PSym0
              NSym0
              (Mul_
                 (CmpInteger_
                    (Fold 'EQ (ConstSym1 'LT) (ConstSym1 'GT) (Normalized b))
                    'EQ
                    (Fold 0 IdSym0 IdSym0 (Normalized b))
                    0)
                 (CmpInteger_
                    (Fold
                       'EQ
                       (ConstSym1 'LT)
                       (ConstSym1 'GT)
                       (Div_ r (Normalized (Normalized a)) (Normalized (Normalized b))))
                    'EQ
                    (Fold
                       0
                       IdSym0
                       IdSym0
                       (Div_ r (Normalized (Normalized a)) (Normalized (Normalized b))))
                    0)
                 (Fold 0 IdSym0 IdSym0 (Normalized b))
                 (Fold
                    0
                    IdSym0
                    IdSym0
                    (Div_
                       r (Normalized (Normalized a)) (Normalized (Normalized b))))))))
forall a b. a -> b
unsafeCoerce Sing i
SInteger i
sm)

--------------------------------------------------------------------------------
-- Rational tools necessary to support 'HalfLT'

data Rat = MkRat Integer Natural
  -- ^ Invariant: 'Natural' is never 0. This is enforced by the 'R' type-family.

type R :: Integer -> Natural -> Rat
type family R n d where
  R _ 0 = L.TypeError ('L.Text "Denominator is 0.")
  R n d = Fold ('MkRat Z 1) (RAuxSym2 NSym0 d) (RAuxSym2 PSym0 d) n

data RAuxSym2 :: (Natural ~> Integer) -> Natural -> Natural ~> Rat
type instance Apply (RAuxSym2 fn d) n = 'MkRat (fn @@ n) d

type RatReduce :: Rat -> Rat
type family RatReduce r where
  RatReduce ('MkRat n d) = 'MkRat
    (P.Signum n P.* FromNatural (L.Div (Abs n) (NatGCD (Abs n) d)))
    (L.Div d (NatGCD (Abs n) d))

type RatAbs :: Rat -> Rat
type family RatAbs r where
  RatAbs ('MkRat n d) = R (P.Abs n) d

type RatAdd :: Rat -> Rat -> Rat
type family RatAdd l r where
  RatAdd ('MkRat ln ld) ('MkRat rn rd) =
    RatReduce (R (ln P.* P rd P.+ rn P.* P ld) (ld P.* rd))

type RatNegate :: Rat -> Rat
type family RatNegate r where
  RatNegate ('MkRat n d) = R (P.Negate n) d

type RatMinus :: Rat -> Rat -> Rat
type RatMinus l r = RatAdd l (RatNegate r)

type RatCmp :: Rat -> Rat -> Ordering
type RatCmp l r = RatCmp_ (RatReduce l) (RatReduce r)
type family RatCmp_ (a :: Rat) (b :: Rat) :: Ordering where
  RatCmp_ a a = 'EQ
  RatCmp_ ('MkRat an ad) ('MkRat bn bd) = Compare (an P.* P bd) (bn P.* P ad)

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

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

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

pSkipSpaces1 :: ReadP.ReadP ()
pSkipSpaces1 :: ReadP ()
pSkipSpaces1 = ReadP String -> ReadP ()
forall (f :: Type -> Type) a. Functor f => f a -> f ()
void (ReadP String -> ReadP ()) -> ReadP String -> ReadP ()
forall a b. (a -> b) -> a -> b
$ (Char -> Bool) -> ReadP String
ReadP.munch1 Char -> Bool
Char.isSpace