0c405883d2777e4428138f055e84b3f98160b1fcChristian Maeder{- |

e9458b1a7a19a63aa4c179f9ab20f4d50681c168Jens ElknerModule : $Id$

c7b8ecdfb448048ad7c716be3a5ceb6d845ad194Christian MaederDescription : Pretty printing for CspCASL

c7b8ecdfb448048ad7c716be3a5ceb6d845ad194Christian MaederCopyright : (c) Andy Gimblett and Uni Bremen 2006

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

0c405883d2777e4428138f055e84b3f98160b1fcChristian Maeder

3f69b6948966979163bdfe8331c38833d5d90ecdChristian MaederMaintainer : a.m.gimblett@swansea.ac.uk

0c405883d2777e4428138f055e84b3f98160b1fcChristian MaederStability : provisional

513ec62039bb1028efafff52f0e0e22d57da261eChristian MaederPortability : portable

0c405883d2777e4428138f055e84b3f98160b1fcChristian Maeder

f3a94a197960e548ecd6520bb768cb0d547457bbChristian MaederPrinting abstract syntax of CSP-CASL

0c405883d2777e4428138f055e84b3f98160b1fcChristian Maeder

0c405883d2777e4428138f055e84b3f98160b1fcChristian Maeder-}

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroedermodule CspCASL.Print_CspCASL where

0c405883d2777e4428138f055e84b3f98160b1fcChristian Maeder

0c405883d2777e4428138f055e84b3f98160b1fcChristian Maederimport CASL.ToDoc ()

ad270004874ce1d0697fb30d7309f180553bb315Christian Maeder

ad270004874ce1d0697fb30d7309f180553bb315Christian Maederimport Common.Doc

0c405883d2777e4428138f055e84b3f98160b1fcChristian Maederimport Common.DocUtils

0c405883d2777e4428138f055e84b3f98160b1fcChristian Maederimport Common.Keywords (colonS, elseS, ifS, thenS)

0c405883d2777e4428138f055e84b3f98160b1fcChristian Maeder

0c405883d2777e4428138f055e84b3f98160b1fcChristian Maederimport CspCASL.AS_CspCASL

513ec62039bb1028efafff52f0e0e22d57da261eChristian Maederimport CspCASL.AS_CspCASL_Process

0c405883d2777e4428138f055e84b3f98160b1fcChristian Maederimport CspCASL.CspCASL_Keywords

0c405883d2777e4428138f055e84b3f98160b1fcChristian Maeder

513ec62039bb1028efafff52f0e0e22d57da261eChristian Maederinstance Pretty CspBasicSpec where

513ec62039bb1028efafff52f0e0e22d57da261eChristian Maeder pretty = printCspBasicSpec

e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian Maeder

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederprintCspBasicSpec :: CspBasicSpec -> Doc

513ec62039bb1028efafff52f0e0e22d57da261eChristian MaederprintCspBasicSpec ccs =

e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian Maeder (text processS) <+> (printProcEqs (processes ccs))

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder

0c405883d2777e4428138f055e84b3f98160b1fcChristian MaederprintProcEqs :: [PROC_EQ] -> Doc

0c405883d2777e4428138f055e84b3f98160b1fcChristian MaederprintProcEqs peqs = foldl ($+$) empty (map pretty peqs)

0c405883d2777e4428138f055e84b3f98160b1fcChristian Maeder

0c405883d2777e4428138f055e84b3f98160b1fcChristian Maederinstance Pretty PROC_EQ where

e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian Maeder pretty = printProcEq

e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian Maeder

e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian MaederprintProcEq :: PROC_EQ -> Doc

0c405883d2777e4428138f055e84b3f98160b1fcChristian MaederprintProcEq (ProcEq pn p) =

0c405883d2777e4428138f055e84b3f98160b1fcChristian Maeder (pretty pn) <+> (text "=") <+> (pretty p)

0c405883d2777e4428138f055e84b3f98160b1fcChristian Maeder

0c405883d2777e4428138f055e84b3f98160b1fcChristian Maederinstance Pretty PARM_PROCNAME where

0c405883d2777e4428138f055e84b3f98160b1fcChristian Maeder pretty = printParmProcname

0c405883d2777e4428138f055e84b3f98160b1fcChristian Maeder

513ec62039bb1028efafff52f0e0e22d57da261eChristian MaederprintParmProcname :: PARM_PROCNAME -> Doc

0c405883d2777e4428138f055e84b3f98160b1fcChristian MaederprintParmProcname (ParmProcname pn args) =

0c405883d2777e4428138f055e84b3f98160b1fcChristian Maeder pretty pn <+> (printArgs args)

0c405883d2777e4428138f055e84b3f98160b1fcChristian Maeder where printArgs [] = text ""

0c405883d2777e4428138f055e84b3f98160b1fcChristian Maeder printArgs a = lparen <+> (ppWithSemis a) <+> rparen

0c405883d2777e4428138f055e84b3f98160b1fcChristian Maeder ppWithSemis = sepBySemis . map pretty

0c405883d2777e4428138f055e84b3f98160b1fcChristian Maeder sepBySemis = fsep . punctuate semi

0c405883d2777e4428138f055e84b3f98160b1fcChristian Maeder

0c405883d2777e4428138f055e84b3f98160b1fcChristian Maederinstance Pretty PARG_DECL where

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder pretty = printPargDecl

0c405883d2777e4428138f055e84b3f98160b1fcChristian Maeder

0c405883d2777e4428138f055e84b3f98160b1fcChristian MaederprintPargDecl :: PARG_DECL -> Doc

0c405883d2777e4428138f055e84b3f98160b1fcChristian MaederprintPargDecl (PargDecl vs es) =

0c405883d2777e4428138f055e84b3f98160b1fcChristian Maeder (ppWithCommas vs) <+> (text colonS) <+> (pretty es)

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder

0c405883d2777e4428138f055e84b3f98160b1fcChristian Maederinstance Pretty PROCESS where

e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian Maeder pretty = printProcess

e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian Maeder

0c405883d2777e4428138f055e84b3f98160b1fcChristian MaederprintProcess :: PROCESS -> Doc

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederprintProcess pr = case pr of

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder -- precedence 0

0c405883d2777e4428138f055e84b3f98160b1fcChristian Maeder Skip -> text skipS

513ec62039bb1028efafff52f0e0e22d57da261eChristian Maeder Stop -> text stopS

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder Div -> text divS

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder Run es -> (text runS) <+> (pretty es)

0c405883d2777e4428138f055e84b3f98160b1fcChristian Maeder Chaos es -> (text chaosS) <+> (pretty es)

0c405883d2777e4428138f055e84b3f98160b1fcChristian Maeder NamedProcess pn es ->

0c405883d2777e4428138f055e84b3f98160b1fcChristian Maeder (pretty pn) <+> lparen <+> (ppWithCommas es) <+> rparen

0c405883d2777e4428138f055e84b3f98160b1fcChristian Maeder -- precedence 1

0c405883d2777e4428138f055e84b3f98160b1fcChristian Maeder ConditionalProcess f p q ->

0c405883d2777e4428138f055e84b3f98160b1fcChristian Maeder ((text ifS) <+> (pretty f) <+>

0c405883d2777e4428138f055e84b3f98160b1fcChristian Maeder (text thenS) <+> (glue pr p) <+>

0c405883d2777e4428138f055e84b3f98160b1fcChristian Maeder (text elseS) <+> (glue pr q)

0c405883d2777e4428138f055e84b3f98160b1fcChristian Maeder )

0c405883d2777e4428138f055e84b3f98160b1fcChristian Maeder -- precedence 2

0c405883d2777e4428138f055e84b3f98160b1fcChristian Maeder Hiding p es ->

0c405883d2777e4428138f055e84b3f98160b1fcChristian Maeder (pretty p) <+> (text hidingS) <+> (pretty es)

0c405883d2777e4428138f055e84b3f98160b1fcChristian Maeder RelationalRenaming p r ->

0c405883d2777e4428138f055e84b3f98160b1fcChristian Maeder ((pretty p) <+>

0c405883d2777e4428138f055e84b3f98160b1fcChristian Maeder (text renaming_openS) <+>

0c405883d2777e4428138f055e84b3f98160b1fcChristian Maeder (ppWithCommas r) <+>

0c405883d2777e4428138f055e84b3f98160b1fcChristian Maeder (text renaming_closeS))

0c405883d2777e4428138f055e84b3f98160b1fcChristian Maeder -- precedence 3

0c405883d2777e4428138f055e84b3f98160b1fcChristian Maeder Sequential p q ->

0c405883d2777e4428138f055e84b3f98160b1fcChristian Maeder (pretty p) <+> semi <+> (glue pr q)

0c405883d2777e4428138f055e84b3f98160b1fcChristian Maeder PrefixProcess ev p ->

0c405883d2777e4428138f055e84b3f98160b1fcChristian Maeder (pretty ev) <+> (text prefixS) <+> (glue pr p)

0c405883d2777e4428138f055e84b3f98160b1fcChristian Maeder InternalPrefixProcess v es p ->

0c405883d2777e4428138f055e84b3f98160b1fcChristian Maeder ((text internal_prefixS) <+> (pretty v) <+>

0c405883d2777e4428138f055e84b3f98160b1fcChristian Maeder (text colonS) <+> (pretty es) <+>

0c405883d2777e4428138f055e84b3f98160b1fcChristian Maeder (text prefixS) <+> (glue pr p)

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder )

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder ExternalPrefixProcess v es p ->

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder ((text external_prefixS) <+> (pretty v) <+>

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder (text colonS) <+> (pretty es) <+>

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder (text prefixS) <+> (glue pr p)

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder )

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder -- precedence 4

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder ExternalChoice p q ->

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder (pretty p) <+> (text external_choiceS) <+> (glue pr q)

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder InternalChoice p q ->

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder (pretty p) <+> (text internal_choiceS) <+> (glue pr q)

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder -- precedence 5

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder Interleaving p q ->

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder (pretty p) <+> (text interleavingS) <+> (glue pr q)

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder SynchronousParallel p q ->

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder (pretty p) <+> (text synchronousS) <+> (glue pr q)

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder GeneralisedParallel p es q ->

((pretty p) <+> (text general_parallel_openS) <+>

(pretty es) <+>

(text general_parallel_closeS) <+> (glue pr q))

AlphabetisedParallel p les res q ->

((pretty p) <+> (text alpha_parallel_openS) <+>

(pretty les) <+> (text alpha_parallel_sepS) <+> (pretty res) <+>

(text alpha_parallel_closeS) <+> (glue pr q)

)

-- 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 RelationalRenaming _ _ -> True

_ -> False

RelationalRenaming _ _ ->

case y of Hiding _ _ -> True

_ -> False

Sequential _ _ ->

case y of InternalPrefixProcess _ _ _ -> True

ExternalPrefixProcess _ _ _ -> True

_ -> False

PrefixProcess _ _ ->

case y of Sequential _ _ -> True

_ -> False

InternalPrefixProcess _ _ _ ->

case y of Sequential _ _ -> True

_ -> False

ExternalPrefixProcess _ _ _ ->

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

printEvent :: EVENT -> Doc

printEvent (Event t) = pretty t

instance Pretty EVENT_SET where

pretty = printEventSet

printEventSet :: EVENT_SET -> Doc

printEventSet (EventSet s) = pretty s

printEventSet EmptyEventSet = text "{}"

instance Pretty CSP_FORMULA where

pretty = printCspFormula

printCspFormula :: CSP_FORMULA -> Doc

printCspFormula (Formula f) = pretty f