{-# LANGUAGE DataKinds                 #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE ExplicitNamespaces        #-}
{-# LANGUAGE FlexibleContexts          #-}
{-# LANGUAGE FlexibleInstances         #-}
{-# LANGUAGE MagicHash                 #-}
{-# LANGUAGE PolyKinds                 #-}
{-# LANGUAGE ScopedTypeVariables       #-}
{-# LANGUAGE Trustworthy               #-}
{-# LANGUAGE TypeApplications          #-}
{-# LANGUAGE TypeFamilies              #-}
{-# LANGUAGE TypeOperators             #-}
{-# LANGUAGE UndecidableInstances      #-}

{-|
Module: Data.TypeNums.Rats
Copyright: (c) 2018-2021 Iris Ward
License: BSD3
Maintainer: aditu.venyhandottir@gmail.com
Stability: experimental

Type level rational numbers expressed as a ratio between a type-level integer
and a type-level natural.  For example @'Neg' 3 :% 2@.

See also: "Data.TypeInts"
-}
module Data.TypeNums.Rats
  ( -- * Construction
    Rat((:%))
    -- * Linking type and value level
  , KnownRat
  , ratVal
  , ratVal'
  , SomeRat(..)
  , someRatVal
  ) where

import Data.TypeNums.Equality (type (/=))
import Data.TypeNums.Ints
import Data.TypeNums.Rats.Type(Rat(..))

import Data.Bifunctor (first)
import Data.Proxy     (Proxy (..))
import Data.Ratio     ((%))
import GHC.Exts       (Proxy#, proxy#)
import GHC.TypeLits   (ErrorMessage (..), KnownNat, Nat, TypeError, natVal')
import Unsafe.Coerce  (unsafeCoerce)

newtype SRat r =
  SRat Rational

-- | This class gives the (value-level) rational associated with a type-level
--   rational.  There are instances of this class for every combination of a
--   concrete integer and concrete natural.
class KnownRat r where
  ratSing :: SRat r

instance {-# OVERLAPPING #-} (TypeError ('Text "Denominator must not equal 0")) =>
                             KnownRat (n ':% 0) where
  ratSing :: SRat (n ':% 0)
ratSing = [Char] -> SRat (n ':% 0)
forall a. HasCallStack => [Char] -> a
error [Char]
"Unreachable"

instance {-# OVERLAPS #-} forall k (n :: k) (d :: Nat). (KnownInt n, KnownNat d, d /= 0) =>
                          KnownRat (n ':% d) where
  ratSing :: SRat (n ':% d)
ratSing = Rational -> SRat (n ':% d)
forall k (r :: k). Rational -> SRat r
SRat (Rational -> SRat (n ':% d)) -> Rational -> SRat (n ':% d)
forall a b. (a -> b) -> a -> b
$! Proxy# n -> Integer
forall k (n :: k). KnownInt n => Proxy# n -> Integer
intVal' (Proxy# n
forall k (a :: k). Proxy# a
proxy# :: Proxy# n) Integer -> Integer -> Rational
forall a. Integral a => a -> a -> Ratio a
% Proxy# d -> Integer
forall (n :: Nat). KnownNat n => Proxy# n -> Integer
natVal' (Proxy# d
forall k (a :: k). Proxy# a
proxy# :: Proxy# d)

instance {-# OVERLAPPABLE #-} forall k (n :: k). (KnownInt n) => KnownRat n where
  ratSing :: SRat n
ratSing = Rational -> SRat n
forall k (r :: k). Rational -> SRat r
SRat (Rational -> SRat n) -> Rational -> SRat n
forall a b. (a -> b) -> a -> b
$! Proxy# n -> Integer
forall k (n :: k). KnownInt n => Proxy# n -> Integer
intVal' (Proxy# n
forall k (a :: k). Proxy# a
proxy# :: Proxy# n) Integer -> Integer -> Rational
forall a. Integral a => a -> a -> Ratio a
% Integer
1

-- | Get the value associated with a type-level rational
ratVal ::
     forall proxy r. KnownRat r
  => proxy r
  -> Rational
ratVal :: proxy r -> Rational
ratVal proxy r
_ =
  case SRat r
forall k (r :: k). KnownRat r => SRat r
ratSing :: SRat r of
    SRat Rational
x -> Rational
x

-- | Get the value associated with a type-level rational.  The difference
--   between this function and 'ratVal' is that it takes a 'Proxy#' parameter,
--   which has zero runtime representation and so is entirely free.
ratVal' ::
     forall r. KnownRat r
  => Proxy# r
  -> Rational
ratVal' :: Proxy# r -> Rational
ratVal' Proxy# r
_ =
  case SRat r
forall k (r :: k). KnownRat r => SRat r
ratSing :: SRat r of
    SRat Rational
x -> Rational
x

-- | This type represents unknown type-level integers.
--
-- @since 0.1.1
data SomeRat =
  forall r. KnownRat r =>
            SomeRat (Proxy r)

instance Eq SomeRat where
  SomeRat Proxy r
x == :: SomeRat -> SomeRat -> Bool
== SomeRat Proxy r
y = Proxy r -> Rational
forall k (proxy :: k -> *) (r :: k).
KnownRat r =>
proxy r -> Rational
ratVal Proxy r
x Rational -> Rational -> Bool
forall a. Eq a => a -> a -> Bool
== Proxy r -> Rational
forall k (proxy :: k -> *) (r :: k).
KnownRat r =>
proxy r -> Rational
ratVal Proxy r
y

instance Ord SomeRat where
  compare :: SomeRat -> SomeRat -> Ordering
compare (SomeRat Proxy r
x) (SomeRat Proxy r
y) = Rational -> Rational -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (Proxy r -> Rational
forall k (proxy :: k -> *) (r :: k).
KnownRat r =>
proxy r -> Rational
ratVal Proxy r
x) (Proxy r -> Rational
forall k (proxy :: k -> *) (r :: k).
KnownRat r =>
proxy r -> Rational
ratVal Proxy r
y)

instance Show SomeRat where
  showsPrec :: Int -> SomeRat -> ShowS
showsPrec Int
p (SomeRat Proxy r
x) = Int -> Rational -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
p (Proxy r -> Rational
forall k (proxy :: k -> *) (r :: k).
KnownRat r =>
proxy r -> Rational
ratVal Proxy r
x)

instance Read SomeRat where
  readsPrec :: Int -> ReadS SomeRat
readsPrec Int
p [Char]
xs = (Rational -> SomeRat) -> (Rational, [Char]) -> (SomeRat, [Char])
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first Rational -> SomeRat
someRatVal ((Rational, [Char]) -> (SomeRat, [Char]))
-> [(Rational, [Char])] -> [(SomeRat, [Char])]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Int -> ReadS Rational
forall a. Read a => Int -> ReadS a
readsPrec Int
p [Char]
xs

-- For implementation notes, see $impl in "Data.TypeNats.Ints"

data SomeRatWithDict =
  forall r. SomeRatWithDict (SRat r)
                            (Proxy r)

-- | Convert a rational into an unknown type-level rational.
--
-- @since 0.1.1
someRatVal :: Rational -> SomeRat
someRatVal :: Rational -> SomeRat
someRatVal Rational
r = SomeRatWithDict -> SomeRat
forall a b. a -> b
unsafeCoerce (SomeRatWithDict -> SomeRat) -> SomeRatWithDict -> SomeRat
forall a b. (a -> b) -> a -> b
$ SRat Any -> Proxy Any -> SomeRatWithDict
forall k (r :: k). SRat r -> Proxy r -> SomeRatWithDict
SomeRatWithDict (Rational -> SRat Any
forall k (r :: k). Rational -> SRat r
SRat Rational
r) Proxy Any
forall k (t :: k). Proxy t
Proxy