{-# 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(..)
  , parallelProgramLength
  , parallelProgramToList
  , parallelProgramFromList
  , parallelProgramAsList
  , flattenParallelProgram
  , Pid(..)
  , Internal(..)
  ) where

import           Data.Bifunctor
                   (bimap)
import           Data.Monoid
                   ((<>))
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

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

data ParallelProgram act
  = ParallelProgram (Program act) [(Program act, Program act)]

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

parallelProgramLength :: ParallelProgram act -> Int
parallelProgramLength (ParallelProgram prefix suffixes) =
  programLength prefix +
  programLength (mconcat (parallelProgramToList suffixes))

parallelProgramFromList :: [Program act] -> [(Program act, Program act)]
parallelProgramFromList
  = map (\prog -> bimap Program Program
                        (splitAt (programLength prog `div` 2) (unProgram prog)))

parallelProgramToList :: [(Program act, Program act)] -> [Program act]
parallelProgramToList = map (\(prog1, prog2) -> prog1 <> prog2)

parallelProgramAsList
  :: ([Program act] -> [Program act])
  -> [(Program act, Program act)]
  -> [(Program act, Program act)]
parallelProgramAsList f = parallelProgramFromList . f . parallelProgramToList

flattenParallelProgram :: ParallelProgram act -> Program act
flattenParallelProgram (ParallelProgram prefix suffixes)
  = prefix <> mconcat (parallelProgramToList suffixes)

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

-- | 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)