{-# OPTIONS_HADDOCK hide, prune, ignore-exports #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE UndecidableSuperClasses #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE MagicHash #-}
{-# LANGUAGE NoStarIsType #-}
module Math.NumberTheory.Padic.Types where
import Data.Ratio
import Data.Maybe (isJust, maybeToList)
import Data.Mod
import Data.Word
import GHC.TypeLits hiding (Mod)
import Data.Constraint (Constraint)
import GHC.Integer (smallInteger)
import GHC.Integer.Logarithms ( integerLogBase# )
type family ValidRadix (m :: Nat) :: Constraint where
ValidRadix 0 = TypeError ('Text "Zero radix!")
ValidRadix 1 = TypeError ('Text "Radix should be more then 1!")
ValidRadix m = ()
type KnownRadix m = ( ValidRadix m , KnownNat m )
type family LiftedRadix p prec where
LiftedRadix p prec = p ^ (2*prec + 1)
type family Radix p prec :: Constraint where
Radix p prec =
( KnownNat prec
, KnownRadix p
, KnownRadix (LiftedRadix p prec)
)
type family SufficientPrecision num (p :: Nat) :: Nat where
SufficientPrecision Word32 2 = 64
SufficientPrecision Word32 3 = 43
SufficientPrecision Word32 5 = 30
SufficientPrecision Word32 6 = 26
SufficientPrecision Word32 7 = 24
SufficientPrecision Word8 p = Div (SufficientPrecision Word32 p) 4
SufficientPrecision Word16 p = Div (SufficientPrecision Word32 p) 2
SufficientPrecision Word64 p = 2 * (SufficientPrecision Word32 p) + 1
SufficientPrecision Int p = 2 * SufficientPrecision Word32 p
SufficientPrecision Word p = SufficientPrecision Word64 p
SufficientPrecision (Ratio t) p = SufficientPrecision t p
SufficientPrecision t p = Div (SufficientPrecision t 2) (Log2 p)
type family Padic num (p :: Nat)
class (Eq n, Num n) => PadicNum n where
type Unit n
type Digit n
precision :: Integral i => n -> i
radix :: Integral i => n -> i
fromDigits :: [Digit n] -> n
digits :: n -> [Digit n]
lifted :: n -> Integer
mkUnit :: Integer -> n
fromUnit :: (Unit n, Int) -> n
splitUnit :: n -> (Unit n, Int)
isInvertible :: n -> Bool
inverse :: n -> Maybe n
firstDigit :: PadicNum n => n -> Digit n
{-# INLINE firstDigit #-}
firstDigit :: n -> Digit n
firstDigit = [Digit n] -> Digit n
forall a. [a] -> a
head ([Digit n] -> Digit n) -> (n -> [Digit n]) -> n -> Digit n
forall b c a. (b -> c) -> (a -> b) -> a -> c
. n -> [Digit n]
forall n. PadicNum n => n -> [Digit n]
digits
reduce :: (KnownRadix p, PadicNum n) => n -> Mod p
reduce :: n -> Mod p
reduce = Integer -> Mod p
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Integer -> Mod p) -> (n -> Integer) -> n -> Mod p
forall b c a. (b -> c) -> (a -> b) -> a -> c
. n -> Integer
forall n. PadicNum n => n -> Integer
lifted
unit :: PadicNum n => n -> Unit n
{-# INLINE unit #-}
unit :: n -> Unit n
unit = (Unit n, Int) -> Unit n
forall a b. (a, b) -> a
fst ((Unit n, Int) -> Unit n) -> (n -> (Unit n, Int)) -> n -> Unit n
forall b c a. (b -> c) -> (a -> b) -> a -> c
. n -> (Unit n, Int)
forall n. PadicNum n => n -> (Unit n, Int)
splitUnit
valuation :: PadicNum n => n -> Int
{-# INLINE valuation #-}
valuation :: n -> Int
valuation = (Unit n, Int) -> Int
forall a b. (a, b) -> b
snd ((Unit n, Int) -> Int) -> (n -> (Unit n, Int)) -> n -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. n -> (Unit n, Int)
forall n. PadicNum n => n -> (Unit n, Int)
splitUnit
norm :: (Integral i, PadicNum n) => n -> Ratio i
{-# INLINE norm #-}
norm :: n -> Ratio i
norm n
n = (n -> i
forall n i. (PadicNum n, Integral i) => n -> i
radix n
n i -> i -> Ratio i
forall a. Integral a => a -> a -> Ratio a
% i
1) Ratio i -> Int -> Ratio i
forall a b. (Fractional a, Integral b) => a -> b -> a
^^ (-n -> Int
forall n. PadicNum n => n -> Int
valuation n
n)
normalize :: PadicNum n => n -> n
normalize :: n -> n
normalize = (Unit n, Int) -> n
forall n. PadicNum n => (Unit n, Int) -> n
fromUnit ((Unit n, Int) -> n) -> (n -> (Unit n, Int)) -> n -> n
forall b c a. (b -> c) -> (a -> b) -> a -> c
. n -> (Unit n, Int)
forall n. PadicNum n => n -> (Unit n, Int)
splitUnit
isZero :: PadicNum n => n -> Bool
{-# INLINE isZero #-}
isZero :: n -> Bool
isZero n
n = n -> Int
forall n. PadicNum n => n -> Int
valuation n
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= n -> Int
forall n i. (PadicNum n, Integral i) => n -> i
precision n
n
liftedRadix :: (PadicNum n, Integral a) => n -> a
{-# INLINE liftedRadix #-}
liftedRadix :: n -> a
liftedRadix n
n = n -> a
forall n i. (PadicNum n, Integral i) => n -> i
radix n
n a -> Integer -> a
forall a b. (Num a, Integral b) => a -> b -> a
^ (Integer
2Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
*n -> Integer
forall n i. (PadicNum n, Integral i) => n -> i
precision n
n Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
1)
sufficientPrecision :: Integral a => Integer -> a -> Integer
sufficientPrecision :: Integer -> a -> Integer
sufficientPrecision Integer
p a
m = Integer -> Integer -> Integer
forall a b. (Integral a, Integral b) => a -> a -> b
ilog Integer
p (Integer
2 Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* a -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral a
m) Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
2
ilog :: (Integral a, Integral b) => a -> a -> b
ilog :: a -> a -> b
ilog a
a a
b =
Integer -> b
forall a. Num a => Integer -> a
fromInteger (Integer -> b) -> Integer -> b
forall a b. (a -> b) -> a -> b
$ Int# -> Integer
smallInteger (Integer -> Integer -> Int#
integerLogBase# (a -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral a
a) (a -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral a
b))
instance KnownRadix p => PadicNum (Mod p) where
type Unit (Mod p) = Mod p
type Digit (Mod p) = Mod p
radix :: Mod p -> i
radix = Integer -> i
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Integer -> i) -> (Mod p -> Integer) -> Mod p -> i
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Mod p -> Integer
forall (n :: Nat) (proxy :: Nat -> Type).
KnownNat n =>
proxy n -> Integer
natVal
precision :: Mod p -> i
precision Mod p
_ = Int -> i
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int
forall a. Bounded a => a
maxBound :: Int)
digits :: Mod p -> [Digit (Mod p)]
digits = Mod p -> [Digit (Mod p)]
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure
fromDigits :: [Digit (Mod p)] -> Mod p
fromDigits = [Digit (Mod p)] -> Mod p
forall a. [a] -> a
head
lifted :: Mod p -> Integer
lifted = Natural -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Natural -> Integer) -> (Mod p -> Natural) -> Mod p -> Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Mod p -> Natural
forall (m :: Nat). Mod m -> Natural
unMod
mkUnit :: Integer -> Mod p
mkUnit = Integer -> Mod p
forall a. Num a => Integer -> a
fromInteger
inverse :: Mod p -> Maybe (Mod p)
inverse = Mod p -> Maybe (Mod p)
forall (m :: Nat). KnownNat m => Mod m -> Maybe (Mod m)
invertMod
isInvertible :: Mod p -> Bool
isInvertible = Maybe (Mod p) -> Bool
forall a. Maybe a -> Bool
isJust (Maybe (Mod p) -> Bool)
-> (Mod p -> Maybe (Mod p)) -> Mod p -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Mod p -> Maybe (Mod p)
forall (m :: Nat). KnownNat m => Mod m -> Maybe (Mod m)
invertMod
fromUnit :: (Unit (Mod p), Int) -> Mod p
fromUnit (Unit (Mod p)
u, Int
0) = Mod p
Unit (Mod p)
u
fromUnit (Unit (Mod p), Int)
_ = Mod p
0
splitUnit :: Mod p -> (Unit (Mod p), Int)
splitUnit Mod p
u = (Mod p
Unit (Mod p)
u, Int
0)