content: {-# LANGUAGE DataKinds           #-}
  {-# LANGUAGE ScopedTypeVariables #-}
  {-# LANGUAGE TypeApplications    #-}
  -- The following warning is disabled due to a necessary instance of SatResult
  -- defined in this module.
  {-# OPTIONS_GHC -fno-warn-orphans #-}
  -- | Test copilot-theorem:Copilot.Theorem.What4.
  module Test.Copilot.Theorem.What4 where
  
  -- External imports
  import Control.Exception                    (Exception, try)
  import Data.Int                             (Int8)
  import Data.Proxy                           (Proxy (..))
  import Data.Typeable                        (typeRep)
  import Data.Word                            (Word32)
  import Test.Framework                       (Test, testGroup)
  import Test.Framework.Providers.QuickCheck2 (testProperty)
  import Test.HUnit                           (Assertion, assertBool,
                                               assertFailure)
  import Test.QuickCheck                      (Arbitrary (arbitrary), Property,
                                               arbitrary, forAll)
  import Test.QuickCheck.Monadic              (monadicIO, run)
  
  -- External imports: Copilot
  import           Copilot.Core.Expr      (Expr (Const, Drop, Op1, Op2), Id)
  import           Copilot.Core.Operators (Op1 (..), Op2 (..))
  import           Copilot.Core.Spec      (Spec (..), Stream (..))
  import qualified Copilot.Core.Spec      as Copilot
  import           Copilot.Core.Type      (Field (..),
                                           Struct (toValues, typeName),
                                           Type (Struct), Typed (typeOf),
                                           Value (..))
  
  -- Internal imports: Modules being tested
  import Copilot.Theorem.What4 (CounterExample (..), ProveException (..),
                                SatResult (..), SatResultCex (..), Solver (..),
                                prove, proveWithCounterExample)
  
  -- * Constants
  
  -- | Unit tests for copilot-theorem:Copilot.Theorem.What4.
  tests :: Test.Framework.Test
  tests =
    testGroup "Copilot.Theorem.What4"
      [ testProperty "Prove via Z3 that true is valid"    testProveZ3True
      , testProperty "Prove via Z3 that false is invalid" testProveZ3False
      , testProperty "Prove via Z3 that x == x is valid"  testProveZ3EqConst
      , testProperty "Prove via Z3 that a struct update is valid" testProveZ3StructUpdate
      , testProperty "Counterexample with invalid base case" testCounterExampleBaseCase
      , testProperty "Counterexample with invalid induction step" testCounterExampleInductionStep
      , testProperty "Check that the What4 backend rejects existential quantification" testWhat4ExistsException
      ]
  
  -- * Individual tests
  
  -- | Test that Z3 is able to prove the following expression valid:
  -- @
  --   constant True
  -- @
  testProveZ3True :: Property
  testProveZ3True =
      monadicIO $ run $ checkResult Z3 propName spec Valid
    where
      propName :: String
      propName = "prop"
  
      spec :: Spec
      spec = forallPropSpec propName [] $ Const typeOf True
  
  -- | Test that Z3 is able to prove the following expression invalid:
  -- @
  --   constant False
  -- @
  testProveZ3False :: Property
  testProveZ3False =
      monadicIO $ run $ checkResult Z3 propName spec Invalid
    where
      propName :: String
      propName = "prop"
  
      spec :: Spec
      spec = forallPropSpec propName [] $ Const typeOf False
  
  -- | Test that Z3 is able to prove the following expresion valid:
  -- @
  --   for all (x :: Int8), constant x == constant x
  -- @
  testProveZ3EqConst :: Property
  testProveZ3EqConst = forAll arbitrary $ \x ->
      monadicIO $ run $ checkResult Z3 propName (spec x) Valid
    where
      propName :: String
      propName = "prop"
  
      spec :: Int8 -> Spec
      spec x = forallPropSpec propName [] $
        Op2 (Eq typeOf) (Const typeOf x) (Const typeOf x)
  
  -- | Test that Z3 is able to prove the following expresion valid:
  -- @
  --   for all (s :: MyStruct),
  --   ((s ## testField =$ (+1)) # testField) == ((s # testField) + 1)
  -- @
  testProveZ3StructUpdate :: Property
  testProveZ3StructUpdate = forAll arbitrary $ \x ->
      monadicIO $ run $ checkResult Z3 propName (spec x) Valid
    where
      propName :: String
      propName = "prop"
  
      spec :: TestStruct -> Spec
      spec s = forallPropSpec propName [] $
        Op2
          (Eq typeOf)
          (getField
            (Op2
              (UpdateField typeOf typeOf testField)
              sExpr
              (add1 (getField sExpr))))
          (add1 (getField sExpr))
        where
          sExpr :: Expr TestStruct
          sExpr = Const typeOf s
  
          getField :: Expr TestStruct -> Expr Word32
          getField = Op1 (GetField typeOf typeOf testField)
  
          add1 :: Expr Word32 -> Expr Word32
          add1 x = Op2 (Add typeOf) x (Const typeOf 1)
  
  -- | Test that Z3 is able to produce a counterexample to the following property,
  -- where the base case is proved invalid:
  --
  -- @
  --   let s :: Stream Bool
  --       s = [False] ++ constant True
  --   in forAll s
  -- @
  testCounterExampleBaseCase :: Property
  testCounterExampleBaseCase =
      monadicIO $ run $
        checkCounterExample Z3 propName spec $ \cex ->
          pure $ not $ and $ baseCases cex
    where
      propName :: String
      propName = "prop"
  
      -- s = [False] ++ constant True
      s :: Stream
      s = Stream
        { streamId       = sId
        , streamBuffer   = [False]
        , streamExpr     = Const typeOf True
        , streamExprType = typeOf
        }
  
      sId :: Id
      sId = 0
  
      spec :: Spec
      spec = forallPropSpec propName [s] $ Drop typeOf 0 sId
  
  -- | Test that Z3 is able to produce a counterexample to the following property,
  -- where the induction step is proved invalid:
  --
  -- @
  --   let s :: Stream Bool
  --       s = [True] ++ constant False
  --   in forAll s
  -- @
  testCounterExampleInductionStep :: Property
  testCounterExampleInductionStep =
      monadicIO $ run $
        checkCounterExample Z3 propName spec $ \cex ->
          pure $ not $ inductionStep cex
    where
      propName :: String
      propName = "prop"
  
      -- s = [True] ++ constant False
      s :: Stream
      s = Stream
        { streamId       = sId
        , streamBuffer   = [True]
        , streamExpr     = Const typeOf False
        , streamExprType = typeOf
        }
  
      sId :: Id
      sId = 0
  
      spec :: Spec
      spec = forallPropSpec propName [s] $ Drop typeOf 0 sId
  
  -- | Test that @copilot-theorem@'s @what4@ backend will throw an exception if it
  -- attempts to prove an existentially quantified proposition.
  testWhat4ExistsException :: Property
  testWhat4ExistsException =
      monadicIO $ run $
        checkException (prove Z3 spec) isUnexpectedExistentialProposition
    where
      isUnexpectedExistentialProposition :: ProveException -> Bool
      isUnexpectedExistentialProposition UnexpectedExistentialProposition = True
  
      propName :: String
      propName = "prop"
  
      spec :: Spec
      spec = existsPropSpec propName [] $ Const typeOf True
  
  -- | A simple data type with a 'Struct' instance and a 'Field'. This is only
  -- used as part of 'testProveZ3StructUpdate'.
  newtype TestStruct = TestStruct { testField :: Field "testField" Word32 }
  
  instance Arbitrary TestStruct where
    arbitrary = do
      w32 <- arbitrary
      return (TestStruct (Field w32))
  
  instance Struct TestStruct where
    typeName _ = "testStruct"
    toValues s = [Value typeOf (testField s)]
  
  instance Typed TestStruct where
    typeOf = Struct (TestStruct (Field 0))
  
  -- | Check that the solver's satisfiability result for the given property in
  -- the given spec matches the expectation.
  checkResult :: Solver -> String -> Spec -> SatResult -> IO Bool
  checkResult solver propName spec expectation = do
    results <- prove solver spec
  
    -- Find the satisfiability result for propName.
    let propResult = lookup propName results
  
    -- The following check also works for the case in which the property name
    -- does not exist in the results, in which case the lookup returns 'Nothing'.
    return $ propResult == Just expectation
  
  -- | Check that the solver produces an invalid result for the given property and
  -- that the resulting 'CounterExample' satifies the given predicate.
  checkCounterExample :: Solver
                      -> String
                      -> Spec
                      -> (CounterExample -> IO Bool)
                      -> IO Bool
  checkCounterExample solver propName spec cexPred = do
    results <- proveWithCounterExample solver spec
  
    -- Find the satisfiability result for propName. If the property name does not
    -- exist in the results, raise an assertion failure.
    propResult <-
      case lookup propName results of
        Just propResult ->
          pure propResult
        Nothing ->
          assertFailure $
            "Could not find property in results: " ++ propName
  
    -- Assert that the solver returned an invalid result and pass the
    -- counterexample to the predicate. If the result is anything other than
    -- invalid, raise an assertion failure.
    case propResult of
      InvalidCex cex ->
        cexPred cex
      ValidCex {} ->
        assertFailure "Expected invalid result, but result was valid"
      UnknownCex {} ->
        assertFailure "Expected invalid result, but result was unknown"
  
  -- | Check that the given 'IO' action throws a particular exception. This is
  -- largely taken from the implementation of @shouldThrow@ in
  -- @hspec-expectations@ (note that this test suite uses @test-framework@ instead
  -- of @hspec@).
  checkException :: forall e a. Exception e => IO a -> (e -> Bool) -> Assertion
  checkException action p = do
      r <- try action
      case r of
        Right _ ->
          assertFailure $
            "did not get expected exception: " ++ exceptionType
        Left e ->
          assertBool
            ("predicate failed on expected exception: " ++ exceptionType ++
             "\n" ++ show e)
            (p e)
    where
      -- String representation of the expected exception's type
      exceptionType = show $ typeRep $ Proxy @e
  
  -- * Auxiliary
  
  -- | Build a 'Spec' that contains one property with the given name, which
  -- contains the given streams, and is defined by the given boolean expression,
  -- which is universally quantified.
  forallPropSpec :: String -> [Stream] -> Expr Bool -> Spec
  forallPropSpec propName propStreams propExpr =
    Spec propStreams [] [] [Copilot.Property propName (Copilot.Forall propExpr)]
  
  -- | Build a 'Spec' that contains one property with the given name, which
  -- contains the given streams, and is defined by the given boolean expression,
  -- which is existentially quantified.
  existsPropSpec :: String -> [Stream] -> Expr Bool -> Spec
  existsPropSpec propName propStreams propExpr =
    Spec propStreams [] [] [Copilot.Property propName (Copilot.Exists propExpr)]
  
  -- | Equality for 'SatResult'.
  --
  -- This is an orphan instance, so we suppress the warning that GHC would
  -- normally produce with a GHC option at the top.
  instance Eq SatResult where
    Valid   == Valid   = True
    Invalid == Invalid = True
    Unknown == Unknown = True
    _       == _       = False
  