b332ea78705d9ed8708bb30eb914c0eb9a8e6361Till Mossakowski{- |

e9458b1a7a19a63aa4c179f9ab20f4d50681c168Jens ElknerModule : $Id$

876bd2c70a93981cc80f8376284616bce4a0fefcChristian MaederDescription : Pretty printing for CspCASL

b332ea78705d9ed8708bb30eb914c0eb9a8e6361Till MossakowskiCopyright : (c) Andy Gimblett and Uni Bremen 2006

98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt

b332ea78705d9ed8708bb30eb914c0eb9a8e6361Till Mossakowski

2eeec5240b424984e3ee26296da1eeab6c6d739eChristian MaederMaintainer : a.m.gimblett@swansea.ac.uk

b332ea78705d9ed8708bb30eb914c0eb9a8e6361Till MossakowskiStability : provisional

b332ea78705d9ed8708bb30eb914c0eb9a8e6361Till MossakowskiPortability : portable

b332ea78705d9ed8708bb30eb914c0eb9a8e6361Till Mossakowski

876bd2c70a93981cc80f8376284616bce4a0fefcChristian MaederPrinting abstract syntax of CSP-CASL

0095c7efbddd0ffeed6aaf8ec015346be161d819Till Mossakowski

b332ea78705d9ed8708bb30eb914c0eb9a8e6361Till Mossakowski-}

b332ea78705d9ed8708bb30eb914c0eb9a8e6361Till Mossakowskimodule CspCASL.Print_CspCASL where

b332ea78705d9ed8708bb30eb914c0eb9a8e6361Till Mossakowski

b332ea78705d9ed8708bb30eb914c0eb9a8e6361Till Mossakowskiimport CASL.AS_Basic_CASL (SORT, TERM)

b332ea78705d9ed8708bb30eb914c0eb9a8e6361Till Mossakowskiimport CASL.ToDoc ()

b332ea78705d9ed8708bb30eb914c0eb9a8e6361Till Mossakowski

0ea724a1bbc3c692c3cc4cc572975e51e45f137eTill Mossakowskiimport Common.Doc

2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maederimport Common.DocUtils

0ea724a1bbc3c692c3cc4cc572975e51e45f137eTill Mossakowskiimport Common.Keywords (elseS, ifS, thenS)

0ea724a1bbc3c692c3cc4cc572975e51e45f137eTill Mossakowski

ea8e98e298f33f9362293f392c8fb192722b8904Eugen Kuksaimport CspCASL.AS_CspCASL

47d6bc7bc9a708427f96be8d805f712697ad3d9eChristian Maederimport CspCASL.AS_CspCASL_Process

f5c16d70215311c0392b5723f427f714e34ba6b9Till Mossakowskiimport CspCASL.CspCASL_Keywords

f5c16d70215311c0392b5723f427f714e34ba6b9Till Mossakowski

b332ea78705d9ed8708bb30eb914c0eb9a8e6361Till Mossakowskiinstance Pretty CspBasicSpec where

2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder pretty = printCspBasicSpec

2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder

2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian MaederprintCspBasicSpec :: CspBasicSpec -> Doc

e1ca87d857ab0461cbcd260484ba0498ec10e1a4Till MossakowskiprintCspBasicSpec ccs =

ea8e98e298f33f9362293f392c8fb192722b8904Eugen Kuksa chan_part $+$ proc_part

f5c16d70215311c0392b5723f427f714e34ba6b9Till Mossakowski where chan_part = case (length chans) of

94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder 0 -> empty

f5c16d70215311c0392b5723f427f714e34ba6b9Till Mossakowski 1 -> (keyword channelS) <+> printChanDecs chans

f5c16d70215311c0392b5723f427f714e34ba6b9Till Mossakowski _ -> (keyword channelsS) <+> printChanDecs chans

47d6bc7bc9a708427f96be8d805f712697ad3d9eChristian Maeder proc_part = (keyword processS) <+>

e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian Maeder (printProcItems (proc_items ccs))

47d6bc7bc9a708427f96be8d805f712697ad3d9eChristian Maeder chans = channels ccs

e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian Maeder

f5c16d70215311c0392b5723f427f714e34ba6b9Till Mossakowski

47d6bc7bc9a708427f96be8d805f712697ad3d9eChristian MaederprintChanDecs :: [CHANNEL_DECL] -> Doc

f5c16d70215311c0392b5723f427f714e34ba6b9Till MossakowskiprintChanDecs cds = (vcat . punctuate semi . map pretty) cds

049d1590fff7cde05c68d63547aa7660c2034a0cTill Mossakowski

049d1590fff7cde05c68d63547aa7660c2034a0cTill Mossakowskiinstance Pretty CHANNEL_DECL where

049d1590fff7cde05c68d63547aa7660c2034a0cTill Mossakowski pretty = printChanDecl

049d1590fff7cde05c68d63547aa7660c2034a0cTill Mossakowski

47d6bc7bc9a708427f96be8d805f712697ad3d9eChristian MaederprintChanDecl :: CHANNEL_DECL -> Doc

47d6bc7bc9a708427f96be8d805f712697ad3d9eChristian MaederprintChanDecl (ChannelDecl ns s) =

94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder (ppWithCommas ns) <+> colon <+> (pretty s)

47d6bc7bc9a708427f96be8d805f712697ad3d9eChristian Maeder

e1ca87d857ab0461cbcd260484ba0498ec10e1a4Till Mossakowski

94e112d16f89130a688db8b03ad3224903f5e97eChristian MaederprintProcItems :: [PROC_ITEM] -> Doc

dece9056c18ada64bcc8f2fba285270374139ee8Christian MaederprintProcItems ps = foldl ($+$) empty (map pretty ps)

47d6bc7bc9a708427f96be8d805f712697ad3d9eChristian Maeder

94e112d16f89130a688db8b03ad3224903f5e97eChristian Maederinstance Pretty PROC_ITEM where

47d6bc7bc9a708427f96be8d805f712697ad3d9eChristian Maeder pretty = printProcItem

f5c16d70215311c0392b5723f427f714e34ba6b9Till Mossakowski

94e112d16f89130a688db8b03ad3224903f5e97eChristian MaederprintProcItem :: PROC_ITEM -> Doc

f5c16d70215311c0392b5723f427f714e34ba6b9Till MossakowskiprintProcItem (Proc_Decl pn args alpha) =

94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder (pretty pn) <> (printArgs args) <+> colon <+> (pretty alpha) <+> semi

f5c16d70215311c0392b5723f427f714e34ba6b9Till Mossakowski where printArgs [] = empty

f5c16d70215311c0392b5723f427f714e34ba6b9Till Mossakowski printArgs a = parens $ ppWithCommas a

2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian MaederprintProcItem (Proc_Eq pn p) =

94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder (pretty pn) <+> equals <+> (pretty p)

94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder

e7ddd5495421698701a2bbc57a5b3390a11d12caChristian Maeder

94e112d16f89130a688db8b03ad3224903f5e97eChristian Maederinstance Pretty PARM_PROCNAME where

f5c16d70215311c0392b5723f427f714e34ba6b9Till Mossakowski pretty = printParmProcname

2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder

47d6bc7bc9a708427f96be8d805f712697ad3d9eChristian MaederprintParmProcname :: PARM_PROCNAME -> Doc

933997b6313fc8fd4711dbc9e01dff7c68f58cd7Till MossakowskiprintParmProcname (ParmProcname pn args) =

933997b6313fc8fd4711dbc9e01dff7c68f58cd7Till Mossakowski pretty pn <> (printArgs args)

933997b6313fc8fd4711dbc9e01dff7c68f58cd7Till Mossakowski where printArgs [] = empty

933997b6313fc8fd4711dbc9e01dff7c68f58cd7Till Mossakowski printArgs a = parens $ ppWithCommas a

47d6bc7bc9a708427f96be8d805f712697ad3d9eChristian Maeder

933997b6313fc8fd4711dbc9e01dff7c68f58cd7Till Mossakowskiinstance Pretty PROC_ALPHABET where

933997b6313fc8fd4711dbc9e01dff7c68f58cd7Till Mossakowski pretty = printProcAlphabet

47d6bc7bc9a708427f96be8d805f712697ad3d9eChristian Maeder

049d1590fff7cde05c68d63547aa7660c2034a0cTill MossakowskiprintProcAlphabet :: PROC_ALPHABET -> Doc

049d1590fff7cde05c68d63547aa7660c2034a0cTill MossakowskiprintProcAlphabet (ProcAlphabet commTypes _) = ppWithCommas commTypes

049d1590fff7cde05c68d63547aa7660c2034a0cTill Mossakowski

94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder

94e112d16f89130a688db8b03ad3224903f5e97eChristian Maederinstance Pretty PROCESS where

94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder pretty = printProcess

94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder

933997b6313fc8fd4711dbc9e01dff7c68f58cd7Till MossakowskiprintProcess :: PROCESS -> Doc

933997b6313fc8fd4711dbc9e01dff7c68f58cd7Till MossakowskiprintProcess pr = case pr of

94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder -- precedence 0

933997b6313fc8fd4711dbc9e01dff7c68f58cd7Till Mossakowski Skip _ -> text skipS

47d6bc7bc9a708427f96be8d805f712697ad3d9eChristian Maeder Stop _ -> text stopS

94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder Div _ -> text divS

94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder Run es _ -> (text runS) <+> lparen <+> (pretty es) <+> rparen

47d6bc7bc9a708427f96be8d805f712697ad3d9eChristian Maeder Chaos es _ -> (text chaosS) <+> lparen <+> (pretty es) <+> rparen

94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder NamedProcess pn ts _ ->

94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder (pretty pn) <+>

adaf5a640e615848c19de372218377a418f954ceFlorian Mossakowski if (null ts)

94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder then ppWithCommas ts

94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder else lparen <+> (ppWithCommas ts) <+> rparen

933997b6313fc8fd4711dbc9e01dff7c68f58cd7Till Mossakowski -- precedence 1

933997b6313fc8fd4711dbc9e01dff7c68f58cd7Till Mossakowski ConditionalProcess f p q _ ->

e57c178845d66be315d6947103db4a14c72a21a9Till Mossakowski ((keyword ifS) <+> (pretty f) <+>

94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder (keyword thenS) <+> (glue pr p) <+>

47d6bc7bc9a708427f96be8d805f712697ad3d9eChristian Maeder (keyword elseS) <+> (glue pr q)

94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder )

94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder -- precedence 2

47d6bc7bc9a708427f96be8d805f712697ad3d9eChristian Maeder Hiding p es _ ->

94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder (pretty p) <+> hiding_proc <+> (pretty es)

adaf5a640e615848c19de372218377a418f954ceFlorian Mossakowski RenamingProcess p r _ ->

773a3d8e40d41417d7c7c92c65c9ff1e49f66ce2Christian Maeder ((pretty p) <+>

e57c178845d66be315d6947103db4a14c72a21a9Till Mossakowski ren_proc_open <+> (pretty r) <+> ren_proc_close)

e57c178845d66be315d6947103db4a14c72a21a9Till Mossakowski -- precedence 3

a3f427df6da9439423c5925c4957ae4124ed908cChristian Maeder Sequential p q _ ->

a3f427df6da9439423c5925c4957ae4124ed908cChristian Maeder (pretty p) <+> sequential <+> (glue pr q)

e32a0dc687d36d32f8135d8b7d88e916164ddb5fFlorian Mossakowski PrefixProcess event p _ ->

a3f427df6da9439423c5925c4957ae4124ed908cChristian Maeder (pretty event) <+> prefix_proc $+$ (glue pr p)

a3f427df6da9439423c5925c4957ae4124ed908cChristian Maeder -- precedence 4

47d6bc7bc9a708427f96be8d805f712697ad3d9eChristian Maeder InternalChoice p q _ ->

47d6bc7bc9a708427f96be8d805f712697ad3d9eChristian Maeder (pretty p) <+> internal_choice <+> (glue pr q)

f5c16d70215311c0392b5723f427f714e34ba6b9Till Mossakowski ExternalChoice p q _ ->

e32a0dc687d36d32f8135d8b7d88e916164ddb5fFlorian Mossakowski (pretty p) <+> external_choice <+> (glue pr q)

933997b6313fc8fd4711dbc9e01dff7c68f58cd7Till Mossakowski -- precedence 5

933997b6313fc8fd4711dbc9e01dff7c68f58cd7Till Mossakowski Interleaving p q _ ->

933997b6313fc8fd4711dbc9e01dff7c68f58cd7Till Mossakowski (pretty p) <+> interleave <+> (glue pr q)

933997b6313fc8fd4711dbc9e01dff7c68f58cd7Till Mossakowski SynchronousParallel p q _ ->

933997b6313fc8fd4711dbc9e01dff7c68f58cd7Till Mossakowski (pretty p) <+> synchronous <+> (glue pr q)

933997b6313fc8fd4711dbc9e01dff7c68f58cd7Till Mossakowski GeneralisedParallel p es q _ ->

94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder ((pretty p) <+> genpar_open <+> (pretty es) <+>

94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder genpar_close <+> (glue pr q))

933997b6313fc8fd4711dbc9e01dff7c68f58cd7Till Mossakowski AlphabetisedParallel p les res q _ ->

933997b6313fc8fd4711dbc9e01dff7c68f58cd7Till Mossakowski ((pretty p) <+> alpar_open <+>

933997b6313fc8fd4711dbc9e01dff7c68f58cd7Till Mossakowski (pretty les) <+> alpar_sep <+> (pretty res) <+>

47d6bc7bc9a708427f96be8d805f712697ad3d9eChristian Maeder alpar_close <+> (glue pr q)

47d6bc7bc9a708427f96be8d805f712697ad3d9eChristian Maeder )

FQProcess p _ _ -> pretty p

-- Alternative pretty printer for FQProcess - Used for debugging

-- FQProcess p commAlpha _ ->

-- let commAlphaList = S.toList commAlpha

-- prettyComms cs = sepByCommas (map pretty cs)

-- in text "[" <+> (pretty p) <> text "]" <+> text "_" <>

-- braces (prettyComms commAlphaList)

instance Pretty CommType where

pretty (CommTypeSort s) = pretty s

pretty (CommTypeChan (TypedChanName c _)) =

-- Only show the channel name

pretty c

-- parens (pretty c <+> comma <+> pretty s)

instance Pretty RENAMING where

pretty renaming = case renaming of

Renaming ids -> ppWithCommas ids

FQRenaming fqTerms -> ppWithCommas fqTerms

-- glue and prec_comp decide whether the child in the parse tree needs

-- to be parenthesised or not. Parentheses are necessary if the

-- right-child is at the same level of precedence as the parent but is

-- a different operator; otherwise, they're not.

glue :: PROCESS -> PROCESS -> Doc

glue x y = if (prec_comp x y)

then lparen <+> pretty y <+> rparen

else pretty y

-- This is really nasty, but sledgehammer effective and allows fine

-- control. Unmaintainable, however. :-( I imagine there's a way to

-- compare the types in a less boilerplate manner, but OTOH there are

-- some special cases where it's nice to be explicit. Also, hiding

-- and renaming are distinctly non-standard. *shrug*

prec_comp :: PROCESS -> PROCESS -> Bool

prec_comp x y =

case x of

Hiding _ _ _ ->

case y of RenamingProcess _ _ _ -> True

_ -> False

RenamingProcess _ _ _ ->

case y of Hiding _ _ _ -> True

_ -> False

Sequential _ _ _ -> False

PrefixProcess _ _ _ ->

case y of Sequential _ _ _ -> True

_ -> False

ExternalChoice _ _ _ ->

case y of InternalChoice _ _ _ -> True

_ -> False

InternalChoice _ _ _ ->

case y of ExternalChoice _ _ _ -> True

_ -> False

Interleaving _ _ _ ->

case y of SynchronousParallel _ _ _ -> True

GeneralisedParallel _ _ _ _ -> True

AlphabetisedParallel _ _ _ _ _ -> True

_ -> False

SynchronousParallel _ _ _ ->

case y of Interleaving _ _ _ -> True

GeneralisedParallel _ _ _ _ -> True

AlphabetisedParallel _ _ _ _ _ -> True

_ -> False

GeneralisedParallel _ _ _ _ ->

case y of Interleaving _ _ _ -> True

SynchronousParallel _ _ _ -> True

AlphabetisedParallel _ _ _ _ _ -> True

_ -> False

AlphabetisedParallel _ _ _ _ _ ->

case y of Interleaving _ _ _ -> True

SynchronousParallel _ _ _ -> True

GeneralisedParallel _ _ _ _ -> True

_ -> False

_ -> False

instance Pretty EVENT where

pretty = printEvent

-- | print an event.

printEvent :: EVENT -> Doc

printEvent ev =

case ev of

TermEvent t _ -> pretty t

InternalPrefixChoice v s _ ->

internal_choice <+> (pretty v) <+> (text svar_sortS) <+> (pretty s)

ExternalPrefixChoice v s _ ->

external_choice <+> (pretty v) <+> (text svar_sortS) <+> (pretty s)

ChanSend cn t _ -> (pretty cn) <+> (text chan_sendS) <+> (pretty t)

ChanNonDetSend cn v s _ ->

(pretty cn) <+> (text chan_sendS) <+> (pretty v)

<+> (text svar_sortS) <+> (pretty s)

ChanRecv cn v s _ ->

(pretty cn) <+> (text chan_receiveS) <+> (pretty v)

<+> (text svar_sortS) <+> (pretty s)

FQEvent e mfqChan fqVar _ -> printFQEvent e mfqChan fqVar

-- | Print a fully qualified event. We need the fully qualified

-- channel (if there is one) and the fully qualified term (which may

-- be an event or a variable). these will be passed in fro mthe

-- printEvent that actually has access to the fully qualfied parts

-- of this fully qualified event.

printFQEvent :: EVENT -> Maybe (CHANNEL_NAME, SORT) -> TERM () -> Doc

printFQEvent ev mfqChan t =

-- We only need to know the underlysing event type as we already

-- have all the fully qualified information.

case ev of

-- mfqChan shoudl be nothing

-- t is the fully qualified term to send

TermEvent _ _ -> pretty t

-- mfqChan shoudl be nothing

-- t is the fully qualified variable

InternalPrefixChoice _ _ _ -> internal_choice <+> pretty t

-- mfqChan shoudl be nothing

-- t is the fully qualified variable

ExternalPrefixChoice _ _ _ -> external_choice <+> pretty t

-- mfqChan should be the fully qualified channel

-- t is the fully qualified term to send

ChanSend _ _ _ ->

case mfqChan of

Just (cn, s) -> (pretty cn) <> colon <> (pretty s)

<+> (text chan_sendS) <+> (pretty t)

Nothing -> text "Error: Case ChanSend in printFQEvent in CspCASL.Print_CspCASL "

-- mfqChan should be the fully qualified channel

-- t is the fully qualified variable

ChanNonDetSend _ _ _ _ ->

case mfqChan of

Just (cn, s) -> (pretty cn) <> colon <> (pretty s)

<+> (text chan_sendS) <+> (pretty t)

Nothing -> text "Error: Case ChanNonDetSend in printFQEvent in CspCASL.Print_CspCASL"

ChanRecv _ _ _ _ ->

case mfqChan of

Just (cn, s) -> (pretty cn) <> colon <> (pretty s)

<+> (text chan_receiveS) <+> (pretty t)

Nothing -> text "Error: Case ChanRecv in printFQEvent in CspCASL.Print_CspCASL"

-- This option should be impossible

FQEvent _ _ _ _ -> text "Error: Case FQEvent in printFQEvent in CspCASL.Print_CspCASL"

instance Pretty EVENT_SET where

pretty = printEventSet

printEventSet :: EVENT_SET -> Doc

printEventSet eventSet =

case eventSet of

EventSet es _ -> ppWithCommas es

FQEventSet es _ -> ppWithCommas es