{-# LANGUAGE StrictData #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE UndecidableSuperClasses #-}

-- | This module provides a type-level representation for term-level
-- 'P.Rational's. This type-level representation is also named 'P.Rational',
-- So import this module qualified to avoid name conflicts.
--
-- @
-- import "KindRational" qualified as KR
-- @
--
-- 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 KindRational {--}
  ( -- * Rational
    Rational
  , type (:%)
  , FromNatural, fromNatural, sFromNatural
  , FromInteger, fromInteger, sFromInteger
  , Num, sNum
  , Den, sDen
  , ToRational(..)
  , sMkRational
  , (%%)
  , (%)

    -- * SRational
  , KnownRational
  , Reduced
  , rationalSing
  , rationalVal
  , withKnownRational
  , SomeRational(..)
  , someRationalVal
  , SRational
  , pattern SRational
  , fromSRational
  , withSomeSRational

    -- * Proofs
  , sNegateRefl

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

    -- * Arithmethic
  , Signum, sSignum, sSignumRefl
  , Recip, sRecip, sRecip'
  , Div, sDiv, div
  , Rem, rem, sRem
  , DivRem, divRem, sDivRem
  , I.Round(..), I.SRound(..)

    -- * Decimals
  , IsTerminating
  , isTerminating
  , termination
  , Terminating
  , NonTerminating
  , pattern SRationalTerminating
  , pattern SRationalNonTerminating

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


    -- * Defunctionalization
  , type (%@#@$), type (%@#@$$), type (%@#@$$$)
  , type (:%@#@$), type (:%@#@$$), type (:%@#@$$$)
  , FromNaturalSym0, FromNaturalSym1
  , FromIntegerSym0, FromIntegerSym1
  , NumSym0, NumSym1
  , DenSym0, DenSym1
  , ToRationalSym0, ToRationalSym1, ToRationalSym2
  , ReducedSym0, ReducedSym1
  , ShowLitSym0, ShowLitSym1
  , ShowsLitSym0, ShowsLitSym1, ShowsLitSym2
  , ShowsPrecLitSym0, ShowsPrecLitSym1, ShowsPrecLitSym2, ShowsPrecLitSym3
  , IsTerminatingSym0, IsTerminatingSym1
  , TerminatingSym0, TerminatingSym1
  , NonTerminatingSym0, NonTerminatingSym1
  , SignumSym0, SignumSym1
  , RecipSym0, RecipSym1
  , DivSym0, DivSym1, DivSym2
  , RemSym0, RemSym1, RemSym2
  , DivRemSym0, DivRemSym1, DivRemSym2
  , I.RoundUpSym0
  , I.RoundDownSym0
  , I.RoundZeroSym0
  , I.RoundAwaySym0
  , I.RoundHalfUpSym0
  , I.RoundHalfDownSym0
  , I.RoundHalfZeroSym0
  , I.RoundHalfAwaySym0
  , I.RoundHalfEvenSym0
  , I.RoundHalfOddSym0
  ) --}
  where

import Control.Monad
import Data.Bits
import Data.Bool.Singletons (SBool(..))
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.Coercion
import Data.Type.Equality (TestEquality(..))
import Data.Type.Ord
import GHC.Base (WithDict(..))
import GHC.Exts (TYPE, Constraint)
import GHC.Read qualified as Read
import GHC.Real qualified as P (Ratio(..), (%))
import GHC.Show (appPrec, appPrec1)
import GHC.Stack (HasCallStack)
import GHC.TypeLits qualified as L hiding (someNatVal)
import GHC.TypeNats qualified as L (someNatVal)
import KindInteger (SInteger, Integer)
import KindInteger qualified as I
import Numeric.Natural (Natural)
import Prelude hiding (Rational, Integer, Num, div, rem, fromInteger)
import Prelude qualified as P
import Prelude.Singletons qualified as P
import Text.ParserCombinators.ReadP as ReadP
import Text.ParserCombinators.ReadPrec as ReadPrec
import Text.Read.Lex qualified as Read
import Text.Show.Singletons (AppPrec1)
import Unsafe.Coerce(unsafeCoerce)

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

-- | Type-level version of "Prelude".'P.Rational', used only as a kind.
--
-- Use t'%' to construct one, use t':%' to pattern-match on it.
data Rational = Integer :% Natural
  -- ^ Note that @n ':%' d@ doesn't guarantee that @n@ be 'I.Normalized', nor
  -- that @d@ be non-zero, nor that the rational number is in 'Reduced' form.
  -- To make sure that's the case, use t'%' to construct type-level rationals,
  -- and use t':%' only for pattern-matching purposes. Alternatively, consider
  -- using the 'KnownRational' constraint or the 'Reduced' type-family. Both
  -- of them will reject any 'Rational' that fails to satisfy any of these
  -- constraints.

  -- Note: We export type-synonym ':%' rather than type-constructor ':%' so
  -- as to avoid having to use the leading tick, and to prevent term-level
  -- uses of the constructor.


-- | Shows just as a term-level "Prelude".'P.Rational'.
instance P.SShow Rational where
  sShowsPrec :: forall (t1 :: Natural) (t2 :: Rational) (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
         (Apply
            (Case_6989586621680028609
               (Case_6989586621679338589 t1 11 (CmpNat t1 11))
               (ShowsPrecSym2 11 (Num_ (Reduced_ t2 (Reduce t2)))
                .@#@$$$ (ShowStringSym1 " % "
                         .@#@$$$ ShowsSym1 (Den_ (Reduced_ t2 (Reduce t2)))))
               t3
               (Case_6989586621679338589 t1 11 (CmpNat t1 11)))
            t3))
-> SSymbol
     (Apply
        (Case_6989586621680028609
           (Case_6989586621679338589 t1 11 (CmpNat t1 11))
           (ShowsPrecSym2 11 (Num_ (Reduced_ t2 (Reduce t2)))
            .@#@$$$ (ShowStringSym1 " % "
                     .@#@$$$ ShowsSym1 (Den_ (Reduced_ t2 (Reduce t2)))))
           t3
           (Case_6989586621679338589 t1 11 (CmpNat t1 11)))
        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 Rational -> String
forall a. Show a => a -> String
show (Sing t2 -> Demote Rational
forall k (a :: k). SingKind k => Sing a -> Demote k
forall (a :: Rational). Sing a -> Demote Rational
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
     (Apply
        (Case_6989586621680028609
           (Case_6989586621679338589 t1 11 (CmpNat t1 11))
           (ShowsPrecSym2 11 (Num_ (Reduced_ t2 (Reduce t2)))
            .@#@$$$ (ShowStringSym1 " % "
                     .@#@$$$ ShowsSym1 (Den_ (Reduced_ t2 (Reduce t2)))))
           t3
           (Case_6989586621679338589 t1 11 (CmpNat t1 11)))
        t3)
Sing a
-> SSymbol
     (Apply
        (Case_6989586621680028609
           (Case_6989586621679338589 t1 11 (CmpNat t1 11))
           (ShowsPrecSym2 11 (Num_ (Reduced_ t2 (Reduce t2)))
            .@#@$$$ (ShowStringSym1 " % "
                     .@#@$$$ ShowsSym1 (Den_ (Reduced_ t2 (Reduce t2)))))
           t3
           (Case_6989586621679338589 t1 11 (CmpNat t1 11)))
        t3)
forall a b. a -> b
forall (a :: Symbol).
Sing a
-> SSymbol
     (Apply
        (Case_6989586621680028609
           (Case_6989586621679338589 t1 11 (CmpNat t1 11))
           (ShowsPrecSym2 11 (Num_ (Reduced_ t2 (Reduce t2)))
            .@#@$$$ (ShowStringSym1 " % "
                     .@#@$$$ ShowsSym1 (Den_ (Reduced_ t2 (Reduce t2)))))
           t3
           (Case_6989586621679338589 t1 11 (CmpNat t1 11)))
        t3)
unsafeCoerce

-- | Shows just as a term-level "Prelude".'P.Rational'.
--
-- 'ShowsPrec' type-checks only if the type-level 'Rational' is 'Reduced'.
instance P.PShow Rational where
  type ShowsPrec p r s = P.ShowParen (p P.>= AppPrec1)
    (P.ShowsPrecSym2 AppPrec1 (Num r) P..@#@$$$
     P.ShowStringSym1 " % " P..@#@$$$
     P.ShowsSym1 (Den r)) s

-- | Shows as a type-level "KindRational".'Rational' apears literally at the
-- type-level. Type-checks only if the type-level 'Rational' is 'Reduced'.
type ShowLit (r :: Rational) = ShowsLit r "" :: L.Symbol

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

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

-- | Shows as a type-level "KindRational".'Rational' apears literally at the
-- type-level. Type-checks only if the type-level 'Rational' is 'Reduced'.
type ShowsLit (r :: Rational) (s :: L.Symbol) = ShowsPrecLit 0 r s :: L.Symbol

data ShowsLitSym0 :: Rational ~> L.Symbol ~> L.Symbol
data ShowsLitSym1 :: Rational -> L.Symbol ~> L.Symbol
type ShowsLitSym2 :: Rational -> 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

-- | Shows as a type-level "KindRational".'Rational' apears literally at the
-- type-level. Type-checks only if the type-level 'Rational' is 'Reduced'.
type ShowsPrecLit (p :: Natural) (r :: Rational) (s :: L.Symbol) =
  P.ShowParen (p P.>= AppPrec1)
    (I.ShowsLitSym1 (Num r) P..@#@$$$
     P.ShowStringSym1 " :% " P..@#@$$$
     P.ShowsSym1 (Den r)) s :: L.Symbol

data ShowsPrecLitSym0 :: Natural ~> Rational ~> L.Symbol ~> L.Symbol
data ShowsPrecLitSym1 :: Natural -> Rational ~> L.Symbol ~> L.Symbol
data ShowsPrecLitSym2 :: Natural -> Rational -> L.Symbol ~> L.Symbol
type ShowsPrecLitSym3 :: Natural -> Rational -> 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'.
sShowLit :: SRational r -> Sing (ShowLit r)
sShowLit :: forall (r :: Rational). SRational r -> Sing (ShowLit r)
sShowLit SRational r
sr = SRational r
-> Sing ""
-> Sing
     (ShowParen
        (0 >= AppPrec1)
        (ShowsLitSym1 (Num r)
         .@#@$$$ (ShowStringSym1 " :% " .@#@$$$ ShowsSym1 (Den r)))
        "")
forall (r :: Rational) (s :: Symbol).
SRational r -> Sing s -> Sing (ShowsLit r s)
sShowsLit SRational r
sr (forall {k} (a :: k). SingI a => Sing a
forall (a :: Symbol). SingI a => Sing a
sing @"")

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

-- | Singleton version of 'ShowsLit'.
sShowsLit :: SRational r -> Sing (s :: P.Symbol) -> Sing (ShowsLit r s)
sShowsLit :: forall (r :: Rational) (s :: Symbol).
SRational r -> Sing s -> Sing (ShowsLit r s)
sShowsLit = Sing 0
-> SRational r
-> Sing s
-> Sing
     (ShowParen
        (0 >= AppPrec1)
        (ShowsLitSym1 (Num r)
         .@#@$$$ (ShowStringSym1 " :% " .@#@$$$ ShowsSym1 (Den r)))
        s)
forall (p :: Natural) (r :: Rational) (s :: Symbol).
Sing p -> SRational r -> Sing s -> Sing (ShowsPrecLit p r 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.Rational -> ShowS
showsLit :: Rational -> ShowS
showsLit = Int -> Rational -> ShowS
showsPrecLit Int
0

-- | Singleton version of 'ShowsPrecLit'.
sShowsPrecLit
  :: Sing (p :: Natural)
  -> SRational r
  -> Sing (s :: P.Symbol)
  -> Sing (ShowsPrecLit p r s)
sShowsPrecLit :: forall (p :: Natural) (r :: Rational) (s :: Symbol).
Sing p -> SRational r -> Sing s -> Sing (ShowsPrecLit p r s)
sShowsPrecLit Sing p
sp SRational r
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 -> Rational -> ShowS
showsPrecLit Int
p (Sing r -> Demote Rational
forall k (a :: k). SingKind k => Sing a -> Demote k
forall (a :: Rational). Sing a -> Demote Rational
fromSing Sing r
SRational r
si) String
"")
  in Demote Symbol
-> (forall (a :: Symbol).
    Sing a
    -> SSymbol
         (Apply
            (Case_6989586621680028609
               (Case_6989586621679338589 p 11 (CmpNat p 11))
               (ShowsLitSym1 (Num r)
                .@#@$$$ (ShowStringSym1 " :% " .@#@$$$ ShowsSym1 (Den r)))
               s
               (Case_6989586621679338589 p 11 (CmpNat p 11)))
            s))
-> SSymbol
     (Apply
        (Case_6989586621680028609
           (Case_6989586621679338589 p 11 (CmpNat p 11))
           (ShowsLitSym1 (Num r)
            .@#@$$$ (ShowStringSym1 " :% " .@#@$$$ ShowsSym1 (Den r)))
           s
           (Case_6989586621679338589 p 11 (CmpNat p 11)))
        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
     (Apply
        (Case_6989586621680028609
           (Case_6989586621679338589 p 11 (CmpNat p 11))
           (ShowsLitSym1 (Num r)
            .@#@$$$ (ShowStringSym1 " :% " .@#@$$$ ShowsSym1 (Den r)))
           s
           (Case_6989586621679338589 p 11 (CmpNat p 11)))
        s)
Sing a
-> SSymbol
     (Apply
        (Case_6989586621680028609
           (Case_6989586621679338589 p 11 (CmpNat p 11))
           (ShowsLitSym1 (Num r)
            .@#@$$$ (ShowStringSym1 " :% " .@#@$$$ ShowsSym1 (Den r)))
           s
           (Case_6989586621679338589 p 11 (CmpNat p 11)))
        s)
forall a b. a -> b
forall (a :: Symbol).
Sing a
-> SSymbol
     (Apply
        (Case_6989586621680028609
           (Case_6989586621679338589 p 11 (CmpNat p 11))
           (ShowsLitSym1 (Num r)
            .@#@$$$ (ShowStringSym1 " :% " .@#@$$$ ShowsSym1 (Den r)))
           s
           (Case_6989586621679338589 p 11 (CmpNat p 11)))
        s)
unsafeCoerce

-- | Demoted version of 'ShowsPrecLit'.
showsPrecLit :: Int -> P.Rational -> ShowS
showsPrecLit :: Int -> Rational -> ShowS
showsPrecLit Int
p Rational
_ | Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
0 = String -> ShowS
forall a. HasCallStack => String -> a
error String
"showsPrecLit: negative precedence"
showsPrecLit Int
p (HasCallStack => Rational -> Rational
Rational -> Rational
unsafeReduced -> Integer
n P.:% Integer
d) =
  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
$
    Int -> Integer -> ShowS
I.showsPrecLit Int
appPrec Integer
n ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
    String -> ShowS
showString String
" :% " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
    Integer -> ShowS
forall a. Show a => a -> ShowS
shows Integer
d

-- | Inverse of 'showsPrecLit'.
readPrecLit :: ReadPrec.ReadPrec P.Rational
readPrecLit :: ReadPrec Rational
readPrecLit = ReadPrec Rational -> ReadPrec Rational
forall a. ReadPrec a -> ReadPrec a
Read.parens (ReadPrec Rational -> ReadPrec Rational)
-> ReadPrec Rational -> ReadPrec Rational
forall a b. (a -> b) -> a -> b
$ do
    Integer
n :: P.Integer <- 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 a. ReadPrec a -> ReadPrec a
ReadPrec.step ReadPrec Integer
I.readPrecLit
    Lexeme -> ReadPrec ()
Read.expectP (String -> Lexeme
Read.Symbol String
":%")
    Natural
d :: Natural <- ReadPrec Natural -> ReadPrec Natural
forall a. ReadPrec a -> ReadPrec a
Read.parens (ReadPrec Natural -> ReadPrec Natural)
-> ReadPrec Natural -> ReadPrec Natural
forall a b. (a -> b) -> a -> b
$ ReadPrec Natural -> ReadPrec Natural
forall a. ReadPrec a -> ReadPrec a
ReadPrec.step (ReadPrec Natural -> ReadPrec Natural)
-> ReadPrec Natural -> ReadPrec Natural
forall a b. (a -> b) -> a -> b
$ ReadP Natural -> ReadPrec Natural
forall a. ReadP a -> ReadPrec a
ReadPrec.lift ReadP Natural
pNatural
    (String -> ReadPrec Rational)
-> (Rational -> ReadPrec Rational)
-> Either String Rational
-> ReadPrec Rational
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either String -> ReadPrec Rational
forall a. String -> ReadPrec a
forall (m :: Type -> Type) a. MonadFail m => String -> m a
fail Rational -> ReadPrec Rational
forall a. a -> ReadPrec a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Either String Rational -> ReadPrec Rational)
-> Either String Rational -> ReadPrec Rational
forall a b. (a -> b) -> a -> b
$ Integer -> Integer -> Either String Rational
rationalLit Integer
n (Natural -> Integer
forall a. Integral a => a -> Integer
toInteger Natural
d)
  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')

-- | Creates a "Prelude".'P.Rational' using the given literal numerator
-- and denominator, if in reduced form with a non-zero denominator.
rationalLit :: P.Integer -> P.Integer -> Either String P.Rational
rationalLit :: Integer -> Integer -> Either String Rational
rationalLit = \Integer
n Integer
d -> do
  Bool -> Either String () -> Either String ()
forall (f :: Type -> Type). Applicative f => Bool -> f () -> f ()
when (Integer
d Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
0) (Either String () -> Either String ())
-> Either String () -> Either String ()
forall a b. (a -> b) -> a -> b
$ String -> Either String ()
forall a b. a -> Either a b
Left String
"Denominator is zero."
  Bool -> Either String () -> Either String ()
forall (f :: Type -> Type). Applicative f => Bool -> f () -> f ()
when (Integer
d Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
0) (Either String () -> Either String ())
-> Either String () -> Either String ()
forall a b. (a -> b) -> a -> b
$ String -> Either String ()
forall a b. a -> Either a b
Left String
"Rational is not reduced."
  let r :: Rational
r@(Integer
n' P.:% Integer
d') = Integer
n Integer -> Integer -> Rational
forall a. Integral a => a -> a -> Ratio a
P.% Integer
d
  Bool -> Either String () -> Either String ()
forall (f :: Type -> Type). Applicative f => Bool -> f () -> f ()
when (Integer
n Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
/= Integer
n' Bool -> Bool -> Bool
|| Integer
d Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
/= Integer
d') (Either String () -> Either String ())
-> Either String () -> Either String ()
forall a b. (a -> b) -> a -> b
$ String -> Either String ()
forall a b. a -> Either a b
Left String
"Rational is not reduced."
  Rational -> Either String Rational
forall a b. b -> Either a b
Right Rational
r

-- | Reduces the given rational. 'error's if it can't be reduced.
unsafeReduce :: HasCallStack => P.Rational -> P.Rational
unsafeReduce :: HasCallStack => Rational -> Rational
unsafeReduce = \case
  Integer
n P.:% Integer
d | Integer
d Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
/= Integer
0 -> Integer
n Integer -> Integer -> Rational
forall a. Integral a => a -> a -> Ratio a
P.% Integer
d
           | Bool
otherwise -> String -> Rational
forall a. HasCallStack => String -> a
error String
"Denominator is zero."

-- | 'error's if the given rational is not reduced.  Otherwise, returns it.
unsafeReduced :: HasCallStack => P.Rational -> P.Rational
unsafeReduced :: HasCallStack => Rational -> Rational
unsafeReduced = \Rational
r0 -> case HasCallStack => Rational -> Rational
Rational -> Rational
unsafeReduce Rational
r0 of
  Rational
r1 | Rational
r0 Rational -> Rational -> Bool
forall a. Eq a => a -> a -> Bool
== Rational
r1 -> Rational
r0
     | Bool
otherwise -> String -> Rational
forall a. HasCallStack => String -> a
error (String -> Rational) -> String -> Rational
forall a b. (a -> b) -> a -> b
$ [String] -> String
forall (t :: Type -> Type) a. Foldable t => t [a] -> [a]
concat
        [ String
"Expected reduced rational ", Int -> Rational -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
appPrec1 Rational
r1 String
""
        , String
", got " , Int -> Rational -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
appPrec1 Rational
r0 String
"." ]

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

-- | Singleton version of 'Num'.
sNum :: SRational r -> SInteger (Num r)
sNum :: forall (r :: Rational). SRational r -> SInteger (Num r)
sNum SRational r
sr | Integer
n P.:% Integer
_ <- Sing r -> Demote Rational
forall k (a :: k). SingKind k => Sing a -> Demote k
forall (a :: Rational). Sing a -> Demote Rational
fromSing Sing r
SRational r
sr =
  Demote Integer
-> (forall (a :: Integer).
    Sing a -> SInteger (Num_ (Reduced_ r (Reduce r))))
-> SInteger (Num_ (Reduced_ r (Reduce r)))
forall k r.
SingKind k =>
Demote k -> (forall (a :: k). Sing a -> r) -> r
withSomeSing Integer
Demote Integer
n SInteger a -> SInteger (Num_ (Reduced_ r (Reduce r)))
Sing a -> SInteger (Num_ (Reduced_ r (Reduce r)))
forall a b. a -> b
forall (a :: Integer).
Sing a -> SInteger (Num_ (Reduced_ r (Reduce r)))
unsafeCoerce

-- | Literal /'Num'erator/ of a type-level 'Rational'.
-- It fails to type-check if the 'Rational' is not 'Reduced'.
type Num (r :: Rational) = Num_ (Reduced r) :: Integer
type family Num_ (r :: Rational) :: Integer where Num_ (n :% _) = n

data NumSym0 :: Rational ~> Integer
type NumSym1 :: Rational -> Integer

type instance Apply NumSym0 i = Num i
type NumSym1 i = Num i

-- | Singleton version of 'Den'.
sDen :: SRational r -> Sing (Den r :: Natural)
sDen :: forall (r :: Rational). SRational r -> Sing (Den r)
sDen SRational r
sr | Integer
_ P.:% Integer
d <- Sing r -> Demote Rational
forall k (a :: k). SingKind k => Sing a -> Demote k
forall (a :: Rational). Sing a -> Demote Rational
fromSing Sing r
SRational r
sr =
  forall k r.
SingKind k =>
Demote k -> (forall (a :: k). Sing a -> r) -> r
withSomeSing @Natural (Integer -> Natural
forall a. Num a => Integer -> a
P.fromInteger Integer
d) SNat a -> SNat (Den_ (Reduced_ r (Reduce r)))
Sing a -> SNat (Den_ (Reduced_ r (Reduce r)))
forall (a :: Natural).
Sing a -> SNat (Den_ (Reduced_ r (Reduce r)))
forall a b. a -> b
unsafeCoerce

-- | Literal /'Den'ominator/ of a type-level 'Rational'.
-- It fails to type-check if the 'Rational' is not 'Reduced'.
type Den (r :: Rational) = Den_ (Reduced r) :: Natural
type family Den_ (r :: Rational) :: Natural where Den_ (_ :% d) = d

data DenSym0 :: Rational ~> Natural
type DenSym1 :: Rational -> Natural

type instance Apply DenSym0 i = Den i
type DenSym1 i = Den i

-- | Pattern-match on a type-level 'Rational'.
--
-- Note that t':%' doesn't check that the 'Rational' be 'Reduced' nor
-- have a non-zero denominator.
--
-- When constructing 'Rational's, use t'%' instead, which not only accepts
-- more polymorphic inputs, but also returns a 'Reduced' result with
-- denominator known to be non-zero.
type (n :: I.Integer) :% (d :: Natural) = n ':% d :: Rational

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

type instance Apply ((:%@#@$$) b) p = (:%@#@$$$) b p
type instance Apply (:%@#@$) b = (:%@#@$$) b
type (:%@#@$$$) b p = b :% p

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

-- | A 'Reduce'd rational number is one in which the numerator and denominator
-- have no common denominators. 'Reduced' fails to type-check if the given
-- type-level 'Rational' is not reduced, otherwise it returns the given
-- 'Rational', unmodified.  It also fails to type-check if the 'I.Integer'
-- numerator isn't 'I.Normalized', or if the denominator is zero.
--
-- Only reduced 'Rational's can be reliably constrained for equality
-- using '~'. Only reduced 'Rational's are 'KnownRational's.
--
-- The type-level functions in the "KindRational" module
-- always produce reduced 'Rational's.
type Reduced (r :: Rational) = Reduced_ r (Reduce r) :: Rational
type family Reduced_ (r :: Rational) (x :: Rational) :: Rational where
  Reduced_ r r = r
  Reduced_ (na :% da) (nb :% db) = L.TypeError
    ('L.Text "Expected reduced rational (" 'L.:<>:
     'L.Text (I.ShowsLit nb " :% ") 'L.:<>:
     'L.Text (P.Shows db "), got (") 'L.:<>:
     'L.Text (I.ShowsLit na " :% ") 'L.:<>:
     'L.Text (P.Shows da ")."))

data ReducedSym0 :: Rational ~> Rational
type ReducedSym1 :: Rational -> Rational

type instance Apply ReducedSym0 i = Reduced i
type ReducedSym1 i = Reduced i

-- | 'SRational's always contain a 'Reduced' 'Rational'.
sReducedRefl :: SRational r -> (r :~: Reduced r)
sReducedRefl :: forall (r :: Rational). SRational r -> r :~: Reduced r
sReducedRefl !SRational r
_ = (Any :~: Any) -> r :~: Reduced_ r (Reduce r)
forall a b. a -> b
unsafeCoerce Any :~: Any
forall {k} (a :: k). a :~: a
Refl

-- | Reduce a type-level 'Rational' so that the numerator and denominator
-- have no common factors. It fails to type-check if the 'I.Integer'
-- numerator isn't 'I.Normalized'.
--
-- Only reduced 'Rational's can be reliably constrained for equality
-- using '~'. Only reduced 'Rational's are 'KnownRational's.
type family Reduce (r :: Rational) :: Rational where
  Reduce (n :% 0) = L.TypeError
    ('L.Text "Denominator is zero in (" 'L.:<>: 'L.Text (I.ShowsLit n " :% 0)"))
  Reduce (n :% d) =
    I.Fold (FromNatural 0) (ReduceNegSym1 d) (ReducePosSym1 d) n

data ReduceNegSym1 :: Natural -> Natural ~> Rational
type instance Apply (ReduceNegSym1 d) n = ReduceNeg d n
type ReduceNeg (d :: Natural) (n :: Natural)
  = ReduceNeg_ (ReducePos d n) :: Rational
type ReduceNeg_ (rpos :: Rational) = P.Negate (Num_ rpos) :% Den_ rpos

data ReducePosSym1 :: Natural -> Natural ~> Rational
type instance Apply (ReducePosSym1 d) n = ReducePos d n
type family ReducePos (d :: Natural) (n :: Natural) :: Rational where
  ReducePos d n =
    I.FromNatural (L.Div n (I.GCD (I.FromNatural n) (I.FromNatural d)))
               :% (L.Div d (I.GCD (I.FromNatural n) (I.FromNatural d)))

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

-- | Construct a type-level 'Rational' from a type-level 'Natural'.
type FromNatural (n :: Natural) = I.FromNatural n :% 1 :: Rational

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

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

-- | Singleton version of 'FromNatural'.
sFromNatural :: Sing (n :: Natural) -> SRational (FromNatural n)
sFromNatural :: forall (n :: Natural). Sing n -> SRational (FromNatural n)
sFromNatural = Rational -> SRational (FromNatural n :% 1)
forall (r :: Rational). Rational -> SRational r
UnsafeSRational (Rational -> SRational (FromNatural n :% 1))
-> (SNat n -> Rational) -> SNat n -> SRational (FromNatural n :% 1)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Natural -> Rational
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Natural -> Rational) -> (SNat n -> Natural) -> SNat n -> Rational
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
{-# INLINE sFromNatural #-}

-- | Demoted version of 'FromNatural'.
fromNatural :: Natural -> P.Rational
fromNatural :: Natural -> Rational
fromNatural = Natural -> Rational
forall a b. (Integral a, Num b) => a -> b
P.fromIntegral
{-# INLINE fromNatural #-}

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

-- | Construct a type-level 'Rational' from a type-level 'Integer'.
-- It fails to type-check if the 'I.Integer' isn't 'I.Normalized'.
type FromInteger (i :: Integer) = I.Normalized i :% 1 :: Rational

data FromIntegerSym0 :: Integer ~> Rational
type FromIntegerSym1 :: Integer -> Rational

type instance Apply FromIntegerSym0 i = FromInteger i
type FromIntegerSym1 i = FromInteger i

-- | Singleton version of 'FromInteger'.
sFromInteger :: SInteger n -> SRational (FromInteger n)
sFromInteger :: forall (n :: Integer). SInteger n -> SRational (FromInteger n)
sFromInteger = Rational -> SRational (Normalized n :% 1)
forall (r :: Rational). Rational -> SRational r
UnsafeSRational (Rational -> SRational (Normalized n :% 1))
-> (SInteger n -> Rational)
-> SInteger n
-> SRational (Normalized n :% 1)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> Rational
fromInteger (Integer -> Rational)
-> (SInteger n -> Integer) -> SInteger n -> Rational
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SInteger n -> Integer
Sing n -> Demote Integer
forall k (a :: k). SingKind k => Sing a -> Demote k
forall (a :: Integer). Sing a -> Demote Integer
fromSing
{-# INLINE sFromInteger #-}

-- | Demoted version of 'FromInteger'.
fromInteger :: P.Integer -> P.Rational
fromInteger :: Integer -> Rational
fromInteger = Integer -> Rational
forall a. Num a => Integer -> a
P.fromInteger
{-# INLINE fromInteger #-}

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

infixl 7 %, %%, :%, :%@#@$$$, %@#@$$$

-- | @'ToRational' kn kd@ enables constructing type-level 'Rational's
-- from a numerator of kind @kn@ and a denominator of kind @kd@.
class (SingKind kn, SingKind kd) => ToRational kn kd where
  -- | @n t'%' d@ constructs and reduces a type-level 'Rational'
  -- with numerator @n@ and denominator @d@.
  --
  -- This type-family accepts any combination of 'Natural', 'Integer' and
  -- 'Rational' as input.
  --
  -- @
  -- ( t'%') :: 'Natural'  -> 'Natural'  -> 'Rational'
  -- ( t'%') :: 'Natural'  -> 'Integer'  -> 'Rational'
  -- ( t'%') :: 'Natural'  -> 'Rational' -> 'Rational'
  --
  -- ( t'%') :: 'Integer'  -> 'Natural'  -> 'Rational'
  -- ( t'%') :: 'Integer'  -> 'Integer'  -> 'Rational'
  -- ( t'%') :: 'Integer'  -> 'Rational' -> 'Rational'
  --
  -- ( t'%') :: 'Rational' -> 'Natural'  -> 'Rational'
  -- ( t'%') :: 'Rational' -> 'Integer'  -> 'Rational'
  -- ( t'%') :: 'Rational' -> 'Rational' -> 'Rational'
  -- @
  --
  -- It's not possible to pattern-match on @n t'%' d@.  Instead, you must
  -- pattern match on @x t':%' y@, where @x t':%' y ~ n t'%' d@.
  type (n :: kn) % (d :: kd) :: Rational
  -- | Demoted version of t'%'. Returns 'Nothing' where t'%' would fail
  -- to type-check (that is, denominator is 0).
  -- See '%' for an unsafe version of this.
  mkRational :: Demote kn -> Demote kd -> Maybe P.Rational

-- | Like 'mkRational', but fails with 'error' where 'mkRational' would
-- fail with 'Nothing'.
(%) :: forall kn kd
    .  (ToRational kn kd, HasCallStack)
    => Demote kn
    -> Demote kd
    -> P.Rational
Demote kn
n % :: forall kn kd.
(ToRational kn kd, HasCallStack) =>
Demote kn -> Demote kd -> Rational
% Demote kd
d = Rational -> Maybe Rational -> Rational
forall a. a -> Maybe a -> a
fromMaybe (String -> Rational
forall a. HasCallStack => String -> a
error String
"Denominator is zero.") (Demote kn -> Demote kd -> Maybe Rational
forall kn kd.
ToRational kn kd =>
Demote kn -> Demote kd -> Maybe Rational
mkRational Demote kn
n Demote kd
d)
{-# INLINE (%) #-}

-- | Like 'sMkRational', but never fails, thanks to a
-- 'KnownRational' constraint.
(%%) :: forall kn kd n d
     .  (ToRational kn kd, KnownRational (n % d))
     => Sing (n :: kn)
     -> Sing (d :: kd)
     -> SRational (n % d)
%% :: forall kn kd (n :: kn) (d :: kd).
(ToRational kn kd, KnownRational (n % d)) =>
Sing n -> Sing d -> SRational (n % d)
(%%) Sing n
sn Sing d
sd = Maybe (SRational (n % d)) -> SRational (n % d)
forall a. HasCallStack => Maybe a -> a
fromJust (Sing n -> Sing d -> Maybe (SRational (n % d))
forall kn kd (n :: kn) (d :: kd).
ToRational kn kd =>
Sing n -> Sing d -> Maybe (SRational (n % d))
sMkRational Sing n
sn Sing d
sd)
{-# INLINE (%%) #-}

-- | Singleton version of 'mkRational'.
sMkRational
  :: forall kn kd n d
  .  (ToRational kn kd)
  => Sing (n :: kn)
  -> Sing (d :: kd)
  -> Maybe (SRational (n % d))
sMkRational :: forall kn kd (n :: kn) (d :: kd).
ToRational kn kd =>
Sing n -> Sing d -> Maybe (SRational (n % d))
sMkRational Sing n
sn Sing d
sd =
  Rational -> SRational (n % d)
forall (r :: Rational). Rational -> SRational r
UnsafeSRational (Rational -> SRational (n % d))
-> Maybe Rational -> Maybe (SRational (n % d))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Demote kn -> Demote kd -> Maybe Rational
forall kn kd.
ToRational kn kd =>
Demote kn -> Demote kd -> Maybe Rational
mkRational (Sing n -> Demote kn
forall (a :: kn). Sing a -> Demote kn
forall k (a :: k). SingKind k => Sing a -> Demote k
fromSing Sing n
sn) (Sing d -> Demote kd
forall (a :: kd). Sing a -> Demote kd
forall k (a :: k). SingKind k => Sing a -> Demote k
fromSing Sing d
sd)
{-# INLINE sMkRational #-}

data ToRationalSym0 :: kkn ~> kkd ~> Constraint
data ToRationalSym1 :: kkn -> kkd ~> Constraint
-- type ToRationalSym2 :: kkn -> kkd -> Constraint  --  (inferred)

type instance Apply ToRationalSym0 kn = ToRationalSym1 kn
type instance Apply (ToRationalSym1 kn) kd = ToRationalSym2 kn kd
type ToRationalSym2 kn kd = ToRational kn kd

data (%@#@$) :: kn ~> kd ~> Rational
data (%@#@$$) :: kn -> kd ~> Rational
type (%@#@$$$) :: kn -> kd -> Rational

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

instance ToRational Natural Natural where
  type n % d = I.FromNatural n % d
  mkRational :: Demote Natural -> Demote Natural -> Maybe Rational
mkRational Demote Natural
_ Demote Natural
0 = Maybe Rational
forall a. Maybe a
Nothing
  mkRational Demote Natural
n Demote Natural
d = Rational -> Maybe Rational
forall a. a -> Maybe a
Just (Rational -> Maybe Rational) -> Rational -> Maybe Rational
forall a b. (a -> b) -> a -> b
$! Natural -> Integer
forall a. Integral a => a -> Integer
toInteger Natural
Demote Natural
n Integer -> Integer -> Rational
forall a. Integral a => a -> a -> Ratio a
P.% Natural -> Integer
forall a. Integral a => a -> Integer
toInteger Natural
Demote Natural
d

instance ToRational Natural Integer where
  type n % d = (I.FromNatural n P.* P.Signum d) % I.Abs d
  mkRational :: Demote Natural -> Demote Integer -> Maybe Rational
mkRational Demote Natural
_ Demote Integer
0 = Maybe Rational
forall a. Maybe a
Nothing
  mkRational Demote Natural
n Demote Integer
d = Rational -> Maybe Rational
forall a. a -> Maybe a
Just (Rational -> Maybe Rational) -> Rational -> Maybe Rational
forall a b. (a -> b) -> a -> b
$! Natural -> Integer
forall a. Integral a => a -> Integer
toInteger Natural
Demote Natural
n Integer -> Integer -> Rational
forall a. Integral a => a -> a -> Ratio a
P.% Integer
Demote Integer
d

instance ToRational Natural Rational where
  type n % d = FromNatural n P.* Recip d
  mkRational :: Demote Natural -> Demote Rational -> Maybe Rational
mkRational Demote Natural
_ Demote Rational
0 = Maybe Rational
forall a. Maybe a
Nothing
  mkRational Demote Natural
n Demote Rational
d = Rational -> Maybe Rational
forall a. a -> Maybe a
Just (Rational -> Maybe Rational) -> Rational -> Maybe Rational
forall a b. (a -> b) -> a -> b
$! Natural -> Rational
forall a b. (Integral a, Num b) => a -> b
fromIntegral Natural
Demote Natural
n Rational -> Rational -> Rational
forall a. Fractional a => a -> a -> a
P./ Rational
Demote Rational
d

instance ToRational Integer Natural where
  type n % d = Reduce (n :% d)
  mkRational :: Demote Integer -> Demote Natural -> Maybe Rational
mkRational Demote Integer
_ Demote Natural
0 = Maybe Rational
forall a. Maybe a
Nothing
  mkRational Demote Integer
n Demote Natural
d = Rational -> Maybe Rational
forall a. a -> Maybe a
Just (Rational -> Maybe Rational) -> Rational -> Maybe Rational
forall a b. (a -> b) -> a -> b
$! Integer
Demote Integer
n Integer -> Integer -> Rational
forall a. Integral a => a -> a -> Ratio a
P.% Natural -> Integer
forall a. Integral a => a -> Integer
toInteger Natural
Demote Natural
d

instance ToRational Integer Integer where
  type n % d = (n P.* P.Signum d) % I.Abs d
  mkRational :: Demote Integer -> Demote Integer -> Maybe Rational
mkRational Demote Integer
_ Demote Integer
0 = Maybe Rational
forall a. Maybe a
Nothing
  mkRational Demote Integer
n Demote Integer
d = Rational -> Maybe Rational
forall a. a -> Maybe a
Just (Rational -> Maybe Rational) -> Rational -> Maybe Rational
forall a b. (a -> b) -> a -> b
$! (Integer
Demote Integer
n Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
P.* Integer -> Integer
forall a. Num a => a -> a
P.signum Integer
Demote Integer
d) Integer -> Integer -> Rational
forall a. Integral a => a -> a -> Ratio a
P.% Integer -> Integer
forall a. Num a => a -> a
P.abs Integer
Demote Integer
d

instance ToRational Integer Rational where
  type n % d = FromInteger n P.* Recip d
  mkRational :: Demote Integer -> Demote Rational -> Maybe Rational
mkRational Demote Integer
_ Demote Rational
0 = Maybe Rational
forall a. Maybe a
Nothing
  mkRational Demote Integer
n Demote Rational
d = Rational -> Maybe Rational
forall a. a -> Maybe a
Just (Rational -> Maybe Rational) -> Rational -> Maybe Rational
forall a b. (a -> b) -> a -> b
$! Integer -> Rational
fromInteger Integer
Demote Integer
n Rational -> Rational -> Rational
forall a. Num a => a -> a -> a
P.* Rational -> Rational
forall a. Fractional a => a -> a
recip Rational
Demote Rational
d

instance ToRational Rational Natural where
  type n % d = n P.* Recip (FromNatural d)
  mkRational :: Demote Rational -> Demote Natural -> Maybe Rational
mkRational Demote Rational
_ Demote Natural
0 = Maybe Rational
forall a. Maybe a
Nothing
  mkRational Demote Rational
n Demote Natural
d = Rational -> Maybe Rational
forall a. a -> Maybe a
Just (Rational -> Maybe Rational) -> Rational -> Maybe Rational
forall a b. (a -> b) -> a -> b
$! Rational
Demote Rational
n Rational -> Rational -> Rational
forall a. Num a => a -> a -> a
P.* Rational -> Rational
forall a. Fractional a => a -> a
P.recip (Natural -> Rational
fromNatural Natural
Demote Natural
d)

instance ToRational Rational Integer where
  type n % d = n P.* Recip (FromInteger d)
  mkRational :: Demote Rational -> Demote Integer -> Maybe Rational
mkRational Demote Rational
_ Demote Integer
0 = Maybe Rational
forall a. Maybe a
Nothing
  mkRational Demote Rational
n Demote Integer
d = Rational -> Maybe Rational
forall a. a -> Maybe a
Just (Rational -> Maybe Rational) -> Rational -> Maybe Rational
forall a b. (a -> b) -> a -> b
$! Rational
Demote Rational
n Rational -> Rational -> Rational
forall a. Num a => a -> a -> a
P.* Rational -> Rational
forall a. Fractional a => a -> a
P.recip (Integer -> Rational
fromInteger Integer
Demote Integer
d)

instance ToRational Rational Rational where
  type n % d = n P.* Recip d
  mkRational :: Demote Rational -> Demote Rational -> Maybe Rational
mkRational Demote Rational
_ Demote Rational
0 = Maybe Rational
forall a. Maybe a
Nothing
  mkRational Demote Rational
n Demote Rational
d = Rational -> Maybe Rational
forall a. a -> Maybe a
Just (Rational -> Maybe Rational) -> Rational -> Maybe Rational
forall a b. (a -> b) -> a -> b
$! Rational
Demote Rational
n Rational -> Rational -> Rational
forall a. Num a => a -> a -> a
P.* Rational -> Rational
forall a. Fractional a => a -> a
P.recip Rational
Demote Rational
d

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

instance P.PNum Rational where
  type l + r = Add l r
  type l - r = Add l (P.Negate r)
  type l * r = Mul l r
  type Negate r = Reduce (P.Negate (Num r) :% Den r)
  type Abs r = Reduce (P.Abs (Num r) :% Den r)
  type Signum r = P.Signum (Num r) :% 1
  type FromInteger n = FromNatural n

instance P.SNum Rational where
  Sing t1
l %+ :: forall (t1 :: Rational) (t2 :: Rational).
Sing t1 -> Sing t2 -> Sing (Apply (Apply (+@#@$) t1) t2)
%+ Sing t2
r = Rational -> SRational (Add_ (Reduce t1) (Reduce t2))
forall (r :: Rational). Rational -> SRational r
UnsafeSRational (Sing t1 -> Demote Rational
forall k (a :: k). SingKind k => Sing a -> Demote k
forall (a :: Rational). Sing a -> Demote Rational
fromSing Sing t1
l Rational -> Rational -> Rational
forall a. Num a => a -> a -> a
+ Sing t2 -> Demote Rational
forall k (a :: k). SingKind k => Sing a -> Demote k
forall (a :: Rational). Sing a -> Demote Rational
fromSing Sing t2
r)
  Sing t1
l %- :: forall (t1 :: Rational) (t2 :: Rational).
Sing t1 -> Sing t2 -> Sing (Apply (Apply (-@#@$) t1) t2)
%- Sing t2
r = Rational
-> SRational
     (Add_
        (Reduce t1)
        (Reduce
           (Reduce
              (Fold Z PSym0 NSym0 (Num_ (Reduced_ t2 (Reduce t2)))
               :% Den_ (Reduced_ t2 (Reduce t2))))))
forall (r :: Rational). Rational -> SRational r
UnsafeSRational (Sing t1 -> Demote Rational
forall k (a :: k). SingKind k => Sing a -> Demote k
forall (a :: Rational). Sing a -> Demote Rational
fromSing Sing t1
l Rational -> Rational -> Rational
forall a. Num a => a -> a -> a
- Sing t2 -> Demote Rational
forall k (a :: k). SingKind k => Sing a -> Demote k
forall (a :: Rational). Sing a -> Demote Rational
fromSing Sing t2
r)
  Sing t1
l %* :: forall (t1 :: Rational) (t2 :: Rational).
Sing t1 -> Sing t2 -> Sing (Apply (Apply (*@#@$) t1) t2)
%* Sing t2
r = Rational -> SRational (Mul_ (Reduce t1) (Reduce t2))
forall (r :: Rational). Rational -> SRational r
UnsafeSRational (Sing t1 -> Demote Rational
forall k (a :: k). SingKind k => Sing a -> Demote k
forall (a :: Rational). Sing a -> Demote Rational
fromSing Sing t1
l Rational -> Rational -> Rational
forall a. Num a => a -> a -> a
* Sing t2 -> Demote Rational
forall k (a :: k). SingKind k => Sing a -> Demote k
forall (a :: Rational). Sing a -> Demote Rational
fromSing Sing t2
r)
  sNegate :: forall (t :: Rational). Sing t -> Sing (Apply NegateSym0 t)
sNegate = Rational
-> SRational
     (Reduce
        (Fold Z PSym0 NSym0 (Num_ (Reduced_ t (Reduce t)))
         :% Den_ (Reduced_ t (Reduce t))))
forall (r :: Rational). Rational -> SRational r
UnsafeSRational (Rational
 -> SRational
      (Reduce
         (Fold Z PSym0 NSym0 (Num_ (Reduced_ t (Reduce t)))
          :% Den_ (Reduced_ t (Reduce t)))))
-> (SRational t -> Rational)
-> SRational t
-> SRational
     (Reduce
        (Fold Z PSym0 NSym0 (Num_ (Reduced_ t (Reduce t)))
         :% Den_ (Reduced_ t (Reduce t))))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rational -> Rational
forall a. Num a => a -> a
negate (Rational -> Rational)
-> (SRational t -> Rational) -> SRational t -> Rational
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sing t -> Demote Rational
SRational t -> Rational
forall k (a :: k). SingKind k => Sing a -> Demote k
forall (a :: Rational). Sing a -> Demote Rational
fromSing
  sAbs :: forall (t :: Rational). Sing t -> Sing (Apply AbsSym0 t)
sAbs = Rational
-> SRational
     (Reduce
        (FromNatural (Fold 0 IdSym0 IdSym0 (Num_ (Reduced_ t (Reduce t))))
         :% Den_ (Reduced_ t (Reduce t))))
forall (r :: Rational). Rational -> SRational r
UnsafeSRational (Rational
 -> SRational
      (Reduce
         (FromNatural (Fold 0 IdSym0 IdSym0 (Num_ (Reduced_ t (Reduce t))))
          :% Den_ (Reduced_ t (Reduce t)))))
-> (SRational t -> Rational)
-> SRational t
-> SRational
     (Reduce
        (FromNatural (Fold 0 IdSym0 IdSym0 (Num_ (Reduced_ t (Reduce t))))
         :% Den_ (Reduced_ t (Reduce t))))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rational -> Rational
forall a. Num a => a -> a
abs (Rational -> Rational)
-> (SRational t -> Rational) -> SRational t -> Rational
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sing t -> Demote Rational
SRational t -> Rational
forall k (a :: k). SingKind k => Sing a -> Demote k
forall (a :: Rational). Sing a -> Demote Rational
fromSing
  sSignum :: forall (t :: Rational). Sing t -> Sing (Apply SignumSym0 t)
sSignum = Rational
-> SRational
     (Fold
        Z
        (ConstSym1 (N 1))
        (ConstSym1 (P 1))
        (Num_ (Reduced_ t (Reduce t)))
      :% 1)
forall (r :: Rational). Rational -> SRational r
UnsafeSRational (Rational
 -> SRational
      (Fold
         Z
         (ConstSym1 (N 1))
         (ConstSym1 (P 1))
         (Num_ (Reduced_ t (Reduce t)))
       :% 1))
-> (SRational t -> Rational)
-> SRational t
-> SRational
     (Fold
        Z
        (ConstSym1 (N 1))
        (ConstSym1 (P 1))
        (Num_ (Reduced_ t (Reduce t)))
      :% 1)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rational -> Rational
forall a. Num a => a -> a
signum (Rational -> Rational)
-> (SRational t -> Rational) -> SRational t -> Rational
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sing t -> Demote Rational
SRational t -> Rational
forall k (a :: k). SingKind k => Sing a -> Demote k
forall (a :: Rational). Sing a -> Demote Rational
fromSing
  sFromInteger :: forall (t :: Natural). Sing t -> Sing (Apply FromIntegerSym0 t)
sFromInteger = Sing t -> Sing (Apply FromIntegerSym0 t)
Sing t -> SRational (FromNatural t)
forall (n :: Natural). Sing n -> SRational (FromNatural n)
sFromNatural

sNegateRefl :: Sing (r :: Rational) -> (r :~: P.Negate (P.Negate r))
sNegateRefl :: forall (r :: Rational). Sing r -> r :~: Negate (Negate r)
sNegateRefl !Sing r
_ = (Any :~: Any)
-> r
   :~: Reduce
         (Fold
            Z
            PSym0
            NSym0
            (Num_
               (Reduced_
                  (Reduce
                     (Fold Z PSym0 NSym0 (Num_ (Reduced_ r (Reduce r)))
                      :% Den_ (Reduced_ r (Reduce r))))
                  (Reduce
                     (Reduce
                        (Fold Z PSym0 NSym0 (Num_ (Reduced_ r (Reduce r)))
                         :% Den_ (Reduced_ r (Reduce r)))))))
          :% Den_
               (Reduced_
                  (Reduce
                     (Fold Z PSym0 NSym0 (Num_ (Reduced_ r (Reduce r)))
                      :% Den_ (Reduced_ r (Reduce r))))
                  (Reduce
                     (Reduce
                        (Fold Z PSym0 NSym0 (Num_ (Reduced_ r (Reduce r)))
                         :% Den_ (Reduced_ r (Reduce r)))))))
forall a b. a -> b
unsafeCoerce Any :~: Any
forall {k} (a :: k). a :~: a
Refl

-- | Sign of type-level 'Rational's, as a type-level 'Integer'.
--
-- * 'I.Z' if zero.
--
-- * @'I.P' 1@ if positive.
--
-- * @'I.N' 1@ if negative.
type Signum (r :: Rational) = P.Signum (Num r) :: Integer

data SignumSym0 :: Rational ~> Integer
type SignumSym1 :: Rational -> Integer

type instance Apply SignumSym0 i = Signum i
type SignumSym1 i = Signum i

-- | Singleton version of 'Signum'.
sSignum :: Sing (r :: Rational) -> SInteger (Signum r)
sSignum :: forall (r :: Rational). Sing r -> SInteger (Signum r)
sSignum Sing r
sr = Sing (Num_ (Reduced r))
-> Sing (Apply SignumSym0 (Num_ (Reduced r)))
forall a (t :: a). SNum a => Sing t -> Sing (Apply SignumSym0 t)
forall (t :: Integer). Sing t -> Sing (Apply SignumSym0 t)
P.sSignum (SRational r -> SInteger (Num_ (Reduced r))
forall (r :: Rational). SRational r -> SInteger (Num r)
sNum Sing r
SRational r
sr)

-- | The 'Signum' of a 'Rational' equals the 'PNum' 'P.Signum' of its
-- 'Num'erator, as well as the 'Num'erator of its 'PNum' 'P.Signum'.
sSignumRefl
  :: SRational r
  -> (Signum r :~: P.Signum (Num r),
      Signum r :~: Num (P.Signum r))
sSignumRefl :: forall (r :: Rational).
SRational r -> (Signum r :~: Signum r, Signum r :~: Num (Signum r))
sSignumRefl !SRational r
_ = (Any :~: Any, Any :~: Any)
-> (Fold Z (ConstSym1 (N 1)) (ConstSym1 (P 1)) (Num_ (Reduced r))
    :~: Fold Z (ConstSym1 (N 1)) (ConstSym1 (P 1)) (Num_ (Reduced r)),
    Fold Z (ConstSym1 (N 1)) (ConstSym1 (P 1)) (Num_ (Reduced r))
    :~: Num_
          (Reduced_
             (Fold Z (ConstSym1 (N 1)) (ConstSym1 (P 1)) (Num_ (Reduced r))
              :% 1)
             (Fold
                (Z :% 1)
                (ReduceNegSym1 1)
                (ReducePosSym1 1)
                (Fold Z (ConstSym1 (N 1)) (ConstSym1 (P 1)) (Num_ (Reduced r))))))
forall a b. a -> b
unsafeCoerce (Any :~: Any
forall {k} (a :: k). a :~: a
Refl, Any :~: Any
forall {k} (a :: k). a :~: a
Refl)

type Mul (a :: Rational) (b :: Rational) =
  Mul_ (Reduce a) (Reduce b) :: Rational
type family Mul_ (a :: Rational) (b :: Rational) where
  Mul_ (n1 :% d1) (n2 :% d2) = Reduce ((n1 P.* n2) :% (d1 L.* d2))

type Add (a :: Rational) (b :: Rational) =
  Add_ (Reduce a) (Reduce b) :: Rational
type family Add_ (a :: Rational) (r :: Rational) :: Rational where
  Add_ (an :% ad) (bn :% bd) =
    (an P.* I.FromNatural bd P.+ bn P.* I.FromNatural ad) % (ad L.* bd)

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

-- | Singleton version of 'Recip'. Type-checks only with a non-zero @r@.
sRecip :: I.Z :% 1 < P.Abs r => SRational r -> SRational (Recip r)
sRecip :: forall (r :: Rational).
((Z :% 1) < Abs r) =>
SRational r -> SRational (Recip r)
sRecip = Rational
-> SRational
     (Reduce
        (Mul_
           (CmpInteger_
              (Fold
                 'EQ
                 (ConstSym1 'LT)
                 (ConstSym1 'GT)
                 (FromNatural (Den_ (Reduced r))))
              'EQ
              (Fold 0 IdSym0 IdSym0 (FromNatural (Den_ (Reduced r))))
              0)
           (CmpInteger_
              (Fold
                 'EQ
                 (ConstSym1 'LT)
                 (ConstSym1 'GT)
                 (Fold Z (ConstSym1 (N 1)) (ConstSym1 (P 1)) (Num_ (Reduced r))))
              'EQ
              (Fold
                 0
                 IdSym0
                 IdSym0
                 (Fold Z (ConstSym1 (N 1)) (ConstSym1 (P 1)) (Num_ (Reduced r))))
              0)
           (Fold 0 IdSym0 IdSym0 (FromNatural (Den_ (Reduced r))))
           (Fold
              0
              IdSym0
              IdSym0
              (Fold Z (ConstSym1 (N 1)) (ConstSym1 (P 1)) (Num_ (Reduced r))))
         :% Fold 0 IdSym0 IdSym0 (Num_ (Reduced r))))
forall (r :: Rational). Rational -> SRational r
UnsafeSRational (Rational
 -> SRational
      (Reduce
         (Mul_
            (CmpInteger_
               (Fold
                  'EQ
                  (ConstSym1 'LT)
                  (ConstSym1 'GT)
                  (FromNatural (Den_ (Reduced r))))
               'EQ
               (Fold 0 IdSym0 IdSym0 (FromNatural (Den_ (Reduced r))))
               0)
            (CmpInteger_
               (Fold
                  'EQ
                  (ConstSym1 'LT)
                  (ConstSym1 'GT)
                  (Fold Z (ConstSym1 (N 1)) (ConstSym1 (P 1)) (Num_ (Reduced r))))
               'EQ
               (Fold
                  0
                  IdSym0
                  IdSym0
                  (Fold Z (ConstSym1 (N 1)) (ConstSym1 (P 1)) (Num_ (Reduced r))))
               0)
            (Fold 0 IdSym0 IdSym0 (FromNatural (Den_ (Reduced r))))
            (Fold
               0
               IdSym0
               IdSym0
               (Fold Z (ConstSym1 (N 1)) (ConstSym1 (P 1)) (Num_ (Reduced r))))
          :% Fold 0 IdSym0 IdSym0 (Num_ (Reduced r)))))
-> (SRational r -> Rational)
-> SRational r
-> SRational
     (Reduce
        (Mul_
           (CmpInteger_
              (Fold
                 'EQ
                 (ConstSym1 'LT)
                 (ConstSym1 'GT)
                 (FromNatural (Den_ (Reduced r))))
              'EQ
              (Fold 0 IdSym0 IdSym0 (FromNatural (Den_ (Reduced r))))
              0)
           (CmpInteger_
              (Fold
                 'EQ
                 (ConstSym1 'LT)
                 (ConstSym1 'GT)
                 (Fold Z (ConstSym1 (N 1)) (ConstSym1 (P 1)) (Num_ (Reduced r))))
              'EQ
              (Fold
                 0
                 IdSym0
                 IdSym0
                 (Fold Z (ConstSym1 (N 1)) (ConstSym1 (P 1)) (Num_ (Reduced r))))
              0)
           (Fold 0 IdSym0 IdSym0 (FromNatural (Den_ (Reduced r))))
           (Fold
              0
              IdSym0
              IdSym0
              (Fold Z (ConstSym1 (N 1)) (ConstSym1 (P 1)) (Num_ (Reduced r))))
         :% Fold 0 IdSym0 IdSym0 (Num_ (Reduced r))))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rational -> Rational
forall a. Fractional a => a -> a
recip (Rational -> Rational)
-> (SRational r -> Rational) -> SRational r -> Rational
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sing r -> Demote Rational
SRational r -> Rational
forall k (a :: k). SingKind k => Sing a -> Demote k
forall (a :: Rational). Sing a -> Demote Rational
fromSing

-- | Like 'sRecip', except it fails with 'Nothing' when @r@ is zero, rather
-- than requiring to satisfy this as a type-level constraint.
sRecip' :: forall r. SRational r -> Maybe (SRational (Recip r))
sRecip' :: forall (r :: Rational). SRational r -> Maybe (SRational (Recip r))
sRecip' SRational r
sa = case Sing r -> Demote Rational
forall k (a :: k). SingKind k => Sing a -> Demote k
forall (a :: Rational). Sing a -> Demote Rational
fromSing Sing r
SRational r
sa of
               Demote Rational
0 -> Maybe (SRational (Recip r))
Maybe
  (SRational
     (Reduce
        (Mul_
           (CmpInteger_
              (Fold
                 'EQ
                 (ConstSym1 'LT)
                 (ConstSym1 'GT)
                 (FromNatural (Den_ (Reduced_ r (Reduce r)))))
              'EQ
              (Fold 0 IdSym0 IdSym0 (FromNatural (Den_ (Reduced_ r (Reduce r)))))
              0)
           (CmpInteger_
              (Fold
                 'EQ
                 (ConstSym1 'LT)
                 (ConstSym1 'GT)
                 (Fold
                    Z
                    (ConstSym1 (N 1))
                    (ConstSym1 (P 1))
                    (Num_ (Reduced_ r (Reduce r)))))
              'EQ
              (Fold
                 0
                 IdSym0
                 IdSym0
                 (Fold
                    Z
                    (ConstSym1 (N 1))
                    (ConstSym1 (P 1))
                    (Num_ (Reduced_ r (Reduce r)))))
              0)
           (Fold 0 IdSym0 IdSym0 (FromNatural (Den_ (Reduced_ r (Reduce r)))))
           (Fold
              0
              IdSym0
              IdSym0
              (Fold
                 Z
                 (ConstSym1 (N 1))
                 (ConstSym1 (P 1))
                 (Num_ (Reduced_ r (Reduce r)))))
         :% Fold 0 IdSym0 IdSym0 (Num_ (Reduced_ r (Reduce r))))))
forall a. Maybe a
Nothing
               Demote Rational
a -> SRational
  (Reduce
     (Mul_
        (CmpInteger_
           (Fold
              'EQ
              (ConstSym1 'LT)
              (ConstSym1 'GT)
              (FromNatural (Den_ (Reduced_ r (Reduce r)))))
           'EQ
           (Fold 0 IdSym0 IdSym0 (FromNatural (Den_ (Reduced_ r (Reduce r)))))
           0)
        (CmpInteger_
           (Fold
              'EQ
              (ConstSym1 'LT)
              (ConstSym1 'GT)
              (Fold
                 Z
                 (ConstSym1 (N 1))
                 (ConstSym1 (P 1))
                 (Num_ (Reduced_ r (Reduce r)))))
           'EQ
           (Fold
              0
              IdSym0
              IdSym0
              (Fold
                 Z
                 (ConstSym1 (N 1))
                 (ConstSym1 (P 1))
                 (Num_ (Reduced_ r (Reduce r)))))
           0)
        (Fold 0 IdSym0 IdSym0 (FromNatural (Den_ (Reduced_ r (Reduce r)))))
        (Fold
           0
           IdSym0
           IdSym0
           (Fold
              Z
              (ConstSym1 (N 1))
              (ConstSym1 (P 1))
              (Num_ (Reduced_ r (Reduce r)))))
      :% Fold 0 IdSym0 IdSym0 (Num_ (Reduced_ r (Reduce r)))))
-> Maybe
     (SRational
        (Reduce
           (Mul_
              (CmpInteger_
                 (Fold
                    'EQ
                    (ConstSym1 'LT)
                    (ConstSym1 'GT)
                    (FromNatural (Den_ (Reduced_ r (Reduce r)))))
                 'EQ
                 (Fold 0 IdSym0 IdSym0 (FromNatural (Den_ (Reduced_ r (Reduce r)))))
                 0)
              (CmpInteger_
                 (Fold
                    'EQ
                    (ConstSym1 'LT)
                    (ConstSym1 'GT)
                    (Fold
                       Z
                       (ConstSym1 (N 1))
                       (ConstSym1 (P 1))
                       (Num_ (Reduced_ r (Reduce r)))))
                 'EQ
                 (Fold
                    0
                    IdSym0
                    IdSym0
                    (Fold
                       Z
                       (ConstSym1 (N 1))
                       (ConstSym1 (P 1))
                       (Num_ (Reduced_ r (Reduce r)))))
                 0)
              (Fold 0 IdSym0 IdSym0 (FromNatural (Den_ (Reduced_ r (Reduce r)))))
              (Fold
                 0
                 IdSym0
                 IdSym0
                 (Fold
                    Z
                    (ConstSym1 (N 1))
                    (ConstSym1 (P 1))
                    (Num_ (Reduced_ r (Reduce r)))))
            :% Fold 0 IdSym0 IdSym0 (Num_ (Reduced_ r (Reduce r))))))
forall a. a -> Maybe a
Just (Rational
-> SRational
     (Reduce
        (Mul_
           (CmpInteger_
              (Fold
                 'EQ
                 (ConstSym1 'LT)
                 (ConstSym1 'GT)
                 (FromNatural (Den_ (Reduced_ r (Reduce r)))))
              'EQ
              (Fold 0 IdSym0 IdSym0 (FromNatural (Den_ (Reduced_ r (Reduce r)))))
              0)
           (CmpInteger_
              (Fold
                 'EQ
                 (ConstSym1 'LT)
                 (ConstSym1 'GT)
                 (Fold
                    Z
                    (ConstSym1 (N 1))
                    (ConstSym1 (P 1))
                    (Num_ (Reduced_ r (Reduce r)))))
              'EQ
              (Fold
                 0
                 IdSym0
                 IdSym0
                 (Fold
                    Z
                    (ConstSym1 (N 1))
                    (ConstSym1 (P 1))
                    (Num_ (Reduced_ r (Reduce r)))))
              0)
           (Fold 0 IdSym0 IdSym0 (FromNatural (Den_ (Reduced_ r (Reduce r)))))
           (Fold
              0
              IdSym0
              IdSym0
              (Fold
                 Z
                 (ConstSym1 (N 1))
                 (ConstSym1 (P 1))
                 (Num_ (Reduced_ r (Reduce r)))))
         :% Fold 0 IdSym0 IdSym0 (Num_ (Reduced_ r (Reduce r)))))
forall (r :: Rational). Rational -> SRational r
UnsafeSRational (Rational -> Rational
forall a. Fractional a => a -> a
recip Rational
Demote Rational
a))

-- | /'Recip'rocal/ of the type-level 'Rational'.
-- Also known as /multiplicative inverse/.
type Recip (a :: Rational) = Den a % Num a :: Rational

data RecipSym0 :: Rational ~> Rational
type RecipSym1 :: Rational -> Rational

type instance Apply RecipSym0 i = Recip i
type RecipSym1 i = Recip i

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

-- | Singleton version of 'Div'.
sDiv :: I.SRound r -> SRational a -> SInteger (Div r a)
sDiv :: forall (r :: Round) (a :: Rational).
SRound r -> SRational a -> SInteger (Div r a)
sDiv SRound r
sr SRational a
sa = Demote Integer
-> (forall (a :: Integer).
    Sing a
    -> SInteger
         (Div_
            r
            (Normalized (Num_ (Reduced_ (Reduce a) (Reduce (Reduce a)))))
            (Normalized
               (FromNatural (Den_ (Reduced_ (Reduce a) (Reduce (Reduce a))))))))
-> SInteger
     (Div_
        r
        (Normalized (Num_ (Reduced_ (Reduce a) (Reduce (Reduce a)))))
        (Normalized
           (FromNatural (Den_ (Reduced_ (Reduce a) (Reduce (Reduce a)))))))
forall k r.
SingKind k =>
Demote k -> (forall (a :: k). Sing a -> r) -> r
withSomeSing (Round -> Rational -> Integer
div (Sing r -> Demote Round
forall k (a :: k). SingKind k => Sing a -> Demote k
forall (a :: Round). Sing a -> Demote Round
fromSing SRound r
Sing r
sr) (Sing a -> Demote Rational
forall k (a :: k). SingKind k => Sing a -> Demote k
forall (a :: Rational). Sing a -> Demote Rational
fromSing Sing a
SRational a
sa)) SInteger a
-> SInteger
     (Div_
        r
        (Normalized (Num_ (Reduced_ (Reduce a) (Reduce (Reduce a)))))
        (Normalized
           (FromNatural (Den_ (Reduced_ (Reduce a) (Reduce (Reduce a)))))))
Sing a
-> SInteger
     (Div_
        r
        (Normalized (Num_ (Reduced_ (Reduce a) (Reduce (Reduce a)))))
        (Normalized
           (FromNatural (Den_ (Reduced_ (Reduce a) (Reduce (Reduce a)))))))
forall a b. a -> b
forall (a :: Integer).
Sing a
-> SInteger
     (Div_
        r
        (Normalized (Num_ (Reduced_ (Reduce a) (Reduce (Reduce a)))))
        (Normalized
           (FromNatural (Den_ (Reduced_ (Reduce a) (Reduce (Reduce a)))))))
unsafeCoerce

-- | Quotient of the 'Div'ision of the 'Num'erator of type-level 'Rational' @a@
-- by its 'Den'ominator, using the specified 'I.Round'ing @r@.
--
-- @
-- forall (r :: 'I.Round') (a :: 'Rational').
--   ('KnownRational' a) =>
--     'Rem' r a  '=='  a '-' 'Div' r a t'%' 1
-- @
--
-- Use this to approximate a type-level 'Rational' to an 'Integer'.
type Div (r :: I.Round) (a :: Rational) = Div_ r (Reduce a) :: Integer
type Div_ (r :: I.Round) (a :: Rational) =
  I.Div r (Num a) (I.FromNatural (Den a)) :: Integer

data DivSym0 :: I.Round ~> Rational ~> Integer
data DivSym1 :: I.Round -> Rational ~> Integer
type DivSym2 :: I.Round -> Rational -> Integer

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

-- | Singleton version of 'Rem'.
sRem :: I.SRound r -> SRational a -> SRational (Rem r a)
sRem :: forall (r :: Round) (a :: Rational).
SRound r -> SRational a -> SRational (Rem r a)
sRem SRound r
sr SRational a
sa = (SInteger
   (Div_
      r
      (Normalized (Num (Reduce a)))
      (Normalized (FromNatural (Den (Reduce a))))),
 SRational
   (Reduce
      (Add_
         (CmpInteger_
            (Fold
               'EQ (ConstSym1 'LT) (ConstSym1 'GT) (Normalized (Num (Reduce a))))
            'EQ
            (Fold 0 IdSym0 IdSym0 (Normalized (Num (Reduce a))))
            0)
         (CmpInteger_
            (Fold
               'EQ
               (ConstSym1 'LT)
               (ConstSym1 'GT)
               (Fold
                  Z
                  PSym0
                  NSym0
                  (Mul_
                     (CmpInteger_
                        (Fold
                           'EQ
                           (ConstSym1 'LT)
                           (ConstSym1 'GT)
                           (Normalized (FromNatural (Den (Reduce a)))))
                        'EQ
                        (Fold 0 IdSym0 IdSym0 (Normalized (FromNatural (Den (Reduce a)))))
                        0)
                     (CmpInteger_
                        (Fold
                           'EQ
                           (ConstSym1 'LT)
                           (ConstSym1 'GT)
                           (Div_
                              r
                              (Normalized (Normalized (Num (Reduce a))))
                              (Normalized (Normalized (FromNatural (Den (Reduce a)))))))
                        'EQ
                        (Fold
                           0
                           IdSym0
                           IdSym0
                           (Div_
                              r
                              (Normalized (Normalized (Num (Reduce a))))
                              (Normalized (Normalized (FromNatural (Den (Reduce a)))))))
                        0)
                     (Fold 0 IdSym0 IdSym0 (Normalized (FromNatural (Den (Reduce a)))))
                     (Fold
                        0
                        IdSym0
                        IdSym0
                        (Div_
                           r
                           (Normalized (Normalized (Num (Reduce a))))
                           (Normalized (Normalized (FromNatural (Den (Reduce a))))))))))
            'EQ
            (Fold
               0
               IdSym0
               IdSym0
               (Fold
                  Z
                  PSym0
                  NSym0
                  (Mul_
                     (CmpInteger_
                        (Fold
                           'EQ
                           (ConstSym1 'LT)
                           (ConstSym1 'GT)
                           (Normalized (FromNatural (Den (Reduce a)))))
                        'EQ
                        (Fold 0 IdSym0 IdSym0 (Normalized (FromNatural (Den (Reduce a)))))
                        0)
                     (CmpInteger_
                        (Fold
                           'EQ
                           (ConstSym1 'LT)
                           (ConstSym1 'GT)
                           (Div_
                              r
                              (Normalized (Normalized (Num (Reduce a))))
                              (Normalized (Normalized (FromNatural (Den (Reduce a)))))))
                        'EQ
                        (Fold
                           0
                           IdSym0
                           IdSym0
                           (Div_
                              r
                              (Normalized (Normalized (Num (Reduce a))))
                              (Normalized (Normalized (FromNatural (Den (Reduce a)))))))
                        0)
                     (Fold 0 IdSym0 IdSym0 (Normalized (FromNatural (Den (Reduce a)))))
                     (Fold
                        0
                        IdSym0
                        IdSym0
                        (Div_
                           r
                           (Normalized (Normalized (Num (Reduce a))))
                           (Normalized (Normalized (FromNatural (Den (Reduce a))))))))))
            0)
         (Fold 0 IdSym0 IdSym0 (Normalized (Num (Reduce a))))
         (Fold
            0
            IdSym0
            IdSym0
            (Fold
               Z
               PSym0
               NSym0
               (Mul_
                  (CmpInteger_
                     (Fold
                        'EQ
                        (ConstSym1 'LT)
                        (ConstSym1 'GT)
                        (Normalized (FromNatural (Den (Reduce a)))))
                     'EQ
                     (Fold 0 IdSym0 IdSym0 (Normalized (FromNatural (Den (Reduce a)))))
                     0)
                  (CmpInteger_
                     (Fold
                        'EQ
                        (ConstSym1 'LT)
                        (ConstSym1 'GT)
                        (Div_
                           r
                           (Normalized (Normalized (Num (Reduce a))))
                           (Normalized (Normalized (FromNatural (Den (Reduce a)))))))
                     'EQ
                     (Fold
                        0
                        IdSym0
                        IdSym0
                        (Div_
                           r
                           (Normalized (Normalized (Num (Reduce a))))
                           (Normalized (Normalized (FromNatural (Den (Reduce a)))))))
                     0)
                  (Fold 0 IdSym0 IdSym0 (Normalized (FromNatural (Den (Reduce a)))))
                  (Fold
                     0
                     IdSym0
                     IdSym0
                     (Div_
                        r
                        (Normalized (Normalized (Num (Reduce a))))
                        (Normalized (Normalized (FromNatural (Den (Reduce a))))))))))
       :% Den (Reduce a))))
-> SRational
     (Reduce
        (Add_
           (CmpInteger_
              (Fold
                 'EQ (ConstSym1 'LT) (ConstSym1 'GT) (Normalized (Num (Reduce a))))
              'EQ
              (Fold 0 IdSym0 IdSym0 (Normalized (Num (Reduce a))))
              0)
           (CmpInteger_
              (Fold
                 'EQ
                 (ConstSym1 'LT)
                 (ConstSym1 'GT)
                 (Fold
                    Z
                    PSym0
                    NSym0
                    (Mul_
                       (CmpInteger_
                          (Fold
                             'EQ
                             (ConstSym1 'LT)
                             (ConstSym1 'GT)
                             (Normalized (FromNatural (Den (Reduce a)))))
                          'EQ
                          (Fold 0 IdSym0 IdSym0 (Normalized (FromNatural (Den (Reduce a)))))
                          0)
                       (CmpInteger_
                          (Fold
                             'EQ
                             (ConstSym1 'LT)
                             (ConstSym1 'GT)
                             (Div_
                                r
                                (Normalized (Normalized (Num (Reduce a))))
                                (Normalized (Normalized (FromNatural (Den (Reduce a)))))))
                          'EQ
                          (Fold
                             0
                             IdSym0
                             IdSym0
                             (Div_
                                r
                                (Normalized (Normalized (Num (Reduce a))))
                                (Normalized (Normalized (FromNatural (Den (Reduce a)))))))
                          0)
                       (Fold 0 IdSym0 IdSym0 (Normalized (FromNatural (Den (Reduce a)))))
                       (Fold
                          0
                          IdSym0
                          IdSym0
                          (Div_
                             r
                             (Normalized (Normalized (Num (Reduce a))))
                             (Normalized (Normalized (FromNatural (Den (Reduce a))))))))))
              'EQ
              (Fold
                 0
                 IdSym0
                 IdSym0
                 (Fold
                    Z
                    PSym0
                    NSym0
                    (Mul_
                       (CmpInteger_
                          (Fold
                             'EQ
                             (ConstSym1 'LT)
                             (ConstSym1 'GT)
                             (Normalized (FromNatural (Den (Reduce a)))))
                          'EQ
                          (Fold 0 IdSym0 IdSym0 (Normalized (FromNatural (Den (Reduce a)))))
                          0)
                       (CmpInteger_
                          (Fold
                             'EQ
                             (ConstSym1 'LT)
                             (ConstSym1 'GT)
                             (Div_
                                r
                                (Normalized (Normalized (Num (Reduce a))))
                                (Normalized (Normalized (FromNatural (Den (Reduce a)))))))
                          'EQ
                          (Fold
                             0
                             IdSym0
                             IdSym0
                             (Div_
                                r
                                (Normalized (Normalized (Num (Reduce a))))
                                (Normalized (Normalized (FromNatural (Den (Reduce a)))))))
                          0)
                       (Fold 0 IdSym0 IdSym0 (Normalized (FromNatural (Den (Reduce a)))))
                       (Fold
                          0
                          IdSym0
                          IdSym0
                          (Div_
                             r
                             (Normalized (Normalized (Num (Reduce a))))
                             (Normalized (Normalized (FromNatural (Den (Reduce a))))))))))
              0)
           (Fold 0 IdSym0 IdSym0 (Normalized (Num (Reduce a))))
           (Fold
              0
              IdSym0
              IdSym0
              (Fold
                 Z
                 PSym0
                 NSym0
                 (Mul_
                    (CmpInteger_
                       (Fold
                          'EQ
                          (ConstSym1 'LT)
                          (ConstSym1 'GT)
                          (Normalized (FromNatural (Den (Reduce a)))))
                       'EQ
                       (Fold 0 IdSym0 IdSym0 (Normalized (FromNatural (Den (Reduce a)))))
                       0)
                    (CmpInteger_
                       (Fold
                          'EQ
                          (ConstSym1 'LT)
                          (ConstSym1 'GT)
                          (Div_
                             r
                             (Normalized (Normalized (Num (Reduce a))))
                             (Normalized (Normalized (FromNatural (Den (Reduce a)))))))
                       'EQ
                       (Fold
                          0
                          IdSym0
                          IdSym0
                          (Div_
                             r
                             (Normalized (Normalized (Num (Reduce a))))
                             (Normalized (Normalized (FromNatural (Den (Reduce a)))))))
                       0)
                    (Fold 0 IdSym0 IdSym0 (Normalized (FromNatural (Den (Reduce a)))))
                    (Fold
                       0
                       IdSym0
                       IdSym0
                       (Div_
                          r
                          (Normalized (Normalized (Num (Reduce a))))
                          (Normalized (Normalized (FromNatural (Den (Reduce a))))))))))
         :% Den (Reduce a)))
forall a b. (a, b) -> b
snd (SRound r
-> SRational a
-> (SInteger
      (Div_
         r
         (Normalized (Num (Reduce a)))
         (Normalized (FromNatural (Den (Reduce a))))),
    SRational
      (Snd
         '(Fst (DivRem r (Num (Reduce a)) (FromNatural (Den (Reduce a)))),
           Reduce
             (Snd (DivRem r (Num (Reduce a)) (FromNatural (Den (Reduce a))))
              :% Den (Reduce a)))))
forall (r :: Round) (a :: Rational).
SRound r
-> SRational a -> (SInteger (Div r a), SRational (Rem r a))
sDivRem SRound r
sr SRational a
sa)

-- | 'Rem'ainder from 'Div'iding the 'Num'erator of the type-level 'Rational'
-- @a@ by its 'Den'ominator, using the specified 'I.Round'ing @r@.
--
-- @
-- forall (r :: 'I.Round') (a :: 'Rational').
--   ('KnownRational' a) =>
--     'Rem' r a  '=='  a '-' 'Div' r a t'%' 1
-- @
type Rem (r :: I.Round) (a :: Rational) = P.Snd (DivRem r a) :: Rational

data RemSym0 :: I.Round ~> Rational ~> Rational
data RemSym1 :: I.Round -> Rational ~> Rational
type RemSym2 :: I.Round -> Rational -> Rational

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

-- | Singleton version of 'DivRem'.
sDivRem :: I.SRound r -> SRational a
        -> (SInteger (Div r a), SRational (Rem r a))
sDivRem :: forall (r :: Round) (a :: Rational).
SRound r
-> SRational a -> (SInteger (Div r a), SRational (Rem r a))
sDivRem SRound r
sr SRational a
sa =
  let (Integer
d1, Rational
r1) = Round -> Rational -> (Integer, Rational)
divRem (Sing r -> Demote Round
forall k (a :: k). SingKind k => Sing a -> Demote k
forall (a :: Round). Sing a -> Demote Round
fromSing SRound r
Sing r
sr) (Sing a -> Demote Rational
forall k (a :: k). SingKind k => Sing a -> Demote k
forall (a :: Rational). Sing a -> Demote Rational
fromSing Sing a
SRational a
sa)
  in (Demote Integer
-> (forall (a :: Integer).
    Sing a
    -> SInteger
         (Div_
            r
            (Normalized (Num_ (Reduced_ (Reduce a) (Reduce (Reduce a)))))
            (Normalized
               (FromNatural (Den_ (Reduced_ (Reduce a) (Reduce (Reduce a))))))))
-> SInteger
     (Div_
        r
        (Normalized (Num_ (Reduced_ (Reduce a) (Reduce (Reduce a)))))
        (Normalized
           (FromNatural (Den_ (Reduced_ (Reduce a) (Reduce (Reduce a)))))))
forall k r.
SingKind k =>
Demote k -> (forall (a :: k). Sing a -> r) -> r
withSomeSing Integer
Demote Integer
d1 SInteger a
-> SInteger
     (Div_
        r
        (Normalized (Num_ (Reduced_ (Reduce a) (Reduce (Reduce a)))))
        (Normalized
           (FromNatural (Den_ (Reduced_ (Reduce a) (Reduce (Reduce a)))))))
Sing a
-> SInteger
     (Div_
        r
        (Normalized (Num_ (Reduced_ (Reduce a) (Reduce (Reduce a)))))
        (Normalized
           (FromNatural (Den_ (Reduced_ (Reduce a) (Reduce (Reduce a)))))))
forall a b. a -> b
forall (a :: Integer).
Sing a
-> SInteger
     (Div_
        r
        (Normalized (Num_ (Reduced_ (Reduce a) (Reduce (Reduce a)))))
        (Normalized
           (FromNatural (Den_ (Reduced_ (Reduce a) (Reduce (Reduce a)))))))
unsafeCoerce, Rational
-> SRational
     (Reduce
        (Add_
           (CmpInteger_
              (Fold
                 'EQ
                 (ConstSym1 'LT)
                 (ConstSym1 'GT)
                 (Normalized (Num_ (Reduced_ (Reduce a) (Reduce (Reduce a))))))
              'EQ
              (Fold
                 0
                 IdSym0
                 IdSym0
                 (Normalized (Num_ (Reduced_ (Reduce a) (Reduce (Reduce a))))))
              0)
           (CmpInteger_
              (Fold
                 'EQ
                 (ConstSym1 'LT)
                 (ConstSym1 'GT)
                 (Fold
                    Z
                    PSym0
                    NSym0
                    (Mul_
                       (CmpInteger_
                          (Fold
                             'EQ
                             (ConstSym1 'LT)
                             (ConstSym1 'GT)
                             (Normalized
                                (FromNatural (Den_ (Reduced_ (Reduce a) (Reduce (Reduce a)))))))
                          'EQ
                          (Fold
                             0
                             IdSym0
                             IdSym0
                             (Normalized
                                (FromNatural (Den_ (Reduced_ (Reduce a) (Reduce (Reduce a)))))))
                          0)
                       (CmpInteger_
                          (Fold
                             'EQ
                             (ConstSym1 'LT)
                             (ConstSym1 'GT)
                             (Div_
                                r
                                (Normalized
                                   (Normalized (Num_ (Reduced_ (Reduce a) (Reduce (Reduce a))))))
                                (Normalized
                                   (Normalized
                                      (FromNatural
                                         (Den_ (Reduced_ (Reduce a) (Reduce (Reduce a)))))))))
                          'EQ
                          (Fold
                             0
                             IdSym0
                             IdSym0
                             (Div_
                                r
                                (Normalized
                                   (Normalized (Num_ (Reduced_ (Reduce a) (Reduce (Reduce a))))))
                                (Normalized
                                   (Normalized
                                      (FromNatural
                                         (Den_ (Reduced_ (Reduce a) (Reduce (Reduce a)))))))))
                          0)
                       (Fold
                          0
                          IdSym0
                          IdSym0
                          (Normalized
                             (FromNatural (Den_ (Reduced_ (Reduce a) (Reduce (Reduce a)))))))
                       (Fold
                          0
                          IdSym0
                          IdSym0
                          (Div_
                             r
                             (Normalized
                                (Normalized (Num_ (Reduced_ (Reduce a) (Reduce (Reduce a))))))
                             (Normalized
                                (Normalized
                                   (FromNatural
                                      (Den_ (Reduced_ (Reduce a) (Reduce (Reduce a))))))))))))
              'EQ
              (Fold
                 0
                 IdSym0
                 IdSym0
                 (Fold
                    Z
                    PSym0
                    NSym0
                    (Mul_
                       (CmpInteger_
                          (Fold
                             'EQ
                             (ConstSym1 'LT)
                             (ConstSym1 'GT)
                             (Normalized
                                (FromNatural (Den_ (Reduced_ (Reduce a) (Reduce (Reduce a)))))))
                          'EQ
                          (Fold
                             0
                             IdSym0
                             IdSym0
                             (Normalized
                                (FromNatural (Den_ (Reduced_ (Reduce a) (Reduce (Reduce a)))))))
                          0)
                       (CmpInteger_
                          (Fold
                             'EQ
                             (ConstSym1 'LT)
                             (ConstSym1 'GT)
                             (Div_
                                r
                                (Normalized
                                   (Normalized (Num_ (Reduced_ (Reduce a) (Reduce (Reduce a))))))
                                (Normalized
                                   (Normalized
                                      (FromNatural
                                         (Den_ (Reduced_ (Reduce a) (Reduce (Reduce a)))))))))
                          'EQ
                          (Fold
                             0
                             IdSym0
                             IdSym0
                             (Div_
                                r
                                (Normalized
                                   (Normalized (Num_ (Reduced_ (Reduce a) (Reduce (Reduce a))))))
                                (Normalized
                                   (Normalized
                                      (FromNatural
                                         (Den_ (Reduced_ (Reduce a) (Reduce (Reduce a)))))))))
                          0)
                       (Fold
                          0
                          IdSym0
                          IdSym0
                          (Normalized
                             (FromNatural (Den_ (Reduced_ (Reduce a) (Reduce (Reduce a)))))))
                       (Fold
                          0
                          IdSym0
                          IdSym0
                          (Div_
                             r
                             (Normalized
                                (Normalized (Num_ (Reduced_ (Reduce a) (Reduce (Reduce a))))))
                             (Normalized
                                (Normalized
                                   (FromNatural
                                      (Den_ (Reduced_ (Reduce a) (Reduce (Reduce a))))))))))))
              0)
           (Fold
              0
              IdSym0
              IdSym0
              (Normalized (Num_ (Reduced_ (Reduce a) (Reduce (Reduce a))))))
           (Fold
              0
              IdSym0
              IdSym0
              (Fold
                 Z
                 PSym0
                 NSym0
                 (Mul_
                    (CmpInteger_
                       (Fold
                          'EQ
                          (ConstSym1 'LT)
                          (ConstSym1 'GT)
                          (Normalized
                             (FromNatural (Den_ (Reduced_ (Reduce a) (Reduce (Reduce a)))))))
                       'EQ
                       (Fold
                          0
                          IdSym0
                          IdSym0
                          (Normalized
                             (FromNatural (Den_ (Reduced_ (Reduce a) (Reduce (Reduce a)))))))
                       0)
                    (CmpInteger_
                       (Fold
                          'EQ
                          (ConstSym1 'LT)
                          (ConstSym1 'GT)
                          (Div_
                             r
                             (Normalized
                                (Normalized (Num_ (Reduced_ (Reduce a) (Reduce (Reduce a))))))
                             (Normalized
                                (Normalized
                                   (FromNatural
                                      (Den_ (Reduced_ (Reduce a) (Reduce (Reduce a)))))))))
                       'EQ
                       (Fold
                          0
                          IdSym0
                          IdSym0
                          (Div_
                             r
                             (Normalized
                                (Normalized (Num_ (Reduced_ (Reduce a) (Reduce (Reduce a))))))
                             (Normalized
                                (Normalized
                                   (FromNatural
                                      (Den_ (Reduced_ (Reduce a) (Reduce (Reduce a)))))))))
                       0)
                    (Fold
                       0
                       IdSym0
                       IdSym0
                       (Normalized
                          (FromNatural (Den_ (Reduced_ (Reduce a) (Reduce (Reduce a)))))))
                    (Fold
                       0
                       IdSym0
                       IdSym0
                       (Div_
                          r
                          (Normalized
                             (Normalized (Num_ (Reduced_ (Reduce a) (Reduce (Reduce a))))))
                          (Normalized
                             (Normalized
                                (FromNatural
                                   (Den_ (Reduced_ (Reduce a) (Reduce (Reduce a))))))))))))
         :% Den_ (Reduced_ (Reduce a) (Reduce (Reduce a)))))
forall (r :: Rational). Rational -> SRational r
UnsafeSRational Rational
r1)

-- | Get both the quotient and the 'Rem'ainder of the 'Div'ision of the
-- 'Num'erator of type-level 'Rational' @a@ by its 'Den'ominator,
-- using the specified 'I.Round'ing @r@.
--
-- @
-- forall (r :: 'I.Round') (a :: 'Rational').
--   ('KnownRational' a) =>
--     'DivRem' r a  '=='  '('Div' r a, 'Rem' r a)
-- @
type DivRem (r :: I.Round) (a :: Rational) =
  DivRem_ r (Reduce a) :: (Integer, Rational)
type DivRem_ (r :: I.Round) (a :: Rational) =
  DivRem__ (Den a) (I.DivRem r (Num a) (I.FromNatural (Den a)))
    :: (Integer, Rational)
type DivRem__ (d :: Natural) (qm :: (Integer, Integer)) =
  '(P.Fst qm, Reduce (P.Snd qm :% d)) :: (Integer, Rational)

data DivRemSym0 :: I.Round ~> Rational ~> (Integer, Rational)
data DivRemSym1 :: I.Round -> Rational ~> (Integer, Rational)
type DivRemSym2 :: I.Round -> Rational -> (Integer, Rational)

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

-- | Term-level version of 'Div'.
--
-- Takes a "KindRational".'Rational' as input, returns a "Prelude"
-- 'P.Integer'.
--
-- NB: 'error's if the 'P.Rational' denominator is 0.
div :: I.Round -> P.Rational -> P.Integer
div :: Round -> Rational -> Integer
div Round
rnd = \(HasCallStack => Rational -> Rational
Rational -> Rational
unsafeReduce -> Integer
n P.:% Integer
d) -> Integer -> Integer -> Integer
f Integer
n Integer
d
  where f :: Integer -> Integer -> Integer
f = Round -> Integer -> Integer -> Integer
I.div Round
rnd

-- | Term-level version of 'Rem'.
--
-- Takes a "Prelude".'P.Rational' as input, returns a "Prelude".'P.Rational'.
--
-- NB: 'error's if the 'P.Rational' denominator is 0.
rem :: I.Round -> P.Rational -> P.Rational
rem :: Round -> Rational -> Rational
rem Round
rnd = (Integer, Rational) -> Rational
forall a b. (a, b) -> b
snd ((Integer, Rational) -> Rational)
-> (Rational -> (Integer, Rational)) -> Rational -> Rational
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Round -> Rational -> (Integer, Rational)
divRem Round
rnd

-- | Term-level version of 'DivRem'.
--
-- Takes a "Prelude".'P.Rational' as input, returns a pair of
-- /(quotient, reminder)/.
--
-- @
-- forall ('r' :: 'I.Round') (a :: 'P.Rational').
--   ('P.denominator' a 'P./=' 0) =>
--     'divRem' r a  'P.=='  ('div' r a, 'rem' r a)
-- @
--
-- NB: 'error's if the 'P.Rational' denominator is 0.
divRem :: I.Round -> P.Rational -> (P.Integer, P.Rational)
divRem :: Round -> Rational -> (Integer, Rational)
divRem Round
rnd = \(HasCallStack => Rational -> Rational
Rational -> Rational
unsafeReduce -> Integer
n P.:% Integer
d) ->
                 let (Integer
q, Integer
m) = Integer -> Integer -> (Integer, Integer)
f Integer
n Integer
d
                 in  (Integer
q, Integer
m Integer -> Integer -> Rational
forall a. a -> a -> Ratio a
P.:% Integer
d) -- (m :% d) == ((n :% d) - q)
  where f :: Integer -> Integer -> (Integer, Integer)
f = Round -> Integer -> Integer -> (Integer, Integer)
I.divRem Round
rnd

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

-- | Determine whether @r@ is 'Terminating' or 'NonTerminating' at the
-- term-level, and create the corresponding type-level proof.
termination
  :: forall r a
  .  (NonTerminating r => a)
  -> (Terminating r => a)
  -> SRational r
  -> a
termination :: forall (r :: Rational) a.
(NonTerminating r => a) -> (Terminating r => a) -> SRational r -> a
termination NonTerminating r => a
f Terminating r => a
t SRational r
sr =
  SRational r -> (KnownRational r => a) -> a
forall (r :: Rational) x.
SRational r -> (KnownRational r => x) -> x
withKnownRational SRational r
sr ((KnownRational r => a) -> a) -> (KnownRational r => a) -> a
forall a b. (a -> b) -> a -> b
$ case Rational -> Bool
isTerminating (SRational r -> Rational
forall (r :: Rational). SRational r -> Rational
fromSRational SRational r
sr) of
    Bool
False | IsTerminating r :~: 'False
Refl <- ((Any :~: Any) -> IsTerminating_ (Den_ r) :~: 'False
forall a b. a -> b
unsafeCoerce Any :~: Any
forall {k} (a :: k). a :~: a
Refl :: IsTerminating r :~: 'False) -> a
NonTerminating r => a
f
    Bool
True  | IsTerminating r :~: 'True
Refl <- ((Any :~: Any) -> IsTerminating_ (Den_ r) :~: 'True
forall a b. a -> b
unsafeCoerce Any :~: Any
forall {k} (a :: k). a :~: a
Refl :: IsTerminating r :~: 'True)  -> a
Terminating r => a
t

-- | This is essentially the same as @('KnownRational' r, 'IsTerminating' r ~ 'True')@,
-- except with a nicer error message when @'IsTerminating' r ~ 'False'@.
type Terminating (r :: Rational) = Terminating_ r (IsTerminating r) :: Constraint
type family Terminating_ r (b :: Bool):: Constraint where
  Terminating_ r 'True = (IsTerminating r ~ 'True, KnownRational r)
  Terminating_ r 'False = L.TypeError
    ('L.Text "Unexpected: IsTerminating ("
     'L.:<>: 'L.ShowType r 'L.:<>: 'L.Text ") ~ 'False")

data TerminatingSym0 :: Rational ~> Constraint
type TerminatingSym1 :: Rational -> Constraint

type instance Apply TerminatingSym0 i = Terminating i
type TerminatingSym1 i = Terminating i

-- | This is essentially the same as @('KnownRational' r, 'IsTerminating' r ~ 'False')@,
-- except with a nicer error message when @'IsTerminating' r ~ 'False'@.
type NonTerminating (r :: Rational) = NonTerminating_ r (IsTerminating r) :: Constraint
type family NonTerminating_ r (b :: Bool):: Constraint where
  NonTerminating_ r 'False = (IsTerminating r ~ 'False, KnownRational r)
  NonTerminating_ r 'True  = L.TypeError
    ('L.Text "Unexpected: IsTerminating ("
     'L.:<>: 'L.ShowType r 'L.:<>: 'L.Text ") ~ 'True")

data NonTerminatingSym0 :: Rational ~> Constraint
type NonTerminatingSym1 :: Rational -> Constraint

type instance Apply NonTerminatingSym0 i = NonTerminating i
type NonTerminatingSym1 i = NonTerminating i


-- | Whether the type-level 'Rational' is terminating. That is, whether
-- it can be fully represented as a finite decimal number.
type IsTerminating (r :: Rational) = IsTerminating_ (Den r) :: Bool
type family IsTerminating_ (n :: Natural) :: Bool where
  IsTerminating_ 5 = 'True
  IsTerminating_ 2 = 'True
  IsTerminating_ 1 = 'True
  IsTerminating_ d = IsTerminating_5 d (L.Mod d 5)

-- @IsTerminating_5@ is here to prevent @IsTerminating_@ from recursing into
-- @IsTerminating_ (Div d 5)@ if it would diverge.
type family IsTerminating_5 (d :: Natural) (md5 :: Natural) :: Bool where
  IsTerminating_5 d 0 = IsTerminating_ (L.Div d 5)
  IsTerminating_5 d _ = IsTerminating_2 d (L.Mod d 2)

-- @IsTerminating_2@ is here to prevent @IsTerminating_5@ from recursing into
-- @IsTerminating_ (Div d 2)@ if it would diverge, and also to prevent calculating
-- @Mod d 2@ unless necessary.
type family IsTerminating_2 (d :: Natural) (md2 :: Natural) :: Bool where
  IsTerminating_2 d 0 = IsTerminating_ (L.Div d 2)
  IsTerminating_2 _ _ = 'False

data IsTerminatingSym0 :: Rational ~> Bool
type IsTerminatingSym1 :: Rational -> Bool

type instance Apply IsTerminatingSym0 i = IsTerminating i
type IsTerminatingSym1 i = IsTerminating i

-- | Term-level version of the "IsTerminating" function.
--
-- NB: 'error's if the 'P.Rational' denominator is 0.
isTerminating :: P.Rational -> Bool
isTerminating :: Rational -> Bool
isTerminating = \(HasCallStack => Rational -> Rational
Rational -> Rational
unsafeReduce -> Integer
_ P.:% Integer
d) -> Integer -> Bool
go Integer
d
  where
    go :: Integer -> Bool
go = \case
      Integer
5 -> Bool
True
      Integer
2 -> Bool
True
      Integer
1 -> Bool
True
      Integer
n | (Integer
q, Integer
0) <- Integer -> Integer -> (Integer, Integer)
forall a. Integral a => a -> a -> (a, a)
P.divMod Integer
n Integer
5 -> Integer -> Bool
go Integer
q
        | (Integer
q, Integer
0) <- Integer -> Integer -> (Integer, Integer)
forall a. Integral a => a -> a -> (a, a)
P.divMod Integer
n Integer
2 -> Integer -> Bool
go Integer
q
      Integer
_ -> Bool
False

{-# COMPLETE SRationalTerminating, SRationalNonTerminating #-}

-- | Matches a 'SRational' that is 'Terminating'.
pattern SRationalTerminating
  :: forall r. () => (Terminating r) => SRational r
pattern $mSRationalTerminating :: forall {r} {r :: Rational}.
SRational r -> (Terminating r => r) -> ((# #) -> r) -> r
SRationalTerminating <-
  (termination Nothing (Just Dict) -> Just (Dict :: Dict (Terminating r)))

-- | Matches a 'SRational' that is 'NonTerminating'.
pattern SRationalNonTerminating
  :: forall r. () => (NonTerminating r) => SRational r
pattern $mSRationalNonTerminating :: forall {r} {r :: Rational}.
SRational r -> (NonTerminating r => r) -> ((# #) -> r) -> r
SRationalNonTerminating <-
  (termination (Just Dict) Nothing -> Just (Dict :: Dict (NonTerminating r)))

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

-- | Comparison of type-level 'Rational's, as a function.
type CmpRational (a :: Rational) (b :: Rational) =
  CmpRational_ (Reduce a) (Reduce b) :: Ordering
type family CmpRational_ (a :: Rational) (b :: Rational) :: Ordering where
  CmpRational_ a a = 'EQ
  CmpRational_ (an :% ad) (bn :% bd) =
    P.Compare (an P.* I.FromNatural bd) (bn P.* I.FromNatural ad)

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

instance OrdS.POrd Rational where
  type Compare a b = CmpRational a b

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

instance EqS.PEq Rational where
  type a == b = CmpRational a b P.== 'EQ

instance EqS.SEq Rational where
  Sing t1
sa %== :: forall (t1 :: Rational) (t2 :: Rational).
Sing t1 -> Sing t2 -> Sing (Apply (Apply (==@#@$) t1) t2)
%== Sing t2
sb
    | Sing t1 -> Demote Rational
forall k (a :: k). SingKind k => Sing a -> Demote k
forall (a :: Rational). Sing a -> Demote Rational
fromSing Sing t1
sa Demote Rational -> Demote Rational -> Bool
forall a. Eq a => a -> a -> Bool
P.== Sing t2 -> Demote Rational
forall k (a :: k). SingKind k => Sing a -> Demote k
forall (a :: Rational). Sing a -> Demote Rational
fromSing Sing t2
sb = SBool 'True
-> SBool
     (TFHelper_6989586621679145179
        (CmpRational_ (Reduce t1) (Reduce t2)) 'EQ)
forall a b. a -> b
unsafeCoerce SBool 'True
STrue
    | Bool
otherwise                    = SBool 'False
-> SBool
     (TFHelper_6989586621679145179
        (CmpRational_ (Reduce t1) (Reduce t2)) 'EQ)
forall a b. a -> b
unsafeCoerce SBool 'False
SFalse

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

-- | This class gives the 'SRational' associated with a type-level 'Rational'.
--
-- There are instances for every 'Reduced' 'Rational'.

-- Note: Ideally, 'KnownRational' wouldn' exist and the 'Constraint's metioned
-- there would be superclasses to 'KnownRational_'. However, 'withDict' doesn't
-- allow superclasses, so we treat 'KnownRational_' as internal an export
-- 'KnownRational' only.
class KnownRational_ (r :: Rational) where
  rationalSing_ :: SRational r

-- | Type-level 'Rational's satisfying 'KnownRational' can be converted to
-- 'SRational's using 'rationalSing'. Moreover, 'KnownRational' implies that
-- the numerator is a 'I.KnownInteger', and that the denominator is a
-- 'L.KnownNat'.
type KnownRational (r :: Rational) =
  ( KnownRational_ r
  , Reduced r ~ r
  , I.KnownInteger (Num r)
  , L.KnownNat (Den r)
  )

-- | Convert an implicit 'KnownRational' to an explicit 'SRational'.
rationalSing :: KnownRational r => SRational r
rationalSing :: forall (r :: Rational). KnownRational r => SRational r
rationalSing = SRational r
forall (r :: Rational). KnownRational_ r => SRational r
rationalSing_ -- The difference is in the constraint.
{-# INLINE rationalSing #-}

instance (KnownRational r) => KnownRational_ r where
  rationalSing_ :: SRational r
rationalSing_ =
    Rational -> SRational r
forall (r :: Rational). Rational -> SRational r
UnsafeSRational (forall {k} (a :: k). (SingKind k, SingI a) => Demote k
forall (a :: Integer).
(SingKind Integer, SingI a) =>
Demote Integer
demote @(Num r) Integer -> Integer -> Rational
forall a. a -> a -> Ratio a
P.:% Proxy (Den_ r) -> 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 @(Den r)))

-- | Normalized term-level "Prelude" 'P.Rational' representation of the
-- type-level 'Rational' @r@.
rationalVal :: forall r proxy. KnownRational r => proxy r -> P.Rational
rationalVal :: forall (r :: Rational) (proxy :: Rational -> Type).
KnownRational r =>
proxy r -> Rational
rationalVal proxy r
_ = case SRational r
forall (r :: Rational). KnownRational r => SRational r
rationalSing :: SRational r of UnsafeSRational Rational
x -> Rational
x
{-# INLINE rationalVal #-}

-- | This type represents unknown type-level 'Rational'.
data SomeRational = forall n. KnownRational n => SomeRational (Proxy n)


-- | Convert a term-level "Prelude".'P.Rational' into an
-- extistentialized 'KnownRational' wrapped in 'SomeRational'.
--
-- NB: 'error's if a non-'Reduced' 'P.Rational' is given.
someRationalVal :: P.Rational -> SomeRational
someRationalVal :: Rational -> SomeRational
someRationalVal = \Rational
r ->
  Rational
-> (forall {r :: Rational}. SRational r -> SomeRational)
-> SomeRational
forall x.
Rational -> (forall (r :: Rational). SRational r -> x) -> x
withSomeSRational Rational
r ((forall {r :: Rational}. SRational r -> SomeRational)
 -> SomeRational)
-> (forall {r :: Rational}. SRational r -> SomeRational)
-> SomeRational
forall a b. (a -> b) -> a -> b
$ \(SRational r
sr :: SRational r) ->
  SRational r -> (KnownRational r => SomeRational) -> SomeRational
forall (r :: Rational) x.
SRational r -> (KnownRational r => x) -> x
withKnownRational SRational r
sr ((KnownRational r => SomeRational) -> SomeRational)
-> (KnownRational r => SomeRational) -> SomeRational
forall a b. (a -> b) -> a -> b
$ Proxy r -> SomeRational
forall (n :: Rational). KnownRational n => Proxy n -> SomeRational
SomeRational (forall {k} (t :: k). Proxy t
forall (t :: Rational). Proxy t
Proxy @r)

instance Eq SomeRational where
  SomeRational Proxy n
x == :: SomeRational -> SomeRational -> Bool
== SomeRational Proxy n
y =
    Proxy n -> Rational
forall (r :: Rational) (proxy :: Rational -> Type).
KnownRational r =>
proxy r -> Rational
rationalVal Proxy n
x Rational -> Rational -> Bool
forall a. Eq a => a -> a -> Bool
P.== Proxy n -> Rational
forall (r :: Rational) (proxy :: Rational -> Type).
KnownRational r =>
proxy r -> Rational
rationalVal Proxy n
y
  {-# INLINE (==) #-}

instance Ord SomeRational where
  compare :: SomeRational -> SomeRational -> Ordering
compare (SomeRational Proxy n
x) (SomeRational Proxy n
y) =
    Rational -> Rational -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (Proxy n -> Rational
forall (r :: Rational) (proxy :: Rational -> Type).
KnownRational r =>
proxy r -> Rational
rationalVal Proxy n
x) (Proxy n -> Rational
forall (r :: Rational) (proxy :: Rational -> Type).
KnownRational r =>
proxy r -> Rational
rationalVal Proxy n
y)
  {-# INLINE compare #-}

-- | As for "Prelude".'P.Rational'.
instance Show SomeRational where
  showsPrec :: Int -> SomeRational -> ShowS
showsPrec Int
p (SomeRational Proxy n
i) = Int -> Rational -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
p (Proxy n -> Rational
forall (r :: Rational) (proxy :: Rational -> Type).
KnownRational r =>
proxy r -> Rational
rationalVal Proxy n
i)

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

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

-- | We either get evidence that this function was instantiated with the
-- same type-level 'Rational's, or 'Nothing'.
sameRational
  :: forall a b proxy1 proxy2
  .  (KnownRational a, KnownRational b)
  => proxy1 a
  -> proxy2 b
  -> Maybe (a :~: b)
sameRational :: forall (a :: Rational) (b :: Rational) (proxy1 :: Rational -> Type)
       (proxy2 :: Rational -> Type).
(KnownRational a, KnownRational b) =>
proxy1 a -> proxy2 b -> Maybe (a :~: b)
sameRational proxy1 a
_ proxy2 b
_ = SRational a -> SRational b -> Maybe (a :~: b)
forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
forall (a :: Rational) (b :: Rational).
SRational a -> SRational b -> Maybe (a :~: b)
testEquality (forall (r :: Rational). KnownRational r => SRational r
rationalSing @a) (forall (r :: Rational). KnownRational r => SRational r
rationalSing @b)

-- | Like 'sameRational', but if the type-level 'Rational's aren't equal, this
-- additionally provides proof of 'LT' or 'GT'.
cmpRational
  :: forall a b proxy1 proxy2
  .  (KnownRational a, KnownRational b)
  => proxy1 a
  -> proxy2 b
  -> OrderingI a b
cmpRational :: forall (a :: Rational) (b :: Rational) (proxy1 :: Rational -> Type)
       (proxy2 :: Rational -> Type).
(KnownRational a, KnownRational b) =>
proxy1 a -> proxy2 b -> OrderingI a b
cmpRational proxy1 a
x proxy2 b
y = case Rational -> Rational -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (proxy1 a -> Rational
forall (r :: Rational) (proxy :: Rational -> Type).
KnownRational r =>
proxy r -> Rational
rationalVal proxy1 a
x) (proxy2 b -> Rational
forall (r :: Rational) (proxy :: Rational -> Type).
KnownRational r =>
proxy r -> Rational
rationalVal proxy2 b
y) of
    Ordering
EQ -> case (Any :~: Any) -> CmpRational_ (Reduce a) (Reduce b) :~: 'EQ
forall a b. a -> b
unsafeCoerce Any :~: Any
forall {k} (a :: k). a :~: a
Refl :: CmpRational a b :~: 'EQ of
      CmpRational_ (Reduce a) (Reduce b) :~: 'EQ
Refl -> case (Any :~: Any) -> a :~: b
forall a b. a -> b
unsafeCoerce Any :~: Any
forall {k} (a :: k). a :~: a
Refl :: a :~: b of
        a :~: b
Refl -> OrderingI a a
OrderingI a b
forall {k} (a :: k). (Compare a a ~ 'EQ) => OrderingI a a
EQI
    Ordering
LT -> case (Any :~: Any) -> CmpRational_ (Reduce a) (Reduce b) :~: 'LT
forall a b. a -> b
unsafeCoerce Any :~: Any
forall {k} (a :: k). a :~: a
Refl :: (CmpRational a b :~: 'LT) of
      CmpRational_ (Reduce a) (Reduce b) :~: 'LT
Refl -> OrderingI a b
forall {k} (a :: k) (b :: k). (Compare a b ~ 'LT) => OrderingI a b
LTI
    Ordering
GT -> case (Any :~: Any) -> CmpRational_ (Reduce a) (Reduce b) :~: 'GT
forall a b. a -> b
unsafeCoerce Any :~: Any
forall {k} (a :: k). a :~: a
Refl :: (CmpRational a b :~: 'GT) of
      CmpRational_ (Reduce a) (Reduce b) :~: 'GT
Refl -> OrderingI a b
forall {k} (a :: k) (b :: k). (Compare a b ~ 'GT) => OrderingI a b
GTI

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

-- | Singleton type for a type-level 'Rational' @r@.
newtype SRational (r :: Rational) = UnsafeSRational P.Rational
type role SRational nominal

-- | A explicitly bidirectional pattern synonym relating an 'SRational' to a
-- 'KnownRational' constraint.
--
-- As an __expression__: Constructs an explicit @'SRational' r@ value from an
-- implicit @'KnownRational' r@ constraint:
--
-- @
-- 'SRational' @r :: 'KnownRational' r => 'SRational' r
-- @
--
-- As a __pattern__: Matches on an explicit @'SRational' r@ value bringing
-- an implicit @'KnownRational' r@ constraint into scope:
--
-- @
-- f :: 'SRational' r -> ..
-- f SRational = {- SRational r in scope -}
-- @
pattern SRational :: forall r. () => KnownRational r => SRational r
pattern $mSRational :: forall {r} {r :: Rational}.
SRational r -> (KnownRational r => r) -> ((# #) -> r) -> r
$bSRational :: forall (r :: Rational). KnownRational r => SRational r
SRational <- (knownRationalInstance -> KnownRationalInstance)
  where SRational = SRational r
forall (r :: Rational). KnownRational_ r => SRational r
rationalSing_

-- | An internal data type that is only used for defining the 'SRational' pattern
-- synonym.
data KnownRationalInstance (r :: Rational) where
  KnownRationalInstance :: KnownRational r => KnownRationalInstance r

-- | An internal function that is only used for defining the 'SRational' pattern
-- synonym.
knownRationalInstance :: SRational r -> KnownRationalInstance r
knownRationalInstance :: forall (r :: Rational). SRational r -> KnownRationalInstance r
knownRationalInstance SRational r
si = SRational r
-> (KnownRational r => KnownRationalInstance r)
-> KnownRationalInstance r
forall (r :: Rational) x.
SRational r -> (KnownRational r => x) -> x
withKnownRational SRational r
si KnownRationalInstance r
KnownRational r => KnownRationalInstance r
forall (r :: Rational). KnownRational r => KnownRationalInstance r
KnownRationalInstance

instance Show (SRational r) where
  showsPrec :: Int -> SRational r -> ShowS
showsPrec Int
p (UnsafeSRational Rational
r) =
    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
"SRational @" ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
      Int -> Rational -> ShowS
showsPrecLit Int
appPrec1 Rational
r

instance Eq (SRational r) where
  SRational r
_ == :: SRational r -> SRational r -> Bool
== SRational r
_ = Bool
True
  {-# INLINE (==) #-}

instance Ord (SRational r) where
  compare :: SRational r -> SRational r -> Ordering
compare SRational r
_ SRational r
_ = Ordering
EQ
  {-# INLINE compare #-}

instance TestEquality SRational where
  testEquality :: forall (a :: Rational) (b :: Rational).
SRational a -> SRational b -> Maybe (a :~: b)
testEquality = Sing a -> Sing b -> Maybe (a :~: b)
SRational a -> SRational b -> Maybe (a :~: b)
forall k (a :: k) (b :: k).
SDecide k =>
Sing a -> Sing b -> Maybe (a :~: b)
decideEquality
  {-# INLINE testEquality #-}

instance TestCoercion SRational where
  testCoercion :: forall (a :: Rational) (b :: Rational).
SRational a -> SRational b -> Maybe (Coercion a b)
testCoercion = Sing a -> Sing b -> Maybe (Coercion a b)
SRational a -> SRational 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.Rational' number corresponding to @r@.
fromSRational :: SRational r -> P.Rational
fromSRational :: forall (r :: Rational). SRational r -> Rational
fromSRational (UnsafeSRational Rational
r) = Rational
r

-- | Convert an explicit @'SRational' r@ value into an implicit
-- @'KnownRational_' r@ constraint.
withKnownRational_
  :: forall r rep (x :: TYPE rep)
  .  SRational r
  -> (KnownRational_ r => x)
  -> x
withKnownRational_ :: forall (r :: Rational) x.
SRational r -> (KnownRational_ r => x) -> x
withKnownRational_ = forall (cls :: Constraint) meth r.
WithDict cls meth =>
meth -> (cls => r) -> r
withDict @(KnownRational_ r)

-- | Convert an explicit @'SRational' r@ value into an implicit
-- @'KnownRational' r@ constraint.
withKnownRational
  :: forall r rep (x :: TYPE rep)
  .  SRational r
  -> (KnownRational r => x)
  -> x
withKnownRational :: forall (r :: Rational) x.
SRational r -> (KnownRational r => x) -> x
withKnownRational SRational r
sr KnownRational r => x
x
  | Integer
n P.:% Integer
d <- SRational r -> Rational
forall (r :: Rational). SRational r -> Rational
fromSRational SRational r
sr
  , I.SomeInteger @n Proxy i
_ <- Integer -> SomeInteger
I.someIntegerVal Integer
n
  , L.SomeNat @d Proxy n
_ <- Natural -> SomeNat
L.someNatVal (Integer -> Natural
forall a. Num a => Integer -> a
P.fromInteger Integer
d)
  , r :~: Reduced r
Refl <- SRational r -> r :~: Reduced r
forall (r :: Rational). SRational r -> r :~: Reduced r
sReducedRefl SRational r
sr
  , -- These unsafeCoreces are safe because this module doesn't offer any tool
    -- for constructing non-reduced SRationals. Very unsafe otherwise.
    n :~: Den r
Refl <- (Any :~: Any) -> n :~: Den_ r
forall a b. a -> b
unsafeCoerce Any :~: Any
forall {k} (a :: k). a :~: a
Refl :: d :~: Den r
  , i :~: Num r
Refl <- (Any :~: Any) -> i :~: Num_ r
forall a b. a -> b
unsafeCoerce Any :~: Any
forall {k} (a :: k). a :~: a
Refl :: n :~: Num r
  = SRational r -> (KnownRational_ r => x) -> x
forall (r :: Rational) x.
SRational r -> (KnownRational_ r => x) -> x
withKnownRational_ SRational r
sr x
KnownRational r => x
KnownRational_ r => x
x

-- | Convert a "Prelude".'P.Rational' number into an @'SRational' n@ value,
-- where @n@ is a fresh type-level 'Rational'.
withSomeSRational
  :: forall rep (x :: TYPE rep). P.Rational -> (forall r. SRational r -> x) -> x
withSomeSRational :: forall x.
Rational -> (forall (r :: Rational). SRational r -> x) -> x
withSomeSRational (HasCallStack => Rational -> Rational
Rational -> Rational
unsafeReduced -> !Rational
r) forall (r :: Rational). SRational r -> x
k = SRational Any -> x
forall (r :: Rational). SRational r -> x
k (Rational -> SRational Any
forall (r :: Rational). Rational -> SRational r
UnsafeSRational Rational
r)
-- It's very important to keep this NOINLINE! See the docs at "GHC.TypeNats"
{-# NOINLINE withSomeSRational #-}

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

type instance Sing = SRational

instance (KnownRational r) => SingI (r :: Rational) where
  sing :: Sing r
sing = Sing r
SRational r
forall (r :: Rational). KnownRational r => SRational r
rationalSing
  {-# INLINE sing #-}

instance SingKind Rational where
  type Demote Rational = P.Rational
  fromSing :: forall (a :: Rational). Sing a -> Demote Rational
fromSing = Sing a -> Demote Rational
SRational a -> Rational
forall (r :: Rational). SRational r -> Rational
fromSRational
  {-# INLINE fromSing #-}
  toSing :: Demote Rational -> SomeSing Rational
toSing Demote Rational
r = Rational
-> (forall (r :: Rational). SRational r -> SomeSing Rational)
-> SomeSing Rational
forall x.
Rational -> (forall (r :: Rational). SRational r -> x) -> x
withSomeSRational Rational
Demote Rational
r Sing r -> SomeSing Rational
SRational r -> SomeSing Rational
forall k (a :: k). Sing a -> SomeSing k
forall (r :: Rational). SRational r -> SomeSing Rational
SomeSing
  {-# INLINE toSing #-}

instance SDecide Rational where
  UnsafeSRational Rational
l %~ :: forall (a :: Rational) (b :: Rational).
Sing a -> Sing b -> Decision (a :~: b)
%~ UnsafeSRational Rational
r =
    -- This is safe because this library doesn't expose any tool to construct
    -- non-normalized SRationals. Otherwise, very unsafe.
    case Rational
l Rational -> Rational -> Bool
forall a. Eq a => a -> a -> Bool
P.== Rational
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
"Rational: SDecide")

--------------------------------------------------------------------------------
-- Extra stuff that doesn't belong here.

data Dict (c :: Constraint) where
  Dict :: c => Dict c