{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -Wno-identities #-}

-- See the note on Modulus for why this warning is disabled

-- | Internal module for 'ModP'.
--
-- @since 0.1
module Numeric.Data.ModP.Internal
  ( -- * Type
    ModP (MkModP, ..),

    -- ** Functions
    mkModP,
    unsafeModP,
    invert,
    reallyUnsafeModP,

    -- ** Misc
    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)

-- $setup
-- >>> import Data.Int (Int8)

-- see NOTE: [Safe finite modular rounding]

-- | Newtype wrapper that represents \( \mathbb{Z}/p\mathbb{Z} \) for prime @p@.
-- 'ModP' is a 'Numeric.Algebra.Field.Field' i.e. supports addition,
-- subtraction, multiplication, and division.
--
-- When constructing a @'ModP' p a@ we must verify that @p@ is prime and the
-- type @a@ is large enough to accommodate @p@, hence the possible failure.
--
-- ==== __Examples__
--
-- >>> import Data.Text.Display (display)
-- >>> display $ unsafeModP @7 10
-- "3 (mod 7)"
--
-- @since 0.1
type ModP :: Nat -> Type -> Type
newtype ModP p a = UnsafeModP a
  deriving stock
    ( -- | @since 0.1
      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,
      -- | @since 0.1
      (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,
      -- | @since 0.1
      (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,
      -- | @since 0.1
      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
    ( -- | @since 0.1
      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,
      -- | @since 0.1
      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,
      -- | @since 0.1
      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
    )

-- | Unidirectional pattern synonym for 'ModP'. This allows us to pattern
-- match on a modp term without exposing the unsafe internal details.
--
-- @since 0.1
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 #-}

-- | @since 0.1
instance (KnownNat p, Show a) => Show (ModP p a) where
  -- manual so we show "MkModP" instead of "UnsafeModP"
  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 #-}

-- | @since 0.1
instance HasField "unModP" (ModP p a) a where
  getField :: ModP p a -> a
getField (UnsafeModP a
x) = a
x

-- | @since 0.1
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 #-}

-- | __WARNING: Partial__
--
-- @since 0.1
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 #-}

-- | @since 0.1
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

-- | @since 0.1
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 (.+.) #-}

-- | __WARNING: Partial__
--
-- @since 0.1
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 #-}

-- | @since 0.1
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 (.-.) #-}

-- | @since 0.1
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 (.*.) #-}

-- | __WARNING: Partial__
--
-- @since 0.1
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 #-}

-- | @since 0.1
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 (.%.) #-}

-- | @since 0.1
instance
  ( AnyUpperBounded a,
    Integral a,
    KnownNat p,
    Typeable a
  ) =>
  Semiring (ModP p a)

-- | @since 0.1
instance
  ( AnyLowerBounded a,
    AnyUpperBounded a,
    Integral a,
    KnownNat p,
    Typeable a
  ) =>
  Ring (ModP p a)

-- | @since 0.1
instance
  ( AnyUpperBounded a,
    Integral a,
    KnownNat p,
    Typeable a
  ) =>
  Semifield (ModP p a)

-- | @since 0.1
instance
  ( AnyLowerBounded a,
    AnyUpperBounded a,
    Integral a,
    KnownNat p,
    Typeable a
  ) =>
  Field (ModP p a)

-- | __WARNING: Partial__
--
-- @since 0.1
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 #-}

-- | Constructor for 'ModP'. Fails if @p@ is not prime. This uses the
-- Miller-Rabin primality test, which has complexity \(O(k \log^3 p)\), and we
-- take \(k = 100\). See
-- [wikipedia](https://en.wikipedia.org/wiki/Miller-Rabin_primality_test#Complexity)
-- for more details.
--
-- ==== __Examples__
-- >>> mkModP @5 7
-- Right (MkModP 2 (mod 5))
--
-- >>> mkModP @10 7
-- Left "Received non-prime: 10"
--
-- >>> mkModP @128 (9 :: Int8)
-- Left "Type 'Int8' has a maximum size of 127. This is not large enough to safely implement mod 128."
--
-- @since 0.1
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 #-}

-- | Variant of 'mkModP' that throws an error when given a non-prime.
--
-- __WARNING: Partial__
--
-- ==== __Examples__
-- >>> unsafeModP @7 12
-- MkModP 5 (mod 7)
--
-- @since 0.1
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 #-}

-- | Given non-zero \(d\), returns the inverse i.e. finds \(e\) s.t.
--
-- \[
-- de \equiv 1 \pmod p.
-- \]
--
-- ==== __Examples__
-- findInverse
-- >>> invert $ unsafeModP @7 5
-- MkModP 3 (mod 7)
--
-- >>> invert $ unsafeModP @19 12
-- MkModP 8 (mod 19)
--
-- @since 0.1
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 #-}

-- | This function reduces the argument modulo @p@ but does __not__ check
-- that @p@ is prime. Note that the correct behavior of some functionality
-- (e.g. division) is reliant on primality, so this is dangerous. This is
-- intended only for when we absolutely know @p@ is prime and the check
-- is undesirable for performance reasons. Exercise extreme caution.
--
-- @since 0.1
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 #-}