    -- Copyright (c) 2011-2015, David Amos. All rights reserved.

    {-# LANGUAGE GeneralizedNewtypeDeriving, MultiParamTypeClasses, FlexibleInstances, DeriveFunctor #-}

    -- |A module defining the algebra of commutative polynomials over a field k.
    -- Polynomials are represented as the free k-vector space with the monomials as basis.
    --
    -- A monomial ordering is required to specify how monomials are to be ordered.
    -- The Lex, Glex, and Grevlex monomial orders are defined, with the possibility to add others.
    --
    -- In order to make use of this module, some variables must be defined, for example:
    --
    -- > [t,u,v,x,y,z] = map glexvar ["t","u","v","x","y","z"]
    module Math.CommutativeAlgebra.Polynomial where

    import Prelude hiding ( (*>) )

    import Math.Core.Field
    import Math.Core.Utils (toSet)
    import Math.Algebras.VectorSpace
    import Math.Algebras.TensorProduct
    import Math.Algebras.Structures

    -- |In order to work with monomials, we need to be able to multiply them and divide them.
    -- Multiplication is defined by the Mon (monoid) class. Division is defined in this class.
    -- The functions here are primarily intended for internal use only.
    class (Eq m, Show m, Mon m) => Monomial m where
        mdivides :: m -> m -> Bool
        mdiv :: m -> m -> m
        mgcd :: m -> m -> m
        mlcm :: m -> m -> m
        mcoprime :: m -> m -> Bool
        mdeg :: m -> Int

    -- mlcm m1 m2 = let m = mgcd m1 m2 in mmult m1 (mdiv m2 m)

    mproperlydivides :: m -> m -> Bool
    mproperlydivides m1 :: m
    m1 m2 :: m
    m2 = m
    m1 m -> m -> Bool
    forall a. Eq a => a -> a -> Bool
    /= m
    m2 Bool -> Bool -> Bool
    && m -> m -> Bool
    forall m. Monomial m => m -> m -> Bool
    mdivides m
    m1 m
    m2

    -- |We want to be able to construct monomials over any set of variables that we choose.
    -- Although we will often use String as the type of our variables,
    -- it is useful to define polymorphic types for monomials.
    class MonomialConstructor m where
        mvar :: v -> m v
        mindices :: m v -> [(v,Int)]

    -- |@var v@ creates a variable in the vector space of polynomials.
    -- For example, if we want to work in Q[x,y,z], we might define:
    --
    -- > [x,y,z] = map var ["x","y","z"] :: [GlexPoly Q String]
    --
    -- Notice that, in general, it is necessary to provide a type annotation so that
    -- the compiler knows which field and which term order to use.
    var :: (Num k, MonomialConstructor m) => v -> Vect k (m v)
    var :: v -> Vect k (m v)
    var = m v -> Vect k (m v)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (m v -> Vect k (m v)) -> (v -> m v) -> v -> Vect k (m v)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . v -> m v
    forall (m :: * -> *) v. MonomialConstructor m => v -> m v
    mvar

    -- class MonomialOrder m where
    --     isGraded :: m -> Bool

    -- MONOMIALS

    -- |The underlying implementation of monomials in variables of type v. Most often, we will be interested in MonImpl String,
    -- with the variable \"x\" represented by M 1 [(\"x\",1)]. However, other types can be used instead.
    --
    -- No Ord instance is defined for MonImpl v, so it cannot be used as the basis for a free vector space of polynomials.
    -- Instead, several different newtype wrappers are provided, corresponding to different monomial orderings.
    data MonImpl v = M Int [(v,Int)] deriving (MonImpl v -> MonImpl v -> Bool
    (MonImpl v -> MonImpl v -> Bool)
    -> (MonImpl v -> MonImpl v -> Bool) -> Eq (MonImpl v)
    forall v. Eq v => MonImpl v -> MonImpl v -> Bool
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    /= :: MonImpl v -> MonImpl v -> Bool
    $c/= :: forall v. Eq v => MonImpl v -> MonImpl v -> Bool
    == :: MonImpl v -> MonImpl v -> Bool
    $c== :: forall v. Eq v => MonImpl v -> MonImpl v -> Bool
    Eq, a -> MonImpl b -> MonImpl a
    (a -> b) -> MonImpl a -> MonImpl b
    (forall a b. (a -> b) -> MonImpl a -> MonImpl b)
    -> (forall a b. a -> MonImpl b -> MonImpl a) -> Functor MonImpl
    forall a b. a -> MonImpl b -> MonImpl a
    forall a b. (a -> b) -> MonImpl a -> MonImpl b
    forall (f :: * -> *).
    (forall a b. (a -> b) -> f a -> f b)
    -> (forall a b. a -> f b -> f a) -> Functor f
    <$ :: a -> MonImpl b -> MonImpl a
    $c<$ :: forall a b. a -> MonImpl b -> MonImpl a
    fmap :: (a -> b) -> MonImpl a -> MonImpl b
    $cfmap :: forall a b. (a -> b) -> MonImpl a -> MonImpl b
    Functor)
    -- The initial Int is the degree of the monomial. Storing it speeds up equality tests and comparisons

    instance Show v => Show (MonImpl v) where
        show :: MonImpl v -> String
    show (M _ []) = "1"
        show (M _ xis :: [(v, Int)]
    xis) = ((v, Int) -> String) -> [(v, Int)] -> String
    forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
    concatMap (\(x :: v
    x,i :: Int
    i) -> if Int
    iInt -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    ==1 then v -> String
    forall a. Show a => a -> String
    showVar v
    x else v -> String
    forall a. Show a => a -> String
    showVar v
    x String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ "^" String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Int -> String
    forall a. Show a => a -> String
    show Int
    i) [(v, Int)]
    xis
            where showVar :: a -> String
    showVar x :: a
    x = (Char -> Bool) -> ShowS
    forall a. (a -> Bool) -> [a] -> [a]
    filter ( Char -> Char -> Bool
    forall a. Eq a => a -> a -> Bool
    /= '"' ) (a -> String
    forall a. Show a => a -> String
    show a
    x) -- in case v == String

    instance (Ord v) => Mon (MonImpl v) where
        munit :: MonImpl v
    munit = Int -> [(v, Int)] -> MonImpl v
    forall v. Int -> [(v, Int)] -> MonImpl v
    M 0 []
        mmult :: MonImpl v -> MonImpl v -> MonImpl v
    mmult (M si :: Int
    si xis :: [(v, Int)]
    xis) (M sj :: Int
    sj yjs :: [(v, Int)]
    yjs) = Int -> [(v, Int)] -> MonImpl v
    forall v. Int -> [(v, Int)] -> MonImpl v
    M (Int
    siInt -> Int -> Int
    forall a. Num a => a -> a -> a
    +Int
    sj) ([(v, Int)] -> MonImpl v) -> [(v, Int)] -> MonImpl v
    forall a b. (a -> b) -> a -> b
    $ [(v, Int)] -> [(v, Int)] -> [(v, Int)]
    forall a b.
    (Ord a, Num b, Eq b) =>
    [(a, b)] -> [(a, b)] -> [(a, b)]
    addmerge [(v, Int)]
    xis [(v, Int)]
    yjs

    instance (Ord v, Show v) => Monomial (MonImpl v) where
        mdivides :: MonImpl v -> MonImpl v -> Bool
    mdivides (M si :: Int
    si xis :: [(v, Int)]
    xis) (M sj :: Int
    sj yjs :: [(v, Int)]
    yjs) = Int
    si Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    <= Int
    sj Bool -> Bool -> Bool
    && [(v, Int)] -> [(v, Int)] -> Bool
    forall a a. (Ord a, Ord a) => [(a, a)] -> [(a, a)] -> Bool
    mdivides' [(v, Int)]
    xis [(v, Int)]
    yjs where
            mdivides' :: [(a, a)] -> [(a, a)] -> Bool
    mdivides' ((x :: a
    x,i :: a
    i):xis :: [(a, a)]
    xis) ((y :: a
    y,j :: a
    j):yjs :: [(a, a)]
    yjs) =
                case a -> a -> Ordering
    forall a. Ord a => a -> a -> Ordering
    compare a
    x a
    y of
                LT -> Bool
    False
                GT -> [(a, a)] -> [(a, a)] -> Bool
    mdivides' ((a
    x,a
    i)(a, a) -> [(a, a)] -> [(a, a)]
    forall a. a -> [a] -> [a]
    :[(a, a)]
    xis) [(a, a)]
    yjs
                EQ -> if a
    ia -> a -> Bool
    forall a. Ord a => a -> a -> Bool
    <=a
    j then [(a, a)] -> [(a, a)] -> Bool
    mdivides' [(a, a)]
    xis [(a, a)]
    yjs else Bool
    False
            mdivides' [] _ = Bool
    True
            mdivides' _ [] = Bool
    False
        mdiv :: MonImpl v -> MonImpl v -> MonImpl v
    mdiv (M si :: Int
    si xis :: [(v, Int)]
    xis) (M sj :: Int
    sj yjs :: [(v, Int)]
    yjs) = Int -> [(v, Int)] -> MonImpl v
    forall v. Int -> [(v, Int)] -> MonImpl v
    M (Int
    siInt -> Int -> Int
    forall a. Num a => a -> a -> a
    -Int
    sj) ([(v, Int)] -> MonImpl v) -> [(v, Int)] -> MonImpl v
    forall a b. (a -> b) -> a -> b
    $ [(v, Int)] -> [(v, Int)] -> [(v, Int)]
    forall a b.
    (Ord a, Num b, Eq b) =>
    [(a, b)] -> [(a, b)] -> [(a, b)]
    addmerge [(v, Int)]
    xis ([(v, Int)] -> [(v, Int)]) -> [(v, Int)] -> [(v, Int)]
    forall a b. (a -> b) -> a -> b
    $ ((v, Int) -> (v, Int)) -> [(v, Int)] -> [(v, Int)]
    forall a b. (a -> b) -> [a] -> [b]
    map (\(y :: v
    y,j :: Int
    j) -> (v
    y,-Int
    j)) [(v, Int)]
    yjs
        -- we don't check that the result has no negative indices
        mgcd :: MonImpl v -> MonImpl v -> MonImpl v
    mgcd (M _ xis :: [(v, Int)]
    xis) (M _ yjs :: [(v, Int)]
    yjs) = Int -> [(v, Int)] -> [(v, Int)] -> [(v, Int)] -> MonImpl v
    forall v.
    Ord v =>
    Int -> [(v, Int)] -> [(v, Int)] -> [(v, Int)] -> MonImpl v
    mgcd' 0 [] [(v, Int)]
    xis [(v, Int)]
    yjs
            where mgcd' :: Int -> [(v, Int)] -> [(v, Int)] -> [(v, Int)] -> MonImpl v
    mgcd' s :: Int
    s zks :: [(v, Int)]
    zks ((x :: v
    x,i :: Int
    i):xis :: [(v, Int)]
    xis) ((y :: v
    y,j :: Int
    j):yjs :: [(v, Int)]
    yjs) =
                      case v -> v -> Ordering
    forall a. Ord a => a -> a -> Ordering
    compare v
    x v
    y of
                      LT -> Int -> [(v, Int)] -> [(v, Int)] -> [(v, Int)] -> MonImpl v
    mgcd' Int
    s [(v, Int)]
    zks [(v, Int)]
    xis ((v
    y,Int
    j)(v, Int) -> [(v, Int)] -> [(v, Int)]
    forall a. a -> [a] -> [a]
    :[(v, Int)]
    yjs)
                      GT -> Int -> [(v, Int)] -> [(v, Int)] -> [(v, Int)] -> MonImpl v
    mgcd' Int
    s [(v, Int)]
    zks ((v
    x,Int
    i)(v, Int) -> [(v, Int)] -> [(v, Int)]
    forall a. a -> [a] -> [a]
    :[(v, Int)]
    xis) [(v, Int)]
    yjs
                      EQ -> let k :: Int
    k = Int -> Int -> Int
    forall a. Ord a => a -> a -> a
    min Int
    i Int
    j in Int -> [(v, Int)] -> [(v, Int)] -> [(v, Int)] -> MonImpl v
    mgcd' (Int
    sInt -> Int -> Int
    forall a. Num a => a -> a -> a
    +Int
    k) ((v
    x,Int
    k)(v, Int) -> [(v, Int)] -> [(v, Int)]
    forall a. a -> [a] -> [a]
    :[(v, Int)]
    zks) [(v, Int)]
    xis [(v, Int)]
    yjs
                  mgcd' s :: Int
    s zks :: [(v, Int)]
    zks _ _ = Int -> [(v, Int)] -> MonImpl v
    forall v. Int -> [(v, Int)] -> MonImpl v
    M Int
    s ([(v, Int)] -> [(v, Int)]
    forall a. [a] -> [a]
    reverse [(v, Int)]
    zks)
        mlcm :: MonImpl v -> MonImpl v -> MonImpl v
    mlcm (M si :: Int
    si xis :: [(v, Int)]
    xis) (M sj :: Int
    sj yjs :: [(v, Int)]
    yjs) = Int -> [(v, Int)] -> [(v, Int)] -> [(v, Int)] -> MonImpl v
    forall v.
    Ord v =>
    Int -> [(v, Int)] -> [(v, Int)] -> [(v, Int)] -> MonImpl v
    mlcm' 0 [] [(v, Int)]
    xis [(v, Int)]
    yjs
            where mlcm' :: Int -> [(v, Int)] -> [(v, Int)] -> [(v, Int)] -> MonImpl v
    mlcm' s :: Int
    s zks :: [(v, Int)]
    zks ((x :: v
    x,i :: Int
    i):xis :: [(v, Int)]
    xis) ((y :: v
    y,j :: Int
    j):yjs :: [(v, Int)]
    yjs) =
                      case v -> v -> Ordering
    forall a. Ord a => a -> a -> Ordering
    compare v
    x v
    y of
                      LT -> Int -> [(v, Int)] -> [(v, Int)] -> [(v, Int)] -> MonImpl v
    mlcm' (Int
    sInt -> Int -> Int
    forall a. Num a => a -> a -> a
    +Int
    i) ((v
    x,Int
    i)(v, Int) -> [(v, Int)] -> [(v, Int)]
    forall a. a -> [a] -> [a]
    :[(v, Int)]
    zks) [(v, Int)]
    xis ((v
    y,Int
    j)(v, Int) -> [(v, Int)] -> [(v, Int)]
    forall a. a -> [a] -> [a]
    :[(v, Int)]
    yjs)
                      GT -> Int -> [(v, Int)] -> [(v, Int)] -> [(v, Int)] -> MonImpl v
    mlcm' (Int
    sInt -> Int -> Int
    forall a. Num a => a -> a -> a
    +Int
    j) ((v
    y,Int
    j)(v, Int) -> [(v, Int)] -> [(v, Int)]
    forall a. a -> [a] -> [a]
    :[(v, Int)]
    zks) ((v
    x,Int
    i)(v, Int) -> [(v, Int)] -> [(v, Int)]
    forall a. a -> [a] -> [a]
    :[(v, Int)]
    xis) [(v, Int)]
    yjs
                      EQ -> let k :: Int
    k = Int -> Int -> Int
    forall a. Ord a => a -> a -> a
    max Int
    i Int
    j in Int -> [(v, Int)] -> [(v, Int)] -> [(v, Int)] -> MonImpl v
    mlcm' (Int
    sInt -> Int -> Int
    forall a. Num a => a -> a -> a
    +Int
    k) ((v
    x,Int
    k)(v, Int) -> [(v, Int)] -> [(v, Int)]
    forall a. a -> [a] -> [a]
    :[(v, Int)]
    zks) [(v, Int)]
    xis [(v, Int)]
    yjs
                  mlcm' s :: Int
    s zks :: [(v, Int)]
    zks xis :: [(v, Int)]
    xis yjs :: [(v, Int)]
    yjs = let zks' :: [(v, Int)]
    zks' = [(v, Int)]
    xis [(v, Int)] -> [(v, Int)] -> [(v, Int)]
    forall a. [a] -> [a] -> [a]
    ++ [(v, Int)]
    yjs; s' :: Int
    s' = [Int] -> Int
    forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
    sum (((v, Int) -> Int) -> [(v, Int)] -> [Int]
    forall a b. (a -> b) -> [a] -> [b]
    map (v, Int) -> Int
    forall a b. (a, b) -> b
    snd [(v, Int)]
    zks') -- either xis or yjs is null
                                        in Int -> [(v, Int)] -> MonImpl v
    forall v. Int -> [(v, Int)] -> MonImpl v
    M (Int
    sInt -> Int -> Int
    forall a. Num a => a -> a -> a
    +Int
    s') ([(v, Int)] -> [(v, Int)]
    forall a. [a] -> [a]
    reverse [(v, Int)]
    zks [(v, Int)] -> [(v, Int)] -> [(v, Int)]
    forall a. [a] -> [a] -> [a]
    ++ [(v, Int)]
    zks')
        mcoprime :: MonImpl v -> MonImpl v -> Bool
    mcoprime (M _ xis :: [(v, Int)]
    xis) (M _ yjs :: [(v, Int)]
    yjs) = [(v, Int)] -> [(v, Int)] -> Bool
    forall a b b. Ord a => [(a, b)] -> [(a, b)] -> Bool
    mcoprime' [(v, Int)]
    xis [(v, Int)]
    yjs
            where mcoprime' :: [(a, b)] -> [(a, b)] -> Bool
    mcoprime' ((x :: a
    x,i :: b
    i):xis :: [(a, b)]
    xis) ((y :: a
    y,j :: b
    j):yjs :: [(a, b)]
    yjs) =
                      case a -> a -> Ordering
    forall a. Ord a => a -> a -> Ordering
    compare a
    x a
    y of
                      LT -> [(a, b)] -> [(a, b)] -> Bool
    mcoprime' [(a, b)]
    xis ((a
    y,b
    j)(a, b) -> [(a, b)] -> [(a, b)]
    forall a. a -> [a] -> [a]
    :[(a, b)]
    yjs)
                      GT -> [(a, b)] -> [(a, b)] -> Bool
    mcoprime' ((a
    x,b
    i)(a, b) -> [(a, b)] -> [(a, b)]
    forall a. a -> [a] -> [a]
    :[(a, b)]
    xis) [(a, b)]
    yjs
                      EQ -> Bool
    False
                  mcoprime' _ _ = Bool
    True
        -- mcoprime m1 m2 = mgcd m1 m2 == munit
        mdeg :: MonImpl v -> Int
    mdeg (M s :: Int
    s _) = Int
    s

    instance MonomialConstructor MonImpl where
        mvar :: v -> MonImpl v
    mvar v :: v
    v = Int -> [(v, Int)] -> MonImpl v
    forall v. Int -> [(v, Int)] -> MonImpl v
    M 1 [(v
    v,1)]
        mindices :: MonImpl v -> [(v, Int)]
    mindices (M si :: Int
    si xis :: [(v, Int)]
    xis) = [(v, Int)]
    xis

    -- LEX ORDER

    -- |A type representing monomials with Lex ordering.
    --
    -- Lex stands for lexicographic ordering.
    -- For example, in Lex ordering, monomials up to degree two would be ordered as follows: x^2+xy+xz+x+y^2+yz+y+z^2+z+1.
    newtype Lex v = Lex (MonImpl v) deriving (Lex v -> Lex v -> Bool
    (Lex v -> Lex v -> Bool) -> (Lex v -> Lex v -> Bool) -> Eq (Lex v)
    forall v. Eq v => Lex v -> Lex v -> Bool
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    /= :: Lex v -> Lex v -> Bool
    $c/= :: forall v. Eq v => Lex v -> Lex v -> Bool
    == :: Lex v -> Lex v -> Bool
    $c== :: forall v. Eq v => Lex v -> Lex v -> Bool
    Eq, a -> Lex b -> Lex a
    (a -> b) -> Lex a -> Lex b
    (forall a b. (a -> b) -> Lex a -> Lex b)
    -> (forall a b. a -> Lex b -> Lex a) -> Functor Lex
    forall a b. a -> Lex b -> Lex a
    forall a b. (a -> b) -> Lex a -> Lex b
    forall (f :: * -> *).
    (forall a b. (a -> b) -> f a -> f b)
    -> (forall a b. a -> f b -> f a) -> Functor f
    <$ :: a -> Lex b -> Lex a
    $c<$ :: forall a b. a -> Lex b -> Lex a
    fmap :: (a -> b) -> Lex a -> Lex b
    $cfmap :: forall a b. (a -> b) -> Lex a -> Lex b
    Functor, Lex v
    Lex v -> Lex v -> Lex v
    Lex v -> (Lex v -> Lex v -> Lex v) -> Mon (Lex v)
    forall m. m -> (m -> m -> m) -> Mon m
    forall v. Ord v => Lex v
    forall v. Ord v => Lex v -> Lex v -> Lex v
    mmult :: Lex v -> Lex v -> Lex v
    $cmmult :: forall v. Ord v => Lex v -> Lex v -> Lex v
    munit :: Lex v
    $cmunit :: forall v. Ord v => Lex v
    Mon, Eq (Lex v)
    Show (Lex v)
    Mon (Lex v)
    (Eq (Lex v), Show (Lex v), Mon (Lex v)) =>
    (Lex v -> Lex v -> Bool)
    -> (Lex v -> Lex v -> Lex v)
    -> (Lex v -> Lex v -> Lex v)
    -> (Lex v -> Lex v -> Lex v)
    -> (Lex v -> Lex v -> Bool)
    -> (Lex v -> Int)
    -> Monomial (Lex v)
    Lex v -> Int
    Lex v -> Lex v -> Bool
    Lex v -> Lex v -> Lex v
    forall m.
    (Eq m, Show m, Mon m) =>
    (m -> m -> Bool)
    -> (m -> m -> m)
    -> (m -> m -> m)
    -> (m -> m -> m)
    -> (m -> m -> Bool)
    -> (m -> Int)
    -> Monomial m
    forall v. (Ord v, Show v) => Eq (Lex v)
    forall v. (Ord v, Show v) => Show (Lex v)
    forall v. (Ord v, Show v) => Mon (Lex v)
    forall v. (Ord v, Show v) => Lex v -> Int
    forall v. (Ord v, Show v) => Lex v -> Lex v -> Bool
    forall v. (Ord v, Show v) => Lex v -> Lex v -> Lex v
    mdeg :: Lex v -> Int
    $cmdeg :: forall v. (Ord v, Show v) => Lex v -> Int
    mcoprime :: Lex v -> Lex v -> Bool
    $cmcoprime :: forall v. (Ord v, Show v) => Lex v -> Lex v -> Bool
    mlcm :: Lex v -> Lex v -> Lex v
    $cmlcm :: forall v. (Ord v, Show v) => Lex v -> Lex v -> Lex v
    mgcd :: Lex v -> Lex v -> Lex v
    $cmgcd :: forall v. (Ord v, Show v) => Lex v -> Lex v -> Lex v
    mdiv :: Lex v -> Lex v -> Lex v
    $cmdiv :: forall v. (Ord v, Show v) => Lex v -> Lex v -> Lex v
    mdivides :: Lex v -> Lex v -> Bool
    $cmdivides :: forall v. (Ord v, Show v) => Lex v -> Lex v -> Bool
    $cp3Monomial :: forall v. (Ord v, Show v) => Mon (Lex v)
    $cp2Monomial :: forall v. (Ord v, Show v) => Show (Lex v)
    $cp1Monomial :: forall v. (Ord v, Show v) => Eq (Lex v)
    Monomial, v -> Lex v
    Lex v -> [(v, Int)]
    (forall v. v -> Lex v)
    -> (forall v. Lex v -> [(v, Int)]) -> MonomialConstructor Lex
    forall v. v -> Lex v
    forall v. Lex v -> [(v, Int)]
    forall (m :: * -> *).
    (forall v. v -> m v)
    -> (forall v. m v -> [(v, Int)]) -> MonomialConstructor m
    mindices :: Lex v -> [(v, Int)]
    $cmindices :: forall v. Lex v -> [(v, Int)]
    mvar :: v -> Lex v
    $cmvar :: forall v. v -> Lex v
    MonomialConstructor) -- GeneralizedNewtypeDeriving

    instance Show v => Show (Lex v) where
        show :: Lex v -> String
    show (Lex m :: MonImpl v
    m) = MonImpl v -> String
    forall a. Show a => a -> String
    show MonImpl v
    m

    instance Ord v => Ord (Lex v) where
        compare :: Lex v -> Lex v -> Ordering
    compare (Lex (M si :: Int
    si xis :: [(v, Int)]
    xis)) (Lex (M sj :: Int
    sj yjs :: [(v, Int)]
    yjs)) = [(v, Int)] -> [(v, Int)] -> Ordering
    forall a a. (Ord a, Ord a) => [(a, a)] -> [(a, a)] -> Ordering
    compare' [(v, Int)]
    xis [(v, Int)]
    yjs
            where compare' :: [(a, a)] -> [(a, a)] -> Ordering
    compare' ((x :: a
    x,i :: a
    i):xis :: [(a, a)]
    xis) ((y :: a
    y,j :: a
    j):yjs :: [(a, a)]
    yjs) =
                      case a -> a -> Ordering
    forall a. Ord a => a -> a -> Ordering
    compare a
    x a
    y of
                      LT -> Ordering
    LT
                      GT -> Ordering
    GT
                      EQ -> case a -> a -> Ordering
    forall a. Ord a => a -> a -> Ordering
    compare a
    i a
    j of
                            LT -> Ordering
    GT
                            GT -> Ordering
    LT
                            EQ -> [(a, a)] -> [(a, a)] -> Ordering
    compare' [(a, a)]
    xis [(a, a)]
    yjs
                  compare' [] [] = Ordering
    EQ
                  compare' _ [] = Ordering
    LT
                  compare' [] _ = Ordering
    GT
            -- unfortunately we can't use the following, because we want [] sorted after everything, not before
            -- compare [(x,-i) | (x,i) <- xis] [(y,-j) | (y,j) <- yjs]

    -- instance MonomialOrder Lex where isGraded _ = False

    -- |A type representing polynomials with Lex term ordering.
    type LexPoly k v = Vect k (Lex v)

    -- |@lexvar v@ creates a variable in the algebra of commutative polynomials over Q with Lex term ordering.
    -- It is provided as a shortcut, to avoid having to provide a type annotation, as with @var@.
    -- For example, the following code creates variables called x, y and z:
    --
    -- > [x,y,z] = map lexvar ["x","y","z"]
    lexvar :: v -> LexPoly Q v
    lexvar :: v -> LexPoly Q v
    lexvar v :: v
    v = Lex v -> LexPoly Q v
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Lex v -> LexPoly Q v) -> Lex v -> LexPoly Q v
    forall a b. (a -> b) -> a -> b
    $ MonImpl v -> Lex v
    forall v. MonImpl v -> Lex v
    Lex (MonImpl v -> Lex v) -> MonImpl v -> Lex v
    forall a b. (a -> b) -> a -> b
    $ Int -> [(v, Int)] -> MonImpl v
    forall v. Int -> [(v, Int)] -> MonImpl v
    M 1 [(v
    v,1)]
    -- lexvar = var

    instance (Eq k, Num k, Ord v, Show v) => Algebra k (Lex v) where
        unit :: k -> Vect k (Lex v)
    unit x :: k
    x = k
    x k -> Vect k (Lex v) -> Vect k (Lex v)
    forall k b. (Eq k, Num k) => k -> Vect k b -> Vect k b
    *> Lex v -> Vect k (Lex v)
    forall (m :: * -> *) a. Monad m => a -> m a
    return Lex v
    forall m. Mon m => m
    munit
        mult :: Vect k (Tensor (Lex v) (Lex v)) -> Vect k (Lex v)
    mult xy :: Vect k (Tensor (Lex v) (Lex v))
    xy = Vect k (Lex v) -> Vect k (Lex v)
    forall k b. (Eq k, Num k, Ord b) => Vect k b -> Vect k b
    nf (Vect k (Lex v) -> Vect k (Lex v))
    -> Vect k (Lex v) -> Vect k (Lex v)
    forall a b. (a -> b) -> a -> b
    $ (Tensor (Lex v) (Lex v) -> Lex v)
    -> Vect k (Tensor (Lex v) (Lex v)) -> Vect k (Lex v)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (\(a :: Lex v
    a,b :: Lex v
    b) -> Lex v
    a Lex v -> Lex v -> Lex v
    forall m. Mon m => m -> m -> m
    `mmult` Lex v
    b) Vect k (Tensor (Lex v) (Lex v))
    xy

    -- GLEX ORDER

    -- |A type representing monomials with Glex ordering.
    --
    -- Glex stands for graded lexicographic. Thus monomials are ordered first by degree, then by lexicographic order.
    -- For example, in Glex ordering, monomials up to degree two would be ordered as follows: x^2+xy+xz+y^2+yz+z^2+x+y+z+1.
    newtype Glex v = Glex (MonImpl v) deriving (Glex v -> Glex v -> Bool
    (Glex v -> Glex v -> Bool)
    -> (Glex v -> Glex v -> Bool) -> Eq (Glex v)
    forall v. Eq v => Glex v -> Glex v -> Bool
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    /= :: Glex v -> Glex v -> Bool
    $c/= :: forall v. Eq v => Glex v -> Glex v -> Bool
    == :: Glex v -> Glex v -> Bool
    $c== :: forall v. Eq v => Glex v -> Glex v -> Bool
    Eq, a -> Glex b -> Glex a
    (a -> b) -> Glex a -> Glex b
    (forall a b. (a -> b) -> Glex a -> Glex b)
    -> (forall a b. a -> Glex b -> Glex a) -> Functor Glex
    forall a b. a -> Glex b -> Glex a
    forall a b. (a -> b) -> Glex a -> Glex b
    forall (f :: * -> *).
    (forall a b. (a -> b) -> f a -> f b)
    -> (forall a b. a -> f b -> f a) -> Functor f
    <$ :: a -> Glex b -> Glex a
    $c<$ :: forall a b. a -> Glex b -> Glex a
    fmap :: (a -> b) -> Glex a -> Glex b
    $cfmap :: forall a b. (a -> b) -> Glex a -> Glex b
    Functor, Glex v
    Glex v -> Glex v -> Glex v
    Glex v -> (Glex v -> Glex v -> Glex v) -> Mon (Glex v)
    forall m. m -> (m -> m -> m) -> Mon m
    forall v. Ord v => Glex v
    forall v. Ord v => Glex v -> Glex v -> Glex v
    mmult :: Glex v -> Glex v -> Glex v
    $cmmult :: forall v. Ord v => Glex v -> Glex v -> Glex v
    munit :: Glex v
    $cmunit :: forall v. Ord v => Glex v
    Mon, Eq (Glex v)
    Show (Glex v)
    Mon (Glex v)
    (Eq (Glex v), Show (Glex v), Mon (Glex v)) =>
    (Glex v -> Glex v -> Bool)
    -> (Glex v -> Glex v -> Glex v)
    -> (Glex v -> Glex v -> Glex v)
    -> (Glex v -> Glex v -> Glex v)
    -> (Glex v -> Glex v -> Bool)
    -> (Glex v -> Int)
    -> Monomial (Glex v)
    Glex v -> Int
    Glex v -> Glex v -> Bool
    Glex v -> Glex v -> Glex v
    forall m.
    (Eq m, Show m, Mon m) =>
    (m -> m -> Bool)
    -> (m -> m -> m)
    -> (m -> m -> m)
    -> (m -> m -> m)
    -> (m -> m -> Bool)
    -> (m -> Int)
    -> Monomial m
    forall v. (Ord v, Show v) => Eq (Glex v)
    forall v. (Ord v, Show v) => Show (Glex v)
    forall v. (Ord v, Show v) => Mon (Glex v)
    forall v. (Ord v, Show v) => Glex v -> Int
    forall v. (Ord v, Show v) => Glex v -> Glex v -> Bool
    forall v. (Ord v, Show v) => Glex v -> Glex v -> Glex v
    mdeg :: Glex v -> Int
    $cmdeg :: forall v. (Ord v, Show v) => Glex v -> Int
    mcoprime :: Glex v -> Glex v -> Bool
    $cmcoprime :: forall v. (Ord v, Show v) => Glex v -> Glex v -> Bool
    mlcm :: Glex v -> Glex v -> Glex v
    $cmlcm :: forall v. (Ord v, Show v) => Glex v -> Glex v -> Glex v
    mgcd :: Glex v -> Glex v -> Glex v
    $cmgcd :: forall v. (Ord v, Show v) => Glex v -> Glex v -> Glex v
    mdiv :: Glex v -> Glex v -> Glex v
    $cmdiv :: forall v. (Ord v, Show v) => Glex v -> Glex v -> Glex v
    mdivides :: Glex v -> Glex v -> Bool
    $cmdivides :: forall v. (Ord v, Show v) => Glex v -> Glex v -> Bool
    $cp3Monomial :: forall v. (Ord v, Show v) => Mon (Glex v)
    $cp2Monomial :: forall v. (Ord v, Show v) => Show (Glex v)
    $cp1Monomial :: forall v. (Ord v, Show v) => Eq (Glex v)
    Monomial, v -> Glex v
    Glex v -> [(v, Int)]
    (forall v. v -> Glex v)
    -> (forall v. Glex v -> [(v, Int)]) -> MonomialConstructor Glex
    forall v. v -> Glex v
    forall v. Glex v -> [(v, Int)]
    forall (m :: * -> *).
    (forall v. v -> m v)
    -> (forall v. m v -> [(v, Int)]) -> MonomialConstructor m
    mindices :: Glex v -> [(v, Int)]
    $cmindices :: forall v. Glex v -> [(v, Int)]
    mvar :: v -> Glex v
    $cmvar :: forall v. v -> Glex v
    MonomialConstructor) -- GeneralizedNewtypeDeriving

    instance Show v => Show (Glex v) where
        show :: Glex v -> String
    show (Glex m :: MonImpl v
    m) = MonImpl v -> String
    forall a. Show a => a -> String
    show MonImpl v
    m

    instance Ord v => Ord (Glex v) where
        compare :: Glex v -> Glex v -> Ordering
    compare (Glex (M si :: Int
    si xis :: [(v, Int)]
    xis)) (Glex (M sj :: Int
    sj yjs :: [(v, Int)]
    yjs)) =
            (Int, [(v, Int)]) -> (Int, [(v, Int)]) -> Ordering
    forall a. Ord a => a -> a -> Ordering
    compare (-Int
    si, [(v
    x,-Int
    i) | (x :: v
    x,i :: Int
    i) <- [(v, Int)]
    xis]) (-Int
    sj, [(v
    y,-Int
    j) | (y :: v
    y,j :: Int
    j) <- [(v, Int)]
    yjs])

    -- instance MonomialOrder Glex where isGraded _ = True

    -- |A type representing polynomials with Glex term ordering.
    type GlexPoly k v = Vect k (Glex v)

    -- |@glexvar v@ creates a variable in the algebra of commutative polynomials over Q with Glex term ordering.
    -- It is provided as a shortcut, to avoid having to provide a type annotation, as with @var@.
    -- For example, the following code creates variables called x, y and z:
    --
    -- > [x,y,z] = map glexvar ["x","y","z"]
    glexvar :: v -> GlexPoly Q v
    glexvar :: v -> GlexPoly Q v
    glexvar v :: v
    v = Glex v -> GlexPoly Q v
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Glex v -> GlexPoly Q v) -> Glex v -> GlexPoly Q v
    forall a b. (a -> b) -> a -> b
    $ MonImpl v -> Glex v
    forall v. MonImpl v -> Glex v
    Glex (MonImpl v -> Glex v) -> MonImpl v -> Glex v
    forall a b. (a -> b) -> a -> b
    $ Int -> [(v, Int)] -> MonImpl v
    forall v. Int -> [(v, Int)] -> MonImpl v
    M 1 [(v
    v,1)]
    -- glexvar = var

    instance (Eq k, Num k, Ord v, Show v) => Algebra k (Glex v) where
        unit :: k -> Vect k (Glex v)
    unit x :: k
    x = k
    x k -> Vect k (Glex v) -> Vect k (Glex v)
    forall k b. (Eq k, Num k) => k -> Vect k b -> Vect k b
    *> Glex v -> Vect k (Glex v)
    forall (m :: * -> *) a. Monad m => a -> m a
    return Glex v
    forall m. Mon m => m
    munit
        mult :: Vect k (Tensor (Glex v) (Glex v)) -> Vect k (Glex v)
    mult xy :: Vect k (Tensor (Glex v) (Glex v))
    xy = Vect k (Glex v) -> Vect k (Glex v)
    forall k b. (Eq k, Num k, Ord b) => Vect k b -> Vect k b
    nf (Vect k (Glex v) -> Vect k (Glex v))
    -> Vect k (Glex v) -> Vect k (Glex v)
    forall a b. (a -> b) -> a -> b
    $ (Tensor (Glex v) (Glex v) -> Glex v)
    -> Vect k (Tensor (Glex v) (Glex v)) -> Vect k (Glex v)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (\(a :: Glex v
    a,b :: Glex v
    b) -> Glex v
    a Glex v -> Glex v -> Glex v
    forall m. Mon m => m -> m -> m
    `mmult` Glex v
    b) Vect k (Tensor (Glex v) (Glex v))
    xy

    -- GREVLEX ORDER

    -- |A type representing monomials with Grevlex ordering.
    --
    -- Grevlex stands for graded reverse lexicographic. Thus monomials are ordered first by degree, then by reverse lexicographic order.
    -- For example, in Grevlex ordering, monomials up to degree two would be ordered as follows: x^2+xy+y^2+xz+yz+z^2+x+y+z+1.
    --
    -- In general, Grevlex leads to the smallest Groebner bases.
    newtype Grevlex v = Grevlex (MonImpl v) deriving (Grevlex v -> Grevlex v -> Bool
    (Grevlex v -> Grevlex v -> Bool)
    -> (Grevlex v -> Grevlex v -> Bool) -> Eq (Grevlex v)
    forall v. Eq v => Grevlex v -> Grevlex v -> Bool
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    /= :: Grevlex v -> Grevlex v -> Bool
    $c/= :: forall v. Eq v => Grevlex v -> Grevlex v -> Bool
    == :: Grevlex v -> Grevlex v -> Bool
    $c== :: forall v. Eq v => Grevlex v -> Grevlex v -> Bool
    Eq, a -> Grevlex b -> Grevlex a
    (a -> b) -> Grevlex a -> Grevlex b
    (forall a b. (a -> b) -> Grevlex a -> Grevlex b)
    -> (forall a b. a -> Grevlex b -> Grevlex a) -> Functor Grevlex
    forall a b. a -> Grevlex b -> Grevlex a
    forall a b. (a -> b) -> Grevlex a -> Grevlex b
    forall (f :: * -> *).
    (forall a b. (a -> b) -> f a -> f b)
    -> (forall a b. a -> f b -> f a) -> Functor f
    <$ :: a -> Grevlex b -> Grevlex a
    $c<$ :: forall a b. a -> Grevlex b -> Grevlex a
    fmap :: (a -> b) -> Grevlex a -> Grevlex b
    $cfmap :: forall a b. (a -> b) -> Grevlex a -> Grevlex b
    Functor, Grevlex v
    Grevlex v -> Grevlex v -> Grevlex v
    Grevlex v
    -> (Grevlex v -> Grevlex v -> Grevlex v) -> Mon (Grevlex v)
    forall m. m -> (m -> m -> m) -> Mon m
    forall v. Ord v => Grevlex v
    forall v. Ord v => Grevlex v -> Grevlex v -> Grevlex v
    mmult :: Grevlex v -> Grevlex v -> Grevlex v
    $cmmult :: forall v. Ord v => Grevlex v -> Grevlex v -> Grevlex v
    munit :: Grevlex v
    $cmunit :: forall v. Ord v => Grevlex v
    Mon, Eq (Grevlex v)
    Show (Grevlex v)
    Mon (Grevlex v)
    (Eq (Grevlex v), Show (Grevlex v), Mon (Grevlex v)) =>
    (Grevlex v -> Grevlex v -> Bool)
    -> (Grevlex v -> Grevlex v -> Grevlex v)
    -> (Grevlex v -> Grevlex v -> Grevlex v)
    -> (Grevlex v -> Grevlex v -> Grevlex v)
    -> (Grevlex v -> Grevlex v -> Bool)
    -> (Grevlex v -> Int)
    -> Monomial (Grevlex v)
    Grevlex v -> Int
    Grevlex v -> Grevlex v -> Bool
    Grevlex v -> Grevlex v -> Grevlex v
    forall m.
    (Eq m, Show m, Mon m) =>
    (m -> m -> Bool)
    -> (m -> m -> m)
    -> (m -> m -> m)
    -> (m -> m -> m)
    -> (m -> m -> Bool)
    -> (m -> Int)
    -> Monomial m
    forall v. (Ord v, Show v) => Eq (Grevlex v)
    forall v. (Ord v, Show v) => Show (Grevlex v)
    forall v. (Ord v, Show v) => Mon (Grevlex v)
    forall v. (Ord v, Show v) => Grevlex v -> Int
    forall v. (Ord v, Show v) => Grevlex v -> Grevlex v -> Bool
    forall v. (Ord v, Show v) => Grevlex v -> Grevlex v -> Grevlex v
    mdeg :: Grevlex v -> Int
    $cmdeg :: forall v. (Ord v, Show v) => Grevlex v -> Int
    mcoprime :: Grevlex v -> Grevlex v -> Bool
    $cmcoprime :: forall v. (Ord v, Show v) => Grevlex v -> Grevlex v -> Bool
    mlcm :: Grevlex v -> Grevlex v -> Grevlex v
    $cmlcm :: forall v. (Ord v, Show v) => Grevlex v -> Grevlex v -> Grevlex v
    mgcd :: Grevlex v -> Grevlex v -> Grevlex v
    $cmgcd :: forall v. (Ord v, Show v) => Grevlex v -> Grevlex v -> Grevlex v
    mdiv :: Grevlex v -> Grevlex v -> Grevlex v
    $cmdiv :: forall v. (Ord v, Show v) => Grevlex v -> Grevlex v -> Grevlex v
    mdivides :: Grevlex v -> Grevlex v -> Bool
    $cmdivides :: forall v. (Ord v, Show v) => Grevlex v -> Grevlex v -> Bool
    $cp3Monomial :: forall v. (Ord v, Show v) => Mon (Grevlex v)
    $cp2Monomial :: forall v. (Ord v, Show v) => Show (Grevlex v)
    $cp1Monomial :: forall v. (Ord v, Show v) => Eq (Grevlex v)
    Monomial, v -> Grevlex v
    Grevlex v -> [(v, Int)]
    (forall v. v -> Grevlex v)
    -> (forall v. Grevlex v -> [(v, Int)])
    -> MonomialConstructor Grevlex
    forall v. v -> Grevlex v
    forall v. Grevlex v -> [(v, Int)]
    forall (m :: * -> *).
    (forall v. v -> m v)
    -> (forall v. m v -> [(v, Int)]) -> MonomialConstructor m
    mindices :: Grevlex v -> [(v, Int)]
    $cmindices :: forall v. Grevlex v -> [(v, Int)]
    mvar :: v -> Grevlex v
    $cmvar :: forall v. v -> Grevlex v
    MonomialConstructor) -- GeneralizedNewtypeDeriving

    instance Show v => Show (Grevlex v) where
        show :: Grevlex v -> String
    show (Grevlex m :: MonImpl v
    m) = MonImpl v -> String
    forall a. Show a => a -> String
    show MonImpl v
    m

    instance Ord v => Ord (Grevlex v) where
        compare :: Grevlex v -> Grevlex v -> Ordering
    compare (Grevlex (M si :: Int
    si xis :: [(v, Int)]
    xis)) (Grevlex (M sj :: Int
    sj yjs :: [(v, Int)]
    yjs)) =
            (Int, [(v, Int)]) -> (Int, [(v, Int)]) -> Ordering
    forall a. Ord a => a -> a -> Ordering
    compare (-Int
    si, [(v, Int)] -> [(v, Int)]
    forall a. [a] -> [a]
    reverse [(v, Int)]
    xis) (-Int
    sj, [(v, Int)] -> [(v, Int)]
    forall a. [a] -> [a]
    reverse [(v, Int)]
    yjs)

    -- instance MonomialOrder Grevlex where isGraded _ = True

    -- |A type representing polynomials with Grevlex term ordering.
    type GrevlexPoly k v = Vect k (Grevlex v)

    -- |@grevlexvar v@ creates a variable in the algebra of commutative polynomials over Q with Grevlex term ordering.
    -- It is provided as a shortcut, to avoid having to provide a type annotation, as with @var@.
    -- For example, the following code creates variables called x, y and z:
    --
    -- > [x,y,z] = map grevlexvar ["x","y","z"]
    grevlexvar :: v -> GrevlexPoly Q v
    grevlexvar :: v -> GrevlexPoly Q v
    grevlexvar v :: v
    v = Grevlex v -> GrevlexPoly Q v
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Grevlex v -> GrevlexPoly Q v) -> Grevlex v -> GrevlexPoly Q v
    forall a b. (a -> b) -> a -> b
    $ MonImpl v -> Grevlex v
    forall v. MonImpl v -> Grevlex v
    Grevlex (MonImpl v -> Grevlex v) -> MonImpl v -> Grevlex v
    forall a b. (a -> b) -> a -> b
    $ Int -> [(v, Int)] -> MonImpl v
    forall v. Int -> [(v, Int)] -> MonImpl v
    M 1 [(v
    v,1)]
    -- grevlexvar = var

    instance (Eq k, Num k, Ord v, Show v) => Algebra k (Grevlex v) where
        unit :: k -> Vect k (Grevlex v)
    unit x :: k
    x = k
    x k -> Vect k (Grevlex v) -> Vect k (Grevlex v)
    forall k b. (Eq k, Num k) => k -> Vect k b -> Vect k b
    *> Grevlex v -> Vect k (Grevlex v)
    forall (m :: * -> *) a. Monad m => a -> m a
    return Grevlex v
    forall m. Mon m => m
    munit
        mult :: Vect k (Tensor (Grevlex v) (Grevlex v)) -> Vect k (Grevlex v)
    mult xy :: Vect k (Tensor (Grevlex v) (Grevlex v))
    xy = Vect k (Grevlex v) -> Vect k (Grevlex v)
    forall k b. (Eq k, Num k, Ord b) => Vect k b -> Vect k b
    nf (Vect k (Grevlex v) -> Vect k (Grevlex v))
    -> Vect k (Grevlex v) -> Vect k (Grevlex v)
    forall a b. (a -> b) -> a -> b
    $ (Tensor (Grevlex v) (Grevlex v) -> Grevlex v)
    -> Vect k (Tensor (Grevlex v) (Grevlex v)) -> Vect k (Grevlex v)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (\(a :: Grevlex v
    a,b :: Grevlex v
    b) -> Grevlex v
    a Grevlex v -> Grevlex v -> Grevlex v
    forall m. Mon m => m -> m -> m
    `mmult` Grevlex v
    b) Vect k (Tensor (Grevlex v) (Grevlex v))
    xy

    -- ELIMINATION ORDER

    data Elim2 a b = Elim2 !a !b deriving (Elim2 a b -> Elim2 a b -> Bool
    (Elim2 a b -> Elim2 a b -> Bool)
    -> (Elim2 a b -> Elim2 a b -> Bool) -> Eq (Elim2 a b)
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    forall a b. (Eq a, Eq b) => Elim2 a b -> Elim2 a b -> Bool
    /= :: Elim2 a b -> Elim2 a b -> Bool
    $c/= :: forall a b. (Eq a, Eq b) => Elim2 a b -> Elim2 a b -> Bool
    == :: Elim2 a b -> Elim2 a b -> Bool
    $c== :: forall a b. (Eq a, Eq b) => Elim2 a b -> Elim2 a b -> Bool
    Eq, a -> Elim2 a b -> Elim2 a a
    (a -> b) -> Elim2 a a -> Elim2 a b
    (forall a b. (a -> b) -> Elim2 a a -> Elim2 a b)
    -> (forall a b. a -> Elim2 a b -> Elim2 a a) -> Functor (Elim2 a)
    forall a b. a -> Elim2 a b -> Elim2 a a
    forall a b. (a -> b) -> Elim2 a a -> Elim2 a b
    forall a a b. a -> Elim2 a b -> Elim2 a a
    forall a a b. (a -> b) -> Elim2 a a -> Elim2 a b
    forall (f :: * -> *).
    (forall a b. (a -> b) -> f a -> f b)
    -> (forall a b. a -> f b -> f a) -> Functor f
    <$ :: a -> Elim2 a b -> Elim2 a a
    $c<$ :: forall a a b. a -> Elim2 a b -> Elim2 a a
    fmap :: (a -> b) -> Elim2 a a -> Elim2 a b
    $cfmap :: forall a a b. (a -> b) -> Elim2 a a -> Elim2 a b
    Functor)

    instance (Ord a, Ord b) => Ord (Elim2 a b) where
        compare :: Elim2 a b -> Elim2 a b -> Ordering
    compare (Elim2 a1 :: a
    a1 b1 :: b
    b1) (Elim2 a2 :: a
    a2 b2 :: b
    b2) = (a, b) -> (a, b) -> Ordering
    forall a. Ord a => a -> a -> Ordering
    compare (a
    a1,b
    b1) (a
    a2,b
    b2)

    instance (Show a, Show b) => Show (Elim2 a b) where
        show :: Elim2 a b -> String
    show (Elim2 ma :: a
    ma mb :: b
    mb) = case (a -> String
    forall a. Show a => a -> String
    show a
    ma, b -> String
    forall a. Show a => a -> String
    show b
    mb) of
                           ("1","1") -> "1"
                           (ma' :: String
    ma',"1") -> String
    ma'
                           ("1",mb' :: String
    mb') -> String
    mb'
                           (ma' :: String
    ma',mb' :: String
    mb') -> String
    ma' String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    mb'

    instance (Mon a, Mon b) => Mon (Elim2 a b) where
        munit :: Elim2 a b
    munit = a -> b -> Elim2 a b
    forall a b. a -> b -> Elim2 a b
    Elim2 a
    forall m. Mon m => m
    munit b
    forall m. Mon m => m
    munit
        mmult :: Elim2 a b -> Elim2 a b -> Elim2 a b
    mmult (Elim2 a1 :: a
    a1 b1 :: b
    b1) (Elim2 a2 :: a
    a2 b2 :: b
    b2) = a -> b -> Elim2 a b
    forall a b. a -> b -> Elim2 a b
    Elim2 (a -> a -> a
    forall m. Mon m => m -> m -> m
    mmult a
    a1 a
    a2) (b -> b -> b
    forall m. Mon m => m -> m -> m
    mmult b
    b1 b
    b2)

    instance (Monomial a, Monomial b) => Monomial (Elim2 a b) where
        mdivides :: Elim2 a b -> Elim2 a b -> Bool
    mdivides (Elim2 a1 :: a
    a1 b1 :: b
    b1) (Elim2 a2 :: a
    a2 b2 :: b
    b2) = a -> a -> Bool
    forall m. Monomial m => m -> m -> Bool
    mdivides a
    a1 a
    a2 Bool -> Bool -> Bool
    && b -> b -> Bool
    forall m. Monomial m => m -> m -> Bool
    mdivides b
    b1 b
    b2
        mdiv :: Elim2 a b -> Elim2 a b -> Elim2 a b
    mdiv (Elim2 a1 :: a
    a1 b1 :: b
    b1) (Elim2 a2 :: a
    a2 b2 :: b
    b2) = a -> b -> Elim2 a b
    forall a b. a -> b -> Elim2 a b
    Elim2 (a -> a -> a
    forall m. Monomial m => m -> m -> m
    mdiv a
    a1 a
    a2) (b -> b -> b
    forall m. Monomial m => m -> m -> m
    mdiv b
    b1 b
    b2)
        mgcd :: Elim2 a b -> Elim2 a b -> Elim2 a b
    mgcd (Elim2 a1 :: a
    a1 b1 :: b
    b1) (Elim2 a2 :: a
    a2 b2 :: b
    b2) = a -> b -> Elim2 a b
    forall a b. a -> b -> Elim2 a b
    Elim2 (a -> a -> a
    forall m. Monomial m => m -> m -> m
    mgcd a
    a1 a
    a2) (b -> b -> b
    forall m. Monomial m => m -> m -> m
    mgcd b
    b1 b
    b2)
        mlcm :: Elim2 a b -> Elim2 a b -> Elim2 a b
    mlcm (Elim2 a1 :: a
    a1 b1 :: b
    b1) (Elim2 a2 :: a
    a2 b2 :: b
    b2) = a -> b -> Elim2 a b
    forall a b. a -> b -> Elim2 a b
    Elim2 (a -> a -> a
    forall m. Monomial m => m -> m -> m
    mlcm a
    a1 a
    a2) (b -> b -> b
    forall m. Monomial m => m -> m -> m
    mlcm b
    b1 b
    b2)
        mcoprime :: Elim2 a b -> Elim2 a b -> Bool
    mcoprime (Elim2 a1 :: a
    a1 b1 :: b
    b1) (Elim2 a2 :: a
    a2 b2 :: b
    b2) = a -> a -> Bool
    forall m. Monomial m => m -> m -> Bool
    mcoprime a
    a1 a
    a2 Bool -> Bool -> Bool
    && b -> b -> Bool
    forall m. Monomial m => m -> m -> Bool
    mcoprime b
    b1 b
    b2
        mdeg :: Elim2 a b -> Int
    mdeg (Elim2 a :: a
    a b :: b
    b) = a -> Int
    forall m. Monomial m => m -> Int
    mdeg a
    a Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + b -> Int
    forall m. Monomial m => m -> Int
    mdeg b
    b

    instance (Eq k, Num k, Ord a, Mon a, Ord b, Mon b) => Algebra k (Elim2 a b) where
        unit :: k -> Vect k (Elim2 a b)
    unit x :: k
    x = k
    x k -> Vect k (Elim2 a b) -> Vect k (Elim2 a b)
    forall k b. (Eq k, Num k) => k -> Vect k b -> Vect k b
    *> Elim2 a b -> Vect k (Elim2 a b)
    forall (m :: * -> *) a. Monad m => a -> m a
    return Elim2 a b
    forall m. Mon m => m
    munit
        mult :: Vect k (Tensor (Elim2 a b) (Elim2 a b)) -> Vect k (Elim2 a b)
    mult xy :: Vect k (Tensor (Elim2 a b) (Elim2 a b))
    xy = Vect k (Elim2 a b) -> Vect k (Elim2 a b)
    forall k b. (Eq k, Num k, Ord b) => Vect k b -> Vect k b
    nf (Vect k (Elim2 a b) -> Vect k (Elim2 a b))
    -> Vect k (Elim2 a b) -> Vect k (Elim2 a b)
    forall a b. (a -> b) -> a -> b
    $ (Tensor (Elim2 a b) (Elim2 a b) -> Elim2 a b)
    -> Vect k (Tensor (Elim2 a b) (Elim2 a b)) -> Vect k (Elim2 a b)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (\(a :: Elim2 a b
    a,b :: Elim2 a b
    b) -> Elim2 a b
    a Elim2 a b -> Elim2 a b -> Elim2 a b
    forall m. Mon m => m -> m -> m
    `mmult` Elim2 a b
    b) Vect k (Tensor (Elim2 a b) (Elim2 a b))
    xy

    -- VARIABLE SUBSTITUTION

    -- |Given (Num k, MonomialConstructor m), then Vect k (m v) is the free commutative algebra over v.
    -- As such, it is a monad (in the mathematical sense). The following pseudo-code (not legal Haskell)
    -- shows how this would work:
    --
    -- > instance (Num k, Monomial m) => Monad (\v -> Vect k (m v)) where
    -- >     return = var
    -- >     (>>=) = bind
    --
    -- bind corresponds to variable substitution, so @v \`bind\` f@ returns the result of making the substitutions
    -- encoded in f into v.
    --
    -- Note that the type signature is slightly more general than that required by (>>=).
    -- For a monad, we would only require:
    --
    -- > bind :: (MonomialConstructor m, Num k, Ord (m v), Show (m v), Algebra k (m v)) =>
    -- >     Vect k (m u) -> (u -> Vect k (m v)) -> Vect k (m v)
    --
    -- Instead, the given type signature allows us to substitute in elements of any algebra.
    -- This is occasionally useful.

    -- |bind performs variable substitution
    bind :: (Eq k, Num k, MonomialConstructor m, Ord a, Show a, Algebra k a) =>
        Vect k (m v) -> (v -> Vect k a) -> Vect k a
    v :: Vect k (m v)
    v bind :: Vect k (m v) -> (v -> Vect k a) -> Vect k a
    `bind` f :: v -> Vect k a
    f = (m v -> Vect k a) -> Vect k (m v) -> Vect k a
    forall k b a.
    (Eq k, Num k, Ord b) =>
    (a -> Vect k b) -> Vect k a -> Vect k b
    linear (\m :: m v
    m -> [Vect k a] -> Vect k a
    forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
    product [v -> Vect k a
    f v
    x Vect k a -> Int -> Vect k a
    forall a b. (Num a, Integral b) => a -> b -> a
    ^ Int
    i | (x :: v
    x,i :: Int
    i) <- m v -> [(v, Int)]
    forall (m :: * -> *) v. MonomialConstructor m => m v -> [(v, Int)]
    mindices m v
    m]) Vect k (m v)
    v
    -- V ts `bind` f = sum [c *> product [f x ^ i | (x,i) <- mindices m] | (m, c) <- ts]

    -- We can't express the Monad instance directly in Haskell, firstly because of the Ord v constraint (? - not used),
    -- secondly because Haskell doesn't support type functions.

    flipbind :: (t -> Vect k b) -> Vect k (m t) -> Vect k b
    flipbind f :: t -> Vect k b
    f = (m t -> Vect k b) -> Vect k (m t) -> Vect k b
    forall k b a.
    (Eq k, Num k, Ord b) =>
    (a -> Vect k b) -> Vect k a -> Vect k b
    linear (\m :: m t
    m -> [Vect k b] -> Vect k b
    forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
    product [t -> Vect k b
    f t
    x Vect k b -> Int -> Vect k b
    forall a b. (Num a, Integral b) => a -> b -> a
    ^ Int
    i | (x :: t
    x,i :: Int
    i) <- m t -> [(t, Int)]
    forall (m :: * -> *) v. MonomialConstructor m => m v -> [(v, Int)]
    mindices m t
    m])

    -- |Evaluate a polynomial at a point.
    -- For example @eval (x^2+y^2) [(x,1),(y,2)]@ evaluates x^2+y^2 at the point (x,y)=(1,2).
    eval :: (Eq k, Num k, MonomialConstructor m, Eq (m v), Show v) =>
        Vect k (m v) -> [(Vect k (m v), k)] -> k
    eval :: Vect k (m v) -> [(Vect k (m v), k)] -> k
    eval f :: Vect k (m v)
    f vs :: [(Vect k (m v), k)]
    vs = Vect k () -> k
    forall k. Num k => Vect k () -> k
    unwrap (Vect k () -> k) -> Vect k () -> k
    forall a b. (a -> b) -> a -> b
    $ Vect k (m v)
    f Vect k (m v) -> (v -> Vect k ()) -> Vect k ()
    forall k (m :: * -> *) a v.
    (Eq k, Num k, MonomialConstructor m, Ord a, Show a, Algebra k a) =>
    Vect k (m v) -> (v -> Vect k a) -> Vect k a
    `bind` v -> Vect k ()
    sub
        where sub :: v -> Vect k ()
    sub x :: v
    x = case Vect k (m v) -> [(Vect k (m v), k)] -> Maybe k
    forall a b. Eq a => a -> [(a, b)] -> Maybe b
    lookup (v -> Vect k (m v)
    forall k (m :: * -> *) v.
    (Num k, MonomialConstructor m) =>
    v -> Vect k (m v)
    var v
    x) [(Vect k (m v), k)]
    vs of
                      Just xval :: k
    xval -> k
    xval k -> Vect k () -> Vect k ()
    forall k b. (Eq k, Num k) => k -> Vect k b -> Vect k b
    *> () -> Vect k ()
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
                      Nothing -> String -> Vect k ()
    forall a. HasCallStack => String -> a
    error ("eval: no binding given for " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ v -> String
    forall a. Show a => a -> String
    show v
    x)

    -- |Perform variable substitution on a polynomial.
    -- For example @subst (x*z-y^2) [(x,u^2),(y,u*v),(z,v^2)]@ performs the substitution x -> u^2, y -> u*v, z -> v^2.
    subst :: (Eq k, Num k, MonomialConstructor m, Eq (m u), Show u, Ord (m v), Show (m v), Algebra k (m v)) =>
        Vect k (m u) -> [(Vect k (m u), Vect k (m v))] -> Vect k (m v)
    subst :: Vect k (m u) -> [(Vect k (m u), Vect k (m v))] -> Vect k (m v)
    subst f :: Vect k (m u)
    f vs :: [(Vect k (m u), Vect k (m v))]
    vs = Vect k (m u)
    f Vect k (m u) -> (u -> Vect k (m v)) -> Vect k (m v)
    forall k (m :: * -> *) a v.
    (Eq k, Num k, MonomialConstructor m, Ord a, Show a, Algebra k a) =>
    Vect k (m v) -> (v -> Vect k a) -> Vect k a
    `bind` u -> Vect k (m v)
    sub
        where sub :: u -> Vect k (m v)
    sub x :: u
    x = case Vect k (m u)
    -> [(Vect k (m u), Vect k (m v))] -> Maybe (Vect k (m v))
    forall a b. Eq a => a -> [(a, b)] -> Maybe b
    lookup (u -> Vect k (m u)
    forall k (m :: * -> *) v.
    (Num k, MonomialConstructor m) =>
    v -> Vect k (m v)
    var u
    x) [(Vect k (m u), Vect k (m v))]
    vs of
                      Just xsub :: Vect k (m v)
    xsub -> Vect k (m v)
    xsub
                      Nothing -> String -> Vect k (m v)
    forall a. HasCallStack => String -> a
    error ("eval: no binding given for " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ u -> String
    forall a. Show a => a -> String
    show u
    x)
    -- The type could be more general than this, but haven't so far found a use case

    -- |List the variables used in a polynomial
    vars :: (Num k, Ord k, MonomialConstructor m, Ord (m v)) =>
         Vect k (m v) -> [Vect k (m v)]
    vars :: Vect k (m v) -> [Vect k (m v)]
    vars f :: Vect k (m v)
    f = [Vect k (m v)] -> [Vect k (m v)]
    forall a. Ord a => [a] -> [a]
    toSet [ v -> Vect k (m v)
    forall k (m :: * -> *) v.
    (Num k, MonomialConstructor m) =>
    v -> Vect k (m v)
    var v
    v | (m :: m v
    m,_) <- Vect k (m v) -> [(m v, k)]
    forall k b. Vect k b -> [(b, k)]
    terms Vect k (m v)
    f, v
    v <- ((v, Int) -> v) -> [(v, Int)] -> [v]
    forall a b. (a -> b) -> [a] -> [b]
    map (v, Int) -> v
    forall a b. (a, b) -> a
    fst (m v -> [(v, Int)]
    forall (m :: * -> *) v. MonomialConstructor m => m v -> [(v, Int)]
    mindices m v
    m) ]

    -- DIVISION ALGORITHM FOR POLYNOMIALS

    lt :: Vect k b -> (b, k)
    lt (V (t :: (b, k)
    t:ts :: [(b, k)]
    ts)) = (b, k)
    t -- leading term
    lm :: Vect b c -> c
    lm = (c, b) -> c
    forall a b. (a, b) -> a
    fst ((c, b) -> c) -> (Vect b c -> (c, b)) -> Vect b c -> c
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Vect b c -> (c, b)
    forall k b. Vect k b -> (b, k)
    lt     -- leading monomial
    lc :: Vect c a -> c
    lc = (a, c) -> c
    forall a b. (a, b) -> b
    snd ((a, c) -> c) -> (Vect c a -> (a, c)) -> Vect c a -> c
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Vect c a -> (a, c)
    forall k b. Vect k b -> (b, k)
    lt     -- leading coefficient

    -- deg :: (Num k, Monomial m, MonomialOrder m) => Vect k m -> Int
    deg :: Vect k m -> Int
    deg (V []) = -1
    deg f :: Vect k m
    f = [Int] -> Int
    forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
    maximum ([Int] -> Int) -> [Int] -> Int
    forall a b. (a -> b) -> a -> b
    $ [m -> Int
    forall m. Monomial m => m -> Int
    mdeg m
    m | (m :: m
    m,c :: k
    c) <- Vect k m -> [(m, k)]
    forall k b. Vect k b -> [(b, k)]
    terms Vect k m
    f]
    {-
    deg f | isGraded (lm f) = mdeg (lm f)
          | otherwise = maximum $ [mdeg m | (m,c) <- terms f]
    -}
    -- the true degree of the polynomial, not the degree of the leading term
    -- required for sugar strategy when computing Groebner basis

    toMonic :: Vect k b -> Vect k b
    toMonic 0 = 0
    toMonic f :: Vect k b
    f = (1 k -> k -> k
    forall a. Fractional a => a -> a -> a
    / Vect k b -> k
    forall c a. Vect c a -> c
    lc Vect k b
    f) k -> Vect k b -> Vect k b
    forall k b. (Eq k, Num k) => k -> Vect k b -> Vect k b
    *> Vect k b
    f

    -- tdivmaybe (m1,x1) (m2,x2) = fmap (\m -> (m,x1/x2)) $ mdivmaybe m1 m2

    tdivides :: (m, b) -> (m, b) -> Bool
    tdivides (m1 :: m
    m1,x1 :: b
    x1) (m2 :: m
    m2,x2 :: b
    x2) = m -> m -> Bool
    forall m. Monomial m => m -> m -> Bool
    mdivides m
    m1 m
    m2

    tdiv :: (a, b) -> (a, b) -> (a, b)
    tdiv (m1 :: a
    m1,x1 :: b
    x1) (m2 :: a
    m2,x2 :: b
    x2) = (a -> a -> a
    forall m. Monomial m => m -> m -> m
    mdiv a
    m1 a
    m2, b
    x1b -> b -> b
    forall a. Fractional a => a -> a -> a
    /b
    x2)

    tgcd :: (a, b) -> (a, b) -> (a, b)
    tgcd (m1 :: a
    m1,_) (m2 :: a
    m2,_) = (a -> a -> a
    forall m. Monomial m => m -> m -> m
    mgcd a
    m1 a
    m2, 1)
    -- tlcm (m1,_) (m2,_) = (mlcm m1 m2, 1)

    tmult :: (a, b) -> (a, b) -> (a, b)
    tmult (m :: a
    m,c :: b
    c) (m' :: a
    m',c' :: b
    c') = (a -> a -> a
    forall m. Mon m => m -> m -> m
    mmult a
    m a
    m',b
    cb -> b -> b
    forall a. Num a => a -> a -> a
    *b
    c')

    infixl 7 *->
    t :: (b, k)
    t *-> :: (b, k) -> Vect k b -> Vect k b
    *-> V ts :: [(b, k)]
    ts = [(b, k)] -> Vect k b
    forall k b. [(b, k)] -> Vect k b
    V ([(b, k)] -> Vect k b) -> [(b, k)] -> Vect k b
    forall a b. (a -> b) -> a -> b
    $ ((b, k) -> (b, k)) -> [(b, k)] -> [(b, k)]
    forall a b. (a -> b) -> [a] -> [b]
    map ((b, k) -> (b, k) -> (b, k)
    forall a b. (Mon a, Num b) => (a, b) -> (a, b) -> (a, b)
    tmult (b, k)
    t) [(b, k)]
    ts -- preserves term order

    -- given f, gs, find as, r such that f = sum (zipWith (*) as gs) + r, with r not divisible by any g
    quotRemMP :: Vect b m -> [Vect b m] -> ([Vect b m], Vect b m)
    quotRemMP f :: Vect b m
    f gs :: [Vect b m]
    gs = Vect b m -> ([Vect b m], Vect b m) -> ([Vect b m], Vect b m)
    quotRemMP' Vect b m
    f (Int -> Vect b m -> [Vect b m]
    forall a. Int -> a -> [a]
    replicate Int
    n 0, 0) where
        n :: Int
    n = [Vect b m] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [Vect b m]
    gs
        quotRemMP' :: Vect b m -> ([Vect b m], Vect b m) -> ([Vect b m], Vect b m)
    quotRemMP' 0 (us :: [Vect b m]
    us,r :: Vect b m
    r) = ([Vect b m]
    us,Vect b m
    r)
        quotRemMP' h :: Vect b m
    h (us :: [Vect b m]
    us,r :: Vect b m
    r) = Vect b m
    -> ([Vect b m], [Vect b m], [Vect b m], Vect b m)
    -> ([Vect b m], Vect b m)
    divisionStep Vect b m
    h ([Vect b m]
    gs,[],[Vect b m]
    us,Vect b m
    r)
        divisionStep :: Vect b m
    -> ([Vect b m], [Vect b m], [Vect b m], Vect b m)
    -> ([Vect b m], Vect b m)
    divisionStep h :: Vect b m
    h (g :: Vect b m
    g:gs :: [Vect b m]
    gs,us' :: [Vect b m]
    us',u :: Vect b m
    u:us :: [Vect b m]
    us,r :: Vect b m
    r) =
            if Vect b m -> (m, b)
    forall k b. Vect k b -> (b, k)
    lt Vect b m
    g (m, b) -> (m, b) -> Bool
    forall m b b. Monomial m => (m, b) -> (m, b) -> Bool
    `tdivides` Vect b m -> (m, b)
    forall k b. Vect k b -> (b, k)
    lt Vect b m
    h
            then let t :: Vect b m
    t = [(m, b)] -> Vect b m
    forall k b. [(b, k)] -> Vect k b
    V [Vect b m -> (m, b)
    forall k b. Vect k b -> (b, k)
    lt Vect b m
    h (m, b) -> (m, b) -> (m, b)
    forall a b.
    (Monomial a, Fractional b) =>
    (a, b) -> (a, b) -> (a, b)
    `tdiv` Vect b m -> (m, b)
    forall k b. Vect k b -> (b, k)
    lt Vect b m
    g]
                     h' :: Vect b m
    h' = Vect b m
    h Vect b m -> Vect b m -> Vect b m
    forall a. Num a => a -> a -> a
    - Vect b m
    tVect b m -> Vect b m -> Vect b m
    forall a. Num a => a -> a -> a
    *Vect b m
    g
                     u' :: Vect b m
    u' = Vect b m
    uVect b m -> Vect b m -> Vect b m
    forall a. Num a => a -> a -> a
    +Vect b m
    t
                 in Vect b m -> ([Vect b m], Vect b m) -> ([Vect b m], Vect b m)
    quotRemMP' Vect b m
    h' ([Vect b m] -> [Vect b m]
    forall a. [a] -> [a]
    reverse [Vect b m]
    us' [Vect b m] -> [Vect b m] -> [Vect b m]
    forall a. [a] -> [a] -> [a]
    ++ Vect b m
    u'Vect b m -> [Vect b m] -> [Vect b m]
    forall a. a -> [a] -> [a]
    :[Vect b m]
    us, Vect b m
    r)
            else Vect b m
    -> ([Vect b m], [Vect b m], [Vect b m], Vect b m)
    -> ([Vect b m], Vect b m)
    divisionStep Vect b m
    h ([Vect b m]
    gs,Vect b m
    uVect b m -> [Vect b m] -> [Vect b m]
    forall a. a -> [a] -> [a]
    :[Vect b m]
    us',[Vect b m]
    us,Vect b m
    r)
        divisionStep h :: Vect b m
    h ([],us' :: [Vect b m]
    us',[],r :: Vect b m
    r) =
            let (lth :: Vect b m
    lth,h' :: Vect b m
    h') = Vect b m -> (Vect b m, Vect b m)
    forall k b. Vect k b -> (Vect k b, Vect k b)
    splitlt Vect b m
    h
            in Vect b m -> ([Vect b m], Vect b m) -> ([Vect b m], Vect b m)
    quotRemMP' Vect b m
    h' ([Vect b m] -> [Vect b m]
    forall a. [a] -> [a]
    reverse [Vect b m]
    us', Vect b m
    rVect b m -> Vect b m -> Vect b m
    forall a. Num a => a -> a -> a
    +Vect b m
    lth)
        splitlt :: Vect k b -> (Vect k b, Vect k b)
    splitlt (V (t :: (b, k)
    t:ts :: [(b, k)]
    ts)) = ([(b, k)] -> Vect k b
    forall k b. [(b, k)] -> Vect k b
    V [(b, k)
    t], [(b, k)] -> Vect k b
    forall k b. [(b, k)] -> Vect k b
    V [(b, k)]
    ts)

    rewrite :: Vect b m -> [Vect b m] -> Vect b m
    rewrite f :: Vect b m
    f gs :: [Vect b m]
    gs = (Vect b m, Vect b m) -> [Vect b m] -> Vect b m
    rewrite' (Vect b m
    f,0) [Vect b m]
    gs where
        rewrite' :: (Vect b m, Vect b m) -> [Vect b m] -> Vect b m
    rewrite' (0,r :: Vect b m
    r) _ = Vect b m
    r
        rewrite' (l :: Vect b m
    l,r :: Vect b m
    r) (h :: Vect b m
    h:hs :: [Vect b m]
    hs) =
            if Vect b m -> (m, b)
    forall k b. Vect k b -> (b, k)
    lt Vect b m
    h (m, b) -> (m, b) -> Bool
    forall m b b. Monomial m => (m, b) -> (m, b) -> Bool
    `tdivides` Vect b m -> (m, b)
    forall k b. Vect k b -> (b, k)
    lt Vect b m
    l -- if lhs of "rewrite rule" h matches
            then let l' :: Vect b m
    l' = Vect b m
    l Vect b m -> Vect b m -> Vect b m
    forall a. Num a => a -> a -> a
    - [(m, b)] -> Vect b m
    forall k b. [(b, k)] -> Vect k b
    V [Vect b m -> (m, b)
    forall k b. Vect k b -> (b, k)
    lt Vect b m
    l (m, b) -> (m, b) -> (m, b)
    forall a b.
    (Monomial a, Fractional b) =>
    (a, b) -> (a, b) -> (a, b)
    `tdiv` Vect b m -> (m, b)
    forall k b. Vect k b -> (b, k)
    lt Vect b m
    h] Vect b m -> Vect b m -> Vect b m
    forall a. Num a => a -> a -> a
    * Vect b m
    h -- apply rewrite rule to eliminate leading term
                 in (Vect b m, Vect b m) -> [Vect b m] -> Vect b m
    rewrite' (Vect b m
    l',Vect b m
    r) [Vect b m]
    gs -- then start again and try to eliminate the new lt.
            else (Vect b m, Vect b m) -> [Vect b m] -> Vect b m
    rewrite' (Vect b m
    l,Vect b m
    r) [Vect b m]
    hs -- else try the next potential divisor
        rewrite' (l :: Vect b m
    l,r :: Vect b m
    r) [] = -- none of the rewrite rules matches lt l
            let (h :: Vect b m
    h,t :: Vect b m
    t) = Vect b m -> (Vect b m, Vect b m)
    forall k b. Vect k b -> (Vect k b, Vect k b)
    split Vect b m
    l
            in (Vect b m, Vect b m) -> [Vect b m] -> Vect b m
    rewrite' (Vect b m
    t, Vect b m
    r Vect b m -> Vect b m -> Vect b m
    forall a. Num a => a -> a -> a
    + Vect b m
    h) [Vect b m]
    gs -- so move it into the remainder r, and try to rewrite the other terms
        split :: Vect k b -> (Vect k b, Vect k b)
    split (V (t :: (b, k)
    t:ts :: [(b, k)]
    ts)) = ([(b, k)] -> Vect k b
    forall k b. [(b, k)] -> Vect k b
    V [(b, k)
    t], [(b, k)] -> Vect k b
    forall k b. [(b, k)] -> Vect k b
    V [(b, k)]
    ts)

    infixl 7 %%

    -- |@f %% gs@ is the reduction of a polynomial f with respect to a list of polynomials gs.
    -- In the case where the gs are a Groebner basis for an ideal I,
    -- then @f %% gs@ is the equivalence class representative of f in R/I,
    -- and is zero if and only if f is in I.
    (%%) :: (Eq k, Fractional k, Monomial m, Ord m, Algebra k m) =>
         Vect k m -> [Vect k m] -> Vect k m
    f :: Vect k m
    f %% :: Vect k m -> [Vect k m] -> Vect k m
    %% gs :: [Vect k m]
    gs = Vect k m -> [Vect k m] -> Vect k m
    forall b m.
    (Eq b, Ord m, Algebra b m, Monomial m, Fractional b) =>
    Vect b m -> [Vect b m] -> Vect b m
    rewrite Vect k m
    f [Vect k m]
    gs
    -- f %% gs = r where (_,r) = quotRemMP f gs

    -- |As a convenience, a partial instance of Fractional is defined for polynomials.
    -- The instance is well-defined only for scalars, and gives an error if used on other values.
    -- The purpose of this is to allow entry of fractional scalars, in expressions such as @x/2@.
    -- On the other hand, an expression such as @2/x@ will return an error.
    instance (Eq k, Fractional k, Monomial m, Ord m, Algebra k m) => Fractional (Vect k m) where
        recip :: Vect k m -> Vect k m
    recip (V [(m :: m
    m,c :: k
    c)]) | m
    m m -> m -> Bool
    forall a. Eq a => a -> a -> Bool
    == m
    forall m. Mon m => m
    munit = [(m, k)] -> Vect k m
    forall k b. [(b, k)] -> Vect k b
    V [(m
    m,1k -> k -> k
    forall a. Fractional a => a -> a -> a
    /k
    c)]
                          | Bool
    otherwise = String -> Vect k m
    forall a. HasCallStack => String -> a
    error "Polynomial recip: only defined for scalars"
        fromRational :: Rational -> Vect k m
    fromRational x :: Rational
    x = [(m, k)] -> Vect k m
    forall k b. [(b, k)] -> Vect k b
    V [(m
    forall m. Mon m => m
    munit, Rational -> k
    forall a. Fractional a => Rational -> a
    fromRational Rational
    x)]