From a9565a57546602076ed9aa65a4a5923d19d46c59 Mon Sep 17 00:00:00 2001 From: Evgeny Poberezkin <2769109+epoberezkin@users.noreply.github.com> Date: Tue, 12 May 2020 19:27:08 +0100 Subject: [PATCH] predicate template to add Auto instances --- definitions/package.yaml | 1 + definitions/src/Predicate.hs | 46 +++++++++++++++++++ definitions/src/Simplex/Messaging/Broker.hs | 24 +++++++++- definitions/src/Simplex/Messaging/Client.hs | 8 ++-- definitions/src/Simplex/Messaging/Protocol.hs | 46 ++++++++----------- 5 files changed, 93 insertions(+), 32 deletions(-) create mode 100644 definitions/src/Predicate.hs diff --git a/definitions/package.yaml b/definitions/package.yaml index 1d3d02560d..0cf8d9db41 100644 --- a/definitions/package.yaml +++ b/definitions/package.yaml @@ -34,6 +34,7 @@ dependencies: - singletons - servant-docs - servant-server + - template-haskell library: source-dirs: src diff --git a/definitions/src/Predicate.hs b/definitions/src/Predicate.hs new file mode 100644 index 0000000000..9564e53d34 --- /dev/null +++ b/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 diff --git a/definitions/src/Simplex/Messaging/Broker.hs b/definitions/src/Simplex/Messaging/Broker.hs index 8b7965b93e..d34c1c9724 100644 --- a/definitions/src/Simplex/Messaging/Broker.hs +++ b/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 diff --git a/definitions/src/Simplex/Messaging/Client.hs b/definitions/src/Simplex/Messaging/Client.hs index 8d3702f925..fa00879565 100644 --- a/definitions/src/Simplex/Messaging/Client.hs +++ b/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 diff --git a/definitions/src/Simplex/Messaging/Protocol.hs b/definitions/src/Simplex/Messaging/Protocol.hs index 0ab9406642..6a40838c4c 100644 --- a/definitions/src/Simplex/Messaging/Protocol.hs +++ b/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)