{-# LANGUAGE CPP #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE ExplicitNamespaces #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE LiberalTypeSynonyms #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE ParallelListComp #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
{-# OPTIONS_GHC -fplugin Data.Type.Natural.Presburger.MinMaxSolver #-}
{-# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise #-}

module Algebra.Ring.Polynomial.Monomial
  ( Monomial,
    OrderedMonomial (OrderedMonomial),
    getMonomial,
    IsOrder (..),
    IsMonomialOrder,
    MonomialOrder,
    IsStrongMonomialOrder,
    isRelativelyPrime,
    totalDegree,
    ProductOrder (..),
    productOrder,
    productOrder',
    WeightProxy,
    WeightOrder (..),
    gcdMonomial,
    divs,
    isPowerOf,
    tryDiv,
    lcmMonomial,
    Lex (..),
    EliminationType,
    EliminationOrder,
    WeightedEliminationOrder,
    eliminationOrder,
    weightedEliminationOrder,
    lex,
    revlex,
    graded,
    grlex,
    grevlex,
    weightOrder,
    Grevlex (..),
    fromList,
    Revlex (..),
    Grlex (..),
    Graded (..),
    castMonomial,
    scastMonomial,
    varMonom,
    changeMonomialOrder,
    changeMonomialOrderProxy,
    sOnes,
    withStrongMonomialOrder,
    cmpAnyMonomial,
    orderMonomial,
    ifoldMapMonom,
  )
where

import Algebra.Internal hiding ((:>))
import AlgebraicPrelude hiding (lex)
import Control.DeepSeq (NFData (..))
import qualified Control.Foldl as Fl
import Control.Lens
  ( Ixed (..),
    imap,
    makeLenses,
    makeWrapped,
    (%~),
    (&),
    (.~),
    _Wrapped,
  )
import qualified Data.Coerce as DC
import Data.Constraint (Dict (..), (:=>) (..))
import qualified Data.Constraint as C
import Data.Constraint.Forall (Forall, inst)
import Data.Kind (Type)
import Data.MonoTraversable
  ( MonoFoldable (..),
    oand,
    ofoldMap,
    ofoldl',
    ofoldlUnwrap,
    osum,
  )
import Data.Monoid (Dual (..), Sum (..))
import qualified Data.Semigroup as Semi

#if MIN_VERSION_singletons(3,0,0)
import Data.List.Singletons (SList, Length, Replicate, sReplicate)
#else
import Data.Singletons.Prelude (SList)
import Data.Singletons.Prelude.List (Length, Replicate, sReplicate)
#endif
import qualified Data.Sized as V
import Data.Type.Natural.Lemma.Order
import qualified Data.Vector.Generic as G
import qualified Data.Vector.Generic.Mutable as M
import Data.Vector.Instances ()
import qualified Data.Vector.Unboxed as UV
import qualified Prelude as P

type Monomial n = USized n Int

-- | A wrapper for monomials with a certain (monomial) order.
newtype OrderedMonomial ordering n = OrderedMonomial {OrderedMonomial ordering n -> Monomial n
getMonomial :: Monomial n}
  deriving (OrderedMonomial ordering n -> ()
(OrderedMonomial ordering n -> ())
-> NFData (OrderedMonomial ordering n)
forall a. (a -> ()) -> NFData a
forall k (ordering :: k) (n :: Nat).
OrderedMonomial ordering n -> ()
rnf :: OrderedMonomial ordering n -> ()
$crnf :: forall k (ordering :: k) (n :: Nat).
OrderedMonomial ordering n -> ()
NFData, OrderedMonomial ordering n -> OrderedMonomial ordering n -> Bool
(OrderedMonomial ordering n -> OrderedMonomial ordering n -> Bool)
-> (OrderedMonomial ordering n
    -> OrderedMonomial ordering n -> Bool)
-> Eq (OrderedMonomial ordering n)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall k (ordering :: k) (n :: Nat).
OrderedMonomial ordering n -> OrderedMonomial ordering n -> Bool
/= :: OrderedMonomial ordering n -> OrderedMonomial ordering n -> Bool
$c/= :: forall k (ordering :: k) (n :: Nat).
OrderedMonomial ordering n -> OrderedMonomial ordering n -> Bool
== :: OrderedMonomial ordering n -> OrderedMonomial ordering n -> Bool
$c== :: forall k (ordering :: k) (n :: Nat).
OrderedMonomial ordering n -> OrderedMonomial ordering n -> Bool
Eq, Int -> OrderedMonomial ordering n -> Int
OrderedMonomial ordering n -> Int
(Int -> OrderedMonomial ordering n -> Int)
-> (OrderedMonomial ordering n -> Int)
-> Hashable (OrderedMonomial ordering n)
forall a. (Int -> a -> Int) -> (a -> Int) -> Hashable a
forall k (ordering :: k) (n :: Nat).
Int -> OrderedMonomial ordering n -> Int
forall k (ordering :: k) (n :: Nat).
OrderedMonomial ordering n -> Int
hash :: OrderedMonomial ordering n -> Int
$chash :: forall k (ordering :: k) (n :: Nat).
OrderedMonomial ordering n -> Int
hashWithSalt :: Int -> OrderedMonomial ordering n -> Int
$chashWithSalt :: forall k (ordering :: k) (n :: Nat).
Int -> OrderedMonomial ordering n -> Int
Hashable)

makeLenses ''OrderedMonomial
makeWrapped ''OrderedMonomial

-- | convert NAry list into Monomial'.
fromList :: SNat n -> [Int] -> Monomial n
fromList :: SNat n -> [Int] -> Monomial n
fromList SNat n
len = SNat n -> Int -> [Int] -> Monomial n
forall (f :: * -> *) (n :: Nat) a.
(Dom f a, CFreeMonoid f) =>
SNat n -> a -> [a] -> Sized f n a
V.fromListWithDefault SNat n
len Int
0

-- We don't call Sized.zipWithSame here; it doesn't uses UV.zipWith at all!
zws :: (KnownNat n, Unbox a) => (Int -> Int -> a) -> USized n Int -> USized n Int -> USized n a
zws :: (Int -> Int -> a) -> USized n Int -> USized n Int -> USized n a
zws = ((Vector a -> USized n a
forall (f :: * -> *) (n :: Nat) a.
(KnownNat n, Dom f a) =>
f a -> Sized f n a
V.unsafeToSized' (Vector a -> USized n a)
-> (USized n Int -> Vector a) -> USized n Int -> USized n a
forall b c a. (b -> c) -> (a -> b) -> a -> c
.) ((USized n Int -> Vector a) -> USized n Int -> USized n a)
-> (USized n Int -> USized n Int -> Vector a)
-> USized n Int
-> USized n Int
-> USized n a
forall b c a. (b -> c) -> (a -> b) -> a -> c
.) ((USized n Int -> USized n Int -> Vector a)
 -> USized n Int -> USized n Int -> USized n a)
-> ((Int -> Int -> a) -> USized n Int -> USized n Int -> Vector a)
-> (Int -> Int -> a)
-> USized n Int
-> USized n Int
-> USized n a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Vector Int -> Vector Int -> Vector a)
-> (USized n Int -> Vector Int)
-> USized n Int
-> USized n Int
-> Vector a
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` USized n Int -> Vector Int
forall (f :: * -> *) (n :: Nat) a. Sized f n a -> f a
V.unsized) ((Vector Int -> Vector Int -> Vector a)
 -> USized n Int -> USized n Int -> Vector a)
-> ((Int -> Int -> a) -> Vector Int -> Vector Int -> Vector a)
-> (Int -> Int -> a)
-> USized n Int
-> USized n Int
-> Vector a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Int -> Int -> a) -> Vector Int -> Vector Int -> Vector a
forall a b c.
(Unbox a, Unbox b, Unbox c) =>
(a -> b -> c) -> Vector a -> Vector b -> Vector c
UV.zipWith
{-# INLINE zws #-}

instance KnownNat n => Multiplicative (Monomial n) where
  * :: Monomial n -> Monomial n -> Monomial n
(*) = (Int -> Int -> Int) -> Monomial n -> Monomial n -> Monomial n
forall (n :: Nat) a.
(KnownNat n, Unbox a) =>
(Int -> Int -> a) -> USized n Int -> USized n Int -> USized n a
zws Int -> Int -> Int
forall r. Additive r => r -> r -> r
(+)
  {-# INLINE (*) #-}

instance KnownNat n => Unital (Monomial n) where
  one :: Monomial n
one = SNat n -> [Int] -> Monomial n
forall (n :: Nat). SNat n -> [Int] -> Monomial n
fromList SNat n
forall (n :: Nat). KnownNat n => SNat n
sNat []

{- | Monomial' order (of degree n). This should satisfy following laws:
 (1) Totality: forall a, b (a < b || a == b || b < a)
 (2) Additivity: a <= b ==> a + c <= b + c
 (3) Non-negative: forall a, 0 <= a
-}
type MonomialOrder n = Monomial n -> Monomial n -> Ordering

isRelativelyPrime :: KnownNat n => OrderedMonomial ord n -> OrderedMonomial ord n -> Bool
isRelativelyPrime :: OrderedMonomial ord n -> OrderedMonomial ord n -> Bool
isRelativelyPrime OrderedMonomial ord n
n OrderedMonomial ord n
m = OrderedMonomial ord n
-> OrderedMonomial ord n -> OrderedMonomial ord n
forall k (n :: Nat) (ord :: k).
KnownNat n =>
OrderedMonomial ord n
-> OrderedMonomial ord n -> OrderedMonomial ord n
lcmMonomial OrderedMonomial ord n
n OrderedMonomial ord n
m OrderedMonomial ord n -> OrderedMonomial ord n -> Bool
forall a. Eq a => a -> a -> Bool
== OrderedMonomial ord n
n OrderedMonomial ord n
-> OrderedMonomial ord n -> OrderedMonomial ord n
forall r. Multiplicative r => r -> r -> r
* OrderedMonomial ord n
m

totalDegree :: OrderedMonomial ord n -> Int
totalDegree :: OrderedMonomial ord n -> Int
totalDegree = Monomial n -> Int
forall mono.
(MonoFoldable mono, Num (Element mono)) =>
mono -> Element mono
osum (Monomial n -> Int)
-> (OrderedMonomial ord n -> Monomial n)
-> OrderedMonomial ord n
-> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. OrderedMonomial ord n -> Monomial n
forall k (ordering :: k) (n :: Nat).
OrderedMonomial ordering n -> Monomial n
getMonomial
{-# INLINE totalDegree #-}

-- | Lexicographical order. This *is* a monomial order.
lex :: KnownNat n => MonomialOrder n
lex :: MonomialOrder n
lex Monomial n
m Monomial n
n = (Element (Sized Vector n (Int, Int)) -> Ordering)
-> Sized Vector n (Int, Int) -> Ordering
forall mono m.
(MonoFoldable mono, Monoid m) =>
(Element mono -> m) -> mono -> m
ofoldMap ((Int -> Int -> Ordering) -> (Int, Int) -> Ordering
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Int -> Int -> Ordering
forall a. Ord a => a -> a -> Ordering
compare) (Sized Vector n (Int, Int) -> Ordering)
-> Sized Vector n (Int, Int) -> Ordering
forall a b. (a -> b) -> a -> b
$ Monomial n -> Monomial n -> Sized Vector n (Int, Int)
forall (f :: * -> *) (n :: Nat) a b.
(Dom f a, CZip f, Dom f b, Dom f (a, b)) =>
Sized f n a -> Sized f n b -> Sized f n (a, b)
V.zipSame Monomial n
m Monomial n
n
{-# INLINE [2] lex #-}

-- | Reversed lexicographical order. This is *not* a monomial order.
revlex :: KnownNat n => MonomialOrder n
revlex :: MonomialOrder n
revlex Monomial n
xs Monomial n
ys =
  WrapOrdering -> Ordering
unWrapOrdering (WrapOrdering -> Ordering)
-> (USized n WrapOrdering -> WrapOrdering)
-> USized n WrapOrdering
-> Ordering
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (WrapOrdering -> Element (USized n WrapOrdering) -> WrapOrdering)
-> WrapOrdering -> USized n WrapOrdering -> WrapOrdering
forall mono a.
MonoFoldable mono =>
(a -> Element mono -> a) -> a -> mono -> a
ofoldl' ((WrapOrdering -> WrapOrdering -> WrapOrdering)
-> WrapOrdering -> WrapOrdering -> WrapOrdering
forall a b c. (a -> b -> c) -> b -> a -> c
flip WrapOrdering -> WrapOrdering -> WrapOrdering
forall a. Semigroup a => a -> a -> a
(<>)) (Ordering -> WrapOrdering
WrapOrdering Ordering
EQ) (USized n WrapOrdering -> Ordering)
-> USized n WrapOrdering -> Ordering
forall a b. (a -> b) -> a -> b
$ (Int -> Int -> WrapOrdering)
-> Monomial n -> Monomial n -> USized n WrapOrdering
forall (n :: Nat) a.
(KnownNat n, Unbox a) =>
(Int -> Int -> a) -> USized n Int -> USized n Int -> USized n a
zws ((Ordering -> WrapOrdering
WrapOrdering (Ordering -> WrapOrdering)
-> (Int -> Ordering) -> Int -> WrapOrdering
forall b c a. (b -> c) -> (a -> b) -> a -> c
.) ((Int -> Ordering) -> Int -> WrapOrdering)
-> (Int -> Int -> Ordering) -> Int -> Int -> WrapOrdering
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Int -> Int -> Ordering) -> Int -> Int -> Ordering
forall a b c. (a -> b -> c) -> b -> a -> c
flip Int -> Int -> Ordering
forall a. Ord a => a -> a -> Ordering
compare) Monomial n
xs Monomial n
ys
{-# INLINE [2] revlex #-}

-- | Convert ordering into graded one.
graded :: MonomialOrder n -> MonomialOrder n
graded :: MonomialOrder n -> MonomialOrder n
graded MonomialOrder n
cmp Monomial n
xs Monomial n
ys = (Monomial n -> Int) -> MonomialOrder n
forall a b. Ord a => (b -> a) -> b -> b -> Ordering
comparing Monomial n -> Int
forall mono.
(MonoFoldable mono, Num (Element mono)) =>
mono -> Element mono
osum Monomial n
xs Monomial n
ys Ordering -> Ordering -> Ordering
forall a. Semigroup a => a -> a -> a
<> MonomialOrder n
cmp Monomial n
xs Monomial n
ys
{-# INLINE [2] graded #-}

{-# RULES
"graded/graded" [~1] forall x. graded (graded x) = graded x
  #-}

-- | Graded lexicographical order. This *is* a monomial order.
grlex :: KnownNat n => MonomialOrder n
grlex :: MonomialOrder n
grlex = MonomialOrder n -> MonomialOrder n
forall (n :: Nat). MonomialOrder n -> MonomialOrder n
graded MonomialOrder n
forall (n :: Nat). KnownNat n => MonomialOrder n
lex
{-# INLINE [2] grlex #-}

newtype WrapOrdering = WrapOrdering {WrapOrdering -> Ordering
unWrapOrdering :: Ordering}
  deriving (ReadPrec [WrapOrdering]
ReadPrec WrapOrdering
Int -> ReadS WrapOrdering
ReadS [WrapOrdering]
(Int -> ReadS WrapOrdering)
-> ReadS [WrapOrdering]
-> ReadPrec WrapOrdering
-> ReadPrec [WrapOrdering]
-> Read WrapOrdering
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
readListPrec :: ReadPrec [WrapOrdering]
$creadListPrec :: ReadPrec [WrapOrdering]
readPrec :: ReadPrec WrapOrdering
$creadPrec :: ReadPrec WrapOrdering
readList :: ReadS [WrapOrdering]
$creadList :: ReadS [WrapOrdering]
readsPrec :: Int -> ReadS WrapOrdering
$creadsPrec :: Int -> ReadS WrapOrdering
Read, Int -> WrapOrdering -> ShowS
[WrapOrdering] -> ShowS
WrapOrdering -> String
(Int -> WrapOrdering -> ShowS)
-> (WrapOrdering -> String)
-> ([WrapOrdering] -> ShowS)
-> Show WrapOrdering
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [WrapOrdering] -> ShowS
$cshowList :: [WrapOrdering] -> ShowS
show :: WrapOrdering -> String
$cshow :: WrapOrdering -> String
showsPrec :: Int -> WrapOrdering -> ShowS
$cshowsPrec :: Int -> WrapOrdering -> ShowS
Show, WrapOrdering -> WrapOrdering -> Bool
(WrapOrdering -> WrapOrdering -> Bool)
-> (WrapOrdering -> WrapOrdering -> Bool) -> Eq WrapOrdering
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: WrapOrdering -> WrapOrdering -> Bool
$c/= :: WrapOrdering -> WrapOrdering -> Bool
== :: WrapOrdering -> WrapOrdering -> Bool
$c== :: WrapOrdering -> WrapOrdering -> Bool
Eq, Eq WrapOrdering
Eq WrapOrdering
-> (WrapOrdering -> WrapOrdering -> Ordering)
-> (WrapOrdering -> WrapOrdering -> Bool)
-> (WrapOrdering -> WrapOrdering -> Bool)
-> (WrapOrdering -> WrapOrdering -> Bool)
-> (WrapOrdering -> WrapOrdering -> Bool)
-> (WrapOrdering -> WrapOrdering -> WrapOrdering)
-> (WrapOrdering -> WrapOrdering -> WrapOrdering)
-> Ord WrapOrdering
WrapOrdering -> WrapOrdering -> Bool
WrapOrdering -> WrapOrdering -> Ordering
WrapOrdering -> WrapOrdering -> WrapOrdering
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: WrapOrdering -> WrapOrdering -> WrapOrdering
$cmin :: WrapOrdering -> WrapOrdering -> WrapOrdering
max :: WrapOrdering -> WrapOrdering -> WrapOrdering
$cmax :: WrapOrdering -> WrapOrdering -> WrapOrdering
>= :: WrapOrdering -> WrapOrdering -> Bool
$c>= :: WrapOrdering -> WrapOrdering -> Bool
> :: WrapOrdering -> WrapOrdering -> Bool
$c> :: WrapOrdering -> WrapOrdering -> Bool
<= :: WrapOrdering -> WrapOrdering -> Bool
$c<= :: WrapOrdering -> WrapOrdering -> Bool
< :: WrapOrdering -> WrapOrdering -> Bool
$c< :: WrapOrdering -> WrapOrdering -> Bool
compare :: WrapOrdering -> WrapOrdering -> Ordering
$ccompare :: WrapOrdering -> WrapOrdering -> Ordering
$cp1Ord :: Eq WrapOrdering
Ord, Semigroup WrapOrdering
WrapOrdering
Semigroup WrapOrdering
-> WrapOrdering
-> (WrapOrdering -> WrapOrdering -> WrapOrdering)
-> ([WrapOrdering] -> WrapOrdering)
-> Monoid WrapOrdering
[WrapOrdering] -> WrapOrdering
WrapOrdering -> WrapOrdering -> WrapOrdering
forall a.
Semigroup a -> a -> (a -> a -> a) -> ([a] -> a) -> Monoid a
mconcat :: [WrapOrdering] -> WrapOrdering
$cmconcat :: [WrapOrdering] -> WrapOrdering
mappend :: WrapOrdering -> WrapOrdering -> WrapOrdering
$cmappend :: WrapOrdering -> WrapOrdering -> WrapOrdering
mempty :: WrapOrdering
$cmempty :: WrapOrdering
$cp1Monoid :: Semigroup WrapOrdering
Monoid, b -> WrapOrdering -> WrapOrdering
NonEmpty WrapOrdering -> WrapOrdering
WrapOrdering -> WrapOrdering -> WrapOrdering
(WrapOrdering -> WrapOrdering -> WrapOrdering)
-> (NonEmpty WrapOrdering -> WrapOrdering)
-> (forall b. Integral b => b -> WrapOrdering -> WrapOrdering)
-> Semigroup WrapOrdering
forall b. Integral b => b -> WrapOrdering -> WrapOrdering
forall a.
(a -> a -> a)
-> (NonEmpty a -> a)
-> (forall b. Integral b => b -> a -> a)
-> Semigroup a
stimes :: b -> WrapOrdering -> WrapOrdering
$cstimes :: forall b. Integral b => b -> WrapOrdering -> WrapOrdering
sconcat :: NonEmpty WrapOrdering -> WrapOrdering
$csconcat :: NonEmpty WrapOrdering -> WrapOrdering
<> :: WrapOrdering -> WrapOrdering -> WrapOrdering
$c<> :: WrapOrdering -> WrapOrdering -> WrapOrdering
Semi.Semigroup)

newtype instance UV.Vector WrapOrdering = V_WrapOrdering (UV.Vector Word8)

newtype instance UV.MVector s WrapOrdering = MV_WrapOrdering (UV.MVector s Word8)

instance Unbox WrapOrdering

instance M.MVector UV.MVector WrapOrdering where
  {-# INLINE basicLength #-}
  {-# INLINE basicUnsafeSlice #-}
  {-# INLINE basicOverlaps #-}
  {-# INLINE basicUnsafeNew #-}
  {-# INLINE basicInitialize #-}
  {-# INLINE basicUnsafeReplicate #-}
  {-# INLINE basicUnsafeRead #-}
  {-# INLINE basicUnsafeWrite #-}
  {-# INLINE basicClear #-}
  {-# INLINE basicSet #-}
  {-# INLINE basicUnsafeCopy #-}
  {-# INLINE basicUnsafeGrow #-}
  basicLength :: MVector s WrapOrdering -> Int
basicLength (MV_WrapOrdering v) = MVector s Word8 -> Int
forall (v :: * -> * -> *) a s. MVector v a => v s a -> Int
M.basicLength MVector s Word8
v
  basicUnsafeSlice :: Int -> Int -> MVector s WrapOrdering -> MVector s WrapOrdering
basicUnsafeSlice Int
i Int
n (MV_WrapOrdering v) = MVector s Word8 -> MVector s WrapOrdering
forall s. MVector s Word8 -> MVector s WrapOrdering
MV_WrapOrdering (MVector s Word8 -> MVector s WrapOrdering)
-> MVector s Word8 -> MVector s WrapOrdering
forall a b. (a -> b) -> a -> b
$ Int -> Int -> MVector s Word8 -> MVector s Word8
forall (v :: * -> * -> *) a s.
MVector v a =>
Int -> Int -> v s a -> v s a
M.basicUnsafeSlice Int
i Int
n MVector s Word8
v
  basicOverlaps :: MVector s WrapOrdering -> MVector s WrapOrdering -> Bool
basicOverlaps (MV_WrapOrdering v1) (MV_WrapOrdering v2) = MVector s Word8 -> MVector s Word8 -> Bool
forall (v :: * -> * -> *) a s.
MVector v a =>
v s a -> v s a -> Bool
M.basicOverlaps MVector s Word8
v1 MVector s Word8
v2
  basicUnsafeNew :: Int -> m (MVector (PrimState m) WrapOrdering)
basicUnsafeNew Int
n = MVector (PrimState m) Word8 -> MVector (PrimState m) WrapOrdering
forall s. MVector s Word8 -> MVector s WrapOrdering
MV_WrapOrdering (MVector (PrimState m) Word8 -> MVector (PrimState m) WrapOrdering)
-> m (MVector (PrimState m) Word8)
-> m (MVector (PrimState m) WrapOrdering)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Int -> m (MVector (PrimState m) Word8)
forall (v :: * -> * -> *) a (m :: * -> *).
(MVector v a, PrimMonad m) =>
Int -> m (v (PrimState m) a)
M.basicUnsafeNew Int
n
  basicInitialize :: MVector (PrimState m) WrapOrdering -> m ()
basicInitialize (MV_WrapOrdering v) = MVector (PrimState m) Word8 -> m ()
forall (v :: * -> * -> *) a (m :: * -> *).
(MVector v a, PrimMonad m) =>
v (PrimState m) a -> m ()
M.basicInitialize MVector (PrimState m) Word8
v
  basicUnsafeReplicate :: Int -> WrapOrdering -> m (MVector (PrimState m) WrapOrdering)
basicUnsafeReplicate Int
n WrapOrdering
x = MVector (PrimState m) Word8 -> MVector (PrimState m) WrapOrdering
forall s. MVector s Word8 -> MVector s WrapOrdering
MV_WrapOrdering (MVector (PrimState m) Word8 -> MVector (PrimState m) WrapOrdering)
-> m (MVector (PrimState m) Word8)
-> m (MVector (PrimState m) WrapOrdering)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Int -> Word8 -> m (MVector (PrimState m) Word8)
forall (v :: * -> * -> *) a (m :: * -> *).
(MVector v a, PrimMonad m) =>
Int -> a -> m (v (PrimState m) a)
M.basicUnsafeReplicate Int
n (WrapOrdering -> Word8
fromWrapOrdering WrapOrdering
x)
  basicUnsafeRead :: MVector (PrimState m) WrapOrdering -> Int -> m WrapOrdering
basicUnsafeRead (MV_WrapOrdering v) Int
i = Word8 -> WrapOrdering
toWrapOrdering (Word8 -> WrapOrdering) -> m Word8 -> m WrapOrdering
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> MVector (PrimState m) Word8 -> Int -> m Word8
forall (v :: * -> * -> *) a (m :: * -> *).
(MVector v a, PrimMonad m) =>
v (PrimState m) a -> Int -> m a
M.basicUnsafeRead MVector (PrimState m) Word8
v Int
i
  basicUnsafeWrite :: MVector (PrimState m) WrapOrdering -> Int -> WrapOrdering -> m ()
basicUnsafeWrite (MV_WrapOrdering v) Int
i WrapOrdering
x = MVector (PrimState m) Word8 -> Int -> Word8 -> m ()
forall (v :: * -> * -> *) a (m :: * -> *).
(MVector v a, PrimMonad m) =>
v (PrimState m) a -> Int -> a -> m ()
M.basicUnsafeWrite MVector (PrimState m) Word8
v Int
i (WrapOrdering -> Word8
fromWrapOrdering WrapOrdering
x)
  basicClear :: MVector (PrimState m) WrapOrdering -> m ()
basicClear (MV_WrapOrdering v) = MVector (PrimState m) Word8 -> m ()
forall (v :: * -> * -> *) a (m :: * -> *).
(MVector v a, PrimMonad m) =>
v (PrimState m) a -> m ()
M.basicClear MVector (PrimState m) Word8
v
  basicSet :: MVector (PrimState m) WrapOrdering -> WrapOrdering -> m ()
basicSet (MV_WrapOrdering v) WrapOrdering
x = MVector (PrimState m) Word8 -> Word8 -> m ()
forall (v :: * -> * -> *) a (m :: * -> *).
(MVector v a, PrimMonad m) =>
v (PrimState m) a -> a -> m ()
M.basicSet MVector (PrimState m) Word8
v (WrapOrdering -> Word8
fromWrapOrdering WrapOrdering
x)
  basicUnsafeCopy :: MVector (PrimState m) WrapOrdering
-> MVector (PrimState m) WrapOrdering -> m ()
basicUnsafeCopy (MV_WrapOrdering v1) (MV_WrapOrdering v2) = MVector (PrimState m) Word8 -> MVector (PrimState m) Word8 -> m ()
forall (v :: * -> * -> *) a (m :: * -> *).
(MVector v a, PrimMonad m) =>
v (PrimState m) a -> v (PrimState m) a -> m ()
M.basicUnsafeCopy MVector (PrimState m) Word8
v1 MVector (PrimState m) Word8
v2
  basicUnsafeMove :: MVector (PrimState m) WrapOrdering
-> MVector (PrimState m) WrapOrdering -> m ()
basicUnsafeMove (MV_WrapOrdering v1) (MV_WrapOrdering v2) = MVector (PrimState m) Word8 -> MVector (PrimState m) Word8 -> m ()
forall (v :: * -> * -> *) a (m :: * -> *).
(MVector v a, PrimMonad m) =>
v (PrimState m) a -> v (PrimState m) a -> m ()
M.basicUnsafeMove MVector (PrimState m) Word8
v1 MVector (PrimState m) Word8
v2
  basicUnsafeGrow :: MVector (PrimState m) WrapOrdering
-> Int -> m (MVector (PrimState m) WrapOrdering)
basicUnsafeGrow (MV_WrapOrdering v) Int
n = MVector (PrimState m) Word8 -> MVector (PrimState m) WrapOrdering
forall s. MVector s Word8 -> MVector s WrapOrdering
MV_WrapOrdering (MVector (PrimState m) Word8 -> MVector (PrimState m) WrapOrdering)
-> m (MVector (PrimState m) Word8)
-> m (MVector (PrimState m) WrapOrdering)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> MVector (PrimState m) Word8
-> Int -> m (MVector (PrimState m) Word8)
forall (v :: * -> * -> *) a (m :: * -> *).
(MVector v a, PrimMonad m) =>
v (PrimState m) a -> Int -> m (v (PrimState m) a)
M.basicUnsafeGrow MVector (PrimState m) Word8
v Int
n

instance G.Vector UV.Vector WrapOrdering where
  {-# INLINE basicUnsafeFreeze #-}
  {-# INLINE basicUnsafeThaw #-}
  {-# INLINE basicLength #-}
  {-# INLINE basicUnsafeSlice #-}
  {-# INLINE basicUnsafeIndexM #-}
  {-# INLINE elemseq #-}
  basicUnsafeFreeze :: Mutable Vector (PrimState m) WrapOrdering
-> m (Vector WrapOrdering)
basicUnsafeFreeze (MV_WrapOrdering v) = Vector Word8 -> Vector WrapOrdering
V_WrapOrdering (Vector Word8 -> Vector WrapOrdering)
-> m (Vector Word8) -> m (Vector WrapOrdering)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Mutable Vector (PrimState m) Word8 -> m (Vector Word8)
forall (v :: * -> *) a (m :: * -> *).
(Vector v a, PrimMonad m) =>
Mutable v (PrimState m) a -> m (v a)
G.basicUnsafeFreeze MVector (PrimState m) Word8
Mutable Vector (PrimState m) Word8
v
  basicUnsafeThaw :: Vector WrapOrdering
-> m (Mutable Vector (PrimState m) WrapOrdering)
basicUnsafeThaw (V_WrapOrdering v) = MVector (PrimState m) Word8 -> MVector (PrimState m) WrapOrdering
forall s. MVector s Word8 -> MVector s WrapOrdering
MV_WrapOrdering (MVector (PrimState m) Word8 -> MVector (PrimState m) WrapOrdering)
-> m (MVector (PrimState m) Word8)
-> m (MVector (PrimState m) WrapOrdering)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Vector Word8 -> m (Mutable Vector (PrimState m) Word8)
forall (v :: * -> *) a (m :: * -> *).
(Vector v a, PrimMonad m) =>
v a -> m (Mutable v (PrimState m) a)
G.basicUnsafeThaw Vector Word8
v
  basicLength :: Vector WrapOrdering -> Int
basicLength (V_WrapOrdering v) = Vector Word8 -> Int
forall (v :: * -> *) a. Vector v a => v a -> Int
G.basicLength Vector Word8
v
  basicUnsafeSlice :: Int -> Int -> Vector WrapOrdering -> Vector WrapOrdering
basicUnsafeSlice Int
i Int
n (V_WrapOrdering v) = Vector Word8 -> Vector WrapOrdering
V_WrapOrdering (Vector Word8 -> Vector WrapOrdering)
-> Vector Word8 -> Vector WrapOrdering
forall a b. (a -> b) -> a -> b
$ Int -> Int -> Vector Word8 -> Vector Word8
forall (v :: * -> *) a. Vector v a => Int -> Int -> v a -> v a
G.basicUnsafeSlice Int
i Int
n Vector Word8
v
  basicUnsafeIndexM :: Vector WrapOrdering -> Int -> m WrapOrdering
basicUnsafeIndexM (V_WrapOrdering v) Int
i = Word8 -> WrapOrdering
toWrapOrdering (Word8 -> WrapOrdering) -> m Word8 -> m WrapOrdering
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Vector Word8 -> Int -> m Word8
forall (v :: * -> *) a (m :: * -> *).
(Vector v a, Monad m) =>
v a -> Int -> m a
G.basicUnsafeIndexM Vector Word8
v Int
i
  basicUnsafeCopy :: Mutable Vector (PrimState m) WrapOrdering
-> Vector WrapOrdering -> m ()
basicUnsafeCopy (MV_WrapOrdering mv) (V_WrapOrdering v) = Mutable Vector (PrimState m) Word8 -> Vector Word8 -> m ()
forall (v :: * -> *) a (m :: * -> *).
(Vector v a, PrimMonad m) =>
Mutable v (PrimState m) a -> v a -> m ()
G.basicUnsafeCopy MVector (PrimState m) Word8
Mutable Vector (PrimState m) Word8
mv Vector Word8
v
  elemseq :: Vector WrapOrdering -> WrapOrdering -> b -> b
elemseq Vector WrapOrdering
_ = WrapOrdering -> b -> b
seq

fromWrapOrdering :: WrapOrdering -> Word8
{-# INLINE fromWrapOrdering #-}
fromWrapOrdering :: WrapOrdering -> Word8
fromWrapOrdering (WrapOrdering Ordering
LT) = Word8
0
fromWrapOrdering (WrapOrdering Ordering
EQ) = Word8
1
fromWrapOrdering (WrapOrdering Ordering
GT) = Word8
2

toWrapOrdering :: Word8 -> WrapOrdering
{-# INLINE toWrapOrdering #-}
toWrapOrdering :: Word8 -> WrapOrdering
toWrapOrdering Word8
0 = Ordering -> WrapOrdering
WrapOrdering Ordering
LT
toWrapOrdering Word8
1 = Ordering -> WrapOrdering
WrapOrdering Ordering
EQ
toWrapOrdering Word8
_ = Ordering -> WrapOrdering
WrapOrdering Ordering
GT

-- | Graded reversed lexicographical order. This *is* a monomial order.
grevlex :: MonomialOrder n
grevlex :: MonomialOrder n
grevlex = MonomialOrder n
forall (n :: Nat). MonomialOrder n
grevlexF
{-# INLINE [2] grevlex #-}

grevlexF :: MonomialOrder n
grevlexF :: MonomialOrder n
grevlexF = ((forall x.
 (x -> (Int, Int) -> x)
 -> x -> (x -> Ordering) -> Vector (Int, Int) -> Ordering)
-> Fold (Int, Int) Ordering -> Vector (Int, Int) -> Ordering
forall a b r.
(forall x. (x -> a -> x) -> x -> (x -> b) -> r) -> Fold a b -> r
Fl.purely forall x.
(x -> (Int, Int) -> x)
-> x -> (x -> Ordering) -> Vector (Int, Int) -> Ordering
forall mono x b.
MonoFoldable mono =>
(x -> Element mono -> x) -> x -> (x -> b) -> mono -> b
ofoldlUnwrap Fold (Int, Int) Ordering
body (Vector (Int, Int) -> Ordering)
-> (Sized Vector n Int -> Vector (Int, Int))
-> Sized Vector n Int
-> Ordering
forall b c a. (b -> c) -> (a -> b) -> a -> c
.) ((Sized Vector n Int -> Vector (Int, Int))
 -> Sized Vector n Int -> Ordering)
-> (Sized Vector n Int -> Sized Vector n Int -> Vector (Int, Int))
-> MonomialOrder n
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Vector Int -> Vector Int -> Vector (Int, Int)
forall a b.
(Unbox a, Unbox b) =>
Vector a -> Vector b -> Vector (a, b)
UV.zip (Vector Int -> Vector Int -> Vector (Int, Int))
-> (Sized Vector n Int -> Vector Int)
-> Sized Vector n Int
-> Sized Vector n Int
-> Vector (Int, Int)
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` Sized Vector n Int -> Vector Int
forall (f :: * -> *) (n :: Nat) a. Sized f n a -> f a
V.unsized)
  where
    body :: Fl.Fold (Int, Int) Ordering
    body :: Fold (Int, Int) Ordering
body =
      Ordering -> Ordering -> Ordering
forall a. Semigroup a => a -> a -> a
(<>) (Ordering -> Ordering -> Ordering)
-> Fold (Int, Int) Ordering
-> Fold (Int, Int) (Ordering -> Ordering)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((Int, Int) -> (Sum Int, Sum Int))
-> ((Sum Int, Sum Int) -> Ordering) -> Fold (Int, Int) Ordering
forall w a b. Monoid w => (a -> w) -> (w -> b) -> Fold a b
Fl.foldMap (Coercible (Int, Int) (Sum Int, Sum Int) =>
(Int, Int) -> (Sum Int, Sum Int)
DC.coerce @_ @(Sum Int, Sum Int)) ((Sum Int -> Sum Int -> Ordering) -> (Sum Int, Sum Int) -> Ordering
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Sum Int -> Sum Int -> Ordering
forall a. Ord a => a -> a -> Ordering
compare)
        Fold (Int, Int) (Ordering -> Ordering)
-> Fold (Int, Int) Ordering -> Fold (Int, Int) Ordering
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ((Int, Int) -> Dual Ordering)
-> (Dual Ordering -> Ordering) -> Fold (Int, Int) Ordering
forall w a b. Monoid w => (a -> w) -> (w -> b) -> Fold a b
Fl.foldMap (Ordering -> Dual Ordering
forall a. a -> Dual a
Dual (Ordering -> Dual Ordering)
-> ((Int, Int) -> Ordering) -> (Int, Int) -> Dual Ordering
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Int -> Int -> Ordering) -> (Int, Int) -> Ordering
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry ((Int -> Int -> Ordering) -> Int -> Int -> Ordering
forall a b c. (a -> b -> c) -> b -> a -> c
flip Int -> Int -> Ordering
forall a. Ord a => a -> a -> Ordering
compare)) Dual Ordering -> Ordering
forall a. Dual a -> a
getDual
{-# INLINE grevlexF #-}

instance KnownNat n => Show (OrderedMonomial ord n) where
  show :: OrderedMonomial ord n -> String
show OrderedMonomial ord n
xs =
    let vs :: [String]
vs =
          [Maybe String] -> [String]
forall a. [Maybe a] -> [a]
catMaybes ([Maybe String] -> [String]) -> [Maybe String] -> [String]
forall a b. (a -> b) -> a -> b
$
            (Int -> Int -> Maybe String) -> [Int] -> [Maybe String]
forall i (f :: * -> *) a b.
FunctorWithIndex i f =>
(i -> a -> b) -> f a -> f b
imap
              ( \Int
n Int
i ->
                  if Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
0
                    then String -> Maybe String
forall a. a -> Maybe a
Just (String
"X_" String -> ShowS
forall w. Monoid w => w -> w -> w
++ Int -> String
forall a. Show a => a -> String
show Int
n String -> ShowS
forall w. Monoid w => w -> w -> w
++ if Int
i Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
1 then String
"" else String
"^" String -> ShowS
forall w. Monoid w => w -> w -> w
++ Int -> String
forall a. Show a => a -> String
show Int
i)
                    else Maybe String
forall a. Maybe a
Nothing
              )
              ([Int] -> [Maybe String]) -> [Int] -> [Maybe String]
forall a b. (a -> b) -> a -> b
$ Monomial n -> [Element (Monomial n)]
forall mono. MonoFoldable mono => mono -> [Element mono]
otoList (Monomial n -> [Element (Monomial n)])
-> Monomial n -> [Element (Monomial n)]
forall a b. (a -> b) -> a -> b
$ OrderedMonomial ord n -> Monomial n
forall k (ordering :: k) (n :: Nat).
OrderedMonomial ordering n -> Monomial n
getMonomial OrderedMonomial ord n
xs
     in if [String] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [String]
vs then String
"1" else [String] -> String
unwords [String]
vs

instance KnownNat n => Multiplicative (OrderedMonomial ord n) where
  OrderedMonomial Monomial n
n * :: OrderedMonomial ord n
-> OrderedMonomial ord n -> OrderedMonomial ord n
* OrderedMonomial Monomial n
m = Monomial n -> OrderedMonomial ord n
forall k (ordering :: k) (n :: Nat).
Monomial n -> OrderedMonomial ordering n
OrderedMonomial (Monomial n -> OrderedMonomial ord n)
-> Monomial n -> OrderedMonomial ord n
forall a b. (a -> b) -> a -> b
$ (Int -> Int -> Int) -> Monomial n -> Monomial n -> Monomial n
forall (n :: Nat) a.
(KnownNat n, Unbox a) =>
(Int -> Int -> a) -> USized n Int -> USized n Int -> USized n a
zws Int -> Int -> Int
forall r. Additive r => r -> r -> r
(+) Monomial n
n Monomial n
m

instance KnownNat n => Division (OrderedMonomial ord n) where
  recip :: OrderedMonomial ord n -> OrderedMonomial ord n
recip (OrderedMonomial Monomial n
n) = Monomial n -> OrderedMonomial ord n
forall k (ordering :: k) (n :: Nat).
Monomial n -> OrderedMonomial ordering n
OrderedMonomial (Monomial n -> OrderedMonomial ord n)
-> Monomial n -> OrderedMonomial ord n
forall a b. (a -> b) -> a -> b
$ (Int -> Int) -> Monomial n -> Monomial n
forall (f :: * -> *) (n :: Nat) a b.
(CFreeMonoid f, Dom f a, Dom f b) =>
(a -> b) -> Sized f n a -> Sized f n b
V.map Int -> Int
forall a. Num a => a -> a
P.negate Monomial n
n
  OrderedMonomial Monomial n
n / :: OrderedMonomial ord n
-> OrderedMonomial ord n -> OrderedMonomial ord n
/ OrderedMonomial Monomial n
m = Monomial n -> OrderedMonomial ord n
forall k (ordering :: k) (n :: Nat).
Monomial n -> OrderedMonomial ordering n
OrderedMonomial (Monomial n -> OrderedMonomial ord n)
-> Monomial n -> OrderedMonomial ord n
forall a b. (a -> b) -> a -> b
$ (Int -> Int -> Int) -> Monomial n -> Monomial n -> Monomial n
forall (n :: Nat) a.
(KnownNat n, Unbox a) =>
(Int -> Int -> a) -> USized n Int -> USized n Int -> USized n a
zws (-) Monomial n
n Monomial n
m

instance KnownNat n => Unital (OrderedMonomial ord n) where
  one :: OrderedMonomial ord n
one = Monomial n -> OrderedMonomial ord n
forall k (ordering :: k) (n :: Nat).
Monomial n -> OrderedMonomial ordering n
OrderedMonomial Monomial n
forall r. Unital r => r
one

-- | Class to lookup ordering from its (type-level) name.
class IsOrder (n :: Nat) (ordering :: Type) where
  cmpMonomial :: Proxy ordering -> MonomialOrder n

-- * Names for orderings.

--   We didn't choose to define one single type for ordering names for the extensibility.

-- | Lexicographical order
data Lex = Lex
  deriving (Int -> Lex -> ShowS
[Lex] -> ShowS
Lex -> String
(Int -> Lex -> ShowS)
-> (Lex -> String) -> ([Lex] -> ShowS) -> Show Lex
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Lex] -> ShowS
$cshowList :: [Lex] -> ShowS
show :: Lex -> String
$cshow :: Lex -> String
showsPrec :: Int -> Lex -> ShowS
$cshowsPrec :: Int -> Lex -> ShowS
Show, Lex -> Lex -> Bool
(Lex -> Lex -> Bool) -> (Lex -> Lex -> Bool) -> Eq Lex
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Lex -> Lex -> Bool
$c/= :: Lex -> Lex -> Bool
== :: Lex -> Lex -> Bool
$c== :: Lex -> Lex -> Bool
Eq, Eq Lex
Eq Lex
-> (Lex -> Lex -> Ordering)
-> (Lex -> Lex -> Bool)
-> (Lex -> Lex -> Bool)
-> (Lex -> Lex -> Bool)
-> (Lex -> Lex -> Bool)
-> (Lex -> Lex -> Lex)
-> (Lex -> Lex -> Lex)
-> Ord Lex
Lex -> Lex -> Bool
Lex -> Lex -> Ordering
Lex -> Lex -> Lex
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Lex -> Lex -> Lex
$cmin :: Lex -> Lex -> Lex
max :: Lex -> Lex -> Lex
$cmax :: Lex -> Lex -> Lex
>= :: Lex -> Lex -> Bool
$c>= :: Lex -> Lex -> Bool
> :: Lex -> Lex -> Bool
$c> :: Lex -> Lex -> Bool
<= :: Lex -> Lex -> Bool
$c<= :: Lex -> Lex -> Bool
< :: Lex -> Lex -> Bool
$c< :: Lex -> Lex -> Bool
compare :: Lex -> Lex -> Ordering
$ccompare :: Lex -> Lex -> Ordering
$cp1Ord :: Eq Lex
Ord)

-- | Reversed lexicographical order
data Revlex = Revlex
  deriving (Int -> Revlex -> ShowS
[Revlex] -> ShowS
Revlex -> String
(Int -> Revlex -> ShowS)
-> (Revlex -> String) -> ([Revlex] -> ShowS) -> Show Revlex
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Revlex] -> ShowS
$cshowList :: [Revlex] -> ShowS
show :: Revlex -> String
$cshow :: Revlex -> String
showsPrec :: Int -> Revlex -> ShowS
$cshowsPrec :: Int -> Revlex -> ShowS
Show, Revlex -> Revlex -> Bool
(Revlex -> Revlex -> Bool)
-> (Revlex -> Revlex -> Bool) -> Eq Revlex
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Revlex -> Revlex -> Bool
$c/= :: Revlex -> Revlex -> Bool
== :: Revlex -> Revlex -> Bool
$c== :: Revlex -> Revlex -> Bool
Eq, Eq Revlex
Eq Revlex
-> (Revlex -> Revlex -> Ordering)
-> (Revlex -> Revlex -> Bool)
-> (Revlex -> Revlex -> Bool)
-> (Revlex -> Revlex -> Bool)
-> (Revlex -> Revlex -> Bool)
-> (Revlex -> Revlex -> Revlex)
-> (Revlex -> Revlex -> Revlex)
-> Ord Revlex
Revlex -> Revlex -> Bool
Revlex -> Revlex -> Ordering
Revlex -> Revlex -> Revlex
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Revlex -> Revlex -> Revlex
$cmin :: Revlex -> Revlex -> Revlex
max :: Revlex -> Revlex -> Revlex
$cmax :: Revlex -> Revlex -> Revlex
>= :: Revlex -> Revlex -> Bool
$c>= :: Revlex -> Revlex -> Bool
> :: Revlex -> Revlex -> Bool
$c> :: Revlex -> Revlex -> Bool
<= :: Revlex -> Revlex -> Bool
$c<= :: Revlex -> Revlex -> Bool
< :: Revlex -> Revlex -> Bool
$c< :: Revlex -> Revlex -> Bool
compare :: Revlex -> Revlex -> Ordering
$ccompare :: Revlex -> Revlex -> Ordering
$cp1Ord :: Eq Revlex
Ord)

-- | Graded reversed lexicographical order. Same as @Graded Revlex@.
data Grevlex = Grevlex
  deriving (Int -> Grevlex -> ShowS
[Grevlex] -> ShowS
Grevlex -> String
(Int -> Grevlex -> ShowS)
-> (Grevlex -> String) -> ([Grevlex] -> ShowS) -> Show Grevlex
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Grevlex] -> ShowS
$cshowList :: [Grevlex] -> ShowS
show :: Grevlex -> String
$cshow :: Grevlex -> String
showsPrec :: Int -> Grevlex -> ShowS
$cshowsPrec :: Int -> Grevlex -> ShowS
Show, Grevlex -> Grevlex -> Bool
(Grevlex -> Grevlex -> Bool)
-> (Grevlex -> Grevlex -> Bool) -> Eq Grevlex
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Grevlex -> Grevlex -> Bool
$c/= :: Grevlex -> Grevlex -> Bool
== :: Grevlex -> Grevlex -> Bool
$c== :: Grevlex -> Grevlex -> Bool
Eq, Eq Grevlex
Eq Grevlex
-> (Grevlex -> Grevlex -> Ordering)
-> (Grevlex -> Grevlex -> Bool)
-> (Grevlex -> Grevlex -> Bool)
-> (Grevlex -> Grevlex -> Bool)
-> (Grevlex -> Grevlex -> Bool)
-> (Grevlex -> Grevlex -> Grevlex)
-> (Grevlex -> Grevlex -> Grevlex)
-> Ord Grevlex
Grevlex -> Grevlex -> Bool
Grevlex -> Grevlex -> Ordering
Grevlex -> Grevlex -> Grevlex
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Grevlex -> Grevlex -> Grevlex
$cmin :: Grevlex -> Grevlex -> Grevlex
max :: Grevlex -> Grevlex -> Grevlex
$cmax :: Grevlex -> Grevlex -> Grevlex
>= :: Grevlex -> Grevlex -> Bool
$c>= :: Grevlex -> Grevlex -> Bool
> :: Grevlex -> Grevlex -> Bool
$c> :: Grevlex -> Grevlex -> Bool
<= :: Grevlex -> Grevlex -> Bool
$c<= :: Grevlex -> Grevlex -> Bool
< :: Grevlex -> Grevlex -> Bool
$c< :: Grevlex -> Grevlex -> Bool
compare :: Grevlex -> Grevlex -> Ordering
$ccompare :: Grevlex -> Grevlex -> Ordering
$cp1Ord :: Eq Grevlex
Ord)

-- | Graded lexicographical order. Same as @Graded Lex@.
data Grlex = Grlex
  deriving (Int -> Grlex -> ShowS
[Grlex] -> ShowS
Grlex -> String
(Int -> Grlex -> ShowS)
-> (Grlex -> String) -> ([Grlex] -> ShowS) -> Show Grlex
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Grlex] -> ShowS
$cshowList :: [Grlex] -> ShowS
show :: Grlex -> String
$cshow :: Grlex -> String
showsPrec :: Int -> Grlex -> ShowS
$cshowsPrec :: Int -> Grlex -> ShowS
Show, Grlex -> Grlex -> Bool
(Grlex -> Grlex -> Bool) -> (Grlex -> Grlex -> Bool) -> Eq Grlex
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Grlex -> Grlex -> Bool
$c/= :: Grlex -> Grlex -> Bool
== :: Grlex -> Grlex -> Bool
$c== :: Grlex -> Grlex -> Bool
Eq, Eq Grlex
Eq Grlex
-> (Grlex -> Grlex -> Ordering)
-> (Grlex -> Grlex -> Bool)
-> (Grlex -> Grlex -> Bool)
-> (Grlex -> Grlex -> Bool)
-> (Grlex -> Grlex -> Bool)
-> (Grlex -> Grlex -> Grlex)
-> (Grlex -> Grlex -> Grlex)
-> Ord Grlex
Grlex -> Grlex -> Bool
Grlex -> Grlex -> Ordering
Grlex -> Grlex -> Grlex
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Grlex -> Grlex -> Grlex
$cmin :: Grlex -> Grlex -> Grlex
max :: Grlex -> Grlex -> Grlex
$cmax :: Grlex -> Grlex -> Grlex
>= :: Grlex -> Grlex -> Bool
$c>= :: Grlex -> Grlex -> Bool
> :: Grlex -> Grlex -> Bool
$c> :: Grlex -> Grlex -> Bool
<= :: Grlex -> Grlex -> Bool
$c<= :: Grlex -> Grlex -> Bool
< :: Grlex -> Grlex -> Bool
$c< :: Grlex -> Grlex -> Bool
compare :: Grlex -> Grlex -> Ordering
$ccompare :: Grlex -> Grlex -> Ordering
$cp1Ord :: Eq Grlex
Ord)

-- | Graded order from another monomial order.
newtype Graded ord = Graded ord
  deriving (ReadPrec [Graded ord]
ReadPrec (Graded ord)
Int -> ReadS (Graded ord)
ReadS [Graded ord]
(Int -> ReadS (Graded ord))
-> ReadS [Graded ord]
-> ReadPrec (Graded ord)
-> ReadPrec [Graded ord]
-> Read (Graded ord)
forall ord. Read ord => ReadPrec [Graded ord]
forall ord. Read ord => ReadPrec (Graded ord)
forall ord. Read ord => Int -> ReadS (Graded ord)
forall ord. Read ord => ReadS [Graded ord]
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
readListPrec :: ReadPrec [Graded ord]
$creadListPrec :: forall ord. Read ord => ReadPrec [Graded ord]
readPrec :: ReadPrec (Graded ord)
$creadPrec :: forall ord. Read ord => ReadPrec (Graded ord)
readList :: ReadS [Graded ord]
$creadList :: forall ord. Read ord => ReadS [Graded ord]
readsPrec :: Int -> ReadS (Graded ord)
$creadsPrec :: forall ord. Read ord => Int -> ReadS (Graded ord)
Read, Int -> Graded ord -> ShowS
[Graded ord] -> ShowS
Graded ord -> String
(Int -> Graded ord -> ShowS)
-> (Graded ord -> String)
-> ([Graded ord] -> ShowS)
-> Show (Graded ord)
forall ord. Show ord => Int -> Graded ord -> ShowS
forall ord. Show ord => [Graded ord] -> ShowS
forall ord. Show ord => Graded ord -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Graded ord] -> ShowS
$cshowList :: forall ord. Show ord => [Graded ord] -> ShowS
show :: Graded ord -> String
$cshow :: forall ord. Show ord => Graded ord -> String
showsPrec :: Int -> Graded ord -> ShowS
$cshowsPrec :: forall ord. Show ord => Int -> Graded ord -> ShowS
Show, Graded ord -> Graded ord -> Bool
(Graded ord -> Graded ord -> Bool)
-> (Graded ord -> Graded ord -> Bool) -> Eq (Graded ord)
forall ord. Eq ord => Graded ord -> Graded ord -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Graded ord -> Graded ord -> Bool
$c/= :: forall ord. Eq ord => Graded ord -> Graded ord -> Bool
== :: Graded ord -> Graded ord -> Bool
$c== :: forall ord. Eq ord => Graded ord -> Graded ord -> Bool
Eq, Eq (Graded ord)
Eq (Graded ord)
-> (Graded ord -> Graded ord -> Ordering)
-> (Graded ord -> Graded ord -> Bool)
-> (Graded ord -> Graded ord -> Bool)
-> (Graded ord -> Graded ord -> Bool)
-> (Graded ord -> Graded ord -> Bool)
-> (Graded ord -> Graded ord -> Graded ord)
-> (Graded ord -> Graded ord -> Graded ord)
-> Ord (Graded ord)
Graded ord -> Graded ord -> Bool
Graded ord -> Graded ord -> Ordering
Graded ord -> Graded ord -> Graded ord
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall ord. Ord ord => Eq (Graded ord)
forall ord. Ord ord => Graded ord -> Graded ord -> Bool
forall ord. Ord ord => Graded ord -> Graded ord -> Ordering
forall ord. Ord ord => Graded ord -> Graded ord -> Graded ord
min :: Graded ord -> Graded ord -> Graded ord
$cmin :: forall ord. Ord ord => Graded ord -> Graded ord -> Graded ord
max :: Graded ord -> Graded ord -> Graded ord
$cmax :: forall ord. Ord ord => Graded ord -> Graded ord -> Graded ord
>= :: Graded ord -> Graded ord -> Bool
$c>= :: forall ord. Ord ord => Graded ord -> Graded ord -> Bool
> :: Graded ord -> Graded ord -> Bool
$c> :: forall ord. Ord ord => Graded ord -> Graded ord -> Bool
<= :: Graded ord -> Graded ord -> Bool
$c<= :: forall ord. Ord ord => Graded ord -> Graded ord -> Bool
< :: Graded ord -> Graded ord -> Bool
$c< :: forall ord. Ord ord => Graded ord -> Graded ord -> Bool
compare :: Graded ord -> Graded ord -> Ordering
$ccompare :: forall ord. Ord ord => Graded ord -> Graded ord -> Ordering
$cp1Ord :: forall ord. Ord ord => Eq (Graded ord)
Ord)

instance IsOrder n ord => IsOrder n (Graded ord) where
  cmpMonomial :: Proxy (Graded ord) -> MonomialOrder n
cmpMonomial Proxy (Graded ord)
Proxy = MonomialOrder n -> MonomialOrder n
forall (n :: Nat). MonomialOrder n -> MonomialOrder n
graded (Proxy ord -> MonomialOrder n
forall (n :: Nat) ordering.
IsOrder n ordering =>
Proxy ordering -> MonomialOrder n
cmpMonomial (Proxy ord
forall k (t :: k). Proxy t
Proxy :: Proxy ord))
  {-# INLINE [1] cmpMonomial #-}

instance IsMonomialOrder n ord => IsMonomialOrder n (Graded ord)

data ProductOrder (n :: Nat) (m :: Nat) (a :: Type) (b :: Type) where
  ProductOrder :: SNat n -> SNat m -> ord -> ord' -> ProductOrder n m ord ord'

productOrder ::
  forall ord ord' n m.
  (IsOrder n ord, IsOrder m ord', KnownNat n, KnownNat m) =>
  Proxy (ProductOrder n m ord ord') ->
  MonomialOrder (n + m)
productOrder :: Proxy (ProductOrder n m ord ord') -> MonomialOrder (n + m)
productOrder Proxy (ProductOrder n m ord ord')
_ Monomial (n + m)
mon Monomial (n + m)
mon' =
  let n :: SNat n
n = SNat n
forall (n :: Nat). KnownNat n => SNat n
sNat :: SNat n
      m :: SNat m
m = SNat m
forall (n :: Nat). KnownNat n => SNat n
sNat :: SNat m
   in IsTrue (n <=? (n + m))
-> (((n <=? (n + m)) ~ 'True) => Ordering) -> Ordering
forall (b :: Bool) r. IsTrue b -> ((b ~ 'True) => r) -> r
withWitness (SNat n -> SNat m -> IsTrue (n <=? (n + m))
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> IsTrue (n <=? (n + m))
plusLeqL SNat n
n SNat m
m) ((((n <=? (n + m)) ~ 'True) => Ordering) -> Ordering)
-> (((n <=? (n + m)) ~ 'True) => Ordering) -> Ordering
forall a b. (a -> b) -> a -> b
$
        case (SNat n
-> Monomial (n + m)
-> (Sized Vector n Int, Sized Vector ((n + m) -. n) Int)
forall (n :: Nat) (f :: * -> *) (m :: Nat) a.
(CFreeMonoid f, Dom f a, n <= m) =>
SNat n -> Sized f m a -> (Sized f n a, Sized f (m -. n) a)
V.splitAt SNat n
n Monomial (n + m)
mon, SNat n
-> Monomial (n + m)
-> (Sized Vector n Int, Sized Vector ((n + m) -. n) Int)
forall (n :: Nat) (f :: * -> *) (m :: Nat) a.
(CFreeMonoid f, Dom f a, n <= m) =>
SNat n -> Sized f m a -> (Sized f n a, Sized f (m -. n) a)
V.splitAt SNat n
n Monomial (n + m)
mon') of
          ((Sized Vector n Int
xs, Sized Vector ((n + m) - n) Int
xs'), (Sized Vector n Int
ys, Sized Vector ((n + m) - n) Int
ys')) ->
            Proxy ord -> MonomialOrder n
forall (n :: Nat) ordering.
IsOrder n ordering =>
Proxy ordering -> MonomialOrder n
cmpMonomial (Proxy ord
forall k (t :: k). Proxy t
Proxy :: Proxy ord) Sized Vector n Int
xs Sized Vector n Int
ys
              Ordering -> Ordering -> Ordering
forall a. Semigroup a => a -> a -> a
<> Proxy ord' -> MonomialOrder ((n + m) - n)
forall (n :: Nat) ordering.
IsOrder n ordering =>
Proxy ordering -> MonomialOrder n
cmpMonomial
                (Proxy ord'
forall k (t :: k). Proxy t
Proxy :: Proxy ord')
                Sized Vector ((n + m) - n) Int
xs'
                Sized Vector ((n + m) - n) Int
ys'

productOrder' ::
  forall n ord ord' m.
  (IsOrder n ord, IsOrder m ord') =>
  SNat n ->
  SNat m ->
  ord ->
  ord' ->
  MonomialOrder (n + m)
productOrder' :: SNat n -> SNat m -> ord -> ord' -> MonomialOrder (n + m)
productOrder' SNat n
n SNat m
m ord
_ ord'
_ =
  SNat n
-> (KnownNat n => MonomialOrder (n + m)) -> MonomialOrder (n + m)
forall (n :: Nat) r. SNat n -> (KnownNat n => r) -> r
withKnownNat SNat n
n ((KnownNat n => MonomialOrder (n + m)) -> MonomialOrder (n + m))
-> (KnownNat n => MonomialOrder (n + m)) -> MonomialOrder (n + m)
forall a b. (a -> b) -> a -> b
$
    SNat m
-> (KnownNat m => MonomialOrder (n + m)) -> MonomialOrder (n + m)
forall (n :: Nat) r. SNat n -> (KnownNat n => r) -> r
withKnownNat SNat m
m ((KnownNat m => MonomialOrder (n + m)) -> MonomialOrder (n + m))
-> (KnownNat m => MonomialOrder (n + m)) -> MonomialOrder (n + m)
forall a b. (a -> b) -> a -> b
$
      Proxy (ProductOrder n m ord ord') -> MonomialOrder (n + m)
forall ord ord' (n :: Nat) (m :: Nat).
(IsOrder n ord, IsOrder m ord', KnownNat n, KnownNat m) =>
Proxy (ProductOrder n m ord ord') -> MonomialOrder (n + m)
productOrder (Proxy (ProductOrder n m ord ord')
forall k (t :: k). Proxy t
Proxy :: Proxy (ProductOrder n m ord ord'))

type WeightProxy (v :: [Nat]) = SList v

data WeightOrder (v :: [Nat]) (ord :: Type) where
  WeightOrder :: SList (v :: [Nat]) -> Proxy ord -> WeightOrder v ord

calcOrderWeight ::
  forall vs n.
  (SingI vs, KnownNat n) =>
  Proxy (vs :: [Nat]) ->
  Monomial n ->
  Int
calcOrderWeight :: Proxy vs -> Monomial n -> Int
calcOrderWeight Proxy vs
Proxy = SList vs -> Monomial n -> Int
forall (vs :: [Nat]) (n :: Nat).
KnownNat n =>
SList vs -> Monomial n -> Int
calcOrderWeight' (SList vs
forall k (a :: k). SingI a => Sing a
sing :: SList vs)
{-# INLINE calcOrderWeight #-}

calcOrderWeight' :: forall vs n. KnownNat n => SList (vs :: [Nat]) -> Monomial n -> Int
calcOrderWeight' :: SList vs -> Monomial n -> Int
calcOrderWeight' SList vs
slst Monomial n
m =
  let cfs :: Monomial n
cfs = Int -> [Int] -> Monomial n
forall (f :: * -> *) (n :: Nat) a.
(KnownNat n, CFreeMonoid f, Dom f a) =>
a -> [a] -> Sized f n a
V.fromListWithDefault' (Int
0 :: Int) ([Int] -> Monomial n) -> [Int] -> Monomial n
forall a b. (a -> b) -> a -> b
$ (Natural -> Int) -> [Natural] -> [Int]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
map Natural -> Int
forall a b. (Integral a, Num b) => a -> b
P.fromIntegral ([Natural] -> [Int]) -> [Natural] -> [Int]
forall a b. (a -> b) -> a -> b
$ Sing vs -> Demote [Nat]
forall k (a :: k). SingKind k => Sing a -> Demote k
fromSing Sing vs
SList vs
slst
   in Monomial n -> Element (Monomial n)
forall mono.
(MonoFoldable mono, Num (Element mono)) =>
mono -> Element mono
osum (Monomial n -> Element (Monomial n))
-> Monomial n -> Element (Monomial n)
forall a b. (a -> b) -> a -> b
$ (Int -> Int -> Int) -> Monomial n -> Monomial n -> Monomial n
forall (n :: Nat) a.
(KnownNat n, Unbox a) =>
(Int -> Int -> a) -> USized n Int -> USized n Int -> USized n a
zws Int -> Int -> Int
forall r. Multiplicative r => r -> r -> r
(*) Monomial n
cfs Monomial n
m
{-# INLINE [2] calcOrderWeight' #-}

weightOrder ::
  forall n ns ord.
  (KnownNat n, IsOrder n ord, SingI ns) =>
  Proxy (WeightOrder ns ord) ->
  MonomialOrder n
weightOrder :: Proxy (WeightOrder ns ord) -> MonomialOrder n
weightOrder Proxy (WeightOrder ns ord)
Proxy Monomial n
m Monomial n
m' =
  (Monomial n -> Int) -> MonomialOrder n
forall a b. Ord a => (b -> a) -> b -> b -> Ordering
comparing (Proxy ns -> Monomial n -> Int
forall (vs :: [Nat]) (n :: Nat).
(SingI vs, KnownNat n) =>
Proxy vs -> Monomial n -> Int
calcOrderWeight (Proxy ns
forall k (t :: k). Proxy t
Proxy :: Proxy ns)) Monomial n
m Monomial n
m'
    Ordering -> Ordering -> Ordering
forall a. Semigroup a => a -> a -> a
<> Proxy ord -> MonomialOrder n
forall (n :: Nat) ordering.
IsOrder n ordering =>
Proxy ordering -> MonomialOrder n
cmpMonomial (Proxy ord
forall k (t :: k). Proxy t
Proxy :: Proxy ord) Monomial n
m Monomial n
m'
{-# INLINE weightOrder #-}

instance
  (KnownNat n, IsOrder n ord, SingI ws) =>
  IsOrder n (WeightOrder ws ord)
  where
  cmpMonomial :: Proxy (WeightOrder ws ord) -> MonomialOrder n
cmpMonomial = Proxy (WeightOrder ws ord) -> MonomialOrder n
forall (n :: Nat) (ns :: [Nat]) ord.
(KnownNat n, IsOrder n ord, SingI ns) =>
Proxy (WeightOrder ns ord) -> MonomialOrder n
weightOrder
  {-# INLINE [1] cmpMonomial #-}

instance
  (IsOrder n ord, IsOrder m ord', KnownNat m, KnownNat n, k ~ (n + m)) =>
  IsOrder k (ProductOrder n m ord ord')
  where
  cmpMonomial :: Proxy (ProductOrder n m ord ord') -> MonomialOrder k
cmpMonomial = Proxy (ProductOrder n m ord ord') -> MonomialOrder k
forall ord ord' (n :: Nat) (m :: Nat).
(IsOrder n ord, IsOrder m ord', KnownNat n, KnownNat m) =>
Proxy (ProductOrder n m ord ord') -> MonomialOrder (n + m)
productOrder
  {-# INLINE [1] cmpMonomial #-}

-- They're all total orderings.
instance KnownNat n => IsOrder n Grevlex where
  cmpMonomial :: Proxy Grevlex -> MonomialOrder n
cmpMonomial Proxy Grevlex
_ = MonomialOrder n
forall (n :: Nat). MonomialOrder n
grevlex
  {-# INLINE [1] cmpMonomial #-}

instance KnownNat n => IsOrder n Revlex where
  cmpMonomial :: Proxy Revlex -> MonomialOrder n
cmpMonomial Proxy Revlex
_ = MonomialOrder n
forall (n :: Nat). KnownNat n => MonomialOrder n
revlex
  {-# INLINE [1] cmpMonomial #-}

instance KnownNat n => IsOrder n Lex where
  cmpMonomial :: Proxy Lex -> MonomialOrder n
cmpMonomial Proxy Lex
_ = MonomialOrder n
forall (n :: Nat). KnownNat n => MonomialOrder n
lex
  {-# INLINE [1] cmpMonomial #-}

instance KnownNat n => IsOrder n Grlex where
  cmpMonomial :: Proxy Grlex -> MonomialOrder n
cmpMonomial Proxy Grlex
_ = MonomialOrder n
forall (n :: Nat). KnownNat n => MonomialOrder n
grlex
  {-# INLINE [1] cmpMonomial #-}

-- | Class for Monomial' orders.
class IsOrder n name => IsMonomialOrder n name

-- Note that Revlex is not a monomial order.
-- This distinction is important when we calculate a quotient or Groebner basis.
instance KnownNat n => IsMonomialOrder n Grlex

instance KnownNat n => IsMonomialOrder n Grevlex

instance KnownNat n => IsMonomialOrder n Lex

instance
  (KnownNat n, KnownNat m, IsMonomialOrder n o, IsMonomialOrder m o', k ~ (n + m)) =>
  IsMonomialOrder k (ProductOrder n m o o')

instance
  (KnownNat k, SingI ws, IsMonomialOrder k ord) =>
  IsMonomialOrder k (WeightOrder ws ord)

lcmMonomial :: KnownNat n => OrderedMonomial ord n -> OrderedMonomial ord n -> OrderedMonomial ord n
lcmMonomial :: OrderedMonomial ord n
-> OrderedMonomial ord n -> OrderedMonomial ord n
lcmMonomial (OrderedMonomial Monomial n
m) (OrderedMonomial Monomial n
n) = Monomial n -> OrderedMonomial ord n
forall k (ordering :: k) (n :: Nat).
Monomial n -> OrderedMonomial ordering n
OrderedMonomial (Monomial n -> OrderedMonomial ord n)
-> Monomial n -> OrderedMonomial ord n
forall a b. (a -> b) -> a -> b
$ (Int -> Int -> Int) -> Monomial n -> Monomial n -> Monomial n
forall (n :: Nat) a.
(KnownNat n, Unbox a) =>
(Int -> Int -> a) -> USized n Int -> USized n Int -> USized n a
zws Int -> Int -> Int
forall a. Ord a => a -> a -> a
max Monomial n
m Monomial n
n
{-# INLINE lcmMonomial #-}

gcdMonomial :: KnownNat n => OrderedMonomial ord n -> OrderedMonomial ord n -> OrderedMonomial ord n
gcdMonomial :: OrderedMonomial ord n
-> OrderedMonomial ord n -> OrderedMonomial ord n
gcdMonomial (OrderedMonomial Monomial n
m) (OrderedMonomial Monomial n
n) = Monomial n -> OrderedMonomial ord n
forall k (ordering :: k) (n :: Nat).
Monomial n -> OrderedMonomial ordering n
OrderedMonomial (Monomial n -> OrderedMonomial ord n)
-> Monomial n -> OrderedMonomial ord n
forall a b. (a -> b) -> a -> b
$ (Int -> Int -> Int) -> Monomial n -> Monomial n -> Monomial n
forall (n :: Nat) a.
(KnownNat n, Unbox a) =>
(Int -> Int -> a) -> USized n Int -> USized n Int -> USized n a
zws Int -> Int -> Int
forall a. Ord a => a -> a -> a
P.min Monomial n
m Monomial n
n
{-# INLINE gcdMonomial #-}

divs :: KnownNat n => OrderedMonomial ord n -> OrderedMonomial ord n -> Bool
(OrderedMonomial Monomial n
xs) divs :: OrderedMonomial ord n -> OrderedMonomial ord n -> Bool
`divs` (OrderedMonomial Monomial n
ys) = USized n Bool -> Bool
forall mono.
(Element mono ~ Bool, MonoFoldable mono) =>
mono -> Bool
oand (USized n Bool -> Bool) -> USized n Bool -> Bool
forall a b. (a -> b) -> a -> b
$ (Int -> Int -> Bool) -> Monomial n -> Monomial n -> USized n Bool
forall (n :: Nat) a.
(KnownNat n, Unbox a) =>
(Int -> Int -> a) -> USized n Int -> USized n Int -> USized n a
zws Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
(<=) Monomial n
xs Monomial n
ys

isPowerOf :: KnownNat n => OrderedMonomial ord n -> OrderedMonomial ord n -> Bool
OrderedMonomial Monomial n
n isPowerOf :: OrderedMonomial ord n -> OrderedMonomial ord n -> Bool
`isPowerOf` OrderedMonomial Monomial n
m =
  case (Int -> Bool) -> Monomial n -> [Ordinal n]
forall (f :: * -> *) (n :: Nat) a.
(CFoldable f, Dom f a, KnownNat n) =>
(a -> Bool) -> Sized f n a -> [Ordinal n]
V.sFindIndices (Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
0) Monomial n
m of
    [Ordinal n
ind] -> Monomial n -> Element (Monomial n)
forall mono.
(MonoFoldable mono, Num (Element mono)) =>
mono -> Element mono
osum Monomial n
n Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Ordinal n -> Monomial n -> Int
forall (f :: * -> *) (n :: Nat) c.
(CFoldable f, Dom f c) =>
Ordinal n -> Sized f n c -> c
V.sIndex Ordinal n
ind Monomial n
n
    [Ordinal n]
_ -> Bool
False

tryDiv :: (KnownNat n, Field r) => (r, OrderedMonomial ord n) -> (r, OrderedMonomial ord n) -> (r, OrderedMonomial ord n)
tryDiv :: (r, OrderedMonomial ord n)
-> (r, OrderedMonomial ord n) -> (r, OrderedMonomial ord n)
tryDiv (r
a, OrderedMonomial ord n
f) (r
b, OrderedMonomial ord n
g)
  | OrderedMonomial ord n
g OrderedMonomial ord n -> OrderedMonomial ord n -> Bool
forall k (n :: Nat) (ord :: k).
KnownNat n =>
OrderedMonomial ord n -> OrderedMonomial ord n -> Bool
`divs` OrderedMonomial ord n
f = (r
a r -> r -> r
forall r. Multiplicative r => r -> r -> r
* r -> r
forall r. Division r => r -> r
recip r
b, Monomial n -> OrderedMonomial ord n
forall k (ordering :: k) (n :: Nat).
Monomial n -> OrderedMonomial ordering n
OrderedMonomial (Monomial n -> OrderedMonomial ord n)
-> Monomial n -> OrderedMonomial ord n
forall a b. (a -> b) -> a -> b
$ (Int -> Int -> Int) -> Monomial n -> Monomial n -> Monomial n
forall (n :: Nat) a.
(KnownNat n, Unbox a) =>
(Int -> Int -> a) -> USized n Int -> USized n Int -> USized n a
zws (-) (OrderedMonomial ord n -> Monomial n
forall k (ordering :: k) (n :: Nat).
OrderedMonomial ordering n -> Monomial n
getMonomial OrderedMonomial ord n
f) (OrderedMonomial ord n -> Monomial n
forall k (ordering :: k) (n :: Nat).
OrderedMonomial ordering n -> Monomial n
getMonomial OrderedMonomial ord n
g))
  | Bool
otherwise = String -> (r, OrderedMonomial ord n)
forall a. HasCallStack => String -> a
error String
"cannot divide."

varMonom :: SNat n -> Ordinal n -> Monomial n
varMonom :: SNat n -> Ordinal n -> Monomial n
varMonom SNat n
len Ordinal n
o = SNat n -> Int -> Monomial n
forall (f :: * -> *) (n :: Nat) a.
(CFreeMonoid f, Dom f a) =>
SNat n -> a -> Sized f n a
V.replicate SNat n
len Int
0 Monomial n -> (Monomial n -> Monomial n) -> Monomial n
forall a b. a -> (a -> b) -> b
& Index (Monomial n)
-> Traversal' (Monomial n) (IxValue (Monomial n))
forall m. Ixed m => Index m -> Traversal' m (IxValue m)
ix Index (Monomial n)
Ordinal n
o ((Int -> Identity Int) -> Monomial n -> Identity (Monomial n))
-> Int -> Monomial n -> Monomial n
forall s t a b. ASetter s t a b -> b -> s -> t
.~ Int
1
{-# INLINE varMonom #-}

{- | Monomial' order which can be use to calculate n-th elimination ideal of m-ary polynomial.
 This should judge monomial to be bigger if it contains variables to eliminate.
-}
class (IsMonomialOrder n ord, KnownNat n) => EliminationType n m ord

instance KnownNat n => EliminationType n m Lex

instance
  (KnownNat n, KnownNat m, IsMonomialOrder n ord, IsMonomialOrder m ord', k ~ (n + m), KnownNat k) =>
  EliminationType k n (ProductOrder n m ord ord')

instance
  ( IsMonomialOrder k ord
  , ones ~ Replicate n 1
  , SingI ones
  , (Length ones <= k)
  , KnownNat k
  ) =>
  EliminationType k n (WeightOrder ones ord)

type EliminationOrder n m = ProductOrder n m Grevlex Grevlex

eliminationOrder :: SNat n -> SNat m -> EliminationOrder n m
eliminationOrder :: SNat n -> SNat m -> EliminationOrder n m
eliminationOrder SNat n
n SNat m
m =
  SNat n
-> (KnownNat n => EliminationOrder n m) -> EliminationOrder n m
forall (n :: Nat) r. SNat n -> (KnownNat n => r) -> r
withKnownNat SNat n
n ((KnownNat n => EliminationOrder n m) -> EliminationOrder n m)
-> (KnownNat n => EliminationOrder n m) -> EliminationOrder n m
forall a b. (a -> b) -> a -> b
$ SNat n -> SNat m -> Grevlex -> Grevlex -> EliminationOrder n m
forall (n :: Nat) (m :: Nat) ord ord'.
SNat n -> SNat m -> ord -> ord' -> ProductOrder n m ord ord'
ProductOrder SNat n
n SNat m
m Grevlex
Grevlex Grevlex
Grevlex

sOnes :: SNat n -> SList (Replicate n 1)
sOnes :: SNat n -> SList (Replicate n 1)
sOnes SNat n
n = Sing n -> Sing 1 -> Sing (Apply (Apply ReplicateSym0 n) 1)
forall a (t1 :: Nat) (t2 :: a).
Sing t1 -> Sing t2 -> Sing (Apply (Apply ReplicateSym0 t1) t2)
sReplicate (SNat n -> Sing n
forall (n :: Nat). SNat n -> Sing n
sNatToSingleton SNat n
n) Sing 1
forall k (a :: k). SingI a => Sing a
sing

weightedEliminationOrder :: SNat n -> WeightedEliminationOrder n Grevlex
weightedEliminationOrder :: SNat n -> WeightedEliminationOrder n Grevlex
weightedEliminationOrder SNat n
n =
  SList (Case_6989586621680379320 n 1 (DefaultEq n 0))
-> Proxy Grevlex
-> WeightOrder
     (Case_6989586621680379320 n 1 (DefaultEq n 0)) Grevlex
forall (v :: [Nat]) ord. SList v -> Proxy ord -> WeightOrder v ord
WeightOrder (SNat n -> SList (Replicate n 1)
forall (n :: Nat). SNat n -> SList (Replicate n 1)
sOnes SNat n
n) (Proxy Grevlex
forall k (t :: k). Proxy t
Proxy :: Proxy Grevlex)

type WeightedEliminationOrder (n :: Nat) (ord :: Type) =
  WeightOrder (Replicate n 1) ord

-- | Special ordering for ordered-monomials.
instance (Eq (Monomial n), IsOrder n name) => Ord (OrderedMonomial name n) where
  OrderedMonomial Monomial n
m compare :: OrderedMonomial name n -> OrderedMonomial name n -> Ordering
`compare` OrderedMonomial Monomial n
n = Proxy name -> MonomialOrder n
forall (n :: Nat) ordering.
IsOrder n ordering =>
Proxy ordering -> MonomialOrder n
cmpMonomial (Proxy name
forall k (t :: k). Proxy t
Proxy :: Proxy name) Monomial n
m Monomial n
n

castMonomial :: (KnownNat m) => OrderedMonomial o n -> OrderedMonomial o' m
castMonomial :: OrderedMonomial o n -> OrderedMonomial o' m
castMonomial = (Monomial n -> Identity (Monomial m))
-> OrderedMonomial o n -> Identity (OrderedMonomial o' m)
forall s t. Rewrapping s t => Iso s t (Unwrapped s) (Unwrapped t)
_Wrapped ((Monomial n -> Identity (Monomial m))
 -> OrderedMonomial o n -> Identity (OrderedMonomial o' m))
-> (Monomial n -> Monomial m)
-> OrderedMonomial o n
-> OrderedMonomial o' m
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ SNat m -> [Int] -> Monomial m
forall (n :: Nat). SNat n -> [Int] -> Monomial n
fromList SNat m
forall (n :: Nat). KnownNat n => SNat n
sNat ([Int] -> Monomial m)
-> (Monomial n -> [Int]) -> Monomial n -> Monomial m
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Monomial n -> [Int]
forall mono. MonoFoldable mono => mono -> [Element mono]
otoList

scastMonomial :: SNat m -> OrderedMonomial o n -> OrderedMonomial o m
scastMonomial :: SNat m -> OrderedMonomial o n -> OrderedMonomial o m
scastMonomial SNat m
sdim = (Monomial n -> Identity (Monomial m))
-> OrderedMonomial o n -> Identity (OrderedMonomial o m)
forall s t. Rewrapping s t => Iso s t (Unwrapped s) (Unwrapped t)
_Wrapped ((Monomial n -> Identity (Monomial m))
 -> OrderedMonomial o n -> Identity (OrderedMonomial o m))
-> (Monomial n -> Monomial m)
-> OrderedMonomial o n
-> OrderedMonomial o m
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ SNat m -> [Int] -> Monomial m
forall (n :: Nat). SNat n -> [Int] -> Monomial n
fromList SNat m
sdim ([Int] -> Monomial m)
-> (Monomial n -> [Int]) -> Monomial n -> Monomial m
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Monomial n -> [Int]
forall mono. MonoFoldable mono => mono -> [Element mono]
otoList

changeMonomialOrder :: o' -> OrderedMonomial ord n -> OrderedMonomial o' n
changeMonomialOrder :: o' -> OrderedMonomial ord n -> OrderedMonomial o' n
changeMonomialOrder o'
_ = OrderedMonomial ord n -> OrderedMonomial o' n
DC.coerce

changeMonomialOrderProxy :: Proxy o' -> OrderedMonomial ord n -> OrderedMonomial o' n
changeMonomialOrderProxy :: Proxy o' -> OrderedMonomial ord n -> OrderedMonomial o' n
changeMonomialOrderProxy Proxy o'
_ = OrderedMonomial ord n -> OrderedMonomial o' n
DC.coerce

class (IsMonomialOrder n ord) => IsMonomialOrder' ord n

instance (IsMonomialOrder n ord) => IsMonomialOrder' ord n

instance IsMonomialOrder' ord n :=> IsMonomialOrder n ord where
  ins :: IsMonomialOrder' ord n :- IsMonomialOrder n ord
ins = (IsMonomialOrder' ord n => Dict (IsMonomialOrder n ord))
-> IsMonomialOrder' ord n :- IsMonomialOrder n ord
forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
C.Sub IsMonomialOrder' ord n => Dict (IsMonomialOrder n ord)
forall (a :: Constraint). a => Dict a
Dict

-- | Monomial' ordering which can do with monomials of arbitrary large arity.
type IsStrongMonomialOrder ord = Forall (IsMonomialOrder' ord)

withStrongMonomialOrder ::
  forall ord n r proxy (proxy' :: Nat -> Type).
  (IsStrongMonomialOrder ord) =>
  proxy ord ->
  proxy' n ->
  (IsMonomialOrder n ord => r) ->
  r
withStrongMonomialOrder :: proxy ord -> proxy' n -> (IsMonomialOrder n ord => r) -> r
withStrongMonomialOrder proxy ord
_ proxy' n
_ IsMonomialOrder n ord => r
r = IsMonomialOrder n ord => r
r (IsMonomialOrder n ord => r)
-> (Forall_ (IsMonomialOrder' ord) :- IsMonomialOrder n ord) -> r
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
C.\\ Forall_ (IsMonomialOrder' ord) :- IsMonomialOrder n ord
dict
  where
    ismToPrim :: IsMonomialOrder' ord n :- IsMonomialOrder n ord
ismToPrim = IsMonomialOrder' ord n :- IsMonomialOrder n ord
forall (b :: Constraint) (h :: Constraint). (b :=> h) => b :- h
ins :: IsMonomialOrder' ord n C.:- IsMonomialOrder n ord
    primeInst :: Forall (IsMonomialOrder' ord) :- IsMonomialOrder' ord n
primeInst = Forall (IsMonomialOrder' ord) :- IsMonomialOrder' ord n
forall k (p :: k -> Constraint) (a :: k). Forall p :- p a
inst :: Forall (IsMonomialOrder' ord) C.:- IsMonomialOrder' ord n
    dict :: Forall_ (IsMonomialOrder' ord) :- IsMonomialOrder n ord
dict = IsMonomialOrder' ord n :- IsMonomialOrder n ord
ismToPrim (IsMonomialOrder' ord n :- IsMonomialOrder n ord)
-> (Forall_ (IsMonomialOrder' ord) :- IsMonomialOrder' ord n)
-> Forall_ (IsMonomialOrder' ord) :- IsMonomialOrder n ord
forall (b :: Constraint) (c :: Constraint) (a :: Constraint).
(b :- c) -> (a :- b) -> a :- c
`C.trans` Forall (IsMonomialOrder' ord) :- IsMonomialOrder' ord n
Forall_ (IsMonomialOrder' ord) :- IsMonomialOrder' ord n
primeInst

{- | Comparing monomials with different arity,
   padding with @0@ at bottom of the shorter monomial to
   make the length equal.
-}
cmpAnyMonomial ::
  (IsStrongMonomialOrder ord, KnownNat n, KnownNat m) =>
  Proxy ord ->
  Monomial n ->
  Monomial m ->
  Ordering
cmpAnyMonomial :: Proxy ord -> Monomial n -> Monomial m -> Ordering
cmpAnyMonomial Proxy ord
pxy Monomial n
t Monomial m
t' =
  let (SNat (MaxAux (m <=? n) n m)
l, USized (MaxAux (m <=? n) n m) Int
u, USized (MaxAux (m <=? n) n m) Int
u') = Int
-> Monomial n
-> Monomial m
-> (SNat (MaxAux (m <=? n) n m), USized (MaxAux (m <=? n) n m) Int,
    USized (MaxAux (m <=? n) n m) Int)
forall a (n :: Nat) (m :: Nat).
(Unbox a, KnownNat n, KnownNat m) =>
a
-> USized n a
-> USized m a
-> (SNat (Max n m), USized (Max n m) a, USized (Max n m) a)
padVecs Int
0 Monomial n
t Monomial m
t'
   in Proxy ord
-> SNat (MaxAux (m <=? n) n m)
-> (IsMonomialOrder (MaxAux (m <=? n) n m) ord => Ordering)
-> Ordering
forall ord (n :: Nat) r (proxy :: * -> *) (proxy' :: Nat -> *).
IsStrongMonomialOrder ord =>
proxy ord -> proxy' n -> (IsMonomialOrder n ord => r) -> r
withStrongMonomialOrder Proxy ord
pxy SNat (MaxAux (m <=? n) n m)
l ((IsMonomialOrder (MaxAux (m <=? n) n m) ord => Ordering)
 -> Ordering)
-> (IsMonomialOrder (MaxAux (m <=? n) n m) ord => Ordering)
-> Ordering
forall a b. (a -> b) -> a -> b
$ Proxy ord -> MonomialOrder (MaxAux (m <=? n) n m)
forall (n :: Nat) ordering.
IsOrder n ordering =>
Proxy ordering -> MonomialOrder n
cmpMonomial Proxy ord
pxy USized (MaxAux (m <=? n) n m) Int
u USized (MaxAux (m <=? n) n m) Int
u'

orderMonomial :: proxy ord -> Monomial n -> OrderedMonomial ord n
orderMonomial :: proxy ord -> Monomial n -> OrderedMonomial ord n
orderMonomial proxy ord
_ = Monomial n -> OrderedMonomial ord n
forall k (ordering :: k) (n :: Nat).
Monomial n -> OrderedMonomial ordering n
OrderedMonomial
{-# INLINE orderMonomial #-}

ifoldMapMonom :: (KnownNat n, Monoid m) => (Ordinal n -> Int -> m) -> Monomial n -> m
ifoldMapMonom :: (Ordinal n -> Int -> m) -> Monomial n -> m
ifoldMapMonom Ordinal n -> Int -> m
f =
  (Int -> Int -> m -> m) -> m -> Vector Int -> m
forall a b. Unbox a => (Int -> a -> b -> b) -> b -> Vector a -> b
UV.ifoldr (\Int
i -> m -> m -> m
forall w. Monoid w => w -> w -> w
mappend (m -> m -> m) -> (Int -> m) -> Int -> m -> m
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Ordinal n -> Int -> m
f (Natural -> Ordinal n
forall (n :: Nat). KnownNat n => Natural -> Ordinal n
unsafeNaturalToOrd (Natural -> Ordinal n) -> Natural -> Ordinal n
forall a b. (a -> b) -> a -> b
$ Int -> Natural
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
i)) m
forall a. Monoid a => a
mempty (Vector Int -> m) -> (Monomial n -> Vector Int) -> Monomial n -> m
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Monomial n -> Vector Int
forall (f :: * -> *) (n :: Nat) a. Sized f n a -> f a
V.unsized