{-# LANGUAGE DataKinds          #-}
{-# LANGUAGE DeriveAnyClass     #-}
# LANGUAGE DeriveGeneric       #
# LANGUAGE DerivingStrategies #
# LANGUAGE FlexibleInstances   #
# LANGUAGE PolyKinds           #
# LANGUAGE StandaloneDeriving #

-----------------------------------------------------------------------------
-- |
  Module       :   Echo
  Copyright    :   ( C ) 2018 ,  
-- License     :  BSD-style (see the file LICENSE)
--
  Maintainer   :     <  >
-- Stability   :  provisional
  Portability :   non - portable ( GHC extensions )
--
------------------------------------------------------------------------

module Echo
  ( mkEnv
  , prop_echoOK
  , prop_echoNParallelOK
  , prop_echoParallelOK
  )
  where

import           Data.Kind
                   (Type)
import           GHC.Generics
                   (Generic, Generic1)
import           Prelude
import           Test.QuickCheck
                   (Gen, Property, arbitrary, oneof, (===))
import           Test.QuickCheck.Monadic
                   (monadicIO)
import           UnliftIO
                   (TVar, atomically, liftIO, newTVarIO, readTVar,
                   writeTVar)

import           Test.StateMachine
import           Test.StateMachine.Types
import qualified Test.StateMachine.Types.Rank2 as Rank2

------------------------------------------------------------------------

-- | Echo API.

data Env = Env
    { _buf :: TVar (Maybe String) }

-- | Create a new environment.
mkEnv :: IO Env
mkEnv = Env <$> newTVarIO Nothing

-- | Input a string. Returns 'True' iff the buffer was empty and the given
-- string was added to it.
input :: Env -> String -> IO Bool
input (Env mBuf) str = atomically $ do
    res <- readTVar mBuf
    case res of
        Nothing -> writeTVar mBuf (Just str) >> return True
        Just _  -> return False

-- | Output the buffer contents.
output :: Env -> IO (Maybe String)
output (Env mBuf) = atomically $ do
    res <- readTVar mBuf
    writeTVar mBuf Nothing
    return res

------------------------------------------------------------------------

-- | Spec for echo.

prop_echoOK :: Property
prop_echoOK = forAllCommands smUnused Nothing $ \cmds -> monadicIO $ do
    env <- liftIO $ mkEnv
    let echoSM' = echoSM env
    (hist, _, res) <- runCommands echoSM' cmds
    prettyCommands echoSM' hist (res === Ok)

prop_echoParallelOK :: Bool -> Property
prop_echoParallelOK problem = forAllParallelCommands smUnused Nothing $ \cmds -> monadicIO $ do
    env <- liftIO $ mkEnv
    let echoSM' = echoSM env
    let n | problem   = 2
          | otherwise = 1
    prettyParallelCommands cmds =<< runParallelCommandsNTimes n echoSM' cmds

prop_echoNParallelOK :: Int -> Bool -> Property
prop_echoNParallelOK np problem = forAllNParallelCommands smUnused np $ \cmds -> monadicIO $ do
    env <- liftIO $ mkEnv
    let echoSM' = echoSM env
    let n | problem   = 2
          | otherwise = 1
    prettyNParallelCommands cmds =<< runNParallelCommandsNTimes n echoSM' cmds

smUnused :: StateMachine Model Action IO Response
smUnused = echoSM $ error "used env during command generation"

echoSM :: Env -> StateMachine Model Action IO Response
echoSM env = StateMachine
    { initModel = Empty
    -- ^ At the beginning of time nothing was received.
    , transition = mTransitions
    , precondition = mPreconditions
    , postcondition = mPostconditions
    , generator = mGenerator
    , invariant = Nothing
    , shrinker = mShrinker
    , semantics = mSemantics
    , mock = mMock
    , cleanup = noCleanup
    }
    where
      mTransitions :: Model r -> Action r -> Response r -> Model r
      mTransitions Empty   (In str) _   = Buf str
      mTransitions (Buf _) Echo     _   = Empty
      mTransitions Empty   Echo     _   = Empty
      -- TODO: qcsm will match the case below. However we don't expect this to happen!
      mTransitions (Buf str) (In _)   _ = Buf str -- Dummy response
          -- error "This shouldn't happen: input transition with full buffer"

      -- | There are no preconditions for this model.
      mPreconditions :: Model Symbolic -> Action Symbolic -> Logic
      mPreconditions _ _ = Top

      -- | Post conditions for the system.
      mPostconditions :: Model Concrete -> Action Concrete -> Response Concrete -> Logic
      mPostconditions Empty     (In _) InAck     = Top
      mPostconditions (Buf _)   (In _) ErrFull   = Top
      mPostconditions _         (In _) _         = Bot
      mPostconditions Empty     Echo   ErrEmpty  = Top
      mPostconditions Empty     Echo   _         = Bot
      mPostconditions (Buf str) Echo   (Out out) = str .== out
      mPostconditions (Buf _)   Echo   _         = Bot

      -- | Generator for symbolic actions.
      mGenerator :: Model Symbolic -> Maybe (Gen (Action Symbolic))
      mGenerator _ =  Just $ oneof
          [ In <$> arbitrary
          , return Echo
          ]

      -- | Trivial shrinker.
      mShrinker :: Model Symbolic -> Action Symbolic -> [Action Symbolic]
      mShrinker _ _ = []

  | Here we 'd do the dispatch to the actual SUT .
      mSemantics :: Action Concrete -> IO (Response Concrete)
      mSemantics (In str) = do
          success <- input env str
          return $ if success
                   then InAck
                   else ErrFull
      mSemantics Echo = maybe ErrEmpty Out <$> output env

      -- | What is the mock for?
      mMock :: Model Symbolic -> Action Symbolic -> GenSym (Response Symbolic)
      mMock Empty (In _)   = return InAck
      mMock (Buf _) (In _) = return ErrFull
      mMock Empty Echo     = return ErrEmpty
      mMock (Buf str) Echo = return (Out str)

deriving anyclass instance ToExpr (Model Concrete)

-- | The model contains the last string that was communicated in an input
-- action.
data Model (r :: Type -> Type)
    = -- | The model hasn't been initialized.
      Empty
    | -- | Last input string (a buffer with size one).
      Buf String
  deriving stock (Eq, Show, Generic)

-- | Actions supported by the system.
data Action (r :: Type -> Type)
    = -- | Input a string, which should be echoed later.
      In String
      -- | Request a string output.
    | Echo
  deriving stock (Show, Generic1)
  deriving anyclass (Rank2.Foldable, Rank2.Traversable, Rank2.Functor, CommandNames)

-- | The system gives a single type of output response, containing a string
-- with the input previously received.
data Response (r :: Type -> Type)
    = -- | Input acknowledgment.
      InAck
      -- | The previous action wasn't an input, so there is no input to echo.
      -- This is: the buffer is empty.
    | ErrEmpty
      -- | There is already a string in the buffer.
    | ErrFull
      -- | Output string.
    | Out String
  deriving stock (Show, Generic1)
  deriving anyclass (Rank2.Foldable, Rank2.Traversable, Rank2.Functor)

# LANGUAGE DataKinds          #
# LANGUAGE DeriveAnyClass     #
---------------------------------------------------------------------------
 |
 License     :  BSD-style (see the file LICENSE)

 Stability   :  provisional

----------------------------------------------------------------------
----------------------------------------------------------------------
 | Echo API.
 | Create a new environment.
 | Input a string. Returns 'True' iff the buffer was empty and the given
 string was added to it.
 | Output the buffer contents.
----------------------------------------------------------------------
 | Spec for echo.
 ^ At the beginning of time nothing was received.
 TODO: qcsm will match the case below. However we don't expect this to happen!
 Dummy response
 error "This shouldn't happen: input transition with full buffer"
 | There are no preconditions for this model.
 | Post conditions for the system.
 | Generator for symbolic actions.
 | Trivial shrinker.
 | What is the mock for?
 | The model contains the last string that was communicated in an input
 action.
 | The model hasn't been initialized.
 | Last input string (a buffer with size one).
 | Actions supported by the system.
 | Input a string, which should be echoed later.
 | Request a string output.
 | The system gives a single type of output response, containing a string
 with the input previously received.
 | Input acknowledgment.
 | The previous action wasn't an input, so there is no input to echo.
 This is: the buffer is empty.
 | There is already a string in the buffer.
 | Output string.
# LANGUAGE DeriveGeneric       #
# LANGUAGE DerivingStrategies #
# LANGUAGE FlexibleInstances   #
# LANGUAGE PolyKinds           #
# LANGUAGE StandaloneDeriving #

  Module       :   Echo
  Copyright    :   ( C ) 2018 ,  
  Maintainer   :     <  >
  Portability :   non - portable ( GHC extensions )

module Echo
  ( mkEnv
  , prop_echoOK
  , prop_echoNParallelOK
  , prop_echoParallelOK
  )
  where

import           Data.Kind
                   (Type)
import           GHC.Generics
                   (Generic, Generic1)
import           Prelude
import           Test.QuickCheck
                   (Gen, Property, arbitrary, oneof, (===))
import           Test.QuickCheck.Monadic
                   (monadicIO)
import           UnliftIO
                   (TVar, atomically, liftIO, newTVarIO, readTVar,
                   writeTVar)

import           Test.StateMachine
import           Test.StateMachine.Types
import qualified Test.StateMachine.Types.Rank2 as Rank2



data Env = Env
    { _buf :: TVar (Maybe String) }

mkEnv :: IO Env
mkEnv = Env <$> newTVarIO Nothing

input :: Env -> String -> IO Bool
input (Env mBuf) str = atomically $ do
    res <- readTVar mBuf
    case res of
        Nothing -> writeTVar mBuf (Just str) >> return True
        Just _  -> return False

output :: Env -> IO (Maybe String)
output (Env mBuf) = atomically $ do
    res <- readTVar mBuf
    writeTVar mBuf Nothing
    return res



prop_echoOK :: Property
prop_echoOK = forAllCommands smUnused Nothing $ \cmds -> monadicIO $ do
    env <- liftIO $ mkEnv
    let echoSM' = echoSM env
    (hist, _, res) <- runCommands echoSM' cmds
    prettyCommands echoSM' hist (res === Ok)

prop_echoParallelOK :: Bool -> Property
prop_echoParallelOK problem = forAllParallelCommands smUnused Nothing $ \cmds -> monadicIO $ do
    env <- liftIO $ mkEnv
    let echoSM' = echoSM env
    let n | problem   = 2
          | otherwise = 1
    prettyParallelCommands cmds =<< runParallelCommandsNTimes n echoSM' cmds

prop_echoNParallelOK :: Int -> Bool -> Property
prop_echoNParallelOK np problem = forAllNParallelCommands smUnused np $ \cmds -> monadicIO $ do
    env <- liftIO $ mkEnv
    let echoSM' = echoSM env
    let n | problem   = 2
          | otherwise = 1
    prettyNParallelCommands cmds =<< runNParallelCommandsNTimes n echoSM' cmds

smUnused :: StateMachine Model Action IO Response
smUnused = echoSM $ error "used env during command generation"

echoSM :: Env -> StateMachine Model Action IO Response
echoSM env = StateMachine
    { initModel = Empty
    , transition = mTransitions
    , precondition = mPreconditions
    , postcondition = mPostconditions
    , generator = mGenerator
    , invariant = Nothing
    , shrinker = mShrinker
    , semantics = mSemantics
    , mock = mMock
    , cleanup = noCleanup
    }
    where
      mTransitions :: Model r -> Action r -> Response r -> Model r
      mTransitions Empty   (In str) _   = Buf str
      mTransitions (Buf _) Echo     _   = Empty
      mTransitions Empty   Echo     _   = Empty

      mPreconditions :: Model Symbolic -> Action Symbolic -> Logic
      mPreconditions _ _ = Top

      mPostconditions :: Model Concrete -> Action Concrete -> Response Concrete -> Logic
      mPostconditions Empty     (In _) InAck     = Top
      mPostconditions (Buf _)   (In _) ErrFull   = Top
      mPostconditions _         (In _) _         = Bot
      mPostconditions Empty     Echo   ErrEmpty  = Top
      mPostconditions Empty     Echo   _         = Bot
      mPostconditions (Buf str) Echo   (Out out) = str .== out
      mPostconditions (Buf _)   Echo   _         = Bot

      mGenerator :: Model Symbolic -> Maybe (Gen (Action Symbolic))
      mGenerator _ =  Just $ oneof
          [ In <$> arbitrary
          , return Echo
          ]

      mShrinker :: Model Symbolic -> Action Symbolic -> [Action Symbolic]
      mShrinker _ _ = []

  | Here we 'd do the dispatch to the actual SUT .
      mSemantics :: Action Concrete -> IO (Response Concrete)
      mSemantics (In str) = do
          success <- input env str
          return $ if success
                   then InAck
                   else ErrFull
      mSemantics Echo = maybe ErrEmpty Out <$> output env

      mMock :: Model Symbolic -> Action Symbolic -> GenSym (Response Symbolic)
      mMock Empty (In _)   = return InAck
      mMock (Buf _) (In _) = return ErrFull
      mMock Empty Echo     = return ErrEmpty
      mMock (Buf str) Echo = return (Out str)

deriving anyclass instance ToExpr (Model Concrete)

data Model (r :: Type -> Type)
      Empty
      Buf String
  deriving stock (Eq, Show, Generic)

data Action (r :: Type -> Type)
      In String
    | Echo
  deriving stock (Show, Generic1)
  deriving anyclass (Rank2.Foldable, Rank2.Traversable, Rank2.Functor, CommandNames)

data Response (r :: Type -> Type)
      InAck
    | ErrEmpty
    | ErrFull
    | Out String
  deriving stock (Show, Generic1)
  deriving anyclass (Rank2.Foldable, Rank2.Traversable, Rank2.Functor)
