{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE NoImplicitPrelude #-}

module Algebra.Algorithms.Groebner.SelectionStrategy
  ( SelectionStrategy (..),
    calcWeight',
    GrevlexStrategy (..),
    NormalStrategy (..),
    SugarStrategy (..),
    GradedStrategy (..),
  )
where

import Algebra.Internal
import Algebra.Prelude.Core
import qualified Data.Foldable as F
import Data.Kind (Type)

{- | Calculate the weight of given polynomials w.r.t. the given strategy.
   Buchberger's algorithm proccesses the pair with the most least weight first.
   This function requires the @Ord@ instance for the weight; this constraint is not required
   in the 'calcWeight' because of the ease of implementation. So use this function.
-}
calcWeight' ::
  (SelectionStrategy (Arity poly) s, IsOrderedPolynomial poly) =>
  s ->
  poly ->
  poly ->
  Weight (Arity poly) s (MOrder poly)
calcWeight' :: s -> poly -> poly -> Weight (Arity poly) s (MOrder poly)
calcWeight' s
s = Proxy s -> poly -> poly -> Weight (Arity poly) s (MOrder poly)
forall k (n :: Nat) (s :: k) poly.
(SelectionStrategy n s, IsOrderedPolynomial poly,
 n ~ Arity poly) =>
Proxy s -> poly -> poly -> Weight n s (MOrder poly)
calcWeight (s -> Proxy s
forall a. a -> Proxy a
toProxy s
s)
{-# INLINE calcWeight' #-}

-- | Type-class for selection strategies in Buchberger's algorithm.
class SelectionStrategy n s where
  type Weight n s ord :: Type

  -- | Calculates the weight for the given pair of polynomial used for selection strategy.
  calcWeight ::
    (IsOrderedPolynomial poly, n ~ Arity poly) =>
    Proxy s ->
    poly ->
    poly ->
    Weight n s (MOrder poly)

{- | Buchberger's normal selection strategy. This selects the pair with
   the least LCM(LT(f), LT(g)) w.r.t. current monomial ordering.
-}
data NormalStrategy = NormalStrategy deriving (ReadPrec [NormalStrategy]
ReadPrec NormalStrategy
Int -> ReadS NormalStrategy
ReadS [NormalStrategy]
(Int -> ReadS NormalStrategy)
-> ReadS [NormalStrategy]
-> ReadPrec NormalStrategy
-> ReadPrec [NormalStrategy]
-> Read NormalStrategy
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
readListPrec :: ReadPrec [NormalStrategy]
$creadListPrec :: ReadPrec [NormalStrategy]
readPrec :: ReadPrec NormalStrategy
$creadPrec :: ReadPrec NormalStrategy
readList :: ReadS [NormalStrategy]
$creadList :: ReadS [NormalStrategy]
readsPrec :: Int -> ReadS NormalStrategy
$creadsPrec :: Int -> ReadS NormalStrategy
Read, Int -> NormalStrategy -> ShowS
[NormalStrategy] -> ShowS
NormalStrategy -> String
(Int -> NormalStrategy -> ShowS)
-> (NormalStrategy -> String)
-> ([NormalStrategy] -> ShowS)
-> Show NormalStrategy
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [NormalStrategy] -> ShowS
$cshowList :: [NormalStrategy] -> ShowS
show :: NormalStrategy -> String
$cshow :: NormalStrategy -> String
showsPrec :: Int -> NormalStrategy -> ShowS
$cshowsPrec :: Int -> NormalStrategy -> ShowS
Show, NormalStrategy -> NormalStrategy -> Bool
(NormalStrategy -> NormalStrategy -> Bool)
-> (NormalStrategy -> NormalStrategy -> Bool) -> Eq NormalStrategy
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: NormalStrategy -> NormalStrategy -> Bool
$c/= :: NormalStrategy -> NormalStrategy -> Bool
== :: NormalStrategy -> NormalStrategy -> Bool
$c== :: NormalStrategy -> NormalStrategy -> Bool
Eq, Eq NormalStrategy
Eq NormalStrategy
-> (NormalStrategy -> NormalStrategy -> Ordering)
-> (NormalStrategy -> NormalStrategy -> Bool)
-> (NormalStrategy -> NormalStrategy -> Bool)
-> (NormalStrategy -> NormalStrategy -> Bool)
-> (NormalStrategy -> NormalStrategy -> Bool)
-> (NormalStrategy -> NormalStrategy -> NormalStrategy)
-> (NormalStrategy -> NormalStrategy -> NormalStrategy)
-> Ord NormalStrategy
NormalStrategy -> NormalStrategy -> Bool
NormalStrategy -> NormalStrategy -> Ordering
NormalStrategy -> NormalStrategy -> NormalStrategy
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 :: NormalStrategy -> NormalStrategy -> NormalStrategy
$cmin :: NormalStrategy -> NormalStrategy -> NormalStrategy
max :: NormalStrategy -> NormalStrategy -> NormalStrategy
$cmax :: NormalStrategy -> NormalStrategy -> NormalStrategy
>= :: NormalStrategy -> NormalStrategy -> Bool
$c>= :: NormalStrategy -> NormalStrategy -> Bool
> :: NormalStrategy -> NormalStrategy -> Bool
$c> :: NormalStrategy -> NormalStrategy -> Bool
<= :: NormalStrategy -> NormalStrategy -> Bool
$c<= :: NormalStrategy -> NormalStrategy -> Bool
< :: NormalStrategy -> NormalStrategy -> Bool
$c< :: NormalStrategy -> NormalStrategy -> Bool
compare :: NormalStrategy -> NormalStrategy -> Ordering
$ccompare :: NormalStrategy -> NormalStrategy -> Ordering
$cp1Ord :: Eq NormalStrategy
Ord)

instance SelectionStrategy n NormalStrategy where
  type Weight n NormalStrategy ord = OrderedMonomial ord n
  calcWeight :: Proxy NormalStrategy
-> poly -> poly -> Weight n NormalStrategy (MOrder poly)
calcWeight Proxy NormalStrategy
_ poly
f poly
g = OrderedMonomial (MOrder poly) n
-> OrderedMonomial (MOrder poly) n
-> OrderedMonomial (MOrder poly) n
forall k (n :: Nat) (ord :: k).
KnownNat n =>
OrderedMonomial ord n
-> OrderedMonomial ord n -> OrderedMonomial ord n
lcmMonomial (poly -> OrderedMonomial (MOrder poly) (Arity poly)
forall poly.
IsOrderedPolynomial poly =>
poly -> OrderedMonomial (MOrder poly) (Arity poly)
leadingMonomial poly
f) (poly -> OrderedMonomial (MOrder poly) (Arity poly)
forall poly.
IsOrderedPolynomial poly =>
poly -> OrderedMonomial (MOrder poly) (Arity poly)
leadingMonomial poly
g)
  {-# INLINE calcWeight #-}

-- | Choose the pair with the least LCM(LT(f), LT(g)) w.r.t. 'Grevlex' order.
data GrevlexStrategy = GrevlexStrategy deriving (ReadPrec [GrevlexStrategy]
ReadPrec GrevlexStrategy
Int -> ReadS GrevlexStrategy
ReadS [GrevlexStrategy]
(Int -> ReadS GrevlexStrategy)
-> ReadS [GrevlexStrategy]
-> ReadPrec GrevlexStrategy
-> ReadPrec [GrevlexStrategy]
-> Read GrevlexStrategy
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
readListPrec :: ReadPrec [GrevlexStrategy]
$creadListPrec :: ReadPrec [GrevlexStrategy]
readPrec :: ReadPrec GrevlexStrategy
$creadPrec :: ReadPrec GrevlexStrategy
readList :: ReadS [GrevlexStrategy]
$creadList :: ReadS [GrevlexStrategy]
readsPrec :: Int -> ReadS GrevlexStrategy
$creadsPrec :: Int -> ReadS GrevlexStrategy
Read, Int -> GrevlexStrategy -> ShowS
[GrevlexStrategy] -> ShowS
GrevlexStrategy -> String
(Int -> GrevlexStrategy -> ShowS)
-> (GrevlexStrategy -> String)
-> ([GrevlexStrategy] -> ShowS)
-> Show GrevlexStrategy
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [GrevlexStrategy] -> ShowS
$cshowList :: [GrevlexStrategy] -> ShowS
show :: GrevlexStrategy -> String
$cshow :: GrevlexStrategy -> String
showsPrec :: Int -> GrevlexStrategy -> ShowS
$cshowsPrec :: Int -> GrevlexStrategy -> ShowS
Show, GrevlexStrategy -> GrevlexStrategy -> Bool
(GrevlexStrategy -> GrevlexStrategy -> Bool)
-> (GrevlexStrategy -> GrevlexStrategy -> Bool)
-> Eq GrevlexStrategy
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: GrevlexStrategy -> GrevlexStrategy -> Bool
$c/= :: GrevlexStrategy -> GrevlexStrategy -> Bool
== :: GrevlexStrategy -> GrevlexStrategy -> Bool
$c== :: GrevlexStrategy -> GrevlexStrategy -> Bool
Eq, Eq GrevlexStrategy
Eq GrevlexStrategy
-> (GrevlexStrategy -> GrevlexStrategy -> Ordering)
-> (GrevlexStrategy -> GrevlexStrategy -> Bool)
-> (GrevlexStrategy -> GrevlexStrategy -> Bool)
-> (GrevlexStrategy -> GrevlexStrategy -> Bool)
-> (GrevlexStrategy -> GrevlexStrategy -> Bool)
-> (GrevlexStrategy -> GrevlexStrategy -> GrevlexStrategy)
-> (GrevlexStrategy -> GrevlexStrategy -> GrevlexStrategy)
-> Ord GrevlexStrategy
GrevlexStrategy -> GrevlexStrategy -> Bool
GrevlexStrategy -> GrevlexStrategy -> Ordering
GrevlexStrategy -> GrevlexStrategy -> GrevlexStrategy
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 :: GrevlexStrategy -> GrevlexStrategy -> GrevlexStrategy
$cmin :: GrevlexStrategy -> GrevlexStrategy -> GrevlexStrategy
max :: GrevlexStrategy -> GrevlexStrategy -> GrevlexStrategy
$cmax :: GrevlexStrategy -> GrevlexStrategy -> GrevlexStrategy
>= :: GrevlexStrategy -> GrevlexStrategy -> Bool
$c>= :: GrevlexStrategy -> GrevlexStrategy -> Bool
> :: GrevlexStrategy -> GrevlexStrategy -> Bool
$c> :: GrevlexStrategy -> GrevlexStrategy -> Bool
<= :: GrevlexStrategy -> GrevlexStrategy -> Bool
$c<= :: GrevlexStrategy -> GrevlexStrategy -> Bool
< :: GrevlexStrategy -> GrevlexStrategy -> Bool
$c< :: GrevlexStrategy -> GrevlexStrategy -> Bool
compare :: GrevlexStrategy -> GrevlexStrategy -> Ordering
$ccompare :: GrevlexStrategy -> GrevlexStrategy -> Ordering
$cp1Ord :: Eq GrevlexStrategy
Ord)

instance SelectionStrategy n GrevlexStrategy where
  type Weight n GrevlexStrategy ord = OrderedMonomial Grevlex n
  calcWeight :: Proxy GrevlexStrategy
-> poly -> poly -> Weight n GrevlexStrategy (MOrder poly)
calcWeight Proxy GrevlexStrategy
_ poly
f poly
g =
    Proxy Grevlex
-> OrderedMonomial (MOrder poly) n -> OrderedMonomial Grevlex n
forall k1 k2 (o' :: k1) (ord :: k2) (n :: Nat).
Proxy o' -> OrderedMonomial ord n -> OrderedMonomial o' n
changeMonomialOrderProxy Proxy Grevlex
forall k (t :: k). Proxy t
Proxy (OrderedMonomial (MOrder poly) n -> OrderedMonomial Grevlex n)
-> OrderedMonomial (MOrder poly) n -> OrderedMonomial Grevlex n
forall a b. (a -> b) -> a -> b
$
      OrderedMonomial (MOrder poly) n
-> OrderedMonomial (MOrder poly) n
-> OrderedMonomial (MOrder poly) n
forall k (n :: Nat) (ord :: k).
KnownNat n =>
OrderedMonomial ord n
-> OrderedMonomial ord n -> OrderedMonomial ord n
lcmMonomial (poly -> OrderedMonomial (MOrder poly) (Arity poly)
forall poly.
IsOrderedPolynomial poly =>
poly -> OrderedMonomial (MOrder poly) (Arity poly)
leadingMonomial poly
f) (poly -> OrderedMonomial (MOrder poly) (Arity poly)
forall poly.
IsOrderedPolynomial poly =>
poly -> OrderedMonomial (MOrder poly) (Arity poly)
leadingMonomial poly
g)
  {-# INLINE calcWeight #-}

data GradedStrategy = GradedStrategy deriving (ReadPrec [GradedStrategy]
ReadPrec GradedStrategy
Int -> ReadS GradedStrategy
ReadS [GradedStrategy]
(Int -> ReadS GradedStrategy)
-> ReadS [GradedStrategy]
-> ReadPrec GradedStrategy
-> ReadPrec [GradedStrategy]
-> Read GradedStrategy
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
readListPrec :: ReadPrec [GradedStrategy]
$creadListPrec :: ReadPrec [GradedStrategy]
readPrec :: ReadPrec GradedStrategy
$creadPrec :: ReadPrec GradedStrategy
readList :: ReadS [GradedStrategy]
$creadList :: ReadS [GradedStrategy]
readsPrec :: Int -> ReadS GradedStrategy
$creadsPrec :: Int -> ReadS GradedStrategy
Read, Int -> GradedStrategy -> ShowS
[GradedStrategy] -> ShowS
GradedStrategy -> String
(Int -> GradedStrategy -> ShowS)
-> (GradedStrategy -> String)
-> ([GradedStrategy] -> ShowS)
-> Show GradedStrategy
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [GradedStrategy] -> ShowS
$cshowList :: [GradedStrategy] -> ShowS
show :: GradedStrategy -> String
$cshow :: GradedStrategy -> String
showsPrec :: Int -> GradedStrategy -> ShowS
$cshowsPrec :: Int -> GradedStrategy -> ShowS
Show, GradedStrategy -> GradedStrategy -> Bool
(GradedStrategy -> GradedStrategy -> Bool)
-> (GradedStrategy -> GradedStrategy -> Bool) -> Eq GradedStrategy
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: GradedStrategy -> GradedStrategy -> Bool
$c/= :: GradedStrategy -> GradedStrategy -> Bool
== :: GradedStrategy -> GradedStrategy -> Bool
$c== :: GradedStrategy -> GradedStrategy -> Bool
Eq, Eq GradedStrategy
Eq GradedStrategy
-> (GradedStrategy -> GradedStrategy -> Ordering)
-> (GradedStrategy -> GradedStrategy -> Bool)
-> (GradedStrategy -> GradedStrategy -> Bool)
-> (GradedStrategy -> GradedStrategy -> Bool)
-> (GradedStrategy -> GradedStrategy -> Bool)
-> (GradedStrategy -> GradedStrategy -> GradedStrategy)
-> (GradedStrategy -> GradedStrategy -> GradedStrategy)
-> Ord GradedStrategy
GradedStrategy -> GradedStrategy -> Bool
GradedStrategy -> GradedStrategy -> Ordering
GradedStrategy -> GradedStrategy -> GradedStrategy
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 :: GradedStrategy -> GradedStrategy -> GradedStrategy
$cmin :: GradedStrategy -> GradedStrategy -> GradedStrategy
max :: GradedStrategy -> GradedStrategy -> GradedStrategy
$cmax :: GradedStrategy -> GradedStrategy -> GradedStrategy
>= :: GradedStrategy -> GradedStrategy -> Bool
$c>= :: GradedStrategy -> GradedStrategy -> Bool
> :: GradedStrategy -> GradedStrategy -> Bool
$c> :: GradedStrategy -> GradedStrategy -> Bool
<= :: GradedStrategy -> GradedStrategy -> Bool
$c<= :: GradedStrategy -> GradedStrategy -> Bool
< :: GradedStrategy -> GradedStrategy -> Bool
$c< :: GradedStrategy -> GradedStrategy -> Bool
compare :: GradedStrategy -> GradedStrategy -> Ordering
$ccompare :: GradedStrategy -> GradedStrategy -> Ordering
$cp1Ord :: Eq GradedStrategy
Ord)

-- | Choose the pair with the least LCM(LT(f), LT(g)) w.r.t. graded current ordering.
instance SelectionStrategy n GradedStrategy where
  type Weight n GradedStrategy ord = OrderedMonomial (Graded ord) n
  calcWeight :: Proxy GradedStrategy
-> poly -> poly -> Weight n GradedStrategy (MOrder poly)
calcWeight Proxy GradedStrategy
_ poly
f poly
g =
    Proxy (Graded (MOrder poly))
-> OrderedMonomial (MOrder poly) n
-> OrderedMonomial (Graded (MOrder poly)) n
forall k1 k2 (o' :: k1) (ord :: k2) (n :: Nat).
Proxy o' -> OrderedMonomial ord n -> OrderedMonomial o' n
changeMonomialOrderProxy Proxy (Graded (MOrder poly))
forall k (t :: k). Proxy t
Proxy (OrderedMonomial (MOrder poly) n
 -> OrderedMonomial (Graded (MOrder poly)) n)
-> OrderedMonomial (MOrder poly) n
-> OrderedMonomial (Graded (MOrder poly)) n
forall a b. (a -> b) -> a -> b
$
      OrderedMonomial (MOrder poly) n
-> OrderedMonomial (MOrder poly) n
-> OrderedMonomial (MOrder poly) n
forall k (n :: Nat) (ord :: k).
KnownNat n =>
OrderedMonomial ord n
-> OrderedMonomial ord n -> OrderedMonomial ord n
lcmMonomial (poly -> OrderedMonomial (MOrder poly) (Arity poly)
forall poly.
IsOrderedPolynomial poly =>
poly -> OrderedMonomial (MOrder poly) (Arity poly)
leadingMonomial poly
f) (poly -> OrderedMonomial (MOrder poly) (Arity poly)
forall poly.
IsOrderedPolynomial poly =>
poly -> OrderedMonomial (MOrder poly) (Arity poly)
leadingMonomial poly
g)
  {-# INLINE calcWeight #-}

-- | Sugar strategy. This chooses the pair with the least phantom homogenized degree and then break the tie with the given strategy (say @s@).
newtype SugarStrategy s = SugarStrategy s deriving (ReadPrec [SugarStrategy s]
ReadPrec (SugarStrategy s)
Int -> ReadS (SugarStrategy s)
ReadS [SugarStrategy s]
(Int -> ReadS (SugarStrategy s))
-> ReadS [SugarStrategy s]
-> ReadPrec (SugarStrategy s)
-> ReadPrec [SugarStrategy s]
-> Read (SugarStrategy s)
forall s. Read s => ReadPrec [SugarStrategy s]
forall s. Read s => ReadPrec (SugarStrategy s)
forall s. Read s => Int -> ReadS (SugarStrategy s)
forall s. Read s => ReadS [SugarStrategy s]
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
readListPrec :: ReadPrec [SugarStrategy s]
$creadListPrec :: forall s. Read s => ReadPrec [SugarStrategy s]
readPrec :: ReadPrec (SugarStrategy s)
$creadPrec :: forall s. Read s => ReadPrec (SugarStrategy s)
readList :: ReadS [SugarStrategy s]
$creadList :: forall s. Read s => ReadS [SugarStrategy s]
readsPrec :: Int -> ReadS (SugarStrategy s)
$creadsPrec :: forall s. Read s => Int -> ReadS (SugarStrategy s)
Read, Int -> SugarStrategy s -> ShowS
[SugarStrategy s] -> ShowS
SugarStrategy s -> String
(Int -> SugarStrategy s -> ShowS)
-> (SugarStrategy s -> String)
-> ([SugarStrategy s] -> ShowS)
-> Show (SugarStrategy s)
forall s. Show s => Int -> SugarStrategy s -> ShowS
forall s. Show s => [SugarStrategy s] -> ShowS
forall s. Show s => SugarStrategy s -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [SugarStrategy s] -> ShowS
$cshowList :: forall s. Show s => [SugarStrategy s] -> ShowS
show :: SugarStrategy s -> String
$cshow :: forall s. Show s => SugarStrategy s -> String
showsPrec :: Int -> SugarStrategy s -> ShowS
$cshowsPrec :: forall s. Show s => Int -> SugarStrategy s -> ShowS
Show, SugarStrategy s -> SugarStrategy s -> Bool
(SugarStrategy s -> SugarStrategy s -> Bool)
-> (SugarStrategy s -> SugarStrategy s -> Bool)
-> Eq (SugarStrategy s)
forall s. Eq s => SugarStrategy s -> SugarStrategy s -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: SugarStrategy s -> SugarStrategy s -> Bool
$c/= :: forall s. Eq s => SugarStrategy s -> SugarStrategy s -> Bool
== :: SugarStrategy s -> SugarStrategy s -> Bool
$c== :: forall s. Eq s => SugarStrategy s -> SugarStrategy s -> Bool
Eq, Eq (SugarStrategy s)
Eq (SugarStrategy s)
-> (SugarStrategy s -> SugarStrategy s -> Ordering)
-> (SugarStrategy s -> SugarStrategy s -> Bool)
-> (SugarStrategy s -> SugarStrategy s -> Bool)
-> (SugarStrategy s -> SugarStrategy s -> Bool)
-> (SugarStrategy s -> SugarStrategy s -> Bool)
-> (SugarStrategy s -> SugarStrategy s -> SugarStrategy s)
-> (SugarStrategy s -> SugarStrategy s -> SugarStrategy s)
-> Ord (SugarStrategy s)
SugarStrategy s -> SugarStrategy s -> Bool
SugarStrategy s -> SugarStrategy s -> Ordering
SugarStrategy s -> SugarStrategy s -> SugarStrategy s
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 s. Ord s => Eq (SugarStrategy s)
forall s. Ord s => SugarStrategy s -> SugarStrategy s -> Bool
forall s. Ord s => SugarStrategy s -> SugarStrategy s -> Ordering
forall s.
Ord s =>
SugarStrategy s -> SugarStrategy s -> SugarStrategy s
min :: SugarStrategy s -> SugarStrategy s -> SugarStrategy s
$cmin :: forall s.
Ord s =>
SugarStrategy s -> SugarStrategy s -> SugarStrategy s
max :: SugarStrategy s -> SugarStrategy s -> SugarStrategy s
$cmax :: forall s.
Ord s =>
SugarStrategy s -> SugarStrategy s -> SugarStrategy s
>= :: SugarStrategy s -> SugarStrategy s -> Bool
$c>= :: forall s. Ord s => SugarStrategy s -> SugarStrategy s -> Bool
> :: SugarStrategy s -> SugarStrategy s -> Bool
$c> :: forall s. Ord s => SugarStrategy s -> SugarStrategy s -> Bool
<= :: SugarStrategy s -> SugarStrategy s -> Bool
$c<= :: forall s. Ord s => SugarStrategy s -> SugarStrategy s -> Bool
< :: SugarStrategy s -> SugarStrategy s -> Bool
$c< :: forall s. Ord s => SugarStrategy s -> SugarStrategy s -> Bool
compare :: SugarStrategy s -> SugarStrategy s -> Ordering
$ccompare :: forall s. Ord s => SugarStrategy s -> SugarStrategy s -> Ordering
$cp1Ord :: forall s. Ord s => Eq (SugarStrategy s)
Ord)

instance SelectionStrategy n s => SelectionStrategy n (SugarStrategy s) where
  type Weight n (SugarStrategy s) ord = (Int, Weight n s ord)
  calcWeight :: Proxy (SugarStrategy s)
-> poly -> poly -> Weight n (SugarStrategy s) (MOrder poly)
calcWeight (Proxy (SugarStrategy s)
Proxy :: Proxy (SugarStrategy s)) poly
f poly
g = (Int
sugar, Proxy s -> poly -> poly -> Weight n s (MOrder poly)
forall k (n :: Nat) (s :: k) poly.
(SelectionStrategy n s, IsOrderedPolynomial poly,
 n ~ Arity poly) =>
Proxy s -> poly -> poly -> Weight n s (MOrder poly)
calcWeight (Proxy s
forall k (t :: k). Proxy t
Proxy :: Proxy s) poly
f poly
g)
    where
      deg' :: poly -> Int
deg' = [Int] -> Int
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum ([Int] -> Int) -> (poly -> [Int]) -> poly -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (OrderedMonomial (MOrder poly) (Arity poly) -> Int)
-> [OrderedMonomial (MOrder poly) (Arity poly)] -> [Int]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
map OrderedMonomial (MOrder poly) (Arity poly) -> Int
forall k (ord :: k) (n :: Nat). OrderedMonomial ord n -> Int
totalDegree ([OrderedMonomial (MOrder poly) (Arity poly)] -> [Int])
-> (poly -> [OrderedMonomial (MOrder poly) (Arity poly)])
-> poly
-> [Int]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set (OrderedMonomial (MOrder poly) (Arity poly))
-> [OrderedMonomial (MOrder poly) (Arity poly)]
forall (t :: * -> *) a. Foldable t => t a -> [a]
F.toList (Set (OrderedMonomial (MOrder poly) (Arity poly))
 -> [OrderedMonomial (MOrder poly) (Arity poly)])
-> (poly -> Set (OrderedMonomial (MOrder poly) (Arity poly)))
-> poly
-> [OrderedMonomial (MOrder poly) (Arity poly)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. poly -> Set (OrderedMonomial (MOrder poly) (Arity poly))
forall poly.
IsOrderedPolynomial poly =>
poly -> Set (OrderedMonomial (MOrder poly) (Arity poly))
orderedMonomials
      tsgr :: poly -> Int
tsgr poly
h = poly -> Int
deg' poly
h Int -> Int -> Int
forall r. Group r => r -> r -> r
- OrderedMonomial (MOrder poly) n -> Int
forall k (ord :: k) (n :: Nat). OrderedMonomial ord n -> Int
totalDegree (poly -> OrderedMonomial (MOrder poly) (Arity poly)
forall poly.
IsOrderedPolynomial poly =>
poly -> OrderedMonomial (MOrder poly) (Arity poly)
leadingMonomial poly
h)
      sugar :: Int
sugar = Int -> Int -> Int
forall a. Ord a => a -> a -> a
max (poly -> Int
tsgr poly
f) (poly -> Int
tsgr poly
g) Int -> Int -> Int
forall r. Additive r => r -> r -> r
+ OrderedMonomial (MOrder poly) n -> Int
forall k (ord :: k) (n :: Nat). OrderedMonomial ord n -> Int
totalDegree (OrderedMonomial (MOrder poly) n
-> OrderedMonomial (MOrder poly) n
-> OrderedMonomial (MOrder poly) n
forall k (n :: Nat) (ord :: k).
KnownNat n =>
OrderedMonomial ord n
-> OrderedMonomial ord n -> OrderedMonomial ord n
lcmMonomial (poly -> OrderedMonomial (MOrder poly) (Arity poly)
forall poly.
IsOrderedPolynomial poly =>
poly -> OrderedMonomial (MOrder poly) (Arity poly)
leadingMonomial poly
f) (poly -> OrderedMonomial (MOrder poly) (Arity poly)
forall poly.
IsOrderedPolynomial poly =>
poly -> OrderedMonomial (MOrder poly) (Arity poly)
leadingMonomial poly
g))
  {-# INLINE calcWeight #-}