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