Updated typed-protocols-doc-demo

Author: coot

typed-protocols-doc/demo/DemoProtocol.hs

@@ -5,26 +5,31 @@
 {-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE PolyKinds #-}
 {-# LANGUAGE StandaloneDeriving #-}
 {-# LANGUAGE TypeApplications #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE UndecidableInstances #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TemplateHaskell #-}
 
+-- for `deriveSerDoc`
+{-# OPTIONS_GHC -Wno-redundant-constraints #-}
+
 module DemoProtocol
 where
 
-import Network.TypedProtocol.Core
-import Data.SerDoc.Info
 import Control.Monad.Identity
 import Control.Monad.Except
+
 import Data.Proxy
-import Data.Word
-import Data.Typeable
 import Data.SerDoc.Class
+import Data.SerDoc.Info
 import Data.SerDoc.TH
 import Data.Text (Text)
+import Data.Word
+
+import Network.TypedProtocol.Core
 
 data PongInfo =
   PongInfo
@@ -44,34 +49,29 @@ data DemoProtocol a where
   -- | End state: either side has terminated the session
   EndState :: DemoProtocol a
 
+data SingDemoProtocol a where
+    SingIdleState         :: SingDemoProtocol (IdleState         :: DemoProtocol a)
+    SingAwaitingPongState :: SingDemoProtocol (AwaitingPongState :: DemoProtocol a)
+    SingEndState          :: SingDemoProtocol (EndState          :: DemoProtocol a)
+
+instance StateTokenI IdleState         where stateToken = SingIdleState
+instance StateTokenI AwaitingPongState where stateToken = SingAwaitingPongState
+instance StateTokenI EndState          where stateToken = SingEndState
+
 instance Protocol (DemoProtocol a) where
   data Message (DemoProtocol a) st st' where
     PingMessage :: Message (DemoProtocol a) IdleState AwaitingPongState
     PongMessage :: Message (DemoProtocol a) AwaitingPongState IdleState
     ComplexPongMessage :: Message (DemoProtocol a) AwaitingPongState IdleState
     EndMessage :: Message (DemoProtocol a) st EndState
 
-  data ServerHasAgency st where
-    TokIdle :: ServerHasAgency IdleState
-
-  data ClientHasAgency st where
-    TokAwaitingPongState :: ClientHasAgency AwaitingPongState
-
-  data NobodyHasAgency st where
-    TokEnd :: NobodyHasAgency EndState
-
+  type StateAgency IdleState         = ServerAgency
+  type StateAgency AwaitingPongState = ClientAgency
+  type StateAgency EndState          = NobodyAgency
 
-  exclusionLemma_ClientAndServerHaveAgency tok1 tok2 =
-    case tok1 of
-      TokAwaitingPongState -> case tok2 of {}
+  type StateToken = SingDemoProtocol
 
-  exclusionLemma_NobodyAndClientHaveAgency tok1 tok2 =
-    case tok1 of
-      TokEnd -> case tok2 of {}
 
-  exclusionLemma_NobodyAndServerHaveAgency tok1 tok2 =
-    case tok1 of
-      TokEnd -> case tok2 of {}
 
 data DemoCodec a
 

typed-protocols-doc/src/Network/TypedProtocol/Documentation/DefaultMain.hs

@@ -65,8 +65,7 @@ pMainOptions =
           )
 
 
-defaultMain :: ( Codec codec
-               , HasInfo codec (DefEnumEncoding codec)
+defaultMain :: ( HasInfo codec (DefEnumEncoding codec)
                , HasInfo codec Word32
                ) => [ProtocolDescription codec] -> IO ()
 defaultMain descriptions = do
@@ -79,8 +78,7 @@ defaultMain descriptions = do
         render = getRenderer (moOutputFormat mainOptions) (moOutputFile mainOptions)
     write . render $ descriptions
 
-getRenderer :: ( Codec codec
-               , HasInfo codec (DefEnumEncoding codec)
+getRenderer :: ( HasInfo codec (DefEnumEncoding codec)
                , HasInfo codec Word32
                )
             => OutputFormat

typed-protocols-doc/test/Network/TypedProtocol/Tests/TestProtocol.hs

@@ -23,7 +23,6 @@ import Control.Monad.Identity
 import Control.Monad.Except
 import Data.Proxy
 import Data.Word
-import Data.Typeable
 import Data.SerDoc.Class
 import Data.SerDoc.TH
 import Data.Text (Text)