{-# 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
  , 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

    -- * Extra
    --
    -- | This stuff should be exported by the "Data.Type.Ord" module.
  , type (==?), type (==), type (/=?), type (/=)
  ) --}
  where

import qualified Control.Exception as Ex
import Control.Monad
import Data.Proxy
import Data.Type.Bool (If)
import Data.Type.Coercion
import Data.Type.Equality (TestEquality(..), (:~:)(..))
import Data.Type.Ord
import GHC.Base (WithDict(..))
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 GHC.Types (TYPE, Constraint)
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 '/'.
    I.Integer :% Natural

num :: Rational -> I.Integer
num :: Rational -> Integer
num (Integer
n :% Natural
_) = Integer
n

den :: Rational -> Natural
den :: Rational -> Natural
den (Integer
_ :% Natural
d) = Natural
d

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 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
$
  Int -> Integer -> ShowS
I.showsPrecTypeLit Int
appPrec (Rational -> Integer
num Rational
r) 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 (Rational -> Natural
den Rational
r)

-- | 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
           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
       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 term-level
-- "Prelude" 'P.Rational'.
--
-- @
-- 'fromPrelude' . 'toPrelude'      == 'Just'
-- 'fmap' 'toPrelude' . 'fromPrelude' == 'Just'
-- @
toPrelude :: Rational -> P.Rational
toPrelude :: Rational -> Rational
toPrelude Rational
r = Integer -> Integer
I.toPrelude (Rational -> Integer
num Rational
r) Integer -> Integer -> Rational
forall a. a -> a -> Ratio a
P.:% Natural -> Integer
forall a. Integral a => a -> Integer
toInteger (Rational -> Natural
den Rational
r)

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

-- | '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' = Natural -> Bool
go (Natural -> Bool) -> (Rational -> Natural) -> Rational -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rational -> Natural
den
  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

instance forall r n d.
  ( Normalize r ~ n % d
  , I.KnownInteger n
  , L.KnownNat d
  ) => KnownRational r where
  rationalSing :: SRational r
rationalSing = Rational -> SRational r
forall (r :: Rational). Rational -> SRational r
UnsafeSRational
    (Integer -> Integer
I.fromPrelude (Proxy n -> Integer
forall (i :: Integer) (proxy :: Integer -> Type).
KnownInteger i =>
proxy i -> Integer
I.integerVal (forall {k} (t :: k). Proxy t
forall (t :: Integer). Proxy t
Proxy @n)) Integer -> Natural -> Rational
:% Proxy d -> 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 @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

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

instance TestEquality SRational where
  testEquality :: forall (a :: Rational) (b :: Rational).
SRational a -> SRational b -> Maybe (a :~: b)
testEquality (UnsafeSRational Rational
x) (UnsafeSRational Rational
y) = do
    Bool -> Maybe ()
forall (f :: Type -> Type). Alternative f => Bool -> f ()
guard (Rational -> Rational
toPrelude Rational
x Rational -> Rational -> Bool
forall a. Eq a => a -> a -> Bool
P.== Rational -> Rational
toPrelude Rational
y)
    (a :~: b) -> Maybe (a :~: b)
forall a. a -> Maybe a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure ((Any :~: Any) -> a :~: b
forall a b. a -> b
unsafeCoerce Any :~: Any
forall {k} (a :: k). a :~: a
Refl)

instance TestCoercion SRational where
  testCoercion :: forall (a :: Rational) (b :: Rational).
SRational a -> SRational b -> Maybe (Coercion a b)
testCoercion SRational a
x SRational b
y = ((a :~: b) -> Coercion a b)
-> Maybe (a :~: b) -> Maybe (Coercion a b)
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap (\a :~: b
Refl -> Coercion a b
forall {k} (a :: k) (b :: k). Coercible a b => Coercion a b
Coercion) (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 SRational a
x SRational b
y)

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

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

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