import Data.Ratio
import Data.List (find)
import GHC.TypeLits
import Padic

pSqrt :: KnownNat p => Rational -> Padic p
pSqrt r = res 
  where
    res = maybe Null mkUnit series 
    (a, b) = (numerator r, denominator r)
    series = case modulo res of

      2 | eqMod 4 a 3 -> Nothing
        | not (eqMod 8 a 1) -> Nothing
        | otherwise -> Just $ 1: 0: go 8 1
        where
          go pk x =
            let q = ((b*x*x - a) `div` pk) `mod` 2
            in q: go (2*pk) (x + q * (pk `div` 2))

      p -> do
        y <- find (\x -> eqMod p (b*x*x) a) [1..p-1]
        df <- recipMod p (2*b*y)
        let go pk x =
              let f = (b*x*x - a) `div` pk
                  d = (f * (p - df)) `mod` p
              in x `div` (pk `div` p): go (p*pk) (x + d*pk)
        Just $ go p y

eqMod :: Integral a => a -> a -> a -> Bool
eqMod p a b = a `mod` p == b `mod` p