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

-- | This module provides a type-level representation for term-level
-- 'P.Rational's. This type-level representation is also named 'P.Rational',
-- So import this module qualified to avoid name conflicts.
--
-- @
-- import "KindRational" qualified as KR
-- @
--
-- The implementation details are the same as the ones for type-level 'Natural's
-- in "GHC.TypeNats" as of @base-4.18@, and it will continue to evolve together
-- with @base@, trying to follow its core API as much as possible until the day
-- @base@ provides its own type-level rationals, making this module redundant.
module KindRational {--}
  ( -- * Rational kind
    Rational
  , type (%)
  , type (/)
  , Normalize
  , Num
  , Den

    -- Prelude support
  , rational
  , fromPrelude
  , toPrelude
  , showsPrecTypeLit

    -- * Types ⇔ Terms
  , KnownRational(rationalSing)
  , rationalVal
  , SomeRational(..)
  , someRationalVal
  , sameRational

    -- * Singletons
  , SRational
  , pattern SRational
  , fromSRational
  , fromSRational'
  , withSomeSRational
  , withKnownRational

    -- * Arithmethic
  , type (+)
  , type (*)
  , type (-)
  , Negate
  , Sign
  , Abs
  , Recip
  , Div
  , div
  , Rem
  , rem
  , DivRem
  , divRem
  , I.Round(..)

    -- * Decimals
  , Terminating
  , withTerminating
  , Terminates
  , terminates

    -- * Comparisons
  , CmpRational
  , cmpRational
  , eqRationalRep

    -- * Extra
    --
    -- | This stuff should be exported by the "Data.Type.Ord" module.
  , type (==?), type (==), type (/=?), type (/=)
  ) --}
  where
import Control.Exception qualified as Ex
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)

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

-- | Type-level version of 'P.Rational'. Use '/' to construct one, use '%' to
-- pattern-match on it.
--
-- 'Rational' is mostly used as a kind, with its types constructed
-- using '/'.  However, it might also be used as type, with its terms
-- constructed using 'rational' or 'fromPrelude'. One reason why you may want a
-- 'Rational' at the term-level is so that you embed it in larger data-types
-- (for example, this 'Rational' embeds the 'I.Integer' similarly offered by
-- the "KindInteger" module). But perhaps more importantly, this 'Rational'
-- offers better safety than the 'P.Rational' from "Prelude", since it's not
-- possible to construct one with a zero denominator, or so large that
-- operating with it would exhaust system resources. Notwithstanding this, for
-- ergonomic reasons, all of the functions exported by this module take
-- "Prelude" 'Rational's as input and produce "Prelude" 'Rational's as outputs.
-- Internally, however, the beforementioned checks are always performed, and
-- fail with 'Ex.throw' if necessary. If you want to be sure those 'error's
-- never happen, just filter your "Prelude" 'Rational's with 'fromPrelude'. In
-- practice, it's very unlikely that you will be affected by this unless if
-- you are unsafelly constructing "Prelude" 'Rational's.
data Rational
  = -- | This constructor is /unsafe/ because it doesn't check for the things
    -- that 'rational' checks for.
    --
    -- * At the term-level, safely construct a 'Rational' using 'rational'
    -- or 'fromPrelude' instead.
    --
    -- * At the type-level, safely construct a 'Rational' using '/'.
    --
    -- * We keep the numerator and denominator unnormalized because we use them
    -- to implement 'SDecide', 'TestEquality' and 'TestCoercion'. Even if “1/2”
    -- and “2/4” mean the same, in 'SDecide' and friends we treat them as the
    -- different types that they are.
    I.Integer :% Natural

-- | Arithmethic equality. That is, \(\frac{1}{2} == \frac{2}{4}\).
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

-- | Same as "Prelude" 'P.Rational'.
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

-- | Same as "Prelude" 'P.Rational'.
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  -- 7 is GHC.Real.ratioPrec
    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

-- | Shows the 'Rational' as it appears literally at the type-level.
--
-- This is remerent from normal 'show' for 'Rational', which shows
-- the term-level value.
--
-- @
-- 'shows'            0 ('rationalVal' ('Proxy' \@(1'/'2))) \"z\" == \"1 % 2z\"
-- 'showsPrecTypeLit' 0 ('rationalVal' ('Proxy' \@(1'/'2))) \"z\" == \"P 1 % 2z\"
-- @
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

-- | Make a term-level "KindRational" 'Rational' number, provided that
-- the numerator is not @0@, and that its numerator and denominator are
-- not so large that they would exhaust system resources. The 'Rational'
-- is 'Normalize'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 -- 'P.%' normalizes
           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 -- Some big enough number. TODO: Pick good number.
    max_ :: Integer
max_ = Integer
10 Integer -> Int -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
^ (Int
1000 :: Int)

-- | Try to obtain a term-level "KindRational" 'Rational' from a term-level
-- "Prelude" 'P.Rational'. This can fail if the "Prelude" 'P.Rational' is
-- infinite, or if it is so big that it would exhaust system resources.
--
-- @
-- 'fromPrelude' . 'toPrelude'      == 'Just'
-- 'fmap' 'toPrelude' . 'fromPrelude' == 'Just'
-- @
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

-- | Like 'fromPrelude', but 'Ex.throw's in situations where
-- 'fromPrelude' fails with 'Nothing'.
unsafeFromPrelude :: P.Rational -> Rational
unsafeFromPrelude :: Rational -> Rational
unsafeFromPrelude = \case
    Integer
n P.:% Integer
d
     | Integer
d Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
0 -> ArithException -> Rational
forall a e. Exception e => e -> a
Ex.throw ArithException
Ex.RatioZeroDenominator
     | 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_ -> ArithException -> Rational
forall a e. Exception e => e -> a
Ex.throw ArithException
Ex.Overflow
     | Bool
otherwise -> let Integer
n1 P.:% Integer
d1 = Integer
n Integer -> Integer -> Rational
forall a. Integral a => a -> a -> Ratio a
P.% Integer
d -- 'P.%' normalizes
                    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 -- Some big enough number. TODO: Pick good number.
    max_ :: Integer
max_ = Integer
10 Integer -> Int -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
^ (Int
1000 :: Int)

-- | Like 'unsafeFromPrelude', but returns a "Prelude" 'P.Rational'.
unsafeCheckPrelude :: P.Rational -> P.Rational
unsafeCheckPrelude :: Rational -> Rational
unsafeCheckPrelude = Rational -> Rational
toPrelude (Rational -> Rational)
-> (Rational -> Rational) -> Rational -> Rational
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rational -> Rational
unsafeFromPrelude

-- | Convert a term-level "KindRational" 'Rational' into a 'Normalized'
-- term-level "Prelude" 'P.Rational'.
--
-- @'fromPrelude' . 'toPrelude' == 'Just'@
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 -- 'P.%' normalizes.

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

-- | 'Normalize'd /'Num'erator/ of the type-level 'Rational'.
type Num (r :: Rational) = Num_ (Normalize r) :: Integer
type family Num_ (r :: Rational) :: Integer where
  Num_ (n :% _) = n

-- | 'Normalize'd /'Den'ominator/ of the type-level 'Rational'.
type Den (r :: Rational) = Den_ (Normalize r) :: Natural
type family Den_ (r :: Rational) :: Natural where
  Den_ (_ :% d) = d

-- | Pattern-match on a type-level 'Rational'.
--
-- __NB:__ When /constructing/ a 'Rational' number, prefer to use '/',
-- which not only accepts more polymorphic inputs, but also 'Normalize's
-- the type-level 'Rational'. Also note that while @n '%' 0@ is a valid
-- type, all tools in the "KindRational" will reject such input.
type (n :: I.Integer) % (d :: Natural) = n :% d :: Rational

-- | Normalize a type-level 'Rational' so that a /0/ denominator fails to
-- type-check, and that the 'Num'erator and denominator have no common factors.
--
-- Only 'Normalize'd 'Rational's can be reliably constrained for equality
-- using '~'.
--
-- All of the functions in the "KindRational" module accept both
-- 'Normalize'd and non-'Normalize'd inputs, but they always produce
-- 'Normalize'd output.
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
-- | @n'/'d@ constructs and 'Normalize's a type-level 'Rational'
-- with numerator @n@ and denominator @d@.
--
-- This type-family accepts any combination of 'Natural', 'Integer' and
-- 'Rational' as input.
--
-- @
-- ('/') :: 'Natural'  -> 'Natural'  -> 'Rational'
-- ('/') :: 'Natural'  -> 'Integer'  -> 'Rational'
-- ('/') :: 'Natural'  -> 'Rational' -> 'Rational'
--
-- ('/') :: 'Integer'  -> 'Natural'  -> 'Rational'
-- ('/') :: 'Integer'  -> 'Integer'  -> 'Rational'
-- ('/') :: 'Integer'  -> 'Rational' -> 'Rational'
--
-- ('/') :: 'Rational' -> 'Natural'  -> 'Rational'
-- ('/') :: 'Rational' -> 'Integer'  -> 'Rational'
-- ('/') :: 'Rational' -> 'Rational' -> 'Rational'
-- @
--
-- It's not possible to pattern-match on @n'/'d@.  Instead, you must
-- pattern match on @x'%'y@, where @x'%'y ~ n'/'d@.
type family n / d :: Rational where
  -- Natural/Natural
  (n :: Natural) / (d :: Natural) = Normalize (P n % d)
  -- Natural/Integer
  (n :: Natural) / (P d :: Integer) = Normalize (P n % d)
  (n :: Natural) / (N d :: Integer) = Normalize (N n % d)
  -- Natural/Rational
  (n :: Natural) / (d :: Rational) = (P n % 1) * Recip d
  -- Integer/Natural
  (i :: Integer) / (d :: Natural) = Normalize (i % d)
  -- Integer/Integer
  (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)
  -- Integer/Rational
  (n :: Integer) / (d :: Rational) = (n % 1) * Recip d
  -- Rational/Natural
  (n :: Rational) / (d :: Natural) = n * Recip (P d % 1)
  -- Rational/Integer
  (n :: Rational) / (d :: Integer) = n * Recip (d % 1)
  -- Rational/Rational
  (n :: Rational) / (d :: Rational) = n * Recip d

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

-- | /'Negate'/ a type-level 'Rational'. Also known as /additive inverse/.
type family Negate (r :: Rational) :: Rational where
  Negate (P n % d) = Normalize (N n % d)
  Negate (N n % d) = Normalize (P n % d)

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

-- | /'Abs'olute/ value of a type-level 'Rational'.
type Abs (r :: Rational) = Normalize (P (I.Abs (Num_ r)) % Den_ r) :: Rational

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

-- | @a t'*' b@ multiplies type-level 'Rational's @a@ and @b@.
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))

-- | /'Recip'rocal/ of the type-level 'Rational'.
-- Also known as /multiplicative inverse/.
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)

-- | @a t'+' b@ adds type-level 'Rational's @a@ and @b@.
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))

-- | @a t'-' b@ subtracts the type-level 'Rational' @b@ from
-- the type-level 'Rational' @a@.
type (a :: Rational) - (b :: Rational) = a + Negate b :: Rational


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

-- | Quotient of the 'Div'ision of the 'Num'erator of type-level 'Rational' @a@
-- by its 'Den'ominator, using the specified 'I.Round'ing @r@.
--
-- @
-- forall (r :: 'I.Round') (a :: 'Rational').
--   ('Den' a '/=' 0) =>
--     'Rem' r a  '=='  a '-' 'Div' r a '%' 1
-- @
--
-- Use this to approximate a type-level 'Rational' to an 'Integer'.
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

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

-- | Get both the quotient and the 'Rem'ainder of the 'Div'ision of the
-- 'Num'erator of type-level 'Rational' @a@ by its 'Den'ominator,
-- using the specified 'I.Round'ing @r@.
--
-- @
-- forall (r :: 'I.Round') (a :: 'Rational').
--   ('Den' a '/=' 0) =>
--     'DivRem' r a  '=='  '('Div' r a, 'Rem' r a)
-- @
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)

-- | Term-level version of 'Div'.
--
-- Takes a "Prelude" 'P.Rational' as input, returns a "Prelude" 'P.Integer'.
div :: I.Round -> P.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 \Rational
a -> let (Integer
n P.:% Integer
d) = Rational -> Rational
unsafeCheckPrelude Rational
a
                 in  Integer -> Integer -> Integer
f Integer
n Integer
d

-- | Term-level version of 'Rem'.
--
-- Takes a "Prelude" 'P.Rational' as input, returns a "Prelude" 'P.Rational'.
rem :: I.Round -> P.Rational -> P.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

-- | Term-level version of 'DivRem'.
--
-- Takes a "Prelude" 'P.Rational' as input, returns a pair of "Prelude"
-- 'P.Rational's /(quotient, remerence)/.
--
-- @
-- forall ('r' :: 'I.Round') (a :: 'P.Rational').
--   ('P.denominator' a 'P./=' 0) =>
--     'divRem' r a  'P.=='  ('div' r a, 'rem' r a)
-- @
divRem :: I.Round -> P.Rational -> (P.Integer, P.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 \Rational
a -> let (Integer
n P.:% Integer
d) = Rational -> Rational
unsafeCheckPrelude Rational
a
                        (Integer
q, Integer
m) = Integer -> Integer -> (Integer, Integer)
f Integer
n Integer
d
                    in  (Integer
q, Integer
m Integer -> Integer -> Rational
forall a. Integral a => a -> a -> Ratio a
P.% Integer
d) -- (m % d) == (a - q)

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

-- | 'Constraint' version of @'Terminates' r@. Satisfied by all type-level
-- 'Rational's that can be represented as a finite decimal number.

-- Written as a class rather than as a type-synonym so that downstream doesn't
-- need to use UndecidableSuperClasses.
class (KnownRational r, Terminates r ~ True)
  => Terminating (r :: Rational)

-- Note: Even if @Terminates r ~ 'False@, GHC shows our @TypeError@ first.
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

-- | Whether the type-level 'Rational' terminates. That is, whether
-- it can be fully represented as a finite decimal number.
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)

-- @Terminates_5@ is here to prevent @Terminates_@ from recursing into
-- @Terminates_ (Div d 5)@ if it would diverge.
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)

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

-- | Term-level version of the "Terminates" function.
-- Takes a "Prelude" 'P.Rational' as input.
terminates :: P.Rational -> Bool
terminates :: Rational -> Bool
terminates = Rational -> Bool
terminates' (Rational -> Bool) -> (Rational -> Rational) -> Rational -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rational -> Rational
unsafeFromPrelude

-- | Term-level version of the "Terminates" function.
-- Takes a "KindRational" 'P.Rational' as input.
terminates' :: Rational -> Bool
terminates' :: Rational -> Bool
terminates' = \(Integer
_ :% Natural
d) -> Natural -> Bool
go Natural
d
  where
    go :: Natural -> Bool
go = \case
      Natural
5 -> Bool
True
      Natural
2 -> Bool
True
      Natural
1 -> Bool
True
      Natural
n | (Natural
q, Natural
0) <- Natural -> Natural -> (Natural, Natural)
forall a. Integral a => a -> a -> (a, a)
P.divMod Natural
n Natural
5 -> Natural -> Bool
go Natural
q
        | (Natural
q, Natural
0) <- Natural -> Natural -> (Natural, Natural)
forall a. Integral a => a -> a -> (a, a)
P.divMod Natural
n Natural
2 -> Natural -> Bool
go Natural
q
      Natural
_ -> Bool
False

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

-- | Comparison of type-level 'Rational's, as a function.
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)

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

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

-- | This class gives the rational associated with a type-level rational.
-- There are instances of the class for every rational.
class KnownRational (r :: Rational) where
  rationalSing :: SRational r

-- | This instance checks that @r@ 'Normalize's, but the obtained 'SRational' is
-- not normalized. This is so that 'SDecide', 'TestEquality' and 'TestCoercion'
-- behave as expected.  If you want a 'Normalize'd 'SRational', then use
-- @'rationalSing' \@('Normalize' 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)

-- | Term-level "KindRational" 'Rational' representation of the type-level
-- 'Rational' @r@.
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

-- | Term-level "Prelude" 'P.Rational' representation of the type-level
-- 'Rational' @r@.
rationalVal :: forall r proxy. KnownRational r => proxy r -> P.Rational
rationalVal :: forall (r :: Rational) (proxy :: Rational -> Type).
KnownRational r =>
proxy r -> Rational
rationalVal = Rational -> Rational
toPrelude (Rational -> Rational)
-> (proxy r -> Rational) -> proxy r -> Rational
forall b c a. (b -> c) -> (a -> b) -> a -> c
. proxy r -> Rational
forall (r :: Rational) (proxy :: Rational -> Type).
KnownRational r =>
proxy r -> Rational
rationalVal'

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

-- | Convert a term-level "Prelude" 'Rational' into an unknown
-- type-level 'Rational'.
someRationalVal :: P.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 -> Rational
unsafeFromPrelude 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)]


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

-- | Like 'sameRational', but if the type-level 'Rational's aren't equal, this
-- additionally provides proof of 'LT' or 'GT'.
cmpRational
  :: forall a b proxy1 proxy2
  .  (KnownRational a, KnownRational b)
  => proxy1 a
  -> proxy2 b
  -> OrderingI a b
cmpRational :: forall (a :: Rational) (b :: Rational) (proxy1 :: Rational -> Type)
       (proxy2 :: Rational -> Type).
(KnownRational a, KnownRational b) =>
proxy1 a -> proxy2 b -> OrderingI a b
cmpRational proxy1 a
x proxy2 b
y = case Rational -> Rational -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (proxy1 a -> Rational
forall (r :: Rational) (proxy :: Rational -> Type).
KnownRational r =>
proxy r -> Rational
rationalVal proxy1 a
x) (proxy2 b -> Rational
forall (r :: Rational) (proxy :: Rational -> Type).
KnownRational r =>
proxy r -> Rational
rationalVal proxy2 b
y) of
    Ordering
EQ -> case (Any :~: Any) -> CmpRational_ (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

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

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

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

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

-- | An internal function that is only used for defining the 'SRational' pattern
-- synonym.
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

-- | Note that this checks for type equality, not arithmetic equality.
-- That is, @'P' 1 '%' 2@ and @'P' 2 '%' 4@ are not equal types,
-- even if they are arithmetically equal.
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 #-}

-- | Note that this checks for type equality, not arithmetic equality.
-- That is, @'P' 1 '%' 2@ and @'P' 2 '%' 4@ are not equal types,
-- even if they are arithmetically equal.
instance TestCoercion SRational where
  testCoercion :: forall (a :: Rational) (b :: Rational).
SRational a -> SRational b -> Maybe (Coercion a b)
testCoercion = Sing a -> Sing b -> Maybe (Coercion a b)
SRational a -> SRational b -> Maybe (Coercion a b)
forall k (a :: k) (b :: k).
SDecide k =>
Sing a -> Sing b -> Maybe (Coercion a b)
decideCoercion
  {-# INLINE testCoercion #-}

-- | Return the term-level "Prelude" 'P.Rational' number corresponding
-- to @r@ in a @'SRational' r@ value. This 'P.Rational' is 'Normalize'd.
fromSRational :: SRational r -> P.Rational
fromSRational :: forall (r :: Rational). SRational r -> Rational
fromSRational (UnsafeSRational Rational
r) = Rational -> Rational
toPrelude Rational
r

-- | Return the term-level "KindRational" 'Rational' number corresponding
-- to @r@ in a @'SRational' r@ value. This 'Rational' is not 'Normalize'd.
fromSRational' :: SRational r -> Rational
fromSRational' :: forall (r :: Rational). SRational r -> Rational
fromSRational' (UnsafeSRational Rational
r) = Rational
r

-- | Whether the internal representation of the 'Rational's are equal.
--
-- Note that this is not the same as '(P.==)'. Use '(P.==)' unless you
-- know what you are doing.
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 #-}

-- | Convert an explicit @'SRational' r@ value into an implicit
-- @'KnownRational' r@ constraint.
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)

-- | Convert a "Prelude" 'P.Rational' number into an @'SRational' n@ value,
-- where @n@ is a fresh type-level 'Rational'.
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)
-- It's very important to keep this NOINLINE! See the docs at "GHC.TypeNats"
{-# NOINLINE withSomeSRational #-}

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

type instance Sing = SRational

-- | Note that this checks for type equality, not arithmetic equality.
-- That is, @'P' 1 '%' 2@ and @'P' 2 '%' 4@ are not equal types,
-- even if they are arithmetically equal.
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")

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

-- | /Greatest Common Divisor/ of 'Natural' numbers @a@ and @b@.
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