{-# LANGUAGE ScopedTypeVariables #-}
module Main (main) where

import           Data.SBV
import           Test.Tasty
import           Test.Tasty.HUnit
import           Test.Tasty.Providers
import           Test.Tasty.Runners
import           Test.Tasty.SBV

main :: IO ()
main = defaultMain tests

tests :: TestTree
tests = testGroup "tasty-sbv"
 [ testVerification
 ]

testVerification :: TestTree
testVerification = testGroup "verification"
 [ testCase "Can prove true" $ do
     let fs = FS (forAll ["x", "y"] $ \(x::SWord8) y -> x `shiftR` 8 .== y `sDiv` 256)
     r <- run mempty fs (const $ pure ())
     assertBool "easy proof failed" $ resultSuccessful r
 , testCase "Can't prove false" $ do
     let fs = FS (forAll ["x", "y"] $ \(x::SWord8) y -> x `shiftL` 2 .== y)
     r <- run mempty fs (const $ pure ())
     assertBool "impossible proof succeded" $ not $ resultSuccessful r
 ]