{-# LANGUAGE DeriveFoldable             #-}
{-# LANGUAGE DeriveFunctor              #-}
{-# LANGUAGE DeriveTraversable          #-}
{-# LANGUAGE FlexibleContexts           #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE MonoLocalBinds             #-}
{-# LANGUAGE Rank2Types                 #-}
{-# LANGUAGE StandaloneDeriving         #-}
{-# LANGUAGE UndecidableInstances       #-}

-----------------------------------------------------------------------------
-- |
-- Module      :  Test.StateMachine.Types
-- Copyright   :  (C) 2017, ATS Advanced Telematic Systems GmbH
-- License     :  BSD-style (see the file LICENSE)
--
-- Maintainer  :  Stevan Andjelkovic <stevan@advancedtelematic.com>
-- Stability   :  provisional
-- Portability :  non-portable (GHC extensions)
--
-----------------------------------------------------------------------------

module Test.StateMachine.Types
  ( StateMachine(..)
  , Command(..)
  , Commands(..)
  , lengthCommands
  , ParallelCommandsF(..)
  , ParallelCommands
  , Pair(..)
  , fromPair
  , toPair
  , Reason(..)
  , module Test.StateMachine.Types.Environment
  , module Test.StateMachine.Types.GenSym
  , module Test.StateMachine.Types.History
  , module Test.StateMachine.Types.References
  ) where

import           Data.Functor.Classes
                   (Ord1, Show1)
import           Data.Matrix
                   (Matrix)
import           Data.Semigroup
                   (Semigroup)
import           Data.Set
                   (Set)
import           Prelude
import           Test.QuickCheck
                   (Gen, Property)

import           Test.StateMachine.Logic
import           Test.StateMachine.Types.Environment
import           Test.StateMachine.Types.GenSym
import           Test.StateMachine.Types.History
import           Test.StateMachine.Types.References

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

data StateMachine model cmd m resp = StateMachine
  { initModel      :: forall r. model r
  , transition     :: forall r. (Show1 r, Ord1 r) => model r -> cmd r -> resp r -> model r
  , precondition   :: model Symbolic -> cmd Symbolic -> Logic
  , postcondition  :: model Concrete -> cmd Concrete -> resp Concrete -> Logic
  , spostcondition :: Maybe (model Symbolic -> cmd Symbolic -> resp Symbolic -> Logic)
  , invariant      :: Maybe (model Concrete -> Logic)
  , generator      :: model Symbolic -> Gen (cmd Symbolic)
  , distribution   :: Maybe (Matrix Int)
  , shrinker       :: cmd Symbolic -> [cmd Symbolic]
  , semantics      :: cmd Concrete -> m (resp Concrete)
  , runner         :: m Property -> IO Property
  , mock           :: model Symbolic -> cmd Symbolic -> GenSym (resp Symbolic)
  }

data Command cmd = Command !(cmd Symbolic) !(Set Var)

deriving instance Show (cmd Symbolic) => Show (Command cmd)

newtype Commands cmd = Commands
  { unCommands :: [Command cmd] }
  deriving (Semigroup, Monoid)

deriving instance Show (cmd Symbolic) => Show (Commands cmd)

lengthCommands :: Commands cmd -> Int
lengthCommands = length . unCommands

data Reason
  = Ok
  | PreconditionFailed
  | PostconditionFailed String
  | InvariantBroken String
  | ExceptionThrown String
  deriving (Eq, Show)

data ParallelCommandsF t cmd = ParallelCommands
  { prefix   :: !(Commands cmd)
  , suffixes :: [t (Commands cmd)]
  }

deriving instance (Show (cmd Symbolic), Show (t (Commands cmd))) =>
  Show (ParallelCommandsF t cmd)

data Pair a = Pair
  { proj1 :: !a
  , proj2 :: !a
  }
  deriving (Eq, Ord, Show, Functor, Foldable, Traversable)

fromPair :: Pair a -> (a, a)
fromPair (Pair x y) = (x, y)

toPair :: (a, a) -> Pair a
toPair (x, y) = Pair x y

type ParallelCommands = ParallelCommandsF Pair