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