module ZkFold.Symbolic.GroebnerBasis.Internal.Reduction where

import           Data.Bool                                    (bool)
import           Prelude                                      hiding (Num (..), drop, lcm, length, sum, take, (!!), (/))

import           ZkFold.Base.Algebra.Basic.Class
import           ZkFold.Symbolic.GroebnerBasis.Internal.Types

reducable :: (Ord a, MultiplicativeMonoid a) => Polynom a c -> Polynom a c -> Bool
reducable :: forall a c.
(Ord a, MultiplicativeMonoid a) =>
Polynom a c -> Polynom a c -> Bool
reducable Polynom a c
l Polynom a c
r = Monom a c -> Monom a c -> Bool
forall a c.
(Ord a, MultiplicativeMonoid a) =>
Monom a c -> Monom a c -> Bool
dividable (Polynom a c -> Monom a c
forall c a. Polynom c a -> Monom c a
lt Polynom a c
l) (Polynom a c -> Monom a c
forall c a. Polynom c a -> Monom c a
lt Polynom a c
r)

reduce :: (Eq c, FiniteField c, Ord a, Ring a) =>
          Polynom a c -> Polynom a c -> Polynom a c
reduce :: forall c a.
(Eq c, FiniteField c, Ord a, Ring a) =>
Polynom a c -> Polynom a c -> Polynom a c
reduce Polynom a c
l Polynom a c
r = Polynom a c -> Polynom a c -> Polynom a c
forall c a.
(Eq c, FiniteField c, Ord a, MultiplicativeMonoid a) =>
Polynom a c -> Polynom a c -> Polynom a c
addPoly Polynom a c
l Polynom a c
r'
    where r' :: Polynom a c
r' = Polynom a c -> Monom a c -> Polynom a c
forall c a.
(FiniteField c, AdditiveMonoid a) =>
Polynom a c -> Monom a c -> Polynom a c
mulPM Polynom a c
r (Integer -> Monom a c -> Monom a c
forall b a. Scale b a => b -> a -> a
scale (-Integer
1 :: Integer) Monom a c
q)
          q :: Monom a c
q = Monom a c -> Monom a c -> Monom a c
forall c a.
(FiniteField c, Eq a, Ring a) =>
Monom a c -> Monom a c -> Monom a c
divideM (Polynom a c -> Monom a c
forall c a. Polynom c a -> Monom c a
lt Polynom a c
l) (Polynom a c -> Monom a c
forall c a. Polynom c a -> Monom c a
lt Polynom a c
r)

reduceMany :: (Eq c, FiniteField c, Ord a, Ring a) =>
              Polynom a c -> [Polynom a c] -> Polynom a c
reduceMany :: forall c a.
(Eq c, FiniteField c, Ord a, Ring a) =>
Polynom a c -> [Polynom a c] -> Polynom a c
reduceMany Polynom a c
h [Polynom a c]
fs = if Bool
reduced then Polynom a c -> [Polynom a c] -> Polynom a c
forall c a.
(Eq c, FiniteField c, Ord a, Ring a) =>
Polynom a c -> [Polynom a c] -> Polynom a c
reduceMany Polynom a c
h' [Polynom a c]
fs else Polynom a c
h'
    where (Polynom a c
h', Bool
reduced) = Polynom a c -> [Polynom a c] -> Bool -> (Polynom a c, Bool)
reduceStep Polynom a c
h [Polynom a c]
fs Bool
False
          reduceStep :: Polynom a c -> [Polynom a c] -> Bool -> (Polynom a c, Bool)
reduceStep Polynom a c
p (Polynom a c
q:[Polynom a c]
qs) Bool
r
              | Polynom a c -> Bool
forall a c. Polynom a c -> Bool
zeroP Polynom a c
h   = (Polynom a c
h, Bool
r)
              | Bool
otherwise =
                    if Polynom a c -> Polynom a c -> Bool
forall a c.
(Ord a, MultiplicativeMonoid a) =>
Polynom a c -> Polynom a c -> Bool
reducable Polynom a c
p Polynom a c
q
                        then (Polynom a c -> Polynom a c -> Polynom a c
forall c a.
(Eq c, FiniteField c, Ord a, Ring a) =>
Polynom a c -> Polynom a c -> Polynom a c
reduce Polynom a c
p Polynom a c
q, Bool
True)
                        else Polynom a c -> [Polynom a c] -> Bool -> (Polynom a c, Bool)
reduceStep Polynom a c
p [Polynom a c]
qs Bool
r
          reduceStep Polynom a c
p [] Bool
r = (Polynom a c
p, Bool
r)

fullReduceMany :: (Eq c, FiniteField c, Ord a, Ring a) =>
    Polynom a c -> [Polynom a c] -> Polynom a c
fullReduceMany :: forall c a.
(Eq c, FiniteField c, Ord a, Ring a) =>
Polynom a c -> [Polynom a c] -> Polynom a c
fullReduceMany Polynom a c
h [Polynom a c]
fs
    | Polynom a c -> Bool
forall a c. Polynom a c -> Bool
zeroP Polynom a c
h'   = Polynom a c
h'
    | Bool
otherwise = [Monom a c] -> Polynom a c
forall a c. [Monom a c] -> Polynom a c
P [Polynom a c -> Monom a c
forall c a. Polynom c a -> Monom c a
lt Polynom a c
h'] Polynom a c -> Polynom a c -> Polynom a c
forall a. AdditiveSemigroup a => a -> a -> a
+ Polynom a c -> [Polynom a c] -> Polynom a c
forall c a.
(Eq c, FiniteField c, Ord a, Ring a) =>
Polynom a c -> [Polynom a c] -> Polynom a c
fullReduceMany (Polynom a c
h' Polynom a c -> Polynom a c -> Polynom a c
forall a. AdditiveGroup a => a -> a -> a
- [Monom a c] -> Polynom a c
forall a c. [Monom a c] -> Polynom a c
P [Polynom a c -> Monom a c
forall c a. Polynom c a -> Monom c a
lt Polynom a c
h']) [Polynom a c]
fs
    where h' :: Polynom a c
h' = Polynom a c -> [Polynom a c] -> Polynom a c
forall c a.
(Eq c, FiniteField c, Ord a, Ring a) =>
Polynom a c -> [Polynom a c] -> Polynom a c
reduceMany Polynom a c
h [Polynom a c]
fs

systemReduce :: (Eq c, FiniteField c, Ord a, Ring a) => [Polynom a c] -> [Polynom a c]
systemReduce :: forall c a.
(Eq c, FiniteField c, Ord a, Ring a) =>
[Polynom a c] -> [Polynom a c]
systemReduce = (Polynom a c -> [Polynom a c] -> [Polynom a c])
-> [Polynom a c] -> [Polynom a c] -> [Polynom a c]
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: Type -> Type) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Polynom a c -> [Polynom a c] -> [Polynom a c]
forall {c} {a}.
(Finite c, Field c, Ord a, Eq c, Ring a) =>
Polynom a c -> [Polynom a c] -> [Polynom a c]
f []
    where f :: Polynom a c -> [Polynom a c] -> [Polynom a c]
f Polynom a c
p [Polynom a c]
ps = let p' :: Polynom a c
p' = Polynom a c -> [Polynom a c] -> Polynom a c
forall c a.
(Eq c, FiniteField c, Ord a, Ring a) =>
Polynom a c -> [Polynom a c] -> Polynom a c
fullReduceMany Polynom a c
p [Polynom a c]
ps in [Polynom a c] -> [Polynom a c] -> Bool -> [Polynom a c]
forall a. a -> a -> Bool -> a
bool [Polynom a c]
ps (Polynom a c
p' Polynom a c -> [Polynom a c] -> [Polynom a c]
forall a. a -> [a] -> [a]
: [Polynom a c]
ps) (Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Polynom a c -> Bool
forall a c. Polynom a c -> Bool
zeroP Polynom a c
p')