content: -----------------------------------------------------------------------------
  -- |
  -- Module    : TestSuite.Basics.BasicTests
  -- Copyright : (c) Levent Erkok
  -- License   : BSD3
  -- Maintainer: erkokl@gmail.com
  -- Stability : experimental
  --
  -- Test suite for Examples.Basics.BasicTests
  -----------------------------------------------------------------------------
  
  {-# LANGUAGE Rank2Types          #-}
  {-# LANGUAGE ScopedTypeVariables #-}
  
  {-# OPTIONS_GHC -Wall -Werror #-}
  
  module TestSuite.Basics.BasicTests(tests) where
  
  import Data.SBV.Control
  import Data.SBV.Internals hiding (free, output)
  import Utils.SBVTestFramework
  
  import Control.Monad       (void)
  import Control.Monad.Trans (liftIO)
  
  import System.Random
  
  import qualified Control.Exception as C
  
  -- Test suite
  tests :: TestTree
  tests = testGroup "Basics.BasicTests"
     [ testCase "basic-0.1" $ test0 f1 `showsAs` "5"
     , testCase "basic-0.2" $ test0 f2 `showsAs` "5"
     , testCase "basic-0.3" $ test0 f3 `showsAs` "25"
     , testCase "basic-0.4" $ test0 f4 `showsAs` "25"
     , testCase "basic-0.5" $ test0 f5 `showsAs` "4"
     , goldenVsStringShow "basic-1_1" $ test1 f1
     , goldenVsStringShow "basic-1_2" $ test1 f2
     , goldenVsStringShow "basic-1_3" $ test1 f3
     , goldenVsStringShow "basic-1_4" $ test1 f4
     , goldenVsStringShow "basic-1_5" $ test1 f5
     , goldenVsStringShow "basic-2_1" $ test2 f1
     , goldenVsStringShow "basic-2_2" $ test2 f2
     , goldenVsStringShow "basic-2_3" $ test2 f3
     , goldenVsStringShow "basic-2_4" $ test2 f4
     , goldenVsStringShow "basic-2_5" $ test2 f5
     , goldenVsStringShow "basic-3_1" $ test3 f1
     , goldenVsStringShow "basic-3_2" $ test3 f2
     , goldenVsStringShow "basic-3_3" $ test3 f3
     , goldenVsStringShow "basic-3_4" $ test3 f4
     , goldenVsStringShow "basic-3_5" $ test3 f5
     , goldenVsStringShow "basic-4_1" $ test4 f1
     , goldenVsStringShow "basic-4_2" $ test4 f2
     , goldenVsStringShow "basic-4_3" $ test4 f3
     , goldenVsStringShow "basic-4_4" $ test4 f4
     , goldenVsStringShow "basic-4_5" $ test4 f5
     , goldenVsStringShow "basic-5_1" $ test5 f1
     , goldenVsStringShow "basic-5_2" $ test5 f2
     , goldenVsStringShow "basic-5_3" $ test5 f3
     , goldenVsStringShow "basic-5_4" $ test5 f4
     , goldenVsStringShow "basic-5_5" $ test5 f5
     , goldenCapturedIO   "nested1"   $ nested nested1
     , goldenCapturedIO   "nested2"   $ nested nested2
     , goldenCapturedIO   "nested3"   $ nested nested3
     , goldenCapturedIO   "nested4"   $ nested nested4
     ]
  
  test0 :: (forall a. Num a => (a -> a -> a)) -> Word8
  test0 f = f (3 :: Word8) 2
  
  test1, test2, test3, test4, test5 :: (forall a. Num a => (a -> a -> a)) -> IO Result
  test1 f = runSAT $ do let x = literal (3 :: Word8)
                            y = literal (2 :: Word8)
                        pure $ f x y
  test2 f = runSAT $ do let x = literal (3 :: Word8)
                        y :: SWord8 <- free "y"
                        pure $ f x y
  test3 f = runSAT $ do x :: SWord8 <- free "x"
                        y :: SWord8 <- free "y"
                        pure $ f x y
  test4 f = runSAT $ do x :: SWord8 <- free "x"
                        pure $ f x x
  test5 f = runSAT $ do x :: SWord8 <- free "x"
                        let r = f x x
                        q :: SWord8 <- free "q"
                        _ <- output q
                        pure r
  
  f1, f2, f3, f4, f5 :: Num a => a -> a -> a
  f1 x y = (x+y)*(x-y)
  f2 x y = (x*x)-(y*y)
  f3 x y = (x+y)*(x+y)
  f4 x y = let z = x + y in z * z
  f5 x _ = x + 1
  
  -- Nested calls are not OK; make sure we catch these
  nested :: (SMTConfig -> IO a) -> FilePath -> IO ()
  nested t rf = do setStdGen (mkStdGen 0)
                   void (t z3{verbose=True, redirectVerbose=Just rf})
                    `C.catch` \(e::C.SomeException) -> do appendFile rf "CAUGHT EXCEPTION\n\n"
                                                          appendFile rf (show e)
  
  nested1 :: SMTConfig -> IO ThmResult
  nested1 cfg = proveWith cfg $ do
    x <- free "x"
    y <- free "y"
    liftIO $ f x y
   where f :: SWord32 -> SWord32 -> IO SBool
         f x y = do
           res <- isSatisfiable $ x .== y
           return $ if res then sTrue else sFalse
  
  nested2 :: SMTConfig -> IO ThmResult
  nested2 cfg = proveWith cfg $ do
    x <- free "x"
    liftIO $ f x
   where f :: SWord32 -> IO SBool
         f x = do
           res <- isSatisfiable $ x .== 2
           return $ if res then sTrue else sFalse
  
  nested3 :: SMTConfig -> IO ThmResult
  nested3 cfg = proveWith cfg $ do
          y <- sBool "y"
          x <- liftIO leak        -- reach in!
          return $ y .== x
    where leak :: IO SBool
          leak = runSMTWith cfg $ do
                          x <- sBool "x"
                          query $ pure x
  
  nested4 :: SMTConfig -> IO Bool
  nested4 cfg = do
    d1 <- runSMT (sArray_ :: Symbolic (SArray Bool Bool))
  
    let sboolOfInterest = readArray d1 sTrue
  
    isSatisfiableWith cfg sboolOfInterest
  