{-# LANGUAGE DataKinds             #-}
{-# LANGUAGE DeriveAnyClass        #-}
{-# LANGUAGE DeriveGeneric         #-}
{-# LANGUAGE DerivingStrategies    #-}
{-# LANGUAGE FlexibleContexts      #-}
{-# LANGUAGE FlexibleInstances     #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE MultiWayIf            #-}
{-# LANGUAGE OverloadedStrings     #-}
{-# LANGUAGE TemplateHaskell       #-}
{-# LANGUAGE TypeApplications      #-}
{-# LANGUAGE TypeFamilies          #-}
{-# LANGUAGE UndecidableInstances  #-}
{-# OPTIONS_GHC -fplugin-opt PlutusTx.Plugin:context-level=3 #-}

module PlutusTx.Ratio(
    -- * Type
    Rational
    -- * Construction
    , unsafeRatio
    , fromInteger
    , ratio
    -- * Other functionality
    , numerator
    , denominator
    , round
    , truncate
    , properFraction
    , recip
    , abs
    , negate
    , half
    , fromGHC
    , toGHC
    , gcd
    ) where

import PlutusTx.Applicative qualified as P
import PlutusTx.Base qualified as P
import PlutusTx.Bool qualified as P
import PlutusTx.Eq qualified as P
import PlutusTx.ErrorCodes qualified as P
import PlutusTx.Integer (Integer)
import PlutusTx.IsData qualified as P
import PlutusTx.Lift (makeLift)
import PlutusTx.Maybe qualified as P
import PlutusTx.Numeric qualified as P
import PlutusTx.Ord qualified as P
import PlutusTx.Trace qualified as P

import PlutusTx.Builtins qualified as Builtins

import Control.Monad (guard)
import Data.Aeson (FromJSON (parseJSON), ToJSON (toJSON), object, withObject, (.:))
import GHC.Generics
import GHC.Real qualified as Ratio
import PlutusTx.Blueprint.Class (HasBlueprintSchema (..))
import PlutusTx.Blueprint.Definition (HasBlueprintDefinition (..), HasSchemaDefinition)
import Prelude (Ord (..), Show, (*))
import Prelude qualified as Haskell
import Prettyprinter (Pretty (..), (<+>))

-- | Represents an arbitrary-precision ratio.
--
-- The following two invariants are maintained:
--
-- 1. The denominator is greater than zero.
-- 2. The numerator and denominator are coprime.
data Rational = Rational Integer Integer
  deriving stock (Rational -> Rational -> Bool
(Rational -> Rational -> Bool)
-> (Rational -> Rational -> Bool) -> Eq Rational
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Rational -> Rational -> Bool
== :: Rational -> Rational -> Bool
$c/= :: Rational -> Rational -> Bool
/= :: Rational -> Rational -> Bool
Haskell.Eq, Int -> Rational -> ShowS
[Rational] -> ShowS
Rational -> String
(Int -> Rational -> ShowS)
-> (Rational -> String) -> ([Rational] -> ShowS) -> Show Rational
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Rational -> ShowS
showsPrec :: Int -> Rational -> ShowS
$cshow :: Rational -> String
show :: Rational -> String
$cshowList :: [Rational] -> ShowS
showList :: [Rational] -> ShowS
Show, (forall x. Rational -> Rep Rational x)
-> (forall x. Rep Rational x -> Rational) -> Generic Rational
forall x. Rep Rational x -> Rational
forall x. Rational -> Rep Rational x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. Rational -> Rep Rational x
from :: forall x. Rational -> Rep Rational x
$cto :: forall x. Rep Rational x -> Rational
to :: forall x. Rep Rational x -> Rational
Generic)

instance Pretty Rational where
  pretty :: forall ann. Rational -> Doc ann
pretty (Rational Integer
a Integer
b) = Doc ann
"Rational:" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Integer -> Doc ann
forall ann. Integer -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty Integer
a Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Integer -> Doc ann
forall ann. Integer -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty Integer
b

instance P.Eq Rational where
  {-# INLINABLE (==) #-}
  Rational Integer
n Integer
d == :: Rational -> Rational -> Bool
== Rational Integer
n' Integer
d' = Integer
n Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
P.== Integer
n' Bool -> Bool -> Bool
P.&& Integer
d Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
P.== Integer
d'

instance P.Ord Rational where
  {-# INLINABLE compare #-}
  compare :: Rational -> Rational -> Ordering
compare (Rational Integer
n Integer
d) (Rational Integer
n' Integer
d') = Integer -> Integer -> Ordering
forall a. Ord a => a -> a -> Ordering
P.compare (Integer
n Integer -> Integer -> Integer
forall a. MultiplicativeSemigroup a => a -> a -> a
P.* Integer
d') (Integer
n' Integer -> Integer -> Integer
forall a. MultiplicativeSemigroup a => a -> a -> a
P.* Integer
d)
  {-# INLINABLE (<=) #-}
  Rational Integer
n Integer
d <= :: Rational -> Rational -> Bool
<= Rational Integer
n' Integer
d' = (Integer
n Integer -> Integer -> Integer
forall a. MultiplicativeSemigroup a => a -> a -> a
P.* Integer
d') Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
P.<= (Integer
n' Integer -> Integer -> Integer
forall a. MultiplicativeSemigroup a => a -> a -> a
P.* Integer
d)
  {-# INLINABLE (>=) #-}
  Rational Integer
n Integer
d >= :: Rational -> Rational -> Bool
>= Rational Integer
n' Integer
d' = (Integer
n Integer -> Integer -> Integer
forall a. MultiplicativeSemigroup a => a -> a -> a
P.* Integer
d') Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
P.>= (Integer
n' Integer -> Integer -> Integer
forall a. MultiplicativeSemigroup a => a -> a -> a
P.* Integer
d)
  {-# INLINABLE (<) #-}
  Rational Integer
n Integer
d < :: Rational -> Rational -> Bool
< Rational Integer
n' Integer
d' = (Integer
n Integer -> Integer -> Integer
forall a. MultiplicativeSemigroup a => a -> a -> a
P.* Integer
d') Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
P.< (Integer
n' Integer -> Integer -> Integer
forall a. MultiplicativeSemigroup a => a -> a -> a
P.* Integer
d)
  {-# INLINABLE (>) #-}
  Rational Integer
n Integer
d > :: Rational -> Rational -> Bool
> Rational Integer
n' Integer
d' = (Integer
n Integer -> Integer -> Integer
forall a. MultiplicativeSemigroup a => a -> a -> a
P.* Integer
d') Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
P.> (Integer
n' Integer -> Integer -> Integer
forall a. MultiplicativeSemigroup a => a -> a -> a
P.* Integer
d)

instance Ord Rational where
  compare :: Rational -> Rational -> Ordering
compare (Rational Integer
n Integer
d) (Rational Integer
n' Integer
d') = Integer -> Integer -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (Integer
n Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Integer
d') (Integer
n' Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Integer
d)
  Rational Integer
n Integer
d <= :: Rational -> Rational -> Bool
<= Rational Integer
n' Integer
d' = (Integer
n Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Integer
d') Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= (Integer
n' Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Integer
d)
  Rational Integer
n Integer
d >= :: Rational -> Rational -> Bool
>= Rational Integer
n' Integer
d' = (Integer
n Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Integer
d') Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= (Integer
n' Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Integer
d)
  Rational Integer
n Integer
d < :: Rational -> Rational -> Bool
< Rational Integer
n' Integer
d' = (Integer
n Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Integer
d') Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< (Integer
n' Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Integer
d)
  Rational Integer
n Integer
d > :: Rational -> Rational -> Bool
> Rational Integer
n' Integer
d' = (Integer
n Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Integer
d') Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> (Integer
n' Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Integer
d)

instance P.AdditiveSemigroup Rational where
  {-# INLINABLE (+) #-}
  Rational Integer
n Integer
d + :: Rational -> Rational -> Rational
+ Rational Integer
n' Integer
d' =
    let newNum :: Integer
newNum = (Integer
n Integer -> Integer -> Integer
forall a. MultiplicativeSemigroup a => a -> a -> a
P.* Integer
d') Integer -> Integer -> Integer
forall a. AdditiveSemigroup a => a -> a -> a
P.+ (Integer
n' Integer -> Integer -> Integer
forall a. MultiplicativeSemigroup a => a -> a -> a
P.* Integer
d)
        newDen :: Integer
newDen = Integer
d Integer -> Integer -> Integer
forall a. MultiplicativeSemigroup a => a -> a -> a
P.* Integer
d'
        gcd' :: Integer
gcd' = Integer -> Integer -> Integer
euclid Integer
newNum Integer
newDen
     in Integer -> Integer -> Rational
Rational (Integer
newNum Integer -> Integer -> Integer
`Builtins.quotientInteger` Integer
gcd')
                 (Integer
newDen Integer -> Integer -> Integer
`Builtins.quotientInteger` Integer
gcd')

instance P.AdditiveMonoid Rational where
  {-# INLINABLE zero #-}
  zero :: Rational
zero = Integer -> Integer -> Rational
Rational Integer
forall a. AdditiveMonoid a => a
P.zero Integer
forall a. MultiplicativeMonoid a => a
P.one

instance P.AdditiveGroup Rational where
  {-# INLINABLE (-) #-}
  Rational Integer
n Integer
d - :: Rational -> Rational -> Rational
- Rational Integer
n' Integer
d' =
    let newNum :: Integer
newNum = (Integer
n Integer -> Integer -> Integer
forall a. MultiplicativeSemigroup a => a -> a -> a
P.* Integer
d') Integer -> Integer -> Integer
forall a. AdditiveGroup a => a -> a -> a
P.- (Integer
n' Integer -> Integer -> Integer
forall a. MultiplicativeSemigroup a => a -> a -> a
P.* Integer
d)
        newDen :: Integer
newDen = Integer
d Integer -> Integer -> Integer
forall a. MultiplicativeSemigroup a => a -> a -> a
P.* Integer
d'
        gcd' :: Integer
gcd' = Integer -> Integer -> Integer
euclid Integer
newNum Integer
newDen
     in Integer -> Integer -> Rational
Rational (Integer
newNum Integer -> Integer -> Integer
`Builtins.quotientInteger` Integer
gcd')
                 (Integer
newDen Integer -> Integer -> Integer
`Builtins.quotientInteger` Integer
gcd')

instance P.MultiplicativeSemigroup Rational where
  {-# INLINABLE (*) #-}
  Rational Integer
n Integer
d * :: Rational -> Rational -> Rational
* Rational Integer
n' Integer
d' =
    let newNum :: Integer
newNum = Integer
n Integer -> Integer -> Integer
forall a. MultiplicativeSemigroup a => a -> a -> a
P.* Integer
n'
        newDen :: Integer
newDen = Integer
d Integer -> Integer -> Integer
forall a. MultiplicativeSemigroup a => a -> a -> a
P.* Integer
d'
        gcd' :: Integer
gcd' = Integer -> Integer -> Integer
euclid Integer
newNum Integer
newDen
     in Integer -> Integer -> Rational
Rational (Integer
newNum Integer -> Integer -> Integer
`Builtins.quotientInteger` Integer
gcd')
                 (Integer
newDen Integer -> Integer -> Integer
`Builtins.quotientInteger` Integer
gcd')

instance P.MultiplicativeMonoid Rational where
  {-# INLINABLE one #-}
  one :: Rational
one = Integer -> Integer -> Rational
Rational Integer
forall a. MultiplicativeMonoid a => a
P.one Integer
forall a. MultiplicativeMonoid a => a
P.one

instance P.Module Integer Rational where
  {-# INLINABLE scale #-}
  scale :: Integer -> Rational -> Rational
scale Integer
i (Rational Integer
n Integer
d) = let newNum :: Integer
newNum = Integer
i Integer -> Integer -> Integer
forall a. MultiplicativeSemigroup a => a -> a -> a
P.* Integer
n
                               gcd' :: Integer
gcd' = Integer -> Integer -> Integer
euclid Integer
newNum Integer
d in
    Integer -> Integer -> Rational
Rational (Integer
newNum Integer -> Integer -> Integer
`Builtins.quotientInteger` Integer
gcd')
             (Integer
d Integer -> Integer -> Integer
`Builtins.quotientInteger` Integer
gcd')

instance HasBlueprintDefinition Rational where
  type Unroll Rational = '[Rational, Integer]

instance
  (HasSchemaDefinition Integer referencedTypes) =>
  HasBlueprintSchema Rational referencedTypes
  where
  schema :: Schema referencedTypes
schema = forall t (referencedTypes :: [*]).
HasBlueprintSchema t referencedTypes =>
Schema referencedTypes
schema @(Integer, Integer)

instance P.ToData Rational where
  {-# INLINABLE toBuiltinData #-}
  toBuiltinData :: Rational -> BuiltinData
toBuiltinData (Rational Integer
n Integer
d) = (Integer, Integer) -> BuiltinData
forall a. ToData a => a -> BuiltinData
P.toBuiltinData (Integer
n, Integer
d)

-- These instances ensure that the following invariants don't break:
--
-- 1. The denominator is greater than 0; and
-- 2. The numerator and denominator are coprime.
--
-- For invariant 1, fromBuiltinData yields Nothing on violation, while
-- unsafeFromData calls error. Invariant 2 is kept maintained by use of
-- unsafeRatio.

instance P.FromData Rational where
  {-# INLINABLE fromBuiltinData #-}
  fromBuiltinData :: BuiltinData -> Maybe Rational
fromBuiltinData BuiltinData
dat = do
    (Integer
n, Integer
d) <- BuiltinData -> Maybe (Integer, Integer)
forall a. FromData a => BuiltinData -> Maybe a
P.fromBuiltinData BuiltinData
dat
    Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Integer
d Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
P./= Integer
forall a. AdditiveMonoid a => a
P.zero)
    Rational -> Maybe Rational
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
P.pure (Rational -> Maybe Rational)
-> (Integer -> Rational) -> Integer -> Maybe Rational
forall b c a. (b -> c) -> (a -> b) -> a -> c
P.. Integer -> Integer -> Rational
unsafeRatio Integer
n (Integer -> Maybe Rational) -> Integer -> Maybe Rational
forall a b. (a -> b) -> a -> b
P.$ Integer
d

instance P.UnsafeFromData Rational where
  {-# INLINABLE unsafeFromBuiltinData #-}
  unsafeFromBuiltinData :: BuiltinData -> Rational
unsafeFromBuiltinData = (Integer -> Integer -> Rational) -> (Integer, Integer) -> Rational
forall a b c. (a -> b -> c) -> (a, b) -> c
P.uncurry Integer -> Integer -> Rational
unsafeRatio ((Integer, Integer) -> Rational)
-> (BuiltinData -> (Integer, Integer)) -> BuiltinData -> Rational
forall b c a. (b -> c) -> (a -> b) -> a -> c
P.. BuiltinData -> (Integer, Integer)
forall a. UnsafeFromData a => BuiltinData -> a
P.unsafeFromBuiltinData

-- | This mimics the behaviour of Aeson's instance for 'GHC.Rational'.
instance ToJSON Rational where
  toJSON :: Rational -> Value
toJSON (Rational Integer
n Integer
d) =
    [Pair] -> Value
object
      [ (Key
"numerator", Integer -> Value
forall a. ToJSON a => a -> Value
toJSON Integer
n)
      , (Key
"denominator", Integer -> Value
forall a. ToJSON a => a -> Value
toJSON Integer
d)
      ]

-- | This mimics the behaviour of Aeson's instance for 'GHC.Rational'.
instance FromJSON Rational where
  parseJSON :: Value -> Parser Rational
parseJSON = String -> (Object -> Parser Rational) -> Value -> Parser Rational
forall a. String -> (Object -> Parser a) -> Value -> Parser a
withObject String
"Rational" ((Object -> Parser Rational) -> Value -> Parser Rational)
-> (Object -> Parser Rational) -> Value -> Parser Rational
forall a b. (a -> b) -> a -> b
Haskell.$ \Object
obj -> do
    Integer
n <- Object
obj Object -> Key -> Parser Integer
forall a. FromJSON a => Object -> Key -> Parser a
.: Key
"numerator"
    Integer
d <- Object
obj Object -> Key -> Parser Integer
forall a. FromJSON a => Object -> Key -> Parser a
.: Key
"denominator"
    case Integer -> Integer -> Maybe Rational
ratio Integer
n Integer
d of
      Maybe Rational
Haskell.Nothing -> String -> Parser Rational
forall a. String -> Parser a
forall (m :: * -> *) a. MonadFail m => String -> m a
Haskell.fail String
"Zero denominator is invalid."
      Haskell.Just Rational
r  -> Rational -> Parser Rational
forall a. a -> Parser a
forall (f :: * -> *) a. Applicative f => a -> f a
Haskell.pure Rational
r

-- | Makes a 'Rational' from a numerator and a denominator.
--
-- = Important note
--
-- If given a zero denominator, this function will error. If you don't mind a
-- size increase, and care about safety, use 'ratio' instead.
unsafeRatio :: Integer -> Integer -> Rational
unsafeRatio :: Integer -> Integer -> Rational
unsafeRatio Integer
n Integer
d
  | Integer
d Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
P.== Integer
forall a. AdditiveMonoid a => a
P.zero = BuiltinString -> Rational
forall a. BuiltinString -> a
P.traceError BuiltinString
P.ratioHasZeroDenominatorError
  | Integer
d Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
P.< Integer
forall a. AdditiveMonoid a => a
P.zero = Integer -> Integer -> Rational
unsafeRatio (Integer -> Integer
forall a. AdditiveGroup a => a -> a
P.negate Integer
n) (Integer -> Integer
forall a. AdditiveGroup a => a -> a
P.negate Integer
d)
  | Bool
P.True =
    let gcd' :: Integer
gcd' = Integer -> Integer -> Integer
euclid Integer
n Integer
d
     in Integer -> Integer -> Rational
Rational (Integer
n Integer -> Integer -> Integer
`Builtins.quotientInteger` Integer
gcd')
                 (Integer
d Integer -> Integer -> Integer
`Builtins.quotientInteger` Integer
gcd')
{-# INLINABLE unsafeRatio #-}

-- | Safely constructs a 'Rational' from a numerator and a denominator. Returns
-- 'Nothing' if given a zero denominator.
ratio :: Integer -> Integer -> P.Maybe Rational
ratio :: Integer -> Integer -> Maybe Rational
ratio Integer
n Integer
d
  | Integer
d Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
P.== Integer
forall a. AdditiveMonoid a => a
P.zero = Maybe Rational
forall a. Maybe a
P.Nothing
  | Integer
d Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
P.< Integer
forall a. AdditiveMonoid a => a
P.zero = Rational -> Maybe Rational
forall a. a -> Maybe a
P.Just (Integer -> Integer -> Rational
unsafeRatio (Integer -> Integer
forall a. AdditiveGroup a => a -> a
P.negate Integer
n) (Integer -> Integer
forall a. AdditiveGroup a => a -> a
P.negate Integer
d))
  | Bool
P.True =
    let gcd' :: Integer
gcd' = Integer -> Integer -> Integer
euclid Integer
n Integer
d
     in Rational -> Maybe Rational
forall a. a -> Maybe a
P.Just (Rational -> Maybe Rational) -> Rational -> Maybe Rational
forall a b. (a -> b) -> a -> b
P.$
          Integer -> Integer -> Rational
Rational (Integer
n Integer -> Integer -> Integer
`Builtins.quotientInteger` Integer
gcd')
                   (Integer
d Integer -> Integer -> Integer
`Builtins.quotientInteger` Integer
gcd')
{-# INLINABLE ratio #-}

-- | Converts a 'Rational' to a GHC 'Ratio.Rational', preserving value. Does not
-- work on-chain.
toGHC :: Rational -> Ratio.Rational
toGHC :: Rational -> Rational
toGHC (Rational Integer
n Integer
d) = Integer
n Integer -> Integer -> Rational
forall a. Integral a => a -> a -> Ratio a
Ratio.% Integer
d

-- | Returns the numerator of its argument.
--
-- = Note
--
-- It is /not/ true in general that @'numerator' '<$>' 'ratio' x y = x@; this
-- will only hold if @x@ and @y@ are coprime. This is due to 'Rational'
-- normalizing the numerator and denominator.
numerator :: Rational -> Integer
numerator :: Rational -> Integer
numerator (Rational Integer
n Integer
_) = Integer
n
{-# INLINABLE numerator #-}

-- | Returns the denominator of its argument. This will always be greater than,
-- or equal to, 1, although the type does not describe this.
--
-- = Note
--
-- It is /not/ true in general that @'denominator' '<$>' 'ratio' x y = y@; this
-- will only hold if @x@ and @y@ are coprime. This is due to 'Rational'
-- normalizing the numerator and denominator.
denominator :: Rational -> Integer
denominator :: Rational -> Integer
denominator (Rational Integer
_ Integer
d) = Integer
d
{-# INLINABLE denominator #-}

-- | 0.5
half :: Rational
half :: Rational
half = Integer -> Integer -> Rational
Rational Integer
1 Integer
2
{-# INLINABLE half #-}

-- | Converts an 'Integer' into the equivalent 'Rational'.
fromInteger :: Integer -> Rational
fromInteger :: Integer -> Rational
fromInteger Integer
num = Integer -> Integer -> Rational
Rational Integer
num Integer
forall a. MultiplicativeMonoid a => a
P.one
{-# INLINABLE fromInteger #-}

-- | Converts a GHC 'Ratio.Rational', preserving value. Does not work on-chain.
fromGHC :: Ratio.Rational -> Rational
fromGHC :: Rational -> Rational
fromGHC Rational
r = Integer -> Integer -> Rational
unsafeRatio (Rational -> Integer
forall a. Ratio a -> a
Ratio.numerator Rational
r) (Rational -> Integer
forall a. Ratio a -> a
Ratio.denominator Rational
r)

-- | Produces the additive inverse of its argument.
--
-- = Note
--
-- This is specialized for 'Rational'; use this instead of the generic version
-- of this function, as it is significantly smaller on-chain.
negate :: Rational -> Rational
negate :: Rational -> Rational
negate (Rational Integer
n Integer
d) = Integer -> Integer -> Rational
Rational (Integer -> Integer
forall a. AdditiveGroup a => a -> a
P.negate Integer
n) Integer
d
{-# INLINABLE negate #-}

-- | Returns the absolute value of its argument.
--
-- = Note
--
-- This is specialized for 'Rational'; use this instead of the generic version
-- in @PlutusTx.Numeric@, as said generic version produces much larger on-chain
-- code than the specialized version here.
abs :: Rational -> Rational
abs :: Rational -> Rational
abs rat :: Rational
rat@(Rational Integer
n Integer
d)
  | Integer
n Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
P.< Integer
forall a. AdditiveMonoid a => a
P.zero = Integer -> Integer -> Rational
Rational (Integer -> Integer
forall a. AdditiveGroup a => a -> a
P.negate Integer
n) Integer
d
  | Bool
P.True = Rational
rat
{-# INLINABLE abs #-}

-- | @'properFraction' r@ returns the pair @(n, f)@, such that all of the
-- following hold:
--
-- * @'fromInteger' n 'P.+' f = r@;
-- * @n@ and @f@ both have the same sign as @r@; and
-- * @'abs' f 'P.<' 'P.one'@.
properFraction :: Rational -> (Integer, Rational)
properFraction :: Rational -> (Integer, Rational)
properFraction (Rational Integer
n Integer
d) =
  (Integer
n Integer -> Integer -> Integer
`Builtins.quotientInteger` Integer
d,
   Integer -> Integer -> Rational
Rational (Integer
n Integer -> Integer -> Integer
`Builtins.remainderInteger` Integer
d) Integer
d)
{-# INLINABLE properFraction #-}

-- | Gives the reciprocal of the argument; specifically, for @r 'P./='
-- 'P.zero'@, @r 'P.*' 'recip' r = 'P.one'@.
--
-- = Important note
--
-- The reciprocal of zero is mathematically undefined; thus, @'recip' 'P.zero'@
-- will error. Use with care.
recip :: Rational -> Rational
recip :: Rational -> Rational
recip (Rational Integer
n Integer
d)
  | Integer
n Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
P.== Integer
forall a. AdditiveMonoid a => a
P.zero = BuiltinString -> Rational
forall a. BuiltinString -> a
P.traceError BuiltinString
P.reciprocalOfZeroError
  | Integer
n Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
P.< Integer
forall a. AdditiveMonoid a => a
P.zero = Integer -> Integer -> Rational
Rational (Integer -> Integer
forall a. AdditiveGroup a => a -> a
P.negate Integer
d) (Integer -> Integer
forall a. AdditiveGroup a => a -> a
P.negate Integer
n)
  | Bool
P.True = Integer -> Integer -> Rational
Rational Integer
d Integer
n
{-# INLINABLE recip #-}

-- | Returns the whole-number part of its argument, dropping any leftover
-- fractional part. More precisely, @'truncate' r = n@ where @(n, _) =
-- 'properFraction' r@, but is much more efficient.
truncate :: Rational -> Integer
truncate :: Rational -> Integer
truncate (Rational Integer
n Integer
d) = Integer
n Integer -> Integer -> Integer
`Builtins.quotientInteger` Integer
d
{-# INLINABLE truncate #-}

-- | @'round' r@ returns the nearest 'Integer' value to @r@. If @r@ is
-- equidistant between two values, the even value will be given.
round :: Rational -> Integer
round :: Rational -> Integer
round Rational
x =
  let (Integer
n, Rational
r) = Rational -> (Integer, Rational)
properFraction Rational
x
      m :: Integer
m = if Rational
r Rational -> Rational -> Bool
forall a. Ord a => a -> a -> Bool
P.< Rational
forall a. AdditiveMonoid a => a
P.zero then Integer
n Integer -> Integer -> Integer
forall a. AdditiveGroup a => a -> a -> a
P.- Integer
forall a. MultiplicativeMonoid a => a
P.one else Integer
n Integer -> Integer -> Integer
forall a. AdditiveSemigroup a => a -> a -> a
P.+ Integer
forall a. MultiplicativeMonoid a => a
P.one
      flag :: Rational
flag = Rational -> Rational
abs Rational
r Rational -> Rational -> Rational
forall a. AdditiveGroup a => a -> a -> a
P.- Rational
half
   in if
          | Rational
flag Rational -> Rational -> Bool
forall a. Ord a => a -> a -> Bool
P.< Rational
forall a. AdditiveMonoid a => a
P.zero -> Integer
n
          | Rational
flag Rational -> Rational -> Bool
forall a. Eq a => a -> a -> Bool
P.== Rational
forall a. AdditiveMonoid a => a
P.zero -> if Integer -> Integer -> Integer
Builtins.modInteger Integer
n Integer
2 Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
P.== Integer
forall a. AdditiveMonoid a => a
P.zero
                                then Integer
n
                                else Integer
m
          | Bool
P.True -> Integer
m
{-# INLINABLE round #-}

-- From GHC.Real
-- | @'gcd' x y@ is the non-negative factor of both @x@ and @y@ of which
-- every common factor of @x@ and @y@ is also a factor; for example
-- @'gcd' 4 2 = 2@, @'gcd' (-4) 6 = 2@, @'gcd' 0 4@ = @4@. @'gcd' 0 0@ = @0@.
gcd :: Integer -> Integer -> Integer
gcd :: Integer -> Integer -> Integer
gcd Integer
a Integer
b = Integer -> Integer -> Integer
gcd' (Integer -> Integer
forall n. (Ord n, AdditiveGroup n) => n -> n
P.abs Integer
a) (Integer -> Integer
forall n. (Ord n, AdditiveGroup n) => n -> n
P.abs Integer
b) where
    gcd' :: Integer -> Integer -> Integer
gcd' Integer
a' Integer
b'
        | Integer
b' Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
P.== Integer
forall a. AdditiveMonoid a => a
P.zero = Integer
a'
        | Bool
P.True         = Integer -> Integer -> Integer
gcd' Integer
b' (Integer
a' Integer -> Integer -> Integer
`Builtins.remainderInteger` Integer
b')
{-# INLINABLE gcd #-}

-- Helpers

-- Euclid's algorithm
euclid :: Integer -> Integer -> Integer
euclid :: Integer -> Integer -> Integer
euclid Integer
x Integer
y
  | Integer
y Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
P.== Integer
forall a. AdditiveMonoid a => a
P.zero = Integer
x
  | Bool
P.True = Integer -> Integer -> Integer
euclid Integer
y (Integer
x Integer -> Integer -> Integer
`Builtins.modInteger` Integer
y)
{-# INLINABLE euclid #-}

$(makeLift ''Rational)

{- HLINT ignore -}

{- Note [Ratio]

An important invariant is that the denominator is always positive. This is
enforced by

* Construction of 'Rational' numbers with 'unsafeRatio' (the constructor
  of 'Rational' is not exposed)
* Normalizing after every numeric operation.

The 'StdLib.Spec' module has some property tests that check the behaviour of
'round', 'truncate', '>=', etc. against that of their counterparts in
'GHC.Real'.

-}

{- Note [Integer division operations]

Plutus Core provides built-in functions 'divideInteger', 'modInteger',
'quotientInteger' and 'remainderInteger' which are implemented as the Haskell
functions 'div', 'mod', 'quot', and 'rem' respectively.

The operations 'div' and 'mod' go together, as do 'quot' and 'rem': * DO NOT use
'div' with 'rem' or 'quot' with 'mod' *.  For most purposes users shoud probably
use 'div' and 'mod': see below for details.

For any integers a and b with b nonzero we have

  a * (a  `div` b) + a `mod` b = a
  a * (a `quot` b) + a `rem` b = a

(all operations give a "divide by zero" error if b = 0).  The analagous
identities for div/rem and quot/mod don't hold in general, and this can
lead to problems if you use the wrong combination of operations.

For positive divisors b, div truncates downwards and mod always returns a
non-negative result (0 <= a `mod` b <= b-1), which is consistent with standard
mathematical practice.  The `quot` operation truncates towards zero and `rem`
will give a negative remainder if a<0 and b>0.  If a<0 and b<0 then `mod` willl
also yield a negative result.  Results for different combinations of signs are
shown below.

-------------------------------
|   n  d | div mod | quot rem |
|-----------------------------|
|  41  5 |  8   1  |   8   1  |
| -41  5 | -9   4  |  -8  -1  |
|  41 -5 | -9  -4  |  -8   1  |
| -41 -5 |  8  -1  |   8  -1  |
-------------------------------

For many purposes (in particular if you're doing modular arithmetic),
a positive remainder is what you want.  Using 'div' and 'mod' achieves
this for positive values of b (but not for b negative, although doing
artimetic modulo a negative number would be unusual).

There is another possibility (Euclidean division) which is arguably more
mathematically correct than both div/mod and quot/rem. Given integers a and b
with b != 0, this returns numbers q and r with a = q*b+r and 0 <= r < |b|.  For
the numbers above this gives

-------------------
|   n  d |  q   r |
|-----------------|
|  41  5 |  8   1 |
| -41  5 | -9   4 |
|  41 -5 | -8   1 |
| -41 -5 |  9   4 |
-------------------

We get a positive remainder in all cases, but note for instance that the pairs
(41,5) and (-41,-5) give different results, which might be unexpected.

For a discussion of the pros and cons of various versions of integer division,
see Raymond T. Boute, "The Euclidean definition of the functions div and mod",
ACM Transactions on Programming Languages and Systems, April 1992.  (PDF at
https://core.ac.uk/download/pdf/187613369.pdf)
-}