```-- |
-- Module:      Math.NumberTheory.Moduli.Chinese
-- Copyright:   (c) 2011 Daniel Fischer, 2018 Andrew Lelechenko
-- Licence:     MIT
-- Maintainer:  Andrew Lelechenko <andrew.lelechenko@gmail.com>
--
-- Chinese remainder theorem
--

{-# LANGUAGE RankNTypes          #-}
{-# LANGUAGE ScopedTypeVariables #-}

module Math.NumberTheory.Moduli.Chinese
( -- * Safe interface
chinese
, chineseSomeMod
) where

import Prelude hiding ((^), (+), (-), (*), rem, mod, quot, gcd, lcm)

import Data.Euclidean
import Data.Mod
import Data.Ratio
import Data.Semiring (Semiring(..), (+), (-), (*), Ring)
import GHC.TypeNats (KnownNat, natVal)

import Math.NumberTheory.Moduli.SomeMod

-- | 'chinese' @(n1, m1)@ @(n2, m2)@ returns @(n, lcm m1 m2)@ such that
-- @n \`mod\` m1 == n1@ and @n \`mod\` m2 == n2@, if exists.
-- Moduli @m1@ and @m2@ are allowed to have common factors.
--
-- >>> chinese (1, 2) (2, 3)
-- Just (-1, 6)
-- >>> chinese (3, 4) (5, 6)
-- Just (-1, 12)
-- >>> chinese (3, 4) (2, 6)
-- Nothing
chinese :: forall a. (Eq a, Ring a, Euclidean a) => (a, a) -> (a, a) -> Maybe (a, a)
chinese :: forall a.
(Eq a, Ring a, Euclidean a) =>
(a, a) -> (a, a) -> Maybe (a, a)
chinese (a
n1, a
m1) (a
n2, a
m2)
| a
d forall a. Eq a => a -> a -> Bool
== forall a. Semiring a => a
one
= forall a. a -> Maybe a
Just ((a
v forall a. Semiring a => a -> a -> a
* a
m2 forall a. Semiring a => a -> a -> a
* a
n1 forall a. Semiring a => a -> a -> a
+ a
u forall a. Semiring a => a -> a -> a
* a
m1 forall a. Semiring a => a -> a -> a
* a
n2) forall a. Euclidean a => a -> a -> a
`rem` a
m, a
m)
| (a
n1 forall a. Ring a => a -> a -> a
- a
n2) forall a. Euclidean a => a -> a -> a
`rem` a
d forall a. Eq a => a -> a -> Bool
== forall a. Semiring a => a
zero
= forall a. a -> Maybe a
Just ((a
v forall a. Semiring a => a -> a -> a
* (a
m2 forall a. Euclidean a => a -> a -> a
`quot` a
d) forall a. Semiring a => a -> a -> a
* a
n1 forall a. Semiring a => a -> a -> a
+ a
u forall a. Semiring a => a -> a -> a
* (a
m1 forall a. Euclidean a => a -> a -> a
`quot` a
d) forall a. Semiring a => a -> a -> a
* a
n2) forall a. Euclidean a => a -> a -> a
`rem` a
m, a
m)
| Bool
otherwise
= forall a. Maybe a
Nothing
where
(a
d, a
u, a
v) = forall a. (Eq a, Ring a, Euclidean a) => a -> a -> (a, a, a)
extendedGCD a
m1 a
m2
m :: a
m = if a
d forall a. Eq a => a -> a -> Bool
== forall a. Semiring a => a
one then a
m1 forall a. Semiring a => a -> a -> a
* a
m2 else (a
m1 forall a. Euclidean a => a -> a -> a
`quot` a
d) forall a. Semiring a => a -> a -> a
* a
m2

{-# SPECIALISE chinese :: (Int, Int) -> (Int, Int) -> Maybe (Int, Int) #-}
{-# SPECIALISE chinese :: (Word, Word) -> (Word, Word) -> Maybe (Word, Word) #-}
{-# SPECIALISE chinese :: (Integer, Integer) -> (Integer, Integer) -> Maybe (Integer, Integer) #-}

isCompatible :: KnownNat m => Mod m -> Rational -> Bool
isCompatible :: forall (m :: Nat). KnownNat m => Mod m -> Rational -> Bool
isCompatible Mod m
n Rational
r = case forall (m :: Nat). KnownNat m => Mod m -> Maybe (Mod m)
invertMod (forall a. Num a => Integer -> a
fromInteger (forall a. Ratio a -> a
denominator Rational
r)) of
Maybe (Mod m)
Nothing -> Bool
False
Just Mod m
r' -> Mod m
r' forall a. Semiring a => a -> a -> a
* forall a. Num a => Integer -> a
fromInteger (forall a. Ratio a -> a
numerator Rational
r) forall a. Eq a => a -> a -> Bool
== Mod m
n

-- | Same as 'chinese', but operates on residues.
--
-- >>> :set -XDataKinds
-- >>> import Data.Mod
-- >>> (1 `modulo` 2) `chineseSomeMod` (2 `modulo` 3)
-- Just (5 `modulo` 6)
-- >>> (3 `modulo` 4) `chineseSomeMod` (5 `modulo` 6)
-- Just (11 `modulo` 12)
-- >>> (3 `modulo` 4) `chineseSomeMod` (2 `modulo` 6)
-- Nothing
chineseSomeMod :: SomeMod -> SomeMod -> Maybe SomeMod
chineseSomeMod :: SomeMod -> SomeMod -> Maybe SomeMod
chineseSomeMod (SomeMod Mod m
n1) (SomeMod Mod m
n2)
= (\(Integer
n, Integer
m) -> Integer
n Integer -> Nat -> SomeMod
`modulo` forall a. Num a => Integer -> a
fromInteger Integer
m) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<\$> forall a.
(Eq a, Ring a, Euclidean a) =>
(a, a) -> (a, a) -> Maybe (a, a)
chinese
(forall a. Integral a => a -> Integer
toInteger forall a b. (a -> b) -> a -> b
\$ forall (m :: Nat). Mod m -> Nat
unMod Mod m
n1, forall a. Integral a => a -> Integer
toInteger forall a b. (a -> b) -> a -> b
\$ forall (n :: Nat) (proxy :: Nat -> *). KnownNat n => proxy n -> Nat
natVal Mod m
n1)
(forall a. Integral a => a -> Integer
toInteger forall a b. (a -> b) -> a -> b
\$ forall (m :: Nat). Mod m -> Nat
unMod Mod m
n2, forall a. Integral a => a -> Integer
toInteger forall a b. (a -> b) -> a -> b
\$ forall (n :: Nat) (proxy :: Nat -> *). KnownNat n => proxy n -> Nat
natVal Mod m
n2)
chineseSomeMod (SomeMod Mod m
n) (InfMod Rational
r)
| forall (m :: Nat). KnownNat m => Mod m -> Rational -> Bool
isCompatible Mod m
n Rational
r = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
\$ Rational -> SomeMod
InfMod Rational
r
| Bool
otherwise        = forall a. Maybe a
Nothing
chineseSomeMod (InfMod Rational
r) (SomeMod Mod m
n)
| forall (m :: Nat). KnownNat m => Mod m -> Rational -> Bool
isCompatible Mod m
n Rational
r = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
\$ Rational -> SomeMod
InfMod Rational
r
| Bool
otherwise        = forall a. Maybe a
Nothing
chineseSomeMod (InfMod Rational
r1) (InfMod Rational
r2)
| Rational
r1 forall a. Eq a => a -> a -> Bool
== Rational
r2  = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
\$ Rational -> SomeMod
InfMod Rational
r1
| Bool
otherwise = forall a. Maybe a
Nothing

-------------------------------------------------------------------------------
-- Utils

extendedGCD :: (Eq a, Ring a, Euclidean a) => a -> a -> (a, a, a)
extendedGCD :: forall a. (Eq a, Ring a, Euclidean a) => a -> a -> (a, a, a)
extendedGCD a
a a
b = (a
g, a
s, a
t)
where
(a
g, a
s) = forall a. (Eq a, Euclidean a, Ring a) => a -> a -> (a, a)
gcdExt a
a a
b
t :: a
t = (a
g forall a. Ring a => a -> a -> a
- a
a forall a. Semiring a => a -> a -> a
* a
s) forall a. Euclidean a => a -> a -> a
`quot` a
b
```