{-# LANGUAGE DataKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}

module Grisette.Core.Data.Class.SymRotateTests (symRotateTests) where

import Data.Bits (Bits (rotate), FiniteBits (finiteBitSize))
import Data.Data (Proxy (Proxy), Typeable, typeRep)
import Data.Int (Int16, Int32, Int64, Int8)
import Data.Word (Word16, Word32, Word64, Word8)
import Grisette
  ( AsKey (AsKey),
    IntN,
    Solvable (con),
    SymIntN,
    SymRotate (symRotate, symRotateNegated),
    SymWordN,
    WordN,
  )
import Grisette.Internal.Core.Data.Class.AsKey (KeyEq)
import Test.Framework (Test, testGroup)
import Test.Framework.Providers.QuickCheck2 (testProperty)
import Test.HUnit (Assertion, (@?=))
import Test.QuickCheck (Arbitrary, chooseInt, forAll, ioProperty)

concreteRotateIsCorrect ::
  (SymRotate a, Show a, Integral a, FiniteBits a) =>
  a ->
  a ->
  Assertion
concreteRotateIsCorrect a s =
  symRotate a s
    @?= rotate
      a
      ( fromIntegral $
          (fromIntegral s :: Integer) `mod` fromIntegral (finiteBitSize a)
      )

concreteRotateNegatedIsCorrect ::
  (SymRotate a, Show a, Integral a, FiniteBits a) =>
  a ->
  a ->
  Assertion
concreteRotateNegatedIsCorrect a s =
  symRotateNegated a s
    @?= rotate
      a
      ( fromIntegral $
          (-fromIntegral s :: Integer) `mod` fromIntegral (finiteBitSize a)
      )

concreteUnsignedTypeSymRotateTests ::
  forall proxy a.
  ( Arbitrary a,
    Show a,
    SymRotate a,
    FiniteBits a,
    Bounded a,
    Typeable a,
    Integral a
  ) =>
  proxy a ->
  Test
concreteUnsignedTypeSymRotateTests p =
  testGroup
    (show $ typeRep p)
    [ testGroup
        "SymRotate"
        [ testProperty "symRotate" $ \(x :: a) ->
            forAll (chooseInt (0, finiteBitSize x)) $
              \(s :: Int) ->
                ioProperty $ concreteRotateIsCorrect x (fromIntegral s),
          testProperty "symRotateNegated" $ \(x :: a) ->
            forAll (chooseInt (0, finiteBitSize x)) $
              \(s :: Int) ->
                ioProperty $ concreteRotateNegatedIsCorrect x (fromIntegral s),
          testProperty "symRotate max" $ \(x :: a) ->
            ioProperty $ concreteRotateIsCorrect x maxBound,
          testProperty "symRotateNegated max" $ \(x :: a) ->
            ioProperty $ concreteRotateNegatedIsCorrect x maxBound
        ]
    ]

concreteSignedTypeSymRotateTests ::
  forall proxy a.
  ( Arbitrary a,
    Show a,
    SymRotate a,
    FiniteBits a,
    Bounded a,
    Typeable a,
    Integral a
  ) =>
  proxy a ->
  Test
concreteSignedTypeSymRotateTests p =
  testGroup
    (show $ typeRep p)
    [ testGroup
        "SymRotate"
        [ testProperty "symRotate" $ \(x :: a) ->
            forAll (chooseInt (-finiteBitSize x, finiteBitSize x)) $
              \(s :: Int) ->
                ioProperty $ concreteRotateIsCorrect x (fromIntegral s),
          testProperty "symRotateNegated" $ \(x :: a) ->
            forAll (chooseInt (-finiteBitSize x, finiteBitSize x)) $
              \(s :: Int) ->
                ioProperty $ concreteRotateNegatedIsCorrect x (fromIntegral s),
          testProperty "symRotate max" $ \(x :: a) ->
            ioProperty $ concreteRotateIsCorrect x maxBound,
          testProperty "symRotateNegated max" $ \(x :: a) ->
            ioProperty $ concreteRotateNegatedIsCorrect x maxBound,
          testProperty "symRotate min" $ \(x :: a) ->
            ioProperty $ concreteRotateIsCorrect x minBound,
          testProperty "symRotateNegated min" $ \(x :: a) ->
            ioProperty $ concreteRotateNegatedIsCorrect x minBound
        ]
    ]

symbolicTypeSymRotateTests ::
  forall proxy c s.
  ( Arbitrary c,
    Show s,
    Num s,
    SymRotate c,
    SymRotate s,
    FiniteBits c,
    Bounded c,
    Typeable s,
    Integral c,
    Solvable c s,
    Show c,
    KeyEq s
  ) =>
  proxy s ->
  Test
symbolicTypeSymRotateTests p =
  testGroup
    (show $ typeRep p)
    [ testGroup
        "SymRotate"
        [ testProperty "concrete/concrete symRotate" $ \(x :: c) ->
            forAll (chooseInt (-finiteBitSize x, finiteBitSize x)) $
              \(s :: Int) ->
                ioProperty $
                  AsKey (symRotate (con x :: s) (fromIntegral s))
                    @?= con (symRotate x (fromIntegral s)),
          testProperty "symRotate max" $ \(x :: c) ->
            ioProperty $
              AsKey (symRotate (con x :: s) (con maxBound))
                @?= con (symRotate x maxBound),
          testProperty "symRotate min" $ \(x :: c) ->
            ioProperty $ do
              AsKey (symRotate (con x :: s) (con minBound))
                @?= con (symRotate x minBound)
        ]
    ]

symRotateTests :: Test
symRotateTests =
  testGroup
    "SymRotate"
    [ concreteUnsignedTypeSymRotateTests (Proxy :: Proxy Word8),
      concreteUnsignedTypeSymRotateTests (Proxy :: Proxy Word16),
      concreteUnsignedTypeSymRotateTests (Proxy :: Proxy Word32),
      concreteUnsignedTypeSymRotateTests (Proxy :: Proxy Word64),
      concreteUnsignedTypeSymRotateTests (Proxy :: Proxy Word),
      concreteUnsignedTypeSymRotateTests (Proxy :: Proxy (WordN 1)),
      concreteUnsignedTypeSymRotateTests (Proxy :: Proxy (WordN 2)),
      concreteUnsignedTypeSymRotateTests (Proxy :: Proxy (WordN 3)),
      concreteUnsignedTypeSymRotateTests (Proxy :: Proxy (WordN 63)),
      concreteUnsignedTypeSymRotateTests (Proxy :: Proxy (WordN 64)),
      concreteUnsignedTypeSymRotateTests (Proxy :: Proxy (WordN 65)),
      concreteUnsignedTypeSymRotateTests (Proxy :: Proxy (WordN 128)),
      concreteSignedTypeSymRotateTests (Proxy :: Proxy Int8),
      concreteSignedTypeSymRotateTests (Proxy :: Proxy Int16),
      concreteSignedTypeSymRotateTests (Proxy :: Proxy Int32),
      concreteSignedTypeSymRotateTests (Proxy :: Proxy Int64),
      concreteSignedTypeSymRotateTests (Proxy :: Proxy Int),
      concreteSignedTypeSymRotateTests (Proxy :: Proxy (IntN 1)),
      concreteSignedTypeSymRotateTests (Proxy :: Proxy (IntN 2)),
      concreteSignedTypeSymRotateTests (Proxy :: Proxy (IntN 3)),
      concreteSignedTypeSymRotateTests (Proxy :: Proxy (IntN 63)),
      concreteSignedTypeSymRotateTests (Proxy :: Proxy (IntN 64)),
      concreteSignedTypeSymRotateTests (Proxy :: Proxy (IntN 65)),
      concreteSignedTypeSymRotateTests (Proxy :: Proxy (IntN 128)),
      symbolicTypeSymRotateTests (Proxy :: Proxy (SymWordN 1)),
      symbolicTypeSymRotateTests (Proxy :: Proxy (SymWordN 2)),
      symbolicTypeSymRotateTests (Proxy :: Proxy (SymWordN 3)),
      symbolicTypeSymRotateTests (Proxy :: Proxy (SymWordN 63)),
      symbolicTypeSymRotateTests (Proxy :: Proxy (SymWordN 64)),
      symbolicTypeSymRotateTests (Proxy :: Proxy (SymWordN 65)),
      symbolicTypeSymRotateTests (Proxy :: Proxy (SymWordN 128)),
      symbolicTypeSymRotateTests (Proxy :: Proxy (SymIntN 1)),
      symbolicTypeSymRotateTests (Proxy :: Proxy (SymIntN 2)),
      symbolicTypeSymRotateTests (Proxy :: Proxy (SymIntN 3)),
      symbolicTypeSymRotateTests (Proxy :: Proxy (SymIntN 63)),
      symbolicTypeSymRotateTests (Proxy :: Proxy (SymIntN 64)),
      symbolicTypeSymRotateTests (Proxy :: Proxy (SymIntN 65)),
      symbolicTypeSymRotateTests (Proxy :: Proxy (SymIntN 128))
    ]