{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DefaultSignatures #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}

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

-- |

--

-- Module      :  Data.Units.Base.Convert

-- Description :  Conversion between units

-- Copyright   :  (c) Alice Rixte 2025

-- License     :  BSD 3

-- Maintainer  :  alice.rixte@u-bordeaux.fr

-- Stability   :  unstable

-- Portability :  non-portable (GHC extensions)

--

-- Conversion between units. Use @'from'@, @'to'@, or  @'fromTo'@ to convert

-- between two units of the same dimension.

--

-- = Implementing conversions for custom units

--

-- Depending on how the custom unit is converted to its standard unit, there are

-- three ways to implement its conversion summarized in the following table and

-- described with further details afterwards:

--

--  +-----------------------+---------------------------+----------------------+

--  |                       | Which instances           | Note                 |

--  |                       | to declare                |                      |

--  +=======================+===========================+======================+

--  | Conversion factor     | @'ConversionFactor'@ and  |                      |

--  |                       | @'ConvertibleUnit'@ using |                      |

--  |                       | the default               | @'fromTo' == @       |

--  |                       | implementations           | @'fromTo''@          |

--  |                       | for 'fromBaseUnit' and    |                      |

--  |                       | 'toBaseUnit'              |                      |

--  +-----------------------+---------------------------+----------------------+

--  | Affine conversion     | @'ConversionFactor'@ and  |                      |

--  |                       | @'ConvertibleUnit'@       |                      |

--  |                       |                           | @'fromTo' /= @       |

--  |                       |                           | @'fromTo''@          |

--  +-----------------------+---------------------------+----------------------+

--  | Non linear conversion |                           | @'from''@, @'to''@   |

--  |                       | @'ConvertibleUnit'@       | and @'fromTo''@      |

--  |                       |                           | cannot be used       |

--  +-----------------------+---------------------------+----------------------+

--

--

-- === Multiplication by a conversion factor

--

-- For units that can be converted to and from their corresponding standard

-- units by multiplication of a converion factor, you only need to declare an

-- instance of @'ConversionFactor'@, like

--

-- @

-- instance Fractional a => ConversionFactor Hour a where

--   factor = 3600

--

-- instance Fractional a => ConvertibleUnit Hour a

--    -- uses default implementations for 'fromBaseUnit' and 'toBaseUnit'

-- @

--

-- >>> fromTo @Hour @Second 1

-- Second 3600.0

-- >>> fromTo' @Hour @Second 1

-- Second 3600.0

--

-- === Affine conversion (with an offset)

--

-- Some units cannot be conversed by a simple multiplication. For instance, the

-- conversion between Celsius degrees and Kelvin degrees involves addition

-- @x °C = x + 273.15 K@.

--

-- However, when considered as /differences/ of temperatures, Celsius degrees

-- are converted to Kelvin degrees by a multiplication of @1@.

--

-- This can be expressed by the following instances:

--

-- @

-- instance Num a => ConversionFactor Celsius a where

--   factor = 1

--

-- instance Fractional a => ConvertibleUnit Celsius a where

--   toBaseUnit (Celsius x) = Kelvin (x - 273.15)

--   fromBaseUnit (Kelvin x) = Celsius (x + 273.15)

-- @

--

-- >>> fromTo @Celsius @Kelvin 0

-- Kelvin 273.15

-- >>> fromTo' @Celsius @Kelvin 0

-- Kelvin 0.0

--

-- === Other conversions

--

-- Any other conversion can be implemented, like for instance logarithmic units.

-- In this case, you should only give an instance for @'ConvertibleUnit'@, and

-- no instance for @'ConversionFactor'@. See for instance linear picth

-- @'Data.Unit.NonStd.Frequency.Tet'@.

--

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


module Data.Units.Base.Convert
  ( DimEq
  -- * Generic conversion between units

  , ConvertibleUnit (..)
  , FromTo
  , fromTo
  , from
  , to
  , ($~)
  , (~&)
  -- * Conversion using conversion factors

  , ConversionFactor (..)
  , toBaseUnit'
  , fromBaseUnit'
  , FromTo'
  , fromTo'
  , from'
  , to'
  )
  where

import Data.Proxy
import Data.Kind
import Data.Type.Bool
import Data.Type.Equality
import GHC.TypeError

import Data.Type.Int

import Data.Units.Base.System

-- | A constraint to test whether two units have

type family DimEq (u :: Unit) (v :: Unit) :: Constraint where
  DimEq u v = DimEqStd u v (DimOf u) (DimOf v)

type family DimEqStd (u :: Unit) (v :: Unit) (du :: Dim) (dv :: Dim)
  :: Constraint where
  DimEqStd u v du dv =
    ( IsUnit u
    , IsUnit v
    , du ~ dv
    , If (du == dv) (() :: Constraint)
      (TypeError (
            Text "Cannot convert unit ‘"
            :<>: ShowUnitType u
            :<>: Text "’ to unit ‘"
            :<>: ShowUnitType v
            :<>: Text "’ because their dimensions do not match."
            :$$: Text "Dimension of ‘"
            :<>: ShowUnitType u
            :<>: Text "’ is: "
            :<>: ShowDimType du
            :$$: Text "Dimension of ‘"
            :<>: ShowUnitType v
            :<>: Text "’ is: "
            :<>: ShowDimType dv
    )))



-- | A unit whose quantities are convertible from that unit to its corresponding

-- base unit.

--

-- Instances must satisfy the following law :

--

-- * @'toBaseUnit' . 'fromBaseUnit' == 'id'@

--

class (IsUnit u, IsUnit (BaseUnitOf u)) => ConvertibleUnit u a where
  -- | Convert a quantity to its base unit.

  --

  -- >>> import Data.Units.NonStd.Time

  -- >>> toBaseUnit @Hour 1

  -- Second 3600.0

  -- >>> toBaseUnit (Hour 1)

  -- Second 3600.0

  -- >>> toBaseUnit @(Kilo Meter ./. Hour) 36

  -- quantity @(Meter .*. Second .^- 1) 10.0

  -- >>> toBaseUnit (Celsius 0)

  -- Kelvin 273.15

  toBaseUnit :: u a -> BaseUnitOf u a
  default toBaseUnit :: ConversionFactor u a => u a -> BaseUnitOf u a
  toBaseUnit = u a -> BaseUnitOf u a
forall (u :: Unit) a. ConversionFactor u a => u a -> BaseUnitOf u a
toBaseUnit'
  {-# INLINE toBaseUnit #-}

  -- | Convert a quantity from its base unit to another unit.

  --

  -- >>> fromBaseUnit @Hour 1800

  -- Hour 0.5

  -- >>> fromBaseUnit 1800 :: Hour Double

  -- Hour 0.5

  -- >>> fromBaseUnit @(Kilo Meter ./. Hour) 10

  -- quantity @(Kilo Meter .*. Hour .^- 1) 36.0

  -- >>> fromBaseUnit @Celsius 0

  -- Celsius (-273.15)

  --

  fromBaseUnit :: BaseUnitOf u a -> u a
  default fromBaseUnit :: ConversionFactor u a => BaseUnitOf u a -> u a
  fromBaseUnit = BaseUnitOf u a -> u a
forall (u :: Unit) a. ConversionFactor u a => BaseUnitOf u a -> u a
fromBaseUnit'
  {-# INLINE fromBaseUnit #-}



-- | A constraint that is satisfied when both units have the same dimension and

-- are such that @u@ can be converted to @v@.

--

type FromTo u v a = (DimEq u v, ConvertibleUnit u a, ConvertibleUnit v a)

-- | Conversion between two quantities with the same dimension.

--

--  >>> fromTo @Celsius @Kelvin 0

--  Kelvin 273.15

-- >>> fromTo @(Milli Second) @Hour 1

-- Hour 2.7777777777777776e-7

-- >>> fromTo (Milli (Second 1)) :: Hour Double

-- Hour 2.7777777777777776e-7

-- >>> fromTo @Turn @Degree (1/4) -- angle conversion

-- Degree 90.0

-- >>> fromTo @(Kilo Meter ./. Hour) @(Milli Meter ./. Milli Second) 36

-- quantity @(Milli Meter .*. Milli Second .^- 1) 10.0

--

fromTo :: FromTo u v a => u a -> v a
fromTo :: forall (u :: Unit) (v :: Unit) a. FromTo u v a => u a -> v a
fromTo = BaseUnitOf v a -> v a
forall (u :: Unit) a. ConvertibleUnit u a => BaseUnitOf u a -> u a
fromBaseUnit (BaseUnitOf v a -> v a) -> (u a -> BaseUnitOf v a) -> u a -> v a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. u a -> BaseUnitOf u a
u a -> BaseUnitOf v a
forall (u :: Unit) a. ConvertibleUnit u a => u a -> BaseUnitOf u a
toBaseUnit
{-# INLINE fromTo #-}

-- | A mere synonym of @'fromTo'@ where it is more intuitive to use only one

-- type application.

--

-- >>> from @Celsius 0 :: Kelvin Double

-- Kelvin 273.15

--

from :: FromTo u v a => u a -> v a
from :: forall (u :: Unit) (v :: Unit) a. FromTo u v a => u a -> v a
from = u a -> v a
forall (u :: Unit) (v :: Unit) a. FromTo u v a => u a -> v a
fromTo
{-# INLINE from #-}

-- | Same as @'fromTo'@ but the type applications are reversed

--

-- >>> to @Kelvin (Celsius 0)

-- Kelvin 273.15

--

to :: forall v u a. FromTo u v a => u a -> v a
to :: forall (v :: Unit) (u :: Unit) a. FromTo u v a => u a -> v a
to = u a -> v a
forall (u :: Unit) (v :: Unit) a. FromTo u v a => u a -> v a
fromTo
{-# INLINE to #-}

-- | A convenient operator for converting a unit before feeding it to a

-- function.

--

-- >>> import Linear

-- >>> rotation (Radian th) = V2 (V2 (cos th) (- sin th)) (V2 (sin th)  (cos th))

-- >>> rotation $~ Degree 90

-- V2 (V2 6.123031769111886e-17 (-1.0)) (V2 1.0 6.123031769111886e-17)

--

($~) :: FromTo u v a => (v a -> b) -> u a -> b
v a -> b
f $~ :: forall (u :: Unit) (v :: Unit) a b.
FromTo u v a =>
(v a -> b) -> u a -> b
$~ u a
x = v a -> b
f (u a -> v a
forall (u :: Unit) (v :: Unit) a. FromTo u v a => u a -> v a
fromTo u a
x)
{-# INLINE ($~) #-}

infixr 0 $~

-- | Same as @'($~)'@ but with arguments flipped.

--

(~&) :: FromTo u v a => u a -> (v a -> b) -> b
~& :: forall (u :: Unit) (v :: Unit) a b.
FromTo u v a =>
u a -> (v a -> b) -> b
(~&) = ((v a -> b) -> u a -> b) -> u a -> (v a -> b) -> b
forall a b c. (a -> b -> c) -> b -> a -> c
flip (v a -> b) -> u a -> b
forall (u :: Unit) (v :: Unit) a b.
FromTo u v a =>
(v a -> b) -> u a -> b
($~)
{-# INLINE (~&) #-}

infixl 1 ~&

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


-- | Unit that can be converted to their corresponding standard unit by

-- multiplication with a conversion factor.

--

-- Instances must satisfy the following laws:

--

-- * @'toBaseUnit' @u ==  'quantity' ('unQuantity' q * 'factor' @u)@

-- * @'fromBaseUnit' @u  == 'quantity' (''unQuantity' q / 'factor' @u)@

--

class (ConvertibleUnit u a, Fractional a) => ConversionFactor u a where
  {-# MINIMAL factor #-}

  -- | Multiplying a quantity of type @u a@ with @'factor'@ will convert it

  -- to its corresponding base unit @BaseUnitOf u a@

  --

  -- >>> factor @Hour :: Double

  -- 3600.0

  -- >>> factor @Celsius :: Double

  -- 1.0

  -- >>> factor @(Kilo Meter ./. Hour) :: Double

  -- 0.2777777777777778

  factor :: a

instance Fractional a => ConvertibleUnit NoUnit a

instance Fractional a => ConversionFactor NoUnit a where
  factor :: a
factor = a
1
  {-# INLINE factor #-}

instance (Num a, ConversionFactor u a, ConversionFactor v a, IsUnit (BaseUnitOf (u .*. v)))
  => ConvertibleUnit (u .*. v) a

instance (Num a, ConversionFactor u a, ConversionFactor v a, IsUnit (BaseUnitOf (u .*. v)))
  =>  ConversionFactor (u .*. v) a where
  factor :: a
factor = forall (u :: Unit) a. ConversionFactor u a => a
factor @u a -> a -> a
forall a. Num a => a -> a -> a
* forall (u :: Unit) a. ConversionFactor u a => a
factor @v
  {-# INLINE factor #-}

instance (ConversionFactor u a, IsUnit (BaseUnitOf (u .^. n)),  KnownInt n)
  => ConvertibleUnit (u .^. n) a

instance (ConversionFactor u a, IsUnit (BaseUnitOf (u .^. n)),  KnownInt n)
  =>  ConversionFactor (u .^. n) a where
  factor :: a
factor = forall (u :: Unit) a. ConversionFactor u a => a
factor @u a -> Integer -> a
forall a b. (Fractional a, Integral b) => a -> b -> a
^^ Proxy n -> Integer
forall (r :: ZZ) (proxy :: ZZ -> *).
KnownInt r =>
proxy r -> Integer
forall (proxy :: ZZ -> *). proxy n -> Integer
intVal (Proxy n
forall {k} (t :: k). Proxy t
Proxy :: Proxy n)
  {-# INLINE factor #-}

-- | Convert a quantity to its corresponding base unit by multiplying it

-- by  @'factor'@.

--

-- >>> toBaseUnit' @Hour 1

-- Second 3600.0

-- >>> toBaseUnit' (Hour 1)

-- Second 3600.0

-- >>> toBaseUnit' @(Kilo Meter ./. Hour) 36

-- quantity @(Meter .*. Second .^- 1) 10.0

-- >>> toBaseUnit' (Celsius 0)

-- Kelvin 0.0

--

toBaseUnit' :: forall u a. ConversionFactor u a
  => u a -> BaseUnitOf u a
toBaseUnit' :: forall (u :: Unit) a. ConversionFactor u a => u a -> BaseUnitOf u a
toBaseUnit' u a
q = a -> DimToUnit (DimOf u) a
forall (u :: Unit) a. IsUnit u => a -> u a
quantity (u a -> a
forall (u :: Unit) a. IsUnit u => u a -> a
unQuantity u a
q a -> a -> a
forall a. Num a => a -> a -> a
* forall (u :: Unit) a. ConversionFactor u a => a
factor @u)
{-# INLINE toBaseUnit' #-}

-- | Convert a standard quantity to a unit @u@ by dividing it by

-- by  @'factor'@.

--

-- >>> fromBaseUnit' @Hour 1800

-- Hour 0.5

-- >>> fromBaseUnit' 1800 :: Hour Double

-- Hour 0.5

-- >>> fromBaseUnit' @(Kilo Meter ./. Hour) 10

-- quantity @(Kilo Meter .*. Hour .^- 1) 36.0

-- >>> fromBaseUnit' @Celsius 0

-- Celsius 0.0

--

fromBaseUnit' :: forall u a. ConversionFactor u a
  => BaseUnitOf u a -> u a
fromBaseUnit' :: forall (u :: Unit) a. ConversionFactor u a => BaseUnitOf u a -> u a
fromBaseUnit' BaseUnitOf u a
q = a -> u a
forall (u :: Unit) a. IsUnit u => a -> u a
quantity (BaseUnitOf u a -> a
forall (u :: Unit) a. IsUnit u => u a -> a
unQuantity BaseUnitOf u a
q a -> a -> a
forall a. Fractional a => a -> a -> a
/ forall (u :: Unit) a. ConversionFactor u a => a
factor @u)
{-# INLINE fromBaseUnit' #-}

-- | A constraint that is satisfied when both units have the same dimension and

-- are such that @u@ can be converted to @v@ by using a conversion factor.

--

type FromTo' u v a = (DimEq u v, ConversionFactor u a, ConversionFactor v a)

-- | Conversion, using conversion factors, between two quantities with the same

-- dimension

--

-- >>> fromTo' @Celsius @Kelvin 0

-- Kelvin 0.0

-- >>> fromTo' @(Milli Second) @Hour 1

-- Hour 2.7777777777777776e-7

-- >>> fromTo' (Milli (Second 1)) :: Hour Double

-- Hour 2.7777777777777776e-7

-- >>> fromTo' @Turn @Degree (1/4) -- angle conversion

-- Degree 90.0

-- >>> fromTo' @(Kilo Meter ./. Hour) @(Milli Meter ./. Milli Second) 36

-- quantity @(Milli Meter .*. Milli Second .^- 1) 10.0

--

fromTo' :: forall u v a.
  FromTo' u v a
  => u a -> v a
fromTo' :: forall (u :: Unit) (v :: Unit) a. FromTo' u v a => u a -> v a
fromTo' u a
q = a -> v a
forall (u :: Unit) a. IsUnit u => a -> u a
quantity (u a -> a
forall (u :: Unit) a. IsUnit u => u a -> a
unQuantity u a
q a -> a -> a
forall a. Num a => a -> a -> a
* (forall (u :: Unit) a. ConversionFactor u a => a
factor @u a -> a -> a
forall a. Fractional a => a -> a -> a
/ forall (u :: Unit) a. ConversionFactor u a => a
factor @v))
{-# INLINE fromTo' #-}



-- | A mere synonym of @'fromTo''@ where it is more intuitive to use only one

-- type application.

--

-- >>> from' @Celsius 0 :: Kelvin Double

-- Kelvin 0.0

--

from' :: FromTo' u v a => u a -> v a
from' :: forall (u :: Unit) (v :: Unit) a. FromTo' u v a => u a -> v a
from' = u a -> v a
forall (u :: Unit) (v :: Unit) a. FromTo' u v a => u a -> v a
fromTo'
{-# INLINE from' #-}

-- | Same as @'fromTo''@ but the type applications are reversed

--

-- >>> to' @Kelvin (Celsius 0)

-- Kelvin 0.0

--

to' :: forall v u a. FromTo' u v a => u a -> v a
to' :: forall (v :: Unit) (u :: Unit) a. FromTo' u v a => u a -> v a
to' = u a -> v a
forall (u :: Unit) (v :: Unit) a. FromTo' u v a => u a -> v a
fromTo'
{-# INLINE to' #-}