```{-# LANGUAGE NoImplicitPrelude #-}
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.ZeroTestable   (isZero)

import PreludeBase
import Prelude (Integer, Int)
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
isUnit :: a -> Bool
stdAssociate, stdUnit, stdUnitInv :: a -> a

stdAssociate x = x * stdUnitInv x
stdUnit      x = div one (stdUnitInv x)  -- should be safeDiv
stdUnitInv   x = div one (stdUnit x)

{- * Instances for atomic types -}

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

instance C Int where
isUnit       = intQuery
stdAssociate = intAssociate
stdUnit      = intStandard
stdUnitInv   = intStandardInverse

instance C Integer where
isUnit       = intQuery
stdAssociate = intAssociate
stdUnit      = intStandard
stdUnitInv   = 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 x  =  stdAssociate x * stdUnit x == x
propInverseUnit x  =    stdUnit x * stdUnitInv x == one
propUniqueAssociate u x =
isUnit u ==> stdAssociate x == stdAssociate (x*u)

{- | Currently some algorithms assume this property. -}
propAssociateProduct =
Laws.homomorphism stdAssociate (*) (*)

```