{- |

Module : ./CspCASL/Print_CspCASL.hs

Description : Pretty printing for CspCASL

Copyright : (c) Andy Gimblett and Uni Bremen 2006

License : GPLv2 or higher, see LICENSE.txt

Maintainer : a.m.gimblett@swansea.ac.uk

Stability : provisional

Portability : portable

Printing abstract syntax of CSP-CASL

-}

module CspCASL.Print_CspCASL where

import CASL.Fold

import CASL.ToDoc

import Common.Doc

import Common.DocUtils

import Common.Keywords (elseS, ifS, thenS, opS, predS)

import CspCASL.AS_CspCASL

import CspCASL.AS_CspCASL_Process

import CspCASL.CspCASL_Keywords

import qualified Data.Set as Set

instance Pretty CspBasicExt where

pretty = printCspBasicExt

instance ListCheck CHANNEL_DECL where

innerList (ChannelDecl l _) = innerList l

printCspBasicExt :: CspBasicExt -> Doc

printCspBasicExt ccs = case ccs of

Channels cs _ -> keyword (channelS ++ pluralS cs)

<+> semiAnnos printChanDecl cs

ProcItems ps _ -> keyword processS

<+> semiAnnos printProcItem ps

instance Pretty FQ_PROCESS_NAME where

pretty = printProcessName

-- | Pretty printing for process profiles

instance Pretty ProcProfile where

pretty = printProcProfile

printCommAlpha :: CommAlpha -> Doc

printCommAlpha = printProcAlphabet . ProcAlphabet . Set.toList

printProcProfile :: ProcProfile -> Doc

printProcProfile (ProcProfile sorts commAlpha) =

sep [printArgs sorts, printCommAlpha commAlpha]

printProcessName :: FQ_PROCESS_NAME -> Doc

printProcessName fqPn = case fqPn of

PROCESS_NAME pn -> pretty pn

FQ_PROCESS_NAME pn profile -> parens $ sep

[ keyword processS <+> pretty pn <> printProcProfile profile]

instance Pretty CHANNEL_DECL where

pretty = printChanDecl

printChanDecl :: CHANNEL_DECL -> Doc

printChanDecl (ChannelDecl ns s) =

ppWithCommas ns <+> colon <+> pretty s

instance Pretty PROC_ITEM where

pretty = printProcItem

printArgs :: Pretty a => [a] -> Doc

printArgs a = if null a then empty else parens $ ppWithCommas a

printProcItem :: PROC_ITEM -> Doc

printProcItem (Proc_Decl pn args alpha) =

sep [pretty pn <> printArgs args, printProcAlphabet alpha]

printProcItem (Proc_Defn pn args alpha p) =

sep [ pretty pn <> printOptArgDecls args

, printProcAlphabet alpha

, equals <+> pretty p]

printProcItem (Proc_Eq pn p) = sep [pretty pn, equals <+> pretty p]

instance Pretty PARM_PROCNAME where

pretty = printParmProcname

printParmProcname :: PARM_PROCNAME -> Doc

printParmProcname (ParmProcname pn args) =

pretty pn <> printArgs args

printProcAlphabet :: PROC_ALPHABET -> Doc

printProcAlphabet (ProcAlphabet commTypes) = colon <+> case commTypes of

[CommTypeSort s] -> pretty s

_ -> braces $ ppWithCommas commTypes

instance Pretty PROCESS where

pretty = printProcess

printProcess :: PROCESS -> Doc

printProcess pr = case pr of

-- precedence 0

Skip _ -> text skipS

Stop _ -> text stopS

Div _ -> text divS

Run es _ -> text runS <+> parens (pretty es)

Chaos es _ -> text chaosS <+> parens (pretty es)

NamedProcess pn ts _ ->

pretty pn <+> printArgs ts

-- precedence 1

ConditionalProcess f p q _ -> fsep

[ keyword ifS <+> pretty f

, keyword thenS <+> pretty p

, keyword elseS <+> pretty q ]

-- precedence 2

Hiding p es _ -> sep

[ lglue pr p, hiding_proc <+> pretty es ]

RenamingProcess p r _ -> sep

[ lglue pr p, ren_proc_open <+> pretty r <+> ren_proc_close ]

-- precedence 3

Sequential p q _ -> sep

[ lglue pr p, sequential <+> glue pr q ]

PrefixProcess event p _ -> sep

[ pretty event <+> prefix_proc, glue pr p ]

-- precedence 4

InternalChoice p q _ -> sep

[ lglue pr p, internal_choice <+> glue pr q ]

ExternalChoice p q _ -> sep

[ lglue pr p, external_choice <+> glue pr q ]

-- precedence 5

Interleaving p q _ -> sep

[ lglue pr p, interleave <+> glue pr q ]

SynchronousParallel p q _ -> sep

[ lglue pr p, synchronous <+> glue pr q ]

GeneralisedParallel p es q _ -> fsep

[ lglue pr p

, genpar_open <+> pretty es <+> genpar_close

, glue pr q ]

AlphabetisedParallel p les res q _ -> fsep

[ lglue pr p

, alpar_open <+> pretty les

, alpar_sep <+> pretty res

, alpar_close <+> glue pr q ]

FQProcess p _ _ -> pretty p

instance Pretty CommType where

pretty (CommTypeSort s) = pretty s

pretty (CommTypeChan (TypedChanName c s)) =

pretty c <+> colon <+> pretty s

instance Pretty Rename where

pretty (Rename i mk) = let n = pretty i in case mk of

Nothing -> n

Just (k, ms) -> case ms of

Nothing -> case k of

BinPred -> keyword predS <+> n

_ -> keyword opS <+> n

Just (s1, s2) -> n <+> colon <+> pretty s1 <+> case k of

BinPred -> cross

TotOp -> funArrow

PartOp -> pfun

<+> pretty s2

instance Pretty RENAMING where

pretty (Renaming ids) = ppWithCommas ids

{- glue and lglue decide whether the child in the parse tree needs

to be parenthesised or not. -}

-- | the second argument is a right argument process of the first argument

glue :: PROCESS -> PROCESS -> Doc

glue x y = let

p = procPrio y

q = procPrio x in

(if p < Cond && (p > q || p == q && p > Pre) then parens else id) $ pretty y

-- | the second argument is a left argument process of the first argument

lglue :: PROCESS -> PROCESS -> Doc

lglue x y =

(if procPrio y > procPrio x || hasRightCond y then parens else id)

$ pretty y

hasRightCond :: PROCESS -> Bool

hasRightCond x = case x of

ConditionalProcess {} -> True

SynchronousParallel _ y _ -> hasRightCond y

GeneralisedParallel _ _ y _ -> hasRightCond y

AlphabetisedParallel _ _ _ y _ -> hasRightCond y

Interleaving _ y _ -> hasRightCond y

ExternalChoice _ y _ -> hasRightCond y

InternalChoice _ y _ -> hasRightCond y

Sequential _ y _ -> hasRightCond y

PrefixProcess _ y _ -> hasRightCond y

_ -> False

{- par binds weakest and is left associative. Then choice follows,

then sequence, then prefix and finally renaming or hiding. -}

data Prio = Prim | Post | Pre | Seq | Choice | Par | Cond deriving (Eq, Ord)

procPrio :: PROCESS -> Prio

procPrio x = case x of

ConditionalProcess {} -> Cond

SynchronousParallel {} -> Par

GeneralisedParallel {} -> Par

AlphabetisedParallel {} -> Par

Interleaving {} -> Par

ExternalChoice {} -> Choice

InternalChoice {} -> Choice

Sequential {} -> Seq

PrefixProcess {} -> Pre

Hiding {} -> Post

RenamingProcess {} -> Post

_ -> Prim

instance Pretty EVENT where

pretty = printEvent

-- | print an event.

printEvent :: EVENT -> Doc

printEvent ev =

let printRecord' = printRecord {

foldQual_var = \ _ v _ _ -> sidDoc v}

caslPrintTerm = foldTerm printRecord'

in case ev of

TermEvent t _ -> caslPrintTerm 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

FQTermEvent t _ -> caslPrintTerm t

FQExternalPrefixChoice t _ -> external_choice <+> pretty t

FQInternalPrefixChoice t _ -> internal_choice <+> pretty t

FQChanSend (cn, s) t _ -> pretty cn <> colon <> pretty s <+>

text chan_sendS <+> pretty t

FQChanNonDetSend (cn, s) v _ -> pretty cn <> colon <> pretty s <+>

text chan_sendS <+> pretty v

FQChanRecv (cn, s) v _ -> pretty cn <> colon <> pretty s <+>

text chan_receiveS <+> pretty v

instance Pretty EVENT_SET where

pretty = printEventSet

printEventSet :: EVENT_SET -> Doc

printEventSet (EventSet es _) = ppWithCommas es