Print_CspCASL.hs revision 876bd2c70a93981cc80f8376284616bce4a0fefc
e9458b1a7a19a63aa4c179f9ab20f4d50681c168Jens ElknerModule : $Id$
81d182b21020b815887e9057959228546cf61b6bChristian MaederDescription : Pretty printing for CspCASL
35597678f1c9da703de8d0b6b66ea63247ebe884Christian MaederCopyright : (c) Andy Gimblett and Uni Bremen 2006
98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
3f69b6948966979163bdfe8331c38833d5d90ecdChristian MaederMaintainer : a.m.gimblett@swansea.ac.uk
ce2eda9624349a4c191dca61cb478b039ab00998Christian MaederStability : provisional
410ff490af511ffa09b52e4de631d36a154b9730Christian MaederPortability : portable
ad97909f160c13effd3bc73155aaa2c29902a5a1Christian MaederPrinting abstract syntax of CSP-CASL
b1719ef0353b9eb5a00dec8e5119a99eaad718e0Christian Maederimport Common.Keywords (elseS, ifS, thenS)
ce2eda9624349a4c191dca61cb478b039ab00998Christian Maederinstance Pretty CspBasicSpec where
410ff490af511ffa09b52e4de631d36a154b9730Christian Maeder pretty = printCspBasicSpec
950e053ba55ac9c7d9c26a1ab48bd00202b29511Christian MaederprintCspBasicSpec :: CspBasicSpec -> Doc
ad97909f160c13effd3bc73155aaa2c29902a5a1Christian MaederprintCspBasicSpec ccs =
ad97909f160c13effd3bc73155aaa2c29902a5a1Christian Maeder chan_part $+$ proc_part
950e053ba55ac9c7d9c26a1ab48bd00202b29511Christian Maeder where chan_part = case (length chans) of
15c12a3ac049a4528da05b1017b78145f308aeb0Christian Maeder 1 -> (keyword channelS) <+> printChanDecs chans
51754d57079619ec1acfc7962d16478b787d3264Christian Maeder _ -> (keyword channelsS) <+> printChanDecs chans
15c12a3ac049a4528da05b1017b78145f308aeb0Christian Maeder proc_part = (keyword processS) <+>
ad270004874ce1d0697fb30d7309f180553bb315Christian Maeder (printProcItems (proc_items ccs))
ad270004874ce1d0697fb30d7309f180553bb315Christian Maeder chans = channels ccs
23a00c966f2aa8da525d7a7c51933c99964426c0Christian MaederprintChanDecs :: [CHANNEL_DECL] -> Doc
c200224a127278d54634ca4a5079591cb989aaf3Christian MaederprintChanDecs cds = (vcat . punctuate semi . map pretty) cds
c200224a127278d54634ca4a5079591cb989aaf3Christian Maederinstance Pretty CHANNEL_DECL where
ad97909f160c13effd3bc73155aaa2c29902a5a1Christian Maeder pretty = printChanDecl
72b9099aeec0762bae4546db3bc4b48721027bf4Christian MaederprintChanDecl :: CHANNEL_DECL -> Doc
abae801b829b32e32fff31d106245cf3b8c0a21fChristian MaederprintChanDecl (ChannelDecl ns s) =
ad97909f160c13effd3bc73155aaa2c29902a5a1Christian Maeder (ppWithCommas ns) <+> colon <+> (pretty s)
410ff490af511ffa09b52e4de631d36a154b9730Christian MaederprintProcItems :: [PROC_ITEM] -> Doc
72909c6c1cfe9702f5910d0a135c8b55729c7917Christian MaederprintProcItems ps = foldl ($+$) empty (map pretty ps)
ad97909f160c13effd3bc73155aaa2c29902a5a1Christian Maederinstance Pretty PROC_ITEM where
90c174bac60a72ffd81bc3bf5ae2dd9a61943b8bChristian Maeder pretty = printProcItem
42c01284bba8d7c8d995c8dfb96ace57d28ed1bcTill MossakowskiprintProcItem :: PROC_ITEM -> Doc
42c01284bba8d7c8d995c8dfb96ace57d28ed1bcTill MossakowskiprintProcItem (Proc_Decl pn args alpha) =
ad97909f160c13effd3bc73155aaa2c29902a5a1Christian Maeder (pretty pn) <> (printArgs args) <+> colon <+> (pretty alpha)
ce2eda9624349a4c191dca61cb478b039ab00998Christian Maeder where printArgs [] = empty
ce2eda9624349a4c191dca61cb478b039ab00998Christian Maeder printArgs a = parens $ ppWithCommas a
ce2eda9624349a4c191dca61cb478b039ab00998Christian MaederprintProcItem (Proc_Eq pn p) =
ce2eda9624349a4c191dca61cb478b039ab00998Christian Maeder (pretty pn) <+> equals <+> (pretty p)
ce2eda9624349a4c191dca61cb478b039ab00998Christian Maederinstance Pretty PARM_PROCNAME where
3bffe0f10ad93403e36288a1a4a92d50356956b5Christian Maeder pretty = printParmProcname
3bffe0f10ad93403e36288a1a4a92d50356956b5Christian MaederprintParmProcname :: PARM_PROCNAME -> Doc
52c28508167eb774d9b7286d585c250078d65818Christian MaederprintParmProcname (ParmProcname pn args) =
3bffe0f10ad93403e36288a1a4a92d50356956b5Christian Maeder pretty pn <> (printArgs args)
3bffe0f10ad93403e36288a1a4a92d50356956b5Christian Maeder where printArgs [] = empty
3bffe0f10ad93403e36288a1a4a92d50356956b5Christian Maeder printArgs a = parens $ ppWithCommas a
96edb3a8e970c02cc10a75d70b96a9165a4e1b91Christian Maederinstance Pretty PROC_ALPHABET where
410ff490af511ffa09b52e4de631d36a154b9730Christian Maeder pretty = printProcAlphabet
81946e2b3f6dde6167f48769bd02c7a634736856Christian MaederprintProcAlphabet :: PROC_ALPHABET -> Doc
96edb3a8e970c02cc10a75d70b96a9165a4e1b91Christian MaederprintProcAlphabet (ProcAlphabet commTypes _) = ppWithCommas commTypes
31400d19240b9a9ce78e7f8a495f8d4951a21e30Christian Maederinstance Pretty PROCESS where
ad97909f160c13effd3bc73155aaa2c29902a5a1Christian Maeder pretty = printProcess
410ff490af511ffa09b52e4de631d36a154b9730Christian MaederprintProcess :: PROCESS -> Doc
88ece6e49930670e8fd3ee79c89a2e918d2fbd0cChristian MaederprintProcess pr = case pr of
410ff490af511ffa09b52e4de631d36a154b9730Christian Maeder -- precedence 0
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder Skip _ -> text skipS
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder Stop _ -> text stopS
dc4bfcb8a5092af158e8a5691c8de8d6bc8b8724Christian Maeder Div _ -> text divS
dc4bfcb8a5092af158e8a5691c8de8d6bc8b8724Christian Maeder Run es _ -> (text runS) <+> lparen <+> (pretty es) <+> rparen
e0dba81bd8957764e49d5f15b5e0ab1f9411aadfChristian Maeder Chaos es _ -> (text chaosS) <+> lparen <+> (pretty es) <+> rparen
8338fbf3cfb9cf981261d893286f070bd9fa17efChristian Maeder NamedProcess pn ts _ ->
89dc77946055c0e4cb4671c4a74c3dcd55ed41a1Christian Maeder (pretty pn) <+>
410ff490af511ffa09b52e4de631d36a154b9730Christian Maeder then ppWithCommas ts
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder else lparen <+> (ppWithCommas ts) <+> rparen
9d515512054aaaf9c8785360391ab73091ad962dChristian Maeder -- precedence 1
0a070d04a5d89ffc97147ab6f5fbbb6994afc1ccChristian Maeder ConditionalProcess f p q _ ->
410ff490af511ffa09b52e4de631d36a154b9730Christian Maeder ((keyword ifS) <+> (pretty f) <+>
410ff490af511ffa09b52e4de631d36a154b9730Christian Maeder (keyword thenS) <+> (glue pr p) <+>
4ef2a978e66e2246ff0b7f00c77deb7aabb28b8eChristian Maeder (keyword elseS) <+> (glue pr q)
72b9099aeec0762bae4546db3bc4b48721027bf4Christian Maeder -- precedence 2
f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian Maeder Hiding p es _ ->
f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian Maeder (pretty p) <+> hiding_proc <+> (pretty es)
f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian Maeder RelationalRenaming p r _ ->
72b9099aeec0762bae4546db3bc4b48721027bf4Christian Maeder ((pretty p) <+>
72b9099aeec0762bae4546db3bc4b48721027bf4Christian Maeder ren_proc_open <+> (ppWithCommas r) <+> ren_proc_close)
4ef2a978e66e2246ff0b7f00c77deb7aabb28b8eChristian Maeder -- precedence 3
ad97909f160c13effd3bc73155aaa2c29902a5a1Christian Maeder Sequential p q _ ->
a18e8529c133e17b95180bdd2bc2abbea232f698Christian Maeder (pretty p) <+> sequential <+> (glue pr q)
a18e8529c133e17b95180bdd2bc2abbea232f698Christian Maeder PrefixProcess ev p _ ->
a18e8529c133e17b95180bdd2bc2abbea232f698Christian Maeder (pretty ev) <+> prefix_proc <+> (glue pr p)
a18e8529c133e17b95180bdd2bc2abbea232f698Christian Maeder InternalPrefixProcess v s p _ ->
a18e8529c133e17b95180bdd2bc2abbea232f698Christian Maeder (internal_choice <+> (pretty v) <+>
227dec9850d66655627ce8b7d443898896597aa9Christian Maeder (text svar_sortS) <+> (pretty s) <+>
227dec9850d66655627ce8b7d443898896597aa9Christian Maeder prefix_proc <+> (glue pr p)
a18e8529c133e17b95180bdd2bc2abbea232f698Christian Maeder ExternalPrefixProcess v s p _ ->
a18e8529c133e17b95180bdd2bc2abbea232f698Christian Maeder (external_choice <+> (pretty v) <+>
a18e8529c133e17b95180bdd2bc2abbea232f698Christian Maeder (text svar_sortS) <+> (pretty s) <+>
a18e8529c133e17b95180bdd2bc2abbea232f698Christian Maeder prefix_proc <+> (glue pr p)
a18e8529c133e17b95180bdd2bc2abbea232f698Christian Maeder -- precedence 4
a18e8529c133e17b95180bdd2bc2abbea232f698Christian Maeder InternalChoice p q _ ->
a18e8529c133e17b95180bdd2bc2abbea232f698Christian Maeder (pretty p) <+> internal_choice <+> (glue pr q)
a18e8529c133e17b95180bdd2bc2abbea232f698Christian Maeder ExternalChoice p q _ ->
a18e8529c133e17b95180bdd2bc2abbea232f698Christian Maeder (pretty p) <+> external_choice <+> (glue pr q)
a18e8529c133e17b95180bdd2bc2abbea232f698Christian Maeder -- precedence 5
a18e8529c133e17b95180bdd2bc2abbea232f698Christian Maeder Interleaving p q _ ->
a18e8529c133e17b95180bdd2bc2abbea232f698Christian Maeder (pretty p) <+> interleave <+> (glue pr q)
a18e8529c133e17b95180bdd2bc2abbea232f698Christian Maeder SynchronousParallel p q _ ->
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder (pretty p) <+> synchronous <+> (glue pr q)
a18e8529c133e17b95180bdd2bc2abbea232f698Christian Maeder GeneralisedParallel p es q _ ->
15c12a3ac049a4528da05b1017b78145f308aeb0Christian Maeder ((pretty p) <+> genpar_open <+> (pretty es) <+>
c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian Maeder genpar_close <+> (glue pr q))
c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian Maeder AlphabetisedParallel p les res q _ ->
c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian Maeder ((pretty p) <+> alpar_open <+>
0dddb504c4375042bc256a7a9b4bd803d1dc18adChristian Maeder (pretty les) <+> alpar_sep <+> (pretty res) <+>
0dddb504c4375042bc256a7a9b4bd803d1dc18adChristian Maeder alpar_close <+> (glue pr q)
36cd83d825e16386e8bedf45be3b0670c9322594Christian Maeder-- glue and prec_comp decide whether the child in the parse tree needs
36cd83d825e16386e8bedf45be3b0670c9322594Christian Maeder-- to be parenthesised or not. Parentheses are necessary if the
36cd83d825e16386e8bedf45be3b0670c9322594Christian Maeder-- right-child is at the same level of precedence as the parent but is
36cd83d825e16386e8bedf45be3b0670c9322594Christian Maeder-- a different operator; otherwise, they're not.
36cd83d825e16386e8bedf45be3b0670c9322594Christian Maederglue :: PROCESS -> PROCESS -> Doc
36cd83d825e16386e8bedf45be3b0670c9322594Christian Maederglue x y = if (prec_comp x y)
03a4f2609d91287af8de36c1b06842b40638b1dfChristian Maeder then lparen <+> pretty y <+> rparen
414eef40244ffc227c16c59a1904e48611617103Christian Maeder else pretty y
03a4f2609d91287af8de36c1b06842b40638b1dfChristian Maeder-- This is really nasty, but sledgehammer effective and allows fine
36cd83d825e16386e8bedf45be3b0670c9322594Christian Maeder-- control. Unmaintainable, however. :-( I imagine there's a way to
36cd83d825e16386e8bedf45be3b0670c9322594Christian Maeder-- compare the types in a less boilerplate manner, but OTOH there are
36cd83d825e16386e8bedf45be3b0670c9322594Christian Maeder-- some special cases where it's nice to be explicit. Also, hiding
36cd83d825e16386e8bedf45be3b0670c9322594Christian Maeder-- and renaming are distinctly non-standard. *shrug*
414eef40244ffc227c16c59a1904e48611617103Christian Maederprec_comp :: PROCESS -> PROCESS -> Bool
414eef40244ffc227c16c59a1904e48611617103Christian Maederprec_comp x y =
f85f722d95f8a5f928aa34b38894e9a4f60dfe84Christian Maeder Hiding _ _ _ ->
f85f722d95f8a5f928aa34b38894e9a4f60dfe84Christian Maeder case y of RelationalRenaming _ _ _ -> True
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder RelationalRenaming _ _ _ ->
a681f9b62698853816145d9f8cfef33f3aea1550Christian Maeder case y of Hiding _ _ _ -> True
f85f722d95f8a5f928aa34b38894e9a4f60dfe84Christian Maeder Sequential _ _ _ ->
03a4f2609d91287af8de36c1b06842b40638b1dfChristian Maeder case y of InternalPrefixProcess _ _ _ _ -> True
a18e8529c133e17b95180bdd2bc2abbea232f698Christian Maeder ExternalPrefixProcess _ _ _ _ -> True
03a4f2609d91287af8de36c1b06842b40638b1dfChristian Maeder PrefixProcess _ _ _ ->
03a4f2609d91287af8de36c1b06842b40638b1dfChristian Maeder case y of Sequential _ _ _ -> True
03a4f2609d91287af8de36c1b06842b40638b1dfChristian Maeder InternalPrefixProcess _ _ _ _ ->
03a4f2609d91287af8de36c1b06842b40638b1dfChristian Maeder case y of Sequential _ _ _ -> True
03a4f2609d91287af8de36c1b06842b40638b1dfChristian Maeder ExternalPrefixProcess _ _ _ _ ->
03a4f2609d91287af8de36c1b06842b40638b1dfChristian Maeder case y of Sequential _ _ _ -> True
03a4f2609d91287af8de36c1b06842b40638b1dfChristian Maeder ExternalChoice _ _ _ ->
03a4f2609d91287af8de36c1b06842b40638b1dfChristian Maeder case y of InternalChoice _ _ _ -> True
03a4f2609d91287af8de36c1b06842b40638b1dfChristian Maeder InternalChoice _ _ _ ->
03a4f2609d91287af8de36c1b06842b40638b1dfChristian Maeder case y of ExternalChoice _ _ _ -> True
03a4f2609d91287af8de36c1b06842b40638b1dfChristian Maeder Interleaving _ _ _ ->
03a4f2609d91287af8de36c1b06842b40638b1dfChristian Maeder case y of SynchronousParallel _ _ _ -> True
03a4f2609d91287af8de36c1b06842b40638b1dfChristian Maeder GeneralisedParallel _ _ _ _ -> True
03a4f2609d91287af8de36c1b06842b40638b1dfChristian Maeder AlphabetisedParallel _ _ _ _ _ -> True
03a4f2609d91287af8de36c1b06842b40638b1dfChristian Maeder SynchronousParallel _ _ _ ->
03a4f2609d91287af8de36c1b06842b40638b1dfChristian Maeder case y of Interleaving _ _ _ -> True
03a4f2609d91287af8de36c1b06842b40638b1dfChristian Maeder GeneralisedParallel _ _ _ _ -> True
03a4f2609d91287af8de36c1b06842b40638b1dfChristian Maeder AlphabetisedParallel _ _ _ _ _ -> True
03a4f2609d91287af8de36c1b06842b40638b1dfChristian Maeder GeneralisedParallel _ _ _ _ ->
03a4f2609d91287af8de36c1b06842b40638b1dfChristian Maeder case y of Interleaving _ _ _ -> True
03a4f2609d91287af8de36c1b06842b40638b1dfChristian Maeder SynchronousParallel _ _ _ -> True
5124a921afd8ade94cfc339a34026cc2d339287eChristian Maeder AlphabetisedParallel _ _ _ _ _ -> True
0dddb504c4375042bc256a7a9b4bd803d1dc18adChristian Maeder AlphabetisedParallel _ _ _ _ _ ->
36cd83d825e16386e8bedf45be3b0670c9322594Christian Maeder case y of Interleaving _ _ _ -> True
36cd83d825e16386e8bedf45be3b0670c9322594Christian Maeder SynchronousParallel _ _ _ -> True
36cd83d825e16386e8bedf45be3b0670c9322594Christian Maeder GeneralisedParallel _ _ _ _ -> True
f85f722d95f8a5f928aa34b38894e9a4f60dfe84Christian Maederinstance Pretty EVENT where
f85f722d95f8a5f928aa34b38894e9a4f60dfe84Christian Maeder pretty = printEvent
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederprintEvent :: EVENT -> Doc
03a4f2609d91287af8de36c1b06842b40638b1dfChristian MaederprintEvent (Event t _) = pretty t
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederprintEvent (Send cn t _) = (pretty cn) <+>
a681f9b62698853816145d9f8cfef33f3aea1550Christian Maeder (text chan_sendS) <+>
36cd83d825e16386e8bedf45be3b0670c9322594Christian MaederprintEvent (NonDetSend cn v s _) =
7703df65ea5ba02e596d409de284a64739ffd317Christian Maeder (pretty cn) <+> (text chan_sendS) <+>
03a4f2609d91287af8de36c1b06842b40638b1dfChristian Maeder (pretty v) <+> (text svar_sortS) <+> (pretty s)
03a4f2609d91287af8de36c1b06842b40638b1dfChristian MaederprintEvent (Receive cn v s _) =
03a4f2609d91287af8de36c1b06842b40638b1dfChristian Maeder (pretty cn) <+> (text chan_receiveS) <+>
03a4f2609d91287af8de36c1b06842b40638b1dfChristian Maeder (pretty v) <+> (text svar_sortS) <+> (pretty s)
03a4f2609d91287af8de36c1b06842b40638b1dfChristian Maederinstance Pretty EVENT_SET where
03a4f2609d91287af8de36c1b06842b40638b1dfChristian Maeder pretty = printEventSet
03a4f2609d91287af8de36c1b06842b40638b1dfChristian MaederprintEventSet :: EVENT_SET -> Doc
7703df65ea5ba02e596d409de284a64739ffd317Christian MaederprintEventSet (EventSet es _) = ppWithCommas es
7703df65ea5ba02e596d409de284a64739ffd317Christian Maederinstance Pretty CSP_FORMULA where
7703df65ea5ba02e596d409de284a64739ffd317Christian Maeder pretty = printCspFormula
03a4f2609d91287af8de36c1b06842b40638b1dfChristian MaederprintCspFormula :: CSP_FORMULA -> Doc
36cd83d825e16386e8bedf45be3b0670c9322594Christian MaederprintCspFormula (Formula f _) = pretty f