{-# LANGUAGE RebindableSyntax #-}
module Algebra.Units (
    {- * Class -}
    C,
    isUnit,
    stdAssociate,
    stdUnit,
    stdUnitInv,

    {- * Standard implementations for instances -}
    intQuery,
    intAssociate,
    intStandard,
    intStandardInverse,

    {- * Properties -}
    propComposition,
    propInverseUnit,
    propUniqueAssociate,
    propAssociateProduct,
  ) where

import qualified Algebra.IntegralDomain as Integral
import qualified Algebra.Ring           as Ring
import qualified Algebra.ZeroTestable   as ZeroTestable

import qualified Algebra.Laws           as Laws

import Algebra.IntegralDomain (div)
import Algebra.Ring           (one, (*))
import Algebra.Additive       (negate)
import Algebra.ZeroTestable   (isZero)

import Data.Int  (Int,  Int8,  Int16,  Int32,  Int64,  )

import NumericPrelude.Base
import Prelude (Integer, )
import qualified Prelude as P
import Test.QuickCheck ((==>), Property)


{- |
This class lets us deal with the units in a ring.
'isUnit' tells whether an element is a unit.
The other operations let us canonically
write an element as a unit times another element.
Two elements a, b of a ring R are _associates_ if a=b*u for a unit u.
For an element a, we want to write it as a=b*u where b is an associate of a.
The map (a->b) is called
"StandardAssociate" by Gap,
"unitCanonical" by Axiom,
and "canAssoc" by DoCon.
The map (a->u) is called
"canInv" by DoCon and
"unitNormal(x).unit" by Axiom.

The laws are

>   stdAssociate x * stdUnit x === x
>     stdUnit x * stdUnitInv x === 1
>  isUnit u ==> stdAssociate x === stdAssociate (x*u)

Currently some algorithms assume

>  stdAssociate(x*y) === stdAssociate x * stdAssociate y

Minimal definition:
   'isUnit' and ('stdUnit' or 'stdUnitInv') and optionally 'stdAssociate'
-}

class (Integral.C a) => C a where
  {-# MINIMAL isUnit, (stdUnit | stdUnitInv) #-}
  isUnit :: a -> Bool
  stdAssociate, stdUnit, stdUnitInv :: a -> a

  stdAssociate a
x = a
x a -> a -> a
forall a. C a => a -> a -> a
* a -> a
forall a. C a => a -> a
stdUnitInv a
x
  stdUnit      a
x = a -> a -> a
forall a. C a => a -> a -> a
div a
forall a. C a => a
one (a -> a
forall a. C a => a -> a
stdUnitInv a
x)  -- should be divChecked
  stdUnitInv   a
x = a -> a -> a
forall a. C a => a -> a -> a
div a
forall a. C a => a
one (a -> a
forall a. C a => a -> a
stdUnit a
x)




{- * Instances for atomic types -}

intQuery :: (P.Integral a, Ring.C a) => a -> Bool
intQuery :: a -> Bool
intQuery = (a -> [a] -> Bool) -> [a] -> a -> Bool
forall a b c. (a -> b -> c) -> b -> a -> c
flip a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem [a
forall a. C a => a
one, a -> a
forall a. C a => a -> a
negate a
forall a. C a => a
one]
{- constraint must be replaced by NumericPrelude.Absolute -}
intAssociate, intStandard, intStandardInverse ::
   (P.Integral a, Ring.C a, ZeroTestable.C a) => a -> a
intAssociate :: a -> a
intAssociate = a -> a
forall a. Num a => a -> a
P.abs
intStandard :: a -> a
intStandard a
x = if a -> Bool
forall a. C a => a -> Bool
isZero a
x then a
forall a. C a => a
one else a -> a
forall a. Num a => a -> a
P.signum a
x
intStandardInverse :: a -> a
intStandardInverse = a -> a
forall a. (Integral a, C a, C a) => a -> a
intStandard

instance C Int where
  isUnit :: Int -> Bool
isUnit       = Int -> Bool
forall a. (Integral a, C a) => a -> Bool
intQuery
  stdAssociate :: Int -> Int
stdAssociate = Int -> Int
forall a. (Integral a, C a, C a) => a -> a
intAssociate
  stdUnit :: Int -> Int
stdUnit      = Int -> Int
forall a. (Integral a, C a, C a) => a -> a
intStandard
  stdUnitInv :: Int -> Int
stdUnitInv   = Int -> Int
forall a. (Integral a, C a, C a) => a -> a
intStandardInverse

instance C Integer where
  isUnit :: Integer -> Bool
isUnit       = Integer -> Bool
forall a. (Integral a, C a) => a -> Bool
intQuery
  stdAssociate :: Integer -> Integer
stdAssociate = Integer -> Integer
forall a. (Integral a, C a, C a) => a -> a
intAssociate
  stdUnit :: Integer -> Integer
stdUnit      = Integer -> Integer
forall a. (Integral a, C a, C a) => a -> a
intStandard
  stdUnitInv :: Integer -> Integer
stdUnitInv   = Integer -> Integer
forall a. (Integral a, C a, C a) => a -> a
intStandardInverse

instance C Int8 where
  isUnit :: Int8 -> Bool
isUnit       = Int8 -> Bool
forall a. (Integral a, C a) => a -> Bool
intQuery
  stdAssociate :: Int8 -> Int8
stdAssociate = Int8 -> Int8
forall a. (Integral a, C a, C a) => a -> a
intAssociate
  stdUnit :: Int8 -> Int8
stdUnit      = Int8 -> Int8
forall a. (Integral a, C a, C a) => a -> a
intStandard
  stdUnitInv :: Int8 -> Int8
stdUnitInv   = Int8 -> Int8
forall a. (Integral a, C a, C a) => a -> a
intStandardInverse

instance C Int16 where
  isUnit :: Int16 -> Bool
isUnit       = Int16 -> Bool
forall a. (Integral a, C a) => a -> Bool
intQuery
  stdAssociate :: Int16 -> Int16
stdAssociate = Int16 -> Int16
forall a. (Integral a, C a, C a) => a -> a
intAssociate
  stdUnit :: Int16 -> Int16
stdUnit      = Int16 -> Int16
forall a. (Integral a, C a, C a) => a -> a
intStandard
  stdUnitInv :: Int16 -> Int16
stdUnitInv   = Int16 -> Int16
forall a. (Integral a, C a, C a) => a -> a
intStandardInverse

instance C Int32 where
  isUnit :: Int32 -> Bool
isUnit       = Int32 -> Bool
forall a. (Integral a, C a) => a -> Bool
intQuery
  stdAssociate :: Int32 -> Int32
stdAssociate = Int32 -> Int32
forall a. (Integral a, C a, C a) => a -> a
intAssociate
  stdUnit :: Int32 -> Int32
stdUnit      = Int32 -> Int32
forall a. (Integral a, C a, C a) => a -> a
intStandard
  stdUnitInv :: Int32 -> Int32
stdUnitInv   = Int32 -> Int32
forall a. (Integral a, C a, C a) => a -> a
intStandardInverse

instance C Int64 where
  isUnit :: Int64 -> Bool
isUnit       = Int64 -> Bool
forall a. (Integral a, C a) => a -> Bool
intQuery
  stdAssociate :: Int64 -> Int64
stdAssociate = Int64 -> Int64
forall a. (Integral a, C a, C a) => a -> a
intAssociate
  stdUnit :: Int64 -> Int64
stdUnit      = Int64 -> Int64
forall a. (Integral a, C a, C a) => a -> a
intStandard
  stdUnitInv :: Int64 -> Int64
stdUnitInv   = Int64 -> Int64
forall a. (Integral a, C a, C a) => a -> a
intStandardInverse


{-
fieldQuery = not . isZero
fieldAssociate = 1
fieldStandard        x = if isZero x then 1 else x
fieldStandardInverse x = if isZero x then 1 else recip x
-}



propComposition      :: (Eq a, C a) => a -> Bool
propInverseUnit      :: (Eq a, C a) => a -> Bool
propUniqueAssociate  :: (Eq a, C a) => a -> a -> Property
propAssociateProduct :: (Eq a, C a) => a -> a -> Bool

propComposition :: a -> Bool
propComposition a
x  =  a -> a
forall a. C a => a -> a
stdAssociate a
x a -> a -> a
forall a. C a => a -> a -> a
* a -> a
forall a. C a => a -> a
stdUnit a
x a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
x
propInverseUnit :: a -> Bool
propInverseUnit a
x  =    a -> a
forall a. C a => a -> a
stdUnit a
x a -> a -> a
forall a. C a => a -> a -> a
* a -> a
forall a. C a => a -> a
stdUnitInv a
x a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
forall a. C a => a
one
propUniqueAssociate :: a -> a -> Property
propUniqueAssociate a
u a
x =
                     a -> Bool
forall a. C a => a -> Bool
isUnit a
u Bool -> Bool -> Property
forall prop. Testable prop => Bool -> prop -> Property
==> a -> a
forall a. C a => a -> a
stdAssociate a
x a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a -> a
forall a. C a => a -> a
stdAssociate (a
xa -> a -> a
forall a. C a => a -> a -> a
*a
u)

{- | Currently some algorithms assume this property. -}
propAssociateProduct :: a -> a -> Bool
propAssociateProduct =
    (a -> a) -> (a -> a -> a) -> (a -> a -> a) -> a -> a -> Bool
forall a b.
Eq a =>
(b -> a) -> (b -> b -> b) -> (a -> a -> a) -> b -> b -> Bool
Laws.homomorphism a -> a
forall a. C a => a -> a
stdAssociate a -> a -> a
forall a. C a => a -> a -> a
(*) a -> a -> a
forall a. C a => a -> a -> a
(*)