{-# LANGUAGE DataKinds           #-}
{-# LANGUAGE FlexibleContexts    #-}
{-# LANGUAGE GADTs               #-}
{-# LANGUAGE NamedFieldPuns      #-}
{-# LANGUAGE PolyKinds           #-}
{-# LANGUAGE RankNTypes          #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeOperators       #-}

module Network.TypedProtocol.Stateful.ReqResp.Codec where

import           Data.Kind (Type)
import           Data.Singletons.Decide
import           Data.Typeable
import           Network.TypedProtocol.Core
import           Network.TypedProtocol.PingPong.Codec (decodeTerminatedFrame)
import           Network.TypedProtocol.Stateful.Codec
import           Network.TypedProtocol.Stateful.ReqResp.Type

data Some (f :: k -> Type) where
    Some :: Typeable a => f a -> Some f


-- | Codec polymorphic in the RPC (e.g. `req` type)
--
codecReqResp
  :: forall req m. Monad m
  => (forall resp. req resp -> String)
  -- ^ encode `req resp`
  -> (String -> Maybe (Some req))
  -- ^ decode `req resp`
  -> (forall resp. req resp -> resp -> String)
  -- ^ encode resp
  -> (forall resp. req resp -> String -> Maybe resp)
  -- ^ decode resp
  -> Codec (ReqResp req) CodecFailure State m String
codecReqResp :: forall (req :: * -> *) (m :: * -> *).
Monad m =>
(forall resp. req resp -> String)
-> (String -> Maybe (Some req))
-> (forall resp. req resp -> resp -> String)
-> (forall resp. req resp -> String -> Maybe resp)
-> Codec (ReqResp req) CodecFailure State m String
codecReqResp forall resp. req resp -> String
encodeReq String -> Maybe (Some req)
decodeReq forall resp. req resp -> resp -> String
encodeResp forall resp. req resp -> String -> Maybe resp
decodeResp =
    Codec { State st -> Message (ReqResp req) st st' -> String
forall (st :: ReqResp req) (st' :: ReqResp req).
(StateTokenI st, ActiveState st) =>
State st -> Message (ReqResp req) st st' -> String
forall (st :: ReqResp req) (st' :: ReqResp req).
State st -> Message (ReqResp req) st st' -> String
encode :: forall (st :: ReqResp req) (st' :: ReqResp req).
State st -> Message (ReqResp req) st st' -> String
encode :: forall (st :: ReqResp req) (st' :: ReqResp req).
(StateTokenI st, ActiveState st) =>
State st -> Message (ReqResp req) st st' -> String
encode, StateToken st
-> State st
-> m (DecodeStep String CodecFailure m (SomeMessage st))
forall (st :: ReqResp req).
ActiveState st =>
StateToken st
-> State st
-> m (DecodeStep String CodecFailure m (SomeMessage st))
decode :: forall (st :: ReqResp req).
ActiveState st =>
StateToken st
-> State st
-> m (DecodeStep String CodecFailure m (SomeMessage st))
decode :: forall (st :: ReqResp req).
ActiveState st =>
StateToken st
-> State st
-> m (DecodeStep String CodecFailure m (SomeMessage st))
decode }
  where
    encode :: State st
           -> Message (ReqResp req) st st'
           -> String
    encode :: forall (st :: ReqResp req) (st' :: ReqResp req).
State st -> Message (ReqResp req) st st' -> String
encode State st
_ (MsgReq req resp
req)       = String
"MsgReq " String -> String -> String
forall a. [a] -> [a] -> [a]
++ req resp -> String
forall resp. req resp -> String
encodeReq req resp
req String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\n"
    encode State st
_ Message (ReqResp req) st st'
R:MessageReqRespfromto req st st'
MsgDone            = String
"MsgDone\n"
    encode (StateBusy req result
req) (MsgResp resp
resp) = String
"MsgResp " String -> String -> String
forall a. [a] -> [a] -> [a]
++ req result -> result -> String
forall resp. req resp -> resp -> String
encodeResp req result
req result
resp
resp String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\n"

    decode :: forall (st :: ReqResp req).
              ActiveState st
           => StateToken st
           -> State st
           -> m (DecodeStep String CodecFailure m (SomeMessage st))
    decode :: forall (st :: ReqResp req).
ActiveState st =>
StateToken st
-> State st
-> m (DecodeStep String CodecFailure m (SomeMessage st))
decode StateToken st
stok State st
state =
      Char
-> (String
    -> Maybe String
    -> DecodeStep String CodecFailure m (SomeMessage st))
-> m (DecodeStep String CodecFailure m (SomeMessage st))
forall (m :: * -> *) a.
Monad m =>
Char
-> (String -> Maybe String -> DecodeStep String CodecFailure m a)
-> m (DecodeStep String CodecFailure m a)
decodeTerminatedFrame Char
'\n' ((String
  -> Maybe String
  -> DecodeStep String CodecFailure m (SomeMessage st))
 -> m (DecodeStep String CodecFailure m (SomeMessage st)))
-> (String
    -> Maybe String
    -> DecodeStep String CodecFailure m (SomeMessage st))
-> m (DecodeStep String CodecFailure m (SomeMessage st))
forall a b. (a -> b) -> a -> b
$ \String
str Maybe String
trailing ->
        case (StateToken st
SReqResp st
stok, State st
state, (Char -> Bool) -> String -> (String, String)
forall a. (a -> Bool) -> [a] -> ([a], [a])
break (Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
==Char
' ') String
str) of
          (SReqResp st
SingIdle, State st
StateIdle, (String
"MsgReq", String
str'))
            |  Just (Some req a
req) <- String -> Maybe (Some req)
decodeReq String
str'
            -> SomeMessage st
-> Maybe String
-> DecodeStep String CodecFailure m (SomeMessage st)
forall bytes failure (m :: * -> *) a.
a -> Maybe bytes -> DecodeStep bytes failure m a
DecodeDone (Message (ReqResp req) st ('StBusy a) -> SomeMessage st
forall ps (st :: ps) (st' :: ps).
(StateTokenI st, StateTokenI st', ActiveState st) =>
Message ps st st' -> SomeMessage st
SomeMessage (req a -> Message (ReqResp req) 'StIdle ('StBusy a)
forall resp (req :: * -> *).
Typeable resp =>
req resp -> Message (ReqResp req) 'StIdle ('StBusy resp)
MsgReq req a
req)) Maybe String
trailing
          (SReqResp st
SingIdle, State st
StateIdle, (String
"MsgDone", String
""))
            -> SomeMessage st
-> Maybe String
-> DecodeStep String CodecFailure m (SomeMessage st)
forall bytes failure (m :: * -> *) a.
a -> Maybe bytes -> DecodeStep bytes failure m a
DecodeDone (Message (ReqResp req) st 'StDone -> SomeMessage st
forall ps (st :: ps) (st' :: ps).
(StateTokenI st, StateTokenI st', ActiveState st) =>
Message ps st st' -> SomeMessage st
SomeMessage Message (ReqResp req) st 'StDone
Message (ReqResp req) 'StIdle 'StDone
forall (req :: * -> *). Message (ReqResp req) 'StIdle 'StDone
MsgDone) Maybe String
trailing
          (SReqResp st
SingBusy, StateBusy req result
req, (String
"MsgResp", String
str'))
            -- note that we need `req` to decode response of the given type
            |  Just result
resp <- req result -> String -> Maybe result
forall resp. req resp -> String -> Maybe resp
decodeResp req result
req String
str'
            -> SomeMessage st
-> Maybe String
-> DecodeStep String CodecFailure m (SomeMessage st)
forall bytes failure (m :: * -> *) a.
a -> Maybe bytes -> DecodeStep bytes failure m a
DecodeDone (Message (ReqResp req) st 'StIdle -> SomeMessage st
forall ps (st :: ps) (st' :: ps).
(StateTokenI st, StateTokenI st', ActiveState st) =>
Message ps st st' -> SomeMessage st
SomeMessage (result -> Message (ReqResp req) ('StBusy result) 'StIdle
forall resp (req :: * -> *).
Typeable resp =>
resp -> Message (ReqResp req) ('StBusy resp) 'StIdle
MsgResp result
resp)) Maybe String
trailing
          (SReqResp st
_, State st
_, (String, String)
_) -> CodecFailure -> DecodeStep String CodecFailure m (SomeMessage st)
forall bytes failure (m :: * -> *) a.
failure -> DecodeStep bytes failure m a
DecodeFail CodecFailure
failure
            where failure :: CodecFailure
failure = String -> CodecFailure
CodecFailure (String
"unexpected server message: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
str)


data Bytes where
    Bytes :: Message (ReqResp FileAPI) st st' -> Bytes

-- | An identity codec which wraps messages into `AnyMessage`.
--
codecReqRespId
  :: forall m.
     Applicative m
  => (forall (res1 :: Type) (res2 :: Type).
           (Typeable res1, Typeable res2)
        => Proxy res1
        -> Proxy res2
        -> Maybe (res1 :~: res2)
     )
  -> Codec FileRPC String State m Bytes
codecReqRespId :: forall (m :: * -> *).
Applicative m =>
(forall res1 res2.
 (Typeable res1, Typeable res2) =>
 Proxy res1 -> Proxy res2 -> Maybe (res1 :~: res2))
-> Codec FileRPC String State m Bytes
codecReqRespId forall res1 res2.
(Typeable res1, Typeable res2) =>
Proxy res1 -> Proxy res2 -> Maybe (res1 :~: res2)
eqRespTypes = Codec { State st -> Message FileRPC st st' -> Bytes
forall {p} {st :: FileRPC} {st' :: FileRPC}.
p -> Message FileRPC st st' -> Bytes
forall (st :: FileRPC) (st' :: FileRPC).
(StateTokenI st, ActiveState st) =>
State st -> Message FileRPC st st' -> Bytes
encode :: forall (st :: FileRPC) (st' :: FileRPC).
(StateTokenI st, ActiveState st) =>
State st -> Message FileRPC st st' -> Bytes
encode :: forall {p} {st :: FileRPC} {st' :: FileRPC}.
p -> Message FileRPC st st' -> Bytes
encode, StateToken st
-> State st -> m (DecodeStep Bytes String m (SomeMessage st))
forall (st :: FileRPC).
ActiveState st =>
StateToken st
-> State st -> m (DecodeStep Bytes String m (SomeMessage st))
decode :: forall (st :: FileRPC).
ActiveState st =>
StateToken st
-> State st -> m (DecodeStep Bytes String m (SomeMessage st))
decode :: forall (st :: FileRPC).
ActiveState st =>
StateToken st
-> State st -> m (DecodeStep Bytes String m (SomeMessage st))
decode }
  where
    encode :: p -> Message FileRPC st st' -> Bytes
encode p
_ = Message FileRPC st st' -> Bytes
forall (st :: FileRPC) (st' :: FileRPC).
Message FileRPC st st' -> Bytes
Bytes

    decode :: forall (st :: ReqResp FileAPI).
              ActiveState st
           => StateToken st
           -> State st
           -> m (DecodeStep Bytes String m (SomeMessage st))
    decode :: forall (st :: FileRPC).
ActiveState st =>
StateToken st
-> State st -> m (DecodeStep Bytes String m (SomeMessage st))
decode StateToken st
stok State st
state = DecodeStep Bytes String m (SomeMessage st)
-> m (DecodeStep Bytes String m (SomeMessage st))
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (DecodeStep Bytes String m (SomeMessage st)
 -> m (DecodeStep Bytes String m (SomeMessage st)))
-> DecodeStep Bytes String m (SomeMessage st)
-> m (DecodeStep Bytes String m (SomeMessage st))
forall a b. (a -> b) -> a -> b
$ (Maybe Bytes -> m (DecodeStep Bytes String m (SomeMessage st)))
-> DecodeStep Bytes String m (SomeMessage st)
forall bytes failure (m :: * -> *) a.
(Maybe bytes -> m (DecodeStep bytes failure m a))
-> DecodeStep bytes failure m a
DecodePartial ((Maybe Bytes -> m (DecodeStep Bytes String m (SomeMessage st)))
 -> DecodeStep Bytes String m (SomeMessage st))
-> (Maybe Bytes -> m (DecodeStep Bytes String m (SomeMessage st)))
-> DecodeStep Bytes String m (SomeMessage st)
forall a b. (a -> b) -> a -> b
$ \Maybe Bytes
bytes -> DecodeStep Bytes String m (SomeMessage st)
-> m (DecodeStep Bytes String m (SomeMessage st))
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (DecodeStep Bytes String m (SomeMessage st)
 -> m (DecodeStep Bytes String m (SomeMessage st)))
-> DecodeStep Bytes String m (SomeMessage st)
-> m (DecodeStep Bytes String m (SomeMessage st))
forall a b. (a -> b) -> a -> b
$
      case (StateToken st
SReqResp st
stok, State st
state, Maybe Bytes
bytes) of
        (SReqResp st
SingIdle, State st
StateIdle, Just (Bytes msg :: Message FileRPC st st'
msg@Message FileRPC st st'
R:MessageReqRespfromto FileAPI st st'
MsgDone))
          -> SomeMessage st
-> Maybe Bytes -> DecodeStep Bytes String m (SomeMessage st)
forall bytes failure (m :: * -> *) a.
a -> Maybe bytes -> DecodeStep bytes failure m a
DecodeDone (Message FileRPC st st' -> SomeMessage st
forall ps (st :: ps) (st' :: ps).
(StateTokenI st, StateTokenI st', ActiveState st) =>
Message ps st st' -> SomeMessage st
SomeMessage Message FileRPC st st'
Message FileRPC st st'
msg) Maybe Bytes
forall a. Maybe a
Nothing
        (SReqResp st
SingIdle, State st
StateIdle, Just (Bytes msg :: Message FileRPC st st'
msg@MsgReq{}))
          -> SomeMessage st
-> Maybe Bytes -> DecodeStep Bytes String m (SomeMessage st)
forall bytes failure (m :: * -> *) a.
a -> Maybe bytes -> DecodeStep bytes failure m a
DecodeDone (Message FileRPC st st' -> SomeMessage st
forall ps (st :: ps) (st' :: ps).
(StateTokenI st, StateTokenI st', ActiveState st) =>
Message ps st st' -> SomeMessage st
SomeMessage Message FileRPC st st'
Message FileRPC st st'
msg) Maybe Bytes
forall a. Maybe a
Nothing
        (SReqResp st
SingBusy, StateBusy FileAPI result
req, Just (Bytes msg :: Message FileRPC st st'
msg@MsgResp{}))
          -- the codec needs to verify that response type of `req` and `msg` agrees
          |  Just result :~: resp
Refl <- Proxy result -> Proxy resp -> Maybe (result :~: resp)
forall res1 res2.
(Typeable res1, Typeable res2) =>
Proxy res1 -> Proxy res2 -> Maybe (res1 :~: res2)
eqRespTypes (FileAPI result -> Proxy result
forall resp. FileAPI resp -> Proxy resp
reqRespType FileAPI result
req) (Message FileRPC ('StBusy resp) 'StIdle -> Proxy resp
forall {k} (resp :: k).
Message FileRPC ('StBusy resp) 'StIdle -> Proxy resp
msgRespType Message FileRPC st st'
Message FileRPC ('StBusy resp) 'StIdle
msg)
          -> SomeMessage st
-> Maybe Bytes -> DecodeStep Bytes String m (SomeMessage st)
forall bytes failure (m :: * -> *) a.
a -> Maybe bytes -> DecodeStep bytes failure m a
DecodeDone (Message FileRPC st st' -> SomeMessage st
forall ps (st :: ps) (st' :: ps).
(StateTokenI st, StateTokenI st', ActiveState st) =>
Message ps st st' -> SomeMessage st
SomeMessage Message FileRPC st st'
Message FileRPC st st'
msg) Maybe Bytes
forall a. Maybe a
Nothing

        (SReqResp st
SingDone, State st
_, Maybe Bytes
_) -> StateToken 'StDone -> forall a. a
forall ps (st :: ps).
(StateAgency st ~ 'NobodyAgency, ActiveState st) =>
StateToken st -> forall a. a
notActiveState StateToken st
StateToken 'StDone
stok
        (SReqResp st
_, State st
_, Maybe Bytes
Nothing) -> String -> DecodeStep Bytes String m (SomeMessage st)
forall bytes failure (m :: * -> *) a.
failure -> DecodeStep bytes failure m a
DecodeFail String
"no bytes"
        (SReqResp st
_, State st
_, Maybe Bytes
_) -> String -> DecodeStep Bytes String m (SomeMessage st)
forall bytes failure (m :: * -> *) a.
failure -> DecodeStep bytes failure m a
DecodeFail String
"no matching message"

    msgRespType :: forall resp. Message (ReqResp FileAPI) (StBusy resp) StIdle
                -> Proxy resp
    msgRespType :: forall {k} (resp :: k).
Message FileRPC ('StBusy resp) 'StIdle -> Proxy resp
msgRespType (MsgResp resp
_) = Proxy resp
forall {k} (t :: k). Proxy t
Proxy

    reqRespType :: forall resp. FileAPI resp -> Proxy resp
    reqRespType :: forall resp. FileAPI resp -> Proxy resp
reqRespType FileAPI resp
_ = Proxy resp
forall {k} (t :: k). Proxy t
Proxy