-- Copyright (c) David Amos, 2008. All rights reserved.

{-# LANGUAGE FlexibleInstances #-}

module Math.Test.TCommutativeAlgebra where

import Math.Algebra.Field.Base
import Math.Algebra.Commutative.Monomial
import Math.Algebra.Commutative.MPoly
import Math.Algebra.Commutative.GBasis

import Test.QuickCheck

-- > quickCheck prop_CommRingMPoly
-- > verboseCheck prop_ComRingMPoly -- to see what input data is being used

-- Commutative Ring (with 1)
prop_CommRing (a,b,c) =
    a+(b+c) == (a+b)+c   &&  -- addition is associative
    a+b == b+a           &&  -- addition is commutative
    a+0 == a             &&  -- additive identity
    a+(-a) == 0          &&  -- additive inverse
    a*(b*c) == (a*b)*c   &&  -- multiplication is associative
    a*b == b*a           &&  -- multiplication is commutative
    a*1 == a             &&  -- multiplicative identity
    a*(b+c) == a*b + a*c     -- distributivity

monomial is = product $ zipWith (^) (map x_ [1..]) (map (max 0) is)

-- mpoly :: [(Integer,[Int])] -> MPoly Grevlex Q
mpoly ais = sum [fromInteger a * monomial is | (a,is) <- ais]

{-
-- can take a long time to run, probably because of the test for associativity of multiplication
prop_CommRingMPoly (ais,bjs,cks) = prop_CommRing (f,g,h) where
    f = mpoly ais
    g = mpoly bjs
    h = mpoly cks
    types = (ais,bjs,cks) :: ( [(Integer,[Int])], [(Integer,[Int])], [(Integer,[Int])] )
-}

instance Arbitrary (MPoly Grevlex Q) where
    -- arbitrary = do ais <- arbitrary :: Gen [(Integer,[Int])]
    arbitrary = do ais <- sized $ \n -> resize (n `div` 2) arbitrary :: Gen [(Integer,[Int])]
                   return (mpoly ais)
    -- coarbitrary = undefined -- !! only required if we want to test functions over the type

prop_CommRingMPoly (f,g,h) = prop_CommRing (f,g,h) where
    types = (f,g,h) :: (MPoly Grevlex Q, MPoly Grevlex Q, MPoly Grevlex Q)


-- Sources for tests:
-- [IVA] - Cox, Little, O'Shea: Ideals, Varieties and Algorithms
-- [UAG] - Cox, Little, O'Shea: Using Algebraic Geometry


test = and [
    gb (map toGlex [x*z-y^2,x^3-z^2]) == map toGlex [y^6-z^5,x*y^4-z^4,x^2*y^2-z^3,x^3-z^2,x*z-y^2], -- IVA p93
    gb (map toLex [x^2+y^2+z^2-1,x^2+z^2-y,x-z]) == map toLex [x-z,y-2*z^2,z^4+1/2*z^2-1/4], -- IVA p94
    gb (map toLex [x^2+y^2+z^2-1,x*y*z-1]) == map toLex [x+y^3*z+y*z^3-y*z,y^4*z^2+y^2*z^4-y^2*z^2+1], -- IVA p116
    gb [x*y+z-x*z,x^2-z,2*x^3-x^2*y*z-1] == [z^4-3*z^3-4*y*z+2*z^2-y+2*z-2,y*z^2+2*y*z-2*z^2+1,y^2-2*y*z+z^2-z,x+y-z] -- Grevlex, UAG p50-1
    ]



{-
http://www.cs.amherst.edu/~dac/iva.html
states that IVA, 2nd ed, 5th printing (the one I have) has a production error causing many +s and -s to appear incorrectly

This explains the following misprints I've found:
p117:
gb (map toLex [x*y-4,y^2-(x^3-1)])
-> [x-1/16y^4-1/16y^2,y^5+y^3-64]
IVA p117 claims it should be -y^3 in the second poly
But my answer is clearly correct, by looking at the reduction sequence for x*y-4
x*y-4 -> 1/16(y^5+y^3)-4 -> 0
  x-1/16(y^4+y^2)  y^5+y^3-64
By contrast, reducing over their set clearly stops at 1/8y^3

gb (map toLex [x-t-u,y-t^2-2*t*u,z-t^3-3*t^2*u])
The answer I get has some sign differences compared to IVA p127
-}

{-
The code has no trouble chomping through some of the examples that took a long time in the Sugar paper, eg
gb [x+y+z+t+u, x*y+y*z+z*t+t*u+u*x, x*y*z+y*z*t+z*t*u+t*u*x+u*x*y, x*y*z*t+y*z*t*u+z*t*u*x+t*u*x*y+u*x*y*z, x*y*z*t*u-1]
gb $ map toLex [x+y+z+t+u, x*y+y*z+z*t+t*u+u*x, x*y*z+y*z*t+z*t*u+t*u*x+u*x*y, x*y*z*t+y*z*t*u+z*t*u*x+t*u*x*y+u*x*y*z, x*y*z*t*u-1]
gb [w^31-w^6-w-x, w^8-y, w^10-z]
gb $ map toLex [w^31-w^6-w-x, w^8-y, w^10-z]

However, for some reason, the code gets indigestion on the following
gb $ map toLex [y*(1+x^2)^4 - 2*(5+19*x^2-45*x^4+x^6-4*x^8), z*(1+x^2)^4-2*(x+51*x^3+3*x^5+17*x^7)]

(For comparison, the v1 implementation of gbasis can manage, even though its performance on the sugar examples is only comparable)
-}