{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}

{- | Quotient rings for eulidean domains.

   See @Algebra.Ring.Polynomial.Quotient@ in @halg-polynomial@
   for an ideal quotient rings of polynomial ring.
-}
module Algebra.Ring.Euclidean.Quotient
  ( Quotient (),
    representative,
    withQuotient,
    reifyQuotient,
    reifyIdealQuotient,
    withIdealQuotient,
    quotient,
    quotientBy,
  )
where

import Algebra.Ring.Ideal
import Algebra.Ring.Polynomial.Class
import AlgebraicPrelude
import Data.Coerce (coerce)
import Data.Kind (Type)
import Data.Proxy
import Data.Reflection
import Numeric.Ring.Class as NA

newtype Quotient r a = Quotient {Quotient r a -> a
runQuotient :: a}
  deriving (Quotient r a -> Quotient r a -> Bool
(Quotient r a -> Quotient r a -> Bool)
-> (Quotient r a -> Quotient r a -> Bool) -> Eq (Quotient r a)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall k (r :: k) a. Eq a => Quotient r a -> Quotient r a -> Bool
/= :: Quotient r a -> Quotient r a -> Bool
$c/= :: forall k (r :: k) a. Eq a => Quotient r a -> Quotient r a -> Bool
== :: Quotient r a -> Quotient r a -> Bool
$c== :: forall k (r :: k) a. Eq a => Quotient r a -> Quotient r a -> Bool
Eq, Eq (Quotient r a)
Eq (Quotient r a)
-> (Quotient r a -> Quotient r a -> Ordering)
-> (Quotient r a -> Quotient r a -> Bool)
-> (Quotient r a -> Quotient r a -> Bool)
-> (Quotient r a -> Quotient r a -> Bool)
-> (Quotient r a -> Quotient r a -> Bool)
-> (Quotient r a -> Quotient r a -> Quotient r a)
-> (Quotient r a -> Quotient r a -> Quotient r a)
-> Ord (Quotient r a)
Quotient r a -> Quotient r a -> Bool
Quotient r a -> Quotient r a -> Ordering
Quotient r a -> Quotient r a -> Quotient r a
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall k (r :: k) a. Ord a => Eq (Quotient r a)
forall k (r :: k) a. Ord a => Quotient r a -> Quotient r a -> Bool
forall k (r :: k) a.
Ord a =>
Quotient r a -> Quotient r a -> Ordering
forall k (r :: k) a.
Ord a =>
Quotient r a -> Quotient r a -> Quotient r a
min :: Quotient r a -> Quotient r a -> Quotient r a
$cmin :: forall k (r :: k) a.
Ord a =>
Quotient r a -> Quotient r a -> Quotient r a
max :: Quotient r a -> Quotient r a -> Quotient r a
$cmax :: forall k (r :: k) a.
Ord a =>
Quotient r a -> Quotient r a -> Quotient r a
>= :: Quotient r a -> Quotient r a -> Bool
$c>= :: forall k (r :: k) a. Ord a => Quotient r a -> Quotient r a -> Bool
> :: Quotient r a -> Quotient r a -> Bool
$c> :: forall k (r :: k) a. Ord a => Quotient r a -> Quotient r a -> Bool
<= :: Quotient r a -> Quotient r a -> Bool
$c<= :: forall k (r :: k) a. Ord a => Quotient r a -> Quotient r a -> Bool
< :: Quotient r a -> Quotient r a -> Bool
$c< :: forall k (r :: k) a. Ord a => Quotient r a -> Quotient r a -> Bool
compare :: Quotient r a -> Quotient r a -> Ordering
$ccompare :: forall k (r :: k) a.
Ord a =>
Quotient r a -> Quotient r a -> Ordering
$cp1Ord :: forall k (r :: k) a. Ord a => Eq (Quotient r a)
Ord)

representative :: Quotient r a -> a
representative :: Quotient r a -> a
representative = Quotient r a -> a
forall k (r :: k) a. Quotient r a -> a
runQuotient

instance (Show a, Reifies r a) => Show (Quotient r a) where
  showsPrec :: Int -> Quotient r a -> ShowS
showsPrec Int
d (Quotient a
a) =
    Bool -> ShowS -> ShowS
showParen (Int
d Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
10) (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$
      Int -> a -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
11 a
a ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> ShowS
showString String
" (mod "
        ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> a -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
11 (Proxy r -> a
forall k (s :: k) a (proxy :: k -> *). Reifies s a => proxy s -> a
reflect (Proxy r
forall k (t :: k). Proxy t
Proxy :: Proxy r))
        ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Char -> ShowS
showChar Char
')'

instance (Show a, Reifies r a, DecidableZero a) => PrettyCoeff (Quotient r a) where
  showsCoeff :: Int -> Quotient r a -> ShowSCoeff
showsCoeff Int
_ (Quotient a
a)
    | a -> Bool
forall r. DecidableZero r => r -> Bool
isZero a
a = ShowSCoeff
Vanished
    | Bool
otherwise =
      ShowS -> ShowSCoeff
Positive (ShowS -> ShowSCoeff) -> ShowS -> ShowSCoeff
forall a b. (a -> b) -> a -> b
$
        Bool -> ShowS -> ShowS
showParen Bool
True (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$
          Bool -> ShowS -> ShowS
showParen Bool
True (a -> ShowS
forall a. Show a => a -> ShowS
shows a
a) ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> ShowS
showString String
" + " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> a -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
11 (Proxy r -> a
forall k (s :: k) a (proxy :: k -> *). Reifies s a => proxy s -> a
reflect (Proxy r
forall k (t :: k). Proxy t
Proxy :: Proxy r))

liftBin ::
  forall r a.
  (Reifies r a, Euclidean a) =>
  (a -> a -> a) ->
  Quotient r a ->
  Quotient r a ->
  Quotient r a
{-# INLINE liftBin #-}
liftBin :: (a -> a -> a) -> Quotient r a -> Quotient r a -> Quotient r a
liftBin = ((a -> Quotient r a
forall k (r :: k) a.
(Reifies r a, Euclidean a) =>
a -> Quotient r a
quotient (a -> Quotient r a)
-> (Quotient r a -> a) -> Quotient r a -> Quotient r a
forall b c a. (b -> c) -> (a -> b) -> a -> c
.) ((Quotient r a -> a) -> Quotient r a -> Quotient r a)
-> (Quotient r a -> Quotient r a -> a)
-> Quotient r a
-> Quotient r a
-> Quotient r a
forall b c a. (b -> c) -> (a -> b) -> a -> c
.) ((Quotient r a -> Quotient r a -> a)
 -> Quotient r a -> Quotient r a -> Quotient r a)
-> ((a -> a -> a) -> Quotient r a -> Quotient r a -> a)
-> (a -> a -> a)
-> Quotient r a
-> Quotient r a
-> Quotient r a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> a -> a) -> Quotient r a -> Quotient r a -> a
coerce

liftUnary ::
  forall r a.
  (Reifies r a, Euclidean a) =>
  (a -> a) ->
  Quotient r a ->
  Quotient r a
{-# INLINE liftUnary #-}
liftUnary :: (a -> a) -> Quotient r a -> Quotient r a
liftUnary = (a -> Quotient r a
forall k (r :: k) a.
(Reifies r a, Euclidean a) =>
a -> Quotient r a
quotient (a -> Quotient r a)
-> (Quotient r a -> a) -> Quotient r a -> Quotient r a
forall b c a. (b -> c) -> (a -> b) -> a -> c
.) ((Quotient r a -> a) -> Quotient r a -> Quotient r a)
-> ((a -> a) -> Quotient r a -> a)
-> (a -> a)
-> Quotient r a
-> Quotient r a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> a) -> Quotient r a -> a
coerce

quotient ::
  forall r a.
  (Reifies r a, Euclidean a) =>
  a ->
  Quotient r a
quotient :: a -> Quotient r a
quotient = a -> Quotient r a
forall k (r :: k) a. a -> Quotient r a
Quotient (a -> Quotient r a) -> (a -> a) -> a -> Quotient r a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> a -> a
forall a. Euclidean a => a -> a -> a
rem' (Proxy r -> a
forall k (s :: k) a (proxy :: k -> *). Reifies s a => proxy s -> a
reflect (Proxy r
forall k (t :: k). Proxy t
Proxy :: Proxy r))

quotientBy ::
  forall r a proxy.
  (Reifies r a, Euclidean a) =>
  proxy r ->
  a ->
  Quotient r a
quotientBy :: proxy r -> a -> Quotient r a
quotientBy = (a -> Quotient r a) -> proxy r -> a -> Quotient r a
forall a b. a -> b -> a
const a -> Quotient r a
forall k (r :: k) a.
(Reifies r a, Euclidean a) =>
a -> Quotient r a
quotient

rem' :: Euclidean a => a -> a -> a
{-# INLINE rem' #-}
rem' :: a -> a -> a
rem' a
a
  | a -> Bool
forall r. DecidableZero r => r -> Bool
isZero a
a = a -> a
forall a. a -> a
id
  | Bool
otherwise = (a -> a -> a
forall a. Euclidean a => a -> a -> a
`rem` a
a)

instance (Euclidean a, Reifies r a) => DecidableZero (Quotient r a) where
  isZero :: Quotient r a -> Bool
isZero (Quotient a
r) = a -> Bool
forall r. DecidableZero r => r -> Bool
isZero a
r

instance (Euclidean a, Reifies r a) => Additive (Quotient r a) where
  + :: Quotient r a -> Quotient r a -> Quotient r a
(+) = (a -> a -> a) -> Quotient r a -> Quotient r a -> Quotient r a
forall k (r :: k) a.
(Reifies r a, Euclidean a) =>
(a -> a -> a) -> Quotient r a -> Quotient r a -> Quotient r a
liftBin a -> a -> a
forall r. Additive r => r -> r -> r
(+)
  {-# INLINE (+) #-}

instance
  (Euclidean a, LeftModule c a, Reifies r a) =>
  LeftModule c (Quotient r a)
  where
  .* :: c -> Quotient r a -> Quotient r a
(.*) = \c
n -> (a -> a) -> Quotient r a -> Quotient r a
forall k (r :: k) a.
(Reifies r a, Euclidean a) =>
(a -> a) -> Quotient r a -> Quotient r a
liftUnary (c
n c -> a -> a
forall r m. LeftModule r m => r -> m -> m
.*)
  {-# INLINE (.*) #-}

instance
  (Euclidean a, RightModule c a, Reifies r a) =>
  RightModule c (Quotient r a)
  where
  *. :: Quotient r a -> c -> Quotient r a
(*.) = \Quotient r a
p c
n -> (a -> a) -> Quotient r a -> Quotient r a
forall k (r :: k) a.
(Reifies r a, Euclidean a) =>
(a -> a) -> Quotient r a -> Quotient r a
liftUnary (a -> c -> a
forall r m. RightModule r m => m -> r -> m
*. c
n) Quotient r a
p
  {-# INLINE (*.) #-}

instance
  (Euclidean a, Reifies r a) =>
  Monoidal (Quotient r a)
  where
  zero :: Quotient r a
zero = a -> Quotient r a
forall k (r :: k) a. a -> Quotient r a
Quotient a
forall m. Monoidal m => m
zero
  {-# INLINE zero #-}
  sumWith :: (a -> Quotient r a) -> f a -> Quotient r a
sumWith a -> Quotient r a
f = (Quotient r a -> a -> Quotient r a)
-> Quotient r a -> f a -> Quotient r a
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' (\Quotient r a
a a
b -> Quotient r a
a Quotient r a -> Quotient r a -> Quotient r a
forall r. Additive r => r -> r -> r
+ a -> Quotient r a
f a
b) Quotient r a
forall m. Monoidal m => m
zero
  {-# INLINE sumWith #-}

instance
  (Euclidean a, Reifies r a) =>
  Abelian (Quotient r a)

instance
  (Euclidean a, Reifies r a) =>
  Multiplicative (Quotient r a)
  where
  * :: Quotient r a -> Quotient r a -> Quotient r a
(*) = (a -> a -> a) -> Quotient r a -> Quotient r a -> Quotient r a
forall k (r :: k) a.
(Reifies r a, Euclidean a) =>
(a -> a -> a) -> Quotient r a -> Quotient r a -> Quotient r a
liftBin a -> a -> a
forall r. Multiplicative r => r -> r -> r
(*)
  {-# INLINE (*) #-}

instance
  (Euclidean a, Reifies r a) =>
  Unital (Quotient r a)
  where
  one :: Quotient r a
one = a -> Quotient r a
forall k (r :: k) a.
(Reifies r a, Euclidean a) =>
a -> Quotient r a
quotient a
forall r. Unital r => r
one
  {-# INLINE one #-}
  productWith :: (a -> Quotient r a) -> f a -> Quotient r a
productWith a -> Quotient r a
f = (Quotient r a -> a -> Quotient r a)
-> Quotient r a -> f a -> Quotient r a
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' (\Quotient r a
a a
b -> Quotient r a
a Quotient r a -> Quotient r a -> Quotient r a
forall r. Multiplicative r => r -> r -> r
* a -> Quotient r a
f a
b) Quotient r a
forall r. Unital r => r
one
  {-# INLINE productWith #-}

instance
  (Euclidean a, Reifies r a) =>
  Commutative (Quotient r a)

instance
  (Euclidean a, Reifies r a) =>
  Semiring (Quotient r a)

instance
  (Euclidean a, Reifies r a) =>
  Group (Quotient r a)
  where
  (-) = (a -> a -> a) -> Quotient r a -> Quotient r a -> Quotient r a
forall k (r :: k) a.
(Reifies r a, Euclidean a) =>
(a -> a -> a) -> Quotient r a -> Quotient r a -> Quotient r a
liftBin (-)
  {-# INLINE (-) #-}
  negate :: Quotient r a -> Quotient r a
negate = (a -> a) -> Quotient r a -> Quotient r a
forall k (r :: k) a.
(Reifies r a, Euclidean a) =>
(a -> a) -> Quotient r a -> Quotient r a
liftUnary a -> a
forall r. Group r => r -> r
negate
  {-# INLINE negate #-}
  subtract :: Quotient r a -> Quotient r a -> Quotient r a
subtract = (a -> a -> a) -> Quotient r a -> Quotient r a -> Quotient r a
forall k (r :: k) a.
(Reifies r a, Euclidean a) =>
(a -> a -> a) -> Quotient r a -> Quotient r a -> Quotient r a
liftBin a -> a -> a
forall r. Group r => r -> r -> r
subtract
  {-# INLINE subtract #-}

instance
  (Euclidean a, Reifies r a) =>
  Rig (Quotient r a)
  where
  fromNatural :: Natural -> Quotient r a
fromNatural = a -> Quotient r a
forall k (r :: k) a.
(Reifies r a, Euclidean a) =>
a -> Quotient r a
quotient (a -> Quotient r a) -> (Natural -> a) -> Natural -> Quotient r a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Natural -> a
forall r. Rig r => Natural -> r
fromNatural
  {-# INLINE fromNatural #-}

instance
  (Euclidean a, Reifies r a) =>
  Ring (Quotient r a)
  where
  fromInteger :: Integer -> Quotient r a
fromInteger = a -> Quotient r a
forall k (r :: k) a.
(Reifies r a, Euclidean a) =>
a -> Quotient r a
quotient (a -> Quotient r a) -> (Integer -> a) -> Integer -> Quotient r a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> a
forall r. Ring r => Integer -> r
NA.fromInteger
  {-# INLINE fromInteger #-}

instance
  (Euclidean a, Reifies r a) =>
  DecidableUnits (Quotient r a)
  where
  recipUnit :: Quotient r a -> Maybe (Quotient r a)
recipUnit = \(Quotient a
i) -> do
    Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> Maybe ()) -> Bool -> Maybe ()
forall a b. (a -> b) -> a -> b
$ Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ a -> Bool
forall r. DecidableZero r => r -> Bool
isZero a
i
    let p :: a
p = Proxy r -> a
forall k (s :: k) a (proxy :: k -> *). Reifies s a => proxy s -> a
reflect (Proxy r
forall k (t :: k). Proxy t
Proxy :: Proxy r)
        (a
u, a
_, a
x) = a -> a -> (a, a, a)
forall d. PID d => d -> d -> (d, d, d)
egcd a
p a
i
    a -> Quotient r a
forall k (r :: k) a.
(Reifies r a, Euclidean a) =>
a -> Quotient r a
quotient (a -> Quotient r a) -> (a -> a) -> a -> Quotient r a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> a -> a
forall r. Multiplicative r => r -> r -> r
* a
x) (a -> Quotient r a) -> Maybe a -> Maybe (Quotient r a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> Maybe a
forall r. DecidableUnits r => r -> Maybe r
recipUnit a
u
  {-# INLINE recipUnit #-}

instance
  (Euclidean a, Reifies r a) =>
  DecidableAssociates (Quotient r a)
  where
  isAssociate :: Quotient r a -> Quotient r a -> Bool
isAssociate (Quotient a
f) (Quotient a
g) =
    case a -> a -> [(a, a, a)]
forall r. Euclidean r => r -> r -> [(r, r, r)]
prs a
f a
g of
      (a
x, a
a, a
b) : [(a, a, a)]
_
        | a -> Bool
forall r. DecidableZero r => r -> Bool
isZero (a
x a -> a -> a
forall a. Euclidean a => a -> a -> a
`rem` Proxy r -> a
forall k (s :: k) a (proxy :: k -> *). Reifies s a => proxy s -> a
reflect (Proxy r
forall k (t :: k). Proxy t
Proxy :: Proxy r)) ->
          a -> a -> Bool
chkUnits a
a a
b
      (a
x, a
s', a
t') : (a
r, a
s, a
t) : [(a, a, a)]
_
        | a -> Bool
forall r. DecidableZero r => r -> Bool
isZero ((a
x a -> a -> a
forall a. Euclidean a => a -> a -> a
`rem` Proxy r -> a
forall k (s :: k) a (proxy :: k -> *). Reifies s a => proxy s -> a
reflect (Proxy r
forall k (t :: k). Proxy t
Proxy :: Proxy r)) a -> a -> a
forall r. Group r => r -> r -> r
- a
forall r. Unital r => r
one) ->
          a -> a -> Bool
chkUnits (a
s a -> a -> a
forall r. Group r => r -> r -> r
- a
r a -> a -> a
forall r. Multiplicative r => r -> r -> r
* a
s') (a
t a -> a -> a
forall r. Group r => r -> r -> r
- a
r a -> a -> a
forall r. Multiplicative r => r -> r -> r
* a
t')
      [(a, a, a)]
_ -> Bool
False
    where
      chkUnits :: a -> a -> Bool
chkUnits a
a a
b =
        Quotient r a -> Bool
forall r. DecidableUnits r => r -> Bool
isUnit (a -> Quotient r a
forall k (r :: k) a.
(Reifies r a, Euclidean a) =>
a -> Quotient r a
quotient a
a :: Quotient r a)
          Bool -> Bool -> Bool
&& Quotient r a -> Bool
forall r. DecidableUnits r => r -> Bool
isUnit (a -> Quotient r a
forall k (r :: k) a.
(Reifies r a, Euclidean a) =>
a -> Quotient r a
quotient a
b :: Quotient r a)

withQuotient ::
  forall a.
  (Euclidean a) =>
  a ->
  (forall (r :: Type). Reifies r a => Quotient r a) ->
  a
{-# INLINE withQuotient #-}
withQuotient :: a -> (forall r. Reifies r a => Quotient r a) -> a
withQuotient a
q forall r. Reifies r a => Quotient r a
a =
  a -> (forall s. Reifies s a => Proxy s -> a) -> a
forall a r. a -> (forall s. Reifies s a => Proxy s -> r) -> r
reify a
q ((forall s. Reifies s a => Proxy s -> a) -> a)
-> (forall s. Reifies s a => Proxy s -> a) -> a
forall a b. (a -> b) -> a -> b
$ \(Proxy s
Proxy :: Proxy r) ->
    Quotient s a -> a
forall k (r :: k) a. Quotient r a -> a
runQuotient (Quotient s a
forall r. Reifies r a => Quotient r a
a :: Quotient r a)

withIdealQuotient ::
  Euclidean a =>
  Ideal a ->
  (forall (r :: Type). Reifies r a => Quotient r a) ->
  a
{-# INLINE withIdealQuotient #-}
withIdealQuotient :: Ideal a -> (forall r. Reifies r a => Quotient r a) -> a
withIdealQuotient Ideal a
is = a -> (forall r. Reifies r a => Quotient r a) -> a
forall a.
Euclidean a =>
a -> (forall r. Reifies r a => Quotient r a) -> a
withQuotient ((a -> a -> a) -> a -> Ideal a -> a
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' a -> a -> a
forall d. GCDDomain d => d -> d -> d
gcd a
forall r. Unital r => r
one Ideal a
is)

reifyQuotient ::
  forall a r.
  (Euclidean a) =>
  a ->
  (forall (s :: Type). Reifies s a => Proxy s -> r) ->
  r
reifyQuotient :: a -> (forall s. Reifies s a => Proxy s -> r) -> r
reifyQuotient = a -> (forall s. Reifies s a => Proxy s -> r) -> r
forall a r. a -> (forall s. Reifies s a => Proxy s -> r) -> r
reify

reifyIdealQuotient ::
  forall a r.
  (Euclidean a) =>
  Ideal a ->
  (forall (s :: Type). Reifies s a => Proxy s -> r) ->
  r
reifyIdealQuotient :: Ideal a -> (forall s. Reifies s a => Proxy s -> r) -> r
reifyIdealQuotient Ideal a
is = a -> (forall s. Reifies s a => Proxy s -> r) -> r
forall a r. a -> (forall s. Reifies s a => Proxy s -> r) -> r
reify ((a -> a -> a) -> a -> Ideal a -> a
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' a -> a -> a
forall d. GCDDomain d => d -> d -> d
gcd a
forall r. Unital r => r
one Ideal a
is)