predicate template to add Auto instances

definitions/package.yaml

@@ -34,6 +34,7 @@ dependencies:
   - singletons
   - servant-docs
   - servant-server
+  - template-haskell
 
 library:
   source-dirs: src

definitions/src/Predicate.hs

@@ -0,0 +1,46 @@
+module Predicate where
+
+import ClassyPrelude
+import Language.Haskell.TH.Syntax
+
+-- This template adds instances of Auto typeclass (from decidable package)
+-- to a given parametrised type definition
+--
+-- Given type definitions:
+--
+-- data P = A | B | C
+--
+-- $(predicate [d|
+--   data T (a :: P) where
+--     TA :: T 'A
+--     TB :: T 'B
+--   |]
+--
+-- `predicate` splice will add these instances:
+--
+-- instance Auto (TyPred T) 'A where auto = TA  -- autoTC could have been used here too
+-- instance Auto (TyPred T) 'B where auto = TB
+--
+-- to be used in type constraints
+
+predicate :: Q [Dec] -> Q [Dec]
+predicate decls = mconcat . map mkInstances <$> decls
+  where
+    mkInstances :: Dec -> [Dec]
+    mkInstances d@(DataD _ tName _ _ constructors _) =
+      d : mapMaybe (mkInstance tName) constructors
+    mkInstances d = [d]
+
+    mkInstance :: Name -> Con -> Maybe InstanceDec
+    mkInstance tName (GadtC [cName] [] (AppT _ pType)) =
+      let tyCon name = AppT (ConT (mkName name))
+          ty =  AppT
+                  (tyCon "Auto"
+                    (tyCon "TyPred"
+                      (ConT tName)))
+                  pType
+          ds =  [ValD
+                  (VarP (mkName "auto"))
+                  (NormalB (ConE cName)) []]
+      in Just $ InstanceD Nothing [] ty ds
+    mkInstance _ _ = Nothing

definitions/src/Simplex/Messaging/Broker.hs

@@ -11,14 +11,15 @@
 module Simplex.Messaging.Broker where
 
 import ClassyPrelude
+import Data.Singletons.TH
 import Simplex.Messaging.Protocol
 import Simplex.Messaging.Types
 
 
 instance Prf HasState Sender s
-         => ProtocolCommandOf Broker
+         => ProtocolCommand Broker
+              Recipient
               CreateConnRequest CreateConnResponse
-              Recipient Broker
               (None <==> None <==| s)
               (New <==> New <==| s)
               Idle Idle 0 0
@@ -26,7 +27,26 @@ instance Prf HasState Sender s
     command = CreateConn
     protoCmd = bCreateConn
 
+instance ( (r /= None && r /= Disabled) ~ True
+         , (b /= None && b /= Disabled) ~ True
+         , Prf HasState Sender s )
+         => ProtocolCommand Broker
+              Recipient
+              () ()
+              (r <==> b <==| s)
+              (r <==> b <==| s)
+              Idle Subscribed n n
+  where
+    command  = Subscribe
+    protoCmd = bSubscribe
+
+
 bCreateConn :: Connection Broker None Idle
             -> CreateConnRequest
             -> Either String (CreateConnResponse, Connection Broker New Idle)
 bCreateConn = protoCmdStub
+
+bSubscribe  :: Connection Broker s Idle
+            -> ()
+            -> Either String ((), Connection Broker s Subscribed)
+bSubscribe = protoCmdStub

definitions/src/Simplex/Messaging/Client.hs

@@ -17,9 +17,9 @@ import Simplex.Messaging.Types
 
 
 instance Prf HasState Sender s
-         => ProtocolActionOf Recipient
+         => ProtocolAction Recipient
+              Broker
               CreateConnRequest CreateConnResponse
-              Recipient Broker
               (None <==> None <==| s)
               (New <==> New <==| s)
               Idle Idle 0 0
@@ -30,9 +30,9 @@ instance Prf HasState Sender s
 instance ( (r /= None && r /= Disabled) ~ True
          , (b /= None && b /= Disabled) ~ True
          , Prf HasState Sender s )
-         => ProtocolActionOf Recipient
+         => ProtocolAction Recipient
+              Broker
               () ()
-              Recipient Broker
               (r <==> b <==| s)
               (r <==> b <==| s)
               Idle Subscribed n n

definitions/src/Simplex/Messaging/Protocol.hs

@@ -28,6 +28,7 @@ import Data.Singletons.TH
 import Data.Type.Predicate
 import Data.Type.Predicate.Auto
 import GHC.TypeLits
+import Predicate
 import Simplex.Messaging.Types
 
 $(singletons [d|
@@ -45,33 +46,25 @@ $(singletons [d|
   data ConnSubscription = Subscribed | Idle
   |])
 
--- broker connection states
 type Prf1 t a = Auto (TyPred t) a
 
-data BrokerCS :: ConnectionState -> Type where
-  BrkNew      :: BrokerCS New
-  BrkSecured  :: BrokerCS Secured
-  BrkDisabled :: BrokerCS Disabled
-  BrkDrained  :: BrokerCS Drained
-  BrkNone     :: BrokerCS None
-
-instance Auto (TyPred BrokerCS) New      where auto = autoTC
-instance Auto (TyPred BrokerCS) Secured  where auto = autoTC
-instance Auto (TyPred BrokerCS) Disabled where auto = autoTC
-instance Auto (TyPred BrokerCS) Drained  where auto = autoTC
-instance Auto (TyPred BrokerCS) None     where auto = autoTC
+$(predicate [d|
+-- broker connection states
+  data BrokerCS :: ConnectionState -> Type where
+    BrkNew      :: BrokerCS New
+    BrkSecured  :: BrokerCS Secured
+    BrkDisabled :: BrokerCS Disabled
+    BrkDrained  :: BrokerCS Drained
+    BrkNone     :: BrokerCS None
 
 -- sender connection states
-data SenderCS :: ConnectionState -> Type where
-  SndNew       :: SenderCS New
-  SndConfirmed :: SenderCS Confirmed
-  SndSecured   :: SenderCS Secured
-  SndNone      :: SenderCS None
+  data SenderCS :: ConnectionState -> Type where
+    SndNew       :: SenderCS New
+    SndConfirmed :: SenderCS Confirmed
+    SndSecured   :: SenderCS Secured
+    SndNone      :: SenderCS None
+  |])
 
-instance Auto (TyPred SenderCS) New       where auto = autoTC
-instance Auto (TyPred SenderCS) Confirmed where auto = autoTC
-instance Auto (TyPred SenderCS) Secured   where auto = autoTC
-instance Auto (TyPred SenderCS) None      where auto = autoTC
 
 -- allowed participant connection states
 data HasState (p :: Participant) (s :: ConnectionState) :: Type where
@@ -140,6 +133,7 @@ data Command arg result
              (ss :: ConnSubscription) (ss' :: ConnSubscription)
              (messages :: Nat) (messages' :: Nat)
              :: Type where
+
   CreateConn   :: Prf HasState Sender s
                => Command
                     CreateConnRequest CreateConnResponse
@@ -279,9 +273,9 @@ type family PConnSt (p :: Participant) state where
 -- of participants actions/functions and connection state transitions (types)
 -- with types of protocol commands defined above.
 
-class me ~ p => ProtocolCommandOf (me :: Participant)
+class ProtocolCommand (p :: Participant)
+        (from :: Participant)
         arg res
-        (from :: Participant) (p :: Participant)
         state state'
         (ss :: ConnSubscription) (ss' :: ConnSubscription)
         (n :: Nat) (n' :: Nat)
@@ -297,9 +291,9 @@ protoCmdStub :: Connection p ps ss
 protoCmdStub _ _ = Left "Command not implemented"
 
 
-class me ~ p => ProtocolActionOf (me :: Participant)
+class ProtocolAction (p :: Participant)
+        (to :: Participant)
         arg res
-        (p :: Participant) (to :: Participant)
         state state'
         (ss :: ConnSubscription) (ss' :: ConnSubscription)
         (n :: Nat) (n' :: Nat)