{-# OPTIONS_HADDOCK hide, prune, ignore-exports #-}

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE FlexibleInstances #-}

module Math.NumberTheory.Padic.Integer  where

import Data.List (intercalate)
import Data.Mod
import Data.Word
import Data.Ratio
import GHC.TypeLits (Nat, natVal)
import GHC.Integer.GMP.Internals (recipModInteger)
import Math.NumberTheory.Padic.Types
import Math.NumberTheory.Padic.Analysis

------------------------------------------------------------

type instance Padic Integer p = Z' p (SufficientPrecision Word p)
type instance Padic Int p = Z' p (SufficientPrecision Int p)
type instance Padic Word8 p = Z' p (SufficientPrecision Word8 p)
type instance Padic Word16 p = Z' p (SufficientPrecision Word16 p)
type instance Padic Word32 p = Z' p (SufficientPrecision Word32 p)
type instance Padic Word64 p = Z' p (SufficientPrecision Word64 p)
type instance Padic Word p = Z' p (SufficientPrecision Word64 p)


-- |  Integer p-adic number (an element of \(\mathbb{Z}_p\)) with default precision.
type Z p = Z' p (SufficientPrecision Word32 p)

-- |  Integer p-adic number with explicitly specified precision.
newtype Z' (p :: Nat) (prec :: Nat) = Z' (R prec p)
newtype R (prec :: Nat ) (p :: Nat) = R (Mod (LiftedRadix p prec))

instance Radix p prec => Eq (Z' p prec) where
  x :: Z' p prec
x@(Z' (R Mod (LiftedRadix p prec)
a)) == :: Z' p prec -> Z' p prec -> Bool
== Z' (R Mod (LiftedRadix p prec)
b) = Mod (p ^ ((2 * prec) + 1)) -> Natural
forall (m :: Nat). Mod m -> Natural
unMod Mod (p ^ ((2 * prec) + 1))
Mod (LiftedRadix p prec)
a Natural -> Natural -> Natural
forall a. Integral a => a -> a -> a
`mod` Natural
pk Natural -> Natural -> Bool
forall a. Eq a => a -> a -> Bool
== Mod (p ^ ((2 * prec) + 1)) -> Natural
forall (m :: Nat). Mod m -> Natural
unMod Mod (p ^ ((2 * prec) + 1))
Mod (LiftedRadix p prec)
b Natural -> Natural -> Natural
forall a. Integral a => a -> a -> a
`mod` Natural
pk
    where
      pk :: Natural
pk = Z' p prec -> Natural
forall n i. (PadicNum n, Integral i) => n -> i
radix Z' p prec
x Natural -> Integer -> Natural
forall a b. (Num a, Integral b) => a -> b -> a
^ Z' p prec -> Integer
forall n i. (PadicNum n, Integral i) => n -> i
precision Z' p prec
x

instance Radix p prec => PadicNum (Z' p prec) where
  type Unit (Z' p prec) = Z' p prec
  type Digit (Z' p prec) = Mod p 

  {-# INLINE precision #-}
  precision :: Z' p prec -> i
precision = Integer -> i
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Integer -> i) -> (Z' p prec -> Integer) -> Z' p prec -> i
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Z' p prec -> Integer
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
natVal

  {-# INLINE  radix #-}
  radix :: Z' p prec -> i
radix (Z' R prec p
r) = Integer -> i
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Integer -> i) -> Integer -> i
forall a b. (a -> b) -> a -> b
$ R prec p -> Integer
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
natVal R prec p
r
  
  {-# INLINE fromDigits #-}
  fromDigits :: [Digit (Z' p prec)] -> Z' p prec
fromDigits = Integer -> Z' p prec
forall n. PadicNum n => Integer -> n
mkUnit (Integer -> Z' p prec)
-> ([Mod p] -> Integer) -> [Mod p] -> Z' p prec
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Mod p] -> Integer
forall (p :: Nat). KnownRadix p => [Mod p] -> Integer
fromRadix

  {-# INLINE digits #-}
  digits :: Z' p prec -> [Digit (Z' p prec)]
digits Z' p prec
n = Integer -> [Mod p]
forall (p :: Nat). KnownRadix p => Integer -> [Mod p]
toRadix (Z' p prec -> Integer
forall n. PadicNum n => n -> Integer
lifted Z' p prec
n)

  {-# INLINE lifted #-}
  lifted :: Z' p prec -> Integer
lifted (Z' (R Mod (LiftedRadix p prec)
n)) = Mod (p ^ ((2 * prec) + 1)) -> Integer
forall n. PadicNum n => n -> Integer
lifted Mod (p ^ ((2 * prec) + 1))
Mod (LiftedRadix p prec)
n

  {-# INLINE mkUnit #-}
  mkUnit :: Integer -> Z' p prec
mkUnit = R prec p -> Z' p prec
forall (p :: Nat) (prec :: Nat). R prec p -> Z' p prec
Z' (R prec p -> Z' p prec)
-> (Integer -> R prec p) -> Integer -> Z' p prec
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Mod (p ^ ((2 * prec) + 1)) -> R prec p
forall (prec :: Nat) (p :: Nat).
Mod (LiftedRadix p prec) -> R prec p
R (Mod (p ^ ((2 * prec) + 1)) -> R prec p)
-> (Integer -> Mod (p ^ ((2 * prec) + 1))) -> Integer -> R prec p
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> Mod (p ^ ((2 * prec) + 1))
forall a. Num a => Integer -> a
fromInteger

  {-# INLINE fromUnit #-}
  fromUnit :: (Unit (Z' p prec), Int) -> Z' p prec
fromUnit (Unit (Z' p prec)
u, Int
v) = Integer -> Z' p prec
forall n. PadicNum n => Integer -> n
mkUnit (Integer -> Z' p prec) -> Integer -> Z' p prec
forall a b. (a -> b) -> a -> b
$ Z' p prec -> Integer
forall n i. (PadicNum n, Integral i) => n -> i
radix Unit (Z' p prec)
Z' p prec
u Integer -> Integer -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
^ Int -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
v Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Z' p prec -> Integer
forall n. PadicNum n => n -> Integer
lifted Unit (Z' p prec)
Z' p prec
u

  splitUnit :: Z' p prec -> (Unit (Z' p prec), Int)
splitUnit Z' p prec
n = case Integer -> Integer -> (Integer, Int)
forall p n. (Integral p, Integral n) => p -> n -> (p, Int)
getUnitZ (Z' p prec -> Integer
forall n i. (PadicNum n, Integral i) => n -> i
radix Z' p prec
n) (Z' p prec -> Integer
forall n. PadicNum n => n -> Integer
lifted Z' p prec
n) of
                  (Integer
0, Int
0) -> (Unit (Z' p prec)
0, Z' p prec -> Int
forall n i. (PadicNum n, Integral i) => n -> i
precision Z' p prec
n)
                  (Integer
u, Int
v) -> (Integer -> Z' p prec
forall n. PadicNum n => Integer -> n
mkUnit Integer
u, Int
v)
  
  isInvertible :: Z' p prec -> Bool
isInvertible Z' p prec
n = (Z' p prec -> Integer
forall n. PadicNum n => n -> Integer
lifted Z' p prec
n Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`mod` Integer
p) Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`gcd` Integer
p Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
1
    where
      p :: Integer
p = Z' p prec -> Integer
forall n i. (PadicNum n, Integral i) => n -> i
radix Z' p prec
n
  
  inverse :: Z' p prec -> Maybe (Z' p prec)
inverse (Z' (R Mod (LiftedRadix p prec)
n))  = R prec p -> Z' p prec
forall (p :: Nat) (prec :: Nat). R prec p -> Z' p prec
Z' (R prec p -> Z' p prec)
-> (Mod (p ^ ((2 * prec) + 1)) -> R prec p)
-> Mod (p ^ ((2 * prec) + 1))
-> Z' p prec
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Mod (p ^ ((2 * prec) + 1)) -> R prec p
forall (prec :: Nat) (p :: Nat).
Mod (LiftedRadix p prec) -> R prec p
R (Mod (p ^ ((2 * prec) + 1)) -> Z' p prec)
-> Maybe (Mod (p ^ ((2 * prec) + 1))) -> Maybe (Z' p prec)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Mod (p ^ ((2 * prec) + 1)) -> Maybe (Mod (p ^ ((2 * prec) + 1)))
forall (m :: Nat). KnownNat m => Mod m -> Maybe (Mod m)
invertMod Mod (p ^ ((2 * prec) + 1))
Mod (LiftedRadix p prec)
n

instance Radix p prec => Show (Z' p prec) where
  show :: Z' p prec -> String
show Z' p prec
n = 
     case Int -> [Mod p] -> Maybe ([Mod p], [Mod p])
forall a. Eq a => Int -> [a] -> Maybe ([a], [a])
findCycle Int
pr [Mod p]
[Digit (Z' p prec)]
ds of
       Maybe ([Mod p], [Mod p])
Nothing | [Mod p] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Mod p]
[Digit (Z' p prec)]
ds Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
pr -> String
ell String -> ShowS
forall a. [a] -> [a] -> [a]
++ [Mod p] -> String
toString (Int -> [Mod p] -> [Mod p]
forall a. Int -> [a] -> [a]
take Int
pr [Mod p]
[Digit (Z' p prec)]
ds)
               | Bool
otherwise -> [Mod p] -> String
toString [Mod p]
[Digit (Z' p prec)]
ds
       Just ([],[Mod p
0]) -> String
"0"
       Just ([Mod p]
pref, [Mod p
0]) -> [Mod p] -> String
toString [Mod p]
pref
       Just ([Mod p]
pref, [Mod p]
cyc)
        | [Mod p] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Mod p]
pref Int -> Int -> Int
forall a. Num a => a -> a -> a
+ [Mod p] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Mod p]
cyc Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
pr ->
          let sp :: String
sp = [Mod p] -> String
toString [Mod p]
pref
              sc :: String
sc = [Mod p] -> String
toString [Mod p]
cyc
           in String
"(" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
sc String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
sep String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
sp
        | Bool
otherwise -> String
ell String -> ShowS
forall a. [a] -> [a] -> [a]
++ [Mod p] -> String
toString (Int -> [Mod p] -> [Mod p]
forall a. Int -> [a] -> [a]
take Int
pr ([Mod p] -> [Mod p]) -> [Mod p] -> [Mod p]
forall a b. (a -> b) -> a -> b
$ [Mod p]
pref [Mod p] -> [Mod p] -> [Mod p]
forall a. [a] -> [a] -> [a]
++ [Mod p]
cyc)
    where
      pr :: Int
pr = Z' p prec -> Int
forall n i. (PadicNum n, Integral i) => n -> i
precision Z' p prec
n
      ds :: [Digit (Z' p prec)]
ds = Z' p prec -> [Digit (Z' p prec)]
forall n. PadicNum n => n -> [Digit n]
digits Z' p prec
n
      showD :: Mod m -> String
showD = Natural -> String
forall a. Show a => a -> String
show (Natural -> String) -> (Mod m -> Natural) -> Mod m -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Mod m -> Natural
forall (m :: Nat). Mod m -> Natural
unMod
      toString :: [Mod p] -> String
toString = String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
sep ([String] -> String) -> ([Mod p] -> [String]) -> [Mod p] -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Mod p -> String) -> [Mod p] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Mod p -> String
forall (m :: Nat). Mod m -> String
showD ([Mod p] -> [String])
-> ([Mod p] -> [Mod p]) -> [Mod p] -> [String]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Mod p] -> [Mod p]
forall a. [a] -> [a]
reverse
      ell :: String
ell = String
"…" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
sep 
      sep :: String
sep
        | Z' p prec -> Integer
forall n i. (PadicNum n, Integral i) => n -> i
radix Z' p prec
n Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
11 = String
""
        | Bool
otherwise = String
" "

instance Radix p prec => Num (Z' p prec) where
  fromInteger :: Integer -> Z' p prec
fromInteger = R prec p -> Z' p prec
forall (p :: Nat) (prec :: Nat). R prec p -> Z' p prec
Z' (R prec p -> Z' p prec)
-> (Integer -> R prec p) -> Integer -> Z' p prec
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Mod (p ^ ((2 * prec) + 1)) -> R prec p
forall (prec :: Nat) (p :: Nat).
Mod (LiftedRadix p prec) -> R prec p
R (Mod (p ^ ((2 * prec) + 1)) -> R prec p)
-> (Integer -> Mod (p ^ ((2 * prec) + 1))) -> Integer -> R prec p
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> Mod (p ^ ((2 * prec) + 1))
forall a. Num a => Integer -> a
fromInteger
  Z' (R Mod (LiftedRadix p prec)
a) + :: Z' p prec -> Z' p prec -> Z' p prec
+ Z' (R Mod (LiftedRadix p prec)
b) = R prec p -> Z' p prec
forall (p :: Nat) (prec :: Nat). R prec p -> Z' p prec
Z' (R prec p -> Z' p prec)
-> (Mod (p ^ ((2 * prec) + 1)) -> R prec p)
-> Mod (p ^ ((2 * prec) + 1))
-> Z' p prec
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Mod (p ^ ((2 * prec) + 1)) -> R prec p
forall (prec :: Nat) (p :: Nat).
Mod (LiftedRadix p prec) -> R prec p
R (Mod (p ^ ((2 * prec) + 1)) -> Z' p prec)
-> Mod (p ^ ((2 * prec) + 1)) -> Z' p prec
forall a b. (a -> b) -> a -> b
$ Mod (p ^ ((2 * prec) + 1))
Mod (LiftedRadix p prec)
a Mod (p ^ ((2 * prec) + 1))
-> Mod (p ^ ((2 * prec) + 1)) -> Mod (p ^ ((2 * prec) + 1))
forall a. Num a => a -> a -> a
+ Mod (p ^ ((2 * prec) + 1))
Mod (LiftedRadix p prec)
b
  Z' (R Mod (LiftedRadix p prec)
a) - :: Z' p prec -> Z' p prec -> Z' p prec
- Z' (R Mod (LiftedRadix p prec)
b) = R prec p -> Z' p prec
forall (p :: Nat) (prec :: Nat). R prec p -> Z' p prec
Z' (R prec p -> Z' p prec)
-> (Mod (p ^ ((2 * prec) + 1)) -> R prec p)
-> Mod (p ^ ((2 * prec) + 1))
-> Z' p prec
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Mod (p ^ ((2 * prec) + 1)) -> R prec p
forall (prec :: Nat) (p :: Nat).
Mod (LiftedRadix p prec) -> R prec p
R (Mod (p ^ ((2 * prec) + 1)) -> Z' p prec)
-> Mod (p ^ ((2 * prec) + 1)) -> Z' p prec
forall a b. (a -> b) -> a -> b
$ Mod (p ^ ((2 * prec) + 1))
Mod (LiftedRadix p prec)
a Mod (p ^ ((2 * prec) + 1))
-> Mod (p ^ ((2 * prec) + 1)) -> Mod (p ^ ((2 * prec) + 1))
forall a. Num a => a -> a -> a
- Mod (p ^ ((2 * prec) + 1))
Mod (LiftedRadix p prec)
b
  Z' (R Mod (LiftedRadix p prec)
a) * :: Z' p prec -> Z' p prec -> Z' p prec
* Z' (R Mod (LiftedRadix p prec)
b) = R prec p -> Z' p prec
forall (p :: Nat) (prec :: Nat). R prec p -> Z' p prec
Z' (R prec p -> Z' p prec)
-> (Mod (p ^ ((2 * prec) + 1)) -> R prec p)
-> Mod (p ^ ((2 * prec) + 1))
-> Z' p prec
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Mod (p ^ ((2 * prec) + 1)) -> R prec p
forall (prec :: Nat) (p :: Nat).
Mod (LiftedRadix p prec) -> R prec p
R (Mod (p ^ ((2 * prec) + 1)) -> Z' p prec)
-> Mod (p ^ ((2 * prec) + 1)) -> Z' p prec
forall a b. (a -> b) -> a -> b
$ Mod (p ^ ((2 * prec) + 1))
Mod (LiftedRadix p prec)
a Mod (p ^ ((2 * prec) + 1))
-> Mod (p ^ ((2 * prec) + 1)) -> Mod (p ^ ((2 * prec) + 1))
forall a. Num a => a -> a -> a
* Mod (p ^ ((2 * prec) + 1))
Mod (LiftedRadix p prec)
b
  negate :: Z' p prec -> Z' p prec
negate (Z' (R Mod (LiftedRadix p prec)
a)) = R prec p -> Z' p prec
forall (p :: Nat) (prec :: Nat). R prec p -> Z' p prec
Z' (R prec p -> Z' p prec)
-> (Mod (p ^ ((2 * prec) + 1)) -> R prec p)
-> Mod (p ^ ((2 * prec) + 1))
-> Z' p prec
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Mod (p ^ ((2 * prec) + 1)) -> R prec p
forall (prec :: Nat) (p :: Nat).
Mod (LiftedRadix p prec) -> R prec p
R (Mod (p ^ ((2 * prec) + 1)) -> Z' p prec)
-> Mod (p ^ ((2 * prec) + 1)) -> Z' p prec
forall a b. (a -> b) -> a -> b
$ Mod (p ^ ((2 * prec) + 1)) -> Mod (p ^ ((2 * prec) + 1))
forall a. Num a => a -> a
negate Mod (p ^ ((2 * prec) + 1))
Mod (LiftedRadix p prec)
a
  abs :: Z' p prec -> Z' p prec
abs Z' p prec
x = if Z' p prec -> Int
forall n. PadicNum n => n -> Int
valuation Z' p prec
x Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0 then Z' p prec
1 else Z' p prec
0
  signum :: Z' p prec -> Z' p prec
signum = Z' p prec -> Z' p prec
forall n (p :: Nat).
(PadicNum n, KnownRadix p, Digit n ~ Mod p) =>
n -> n
pSignum

instance Radix p prec  => Enum (Z' p prec) where
  toEnum :: Int -> Z' p prec
toEnum = Int -> Z' p prec
forall a b. (Integral a, Num b) => a -> b
fromIntegral
  fromEnum :: Z' p prec -> Int
fromEnum = Integer -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Integer -> Int) -> (Z' p prec -> Integer) -> Z' p prec -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Z' p prec -> Integer
forall a. Integral a => a -> Integer
toInteger

instance Radix p prec => Real (Z' p prec) where
  toRational :: Z' p prec -> Rational
toRational Z' p prec
0 = Rational
0
  toRational Z' p prec
n = (Integer, Integer) -> Rational
forall i. Integral i => (Integer, Integer) -> Ratio i
extEuclid (Z' p prec -> Integer
forall n. PadicNum n => n -> Integer
lifted Z' p prec
n, Z' p prec -> Integer
forall n a. (PadicNum n, Integral a) => n -> a
liftedRadix Z' p prec
n)

instance Radix p prec => Integral (Z' p prec) where
  toInteger :: Z' p prec -> Integer
toInteger Z' p prec
n = if Rational -> Integer
forall a. Ratio a -> a
denominator Rational
r Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
1
                then Rational -> Integer
forall a. Ratio a -> a
numerator Rational
r
                else Z' p prec -> Integer
forall n. PadicNum n => n -> Integer
lifted Z' p prec
n Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`mod` (Z' p prec -> Integer
forall n i. (PadicNum n, Integral i) => n -> i
radix Z' p prec
n Integer -> Integer -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
^ Z' p prec -> Integer
forall n i. (PadicNum n, Integral i) => n -> i
precision Z' p prec
n)
    where
      r :: Rational
r = Z' p prec -> Rational
forall a. Real a => a -> Rational
toRational Z' p prec
n
  Z' p prec
a quotRem :: Z' p prec -> Z' p prec -> (Z' p prec, Z' p prec)
`quotRem` Z' p prec
b = case Z' p prec -> Maybe (Z' p prec)
forall n. PadicNum n => n -> Maybe n
inverse Z' p prec
b of
    Maybe (Z' p prec)
Nothing -> String -> (Z' p prec, Z' p prec)
forall a. HasCallStack => String -> a
error (String -> (Z' p prec, Z' p prec))
-> String -> (Z' p prec, Z' p prec)
forall a b. (a -> b) -> a -> b
$ Z' p prec -> String
forall a. Show a => a -> String
show Z' p prec
b String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" is not divisible modulo " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Integer -> String
forall a. Show a => a -> String
show (Z' p prec -> Integer
forall n i. (PadicNum n, Integral i) => n -> i
radix Z' p prec
a) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"!" 
    Just Z' p prec
r -> let q :: Z' p prec
q = Z' p prec
aZ' p prec -> Z' p prec -> Z' p prec
forall a. Num a => a -> a -> a
*Z' p prec
r in (Z' p prec
q, Z' p prec
a Z' p prec -> Z' p prec -> Z' p prec
forall a. Num a => a -> a -> a
- Z' p prec
q Z' p prec -> Z' p prec -> Z' p prec
forall a. Num a => a -> a -> a
* Z' p prec
b)


instance Radix p prec => Ord (Z' p prec) where
  compare :: Z' p prec -> Z' p prec -> Ordering
compare = String -> Z' p prec -> Z' p prec -> Ordering
forall a. HasCallStack => String -> a
error String
"ordering is not defined for Z"

{-| Integer power function (analog of (^) operator ) -}
zPow :: Radix p prec => Z' p prec -> Z' p prec -> Z' p prec
zPow :: Z' p prec -> Z' p prec -> Z' p prec
zPow (Z' (R Mod (LiftedRadix p prec)
a)) (Z' (R Mod (LiftedRadix p prec)
b)) = R prec p -> Z' p prec
forall (p :: Nat) (prec :: Nat). R prec p -> Z' p prec
Z' (R prec p -> Z' p prec)
-> (Mod (p ^ ((2 * prec) + 1)) -> R prec p)
-> Mod (p ^ ((2 * prec) + 1))
-> Z' p prec
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Mod (p ^ ((2 * prec) + 1)) -> R prec p
forall (prec :: Nat) (p :: Nat).
Mod (LiftedRadix p prec) -> R prec p
R (Mod (p ^ ((2 * prec) + 1)) -> Z' p prec)
-> Mod (p ^ ((2 * prec) + 1)) -> Z' p prec
forall a b. (a -> b) -> a -> b
$  Mod (p ^ ((2 * prec) + 1))
Mod (LiftedRadix p prec)
a Mod (p ^ ((2 * prec) + 1)) -> Integer -> Mod (p ^ ((2 * prec) + 1))
forall (m :: Nat) a.
(KnownNat m, Integral a) =>
Mod m -> a -> Mod m
^% Natural -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Mod (p ^ ((2 * prec) + 1)) -> Natural
forall (m :: Nat). Mod m -> Natural
unMod Mod (p ^ ((2 * prec) + 1))
Mod (LiftedRadix p prec)
b)