finite-field-0.10.0: test/TestPrimeField.hs

{-# LANGUAGE TemplateHaskell, ScopedTypeVariables, GADTs, DataKinds, CPP, TypeOperators #-}
{-# OPTIONS_GHC -fcontext-stack=32 #-}

import Prelude hiding (toInteger)

import Test.Tasty
import Test.Tasty.QuickCheck
import Test.Tasty.HUnit
import Test.Tasty.TH
import qualified Test.QuickCheck.Monadic as QM

import Control.DeepSeq
import Control.Exception
import Control.Monad
import Data.Either
import Data.Hashable
import Data.List (genericLength)
import Data.Numbers.Primes (primes)
import Data.Proxy
import Data.Ratio

import Data.FiniteField
#ifdef UseGHCTypeLits
import Data.Maybe
import GHC.TypeLits
#else
import TypeLevel.Number.Nat
#endif

-- ----------------------------------------------------------------------
-- addition

prop_add_comm =
  forAll smallPrimes $ \(SomeNat' (_ :: Proxy p)) ->
    forAll arbitrary $ \(a :: PrimeField p) ->
    forAll arbitrary $ \b ->
      a + b == b + a

prop_add_assoc =
  forAll smallPrimes $ \(SomeNat' (_ :: Proxy p)) ->
    forAll arbitrary $ \(a :: PrimeField p) ->
    forAll arbitrary $ \b ->
    forAll arbitrary $ \c ->
      (a + b) + c == a + (b + c)

prop_add_unitl =
  forAll smallPrimes $ \(SomeNat' (_ :: Proxy p)) ->
    forAll arbitrary $ \(a :: PrimeField p) ->
      0 + a == a

prop_add_unitr =
  forAll smallPrimes $ \(SomeNat' (_ :: Proxy p)) ->
    forAll arbitrary $ \(a :: PrimeField p) ->
      a + 0 == a

prop_negate =
  forAll smallPrimes $ \(SomeNat' (_ :: Proxy p)) ->
    forAll arbitrary $ \(a :: PrimeField p) ->
      a + negate a == 0

prop_sub_negate =
  forAll smallPrimes $ \(SomeNat' (_ :: Proxy p)) ->
    forAll arbitrary $ \(a :: PrimeField p) ->
    forAll arbitrary $ \(b :: PrimeField p) ->
      a - b == a + negate b

-- ----------------------------------------------------------------------
-- multiplication

prop_mult_comm =
  forAll smallPrimes $ \(SomeNat' (_ :: Proxy p)) ->
    forAll arbitrary $ \(a :: PrimeField p) ->
    forAll arbitrary $ \b ->
      a * b == b * a

prop_mult_assoc =
  forAll smallPrimes $ \(SomeNat' (_ :: Proxy p)) ->
    forAll arbitrary $ \(a :: PrimeField p) ->
    forAll arbitrary $ \b ->
    forAll arbitrary $ \c ->
      (a * b) * c == a * (b * c)

prop_mult_unitl =
  forAll smallPrimes $ \(SomeNat' (_ :: Proxy p)) ->
    forAll arbitrary $ \(a :: PrimeField p) ->
      1 * a == a

prop_mult_unitr =
  forAll smallPrimes $ \(SomeNat' (_ :: Proxy p)) ->
    forAll arbitrary $ \(a :: PrimeField p) ->
      a * 1 == a

prop_mult_zero_l =
  forAll smallPrimes $ \(SomeNat' (_ :: Proxy p)) ->
    forAll arbitrary $ \(a :: PrimeField p) ->
      0*a == 0

prop_mult_zero_r =
  forAll smallPrimes $ \(SomeNat' (_ :: Proxy p)) ->
        forAll arbitrary $ \(a :: PrimeField p) ->
          a*0 == 0

-- ----------------------------------------------------------------------
-- distributivity

prop_distl =
  forAll smallPrimes $ \(SomeNat' (_ :: Proxy p)) ->
    forAll arbitrary $ \(a :: PrimeField p) ->
    forAll arbitrary $ \b ->
    forAll arbitrary $ \c ->
      a * (b + c) == a*b + a*c

prop_distr =
  forAll smallPrimes $ \(SomeNat' (_ :: Proxy p)) ->
    forAll arbitrary $ \(a :: PrimeField p) ->
    forAll arbitrary $ \b ->
    forAll arbitrary $ \c ->
      (b + c) * a == b*a + c*a

-- ----------------------------------------------------------------------
-- misc Num methods

prop_abs =
  forAll smallPrimes $ \(SomeNat' (_ :: Proxy p)) ->
    forAll arbitrary $ \(a :: PrimeField p) ->
      abs a == a

prop_signum =
  forAll smallPrimes $ \(SomeNat' (_ :: Proxy p)) ->
    forAll arbitrary $ \(a :: PrimeField p) ->
      signum a == 1

-- ----------------------------------------------------------------------
-- Fractional

prop_fromRational =
  forAll smallPrimes $ \(SomeNat' (_ :: Proxy p)) ->
    forAll arbitrary $ \(r :: Rational) ->
      (fromRational r :: PrimeField p) == fromInteger (numerator r) / fromInteger (denominator r)

prop_recip =
  forAll smallPrimes $ \(SomeNat' (_ :: Proxy p)) ->
    forAll arbitrary $ \(a :: PrimeField p) ->
      a /= 0 ==> a * (recip a) == 1

-- ----------------------------------------------------------------------
-- FiniteField

prop_pthRoot =
  forAll smallPrimes $ \(SomeNat' (_ :: Proxy p)) ->
    forAll arbitrary $ \(a :: PrimeField p) ->
      pthRoot a ^ char a == a

prop_allValues = do
  forAll smallPrimes $ \(SomeNat' (_ :: Proxy p)) ->
    genericLength (allValues :: [PrimeField p]) == order (undefined :: PrimeField p)

-- ----------------------------------------------------------------------
-- Show / Read

prop_read_show =
  forAll smallPrimes $ \(SomeNat' (_ :: Proxy p)) ->
    forAll arbitrary $ \(a :: PrimeField p) ->
      read (show a) == a  

-- ----------------------------------------------------------------------
-- Ord

prop_zero_minimum =
  forAll smallPrimes $ \(SomeNat' (_ :: Proxy p)) ->
    forAll arbitrary $ \(a :: PrimeField p) ->
      0 <= a

-- ----------------------------------------------------------------------
-- NFData

prop_rnf =
  forAll smallPrimes $ \(SomeNat' (_ :: Proxy p)) ->
    forAll arbitrary $ \(a :: PrimeField p) ->
      rnf a == ()

-- ----------------------------------------------------------------------
-- Enum

prop_toEnum_fromEnum =
  forAll smallPrimes $ \(SomeNat' (_ :: Proxy p)) ->
    forAll arbitrary $ \(a :: PrimeField p) ->
      toEnum (fromEnum a) == a

prop_toEnum_negative = QM.monadicIO $ do
  SomeNat' (_ :: Proxy p) <- QM.pick smallPrimes
  let a :: PrimeField p
      a = toEnum (-1)
  (ret :: Either SomeException (PrimeField p)) <- QM.run $ try $ evaluate $ a
  QM.assert $ isLeft ret

-- https://github.com/msakai/finite-field/issues/2
case_toEnum_big_integer =
  (toEnum 7 :: $(primeField (2^127 - 1))) @?= 7  

-- ----------------------------------------------------------------------

prop_hash =
  forAll smallPrimes $ \(SomeNat' (_ :: Proxy p)) ->
    forAll arbitrary $ \(a :: PrimeField p) ->
      hash a `seq` () == ()

-- ----------------------------------------------------------------------
-- misc

prop_fromInteger_toInteger =
  forAll smallPrimes $ \(SomeNat' (_ :: Proxy p)) ->
    forAll arbitrary $ \(a :: PrimeField p) ->
      fromInteger (toInteger a) == a

case_primeFieldT = a @?= 1
  where
    a :: $(primeField 15485867)
    a = 15485867 + 1

------------------------------------------------------------------------

#ifdef UseGHCTypeLits

data SomeNat' where
  SomeNat' :: KnownNat p => Proxy p -> SomeNat'

instance Show SomeNat' where
  showsPrec p (SomeNat' x) = showsPrec p (natVal x)

#else

data SomeNat' where
  SomeNat' :: Nat p => Proxy p -> SomeNat'

instance Show SomeNat' where
  showsPrec p (SomeNat' (x :: Proxy p)) = showsPrec p (toInt (undefined :: p))

#endif

smallPrimes :: Gen SomeNat'
smallPrimes = do
  i <- choose (0, 2^(16::Int))
#ifdef UseGHCTypeLits
  case fromJust $ someNatVal $ primes !! i of
    SomeNat proxy -> return $ SomeNat' proxy
#else
  let f :: forall p. Nat p => p -> SomeNat'
      f _ = SomeNat' (Proxy :: Proxy p)
  return $ withNat f (primes !! i)
#endif

#ifdef UseGHCTypeLits
instance KnownNat p => Arbitrary (PrimeField p) where
#else
instance Nat p => Arbitrary (PrimeField p) where
#endif
  arbitrary = liftM fromInteger arbitrary

------------------------------------------------------------------------
-- Test harness

main :: IO ()
main = $(defaultMainGenerator)

#if !MIN_VERSION_base(4,7,0)

isLeft :: Either a b -> Bool
isLeft (Left  _) = True
isLeft (Right _) = False

isRight :: Either a b -> Bool
isRight (Left  _) = False
isRight (Right _) = True

#endif