IntegralDomain.hs

{-# LANGUAGE NoImplicitPrelude #-}
module Algebra.IntegralDomain (
    {- * Class -}
    C,
    div, mod, divMod,

    {- * Derived functions -}
    divModZero,
    divides,
    sameResidueClass,
    divChecked, safeDiv,
    even,
    odd,

    divUp,
    roundDown,
    roundUp,

    {- * Algorithms -}
    decomposeVarPositional,
    decomposeVarPositionalInf,

    {- * Properties -}
    propInverse,
    propMultipleDiv,
    propMultipleMod,
    propProjectAddition,
    propProjectMultiplication,
    propUniqueRepresentative,
    propZeroRepresentative,
    propSameResidueClass,
  ) where

import qualified Algebra.Ring         as Ring
-- import qualified Algebra.Additive     as Additive
import qualified Algebra.ZeroTestable as ZeroTestable

import Algebra.Ring     ((*), fromInteger, )
import Algebra.Additive (zero, (+), (-), negate, )
import Algebra.ZeroTestable (isZero, )

import Data.Bool.HT (implies, )
import Data.List (mapAccumL, )

import Test.QuickCheck ((==>), Property)

import Data.Int  (Int,  Int8,  Int16,  Int32,  Int64,  )
import Data.Word (Word, Word8, Word16, Word32, Word64, )

import NumericPrelude.Base
import Prelude (Integer, )
import qualified Prelude as P



infixl 7 `div`, `mod`


{-
Shall we require
                   @ a `mod` 0 === a @   (divModZero)
or
                   @ a `mod` 0 === undefined @
?
-}


{- |
@IntegralDomain@ corresponds to a commutative ring,
where @a `mod` b@ picks a canonical element
of the equivalence class of @a@ in the ideal generated by @b@.
'div' and 'mod' satisfy the laws

>                         a * b === b * a
> (a `div` b) * b + (a `mod` b) === a
>               (a+k*b) `mod` b === a `mod` b
>                     0 `mod` b === 0

Typical examples of @IntegralDomain@ include integers and
polynomials over a field.
Note that for a field, there is a canonical instance
defined by the above rules; e.g.,

> instance IntegralDomain.C Rational where
>     divMod a b =
>        if isZero b
>          then (undefined,a)
>          else (a\/b,0)

It shall be noted, that 'div', 'mod', 'divMod' have a parameter order
which is unfortunate for partial application.
But it is adapted to mathematical conventions,
where the operators are used in infix notation.

Minimal definition: 'divMod' or ('div' and 'mod')
-}
class (Ring.C a) => C a where
    div, mod :: a -> a -> a
    divMod :: a -> a -> (a,a)

    {-# INLINE div #-}
    {-# INLINE mod #-}
    {-# INLINE divMod #-}
    div a b = fst (divMod a b)
    mod a b = snd (divMod a b)
    divMod a b = (div a b, mod a b)


{-# INLINE divides #-}
divides :: (C a, ZeroTestable.C a) => a -> a -> Bool
divides y x  =  isZero (mod x y)

{-# INLINE sameResidueClass #-}
sameResidueClass :: (C a, ZeroTestable.C a) => a -> a -> a -> Bool
sameResidueClass m x y = divides m (x-y)



{- |
@decomposeVarPositional [b0,b1,b2,...] x@
decomposes @x@ into a positional representation with mixed bases
@x0 + b0*(x1 + b1*(x2 + b2*x3))@
E.g. @decomposeVarPositional (repeat 10) 123 == [3,2,1]@
-}
decomposeVarPositional :: (C a, ZeroTestable.C a) => [a] -> a -> [a]
decomposeVarPositional bs x =
   map fst $
   takeWhile (not . isZero . snd) $
   decomposeVarPositionalInfAux bs x

decomposeVarPositionalInf :: (C a) => [a] -> a -> [a]
decomposeVarPositionalInf bs =
   map fst . decomposeVarPositionalInfAux bs

decomposeVarPositionalInfAux :: (C a) => [a] -> a -> [(a,a)]
decomposeVarPositionalInfAux bs x =
   let (endN,digits) =
          mapAccumL
             (\n b -> let (q,r) = divMod n b in (q,(r,n)))
             x bs
   in  digits ++ [(endN,endN)]



{- |
Returns the result of the division, if divisible.
Otherwise undefined.
-}
{-# INLINE divChecked #-}
divChecked, safeDiv :: (ZeroTestable.C a, C a) => a -> a -> a
divChecked a b =
   let (q,r) = divMod a b
   in  if isZero r
         then q
         else error "safeDiv: indivisible term"

{-# DEPRECATED safeDiv "use divChecked instead" #-}
safeDiv = divChecked

{- |
Allows division by zero.
If the divisor is zero, then the dividend is returned as remainder.
-}
{-# INLINE divModZero #-}
divModZero :: (C a, ZeroTestable.C a) => a -> a -> (a,a)
divModZero x y =
   if isZero y
     then (zero,x)
     else divMod x y



{-# INLINE even #-}
{-# INLINE odd #-}
even, odd :: (C a, ZeroTestable.C a) => a -> Bool
even n    =  divides 2 n
odd       =  not . even


{- |
@roundDown n m@ rounds @n@ down to the next multiple of @m@.
That is, @roundDown n m@ is the greatest multiple of @m@
that is at most @n@.
The parameter order is consistent with @div@ and friends,
but maybe not useful for partial application.
-}
roundDown :: C a => a -> a -> a
roundDown n m = n - mod n m

{- |
@roundUp n m@ rounds @n@ up to the next multiple of @m@.
That is, @roundUp n m@ is the greatest multiple of @m@
that is at most @n@.
-}
roundUp :: C a => a -> a -> a
roundUp n m = n + mod (-n) m

{- |
@divUp n m@ is similar to @div@
but it rounds up the quotient,
such that @divUp n m * m = roundUp n m@.
-}
divUp :: C a => a -> a -> a
divUp n m = - div (-n) m

{-
What sign of the remainder is most appropriate?

divModUp :: C a => a -> a -> (a,a)
divModUp n m = mapFst negate $ divMod (-n) m
-}


{- * Instances for atomic types -}

instance C Integer where
   {-# INLINE div #-}
   {-# INLINE mod #-}
   {-# INLINE divMod #-}
   div = P.div
   mod = P.mod
   divMod = P.divMod

instance C Int     where
   {-# INLINE div #-}
   {-# INLINE mod #-}
   {-# INLINE divMod #-}
   div = P.div
   mod = P.mod
   divMod = P.divMod

instance C Int8    where
   {-# INLINE div #-}
   {-# INLINE mod #-}
   {-# INLINE divMod #-}
   div = P.div
   mod = P.mod
   divMod = P.divMod

instance C Int16   where
   {-# INLINE div #-}
   {-# INLINE mod #-}
   {-# INLINE divMod #-}
   div = P.div
   mod = P.mod
   divMod = P.divMod

instance C Int32   where
   {-# INLINE div #-}
   {-# INLINE mod #-}
   {-# INLINE divMod #-}
   div = P.div
   mod = P.mod
   divMod = P.divMod

instance C Int64   where
   {-# INLINE div #-}
   {-# INLINE mod #-}
   {-# INLINE divMod #-}
   div = P.div
   mod = P.mod
   divMod = P.divMod


instance C Word    where
   {-# INLINE div #-}
   {-# INLINE mod #-}
   {-# INLINE divMod #-}
   div = P.div
   mod = P.mod
   divMod = P.divMod

instance C Word8   where
   {-# INLINE div #-}
   {-# INLINE mod #-}
   {-# INLINE divMod #-}
   div = P.div
   mod = P.mod
   divMod = P.divMod

instance C Word16  where
   {-# INLINE div #-}
   {-# INLINE mod #-}
   {-# INLINE divMod #-}
   div = P.div
   mod = P.mod
   divMod = P.divMod

instance C Word32  where
   {-# INLINE div #-}
   {-# INLINE mod #-}
   {-# INLINE divMod #-}
   div = P.div
   mod = P.mod
   divMod = P.divMod

instance C Word64  where
   {-# INLINE div #-}
   {-# INLINE mod #-}
   {-# INLINE divMod #-}
   div = P.div
   mod = P.mod
   divMod = P.divMod




-- Ring.propCommutative and ...
propInverse               :: (Eq a, C a, ZeroTestable.C a) => a -> a -> Property
propMultipleDiv           :: (Eq a, C a, ZeroTestable.C a) => a -> a -> Property
propMultipleMod           :: (Eq a, C a, ZeroTestable.C a) => a -> a -> Property
propProjectAddition       :: (Eq a, C a, ZeroTestable.C a) => a -> a -> a -> Property
propProjectMultiplication :: (Eq a, C a, ZeroTestable.C a) => a -> a -> a -> Property
propSameResidueClass      :: (Eq a, C a, ZeroTestable.C a) => a -> a -> a -> Property
propUniqueRepresentative  :: (Eq a, C a, ZeroTestable.C a) => a -> a -> a -> Property
propZeroRepresentative    :: (Eq a, C a, ZeroTestable.C a) => a -> Property


propInverse     m a =
   not (isZero m) ==> (a `div` m) * m + (a `mod` m)  ==  a
propMultipleDiv m a =
   not (isZero m) ==>                 (a*m) `div` m  ==  a
propMultipleMod m a =
   not (isZero m) ==>                 (a*m) `mod` m  ==  0
propProjectAddition m a b =
   not (isZero m) ==>
      (a+b) `mod` m  ==  ((a`mod`m)+(b`mod`m)) `mod` m
propProjectMultiplication m a b =
   not (isZero m) ==>
      (a*b) `mod` m  ==  ((a`mod`m)*(b`mod`m)) `mod` m
propUniqueRepresentative m k a =
   not (isZero m) ==>
      (a+k*m) `mod` m  ==  a `mod` m
propZeroRepresentative m =
   not (isZero m) ==>
      zero `mod` m  ==  zero
propSameResidueClass m a b =
   not (isZero m) ==>
      a `mod` m == b `mod` m   `implies`   sameResidueClass m a b