From bdec751725fee09151bacbaa2b59b53a00a9893e Mon Sep 17 00:00:00 2001 From: Evgeny Poberezkin <2769109+epoberezkin@users.noreply.github.com> Date: Thu, 14 May 2020 21:30:37 +0100 Subject: [PATCH] Instance template (#33) * protocol instance template [WIP] * protocol instances template * add methods to check correctness of participant types in protocol TH * PushConfirm and and PushMsg implementation types * check Command type + doctest --- definitions/package.yaml | 13 ++ definitions/src/Predicate.hs | 32 +++- definitions/src/Simplex/Messaging/Broker.hs | 61 +++--- definitions/src/Simplex/Messaging/Client.hs | 70 +++---- definitions/src/Simplex/Messaging/Protocol.hs | 179 ++++++++++++++---- .../src/Simplex/Messaging/ProtocolDo.hs | 23 +++ .../src/Simplex/Messaging/Scenarios.hs | 1 + definitions/tests/doctest-driver.hs | 1 + 8 files changed, 262 insertions(+), 118 deletions(-) create mode 100644 definitions/src/Simplex/Messaging/ProtocolDo.hs create mode 100644 definitions/tests/doctest-driver.hs diff --git a/definitions/package.yaml b/definitions/package.yaml index 0cf8d9db41..eb06bbf05a 100644 --- a/definitions/package.yaml +++ b/definitions/package.yaml @@ -19,7 +19,9 @@ ghc-options: - -Wincomplete-uni-patterns default-extensions: + - BlockArguments - DuplicateRecordFields + - LambdaCase - NamedFieldPuns - NoImplicitPrelude - OverloadedStrings @@ -35,10 +37,12 @@ dependencies: - servant-docs - servant-server - template-haskell + # - pretty-show library: source-dirs: src exposed-modules: + - Predicate - Simplex.Messaging.Types - Simplex.Messaging.ServerAPI @@ -46,3 +50,12 @@ executables: api-docs: source-dirs: src main: Main.hs + +tests: + simplex-definitions-doctests: + source-dirs: tests + main: doctest-driver.hs + ghc-options: -threaded + dependencies: + - doctest + - doctest-driver-gen diff --git a/definitions/src/Predicate.hs b/definitions/src/Predicate.hs index a3f800b81a..0f60757ce2 100644 --- a/definitions/src/Predicate.hs +++ b/definitions/src/Predicate.hs @@ -5,8 +5,7 @@ module Predicate where import ClassyPrelude import Data.Type.Predicate import Data.Type.Predicate.Auto -import Language.Haskell.TH.Lib -import Language.Haskell.TH.Syntax +import Language.Haskell.TH -- This template adds instances of Auto typeclass (from decidable package) -- to a given parametrised type definition @@ -19,7 +18,7 @@ import Language.Haskell.TH.Syntax -- data T (a :: P) where -- TA :: T 'A -- TB :: T 'B --- |] +-- |]) -- -- `predicate` splice will add these instances: -- @@ -32,15 +31,28 @@ predicate :: Q [Dec] -> Q [Dec] predicate decls = concat <$> (decls >>= mapM addInstances) where addInstances :: Dec -> Q [Dec] - addInstances d@(DataD _ ty _ _ constructors _) = do - ds <- mapM (mkInstance ty) constructors - return $ d : concat ds - addInstances d = return [d] + addInstances d@(DataD _ _ _ _ constructors _) = do + ds <- mapM mkInstance constructors + if any null ds + then do + reportWarning $ + "warning: not a parametrised GADT predicate (no instances added)\n" + ++ pprint d + return [d] + else + return $ d : concat ds + addInstances d = do + reportWarning $ "warning: not a data type declaration\n" ++ pprint d + return [d] - mkInstance :: Name -> Con -> Q [Dec] - mkInstance ty (GadtC [con] [] (AppT _ (PromotedT p))) = + mkInstance :: Con -> Q [Dec] + mkInstance (GadtC + [con] _ + (AppT + (ConT ty) + (PromotedT p))) = [d| instance Auto (TyPred $(conT ty)) $(promotedT p) where auto = $(conE con) |] - mkInstance _ _ = return [] + mkInstance _ = return [] diff --git a/definitions/src/Simplex/Messaging/Broker.hs b/definitions/src/Simplex/Messaging/Broker.hs index d34c1c9724..dd48e31851 100644 --- a/definitions/src/Simplex/Messaging/Broker.hs +++ b/definitions/src/Simplex/Messaging/Broker.hs @@ -1,52 +1,47 @@ {-# OPTIONS_GHC -fno-warn-unticked-promoted-constructors #-} {-# OPTIONS_GHC -fno-warn-orphans #-} +-- {-# OPTIONS_GHC -ddump-splices #-} {-# LANGUAGE AllowAmbiguousTypes #-} {-# LANGUAGE DataKinds #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE TemplateHaskell #-} {-# LANGUAGE TypeOperators #-} module Simplex.Messaging.Broker where import ClassyPrelude -import Data.Singletons.TH import Simplex.Messaging.Protocol import Simplex.Messaging.Types - -instance Prf HasState Sender s - => ProtocolCommand Broker - Recipient - CreateConnRequest CreateConnResponse - (None <==> None <==| s) - (New <==> New <==| s) - Idle Idle 0 0 - where - 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 +$(protocol Broker [d| + bcCreateConn = CreateConn <-- Recipient + bcSubscribe = Subscribe <-- Recipient + baPushConfirm = PushConfirm --> Recipient + baPushMsg = PushMsg --> Recipient + |]) -bCreateConn :: Connection Broker None Idle - -> CreateConnRequest - -> Either String (CreateConnResponse, Connection Broker New Idle) -bCreateConn = protoCmdStub +bcCreateConn :: Connection Broker None Idle + -> CreateConnRequest + -> Either String (CreateConnResponse, Connection Broker New Idle) +bcCreateConn = protoCmdStub -bSubscribe :: Connection Broker s Idle - -> () - -> Either String ((), Connection Broker s Subscribed) -bSubscribe = protoCmdStub +bcSubscribe :: Connection Broker s Idle + -> () + -> Either String ((), Connection Broker s Subscribed) +bcSubscribe = protoCmdStub + +baPushConfirm :: Connection Broker New Subscribed + -> SecureConnRequest + -> Either String () + -> Either String (Connection Broker New Subscribed) +baPushConfirm = protoActionStub + +baPushMsg :: Connection Broker Secured Subscribed + -> MessagesResponse -- TODO, has to be a single message + -> Either String () + -> Either String (Connection Broker Secured Subscribed) +baPushMsg = protoActionStub diff --git a/definitions/src/Simplex/Messaging/Client.hs b/definitions/src/Simplex/Messaging/Client.hs index 6abc3b8569..05a57e8d99 100644 --- a/definitions/src/Simplex/Messaging/Client.hs +++ b/definitions/src/Simplex/Messaging/Client.hs @@ -1,62 +1,48 @@ {-# OPTIONS_GHC -fno-warn-unticked-promoted-constructors #-} {-# OPTIONS_GHC -fno-warn-orphans #-} +-- {-# OPTIONS_GHC -ddump-splices #-} {-# LANGUAGE AllowAmbiguousTypes #-} {-# LANGUAGE DataKinds #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE TemplateHaskell #-} {-# LANGUAGE TypeOperators #-} module Simplex.Messaging.Client where import ClassyPrelude -import Data.Singletons.TH import Simplex.Messaging.Protocol import Simplex.Messaging.Types --- $(protocol Recipient [d| --- raCreateConn :: (--> Broker) CreateConn --- raSubscribe :: (--> Broker) Subscribe --- rcPushConfirm :: (<-- Broker) PushConfirm --- rcPushMsg :: (<-- Broker) PushMsg --- ... --- |] - -instance Prf HasState Sender s - => ProtocolAction Recipient - Broker - CreateConnRequest CreateConnResponse - (None <==> None <==| s) - (New <==> New <==| s) - Idle Idle 0 0 - where - action = CreateConn - protoAction = rCreateConn - -instance ( (r /= None && r /= Disabled) ~ True - , (b /= None && b /= Disabled) ~ True - , Prf HasState Sender s ) - => ProtocolAction Recipient - Broker - () () - (r <==> b <==| s) - (r <==> b <==| s) - Idle Subscribed n n - where - action = Subscribe - protoAction = rSubscribe +$(protocol Recipient [d| + raCreateConn = CreateConn --> Broker + raSubscribe = Subscribe --> Broker + rcPushConfirm = PushConfirm <-- Broker + rcPushMsg = PushMsg <-- Broker + |]) -rCreateConn :: Connection Recipient None Idle - -> CreateConnRequest - -> Either String CreateConnResponse - -> Either String (Connection Recipient New Idle) -rCreateConn = protoActionStub +raCreateConn :: Connection Recipient None Idle + -> CreateConnRequest + -> Either String CreateConnResponse + -> Either String (Connection Recipient New Idle) +raCreateConn = protoActionStub -rSubscribe :: Connection Recipient s Idle - -> () - -> Either String () - -> Either String (Connection Recipient s Subscribed) -rSubscribe = protoActionStub +raSubscribe :: Connection Recipient s Idle + -> () + -> Either String () + -> Either String (Connection Recipient s Subscribed) +raSubscribe = protoActionStub + +rcPushConfirm :: Connection Recipient Pending Subscribed + -> SecureConnRequest + -> Either String ((), Connection Recipient Confirmed Subscribed) +rcPushConfirm = protoCmdStub + +rcPushMsg :: Connection Recipient Secured Subscribed + -> MessagesResponse -- TODO, has to be a single message + -> Either String ((), Connection Recipient Secured Subscribed) +rcPushMsg = protoCmdStub diff --git a/definitions/src/Simplex/Messaging/Protocol.hs b/definitions/src/Simplex/Messaging/Protocol.hs index 6a40838c4c..b67cabe8ff 100644 --- a/definitions/src/Simplex/Messaging/Protocol.hs +++ b/definitions/src/Simplex/Messaging/Protocol.hs @@ -21,6 +21,7 @@ module Simplex.Messaging.Protocol where import ClassyPrelude +import Control.Monad.Fail import Data.Kind import Data.Singletons import Data.Singletons.ShowSing @@ -28,11 +29,15 @@ import Data.Singletons.TH import Data.Type.Predicate import Data.Type.Predicate.Auto import GHC.TypeLits +import Language.Haskell.TH hiding (Type) +import qualified Language.Haskell.TH as TH import Predicate import Simplex.Messaging.Types +-- import Text.Show.Pretty (ppShow) $(singletons [d| data Participant = Recipient | Broker | Sender + deriving (Show, Eq) data ConnectionState = None -- (all) not available or removed from the broker | New -- (participants: all) connection created (or received from sender) @@ -120,14 +125,21 @@ deriving instance Show (rs <==> bs <==| ss) st2 :: Pending <==> New <==| Confirmed st2 = SPending :<==> SNew :<==| SConfirmed --- this must not type check +-- | Using not allowed connection type results in type error +-- +-- >>> :{ -- stBad :: 'Pending <==> 'Confirmed <==| 'Confirmed -- stBad = SPending :<==> SConfirmed :<==| SConfirmed +-- :} +-- ... +-- ... No instance for (Auto (TyPred BrokerCS) 'Confirmed) +-- ... arising from a use of ‘:<==>’ +-- ... infixl 4 :>>, :>>= -data Command arg result +data Command arg res (from :: Participant) (to :: Participant) state state' (ss :: ConnSubscription) (ss' :: ConnSubscription) @@ -239,20 +251,6 @@ data Command arg result Fail :: String -> Command a String from to state (None <==> None <==| None) ss ss n n --- redifine Monad operators to compose commands --- using `do` notation with RebindableSyntax extension -(>>=) :: Command a b from1 to1 s1 s2 ss1 ss2 n1 n2 - -> (b -> Command b c from2 to2 s2 s3 ss2 ss3 n2 n3) - -> Command a c from1 to2 s1 s3 ss1 ss3 n1 n3 -(>>=) = (:>>=) - -(>>) :: Command a b from1 to1 s1 s2 ss1 ss2 n1 n2 - -> Command c d from2 to2 s2 s3 ss2 ss3 n2 n3 - -> Command a d from1 to2 s1 s3 ss1 ss3 n1 n3 -(>>) = (:>>) - -fail :: String -> Command a String from to state (None <==> None <==| None) ss ss n n -fail = Fail -- show and validate expexcted command participants infix 6 --> @@ -270,42 +268,157 @@ type family PConnSt (p :: Participant) state where -- Type classes to ensure consistency of types of implementations --- of participants actions/functions and connection state transitions (types) +-- of participants commands/actions and connection state transitions (types) -- with types of protocol commands defined above. +-- One participant's command is another participant's action. -class ProtocolCommand (p :: Participant) - (from :: Participant) +class ProtocolCommand arg res + (from :: Participant) (to :: Participant) state state' (ss :: ConnSubscription) (ss' :: ConnSubscription) - (n :: Nat) (n' :: Nat) + (messages :: Nat) (messages' :: Nat) where - command :: Command arg res from p state state' ss ss' n n' - protoCmd :: Connection p (PConnSt p state) ss + command :: Command arg res from to state state' ss ss' messages messages' + cmdMe :: Sing to + cmdOther :: Sing from + protoCmd :: Connection to (PConnSt to state) ss -> arg - -> Either String (res, Connection p (PConnSt p state') ss') + -> Either String (res, Connection to (PConnSt to state') ss') -protoCmdStub :: Connection p ps ss +protoCmdStub :: Connection to ps ss -> arg - -> Either String (res, Connection p ps' ss') + -> Either String (res, Connection to ps' ss') protoCmdStub _ _ = Left "Command not implemented" -class ProtocolAction (p :: Participant) - (to :: Participant) +class ProtocolAction arg res + (from :: Participant) (to :: Participant) state state' (ss :: ConnSubscription) (ss' :: ConnSubscription) - (n :: Nat) (n' :: Nat) + (messages :: Nat) (messages' :: Nat) where - action :: Command arg res p to state state' ss ss' n n' - protoAction :: Connection p (PConnSt p state) ss + action :: Command arg res from to state state' ss ss' messages messages' + actionMe :: Sing from + actionOther :: Sing to + protoAction :: Connection from (PConnSt from state) ss -> arg -> Either String res - -> Either String (Connection p (PConnSt p state') ss') + -> Either String (Connection from (PConnSt from state') ss') -protoActionStub :: Connection p ps ss +protoActionStub :: Connection from ps ss -> arg -> Either String res - -> Either String (Connection p ps' ss') + -> Either String (Connection from ps' ss') protoActionStub _ _ _ = Left "Action not implemented" + + +-- TH to generate typeclasse instances for ProtocolCommand +-- and ProtocolAction classes from implementation definition syntax. +-- +-- Given this declaration: +-- +-- $(protocol Recipient [d| +-- rcPushConfirm = PushConfirm <-- Broker +-- raCreateConn = CreateConn --> Broker +-- |]) +-- +-- two instance declarations will be generated: +-- - for ProtocolCommand with `protoCmd = rcPushConfirm` and `command = PushConfirm` +-- - for ProtocolAction class with `protoAction = raCreateConn` and `action = CreateConn` +-- matching PushConfirm and CreateConn constructors types +-- Type definitions for functions rcPushConfirm and raCreateConn have to be written manually - +-- they have to be consistent with the typeclass. + +data ProtocolOpeartion = POCommand | POAction | POUndefined +data ProtocolClassDescription = ProtocolClassDescription + { clsName :: String + , mthd :: String + , meSing :: String + , otherSing :: String + , protoMthd :: String } + +protocol :: Participant -> Q [Dec] -> Q [Dec] +protocol me ds = ds >>= mapM mkProtocolInstance + where + getCls :: ProtocolOpeartion -> Maybe ProtocolClassDescription + getCls POUndefined = Nothing + getCls POCommand = Just ProtocolClassDescription + { clsName = "ProtocolCommand" + , mthd = "command" + , meSing = "cmdMe" + , otherSing = "cmdOther" + , protoMthd = "protoCmd" } + getCls POAction = Just ProtocolClassDescription + { clsName = "ProtocolAction" + , mthd = "action" + , meSing = "actionMe" + , otherSing = "actionOther" + , protoMthd = "protoAction" } + + mkProtocolInstance :: Dec -> Q Dec + mkProtocolInstance d = case d of + ValD + (VarP fName) + (NormalB + (InfixE + (Just (ConE cmd)) + opExp + (Just (ConE other)))) [] -> + case getCls (getOperation opExp) of + Nothing -> badSyntax d + Just cls -> instanceDecl d fName cmd other cls + _ -> badSyntax d + + instanceDecl :: Dec + -> Name -> Name -> Name + -> ProtocolClassDescription + -> Q Dec + instanceDecl d fName cmd other ProtocolClassDescription{..} = + reify cmd >>= \case + DataConI _ (ForallT _ ctxs ty) _ -> do + tc <- changeTyCon d ty clsName + return $ + InstanceD Nothing ctxs tc + [ mkMethod mthd (ConE cmd) + , mkMethod meSing (mkSing $ show me) + , mkMethod otherSing (mkSing $ nameBase other) + , mkMethod protoMthd (VarE . mkName $ nameBase fName) ] + _ -> badSyntax d + + mkMethod :: String -> Exp -> Dec + mkMethod name rhs = ValD (VarP (mkName name)) (NormalB rhs) [] + + mkSing :: String -> Exp + mkSing = ConE . mkName . ('S':) + + changeTyCon :: Dec -> TH.Type -> String -> Q TH.Type + changeTyCon d (AppT t1 t2) n = + (`AppT` t2) <$> changeTyCon d t1 n + changeTyCon d (ConT name) n = + if nameBase name == "Command" + then conT $ mkName n + else badConstructor d + changeTyCon d _ _ = badConstructor d + + badConstructor :: Dec -> Q TH.Type + badConstructor d = fail $ "constructor type must be Command\n" ++ pprint d + + getOperation :: Exp -> ProtocolOpeartion + getOperation = \case + VarE name -> getOp name + UnboundVarE name -> getOp name + _ -> POUndefined + where + getOp n = case nameBase n of + "<--" -> POCommand + "-->" -> POAction + _ -> POUndefined + + badSyntax :: Dec -> Q Dec + badSyntax d = fail $ "invalid protocol syntax: " ++ pprint d + + +-- introspect :: Name -> Q Exp +-- introspect n = reify n >>= runIO . putStrLn . pack . ppShow >> [|return ()|] diff --git a/definitions/src/Simplex/Messaging/ProtocolDo.hs b/definitions/src/Simplex/Messaging/ProtocolDo.hs new file mode 100644 index 0000000000..7e1ddbee07 --- /dev/null +++ b/definitions/src/Simplex/Messaging/ProtocolDo.hs @@ -0,0 +1,23 @@ +{-# OPTIONS_GHC -fno-warn-unticked-promoted-constructors #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE TypeOperators #-} + +module Simplex.Messaging.ProtocolDo where + +import ClassyPrelude +import Simplex.Messaging.Protocol + +-- redifine Monad operators to compose commands +-- using `do` notation with RebindableSyntax extension +(>>=) :: Command a b from1 to1 s1 s2 ss1 ss2 n1 n2 + -> (b -> Command b c from2 to2 s2 s3 ss2 ss3 n2 n3) + -> Command a c from1 to2 s1 s3 ss1 ss3 n1 n3 +(>>=) = (:>>=) + +(>>) :: Command a b from1 to1 s1 s2 ss1 ss2 n1 n2 + -> Command c d from2 to2 s2 s3 ss2 ss3 n2 n3 + -> Command a d from1 to2 s1 s3 ss1 ss3 n1 n3 +(>>) = (:>>) + +fail :: String -> Command a String from to state (None <==> None <==| None) ss ss n n +fail = Fail diff --git a/definitions/src/Simplex/Messaging/Scenarios.hs b/definitions/src/Simplex/Messaging/Scenarios.hs index c60395aaf2..dfb9aa487d 100644 --- a/definitions/src/Simplex/Messaging/Scenarios.hs +++ b/definitions/src/Simplex/Messaging/Scenarios.hs @@ -12,6 +12,7 @@ module Simplex.Messaging.Scenarios where import ClassyPrelude hiding ((>>=), (>>), fail) import Data.Singletons import Simplex.Messaging.Protocol +import Simplex.Messaging.ProtocolDo import Simplex.Messaging.Types r :: Sing Recipient diff --git a/definitions/tests/doctest-driver.hs b/definitions/tests/doctest-driver.hs new file mode 100644 index 0000000000..48e0aa73d9 --- /dev/null +++ b/definitions/tests/doctest-driver.hs @@ -0,0 +1 @@ +{-# OPTIONS_GHC -F -pgmF doctest-driver-gen -optF src -optF -XBlockArguments -optF -XDuplicateRecordFields -optF -XLambdaCase -optF -XNamedFieldPuns -optF -XNoImplicitPrelude -optF -XOverloadedStrings -optF -XRecordWildCards -optF -XAllowAmbiguousTypes -optF -XConstraintKinds -optF -XDeriveAnyClass -optF -XEmptyCase -optF -XFlexibleContexts -optF -XFlexibleInstances -optF -XGADTs -optF -XInstanceSigs -optF -XMultiParamTypeClasses -optF -XNoStarIsType -optF -XScopedTypeVariables -optF -XStandaloneDeriving -optF -XTemplateHaskell -optF -XTypeApplications -optF -XTypeFamilies -optF -XTypeInType -optF -XTypeOperators -optF -XUndecidableInstances #-}