-- | Multivariate polynomials where the variable set 
-- looks like @{x_1, x_2, ... , x_N}@ 

{-# LANGUAGE 
      BangPatterns, TypeFamilies, DataKinds, KindSignatures, ScopedTypeVariables,
      FlexibleContexts, StandaloneDeriving
  #-}
module Math.Algebra.Polynomial.Multivariate.Indexed
  (
    Poly(..) , unPoly , polyVar , nOfPoly , renamePolyVar
  , ZPoly , QPoly , fromZPoly, fromQPoly
  , embed
  , XS(..)
  )
  where

--------------------------------------------------------------------------------

import Data.Maybe
import Data.List
import Data.Array.Unboxed 

import Data.Typeable
import GHC.TypeLits
import Data.Proxy
import Unsafe.Coerce as Unsafe

import Data.Foldable as F 

import qualified Math.Algebra.Polynomial.FreeModule as ZMod
import Math.Algebra.Polynomial.FreeModule ( FreeMod , FreeModule(..) ) -- , ZMod , QMod )

import Math.Algebra.Polynomial.Monomial.Indexed 

import Math.Algebra.Polynomial.Class
import Math.Algebra.Polynomial.Pretty
import Math.Algebra.Polynomial.Misc

--------------------------------------------------------------------------------
-- * Polynomials

-- | A multivariate polynomial in with a given coefficient ring. 
--
-- It is also indexed by the (shared) /name/ of the variables and the /number of/
-- variable. For example @Polyn Rational "x" 3@ the type of polynomials in the
-- variables @x1, x2, x3@ with rational coefficients.
newtype Poly (coeff :: *) (var :: Symbol) (n :: Nat) 
  = Poly (FreeMod coeff (XS var n))
  deriving (Poly coeff var n -> Poly coeff var n -> Bool
(Poly coeff var n -> Poly coeff var n -> Bool)
-> (Poly coeff var n -> Poly coeff var n -> Bool)
-> Eq (Poly coeff var n)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall coeff (var :: Symbol) (n :: Nat).
Eq coeff =>
Poly coeff var n -> Poly coeff var n -> Bool
/= :: Poly coeff var n -> Poly coeff var n -> Bool
$c/= :: forall coeff (var :: Symbol) (n :: Nat).
Eq coeff =>
Poly coeff var n -> Poly coeff var n -> Bool
== :: Poly coeff var n -> Poly coeff var n -> Bool
$c== :: forall coeff (var :: Symbol) (n :: Nat).
Eq coeff =>
Poly coeff var n -> Poly coeff var n -> Bool
Eq,Eq (Poly coeff var n)
Eq (Poly coeff var n)
-> (Poly coeff var n -> Poly coeff var n -> Ordering)
-> (Poly coeff var n -> Poly coeff var n -> Bool)
-> (Poly coeff var n -> Poly coeff var n -> Bool)
-> (Poly coeff var n -> Poly coeff var n -> Bool)
-> (Poly coeff var n -> Poly coeff var n -> Bool)
-> (Poly coeff var n -> Poly coeff var n -> Poly coeff var n)
-> (Poly coeff var n -> Poly coeff var n -> Poly coeff var n)
-> Ord (Poly coeff var n)
Poly coeff var n -> Poly coeff var n -> Bool
Poly coeff var n -> Poly coeff var n -> Ordering
Poly coeff var n -> Poly coeff var n -> Poly coeff var n
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 coeff (var :: Symbol) (n :: Nat).
Ord coeff =>
Eq (Poly coeff var n)
forall coeff (var :: Symbol) (n :: Nat).
Ord coeff =>
Poly coeff var n -> Poly coeff var n -> Bool
forall coeff (var :: Symbol) (n :: Nat).
Ord coeff =>
Poly coeff var n -> Poly coeff var n -> Ordering
forall coeff (var :: Symbol) (n :: Nat).
Ord coeff =>
Poly coeff var n -> Poly coeff var n -> Poly coeff var n
min :: Poly coeff var n -> Poly coeff var n -> Poly coeff var n
$cmin :: forall coeff (var :: Symbol) (n :: Nat).
Ord coeff =>
Poly coeff var n -> Poly coeff var n -> Poly coeff var n
max :: Poly coeff var n -> Poly coeff var n -> Poly coeff var n
$cmax :: forall coeff (var :: Symbol) (n :: Nat).
Ord coeff =>
Poly coeff var n -> Poly coeff var n -> Poly coeff var n
>= :: Poly coeff var n -> Poly coeff var n -> Bool
$c>= :: forall coeff (var :: Symbol) (n :: Nat).
Ord coeff =>
Poly coeff var n -> Poly coeff var n -> Bool
> :: Poly coeff var n -> Poly coeff var n -> Bool
$c> :: forall coeff (var :: Symbol) (n :: Nat).
Ord coeff =>
Poly coeff var n -> Poly coeff var n -> Bool
<= :: Poly coeff var n -> Poly coeff var n -> Bool
$c<= :: forall coeff (var :: Symbol) (n :: Nat).
Ord coeff =>
Poly coeff var n -> Poly coeff var n -> Bool
< :: Poly coeff var n -> Poly coeff var n -> Bool
$c< :: forall coeff (var :: Symbol) (n :: Nat).
Ord coeff =>
Poly coeff var n -> Poly coeff var n -> Bool
compare :: Poly coeff var n -> Poly coeff var n -> Ordering
$ccompare :: forall coeff (var :: Symbol) (n :: Nat).
Ord coeff =>
Poly coeff var n -> Poly coeff var n -> Ordering
$cp1Ord :: forall coeff (var :: Symbol) (n :: Nat).
Ord coeff =>
Eq (Poly coeff var n)
Ord,Int -> Poly coeff var n -> ShowS
[Poly coeff var n] -> ShowS
Poly coeff var n -> String
(Int -> Poly coeff var n -> ShowS)
-> (Poly coeff var n -> String)
-> ([Poly coeff var n] -> ShowS)
-> Show (Poly coeff var n)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall coeff (var :: Symbol) (n :: Nat).
Show coeff =>
Int -> Poly coeff var n -> ShowS
forall coeff (var :: Symbol) (n :: Nat).
Show coeff =>
[Poly coeff var n] -> ShowS
forall coeff (var :: Symbol) (n :: Nat).
Show coeff =>
Poly coeff var n -> String
showList :: [Poly coeff var n] -> ShowS
$cshowList :: forall coeff (var :: Symbol) (n :: Nat).
Show coeff =>
[Poly coeff var n] -> ShowS
show :: Poly coeff var n -> String
$cshow :: forall coeff (var :: Symbol) (n :: Nat).
Show coeff =>
Poly coeff var n -> String
showsPrec :: Int -> Poly coeff var n -> ShowS
$cshowsPrec :: forall coeff (var :: Symbol) (n :: Nat).
Show coeff =>
Int -> Poly coeff var n -> ShowS
Show,Typeable)

-- deriving instance (Ord coeff) => Ord (Poly coeff var n)

unPoly :: Poly c v n -> FreeMod c (XS v n) 
unPoly :: Poly c v n -> FreeMod c (XS v n)
unPoly (Poly FreeMod c (XS v n)
p) = FreeMod c (XS v n)
p

-- | Name of the variables
polyVar :: KnownSymbol var => Poly c var n -> String
polyVar :: Poly c var n -> String
polyVar = Proxy var -> String
forall (n :: Symbol) (proxy :: Symbol -> *).
KnownSymbol n =>
proxy n -> String
symbolVal (Proxy var -> String)
-> (Poly c var n -> Proxy var) -> Poly c var n -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Poly c var n -> Proxy var
forall c (var :: Symbol) (n :: Nat). Poly c var n -> Proxy var
varProxy where
  varProxy :: Poly c var n -> Proxy var
  varProxy :: Poly c var n -> Proxy var
varProxy Poly c var n
_ = Proxy var
forall k (t :: k). Proxy t
Proxy

-- | Number of variables
nOfPoly :: KnownNat n => Poly c var n -> Int
nOfPoly :: Poly c var n -> Int
nOfPoly = Integer -> Int
forall a. Num a => Integer -> a
fromInteger (Integer -> Int)
-> (Poly c var n -> Integer) -> Poly c var n -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Proxy n -> Integer
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
natVal (Proxy n -> Integer)
-> (Poly c var n -> Proxy n) -> Poly c var n -> Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Poly c var n -> Proxy n
forall c (var :: Symbol) (n :: Nat). Poly c var n -> Proxy n
natProxy where
  natProxy :: Poly c var n -> Proxy n
  natProxy :: Poly c var n -> Proxy n
natProxy Poly c var n
_ = Proxy n
forall k (t :: k). Proxy t
Proxy

instance FreeModule (Poly c v n) where
  type BaseF  (Poly c v n) = XS v n
  type CoeffF (Poly c v n) = c
  toFreeModule :: Poly c v n -> FreeMod (CoeffF (Poly c v n)) (BaseF (Poly c v n))
toFreeModule   = Poly c v n -> FreeMod (CoeffF (Poly c v n)) (BaseF (Poly c v n))
forall c (v :: Symbol) (n :: Nat). Poly c v n -> FreeMod c (XS v n)
unPoly
  fromFreeModule :: FreeMod (CoeffF (Poly c v n)) (BaseF (Poly c v n)) -> Poly c v n
fromFreeModule = FreeMod (CoeffF (Poly c v n)) (BaseF (Poly c v n)) -> Poly c v n
forall coeff (var :: Symbol) (n :: Nat).
FreeMod coeff (XS var n) -> Poly coeff var n
Poly

renamePolyVar :: Poly c var1 n -> Poly c var2 n
renamePolyVar :: Poly c var1 n -> Poly c var2 n
renamePolyVar = Poly c var1 n -> Poly c var2 n
forall a b. a -> b
Unsafe.unsafeCoerce

--------------------------------------------------------------------------------

type ZPoly = Poly Integer
type QPoly = Poly Rational

-- | Change the coefficient ring (from integers)
fromZPoly :: (Ring c, KnownSymbol v, KnownNat n) => Poly Integer v n -> Poly c v n
fromZPoly :: Poly Integer v n -> Poly c v n
fromZPoly= FreeMod c (XS v n) -> Poly c v n
forall coeff (var :: Symbol) (n :: Nat).
FreeMod coeff (XS var n) -> Poly coeff var n
Poly (FreeMod c (XS v n) -> Poly c v n)
-> (Poly Integer v n -> FreeMod c (XS v n))
-> Poly Integer v n
-> Poly c v n
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ZMod (XS v n) -> FreeMod c (XS v n)
forall c b.
(Num c, Typeable c, Eq c, Num c, Ord b, Typeable b) =>
ZMod b -> FreeMod c b
ZMod.fromZMod (ZMod (XS v n) -> FreeMod c (XS v n))
-> (Poly Integer v n -> ZMod (XS v n))
-> Poly Integer v n
-> FreeMod c (XS v n)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Poly Integer v n -> ZMod (XS v n)
forall c (v :: Symbol) (n :: Nat). Poly c v n -> FreeMod c (XS v n)
unPoly

-- | Change the coefficient field (from rationals)
fromQPoly :: (Field c, KnownSymbol v, KnownNat n) => Poly Rational v n -> Poly c v n
fromQPoly :: Poly Rational v n -> Poly c v n
fromQPoly = FreeMod c (XS v n) -> Poly c v n
forall coeff (var :: Symbol) (n :: Nat).
FreeMod coeff (XS var n) -> Poly coeff var n
Poly (FreeMod c (XS v n) -> Poly c v n)
-> (Poly Rational v n -> FreeMod c (XS v n))
-> Poly Rational v n
-> Poly c v n
forall b c a. (b -> c) -> (a -> b) -> a -> c
. QMod (XS v n) -> FreeMod c (XS v n)
forall c b.
(Fractional c, Typeable c, Eq c, Num c, Ord b, Typeable b) =>
QMod b -> FreeMod c b
ZMod.fromQMod (QMod (XS v n) -> FreeMod c (XS v n))
-> (Poly Rational v n -> QMod (XS v n))
-> Poly Rational v n
-> FreeMod c (XS v n)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Poly Rational v n -> QMod (XS v n)
forall c (v :: Symbol) (n :: Nat). Poly c v n -> FreeMod c (XS v n)
unPoly

--------------------------------------------------------------------------------

instance (Ring c, KnownSymbol v, KnownNat n) => AlmostPolynomial (Poly c v n) where
  type CoeffP (Poly c v n) = c
  type MonomP (Poly c v n) = XS v n
  type VarP   (Poly c v n) = Index

  zeroP :: Poly c v n
zeroP         = FreeMod c (XS v n) -> Poly c v n
forall coeff (var :: Symbol) (n :: Nat).
FreeMod coeff (XS var n) -> Poly coeff var n
Poly FreeMod c (XS v n)
forall c b. FreeMod c b
ZMod.zero
  isZeroP :: Poly c v n -> Bool
isZeroP       = FreeMod c (XS v n) -> Bool
forall b c. Ord b => FreeMod c b -> Bool
ZMod.isZero (FreeMod c (XS v n) -> Bool)
-> (Poly c v n -> FreeMod c (XS v n)) -> Poly c v n -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Poly c v n -> FreeMod c (XS v n)
forall c (v :: Symbol) (n :: Nat). Poly c v n -> FreeMod c (XS v n)
unPoly
  oneP :: Poly c v n
oneP          = FreeMod c (XS v n) -> Poly c v n
forall coeff (var :: Symbol) (n :: Nat).
FreeMod coeff (XS var n) -> Poly coeff var n
Poly (XS v n -> FreeMod c (XS v n)
forall c b. Num c => b -> FreeMod c b
ZMod.generator XS v n
forall (n :: Nat) (v :: Symbol). KnownNat n => XS v n
emptyXS)

  fromListP :: [(MonomP (Poly c v n), CoeffP (Poly c v n))] -> Poly c v n
fromListP     = FreeMod c (XS v n) -> Poly c v n
forall coeff (var :: Symbol) (n :: Nat).
FreeMod coeff (XS var n) -> Poly coeff var n
Poly (FreeMod c (XS v n) -> Poly c v n)
-> ([(XS v n, c)] -> FreeMod c (XS v n))
-> [(XS v n, c)]
-> Poly c v n
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(XS v n, c)] -> FreeMod c (XS v n)
forall c b. (Eq c, Num c, Ord b) => [(b, c)] -> FreeMod c b
ZMod.fromList
  toListP :: Poly c v n -> [(MonomP (Poly c v n), CoeffP (Poly c v n))]
toListP       = FreeMod c (XS v n) -> [(XS v n, c)]
forall c b. FreeMod c b -> [(b, c)]
ZMod.toList (FreeMod c (XS v n) -> [(XS v n, c)])
-> (Poly c v n -> FreeMod c (XS v n))
-> Poly c v n
-> [(XS v n, c)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Poly c v n -> FreeMod c (XS v n)
forall c (v :: Symbol) (n :: Nat). Poly c v n -> FreeMod c (XS v n)
unPoly

  variableP :: VarP (Poly c v n) -> Poly c v n
variableP     = FreeMod c (XS v n) -> Poly c v n
forall coeff (var :: Symbol) (n :: Nat).
FreeMod coeff (XS var n) -> Poly coeff var n
Poly (FreeMod c (XS v n) -> Poly c v n)
-> (Index -> FreeMod c (XS v n)) -> Index -> Poly c v n
forall b c a. (b -> c) -> (a -> b) -> a -> c
. XS v n -> FreeMod c (XS v n)
forall c b. Num c => b -> FreeMod c b
ZMod.generator (XS v n -> FreeMod c (XS v n))
-> (Index -> XS v n) -> Index -> FreeMod c (XS v n)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Index -> XS v n
forall (n :: Nat) (v :: Symbol). KnownNat n => Index -> XS v n
variableXS
  singletonP :: VarP (Poly c v n) -> Int -> Poly c v n
singletonP    = \VarP (Poly c v n)
v Int
e -> FreeMod c (XS v n) -> Poly c v n
forall coeff (var :: Symbol) (n :: Nat).
FreeMod coeff (XS var n) -> Poly coeff var n
Poly (XS v n -> FreeMod c (XS v n)
forall c b. Num c => b -> FreeMod c b
ZMod.generator (Index -> Int -> XS v n
forall (n :: Nat) (v :: Symbol).
KnownNat n =>
Index -> Int -> XS v n
singletonXS VarP (Poly c v n)
Index
v Int
e))
  monomP :: MonomP (Poly c v n) -> Poly c v n
monomP        = \MonomP (Poly c v n)
m     -> FreeMod c (XS v n) -> Poly c v n
forall coeff (var :: Symbol) (n :: Nat).
FreeMod coeff (XS var n) -> Poly coeff var n
Poly (FreeMod c (XS v n) -> Poly c v n)
-> FreeMod c (XS v n) -> Poly c v n
forall a b. (a -> b) -> a -> b
$ XS v n -> FreeMod c (XS v n)
forall c b. Num c => b -> FreeMod c b
ZMod.generator MonomP (Poly c v n)
XS v n
m
  monomP' :: MonomP (Poly c v n) -> CoeffP (Poly c v n) -> Poly c v n
monomP'       = \MonomP (Poly c v n)
m CoeffP (Poly c v n)
c   -> FreeMod c (XS v n) -> Poly c v n
forall coeff (var :: Symbol) (n :: Nat).
FreeMod coeff (XS var n) -> Poly coeff var n
Poly (FreeMod c (XS v n) -> Poly c v n)
-> FreeMod c (XS v n) -> Poly c v n
forall a b. (a -> b) -> a -> b
$ XS v n -> c -> FreeMod c (XS v n)
forall b c. (Ord b, Num c, Eq c) => b -> c -> FreeMod c b
ZMod.singleton MonomP (Poly c v n)
XS v n
m c
CoeffP (Poly c v n)
c
  scalarP :: CoeffP (Poly c v n) -> Poly c v n
scalarP       = \CoeffP (Poly c v n)
s     -> FreeMod c (XS v n) -> Poly c v n
forall coeff (var :: Symbol) (n :: Nat).
FreeMod coeff (XS var n) -> Poly coeff var n
Poly (FreeMod c (XS v n) -> Poly c v n)
-> FreeMod c (XS v n) -> Poly c v n
forall a b. (a -> b) -> a -> b
$ XS v n -> c -> FreeMod c (XS v n)
forall b c. (Ord b, Num c, Eq c) => b -> c -> FreeMod c b
ZMod.singleton XS v n
forall (n :: Nat) (v :: Symbol). KnownNat n => XS v n
emptyXS c
CoeffP (Poly c v n)
s

  addP :: Poly c v n -> Poly c v n -> Poly c v n
addP          = \Poly c v n
p1 Poly c v n
p2 -> FreeMod c (XS v n) -> Poly c v n
forall coeff (var :: Symbol) (n :: Nat).
FreeMod coeff (XS var n) -> Poly coeff var n
Poly (FreeMod c (XS v n) -> Poly c v n)
-> FreeMod c (XS v n) -> Poly c v n
forall a b. (a -> b) -> a -> b
$ FreeMod c (XS v n) -> FreeMod c (XS v n) -> FreeMod c (XS v n)
forall b c.
(Ord b, Eq c, Num c) =>
FreeMod c b -> FreeMod c b -> FreeMod c b
ZMod.add (Poly c v n -> FreeMod c (XS v n)
forall c (v :: Symbol) (n :: Nat). Poly c v n -> FreeMod c (XS v n)
unPoly Poly c v n
p1) (Poly c v n -> FreeMod c (XS v n)
forall c (v :: Symbol) (n :: Nat). Poly c v n -> FreeMod c (XS v n)
unPoly Poly c v n
p2)
  subP :: Poly c v n -> Poly c v n -> Poly c v n
subP          = \Poly c v n
p1 Poly c v n
p2 -> FreeMod c (XS v n) -> Poly c v n
forall coeff (var :: Symbol) (n :: Nat).
FreeMod coeff (XS var n) -> Poly coeff var n
Poly (FreeMod c (XS v n) -> Poly c v n)
-> FreeMod c (XS v n) -> Poly c v n
forall a b. (a -> b) -> a -> b
$ FreeMod c (XS v n) -> FreeMod c (XS v n) -> FreeMod c (XS v n)
forall b c.
(Ord b, Eq c, Num c) =>
FreeMod c b -> FreeMod c b -> FreeMod c b
ZMod.sub (Poly c v n -> FreeMod c (XS v n)
forall c (v :: Symbol) (n :: Nat). Poly c v n -> FreeMod c (XS v n)
unPoly Poly c v n
p1) (Poly c v n -> FreeMod c (XS v n)
forall c (v :: Symbol) (n :: Nat). Poly c v n -> FreeMod c (XS v n)
unPoly Poly c v n
p2)
  negP :: Poly c v n -> Poly c v n
negP          = FreeMod c (XS v n) -> Poly c v n
forall coeff (var :: Symbol) (n :: Nat).
FreeMod coeff (XS var n) -> Poly coeff var n
Poly (FreeMod c (XS v n) -> Poly c v n)
-> (Poly c v n -> FreeMod c (XS v n)) -> Poly c v n -> Poly c v n
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FreeMod c (XS v n) -> FreeMod c (XS v n)
forall c b. Num c => FreeMod c b -> FreeMod c b
ZMod.neg (FreeMod c (XS v n) -> FreeMod c (XS v n))
-> (Poly c v n -> FreeMod c (XS v n))
-> Poly c v n
-> FreeMod c (XS v n)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Poly c v n -> FreeMod c (XS v n)
forall c (v :: Symbol) (n :: Nat). Poly c v n -> FreeMod c (XS v n)
unPoly
  mulP :: Poly c v n -> Poly c v n -> Poly c v n
mulP          = \Poly c v n
p1 Poly c v n
p2 -> FreeMod c (XS v n) -> Poly c v n
forall coeff (var :: Symbol) (n :: Nat).
FreeMod coeff (XS var n) -> Poly coeff var n
Poly (FreeMod c (XS v n) -> Poly c v n)
-> FreeMod c (XS v n) -> Poly c v n
forall a b. (a -> b) -> a -> b
$ (XS v n -> XS v n -> XS v n)
-> FreeMod c (XS v n) -> FreeMod c (XS v n) -> FreeMod c (XS v n)
forall b c.
(Ord b, Eq c, Num c) =>
(b -> b -> b) -> FreeMod c b -> FreeMod c b -> FreeMod c b
ZMod.mulWith XS v n -> XS v n -> XS v n
forall (n :: Nat) (v :: Symbol).
KnownNat n =>
XS v n -> XS v n -> XS v n
mulXS (Poly c v n -> FreeMod c (XS v n)
forall c (v :: Symbol) (n :: Nat). Poly c v n -> FreeMod c (XS v n)
unPoly Poly c v n
p1) (Poly c v n -> FreeMod c (XS v n)
forall c (v :: Symbol) (n :: Nat). Poly c v n -> FreeMod c (XS v n)
unPoly Poly c v n
p2)

  coeffOfP :: MonomP (Poly c v n) -> Poly c v n -> CoeffP (Poly c v n)
coeffOfP      = \MonomP (Poly c v n)
m Poly c v n
p   -> XS v n -> FreeMod c (XS v n) -> c
forall b c. (Ord b, Num c) => b -> FreeMod c b -> c
ZMod.coeffOf MonomP (Poly c v n)
XS v n
m (Poly c v n -> FreeMod c (XS v n)
forall c (v :: Symbol) (n :: Nat). Poly c v n -> FreeMod c (XS v n)
unPoly Poly c v n
p)
  productP :: [Poly c v n] -> Poly c v n
productP      = \[Poly c v n]
ps    -> FreeMod c (XS v n) -> Poly c v n
forall coeff (var :: Symbol) (n :: Nat).
FreeMod coeff (XS var n) -> Poly coeff var n
Poly (FreeMod c (XS v n) -> Poly c v n)
-> FreeMod c (XS v n) -> Poly c v n
forall a b. (a -> b) -> a -> b
$ XS v n
-> (XS v n -> XS v n -> XS v n)
-> [FreeMod c (XS v n)]
-> FreeMod c (XS v n)
forall b c.
(Ord b, Eq c, Num c) =>
b -> (b -> b -> b) -> [FreeMod c b] -> FreeMod c b
ZMod.productWith XS v n
forall (n :: Nat) (v :: Symbol). KnownNat n => XS v n
emptyXS XS v n -> XS v n -> XS v n
forall (n :: Nat) (v :: Symbol).
KnownNat n =>
XS v n -> XS v n -> XS v n
mulXS ([FreeMod c (XS v n)] -> FreeMod c (XS v n))
-> [FreeMod c (XS v n)] -> FreeMod c (XS v n)
forall a b. (a -> b) -> a -> b
$ (Poly c v n -> FreeMod c (XS v n))
-> [Poly c v n] -> [FreeMod c (XS v n)]
forall a b. (a -> b) -> [a] -> [b]
map Poly c v n -> FreeMod c (XS v n)
forall c (v :: Symbol) (n :: Nat). Poly c v n -> FreeMod c (XS v n)
unPoly [Poly c v n]
ps
  mulByMonomP :: MonomP (Poly c v n) -> Poly c v n -> Poly c v n
mulByMonomP   = \MonomP (Poly c v n)
m Poly c v n
p   -> FreeMod c (XS v n) -> Poly c v n
forall coeff (var :: Symbol) (n :: Nat).
FreeMod coeff (XS var n) -> Poly coeff var n
Poly (FreeMod c (XS v n) -> Poly c v n)
-> FreeMod c (XS v n) -> Poly c v n
forall a b. (a -> b) -> a -> b
$ XS v n -> FreeMod c (XS v n) -> FreeMod c (XS v n)
forall b c. (Ord b, Monoid b) => b -> FreeMod c b -> FreeMod c b
ZMod.unsafeMulByMonom MonomP (Poly c v n)
XS v n
m (Poly c v n -> FreeMod c (XS v n)
forall c (v :: Symbol) (n :: Nat). Poly c v n -> FreeMod c (XS v n)
unPoly Poly c v n
p)
  scaleP :: CoeffP (Poly c v n) -> Poly c v n -> Poly c v n
scaleP        = \CoeffP (Poly c v n)
s Poly c v n
p   -> FreeMod c (XS v n) -> Poly c v n
forall coeff (var :: Symbol) (n :: Nat).
FreeMod coeff (XS var n) -> Poly coeff var n
Poly (FreeMod c (XS v n) -> Poly c v n)
-> FreeMod c (XS v n) -> Poly c v n
forall a b. (a -> b) -> a -> b
$ c -> FreeMod c (XS v n) -> FreeMod c (XS v n)
forall b c. (Ord b, Eq c, Num c) => c -> FreeMod c b -> FreeMod c b
ZMod.scale c
CoeffP (Poly c v n)
s (Poly c v n -> FreeMod c (XS v n)
forall c (v :: Symbol) (n :: Nat). Poly c v n -> FreeMod c (XS v n)
unPoly Poly c v n
p) 

instance (Ring c, KnownSymbol v, KnownNat n) => Polynomial (Poly c v n) where
  evalP :: (CoeffP (Poly c v n) -> d)
-> (VarP (Poly c v n) -> d) -> Poly c v n -> d
evalP         = \CoeffP (Poly c v n) -> d
g VarP (Poly c v n) -> d
f Poly c v n
p -> let { !z :: XS v n -> d
z = (VarM (XS v n) -> d) -> XS v n -> d
forall m c. (Monomial m, Num c) => (VarM m -> c) -> m -> c
evalM VarP (Poly c v n) -> d
VarM (XS v n) -> d
f ; h :: (XS v n, c) -> d
h (!XS v n
m,!c
c) = CoeffP (Poly c v n) -> d
g c
CoeffP (Poly c v n)
c d -> d -> d
forall a. Num a => a -> a -> a
* XS v n -> d
z XS v n
m } in [d] -> d
forall a. Num a => [a] -> a
sum' ([d] -> d) -> [d] -> d
forall a b. (a -> b) -> a -> b
$ ((XS v n, c) -> d) -> [(XS v n, c)] -> [d]
forall a b. (a -> b) -> [a] -> [b]
map (XS v n, c) -> d
h ([(XS v n, c)] -> [d]) -> [(XS v n, c)] -> [d]
forall a b. (a -> b) -> a -> b
$ FreeMod c (XS v n) -> [(XS v n, c)]
forall c b. FreeMod c b -> [(b, c)]
ZMod.toList (FreeMod c (XS v n) -> [(XS v n, c)])
-> FreeMod c (XS v n) -> [(XS v n, c)]
forall a b. (a -> b) -> a -> b
$ Poly c v n -> FreeMod c (XS v n)
forall c (v :: Symbol) (n :: Nat). Poly c v n -> FreeMod c (XS v n)
unPoly Poly c v n
p
  varSubsP :: (VarP (Poly c v n) -> VarP (Poly c v n))
-> Poly c v n -> Poly c v n
varSubsP      = \VarP (Poly c v n) -> VarP (Poly c v n)
f Poly c v n
p   -> FreeMod c (XS v n) -> Poly c v n
forall coeff (var :: Symbol) (n :: Nat).
FreeMod coeff (XS var n) -> Poly coeff var n
Poly (FreeMod c (XS v n) -> Poly c v n)
-> FreeMod c (XS v n) -> Poly c v n
forall a b. (a -> b) -> a -> b
$ (XS v n -> XS v n) -> FreeMod c (XS v n) -> FreeMod c (XS v n)
forall a b c.
(Ord a, Ord b, Eq c, Num c) =>
(a -> b) -> FreeMod c a -> FreeMod c b
ZMod.mapBase ((Index -> Index) -> XS v n -> XS v n
forall (n :: Nat) (v :: Symbol).
KnownNat n =>
(Index -> Index) -> XS v n -> XS v n
varSubsXS VarP (Poly c v n) -> VarP (Poly c v n)
Index -> Index
f) (Poly c v n -> FreeMod c (XS v n)
forall c (v :: Symbol) (n :: Nat). Poly c v n -> FreeMod c (XS v n)
unPoly Poly c v n
p)
  coeffSubsP :: (VarP (Poly c v n) -> Maybe (CoeffP (Poly c v n)))
-> Poly c v n -> Poly c v n
coeffSubsP    = \VarP (Poly c v n) -> Maybe (CoeffP (Poly c v n))
f Poly c v n
p   -> FreeMod c (XS v n) -> Poly c v n
forall coeff (var :: Symbol) (n :: Nat).
FreeMod coeff (XS var n) -> Poly coeff var n
Poly (FreeMod c (XS v n) -> Poly c v n)
-> FreeMod c (XS v n) -> Poly c v n
forall a b. (a -> b) -> a -> b
$ [(XS v n, c)] -> FreeMod c (XS v n)
forall c b. (Eq c, Num c, Ord b) => [(b, c)] -> FreeMod c b
ZMod.fromList ([(XS v n, c)] -> FreeMod c (XS v n))
-> [(XS v n, c)] -> FreeMod c (XS v n)
forall a b. (a -> b) -> a -> b
$ ((XS v n, c) -> (XS v n, c)) -> [(XS v n, c)] -> [(XS v n, c)]
forall a b. (a -> b) -> [a] -> [b]
map ((Index -> Maybe c) -> (XS v n, c) -> (XS v n, c)
forall (n :: Nat) c (v :: Symbol).
(KnownNat n, Num c) =>
(Index -> Maybe c) -> (XS v n, c) -> (XS v n, c)
termSubsXS VarP (Poly c v n) -> Maybe (CoeffP (Poly c v n))
Index -> Maybe c
f) ([(XS v n, c)] -> [(XS v n, c)]) -> [(XS v n, c)] -> [(XS v n, c)]
forall a b. (a -> b) -> a -> b
$ FreeMod c (XS v n) -> [(XS v n, c)]
forall c b. FreeMod c b -> [(b, c)]
ZMod.toList (FreeMod c (XS v n) -> [(XS v n, c)])
-> FreeMod c (XS v n) -> [(XS v n, c)]
forall a b. (a -> b) -> a -> b
$ Poly c v n -> FreeMod c (XS v n)
forall c (v :: Symbol) (n :: Nat). Poly c v n -> FreeMod c (XS v n)
unPoly Poly c v n
p 
  subsP :: (VarP (Poly c v n) -> Poly c v n) -> Poly c v n -> Poly c v n
subsP         = \VarP (Poly c v n) -> Poly c v n
f Poly c v n
p   -> FreeMod c (XS v n) -> Poly c v n
forall coeff (var :: Symbol) (n :: Nat).
FreeMod coeff (XS var n) -> Poly coeff var n
Poly (FreeMod c (XS v n) -> Poly c v n)
-> FreeMod c (XS v n) -> Poly c v n
forall a b. (a -> b) -> a -> b
$ (XS v n -> FreeMod c (XS v n))
-> FreeMod c (XS v n) -> FreeMod c (XS v n)
forall b1 b2 c.
(Ord b1, Ord b2, Eq c, Num c) =>
(b1 -> FreeMod c b2) -> FreeMod c b1 -> FreeMod c b2
ZMod.flatMap ((Index -> FreeMod c (XS v n)) -> XS v n -> FreeMod c (XS v n)
forall c (v :: Symbol) (n :: Nat).
Num c =>
(Index -> c) -> XS v n -> c
evalXS (Poly c v n -> FreeMod c (XS v n)
forall c (v :: Symbol) (n :: Nat). Poly c v n -> FreeMod c (XS v n)
unPoly (Poly c v n -> FreeMod c (XS v n))
-> (Index -> Poly c v n) -> Index -> FreeMod c (XS v n)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. VarP (Poly c v n) -> Poly c v n
Index -> Poly c v n
f)) (Poly c v n -> FreeMod c (XS v n)
forall c (v :: Symbol) (n :: Nat). Poly c v n -> FreeMod c (XS v n)
unPoly Poly c v n
p)

instance (Ring c, KnownSymbol v, KnownNat n) => Num (Poly c v n) where
  fromInteger :: Integer -> Poly c v n
fromInteger = c -> Poly c v n
forall p. AlmostPolynomial p => CoeffP p -> p
scalarP (c -> Poly c v n) -> (Integer -> c) -> Integer -> Poly c v n
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> c
forall a. Num a => Integer -> a
fromInteger
  + :: Poly c v n -> Poly c v n -> Poly c v n
(+)    = Poly c v n -> Poly c v n -> Poly c v n
forall p. AlmostPolynomial p => p -> p -> p
addP
  (-)    = Poly c v n -> Poly c v n -> Poly c v n
forall p. AlmostPolynomial p => p -> p -> p
subP
  negate :: Poly c v n -> Poly c v n
negate = Poly c v n -> Poly c v n
forall p. AlmostPolynomial p => p -> p
negP
  * :: Poly c v n -> Poly c v n -> Poly c v n
(*)    = Poly c v n -> Poly c v n -> Poly c v n
forall p. AlmostPolynomial p => p -> p -> p
mulP
  abs :: Poly c v n -> Poly c v n
abs    = Poly c v n -> Poly c v n
forall a. a -> a
id
  signum :: Poly c v n -> Poly c v n
signum = \Poly c v n
_ -> CoeffP (Poly c v n) -> Poly c v n
forall p. AlmostPolynomial p => CoeffP p -> p
scalarP CoeffP (Poly c v n)
1

instance (Ring c, KnownSymbol v, KnownNat n, Pretty (XS v n)) => Pretty (Poly c v n) where
  pretty :: Poly c v n -> String
pretty poly :: Poly c v n
poly@(Poly FreeMod c (XS v n)
fm) = if Proxy c -> Bool
forall c. Ring c => Proxy c -> Bool
isSignedR (Poly c v n -> Proxy (CoeffP (Poly c v n))
forall p. AlmostPolynomial p => p -> Proxy (CoeffP p)
proxyCoeffP Poly c v n
poly)
    then Bool -> (XS v n -> String) -> FreeMod c (XS v n) -> String
forall c b.
(Num c, Eq c, IsSigned c, Pretty c) =>
Bool -> (b -> String) -> FreeMod c b -> String
prettyFreeMod'  Bool
True   XS v n -> String
forall a. Pretty a => a -> String
pretty FreeMod c (XS v n)
fm
    else (c -> String) -> (XS v n -> String) -> FreeMod c (XS v n) -> String
forall c b. (c -> String) -> (b -> String) -> FreeMod c b -> String
prettyFreeMod'' c -> String
forall a. Pretty a => a -> String
pretty XS v n -> String
forall a. Pretty a => a -> String
pretty FreeMod c (XS v n)
fm

-- hackety hack hack...
instance IsSigned (Poly c v n) where
  signOf :: Poly c v n -> Maybe Sign
signOf = Maybe Sign -> Poly c v n -> Maybe Sign
forall a b. a -> b -> a
const (Sign -> Maybe Sign
forall a. a -> Maybe a
Just Sign
Plus)

-- So that we can use it again as a coefficient ring
instance (Ring c, KnownSymbol v, KnownNat n) => Ring (Poly c v n) where
  isZeroR :: Poly c v n -> Bool
isZeroR   = FreeMod c (XS v n) -> Bool
forall b c. Ord b => FreeMod c b -> Bool
ZMod.isZero (FreeMod c (XS v n) -> Bool)
-> (Poly c v n -> FreeMod c (XS v n)) -> Poly c v n -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Poly c v n -> FreeMod c (XS v n)
forall c (v :: Symbol) (n :: Nat). Poly c v n -> FreeMod c (XS v n)
unPoly
  isAtomicR :: Proxy (Poly c v n) -> Bool
isAtomicR = Bool -> Proxy (Poly c v n) -> Bool
forall a b. a -> b -> a
const Bool
False
  isSignedR :: Proxy (Poly c v n) -> Bool
isSignedR = Bool -> Proxy (Poly c v n) -> Bool
forall a b. a -> b -> a
const Bool
False
  absR :: Poly c v n -> Poly c v n
absR      = Poly c v n -> Poly c v n
forall a. a -> a
id
  signumR :: Poly c v n -> Maybe Sign
signumR   = Maybe Sign -> Poly c v n -> Maybe Sign
forall a b. a -> b -> a
const (Sign -> Maybe Sign
forall a. a -> Maybe a
Just Sign
Plus)

--------------------------------------------------------------------------------

-- | You can always increase the number of variables; 
-- you can also decrease, if don't use the last few ones.
--
-- This will throw an error if you try to eliminate variables which are in fact used.
-- To do that, you can instead substitute 0 or 1 into them.
--
embed :: (Ring c, KnownNat n, KnownNat m) => Poly c v n -> Poly c v m
embed :: Poly c v n -> Poly c v m
embed old :: Poly c v n
old@(Poly FreeMod c (XS v n)
old_fm) = Poly c v m
new where
  n :: Int
n = Poly c v n -> Int
forall (n :: Nat) c (var :: Symbol).
KnownNat n =>
Poly c var n -> Int
nOfPoly Poly c v n
old
  m :: Int
m = Poly c v m -> Int
forall (n :: Nat) c (var :: Symbol).
KnownNat n =>
Poly c var n -> Int
nOfPoly Poly c v m
new
  new :: Poly c v m
new = FreeMod c (XS v m) -> Poly c v m
forall coeff (var :: Symbol) (n :: Nat).
FreeMod coeff (XS var n) -> Poly coeff var n
Poly (FreeMod c (XS v m) -> Poly c v m)
-> FreeMod c (XS v m) -> Poly c v m
forall a b. (a -> b) -> a -> b
$ case Int -> Int -> Ordering
forall a. Ord a => a -> a -> Ordering
compare Int
m Int
n of 
    Ordering
LT -> (XS v n -> XS v m) -> FreeMod c (XS v n) -> FreeMod c (XS v m)
forall a b c.
(Ord a, Ord b) =>
(a -> b) -> FreeMod c a -> FreeMod c b
ZMod.unsafeMapBase XS v n -> XS v m
project FreeMod c (XS v n)
old_fm
    Ordering
EQ -> (XS v n -> XS v m) -> FreeMod c (XS v n) -> FreeMod c (XS v m)
forall a b c.
(Ord a, Ord b) =>
(a -> b) -> FreeMod c a -> FreeMod c b
ZMod.unsafeMapBase XS v n -> XS v m
forall (var :: Symbol) (n :: Nat) (var :: Symbol) (n :: Nat).
XS var n -> XS var n
keep    FreeMod c (XS v n)
old_fm
    Ordering
GT -> (XS v n -> XS v m) -> FreeMod c (XS v n) -> FreeMod c (XS v m)
forall a b c.
(Ord a, Ord b) =>
(a -> b) -> FreeMod c a -> FreeMod c b
ZMod.unsafeMapBase XS v n -> XS v m
extend  FreeMod c (XS v n)
old_fm
  extend :: XS v n -> XS v m
extend  (XS UArray Int Int
arr) = UArray Int Int -> XS v m
forall (var :: Symbol) (n :: Nat). UArray Int Int -> XS var n
XS (UArray Int Int -> XS v m) -> UArray Int Int -> XS v m
forall a b. (a -> b) -> a -> b
$ (Int, Int) -> [Int] -> UArray Int Int
forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
(i, i) -> [e] -> a i e
listArray (Int
1,Int
m) (UArray Int Int -> [Int]
forall (a :: * -> * -> *) e i. (IArray a e, Ix i) => a i e -> [e]
elems UArray Int Int
arr [Int] -> [Int] -> [Int]
forall a. [a] -> [a] -> [a]
++ Int -> Int -> [Int]
forall a. Int -> a -> [a]
replicate (Int
mInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
n) Int
0)
  keep :: XS var n -> XS var n
keep    (XS UArray Int Int
arr) = UArray Int Int -> XS var n
forall (var :: Symbol) (n :: Nat). UArray Int Int -> XS var n
XS UArray Int Int
arr
  project :: XS v n -> XS v m
project (XS UArray Int Int
arr) = 
    let old :: [Int]
old = UArray Int Int -> [Int]
forall (a :: * -> * -> *) e i. (IArray a e, Ix i) => a i e -> [e]
elems UArray Int Int
arr
        ([Int]
new,[Int]
rest) = Int -> [Int] -> ([Int], [Int])
forall a. Int -> [a] -> ([a], [a])
splitAt Int
m [Int]
old
    in  if (Int -> Bool) -> [Int] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
==Int
0) [Int]
rest 
          then UArray Int Int -> XS v m
forall (var :: Symbol) (n :: Nat). UArray Int Int -> XS var n
XS (UArray Int Int -> XS v m) -> UArray Int Int -> XS v m
forall a b. (a -> b) -> a -> b
$ (Int, Int) -> [Int] -> UArray Int Int
forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
(i, i) -> [e] -> a i e
listArray (Int
1,Int
m) [Int]
new
          else String -> XS v m
forall a. HasCallStack => String -> a
error String
"Indexed/embed: the projected variables are actually used!"

--------------------------------------------------------------------------------