-- | This module allows to prove statements in tasty.
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE TypeApplications #-}
module Test.Tasty.SBV
 ( testStatement
 , SbvPrintBase(..)
 , SbvPrintRealPrec(..)
 , SbvValidateModel(..)
 , SbvTranscript(..)
 , SbvVerbose(..)
 , SbvRedirectVerbose(..)
 , SbvSolver(..)
 , SbvQuickCheck(..)
 , FS(..)
 ) where

import           Data.SBV
import           Data.Tagged
import           Data.Typeable
import           Test.Tasty.Providers
import qualified Test.Tasty.Providers as T
import           Test.Tasty.Options
import           Test.Tasty.QuickCheck (QC(QC), Testable(property))

data FS = forall a . (Testable a, Provable a) => FS a
  deriving (Typeable)

-- | Create a test that attempts to proves a statement.
--   When checking via QuickCheck is requested, tasty-quickcheck options
--   will be respected.
testStatement :: (Testable a, Provable a) => TestName -> a -> TestTree
testStatement n = singleTest n . FS

-- | The base to use for integer literal printing (2, 10, and 16 are supported).
newtype SbvPrintBase = SbvPrintBase Int
  deriving (Eq, Ord, Show, Typeable)

instance IsOption SbvPrintBase where
  defaultValue = SbvPrintBase 10
  parseValue = fmap SbvPrintBase . safeRead
  optionName = return "sbv-print-base"
  optionHelp = return "Print integral literals in this base (2, 10, and 16 are supported.)"

-- | The precision to print real values with (SReal, default is 16).
newtype SbvPrintRealPrec = SbvPrintRealPrec Int
  deriving (Eq, Ord, Show, Typeable)

instance IsOption SbvPrintRealPrec where
  defaultValue = SbvPrintRealPrec 16
  parseValue = fmap SbvPrintRealPrec . safeRead
  optionName = return "sbv-print-real-prec"
  optionHelp = return "Print algebraic real values with this precision. (SReal, default: 16)"

-- | If 'sbv' should attempt to validate the model it gets back from the solver.
newtype SbvValidateModel = SbvValidateModel Bool
  deriving (Eq, Ord, Show, Typeable)

instance IsOption SbvValidateModel where
  defaultValue = SbvValidateModel False
  parseValue = fmap SbvValidateModel . safeReadBool
  optionName = return "sbv-validate-model"
  optionHelp = return "If SBV should attempt to validate the model it gets back from the solver."

-- | Where and if 'sbv' should save a replayble transcript.
newtype SbvTranscript = SbvTranscript (Maybe FilePath)
  deriving (Eq, Ord, Show, Typeable)

instance IsOption SbvTranscript  where
  defaultValue = SbvTranscript Nothing
  parseValue = Just . SbvTranscript . Just
  optionName = return "sbv-transcript"
  optionHelp = return "Where SBV should save a replayble transcript if set."

-- | Verbose debug output.
newtype SbvVerbose = SbvVerbose Bool
  deriving (Eq, Ord, Show, Typeable)

instance IsOption SbvVerbose where
  defaultValue = SbvVerbose False
  parseValue = fmap SbvVerbose . safeReadBool
  optionName = return "sbv-verbose"
  optionHelp = return "Enable verbose debug output."

-- | If we should save the verbose output to a file instead of printing to stdout, and what it is.
newtype SbvRedirectVerbose = SbvRedirectVerbose (Maybe FilePath)
  deriving (Eq, Ord, Show, Typeable)

instance IsOption SbvRedirectVerbose where
  defaultValue = SbvRedirectVerbose Nothing
  parseValue = Just . SbvRedirectVerbose . Just
  optionName = return "sbv-verbose-save"
  optionHelp = return "Where we should save verbose output, instead of printing to stdout."

-- | Which solver 'sbv' shoul use.
--   The current options are z3 (the default), yices, boolector, cvc4, mathsat, and abc.
newtype SbvSolver = SbvSolver Solver
  deriving (Show, Typeable)

instance IsOption SbvSolver where
  defaultValue = SbvSolver Z3
  parseValue = \case
    "z3"        -> Just $ SbvSolver Z3
    "yices"     -> Just $ SbvSolver Yices
    "boolector" -> Just $ SbvSolver Boolector
    "cvc4"      -> Just $ SbvSolver CVC4
    "mathsat"   -> Just $ SbvSolver MathSAT
    "abc"       -> Just $ SbvSolver ABC
    _           -> Nothing
  optionName = return "sbv-solver"
  optionHelp = return "The backend solver to use, from z3 (the default), yices, boolector, cvc4, mathsat, and abc."

-- | Check properties with QuickCheck instead of a solver.
--   This allows basic checking of the statement even without a solver installed on the system.
newtype SbvQuickCheck = SbvQuickCheck Bool
  deriving (Eq, Ord, Show, Typeable)

instance IsOption SbvQuickCheck where
  defaultValue = SbvQuickCheck False
  parseValue = fmap SbvQuickCheck . safeReadBool
  optionName = return "sbv-quickcheck"
  optionHelp = return "Check properties with QuickCheck instead of a solver."

instance T.IsTest FS where
  testOptions = pure $
    [ Option (Proxy :: Proxy SbvPrintBase)
    , Option (Proxy :: Proxy SbvPrintRealPrec)
    , Option (Proxy :: Proxy SbvValidateModel)
    , Option (Proxy :: Proxy SbvTranscript)
    , Option (Proxy :: Proxy SbvVerbose)
    , Option (Proxy :: Proxy SbvRedirectVerbose)
    , Option (Proxy :: Proxy SbvSolver)
    , Option (Proxy :: Proxy SbvQuickCheck)
    ] ++ (unTagged $ testOptions @QC)

  run opts (FS thm) yieldProgress =
      if qc
        then run opts (QC $ property thm) yieldProgress
        else beTheReader
    where
      SbvQuickCheck            qc    = lookupOption opts
      SbvPrintBase            pbase = lookupOption opts
      SbvPrintRealPrec        pprec = lookupOption opts
      SbvValidateModel        vm    = lookupOption opts
      SbvTranscript           mt    = lookupOption opts
      SbvVerbose              v     = lookupOption opts
      SbvRedirectVerbose      rv    = lookupOption opts
      SbvSolver               slv   = lookupOption opts
      config = (case slv of
                  Z3        -> z3
                  Yices     -> yices
                  Boolector -> boolector
                  CVC4      -> cvc4
                  MathSAT   -> mathSAT
                  ABC       -> abc
               ) { verbose         = v
                 , printBase       = pbase
                 , printRealPrec   = pprec
                 , validateModel   = vm
                 , transcript      = mt
                 , redirectVerbose = rv
                 }
      beTheReader = do
        tres@(ThmResult sres) <- proveWith config thm
        case sres of
          Unsatisfiable _ _ -> pure $ testPassed ""
          _ -> pure $ testFailed $ show tres