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