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')