e071fb22ea9923a2a4ff41184d80ca46b55ee932Till MossakowskiDescription : Pretty printing for CspCASL
020cdb5dad6b871aba61136a0e1567c00426de87Andy GimblettCopyright : (c) Andy Gimblett and Uni Bremen 2006
98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuLicense : GPLv2 or higher, see LICENSE.txt
020cdb5dad6b871aba61136a0e1567c00426de87Andy GimblettMaintainer : a.m.gimblett@swansea.ac.uk
020cdb5dad6b871aba61136a0e1567c00426de87Andy GimblettStability : provisional
020cdb5dad6b871aba61136a0e1567c00426de87Andy GimblettPortability : portable
020cdb5dad6b871aba61136a0e1567c00426de87Andy GimblettPrinting abstract syntax of CSP-CASL
50c62c8c45643f09bcb2f4a99b07bf1d072ecf40Christian Maederimport Common.Keywords (elseS, ifS, thenS, opS, predS)
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reillyimport qualified Data.Set as Set
12b2ae689353ecbaad720a9af9f9be01c1a3fe2dChristian Maederinstance Pretty CspBasicExt where
12b2ae689353ecbaad720a9af9f9be01c1a3fe2dChristian Maeder pretty = printCspBasicExt
12b2ae689353ecbaad720a9af9f9be01c1a3fe2dChristian Maederinstance ListCheck CHANNEL_DECL where
12b2ae689353ecbaad720a9af9f9be01c1a3fe2dChristian Maeder innerList (ChannelDecl l _) = innerList l
12b2ae689353ecbaad720a9af9f9be01c1a3fe2dChristian MaederprintCspBasicExt :: CspBasicExt -> Doc
12b2ae689353ecbaad720a9af9f9be01c1a3fe2dChristian MaederprintCspBasicExt ccs = case ccs of
8db2221917c1bc569614f3481bcdb3b988facaedChristian Maeder Channels cs _ -> keyword (channelS ++ pluralS cs)
12b2ae689353ecbaad720a9af9f9be01c1a3fe2dChristian Maeder <+> semiAnnos printChanDecl cs
8db2221917c1bc569614f3481bcdb3b988facaedChristian Maeder ProcItems ps _ -> keyword processS
12b2ae689353ecbaad720a9af9f9be01c1a3fe2dChristian Maeder <+> semiAnnos printProcItem ps
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reillyinstance Pretty FQ_PROCESS_NAME where
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly pretty = printProcessName
9f93b2a8b552789cd939d599504d39732672dc84Christian Maeder-- | Pretty printing for process profiles
9f93b2a8b552789cd939d599504d39732672dc84Christian Maederinstance Pretty ProcProfile where
9f93b2a8b552789cd939d599504d39732672dc84Christian Maeder pretty = printProcProfile
dd7da1b5fedc05b92ba023ebd803e6f4a662503bChristian MaederprintCommAlpha :: CommAlpha -> Doc
dd7da1b5fedc05b92ba023ebd803e6f4a662503bChristian MaederprintCommAlpha = printProcAlphabet . ProcAlphabet . Set.toList
9f93b2a8b552789cd939d599504d39732672dc84Christian MaederprintProcProfile :: ProcProfile -> Doc
9f93b2a8b552789cd939d599504d39732672dc84Christian MaederprintProcProfile (ProcProfile sorts commAlpha) =
dd7da1b5fedc05b92ba023ebd803e6f4a662503bChristian Maeder sep [printArgs sorts, printCommAlpha commAlpha]
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'ReillyprintProcessName :: FQ_PROCESS_NAME -> Doc
0b8146e4f675518993a34eb2255ad7ddd7bf82a4Christian MaederprintProcessName fqPn = case fqPn of
23a073e0a3433ca80a286d46202841b569ec36fdChristian Maeder PROCESS_NAME pn -> pretty pn
05cc55892e6c93bdd7b9c3f100ab1bb65fe6a21eLiam O'Reilly FQ_PROCESS_NAME pn profile -> parens $ sep
05cc55892e6c93bdd7b9c3f100ab1bb65fe6a21eLiam O'Reilly [ keyword processS <+> pretty pn <> printProcProfile profile]
53f89daf88665d3ea96d871110a5c0d9d8326bd2Andy Gimblettinstance Pretty CHANNEL_DECL where
1c7c4d95775a8ad5f7373e5cf0bad86f8301c56cAndy Gimblett pretty = printChanDecl
53f89daf88665d3ea96d871110a5c0d9d8326bd2Andy GimblettprintChanDecl :: CHANNEL_DECL -> Doc
53f89daf88665d3ea96d871110a5c0d9d8326bd2Andy GimblettprintChanDecl (ChannelDecl ns s) =
12b2ae689353ecbaad720a9af9f9be01c1a3fe2dChristian Maeder ppWithCommas ns <+> colon <+> pretty s
c052e3ee4a53ee3a2da829aa142fd596ef6c9e3dAndy Gimblettinstance Pretty PROC_ITEM where
c052e3ee4a53ee3a2da829aa142fd596ef6c9e3dAndy Gimblett pretty = printProcItem
b25c72845890740c2f8a21214752574990b943cfChristian MaederprintArgs :: Pretty a => [a] -> Doc
b25c72845890740c2f8a21214752574990b943cfChristian MaederprintArgs a = if null a then empty else parens $ ppWithCommas a
c052e3ee4a53ee3a2da829aa142fd596ef6c9e3dAndy GimblettprintProcItem :: PROC_ITEM -> Doc
a09bfcbcb0fba5663fca1968aa82daebf2e092c4Andy GimblettprintProcItem (Proc_Decl pn args alpha) =
a5f3a8cdc3ceb045c3c166ee840d3e59ec7efac6Christian Maeder sep [pretty pn <> printArgs args, printProcAlphabet alpha]
dfc58f5ec6492d1a9b9babd9cdcdbb15baa6e657Christian MaederprintProcItem (Proc_Defn pn args alpha p) =
a5f3a8cdc3ceb045c3c166ee840d3e59ec7efac6Christian Maeder sep [ pretty pn <> printOptArgDecls args
a5f3a8cdc3ceb045c3c166ee840d3e59ec7efac6Christian Maeder , printProcAlphabet alpha
dfc58f5ec6492d1a9b9babd9cdcdbb15baa6e657Christian Maeder , equals <+> pretty p]
b25c72845890740c2f8a21214752574990b943cfChristian MaederprintProcItem (Proc_Eq pn p) = sep [pretty pn, equals <+> pretty p]
61051521e4d82769a47f23aecb5fb477de47d534Andy Gimblettinstance Pretty PARM_PROCNAME where
61051521e4d82769a47f23aecb5fb477de47d534Andy Gimblett pretty = printParmProcname
61051521e4d82769a47f23aecb5fb477de47d534Andy GimblettprintParmProcname :: PARM_PROCNAME -> Doc
61051521e4d82769a47f23aecb5fb477de47d534Andy GimblettprintParmProcname (ParmProcname pn args) =
b25c72845890740c2f8a21214752574990b943cfChristian Maeder pretty pn <> printArgs args
b22c258cca179a5ffe777b64b32e10687c5f6b2cAndy GimblettprintProcAlphabet :: PROC_ALPHABET -> Doc
a5f3a8cdc3ceb045c3c166ee840d3e59ec7efac6Christian MaederprintProcAlphabet (ProcAlphabet commTypes) = colon <+> case commTypes of
23a073e0a3433ca80a286d46202841b569ec36fdChristian Maeder [CommTypeSort s] -> pretty s
23a073e0a3433ca80a286d46202841b569ec36fdChristian Maeder _ -> braces $ ppWithCommas commTypes
aa0d5f8be9950e788884f7431cf4cb7bee74788cAndy Gimblettinstance Pretty PROCESS where
aa0d5f8be9950e788884f7431cf4cb7bee74788cAndy Gimblett pretty = printProcess
aa0d5f8be9950e788884f7431cf4cb7bee74788cAndy GimblettprintProcess :: PROCESS -> Doc
afc52bfaabee38c4d55cee9f35b1a0028ba3854aAndy GimblettprintProcess pr = case pr of
afc52bfaabee38c4d55cee9f35b1a0028ba3854aAndy Gimblett -- precedence 0
197888c54795ec1e79e77289b7e20436a6db74c0Andy Gimblett Skip _ -> text skipS
197888c54795ec1e79e77289b7e20436a6db74c0Andy Gimblett Stop _ -> text stopS
197888c54795ec1e79e77289b7e20436a6db74c0Andy Gimblett Div _ -> text divS
b25c72845890740c2f8a21214752574990b943cfChristian Maeder Run es _ -> text runS <+> parens (pretty es)
b25c72845890740c2f8a21214752574990b943cfChristian Maeder Chaos es _ -> text chaosS <+> parens (pretty es)
a1f6118e7ce7f8892fc4299e316630ec74083f0aAndy Gimblett NamedProcess pn ts _ ->
b25c72845890740c2f8a21214752574990b943cfChristian Maeder pretty pn <+> printArgs ts
afc52bfaabee38c4d55cee9f35b1a0028ba3854aAndy Gimblett -- precedence 1
fcd11c35e645b0744a308f7961a519826bbaa2f5Christian Maeder ConditionalProcess f p q _ -> fsep
b25c72845890740c2f8a21214752574990b943cfChristian Maeder [ keyword ifS <+> pretty f
4f4e94264f48e255d4125f47649f585d9d062fabChristian Maeder , keyword thenS <+> pretty p
4f4e94264f48e255d4125f47649f585d9d062fabChristian Maeder , keyword elseS <+> pretty q ]
afc52bfaabee38c4d55cee9f35b1a0028ba3854aAndy Gimblett -- precedence 2
4f4e94264f48e255d4125f47649f585d9d062fabChristian Maeder Hiding p es _ -> sep
4f4e94264f48e255d4125f47649f585d9d062fabChristian Maeder [ lglue pr p, hiding_proc <+> pretty es ]
b25c72845890740c2f8a21214752574990b943cfChristian Maeder RenamingProcess p r _ -> sep
4f4e94264f48e255d4125f47649f585d9d062fabChristian Maeder [ lglue pr p, ren_proc_open <+> pretty r <+> ren_proc_close ]
afc52bfaabee38c4d55cee9f35b1a0028ba3854aAndy Gimblett -- precedence 3
fcd11c35e645b0744a308f7961a519826bbaa2f5Christian Maeder Sequential p q _ -> sep
4f4e94264f48e255d4125f47649f585d9d062fabChristian Maeder [ lglue pr p, sequential <+> glue pr q ]
4f4e94264f48e255d4125f47649f585d9d062fabChristian Maeder PrefixProcess event p _ -> sep
4f4e94264f48e255d4125f47649f585d9d062fabChristian Maeder [ pretty event <+> prefix_proc, glue pr p ]
afc52bfaabee38c4d55cee9f35b1a0028ba3854aAndy Gimblett -- precedence 4
b25c72845890740c2f8a21214752574990b943cfChristian Maeder InternalChoice p q _ -> sep
4f4e94264f48e255d4125f47649f585d9d062fabChristian Maeder [ lglue pr p, internal_choice <+> glue pr q ]
b25c72845890740c2f8a21214752574990b943cfChristian Maeder ExternalChoice p q _ -> sep
4f4e94264f48e255d4125f47649f585d9d062fabChristian Maeder [ lglue pr p, external_choice <+> glue pr q ]
afc52bfaabee38c4d55cee9f35b1a0028ba3854aAndy Gimblett -- precedence 5
b25c72845890740c2f8a21214752574990b943cfChristian Maeder Interleaving p q _ -> sep
4f4e94264f48e255d4125f47649f585d9d062fabChristian Maeder [ lglue pr p, interleave <+> glue pr q ]
b25c72845890740c2f8a21214752574990b943cfChristian Maeder SynchronousParallel p q _ -> sep
4f4e94264f48e255d4125f47649f585d9d062fabChristian Maeder [ lglue pr p, synchronous <+> glue pr q ]
b25c72845890740c2f8a21214752574990b943cfChristian Maeder GeneralisedParallel p es q _ -> fsep
b25c72845890740c2f8a21214752574990b943cfChristian Maeder , genpar_open <+> pretty es <+> genpar_close
b25c72845890740c2f8a21214752574990b943cfChristian Maeder , glue pr q ]
b25c72845890740c2f8a21214752574990b943cfChristian Maeder AlphabetisedParallel p les res q _ -> fsep
b25c72845890740c2f8a21214752574990b943cfChristian Maeder , alpar_open <+> pretty les
b25c72845890740c2f8a21214752574990b943cfChristian Maeder , alpar_sep <+> pretty res
b25c72845890740c2f8a21214752574990b943cfChristian Maeder , alpar_close <+> glue pr q ]
0a83f8dcd5598436966584b858313eb5efd95d5bLiam O'Reilly FQProcess p _ _ -> pretty p
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reillyinstance Pretty CommType where
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly pretty (CommTypeSort s) = pretty s
23a073e0a3433ca80a286d46202841b569ec36fdChristian Maeder pretty (CommTypeChan (TypedChanName c s)) =
23a073e0a3433ca80a286d46202841b569ec36fdChristian Maeder pretty c <+> colon <+> pretty s
50c62c8c45643f09bcb2f4a99b07bf1d072ecf40Christian Maederinstance Pretty Rename where
50c62c8c45643f09bcb2f4a99b07bf1d072ecf40Christian Maeder pretty (Rename i mk) = let n = pretty i in case mk of
50c62c8c45643f09bcb2f4a99b07bf1d072ecf40Christian Maeder Just (k, ms) -> case ms of
50c62c8c45643f09bcb2f4a99b07bf1d072ecf40Christian Maeder Nothing -> case k of
50c62c8c45643f09bcb2f4a99b07bf1d072ecf40Christian Maeder BinPred -> keyword predS <+> n
50c62c8c45643f09bcb2f4a99b07bf1d072ecf40Christian Maeder _ -> keyword opS <+> n
50c62c8c45643f09bcb2f4a99b07bf1d072ecf40Christian Maeder Just (s1, s2) -> n <+> colon <+> pretty s1 <+> case k of
50c62c8c45643f09bcb2f4a99b07bf1d072ecf40Christian Maeder BinPred -> cross
50c62c8c45643f09bcb2f4a99b07bf1d072ecf40Christian Maeder TotOp -> funArrow
50c62c8c45643f09bcb2f4a99b07bf1d072ecf40Christian Maeder PartOp -> pfun
50c62c8c45643f09bcb2f4a99b07bf1d072ecf40Christian Maeder <+> pretty s2
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reillyinstance Pretty RENAMING where
50c62c8c45643f09bcb2f4a99b07bf1d072ecf40Christian Maeder pretty (Renaming ids) = ppWithCommas ids
4f4e94264f48e255d4125f47649f585d9d062fabChristian Maeder{- glue and lglue decide whether the child in the parse tree needs
4f4e94264f48e255d4125f47649f585d9d062fabChristian Maederto be parenthesised or not. -}
4f4e94264f48e255d4125f47649f585d9d062fabChristian Maeder-- | the second argument is a right argument process of the first argument
4f4e94264f48e255d4125f47649f585d9d062fabChristian Maederglue :: PROCESS -> PROCESS -> Doc
310d12b88f902a597cdb08a1c7d11ae7130855eeChristian Maederglue x y = let
310d12b88f902a597cdb08a1c7d11ae7130855eeChristian Maeder p = procPrio y
310d12b88f902a597cdb08a1c7d11ae7130855eeChristian Maeder q = procPrio x in
310d12b88f902a597cdb08a1c7d11ae7130855eeChristian Maeder (if p < Cond && (p > q || p == q && p > Pre) then parens else id) $ pretty y
4f4e94264f48e255d4125f47649f585d9d062fabChristian Maeder-- | the second argument is a left argument process of the first argument
4f4e94264f48e255d4125f47649f585d9d062fabChristian Maederlglue :: PROCESS -> PROCESS -> Doc
9efe365d7ce90313e53ea5cfeca391d118fd8629Christian Maeder (if procPrio y > procPrio x || hasRightCond y then parens else id)
9efe365d7ce90313e53ea5cfeca391d118fd8629Christian MaederhasRightCond :: PROCESS -> Bool
9efe365d7ce90313e53ea5cfeca391d118fd8629Christian MaederhasRightCond x = case x of
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder ConditionalProcess {} -> True
9efe365d7ce90313e53ea5cfeca391d118fd8629Christian Maeder SynchronousParallel _ y _ -> hasRightCond y
9efe365d7ce90313e53ea5cfeca391d118fd8629Christian Maeder GeneralisedParallel _ _ y _ -> hasRightCond y
9efe365d7ce90313e53ea5cfeca391d118fd8629Christian Maeder AlphabetisedParallel _ _ _ y _ -> hasRightCond y
9efe365d7ce90313e53ea5cfeca391d118fd8629Christian Maeder Interleaving _ y _ -> hasRightCond y
9efe365d7ce90313e53ea5cfeca391d118fd8629Christian Maeder ExternalChoice _ y _ -> hasRightCond y
9efe365d7ce90313e53ea5cfeca391d118fd8629Christian Maeder InternalChoice _ y _ -> hasRightCond y
9efe365d7ce90313e53ea5cfeca391d118fd8629Christian Maeder Sequential _ y _ -> hasRightCond y
9efe365d7ce90313e53ea5cfeca391d118fd8629Christian Maeder PrefixProcess _ y _ -> hasRightCond y
4f4e94264f48e255d4125f47649f585d9d062fabChristian Maeder{- par binds weakest and is left associative. Then choice follows,
4f4e94264f48e255d4125f47649f585d9d062fabChristian Maederthen sequence, then prefix and finally renaming or hiding. -}
4f4e94264f48e255d4125f47649f585d9d062fabChristian Maederdata Prio = Prim | Post | Pre | Seq | Choice | Par | Cond deriving (Eq, Ord)
4f4e94264f48e255d4125f47649f585d9d062fabChristian MaederprocPrio :: PROCESS -> Prio
4f4e94264f48e255d4125f47649f585d9d062fabChristian MaederprocPrio x = case x of
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder ConditionalProcess {} -> Cond
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder SynchronousParallel {} -> Par
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder GeneralisedParallel {} -> Par
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder AlphabetisedParallel {} -> Par
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder Interleaving {} -> Par
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder ExternalChoice {} -> Choice
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder InternalChoice {} -> Choice
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder Sequential {} -> Seq
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder PrefixProcess {} -> Pre
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder Hiding {} -> Post
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder RenamingProcess {} -> Post
7371f8fe3a9a286a74ea30a3cd18e7740f67d537Andy Gimblettinstance Pretty EVENT where
7371f8fe3a9a286a74ea30a3cd18e7740f67d537Andy Gimblett pretty = printEvent
576a4ca6de740c90afd448607c2323477139de24Liam O'Reilly-- | print an event.
7371f8fe3a9a286a74ea30a3cd18e7740f67d537Andy GimblettprintEvent :: EVENT -> Doc
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'ReillyprintEvent ev =
7447e9fcbe38c1d04effa0df67f49240bd9963d6Liam O'Reilly let printRecord' = printRecord {
7447e9fcbe38c1d04effa0df67f49240bd9963d6Liam O'Reilly foldQual_var = \ _ v _ _ -> sidDoc v}
7447e9fcbe38c1d04effa0df67f49240bd9963d6Liam O'Reilly caslPrintTerm = foldTerm printRecord'
7447e9fcbe38c1d04effa0df67f49240bd9963d6Liam O'Reilly in case ev of
7447e9fcbe38c1d04effa0df67f49240bd9963d6Liam O'Reilly TermEvent t _ -> caslPrintTerm t
576a4ca6de740c90afd448607c2323477139de24Liam O'Reilly InternalPrefixChoice v s _ ->
b25c72845890740c2f8a21214752574990b943cfChristian Maeder internal_choice <+> pretty v <+> text svar_sortS <+> pretty s
576a4ca6de740c90afd448607c2323477139de24Liam O'Reilly ExternalPrefixChoice v s _ ->
b25c72845890740c2f8a21214752574990b943cfChristian Maeder external_choice <+> pretty v <+> text svar_sortS <+> pretty s
b25c72845890740c2f8a21214752574990b943cfChristian Maeder ChanSend cn t _ -> pretty cn <+> text chan_sendS <+> pretty t
576a4ca6de740c90afd448607c2323477139de24Liam O'Reilly ChanNonDetSend cn v s _ ->
b25c72845890740c2f8a21214752574990b943cfChristian Maeder pretty cn <+> text chan_sendS <+> pretty v
b25c72845890740c2f8a21214752574990b943cfChristian Maeder <+> text svar_sortS <+> pretty s
576a4ca6de740c90afd448607c2323477139de24Liam O'Reilly ChanRecv cn v s _ ->
b25c72845890740c2f8a21214752574990b943cfChristian Maeder pretty cn <+> text chan_receiveS <+> pretty v
b25c72845890740c2f8a21214752574990b943cfChristian Maeder <+> text svar_sortS <+> pretty s
7447e9fcbe38c1d04effa0df67f49240bd9963d6Liam O'Reilly FQTermEvent t _ -> caslPrintTerm t
9e5f4073e948104307d43c3962d624b8416f191fLiam O'Reilly FQExternalPrefixChoice t _ -> external_choice <+> pretty t
9e5f4073e948104307d43c3962d624b8416f191fLiam O'Reilly FQInternalPrefixChoice t _ -> internal_choice <+> pretty t
9e5f4073e948104307d43c3962d624b8416f191fLiam O'Reilly FQChanSend (cn, s) t _ -> pretty cn <> colon <> pretty s <+>
9e5f4073e948104307d43c3962d624b8416f191fLiam O'Reilly text chan_sendS <+> pretty t
9e5f4073e948104307d43c3962d624b8416f191fLiam O'Reilly FQChanNonDetSend (cn, s) v _ -> pretty cn <> colon <> pretty s <+>
9e5f4073e948104307d43c3962d624b8416f191fLiam O'Reilly text chan_sendS <+> pretty v
9e5f4073e948104307d43c3962d624b8416f191fLiam O'Reilly FQChanRecv (cn, s) v _ -> pretty cn <> colon <> pretty s <+>
9e5f4073e948104307d43c3962d624b8416f191fLiam O'Reilly text chan_receiveS <+> pretty v
7371f8fe3a9a286a74ea30a3cd18e7740f67d537Andy Gimblettinstance Pretty EVENT_SET where
7371f8fe3a9a286a74ea30a3cd18e7740f67d537Andy Gimblett pretty = printEventSet
7371f8fe3a9a286a74ea30a3cd18e7740f67d537Andy GimblettprintEventSet :: EVENT_SET -> Doc
dd7da1b5fedc05b92ba023ebd803e6f4a662503bChristian MaederprintEventSet (EventSet es _) = ppWithCommas es