{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MagicHash #-}
{-# LANGUAGE NamedFieldPuns #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeApplications #-}
{-# OPTIONS_GHC -Wno-unused-imports #-}
{-# OPTIONS_GHC -split-sections #-}

module TypedSession.TH (protocol, protocol') where

import Control.Monad (forM, when)
import Data.Either (fromRight)
import Data.IFunctor (Sing, SingI (..))
import Data.Kind
import qualified Data.Set as Set
import Data.Traversable (for)
import GHC.Exts (DataToTag (..), Int (..))
import Language.Haskell.TH hiding (Type)
import qualified Language.Haskell.TH as TH
import Language.Haskell.TH.Quote
import TypedSession.Core (SingToInt (..))
import qualified TypedSession.Core as TSC
import TypedSession.State.Parser (runProtocolParser)
import TypedSession.State.Pipeline (PipeResult (..), genGraph, pipe)
import TypedSession.State.Render
import TypedSession.State.Type (BranchSt (..), Creat, MsgOrLabel (..), MsgT1, Protocol (..), ProtocolError, T (..))

roleDecs :: Name -> Q [Dec]
roleDecs :: Name -> Q [Dec]
roleDecs Name
name = do
  res <- Name -> Q Info
reify Name
name
  case res of
    TyConI (DataD [] Name
dName [] Maybe Pred
Nothing [Con]
cons [DerivClause]
_) -> do
      aVar <- String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
newName String
"a"
      xVar <- newName "x"
      let
        addPerfixS :: Name -> Name
        addPerfixS Name
vname =
          let n :: String
n = (Name -> String
nameBase Name
vname)
           in String -> Name
mkName (String
"S" String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
n)

        roleSingleton =
          [ [Pred]
-> Name
-> [TyVarBndr BndrVis]
-> Maybe Pred
-> [Con]
-> [DerivClause]
-> Dec
DataD
              []
              (Name -> Name
addPerfixS Name
dName)
              [Name -> BndrVis -> Pred -> TyVarBndr BndrVis
forall flag. Name -> flag -> Pred -> TyVarBndr flag
KindedTV Name
aVar BndrVis
BndrReq (Name -> Pred
ConT Name
dName)]
              Maybe Pred
forall a. Maybe a
Nothing
              [[Name] -> [BangType] -> Pred -> Con
GadtC [Name -> Name
addPerfixS Name
n] [] (Pred -> Pred -> Pred
AppT (Name -> Pred
ConT (Name -> Name
addPerfixS Name
dName)) (Name -> Pred
PromotedT Name
n)) | NormalC Name
n [] <- [Con]
cons]
              []
          ]
        singToSRole = [TySynEqn -> Dec
TySynInstD (Maybe [TyVarBndr ()] -> Pred -> Pred -> TySynEqn
TySynEqn Maybe [TyVarBndr ()]
forall a. Maybe a
Nothing (Name -> Pred
ConT ''Sing) (Name -> Pred
ConT (Name -> Name
addPerfixS Name
dName)))]
        instanceSingI =
          [ Maybe Overlap -> [Pred] -> Pred -> [Dec] -> Dec
InstanceD
              Maybe Overlap
forall a. Maybe a
Nothing
              []
              (Pred -> Pred -> Pred
AppT (Name -> Pred
ConT ''SingI) (Name -> Pred
PromotedT Name
n))
              [Name -> [Clause] -> Dec
FunD 'sing [[Pat] -> Body -> [Dec] -> Clause
Clause [] (Exp -> Body
NormalB (Name -> Exp
ConE (Name -> Name
addPerfixS Name
n))) []]]
          | NormalC Name
n [] <- [Con]
cons
          ]
        instanceSingToInt =
          [ Maybe Overlap -> [Pred] -> Pred -> [Dec] -> Dec
InstanceD
              Maybe Overlap
forall a. Maybe a
Nothing
              []
              (Pred -> Pred -> Pred
AppT (Name -> Pred
ConT ''SingToInt) (Name -> Pred
ConT Name
name))
              [ Name -> [Clause] -> Dec
FunD
                  'singToInt
                  [[Pat] -> Body -> [Dec] -> Clause
Clause [Name -> Pat
VarP Name
xVar] (Exp -> Body
NormalB (Exp -> Exp -> Exp
AppE (Name -> Exp
ConE 'I#) (Exp -> Exp -> Exp
AppE (Name -> Exp
VarE 'dataToTag#) (Name -> Exp
VarE Name
xVar)))) []]
              ]
          ]
      pure $ roleSingleton ++ singToSRole ++ instanceSingI ++ instanceSingToInt
    Info
_ -> String -> Q [Dec]
forall a. HasCallStack => String -> a
error (String -> Q [Dec]) -> String -> Q [Dec]
forall a b. (a -> b) -> a -> b
$ String
"Name: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Name -> String
forall a. Show a => a -> String
show Name
name String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" is not a data constructor"

protDecsAndMsgDecs :: forall r bst. (Show r, Show bst, Enum r, Bounded r) => String -> Name -> Name -> PipeResult r bst -> Q [Dec]
protDecsAndMsgDecs :: forall r bst.
(Show r, Show bst, Enum r, Bounded r) =>
String -> Name -> Name -> PipeResult r bst -> Q [Dec]
protDecsAndMsgDecs String
protN Name
roleName Name
bstName PipeResult{Protocol (MsgT r bst) r bst
msgT :: Protocol (MsgT r bst) r bst
msgT :: forall r bst. PipeResult r bst -> Protocol (MsgT r bst) r bst
msgT, Protocol (MsgT1 r bst) r bst
msgT1 :: Protocol (MsgT1 r bst) r bst
msgT1 :: forall r bst. PipeResult r bst -> Protocol (MsgT1 r bst) r bst
msgT1, Set Int
dnySet :: Set Int
dnySet :: forall r bst. PipeResult r bst -> Set Int
dnySet, [Int]
stList :: [Int]
stList :: forall r bst. PipeResult r bst -> [Int]
stList, [(String, [(bst, [[String]], T bst)])]
branchResultTypeInfo :: [(String, [(bst, [[String]], T bst)])]
branchResultTypeInfo :: forall r bst.
PipeResult r bst -> [(String, [(bst, [[String]], T bst)])]
branchResultTypeInfo, [(r, String, T bst)]
branchFunList :: [(r, String, T bst)]
branchFunList :: forall r bst. PipeResult r bst -> [(r, String, T bst)]
branchFunList, [(String, [T bst], [T bst])]
allMsgBATypes :: [(String, [T bst], [T bst])]
allMsgBATypes :: forall r bst. PipeResult r bst -> [(String, [T bst], [T bst])]
allMsgBATypes} = do
  let protName :: Name
protName = String -> Name
mkName String
protN
      protSName :: Name
protSName = String -> Name
mkName (String
"S" String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
protN)
      mkSiName :: a -> Name
mkSiName a
i = String -> Name
mkName (String -> Name) -> String -> Name
forall a b. (a -> b) -> a -> b
$ String
"S" String -> String -> String
forall a. Semigroup a => a -> a -> a
<> a -> String
forall a. Show a => a -> String
show a
i
      mkSSiName :: a -> Name
mkSSiName a
i = String -> Name
mkName (String -> Name) -> String -> Name
forall a b. (a -> b) -> a -> b
$ String
"SS" String -> String -> String
forall a. Semigroup a => a -> a -> a
<> a -> String
forall a. Show a => a -> String
show a
i
      genConstr :: Int -> Con
genConstr Int
i =
        if Int
i Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== -Int
1
          then Name -> [BangType] -> Con
NormalC (String -> Name
mkName String
"End") []
          else
            if Int
i Int -> Set Int -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` Set Int
dnySet
              then
                Name -> [BangType] -> Con
NormalC
                  (Int -> Name
forall {a}. Show a => a -> Name
mkSiName Int
i)
                  [(SourceUnpackedness -> SourceStrictness -> Bang
Bang SourceUnpackedness
NoSourceUnpackedness SourceStrictness
NoSourceStrictness, Name -> Pred
ConT Name
bstName)]
              else Name -> [BangType] -> Con
NormalC (Int -> Name
forall {a}. Show a => a -> Name
mkSiName Int
i) []
      -- generate protocol data type
      dataProt :: [Dec]
dataProt = [[Pred]
-> Name
-> [TyVarBndr BndrVis]
-> Maybe Pred
-> [Con]
-> [DerivClause]
-> Dec
DataD [] Name
protName [] Maybe Pred
forall a. Maybe a
Nothing [Int -> Con
genConstr Int
i | Int
i <- [Int]
stList] []]

  let tAnyToType :: Name -> T bst -> TH.Type
      tAnyToType :: Name -> T bst -> Pred
tAnyToType Name
s = \case
        TNum Int
i -> Name -> Pred
PromotedT (Int -> Name
forall {a}. Show a => a -> Name
mkSiName Int
i)
        BstList Int
i bst
bst -> Pred -> Pred -> Pred
AppT (Name -> Pred
PromotedT (Int -> Name
forall {a}. Show a => a -> Name
mkSiName Int
i)) (Name -> Pred
PromotedT (String -> Name
mkName (bst -> String
forall a. Show a => a -> String
show bst
bst)))
        TAny Int
i -> Pred -> Pred -> Pred
AppT (Name -> Pred
PromotedT (Int -> Name
forall {a}. Show a => a -> Name
mkSiName Int
i)) (Name -> Pred
VarT Name
s)
        T bst
TEnd -> Name -> Pred
PromotedT (Name -> Pred) -> Name -> Pred
forall a b. (a -> b) -> a -> b
$ String -> Name
mkName String
"End"
      mkArgs :: [[String]] -> [BangType]
mkArgs [[String]]
args =
        [ ( SourceUnpackedness -> SourceStrictness -> Bang
Bang SourceUnpackedness
NoSourceUnpackedness SourceStrictness
NoSourceStrictness
          , case [String]
ag of
              [] -> String -> Pred
forall a. HasCallStack => String -> a
error String
"np"
              (String
x : [String]
xs) -> (Pred -> Pred -> Pred) -> Pred -> [Pred] -> Pred
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' Pred -> Pred -> Pred
AppT (Name -> Pred
ConT (String -> Name
mkName String
x)) ((String -> Pred) -> [String] -> [Pred]
forall a b. (a -> b) -> [a] -> [b]
map (Name -> Pred
ConT (Name -> Pred) -> (String -> Name) -> String -> Pred
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Name
mkName) [String]
xs)
          )
        | [String]
ag <- [[String]]
args
        ]
      typeListT :: [TH.Type] -> TH.Type
      typeListT :: [Pred] -> Pred
typeListT = (Pred -> Pred -> Pred) -> [Pred] -> Pred
forall a. (a -> a -> a) -> [a] -> a
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldl1 Pred -> Pred -> Pred
AppT

      isTAny :: T bst -> Bool
      isTAny :: T bst -> Bool
isTAny = \case
        TAny Int
_ -> Bool
True
        T bst
_ -> Bool
False

  sVar <- String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
newName String
"s"
  aVar <- newName "a"
  let genSConstr Int
i =
        if Int
i Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== -Int
1
          then
            [Name] -> [BangType] -> Pred -> Con
GadtC [String -> Name
mkName String
"SEnd"] [] (Pred -> Pred -> Pred
AppT (Name -> Pred
ConT Name
protSName) (Name -> Pred
PromotedT (String -> Name
mkName String
"End")))
          else
            if Int
i Int -> Set Int -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` Set Int
dnySet
              then
                [TyVarBndr Specificity] -> [Pred] -> Con -> Con
ForallC
                  [Name -> Specificity -> Pred -> TyVarBndr Specificity
forall flag. Name -> flag -> Pred -> TyVarBndr flag
KindedTV Name
sVar Specificity
SpecifiedSpec (Name -> Pred
ConT Name
bstName)]
                  []
                  ( [Name] -> [BangType] -> Pred -> Con
GadtC
                      [Int -> Name
forall {a}. Show a => a -> Name
mkSSiName Int
i]
                      []
                      (Pred -> Pred -> Pred
AppT (Name -> Pred
ConT Name
protSName) (Pred -> Pred -> Pred
AppT (Name -> Pred
PromotedT (Name -> Pred) -> Name -> Pred
forall a b. (a -> b) -> a -> b
$ Int -> Name
forall {a}. Show a => a -> Name
mkSiName Int
i) (Name -> Pred
VarT Name
sVar)))
                  )
              else
                [Name] -> [BangType] -> Pred -> Con
GadtC [Int -> Name
forall {a}. Show a => a -> Name
mkSSiName Int
i] [] (Pred -> Pred -> Pred
AppT (Name -> Pred
ConT Name
protSName) (Name -> Pred
PromotedT (Name -> Pred) -> Name -> Pred
forall a b. (a -> b) -> a -> b
$ Int -> Name
forall {a}. Show a => a -> Name
mkSiName Int
i))
      -- generate protocol singleton data type
      dataSingletonProt = [[Pred]
-> Name
-> [TyVarBndr BndrVis]
-> Maybe Pred
-> [Con]
-> [DerivClause]
-> Dec
DataD [] Name
protSName [Name -> BndrVis -> Pred -> TyVarBndr BndrVis
forall flag. Name -> flag -> Pred -> TyVarBndr flag
KindedTV Name
aVar BndrVis
BndrReq (Name -> Pred
ConT Name
protName)] Maybe Pred
forall a. Maybe a
Nothing [Int -> Con
genSConstr Int
i | Int
i <- [Int]
stList] []]

  -- generate type family Sing to Singleton protocol
  let singSingletonProt = [TySynEqn -> Dec
TySynInstD (Maybe [TyVarBndr ()] -> Pred -> Pred -> TySynEqn
TySynEqn Maybe [TyVarBndr ()]
forall a. Maybe a
Nothing (Name -> Pred
ConT ''Sing) (Name -> Pred
ConT Name
protSName))]

  aVar1 <- newName "a"
  let branchResultDatas =
        [ [Pred]
-> Name
-> [TyVarBndr BndrVis]
-> Maybe Pred
-> [Con]
-> [DerivClause]
-> Dec
DataD
            []
            Name
dataName
            [Name -> BndrVis -> Pred -> TyVarBndr BndrVis
forall flag. Name -> flag -> Pred -> TyVarBndr flag
KindedTV Name
aVar1 BndrVis
BndrReq (Name -> Pred
ConT Name
protName)]
            Maybe Pred
forall a. Maybe a
Nothing
            [ [Name] -> [BangType] -> Pred -> Con
GadtC [Name
constrName] ([[String]] -> [BangType]
mkArgs [[String]]
args) (Pred -> Pred -> Pred
AppT (Name -> Pred
ConT Name
dataName) (Name -> T bst -> Pred
tAnyToType (String -> Name
mkName String
"s") T bst
t))
            | (bst
bst, [[String]]
args, T bst
t) <- [(bst, [[String]], T bst)]
constrs
            , let constrName :: Name
constrName = String -> Name
mkName (String
"BranchSt_" String -> String -> String
forall a. Semigroup a => a -> a -> a
<> bst -> String
forall a. Show a => a -> String
show bst
bst)
            ]
            []
        | (String
name, [(bst, [[String]], T bst)]
constrs) <- [(String, [(bst, [[String]], T bst)])]
branchResultTypeInfo
        , let dataName :: Name
dataName = String -> Name
mkName String
name
        ]
  branchFunTypes <- for branchFunList $ \(r
r, String
st, T bst
t) -> do
    mVar <- String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
newName String
"m"
    pure
      ( TySynD
          (mkName (st <> "Fun"))
          [KindedTV mVar BndrReq (AppT (AppT ArrowT StarT) StarT)]
          ( typeListT
              [ ConT ''TSC.Peer
              , ConT roleName
              , ConT protName
              , ConT (mkName (show r))
              , VarT mVar
              , ConT (mkName st)
              , (tAnyToType (mkName "s") t)
              ]
          )
      )
  let firstTList = case Protocol (MsgT r bst) r bst
msgT of
        Msg ([T bst]
ts, (r, r)
_, Int
_) String
_ [[String]]
_ r
_ r
_ :> Protocol (MsgT r bst) r bst
_ -> [T bst]
ts
        Label ([T bst]
ts, Int
_) Int
_ :> Protocol (MsgT r bst) r bst
_ -> [T bst]
ts
        Branch XBranch (MsgT r bst)
ts r
_ String
_ [BranchSt (MsgT r bst) r bst]
_ -> [T bst]
XBranch (MsgT r bst)
ts
        Goto ([T bst]
ts, Int
_) Int
_ -> [T bst]
ts
        Terminal XTerminal (MsgT r bst)
ts -> [T bst]
XTerminal (MsgT r bst)
ts

      mkTySynDFun Name
name T bst
t =
        if T bst -> Bool
isTAny T bst
t
          then do
            sVar1 <- forall (m :: * -> *). Quote m => String -> m Name
newName @Q String
"s"
            pure (TySynD name [KindedTV sVar1 BndrReq (ConT bstName)] (tAnyToType sVar1 t))
          else Dec -> Q Dec
forall a. a -> Q a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Name -> [TyVarBndr BndrVis] -> Pred -> Dec
TySynD Name
name [] (Name -> T bst -> Pred
tAnyToType (String -> Name
mkName String
"s") T bst
t))

      mkAllRoleTySynDFun r -> Name
nameFun [T bst]
ts =
        [(r, T bst)] -> ((r, T bst) -> Q Dec) -> Q [Dec]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
t a -> (a -> f b) -> f (t b)
for ([r] -> [T bst] -> [(r, T bst)]
forall a b. [a] -> [b] -> [(a, b)]
zip [forall a. Bounded a => a
minBound @r .. r
forall a. Bounded a => a
maxBound] [T bst]
ts) (((r, T bst) -> Q Dec) -> Q [Dec])
-> ((r, T bst) -> Q Dec) -> Q [Dec]
forall a b. (a -> b) -> a -> b
$
          \(r
r, T bst
t) -> Name -> T bst -> Q Dec
mkTySynDFun (r -> Name
nameFun r
r) T bst
t

  roleStartSts <- mkAllRoleTySynDFun (\r
r -> (String -> Name
mkName (r -> String
forall a. Show a => a -> String
show r
r String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
"StartSt"))) firstTList

  allMsgBADecs <-
    concat <$> do
      for allMsgBATypes $ \(String
cname, [T bst]
beforeSt, [T bst]
afterSt) -> do
        bfs <- (r -> Name) -> [T bst] -> Q [Dec]
mkAllRoleTySynDFun (\r
r -> String -> Name
mkName (r -> String
forall a. Show a => a -> String
show r
r String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
"Before" String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
cname String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
"St")) [T bst]
beforeSt
        afs <- mkAllRoleTySynDFun (\r
r -> String -> Name
mkName (r -> String
forall a. Show a => a -> String
show r
r String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
"After" String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
cname String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
"St")) afterSt
        pure (bfs <> afs)

  s1 <- newName "s1"
  -- generate instance SingI
  let instanceSingI =
        [ Maybe Overlap -> [Pred] -> Pred -> [Dec] -> Dec
InstanceD
            Maybe Overlap
forall a. Maybe a
Nothing
            []
            ( Pred -> Pred -> Pred
AppT
                (Name -> Pred
ConT ''SingI)
                ( if Int
i Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== -Int
1
                    then Name -> Pred
PromotedT (String -> Name
mkName String
"End")
                    else
                      if Int
i Int -> Set Int -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` Set Int
dnySet
                        then Pred -> Pred -> Pred
SigT (Pred -> Pred -> Pred
AppT (Name -> Pred
PromotedT (Int -> Name
forall {a}. Show a => a -> Name
mkSiName Int
i)) (Name -> Pred
VarT Name
s1)) (Name -> Pred
ConT Name
protName)
                        else Name -> Pred
PromotedT (Int -> Name
forall {a}. Show a => a -> Name
mkSiName Int
i)
                )
            )
            [Name -> [Clause] -> Dec
FunD 'sing [[Pat] -> Body -> [Dec] -> Clause
Clause [] (Exp -> Body
NormalB (Name -> Exp
ConE (String -> Name
mkName (String -> Name) -> String -> Name
forall a b. (a -> b) -> a -> b
$ String
"S" String -> String -> String
forall a. Semigroup a => a -> a -> a
<> (if Int
i Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== -Int
1 then String
"End" else (String
"S" String -> String -> String
forall a. Semigroup a => a -> a -> a
<> Int -> String
forall a. Show a => a -> String
show Int
i))))) []]]
        | Int
i <- [Int]
stList
        ]

  xVar <- newName "x"
  -- generate instance SingToInt
  let instanceSingToInt =
        [ Maybe Overlap -> [Pred] -> Pred -> [Dec] -> Dec
InstanceD
            Maybe Overlap
forall a. Maybe a
Nothing
            []
            (Pred -> Pred -> Pred
AppT (Name -> Pred
ConT ''SingToInt) (Name -> Pred
ConT Name
protName))
            [ Name -> [Clause] -> Dec
FunD 'singToInt [[Pat] -> Body -> [Dec] -> Clause
Clause [Name -> Pat
VarP Name
xVar] (Exp -> Body
NormalB (Exp -> Exp -> Exp
AppE (Name -> Exp
ConE 'I#) (Exp -> Exp -> Exp
AppE (Name -> Exp
VarE 'dataToTag#) (Name -> Exp
VarE Name
xVar)))) []]
            ]
        ]

  -- make instance type family Done
  roleRes <- reify roleName
  instDoneDesc <- case roleRes of
    TyConI (DataD [] Name
_ [] Maybe Pred
Nothing [Con]
cons [DerivClause]
_) -> do
      [Dec] -> Q [Dec]
forall a. a -> Q a
forall (f :: * -> *) a. Applicative f => a -> f a
pure
        [ TySynEqn -> Dec
TySynInstD
            ( Maybe [TyVarBndr ()] -> Pred -> Pred -> TySynEqn
TySynEqn
                Maybe [TyVarBndr ()]
forall a. Maybe a
Nothing
                (Pred -> Pred -> Pred
AppT (Name -> Pred
ConT (String -> Name
mkName String
"Done")) (Name -> Pred
PromotedT Name
n))
                (Name -> Pred
PromotedT (String -> Name
mkName String
"End"))
            )
        | NormalC Name
n [] <- [Con]
cons
        ]
    Info
_ -> String -> Q [Dec]
forall a. HasCallStack => String -> a
error (String -> Q [Dec]) -> String -> Q [Dec]
forall a b. (a -> b) -> a -> b
$ String
"Name: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Name -> String
forall a. Show a => a -> String
show Name
roleName String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" is not a data constructor"

  let mkDataInstanceMsg :: Name -> Protocol (MsgT1 r bst) r bst -> Q [Con]
      mkDataInstanceMsg Name
s = \case
        Msg ((T bst
a, T bst
b, T bst
c), (r
from, r
to), Int
_) String
constr [[String]]
args r
_ r
_ :> Protocol (MsgT1 r bst) r bst
prots -> do
          let mkTName :: Pred
mkTName =
                [Pred] -> Pred
typeListT
                  [ Name -> Pred
ConT ''TSC.Msg
                  , Name -> Pred
ConT Name
roleName
                  , Name -> Pred
ConT Name
protName
                  , Name -> T bst -> Pred
tAnyToType Name
s T bst
a
                  , Name -> Pred
PromotedT (String -> Name
mkName (r -> String
forall a. Show a => a -> String
show r
from))
                  , Name -> T bst -> Pred
tAnyToType Name
s T bst
b
                  , Name -> Pred
PromotedT (String -> Name
mkName (r -> String
forall a. Show a => a -> String
show r
to))
                  , Name -> T bst -> Pred
tAnyToType Name
s T bst
c
                  ]
          let val :: Con
val =
                let gadtc :: Con
gadtc =
                      [Name] -> [BangType] -> Pred -> Con
GadtC
                        [String -> Name
mkName String
constr]
                        ([[String]] -> [BangType]
mkArgs [[String]]
args)
                        Pred
mkTName
                 in if (T bst -> Bool) -> [T bst] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any T bst -> Bool
isTAny [T bst
a, T bst
b, T bst
c]
                      then [TyVarBndr Specificity] -> [Pred] -> Con -> Con
ForallC [Name -> Specificity -> Pred -> TyVarBndr Specificity
forall flag. Name -> flag -> Pred -> TyVarBndr flag
KindedTV Name
s Specificity
SpecifiedSpec (Name -> Pred
ConT Name
bstName)] [] Con
gadtc
                      else Con
gadtc
          vals <- Name -> Protocol (MsgT1 r bst) r bst -> Q [Con]
mkDataInstanceMsg Name
s Protocol (MsgT1 r bst) r bst
prots
          pure (val : vals)
        Label XLabel (MsgT1 r bst)
_ Int
_ :> Protocol (MsgT1 r bst) r bst
prots -> Name -> Protocol (MsgT1 r bst) r bst -> Q [Con]
mkDataInstanceMsg Name
s Protocol (MsgT1 r bst) r bst
prots
        Branch XBranch (MsgT1 r bst)
_ r
_ String
_ [BranchSt (MsgT1 r bst) r bst]
ls -> do
          ls' <- [BranchSt (MsgT1 r bst) r bst]
-> (BranchSt (MsgT1 r bst) r bst -> Q [Con]) -> Q [[Con]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [BranchSt (MsgT1 r bst) r bst]
ls ((BranchSt (MsgT1 r bst) r bst -> Q [Con]) -> Q [[Con]])
-> (BranchSt (MsgT1 r bst) r bst -> Q [Con]) -> Q [[Con]]
forall a b. (a -> b) -> a -> b
$ \(BranchSt XBranchSt (MsgT1 r bst)
_ bst
_ [[String]]
_ Protocol (MsgT1 r bst) r bst
prot) -> Name -> Protocol (MsgT1 r bst) r bst -> Q [Con]
mkDataInstanceMsg Name
s Protocol (MsgT1 r bst) r bst
prot
          pure $ concat ls'
        Protocol (MsgT1 r bst) r bst
_ -> [Con] -> Q [Con]
forall a. a -> Q a
forall (f :: * -> *) a. Applicative f => a -> f a
pure []

  -- make data instance Msg
  ssVar <- newName "s"
  instMsgDesc <- mkDataInstanceMsg ssVar (msgT1)
  fromVar <- newName "from"
  sendVar <- newName "send"
  sendNewStVar <- newName "sendNewSt"
  recvVar <- newName "recv"
  receiverNewStVar <- newName "receiverNewSt"
  let instanceMsg =
        [ Maybe Overlap -> [Pred] -> Pred -> [Dec] -> Dec
InstanceD
            Maybe Overlap
forall a. Maybe a
Nothing
            []
            (Pred -> Pred -> Pred
AppT (Pred -> Pred -> Pred
AppT (Name -> Pred
ConT ''TSC.Protocol) (Name -> Pred
ConT Name
roleName)) (Name -> Pred
ConT Name
protName))
            ( [Dec]
instDoneDesc
                [Dec] -> [Dec] -> [Dec]
forall a. [a] -> [a] -> [a]
++ [ [Pred]
-> Maybe [TyVarBndr ()]
-> Pred
-> Maybe Pred
-> [Con]
-> [DerivClause]
-> Dec
DataInstD
                      []
                      ( [TyVarBndr ()] -> Maybe [TyVarBndr ()]
forall a. a -> Maybe a
Just
                          [ Name -> () -> Pred -> TyVarBndr ()
forall flag. Name -> flag -> Pred -> TyVarBndr flag
KindedTV Name
fromVar () (Name -> Pred
ConT Name
protName)
                          , Name -> () -> Pred -> TyVarBndr ()
forall flag. Name -> flag -> Pred -> TyVarBndr flag
KindedTV Name
sendVar () (Name -> Pred
ConT Name
roleName)
                          , Name -> () -> Pred -> TyVarBndr ()
forall flag. Name -> flag -> Pred -> TyVarBndr flag
KindedTV Name
sendNewStVar () (Name -> Pred
ConT Name
protName)
                          , Name -> () -> Pred -> TyVarBndr ()
forall flag. Name -> flag -> Pred -> TyVarBndr flag
KindedTV Name
recvVar () (Name -> Pred
ConT Name
roleName)
                          , Name -> () -> Pred -> TyVarBndr ()
forall flag. Name -> flag -> Pred -> TyVarBndr flag
KindedTV Name
receiverNewStVar () (Name -> Pred
ConT Name
protName)
                          ]
                      )
                      ( [Pred] -> Pred
typeListT
                          [ Name -> Pred
ConT ''TSC.Msg
                          , Name -> Pred
ConT Name
roleName
                          , Name -> Pred
ConT Name
protName
                          , (Pred -> Pred -> Pred
SigT (Name -> Pred
VarT Name
fromVar) (Name -> Pred
ConT Name
protName))
                          , (Pred -> Pred -> Pred
SigT (Name -> Pred
VarT Name
sendVar) (Name -> Pred
ConT Name
roleName))
                          , (Pred -> Pred -> Pred
SigT (Name -> Pred
VarT Name
sendNewStVar) (Name -> Pred
ConT Name
protName))
                          , (Pred -> Pred -> Pred
SigT (Name -> Pred
VarT Name
recvVar) (Name -> Pred
ConT Name
roleName))
                          , (Pred -> Pred -> Pred
SigT (Name -> Pred
VarT Name
receiverNewStVar) (Name -> Pred
ConT Name
protName))
                          ]
                      )
                      Maybe Pred
forall a. Maybe a
Nothing
                      [Con]
instMsgDesc
                      []
                   ]
            )
        ]

  pure $
    dataProt
      ++ dataSingletonProt
      ++ singSingletonProt
      ++ branchResultDatas
      ++ branchFunTypes
      ++ roleStartSts
      ++ allMsgBADecs
      ++ instanceSingI
      ++ instanceSingToInt
      ++ instanceMsg

protocol'
  :: forall r bst
   . ( Enum r
     , Bounded r
     , Show r
     , Enum bst
     , Bounded bst
     , Show bst
     , Ord r
     )
  => String -> Name -> Name -> Bool -> QuasiQuoter
protocol' :: forall r bst.
(Enum r, Bounded r, Show r, Enum bst, Bounded bst, Show bst,
 Ord r) =>
String -> Name -> Name -> Bool -> QuasiQuoter
protocol' String
protN Name
roleName Name
bstName Bool
b =
  QuasiQuoter
    { quoteExp :: String -> Q Exp
quoteExp = Q Exp -> String -> Q Exp
forall a b. a -> b -> a
const (Q Exp -> String -> Q Exp) -> Q Exp -> String -> Q Exp
forall a b. (a -> b) -> a -> b
$ String -> Q Exp
forall a. String -> Q a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"No protocol parse for exp"
    , quotePat :: String -> Q Pat
quotePat = Q Pat -> String -> Q Pat
forall a b. a -> b -> a
const (Q Pat -> String -> Q Pat) -> Q Pat -> String -> Q Pat
forall a b. (a -> b) -> a -> b
$ String -> Q Pat
forall a. String -> Q a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"No protocol parse for pat"
    , quoteType :: String -> Q Pred
quoteType = Q Pred -> String -> Q Pred
forall a b. a -> b -> a
const (Q Pred -> String -> Q Pred) -> Q Pred -> String -> Q Pred
forall a b. (a -> b) -> a -> b
$ String -> Q Pred
forall a. String -> Q a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"No protocol parser for type"
    , quoteDec :: String -> Q [Dec]
quoteDec = String -> Q [Dec]
parseOrThrow
    }
 where
  parseOrThrow :: String -> Q [Dec]
  parseOrThrow :: String -> Q [Dec]
parseOrThrow String
st = case forall r bst.
(Enum r, Enum bst, Bounded r, Bounded bst, Show r, Show bst) =>
String -> Either String (Protocol Creat r bst)
runProtocolParser @r @bst String
st of
    Left String
e -> String -> Q [Dec]
forall a. String -> Q a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String -> String
forall a. Show a => a -> String
show String
e)
    Right Protocol Creat r bst
protCreat -> case Protocol Creat r bst
-> Either (ProtocolError r bst) (PipeResult r bst)
forall r bst.
(Enum r, Bounded r, Eq r, Ord r, Show bst) =>
Protocol Creat r bst
-> Either (ProtocolError r bst) (PipeResult r bst)
pipe Protocol Creat r bst
protCreat of
      Left ProtocolError r bst
e -> String -> Q [Dec]
forall a. String -> Q a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (ProtocolError r bst -> String
forall a. Show a => a -> String
show ProtocolError r bst
e)
      Right PipeResult r bst
pipResult -> do
        let graphStr :: String
graphStr = forall r bst.
(Enum r, Bounded r, Show bst, Ord r, Show r) =>
PipeResult r bst -> String
genGraph @r @bst PipeResult r bst
pipResult
        Bool -> Q () -> Q ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
b (Q () -> Q ()) -> Q () -> Q ()
forall a b. (a -> b) -> a -> b
$ IO () -> Q ()
forall a. IO a -> Q a
runIO (IO () -> Q ()) -> IO () -> Q ()
forall a b. (a -> b) -> a -> b
$ do
          String -> String -> IO ()
writeFile (String
protN String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
".prot") String
graphStr
          String -> IO ()
putStrLn String
graphStr
        d1 <- Name -> Q [Dec]
roleDecs Name
roleName
        d2 <- protDecsAndMsgDecs protN roleName bstName pipResult
        pure (d1 ++ d2)

protocol
  :: forall r bst
   . ( Enum r
     , Bounded r
     , Show r
     , Enum bst
     , Bounded bst
     , Show bst
     , Ord r
     )
  => String -> Name -> Name -> QuasiQuoter
protocol :: forall r bst.
(Enum r, Bounded r, Show r, Enum bst, Bounded bst, Show bst,
 Ord r) =>
String -> Name -> Name -> QuasiQuoter
protocol String
protN Name
roleName Name
bstName =
  forall r bst.
(Enum r, Bounded r, Show r, Enum bst, Bounded bst, Show bst,
 Ord r) =>
String -> Name -> Name -> Bool -> QuasiQuoter
protocol' @r @bst String
protN Name
roleName Name
bstName Bool
False