{-# LANGUAGE StrictData #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE UndecidableSuperClasses #-}
module KindRational
(
Rational
, type (:%)
, FromNatural, fromNatural, sFromNatural
, FromInteger, fromInteger, sFromInteger
, Num, sNum
, Den, sDen
, ToRational(..)
, sMkRational
, (%%)
, (%)
, KnownRational
, Reduced
, rationalSing
, rationalVal
, withKnownRational
, SomeRational(..)
, someRationalVal
, SRational
, pattern SRational
, fromSRational
, withSomeSRational
, sNegateRefl
, ShowLit, showLit, sShowLit
, ShowsLit, showsLit, sShowsLit
, ShowsPrecLit, showsPrecLit, sShowsPrecLit
, readPrecLit
, Signum, sSignum, sSignumRefl
, Recip, sRecip, sRecip'
, Div, sDiv, div
, Rem, rem, sRem
, DivRem, divRem, sDivRem
, I.Round(..), I.SRound(..)
, IsTerminating
, isTerminating
, termination
, Terminating
, NonTerminating
, pattern SRationalTerminating
, pattern SRationalNonTerminating
, cmpRational
, sameRational
, 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)
data Rational = Integer :% Natural
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
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
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
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
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
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 @"")
showLit :: P.Rational -> String
showLit :: Rational -> String
showLit Rational
r = Rational -> ShowS
showsLit Rational
r String
""
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)
showsLit :: P.Rational -> ShowS
showsLit :: Rational -> ShowS
showsLit = Int -> Rational -> ShowS
showsPrecLit Int
0
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
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
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')
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
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."
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
"." ]
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
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
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
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
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
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
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
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)))
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
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 #-}
fromNatural :: Natural -> P.Rational
fromNatural :: Natural -> Rational
fromNatural = Natural -> Rational
forall a b. (Integral a, Num b) => a -> b
P.fromIntegral
{-# INLINE fromNatural #-}
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
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 #-}
fromInteger :: P.Integer -> P.Rational
fromInteger :: Integer -> Rational
fromInteger = Integer -> Rational
forall a. Num a => Integer -> a
P.fromInteger
{-# INLINE fromInteger #-}
infixl 7 %, %%, :%, :%@#@$$$, %@#@$$$
class (SingKind kn, SingKind kd) => ToRational kn kd where
type (n :: kn) % (d :: kd) :: Rational
mkRational :: Demote kn -> Demote kd -> Maybe P.Rational
(%) :: 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 (%) #-}
(%%) :: 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 (%%) #-}
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 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
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
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)
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)
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
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))
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
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
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
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)
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
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)
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
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
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
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)
where f :: Integer -> Integer -> (Integer, Integer)
f = Round -> Integer -> Integer -> (Integer, Integer)
I.divRem Round
rnd
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
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
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
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)
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)
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
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 #-}
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)))
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)))
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)
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
class KnownRational_ (r :: Rational) where
rationalSing_ :: SRational r
type KnownRational (r :: Rational) =
( KnownRational_ r
, Reduced r ~ r
, I.KnownInteger (Num r)
, L.KnownNat (Den r)
)
rationalSing :: KnownRational r => SRational r
rationalSing :: forall (r :: Rational). KnownRational r => SRational r
rationalSing = SRational r
forall (r :: Rational). KnownRational_ r => SRational r
rationalSing_
{-# 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)))
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 #-}
data SomeRational = forall n. KnownRational n => SomeRational (Proxy n)
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 #-}
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)
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
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)
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
newtype SRational (r :: Rational) = UnsafeSRational P.Rational
type role SRational nominal
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_
data KnownRationalInstance (r :: Rational) where
KnownRationalInstance :: KnownRational r => KnownRationalInstance r
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 #-}
fromSRational :: SRational r -> P.Rational
fromSRational :: forall (r :: Rational). SRational r -> Rational
fromSRational (UnsafeSRational Rational
r) = Rational
r
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)
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
,
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
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)
{-# 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 =
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")
data Dict (c :: Constraint) where
Dict :: c => Dict c