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)