-----------------------------------------------------------------------------
-- |
-- Module    : TestSuite.Arrays.InitVals
-- Copyright : (c) Levent Erkok
-- License   : BSD3
-- Maintainer: erkokl@gmail.com
-- Stability : experimental
--
-- Testing arrays with initializers
-----------------------------------------------------------------------------

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

{-# OPTIONS_GHC -Wall -Werror #-}

module TestSuite.Arrays.InitVals(tests) where

import Data.SBV
import Utils.SBVTestFramework

readDef :: Predicate
readDef = do c :: SInteger <- free "c"
             i :: SInteger <- free "i"
             j <- free "j"
             let a = lambdaArray (const c)

             let a' = writeArray a j 32

             return $ ite (i ./= j) (readArray a' i .== c)
                                    (readArray a' i .== 32)

readNoDef :: Predicate
readNoDef = do i :: SInteger <- free "i"
               j :: SInteger <- free "j"

               a <- sArray_

               return $ readArray a i .== j

constArr :: Predicate
constArr = do i :: SInteger <- sInteger "i"
              j :: SInteger <- sInteger "j"

              constrain $ i .< j
              constrain $ i `sElem` [1, 2, 3, 75]
              pure $ readArray myArray i .== readArray myArray j
  where myArray = listArray [(1, 12), (2, 5) , (3, 6), (75, 5)] (7 :: Integer)

constArr2 :: Predicate
constArr2 = do i :: SInteger <- sInteger "i"
               j :: SInteger <- sInteger "j"

               constrain $ i .< j
               constrain $ i `sElem` [1, 2, 3, 75]
               pure $ readArray myArray i .== readArray myArray j
  where myArray = listArray [(1, 12), (2, 5) , (3, 6), (75, 5)] (2 :: Integer)

tests :: TestTree
tests = testGroup "Arrays" [
    testGroup "Arrays.InitVals"
      [ testCase "readDef_SArray"           $ assertIsThm readDef
      , testCase "readDef2_SArray2"         $ assertIsSat readNoDef
      , goldenCapturedIO "constArr_SArray"  $ t satWith constArr
      , goldenCapturedIO "constArr2_SArray" $ t satWith constArr2
      ]
  , testGroup "Arrays.Misc"
      [ goldenCapturedIO "array_misc_1"  $ t proveWith $ \i -> readArray (listArray [(True,1),(False,0)] 3) i .<= (1::SInteger)

      , goldenCapturedIO "array_misc_2"  $ t satWith   $ \(x :: SArray Integer Integer) i1 i2 i3 ->
                                                                 readArray x i1 .== 4 .&& readArray x i2 .== 5 .&& readArray x i3 .== 12

      , goldenCapturedIO "array_misc_3"  $ t proveWith $      write (empty False) [(True, True), (False, False)]
                                                          .== write (empty True)  [(True, True), (False, False)]

      , testCase         "array_misc_4"  $                   (write (empty False) [(True, True), (False, False)]
                                                          .== write (empty True)  [(True, True), (False, False)]) `showsAs` "True"

      -- Interestingly, z3 says UNKNOWN if the logic below isn't set to ALL.
      , goldenCapturedIO "array_misc_5"  $ t proveWith $ do setLogic Logic_ALL
                                                            pure (    write (empty 0) [(i, i) | i <- [0 .. (3 :: WordN 2)]]
                                                                  .== write (empty 1) [(i, i) | i <- [0 .. (3 :: WordN 2)]]) :: Symbolic SBool

      , testCase         "array_misc_6"  $                   (write (empty 0) [(i, i) | i <- [0 .. (3 :: WordN 2)]]
                                                          .== write (empty 1) [(i, i) | i <- [0 .. (3 :: WordN 2)]]) `showsAs` "<symbolic> :: SBool"

      , goldenCapturedIO "array_misc_7"  $ t proveWith $      write (empty 0) [(i, i) | i <- [0 .. (3 :: WordN 2)]]
                                                          .== write (empty 0) [(i, i) | i <- [0 .. (3 :: WordN 2)]]

      , testCase         "array_misc_8"  $                   (write (empty 0) [(i, i) | i <- [0 .. (3 :: WordN 2)]]
                                                          .== write (empty 0) [(i, i) | i <- [0 .. (3 :: WordN 2)]]) `showsAs` "True"

      , goldenCapturedIO "array_misc_9"   $ t proveWith $     write (empty 0) [(i, i+1) | i <- [0 .. (3 :: WordN 2)]]
                                                          .== write (empty 0) [(i, i)   | i <- [0 .. (3 :: WordN 2)]]

      , testCase         "array_misc_10" $                   (write (empty 0) [(i, i+1) | i <- [0 .. (3 :: WordN 2)]]
                                                          .== write (empty 0) [(i, i  ) | i <- [0 .. (3 :: WordN 2)]]) `showsAs` "False"

      , goldenCapturedIO "array_misc_11" $ t satWith $ \(a :: SArray (Integer, Integer) Integer) -> readArray a (literal (1, 2)) .== 3
      , goldenCapturedIO "array_misc_12" $ t satWith $ \(a :: SArray Integer (Integer, Integer)) -> readArray a 3 .== literal (1, 2)

      , goldenCapturedIO "array_misc_13" $ t satWith $ \(a :: SArray (Integer, Integer) (Integer, Integer)) -> readArray a (literal (1, 2)) .== literal (1, 2)
      , goldenCapturedIO "array_misc_14" $ t satWith $ \(a :: SArray Integer Float)   -> fpIsNaN (readArray a 2)
      , goldenCapturedIO "array_misc_15" $ t satWith $ \(a :: SArray Float   Integer) -> readArray a (0/0) .== 3

      , goldenCapturedIO "array_misc_16" $ t satWith (.== readArray (listArray [(0, 12)] 3 :: SArray Float                Integer) 0)
      , goldenCapturedIO "array_misc_17" $ t satWith (.== readArray (listArray [(0, 12)] 3 :: SArray Double               Integer) 0)
      , goldenCapturedIO "array_misc_18" $ t satWith (.== readArray (listArray [(0, 12)] 3 :: SArray (FloatingPoint 10 4) Integer) (0 :: SFloatingPoint 10 4))

      , goldenCapturedIO "array_misc_19" $ t satWith (.== readArray (listArray [(0, 12)] 3 :: SArray Float                Integer) (-0))
      , goldenCapturedIO "array_misc_20" $ t satWith (.== readArray (listArray [(0, 12)] 3 :: SArray Double               Integer) (-0))
      , goldenCapturedIO "array_misc_21" $ t satWith (.== readArray (listArray [(0, 12)] 3 :: SArray (FloatingPoint 10 4) Integer) (-(0 :: SFloatingPoint 10 4)))

      , goldenCapturedIO "array_misc_22" $ t satWith (.== readArray (listArray [(0/0, 12)] 3 :: SArray Float                Integer) (0/0))
      , goldenCapturedIO "array_misc_23" $ t satWith (.== readArray (listArray [(0/0, 12)] 3 :: SArray Double               Integer) (0/0))
      , goldenCapturedIO "array_misc_24" $ t satWith (.== readArray (listArray [(0/0, 12)] 3 :: SArray (FloatingPoint 10 4) Integer) (0/0))

      , goldenCapturedIO "array_misc_25" $ t satWith (.== readArray (listArray [(1/0, 12)] 3 :: SArray Float                Integer) (1/0))
      , goldenCapturedIO "array_misc_26" $ t satWith (.== readArray (listArray [(1/0, 12)] 3 :: SArray Double               Integer) (1/0))
      , goldenCapturedIO "array_misc_27" $ t satWith (.== readArray (listArray [(1/0, 12)] 3 :: SArray (FloatingPoint 10 4) Integer) (1/0))

      , goldenCapturedIO "array_misc_28" $ t satWith (.== readArray (listArray [(1/0, 12)] 3 :: SArray Float                Integer) (-(1/0)))
      , goldenCapturedIO "array_misc_29" $ t satWith (.== readArray (listArray [(1/0, 12)] 3 :: SArray Double               Integer) (-(1/0)))
      , goldenCapturedIO "array_misc_30" $ t satWith (.== readArray (listArray [(1/0, 12)] 3 :: SArray (FloatingPoint 10 4) Integer) (-(1/0)))

      , goldenCapturedIO "array_misc_31" $ t proveWith (listArray [(1, 2), (3, 4)] 5 .== listArray [(3 :: Integer, 4), (1, 2)] (5 :: Integer))
      , goldenCapturedIO "array_misc_32" $ t proveWith (listArray [(1, 2), (3, 4)] 5 .== listArray [(3 :: Integer, 4), (1, 2)] (5 :: Double))
      , goldenCapturedIO "array_misc_33" $ t proveWith (listArray [(1, 2), (3, 1)] 5 .== listArray [(3 :: Integer, 4), (1, 2)] (5 :: Double))
      , goldenCapturedIO "array_misc_34" $ t proveWith (listArray [(1, 2), (3, 1)] 5 ./= listArray [(3 :: Integer, 4), (1, 2)] (5 :: Double))
      ]
  ]
  where t p f goldFile = do r <- p defaultSMTCfg{verbose=True, redirectVerbose = Just goldFile} f
                            appendFile goldFile ("\nFINAL OUTPUT:\n" ++ show r ++ "\n")

        empty :: (SymVal a, SymVal b) => b -> SArray a b
        empty = listArray []

        write :: (SymVal a, SymVal b) => SArray a b -> [(a, b)] -> SArray a b
        write = foldr (\(k, v) a -> writeArray a (literal k) (literal v))

{- HLint ignore module "Reduce duplication" -}