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

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

module Math.NumberTheory.Padic.Rational where

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

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

type instance Padic Rational p = Q' p (SufficientPrecision Word p)
type instance Padic (Ratio Int) p = Q' p (SufficientPrecision Int p)
type instance Padic (Ratio Word8) p = Q' p (SufficientPrecision Word8 p)
type instance Padic (Ratio Word16) p = Q' p (SufficientPrecision Word16 p)
type instance Padic (Ratio Word32) p = Q' p (SufficientPrecision Word32 p)
type instance Padic (Ratio Word64) p = Q' p (SufficientPrecision Word64 p)
type instance Padic (Ratio Word) p = Q' p (SufficientPrecision Word64 p)

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

-- |  Rational p-adic number with explicitly specified precision.
data Q' (p :: Nat) (prec :: Nat) = Q' !(Z' p prec) !Int

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

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

  {-# INLINE  radix #-}
  radix :: Q' p prec -> i
radix (Q' Z' p prec
u Int
_) = Z' p prec -> i
forall n i. (PadicNum n, Integral i) => n -> i
radix Z' p prec
u

  {-# INLINE digits #-}
  digits :: Q' p prec -> [Digit (Q' p prec)]
digits (Q' Z' p prec
u Int
v) = Int -> Mod p -> [Mod p]
forall a. Int -> a -> [a]
replicate Int
v Mod p
0 [Mod p] -> [Mod p] -> [Mod p]
forall a. [a] -> [a] -> [a]
++ 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
u)

  {-# INLINE fromDigits #-}
  fromDigits :: [Digit (Q' p prec)] -> Q' p prec
fromDigits [Digit (Q' p prec)]
ds = Q' p prec -> Q' p prec
forall n. PadicNum n => n -> n
normalize (Q' p prec -> Q' p prec) -> Q' p prec -> Q' p prec
forall a b. (a -> b) -> a -> b
$ Z' p prec -> Int -> Q' p prec
forall (p :: Nat) (prec :: Nat). Z' p prec -> Int -> Q' p prec
Q' ([Digit (Z' p prec)] -> Z' p prec
forall n. PadicNum n => [Digit n] -> n
fromDigits [Digit (Z' p prec)]
[Digit (Q' p prec)]
ds) Int
0

  {-# INLINE lifted #-}
  lifted :: Q' p prec -> Integer
lifted (Q' Z' p prec
u Int
_) = Z' p prec -> Integer
forall n. PadicNum n => n -> Integer
lifted Z' p prec
u

  {-# INLINE mkUnit #-}
  mkUnit :: Integer -> Q' p prec
mkUnit Integer
ds = Q' p prec -> Q' p prec
forall n. PadicNum n => n -> n
normalize (Q' p prec -> Q' p prec) -> Q' p prec -> Q' p prec
forall a b. (a -> b) -> a -> b
$ Z' p prec -> Int -> Q' p prec
forall (p :: Nat) (prec :: Nat). Z' p prec -> Int -> Q' p prec
Q' (Integer -> Z' p prec
forall n. PadicNum n => Integer -> n
mkUnit Integer
ds) Int
0

  {-# INLINE fromUnit #-}
  fromUnit :: (Unit (Q' p prec), Int) -> Q' p prec
fromUnit (Unit (Q' p prec)
u, Int
v) = Z' p prec -> Int -> Q' p prec
forall (p :: Nat) (prec :: Nat). Z' p prec -> Int -> Q' p prec
Q' Unit (Q' p prec)
Z' p prec
u Int
v

  splitUnit :: Q' p prec -> (Unit (Q' p prec), Int)
splitUnit n :: Q' p prec
n@(Q' Z' p prec
u Int
v) =
    let pr :: Int
pr = Q' p prec -> Int
forall n i. (PadicNum n, Integral i) => n -> i
precision Q' p prec
n
        (Z' p prec
u', Int
v') = Z' p prec -> (Unit (Z' p prec), Int)
forall n. PadicNum n => n -> (Unit n, Int)
splitUnit Z' p prec
u
    in if Int
v Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
v' Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
pr then (Unit (Q' p prec)
0, Int
pr) else (Unit (Q' p prec)
Z' p prec
u', Int
v Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
v')     
  
  isInvertible :: Q' p prec -> Bool
isInvertible = Z' p prec -> Bool
forall n. PadicNum n => n -> Bool
isInvertible (Z' p prec -> Bool)
-> (Q' p prec -> Z' p prec) -> Q' p prec -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Q' p prec -> Z' p prec
forall n. PadicNum n => n -> Unit n
unit (Q' p prec -> Z' p prec)
-> (Q' p prec -> Q' p prec) -> Q' p prec -> Z' p prec
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Q' p prec -> Q' p prec
forall n. PadicNum n => n -> n
normalize
  
  inverse :: Q' p prec -> Maybe (Q' p prec)
inverse Q' p prec
n = do Z' p prec
r <- Z' p prec -> Maybe (Z' p prec)
forall n. PadicNum n => n -> Maybe n
inverse (Q' p prec -> Unit (Q' p prec)
forall n. PadicNum n => n -> Unit n
unit Q' p prec
n)
                 Q' p prec -> Maybe (Q' p prec)
forall (m :: * -> *) a. Monad m => a -> m a
return (Q' p prec -> Maybe (Q' p prec)) -> Q' p prec -> Maybe (Q' p prec)
forall a b. (a -> b) -> a -> b
$ (Unit (Q' p prec), Int) -> Q' p prec
forall n. PadicNum n => (Unit n, Int) -> n
fromUnit (Unit (Q' p prec)
Z' p prec
r, - Q' p prec -> Int
forall n. PadicNum n => n -> Int
valuation Q' p prec
n)

instance Radix p prec => Show (Q' p prec) where
  show :: Q' p prec -> String
show Q' p prec
n = String
si String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
sep 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
sf
    where
      (Z' p prec
u, Int
k) = Q' p prec -> (Unit (Q' p prec), Int)
forall n. PadicNum n => n -> (Unit n, Int)
splitUnit (Q' p prec -> Q' p prec
forall n. PadicNum n => n -> n
normalize Q' p prec
n)
      pr :: Int
pr = Q' p prec -> Int
forall n i. (PadicNum n, Integral i) => n -> i
precision Q' 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
u
      ([Mod p]
f, [Mod p]
i) =
        case Int -> Int -> Ordering
forall a. Ord a => a -> a -> Ordering
compare Int
k Int
0 of
          Ordering
EQ -> ([Mod p
0], [Mod p]
[Digit (Z' p prec)]
ds)
          Ordering
GT -> ([Mod p
0], Int -> Mod p -> [Mod p]
forall a. Int -> a -> [a]
replicate Int
k Mod p
0 [Mod p] -> [Mod p] -> [Mod p]
forall a. [a] -> [a] -> [a]
++ [Mod p]
[Digit (Z' p prec)]
ds)
          Ordering
LT -> Int -> [Mod p] -> ([Mod p], [Mod p])
forall a. Int -> [a] -> ([a], [a])
splitAt (-Int
k) ([Mod p]
[Digit (Z' p prec)]
ds [Mod p] -> [Mod p] -> [Mod p]
forall a. [a] -> [a] -> [a]
++ Int -> Mod p -> [Mod p]
forall a. Int -> a -> [a]
replicate (Int
pr Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
k) Mod p
0)
      sf :: String
sf = String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
sep ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ Mod p -> String
forall (m :: Nat). Mod m -> String
showD (Mod p -> String) -> [Mod p] -> [String]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Mod p] -> [Mod p]
forall a. [a] -> [a]
reverse [Mod p]
f
      si :: String
si =
        case Int -> [Mod p] -> Maybe ([Mod p], [Mod p])
forall a. Eq a => Int -> [a] -> Maybe ([a], [a])
findCycle Int
pr [Mod p]
i of
          Maybe ([Mod p], [Mod p])
Nothing
            | [Mod p] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Mod p]
i -> String
"0"
            | [Mod p] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Mod p]
i 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]
i)
            | Bool
otherwise -> [Mod p] -> String
toString [Mod p]
i
          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)
      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
        | Q' p prec -> Integer
forall n i. (PadicNum n, Integral i) => n -> i
radix Q' p prec
n Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
11 = String
""
        | Bool
otherwise = String
" "
    
instance Radix p prec => Eq (Q' p prec) where
  Q' p prec
a' == :: Q' p prec -> Q' p prec -> Bool
== Q' p prec
b' =
    (Q' p prec -> Bool
forall n. PadicNum n => n -> Bool
isZero Q' p prec
a Bool -> Bool -> Bool
&& Q' p prec -> Bool
forall n. PadicNum n => n -> Bool
isZero Q' p prec
b)
    Bool -> Bool -> Bool
|| (Q' p prec -> Int
forall n. PadicNum n => n -> Int
valuation Q' p prec
a Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Q' p prec -> Int
forall n. PadicNum n => n -> Int
valuation Q' p prec
b Bool -> Bool -> Bool
&& Q' p prec -> Unit (Q' p prec)
forall n. PadicNum n => n -> Unit n
unit Q' p prec
a Z' p prec -> Z' p prec -> Bool
forall a. Eq a => a -> a -> Bool
== Q' p prec -> Unit (Q' p prec)
forall n. PadicNum n => n -> Unit n
unit Q' p prec
b)
    where
      a :: Q' p prec
a = Q' p prec -> Q' p prec
forall n. PadicNum n => n -> n
normalize Q' p prec
a'
      b :: Q' p prec
b = Q' p prec -> Q' p prec
forall n. PadicNum n => n -> n
normalize Q' p prec
b'

instance Radix p prec => Ord (Q' p prec) where
  compare :: Q' p prec -> Q' p prec -> Ordering
compare = String -> Q' p prec -> Q' p prec -> Ordering
forall a. HasCallStack => String -> a
error String
"Order is nor defined for p-adics."

instance Radix p prec => Num (Q' p prec) where
  fromInteger :: Integer -> Q' p prec
fromInteger Integer
n = Q' p prec -> Q' p prec
forall n. PadicNum n => n -> n
normalize (Q' p prec -> Q' p prec) -> Q' p prec -> Q' p prec
forall a b. (a -> b) -> a -> b
$ Z' p prec -> Int -> Q' p prec
forall (p :: Nat) (prec :: Nat). Z' p prec -> Int -> Q' p prec
Q' (Integer -> Z' p prec
forall a. Num a => Integer -> a
fromInteger Integer
n) Int
0
          
  x :: Q' p prec
x@(Q' (Z' (R Mod (LiftedRadix p prec)
a)) Int
va) + :: Q' p prec -> Q' p prec -> Q' p prec
+ Q' (Z' (R Mod (LiftedRadix p prec)
b)) Int
vb =
    case Int -> Int -> Ordering
forall a. Ord a => a -> a -> Ordering
compare Int
va Int
vb of
      Ordering
LT -> Z' p prec -> Int -> Q' p prec
forall (p :: Nat) (prec :: Nat). Z' p prec -> Int -> Q' p prec
Q' (R prec p -> Z' p prec
forall (p :: Nat) (prec :: Nat). R prec p -> Z' p prec
Z' (Mod (LiftedRadix p prec) -> R prec p
forall (prec :: Nat) (p :: Nat).
Mod (LiftedRadix p prec) -> R prec p
R (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))
p Mod (p ^ ((2 * prec) + 1)) -> Int -> Mod (p ^ ((2 * prec) + 1))
forall (m :: Nat) a.
(KnownNat m, Integral a) =>
Mod m -> a -> Mod m
^% (Int
vb Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
va) 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))) Int
va
      Ordering
EQ -> Z' p prec -> Int -> Q' p prec
forall (p :: Nat) (prec :: Nat). Z' p prec -> Int -> Q' p prec
Q' (R prec p -> Z' p prec
forall (p :: Nat) (prec :: Nat). R prec p -> Z' p prec
Z' (Mod (LiftedRadix p prec) -> R prec p
forall (prec :: Nat) (p :: Nat).
Mod (LiftedRadix p prec) -> R prec p
R (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))) Int
va
      Ordering
GT -> Z' p prec -> Int -> Q' p prec
forall (p :: Nat) (prec :: Nat). Z' p prec -> Int -> Q' p prec
Q' (R prec p -> Z' p prec
forall (p :: Nat) (prec :: Nat). R prec p -> Z' p prec
Z' (Mod (LiftedRadix p prec) -> R prec p
forall (prec :: Nat) (p :: Nat).
Mod (LiftedRadix p prec) -> R prec p
R (Mod (p ^ ((2 * prec) + 1))
p Mod (p ^ ((2 * prec) + 1)) -> Int -> Mod (p ^ ((2 * prec) + 1))
forall (m :: Nat) a.
(KnownNat m, Integral a) =>
Mod m -> a -> Mod m
^% (Int
va Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
vb) 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)
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))) Int
vb
    where
      p :: Mod (p ^ ((2 * prec) + 1))
p = Integer -> Mod (p ^ ((2 * prec) + 1))
forall a. Num a => Integer -> a
fromInteger (Q' p prec -> Integer
forall n i. (PadicNum n, Integral i) => n -> i
radix Q' p prec
x)
      
  Q' (Z' (R Mod (LiftedRadix p prec)
a)) Int
va * :: Q' p prec -> Q' p prec -> Q' p prec
* Q' (Z' (R Mod (LiftedRadix p prec)
b)) Int
vb = Z' p prec -> Int -> Q' p prec
forall (p :: Nat) (prec :: Nat). Z' p prec -> Int -> Q' p prec
Q' (R prec p -> Z' p prec
forall (p :: Nat) (prec :: Nat). R prec p -> Z' p prec
Z' (Mod (LiftedRadix p prec) -> R prec p
forall (prec :: Nat) (p :: Nat).
Mod (LiftedRadix p prec) -> R prec p
R (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))) (Int
va Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
vb)
      
  negate :: Q' p prec -> Q' p prec
negate (Q' Z' p prec
u Int
v) = Z' p prec -> Int -> Q' p prec
forall (p :: Nat) (prec :: Nat). Z' p prec -> Int -> Q' p prec
Q' (Z' p prec -> Z' p prec
forall a. Num a => a -> a
negate Z' p prec
u) Int
v
  abs :: Q' p prec -> Q' p prec
abs = Rational -> Q' p prec
forall a. Fractional a => Rational -> a
fromRational (Rational -> Q' p prec)
-> (Q' p prec -> Rational) -> Q' p prec -> Q' p prec
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Q' p prec -> Rational
forall i n. (Integral i, PadicNum n) => n -> Ratio i
norm
  signum :: Q' p prec -> Q' p prec
signum = Q' p prec -> Q' p prec
forall n (p :: Nat).
(PadicNum n, KnownRadix p, Digit n ~ Mod p) =>
n -> n
pSignum

newtype Delay prec p = Delay (Q' p prec)

instance Radix p prec => Fractional (Q' p prec) where
  fromRational :: Rational -> Q' p prec
fromRational Rational
0 = Q' p prec
0
  fromRational Rational
x = Q' p prec
res
    where
      res :: Q' p prec
res = Z' p prec -> Int -> Q' p prec
forall (p :: Nat) (prec :: Nat). Z' p prec -> Int -> Q' p prec
Q' (Z' p prec
n Z' p prec -> Z' p prec -> Z' p prec
forall a. Integral a => a -> a -> a
`div` Z' p prec
d) Int
v
      p :: Integer
p = Integer -> Integer
forall a. Num a => Integer -> a
fromInteger (Integer -> Integer) -> Integer -> Integer
forall a b. (a -> b) -> a -> b
$ Delay prec p -> Integer
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
natVal (Q' p prec -> Delay prec p
forall (prec :: Nat) (p :: Nat). Q' p prec -> Delay prec p
Delay Q' p prec
res)
      (Rational
q, Int
v) = Integer -> Rational -> (Rational, Int)
forall p. Integral p => p -> Ratio p -> (Ratio p, Int)
getUnitQ Integer
p Rational
x
      (Z' p prec
n, Z' p prec
d) = (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
$ Rational -> Integer
forall a. Ratio a -> a
numerator Rational
q, 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
$ Rational -> Integer
forall a. Ratio a -> a
denominator Rational
q)
  Q' p prec
a / :: Q' p prec -> Q' p prec -> Q' p prec
/ Q' p prec
b = Z' p prec -> Int -> Q' p prec
forall (p :: Nat) (prec :: Nat). Z' p prec -> Int -> Q' p prec
Q' Z' p prec
u (Int
v Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Q' p prec -> Int
forall n. PadicNum n => n -> Int
valuation Q' p prec
a Int -> Int -> Int
forall a. Num a => a -> a -> a
- Q' p prec -> Int
forall n. PadicNum n => n -> Int
valuation Q' p prec
b')
    where
      b' :: Q' p prec
b' = Q' p prec -> Q' p prec
forall n. PadicNum n => n -> n
normalize Q' p prec
b
      Q' Z' p prec
u Int
v = Rational -> Q' p prec
forall a. Fractional a => Rational -> a
fromRational (Q' p prec -> Integer
forall n. PadicNum n => n -> Integer
lifted Q' p prec
a Integer -> Integer -> Rational
forall a. Integral a => a -> a -> Ratio a
% Q' p prec -> Integer
forall n. PadicNum n => n -> Integer
lifted Q' p prec
b')

instance Radix p prec => Real (Q' p prec) where
  toRational :: Q' p prec -> Rational
toRational Q' p prec
n = Z' p prec -> Rational
forall a. Real a => a -> Rational
toRational (Q' p prec -> Unit (Q' p prec)
forall n. PadicNum n => n -> Unit n
unit Q' p prec
n) Rational -> Rational -> Rational
forall a. Fractional a => a -> a -> a
/ Q' p prec -> Rational
forall i n. (Integral i, PadicNum n) => n -> Ratio i
norm Q' p prec
n

pUndefinedError :: String -> a
pUndefinedError String
s = String -> a
forall a. HasCallStack => String -> a
error (String -> a) -> String -> a
forall a b. (a -> b) -> a -> b
$ String
s String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" is undifined for p-adics."

fromEither :: Either String c -> c
fromEither = (String -> c) -> (c -> c) -> Either String c -> c
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either String -> c
forall a. HasCallStack => String -> a
error c -> c
forall a. a -> a
id

instance Radix p prec => Floating (Q' p prec) where
  Q' p prec
x ** :: Q' p prec -> Q' p prec -> Q' p prec
** Q' p prec
y = Either String (Q' p prec) -> Q' p prec
forall c. Either String c -> c
fromEither (Either String (Q' p prec) -> Q' p prec)
-> Either String (Q' p prec) -> Q' p prec
forall a b. (a -> b) -> a -> b
$ Q' p prec -> Q' p prec -> Either String (Q' p prec)
forall p. (PadicNum p, Fractional p) => p -> p -> Either String p
pPow Q' p prec
x Q' p prec
y
  exp :: Q' p prec -> Q' p prec
exp = Either String (Q' p prec) -> Q' p prec
forall c. Either String c -> c
fromEither (Either String (Q' p prec) -> Q' p prec)
-> (Q' p prec -> Either String (Q' p prec))
-> Q' p prec
-> Q' p prec
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Q' p prec -> Either String (Q' p prec)
forall n. (Eq n, PadicNum n, Fractional n) => n -> Either String n
pExp
  log :: Q' p prec -> Q' p prec
log = Either String (Q' p prec) -> Q' p prec
forall c. Either String c -> c
fromEither (Either String (Q' p prec) -> Q' p prec)
-> (Q' p prec -> Either String (Q' p prec))
-> Q' p prec
-> Q' p prec
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Q' p prec -> Either String (Q' p prec)
forall n. (Eq n, PadicNum n, Fractional n) => n -> Either String n
pLog
  sinh :: Q' p prec -> Q' p prec
sinh = Either String (Q' p prec) -> Q' p prec
forall c. Either String c -> c
fromEither (Either String (Q' p prec) -> Q' p prec)
-> (Q' p prec -> Either String (Q' p prec))
-> Q' p prec
-> Q' p prec
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Q' p prec -> Either String (Q' p prec)
forall b. (PadicNum b, Fractional b) => b -> Either String b
pSinh
  cosh :: Q' p prec -> Q' p prec
cosh = Either String (Q' p prec) -> Q' p prec
forall c. Either String c -> c
fromEither (Either String (Q' p prec) -> Q' p prec)
-> (Q' p prec -> Either String (Q' p prec))
-> Q' p prec
-> Q' p prec
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Q' p prec -> Either String (Q' p prec)
forall b. (PadicNum b, Fractional b) => b -> Either String b
pCosh
  sin :: Q' p prec -> Q' p prec
sin = Either String (Q' p prec) -> Q' p prec
forall c. Either String c -> c
fromEither (Either String (Q' p prec) -> Q' p prec)
-> (Q' p prec -> Either String (Q' p prec))
-> Q' p prec
-> Q' p prec
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Q' p prec -> Either String (Q' p prec)
forall b. (PadicNum b, Fractional b) => b -> Either String b
pSin
  cos :: Q' p prec -> Q' p prec
cos = Either String (Q' p prec) -> Q' p prec
forall c. Either String c -> c
fromEither (Either String (Q' p prec) -> Q' p prec)
-> (Q' p prec -> Either String (Q' p prec))
-> Q' p prec
-> Q' p prec
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Q' p prec -> Either String (Q' p prec)
forall b. (PadicNum b, Fractional b) => b -> Either String b
pCos
  asinh :: Q' p prec -> Q' p prec
asinh = Either String (Q' p prec) -> Q' p prec
forall c. Either String c -> c
fromEither (Either String (Q' p prec) -> Q' p prec)
-> (Q' p prec -> Either String (Q' p prec))
-> Q' p prec
-> Q' p prec
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Q' p prec -> Either String (Q' p prec)
forall b. (PadicNum b, Fractional b) => b -> Either String b
pAsinh
  acosh :: Q' p prec -> Q' p prec
acosh = Either String (Q' p prec) -> Q' p prec
forall c. Either String c -> c
fromEither (Either String (Q' p prec) -> Q' p prec)
-> (Q' p prec -> Either String (Q' p prec))
-> Q' p prec
-> Q' p prec
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Q' p prec -> Either String (Q' p prec)
forall b. (PadicNum b, Fractional b) => b -> Either String b
pCosh
  atanh :: Q' p prec -> Q' p prec
atanh = Either String (Q' p prec) -> Q' p prec
forall c. Either String c -> c
fromEither (Either String (Q' p prec) -> Q' p prec)
-> (Q' p prec -> Either String (Q' p prec))
-> Q' p prec
-> Q' p prec
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Q' p prec -> Either String (Q' p prec)
forall b. (Fractional b, PadicNum b) => b -> Either String b
pTanh
  asin :: Q' p prec -> Q' p prec
asin = Either String (Q' p prec) -> Q' p prec
forall c. Either String c -> c
fromEither (Either String (Q' p prec) -> Q' p prec)
-> (Q' p prec -> Either String (Q' p prec))
-> Q' p prec
-> Q' p prec
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Q' p prec -> Either String (Q' p prec)
forall b. (Fractional b, PadicNum b) => b -> Either String b
pAsin
  sqrt :: Q' p prec -> Q' p prec
sqrt Q' p prec
x = case Q' p prec -> [Q' p prec]
forall n (p :: Nat).
(Fractional n, PadicNum n, KnownRadix p, Digit n ~ Mod p) =>
n -> [n]
pSqrt Q' p prec
x of
    Q' p prec
res:[Q' p prec]
_ -> Q' p prec
res
    [] -> String -> Q' p prec
forall a. HasCallStack => String -> a
error (String -> Q' p prec) -> String -> Q' p prec
forall a b. (a -> b) -> a -> b
$ String
"sqrt: digit " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Mod p -> String
forall a. Show a => a -> String
show (Q' p prec -> Digit (Q' p prec)
forall n. PadicNum n => n -> Digit n
firstDigit Q' p prec
x) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" is not a square residue!"
  pi :: Q' p prec
pi = String -> Q' p prec
forall a. String -> a
pUndefinedError String
"pi"
  acos :: Q' p prec -> Q' p prec
acos = String -> Q' p prec -> Q' p prec
forall a. String -> a
pUndefinedError String
"acos"
  atan :: Q' p prec -> Q' p prec
atan = String -> Q' p prec -> Q' p prec
forall a. String -> a
pUndefinedError String
"atan"