content: {-# LANGUAGE DataKinds #-}
  {-# OPTIONS_GHC -fno-warn-unused-imports #-}
  module Main where
  import Algebra.Algorithms.Groebner
  import Algebra.Ring.Ideal
  import Algebra.Ring.Polynomial
  import Data.Type.Monomorphic
  import Data.Type.Natural           hiding (one, promote, zero)
  import Test.Hspec
  import Test.Hspec.QuickCheck
  import Test.QuickCheck             hiding (promote)
  import Utils
  
  main :: IO ()
  main = hspec $ do
    describe "divModPolynomial'" $ do
      prop "quotient cannot be diveided by any denoms (ternary)" $
        checkForArity [3] prop_indivisible
      prop "satisfies a_i f_i /= 0 ==> deg(f) >= deg (a_i f_i)" $
        checkForArity [3] prop_degdecay
      prop "divides correctly" $
        checkForArity [3] prop_divCorrect
  
  prop_divCorrect :: SingI n => SNat n -> Property
  prop_divCorrect sdim =
    forAll (polyOfDim sdim) $ \poly ->
    forAll (idealOfDim sdim) $ \ideal ->
    let dvs = take 5 $ generators ideal
        (qds, r) = poly `divModPolynomial'` dvs
    in poly == sum (map (uncurry (*)) qds) + r
  
  prop_indivisible :: SingI n => SNat n -> Property
  prop_indivisible sdim =
    forAll (polyOfDim sdim) $ \poly ->
    forAll (idealOfDim sdim) $ \ideal ->
    let dvs = take 5 $ generators ideal
        (_, r) = changeOrder Grevlex poly `divModPolynomial'` dvs
    in r /= 0 ==> all (\f -> all (\(_, m) -> not $ leadingMonomial f `divs` m) $ getTerms r)  dvs
  
  prop_degdecay :: SingI n => SNat n -> Property
  prop_degdecay sdim =
    forAll (polyOfDim sdim) $ \poly ->
    forAll (idealOfDim sdim) $ \ideal ->
    let dvs = take 5 $ generators ideal
        (qs, _) = poly `divModPolynomial'` dvs
    in all (\(a, f) -> (a * f == 0) || (leadingMonomial poly >= leadingMonomial (a * f))) qs
  