{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
module Math.NumberTheory.Moduli.Chinese
(
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 :: 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
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
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