{-# LANGUAGE RebindableSyntax #-}
module Number.ResidueClass.Check where

import qualified Number.ResidueClass as Res

import qualified Algebra.PrincipalIdealDomain as PID
import qualified Algebra.IntegralDomain as Integral
import qualified Algebra.Field          as Field
import qualified Algebra.Ring           as Ring
import qualified Algebra.Additive       as Additive
import qualified Algebra.ZeroTestable   as ZeroTestable

import Algebra.ZeroTestable(isZero)

import qualified Data.Function.HT as Func
import Data.Maybe.HT (toMaybe, )
import Text.Show.HT (showsInfixPrec, )
import Text.Read.HT (readsInfixPrec, )

import NumericPrelude.Base
import NumericPrelude.Numeric (Int, Integer, mod, (*), )


infix 7 /:, `Cons`

{- |
The best solution seems to let 'modulus' be part of the type.
This could happen with a phantom type for modulus
and a @run@ function like 'Control.Monad.ST.runST'.
Then operations with non-matching moduli could be detected at compile time
and 'zero' and 'one' could be generated with the correct modulus.
An alternative trial can be found in module ResidueClassMaybe.
-}
data T a
  = Cons {T a -> a
modulus        :: !a
         ,T a -> a
representative :: !a
         }

factorPrec :: Int
factorPrec :: Int
factorPrec = String -> Int
forall a. Read a => String -> a
read String
"7"

instance (Show a) => Show (T a) where
   showsPrec :: Int -> T a -> ShowS
showsPrec Int
prec (Cons a
m a
r) = String -> Int -> Int -> a -> a -> ShowS
forall a b.
(Show a, Show b) =>
String -> Int -> Int -> a -> b -> ShowS
showsInfixPrec String
"/:" Int
factorPrec Int
prec a
r a
m

instance (Read a, Integral.C a) => Read (T a) where
   readsPrec :: Int -> ReadS (T a)
readsPrec Int
prec = String -> Int -> Int -> (a -> a -> T a) -> ReadS (T a)
forall a b c.
(Read a, Read b) =>
String -> Int -> Int -> (a -> b -> c) -> ReadS c
readsInfixPrec String
"/:" Int
factorPrec Int
prec a -> a -> T a
forall a. C a => a -> a -> T a
(/:)


-- | @r \/: m@ is the residue class containing @r@ with respect to the modulus @m@
(/:) :: (Integral.C a) => a -> a -> T a
/: :: a -> a -> T a
(/:) a
r a
m = a -> a -> T a
forall a. a -> a -> T a
Cons a
m (a -> a -> a
forall a. C a => a -> a -> a
mod a
r a
m)

-- | Check if two residue classes share the same modulus
isCompatible :: (Eq a) => T a -> T a -> Bool
isCompatible :: T a -> T a -> Bool
isCompatible T a
x T a
y  =  T a -> a
forall a. T a -> a
modulus T a
x a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== T a -> a
forall a. T a -> a
modulus T a
y

maybeCompatible :: (Eq a) => T a -> T a -> Maybe a
maybeCompatible :: T a -> T a -> Maybe a
maybeCompatible T a
x T a
y =
   let mx :: a
mx = T a -> a
forall a. T a -> a
modulus T a
x
       my :: a
my = T a -> a
forall a. T a -> a
modulus T a
y
   in  Bool -> a -> Maybe a
forall a. Bool -> a -> Maybe a
toMaybe (a
mxa -> a -> Bool
forall a. Eq a => a -> a -> Bool
==a
my) a
mx


fromRepresentative :: (Integral.C a) => a -> a -> T a
fromRepresentative :: a -> a -> T a
fromRepresentative a
m a
x = a -> a -> T a
forall a. a -> a -> T a
Cons a
m (a -> a -> a
forall a. C a => a -> a -> a
mod a
x a
m)

lift1 :: (Eq a) => (a -> a -> a) -> T a -> T a
lift1 :: (a -> a -> a) -> T a -> T a
lift1 a -> a -> a
f T a
x =
   let m :: a
m = T a -> a
forall a. T a -> a
modulus T a
x
   in  a -> a -> T a
forall a. a -> a -> T a
Cons a
m (a -> a -> a
f a
m (T a -> a
forall a. T a -> a
representative T a
x))

lift2 :: (Eq a) => (a -> a -> a -> a) -> T a -> T a -> T a
lift2 :: (a -> a -> a -> a) -> T a -> T a -> T a
lift2 a -> a -> a -> a
f T a
x T a
y =
   T a -> (a -> T a) -> Maybe a -> T a
forall b a. b -> (a -> b) -> Maybe a -> b
maybe
      (T a
forall a. a
errIncompat)
      (\a
m -> a -> a -> T a
forall a. a -> a -> T a
Cons a
m (a -> a -> a -> a
f (T a -> a
forall a. T a -> a
modulus T a
x) (T a -> a
forall a. T a -> a
representative T a
x) (T a -> a
forall a. T a -> a
representative T a
y)))
      (T a -> T a -> Maybe a
forall a. Eq a => T a -> T a -> Maybe a
maybeCompatible T a
x T a
y)

errIncompat :: a
errIncompat :: a
errIncompat = String -> a
forall a. HasCallStack => String -> a
error String
"Residue class: Incompatible operands"


zero :: (Additive.C a) => a -> T a
zero :: a -> T a
zero a
m = a -> a -> T a
forall a. a -> a -> T a
Cons a
m a
forall a. C a => a
Additive.zero

one :: (Ring.C a) => a -> T a
one :: a -> T a
one  a
m = a -> a -> T a
forall a. a -> a -> T a
Cons a
m a
forall a. C a => a
Ring.one

fromInteger :: (Integral.C a) => a -> Integer -> T a
fromInteger :: a -> Integer -> T a
fromInteger a
m Integer
x = a -> a -> T a
forall a. C a => a -> a -> T a
fromRepresentative a
m (Integer -> a
forall a. C a => Integer -> a
Ring.fromInteger Integer
x)



instance  (Eq a) => Eq (T a)  where
    == :: T a -> T a -> Bool
(==) T a
x T a
y  =
        Bool -> (a -> Bool) -> Maybe a -> Bool
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
forall a. a
errIncompat
           (Bool -> a -> Bool
forall a b. a -> b -> a
const (T a -> a
forall a. T a -> a
representative T a
x a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== T a -> a
forall a. T a -> a
representative T a
y))
           (T a -> T a -> Maybe a
forall a. Eq a => T a -> T a -> Maybe a
maybeCompatible T a
x T a
y)

instance  (ZeroTestable.C a) => ZeroTestable.C (T a)  where
    isZero :: T a -> Bool
isZero (Cons a
_ a
r)   =  a -> Bool
forall a. C a => a -> Bool
isZero a
r

instance  (Eq a, Integral.C a) => Additive.C (T a)  where
    zero :: T a
zero                =  String -> T a
forall a. HasCallStack => String -> a
error String
"no generic zero in a residue class, use ResidueClass.zero"
    + :: T a -> T a -> T a
(+)                 =  (a -> a -> a -> a) -> T a -> T a -> T a
forall a. Eq a => (a -> a -> a -> a) -> T a -> T a -> T a
lift2 a -> a -> a -> a
forall a. C a => a -> a -> a -> a
Res.add
    (-)                 =  (a -> a -> a -> a) -> T a -> T a -> T a
forall a. Eq a => (a -> a -> a -> a) -> T a -> T a -> T a
lift2 a -> a -> a -> a
forall a. C a => a -> a -> a -> a
Res.sub
    negate :: T a -> T a
negate              =  (a -> a -> a) -> T a -> T a
forall a. Eq a => (a -> a -> a) -> T a -> T a
lift1 a -> a -> a
forall a. C a => a -> a -> a
Res.neg

instance  (Eq a, Integral.C a) => Ring.C (T a)  where
    one :: T a
one                 =  String -> T a
forall a. HasCallStack => String -> a
error String
"no generic one in a residue class, use ResidueClass.one"
    * :: T a -> T a -> T a
(*)                 =  (a -> a -> a -> a) -> T a -> T a -> T a
forall a. Eq a => (a -> a -> a -> a) -> T a -> T a -> T a
lift2 a -> a -> a -> a
forall a. C a => a -> a -> a -> a
Res.mul
    fromInteger :: Integer -> T a
fromInteger         =  String -> Integer -> T a
forall a. HasCallStack => String -> a
error String
"no generic integer in a residue class, use ResidueClass.fromInteger"
    T a
x^ :: T a -> Integer -> T a
^Integer
n                 =  (T a -> T a -> T a) -> T a -> T a -> Integer -> T a
forall a. (a -> a -> a) -> a -> a -> Integer -> a
Func.powerAssociative T a -> T a -> T a
forall a. C a => a -> a -> a
(*) (a -> T a
forall a. C a => a -> T a
one (T a -> a
forall a. T a -> a
modulus T a
x)) T a
x Integer
n

instance  (Eq a, PID.C a) => Field.C (T a)  where
    / :: T a -> T a -> T a
(/)                 =  (a -> a -> a -> a) -> T a -> T a -> T a
forall a. Eq a => (a -> a -> a -> a) -> T a -> T a -> T a
lift2 a -> a -> a -> a
forall a. C a => a -> a -> a -> a
Res.divide
    recip :: T a -> T a
recip               =  (a -> a -> a) -> T a -> T a
forall a. Eq a => (a -> a -> a) -> T a -> T a
lift1 ((a -> a -> a -> a) -> a -> a -> a -> a
forall a b c. (a -> b -> c) -> b -> a -> c
flip a -> a -> a -> a
forall a. C a => a -> a -> a -> a
Res.divide a
forall a. C a => a
Ring.one)
    fromRational' :: Rational -> T a
fromRational'       =  String -> Rational -> T a
forall a. HasCallStack => String -> a
error String
"no conversion from rational to residue class"