{-# LANGUAGE RebindableSyntax #-}
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.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


{- $setup
>>> import Algebra.IntegralDomain (roundDown, roundUp, divUp)
>>> import qualified Test.QuickCheck as QC
>>> import NumericPrelude.Base as P
>>> import NumericPrelude.Numeric as NP
>>> import Prelude ()
-}


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
    {-# MINIMAL divMod | (div, mod) #-}
    div, mod :: a -> a -> a
    {- |
    prop> \n (QC.NonZero m) -> let (q,r) = divMod n m in n == (q*m+r :: Integer)
    -}
    divMod :: a -> a -> (a,a)

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


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

{-# INLINE sameResidueClass #-}
sameResidueClass :: (C a, ZeroTestable.C a) => a -> a -> a -> Bool
sameResidueClass :: a -> a -> a -> Bool
sameResidueClass a
m a
x a
y = a -> a -> Bool
forall a. (C a, C a) => a -> a -> Bool
divides a
m (a
xa -> a -> a
forall a. C a => a -> a -> a
-a
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 :: [a] -> a -> [a]
decomposeVarPositional [a]
bs a
x =
   ((a, a) -> a) -> [(a, a)] -> [a]
forall a b. (a -> b) -> [a] -> [b]
map (a, a) -> a
forall a b. (a, b) -> a
fst ([(a, a)] -> [a]) -> [(a, a)] -> [a]
forall a b. (a -> b) -> a -> b
$
   ((a, a) -> Bool) -> [(a, a)] -> [(a, a)]
forall a. (a -> Bool) -> [a] -> [a]
takeWhile (Bool -> Bool
not (Bool -> Bool) -> ((a, a) -> Bool) -> (a, a) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Bool
forall a. C a => a -> Bool
isZero (a -> Bool) -> ((a, a) -> a) -> (a, a) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a, a) -> a
forall a b. (a, b) -> b
snd) ([(a, a)] -> [(a, a)]) -> [(a, a)] -> [(a, a)]
forall a b. (a -> b) -> a -> b
$
   [a] -> a -> [(a, a)]
forall a. C a => [a] -> a -> [(a, a)]
decomposeVarPositionalInfAux [a]
bs a
x

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

decomposeVarPositionalInfAux :: (C a) => [a] -> a -> [(a,a)]
decomposeVarPositionalInfAux :: [a] -> a -> [(a, a)]
decomposeVarPositionalInfAux [a]
bs a
x =
   let (a
endN,[(a, a)]
digits) =
          (a -> a -> (a, (a, a))) -> a -> [a] -> (a, [(a, a)])
forall (t :: * -> *) a b c.
Traversable t =>
(a -> b -> (a, c)) -> a -> t b -> (a, t c)
mapAccumL
             (\a
n a
b -> let (a
q,a
r) = a -> a -> (a, a)
forall a. C a => a -> a -> (a, a)
divMod a
n a
b in (a
q,(a
r,a
n)))
             a
x [a]
bs
   in  [(a, a)]
digits [(a, a)] -> [(a, a)] -> [(a, a)]
forall a. [a] -> [a] -> [a]
++ [(a
endN,a
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 -> a -> a
divChecked a
a a
b =
   let (a
q,a
r) = a -> a -> (a, a)
forall a. C a => a -> a -> (a, a)
divMod a
a a
b
   in  if a -> Bool
forall a. C a => a -> Bool
isZero a
r
         then a
q
         else [Char] -> a
forall a. HasCallStack => [Char] -> a
error [Char]
"safeDiv: indivisible term"

{-# DEPRECATED safeDiv "use divChecked instead" #-}
safeDiv :: a -> a -> a
safeDiv = a -> a -> a
forall a. (C a, C a) => a -> a -> a
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 :: a -> a -> (a, a)
divModZero a
x a
y =
   if a -> Bool
forall a. C a => a -> Bool
isZero a
y
     then (a
forall a. C a => a
zero,a
x)
     else a -> a -> (a, a)
forall a. C a => a -> a -> (a, a)
divMod a
x a
y



{-# INLINE even #-}
{-# INLINE odd #-}
even, odd :: (C a, ZeroTestable.C a) => a -> Bool
even :: a -> Bool
even a
n    =  a -> a -> Bool
forall a. (C a, C a) => a -> a -> Bool
divides a
2 a
n
odd :: a -> Bool
odd       =  Bool -> Bool
not (Bool -> Bool) -> (a -> Bool) -> a -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Bool
forall a. (C a, C a) => a -> Bool
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.

prop> \n (QC.NonZero m) -> div n m * m == (roundDown n m :: Integer)
-}
roundDown :: C a => a -> a -> a
roundDown :: a -> a -> a
roundDown a
n a
m = a
n a -> a -> a
forall a. C a => a -> a -> a
- a -> a -> a
forall a. C a => a -> a -> a
mod a
n a
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@.

prop> \n (QC.NonZero m) -> divUp n m * m == (roundUp n m :: Integer)
prop> \n (QC.Positive m) -> let x = roundDown n m in  n-m < x && x <= (n :: Integer)
prop> \n (QC.NonZero m) -> - roundDown n m == (roundUp (-n) m :: Integer)
-}
roundUp :: C a => a -> a -> a
roundUp :: a -> a -> a
roundUp a
n a
m = a
n a -> a -> a
forall a. C a => a -> a -> a
+ a -> a -> a
forall a. C a => a -> a -> a
mod (-a
n) a
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 :: a -> a -> a
divUp a
n a
m = - a -> a -> a
forall a. C a => a -> a -> a
div (-a
n) a
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 :: Integer -> Integer -> Integer
div = Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
P.div
   mod :: Integer -> Integer -> Integer
mod = Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
P.mod
   divMod :: Integer -> Integer -> (Integer, Integer)
divMod = Integer -> Integer -> (Integer, Integer)
forall a. Integral a => a -> a -> (a, a)
P.divMod

instance C Int     where
   {-# INLINE div #-}
   {-# INLINE mod #-}
   {-# INLINE divMod #-}
   div :: Int -> Int -> Int
div = Int -> Int -> Int
forall a. Integral a => a -> a -> a
P.div
   mod :: Int -> Int -> Int
mod = Int -> Int -> Int
forall a. Integral a => a -> a -> a
P.mod
   divMod :: Int -> Int -> (Int, Int)
divMod = Int -> Int -> (Int, Int)
forall a. Integral a => a -> a -> (a, a)
P.divMod

instance C Int8    where
   {-# INLINE div #-}
   {-# INLINE mod #-}
   {-# INLINE divMod #-}
   div :: Int8 -> Int8 -> Int8
div = Int8 -> Int8 -> Int8
forall a. Integral a => a -> a -> a
P.div
   mod :: Int8 -> Int8 -> Int8
mod = Int8 -> Int8 -> Int8
forall a. Integral a => a -> a -> a
P.mod
   divMod :: Int8 -> Int8 -> (Int8, Int8)
divMod = Int8 -> Int8 -> (Int8, Int8)
forall a. Integral a => a -> a -> (a, a)
P.divMod

instance C Int16   where
   {-# INLINE div #-}
   {-# INLINE mod #-}
   {-# INLINE divMod #-}
   div :: Int16 -> Int16 -> Int16
div = Int16 -> Int16 -> Int16
forall a. Integral a => a -> a -> a
P.div
   mod :: Int16 -> Int16 -> Int16
mod = Int16 -> Int16 -> Int16
forall a. Integral a => a -> a -> a
P.mod
   divMod :: Int16 -> Int16 -> (Int16, Int16)
divMod = Int16 -> Int16 -> (Int16, Int16)
forall a. Integral a => a -> a -> (a, a)
P.divMod

instance C Int32   where
   {-# INLINE div #-}
   {-# INLINE mod #-}
   {-# INLINE divMod #-}
   div :: Int32 -> Int32 -> Int32
div = Int32 -> Int32 -> Int32
forall a. Integral a => a -> a -> a
P.div
   mod :: Int32 -> Int32 -> Int32
mod = Int32 -> Int32 -> Int32
forall a. Integral a => a -> a -> a
P.mod
   divMod :: Int32 -> Int32 -> (Int32, Int32)
divMod = Int32 -> Int32 -> (Int32, Int32)
forall a. Integral a => a -> a -> (a, a)
P.divMod

instance C Int64   where
   {-# INLINE div #-}
   {-# INLINE mod #-}
   {-# INLINE divMod #-}
   div :: Int64 -> Int64 -> Int64
div = Int64 -> Int64 -> Int64
forall a. Integral a => a -> a -> a
P.div
   mod :: Int64 -> Int64 -> Int64
mod = Int64 -> Int64 -> Int64
forall a. Integral a => a -> a -> a
P.mod
   divMod :: Int64 -> Int64 -> (Int64, Int64)
divMod = Int64 -> Int64 -> (Int64, Int64)
forall a. Integral a => a -> a -> (a, a)
P.divMod


instance C Word    where
   {-# INLINE div #-}
   {-# INLINE mod #-}
   {-# INLINE divMod #-}
   div :: Word -> Word -> Word
div = Word -> Word -> Word
forall a. Integral a => a -> a -> a
P.div
   mod :: Word -> Word -> Word
mod = Word -> Word -> Word
forall a. Integral a => a -> a -> a
P.mod
   divMod :: Word -> Word -> (Word, Word)
divMod = Word -> Word -> (Word, Word)
forall a. Integral a => a -> a -> (a, a)
P.divMod

instance C Word8   where
   {-# INLINE div #-}
   {-# INLINE mod #-}
   {-# INLINE divMod #-}
   div :: Word8 -> Word8 -> Word8
div = Word8 -> Word8 -> Word8
forall a. Integral a => a -> a -> a
P.div
   mod :: Word8 -> Word8 -> Word8
mod = Word8 -> Word8 -> Word8
forall a. Integral a => a -> a -> a
P.mod
   divMod :: Word8 -> Word8 -> (Word8, Word8)
divMod = Word8 -> Word8 -> (Word8, Word8)
forall a. Integral a => a -> a -> (a, a)
P.divMod

instance C Word16  where
   {-# INLINE div #-}
   {-# INLINE mod #-}
   {-# INLINE divMod #-}
   div :: Word16 -> Word16 -> Word16
div = Word16 -> Word16 -> Word16
forall a. Integral a => a -> a -> a
P.div
   mod :: Word16 -> Word16 -> Word16
mod = Word16 -> Word16 -> Word16
forall a. Integral a => a -> a -> a
P.mod
   divMod :: Word16 -> Word16 -> (Word16, Word16)
divMod = Word16 -> Word16 -> (Word16, Word16)
forall a. Integral a => a -> a -> (a, a)
P.divMod

instance C Word32  where
   {-# INLINE div #-}
   {-# INLINE mod #-}
   {-# INLINE divMod #-}
   div :: Word32 -> Word32 -> Word32
div = Word32 -> Word32 -> Word32
forall a. Integral a => a -> a -> a
P.div
   mod :: Word32 -> Word32 -> Word32
mod = Word32 -> Word32 -> Word32
forall a. Integral a => a -> a -> a
P.mod
   divMod :: Word32 -> Word32 -> (Word32, Word32)
divMod = Word32 -> Word32 -> (Word32, Word32)
forall a. Integral a => a -> a -> (a, a)
P.divMod

instance C Word64  where
   {-# INLINE div #-}
   {-# INLINE mod #-}
   {-# INLINE divMod #-}
   div :: Word64 -> Word64 -> Word64
div = Word64 -> Word64 -> Word64
forall a. Integral a => a -> a -> a
P.div
   mod :: Word64 -> Word64 -> Word64
mod = Word64 -> Word64 -> Word64
forall a. Integral a => a -> a -> a
P.mod
   divMod :: Word64 -> Word64 -> (Word64, Word64)
divMod = Word64 -> Word64 -> (Word64, Word64)
forall a. Integral a => a -> a -> (a, a)
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 :: a -> a -> Property
propInverse     a
m a
a =
   Bool -> Bool
not (a -> Bool
forall a. C a => a -> Bool
isZero a
m) Bool -> Bool -> Property
forall prop. Testable prop => Bool -> prop -> Property
==> (a
a a -> a -> a
forall a. C a => a -> a -> a
`div` a
m) a -> a -> a
forall a. C a => a -> a -> a
* a
m a -> a -> a
forall a. C a => a -> a -> a
+ (a
a a -> a -> a
forall a. C a => a -> a -> a
`mod` a
m)  a -> a -> Bool
forall a. Eq a => a -> a -> Bool
==  a
a
propMultipleDiv :: a -> a -> Property
propMultipleDiv a
m a
a =
   Bool -> Bool
not (a -> Bool
forall a. C a => a -> Bool
isZero a
m) Bool -> Bool -> Property
forall prop. Testable prop => Bool -> prop -> Property
==>                 (a
aa -> a -> a
forall a. C a => a -> a -> a
*a
m) a -> a -> a
forall a. C a => a -> a -> a
`div` a
m  a -> a -> Bool
forall a. Eq a => a -> a -> Bool
==  a
a
propMultipleMod :: a -> a -> Property
propMultipleMod a
m a
a =
   Bool -> Bool
not (a -> Bool
forall a. C a => a -> Bool
isZero a
m) Bool -> Bool -> Property
forall prop. Testable prop => Bool -> prop -> Property
==>                 (a
aa -> a -> a
forall a. C a => a -> a -> a
*a
m) a -> a -> a
forall a. C a => a -> a -> a
`mod` a
m  a -> a -> Bool
forall a. Eq a => a -> a -> Bool
==  a
0
propProjectAddition :: a -> a -> a -> Property
propProjectAddition a
m a
a a
b =
   Bool -> Bool
not (a -> Bool
forall a. C a => a -> Bool
isZero a
m) Bool -> Bool -> Property
forall prop. Testable prop => Bool -> prop -> Property
==>
      (a
aa -> a -> a
forall a. C a => a -> a -> a
+a
b) a -> a -> a
forall a. C a => a -> a -> a
`mod` a
m  a -> a -> Bool
forall a. Eq a => a -> a -> Bool
==  ((a
aa -> a -> a
forall a. C a => a -> a -> a
`mod`a
m)a -> a -> a
forall a. C a => a -> a -> a
+(a
ba -> a -> a
forall a. C a => a -> a -> a
`mod`a
m)) a -> a -> a
forall a. C a => a -> a -> a
`mod` a
m
propProjectMultiplication :: a -> a -> a -> Property
propProjectMultiplication a
m a
a a
b =
   Bool -> Bool
not (a -> Bool
forall a. C a => a -> Bool
isZero a
m) Bool -> Bool -> Property
forall prop. Testable prop => Bool -> prop -> Property
==>
      (a
aa -> a -> a
forall a. C a => a -> a -> a
*a
b) a -> a -> a
forall a. C a => a -> a -> a
`mod` a
m  a -> a -> Bool
forall a. Eq a => a -> a -> Bool
==  ((a
aa -> a -> a
forall a. C a => a -> a -> a
`mod`a
m)a -> a -> a
forall a. C a => a -> a -> a
*(a
ba -> a -> a
forall a. C a => a -> a -> a
`mod`a
m)) a -> a -> a
forall a. C a => a -> a -> a
`mod` a
m
propUniqueRepresentative :: a -> a -> a -> Property
propUniqueRepresentative a
m a
k a
a =
   Bool -> Bool
not (a -> Bool
forall a. C a => a -> Bool
isZero a
m) Bool -> Bool -> Property
forall prop. Testable prop => Bool -> prop -> Property
==>
      (a
aa -> a -> a
forall a. C a => a -> a -> a
+a
ka -> a -> a
forall a. C a => a -> a -> a
*a
m) a -> a -> a
forall a. C a => a -> a -> a
`mod` a
m  a -> a -> Bool
forall a. Eq a => a -> a -> Bool
==  a
a a -> a -> a
forall a. C a => a -> a -> a
`mod` a
m
propZeroRepresentative :: a -> Property
propZeroRepresentative a
m =
   Bool -> Bool
not (a -> Bool
forall a. C a => a -> Bool
isZero a
m) Bool -> Bool -> Property
forall prop. Testable prop => Bool -> prop -> Property
==>
      a
forall a. C a => a
zero a -> a -> a
forall a. C a => a -> a -> a
`mod` a
m  a -> a -> Bool
forall a. Eq a => a -> a -> Bool
==  a
forall a. C a => a
zero
propSameResidueClass :: a -> a -> a -> Property
propSameResidueClass a
m a
a a
b =
   Bool -> Bool
not (a -> Bool
forall a. C a => a -> Bool
isZero a
m) Bool -> Bool -> Property
forall prop. Testable prop => Bool -> prop -> Property
==>
      a
a a -> a -> a
forall a. C a => a -> a -> a
`mod` a
m a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
b a -> a -> a
forall a. C a => a -> a -> a
`mod` a
m   Bool -> Bool -> Bool
`implies`   a -> a -> a -> Bool
forall a. (C a, C a) => a -> a -> a -> Bool
sameResidueClass a
m a
a a
b