typed-protocols: added application specific singletons for protocol s…

…tates

We still have `singletons` as a dependency though.

typed-protocols-cborg/src/Network/TypedProtocol/Codec/CBOR.hs

@@ -24,7 +24,6 @@ import qualified Data.ByteString.Builder as BS
 import qualified Data.ByteString.Builder.Extra as BS
 import qualified Data.ByteString.Lazy as LBS
 import qualified Data.ByteString.Lazy.Internal as LBS (smallChunkSize)
-import           Data.Singletons
 
 import           Network.TypedProtocol.Codec
 import           Network.TypedProtocol.Core
@@ -48,13 +47,13 @@ mkCodecCborStrictBS
   :: forall ps m. MonadST m
 
   => (forall (st :: ps) (st' :: ps).
-             SingI st
+             StateTokenI st
           => ActiveState st
           => Message ps st st' -> CBOR.Encoding)
 
   -> (forall (st :: ps) s.
              ActiveState st
-          => Sing st
+          => StateToken st
           -> CBOR.Decoder s (SomeMessage st))
 
   -> Codec ps DeserialiseFailure m BS.ByteString
@@ -104,13 +103,13 @@ mkCodecCborLazyBS
   :: forall ps m. MonadST m
 
   => (forall (st :: ps) (st' :: ps).
-             SingI st
+             StateTokenI st
           => ActiveState st
           => Message ps st st' -> CBOR.Encoding)
 
   -> (forall (st :: ps) s.
              ActiveState st
-          => Sing st
+          => StateToken st
           -> CBOR.Decoder s (SomeMessage st))
 
   -> Codec ps CBOR.DeserialiseFailure m LBS.ByteString

typed-protocols-examples/src/Network/TypedProtocol/Driver/Simple.hs

@@ -32,8 +32,6 @@ module Network.TypedProtocol.Driver.Simple
   , runDecoderWithChannel
   ) where
 
-import           Data.Singletons
-
 import           Network.TypedProtocol.Channel
 import           Network.TypedProtocol.Codec
 import           Network.TypedProtocol.Core
@@ -91,7 +89,7 @@ driverSimple tracer Codec{encode, decode} channel@Channel{send} =
     Driver { sendMessage, recvMessage, initialDState = Nothing }
   where
     sendMessage :: forall (st :: ps) (st' :: ps).
-                   ( SingI st
+                   ( StateTokenI st
                    , ActiveState st
                    )
                 => ReflRelativeAgency (StateAgency st)
@@ -104,7 +102,7 @@ driverSimple tracer Codec{encode, decode} channel@Channel{send} =
       traceWith tracer (TraceSendMsg (AnyMessage msg))
 
     recvMessage :: forall (st :: ps).
-                   ( SingI st
+                   ( StateTokenI st
                    , ActiveState st
                    )
                 => ReflRelativeAgency (StateAgency st)
@@ -113,7 +111,7 @@ driverSimple tracer Codec{encode, decode} channel@Channel{send} =
                 -> Maybe bytes
                 -> m (SomeMessage st, Maybe bytes)
     recvMessage !_refl trailing = do
-      decoder <- decode sing
+      decoder <- decode stateToken
       result  <- runDecoderWithChannel channel trailing decoder
       case result of
         Right x@(SomeMessage msg, _trailing') -> do

typed-protocols-examples/src/Network/TypedProtocol/PingPong/Codec.hs

@@ -7,8 +7,6 @@
 
 module Network.TypedProtocol.PingPong.Codec where
 
-import           Data.Singletons
-
 import           Network.TypedProtocol.Codec
 import           Network.TypedProtocol.Core
 import           Network.TypedProtocol.PingPong.Type
@@ -29,7 +27,7 @@ codecPingPong =
 
     decode :: forall (st :: PingPong).
               ActiveState st
-           => Sing st
+           => StateToken st
            -> m (DecodeStep String CodecFailure m (SomeMessage st))
     decode stok =
       decodeTerminatedFrame '\n' $ \str trailing ->
@@ -72,7 +70,7 @@ codecPingPongId =
     Codec{encode,decode}
   where
     encode :: forall (st :: PingPong) (st' :: PingPong)
-           .  ( SingI st
+           .  ( StateTokenI st
               , ActiveState st
               )
            => Message PingPong st st'
@@ -81,7 +79,7 @@ codecPingPongId =
 
     decode :: forall (st :: PingPong).
               ActiveState st
-           => Sing st
+           => StateToken st
            -> m (DecodeStep (AnyMessage PingPong) CodecFailure m (SomeMessage st))
     decode stok =
       pure $ DecodePartial $ \mb ->

typed-protocols-examples/src/Network/TypedProtocol/PingPong/Codec/CBOR.hs

@@ -10,7 +10,6 @@ module Network.TypedProtocol.PingPong.Codec.CBOR where
 import           Control.Monad.Class.MonadST
 
 import           Data.ByteString.Lazy (ByteString)
-import           Data.Singletons
 
 import qualified Codec.CBOR.Decoding as CBOR (Decoder, decodeWord)
 import qualified Codec.CBOR.Encoding as CBOR (Encoding, encodeWord)
@@ -36,7 +35,7 @@ codecPingPong = mkCodecCborLazyBS encodeMsg decodeMsg
 
   decodeMsg :: forall s (st :: PingPong).
                ActiveState st
-            => Sing st
+            => StateToken st
             -> CBOR.Decoder s (SomeMessage st)
   decodeMsg stok = do
     key <- CBOR.decodeWord

typed-protocols-examples/src/Network/TypedProtocol/PingPong/Type.hs

@@ -8,8 +8,6 @@
 
 module Network.TypedProtocol.PingPong.Type where
 
-import           Data.Singletons
-
 import           Network.TypedProtocol.Core
 
 
@@ -44,14 +42,12 @@ data SPingPong (st :: PingPong) where
 
 deriving instance Show (SPingPong st)
 
-type instance Sing = SPingPong
-instance SingI StIdle where
-    sing = SingIdle
-instance SingI StBusy where
-    sing = SingBusy
-instance SingI StDone where
-    sing = SingDone
-
+instance StateTokenI StIdle where
+    stateToken = SingIdle
+instance StateTokenI StBusy where
+    stateToken = SingBusy
+instance StateTokenI StDone where
+    stateToken = SingDone
 
 instance Protocol PingPong where
 

typed-protocols-examples/src/Network/TypedProtocol/ReqResp/Codec.hs

@@ -8,8 +8,6 @@
 
 module Network.TypedProtocol.ReqResp.Codec where
 
-import           Data.Singletons
-
 import           Network.TypedProtocol.Codec
 import           Network.TypedProtocol.Core
 import           Network.TypedProtocol.PingPong.Codec (decodeTerminatedFrame)
@@ -35,7 +33,7 @@ codecReqResp =
     decode :: forall req' resp' m'
                      (st :: ReqResp req' resp')
            .  (Monad m', Read req', Read resp', ActiveState st)
-           => Sing st
+           => StateToken st
            -> m' (DecodeStep String CodecFailure m' (SomeMessage st))
     decode stok =
       decodeTerminatedFrame '\n' $ \str trailing ->
@@ -62,15 +60,15 @@ codecReqRespId =
   where
     encode :: forall (st  :: ReqResp req resp)
                      (st' :: ReqResp req resp)
-           .  SingI st
+           .  StateTokenI st
            => ActiveState st
            => Message (ReqResp req resp) st st'
            -> AnyMessage (ReqResp req resp)
     encode msg = AnyMessage msg
 
     decode :: forall (st :: ReqResp req resp)
            .  ActiveState st
-           => Sing st
+           => StateToken st
            -> m (DecodeStep (AnyMessage (ReqResp req resp)) CodecFailure m (SomeMessage st))
     decode stok =
       pure $ DecodePartial $ \mb ->

typed-protocols-examples/src/Network/TypedProtocol/ReqResp/Codec/CBOR.hs

@@ -10,7 +10,6 @@ module Network.TypedProtocol.ReqResp.Codec.CBOR where
 import           Control.Monad.Class.MonadST
 
 import           Data.ByteString.Lazy (ByteString)
-import           Data.Singletons
 
 import qualified Codec.CBOR.Decoding as CBOR (Decoder, decodeListLen,
                      decodeWord)
@@ -46,7 +45,7 @@ codecReqResp = mkCodecCborLazyBS encodeMsg decodeMsg
 
   decodeMsg :: forall s (st :: ReqResp req resp).
                ActiveState st
-            => Sing st
+            => StateToken st
             -> CBOR.Decoder s (SomeMessage st)
   decodeMsg stok = do
     _ <- CBOR.decodeListLen

typed-protocols-examples/src/Network/TypedProtocol/ReqResp/Type.hs

@@ -9,8 +9,6 @@
 
 module Network.TypedProtocol.ReqResp.Type where
 
-import           Data.Singletons
-
 import           Network.TypedProtocol.Core
 
 
@@ -26,13 +24,12 @@ data SReqResp (st :: ReqResp req resp) where
 
 deriving instance Show (SReqResp st)
 
-type instance Sing = SReqResp
-instance SingI StIdle where
-    sing = SingIdle
-instance SingI StBusy where
-    sing = SingBusy
-instance SingI StDone where
-    sing = SingDone
+instance StateTokenI StIdle where
+    stateToken = SingIdle
+instance StateTokenI StBusy where
+    stateToken = SingBusy
+instance StateTokenI StDone where
+    stateToken = SingDone
 
 
 instance Protocol (ReqResp req resp) where

typed-protocols-examples/src/Network/TypedProtocol/ReqResp2/Client.hs

@@ -1,12 +1,9 @@
 {-# LANGUAGE BangPatterns        #-}
 {-# LANGUAGE DataKinds           #-}
 {-# LANGUAGE GADTs               #-}
-{-# LANGUAGE KindSignatures      #-}
-{-# LANGUAGE LambdaCase          #-}
 {-# LANGUAGE PolyKinds           #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TypeApplications    #-}
-{-# LANGUAGE TypeOperators       #-}
 
 
 

typed-protocols-examples/src/Network/TypedProtocol/ReqResp2/Type.hs

@@ -9,8 +9,6 @@
 
 module Network.TypedProtocol.ReqResp2.Type where
 
-import           Data.Singletons
-
 import           Network.TypedProtocol.Core
 
 
@@ -28,15 +26,14 @@ data SReqResp2 (st :: ReqResp2 req resp) where
 
 deriving instance Show (SReqResp2 st)
 
-type instance Sing = SReqResp2
-instance SingI StIdle where
-    sing = SingIdle
-instance SingI StBusy where
-    sing = SingBusy
-instance SingI StBusy' where
-    sing = SingBusy'
-instance SingI StDone where
-    sing = SingDone
+instance StateTokenI StIdle where
+    stateToken = SingIdle
+instance StateTokenI StBusy where
+    stateToken = SingBusy
+instance StateTokenI StBusy' where
+    stateToken = SingBusy'
+instance StateTokenI StDone where
+    stateToken = SingDone
 
 
 instance Protocol (ReqResp2 req resp) where

typed-protocols-examples/src/Network/TypedProtocol/Trans/Wedge.hs

@@ -15,8 +15,6 @@
 
 module Network.TypedProtocol.Trans.Wedge where
 
-import           Data.Singletons
-
 import           Network.TypedProtocol.Core
 
 import qualified Network.TypedProtocol.Peer.Client as Client
@@ -37,25 +35,24 @@ data Wedge ps (stIdle :: ps) ps' (stIdle' :: ps') where
 
 data SingWedge (st ::  Wedge ps (stIdle :: ps) ps' (stIdle' :: ps')) where
     SingStIdle :: SingWedge StIdle
-    SingStFst  :: Sing st
+    SingStFst  :: StateToken st
                -> SingWedge (StFst st)
-    SingStSnd  :: Sing st'
+    SingStSnd  :: StateToken st'
                -> SingWedge (StSnd st')
 
 instance Show (SingWedge StIdle) where
     show SingStIdle    = "SingStIdle"
-instance Show (Sing st) => Show (SingWedge (StFst st)) where
+instance Show (StateToken st) => Show (SingWedge (StFst st)) where
     show (SingStFst s) = "SingStFst " ++ show s
-instance Show (Sing st) => Show (SingWedge (StSnd st)) where
+instance Show (StateToken st) => Show (SingWedge (StSnd st)) where
     show (SingStSnd s) = "SingStSnd " ++ show s
 
-type instance Sing = SingWedge
-instance SingI StIdle where
-    sing = SingStIdle
-instance SingI st => SingI (StFst st) where
-    sing = SingStFst (sing @st)
-instance SingI st => SingI (StSnd st) where
-    sing = SingStSnd (sing @st)
+instance StateTokenI StIdle where
+    stateToken = SingStIdle
+instance StateTokenI st => StateTokenI (StFst st) where
+    stateToken = SingStFst (stateToken @st)
+instance StateTokenI st => StateTokenI (StSnd st) where
+    stateToken = SingStSnd (stateToken @st)
 
 
 -- | A Singleton type which allows to pick the starting protocol state.