module ZkFold.Symbolic.GroebnerBasis (
    module ZkFold.Symbolic.GroebnerBasis.Types,
    boundVariables,
    makeTheorem,
    verify,
    groebner,
    variableTypes,
    -- Internal
    lt,
    zeroM,
    zeroP,
    similarM,
    makeSPoly,
    fullReduceMany,
    groebnerStep,
    groebnerStepMax
    ) where

import           Data.Bool                                        (bool)
import           Data.List                                        (nub, sortBy)
import           Data.Map                                         (Map, elems, empty, keys, mapWithKey, singleton)
import           Data.Maybe                                       (mapMaybe)
import           GHC.IsList                                       (IsList (..))
import           Numeric.Natural                                  (Natural)
import           Prelude                                          hiding (Num (..), length, replicate, (!!))

import           ZkFold.Base.Algebra.Basic.Class
import           ZkFold.Base.Algebra.Basic.Field                  (Zp)
import           ZkFold.Base.Algebra.Basic.Number                 (Prime)
import           ZkFold.Prelude                                   ((!!))
import           ZkFold.Symbolic.Compiler
import           ZkFold.Symbolic.GroebnerBasis.Internal
import           ZkFold.Symbolic.GroebnerBasis.Internal.Reduction
import           ZkFold.Symbolic.GroebnerBasis.Internal.Types
import           ZkFold.Symbolic.GroebnerBasis.Types

boundVariables :: forall p . PrimeField (Zp p) => Polynomial p -> [Polynomial p] -> Polynomial p
boundVariables :: forall (p :: Natural).
PrimeField (Zp p) =>
Polynomial p -> [Polynomial p] -> Polynomial p
boundVariables Polynom Integer (Zp p)
p [Polynom Integer (Zp p)]
ps = ((Natural, Polynom Integer (Zp p))
 -> Polynom Integer (Zp p) -> Polynom Integer (Zp p))
-> Polynom Integer (Zp p)
-> [(Natural, Polynom Integer (Zp p))]
-> Polynom Integer (Zp p)
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 ((Natural, Variable p)
-> Polynom Integer (Zp p) -> Polynom Integer (Zp p)
makeBound ((Natural, Variable p)
 -> Polynom Integer (Zp p) -> Polynom Integer (Zp p))
-> ((Natural, Polynom Integer (Zp p)) -> (Natural, Variable p))
-> (Natural, Polynom Integer (Zp p))
-> Polynom Integer (Zp p)
-> Polynom Integer (Zp p)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Natural, Polynom Integer (Zp p)) -> (Natural, Variable p)
findVar) Polynom Integer (Zp p)
p ([(Natural, Polynom Integer (Zp p))] -> Polynom Integer (Zp p))
-> [(Natural, Polynom Integer (Zp p))] -> Polynom Integer (Zp p)
forall a b. (a -> b) -> a -> b
$ [Natural]
-> [Polynom Integer (Zp p)] -> [(Natural, Polynom Integer (Zp p))]
forall a b. [a] -> [b] -> [(a, b)]
zip [Natural
0..] [Polynom Integer (Zp p)]
ps
    where
        findVar :: (Natural, Polynomial p) -> (Natural, Variable p)
        findVar :: (Natural, Polynom Integer (Zp p)) -> (Natural, Variable p)
findVar (Natural
k, Polynom Integer (Zp p)
h) = (Natural
i, Variable p
v)
            where
                M Zp p
_ Map Natural (Variable p)
as = Polynom Integer (Zp p) -> Monom Integer (Zp p)
forall c a. Polynom c a -> Monom c a
lt Polynom Integer (Zp p)
h
                i :: Natural
i = [Natural] -> Natural
forall a. Ord a => [a] -> a
forall (t :: Type -> Type) a. (Foldable t, Ord a) => t a -> a
minimum ([Natural] -> Natural) -> [Natural] -> Natural
forall a b. (a -> b) -> a -> b
$ Map Natural (Variable p) -> [Natural]
forall k a. Map k a -> [k]
keys Map Natural (Variable p)
as
                s :: Polynom Integer (Zp p)
s = if Natural
k Natural -> Natural -> Bool
forall a. Ord a => a -> a -> Bool
> Natural
0 then Polynom Integer (Zp p)
-> Polynom Integer (Zp p) -> Polynom Integer (Zp p)
forall c a.
(Eq c, FiniteField c, Ord a, Ring a) =>
Polynom a c -> Polynom a c -> Polynom a c
makeSPoly ([Polynom Integer (Zp p)]
ps [Polynom Integer (Zp p)] -> Natural -> Polynom Integer (Zp p)
forall a. [a] -> Natural -> a
!! (Natural
kNatural -> Natural -> Natural
-!Natural
1)) Polynom Integer (Zp p)
h else Polynom Integer (Zp p)
forall a. AdditiveMonoid a => a
zero
                s' :: Polynom Integer (Zp p)
s' = [Monom Integer (Zp p)] -> Polynom Integer (Zp p)
forall a c. [Monom a c] -> Polynom a c
P [Zp p -> Map Natural (Variable p) -> Monom Integer (Zp p)
forall a c. c -> Map Natural (Var a c) -> Monom a c
M Zp p
forall a. MultiplicativeMonoid a => a
one (Natural -> Variable p -> Map Natural (Variable p)
forall k a. k -> a -> Map k a
singleton Natural
i (Integer -> Variable p
forall (p :: Natural). Integer -> Variable p
variable Integer
2))] Polynom Integer (Zp p)
-> Polynom Integer (Zp p) -> Polynom Integer (Zp p)
forall a. AdditiveGroup a => a -> a -> a
- [Monom Integer (Zp p)] -> Polynom Integer (Zp p)
forall a c. [Monom a c] -> Polynom a c
P [Zp p -> Map Natural (Variable p) -> Monom Integer (Zp p)
forall a c. c -> Map Natural (Var a c) -> Monom a c
M Zp p
forall a. MultiplicativeMonoid a => a
one (Natural -> Variable p -> Map Natural (Variable p)
forall k a. k -> a -> Map k a
singleton Natural
i (Integer -> Variable p
forall (p :: Natural). Integer -> Variable p
variable Integer
1))]
                v :: Variable p
v = Variable p -> Variable p -> Bool -> Variable p
forall a. a -> a -> Bool -> a
bool (Integer -> Natural -> Variable p
forall {k} a (c :: k). a -> Natural -> Var a c
Bound Integer
1 Natural
k) (Natural -> Variable p
forall {k} a (c :: k). Natural -> Var a c
Boolean Natural
k) (Bool -> Variable p) -> Bool -> Variable p
forall a b. (a -> b) -> a -> b
$ Polynom Integer (Zp p) -> Bool
forall a c. Polynom a c -> Bool
zeroP (Polynom Integer (Zp p) -> Bool) -> Polynom Integer (Zp p) -> Bool
forall a b. (a -> b) -> a -> b
$ Polynom Integer (Zp p)
s Polynom Integer (Zp p)
-> Polynom Integer (Zp p) -> Polynom Integer (Zp p)
forall c a.
(Eq c, FiniteField c, Ord a, Ring a) =>
Polynom a c -> Polynom a c -> Polynom a c
`reduce` Polynom Integer (Zp p)
s'

        makeBound :: (Natural, Variable p) -> Polynomial p -> Polynomial p
        makeBound :: (Natural, Variable p)
-> Polynom Integer (Zp p) -> Polynom Integer (Zp p)
makeBound (Natural
i, Variable p
v) = Polynom Integer (Zp p) -> Polynom Integer (Zp p)
makeBoundPolynomial
            where
                makeBoundVar :: Variable p -> Variable p
                makeBoundVar :: Variable p -> Variable p
makeBoundVar Variable p
v' = Integer -> Variable p -> Variable p
forall {k} a (c :: k). a -> Var a c -> Var a c
setPower (Variable p -> Integer
forall {k} a (c :: k). MultiplicativeMonoid a => Var a c -> a
getPower Variable p
v') Variable p
v

                makeBoundMonomial :: Monomial p -> Monomial p
                makeBoundMonomial :: Monom Integer (Zp p) -> Monom Integer (Zp p)
makeBoundMonomial (M Zp p
c Map Natural (Variable p)
as) = Zp p -> Map Natural (Variable p) -> Monom Integer (Zp p)
forall a c. c -> Map Natural (Var a c) -> Monom a c
M Zp p
c (Map Natural (Variable p) -> Monom Integer (Zp p))
-> Map Natural (Variable p) -> Monom Integer (Zp p)
forall a b. (a -> b) -> a -> b
$ (Natural -> Variable p -> Variable p)
-> Map Natural (Variable p) -> Map Natural (Variable p)
forall k a b. (k -> a -> b) -> Map k a -> Map k b
mapWithKey (\Natural
j Variable p
v' -> if Natural
j Natural -> Natural -> Bool
forall a. Eq a => a -> a -> Bool
== Natural
i then Variable p -> Variable p
makeBoundVar Variable p
v' else Variable p
v') Map Natural (Variable p)
as

                makeBoundPolynomial :: Polynomial p -> Polynomial p
                makeBoundPolynomial :: Polynom Integer (Zp p) -> Polynom Integer (Zp p)
makeBoundPolynomial (P [Monom Integer (Zp p)]
ms) = [Monom Integer (Zp p)] -> Polynom Integer (Zp p)
forall a c. [Monom a c] -> Polynom a c
P ([Monom Integer (Zp p)] -> Polynom Integer (Zp p))
-> [Monom Integer (Zp p)] -> Polynom Integer (Zp p)
forall a b. (a -> b) -> a -> b
$ (Monom Integer (Zp p) -> Monom Integer (Zp p))
-> [Monom Integer (Zp p)] -> [Monom Integer (Zp p)]
forall a b. (a -> b) -> [a] -> [b]
map Monom Integer (Zp p) -> Monom Integer (Zp p)
makeBoundMonomial [Monom Integer (Zp p)]
ms

variableTypes :: forall p . Prime p => [Polynomial p] -> [(Monomial p, VarType)]
variableTypes :: forall (p :: Natural).
Prime p =>
[Polynomial p] -> [(Monomial p, VarType)]
variableTypes = [(Monomial p, VarType)] -> [(Monomial p, VarType)]
forall a. Eq a => [a] -> [a]
nub ([(Monomial p, VarType)] -> [(Monomial p, VarType)])
-> ([Polynomial p] -> [(Monomial p, VarType)])
-> [Polynomial p]
-> [(Monomial p, VarType)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Monomial p, VarType) -> (Monomial p, VarType) -> Ordering)
-> [(Monomial p, VarType)] -> [(Monomial p, VarType)]
forall a. (a -> a -> Ordering) -> [a] -> [a]
sortBy (\(Monomial p
x1, VarType
_) (Monomial p
x2, VarType
_) -> Monomial p -> Monomial p -> Ordering
forall a. Ord a => a -> a -> Ordering
compare Monomial p
x2 Monomial p
x1) ([(Monomial p, VarType)] -> [(Monomial p, VarType)])
-> ([Polynomial p] -> [(Monomial p, VarType)])
-> [Polynomial p]
-> [(Monomial p, VarType)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Polynomial p -> [(Monomial p, VarType)])
-> [Polynomial p] -> [(Monomial p, VarType)]
forall (t :: Type -> Type) a b.
Foldable t =>
(a -> [b]) -> t a -> [b]
concatMap Polynomial p -> [(Monomial p, VarType)]
variableTypes'
    where
        variableTypes' :: Polynomial p -> [(Monomial p, VarType)]
        variableTypes' :: Polynomial p -> [(Monomial p, VarType)]
variableTypes' (P [Monomial p]
ms) = (Monomial p -> [(Monomial p, VarType)])
-> [Monomial p] -> [(Monomial p, VarType)]
forall (t :: Type -> Type) a b.
Foldable t =>
(a -> [b]) -> t a -> [b]
concatMap Monomial p -> [(Monomial p, VarType)]
variableTypes'' [Monomial p]
ms

        variableTypes'' :: Monomial p -> [(Monomial p, VarType)]
        variableTypes'' :: Monomial p -> [(Monomial p, VarType)]
variableTypes'' (M Zp p
_ Map Natural (Var Integer (Zp p))
as) = ((Natural, Var Integer (Zp p)) -> (Monomial p, VarType))
-> [(Natural, Var Integer (Zp p))] -> [(Monomial p, VarType)]
forall a b. (a -> b) -> [a] -> [b]
map (\(Natural
j, Var Integer (Zp p)
v) -> (Zp p -> Map Natural (Var Integer (Zp p)) -> Monomial p
forall a c. c -> Map Natural (Var a c) -> Monom a c
M Zp p
forall a. MultiplicativeMonoid a => a
one (Natural -> Var Integer (Zp p) -> Map Natural (Var Integer (Zp p))
forall k a. k -> a -> Map k a
singleton Natural
j (Integer -> Var Integer (Zp p) -> Var Integer (Zp p)
forall {k} a (c :: k). a -> Var a c -> Var a c
setPower Integer
1 Var Integer (Zp p)
v)), Var Integer (Zp p) -> VarType
forall {k} a (c :: k). Var a c -> VarType
getVarType Var Integer (Zp p)
v)) ([(Natural, Var Integer (Zp p))] -> [(Monomial p, VarType)])
-> [(Natural, Var Integer (Zp p))] -> [(Monomial p, VarType)]
forall a b. (a -> b) -> a -> b
$ Map Natural (Var Integer (Zp p))
-> [Item (Map Natural (Var Integer (Zp p)))]
forall l. IsList l => l -> [Item l]
toList Map Natural (Var Integer (Zp p))
as

makeTheorem :: forall p . PrimeField (Zp p) => ArithmeticCircuit (Zp p) -> (Polynomial p, [Polynomial p])
makeTheorem :: forall (p :: Natural).
PrimeField (Zp p) =>
ArithmeticCircuit (Zp p) -> (Polynomial p, [Polynomial p])
makeTheorem ArithmeticCircuit (Zp p)
r = (Polynomial p -> [Polynomial p] -> Polynomial p
forall (p :: Natural).
PrimeField (Zp p) =>
Polynomial p -> [Polynomial p] -> Polynomial p
boundVariables Polynomial p
p0 [Polynomial p]
ps, --systemReduce $
        (Polynomial p -> Polynomial p) -> [Polynomial p] -> [Polynomial p]
forall a b. (a -> b) -> [a] -> [b]
map (Polynomial p -> [Polynomial p] -> Polynomial p
forall (p :: Natural).
PrimeField (Zp p) =>
Polynomial p -> [Polynomial p] -> Polynomial p
`boundVariables` [Polynomial p]
ps) [Polynomial p]
ps)
    where
        m :: Map Natural (Constraint (Zp p))
m  = ArithmeticCircuit (Zp p) -> Map Natural (Constraint (Zp p))
forall a. ArithmeticCircuit a -> Map Natural (Constraint a)
acSystem ArithmeticCircuit (Zp p)
r
        xs :: [Natural]
xs = [Natural] -> [Natural]
forall a. [a] -> [a]
reverse ([Natural] -> [Natural]) -> [Natural] -> [Natural]
forall a b. (a -> b) -> a -> b
$ Map (Natural, Natural) Natural -> [Natural]
forall k a. Map k a -> [a]
elems (Map (Natural, Natural) Natural -> [Natural])
-> Map (Natural, Natural) Natural -> [Natural]
forall a b. (a -> b) -> a -> b
$ ArithmeticCircuit (Zp p) -> Map (Natural, Natural) Natural
forall a. ArithmeticCircuit a -> Map (Natural, Natural) Natural
acVarOrder ArithmeticCircuit (Zp p)
r
        ps :: [Polynomial p]
ps = (Polynomial p -> Polynomial p -> Ordering)
-> [Polynomial p] -> [Polynomial p]
forall a. (a -> a -> Ordering) -> [a] -> [a]
sortBy ((Polynomial p -> Polynomial p -> Ordering)
-> Polynomial p -> Polynomial p -> Ordering
forall a b c. (a -> b -> c) -> b -> a -> c
flip Polynomial p -> Polynomial p -> Ordering
forall a. Ord a => a -> a -> Ordering
compare) ([Polynomial p] -> [Polynomial p])
-> [Polynomial p] -> [Polynomial p]
forall a b. (a -> b) -> a -> b
$ (Constraint (Zp p) -> Polynomial p)
-> [Constraint (Zp p)] -> [Polynomial p]
forall a b. (a -> b) -> [a] -> [b]
map Constraint (Zp p) -> Polynomial p
convert ([Constraint (Zp p)] -> [Polynomial p])
-> [Constraint (Zp p)] -> [Polynomial p]
forall a b. (a -> b) -> a -> b
$ Map Natural (Constraint (Zp p)) -> [Constraint (Zp p)]
forall k a. Map k a -> [a]
elems Map Natural (Constraint (Zp p))
m

        k :: Natural
k  = ArithmeticCircuit (Zp p) -> Natural
forall a. ArithmeticCircuit a -> Natural
acOutput ArithmeticCircuit (Zp p)
r
        p0 :: Polynomial p
p0 = [Monomial p] -> Polynomial p
forall (p :: Natural).
PrimeField (Zp p) =>
[Monomial p] -> Polynomial p
polynomial [Zp p -> Map Natural (Var Integer (Zp p)) -> Monomial p
forall a c. c -> Map Natural (Var a c) -> Monom a c
M Zp p
forall a. MultiplicativeMonoid a => a
one (Natural -> Var Integer (Zp p) -> Map Natural (Var Integer (Zp p))
forall k a. k -> a -> Map k a
singleton (Natural -> Natural
mapVars Natural
k) (Integer -> Var Integer (Zp p)
forall {k} a (c :: k). a -> Var a c
Free Integer
1))] Polynomial p -> Polynomial p -> Polynomial p
forall a. AdditiveGroup a => a -> a -> a
- [Monomial p] -> Polynomial p
forall (p :: Natural).
PrimeField (Zp p) =>
[Monomial p] -> Polynomial p
polynomial [Zp p -> Map Natural (Var Integer (Zp p)) -> Monomial p
forall a c. c -> Map Natural (Var a c) -> Monom a c
M Zp p
forall a. MultiplicativeMonoid a => a
one Map Natural (Var Integer (Zp p))
forall k a. Map k a
empty]

        mapVars :: Natural -> Natural
        mapVars :: Natural -> Natural
mapVars Natural
x
            | Natural
x Natural -> Natural -> Bool
forall a. Eq a => a -> a -> Bool
== Natural
0    = Natural
0
            | Bool
otherwise = case Natural -> [(Natural, Natural)] -> Maybe Natural
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Natural
x ([Natural] -> [Natural] -> [(Natural, Natural)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Natural]
xs [Natural
1..]) of
                Just Natural
i  -> Natural
i
                Maybe Natural
Nothing -> [Char] -> Natural
forall a. HasCallStack => [Char] -> a
error ([Char] -> Natural) -> [Char] -> Natural
forall a b. (a -> b) -> a -> b
$ [Char]
"mapVars: variable " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Natural -> [Char]
forall a. Show a => a -> [Char]
show Natural
x [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" not found!"

        convert :: Constraint (Zp p) -> Polynomial p
        convert :: Constraint (Zp p) -> Polynomial p
convert Constraint (Zp p)
ms = [Monomial p] -> Polynomial p
forall (p :: Natural).
PrimeField (Zp p) =>
[Monomial p] -> Polynomial p
polynomial ([Monomial p] -> Polynomial p) -> [Monomial p] -> Polynomial p
forall a b. (a -> b) -> a -> b
$ (Zp p, Map Natural Natural) -> Monomial p
convert' ((Zp p, Map Natural Natural) -> Monomial p)
-> [(Zp p, Map Natural Natural)] -> [Monomial p]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Constraint (Zp p) -> [Item (Constraint (Zp p))]
forall l. IsList l => l -> [Item l]
toList Constraint (Zp p)
ms
            where
                convert' :: (Zp p, Map Natural Natural) -> Monomial p
                convert' :: (Zp p, Map Natural Natural) -> Monomial p
convert' (Zp p
c, Map Natural Natural
as) = Zp p -> Map Natural (Var Integer (Zp p)) -> Monomial p
forall a c. c -> Map Natural (Var a c) -> Monom a c
M Zp p
c (Map Natural (Var Integer (Zp p)) -> Monomial p)
-> (Map Natural Natural -> Map Natural (Var Integer (Zp p)))
-> Map Natural Natural
-> Monomial p
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(Natural, Var Integer (Zp p))] -> Map Natural (Var Integer (Zp p))
[Item (Map Natural (Var Integer (Zp p)))]
-> Map Natural (Var Integer (Zp p))
forall l. IsList l => [Item l] -> l
fromList ([(Natural, Var Integer (Zp p))]
 -> Map Natural (Var Integer (Zp p)))
-> (Map Natural Natural -> [(Natural, Var Integer (Zp p))])
-> Map Natural Natural
-> Map Natural (Var Integer (Zp p))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Natural, Natural) -> Maybe (Natural, Var Integer (Zp p)))
-> [(Natural, Natural)] -> [(Natural, Var Integer (Zp p))]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (Natural, Natural) -> Maybe (Natural, Var Integer (Zp p))
convert'' ([(Natural, Natural)] -> [(Natural, Var Integer (Zp p))])
-> (Map Natural Natural -> [(Natural, Natural)])
-> Map Natural Natural
-> [(Natural, Var Integer (Zp p))]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map Natural Natural -> [(Natural, Natural)]
Map Natural Natural -> [Item (Map Natural Natural)]
forall l. IsList l => l -> [Item l]
toList (Map Natural Natural -> Monomial p)
-> Map Natural Natural -> Monomial p
forall a b. (a -> b) -> a -> b
$ Map Natural Natural
as
                    where
                        convert'' :: (Natural, Natural) -> Maybe (Natural, Variable p)
                        convert'' :: (Natural, Natural) -> Maybe (Natural, Var Integer (Zp p))
convert'' (Natural
j, Natural
i) =
                            let ind :: Natural
ind = Natural -> Natural
mapVars Natural
j
                            in if Natural
ind Natural -> Natural -> Bool
forall a. Ord a => a -> a -> Bool
> Natural
0 then (Natural, Var Integer (Zp p))
-> Maybe (Natural, Var Integer (Zp p))
forall a. a -> Maybe a
Just (Natural
ind, Integer -> Var Integer (Zp p)
forall {k} a (c :: k). a -> Var a c
Free (Natural -> Integer
forall a b. FromConstant a b => a -> b
fromConstant Natural
i)) else Maybe (Natural, Var Integer (Zp p))
forall a. Maybe a
Nothing

groebnerStepMax :: Integer
groebnerStepMax :: Integer
groebnerStepMax = Integer
200

verify :: forall p . PrimeField (Zp p) => (Polynomial p, [Polynomial p]) -> Bool
verify :: forall (p :: Natural).
PrimeField (Zp p) =>
(Polynomial p, [Polynomial p]) -> Bool
verify (Polynomial p
p0, [Polynomial p]
ps) = Polynomial p -> Bool
forall a c. Polynom a c -> Bool
zeroP (Polynomial p -> Bool) -> Polynomial p -> Bool
forall a b. (a -> b) -> a -> b
$ (Polynomial p, [Polynomial p]) -> Polynomial p
forall a b. (a, b) -> a
fst ((Polynomial p, [Polynomial p]) -> Polynomial p)
-> (Polynomial p, [Polynomial p]) -> Polynomial p
forall a b. (a -> b) -> a -> b
$ ((Polynomial p, [Polynomial p])
 -> Integer -> (Polynomial p, [Polynomial p]))
-> (Polynomial p, [Polynomial p])
-> [Integer]
-> (Polynomial p, [Polynomial p])
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: Type -> Type) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (\(Polynomial p, [Polynomial p])
args Integer
_ -> (Polynomial p -> [Polynomial p] -> (Polynomial p, [Polynomial p]))
-> (Polynomial p, [Polynomial p]) -> (Polynomial p, [Polynomial p])
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Polynomial p -> [Polynomial p] -> (Polynomial p, [Polynomial p])
forall c a.
(Eq c, FiniteField c, Ord a, Ring a) =>
Polynom a c -> [Polynom a c] -> (Polynom a c, [Polynom a c])
groebnerStep (Polynomial p, [Polynomial p])
args) (Polynomial p
p0, [Polynomial p]
ps) [Integer
1..Integer
groebnerStepMax]

groebner :: forall p . PrimeField (Zp p) => [Polynomial p] -> [Polynomial p]
groebner :: forall (p :: Natural).
PrimeField (Zp p) =>
[Polynomial p] -> [Polynomial p]
groebner [Polynomial p]
ps = (Polynomial p, [Polynomial p]) -> [Polynomial p]
forall a b. (a, b) -> b
snd ((Polynomial p, [Polynomial p]) -> [Polynomial p])
-> (Polynomial p, [Polynomial p]) -> [Polynomial p]
forall a b. (a -> b) -> a -> b
$ ((Polynomial p, [Polynomial p])
 -> Integer -> (Polynomial p, [Polynomial p]))
-> (Polynomial p, [Polynomial p])
-> [Integer]
-> (Polynomial p, [Polynomial p])
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: Type -> Type) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (\(Polynomial p, [Polynomial p])
args Integer
_ -> (Polynomial p -> [Polynomial p] -> (Polynomial p, [Polynomial p]))
-> (Polynomial p, [Polynomial p]) -> (Polynomial p, [Polynomial p])
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Polynomial p -> [Polynomial p] -> (Polynomial p, [Polynomial p])
forall c a.
(Eq c, FiniteField c, Ord a, Ring a) =>
Polynom a c -> [Polynom a c] -> (Polynom a c, [Polynom a c])
groebnerStep (Polynomial p, [Polynomial p])
args) (Polynomial p
p, [Polynomial p]
ps) [Integer
1..Integer
groebnerStepMax]
    where p :: Polynomial p
p = [Monomial p] -> Polynomial p
forall (p :: Natural).
PrimeField (Zp p) =>
[Monomial p] -> Polynomial p
polynomial [Polynomial p -> Monomial p
forall c a. Polynom c a -> Monom c a
lt (Polynomial p -> Monomial p) -> Polynomial p -> Monomial p
forall a b. (a -> b) -> a -> b
$ [Polynomial p] -> Polynomial p
forall a. HasCallStack => [a] -> a
head [Polynomial p]
ps, Zp p -> Map Natural (Variable p) -> Monomial p
forall (p :: Natural).
Zp p -> Map Natural (Variable p) -> Monomial p
monomial (Zp p -> Zp p
forall a. AdditiveGroup a => a -> a
negate Zp p
forall a. MultiplicativeMonoid a => a
one) Map Natural (Variable p)
forall k a. Map k a
empty]