-- | 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 ]) 
  
--------------------------------------------------------------------------------