content: module Test.Field where
  
  import Protolude
  
  import Data.Field.Galois as F hiding (recip)
  import Data.Group
  import Test.Tasty
  import Test.Tasty.HUnit
  import Test.Tasty.QuickCheck
  
  annihilation :: Eq a => (a -> a -> a) -> a -> a -> Bool
  annihilation op e x = op x e == e && op e x == e
  
  associativity :: Eq a => (a -> a -> a) -> a -> a -> a -> Bool
  associativity op x y z = op x (op y z) == op (op x y) z
  
  commutativity :: Eq a => (a -> a -> a) -> a -> a -> Bool
  commutativity op x y = op x y == op y x
  
  distributivity :: Eq a => (a -> a -> a) -> (a -> a -> a) -> a -> a -> a -> Bool
  distributivity op op' x y z = op (op' x y) z == op' (op x z) (op y z)
                             && op x (op' y z) == op' (op x y) (op x z)
  
  identities :: Eq a => (a -> a -> a) -> a -> a -> Bool
  identities op e x = op x e == x && op e x == x
  
  inverses :: Eq a => (a -> a -> a) -> (a -> a) -> a -> a -> Bool
  inverses op inv e x = op x (inv x) == e && op (inv x) x == e
  
  groupAxioms :: forall g . (Arbitrary g, Eq g, Show g)
    => (g -> g -> g) -> (g -> g) -> g -> (g -> Bool) -> [TestTree]
  groupAxioms add inv id cond =
    [ testProperty "associativity" $
      associativity add
    , testProperty "commutativity" $
      commutativity add
    , testProperty "identity" $
      identities add id
    , testProperty "inverses" $
      \x -> cond x ==> inverses add inv id x
    ]
  
  fieldAxioms :: forall k . GaloisField k => k -> TestTree
  fieldAxioms _ = testGroup "Field axioms"
    [ testGroup "additive group axioms" $
      groupAxioms (+) negate (0 :: k) (const True)
    , testGroup "multiplicative group axioms" $
      groupAxioms (*) recip (1 :: k) (/= 0)
    , testProperty "distributivity of multiplication over addition" $
      distributivity ((*) :: k -> k -> k) (+)
    , testProperty "multiplicative annihilation" $
      annihilation ((*) :: k -> k -> k) 0
    ]
  
  frobeniusEndomorphisms :: forall k . GaloisField k => k -> TestTree
  frobeniusEndomorphisms _ = localOption (QuickCheckTests 10) $ testGroup "Frobenius endomorphisms"
    [ testProperty "frobenius endomorphisms are characteristic powers" $
      \(x :: k) -> frob x == F.pow x (char (witness :: k))
    , testProperty "frobenius endomorphisms are ring homomorphisms" $
      \(x :: k) (y :: k) (z :: k) -> frob (x * y + z) == frob x * frob y + frob z
    ]
  
  testField :: forall k . GaloisField k => TestName -> k -> TestTree
  testField s x = testGroup s [fieldAxioms x, frobeniusEndomorphisms x]
  
  testUnity :: forall n k . (KnownNat n, GaloisField k, CyclicSubgroup (RootsOfUnity n k))
    => TestName -> RootsOfUnity n k -> TestTree
  testUnity s g = testGroup s
    [ localOption (QuickCheckTests 10) . testGroup "Group axioms" $
      groupAxioms (<>) invert (mempty :: RootsOfUnity n k) (const True)
    , testCase "roots of unity" $
      isRootOfUnity g @?= True
    ]
  