```{-# OPTIONS -fno-implicit-prelude #-}
module Algebra.IntegralDomain (
{- * Class -}
C,
div, mod, divMod,

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

{- * Algorithms -}
decomposeVarPositional,
decomposeVarPositionalInf,

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

import qualified Algebra.Ring         as Ring
import qualified Algebra.ZeroTestable as ZeroTestable

import Algebra.Ring     ((*), fromInteger)
import Algebra.ZeroTestable (isZero)

import NumericPrelude.Condition(implies)
import Data.List(mapAccumL)

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

import PreludeBase
import Prelude (Integer, Int)
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)

div a b = fst (divMod a b)
mod a b = snd (divMod a b)
divMod a b = (div a b, mod a b)

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

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.
-}
safeDiv :: (ZeroTestable.C a, C a) => a -> a -> a
safeDiv a b =
let (q,r) = divMod a b
in  if isZero r
then q
else error "safeDiv: indivisible term"

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

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

{- * Instances for atomic types -}

instance C Integer where
divMod = P.divMod

instance C Int where
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
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
```