{-# LANGUAGE BinaryLiterals #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}

module Grisette.SymPrim.Prim.BitsTests (bitsTests) where

import Data.Bits (Bits (rotateL, rotateR), FiniteBits)
import Data.Data (Proxy (Proxy))
import Grisette (IntN, SupportedPrim, WordN)
import Grisette.Internal.SymPrim.Prim.Term
  ( PEvalBitwiseTerm
      ( pevalAndBitsTerm,
        pevalComplementBitsTerm,
        pevalOrBitsTerm,
        pevalXorBitsTerm
      ),
    PEvalRotateTerm
      ( pevalRotateLeftTerm,
        pevalRotateRightTerm
      ),
    PEvalShiftTerm
      ( pevalShiftLeftTerm,
        pevalShiftRightTerm
      ),
    Term,
    andBitsTerm,
    bvConcatTerm,
    bvExtendTerm,
    bvSelectTerm,
    complementBitsTerm,
    conTerm,
    orBitsTerm,
    rotateLeftTerm,
    rotateRightTerm,
    shiftLeftTerm,
    shiftRightTerm,
    ssymTerm,
    xorBitsTerm,
  )
import Test.Framework (Test, testGroup)
import Test.Framework.Providers.HUnit (testCase)
import Test.Framework.Providers.QuickCheck2 (testProperty)
import Test.HUnit ((@?=))
import Test.QuickCheck (Property, discard, ioProperty)

bitsTests :: Test
bitsTests =
  testGroup
    "Bits"
    [ testGroup
        "AndBits"
        [ testCase "On both concrete" $ do
            pevalAndBitsTerm
              (conTerm 3 :: Term (WordN 4))
              (conTerm 5)
              @?= conTerm 1,
          testCase "On zeroBits" $ do
            pevalAndBitsTerm
              (conTerm 0 :: Term (WordN 4))
              (ssymTerm "a")
              @?= conTerm 0
            pevalAndBitsTerm
              (ssymTerm "a")
              (conTerm 0 :: Term (WordN 4))
              @?= conTerm 0,
          testCase "On all one bits" $ do
            pevalAndBitsTerm
              (conTerm 15 :: Term (WordN 4))
              (ssymTerm "a")
              @?= ssymTerm "a"
            pevalAndBitsTerm
              (ssymTerm "a")
              (conTerm 15 :: Term (WordN 4))
              @?= ssymTerm "a",
          testCase "On symbolic" $ do
            pevalAndBitsTerm
              (ssymTerm "a" :: Term (WordN 4))
              (ssymTerm "b")
              @?= andBitsTerm
                (ssymTerm "a" :: Term (WordN 4))
                (ssymTerm "b" :: Term (WordN 4))
        ],
      testGroup
        "OrBits"
        [ testCase "On both concrete" $ do
            pevalOrBitsTerm
              (conTerm 3 :: Term (WordN 4))
              (conTerm 5)
              @?= conTerm 7,
          testCase "On zeroBits" $ do
            pevalOrBitsTerm
              (conTerm 0 :: Term (WordN 4))
              (ssymTerm "a")
              @?= ssymTerm "a"
            pevalOrBitsTerm
              (ssymTerm "a")
              (conTerm 0 :: Term (WordN 4))
              @?= ssymTerm "a",
          testCase "On all one bits" $ do
            pevalOrBitsTerm
              (conTerm 15 :: Term (WordN 4))
              (ssymTerm "a")
              @?= conTerm 15
            pevalOrBitsTerm
              (ssymTerm "a")
              (conTerm 15 :: Term (WordN 4))
              @?= conTerm 15,
          testCase "On symbolic" $ do
            pevalOrBitsTerm
              (ssymTerm "a" :: Term (WordN 4))
              (ssymTerm "b")
              @?= orBitsTerm
                (ssymTerm "a" :: Term (WordN 4))
                (ssymTerm "b" :: Term (WordN 4))
        ],
      testGroup
        "XorBits"
        [ testCase "On both concrete" $ do
            pevalXorBitsTerm
              (conTerm 3 :: Term (WordN 4))
              (conTerm 5)
              @?= conTerm 6,
          testCase "On zeroBits" $ do
            pevalXorBitsTerm
              (conTerm 0 :: Term (WordN 4))
              (ssymTerm "a")
              @?= ssymTerm "a"
            pevalXorBitsTerm
              (ssymTerm "a")
              (conTerm 0 :: Term (WordN 4))
              @?= ssymTerm "a",
          testCase "On all one bits" $ do
            pevalXorBitsTerm
              (conTerm 15 :: Term (WordN 4))
              (ssymTerm "a")
              @?= pevalComplementBitsTerm (ssymTerm "a")
            pevalXorBitsTerm
              (ssymTerm "a")
              (conTerm 15 :: Term (WordN 4))
              @?= pevalComplementBitsTerm (ssymTerm "a"),
          testCase "On single complement" $ do
            pevalXorBitsTerm
              (pevalComplementBitsTerm $ ssymTerm "a" :: Term (WordN 4))
              (ssymTerm "b")
              @?= pevalComplementBitsTerm (pevalXorBitsTerm (ssymTerm "a") (ssymTerm "b"))
            pevalXorBitsTerm
              (ssymTerm "a" :: Term (WordN 4))
              (pevalComplementBitsTerm $ ssymTerm "b")
              @?= pevalComplementBitsTerm (pevalXorBitsTerm (ssymTerm "a") (ssymTerm "b")),
          testCase "On both complement" $ do
            pevalXorBitsTerm
              (pevalComplementBitsTerm $ ssymTerm "a" :: Term (WordN 4))
              (pevalComplementBitsTerm $ ssymTerm "b")
              @?= pevalXorBitsTerm (ssymTerm "a") (ssymTerm "b"),
          testCase "On symbolic" $ do
            pevalXorBitsTerm
              (ssymTerm "a" :: Term (WordN 4))
              (ssymTerm "b")
              @?= xorBitsTerm
                (ssymTerm "a" :: Term (WordN 4))
                (ssymTerm "b" :: Term (WordN 4))
        ],
      testGroup
        "ComplementBits"
        [ testCase "On concrete" $ do
            pevalComplementBitsTerm (conTerm 5 :: Term (WordN 4)) @?= conTerm 10,
          testCase "On complement" $ do
            pevalComplementBitsTerm (pevalComplementBitsTerm (ssymTerm "a") :: Term (WordN 4)) @?= ssymTerm "a",
          testCase "On symbolic" $ do
            pevalComplementBitsTerm (ssymTerm "a" :: Term (WordN 4))
              @?= complementBitsTerm (ssymTerm "a" :: Term (WordN 4))
        ],
      testGroup
        "ShiftLeft"
        [ testCase "On concrete" $ do
            pevalShiftLeftTerm (conTerm 15 :: Term (WordN 4)) (conTerm 2) @?= conTerm 12
            pevalShiftLeftTerm (conTerm 15 :: Term (IntN 4)) (conTerm 2) @?= conTerm 12,
          testCase "shift 0" $ do
            pevalShiftLeftTerm (ssymTerm "a" :: Term (WordN 4)) (conTerm 0) @?= ssymTerm "a"
            pevalShiftLeftTerm (ssymTerm "a" :: Term (IntN 4)) (conTerm 0) @?= ssymTerm "a",
          testCase "shift greater or equal to left bitsize" $ do
            pevalShiftLeftTerm (ssymTerm "a" :: Term (WordN 4)) (conTerm 4) @?= conTerm 0
            pevalShiftLeftTerm (ssymTerm "a" :: Term (IntN 4)) (conTerm 4) @?= conTerm 0
            pevalShiftLeftTerm (ssymTerm "a" :: Term (WordN 4)) (conTerm 5) @?= conTerm 0
            pevalShiftLeftTerm (ssymTerm "a" :: Term (IntN 4)) (conTerm 5) @?= conTerm 0,
          testCase "shift negative amount is undefined on for IntN" $ do
            pevalShiftLeftTerm (conTerm 15 :: Term (IntN 4)) (conTerm $ -1)
              @?= shiftLeftTerm (conTerm 15) (conTerm $ -1)
            pevalShiftLeftTerm (conTerm 15 :: Term (IntN 4)) (conTerm $ -8)
              @?= shiftLeftTerm (conTerm 15) (conTerm $ -8),
          testCase "shift symbolic" $ do
            pevalShiftLeftTerm (ssymTerm "a" :: Term (WordN 4)) (ssymTerm "b")
              @?= shiftLeftTerm (ssymTerm "a" :: Term (WordN 4)) (ssymTerm "b"),
          testCase "shift symbolic by concrete" $ do
            pevalShiftLeftTerm (ssymTerm "a" :: Term (WordN 4)) (conTerm 2)
              @?= bvConcatTerm
                (bvSelectTerm (Proxy @0) (Proxy @2) (ssymTerm "a" :: Term (WordN 4)))
                (conTerm 0 :: Term (WordN 2)),
          testCase "Regression: shift by very large number" $ do
            pevalShiftLeftTerm (conTerm 15 :: Term (IntN 128)) (conTerm maxBound) @?= conTerm 0
            pevalShiftLeftTerm (conTerm 15 :: Term (WordN 128)) (conTerm maxBound) @?= conTerm 0
        ],
      testGroup
        "ShiftRight"
        [ testCase "On concrete, should perform arithmetic shifting on IntN" $ do
            pevalShiftRightTerm (conTerm 7 :: Term (IntN 4)) (conTerm 2) @?= conTerm 1
            pevalShiftRightTerm (conTerm 15 :: Term (IntN 4)) (conTerm 2) @?= conTerm 15,
          testCase "On concrete, should perform logical shifting on WordN" $ do
            pevalShiftRightTerm (conTerm 7 :: Term (WordN 4)) (conTerm 2) @?= conTerm 1
            pevalShiftRightTerm (conTerm 15 :: Term (WordN 4)) (conTerm 2) @?= conTerm 3,
          testCase "shift 0" $ do
            pevalShiftRightTerm (ssymTerm "a" :: Term (WordN 4)) (conTerm 0) @?= ssymTerm "a"
            pevalShiftRightTerm (ssymTerm "a" :: Term (IntN 4)) (conTerm 0) @?= ssymTerm "a",
          testCase "shift greater or equal to left bitsize on WordN" $ do
            pevalShiftRightTerm (ssymTerm "a" :: Term (WordN 4)) (conTerm 4) @?= conTerm 0
            pevalShiftRightTerm (ssymTerm "a" :: Term (WordN 4)) (conTerm 5) @?= conTerm 0,
          testCase "shift greater or equal to left bitsize on IntN" $ do
            pevalShiftRightTerm (ssymTerm "a" :: Term (IntN 4)) (conTerm 5)
              @?= bvExtendTerm
                True
                (Proxy @4)
                ( bvSelectTerm
                    (Proxy @3)
                    (Proxy @1)
                    (ssymTerm "a" :: Term (IntN 4))
                )
            pevalShiftRightTerm (ssymTerm "a" :: Term (IntN 4)) (conTerm 4)
              @?= bvExtendTerm
                True
                (Proxy @4)
                ( bvSelectTerm
                    (Proxy @3)
                    (Proxy @1)
                    (ssymTerm "a" :: Term (IntN 4))
                ),
          testCase "shift negative amount is undefined on for IntN" $ do
            pevalShiftRightTerm (conTerm 15 :: Term (IntN 4)) (conTerm $ -1)
              @?= shiftRightTerm (conTerm 15) (conTerm $ -1)
            pevalShiftRightTerm (conTerm 15 :: Term (IntN 4)) (conTerm $ -8)
              @?= shiftRightTerm (conTerm 15) (conTerm $ -8),
          testCase "shift symbolic" $ do
            pevalShiftRightTerm (ssymTerm "a" :: Term (WordN 4)) (ssymTerm "b")
              @?= shiftRightTerm (ssymTerm "a" :: Term (WordN 4)) (ssymTerm "b"),
          testCase "shift symbolic by concrete" $ do
            pevalShiftRightTerm (ssymTerm "a" :: Term (WordN 4)) (conTerm 2)
              @?= bvConcatTerm
                (conTerm 0 :: Term (WordN 2))
                (bvSelectTerm (Proxy @2) (Proxy @2) (ssymTerm "a" :: Term (WordN 4)))
            pevalShiftRightTerm (ssymTerm "a" :: Term (IntN 4)) (conTerm 2)
              @?= bvExtendTerm
                True
                (Proxy @4)
                (bvSelectTerm (Proxy @2) (Proxy @2) (ssymTerm "a" :: Term (IntN 4))),
          testCase "Regression: shift by very large number" $ do
            pevalShiftRightTerm (conTerm 15 :: Term (IntN 128)) (conTerm maxBound) @?= conTerm 0
            pevalShiftRightTerm (conTerm 15 :: Term (WordN 128)) (conTerm maxBound) @?= conTerm 0
        ],
      testGroup
        "RotateLeft"
        [ testCase "On concrete" $ do
            pevalRotateLeftTerm (conTerm 0b10100101 :: Term (WordN 8)) (conTerm 2) @?= conTerm 0b10010110
            pevalRotateLeftTerm (conTerm 0b10100101 :: Term (IntN 8)) (conTerm 2) @?= conTerm 0b10010110,
          testCase "rotate 0" $ do
            pevalRotateLeftTerm (ssymTerm "a" :: Term (WordN 4)) (conTerm 0) @?= ssymTerm "a"
            pevalRotateLeftTerm (ssymTerm "a" :: Term (IntN 4)) (conTerm 0) @?= ssymTerm "a",
          testCase "rotate bitsize" $ do
            pevalRotateLeftTerm (ssymTerm "a" :: Term (WordN 4)) (conTerm 4)
              @?= ssymTerm "a"
            pevalRotateLeftTerm (ssymTerm "a" :: Term (IntN 4)) (conTerm 4)
              @?= ssymTerm "a",
          testCase "rotate greater than left bitsize" $ do
            pevalRotateLeftTerm (ssymTerm "a" :: Term (WordN 4)) (conTerm 5)
              @?= rotateLeftTerm (ssymTerm "a" :: Term (WordN 4)) (conTerm 1)
            pevalRotateLeftTerm (ssymTerm "a" :: Term (IntN 4)) (conTerm 5)
              @?= rotateLeftTerm (ssymTerm "a" :: Term (IntN 4)) (conTerm 1),
          testCase "rotate negative amount is undefined on for IntN" $ do
            pevalRotateLeftTerm (conTerm 15 :: Term (IntN 4)) (conTerm $ -1)
              @?= rotateLeftTerm (conTerm 15) (conTerm $ -1)
            pevalRotateLeftTerm (conTerm 15 :: Term (IntN 4)) (conTerm $ -8)
              @?= rotateLeftTerm (conTerm 15) (conTerm $ -8),
          testCase "rotate symbolic" $ do
            pevalRotateLeftTerm (ssymTerm "a" :: Term (WordN 4)) (conTerm 2)
              @?= rotateLeftTerm (ssymTerm "a" :: Term (WordN 4)) (conTerm 2),
          testCase "Regression: rotate by very large number" $ do
            pevalRotateLeftTerm (conTerm 15 :: Term (IntN 128)) (conTerm maxBound) @?= conTerm (rotateR 15 1)
            pevalRotateLeftTerm (conTerm 15 :: Term (WordN 128)) (conTerm maxBound) @?= conTerm (rotateR 15 1)
        ],
      testGroup
        "RotateRight"
        [ testProperty "On concrete WordN 1" $
            concreteSmallRotateRightCorrect @(WordN 1),
          testProperty "On concrete WordN 2" $
            concreteSmallRotateRightCorrect @(WordN 2),
          testProperty "On concrete WordN 3" $
            concreteSmallRotateRightCorrect @(WordN 3),
          testProperty "On concrete WordN 4" $
            concreteSmallRotateRightCorrect @(WordN 4),
          testProperty "On concrete WordN 8" $
            concreteSmallRotateRightCorrect @(WordN 8),
          testProperty "On concrete IntN 1" $
            concreteSmallRotateRightCorrect @(IntN 1),
          testProperty "On concrete IntN 2" $
            concreteSmallRotateRightCorrect @(IntN 2),
          testProperty "On concrete IntN 3" $
            concreteSmallRotateRightCorrect @(IntN 3),
          testProperty "On concrete IntN 4" $
            concreteSmallRotateRightCorrect @(IntN 4),
          testProperty "On concrete IntN 8" $
            concreteSmallRotateRightCorrect @(IntN 8),
          testCase "rotate 0" $ do
            pevalRotateRightTerm (ssymTerm "a" :: Term (WordN 4)) (conTerm 0) @?= ssymTerm "a"
            pevalRotateRightTerm (ssymTerm "a" :: Term (IntN 4)) (conTerm 0) @?= ssymTerm "a",
          testCase "rotate bitsize" $ do
            pevalRotateRightTerm (ssymTerm "a" :: Term (WordN 4)) (conTerm 4)
              @?= ssymTerm "a"
            pevalRotateRightTerm (ssymTerm "a" :: Term (IntN 4)) (conTerm 4)
              @?= ssymTerm "a",
          testCase "rotate greater than left bitsize" $ do
            pevalRotateRightTerm (ssymTerm "a" :: Term (WordN 4)) (conTerm 5)
              @?= rotateRightTerm (ssymTerm "a" :: Term (WordN 4)) (conTerm 1)
            pevalRotateRightTerm (ssymTerm "a" :: Term (IntN 4)) (conTerm 5)
              @?= rotateRightTerm (ssymTerm "a" :: Term (IntN 4)) (conTerm 1),
          testCase "rotate negative amount is undefined on for IntN" $ do
            pevalRotateRightTerm (conTerm 15 :: Term (IntN 4)) (conTerm $ -1)
              @?= rotateRightTerm (conTerm 15) (conTerm $ -1)
            pevalRotateRightTerm (conTerm 15 :: Term (IntN 4)) (conTerm $ -8)
              @?= rotateRightTerm (conTerm 15) (conTerm $ -8),
          testCase "rotate symbolic" $ do
            pevalRotateRightTerm (ssymTerm "a" :: Term (WordN 4)) (conTerm 2)
              @?= rotateRightTerm (ssymTerm "a" :: Term (WordN 4)) (conTerm 2),
          testCase "Regression: rotate by very large number" $ do
            pevalRotateRightTerm (conTerm 15 :: Term (IntN 128)) (conTerm maxBound) @?= conTerm (rotateL 15 1)
            pevalRotateRightTerm (conTerm 15 :: Term (WordN 128)) (conTerm maxBound) @?= conTerm (rotateL 15 1)
        ]
    ]

concreteSmallRotateRightCorrect ::
  (PEvalRotateTerm a, Integral a, FiniteBits a, SupportedPrim a) =>
  a ->
  a ->
  Property
concreteSmallRotateRightCorrect _ b | b < 0 = discard
concreteSmallRotateRightCorrect a b = ioProperty $ do
  pevalRotateRightTerm (conTerm a) (conTerm b)
    @?= conTerm (rotateR a (fromIntegral b))