{-# LANGUAGE DeriveFunctor        #-}
{-# LANGUAGE FlexibleContexts     #-}
{-# LANGUAGE GADTs                #-}
{-# LANGUAGE KindSignatures       #-}
{-# LANGUAGE StandaloneDeriving   #-}
{-# LANGUAGE UndecidableInstances #-}

-----------------------------------------------------------------------------
-- |
-- Module      :  Test.StateMachine.Internal.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)
--
-- This module exports some types that are used internally by the library.
--
-----------------------------------------------------------------------------

module Test.StateMachine.Internal.Types
  ( Program(..)
  , programLength
  , ParallelProgram(..)
  , Pid(..)
  , Fork(..)
  , Internal(..)
  ) where

import           Data.Typeable
                   (Typeable)
import           Text.Read
                   (Lexeme(Ident), lexP, parens, prec, readPrec, step)

import           Test.StateMachine.Types
                   (Untyped(Untyped))
import           Test.StateMachine.Types.References

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

-- | A (sequential) program is an abstract datatype representing a list
--   of actions.
--
-- The idea is that the user shows how to generate, shrink, execute and
-- modelcheck individual actions, and then the below combinators lift
-- those things to whole programs.
newtype Program act = Program { unProgram :: [Internal act] }

instance Eq (Internal act) => Eq (Program act) where
  Program acts1 == Program acts2 = acts1 == acts2

instance Monoid (Program act) where
  mempty                                = Program []
  Program acts1 `mappend` Program acts2 = Program (acts1 ++ acts2)

deriving instance Show (Untyped act) => Show (Program act)
deriving instance Read (Untyped act) => Read (Program act)

-- | Returns the number of actions in a program.
programLength :: Program act -> Int
programLength = length . unProgram

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

-- | A parallel program is an abstract datatype that represents three
--   sequences of actions; a sequential prefix and two parallel
--   suffixes. Analogous to the sequential case, the user shows how to
--   generate, shrink, execute and modelcheck individual actions, and
--   then the below combinators lift those things to whole parallel
--   programs.
newtype ParallelProgram act = ParallelProgram
  { unParallelProgram :: Fork (Program act) }

deriving instance Show (Untyped act) => Show (ParallelProgram act)
deriving instance Read (Untyped act) => Read (ParallelProgram act)

-- | Forks are used to represent parallel programs.
data Fork a = Fork a a a
  deriving (Eq, Functor, Show, Ord, Read)

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

-- | An internal action is an action together with the symbolic variable
--   that will hold its result.
data Internal (act :: (* -> *) -> * -> *) where
  Internal :: (Show resp, Typeable resp) =>
    act Symbolic resp -> Symbolic resp -> Internal act

instance Eq (Untyped act) => Eq (Internal act) where
  Internal a1 _ == Internal a2 _ = Untyped a1 == Untyped a2

instance Show (Untyped act) => Show (Internal act) where
  showsPrec p (Internal action v) = showParen (p > appPrec) $
    showString "Internal " .
    showsPrec (appPrec + 1) (Untyped action) .
    showString " " .
    showsPrec (appPrec + 1) v
    where
      appPrec = 10

instance Read (Untyped act) => Read (Internal act) where
  readPrec = parens $
    prec appPrec $ do
      Ident "Internal" <- lexP
      Untyped action <- step readPrec
      v <- step readPrec
      return (Internal action v)
    where
      appPrec = 10

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

-- | A process id.
newtype Pid = Pid Int
  deriving (Eq, Show)