Fix typed-protocols-doc

cabal.project

@@ -19,7 +19,7 @@ packages: ./typed-protocols
           ./typed-protocols-stateful
           ./typed-protocols-stateful-cborg
           ./typed-protocols-examples
-          -- ./typed-protocols-doc
+          ./typed-protocols-doc
 
 test-show-details: direct
 

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

@@ -15,6 +15,7 @@ import Control.Monad
 -- This import is only needed when 'getDoc' is available.
 import Data.Maybe (maybeToList)
 #endif
+import Data.Maybe (mapMaybe)
 import Data.Proxy
 import Language.Haskell.TH
 import Language.Haskell.TH.Datatype
@@ -34,45 +35,29 @@ describeProtocol protoTyCon protoTyArgs codecTyCon codecTyArgs = do
   protoDescription <- getDescription protoTyCon
   let pname = nameBase (datatypeName info)
 
-  let extractMessageStateNames :: InstanceDec -> [Name]
-      extractMessageStateNames (DataInstD _ _ _ _ tys _) =
-        [ case ty of
-            ForallC _ _ (GadtC _ _ ty') -> go ty'
-            GadtC _ _ ty' -> go ty'
-            _ -> error $ "Not a GADT: " ++ show ty
-        | ty <- tys
-        ]
-        where
-          go (PromotedT tyName) = tyName
-          go (SigT ty' _) = go ty'
-          go (AppT _ ty') = go ty'
-          go ty' = error $ "Cannot detect message name from type: " ++ show ty'
-      extractMessageStateNames i = error $ "Not a DataInstD: " ++ show i
+  let extractAgency :: InstanceDec -> Maybe Name
+      extractAgency (TySynInstD (TySynEqn _ _ (PromotedT agency))) = Just agency
+      extractAgency dec = error $ "Unexpected InstanceDec: " ++ show dec
+
+  let extractAgencies :: [InstanceDec] -> [Name]
+      extractAgencies = mapMaybe extractAgency
+
+  let extractTheAgency :: [InstanceDec] -> Name
+      extractTheAgency inst = case extractAgencies inst of
+        [agency] -> agency
+        xs -> error $ "Incorrect number of agencies: " ++ show xs
 
   pstates <- forM (datatypeCons info) $ \conInfo -> do
     let conName = constructorName conInfo
     stateDescription <- getDescription conName
 
-    serverAgencies <- reifyInstances ''ServerHasAgency [ConT conName]
-    let serverAgencies' =
-          [ nameBase tyName
-          | inst <- serverAgencies
-          , tyName <- extractMessageStateNames inst
-          , nameBase tyName == nameBase conName
-          ]
-    clientAgencies <- reifyInstances ''ClientHasAgency [ConT conName]
-    let clientAgencies' =
-          [ nameBase tyName
-          | inst <- clientAgencies
-          , tyName <- extractMessageStateNames inst
-          , nameBase tyName == nameBase conName
-          ]
-
-    let agencyID = case (serverAgencies', clientAgencies') of
-          ([], []) -> NobodyAgencyID
-          (_, []) -> ServerAgencyID
-          ([], _) -> ClientAgencyID
-          _ -> error $ show (nameBase conName, serverAgencies', clientAgencies')
+    stateAgencies <- reifyInstances ''StateAgency [ConT conName]
+    let agencyName = extractTheAgency stateAgencies
+        agencyID = case nameBase agencyName of
+          "ServerAgency" -> 'ServerAgencyID
+          "ClientAgency" -> 'ClientAgencyID
+          "NobodyAgency" -> 'NobodyAgencyID
+          x -> error $ "Unknown agency type " ++ x ++ " in state " ++ nameBase conName
 
     return (conName, stateDescription, agencyID)
 
@@ -87,7 +72,7 @@ describeProtocol protoTyCon protoTyArgs codecTyCon codecTyArgs = do
         protoDescription
         ""
         $(listE
-            [ [| ( $(makeState $ ConT conName), stateDescription, agencyID) |]
+            [ [| ( $(makeState $ ConT conName), stateDescription, $(conE agencyID)) |]
             | (conName, stateDescription, agencyID) <- pstates
             ]
          )

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

@@ -1,3 +1,5 @@
+{-# OPTIONS_GHC -Wno-redundant-constraints #-}
+
 {-# LANGUAGE DataKinds #-}
 {-# LANGUAGE DerivingVia #-}
 {-# LANGUAGE EmptyCase #-}
@@ -30,10 +32,10 @@ import Data.Typeable
 import Data.Word
 import Network.TypedProtocol.Core
 
-data AgentInfo c =
+data AgentInfo =
   AgentInfo
-    { agentInfoCurrentBundle :: !(Maybe (BundleInfo c))
-    , agentInfoStagedKey :: !(Maybe (KeyInfo c))
+    { agentInfoCurrentBundle :: !(Maybe BundleInfo)
+    , agentInfoStagedKey :: !(Maybe KeyInfo)
     , agentInfoBootstrapConnections :: ![BootstrapInfo]
     }
     deriving (Show, Eq)
@@ -50,7 +52,6 @@ deriving via (ViaEnum Command)
   instance
     ( Codec codec
     , HasInfo codec (DefEnumEncoding codec)
-    , Integral (DefEnumEncoding codec)
     ) => HasInfo codec Command
 
 instance
@@ -63,16 +64,16 @@ instance
     encode codec = encodeEnum codec (Proxy @(DefEnumEncoding codec))
     decode codec = decodeEnum codec (Proxy @(DefEnumEncoding codec))
 
-newtype FakeKey k = FakeKey { fakeKeyData :: ByteString }
+newtype FakeKey = FakeKey { fakeKeyData :: ByteString }
   deriving (Show, Eq, Ord)
 
 newtype VersionIdentifier = VersionIdentifier { versionIdentifierData :: ByteString }
   deriving (Show, Eq, Ord)
 
-instance HasInfo (TestCodec ()) VersionIdentifier where
+instance HasInfo TestCodec VersionIdentifier where
   info _ _ = basicField "Bytes" (FixedSize 32)
 
-instance HasInfo (TestCodec ()) (FakeKey k) where
+instance HasInfo TestCodec FakeKey where
   info _ _ = basicField "Bytes" (FixedSize 128)
 
 data BootstrapInfo =
@@ -92,25 +93,25 @@ deriving via (ViaEnum ConnectionStatus)
   instance (Codec codec, HasInfo codec (DefEnumEncoding codec))
     => HasInfo codec ConnectionStatus
 
-data BundleInfo c =
+data BundleInfo =
   BundleInfo
     { bundleInfoEvolution :: !Word32
     , bundleInfoOCertN :: !Word64
-    , bundleInfoVK :: !(FakeKey c)
+    , bundleInfoVK :: !FakeKey
     }
     deriving (Show, Eq)
 
-newtype KeyInfo c =
+newtype KeyInfo =
   KeyInfo
-    { keyInfoVK :: FakeKey c
+    { keyInfoVK :: FakeKey
     }
     deriving (Show, Eq)
 
 deriving newtype
   instance
-    ( HasInfo codec (FakeKey c)
+    ( HasInfo codec FakeKey
     , Codec codec
-    ) => HasInfo codec (KeyInfo c)
+    ) => HasInfo codec KeyInfo
 
 $(deriveSerDoc ''TestCodec [] ''BundleInfo)
 $(deriveSerDoc ''TestCodec [] ''BootstrapInfo)
@@ -129,27 +130,27 @@ $(deriveSerDoc ''TestCodec [] ''AgentInfo)
 -- through. This allows the control client to report success to the user, but it
 -- also helps make things more predictable in testing, because it means that
 -- sending keys is now synchronous.
-data ControlProtocol (m :: Type -> Type) (k :: Type) where
+data ControlProtocol (m :: Type -> Type) (c :: Type) where
   -- | Default state after connecting, but before the protocol version has been
   -- negotiated.
-  InitialState :: ControlProtocol m k
+  InitialState :: ControlProtocol m c
 
   -- | System is idling, waiting for the server to push the next key.
-  IdleState :: ControlProtocol m k
+  IdleState :: ControlProtocol m c
 
   -- | Client has requested a new KES key to be generated in the staging area.
-  WaitForPublicKeyState :: ControlProtocol m k
+  WaitForPublicKeyState :: ControlProtocol m c
 
   -- | Client has requested agent information
-  WaitForInfoState :: ControlProtocol m k
+  WaitForInfoState :: ControlProtocol m c
 
   -- | An OpCert has been pushed, client must now confirm that it has been
   -- received, and that it matches the staged KES key.
-  WaitForConfirmationState :: ControlProtocol m k
+  WaitForConfirmationState :: ControlProtocol m c
 
   -- | The server has closed the connection, thus signalling the end of the
   -- session.
-  EndState :: ControlProtocol m k
+  EndState :: ControlProtocol m c
 
 {-# ANN VersionMessage (Description ["Announce the protocol version."]) #-}
 {-# ANN GenStagedKeyMessage
@@ -217,61 +218,49 @@ instance Protocol (ControlProtocol m c) where
 
           DropStagedKeyMessage :: Message (ControlProtocol m c) IdleState WaitForPublicKeyState
 
-          PublicKeyMessage :: Maybe (FakeKey c)
+          PublicKeyMessage :: Maybe FakeKey
                            -> Message (ControlProtocol m c) WaitForPublicKeyState IdleState
 
-          InstallKeyMessage :: FakeKey c
+          InstallKeyMessage :: FakeKey
                             -> Message (ControlProtocol m c) IdleState WaitForConfirmationState
 
           InstallResultMessage :: Word32
                                -> Message (ControlProtocol m c) WaitForConfirmationState IdleState
 
           RequestInfoMessage :: Message (ControlProtocol m c) IdleState WaitForInfoState
 
-          InfoMessage :: AgentInfo c
+          InfoMessage :: AgentInfo
                       -> Message (ControlProtocol m c) WaitForInfoState IdleState
 
           AbortMessage :: Message (ControlProtocol m c) InitialState EndState
           EndMessage :: Message (ControlProtocol m c) IdleState EndState
           ProtocolErrorMessage :: Message (ControlProtocol m c) a EndState
 
   -- | Server always has agency, except between sending a key and confirming it
-  data ServerHasAgency st where
-    TokInitial :: ServerHasAgency InitialState
-    TokIdle :: ServerHasAgency IdleState
-
-  -- | Client only has agency between sending a key and confirming it
-  data ClientHasAgency st where
-    TokWaitForConfirmation :: ClientHasAgency WaitForConfirmationState
-    TokWaitForPublicKey :: ClientHasAgency WaitForPublicKeyState
-    TokWaitForInfo :: ClientHasAgency WaitForInfoState
-
-  -- | Someone, i.e., the server, always has agency
-  data NobodyHasAgency st where
-    TokEnd :: NobodyHasAgency EndState
-
-  exclusionLemma_ClientAndServerHaveAgency tok1 tok2 =
-    case tok1 of
-      TokWaitForConfirmation ->
-        case tok2 of {}
-      TokWaitForPublicKey ->
-        case tok2 of {}
-      TokWaitForInfo ->
-        case tok2 of {}
-  exclusionLemma_NobodyAndClientHaveAgency tok1 tok2 =
-    case tok1 of
-      TokEnd -> case tok2 of {}
-  exclusionLemma_NobodyAndServerHaveAgency tok1 tok2 =
-    case tok1 of
-      TokEnd -> case tok2 of {}
-
-instance HasInfo (TestCodec ()) (Message (ControlProtocol m c) InitialState IdleState) where
+  type StateAgency InitialState = ServerAgency
+  type StateAgency IdleState = ServerAgency
+  type StateAgency WaitForConfirmationState = ClientAgency
+  type StateAgency WaitForPublicKeyState = ClientAgency
+  type StateAgency WaitForInfoState = ClientAgency
+  type StateAgency EndState = NobodyAgency
+
+  type StateToken = SControlProtocol
+
+data SControlProtocol (st :: ControlProtocol m c) where
+  SInitialState :: SControlProtocol InitialState
+  SIdleState :: SControlProtocol IdleState
+  SWaitForConfirmationState :: SControlProtocol WaitForConfirmationState
+  SWaitForPublicKeyState :: SControlProtocol WaitForPublicKeyState
+  SWaitForInfoState :: SControlProtocol WaitForInfoState
+  SEndState :: SControlProtocol EndState
+
+instance HasInfo TestCodec (Message (ControlProtocol m c) InitialState IdleState) where
   info codec _ = aliasField
             ("Message<" ++
               "InitialState,IdleState" ++
               ">")
             (info codec (Proxy @VersionIdentifier))
-instance HasInfo (TestCodec ()) (Message (ControlProtocol m c) IdleState WaitForPublicKeyState) where
+instance HasInfo TestCodec (Message (ControlProtocol m c) IdleState WaitForPublicKeyState) where
   info codec _ = aliasField
             ("Message<" ++
               "IdleState,WaitForPublicKeyState" ++
@@ -283,39 +272,39 @@ instance HasInfo (TestCodec ()) (Message (ControlProtocol m c) IdleState WaitFor
 --    QueryStagedKeyMessage -> infoOf QueryStagedKeyCmd
 --    DropStagedKeyMessage -> infoOf DropStagedKeyCmd
 
-instance (HasInfo (TestCodec ()) (FakeKey c)) => HasInfo (TestCodec ()) (Message (ControlProtocol m c) WaitForPublicKeyState IdleState) where
+instance (HasInfo TestCodec FakeKey) => HasInfo TestCodec (Message (ControlProtocol m c) WaitForPublicKeyState IdleState) where
   info codec _ = aliasField
             ("Message<" ++
               "WaitForPublicKeyState,IdleState" ++
               ">")
-            (info codec (Proxy @(Maybe (FakeKey c))))
-instance (HasInfo (TestCodec ()) (FakeKey c)) => HasInfo (TestCodec ()) (Message (ControlProtocol m c) IdleState WaitForConfirmationState) where
+            (info codec (Proxy @(Maybe FakeKey)))
+instance (HasInfo TestCodec FakeKey) => HasInfo TestCodec (Message (ControlProtocol m c) IdleState WaitForConfirmationState) where
   info codec _ = aliasField
             ("Message<" ++
               "IdleState,WaitForConfirmationState" ++
               ">")
-            (info codec (Proxy @(FakeKey c)))
-instance HasInfo (TestCodec ()) (Message (ControlProtocol m c) WaitForConfirmationState IdleState) where
+            (info codec (Proxy @FakeKey))
+instance HasInfo TestCodec (Message (ControlProtocol m c) WaitForConfirmationState IdleState) where
   info codec _ = aliasField
             ("Message<" ++
               "WaitForConfirmationState,IdleState" ++
               ">")
             (info codec (Proxy @Word32))
-instance HasInfo (TestCodec ()) (Message (ControlProtocol m c) IdleState WaitForInfoState) where
+instance HasInfo TestCodec (Message (ControlProtocol m c) IdleState WaitForInfoState) where
   info codec _ = aliasField
             ("Message<" ++
               "IdleState,WaitForInfoState" ++
               ">")
             (info codec (Proxy @()))
-instance ( HasInfo (TestCodec ()) (FakeKey c)
-         , HasInfo (TestCodec ()) (AgentInfo c)
-         ) => HasInfo (TestCodec ()) (Message (ControlProtocol m c) WaitForInfoState IdleState) where
+instance ( HasInfo TestCodec FakeKey
+         , HasInfo TestCodec AgentInfo
+         ) => HasInfo TestCodec (Message (ControlProtocol m c) WaitForInfoState IdleState) where
   info codec _ = aliasField
             ("Message<" ++
               "WaitForInfoState,IdleState" ++
               ">")
-            (info codec (Proxy @(AgentInfo c)))
-instance HasInfo (TestCodec ()) (Message (ControlProtocol m c) _st EndState) where
+            (info codec (Proxy @AgentInfo))
+instance HasInfo TestCodec (Message (ControlProtocol m c) _st EndState) where
   info codec _ = aliasField
             ("Message<" ++
               "st,EndState" ++

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

@@ -24,10 +24,10 @@ tests = testGroup "Documentation"
           , testProperty "state transitions" (p_correctStateTransitions testProtocolDescription)
           ]
 
-testProtocolDescription :: ProtocolDescription (TestCodec ())
-testProtocolDescription = $(describeProtocol ''ControlProtocol [''IO, ''()] ''TestCodec [''()])
+testProtocolDescription :: ProtocolDescription TestCodec
+testProtocolDescription = $(describeProtocol ''ControlProtocol [''IO, ''()] ''TestCodec [])
 
-p_correctAgencies :: ProtocolDescription (TestCodec ()) -> Property
+p_correctAgencies :: ProtocolDescription TestCodec -> Property
 p_correctAgencies d =
   counterexample (show stateAgencyMap) .
   once $
@@ -45,7 +45,7 @@ p_correctAgencies d =
   where
     stateAgencyMap = [(state, agency) | (state, _, agency) <- protocolStates d]
 
-p_correctStateTransitions :: ProtocolDescription (TestCodec ()) -> Property
+p_correctStateTransitions :: ProtocolDescription TestCodec -> Property
 p_correctStateTransitions d =
   once $
     checkMessage "VersionMessage" (State "InitialState") (State "IdleState")
@@ -83,6 +83,6 @@ p_correctStateTransitions d =
           counterexample "toState"
             (messageToState msg === toState)
 
-    findMessage :: String -> Maybe (MessageDescription (TestCodec ()))
+    findMessage :: String -> Maybe (MessageDescription TestCodec)
     findMessage msgName =
       listToMaybe [ msg | msg <- protocolMessages d, messageName msg == msgName ]