{-# LANGUAGE StrictData #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE UndecidableSuperClasses #-}
module KindRational
(
Rational
, type (%)
, type (/)
, Normalize
, Num
, Den
, rational
, fromPrelude
, toPrelude
, showsPrecTypeLit
, KnownRational(rationalSing)
, rationalVal
, SomeRational(..)
, someRationalVal
, sameRational
, SRational
, pattern SRational
, fromSRational
, withSomeSRational
, withKnownRational
, type (+)
, type (*)
, type (-)
, Negate
, Sign
, Abs
, Recip
, Div
, div
, Rem
, rem
, DivRem
, divRem
, I.Round(..)
, Terminating
, withTerminating
, Terminates
, terminates
, CmpRational
, cmpRational
, eqRationalRep
, type (==?), type (==), type (/=?), type (/=)
)
where
import Control.Monad
import Data.Proxy
import Data.Singletons
import Data.Singletons.Decide
import Data.Type.Bool (If)
import Data.Type.Coercion
import Data.Type.Equality (TestEquality(..))
import Data.Type.Ord
import GHC.Base (WithDict(..))
import GHC.Exts (TYPE, Constraint)
import GHC.Read qualified as Read
import GHC.Real qualified as P (Ratio(..), (%))
import GHC.Show (appPrec, appPrec1)
import GHC.TypeLits qualified as L
import GHC.TypeNats qualified as N
import KindInteger (Integer, N, P)
import KindInteger (type (==?), type (==), type (/=?), type (/=))
import KindInteger qualified as I
import Numeric.Natural (Natural)
import Prelude hiding (Rational, Integer, Num, div, rem)
import Prelude qualified as P
import Text.ParserCombinators.ReadPrec as Read
import Text.Read.Lex qualified as Read
import Unsafe.Coerce(unsafeCoerce)
data Rational
=
I.Integer :% Natural
instance Eq Rational where
Rational
a == :: Rational -> Rational -> Bool
== Rational
b = Rational -> Rational
toPrelude Rational
a Rational -> Rational -> Bool
forall a. Eq a => a -> a -> Bool
== Rational -> Rational
toPrelude Rational
b
instance Ord Rational where
compare :: Rational -> Rational -> Ordering
compare Rational
a Rational
b = Rational -> Rational -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (Rational -> Rational
toPrelude Rational
a) (Rational -> Rational
toPrelude Rational
b)
Rational
a <= :: Rational -> Rational -> Bool
<= Rational
b = Rational -> Rational
toPrelude Rational
a Rational -> Rational -> Bool
forall a. Ord a => a -> a -> Bool
<= Rational -> Rational
toPrelude Rational
b
instance Show Rational where
showsPrec :: Int -> Rational -> ShowS
showsPrec Int
p = Int -> Rational -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
p (Rational -> ShowS) -> (Rational -> Rational) -> Rational -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rational -> Rational
toPrelude
instance Read Rational where
readPrec :: ReadPrec Rational
readPrec = 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
$ Int -> ReadPrec Rational -> ReadPrec Rational
forall a. Int -> ReadPrec a -> ReadPrec a
Read.prec Int
7 (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.step ReadPrec Integer
forall a. Read a => ReadPrec a
Read.readPrec
Lexeme -> ReadPrec ()
Read.expectP (String -> Lexeme
Read.Symbol String
"%")
Integer
d :: P.Integer <- ReadPrec Integer -> ReadPrec Integer
forall a. ReadPrec a -> ReadPrec a
Read.step ReadPrec Integer
forall a. Read a => ReadPrec a
Read.readPrec
Just Rational
r <- Maybe Rational -> ReadPrec (Maybe Rational)
forall a. a -> ReadPrec a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Integer -> Integer -> Maybe Rational
forall num den.
(Integral num, Integral den) =>
num -> den -> Maybe Rational
rational Integer
n Integer
d)
Rational -> ReadPrec Rational
forall a. a -> ReadPrec a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure Rational
r
showsPrecTypeLit :: Int -> Rational -> ShowS
showsPrecTypeLit :: Int -> Rational -> ShowS
showsPrecTypeLit Int
p (Integer
n :% Natural
d) = Bool -> ShowS -> ShowS
showParen (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
appPrec) (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$
Int -> Integer -> ShowS
I.showsPrecTypeLit 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
. Natural -> ShowS
forall a. Show a => a -> ShowS
shows Natural
d
rational :: (Integral num, Integral den) => num -> den -> Maybe Rational
rational :: forall num den.
(Integral num, Integral den) =>
num -> den -> Maybe Rational
rational = \(num -> Integer
forall a. Integral a => a -> Integer
toInteger -> Integer
n) (den -> Integer
forall a. Integral a => a -> Integer
toInteger -> Integer
d) -> do
Bool -> Maybe ()
forall (f :: Type -> Type). Alternative f => Bool -> f ()
guard (Integer
d Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
/= Integer
0 Bool -> Bool -> Bool
&& Integer -> Integer
forall a. Num a => a -> a
abs Integer
n Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= Integer
max_ Bool -> Bool -> Bool
&& Integer -> Integer
forall a. Num a => a -> a
abs Integer
d Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= Integer
max_)
Rational -> Maybe Rational
forall a. a -> Maybe a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Rational -> Maybe Rational) -> Rational -> Maybe Rational
forall a b. (a -> b) -> a -> b
$ let Integer
n1 P.:% Integer
d1 = Integer
n Integer -> Integer -> Rational
forall a. Integral a => a -> a -> Ratio a
P.% Integer
d
in Integer -> Integer
I.fromPrelude Integer
n1 Integer -> Natural -> Rational
:% Integer -> Natural
forall a. Num a => Integer -> a
fromInteger Integer
d1
where
max_ :: P.Integer
max_ :: Integer
max_ = Integer
10 Integer -> Int -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
^ (Int
1000 :: Int)
fromPrelude :: P.Rational -> Maybe Rational
fromPrelude :: Rational -> Maybe Rational
fromPrelude (Integer
n P.:% Integer
d) = Integer -> Integer -> Maybe Rational
forall num den.
(Integral num, Integral den) =>
num -> den -> Maybe Rational
rational Integer
n Integer
d
toPrelude :: Rational -> P.Rational
toPrelude :: Rational -> Rational
toPrelude (Integer
n :% Natural
d) = Integer -> Integer
I.toPrelude Integer
n Integer -> Integer -> Rational
forall a. Integral a => a -> a -> Ratio a
P.% Natural -> Integer
forall a. Integral a => a -> Integer
toInteger Natural
d
type Num (r :: Rational) = Num_ (Normalize r) :: Integer
type family Num_ (r :: Rational) :: Integer where
Num_ (n :% _) = n
type Den (r :: Rational) = Den_ (Normalize r) :: Natural
type family Den_ (r :: Rational) :: Natural where
Den_ (_ :% d) = d
type (n :: I.Integer) % (d :: Natural) = n :% d :: Rational
type family Normalize (r :: Rational) :: Rational where
Normalize (_ % 0) = L.TypeError ('L.Text "KindRational: Denominator is zero")
Normalize (P 0 % _) = P 0 % 1
Normalize (N 0 % _) = P 0 % 1
Normalize (P n % d) = P (L.Div n (GCD n d)) % L.Div d (GCD n d)
Normalize (N n % d) = N (L.Div n (GCD n d)) % L.Div d (GCD n d)
infixl 6 +, -
infixl 7 *, /
type (/) :: kn -> kd -> Rational
type family n / d :: Rational where
(n :: Natural) / (d :: Natural) = Normalize (P n % d)
(n :: Natural) / (P d :: Integer) = Normalize (P n % d)
(n :: Natural) / (N d :: Integer) = Normalize (N n % d)
(n :: Natural) / (d :: Rational) = (P n % 1) * Recip d
(i :: Integer) / (d :: Natural) = Normalize (i % d)
(P n :: Integer) / (P d :: Integer) = Normalize (P n % d)
(N n :: Integer) / (N d :: Integer) = Normalize (P n % d)
(P n :: Integer) / (N d :: Integer) = Normalize (N n % d)
(N n :: Integer) / (P d :: Integer) = Normalize (N n % d)
(n :: Integer) / (d :: Rational) = (n % 1) * Recip d
(n :: Rational) / (d :: Natural) = n * Recip (P d % 1)
(n :: Rational) / (d :: Integer) = n * Recip (d % 1)
(n :: Rational) / (d :: Rational) = n * Recip d
type family Negate (r :: Rational) :: Rational where
Negate (P n % d) = Normalize (N n % d)
Negate (N n % d) = Normalize (P n % d)
type Sign (r :: Rational) = I.Sign (Num r) :: Integer
type Abs (r :: Rational) = Normalize (P (I.Abs (Num_ r)) % Den_ r) :: Rational
type (a :: Rational) * (b :: Rational) =
Mul_ (Normalize a) (Normalize b) :: Rational
type family Mul_ (a :: Rational) (b :: Rational) where
Mul_ (n1 % d1) (n2 % d2) = Normalize ((n1 I.* n2) % (d1 L.* d2))
type Recip (a :: Rational) = Recip_ (Normalize a) :: Rational
type family Recip_ (a :: Rational) :: Rational where
Recip_ (P n % d) = Normalize (P d % n)
Recip_ (N n % d) = Normalize (N d % n)
type (a :: Rational) + (b :: Rational) =
Add_ (Normalize a) (Normalize b) :: Rational
type family Add_ (a :: Rational) (r :: Rational) :: Rational where
Add_ (an % ad) (bn % bd) =
Normalize ((an I.* P bd I.+ bn I.* P ad) % (ad L.* bd))
type (a :: Rational) - (b :: Rational) = a + Negate b :: Rational
type Div (r :: I.Round) (a :: Rational) =
Div_ r (Normalize a) :: Integer
type Div_ (r :: I.Round) (a :: Rational) =
I.Div r (Num_ a) (P (Den_ a)) :: Integer
type Rem (r :: I.Round) (a :: Rational) = Snd (DivRem r a) :: Rational
type DivRem (r :: I.Round) (a :: Rational) =
DivRem_ r (Normalize a) :: (Integer, Rational)
type DivRem_ (r :: I.Round) (a :: Rational) =
DivRem__ (Den_ a) (I.DivRem r (Num_ a) (P (Den_ a))) :: (Integer, Rational)
type DivRem__ (d :: Natural) (qm :: (Integer, Integer)) =
'(Fst qm, Normalize (Snd qm % d)) :: (Integer, Rational)
div :: I.Round -> Rational -> P.Integer
div :: Round -> Rational -> Integer
div Round
r = let f :: Integer -> Integer -> Integer
f = Round -> Integer -> Integer -> Integer
I.div Round
r
in \(Integer
n :% Natural
d) -> Integer -> Integer -> Integer
f (Integer -> Integer
I.toPrelude Integer
n) (Natural -> Integer
forall a. Integral a => a -> Integer
toInteger Natural
d)
rem :: I.Round -> Rational -> Rational
rem :: Round -> Rational -> Rational
rem Round
r = (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
r
divRem :: I.Round -> Rational -> (P.Integer, Rational)
divRem :: Round -> Rational -> (Integer, Rational)
divRem Round
r = let f :: Integer -> Integer -> (Integer, Integer)
f = Round -> Integer -> Integer -> (Integer, Integer)
I.divRem Round
r
in \(Integer
n :% Natural
d) -> let (Integer
q, Integer
m) = Integer -> Integer -> (Integer, Integer)
f (Integer -> Integer
I.toPrelude Integer
n) (Natural -> Integer
forall a. Integral a => a -> Integer
toInteger Natural
d)
in (Integer
q, Integer -> Integer
I.fromPrelude Integer
m Integer -> Natural -> Rational
:% Natural
d)
class (KnownRational r, Terminates r ~ True)
=> Terminating (r :: Rational)
instance
( KnownRational r
, Terminates r ~ 'True
, If (Terminates r)
(() :: Constraint)
(L.TypeError ('L.Text "‘" 'L.:<>: 'L.ShowType r 'L.:<>:
'L.Text "’ is not a terminating "
'L.:<>: 'L.ShowType Rational))
) => Terminating r
withTerminating
:: forall r a
. KnownRational r
=> (Terminating r => a)
-> Maybe a
withTerminating :: forall (r :: Rational) a.
KnownRational r =>
(Terminating r => a) -> Maybe a
withTerminating Terminating r => a
g = do
Bool -> Maybe ()
forall (f :: Type -> Type). Alternative f => Bool -> f ()
guard (Rational -> Bool
terminates (Proxy r -> Rational
forall (r :: Rational) (proxy :: Rational -> Type).
KnownRational r =>
proxy r -> Rational
rationalVal (forall {k} (t :: k). Proxy t
forall (t :: Rational). Proxy t
Proxy @r)))
case Dict (Terminating (P 1 % 1)) -> Dict (Terminating r)
forall a b. a -> b
unsafeCoerce (forall (c :: Constraint). c => Dict c
Dict @(Terminating (P 1 % 1))) of
(Dict (Terminating r)
Dict :: Dict (Terminating r)) -> a -> Maybe a
forall a. a -> Maybe a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure a
Terminating r => a
g
type Terminates (r :: Rational) = Terminates_ (Den r) :: Bool
type family Terminates_ (n :: Natural) :: Bool where
Terminates_ 5 = 'True
Terminates_ 2 = 'True
Terminates_ 1 = 'True
Terminates_ d = Terminates_5 d (L.Mod d 5)
type family Terminates_5 (d :: Natural) (md5 :: Natural) :: Bool where
Terminates_5 d 0 = Terminates_ (L.Div d 5)
Terminates_5 d _ = Terminates_2 d (L.Mod d 2)
type family Terminates_2 (d :: Natural) (md2 :: Natural) :: Bool where
Terminates_2 d 0 = Terminates_ (L.Div d 2)
Terminates_2 _ _ = 'False
terminates :: Rational -> Bool
terminates :: Rational -> Bool
terminates = \(Integer
_ :% Natural
d) -> Integer -> Bool
go (Natural -> Integer
forall a. Integral a => a -> Integer
toInteger Natural
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
type CmpRational (a :: Rational) (b :: Rational) =
CmpRational_ (Normalize a) (Normalize b) :: Ordering
type family CmpRational_ (a :: Rational) (b :: Rational) :: Ordering where
CmpRational_ a a = 'EQ
CmpRational_ (an % ad) (bn % bd) = I.CmpInteger (an I.* P bd) (bn I.* P ad)
type instance Compare (a :: Rational) (b :: Rational) = CmpRational a b
class KnownRational (r :: Rational) where
rationalSing :: SRational r
instance forall r n d.
( Normalize r ~ n % d
, I.KnownInteger (Num_ r)
, L.KnownNat (Den_ r)
) => KnownRational r where
rationalSing :: SRational r
rationalSing =
let n :: Integer
n = SInteger (Num_ r) -> Integer
forall (i :: Integer). SInteger i -> Integer
I.fromSInteger (forall (i :: Integer). KnownInteger i => SInteger i
I.SInteger @(Num_ r))
d :: Natural
d = Proxy (Den_ r) -> Natural
forall (n :: Natural) (proxy :: Natural -> Type).
KnownNat n =>
proxy n -> Natural
N.natVal (forall (t :: Natural). Proxy t
forall {k} (t :: k). Proxy t
Proxy @(Den_ r))
in Rational -> SRational r
forall (r :: Rational). Rational -> SRational r
UnsafeSRational (Integer
n Integer -> Natural -> Rational
:% Natural
d)
rationalVal :: forall r proxy. KnownRational r => proxy r -> 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
data SomeRational = forall n. KnownRational n => SomeRational (Proxy n)
someRationalVal :: Rational -> SomeRational
someRationalVal :: Rational -> SomeRational
someRationalVal Rational
r = Rational
-> (forall {r :: Rational}. SRational r -> SomeRational)
-> SomeRational
forall a.
Rational -> (forall (r :: Rational). SRational r -> a) -> a
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) a.
SRational r -> (KnownRational r => a) -> a
withKnownRational SRational r
sr (forall (n :: Rational). KnownRational n => Proxy n -> SomeRational
SomeRational @r Proxy r
forall {k} (t :: k). Proxy t
Proxy)
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
instance Ord 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. Ord a => a -> a -> Bool
<= Proxy n -> Rational
forall (r :: Rational) (proxy :: Rational -> Type).
KnownRational r =>
proxy r -> Rational
rationalVal Proxy n
y
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)
instance Show SomeRational where
showsPrec :: Int -> SomeRational -> ShowS
showsPrec Int
p (SomeRational Proxy n
x) = 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
x)
instance Read SomeRational where
readsPrec :: Int -> ReadS SomeRational
readsPrec Int
p String
xs = do (Rational
a, String
ys) <- Int -> ReadS Rational
forall a. Read a => Int -> ReadS a
readsPrec Int
p String
xs
[(Rational -> SomeRational
someRationalVal Rational
a, String
ys)]
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_ (Normalize a) (Normalize b) :~: 'EQ
forall a b. a -> b
unsafeCoerce Any :~: Any
forall {k} (a :: k). a :~: a
Refl :: CmpRational a b :~: 'EQ of
CmpRational_ (Normalize a) (Normalize b) :~: 'EQ
Refl -> case (Any :~: Any) -> a :~: b
forall a b. a -> b
unsafeCoerce Any :~: Any
forall {k} (a :: k). a :~: a
Refl :: a :~: b of
a :~: b
Refl -> OrderingI a a
OrderingI a b
forall {k} (a :: k). (Compare a a ~ 'EQ) => OrderingI a a
EQI
Ordering
LT -> case (Any :~: Any) -> CmpRational_ (Normalize a) (Normalize b) :~: 'LT
forall a b. a -> b
unsafeCoerce Any :~: Any
forall {k} (a :: k). a :~: a
Refl :: (CmpRational a b :~: 'LT) of
CmpRational_ (Normalize a) (Normalize b) :~: 'LT
Refl -> OrderingI a b
forall {k} (a :: k) (b :: k). (Compare a b ~ 'LT) => OrderingI a b
LTI
Ordering
GT -> case (Any :~: Any) -> CmpRational_ (Normalize a) (Normalize b) :~: 'GT
forall a b. a -> b
unsafeCoerce Any :~: Any
forall {k} (a :: k). a :~: a
Refl :: (CmpRational a b :~: 'GT) of
CmpRational_ (Normalize a) (Normalize 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 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 -> KnownRationalegerInstance)
where SRational = SRational r
forall (r :: Rational). KnownRational r => SRational r
rationalSing
data KnownRationalegerInstance (r :: Rational) where
KnownRationalegerInstance :: KnownRational r => KnownRationalegerInstance r
knownRationalInstance :: SRational r -> KnownRationalegerInstance r
knownRationalInstance :: forall (r :: Rational). SRational r -> KnownRationalegerInstance r
knownRationalInstance SRational r
si = SRational r
-> (KnownRational r => KnownRationalegerInstance r)
-> KnownRationalegerInstance r
forall (r :: Rational) a.
SRational r -> (KnownRational r => a) -> a
withKnownRational SRational r
si KnownRationalegerInstance r
KnownRational r => KnownRationalegerInstance r
forall (r :: Rational).
KnownRational r =>
KnownRationalegerInstance r
KnownRationalegerInstance
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
appPrec) (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
showsPrecTypeLit Int
appPrec1 Rational
r
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 -> Rational
fromSRational :: forall (r :: Rational). SRational r -> Rational
fromSRational (UnsafeSRational Rational
r) = Rational
r
eqRationalRep :: Rational -> Rational -> Bool
eqRationalRep :: Rational -> Rational -> Bool
eqRationalRep (Integer
ln :% Natural
ld) (Integer
rn :% Natural
rd) = Integer -> Integer -> Bool
I.eqIntegerRep Integer
ln Integer
rn Bool -> Bool -> Bool
&& Natural
ld Natural -> Natural -> Bool
forall a. Eq a => a -> a -> Bool
P.== Natural
rd
{-# INLINE eqRationalRep #-}
withKnownRational
:: forall r rep (a :: TYPE rep). SRational r -> (KnownRational r => a) -> a
withKnownRational :: forall (r :: Rational) a.
SRational r -> (KnownRational r => a) -> a
withKnownRational = forall (cls :: Constraint) meth r.
WithDict cls meth =>
meth -> (cls => r) -> r
withDict @(KnownRational r)
withSomeSRational
:: forall rep (a :: TYPE rep). Rational -> (forall r. SRational r -> a) -> a
withSomeSRational :: forall a.
Rational -> (forall (r :: Rational). SRational r -> a) -> a
withSomeSRational Rational
r forall (r :: Rational). SRational r -> a
k = SRational Any -> a
forall (r :: Rational). SRational r -> a
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 = 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 a.
Rational -> (forall (r :: Rational). SRational r -> a) -> a
withSomeSRational Demote Rational
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 -> Rational -> Bool
eqRationalRep Rational
l 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
"SDecide.Rational")
type GCD (a :: Natural) (b :: Natural) = I.GCD (P a) (P b) :: Natural
data Dict c where Dict :: c => Dict c
type family Fst (ab :: (a, b)) :: a where Fst '(a, b) = a
type family Snd (ab :: (a, b)) :: b where Snd '(a, b) = b