{-# LANGUAGE DataKinds #-} {-# LANGUAGE DeriveFunctor #-} {-# LANGUAGE ExplicitNamespaces #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE PolyKinds #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeInType #-} {-# LANGUAGE TypeOperators #-} {-# 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 -- Stability : provisional -- Portability : non-portable (GHC extensions) -- -- This module exports some types that are used internally by the library. -- ----------------------------------------------------------------------------- module Test.StateMachine.Internal.Types ( IntRef(..) , Pid(..) , Ref(..) , ConstIntRef , IntRefed(..) , Fork(..) , showResponse_ , MayResponse_ ) where import Data.Kind (Type) import Data.Monoid ((<>)) import Data.Singletons.Prelude (type (@@), TyFun) import Data.Typeable (Typeable) import Text.PrettyPrint.ANSI.Leijen (Pretty, align, dot, indent, int, pretty, text, underline, vsep, (<+>)) import Test.StateMachine.Internal.Types.IntRef import Test.StateMachine.Types ------------------------------------------------------------------------ -- | Type-level function that maybe returns a reference. type family MayResponse_ (refs :: TyFun ix k -> Type) (resp :: Response ix) :: k where MayResponse_ refs ('Response t) = () MayResponse_ refs ('Reference i) = refs @@ i -- | Internal untyped commands. data IntRefed (f :: Signature ix) where IntRefed :: ( Show (GetResponse_ resp) , Typeable (Response_ ConstIntRef resp) , Typeable resp ) => f ConstIntRef resp -> MayResponse_ ConstIntRef resp -> IntRefed f instance (IxFunctor cmd, ShowCmd cmd, HasResponse cmd) => Show (IntRefed cmd) where show (IntRefed cmd miref) = showCmd (ifmap (\ _ r -> "(" ++ show r ++ ")") cmd) ++ " " ++ case response cmd of SResponse -> "()" SReference _ -> "(" ++ show miref ++ ")" -- | Forks are used to represent parallel programs. They have a sequential -- prefix (the middle argument of the constructor), and two parallel suffixes -- (the left- and right-most argument of the constructor). data Fork a = Fork a a a deriving (Eq, Functor, Show, Ord, Read) instance Pretty a => Pretty (Fork a) where pretty (Fork l p r) = vsep [ underline $ text "Prefix:" , indent 5 $ pretty p , underline $ text "Parallel:" , indent 2 $ int 1 <> dot <+> align (pretty l) , indent 2 $ int 2 <> dot <+> align (pretty r) ] ------------------------------------------------------------------------ -- | Show function for 'Response_'. showResponse_ :: Show (GetResponse_ resp) => SResponse ix resp -> Response_ ConstIntRef resp -> String showResponse_ SResponse = show showResponse_ (SReference _) = showRef