-- | Tests for the equivariant CSM class
{-# LANGUAGE Rank2Types, GADTs, TypeFamilies #-}
module Tests.CSM.Equivariant where
--------------------------------------------------------------------------------
import Data.Proxy
import Math.Combinat.Classes
import Math.Combinat.Partitions.Integer
import Math.Combinat.Partitions.Set
import qualified Math.RootLoci.Algebra.FreeMod as ZMod
import Math.RootLoci.Algebra
import Math.RootLoci.Geometry
import Math.RootLoci.Misc
import qualified Math.RootLoci.CSM.Equivariant.Ordered as Ordered
import qualified Math.RootLoci.CSM.Equivariant.Recursive as Recur
import qualified Math.RootLoci.CSM.Equivariant.Direct as Direct
import qualified Math.RootLoci.CSM.Equivariant.Umbral as Umbral
import Math.RootLoci.Classic
import Math.RootLoci.CSM.Aluffi
import Tests.Common
import Test.Tasty
import Test.Tasty.HUnit
--------------------------------------------------------------------------------
all_tests = testGroup "equivariant (projective) CSM classes"
[ testGroup "ordered"
[ testCase "structure lemma" (forList [-3..4] "failed" prop_structure_lemma )
, testCase "rec. ord. distinct = U(n) formula /AB" (forAllInt 7 "failed" $ prop_Un_equals_recursive ChernRoot )
, testCase "rec. ord. distinct = U(n) formula /Chern" (forAllInt 7 "failed" $ prop_Un_equals_recursive ChernClass )
, testCase "recur. upper = sum of direct opens /AB" (forAllSetp 6 "failed" $ prop_ord_rec_upper_vs_sum_direct ChernRoot )
, testCase "recur. upper = sum of direct opens /Chern" (forAllSetp 6 "failed" $ prop_ord_rec_upper_vs_sum_direct ChernClass )
, testCase "tangent class = sum of all strata" (forAllInt 7 "failed" $ prop_tangent_class_equals_sum ChernClass)
]
, testGroup "unordered"
[ testGroup "direct"
[ testCase "recursive CSM = direct CSM (open) /AB" (forAllPart 8 "failed" $ prop_recur_direct_open ChernRoot )
, testCase "recursive CSM = direct CSM (open) /Chern" (forAllPart 8 "failed" $ prop_recur_direct_open ChernClass )
, testCase "recursive CSM = direct CSM (closed) /AB" (forAllPart 8 "failed" $ prop_recur_direct_closed ChernRoot )
, testCase "recursive CSM = direct CSM (closed) /Chern" (forAllPart 8 "failed" $ prop_recur_direct_closed ChernClass )
]
, testGroup "umbral"
[ testCase "umbral CSM = direct CSM (open) /AB" (forAllPart 10 "failed" $ prop_umbral_vs_direct_open ChernRoot )
, testCase "umbral CSM = direct CSM (open) /Chern" (forAllPart 10 "failed" $ prop_umbral_vs_direct_open ChernClass )
, testCase "umbral CSM = direct CSM (closed) /AB" (forAllPart 10 "failed" $ prop_umbral_vs_direct_closed ChernRoot )
, testCase "umbral CSM = direct CSM (closed) /Chern" (forAllPart 10 "failed" $ prop_umbral_vs_direct_closed ChernClass )
]
]
]
--------------------------------------------------------------------------------
prop_umbral_vs_direct_open sing part
= ( spec2' sing (Direct.directOpenCSM part) == spec2' sing (Umbral.umbralOpenCSM part) )
prop_umbral_vs_direct_closed sing part
= ( spec2' sing (Direct.directClosedCSM part) == spec2' sing (Umbral.umbralClosedCSM part) )
prop_recur_direct_open sing part = (spec2' sing (Direct.directOpenCSM part) == spec2' sing (Recur.openCSM part))
prop_recur_direct_closed sing part = (spec2' sing (Direct.directClosedCSM part) == spec2' sing (Recur.closedCSM part))
--------------------------------------------------------------------------------
-- very slow for n>=5 !! (because we have +3, so 5 -> 8)
prop_structure_lemma n = (Ordered.computeQPolys n == Ordered.formulaQPoly n)
prop_Un_equals_recursive sing n =
(spec2' sing $ Ordered.computeOpenStratumCSM n) ==
(spec2' sing $ Ordered.formulaDistinctCSM n)
prop_ord_rec_upper_vs_sum_direct sing setp =
(spec2' sing $ unsafeEtaToOmega (Recur.upperClass setp)) ==
(spec2' sing $ Ordered.computeClosureOfAnyStratumCSM setp )
prop_tangent_class_equals_sum sing n =
(spec2' sing $ Ordered.tangentChernClass n) ==
(spec2' sing $ ZMod.sum [ Ordered.formulaAnyStratumCSM setp | setp <- setPartitions n ])
--------------------------------------------------------------------------------