{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -Wno-identities #-}
module Numeric.Data.ModP.Internal
(
ModP (MkModP, ..),
mkModP,
unsafeModP,
invert,
reallyUnsafeModP,
Prime.errMsg,
)
where
import Control.DeepSeq (NFData)
import Data.Bounds
( AnyLowerBounded,
AnyUpperBounded,
LowerBounded,
UpperBounded,
)
import Data.Data (Proxy (Proxy))
import Data.Kind (Type)
import Data.Text.Display (Display (displayBuilder))
import Data.Typeable (Typeable)
import GHC.Generics (Generic)
import GHC.Records (HasField (getField))
import GHC.Stack (HasCallStack)
import GHC.TypeNats (KnownNat, Nat, natVal)
import Language.Haskell.TH.Syntax (Lift)
import Numeric.Algebra.Additive.AGroup (AGroup ((.-.)))
import Numeric.Algebra.Additive.AMonoid (AMonoid (zero))
import Numeric.Algebra.Additive.ASemigroup (ASemigroup ((.+.)))
import Numeric.Algebra.Field (Field)
import Numeric.Algebra.Multiplicative.MGroup (MGroup ((.%.)))
import Numeric.Algebra.Multiplicative.MMonoid (MMonoid (one))
import Numeric.Algebra.Multiplicative.MSemigroup (MSemigroup ((.*.)))
import Numeric.Algebra.Ring (Ring)
import Numeric.Algebra.Semifield (Semifield)
import Numeric.Algebra.Semiring (Semiring)
import Numeric.Data.Internal.Utils qualified as Utils
import Numeric.Data.ModP.Internal.Primality
( MaybePrime
( Composite,
ProbablyPrime
),
)
import Numeric.Data.ModP.Internal.Primality qualified as Prime
import Numeric.Literal.Integer (FromInteger (afromInteger))
import Optics.Core (A_Getter, LabelOptic (labelOptic), to)
type ModP :: Nat -> Type -> Type
newtype ModP p a = UnsafeModP a
deriving stock
(
ModP p a -> ModP p a -> Bool
(ModP p a -> ModP p a -> Bool)
-> (ModP p a -> ModP p a -> Bool) -> Eq (ModP p a)
forall (p :: Nat) a. Eq a => ModP p a -> ModP p a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall (p :: Nat) a. Eq a => ModP p a -> ModP p a -> Bool
== :: ModP p a -> ModP p a -> Bool
$c/= :: forall (p :: Nat) a. Eq a => ModP p a -> ModP p a -> Bool
/= :: ModP p a -> ModP p a -> Bool
Eq,
(forall x. ModP p a -> Rep (ModP p a) x)
-> (forall x. Rep (ModP p a) x -> ModP p a) -> Generic (ModP p a)
forall (p :: Nat) a x. Rep (ModP p a) x -> ModP p a
forall (p :: Nat) a x. ModP p a -> Rep (ModP p a) x
forall x. Rep (ModP p a) x -> ModP p a
forall x. ModP p a -> Rep (ModP p a) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall (p :: Nat) a x. ModP p a -> Rep (ModP p a) x
from :: forall x. ModP p a -> Rep (ModP p a) x
$cto :: forall (p :: Nat) a x. Rep (ModP p a) x -> ModP p a
to :: forall x. Rep (ModP p a) x -> ModP p a
Generic,
(forall (m :: Type -> Type). Quote m => ModP p a -> m Exp)
-> (forall (m :: Type -> Type).
Quote m =>
ModP p a -> Code m (ModP p a))
-> Lift (ModP p a)
forall (p :: Nat) a (m :: Type -> Type).
(Lift a, Quote m) =>
ModP p a -> m Exp
forall (p :: Nat) a (m :: Type -> Type).
(Lift a, Quote m) =>
ModP p a -> Code m (ModP p a)
forall t.
(forall (m :: Type -> Type). Quote m => t -> m Exp)
-> (forall (m :: Type -> Type). Quote m => t -> Code m t) -> Lift t
forall (m :: Type -> Type). Quote m => ModP p a -> m Exp
forall (m :: Type -> Type).
Quote m =>
ModP p a -> Code m (ModP p a)
$clift :: forall (p :: Nat) a (m :: Type -> Type).
(Lift a, Quote m) =>
ModP p a -> m Exp
lift :: forall (m :: Type -> Type). Quote m => ModP p a -> m Exp
$cliftTyped :: forall (p :: Nat) a (m :: Type -> Type).
(Lift a, Quote m) =>
ModP p a -> Code m (ModP p a)
liftTyped :: forall (m :: Type -> Type).
Quote m =>
ModP p a -> Code m (ModP p a)
Lift,
Eq (ModP p a)
Eq (ModP p a) =>
(ModP p a -> ModP p a -> Ordering)
-> (ModP p a -> ModP p a -> Bool)
-> (ModP p a -> ModP p a -> Bool)
-> (ModP p a -> ModP p a -> Bool)
-> (ModP p a -> ModP p a -> Bool)
-> (ModP p a -> ModP p a -> ModP p a)
-> (ModP p a -> ModP p a -> ModP p a)
-> Ord (ModP p a)
ModP p a -> ModP p a -> Bool
ModP p a -> ModP p a -> Ordering
ModP p a -> ModP p a -> ModP p a
forall (p :: Nat) a. Ord a => Eq (ModP p a)
forall (p :: Nat) a. Ord a => ModP p a -> ModP p a -> Bool
forall (p :: Nat) a. Ord a => ModP p a -> ModP p a -> Ordering
forall (p :: Nat) a. Ord a => ModP p a -> ModP p a -> ModP p a
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: forall (p :: Nat) a. Ord a => ModP p a -> ModP p a -> Ordering
compare :: ModP p a -> ModP p a -> Ordering
$c< :: forall (p :: Nat) a. Ord a => ModP p a -> ModP p a -> Bool
< :: ModP p a -> ModP p a -> Bool
$c<= :: forall (p :: Nat) a. Ord a => ModP p a -> ModP p a -> Bool
<= :: ModP p a -> ModP p a -> Bool
$c> :: forall (p :: Nat) a. Ord a => ModP p a -> ModP p a -> Bool
> :: ModP p a -> ModP p a -> Bool
$c>= :: forall (p :: Nat) a. Ord a => ModP p a -> ModP p a -> Bool
>= :: ModP p a -> ModP p a -> Bool
$cmax :: forall (p :: Nat) a. Ord a => ModP p a -> ModP p a -> ModP p a
max :: ModP p a -> ModP p a -> ModP p a
$cmin :: forall (p :: Nat) a. Ord a => ModP p a -> ModP p a -> ModP p a
min :: ModP p a -> ModP p a -> ModP p a
Ord
)
deriving anyclass
(
ModP p a
ModP p a -> LowerBounded (ModP p a)
forall (p :: Nat) a.
(AnyUpperBounded a, Integral a, KnownNat p, Typeable a) =>
ModP p a
forall a. a -> LowerBounded a
$clowerBound :: forall (p :: Nat) a.
(AnyUpperBounded a, Integral a, KnownNat p, Typeable a) =>
ModP p a
lowerBound :: ModP p a
LowerBounded,
ModP p a -> ()
(ModP p a -> ()) -> NFData (ModP p a)
forall (p :: Nat) a. NFData a => ModP p a -> ()
forall a. (a -> ()) -> NFData a
$crnf :: forall (p :: Nat) a. NFData a => ModP p a -> ()
rnf :: ModP p a -> ()
NFData,
ModP p a
ModP p a -> UpperBounded (ModP p a)
forall (p :: Nat) a.
(AnyUpperBounded a, Integral a, KnownNat p, Typeable a) =>
ModP p a
forall a. a -> UpperBounded a
$cupperBound :: forall (p :: Nat) a.
(AnyUpperBounded a, Integral a, KnownNat p, Typeable a) =>
ModP p a
upperBound :: ModP p a
UpperBounded
)
pattern MkModP :: a -> ModP p a
pattern $mMkModP :: forall {r} {a} {p :: Nat}.
ModP p a -> (a -> r) -> ((# #) -> r) -> r
MkModP x <- UnsafeModP x
{-# COMPLETE MkModP #-}
instance (KnownNat p, Show a) => Show (ModP p a) where
showsPrec :: Int -> ModP p a -> ShowS
showsPrec Int
i (UnsafeModP a
x) =
Bool -> ShowS -> ShowS
showParen
(Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
11)
(String -> ShowS
showString String
"MkModP " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> a -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
11 a
x ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> ShowS
showString String
modStr)
where
modStr :: String
modStr = String
" (mod " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> Nat -> String
forall a. Show a => a -> String
show Nat
p' String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
")"
p' :: Nat
p' = forall (n :: Nat) (proxy :: Nat -> Type).
KnownNat n =>
proxy n -> Nat
natVal @p Proxy p
forall {k} (t :: k). Proxy t
Proxy
{-# INLINEABLE showsPrec #-}
instance HasField "unModP" (ModP p a) a where
getField :: ModP p a -> a
getField (UnsafeModP a
x) = a
x
instance
( k ~ A_Getter,
x ~ a,
y ~ a
) =>
LabelOptic "unModP" k (ModP p a) (ModP p a) x y
where
labelOptic :: Optic k NoIx (ModP p a) (ModP p a) x y
labelOptic = (ModP p a -> x) -> Getter (ModP p a) x
forall s a. (s -> a) -> Getter s a
to (\(UnsafeModP a
x) -> x
a
x)
{-# INLINE labelOptic #-}
instance
( AnyUpperBounded a,
Integral a,
KnownNat p,
Typeable a
) =>
Bounded (ModP p a)
where
minBound :: ModP p a
minBound = a -> ModP p a
forall (p :: Nat) a.
(AnyUpperBounded a, HasCallStack, Integral a, KnownNat p,
Typeable a) =>
a -> ModP p a
unsafeModP a
0
maxBound :: ModP p a
maxBound = a -> ModP p a
forall (p :: Nat) a.
(AnyUpperBounded a, HasCallStack, Integral a, KnownNat p,
Typeable a) =>
a -> ModP p a
unsafeModP (a -> ModP p a) -> a -> ModP p a
forall a b. (a -> b) -> a -> b
$ Nat -> a
forall a b. (Integral a, Num b) => a -> b
fromIntegral (forall (n :: Nat) (proxy :: Nat -> Type).
KnownNat n =>
proxy n -> Nat
natVal @p Proxy p
forall {k} (t :: k). Proxy t
Proxy Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
- Nat
1)
{-# INLINEABLE minBound #-}
{-# INLINEABLE maxBound #-}
instance (KnownNat p, Show a) => Display (ModP p a) where
displayBuilder :: ModP p a -> Builder
displayBuilder (UnsafeModP a
x) =
[Builder] -> Builder
forall a. Monoid a => [a] -> a
mconcat
[ String -> Builder
forall a. Display a => a -> Builder
displayBuilder (String -> Builder) -> String -> Builder
forall a b. (a -> b) -> a -> b
$ a -> String
forall a. Show a => a -> String
show a
x,
forall a. Display a => a -> Builder
displayBuilder @String String
" (mod ",
String -> Builder
forall a. Display a => a -> Builder
displayBuilder (String -> Builder) -> String -> Builder
forall a b. (a -> b) -> a -> b
$ Nat -> String
forall a. Show a => a -> String
show Nat
p',
forall a. Display a => a -> Builder
displayBuilder @String String
")"
]
where
p' :: Nat
p' = forall (n :: Nat) (proxy :: Nat -> Type).
KnownNat n =>
proxy n -> Nat
natVal @p Proxy p
forall {k} (t :: k). Proxy t
Proxy
instance
( AnyUpperBounded a,
Integral a,
KnownNat p
) =>
ASemigroup (ModP p a)
where
UnsafeModP a
x .+. :: ModP p a -> ModP p a -> ModP p a
.+. UnsafeModP a
y =
a -> ModP p a
forall (p :: Nat) a. a -> ModP p a
UnsafeModP (a -> ModP p a) -> a -> ModP p a
forall a b. (a -> b) -> a -> b
$ a -> a -> a -> a
forall a. (AnyUpperBounded a, Integral a) => a -> a -> a -> a
Utils.modSafeAdd a
x a
y (Nat -> a
forall a b. (Integral a, Num b) => a -> b
fromIntegral Nat
p')
where
p' :: Nat
p' = forall (n :: Nat) (proxy :: Nat -> Type).
KnownNat n =>
proxy n -> Nat
natVal @p Proxy p
forall {k} (t :: k). Proxy t
Proxy
{-# INLINEABLE (.+.) #-}
instance
( AnyUpperBounded a,
Integral a,
KnownNat p,
Typeable a
) =>
AMonoid (ModP p a)
where
zero :: ModP p a
zero = a -> ModP p a
forall (p :: Nat) a.
(AnyUpperBounded a, HasCallStack, Integral a, KnownNat p,
Typeable a) =>
a -> ModP p a
unsafeModP a
0
{-# INLINEABLE zero #-}
instance
( AnyLowerBounded a,
AnyUpperBounded a,
Integral a,
KnownNat p,
Typeable a
) =>
AGroup (ModP p a)
where
UnsafeModP a
x .-. :: ModP p a -> ModP p a -> ModP p a
.-. UnsafeModP a
y =
a -> ModP p a
forall (p :: Nat) a. a -> ModP p a
UnsafeModP (a -> ModP p a) -> a -> ModP p a
forall a b. (a -> b) -> a -> b
$ a -> a -> a -> a
forall a. (AnyLowerBounded a, Integral a) => a -> a -> a -> a
Utils.modSafeSub a
x a
y (Nat -> a
forall a b. (Integral a, Num b) => a -> b
fromIntegral Nat
p')
where
p' :: Nat
p' = forall (n :: Nat) (proxy :: Nat -> Type).
KnownNat n =>
proxy n -> Nat
natVal @p Proxy p
forall {k} (t :: k). Proxy t
Proxy
{-# INLINEABLE (.-.) #-}
instance
( AnyUpperBounded a,
Integral a,
KnownNat p
) =>
MSemigroup (ModP p a)
where
UnsafeModP a
x .*. :: ModP p a -> ModP p a -> ModP p a
.*. UnsafeModP a
y =
a -> ModP p a
forall (p :: Nat) a. a -> ModP p a
UnsafeModP (a -> ModP p a) -> a -> ModP p a
forall a b. (a -> b) -> a -> b
$ a -> a -> a -> a
forall a. (AnyUpperBounded a, Integral a) => a -> a -> a -> a
Utils.modSafeMult a
x a
y (Nat -> a
forall a b. (Integral a, Num b) => a -> b
fromIntegral Nat
p')
where
p' :: Nat
p' = forall (n :: Nat) (proxy :: Nat -> Type).
KnownNat n =>
proxy n -> Nat
natVal @p Proxy p
forall {k} (t :: k). Proxy t
Proxy
{-# INLINEABLE (.*.) #-}
instance
( AnyUpperBounded a,
Integral a,
KnownNat p,
Typeable a
) =>
MMonoid (ModP p a)
where
one :: ModP p a
one = a -> ModP p a
forall (p :: Nat) a.
(AnyUpperBounded a, HasCallStack, Integral a, KnownNat p,
Typeable a) =>
a -> ModP p a
unsafeModP a
1
{-# INLINEABLE one #-}
instance
( AnyUpperBounded a,
Integral a,
KnownNat p,
Typeable a
) =>
MGroup (ModP p a)
where
ModP p a
x .%. :: ModP p a -> ModP p a -> ModP p a
.%. ModP p a
d = ModP p a
x ModP p a -> ModP p a -> ModP p a
forall s. MSemigroup s => s -> s -> s
.*. ModP p a -> ModP p a
forall (p :: Nat) a.
(Integral a, KnownNat p) =>
ModP p a -> ModP p a
invert ModP p a
d
{-# INLINEABLE (.%.) #-}
instance
( AnyUpperBounded a,
Integral a,
KnownNat p,
Typeable a
) =>
Semiring (ModP p a)
instance
( AnyLowerBounded a,
AnyUpperBounded a,
Integral a,
KnownNat p,
Typeable a
) =>
Ring (ModP p a)
instance
( AnyUpperBounded a,
Integral a,
KnownNat p,
Typeable a
) =>
Semifield (ModP p a)
instance
( AnyLowerBounded a,
AnyUpperBounded a,
Integral a,
KnownNat p,
Typeable a
) =>
Field (ModP p a)
instance
( AnyUpperBounded a,
Integral a,
KnownNat p,
Typeable a
) =>
FromInteger (ModP p a)
where
afromInteger :: HasCallStack => Integer -> ModP p a
afromInteger = a -> ModP p a
forall (p :: Nat) a.
(AnyUpperBounded a, HasCallStack, Integral a, KnownNat p,
Typeable a) =>
a -> ModP p a
unsafeModP (a -> ModP p a) -> (Integer -> a) -> Integer -> ModP p a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> a
forall a. Num a => Integer -> a
fromInteger
{-# INLINEABLE afromInteger #-}
mkModP ::
forall p a.
( AnyUpperBounded a,
Integral a,
KnownNat p,
Typeable a
) =>
a ->
Either String (ModP p a)
mkModP :: forall (p :: Nat) a.
(AnyUpperBounded a, Integral a, KnownNat p, Typeable a) =>
a -> Either String (ModP p a)
mkModP a
x = Either String (ModP p a)
-> (String -> Either String (ModP p a))
-> Maybe String
-> Either String (ModP p a)
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Either String (ModP p a)
modP String -> Either String (ModP p a)
forall a b. a -> Either a b
Left (a -> Integer -> Maybe String
forall a.
(AnyUpperBounded a, Integral a, Typeable a) =>
a -> Integer -> Maybe String
Utils.checkModBound a
x Integer
p')
where
modP :: Either String (ModP p a)
modP = case Integer -> MaybePrime
Prime.isPrime Integer
p' of
MaybePrime
Composite -> String -> Either String (ModP p a)
forall a b. a -> Either a b
Left (String -> Either String (ModP p a))
-> String -> Either String (ModP p a)
forall a b. (a -> b) -> a -> b
$ String
"Received non-prime: " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> Integer -> String
forall a. Show a => a -> String
show Integer
p'
MaybePrime
ProbablyPrime -> ModP p a -> Either String (ModP p a)
forall a b. b -> Either a b
Right (ModP p a -> Either String (ModP p a))
-> ModP p a -> Either String (ModP p a)
forall a b. (a -> b) -> a -> b
$ a -> ModP p a
forall (p :: Nat) a. a -> ModP p a
UnsafeModP a
x'
p' :: Integer
p' = Nat -> Integer
forall a. Integral a => a -> Integer
toInteger (Nat -> Integer) -> Nat -> Integer
forall a b. (a -> b) -> a -> b
$ forall (n :: Nat) (proxy :: Nat -> Type).
KnownNat n =>
proxy n -> Nat
natVal @p Proxy p
forall {k} (t :: k). Proxy t
Proxy
x' :: a
x' = a
x a -> a -> a
forall a. Integral a => a -> a -> a
`mod` Integer -> a
forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
p'
{-# INLINEABLE mkModP #-}
unsafeModP ::
forall p a.
( AnyUpperBounded a,
HasCallStack,
Integral a,
KnownNat p,
Typeable a
) =>
a ->
ModP p a
unsafeModP :: forall (p :: Nat) a.
(AnyUpperBounded a, HasCallStack, Integral a, KnownNat p,
Typeable a) =>
a -> ModP p a
unsafeModP a
x = case a -> Either String (ModP p a)
forall (p :: Nat) a.
(AnyUpperBounded a, Integral a, KnownNat p, Typeable a) =>
a -> Either String (ModP p a)
mkModP a
x of
Right ModP p a
mp -> ModP p a
mp
Left String
err -> String -> ModP p a
forall a. HasCallStack => String -> a
error (String -> ModP p a) -> String -> ModP p a
forall a b. (a -> b) -> a -> b
$ String -> ShowS
Prime.errMsg String
"unsafeModP" String
err
{-# INLINEABLE unsafeModP #-}
invert :: forall p a. (Integral a, KnownNat p) => ModP p a -> ModP p a
invert :: forall (p :: Nat) a.
(Integral a, KnownNat p) =>
ModP p a -> ModP p a
invert (UnsafeModP a
d) =
a -> ModP p a
forall (p :: Nat) a. (Integral a, KnownNat p) => a -> ModP p a
reallyUnsafeModP (a -> ModP p a) -> a -> ModP p a
forall a b. (a -> b) -> a -> b
$ Nat -> a
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Nat -> a) -> Nat -> a
forall a b. (a -> b) -> a -> b
$ forall (p :: Nat). KnownNat p => Nat -> Nat
Prime.invert @p (a -> Nat
forall a b. (Integral a, Num b) => a -> b
fromIntegral a
d)
{-# INLINEABLE invert #-}
reallyUnsafeModP :: forall p a. (Integral a, KnownNat p) => a -> ModP p a
reallyUnsafeModP :: forall (p :: Nat) a. (Integral a, KnownNat p) => a -> ModP p a
reallyUnsafeModP = a -> ModP p a
forall (p :: Nat) a. a -> ModP p a
UnsafeModP (a -> ModP p a) -> (a -> a) -> a -> ModP p a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> a -> a
forall a. Integral a => a -> a -> a
`mod` a
p')
where
p' :: a
p' = Nat -> a
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Nat -> a) -> Nat -> a
forall a b. (a -> b) -> a -> b
$ forall (n :: Nat) (proxy :: Nat -> Type).
KnownNat n =>
proxy n -> Nat
natVal @p Proxy p
forall {k} (t :: k). Proxy t
Proxy
{-# INLINEABLE reallyUnsafeModP #-}