{-# LANGUAGE CPP #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
module Math.NumberTheory.Moduli.SomeMod
( SomeMod(..)
, modulo
, invertSomeMod
, powSomeMod
) where
import Data.Euclidean (GcdDomain(..), Euclidean(..), Field)
import Data.Mod
import Data.Proxy
#if __GLASGOW_HASKELL__ < 803
import Data.Semigroup
#endif
import Data.Semiring (Semiring(..), Ring(..))
import Data.Type.Equality
import GHC.TypeNats (KnownNat, SomeNat(..), sameNat, natVal, someNatVal)
import Numeric.Natural
data SomeMod where
SomeMod :: KnownNat m => Mod m -> SomeMod
InfMod :: Rational -> SomeMod
instance Eq SomeMod where
SomeMod mx == SomeMod my =
natVal mx == natVal my && unMod mx == unMod my
InfMod rx == InfMod ry = rx == ry
_ == _ = False
instance Ord SomeMod where
SomeMod mx `compare` SomeMod my =
natVal mx `compare` natVal my <> unMod mx `compare` unMod my
SomeMod{} `compare` InfMod{} = LT
InfMod{} `compare` SomeMod{} = GT
InfMod rx `compare` InfMod ry = rx `compare` ry
instance Show SomeMod where
show = \case
SomeMod m -> show m
InfMod r -> show r
modulo :: Integer -> Natural -> SomeMod
modulo n m = case someNatVal m of
SomeNat (_ :: Proxy t) -> SomeMod (fromInteger n :: Mod t)
{-# INLINABLE modulo #-}
infixl 7 `modulo`
liftUnOp
:: (forall k. KnownNat k => Mod k -> Mod k)
-> (Rational -> Rational)
-> SomeMod
-> SomeMod
liftUnOp fm fr = \case
SomeMod m -> SomeMod (fm m)
InfMod r -> InfMod (fr r)
{-# INLINEABLE liftUnOp #-}
liftBinOpMod
:: (KnownNat m, KnownNat n)
=> (forall k. KnownNat k => Mod k -> Mod k -> Mod k)
-> Mod m
-> Mod n
-> SomeMod
liftBinOpMod f mx my = case someNatVal m of
SomeNat (_ :: Proxy t) ->
SomeMod (fromIntegral (x `mod` m) `f` fromIntegral (y `mod` m) :: Mod t)
where
x = unMod mx
y = unMod my
m = natVal mx `Prelude.gcd` natVal my
liftBinOp
:: (forall k. KnownNat k => Mod k -> Mod k -> Mod k)
-> (Rational -> Rational -> Rational)
-> SomeMod
-> SomeMod
-> SomeMod
liftBinOp _ fr (InfMod rx) (InfMod ry) = InfMod (rx `fr` ry)
liftBinOp fm _ (InfMod rx) (SomeMod my) = SomeMod (fromRational rx `fm` my)
liftBinOp fm _ (SomeMod mx) (InfMod ry) = SomeMod (mx `fm` fromRational ry)
liftBinOp fm _ (SomeMod (mx :: Mod m)) (SomeMod (my :: Mod n))
= case (Proxy :: Proxy m) `sameNat` (Proxy :: Proxy n) of
Nothing -> liftBinOpMod fm mx my
Just Refl -> SomeMod (mx `fm` my)
instance Num SomeMod where
(+) = liftBinOp (+) (+)
(-) = liftBinOp (-) (-)
negate = liftUnOp Prelude.negate Prelude.negate
{-# INLINE negate #-}
(*) = liftBinOp (*) (*)
abs = id
{-# INLINE abs #-}
signum = const 1
{-# INLINE signum #-}
fromInteger = InfMod . fromInteger
{-# INLINE fromInteger #-}
instance Semiring SomeMod where
plus = (+)
times = (*)
zero = InfMod 0
one = InfMod 1
fromNatural = fromIntegral
instance Ring SomeMod where
negate = Prelude.negate
instance Fractional SomeMod where
fromRational = InfMod
{-# INLINE fromRational #-}
recip x = case invertSomeMod x of
Nothing -> error $ "recip{SomeMod}: residue is not coprime with modulo"
Just y -> y
instance GcdDomain SomeMod where
divide x y = Just (x / y)
gcd = const $ const 1
lcm = const $ const 1
coprime = const $ const True
instance Euclidean SomeMod where
degree = const 0
quotRem x y = (x / y, 0)
quot = (/)
rem = const $ const 0
instance Field SomeMod
invertSomeMod :: SomeMod -> Maybe SomeMod
invertSomeMod = \case
SomeMod m -> fmap SomeMod (invertMod m)
InfMod r -> Just (InfMod (recip r))
{-# INLINABLE [1] invertSomeMod #-}
{-# SPECIALISE [1] powSomeMod ::
SomeMod -> Integer -> SomeMod,
SomeMod -> Natural -> SomeMod,
SomeMod -> Int -> SomeMod,
SomeMod -> Word -> SomeMod #-}
powSomeMod :: Integral a => SomeMod -> a -> SomeMod
powSomeMod (SomeMod m) a = SomeMod (m ^% a)
powSomeMod (InfMod r) a = InfMod (r ^ a)
{-# INLINABLE [1] powSomeMod #-}
{-# RULES "^%SomeMod" forall x p. x ^ p = powSomeMod x p #-}