module ZkFold.Symbolic.GroebnerBasis.Internal where

import           Data.List                                        (sortBy)
import           Data.Map                                         (notMember)
import           Numeric.Natural                                  (Natural)
import           Prelude                                          hiding (Num (..), drop, lcm, length, sum, take, (!!),
                                                                   (/))

import           ZkFold.Base.Algebra.Basic.Class
import           ZkFold.Prelude                                   (length)
import           ZkFold.Symbolic.GroebnerBasis.Internal.Reduction
import           ZkFold.Symbolic.GroebnerBasis.Internal.Types

makeSPoly :: (Eq c, FiniteField c, Ord a, Ring a) =>
             Polynom a c -> Polynom a c -> Polynom a c
makeSPoly :: forall c a.
(Eq c, FiniteField c, Ord a, Ring a) =>
Polynom a c -> Polynom a c -> Polynom a c
makeSPoly Polynom a c
l Polynom a c
r = if Map Natural (Var a c) -> Bool
forall a. Map Natural a -> Bool
forall (t :: Type -> Type) a. Foldable t => t a -> Bool
null Map Natural (Var a c)
as then Polynom a c
forall a. AdditiveMonoid a => a
zero else 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 M c
_ Map Natural (Var a c)
as = Monom a c -> Monom a c -> Monom a c
forall c a.
(FiniteField c, Ord a, MultiplicativeMonoid a) =>
Monom a c -> Monom a c -> Monom a c
gcdM (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)
          l' :: Polynom a c
l'  = 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
l Monom a c
ra
          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 Monom a c
la
          lcm :: Monom a c
lcm = Monom a c -> Monom a c -> Monom a c
forall c a.
(FiniteField c, Ord a, MultiplicativeMonoid a) =>
Monom a c -> Monom a c -> Monom a c
lcmM (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)
          ra :: Monom a c
ra  = 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 Monom a c
lcm (Polynom a c -> Monom a c
forall c a. Polynom c a -> Monom c a
lt Polynom a c
l)
          la :: Monom a c
la  = Integer -> Monom a c -> Monom a c
forall b a. Scale b a => b -> a -> a
scale (-Integer
1 :: Integer) (Monom a c -> Monom a c) -> Monom a c -> Monom a c
forall a b. (a -> b) -> a -> b
$ 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 Monom a c
lcm (Polynom a c -> Monom a c
forall c a. Polynom c a -> Monom c a
lt Polynom a c
r)

varNumber :: Polynom a c -> Natural
varNumber :: forall a c. Polynom a c -> Natural
varNumber (P [])         = Natural
0
varNumber (P (M c
_ Map Natural (Var a c)
as:[Monom a c]
_)) = Map Natural (Var a c) -> Natural
forall (t :: Type -> Type) a. Foldable t => t a -> Natural
length Map Natural (Var a c)
as

varIsMissing :: Natural -> Polynom a c -> Bool
varIsMissing :: forall a c. Natural -> Polynom a c -> Bool
varIsMissing Natural
i (P [Monom a c]
ms) = (Monom a c -> Bool) -> [Monom a c] -> Bool
forall (t :: Type -> Type) a.
Foldable t =>
(a -> Bool) -> t a -> Bool
all (\(M c
_ Map Natural (Var a c)
as) -> Natural -> Map Natural (Var a c) -> Bool
forall k a. Ord k => k -> Map k a -> Bool
notMember (Natural
i Natural -> Natural -> Natural
-! Natural
1) Map Natural (Var a c)
as) [Monom a c]
ms

checkVarUnique :: Natural -> [Polynom a c] -> Bool
checkVarUnique :: forall a c. Natural -> [Polynom a c] -> Bool
checkVarUnique Natural
i [Polynom a c]
fs = [Bool] -> Natural
forall (t :: Type -> Type) a. Foldable t => t a -> Natural
length ((Bool -> Bool) -> [Bool] -> [Bool]
forall a. (a -> Bool) -> [a] -> [a]
filter Bool -> Bool
not ([Bool] -> [Bool]) -> [Bool] -> [Bool]
forall a b. (a -> b) -> a -> b
$ (Polynom a c -> Bool) -> [Polynom a c] -> [Bool]
forall a b. (a -> b) -> [a] -> [b]
map (Natural -> Polynom a c -> Bool
forall a c. Natural -> Polynom a c -> Bool
varIsMissing Natural
i) [Polynom a c]
fs) Natural -> Natural -> Bool
forall a. Eq a => a -> a -> Bool
== Natural
1

checkLTSimple :: Polynom a c -> Bool
checkLTSimple :: forall a c. Polynom a c -> Bool
checkLTSimple (P [])         = Bool
True
checkLTSimple (P (M c
_ Map Natural (Var a c)
as:[Monom a c]
_)) = Map Natural (Var a c) -> Natural
forall (t :: Type -> Type) a. Foldable t => t a -> Natural
length Map Natural (Var a c)
as Natural -> Natural -> Bool
forall a. Ord a => a -> a -> Bool
<= Natural
1

trimSystem :: (Eq c, Ord a, AdditiveMonoid a) => Polynom a c -> [Polynom a c] -> [Polynom a c]
trimSystem :: forall c a.
(Eq c, Ord a, AdditiveMonoid a) =>
Polynom a c -> [Polynom a c] -> [Polynom a c]
trimSystem Polynom a c
h [Polynom a c]
fs = (Polynom a c -> Bool) -> [Polynom a c] -> [Polynom a c]
forall a. (a -> Bool) -> [a] -> [a]
filter (\Polynom a c
f -> Polynom a c -> Natural
forall a c. Polynom a c -> Natural
lv Polynom a c
f Natural -> Natural -> Bool
forall a. Ord a => a -> a -> Bool
>= Polynom a c -> Natural
forall a c. Polynom a c -> Natural
lv Polynom a c
h) ([Polynom a c] -> [Polynom a c]) -> [Polynom a c] -> [Polynom a c]
forall a b. (a -> b) -> a -> b
$
        Natural -> [Polynom a c]
go (Polynom a c -> Natural
forall a c. Polynom a c -> Natural
varNumber Polynom a c
h)
    where
        go :: Natural -> [Polynom a c]
go Natural
0 = [Polynom a c]
fs
        go Natural
i = if Natural -> Polynom a c -> Bool
forall a c. Natural -> Polynom a c -> Bool
varIsMissing Natural
i Polynom a c
h Bool -> Bool -> Bool
&& Natural -> [Polynom a c] -> Bool
forall a c. Natural -> [Polynom a c] -> Bool
checkVarUnique Natural
i [Polynom a c]
fs Bool -> Bool -> Bool
&& (Polynom a c -> Bool) -> [Polynom a c] -> Bool
forall (t :: Type -> Type) a.
Foldable t =>
(a -> Bool) -> t a -> Bool
any Polynom a c -> Bool
forall a c. Polynom a c -> Bool
checkLTSimple [Polynom a c]
fs
            then Polynom a c -> [Polynom a c] -> [Polynom a c]
forall c a.
(Eq c, Ord a, AdditiveMonoid a) =>
Polynom a c -> [Polynom a c] -> [Polynom a c]
trimSystem Polynom a c
h ((Polynom a c -> Bool) -> [Polynom a c] -> [Polynom a c]
forall a. (a -> Bool) -> [a] -> [a]
filter (Natural -> Polynom a c -> Bool
forall a c. Natural -> Polynom a c -> Bool
varIsMissing Natural
i) [Polynom a c]
fs)
            else Natural -> [Polynom a c]
go (Natural
i Natural -> Natural -> Natural
-! Natural
1)

addSPolyStep :: (Eq c, FiniteField c, Ord a, Ring a) =>
            [Polynom a c] -> [Polynom a c] -> [Polynom a c] -> [Polynom a c]
addSPolyStep :: forall c a.
(Eq c, FiniteField c, Ord a, Ring a) =>
[Polynom a c] -> [Polynom a c] -> [Polynom a c] -> [Polynom a c]
addSPolyStep [] [Polynom a c]
_ [Polynom a c]
rs = [Polynom a c]
rs
addSPolyStep [Polynom a c]
_ [] [Polynom a c]
rs = [Polynom a c]
rs
addSPolyStep (Polynom a c
p:[Polynom a c]
ps) (Polynom a c
q:[Polynom a c]
qs) [Polynom a c]
rs
    | Bool -> Bool
not (Polynom a c -> Bool
forall a c. Polynom a c -> Bool
zeroP Polynom a c
s)  = (Polynom a c -> Polynom a c -> Ordering)
-> [Polynom a c] -> [Polynom a c]
forall a. (a -> a -> Ordering) -> [a] -> [a]
sortBy ((Polynom a c -> Polynom a c -> Ordering)
-> Polynom a c -> Polynom a c -> Ordering
forall a b c. (a -> b -> c) -> b -> a -> c
flip Polynom a c -> Polynom a c -> Ordering
forall a. Ord a => a -> a -> Ordering
compare) (Polynom a c
s Polynom a c -> [Polynom a c] -> [Polynom a c]
forall a. a -> [a] -> [a]
: [Polynom a c]
rs')
    | Polynom a c -> Monom a c
forall c a. Polynom c a -> Monom c a
lt Polynom a c
p Monom a c -> Monom a c -> Bool
forall a. Eq a => a -> a -> Bool
== Polynom a c -> Monom a c
forall c a. Polynom c a -> Monom c a
lt Polynom a c
q   = [Polynom a c] -> [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] -> [Polynom a c]
addSPolyStep [Polynom a c]
ps ([Polynom a c] -> [Polynom a c]
forall a. [a] -> [a]
reverse [Polynom a c]
rs) [Polynom a c]
rs
    | Bool
otherwise      = [Polynom a c] -> [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] -> [Polynom a c]
addSPolyStep (Polynom a c
pPolynom a c -> [Polynom a c] -> [Polynom a c]
forall a. a -> [a] -> [a]
:[Polynom a c]
ps) [Polynom a c]
qs [Polynom a c]
rs
        where
            s :: Polynom a c
s = 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 -> 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
makeSPoly Polynom a c
p Polynom a c
q) [Polynom a c]
rs
            rs' :: [Polynom a c]
rs' = (Polynom a c -> Bool) -> [Polynom a c] -> [Polynom a c]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool) -> (Polynom a c -> Bool) -> Polynom a c -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Polynom a c -> Bool
forall a c. Polynom a c -> Bool
zeroP) ([Polynom a c] -> [Polynom a c]) -> [Polynom a c] -> [Polynom a c]
forall a b. (a -> b) -> a -> b
$ (Polynom a c -> Polynom a c) -> [Polynom a c] -> [Polynom a c]
forall a b. (a -> b) -> [a] -> [b]
map (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
s]) [Polynom a c]
rs

groebnerStep :: (Eq c, FiniteField c, Ord a, Ring a) =>
                Polynom a c -> [Polynom a c] -> (Polynom a c, [Polynom a c])
groebnerStep :: forall c a.
(Eq c, FiniteField c, Ord a, Ring a) =>
Polynom a c -> [Polynom a c] -> (Polynom a c, [Polynom a c])
groebnerStep 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, [Polynom a c]
fs)
    | Bool
otherwise =
        let 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
fullReduceMany Polynom a c
h [Polynom a c]
fs
            fs' :: [Polynom a c]
fs'  = Polynom a c -> [Polynom a c] -> [Polynom a c]
forall c a.
(Eq c, Ord a, AdditiveMonoid a) =>
Polynom a c -> [Polynom a c] -> [Polynom a c]
trimSystem Polynom a c
h' [Polynom a c]
fs
            fs'' :: [Polynom a c]
fs'' = [Polynom a c] -> [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] -> [Polynom a c]
addSPolyStep ([Polynom a c] -> [Polynom a c]
forall a. [a] -> [a]
reverse [Polynom a c]
fs') ([Polynom a c] -> [Polynom a c]
forall a. [a] -> [a]
reverse [Polynom a c]
fs') [Polynom a c]
fs'
        in (Polynom a c
h', [Polynom a c]
fs'')