convert-units-0.1: test/Data/Units/Core/ArithmeticProp.hs

{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE TypeApplications #-}

module Data.Units.Core.ArithmeticProp where

import Data.Coerce

import Test.QuickCheck
import Test.Hspec

import Data.AEq

import Data.Units

import Data.Units.Core.ConvertProp


------------------------- Num and fractional instances -------------------------

addNumProp :: forall u a.
  ( IsUnit u, Floating (u a)
  , Show a, AEq a, Floating a, Eq a, Arbitrary a) =>  Property
addNumProp = property (\ (a :: a) (b :: a) ->
  a + b + pi ==
    coerce (coerce a + coerce b + pi :: u a)
  )

divNumProp :: forall u a.
 ( IsUnit u, Fractional (u a)
 , Show a, AEq a, Fractional a, Eq a, Arbitrary a)
 => Property
divNumProp = property (\ (a :: a) (b :: a) -> b == 0 ||
  a / b ==
    coerce (coerce a / coerce b :: u a))

floatingSpec :: forall u a.
  ( IsUnit u, Floating (u a), ShowUnit u
  , Show a, AEq a, Floating a, Eq a, Arbitrary a
  )
  =>  Spec
floatingSpec = it ("Floating instance for " ++ showUnit @u ) $
  addNumProp @u @a .&&. divNumProp @u @a


-------------------------- Arithmetic same dimension ---------------------------



addRight :: forall u v a.
  ( FromTo' v u a
  )
  => a -> a -> a
addRight u v = coerce $ (coerce u :: u a) .+~ (coerce v :: v a)

addRightProp :: forall u v a.
  ( FromTo' v u a
  , DimEq u v
  , Show a, AEq a, Arbitrary a
  )
  => Property
addRightProp = property (\(a :: a) (b :: a) ->
    (coerce (fromTo' (coerce a :: u a) :: v a) + b :: a)
    ~==  addRight @u @v a b
  )

addRightSpec :: forall u v a.
  ( FromTo' v u a
  , DimEq u v
  , ShowUnit u, ShowUnit v
  , Show a, AEq a, Arbitrary a
  ) => Spec
addRightSpec = it (showUnit @u ++ " .+~ " ++ showUnit @v)
  $ addRightProp @u @v @a

addLeft :: forall u v a.
  ( FromTo' u v a
  )
  => a -> a -> a
addLeft u v = coerce $ (coerce u :: u a) ~+. (coerce v :: v a)

addLeftProp :: forall u v a.
  ( FromTo' u v a
  , DimEq u v
  , Show a, AEq a, Arbitrary a
  )
  => Property
addLeftProp = property (\(a :: a) (b :: a) ->
    (coerce (fromTo' (coerce a :: u a) :: v a) + b :: a)
    ~== addLeft @u @v a b
  )

addLeftSpec :: forall u v a.
  ( FromTo' u v a
  , DimEq u v
  , ShowUnit u, ShowUnit v
  , Show a, AEq a, Arbitrary a
  ) => Spec
addLeftSpec = it (showUnit @u ++ " ~+. " ++ showUnit @v)
  $ addLeftProp @u @v @a


addSame :: forall u v a.
  FromTo' u v a
  => a -> a -> a
addSame u v = coerce $ (coerce u :: u a) ~+~ (coerce v :: v a)

addSameProp :: forall u v a.
  ( FromTo' u v a
  , DimEq u v
  , Show a, AEq a, Arbitrary a
  )
  => Property
addSameProp = property (\(a :: a) (b :: a) ->
  (coerce (fromTo' (coerce a :: u a) :: v a) + b :: a)
    ~== addSame @u @v a b)

addSameSpec :: forall u v a.
  ( FromTo' u v a
  , DimEq u v
  , ShowUnit u, ShowUnit v
  , Show a, AEq a, Arbitrary a
  ) => Spec
addSameSpec = it (showUnit @u ++ " ~+~ " ++ showUnit @v)
  $ addSameProp @u @v @a

--------------------------------- Subtraction ----------------------------------

subRight :: forall u v a.
  ( FromTo' v u a
  )
  => a -> a -> a
subRight u v = coerce $ (coerce u :: u a) .-~ (coerce v :: v a)

subRightProp :: forall u v a.
  ( FromTo' v u a
  , DimEq u v
  , Show a, AEq a, Arbitrary a
  )
  => Property
subRightProp = property (\(a :: a) (b :: a) ->
  (coerce (fromTo' (coerce a :: u a) :: v a) - b :: a)
  ~== subRight @u @v a b
  )

subRightSpec :: forall u v a.
  ( FromTo' v u a
  , DimEq u v
  , ShowUnit u, ShowUnit v
  , Show a, AEq a, Arbitrary a
  ) => Spec
subRightSpec = it (showUnit @u ++ " .-~ " ++ showUnit @v)
  $ subRightProp @u @v @a

subLeft :: forall u v a.
  ( FromTo' u v a
  )
  => a -> a -> a
subLeft u v = coerce $ (coerce u :: u a) ~-. (coerce v :: v a)

subLeftProp :: forall u v a.
  ( FromTo' u v a
  , DimEq u v
  , Show a, AEq a, Arbitrary a
  )
  => Property
subLeftProp = property (\(a :: a) (b :: a) ->
  (coerce (fromTo' (coerce a :: u a) :: v a) - b :: a)
    ~== subLeft @u @v a b
  )

subLeftSpec :: forall u v a.
  ( FromTo' u v a
  , DimEq u v
  , ShowUnit u, ShowUnit v
  , Show a, AEq a, Arbitrary a
  ) => Spec
subLeftSpec = it (showUnit @u ++ " ~-. " ++ showUnit @v)
  $ subLeftProp @u @v @a


subSame :: forall u v a.
  FromTo' u v a
  => a -> a -> a
subSame u v = coerce $ (coerce u :: u a) ~-~ (coerce v :: v a)

subSameProp :: forall u v a.
  ( FromTo' u v a
  , DimEq u v
  , Show a, AEq a, Arbitrary a
  )
  => Property
subSameProp = property (\(a :: a) (b :: a) ->
  (coerce (fromTo' (coerce a :: u a) :: v a) - b :: a)
  ~== subSame @u @v a b
  )

subSameSpec :: forall u v a.
  ( FromTo' u v a
  , DimEq u v
  , ShowUnit u, ShowUnit v
  , Show a, AEq a, Arbitrary a
  ) => Spec
subSameSpec = it (showUnit @u ++ " ~-~ " ++ showUnit @v)
  $ subSameProp @u @v @a


-------------------------------- Multiplication --------------------------------

mulSame :: forall u v a u2 .
  ( u2 ~ BaseUnitOf u .^+ 2, IsUnit u2
  , DimEq u v
  , ConversionFactor u a, ConversionFactor v a
  )
  => a -> a -> a
mulSame u v = coerce $ (coerce u :: u a) ~*~ (coerce v :: v a)

mulSameProp :: forall u v a u2 .
  ( u2 ~ BaseUnitOf u .^+ 2, IsUnit u2
  , DimEq u v
  , ConversionFactor u a, ConversionFactor v a
  , Show a, AEq a, Arbitrary a
  )
  => Property
mulSameProp = property (\(a :: a) (b :: a) ->
    (coerce (fromTo' (coerce a :: u a) :: v a) * b :: a)
    ~== mulSame @u @v a b
  )

mulSameSpec :: forall u v a u2 .
  ( u2 ~ BaseUnitOf u .^+ 2, IsUnit u2
  , DimEq u v
  , ConversionFactor u a, ConversionFactor v a
  , ShowUnit u, ShowUnit v
  , Show a, AEq a, Arbitrary a
  )
  => Spec
mulSameSpec = it (showUnit @u ++ " ~*~ " ++ showUnit @v)
  $ mulSameProp @u @v @a

divSame :: forall u v a u2 .
  ( u2 ~ BaseUnitOf u .^+ 2, IsUnit u2
  , DimEq u v
  , ConversionFactor u a, ConversionFactor v a
  )
  => a -> a -> a
divSame u v = coerce $ (coerce u :: u a) ~/~ (coerce v :: v a)

divSameProp :: forall u v a u2 .
  ( u2 ~ BaseUnitOf u .^+ 2, IsUnit u2
  , DimEq u v
  , ConversionFactor u a, ConversionFactor v a
  , Show a, AEq a, Eq a, Arbitrary a
  )
  => Property
divSameProp = property (\(a :: a) (b :: a) -> b == 0 ||
    (coerce (fromTo' (coerce a :: u a) :: v a) / b :: a)
    ~== divSame @u @v a b
  )

divSameSpec :: forall u v a u2 .
  ( u2 ~ BaseUnitOf u .^+ 2, IsUnit u2
  , DimEq u v
  , ConversionFactor u a, ConversionFactor v a
  , ShowUnit u, ShowUnit v
  , Show a, AEq a, Eq a, Arbitrary a
  )
  => Spec
divSameSpec = it (showUnit @u ++ " ~/~ " ++ showUnit @v)
  $ divSameProp @u @v @a

------------------ Arithmetic with two different dimensions  -------------------

-- mulRight :: forall u v a u2.
--   ( u2 ~ BaseUnitOf' (u .^+ 2) , IsUnit u2
--   , DimEq u v
--   , FromTo' v u a
--   )
--   => a -> a -> a
-- mulRight u v = coerce $ (coerce u :: u a) .*~ (coerce v :: v a)

-- mulRightProp :: forall u v a u2.
--   ( u2 ~ BaseUnitOf' (u .^+ 2) , IsUnit u2
--   , DimEq u v
--   , FromTo' v u a
--   , Show a, AEq a, Arbitrary a
--   )
--   => Property
-- mulRightProp = property (\(a :: a) (b :: a) ->
--    (coerce (fromTo' (coerce a :: u a) :: v a) * b :: a)
--    ~== mulRight @u @v a b
--  )

-- mulRightSpec :: forall u v a u2.
--   ( u2 ~ BaseUnitOf' (u .^+ 2) , IsUnit u2
--   , DimEq u v
--   , FromTo' v u a
--   , ShowUnit u, ShowUnit v
--   , Show a, AEq a, Arbitrary a
--   ) => Spec
-- mulRightSpec = it (showUnit @u ++ " .*~ " ++ showUnit @v)
--   $ mulRightProp @u @v @a

-- mulLeft :: forall u v a v2.
--   ( v2 ~ BaseUnitOf' (v .^+ 2), IsUnit v2
--   , DimEq v u
--   , FromTo' u v a
--   )
--   => a -> a -> a
-- mulLeft u v = coerce $ (coerce u :: u a) ~*. (coerce v :: v a)

-- mulLeftProp :: forall u v a v2.
--   ( v2 ~ BaseUnitOf' (v .^+ 2), IsUnit v2
--   , DimEq v u
--   , FromTo' u v a
--   , Show a, AEq a, Arbitrary a
--   )
--   => Property
-- mulLeftProp = property (\(a :: a) (b :: a) ->
--      (coerce (fromTo' (coerce a :: u a) :: v a) * b :: a)
--      ~== mulLeft @u @v a b
--   )

-- mulLeftSpec :: forall u v a v2.
--   ( v2 ~ BaseUnitOf' (v .^+ 2), IsUnit v2
--   , DimEq v u
--   , FromTo' u v a
--   , ShowUnit u, ShowUnit v
--   , Show a, AEq a, Arbitrary a
--   ) => Spec
-- mulLeftSpec = it (showUnit @u ++ " ~*. " ++ showUnit @v)
--   $ mulLeftProp @u @v @a


mulDiffDim :: forall u v a.
  ( ConversionFactor u a, ConversionFactor v a)
  => a -> a -> a
mulDiffDim u v = coerce $ (coerce u :: u a) .*. (coerce v :: v a)

mulDiffDimProp :: forall u v a.
  ( ConversionFactor u a, ConversionFactor v a
  , ConversionFactor (u .*. v) a
  , Arbitrary a, Show a, AEq a
  )
  => Property
mulDiffDimProp =
  property (\a b -> a * b ~== mulDiffDim @u @v @a a b)
  .&&. toFromProp @(u .*. v) @a

mulDiffDimSpec :: forall u v a.
  ( ConversionFactor u a, ConversionFactor v a
  , ConversionFactor (u .*. v) a
  , Arbitrary a, Show a, AEq a
  , ShowUnit u, ShowUnit v
  )
  => Spec
mulDiffDimSpec = it (showUnit @u ++ " .*. " ++ showUnit @v)
    $ mulDiffDimProp @u @v @a

divDiffDim :: forall u v a.
  ( IsUnit u, IsUnit v, IsUnit (u ./. v)
  , Fractional a
  )
  => a -> a -> a
divDiffDim u v = coerce $ (coerce u :: u a) ./. (coerce v :: v a)

divDiffDimProp :: forall u v a.
  ( IsUnit u, IsUnit v, IsUnit (u ./. v)
  , ConversionFactor (u ./. v) a
  , IsUnit (u ./. v)
  , Arbitrary a, Show a, AEq a, Eq a, Fractional a
  )
  => Property
divDiffDimProp =
  property (\a b -> b == 0 || a / b ~== divDiffDim @u @v @a a b)
  .&&. toFromProp @(u ./. v) @a

divDiffDimSpec :: forall u v a.
  (IsUnit u, IsUnit v, IsUnit (u ./. v)
  , ConversionFactor (u ./. v) a
  , IsUnit (u ./. v)
  , Arbitrary a, Show a, AEq a, Eq a, Fractional a
  , ShowUnit u, ShowUnit v
  )
  => Spec
divDiffDimSpec =  it (showUnit @u ++ " ./. " ++ showUnit @v)
  $ divDiffDimProp @u @v @a

-------------------------------- Exponentiation --------------------------------

exp2 :: forall u a.
  ConversionFactor u a
  => a -> a
exp2 u = coerce $ (coerce u :: u a) .^. pos2

expm1 :: forall u a.
  ConversionFactor u a
  => a -> a
expm1 u = coerce $ (coerce u :: u a) .^. neg1

exp2Prop :: forall u a.
  ( ConversionFactor u a
  , Arbitrary a, Show a, AEq a
  )
  => Property
exp2Prop =
  property (\a -> a * a ~== exp2 @u @a a)

expm1Prop :: forall u a.
  ( ConversionFactor u a
  , Arbitrary a, Show a,  Eq a, AEq a
  )
  => Property
expm1Prop =
  property (\a -> a == 0 || 1 / a ~== expm1 @u @a a)

expSpec :: forall u a.
  ( ConversionFactor u a
  , ShowUnit u
  , Arbitrary a, Show a,  Eq a, AEq a
  )
  => Spec
expSpec = it (showUnit @u ++ " .^+ 2  ," ++ showUnit @u ++ " .^- 1") $
  exp2Prop @u @a .&&. expm1Prop @u @a

exp2Conv :: forall u a.
  ConversionFactor u a
  => a -> a
exp2Conv u = coerce $ (coerce u :: u a) ~^~ pos2

expm1Conv :: forall u a.
  ConversionFactor u a
  => a -> a
expm1Conv u = coerce $ (coerce u :: u a) ~^~ neg1

exp2ConvProp :: forall u a.
  ( ConversionFactor u a
  , Arbitrary a, Show a, AEq a
  )
  => Property
exp2ConvProp =
  property (\a ->
    coerce (toBaseUnit' (coerce a :: u a)) ^^ (2 :: Int) ~== exp2Conv @u @a a)

expm1ConvProp :: forall u a.
  ( ConversionFactor u a
  , Arbitrary a, Show a, Eq a, AEq a
  )
  => Property
expm1ConvProp =
  property (\a -> a == 0 ||
    coerce (toBaseUnit' (coerce a :: u a)) ^^ (-1 :: Int) ~== expm1Conv @u @a a)


expConvSpec :: forall u a.
  ( ConversionFactor u a
  , ShowUnit u
  , Arbitrary a, Show a,  Eq a, AEq a
  )
  => Spec
expConvSpec = it (showUnit @u ++ "~^~ pos2  ," ++ showUnit @u ++ "~^~ neg1") $
  exp2ConvProp @u @a .&&. expm1ConvProp @u @a