{-# LANGUAGE GADTs #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}
{-# OPTIONS_GHC -fplugin Data.Singletons.TypeNats.Presburger #-}
{-# OPTIONS_GHC -fplugin GHC.TypeLits.KnownNat.Solver #-}
{-# OPTIONS_GHC -fplugin GHC.TypeLits.Presburger #-}
{-# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise #-}

module Algebra.Ring.Polynomial.Homogenised (Homogenised, homogenise, unhomogenise, tryHomogenise, HomogOrder) where

import Algebra.Prelude.Core
import Algebra.Ring.Polynomial.Univariate
import Data.Foldable (toList)
import qualified Data.Map as M
import Data.MonoTraversable (osum)
import qualified Data.Sized as SV
import Data.Type.Equality (gcastWith)
import Data.Type.Natural.Lemma.Arithmetic (succInj, succInj')

newtype Homogenised poly = Homogenised (OrderedPolynomial (Unipol (Coefficient poly)) (MOrder poly) (Arity poly))

deriving instance IsOrderedPolynomial poly => Additive (Homogenised poly)

deriving instance IsOrderedPolynomial poly => Unital (Homogenised poly)

deriving instance IsOrderedPolynomial poly => LeftModule Natural (Homogenised poly)

deriving instance IsOrderedPolynomial poly => RightModule Natural (Homogenised poly)

deriving instance IsOrderedPolynomial poly => LeftModule Integer (Homogenised poly)

deriving instance IsOrderedPolynomial poly => RightModule Integer (Homogenised poly)

deriving instance IsOrderedPolynomial poly => Multiplicative (Homogenised poly)

deriving instance IsOrderedPolynomial poly => Monoidal (Homogenised poly)

deriving instance IsOrderedPolynomial poly => Group (Homogenised poly)

deriving instance IsOrderedPolynomial poly => Abelian (Homogenised poly)

deriving instance IsOrderedPolynomial poly => Commutative (Homogenised poly)

deriving instance IsOrderedPolynomial poly => Eq (Homogenised poly)

deriving instance IsOrderedPolynomial poly => DecidableZero (Homogenised poly)

deriving instance IsOrderedPolynomial poly => Semiring (Homogenised poly)

deriving instance IsOrderedPolynomial poly => Rig (Homogenised poly)

deriving instance IsOrderedPolynomial poly => Ring (Homogenised poly)

deriving instance IsOrderedPolynomial poly => Num (Homogenised poly)

instance
  (IsOrderedPolynomial poly, k ~ Coefficient poly) =>
  LeftModule (Scalar k) (Homogenised poly)
  where
  Scalar k
r .* :: Scalar k -> Homogenised poly -> Homogenised poly
.* Homogenised OrderedPolynomial
  (Unipol (Coefficient poly)) (MOrder poly) (Arity poly)
f = OrderedPolynomial
  (Unipol (Coefficient poly)) (MOrder poly) (Arity poly)
-> Homogenised poly
forall poly.
OrderedPolynomial
  (Unipol (Coefficient poly)) (MOrder poly) (Arity poly)
-> Homogenised poly
Homogenised (OrderedPolynomial
   (Unipol (Coefficient poly)) (MOrder poly) (Arity poly)
 -> Homogenised poly)
-> OrderedPolynomial
     (Unipol (Coefficient poly)) (MOrder poly) (Arity poly)
-> Homogenised poly
forall a b. (a -> b) -> a -> b
$ (Coefficient
   (OrderedPolynomial (Unipol k) (MOrder poly) (Arity poly))
 -> Coefficient
      (OrderedPolynomial (Unipol k) (MOrder poly) (Arity poly)))
-> OrderedPolynomial (Unipol k) (MOrder poly) (Arity poly)
-> OrderedPolynomial (Unipol k) (MOrder poly) (Arity poly)
forall poly.
IsPolynomial poly =>
(Coefficient poly -> Coefficient poly) -> poly -> poly
mapCoeff' (Scalar k
r Scalar k -> Unipol k -> Unipol k
forall r m. LeftModule r m => r -> m -> m
.*) OrderedPolynomial (Unipol k) (MOrder poly) (Arity poly)
OrderedPolynomial
  (Unipol (Coefficient poly)) (MOrder poly) (Arity poly)
f

instance
  (IsOrderedPolynomial poly, k ~ Coefficient poly) =>
  RightModule (Scalar k) (Homogenised poly)
  where
  Homogenised OrderedPolynomial
  (Unipol (Coefficient poly)) (MOrder poly) (Arity poly)
f *. :: Homogenised poly -> Scalar k -> Homogenised poly
*. Scalar k
r = OrderedPolynomial
  (Unipol (Coefficient poly)) (MOrder poly) (Arity poly)
-> Homogenised poly
forall poly.
OrderedPolynomial
  (Unipol (Coefficient poly)) (MOrder poly) (Arity poly)
-> Homogenised poly
Homogenised (OrderedPolynomial
   (Unipol (Coefficient poly)) (MOrder poly) (Arity poly)
 -> Homogenised poly)
-> OrderedPolynomial
     (Unipol (Coefficient poly)) (MOrder poly) (Arity poly)
-> Homogenised poly
forall a b. (a -> b) -> a -> b
$ (Coefficient
   (OrderedPolynomial (Unipol k) (MOrder poly) (Arity poly))
 -> Coefficient
      (OrderedPolynomial (Unipol k) (MOrder poly) (Arity poly)))
-> OrderedPolynomial (Unipol k) (MOrder poly) (Arity poly)
-> OrderedPolynomial (Unipol k) (MOrder poly) (Arity poly)
forall poly.
IsPolynomial poly =>
(Coefficient poly -> Coefficient poly) -> poly -> poly
mapCoeff' (Unipol k -> Scalar k -> Unipol k
forall r m. RightModule r m => m -> r -> m
*. Scalar k
r) OrderedPolynomial (Unipol k) (MOrder poly) (Arity poly)
OrderedPolynomial
  (Unipol (Coefficient poly)) (MOrder poly) (Arity poly)
f

instance IsOrderedPolynomial poly => IsPolynomial (Homogenised poly) where
  type Coefficient (Homogenised poly) = Coefficient poly
  type Arity (Homogenised poly) = Arity poly + 1
  sArity :: proxy (Homogenised poly) -> SNat (Arity (Homogenised poly))
sArity proxy (Homogenised poly)
_ = SNat (Arity (Homogenised poly))
forall (n :: Nat). KnownNat n => SNat n
sNat
  injectCoeff :: Coefficient (Homogenised poly) -> Homogenised poly
injectCoeff = OrderedPolynomial
  (Unipol (Coefficient poly)) (MOrder poly) (Arity poly)
-> Homogenised poly
forall poly.
OrderedPolynomial
  (Unipol (Coefficient poly)) (MOrder poly) (Arity poly)
-> Homogenised poly
Homogenised (OrderedPolynomial
   (Unipol (Coefficient poly)) (MOrder poly) (Arity poly)
 -> Homogenised poly)
-> (Coefficient poly
    -> OrderedPolynomial
         (Unipol (Coefficient poly)) (MOrder poly) (Arity poly))
-> Coefficient poly
-> Homogenised poly
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Unipol (Coefficient poly)
-> OrderedPolynomial
     (Unipol (Coefficient poly)) (MOrder poly) (Arity poly)
forall poly. IsPolynomial poly => Coefficient poly -> poly
injectCoeff (Unipol (Coefficient poly)
 -> OrderedPolynomial
      (Unipol (Coefficient poly)) (MOrder poly) (Arity poly))
-> (Coefficient poly -> Unipol (Coefficient poly))
-> Coefficient poly
-> OrderedPolynomial
     (Unipol (Coefficient poly)) (MOrder poly) (Arity poly)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Coefficient poly -> Unipol (Coefficient poly)
forall poly. IsPolynomial poly => Coefficient poly -> poly
injectCoeff
  fromMonomial :: Monomial (Arity (Homogenised poly)) -> Homogenised poly
fromMonomial ((os :: USized k Int) :> o) =
    (n1 :~: Arity poly)
-> ((n1 ~ Arity poly) => Homogenised poly) -> Homogenised poly
forall k (a :: k) (b :: k) r. (a :~: b) -> ((a ~ b) => r) -> r
gcastWith ((Succ n1 :~: Succ (Arity poly)) -> n1 :~: Arity poly
forall (n :: Nat) (m :: Nat). (Succ n :~: Succ m) -> n :~: m
succInj (Succ n1 :~: Succ (Arity poly)
forall k (a :: k). a :~: a
Refl :: k + 1 :~: Arity poly + 1)) (((n1 ~ Arity poly) => Homogenised poly) -> Homogenised poly)
-> ((n1 ~ Arity poly) => Homogenised poly) -> Homogenised poly
forall a b. (a -> b) -> a -> b
$
      OrderedPolynomial
  (Unipol (Coefficient poly)) (MOrder poly) (Arity poly)
-> Homogenised poly
forall poly.
OrderedPolynomial
  (Unipol (Coefficient poly)) (MOrder poly) (Arity poly)
-> Homogenised poly
Homogenised (OrderedPolynomial
   (Unipol (Coefficient poly)) (MOrder poly) (Arity poly)
 -> Homogenised poly)
-> OrderedPolynomial
     (Unipol (Coefficient poly)) (MOrder poly) (Arity poly)
-> Homogenised poly
forall a b. (a -> b) -> a -> b
$ Monomial (Arity (Unipol (Coefficient poly)))
-> Unipol (Coefficient poly)
forall poly. IsPolynomial poly => Monomial (Arity poly) -> poly
fromMonomial (Int -> Sized Vector 1 Int
forall (f :: * -> *) a. (CPointed f, Dom f a) => a -> Sized f 1 a
SV.singleton Int
o) Coefficient
  (OrderedPolynomial
     (Unipol (Coefficient poly)) (MOrder poly) (Arity poly))
-> OrderedPolynomial
     (Unipol (Coefficient poly)) (MOrder poly) (Arity poly)
-> OrderedPolynomial
     (Unipol (Coefficient poly)) (MOrder poly) (Arity poly)
forall poly. IsPolynomial poly => Coefficient poly -> poly -> poly
!* Monomial
  (Arity
     (OrderedPolynomial
        (Unipol (Coefficient poly)) (MOrder poly) (Arity poly)))
-> OrderedPolynomial
     (Unipol (Coefficient poly)) (MOrder poly) (Arity poly)
forall poly. IsPolynomial poly => Monomial (Arity poly) -> poly
fromMonomial USized n1 Int
Monomial
  (Arity
     (OrderedPolynomial
        (Unipol (Coefficient poly)) (MOrder poly) (Arity poly)))
os
  fromMonomial Monomial (Arity (Homogenised poly))
_ = [Char] -> Homogenised poly
forall a. HasCallStack => [Char] -> a
error [Char]
"Cannot happen!"
  terms' :: Homogenised poly
-> Map
     (Monomial (Arity (Homogenised poly)))
     (Coefficient (Homogenised poly))
terms' (Homogenised OrderedPolynomial
  (Unipol (Coefficient poly)) (MOrder poly) (Arity poly)
f) =
    [(Sized Vector (Succ (Arity poly)) Int, Coefficient poly)]
-> Map (Sized Vector (Succ (Arity poly)) Int) (Coefficient poly)
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList
      [ (Sized Vector (Arity poly) Int
ml Sized Vector (Arity poly) Int
-> Sized Vector 1 Int -> Sized Vector (Succ (Arity poly)) Int
forall (f :: * -> *) (n :: Nat) (m :: Nat) a.
(CFreeMonoid f, Dom f a) =>
Sized f n a -> Sized f m a -> Sized f (n + m) a
SV.++ Sized Vector 1 Int
mr, Coefficient poly
cf)
      | (Sized Vector (Arity poly) Int
ml, Unipol (Coefficient poly)
fpol) <- Map (Sized Vector (Arity poly) Int) (Unipol (Coefficient poly))
-> [(Sized Vector (Arity poly) Int, Unipol (Coefficient poly))]
forall k a. Map k a -> [(k, a)]
M.toList (Map (Sized Vector (Arity poly) Int) (Unipol (Coefficient poly))
 -> [(Sized Vector (Arity poly) Int, Unipol (Coefficient poly))])
-> Map (Sized Vector (Arity poly) Int) (Unipol (Coefficient poly))
-> [(Sized Vector (Arity poly) Int, Unipol (Coefficient poly))]
forall a b. (a -> b) -> a -> b
$ OrderedPolynomial
  (Unipol (Coefficient poly)) (MOrder poly) (Arity poly)
-> Map
     (Monomial
        (Arity
           (OrderedPolynomial
              (Unipol (Coefficient poly)) (MOrder poly) (Arity poly))))
     (Coefficient
        (OrderedPolynomial
           (Unipol (Coefficient poly)) (MOrder poly) (Arity poly)))
forall poly.
IsPolynomial poly =>
poly -> Map (Monomial (Arity poly)) (Coefficient poly)
terms' OrderedPolynomial
  (Unipol (Coefficient poly)) (MOrder poly) (Arity poly)
f
      , (Sized Vector 1 Int
mr, Coefficient poly
cf) <- Map (Sized Vector 1 Int) (Coefficient poly)
-> [(Sized Vector 1 Int, Coefficient poly)]
forall k a. Map k a -> [(k, a)]
M.toList (Map (Sized Vector 1 Int) (Coefficient poly)
 -> [(Sized Vector 1 Int, Coefficient poly)])
-> Map (Sized Vector 1 Int) (Coefficient poly)
-> [(Sized Vector 1 Int, Coefficient poly)]
forall a b. (a -> b) -> a -> b
$ Unipol (Coefficient poly)
-> Map
     (Monomial (Arity (Unipol (Coefficient poly))))
     (Coefficient (Unipol (Coefficient poly)))
forall poly.
IsPolynomial poly =>
poly -> Map (Monomial (Arity poly)) (Coefficient poly)
terms' Unipol (Coefficient poly)
fpol
      ]
  liftMap :: (Ordinal (Arity (Homogenised poly)) -> alg)
-> Homogenised poly -> alg
liftMap Ordinal (Arity (Homogenised poly)) -> alg
gen (Homogenised OrderedPolynomial
  (Unipol (Coefficient poly)) (MOrder poly) (Arity poly)
f) =
    SNat (1 + Arity poly) -> (KnownNat (1 + Arity poly) => alg) -> alg
forall (n :: Nat) r. SNat n -> (KnownNat n => r) -> r
withKnownNat (KnownNat 1 => SNat 1
forall (n :: Nat). KnownNat n => SNat n
sNat @1 SNat 1 -> SNat (Arity poly) -> SNat (1 + Arity poly)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n + m)
%+ KnownNat (Arity poly) => SNat (Arity poly)
forall (n :: Nat). KnownNat n => SNat n
sNat @(Arity poly)) ((KnownNat (1 + Arity poly) => alg) -> alg)
-> (KnownNat (1 + Arity poly) => alg) -> alg
forall a b. (a -> b) -> a -> b
$
      (Coefficient
   (OrderedPolynomial
      (Unipol (Coefficient poly)) (MOrder poly) (Arity poly))
 -> alg -> alg)
-> Sized
     (Arity
        (OrderedPolynomial
           (Unipol (Coefficient poly)) (MOrder poly) (Arity poly)))
     alg
-> OrderedPolynomial
     (Unipol (Coefficient poly)) (MOrder poly) (Arity poly)
-> alg
forall poly m.
(IsPolynomial poly, Ring m) =>
(Coefficient poly -> m -> m) -> Sized (Arity poly) m -> poly -> m
substWith
        ( \Coefficient
  (OrderedPolynomial
     (Unipol (Coefficient poly)) (MOrder poly) (Arity poly))
g alg
alg ->
            alg
alg alg -> alg -> alg
forall r. Multiplicative r => r -> r -> r
* (Ordinal 1 -> alg) -> Unipol (Coefficient poly) -> alg
forall k r.
(Module (Scalar k) r, Monoidal k, Unital r) =>
(Ordinal 1 -> r) -> Unipol k -> r
liftMapUnipol (alg -> Ordinal 1 -> alg
forall a b. a -> b -> a
const (alg -> Ordinal 1 -> alg) -> alg -> Ordinal 1 -> alg
forall a b. (a -> b) -> a -> b
$ Ordinal (Arity (Homogenised poly)) -> alg
gen (Ordinal (Succ (Arity poly))
forall a. Bounded a => a
maxBound :: Ordinal (Arity poly + 1))) Coefficient
  (OrderedPolynomial
     (Unipol (Coefficient poly)) (MOrder poly) (Arity poly))
Unipol (Coefficient poly)
g
        )
        (SNat (Arity poly)
-> (Ordinal (Arity poly) -> alg) -> Sized Vector (Arity poly) alg
forall (f :: * -> *) (n :: Nat) a.
(CFreeMonoid f, Dom f a) =>
SNat n -> (Ordinal n -> a) -> Sized f n a
generate SNat (Arity poly)
forall (n :: Nat). KnownNat n => SNat n
sNat ((Ordinal (Arity poly) -> alg) -> Sized Vector (Arity poly) alg)
-> (Ordinal (Arity poly) -> alg) -> Sized Vector (Arity poly) alg
forall a b. (a -> b) -> a -> b
$ Ordinal (Succ (Arity poly)) -> alg
Ordinal (Arity (Homogenised poly)) -> alg
gen (Ordinal (Succ (Arity poly)) -> alg)
-> (Ordinal (Arity poly) -> Ordinal (Succ (Arity poly)))
-> Ordinal (Arity poly)
-> alg
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Ordinal (Arity poly) -> Ordinal (Succ (Arity poly))
forall (n :: Nat) (m :: Nat). (n <= m) => Ordinal n -> Ordinal m
inclusion)
        OrderedPolynomial
  (Unipol (Coefficient poly)) (MOrder poly) (Arity poly)
f

type HomogOrder n ord = ProductOrder n 1 ord Lex

instance IsOrderedPolynomial poly => IsOrderedPolynomial (Homogenised poly) where
  type MOrder (Homogenised poly) = HomogOrder (Arity poly) (MOrder poly)
  leadingTerm :: Homogenised poly
-> (Coefficient (Homogenised poly),
    OrderedMonomial
      (MOrder (Homogenised poly)) (Arity (Homogenised poly)))
leadingTerm (Homogenised OrderedPolynomial
  (Unipol (Coefficient poly)) (MOrder poly) (Arity poly)
poly) =
    let (Unipol (Coefficient poly)
p, OrderedMonomial (MOrder poly) (Arity poly)
l) = OrderedPolynomial
  (Unipol (Coefficient poly)) (MOrder poly) (Arity poly)
-> (Coefficient
      (OrderedPolynomial
         (Unipol (Coefficient poly)) (MOrder poly) (Arity poly)),
    OrderedMonomial
      (MOrder
         (OrderedPolynomial
            (Unipol (Coefficient poly)) (MOrder poly) (Arity poly)))
      (Arity
         (OrderedPolynomial
            (Unipol (Coefficient poly)) (MOrder poly) (Arity poly))))
forall poly.
IsOrderedPolynomial poly =>
poly
-> (Coefficient poly, OrderedMonomial (MOrder poly) (Arity poly))
leadingTerm OrderedPolynomial
  (Unipol (Coefficient poly)) (MOrder poly) (Arity poly)
poly
        (Coefficient poly
c, OrderedMonomial Grevlex 1
r) = Unipol (Coefficient poly)
-> (Coefficient (Unipol (Coefficient poly)),
    OrderedMonomial
      (MOrder (Unipol (Coefficient poly)))
      (Arity (Unipol (Coefficient poly))))
forall poly.
IsOrderedPolynomial poly =>
poly
-> (Coefficient poly, OrderedMonomial (MOrder poly) (Arity poly))
leadingTerm Unipol (Coefficient poly)
p
     in (Coefficient poly
Coefficient (Homogenised poly)
c, Monomial (Arity poly + 1)
-> OrderedMonomial
     (HomogOrder (Arity poly) (MOrder poly)) (Arity poly + 1)
forall k (ordering :: k) (n :: Nat).
Monomial n -> OrderedMonomial ordering n
OrderedMonomial (Monomial (Arity poly + 1)
 -> OrderedMonomial
      (HomogOrder (Arity poly) (MOrder poly)) (Arity poly + 1))
-> Monomial (Arity poly + 1)
-> OrderedMonomial
     (HomogOrder (Arity poly) (MOrder poly)) (Arity poly + 1)
forall a b. (a -> b) -> a -> b
$ OrderedMonomial (MOrder poly) (Arity poly) -> Monomial (Arity poly)
forall k (ordering :: k) (n :: Nat).
OrderedMonomial ordering n -> Monomial n
getMonomial OrderedMonomial (MOrder poly) (Arity poly)
l Monomial (Arity poly)
-> Sized Vector 1 Int -> Monomial (Arity poly + 1)
forall (f :: * -> *) (n :: Nat) (m :: Nat) a.
(CFreeMonoid f, Dom f a) =>
Sized f n a -> Sized f m a -> Sized f (n + m) a
SV.++ OrderedMonomial Grevlex 1 -> Sized Vector 1 Int
forall k (ordering :: k) (n :: Nat).
OrderedMonomial ordering n -> Monomial n
getMonomial OrderedMonomial Grevlex 1
r)
  {-# INLINE leadingTerm #-}
  splitLeadingTerm :: Homogenised poly
-> ((Coefficient (Homogenised poly),
     OrderedMonomial
       (MOrder (Homogenised poly)) (Arity (Homogenised poly))),
    Homogenised poly)
splitLeadingTerm (Homogenised OrderedPolynomial
  (Unipol (Coefficient poly)) (MOrder poly) (Arity poly)
poly) =
    let ((Unipol (Coefficient poly)
p, OrderedMonomial (MOrder poly) (Arity poly)
l), OrderedPolynomial
  (Unipol (Coefficient poly)) (MOrder poly) (Arity poly)
rest) = OrderedPolynomial
  (Unipol (Coefficient poly)) (MOrder poly) (Arity poly)
-> ((Coefficient
       (OrderedPolynomial
          (Unipol (Coefficient poly)) (MOrder poly) (Arity poly)),
     OrderedMonomial
       (MOrder
          (OrderedPolynomial
             (Unipol (Coefficient poly)) (MOrder poly) (Arity poly)))
       (Arity
          (OrderedPolynomial
             (Unipol (Coefficient poly)) (MOrder poly) (Arity poly)))),
    OrderedPolynomial
      (Unipol (Coefficient poly)) (MOrder poly) (Arity poly))
forall poly.
IsOrderedPolynomial poly =>
poly
-> ((Coefficient poly, OrderedMonomial (MOrder poly) (Arity poly)),
    poly)
splitLeadingTerm OrderedPolynomial
  (Unipol (Coefficient poly)) (MOrder poly) (Arity poly)
poly
        ((Coefficient poly
c, OrderedMonomial Grevlex 1
r), Unipol (Coefficient poly)
grest) = Unipol (Coefficient poly)
-> ((Coefficient (Unipol (Coefficient poly)),
     OrderedMonomial
       (MOrder (Unipol (Coefficient poly)))
       (Arity (Unipol (Coefficient poly)))),
    Unipol (Coefficient poly))
forall poly.
IsOrderedPolynomial poly =>
poly
-> ((Coefficient poly, OrderedMonomial (MOrder poly) (Arity poly)),
    poly)
splitLeadingTerm Unipol (Coefficient poly)
p
        g :: OrderedPolynomial
  (Unipol (Coefficient poly)) (MOrder poly) (Arity poly)
g = (Coefficient
   (OrderedPolynomial
      (Unipol (Coefficient poly)) (MOrder poly) (Arity poly)),
 OrderedMonomial
   (MOrder
      (OrderedPolynomial
         (Unipol (Coefficient poly)) (MOrder poly) (Arity poly)))
   (Arity
      (OrderedPolynomial
         (Unipol (Coefficient poly)) (MOrder poly) (Arity poly))))
-> OrderedPolynomial
     (Unipol (Coefficient poly)) (MOrder poly) (Arity poly)
forall poly.
IsOrderedPolynomial poly =>
(Coefficient poly, OrderedMonomial (MOrder poly) (Arity poly))
-> poly
toPolynomial (Coefficient
  (OrderedPolynomial
     (Unipol (Coefficient poly)) (MOrder poly) (Arity poly))
Unipol (Coefficient poly)
grest, OrderedMonomial (MOrder poly) (Arity poly)
OrderedMonomial
  (MOrder
     (OrderedPolynomial
        (Unipol (Coefficient poly)) (MOrder poly) (Arity poly)))
  (Arity
     (OrderedPolynomial
        (Unipol (Coefficient poly)) (MOrder poly) (Arity poly)))
l) OrderedPolynomial
  (Unipol (Coefficient poly)) (MOrder poly) (Arity poly)
-> OrderedPolynomial
     (Unipol (Coefficient poly)) (MOrder poly) (Arity poly)
-> OrderedPolynomial
     (Unipol (Coefficient poly)) (MOrder poly) (Arity poly)
forall r. Additive r => r -> r -> r
+ OrderedPolynomial
  (Unipol (Coefficient poly)) (MOrder poly) (Arity poly)
rest
     in ((Coefficient poly
Coefficient (Homogenised poly)
c, Monomial (Arity poly + 1)
-> OrderedMonomial
     (HomogOrder (Arity poly) (MOrder poly)) (Arity poly + 1)
forall k (ordering :: k) (n :: Nat).
Monomial n -> OrderedMonomial ordering n
OrderedMonomial (Monomial (Arity poly + 1)
 -> OrderedMonomial
      (HomogOrder (Arity poly) (MOrder poly)) (Arity poly + 1))
-> Monomial (Arity poly + 1)
-> OrderedMonomial
     (HomogOrder (Arity poly) (MOrder poly)) (Arity poly + 1)
forall a b. (a -> b) -> a -> b
$ OrderedMonomial (MOrder poly) (Arity poly) -> Monomial (Arity poly)
forall k (ordering :: k) (n :: Nat).
OrderedMonomial ordering n -> Monomial n
getMonomial OrderedMonomial (MOrder poly) (Arity poly)
l Monomial (Arity poly)
-> Sized Vector 1 Int -> Monomial (Arity poly + 1)
forall (f :: * -> *) (n :: Nat) (m :: Nat) a.
(CFreeMonoid f, Dom f a) =>
Sized f n a -> Sized f m a -> Sized f (n + m) a
SV.++ OrderedMonomial Grevlex 1 -> Sized Vector 1 Int
forall k (ordering :: k) (n :: Nat).
OrderedMonomial ordering n -> Monomial n
getMonomial OrderedMonomial Grevlex 1
r), OrderedPolynomial
  (Unipol (Coefficient poly)) (MOrder poly) (Arity poly)
-> Homogenised poly
forall poly.
OrderedPolynomial
  (Unipol (Coefficient poly)) (MOrder poly) (Arity poly)
-> Homogenised poly
Homogenised OrderedPolynomial
  (Unipol (Coefficient poly)) (MOrder poly) (Arity poly)
g)
  {-# INLINE splitLeadingTerm #-}

instance
  (IsOrderedPolynomial poly, PrettyCoeff (Coefficient poly)) =>
  Show (Homogenised poly)
  where
  showsPrec :: Int -> Homogenised poly -> ShowS
showsPrec = Sized (Arity (Homogenised poly)) [Char]
-> Int -> Homogenised poly -> ShowS
forall poly.
(IsOrderedPolynomial poly, PrettyCoeff (Coefficient poly)) =>
Sized (Arity poly) [Char] -> Int -> poly -> ShowS
showsPolynomialWith (Sized (Arity (Homogenised poly)) [Char]
 -> Int -> Homogenised poly -> ShowS)
-> Sized (Arity (Homogenised poly)) [Char]
-> Int
-> Homogenised poly
-> ShowS
forall a b. (a -> b) -> a -> b
$ SNat (Arity poly + 1)
-> (Ordinal (Arity poly + 1) -> [Char])
-> Sized Vector (Arity poly + 1) [Char]
forall (f :: * -> *) (n :: Nat) a.
(CFreeMonoid f, Dom f a) =>
SNat n -> (Ordinal n -> a) -> Sized f n a
generate SNat (Arity poly + 1)
forall (n :: Nat). KnownNat n => SNat n
sNat (\Ordinal (Arity poly + 1)
i -> [Char]
"X_" [Char] -> ShowS
forall w. Monoid w => w -> w -> w
++ Int -> [Char]
forall a. Show a => a -> [Char]
show (Ordinal (Arity poly + 1) -> Int
forall a. Enum a => a -> Int
fromEnum Ordinal (Arity poly + 1)
i))

instance (IsOrderedPolynomial poly) => ZeroProductSemiring (Homogenised poly)

instance (Field (Coefficient poly), IsOrderedPolynomial poly) => UFD (Homogenised poly)

instance (Field (Coefficient poly), IsOrderedPolynomial poly) => PID (Homogenised poly)

instance
  (Field (Coefficient poly), IsOrderedPolynomial poly) =>
  Euclidean (Homogenised poly)
  where
  Homogenised poly
f0 divide :: Homogenised poly
-> Homogenised poly -> (Homogenised poly, Homogenised poly)
`divide` Homogenised poly
g = Homogenised poly
-> Homogenised poly -> (Homogenised poly, Homogenised poly)
step Homogenised poly
f0 Homogenised poly
forall m. Monoidal m => m
zero
    where
      lm :: OrderedMonomial
  (MOrder (Homogenised poly)) (Arity (Homogenised poly))
lm = Homogenised poly
-> OrderedMonomial
     (MOrder (Homogenised poly)) (Arity (Homogenised poly))
forall poly.
IsOrderedPolynomial poly =>
poly -> OrderedMonomial (MOrder poly) (Arity poly)
leadingMonomial Homogenised poly
g
      step :: Homogenised poly
-> Homogenised poly -> (Homogenised poly, Homogenised poly)
step Homogenised poly
p Homogenised poly
quo
        | Homogenised poly -> Bool
forall r. DecidableZero r => r -> Bool
isZero Homogenised poly
p = (Homogenised poly
quo, Homogenised poly
p)
        | OrderedMonomial
  (MOrder (Homogenised poly)) (Arity (Homogenised poly))
OrderedMonomial
  (HomogOrder (Arity poly) (MOrder poly)) (Arity poly + 1)
lm OrderedMonomial
  (HomogOrder (Arity poly) (MOrder poly)) (Arity poly + 1)
-> OrderedMonomial
     (HomogOrder (Arity poly) (MOrder poly)) (Arity poly + 1)
-> Bool
forall k (n :: Nat) (ord :: k).
KnownNat n =>
OrderedMonomial ord n -> OrderedMonomial ord n -> Bool
`divs` Homogenised poly
-> OrderedMonomial
     (MOrder (Homogenised poly)) (Arity (Homogenised poly))
forall poly.
IsOrderedPolynomial poly =>
poly -> OrderedMonomial (MOrder poly) (Arity poly)
leadingMonomial Homogenised poly
p =
          let q :: Homogenised poly
q = (Coefficient (Homogenised poly),
 OrderedMonomial
   (MOrder (Homogenised poly)) (Arity (Homogenised poly)))
-> Homogenised poly
forall poly.
IsOrderedPolynomial poly =>
(Coefficient poly, OrderedMonomial (MOrder poly) (Arity poly))
-> poly
toPolynomial ((Coefficient (Homogenised poly),
  OrderedMonomial
    (MOrder (Homogenised poly)) (Arity (Homogenised poly)))
 -> Homogenised poly)
-> (Coefficient (Homogenised poly),
    OrderedMonomial
      (MOrder (Homogenised poly)) (Arity (Homogenised poly)))
-> Homogenised poly
forall a b. (a -> b) -> a -> b
$ Homogenised poly
-> (Coefficient (Homogenised poly),
    OrderedMonomial
      (MOrder (Homogenised poly)) (Arity (Homogenised poly)))
forall poly.
IsOrderedPolynomial poly =>
poly
-> (Coefficient poly, OrderedMonomial (MOrder poly) (Arity poly))
leadingTerm Homogenised poly
p (Coefficient poly,
 OrderedMonomial
   (HomogOrder (Arity poly) (MOrder poly)) (Arity poly + 1))
-> (Coefficient poly,
    OrderedMonomial
      (HomogOrder (Arity poly) (MOrder poly)) (Arity poly + 1))
-> (Coefficient poly,
    OrderedMonomial
      (HomogOrder (Arity poly) (MOrder poly)) (Arity poly + 1))
forall k (n :: Nat) r (ord :: k).
(KnownNat n, Field r) =>
(r, OrderedMonomial ord n)
-> (r, OrderedMonomial ord n) -> (r, OrderedMonomial ord n)
`tryDiv` Homogenised poly
-> (Coefficient (Homogenised poly),
    OrderedMonomial
      (MOrder (Homogenised poly)) (Arity (Homogenised poly)))
forall poly.
IsOrderedPolynomial poly =>
poly
-> (Coefficient poly, OrderedMonomial (MOrder poly) (Arity poly))
leadingTerm Homogenised poly
g
           in Homogenised poly
-> Homogenised poly -> (Homogenised poly, Homogenised poly)
step (Homogenised poly
p Homogenised poly -> Homogenised poly -> Homogenised poly
forall r. Group r => r -> r -> r
- (Homogenised poly
q Homogenised poly -> Homogenised poly -> Homogenised poly
forall r. Multiplicative r => r -> r -> r
* Homogenised poly
g)) (Homogenised poly
quo Homogenised poly -> Homogenised poly -> Homogenised poly
forall r. Additive r => r -> r -> r
+ Homogenised poly
q)
        | Bool
otherwise = (Homogenised poly
quo, Homogenised poly
p)

  degree :: Homogenised poly -> Maybe Natural
degree Homogenised poly
f
    | Homogenised poly -> Bool
forall r. DecidableZero r => r -> Bool
isZero Homogenised poly
f = Maybe Natural
forall a. Maybe a
Nothing
    | Bool
otherwise = Natural -> Maybe Natural
forall a. a -> Maybe a
Just (Natural -> Maybe Natural) -> Natural -> Maybe Natural
forall a b. (a -> b) -> a -> b
$ Int -> Natural
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int -> Natural) -> Int -> Natural
forall a b. (a -> b) -> a -> b
$ Homogenised poly -> Int
forall poly. IsPolynomial poly => poly -> Int
totalDegree' Homogenised poly
f

instance (Field (Coefficient poly), IsOrderedPolynomial poly) => IntegralDomain (Homogenised poly)

instance (Field (Coefficient poly), IsOrderedPolynomial poly) => GCDDomain (Homogenised poly)

instance (Field (Coefficient poly), IsOrderedPolynomial poly) => UnitNormalForm (Homogenised poly) where
  splitUnit :: Homogenised poly -> (Homogenised poly, Homogenised poly)
splitUnit = Homogenised poly -> (Homogenised poly, Homogenised poly)
forall r poly.
(UnitNormalForm r, Coefficient poly ~ r,
 IsOrderedPolynomial poly) =>
poly -> (poly, poly)
splitUnitDefault

instance (Field (Coefficient poly), IsOrderedPolynomial poly) => DecidableUnits (Homogenised poly) where
  recipUnit :: Homogenised poly -> Maybe (Homogenised poly)
recipUnit = Homogenised poly -> Maybe (Homogenised poly)
forall r poly.
(DecidableUnits r, Coefficient poly ~ r, IsPolynomial poly) =>
poly -> Maybe poly
recipUnitDefault
  isUnit :: Homogenised poly -> Bool
isUnit = Homogenised poly -> Bool
forall r poly.
(DecidableUnits r, Coefficient poly ~ r, IsPolynomial poly) =>
poly -> Bool
isUnitDefault

instance (Field (Coefficient poly), IsOrderedPolynomial poly) => DecidableAssociates (Homogenised poly) where
  isAssociate :: Homogenised poly -> Homogenised poly -> Bool
isAssociate = Homogenised poly -> Homogenised poly -> Bool
forall r poly.
(UnitNormalForm r, Coefficient poly ~ r,
 IsOrderedPolynomial poly) =>
poly -> poly -> Bool
isAssociateDefault

homogenise :: IsOrderedPolynomial poly => poly -> Homogenised poly
homogenise :: poly -> Homogenised poly
homogenise poly
p =
  let d :: Int
d = poly -> Int
forall poly. IsPolynomial poly => poly -> Int
totalDegree' poly
p
   in OrderedPolynomial
  (Unipol (Coefficient poly)) (MOrder poly) (Arity poly)
-> Homogenised poly
forall poly.
OrderedPolynomial
  (Unipol (Coefficient poly)) (MOrder poly) (Arity poly)
-> Homogenised poly
Homogenised (OrderedPolynomial
   (Unipol (Coefficient poly)) (MOrder poly) (Arity poly)
 -> Homogenised poly)
-> OrderedPolynomial
     (Unipol (Coefficient poly)) (MOrder poly) (Arity poly)
-> Homogenised poly
forall a b. (a -> b) -> a -> b
$
        Map
  (OrderedMonomial
     (MOrder
        (OrderedPolynomial
           (Unipol (Coefficient poly)) (MOrder poly) (Arity poly)))
     (Arity
        (OrderedPolynomial
           (Unipol (Coefficient poly)) (MOrder poly) (Arity poly))))
  (Coefficient
     (OrderedPolynomial
        (Unipol (Coefficient poly)) (MOrder poly) (Arity poly)))
-> OrderedPolynomial
     (Unipol (Coefficient poly)) (MOrder poly) (Arity poly)
forall poly.
IsOrderedPolynomial poly =>
Map (OrderedMonomial (MOrder poly) (Arity poly)) (Coefficient poly)
-> poly
polynomial (Map
   (OrderedMonomial
      (MOrder
         (OrderedPolynomial
            (Unipol (Coefficient poly)) (MOrder poly) (Arity poly)))
      (Arity
         (OrderedPolynomial
            (Unipol (Coefficient poly)) (MOrder poly) (Arity poly))))
   (Coefficient
      (OrderedPolynomial
         (Unipol (Coefficient poly)) (MOrder poly) (Arity poly)))
 -> OrderedPolynomial
      (Unipol (Coefficient poly)) (MOrder poly) (Arity poly))
-> Map
     (OrderedMonomial
        (MOrder
           (OrderedPolynomial
              (Unipol (Coefficient poly)) (MOrder poly) (Arity poly)))
        (Arity
           (OrderedPolynomial
              (Unipol (Coefficient poly)) (MOrder poly) (Arity poly))))
     (Coefficient
        (OrderedPolynomial
           (Unipol (Coefficient poly)) (MOrder poly) (Arity poly)))
-> OrderedPolynomial
     (Unipol (Coefficient poly)) (MOrder poly) (Arity poly)
forall a b. (a -> b) -> a -> b
$
          (OrderedMonomial (MOrder poly) (Arity poly)
 -> Coefficient poly -> Unipol (Coefficient poly))
-> Map
     (OrderedMonomial (MOrder poly) (Arity poly)) (Coefficient poly)
-> Map
     (OrderedMonomial (MOrder poly) (Arity poly))
     (Unipol (Coefficient poly))
forall k a b. (k -> a -> b) -> Map k a -> Map k b
M.mapWithKey (\OrderedMonomial (MOrder poly) (Arity poly)
k Coefficient poly
v -> (Coefficient (Unipol (Coefficient poly)),
 OrderedMonomial
   (MOrder (Unipol (Coefficient poly)))
   (Arity (Unipol (Coefficient poly))))
-> Unipol (Coefficient poly)
forall poly.
IsOrderedPolynomial poly =>
(Coefficient poly, OrderedMonomial (MOrder poly) (Arity poly))
-> poly
toPolynomial (Coefficient poly
Coefficient (Unipol (Coefficient poly))
v, Sized Vector 1 Int -> OrderedMonomial Grevlex 1
forall k (ordering :: k) (n :: Nat).
Monomial n -> OrderedMonomial ordering n
OrderedMonomial (Sized Vector 1 Int -> OrderedMonomial Grevlex 1)
-> Sized Vector 1 Int -> OrderedMonomial Grevlex 1
forall a b. (a -> b) -> a -> b
$ Int -> Sized Vector 1 Int
forall (f :: * -> *) a. (CPointed f, Dom f a) => a -> Sized f 1 a
SV.singleton (Int
d Int -> Int -> Int
forall r. Group r => r -> r -> r
- OrderedMonomial (MOrder poly) (Arity poly) -> Int
forall k (ord :: k) (n :: Nat). OrderedMonomial ord n -> Int
totalDegree OrderedMonomial (MOrder poly) (Arity poly)
k))) (Map
   (OrderedMonomial (MOrder poly) (Arity poly)) (Coefficient poly)
 -> Map
      (OrderedMonomial (MOrder poly) (Arity poly))
      (Unipol (Coefficient poly)))
-> Map
     (OrderedMonomial (MOrder poly) (Arity poly)) (Coefficient poly)
-> Map
     (OrderedMonomial (MOrder poly) (Arity poly))
     (Unipol (Coefficient poly))
forall a b. (a -> b) -> a -> b
$
            poly
-> Map
     (OrderedMonomial (MOrder poly) (Arity poly)) (Coefficient poly)
forall poly.
IsOrderedPolynomial poly =>
poly
-> Map
     (OrderedMonomial (MOrder poly) (Arity poly)) (Coefficient poly)
terms poly
p

unhomogenise :: IsOrderedPolynomial poly => Homogenised poly -> poly
unhomogenise :: Homogenised poly -> poly
unhomogenise (Homogenised OrderedPolynomial
  (Unipol (Coefficient poly)) (MOrder poly) (Arity poly)
f) =
  OrderedPolynomial (Coefficient poly) (MOrder poly) (Arity poly)
-> poly
forall poly poly'.
(IsOrderedPolynomial poly, IsOrderedPolynomial poly',
 Coefficient poly ~ Coefficient poly', MOrder poly ~ MOrder poly',
 Arity poly ~ Arity poly') =>
poly -> poly'
convertPolynomial (OrderedPolynomial (Coefficient poly) (MOrder poly) (Arity poly)
 -> poly)
-> OrderedPolynomial (Coefficient poly) (MOrder poly) (Arity poly)
-> poly
forall a b. (a -> b) -> a -> b
$
    (Unipol (Coefficient poly) -> Coefficient poly)
-> OrderedPolynomial
     (Unipol (Coefficient poly)) (MOrder poly) (Arity poly)
-> OrderedPolynomial (Coefficient poly) (MOrder poly) (Arity poly)
forall (n :: Nat) b ord a.
(KnownNat n, CoeffRing b, IsMonomialOrder n ord) =>
(a -> b) -> OrderedPolynomial a ord n -> OrderedPolynomial b ord n
mapCoeff ((Coefficient (Unipol (Coefficient poly))
 -> Coefficient poly -> Coefficient poly)
-> Sized (Arity (Unipol (Coefficient poly))) (Coefficient poly)
-> Unipol (Coefficient poly)
-> Coefficient poly
forall poly m.
(IsPolynomial poly, Ring m) =>
(Coefficient poly -> m -> m) -> Sized (Arity poly) m -> poly -> m
substWith Coefficient (Unipol (Coefficient poly))
-> Coefficient poly -> Coefficient poly
forall r. Multiplicative r => r -> r -> r
(*) (Coefficient poly -> Sized Vector 1 (Coefficient poly)
forall (f :: * -> *) a. (CPointed f, Dom f a) => a -> Sized f 1 a
SV.singleton Coefficient poly
forall r. Unital r => r
one)) OrderedPolynomial
  (Unipol (Coefficient poly)) (MOrder poly) (Arity poly)
f

isHomogeneous ::
  IsOrderedPolynomial poly =>
  poly ->
  Bool
isHomogeneous :: poly -> Bool
isHomogeneous poly
poly =
  let degs :: [Int]
degs = (Monomial (Arity poly) -> Int) -> [Monomial (Arity poly)] -> [Int]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
map Monomial (Arity poly) -> Int
forall mono.
(MonoFoldable mono, Num (Element mono)) =>
mono -> Element mono
osum ([Monomial (Arity poly)] -> [Int])
-> [Monomial (Arity poly)] -> [Int]
forall a b. (a -> b) -> a -> b
$ HashSet (Monomial (Arity poly)) -> [Monomial (Arity poly)]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList (HashSet (Monomial (Arity poly)) -> [Monomial (Arity poly)])
-> HashSet (Monomial (Arity poly)) -> [Monomial (Arity poly)]
forall a b. (a -> b) -> a -> b
$ poly -> HashSet (Monomial (Arity poly))
forall poly.
IsPolynomial poly =>
poly -> HashSet (Monomial (Arity poly))
monomials poly
poly
   in [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and ([Bool] -> Bool) -> [Bool] -> Bool
forall a b. (a -> b) -> a -> b
$ (Int -> Int -> Bool) -> [Int] -> [Int] -> [Bool]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
(==) [Int]
degs ([Int] -> [Int]
forall a. [a] -> [a]
tail [Int]
degs)

tryHomogenise :: IsOrderedPolynomial poly => poly -> Either poly (Homogenised poly)
tryHomogenise :: poly -> Either poly (Homogenised poly)
tryHomogenise poly
f
  | poly -> Bool
forall poly. IsOrderedPolynomial poly => poly -> Bool
isHomogeneous poly
f = poly -> Either poly (Homogenised poly)
forall a b. a -> Either a b
Left poly
f
  | Bool
otherwise = Homogenised poly -> Either poly (Homogenised poly)
forall a b. b -> Either a b
Right (Homogenised poly -> Either poly (Homogenised poly))
-> Homogenised poly -> Either poly (Homogenised poly)
forall a b. (a -> b) -> a -> b
$ poly -> Homogenised poly
forall poly. IsOrderedPolynomial poly => poly -> Homogenised poly
homogenise poly
f