-- | Exterior algebra where the variable set 
-- looks like @{x_1, x_2, ... , x_N}@ 
--
-- See <https://en.wikipedia.org/wiki/Exterior_algebra>

{-# LANGUAGE 
      BangPatterns, TypeFamilies, DataKinds, KindSignatures, ScopedTypeVariables,
      FlexibleContexts, StandaloneDeriving
  #-}
module Math.Algebra.Polynomial.Exterior.Indexed
  (
    ExtAlg(..) , unExtAlg , polyVar , nOfExtAlg
  , ZExtAlg , QExtAlg
  , embed
  , Ext(..)
  )
  where

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

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

import Data.Typeable
import GHC.TypeLits
import Data.Proxy

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.Exterior.Indexed 

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

--------------------------------------------------------------------------------
-- * Exterior algebra

-- | An exterior 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 @ExtAlgn Rational "x" 3@ the type of polynomials in the
-- variables @x1, x2, x3@ with rational coefficients.
newtype ExtAlg (coeff :: *) (var :: Symbol) (n :: Nat) 
  = ExtAlg (FreeMod coeff (Ext var n))
  deriving (ExtAlg coeff var n -> ExtAlg coeff var n -> Bool
(ExtAlg coeff var n -> ExtAlg coeff var n -> Bool)
-> (ExtAlg coeff var n -> ExtAlg coeff var n -> Bool)
-> Eq (ExtAlg coeff var n)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall coeff (var :: Symbol) (n :: Nat).
Eq coeff =>
ExtAlg coeff var n -> ExtAlg coeff var n -> Bool
/= :: ExtAlg coeff var n -> ExtAlg coeff var n -> Bool
$c/= :: forall coeff (var :: Symbol) (n :: Nat).
Eq coeff =>
ExtAlg coeff var n -> ExtAlg coeff var n -> Bool
== :: ExtAlg coeff var n -> ExtAlg coeff var n -> Bool
$c== :: forall coeff (var :: Symbol) (n :: Nat).
Eq coeff =>
ExtAlg coeff var n -> ExtAlg coeff var n -> Bool
Eq,Eq (ExtAlg coeff var n)
Eq (ExtAlg coeff var n)
-> (ExtAlg coeff var n -> ExtAlg coeff var n -> Ordering)
-> (ExtAlg coeff var n -> ExtAlg coeff var n -> Bool)
-> (ExtAlg coeff var n -> ExtAlg coeff var n -> Bool)
-> (ExtAlg coeff var n -> ExtAlg coeff var n -> Bool)
-> (ExtAlg coeff var n -> ExtAlg coeff var n -> Bool)
-> (ExtAlg coeff var n -> ExtAlg coeff var n -> ExtAlg coeff var n)
-> (ExtAlg coeff var n -> ExtAlg coeff var n -> ExtAlg coeff var n)
-> Ord (ExtAlg coeff var n)
ExtAlg coeff var n -> ExtAlg coeff var n -> Bool
ExtAlg coeff var n -> ExtAlg coeff var n -> Ordering
ExtAlg coeff var n -> ExtAlg coeff var n -> ExtAlg 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 (ExtAlg coeff var n)
forall coeff (var :: Symbol) (n :: Nat).
Ord coeff =>
ExtAlg coeff var n -> ExtAlg coeff var n -> Bool
forall coeff (var :: Symbol) (n :: Nat).
Ord coeff =>
ExtAlg coeff var n -> ExtAlg coeff var n -> Ordering
forall coeff (var :: Symbol) (n :: Nat).
Ord coeff =>
ExtAlg coeff var n -> ExtAlg coeff var n -> ExtAlg coeff var n
min :: ExtAlg coeff var n -> ExtAlg coeff var n -> ExtAlg coeff var n
$cmin :: forall coeff (var :: Symbol) (n :: Nat).
Ord coeff =>
ExtAlg coeff var n -> ExtAlg coeff var n -> ExtAlg coeff var n
max :: ExtAlg coeff var n -> ExtAlg coeff var n -> ExtAlg coeff var n
$cmax :: forall coeff (var :: Symbol) (n :: Nat).
Ord coeff =>
ExtAlg coeff var n -> ExtAlg coeff var n -> ExtAlg coeff var n
>= :: ExtAlg coeff var n -> ExtAlg coeff var n -> Bool
$c>= :: forall coeff (var :: Symbol) (n :: Nat).
Ord coeff =>
ExtAlg coeff var n -> ExtAlg coeff var n -> Bool
> :: ExtAlg coeff var n -> ExtAlg coeff var n -> Bool
$c> :: forall coeff (var :: Symbol) (n :: Nat).
Ord coeff =>
ExtAlg coeff var n -> ExtAlg coeff var n -> Bool
<= :: ExtAlg coeff var n -> ExtAlg coeff var n -> Bool
$c<= :: forall coeff (var :: Symbol) (n :: Nat).
Ord coeff =>
ExtAlg coeff var n -> ExtAlg coeff var n -> Bool
< :: ExtAlg coeff var n -> ExtAlg coeff var n -> Bool
$c< :: forall coeff (var :: Symbol) (n :: Nat).
Ord coeff =>
ExtAlg coeff var n -> ExtAlg coeff var n -> Bool
compare :: ExtAlg coeff var n -> ExtAlg coeff var n -> Ordering
$ccompare :: forall coeff (var :: Symbol) (n :: Nat).
Ord coeff =>
ExtAlg coeff var n -> ExtAlg coeff var n -> Ordering
$cp1Ord :: forall coeff (var :: Symbol) (n :: Nat).
Ord coeff =>
Eq (ExtAlg coeff var n)
Ord,Int -> ExtAlg coeff var n -> ShowS
[ExtAlg coeff var n] -> ShowS
ExtAlg coeff var n -> String
(Int -> ExtAlg coeff var n -> ShowS)
-> (ExtAlg coeff var n -> String)
-> ([ExtAlg coeff var n] -> ShowS)
-> Show (ExtAlg coeff var n)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall coeff (var :: Symbol) (n :: Nat).
Show coeff =>
Int -> ExtAlg coeff var n -> ShowS
forall coeff (var :: Symbol) (n :: Nat).
Show coeff =>
[ExtAlg coeff var n] -> ShowS
forall coeff (var :: Symbol) (n :: Nat).
Show coeff =>
ExtAlg coeff var n -> String
showList :: [ExtAlg coeff var n] -> ShowS
$cshowList :: forall coeff (var :: Symbol) (n :: Nat).
Show coeff =>
[ExtAlg coeff var n] -> ShowS
show :: ExtAlg coeff var n -> String
$cshow :: forall coeff (var :: Symbol) (n :: Nat).
Show coeff =>
ExtAlg coeff var n -> String
showsPrec :: Int -> ExtAlg coeff var n -> ShowS
$cshowsPrec :: forall coeff (var :: Symbol) (n :: Nat).
Show coeff =>
Int -> ExtAlg coeff var n -> ShowS
Show,Typeable)

unExtAlg :: ExtAlg c v n -> FreeMod c (Ext v n) 
unExtAlg :: ExtAlg c v n -> FreeMod c (Ext v n)
unExtAlg (ExtAlg FreeMod c (Ext v n)
p) = FreeMod c (Ext v n)
p

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

-- | Number of variables
nOfExtAlg :: KnownNat n => ExtAlg c var n -> Int
nOfExtAlg :: ExtAlg c var n -> Int
nOfExtAlg = Integer -> Int
forall a. Num a => Integer -> a
fromInteger (Integer -> Int)
-> (ExtAlg c var n -> Integer) -> ExtAlg 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)
-> (ExtAlg c var n -> Proxy n) -> ExtAlg c var n -> Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ExtAlg c var n -> Proxy n
forall c (var :: Symbol) (n :: Nat). ExtAlg c var n -> Proxy n
natProxy where
  natProxy :: ExtAlg c var n -> Proxy n
  natProxy :: ExtAlg c var n -> Proxy n
natProxy ExtAlg c var n
_ = Proxy n
forall k (t :: k). Proxy t
Proxy

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

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

type ZExtAlg = ExtAlg Integer
type QExtAlg = ExtAlg Rational

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

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

  zeroP :: ExtAlg c v n
zeroP         = FreeMod c (Ext v n) -> ExtAlg c v n
forall coeff (var :: Symbol) (n :: Nat).
FreeMod coeff (Ext var n) -> ExtAlg coeff var n
ExtAlg FreeMod c (Ext v n)
forall c b. FreeMod c b
ZMod.zero
  isZeroP :: ExtAlg c v n -> Bool
isZeroP       = FreeMod c (Ext v n) -> Bool
forall b c. Ord b => FreeMod c b -> Bool
ZMod.isZero (FreeMod c (Ext v n) -> Bool)
-> (ExtAlg c v n -> FreeMod c (Ext v n)) -> ExtAlg c v n -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ExtAlg c v n -> FreeMod c (Ext v n)
forall c (v :: Symbol) (n :: Nat).
ExtAlg c v n -> FreeMod c (Ext v n)
unExtAlg
  oneP :: ExtAlg c v n
oneP          = FreeMod c (Ext v n) -> ExtAlg c v n
forall coeff (var :: Symbol) (n :: Nat).
FreeMod coeff (Ext var n) -> ExtAlg coeff var n
ExtAlg (Ext v n -> FreeMod c (Ext v n)
forall c b. Num c => b -> FreeMod c b
ZMod.generator Ext v n
forall (n :: Nat) (v :: Symbol). KnownNat n => Ext v n
emptyExt)

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

  variableP :: VarP (ExtAlg c v n) -> ExtAlg c v n
variableP     = FreeMod c (Ext v n) -> ExtAlg c v n
forall coeff (var :: Symbol) (n :: Nat).
FreeMod coeff (Ext var n) -> ExtAlg coeff var n
ExtAlg (FreeMod c (Ext v n) -> ExtAlg c v n)
-> (Index -> FreeMod c (Ext v n)) -> Index -> ExtAlg c v n
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Ext v n -> FreeMod c (Ext v n)
forall c b. Num c => b -> FreeMod c b
ZMod.generator (Ext v n -> FreeMod c (Ext v n))
-> (Index -> Ext v n) -> Index -> FreeMod c (Ext v n)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Index -> Ext v n
forall (n :: Nat) (v :: Symbol). KnownNat n => Index -> Ext v n
variableExt
  singletonP :: VarP (ExtAlg c v n) -> Int -> ExtAlg c v n
singletonP    = String -> Index -> Int -> ExtAlg c v n
forall a. HasCallStack => String -> a
error String
"ExtAlg/singletonP: not implemented (because it is meaningless)"
  monomP :: MonomP (ExtAlg c v n) -> ExtAlg c v n
monomP        = \MonomP (ExtAlg c v n)
m     -> FreeMod c (Ext v n) -> ExtAlg c v n
forall coeff (var :: Symbol) (n :: Nat).
FreeMod coeff (Ext var n) -> ExtAlg coeff var n
ExtAlg (FreeMod c (Ext v n) -> ExtAlg c v n)
-> FreeMod c (Ext v n) -> ExtAlg c v n
forall a b. (a -> b) -> a -> b
$ Ext v n -> FreeMod c (Ext v n)
forall c b. Num c => b -> FreeMod c b
ZMod.generator MonomP (ExtAlg c v n)
Ext v n
m
  monomP' :: MonomP (ExtAlg c v n) -> CoeffP (ExtAlg c v n) -> ExtAlg c v n
monomP'       = \MonomP (ExtAlg c v n)
m CoeffP (ExtAlg c v n)
c   -> FreeMod c (Ext v n) -> ExtAlg c v n
forall coeff (var :: Symbol) (n :: Nat).
FreeMod coeff (Ext var n) -> ExtAlg coeff var n
ExtAlg (FreeMod c (Ext v n) -> ExtAlg c v n)
-> FreeMod c (Ext v n) -> ExtAlg c v n
forall a b. (a -> b) -> a -> b
$ Ext v n -> c -> FreeMod c (Ext v n)
forall b c. (Ord b, Num c, Eq c) => b -> c -> FreeMod c b
ZMod.singleton MonomP (ExtAlg c v n)
Ext v n
m c
CoeffP (ExtAlg c v n)
c
  scalarP :: CoeffP (ExtAlg c v n) -> ExtAlg c v n
scalarP       = \CoeffP (ExtAlg c v n)
s     -> FreeMod c (Ext v n) -> ExtAlg c v n
forall coeff (var :: Symbol) (n :: Nat).
FreeMod coeff (Ext var n) -> ExtAlg coeff var n
ExtAlg (FreeMod c (Ext v n) -> ExtAlg c v n)
-> FreeMod c (Ext v n) -> ExtAlg c v n
forall a b. (a -> b) -> a -> b
$ Ext v n -> c -> FreeMod c (Ext v n)
forall b c. (Ord b, Num c, Eq c) => b -> c -> FreeMod c b
ZMod.singleton Ext v n
forall (n :: Nat) (v :: Symbol). KnownNat n => Ext v n
emptyExt c
CoeffP (ExtAlg c v n)
s

  addP :: ExtAlg c v n -> ExtAlg c v n -> ExtAlg c v n
addP          = \ExtAlg c v n
p1 ExtAlg c v n
p2 -> FreeMod c (Ext v n) -> ExtAlg c v n
forall coeff (var :: Symbol) (n :: Nat).
FreeMod coeff (Ext var n) -> ExtAlg coeff var n
ExtAlg (FreeMod c (Ext v n) -> ExtAlg c v n)
-> FreeMod c (Ext v n) -> ExtAlg c v n
forall a b. (a -> b) -> a -> b
$ FreeMod c (Ext v n) -> FreeMod c (Ext v n) -> FreeMod c (Ext v n)
forall b c.
(Ord b, Eq c, Num c) =>
FreeMod c b -> FreeMod c b -> FreeMod c b
ZMod.add (ExtAlg c v n -> FreeMod c (Ext v n)
forall c (v :: Symbol) (n :: Nat).
ExtAlg c v n -> FreeMod c (Ext v n)
unExtAlg ExtAlg c v n
p1) (ExtAlg c v n -> FreeMod c (Ext v n)
forall c (v :: Symbol) (n :: Nat).
ExtAlg c v n -> FreeMod c (Ext v n)
unExtAlg ExtAlg c v n
p2)
  subP :: ExtAlg c v n -> ExtAlg c v n -> ExtAlg c v n
subP          = \ExtAlg c v n
p1 ExtAlg c v n
p2 -> FreeMod c (Ext v n) -> ExtAlg c v n
forall coeff (var :: Symbol) (n :: Nat).
FreeMod coeff (Ext var n) -> ExtAlg coeff var n
ExtAlg (FreeMod c (Ext v n) -> ExtAlg c v n)
-> FreeMod c (Ext v n) -> ExtAlg c v n
forall a b. (a -> b) -> a -> b
$ FreeMod c (Ext v n) -> FreeMod c (Ext v n) -> FreeMod c (Ext v n)
forall b c.
(Ord b, Eq c, Num c) =>
FreeMod c b -> FreeMod c b -> FreeMod c b
ZMod.sub (ExtAlg c v n -> FreeMod c (Ext v n)
forall c (v :: Symbol) (n :: Nat).
ExtAlg c v n -> FreeMod c (Ext v n)
unExtAlg ExtAlg c v n
p1) (ExtAlg c v n -> FreeMod c (Ext v n)
forall c (v :: Symbol) (n :: Nat).
ExtAlg c v n -> FreeMod c (Ext v n)
unExtAlg ExtAlg c v n
p2)
  negP :: ExtAlg c v n -> ExtAlg c v n
negP          = FreeMod c (Ext v n) -> ExtAlg c v n
forall coeff (var :: Symbol) (n :: Nat).
FreeMod coeff (Ext var n) -> ExtAlg coeff var n
ExtAlg (FreeMod c (Ext v n) -> ExtAlg c v n)
-> (ExtAlg c v n -> FreeMod c (Ext v n))
-> ExtAlg c v n
-> ExtAlg c v n
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FreeMod c (Ext v n) -> FreeMod c (Ext v n)
forall c b. Num c => FreeMod c b -> FreeMod c b
ZMod.neg (FreeMod c (Ext v n) -> FreeMod c (Ext v n))
-> (ExtAlg c v n -> FreeMod c (Ext v n))
-> ExtAlg c v n
-> FreeMod c (Ext v n)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ExtAlg c v n -> FreeMod c (Ext v n)
forall c (v :: Symbol) (n :: Nat).
ExtAlg c v n -> FreeMod c (Ext v n)
unExtAlg
  mulP :: ExtAlg c v n -> ExtAlg c v n -> ExtAlg c v n
mulP          = \ExtAlg c v n
p1 ExtAlg c v n
p2 -> FreeMod c (Ext v n) -> ExtAlg c v n
forall coeff (var :: Symbol) (n :: Nat).
FreeMod coeff (Ext var n) -> ExtAlg coeff var n
ExtAlg (FreeMod c (Ext v n) -> ExtAlg c v n)
-> FreeMod c (Ext v n) -> ExtAlg c v n
forall a b. (a -> b) -> a -> b
$ (Ext v n -> Ext v n -> Maybe (Ext v n, c))
-> FreeMod c (Ext v n)
-> FreeMod c (Ext v n)
-> FreeMod c (Ext v n)
forall b c.
(Ord b, Eq c, Num c) =>
(b -> b -> Maybe (b, c))
-> FreeMod c b -> FreeMod c b -> FreeMod c b
ZMod.mulWith'' Ext v n -> Ext v n -> Maybe (Ext v n, c)
forall c (n :: Nat) (v :: Symbol).
(Num c, KnownNat n) =>
Ext v n -> Ext v n -> Maybe (Ext v n, c)
mulExtCoeff (ExtAlg c v n -> FreeMod c (Ext v n)
forall c (v :: Symbol) (n :: Nat).
ExtAlg c v n -> FreeMod c (Ext v n)
unExtAlg ExtAlg c v n
p1) (ExtAlg c v n -> FreeMod c (Ext v n)
forall c (v :: Symbol) (n :: Nat).
ExtAlg c v n -> FreeMod c (Ext v n)
unExtAlg ExtAlg c v n
p2)

  coeffOfP :: MonomP (ExtAlg c v n) -> ExtAlg c v n -> CoeffP (ExtAlg c v n)
coeffOfP      = \MonomP (ExtAlg c v n)
m ExtAlg c v n
p   -> Ext v n -> FreeMod c (Ext v n) -> c
forall b c. (Ord b, Num c) => b -> FreeMod c b -> c
ZMod.coeffOf MonomP (ExtAlg c v n)
Ext v n
m (ExtAlg c v n -> FreeMod c (Ext v n)
forall c (v :: Symbol) (n :: Nat).
ExtAlg c v n -> FreeMod c (Ext v n)
unExtAlg ExtAlg c v n
p)
  productP :: [ExtAlg c v n] -> ExtAlg c v n
productP      = \[ExtAlg c v n]
ps    -> FreeMod c (Ext v n) -> ExtAlg c v n
forall coeff (var :: Symbol) (n :: Nat).
FreeMod coeff (Ext var n) -> ExtAlg coeff var n
ExtAlg (FreeMod c (Ext v n) -> ExtAlg c v n)
-> FreeMod c (Ext v n) -> ExtAlg c v n
forall a b. (a -> b) -> a -> b
$ Ext v n
-> (Ext v n -> Ext v n -> Maybe (Ext v n, c))
-> [FreeMod c (Ext v n)]
-> FreeMod c (Ext v n)
forall b c.
(Ord b, Eq c, Num c) =>
b -> (b -> b -> Maybe (b, c)) -> [FreeMod c b] -> FreeMod c b
ZMod.productWith'' Ext v n
forall (n :: Nat) (v :: Symbol). KnownNat n => Ext v n
emptyExt Ext v n -> Ext v n -> Maybe (Ext v n, c)
forall c (n :: Nat) (v :: Symbol).
(Num c, KnownNat n) =>
Ext v n -> Ext v n -> Maybe (Ext v n, c)
mulExtCoeff ([FreeMod c (Ext v n)] -> FreeMod c (Ext v n))
-> [FreeMod c (Ext v n)] -> FreeMod c (Ext v n)
forall a b. (a -> b) -> a -> b
$ (ExtAlg c v n -> FreeMod c (Ext v n))
-> [ExtAlg c v n] -> [FreeMod c (Ext v n)]
forall a b. (a -> b) -> [a] -> [b]
map ExtAlg c v n -> FreeMod c (Ext v n)
forall c (v :: Symbol) (n :: Nat).
ExtAlg c v n -> FreeMod c (Ext v n)
unExtAlg [ExtAlg c v n]
ps
  mulByMonomP :: MonomP (ExtAlg c v n) -> ExtAlg c v n -> ExtAlg c v n
mulByMonomP   = \MonomP (ExtAlg c v n)
m ExtAlg c v n
p   -> FreeMod c (Ext v n) -> ExtAlg c v n
forall coeff (var :: Symbol) (n :: Nat).
FreeMod coeff (Ext var n) -> ExtAlg coeff var n
ExtAlg (FreeMod c (Ext v n) -> ExtAlg c v n)
-> FreeMod c (Ext v n) -> ExtAlg c v n
forall a b. (a -> b) -> a -> b
$ (Ext v n -> Maybe (Ext v n, c))
-> FreeMod c (Ext v n) -> FreeMod c (Ext v n)
forall a b c.
(Ord a, Ord b, Eq c, Num c) =>
(a -> Maybe (b, c)) -> FreeMod c a -> FreeMod c b
ZMod.mapMaybeBaseCoeff (Ext v n -> Ext v n -> Maybe (Ext v n, c)
forall c (n :: Nat) (v :: Symbol).
(Num c, KnownNat n) =>
Ext v n -> Ext v n -> Maybe (Ext v n, c)
mulExtCoeff MonomP (ExtAlg c v n)
Ext v n
m) (ExtAlg c v n -> FreeMod c (Ext v n)
forall c (v :: Symbol) (n :: Nat).
ExtAlg c v n -> FreeMod c (Ext v n)
unExtAlg ExtAlg c v n
p)    -- not injective!!!
  scaleP :: CoeffP (ExtAlg c v n) -> ExtAlg c v n -> ExtAlg c v n
scaleP        = \CoeffP (ExtAlg c v n)
s ExtAlg c v n
p   -> FreeMod c (Ext v n) -> ExtAlg c v n
forall coeff (var :: Symbol) (n :: Nat).
FreeMod coeff (Ext var n) -> ExtAlg coeff var n
ExtAlg (FreeMod c (Ext v n) -> ExtAlg c v n)
-> FreeMod c (Ext v n) -> ExtAlg c v n
forall a b. (a -> b) -> a -> b
$ c -> FreeMod c (Ext v n) -> FreeMod c (Ext v n)
forall b c. (Ord b, Eq c, Num c) => c -> FreeMod c b -> FreeMod c b
ZMod.scale c
CoeffP (ExtAlg c v n)
s (ExtAlg c v n -> FreeMod c (Ext v n)
forall c (v :: Symbol) (n :: Nat).
ExtAlg c v n -> FreeMod c (Ext v n)
unExtAlg ExtAlg c v n
p) 

{-
  evalP      = error "ExtAlg/evalP: not implemented"
  varSubsP   = error "ExtAlg/varSubsP: not implemented"
  coeffSubsP = error "ExtAlg/coeffSubsP: not implemented"
  subsP      = error "ExtAlg/subsP: not implemented"
-}


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

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

-- hackety hack hack...
instance IsSigned (ExtAlg c v n) where
  signOf :: ExtAlg c v n -> Maybe Sign
signOf = Maybe Sign -> ExtAlg 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 (ExtAlg c v n) where
  isZeroR :: ExtAlg c v n -> Bool
isZeroR   = FreeMod c (Ext v n) -> Bool
forall b c. Ord b => FreeMod c b -> Bool
ZMod.isZero (FreeMod c (Ext v n) -> Bool)
-> (ExtAlg c v n -> FreeMod c (Ext v n)) -> ExtAlg c v n -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ExtAlg c v n -> FreeMod c (Ext v n)
forall c (v :: Symbol) (n :: Nat).
ExtAlg c v n -> FreeMod c (Ext v n)
unExtAlg
  isAtomicR :: Proxy (ExtAlg c v n) -> Bool
isAtomicR = Bool -> Proxy (ExtAlg c v n) -> Bool
forall a b. a -> b -> a
const Bool
False
  isSignedR :: Proxy (ExtAlg c v n) -> Bool
isSignedR = Bool -> Proxy (ExtAlg c v n) -> Bool
forall a b. a -> b -> a
const Bool
False
  absR :: ExtAlg c v n -> ExtAlg c v n
absR      = ExtAlg c v n -> ExtAlg c v n
forall a. a -> a
id
  signumR :: ExtAlg c v n -> Maybe Sign
signumR   = Maybe Sign -> ExtAlg 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 1 or 0 into them.
--
embed :: (Ring c, KnownNat n, KnownNat m) => ExtAlg c v n -> ExtAlg c v m
embed :: ExtAlg c v n -> ExtAlg c v m
embed old :: ExtAlg c v n
old@(ExtAlg FreeMod c (Ext v n)
old_fm) = ExtAlg c v m
new where
  n :: Int
n = ExtAlg c v n -> Int
forall (n :: Nat) c (var :: Symbol).
KnownNat n =>
ExtAlg c var n -> Int
nOfExtAlg ExtAlg c v n
old
  m :: Int
m = ExtAlg c v m -> Int
forall (n :: Nat) c (var :: Symbol).
KnownNat n =>
ExtAlg c var n -> Int
nOfExtAlg ExtAlg c v m
new
  new :: ExtAlg c v m
new = FreeMod c (Ext v m) -> ExtAlg c v m
forall coeff (var :: Symbol) (n :: Nat).
FreeMod coeff (Ext var n) -> ExtAlg coeff var n
ExtAlg (FreeMod c (Ext v m) -> ExtAlg c v m)
-> FreeMod c (Ext v m) -> ExtAlg 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 -> (Ext v n -> Ext v m) -> FreeMod c (Ext v n) -> FreeMod c (Ext v m)
forall a b c.
(Ord a, Ord b) =>
(a -> b) -> FreeMod c a -> FreeMod c b
ZMod.unsafeMapBase Ext v n -> Ext v m
forall (n :: Nat) (var :: Symbol) (n :: Nat) (v :: Symbol).
KnownNat n =>
Ext var n -> Ext v n
project FreeMod c (Ext v n)
old_fm
    Ordering
EQ -> (Ext v n -> Ext v m) -> FreeMod c (Ext v n) -> FreeMod c (Ext v m)
forall a b c.
(Ord a, Ord b) =>
(a -> b) -> FreeMod c a -> FreeMod c b
ZMod.unsafeMapBase Ext v n -> Ext v m
forall (var :: Symbol) (n :: Nat) (var :: Symbol) (n :: Nat).
Ext var n -> Ext var n
keep    FreeMod c (Ext v n)
old_fm
    Ordering
GT -> (Ext v n -> Ext v m) -> FreeMod c (Ext v n) -> FreeMod c (Ext v m)
forall a b c.
(Ord a, Ord b) =>
(a -> b) -> FreeMod c a -> FreeMod c b
ZMod.unsafeMapBase Ext v n -> Ext v m
forall (var :: Symbol) (n :: Nat) (var :: Symbol) (n :: Nat).
Ext var n -> Ext var n
extend  FreeMod c (Ext v n)
old_fm
  extend :: Ext var n -> Ext var n
extend  (Ext Integer
int) = Integer -> Ext var n
forall (var :: Symbol) (n :: Nat). Integer -> Ext var n
Ext Integer
int
  keep :: Ext var n -> Ext var n
keep    (Ext Integer
int) = Integer -> Ext var n
forall (var :: Symbol) (n :: Nat). Integer -> Ext var n
Ext Integer
int
  project :: Ext var n -> Ext v n
project (Ext Integer
int) = let new :: Ext v n
new = Integer -> Ext v n
forall (var :: Symbol) (n :: Nat). Integer -> Ext var n
Ext Integer
int 
                      in  if Ext v n -> Bool
forall (n :: Nat) (v :: Symbol). KnownNat n => Ext v n -> Bool
isNormalExt Ext v n
new 
                            then Ext v n
new
                            else String -> Ext v n
forall a. HasCallStack => String -> a
error String
"Exterior/Indexed/embed: the projected variables are actually used!"

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