-- SPDX-FileCopyrightText: 2021 Tocqueville Group
--
-- SPDX-License-Identifier: LicenseRef-MIT-TQ

{-# LANGUAGE RebindableSyntax #-}
{-# LANGUAGE NoApplicativeDo #-}
{-# OPTIONS_GHC -Wno-unused-do-bind #-}
{-# OPTIONS_GHC -Wno-orphans #-}

module Lorentz.CustomArith.Conversions
 ( -- * Rational to Fixed/NFixed
   convertFixedToRational
 , convertNFixedToRational
 , convertRationalToFixed
 , convertRationalToNFixed
 , unsafeConvertRationalToNFixed

   -- * NRational to Fixed/NFixed
 , convertFixedToNRational
 , unsafeConvertFixedToNRational
 , convertNFixedToNRational
 , convertNRationalToFixed
 , convertNRationalToNFixed
 ) where

import Data.Fixed (HasResolution)
import Prelude (Maybe)

import Lorentz.CustomArith.FixedArith
import Lorentz.CustomArith.RationalArith

import Lorentz.Base
import Lorentz.Coercions
import Lorentz.Errors
import Lorentz.Instr
import Lorentz.Macro
import Lorentz.Rebinded

convertRationalToNRational :: Rational : s :-> Maybe (NRational) : s
convertRationalToNRational :: forall (s :: [*]). (Rational : s) :-> (Maybe NRational : s)
convertRationalToNRational = do
  (Rational : s) :-> (Rational : Rational : s)
forall a (s :: [*]). Dupable a => (a : s) :-> (a : a : s)
dup; (Rational : Rational : s) :-> (Integer : Rational : s)
forall r a (s :: [*]).
(LorentzRational r, Unwrappabled r ~ (a, Natural)) =>
(r : s) :-> (a : s)
numerator
  ((Rational : s) :-> (Maybe NRational : s))
-> ((Rational : s) :-> (Maybe NRational : s))
-> (Integer : Rational : s) :-> (Maybe NRational : s)
forall a (s :: [*]) (s' :: [*]).
IfCmp0Constraints a Ge =>
(s :-> s') -> (s :-> s') -> (a : s) :-> s'
ifGe0 ((Rational : s) :-> (NRational : s)
forall (s :: [*]). (Rational : s) :-> (NRational : s)
unsafeConvertRationalToNRational ((Rational : s) :-> (NRational : s))
-> ((NRational : s) :-> (Maybe NRational : s))
-> (Rational : s) :-> (Maybe NRational : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (NRational : s) :-> (Maybe NRational : s)
forall a (s :: [*]). (a : s) :-> (Maybe a : s)
some) ((Rational : s) :-> s
forall a (s :: [*]). (a : s) :-> s
drop ((Rational : s) :-> s)
-> (s :-> (Maybe NRational : s))
-> (Rational : s) :-> (Maybe NRational : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# s :-> (Maybe NRational : s)
forall a (s :: [*]). KnownValue a => s :-> (Maybe a : s)
none)

unsafeConvertRationalToNRational :: Rational : s :-> NRational : s
unsafeConvertRationalToNRational :: forall (s :: [*]). (Rational : s) :-> (NRational : s)
unsafeConvertRationalToNRational = (Rational : s) :-> (Integer : Natural : s)
forall r a (s :: [*]).
(LorentzRational r, Unwrappabled r ~ (a, Natural)) =>
(r : s) :-> (a : Natural : s)
deconstructRational ((Rational : s) :-> (Integer : Natural : s))
-> ((Integer : Natural : s) :-> (Natural : Natural : s))
-> (Rational : s) :-> (Natural : Natural : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (Integer : Natural : s) :-> (Natural : Natural : s)
forall n (s :: [*]).
UnaryArithOpHs Abs n =>
(n : s) :-> (UnaryArithResHs Abs n : s)
abs ((Rational : s) :-> (Natural : Natural : s))
-> ((Natural : Natural : s) :-> (NRational : s))
-> (Rational : s) :-> (NRational : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (Natural : Natural : s) :-> (NRational : s)
forall r a (s :: [*]).
(LorentzRational r, Unwrappabled r ~ (a, Natural)) =>
(a : Natural : s) :-> (r : s)
constructRational

convertNRationalToRational :: NRational : s :-> Rational : s
convertNRationalToRational :: forall (s :: [*]). (NRational : s) :-> (Rational : s)
convertNRationalToRational = (NRational : s) :-> (Natural : Natural : s)
forall r a (s :: [*]).
(LorentzRational r, Unwrappabled r ~ (a, Natural)) =>
(r : s) :-> (a : Natural : s)
deconstructRational ((NRational : s) :-> (Natural : Natural : s))
-> ((Natural : Natural : s) :-> (Integer : Natural : s))
-> (NRational : s) :-> (Integer : Natural : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (Natural : Natural : s) :-> (Integer : Natural : s)
forall i (s :: [*]).
ToIntegerArithOpHs i =>
(i : s) :-> (Integer : s)
int ((NRational : s) :-> (Integer : Natural : s))
-> ((Integer : Natural : s) :-> (Rational : s))
-> (NRational : s) :-> (Rational : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (Integer : Natural : s) :-> (Rational : s)
forall r a (s :: [*]).
(LorentzRational r, Unwrappabled r ~ (a, Natural)) =>
(a : Natural : s) :-> (r : s)
constructRational

----------------------------------------------------------------------------------------------------
-- Rationals
----------------------------------------------------------------------------------------------------

-- | Converts 'Rational' to 'Fixed' using value inside as numerator and base as denominator
convertFixedToRational :: forall a s. HasResolution a =>  Fixed a : s :-> Rational : s
convertFixedToRational :: forall {k} (a :: k) (s :: [*]).
HasResolution a =>
(Fixed a : s) :-> (Rational : s)
convertFixedToRational = do
  (Fixed a : s) :-> (Integer : s)
forall a (s :: [*]).
Unwrappable a =>
(a : s) :-> (Unwrappabled a : s)
coerceUnwrap
  Natural -> (Integer : s) :-> (Natural : Integer : s)
forall t (s :: [*]). NiceConstant t => t -> s :-> (t : s)
push (forall (a :: k). HasResolution a => Natural
forall {k} (a :: k). HasResolution a => Natural
resolution_ @a)
  (Natural : Integer : s) :-> (Integer : Natural : s)
forall a b (s :: [*]). (a : b : s) :-> (b : a : s)
swap
  (Integer : Natural : s) :-> (Rational : s)
forall r a (s :: [*]).
(LorentzRational r, Unwrappabled r ~ (a, Natural)) =>
(a : Natural : s) :-> (r : s)
constructRational

-- | Converts 'Rational' to 'NFixed' using value inside as numerator and base as denominator
convertNFixedToRational ::forall a s. HasResolution a => NFixed a : s :-> Rational : s
convertNFixedToRational :: forall {k} (a :: k) (s :: [*]).
HasResolution a =>
(NFixed a : s) :-> (Rational : s)
convertNFixedToRational = do
  (NFixed a : s) :-> (Natural : s)
forall a (s :: [*]).
Unwrappable a =>
(a : s) :-> (Unwrappabled a : s)
coerceUnwrap; (Natural : s) :-> (Integer : s)
forall i (s :: [*]).
ToIntegerArithOpHs i =>
(i : s) :-> (Integer : s)
int
  Natural -> (Integer : s) :-> (Natural : Integer : s)
forall t (s :: [*]). NiceConstant t => t -> s :-> (t : s)
push (forall (a :: k). HasResolution a => Natural
forall {k} (a :: k). HasResolution a => Natural
resolution_ @a)
  (Natural : Integer : s) :-> (Integer : Natural : s)
forall a b (s :: [*]). (a : b : s) :-> (b : a : s)
swap
  (Integer : Natural : s) :-> (Rational : s)
forall r a (s :: [*]).
(LorentzRational r, Unwrappabled r ~ (a, Natural)) =>
(a : Natural : s) :-> (r : s)
constructRational

-- | Converts 'Fixed' to 'Rational' according to formulae: numerator * base / denominator
-- Note: Since result's base is determined by user, it is recommended to use higher value in order to achieve
-- better accuracy
convertRationalToFixed :: forall a s. HasResolution a => Rational : s :-> Fixed a : s
convertRationalToFixed :: forall {k} (a :: k) (s :: [*]).
HasResolution a =>
(Rational : s) :-> (Fixed a : s)
convertRationalToFixed = do
  (Rational : s) :-> (Integer : Natural : s)
forall r a (s :: [*]).
(LorentzRational r, Unwrappabled r ~ (a, Natural)) =>
(r : s) :-> (a : Natural : s)
deconstructRational
  Natural
-> (Integer : Natural : s) :-> (Natural : Integer : Natural : s)
forall t (s :: [*]). NiceConstant t => t -> s :-> (t : s)
push (forall (a :: k). HasResolution a => Natural
forall {k} (a :: k). HasResolution a => Natural
resolution_ @a)
  (Natural : Integer : Natural : s) :-> (Integer : Natural : s)
forall n m r (s :: [*]).
ArithOpHs Mul n m r =>
(n : m : s) :-> (r : s)
mul
  (Integer : Natural : s) :-> (Maybe (Integer, Natural) : s)
forall n m r (s :: [*]).
ArithOpHs EDiv n m r =>
(n : m : s) :-> (r : s)
ediv
  Impossible "Division by zero impossible"
-> (Maybe (Integer, Natural) : s) :-> ((Integer, Natural) : s)
forall err a (s :: [*]).
IsError err =>
err -> (Maybe a : s) :-> (a : s)
assertSome (forall (reason :: Symbol). HasCallStack => Impossible reason
Impossible @"Division by zero impossible")
  ((Integer, Natural) : s) :-> (Integer : Natural : s)
forall a b (s :: [*]). ((a, b) : s) :-> (a : b : s)
unpair
  (Integer : Natural : s) :-> (Integer : s)
forall n m r (s :: [*]).
ArithOpHs Add n m r =>
(n : m : s) :-> (r : s)
add
  (Integer : s) :-> (Fixed a : s)
forall a (s :: [*]).
Unwrappable a =>
(Unwrappabled a : s) :-> (a : s)
unsafeCoerceWrap

unsafeConvertRationalToNFixed :: forall a s. HasResolution a => Rational : s :-> NFixed a : s
unsafeConvertRationalToNFixed :: forall {k} (a :: k) (s :: [*]).
HasResolution a =>
(Rational : s) :-> (NFixed a : s)
unsafeConvertRationalToNFixed = (Rational : s) :-> (Fixed a : s)
forall {k} (a :: k) (s :: [*]).
HasResolution a =>
(Rational : s) :-> (Fixed a : s)
convertRationalToFixed ((Rational : s) :-> (Fixed a : s))
-> ((Fixed a : s) :-> (NFixed a : s))
-> (Rational : s) :-> (NFixed a : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (Fixed a : s) :-> (NFixed a : s)
forall {k} (p :: k) (s :: [*]). (Fixed p : s) :-> (NFixed p : s)
unsafeCastFixedToNFixed

convertRationalToNFixed :: forall a s. HasResolution a => Rational : s :-> Maybe (NFixed a) : s
convertRationalToNFixed :: forall {k} (a :: k) (s :: [*]).
HasResolution a =>
(Rational : s) :-> (Maybe (NFixed a) : s)
convertRationalToNFixed = (Rational : s) :-> (Fixed a : s)
forall {k} (a :: k) (s :: [*]).
HasResolution a =>
(Rational : s) :-> (Fixed a : s)
convertRationalToFixed ((Rational : s) :-> (Fixed a : s))
-> ((Fixed a : s) :-> (Maybe (NFixed a) : s))
-> (Rational : s) :-> (Maybe (NFixed a) : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (Fixed a : s) :-> (Maybe (NFixed a) : s)
forall {k} (p :: k) (s :: [*]).
(Fixed p : s) :-> (Maybe (NFixed p) : s)
castFixedToNFixed

----------------------------------------------------------------------------------------------------
-- NRationals
----------------------------------------------------------------------------------------------------
-- | Converts 'NRational' to 'Fixed'.
convertNRationalToFixed :: forall a s. HasResolution a => NRational : s :-> Fixed a : s
convertNRationalToFixed :: forall {k} (a :: k) (s :: [*]).
HasResolution a =>
(NRational : s) :-> (Fixed a : s)
convertNRationalToFixed = (NRational : s) :-> (Rational : s)
forall (s :: [*]). (NRational : s) :-> (Rational : s)
convertNRationalToRational ((NRational : s) :-> (Rational : s))
-> ((Rational : s) :-> (Fixed a : s))
-> (NRational : s) :-> (Fixed a : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (Rational : s) :-> (Fixed a : s)
forall {k} (a :: k) (s :: [*]).
HasResolution a =>
(Rational : s) :-> (Fixed a : s)
convertRationalToFixed

-- | Converts 'NRational' to 'NFixed'.
convertNRationalToNFixed :: forall a s. HasResolution a => NRational : s :-> NFixed a : s
convertNRationalToNFixed :: forall {k} (a :: k) (s :: [*]).
HasResolution a =>
(NRational : s) :-> (NFixed a : s)
convertNRationalToNFixed = do
  (NRational : s) :-> (Natural : Natural : s)
forall r a (s :: [*]).
(LorentzRational r, Unwrappabled r ~ (a, Natural)) =>
(r : s) :-> (a : Natural : s)
deconstructRational
  Natural
-> (Natural : Natural : s) :-> (Natural : Natural : Natural : s)
forall t (s :: [*]). NiceConstant t => t -> s :-> (t : s)
push (forall (a :: k). HasResolution a => Natural
forall {k} (a :: k). HasResolution a => Natural
resolution_ @a)
  (Natural : Natural : Natural : s) :-> (Natural : Natural : s)
forall n m r (s :: [*]).
ArithOpHs Mul n m r =>
(n : m : s) :-> (r : s)
mul
  (Natural : Natural : s) :-> (Maybe (Natural, Natural) : s)
forall n m r (s :: [*]).
ArithOpHs EDiv n m r =>
(n : m : s) :-> (r : s)
ediv
  Impossible "Division by zero impossible"
-> (Maybe (Natural, Natural) : s) :-> ((Natural, Natural) : s)
forall err a (s :: [*]).
IsError err =>
err -> (Maybe a : s) :-> (a : s)
assertSome (forall (reason :: Symbol). HasCallStack => Impossible reason
Impossible @"Division by zero impossible")
  ((Natural, Natural) : s) :-> (Natural : Natural : s)
forall a b (s :: [*]). ((a, b) : s) :-> (a : b : s)
unpair
  (Natural : Natural : s) :-> (Natural : s)
forall n m r (s :: [*]).
ArithOpHs Add n m r =>
(n : m : s) :-> (r : s)
add
  (Natural : s) :-> (NFixed a : s)
forall a (s :: [*]).
Unwrappable a =>
(Unwrappabled a : s) :-> (a : s)
unsafeCoerceWrap

-- | Converts 'NFixed' to 'NRational'.
convertNFixedToNRational :: forall a s. HasResolution a => NFixed a : s :-> NRational : s
convertNFixedToNRational :: forall {k} (a :: k) (s :: [*]).
HasResolution a =>
(NFixed a : s) :-> (NRational : s)
convertNFixedToNRational = do
  (NFixed a : s) :-> (Natural : s)
forall a (s :: [*]).
Unwrappable a =>
(a : s) :-> (Unwrappabled a : s)
coerceUnwrap
  Natural -> (Natural : s) :-> (Natural : Natural : s)
forall t (s :: [*]). NiceConstant t => t -> s :-> (t : s)
push (forall (a :: k). HasResolution a => Natural
forall {k} (a :: k). HasResolution a => Natural
resolution_ @a)
  (Natural : Natural : s) :-> (Natural : Natural : s)
forall a b (s :: [*]). (a : b : s) :-> (b : a : s)
swap
  (Natural : Natural : s) :-> (NRational : s)
forall r a (s :: [*]).
(LorentzRational r, Unwrappabled r ~ (a, Natural)) =>
(a : Natural : s) :-> (r : s)
constructRational

-- | Converts 'Fixed' to 'NRational' if it is greater than zero. If not, returns 'Data.Maybe.Nothing'
convertFixedToNRational :: forall a s. HasResolution a => Fixed a : s :-> Maybe (NRational) : s
convertFixedToNRational :: forall {k} (a :: k) (s :: [*]).
HasResolution a =>
(Fixed a : s) :-> (Maybe NRational : s)
convertFixedToNRational = (Fixed a : s) :-> (Rational : s)
forall {k} (a :: k) (s :: [*]).
HasResolution a =>
(Fixed a : s) :-> (Rational : s)
convertFixedToRational ((Fixed a : s) :-> (Rational : s))
-> ((Rational : s) :-> (Maybe NRational : s))
-> (Fixed a : s) :-> (Maybe NRational : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (Rational : s) :-> (Maybe NRational : s)
forall (s :: [*]). (Rational : s) :-> (Maybe NRational : s)
convertRationalToNRational

-- | Converts 'Fixed' to 'NRational', using 'abs' on numerator.
unsafeConvertFixedToNRational :: forall a s. HasResolution a => Fixed a : s :-> NRational : s
unsafeConvertFixedToNRational :: forall {k} (a :: k) (s :: [*]).
HasResolution a =>
(Fixed a : s) :-> (NRational : s)
unsafeConvertFixedToNRational = (Fixed a : s) :-> (Rational : s)
forall {k} (a :: k) (s :: [*]).
HasResolution a =>
(Fixed a : s) :-> (Rational : s)
convertFixedToRational ((Fixed a : s) :-> (Rational : s))
-> ((Rational : s) :-> (NRational : s))
-> (Fixed a : s) :-> (NRational : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (Rational : s) :-> (NRational : s)
forall (s :: [*]). (Rational : s) :-> (NRational : s)
unsafeConvertRationalToNRational