module ZkFold.Symbolic.GroebnerBasis.Internal.Types where import Data.List (foldl', intercalate) import Data.Map (Map, differenceWith, empty, intersectionWith, isSubmapOfBy, keys, toList, unionWith) import qualified Data.Map as Map import Numeric.Natural (Natural) import Prelude hiding (Num (..), drop, lcm, length, sum, take, (!!), (/)) import ZkFold.Base.Algebra.Basic.Class data VarType = VarTypeFree | VarTypeBound | VarTypeBoolean deriving VarType -> VarType -> Bool (VarType -> VarType -> Bool) -> (VarType -> VarType -> Bool) -> Eq VarType forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a $c== :: VarType -> VarType -> Bool == :: VarType -> VarType -> Bool $c/= :: VarType -> VarType -> Bool /= :: VarType -> VarType -> Bool Eq instance Show VarType where show :: VarType -> String show VarType VarTypeFree = String "Free" show VarType VarTypeBound = String "Bound" show VarType VarTypeBoolean = String "Boolean" data Var a c = Free a | Bound a Natural | Boolean Natural deriving (forall a b. (a -> b) -> Var a a -> Var a b) -> (forall a b. a -> Var a b -> Var a a) -> Functor (Var a) forall a b. a -> Var a b -> Var a a forall a b. (a -> b) -> Var a a -> Var a b forall a a b. a -> Var a b -> Var a a forall a a b. (a -> b) -> Var a a -> Var a b forall (f :: Type -> Type). (forall a b. (a -> b) -> f a -> f b) -> (forall a b. a -> f b -> f a) -> Functor f $cfmap :: forall a a b. (a -> b) -> Var a a -> Var a b fmap :: forall a b. (a -> b) -> Var a a -> Var a b $c<$ :: forall a a b. a -> Var a b -> Var a a <$ :: forall a b. a -> Var a b -> Var a a Functor instance (Show a, MultiplicativeMonoid a) => Show (Var a c) where show :: Var a c -> String show = a -> String forall a. Show a => a -> String show (a -> String) -> (Var a c -> a) -> Var a c -> String forall b c a. (b -> c) -> (a -> b) -> a -> c . Var a c -> a forall {k} a (c :: k). MultiplicativeMonoid a => Var a c -> a getPower instance (Eq a, MultiplicativeMonoid a) => Eq (Var a c) where == :: Var a c -> Var a c -> Bool (==) Var a c vx Var a c vy = Var a c -> a forall {k} a (c :: k). MultiplicativeMonoid a => Var a c -> a getPower Var a c vx a -> a -> Bool forall a. Eq a => a -> a -> Bool == Var a c -> a forall {k} a (c :: k). MultiplicativeMonoid a => Var a c -> a getPower Var a c vy instance (Ord a, MultiplicativeMonoid a) => Ord (Var a c) where compare :: Var a c -> Var a c -> Ordering compare Var a c vx Var a c vy = a -> a -> Ordering forall a. Ord a => a -> a -> Ordering compare (Var a c -> a forall {k} a (c :: k). MultiplicativeMonoid a => Var a c -> a getPower Var a c vx) (Var a c -> a forall {k} a (c :: k). MultiplicativeMonoid a => Var a c -> a getPower Var a c vy) getVarType :: Var a c -> VarType getVarType :: forall {k} a (c :: k). Var a c -> VarType getVarType (Free a _) = VarType VarTypeFree getVarType (Bound a _ Natural _) = VarType VarTypeBound getVarType (Boolean Natural _) = VarType VarTypeBoolean getPower :: MultiplicativeMonoid a => Var a c -> a getPower :: forall {k} a (c :: k). MultiplicativeMonoid a => Var a c -> a getPower (Bound a j Natural _) = a j getPower (Boolean Natural _) = a forall a. MultiplicativeMonoid a => a one getPower (Free a j) = a j setPower :: a -> Var a c -> Var a c setPower :: forall {k} a (c :: k). a -> Var a c -> Var a c setPower a j (Bound a _ Natural i) = a -> Natural -> Var a c forall {k} a (c :: k). a -> Natural -> Var a c Bound a j Natural i setPower a _ (Boolean Natural i) = Natural -> Var a c forall {k} a (c :: k). Natural -> Var a c Boolean Natural i setPower a j (Free a _) = a -> Var a c forall {k} a (c :: k). a -> Var a c Free a j getPoly :: Var a c -> Natural getPoly :: forall {k} a (c :: k). Var a c -> Natural getPoly (Bound a _ Natural p) = Natural p getPoly (Boolean Natural p) = Natural p getPoly Var a c _ = String -> Natural forall a. HasCallStack => String -> a error String "getPoly: VarType mismatch" data Monom a c = M c (Map Natural (Var a c)) deriving (Monom a c -> Monom a c -> Bool (Monom a c -> Monom a c -> Bool) -> (Monom a c -> Monom a c -> Bool) -> Eq (Monom a c) forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a forall a c. (Eq c, Eq a, MultiplicativeMonoid a) => Monom a c -> Monom a c -> Bool $c== :: forall a c. (Eq c, Eq a, MultiplicativeMonoid a) => Monom a c -> Monom a c -> Bool == :: Monom a c -> Monom a c -> Bool $c/= :: forall a c. (Eq c, Eq a, MultiplicativeMonoid a) => Monom a c -> Monom a c -> Bool /= :: Monom a c -> Monom a c -> Bool Eq, (forall a b. (a -> b) -> Monom a a -> Monom a b) -> (forall a b. a -> Monom a b -> Monom a a) -> Functor (Monom a) forall a b. a -> Monom a b -> Monom a a forall a b. (a -> b) -> Monom a a -> Monom a b forall a a b. a -> Monom a b -> Monom a a forall a a b. (a -> b) -> Monom a a -> Monom a b forall (f :: Type -> Type). (forall a b. (a -> b) -> f a -> f b) -> (forall a b. a -> f b -> f a) -> Functor f $cfmap :: forall a a b. (a -> b) -> Monom a a -> Monom a b fmap :: forall a b. (a -> b) -> Monom a a -> Monom a b $c<$ :: forall a a b. a -> Monom a b -> Monom a a <$ :: forall a b. a -> Monom a b -> Monom a a Functor) newtype Polynom a c = P [Monom a c] deriving (Polynom a c -> Polynom a c -> Bool (Polynom a c -> Polynom a c -> Bool) -> (Polynom a c -> Polynom a c -> Bool) -> Eq (Polynom a c) forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a forall a c. (Eq c, Eq a, MultiplicativeMonoid a) => Polynom a c -> Polynom a c -> Bool $c== :: forall a c. (Eq c, Eq a, MultiplicativeMonoid a) => Polynom a c -> Polynom a c -> Bool == :: Polynom a c -> Polynom a c -> Bool $c/= :: forall a c. (Eq c, Eq a, MultiplicativeMonoid a) => Polynom a c -> Polynom a c -> Bool /= :: Polynom a c -> Polynom a c -> Bool Eq, (forall a b. (a -> b) -> Polynom a a -> Polynom a b) -> (forall a b. a -> Polynom a b -> Polynom a a) -> Functor (Polynom a) forall a b. a -> Polynom a b -> Polynom a a forall a b. (a -> b) -> Polynom a a -> Polynom a b forall a a b. a -> Polynom a b -> Polynom a a forall a a b. (a -> b) -> Polynom a a -> Polynom a b forall (f :: Type -> Type). (forall a b. (a -> b) -> f a -> f b) -> (forall a b. a -> f b -> f a) -> Functor f $cfmap :: forall a a b. (a -> b) -> Polynom a a -> Polynom a b fmap :: forall a b. (a -> b) -> Polynom a a -> Polynom a b $c<$ :: forall a a b. a -> Polynom a b -> Polynom a a <$ :: forall a b. a -> Polynom a b -> Polynom a a Functor) instance (Show c, Eq c, FiniteField c, Show a, Eq a, AdditiveGroup a, MultiplicativeMonoid a) => Show (Monom a c) where show :: Monom a c -> String show (M c c Map Natural (Var a c) as) = (if c c c -> c -> Bool forall a. Eq a => a -> a -> Bool == c forall a. MultiplicativeMonoid a => a one then String "" else c -> String forall a. Show a => a -> String show c c) String -> ShowS forall a. [a] -> [a] -> [a] ++ String -> [String] -> String forall a. [a] -> [[a]] -> [a] intercalate String "∙" (((Natural, Var a c) -> String) -> [(Natural, Var a c)] -> [String] forall a b. (a -> b) -> [a] -> [b] map (Natural, Var a c) -> String showOne ([(Natural, Var a c)] -> [String]) -> [(Natural, Var a c)] -> [String] forall a b. (a -> b) -> a -> b $ Map Natural (Var a c) -> [(Natural, Var a c)] forall k a. Map k a -> [(k, a)] toList Map Natural (Var a c) as) where showOne :: (Natural, Var a c) -> String showOne :: (Natural, Var a c) -> String showOne (Natural i, Var a c p) = String "x" String -> ShowS forall a. [a] -> [a] -> [a] ++ Natural -> String forall a. Show a => a -> String show Natural i String -> ShowS forall a. [a] -> [a] -> [a] ++ (if Var a c -> a forall {k} a (c :: k). MultiplicativeMonoid a => Var a c -> a getPower Var a c p a -> a -> Bool forall a. Eq a => a -> a -> Bool == a forall a. MultiplicativeMonoid a => a one then String "" else String "^" String -> ShowS forall a. [a] -> [a] -> [a] ++ Var a c -> String forall a. Show a => a -> String show Var a c p) instance (Show c, Eq c, FiniteField c, Show a, Eq a, AdditiveGroup a, MultiplicativeMonoid a) => Show (Polynom a c) where show :: Polynom a c -> String show (P [Monom a c] ms) = String -> [String] -> String forall a. [a] -> [[a]] -> [a] intercalate String " + " ([String] -> String) -> [String] -> String forall a b. (a -> b) -> a -> b $ (Monom a c -> String) -> [Monom a c] -> [String] forall a b. (a -> b) -> [a] -> [b] map Monom a c -> String forall a. Show a => a -> String show [Monom a c] ms instance (AdditiveMonoid c, Eq c, Ord a, MultiplicativeMonoid a) => Ord (Monom a c) where compare :: Monom a c -> Monom a c -> Ordering compare (M c c1 Map Natural (Var a c) asl) (M c c2 Map Natural (Var a c) asr) | c c1 c -> c -> Bool forall a. Eq a => a -> a -> Bool == c forall a. AdditiveMonoid a => a zero Bool -> Bool -> Bool && c c2 c -> c -> Bool forall a. Eq a => a -> a -> Bool == c forall a. AdditiveMonoid a => a zero = Ordering EQ | c c1 c -> c -> Bool forall a. Eq a => a -> a -> Bool == c forall a. AdditiveMonoid a => a zero = Ordering LT | c c2 c -> c -> Bool forall a. Eq a => a -> a -> Bool == c forall a. AdditiveMonoid a => a zero = Ordering GT | Bool otherwise = [(Natural, Var a c)] -> [(Natural, Var a c)] -> Ordering forall {a} {a}. (Ord a, Ord a) => [(a, a)] -> [(a, a)] -> Ordering go (Map Natural (Var a c) -> [(Natural, Var a c)] forall k a. Map k a -> [(k, a)] toList Map Natural (Var a c) asl) (Map Natural (Var a c) -> [(Natural, Var a c)] forall k a. Map k a -> [(k, a)] toList Map Natural (Var a c) asr) where go :: [(a, a)] -> [(a, a)] -> Ordering go [] [] = Ordering EQ go [] [(a, a)] _ = Ordering LT go [(a, a)] _ [] = Ordering GT go ((a k1, a a1):[(a, a)] xs) ((a k2, a a2):[(a, a)] ys) | a k1 a -> a -> Bool forall a. Eq a => a -> a -> Bool == a k2 = if a a1 a -> a -> Bool forall a. Eq a => a -> a -> Bool == a a2 then [(a, a)] -> [(a, a)] -> Ordering go [(a, a)] xs [(a, a)] ys else a -> a -> Ordering forall a. Ord a => a -> a -> Ordering compare a a1 a a2 | Bool otherwise = a -> a -> Ordering forall a. Ord a => a -> a -> Ordering compare a k2 a k1 instance (AdditiveMonoid c, Eq c, Ord a, MultiplicativeMonoid a) => Ord (Polynom a c) where compare :: Polynom a c -> Polynom a c -> Ordering compare (P [Monom a c] l) (P [Monom a c] r) = [Monom a c] -> [Monom a c] -> Ordering forall a. Ord a => a -> a -> Ordering compare [Monom a c] l [Monom a c] r instance (Eq c, FiniteField c, Ord a, MultiplicativeMonoid a) => AdditiveSemigroup (Polynom a c) where P [Monom a c] l + :: Polynom a c -> Polynom a c -> Polynom a c + P [Monom 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 ([Monom a c] -> Polynom a c forall a c. [Monom a c] -> Polynom a c P [Monom a c] l) ([Monom a c] -> Polynom a c forall a c. [Monom a c] -> Polynom a c P [Monom a c] r) instance (Eq c, FiniteField c, Ord a, MultiplicativeMonoid a) => AdditiveMonoid (Polynom a c) where zero :: Polynom a c zero = [Monom a c] -> Polynom a c forall a c. [Monom a c] -> Polynom a c P [] instance (Eq c, FiniteField c, Ord a, MultiplicativeMonoid a) => AdditiveGroup (Polynom a c) where negate :: Polynom a c -> Polynom a c negate = Integer -> Polynom a c -> Polynom a c forall b a. Scale b a => b -> a -> a scale (-Integer 1 :: Integer) P [Monom a c] l - :: Polynom a c -> Polynom a c -> Polynom a c - P [Monom 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 ([Monom a c] -> Polynom a c forall a c. [Monom a c] -> Polynom a c P [Monom a c] l) (Polynom a c -> Polynom a c forall a. AdditiveGroup a => a -> a negate (Polynom a c -> Polynom a c) -> Polynom a c -> Polynom a c forall a b. (a -> b) -> a -> b $ [Monom a c] -> Polynom a c forall a c. [Monom a c] -> Polynom a c P [Monom a c] r) instance (Eq c, FiniteField c, Ord a, AdditiveGroup a, MultiplicativeMonoid a) => MultiplicativeSemigroup (Polynom a c) where P [Monom a c] l * :: Polynom a c -> Polynom a c -> Polynom a c * P [Monom a c] r = Polynom a c -> Polynom a c -> Polynom a c forall c a. (Eq c, FiniteField c, Ord a, AdditiveGroup a, MultiplicativeMonoid a) => Polynom a c -> Polynom a c -> Polynom a c mulM ([Monom a c] -> Polynom a c forall a c. [Monom a c] -> Polynom a c P [Monom a c] l) ([Monom a c] -> Polynom a c forall a c. [Monom a c] -> Polynom a c P [Monom a c] r) instance MultiplicativeMonoid (Polynom a c) => Exponent (Polynom a c) Natural where ^ :: Polynom a c -> Natural -> Polynom a c (^) = Polynom a c -> Natural -> Polynom a c forall a. MultiplicativeMonoid a => a -> Natural -> a natPow instance (Eq c, FiniteField c, Ord a, AdditiveGroup a, MultiplicativeMonoid a) => MultiplicativeMonoid (Polynom a c) where one :: Polynom a c one = [Monom a c] -> Polynom a c forall a c. [Monom a c] -> Polynom a c P [c -> Map Natural (Var a c) -> Monom a c forall a c. c -> Map Natural (Var a c) -> Monom a c M c forall a. MultiplicativeMonoid a => a one Map Natural (Var a c) forall k a. Map k a empty] lt :: Polynom c a -> Monom c a lt :: forall c a. Polynom c a -> Monom c a lt (P [Monom c a] as) = [Monom c a] -> Monom c a forall a. HasCallStack => [a] -> a head [Monom c a] as lv :: Polynom c a -> Natural lv :: forall c a. Polynom c a -> Natural lv Polynom c a p | Map Natural (Var c a) -> Bool forall a. Map Natural a -> Bool forall (t :: Type -> Type) a. Foldable t => t a -> Bool null Map Natural (Var c a) as = Natural 0 | Bool otherwise = [Natural] -> Natural forall a. HasCallStack => [a] -> a head ([Natural] -> Natural) -> [Natural] -> Natural forall a b. (a -> b) -> a -> b $ Map Natural (Var c a) -> [Natural] forall k a. Map k a -> [k] keys Map Natural (Var c a) as where M a _ Map Natural (Var c a) as = Polynom c a -> Monom c a forall c a. Polynom c a -> Monom c a lt Polynom c a p oneV :: (Eq a, AdditiveMonoid a, MultiplicativeMonoid a) => Var a c -> Bool oneV :: forall {k} a (c :: k). (Eq a, AdditiveMonoid a, MultiplicativeMonoid a) => Var a c -> Bool oneV Var a c v = Var a c -> a forall {k} a (c :: k). MultiplicativeMonoid a => Var a c -> a getPower Var a c v a -> a -> Bool forall a. Eq a => a -> a -> Bool == a forall a. AdditiveMonoid a => a zero zeroM :: (Eq c, FiniteField c) => Monom a c -> Bool zeroM :: forall c a. (Eq c, FiniteField c) => Monom a c -> Bool zeroM (M c c Map Natural (Var a c) _) = c c c -> c -> Bool forall a. Eq a => a -> a -> Bool == c forall a. AdditiveMonoid a => a zero zeroP :: Polynom a c -> Bool zeroP :: forall a c. Polynom a c -> Bool zeroP (P [Monom a c] as) = [Monom a c] -> Bool forall a. [a] -> Bool forall (t :: Type -> Type) a. Foldable t => t a -> Bool null [Monom a c] as addPower :: (AdditiveSemigroup a) => Var a c -> Var a c -> Var a c addPower :: forall {k} a (c :: k). AdditiveSemigroup a => Var a c -> Var a c -> Var a c addPower (Bound a x Natural p) (Bound a y Natural q) | Natural p Natural -> Natural -> Bool forall a. Eq a => a -> a -> Bool == Natural q = a -> Natural -> Var a c forall {k} a (c :: k). a -> Natural -> Var a c Bound (a x a -> a -> a forall a. AdditiveSemigroup a => a -> a -> a + a y) Natural p | Bool otherwise = String -> Var a c forall a. HasCallStack => String -> a error String "addPowers: VarType mismatch" addPower (Boolean Natural p) (Boolean Natural q) | Natural p Natural -> Natural -> Bool forall a. Eq a => a -> a -> Bool == Natural q = Natural -> Var a c forall {k} a (c :: k). Natural -> Var a c Boolean Natural p | Bool otherwise = String -> Var a c forall a. HasCallStack => String -> a error String "addPowers: VarType mismatch" addPower (Free a x) (Free a y) = a -> Var a c forall {k} a (c :: k). a -> Var a c Free (a x a -> a -> a forall a. AdditiveSemigroup a => a -> a -> a + a y) addPower Var a c _ Var a c _ = String -> Var a c forall a. HasCallStack => String -> a error String "addPowers: VarType mismatch" subPower :: AdditiveGroup a => Var a c -> Var a c -> Maybe (Var a c) subPower :: forall {k} a (c :: k). AdditiveGroup a => Var a c -> Var a c -> Maybe (Var a c) subPower (Bound a x Natural p) (Bound a y Natural q) | Natural p Natural -> Natural -> Bool forall a. Eq a => a -> a -> Bool == Natural q = Var a c -> Maybe (Var a c) forall a. a -> Maybe a Just (Var a c -> Maybe (Var a c)) -> Var a c -> Maybe (Var a c) forall a b. (a -> b) -> a -> b $ a -> Natural -> Var a c forall {k} a (c :: k). a -> Natural -> Var a c Bound (a x a -> a -> a forall a. AdditiveGroup a => a -> a -> a - a y) Natural p | Bool otherwise = String -> Maybe (Var a c) forall a. HasCallStack => String -> a error String "subPower: VarType mismatch" subPower (Boolean Natural p) (Boolean Natural q) | Natural p Natural -> Natural -> Bool forall a. Eq a => a -> a -> Bool == Natural q = Maybe (Var a c) forall a. Maybe a Nothing | Bool otherwise = String -> Maybe (Var a c) forall a. HasCallStack => String -> a error String "subPower: VarType mismatch" subPower (Free a x) (Free a y) = Var a c -> Maybe (Var a c) forall a. a -> Maybe a Just (Var a c -> Maybe (Var a c)) -> Var a c -> Maybe (Var a c) forall a b. (a -> b) -> a -> b $ a -> Var a c forall {k} a (c :: k). a -> Var a c Free (a x a -> a -> a forall a. AdditiveGroup a => a -> a -> a - a y) subPower Var a c _ Var a c _ = String -> Maybe (Var a c) forall a. HasCallStack => String -> a error String "subPower: VarType mismatch" similarM :: (Eq a, MultiplicativeMonoid a) => Monom a c -> Monom a c -> Bool similarM :: forall a c. (Eq a, MultiplicativeMonoid a) => Monom a c -> Monom a c -> Bool similarM (M c _ Map Natural (Var a c) asl) (M c _ Map Natural (Var a c) asr) = Map Natural (Var a c) asl Map Natural (Var a c) -> Map Natural (Var a c) -> Bool forall a. Eq a => a -> a -> Bool == Map Natural (Var a c) asr addSimilar :: FiniteField c => Monom a c -> Monom a c -> Monom a c addSimilar :: forall c a. FiniteField c => Monom a c -> Monom a c -> Monom a c addSimilar (M c cl Map Natural (Var a c) as) (M c cr Map Natural (Var a c) _) = c -> Map Natural (Var a c) -> Monom a c forall a c. c -> Map Natural (Var a c) -> Monom a c M (c clc -> c -> c forall a. AdditiveSemigroup a => a -> a -> a +c cr) Map Natural (Var a c) as addPoly :: (Eq c, FiniteField c, Ord a, MultiplicativeMonoid a) => Polynom a c -> Polynom a c -> Polynom a c addPoly :: forall c a. (Eq c, FiniteField c, Ord a, MultiplicativeMonoid a) => Polynom a c -> Polynom a c -> Polynom a c addPoly (P [Monom a c] l) (P [Monom a c] r) = [Monom a c] -> Polynom a c forall a c. [Monom a c] -> Polynom a c P ([Monom a c] -> Polynom a c) -> [Monom a c] -> Polynom a c forall a b. (a -> b) -> a -> b $ [Monom a c] -> [Monom a c] -> [Monom a c] forall {a} {c}. (Eq c, Finite c, Field c, Ord a, MultiplicativeMonoid a) => [Monom a c] -> [Monom a c] -> [Monom a c] go [Monom a c] l [Monom a c] r where go :: [Monom a c] -> [Monom a c] -> [Monom a c] go [] [] = [] go [Monom a c] as [] = [Monom a c] as go [] [Monom a c] bs = [Monom a c] bs go (Monom a c a:[Monom a c] as) (Monom a c b:[Monom a c] bs) | Monom a c -> Monom a c -> Bool forall a c. (Eq a, MultiplicativeMonoid a) => Monom a c -> Monom a c -> Bool similarM Monom a c a Monom a c b = if Monom a c -> Bool forall c a. (Eq c, FiniteField c) => Monom a c -> Bool zeroM (Monom a c -> Monom a c -> Monom a c forall c a. FiniteField c => Monom a c -> Monom a c -> Monom a c addSimilar Monom a c a Monom a c b) then [Monom a c] -> [Monom a c] -> [Monom a c] go [Monom a c] as [Monom a c] bs else Monom a c -> Monom a c -> Monom a c forall c a. FiniteField c => Monom a c -> Monom a c -> Monom a c addSimilar Monom a c a Monom a c b Monom a c -> [Monom a c] -> [Monom a c] forall a. a -> [a] -> [a] : [Monom a c] -> [Monom a c] -> [Monom a c] go [Monom a c] as [Monom a c] bs | Monom a c a Monom a c -> Monom a c -> Bool forall a. Ord a => a -> a -> Bool > Monom a c b = Monom a c a Monom a c -> [Monom a c] -> [Monom a c] forall a. a -> [a] -> [a] : [Monom a c] -> [Monom a c] -> [Monom a c] go [Monom a c] as (Monom a c bMonom a c -> [Monom a c] -> [Monom a c] forall a. a -> [a] -> [a] :[Monom a c] bs) | Bool otherwise = Monom a c b Monom a c -> [Monom a c] -> [Monom a c] forall a. a -> [a] -> [a] : [Monom a c] -> [Monom a c] -> [Monom a c] go (Monom a c aMonom a c -> [Monom a c] -> [Monom a c] forall a. a -> [a] -> [a] :[Monom a c] as) [Monom a c] bs mulMono :: (FiniteField c, AdditiveMonoid a) => Monom a c -> Monom a c -> Monom a c mulMono :: forall c a. (FiniteField c, AdditiveMonoid a) => Monom a c -> Monom a c -> Monom a c mulMono (M c cl Map Natural (Var a c) asl) (M c cr Map Natural (Var a c) asr) = c -> Map Natural (Var a c) -> Monom a c forall a c. c -> Map Natural (Var a c) -> Monom a c M (c clc -> c -> c forall a. MultiplicativeSemigroup a => a -> a -> a *c cr) ((Var a c -> Var a c -> Var a c) -> Map Natural (Var a c) -> Map Natural (Var a c) -> Map Natural (Var a c) forall k a. Ord k => (a -> a -> a) -> Map k a -> Map k a -> Map k a unionWith Var a c -> Var a c -> Var a c forall {k} a (c :: k). AdditiveSemigroup a => Var a c -> Var a c -> Var a c addPower Map Natural (Var a c) asl Map Natural (Var a c) asr) mulPM :: (FiniteField c, AdditiveMonoid a) => Polynom a c -> Monom a c -> Polynom a c mulPM :: forall c a. (FiniteField c, AdditiveMonoid a) => Polynom a c -> Monom a c -> Polynom a c mulPM (P [Monom a c] as) Monom a c m = [Monom a c] -> Polynom a c forall a c. [Monom a c] -> Polynom a c P ([Monom a c] -> Polynom a c) -> [Monom a c] -> Polynom a c forall a b. (a -> b) -> a -> b $ (Monom a c -> Monom a c) -> [Monom a c] -> [Monom a c] forall a b. (a -> b) -> [a] -> [b] map (Monom a c -> Monom a c -> Monom a c forall c a. (FiniteField c, AdditiveMonoid a) => Monom a c -> Monom a c -> Monom a c mulMono Monom a c m) [Monom a c] as mulM :: (Eq c, FiniteField c, Ord a, AdditiveGroup a, MultiplicativeMonoid a) => Polynom a c -> Polynom a c -> Polynom a c mulM :: forall c a. (Eq c, FiniteField c, Ord a, AdditiveGroup a, MultiplicativeMonoid a) => Polynom a c -> Polynom a c -> Polynom a c mulM (P [Monom a c] ml) Polynom a c r = (Polynom a c -> Polynom a c -> Polynom a c) -> Polynom a c -> [Polynom a c] -> Polynom a c 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' 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 ([Monom a c] -> Polynom a c forall a c. [Monom a c] -> Polynom a c P []) ([Polynom a c] -> Polynom a c) -> [Polynom a c] -> Polynom a c forall a b. (a -> b) -> a -> b $ (Monom a c -> Polynom a c) -> [Monom a c] -> [Polynom a c] forall a b. (a -> b) -> [a] -> [b] map (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] ml dividable :: (Ord a, MultiplicativeMonoid a) => Monom a c -> Monom a c -> Bool dividable :: forall a c. (Ord a, MultiplicativeMonoid a) => Monom a c -> Monom a c -> Bool dividable (M c _ Map Natural (Var a c) al) (M c _ Map Natural (Var a c) ar) = (Var a c -> Var a c -> Bool) -> Map Natural (Var a c) -> Map Natural (Var a c) -> Bool forall k a b. Ord k => (a -> b -> Bool) -> Map k a -> Map k b -> Bool isSubmapOfBy Var a c -> Var a c -> Bool forall a. Ord a => a -> a -> Bool (<=) Map Natural (Var a c) ar Map Natural (Var a c) al divideM :: (FiniteField c, Eq a, Ring a) => Monom a c -> Monom a c -> Monom a c divideM :: forall c a. (FiniteField c, Eq a, Ring a) => Monom a c -> Monom a c -> Monom a c divideM (M c cl Map Natural (Var a c) al) (M c cr Map Natural (Var a c) ar) = c -> Map Natural (Var a c) -> Monom a c forall a c. c -> Map Natural (Var a c) -> Monom a c M (c clc -> c -> c forall a. Field a => a -> a -> a //c cr) ((Var a c -> Bool) -> Map Natural (Var a c) -> Map Natural (Var a c) forall a k. (a -> Bool) -> Map k a -> Map k a Map.filter (Bool -> Bool not (Bool -> Bool) -> (Var a c -> Bool) -> Var a c -> Bool forall b c a. (b -> c) -> (a -> b) -> a -> c . Var a c -> Bool forall {k} a (c :: k). (Eq a, AdditiveMonoid a, MultiplicativeMonoid a) => Var a c -> Bool oneV) (Map Natural (Var a c) -> Map Natural (Var a c)) -> Map Natural (Var a c) -> Map Natural (Var a c) forall a b. (a -> b) -> a -> b $ (Var a c -> Var a c -> Maybe (Var a c)) -> Map Natural (Var a c) -> Map Natural (Var a c) -> Map Natural (Var a c) forall k a b. Ord k => (a -> b -> Maybe a) -> Map k a -> Map k b -> Map k a differenceWith Var a c -> Var a c -> Maybe (Var a c) forall {k} a (c :: k). AdditiveGroup a => Var a c -> Var a c -> Maybe (Var a c) subPower Map Natural (Var a c) al Map Natural (Var a c) ar) lcmM :: (FiniteField c, Ord a, MultiplicativeMonoid a) => Monom a c -> Monom a c -> Monom a c lcmM :: forall c a. (FiniteField c, Ord a, MultiplicativeMonoid a) => Monom a c -> Monom a c -> Monom a c lcmM (M c cl Map Natural (Var a c) al) (M c cr Map Natural (Var a c) ar) = c -> Map Natural (Var a c) -> Monom a c forall a c. c -> Map Natural (Var a c) -> Monom a c M (c clc -> c -> c forall a. MultiplicativeSemigroup a => a -> a -> a *c cr) ((Var a c -> Var a c -> Var a c) -> Map Natural (Var a c) -> Map Natural (Var a c) -> Map Natural (Var a c) forall k a. Ord k => (a -> a -> a) -> Map k a -> Map k a -> Map k a unionWith Var a c -> Var a c -> Var a c forall a. Ord a => a -> a -> a max Map Natural (Var a c) al Map Natural (Var a c) ar) gcdM :: (FiniteField c, Ord a, MultiplicativeMonoid a) => Monom a c -> Monom a c -> Monom a c gcdM :: forall c a. (FiniteField c, Ord a, MultiplicativeMonoid a) => Monom a c -> Monom a c -> Monom a c gcdM (M c cl Map Natural (Var a c) al) (M c cr Map Natural (Var a c) ar) = c -> Map Natural (Var a c) -> Monom a c forall a c. c -> Map Natural (Var a c) -> Monom a c M (c clc -> c -> c forall a. MultiplicativeSemigroup a => a -> a -> a *c cr) ((Var a c -> Var a c -> Var a c) -> Map Natural (Var a c) -> Map Natural (Var a c) -> Map Natural (Var a c) forall k a b c. Ord k => (a -> b -> c) -> Map k a -> Map k b -> Map k c intersectionWith Var a c -> Var a c -> Var a c forall a. Ord a => a -> a -> a min Map Natural (Var a c) al Map Natural (Var a c) ar)