{- |
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 :: CspBasicExt -> Doc
pretty = CspBasicExt -> Doc
printCspBasicExt

instance ListCheck CHANNEL_DECL where
  innerList :: CHANNEL_DECL -> [()]
innerList (ChannelDecl l :: [CHANNEL_NAME]
l _) = [CHANNEL_NAME] -> [()]
forall a. ListCheck a => a -> [()]
innerList [CHANNEL_NAME]
l

printCspBasicExt :: CspBasicExt -> Doc
printCspBasicExt :: CspBasicExt -> Doc
printCspBasicExt ccs :: CspBasicExt
ccs = case CspBasicExt
ccs of
  Channels cs :: [Annoted CHANNEL_DECL]
cs _ -> String -> Doc
keyword (String
channelS String -> String -> String
forall a. [a] -> [a] -> [a]
++ [Annoted CHANNEL_DECL] -> String
forall a. ListCheck a => a -> String
pluralS [Annoted CHANNEL_DECL]
cs)
    Doc -> Doc -> Doc
<+> (CHANNEL_DECL -> Doc) -> [Annoted CHANNEL_DECL] -> Doc
forall a. (a -> Doc) -> [Annoted a] -> Doc
semiAnnos CHANNEL_DECL -> Doc
printChanDecl [Annoted CHANNEL_DECL]
cs
  ProcItems ps :: [Annoted PROC_ITEM]
ps _ -> String -> Doc
keyword String
processS
    Doc -> Doc -> Doc
<+> (PROC_ITEM -> Doc) -> [Annoted PROC_ITEM] -> Doc
forall a. (a -> Doc) -> [Annoted a] -> Doc
semiAnnos PROC_ITEM -> Doc
printProcItem [Annoted PROC_ITEM]
ps

instance Pretty FQ_PROCESS_NAME where
  pretty :: FQ_PROCESS_NAME -> Doc
pretty = FQ_PROCESS_NAME -> Doc
printProcessName

-- | Pretty printing for process profiles
instance Pretty ProcProfile where
  pretty :: ProcProfile -> Doc
pretty = ProcProfile -> Doc
printProcProfile

printCommAlpha :: CommAlpha -> Doc
printCommAlpha :: CommAlpha -> Doc
printCommAlpha = PROC_ALPHABET -> Doc
printProcAlphabet (PROC_ALPHABET -> Doc)
-> (CommAlpha -> PROC_ALPHABET) -> CommAlpha -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [CommType] -> PROC_ALPHABET
ProcAlphabet ([CommType] -> PROC_ALPHABET)
-> (CommAlpha -> [CommType]) -> CommAlpha -> PROC_ALPHABET
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CommAlpha -> [CommType]
forall a. Set a -> [a]
Set.toList

printProcProfile :: ProcProfile -> Doc
printProcProfile :: ProcProfile -> Doc
printProcProfile (ProcProfile sorts :: [CHANNEL_NAME]
sorts commAlpha :: CommAlpha
commAlpha) =
  [Doc] -> Doc
sep [[CHANNEL_NAME] -> Doc
forall a. Pretty a => [a] -> Doc
printArgs [CHANNEL_NAME]
sorts, CommAlpha -> Doc
printCommAlpha CommAlpha
commAlpha]

printProcessName :: FQ_PROCESS_NAME -> Doc
printProcessName :: FQ_PROCESS_NAME -> Doc
printProcessName fqPn :: FQ_PROCESS_NAME
fqPn = case FQ_PROCESS_NAME
fqPn of
    PROCESS_NAME pn :: CHANNEL_NAME
pn -> CHANNEL_NAME -> Doc
forall a. Pretty a => a -> Doc
pretty CHANNEL_NAME
pn
    FQ_PROCESS_NAME pn :: CHANNEL_NAME
pn profile :: ProcProfile
profile -> Doc -> Doc
parens (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
sep
      [ String -> Doc
keyword String
processS Doc -> Doc -> Doc
<+> CHANNEL_NAME -> Doc
forall a. Pretty a => a -> Doc
pretty CHANNEL_NAME
pn Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> ProcProfile -> Doc
printProcProfile ProcProfile
profile]

instance Pretty CHANNEL_DECL where
    pretty :: CHANNEL_DECL -> Doc
pretty = CHANNEL_DECL -> Doc
printChanDecl

printChanDecl :: CHANNEL_DECL -> Doc
printChanDecl :: CHANNEL_DECL -> Doc
printChanDecl (ChannelDecl ns :: [CHANNEL_NAME]
ns s :: CHANNEL_NAME
s) =
    [CHANNEL_NAME] -> Doc
forall a. Pretty a => [a] -> Doc
ppWithCommas [CHANNEL_NAME]
ns Doc -> Doc -> Doc
<+> Doc
colon Doc -> Doc -> Doc
<+> CHANNEL_NAME -> Doc
forall a. Pretty a => a -> Doc
pretty CHANNEL_NAME
s

instance Pretty PROC_ITEM where
    pretty :: PROC_ITEM -> Doc
pretty = PROC_ITEM -> Doc
printProcItem

printArgs :: Pretty a => [a] -> Doc
printArgs :: [a] -> Doc
printArgs a :: [a]
a = if [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [a]
a then Doc
empty else Doc -> Doc
parens (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [a] -> Doc
forall a. Pretty a => [a] -> Doc
ppWithCommas [a]
a

printProcItem :: PROC_ITEM -> Doc
printProcItem :: PROC_ITEM -> Doc
printProcItem (Proc_Decl pn :: CHANNEL_NAME
pn args :: [CHANNEL_NAME]
args alpha :: PROC_ALPHABET
alpha) =
    [Doc] -> Doc
sep [CHANNEL_NAME -> Doc
forall a. Pretty a => a -> Doc
pretty CHANNEL_NAME
pn Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> [CHANNEL_NAME] -> Doc
forall a. Pretty a => [a] -> Doc
printArgs [CHANNEL_NAME]
args, PROC_ALPHABET -> Doc
printProcAlphabet PROC_ALPHABET
alpha]
printProcItem (Proc_Defn pn :: CHANNEL_NAME
pn args :: [VAR_DECL]
args alpha :: PROC_ALPHABET
alpha p :: PROCESS
p) =
    [Doc] -> Doc
sep [ CHANNEL_NAME -> Doc
forall a. Pretty a => a -> Doc
pretty CHANNEL_NAME
pn Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> [VAR_DECL] -> Doc
printOptArgDecls [VAR_DECL]
args
        , PROC_ALPHABET -> Doc
printProcAlphabet PROC_ALPHABET
alpha
        , Doc
equals Doc -> Doc -> Doc
<+> PROCESS -> Doc
forall a. Pretty a => a -> Doc
pretty PROCESS
p]
printProcItem (Proc_Eq pn :: PARM_PROCNAME
pn p :: PROCESS
p) = [Doc] -> Doc
sep [PARM_PROCNAME -> Doc
forall a. Pretty a => a -> Doc
pretty PARM_PROCNAME
pn, Doc
equals Doc -> Doc -> Doc
<+> PROCESS -> Doc
forall a. Pretty a => a -> Doc
pretty PROCESS
p]

instance Pretty PARM_PROCNAME where
    pretty :: PARM_PROCNAME -> Doc
pretty = PARM_PROCNAME -> Doc
printParmProcname

printParmProcname :: PARM_PROCNAME -> Doc
printParmProcname :: PARM_PROCNAME -> Doc
printParmProcname (ParmProcname pn :: FQ_PROCESS_NAME
pn args :: [VAR]
args) =
    FQ_PROCESS_NAME -> Doc
forall a. Pretty a => a -> Doc
pretty FQ_PROCESS_NAME
pn Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> [VAR] -> Doc
forall a. Pretty a => [a] -> Doc
printArgs [VAR]
args

printProcAlphabet :: PROC_ALPHABET -> Doc
printProcAlphabet :: PROC_ALPHABET -> Doc
printProcAlphabet (ProcAlphabet commTypes :: [CommType]
commTypes) = Doc
colon Doc -> Doc -> Doc
<+> case [CommType]
commTypes of
  [CommTypeSort s :: CHANNEL_NAME
s] -> CHANNEL_NAME -> Doc
forall a. Pretty a => a -> Doc
pretty CHANNEL_NAME
s
  _ -> Doc -> Doc
braces (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [CommType] -> Doc
forall a. Pretty a => [a] -> Doc
ppWithCommas [CommType]
commTypes

instance Pretty PROCESS where
    pretty :: PROCESS -> Doc
pretty = PROCESS -> Doc
printProcess

printProcess :: PROCESS -> Doc
printProcess :: PROCESS -> Doc
printProcess pr :: PROCESS
pr = case PROCESS
pr of
    -- precedence 0
    Skip _ -> String -> Doc
text String
skipS
    Stop _ -> String -> Doc
text String
stopS
    Div _ -> String -> Doc
text String
divS
    Run es :: EVENT_SET
es _ -> String -> Doc
text String
runS Doc -> Doc -> Doc
<+> Doc -> Doc
parens (EVENT_SET -> Doc
forall a. Pretty a => a -> Doc
pretty EVENT_SET
es)
    Chaos es :: EVENT_SET
es _ -> String -> Doc
text String
chaosS Doc -> Doc -> Doc
<+> Doc -> Doc
parens (EVENT_SET -> Doc
forall a. Pretty a => a -> Doc
pretty EVENT_SET
es)
    NamedProcess pn :: FQ_PROCESS_NAME
pn ts :: [TERM ()]
ts _ ->
        FQ_PROCESS_NAME -> Doc
forall a. Pretty a => a -> Doc
pretty FQ_PROCESS_NAME
pn Doc -> Doc -> Doc
<+> [TERM ()] -> Doc
forall a. Pretty a => [a] -> Doc
printArgs [TERM ()]
ts
    -- precedence 1
    ConditionalProcess f :: FORMULA ()
f p :: PROCESS
p q :: PROCESS
q _ -> [Doc] -> Doc
fsep
        [ String -> Doc
keyword String
ifS Doc -> Doc -> Doc
<+> FORMULA () -> Doc
forall a. Pretty a => a -> Doc
pretty FORMULA ()
f
        , String -> Doc
keyword String
thenS Doc -> Doc -> Doc
<+> PROCESS -> Doc
forall a. Pretty a => a -> Doc
pretty PROCESS
p
        , String -> Doc
keyword String
elseS Doc -> Doc -> Doc
<+> PROCESS -> Doc
forall a. Pretty a => a -> Doc
pretty PROCESS
q ]
    -- precedence 2
    Hiding p :: PROCESS
p es :: EVENT_SET
es _ -> [Doc] -> Doc
sep
        [ PROCESS -> PROCESS -> Doc
lglue PROCESS
pr PROCESS
p, Doc
hiding_proc Doc -> Doc -> Doc
<+> EVENT_SET -> Doc
forall a. Pretty a => a -> Doc
pretty EVENT_SET
es ]
    RenamingProcess p :: PROCESS
p r :: RENAMING
r _ -> [Doc] -> Doc
sep
        [ PROCESS -> PROCESS -> Doc
lglue PROCESS
pr PROCESS
p, Doc
ren_proc_open Doc -> Doc -> Doc
<+> RENAMING -> Doc
forall a. Pretty a => a -> Doc
pretty RENAMING
r Doc -> Doc -> Doc
<+> Doc
ren_proc_close ]
    -- precedence 3
    Sequential p :: PROCESS
p q :: PROCESS
q _ -> [Doc] -> Doc
sep
        [ PROCESS -> PROCESS -> Doc
lglue PROCESS
pr PROCESS
p, Doc
sequential Doc -> Doc -> Doc
<+> PROCESS -> PROCESS -> Doc
glue PROCESS
pr PROCESS
q ]
    PrefixProcess event :: EVENT
event p :: PROCESS
p _ -> [Doc] -> Doc
sep
        [ EVENT -> Doc
forall a. Pretty a => a -> Doc
pretty EVENT
event Doc -> Doc -> Doc
<+> Doc
prefix_proc, PROCESS -> PROCESS -> Doc
glue PROCESS
pr PROCESS
p ]
    -- precedence 4
    InternalChoice p :: PROCESS
p q :: PROCESS
q _ -> [Doc] -> Doc
sep
        [ PROCESS -> PROCESS -> Doc
lglue PROCESS
pr PROCESS
p, Doc
internal_choice Doc -> Doc -> Doc
<+> PROCESS -> PROCESS -> Doc
glue PROCESS
pr PROCESS
q ]
    ExternalChoice p :: PROCESS
p q :: PROCESS
q _ -> [Doc] -> Doc
sep
        [ PROCESS -> PROCESS -> Doc
lglue PROCESS
pr PROCESS
p, Doc
external_choice Doc -> Doc -> Doc
<+> PROCESS -> PROCESS -> Doc
glue PROCESS
pr PROCESS
q ]
    -- precedence 5
    Interleaving p :: PROCESS
p q :: PROCESS
q _ -> [Doc] -> Doc
sep
        [ PROCESS -> PROCESS -> Doc
lglue PROCESS
pr PROCESS
p, Doc
interleave Doc -> Doc -> Doc
<+> PROCESS -> PROCESS -> Doc
glue PROCESS
pr PROCESS
q ]
    SynchronousParallel p :: PROCESS
p q :: PROCESS
q _ -> [Doc] -> Doc
sep
        [ PROCESS -> PROCESS -> Doc
lglue PROCESS
pr PROCESS
p, Doc
synchronous Doc -> Doc -> Doc
<+> PROCESS -> PROCESS -> Doc
glue PROCESS
pr PROCESS
q ]
    GeneralisedParallel p :: PROCESS
p es :: EVENT_SET
es q :: PROCESS
q _ -> [Doc] -> Doc
fsep
        [ PROCESS -> PROCESS -> Doc
lglue PROCESS
pr PROCESS
p
        , Doc
genpar_open Doc -> Doc -> Doc
<+> EVENT_SET -> Doc
forall a. Pretty a => a -> Doc
pretty EVENT_SET
es Doc -> Doc -> Doc
<+> Doc
genpar_close
        , PROCESS -> PROCESS -> Doc
glue PROCESS
pr PROCESS
q ]
    AlphabetisedParallel p :: PROCESS
p les :: EVENT_SET
les res :: EVENT_SET
res q :: PROCESS
q _ -> [Doc] -> Doc
fsep
        [ PROCESS -> PROCESS -> Doc
lglue PROCESS
pr PROCESS
p
        , Doc
alpar_open Doc -> Doc -> Doc
<+> EVENT_SET -> Doc
forall a. Pretty a => a -> Doc
pretty EVENT_SET
les
        , Doc
alpar_sep Doc -> Doc -> Doc
<+> EVENT_SET -> Doc
forall a. Pretty a => a -> Doc
pretty EVENT_SET
res
        , Doc
alpar_close Doc -> Doc -> Doc
<+> PROCESS -> PROCESS -> Doc
glue PROCESS
pr PROCESS
q ]
    FQProcess p :: PROCESS
p _ _ -> PROCESS -> Doc
forall a. Pretty a => a -> Doc
pretty PROCESS
p

instance Pretty CommType where
    pretty :: CommType -> Doc
pretty (CommTypeSort s :: CHANNEL_NAME
s) = CHANNEL_NAME -> Doc
forall a. Pretty a => a -> Doc
pretty CHANNEL_NAME
s
    pretty (CommTypeChan (TypedChanName c :: CHANNEL_NAME
c s :: CHANNEL_NAME
s)) =
        CHANNEL_NAME -> Doc
forall a. Pretty a => a -> Doc
pretty CHANNEL_NAME
c Doc -> Doc -> Doc
<+> Doc
colon Doc -> Doc -> Doc
<+> CHANNEL_NAME -> Doc
forall a. Pretty a => a -> Doc
pretty CHANNEL_NAME
s

instance Pretty Rename where
  pretty :: Rename -> Doc
pretty (Rename i :: CHANNEL_NAME
i mk :: Maybe (RenameKind, Maybe (CHANNEL_NAME, CHANNEL_NAME))
mk) = let n :: Doc
n = CHANNEL_NAME -> Doc
forall a. Pretty a => a -> Doc
pretty CHANNEL_NAME
i in case Maybe (RenameKind, Maybe (CHANNEL_NAME, CHANNEL_NAME))
mk of
    Nothing -> Doc
n
    Just (k :: RenameKind
k, ms :: Maybe (CHANNEL_NAME, CHANNEL_NAME)
ms) -> case Maybe (CHANNEL_NAME, CHANNEL_NAME)
ms of
      Nothing -> case RenameKind
k of
        BinPred -> String -> Doc
keyword String
predS Doc -> Doc -> Doc
<+> Doc
n
        _ -> String -> Doc
keyword String
opS Doc -> Doc -> Doc
<+> Doc
n
      Just (s1 :: CHANNEL_NAME
s1, s2 :: CHANNEL_NAME
s2) -> Doc
n Doc -> Doc -> Doc
<+> Doc
colon Doc -> Doc -> Doc
<+> CHANNEL_NAME -> Doc
forall a. Pretty a => a -> Doc
pretty CHANNEL_NAME
s1 Doc -> Doc -> Doc
<+> case RenameKind
k of
          BinPred -> Doc
cross
          TotOp -> Doc
funArrow
          PartOp -> Doc
pfun
        Doc -> Doc -> Doc
<+> CHANNEL_NAME -> Doc
forall a. Pretty a => a -> Doc
pretty CHANNEL_NAME
s2

instance Pretty RENAMING where
    pretty :: RENAMING -> Doc
pretty (Renaming ids :: [Rename]
ids) = [Rename] -> Doc
forall a. Pretty a => [a] -> Doc
ppWithCommas [Rename]
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 :: PROCESS -> PROCESS -> Doc
glue x :: PROCESS
x y :: PROCESS
y = let
  p :: Prio
p = PROCESS -> Prio
procPrio PROCESS
y
  q :: Prio
q = PROCESS -> Prio
procPrio PROCESS
x in
  (if Prio
p Prio -> Prio -> Bool
forall a. Ord a => a -> a -> Bool
< Prio
Cond Bool -> Bool -> Bool
&& (Prio
p Prio -> Prio -> Bool
forall a. Ord a => a -> a -> Bool
> Prio
q Bool -> Bool -> Bool
|| Prio
p Prio -> Prio -> Bool
forall a. Eq a => a -> a -> Bool
== Prio
q Bool -> Bool -> Bool
&& Prio
p Prio -> Prio -> Bool
forall a. Ord a => a -> a -> Bool
> Prio
Pre) then Doc -> Doc
parens else Doc -> Doc
forall a. a -> a
id) (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ PROCESS -> Doc
forall a. Pretty a => a -> Doc
pretty PROCESS
y

-- | the second argument is a left argument process of the first argument
lglue :: PROCESS -> PROCESS -> Doc
lglue :: PROCESS -> PROCESS -> Doc
lglue x :: PROCESS
x y :: PROCESS
y =
  (if PROCESS -> Prio
procPrio PROCESS
y Prio -> Prio -> Bool
forall a. Ord a => a -> a -> Bool
> PROCESS -> Prio
procPrio PROCESS
x Bool -> Bool -> Bool
|| PROCESS -> Bool
hasRightCond PROCESS
y then Doc -> Doc
parens else Doc -> Doc
forall a. a -> a
id)
  (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ PROCESS -> Doc
forall a. Pretty a => a -> Doc
pretty PROCESS
y

hasRightCond :: PROCESS -> Bool
hasRightCond :: PROCESS -> Bool
hasRightCond x :: PROCESS
x = case PROCESS
x of
  ConditionalProcess {} -> Bool
True
  SynchronousParallel _ y :: PROCESS
y _ -> PROCESS -> Bool
hasRightCond PROCESS
y
  GeneralisedParallel _ _ y :: PROCESS
y _ -> PROCESS -> Bool
hasRightCond PROCESS
y
  AlphabetisedParallel _ _ _ y :: PROCESS
y _ -> PROCESS -> Bool
hasRightCond PROCESS
y
  Interleaving _ y :: PROCESS
y _ -> PROCESS -> Bool
hasRightCond PROCESS
y
  ExternalChoice _ y :: PROCESS
y _ -> PROCESS -> Bool
hasRightCond PROCESS
y
  InternalChoice _ y :: PROCESS
y _ -> PROCESS -> Bool
hasRightCond PROCESS
y
  Sequential _ y :: PROCESS
y _ -> PROCESS -> Bool
hasRightCond PROCESS
y
  PrefixProcess _ y :: PROCESS
y _ -> PROCESS -> Bool
hasRightCond PROCESS
y
  _ -> Bool
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 (Prio -> Prio -> Bool
(Prio -> Prio -> Bool) -> (Prio -> Prio -> Bool) -> Eq Prio
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Prio -> Prio -> Bool
$c/= :: Prio -> Prio -> Bool
== :: Prio -> Prio -> Bool
$c== :: Prio -> Prio -> Bool
Eq, Eq Prio
Eq Prio =>
(Prio -> Prio -> Ordering)
-> (Prio -> Prio -> Bool)
-> (Prio -> Prio -> Bool)
-> (Prio -> Prio -> Bool)
-> (Prio -> Prio -> Bool)
-> (Prio -> Prio -> Prio)
-> (Prio -> Prio -> Prio)
-> Ord Prio
Prio -> Prio -> Bool
Prio -> Prio -> Ordering
Prio -> Prio -> Prio
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Prio -> Prio -> Prio
$cmin :: Prio -> Prio -> Prio
max :: Prio -> Prio -> Prio
$cmax :: Prio -> Prio -> Prio
>= :: Prio -> Prio -> Bool
$c>= :: Prio -> Prio -> Bool
> :: Prio -> Prio -> Bool
$c> :: Prio -> Prio -> Bool
<= :: Prio -> Prio -> Bool
$c<= :: Prio -> Prio -> Bool
< :: Prio -> Prio -> Bool
$c< :: Prio -> Prio -> Bool
compare :: Prio -> Prio -> Ordering
$ccompare :: Prio -> Prio -> Ordering
$cp1Ord :: Eq Prio
Ord)

procPrio :: PROCESS -> Prio
procPrio :: PROCESS -> Prio
procPrio x :: PROCESS
x = case PROCESS
x of
  ConditionalProcess {} -> Prio
Cond
  SynchronousParallel {} -> Prio
Par
  GeneralisedParallel {} -> Prio
Par
  AlphabetisedParallel {} -> Prio
Par
  Interleaving {} -> Prio
Par
  ExternalChoice {} -> Prio
Choice
  InternalChoice {} -> Prio
Choice
  Sequential {} -> Prio
Seq
  PrefixProcess {} -> Prio
Pre
  Hiding {} -> Prio
Post
  RenamingProcess {} -> Prio
Post
  _ -> Prio
Prim

instance Pretty EVENT where
    pretty :: EVENT -> Doc
pretty = EVENT -> Doc
printEvent

-- | print an event.
printEvent :: EVENT -> Doc
printEvent :: EVENT -> Doc
printEvent ev :: EVENT
ev =
    let printRecord' :: Record () Doc Doc
printRecord' = Record () Doc Doc
forall f. FormExtension f => Record f Doc Doc
printRecord {
          foldQual_var :: TERM () -> VAR -> CHANNEL_NAME -> Range -> Doc
foldQual_var = \ _ v :: VAR
v _ _ -> VAR -> Doc
sidDoc VAR
v}

        caslPrintTerm :: TERM () -> Doc
caslPrintTerm = Record () Doc Doc -> TERM () -> Doc
forall f a b. Record f a b -> TERM f -> b
foldTerm Record () Doc Doc
printRecord'
    in case EVENT
ev of
      TermEvent t :: TERM ()
t _ -> TERM () -> Doc
caslPrintTerm TERM ()
t
      InternalPrefixChoice v :: VAR
v s :: CHANNEL_NAME
s _ ->
          Doc
internal_choice Doc -> Doc -> Doc
<+> VAR -> Doc
forall a. Pretty a => a -> Doc
pretty VAR
v Doc -> Doc -> Doc
<+> String -> Doc
text String
svar_sortS Doc -> Doc -> Doc
<+> CHANNEL_NAME -> Doc
forall a. Pretty a => a -> Doc
pretty CHANNEL_NAME
s
      ExternalPrefixChoice v :: VAR
v s :: CHANNEL_NAME
s _ ->
          Doc
external_choice Doc -> Doc -> Doc
<+> VAR -> Doc
forall a. Pretty a => a -> Doc
pretty VAR
v Doc -> Doc -> Doc
<+> String -> Doc
text String
svar_sortS Doc -> Doc -> Doc
<+> CHANNEL_NAME -> Doc
forall a. Pretty a => a -> Doc
pretty CHANNEL_NAME
s
      ChanSend cn :: CHANNEL_NAME
cn t :: TERM ()
t _ -> CHANNEL_NAME -> Doc
forall a. Pretty a => a -> Doc
pretty CHANNEL_NAME
cn Doc -> Doc -> Doc
<+> String -> Doc
text String
chan_sendS Doc -> Doc -> Doc
<+> TERM () -> Doc
forall a. Pretty a => a -> Doc
pretty TERM ()
t
      ChanNonDetSend cn :: CHANNEL_NAME
cn v :: VAR
v s :: CHANNEL_NAME
s _ ->
          CHANNEL_NAME -> Doc
forall a. Pretty a => a -> Doc
pretty CHANNEL_NAME
cn Doc -> Doc -> Doc
<+> String -> Doc
text String
chan_sendS Doc -> Doc -> Doc
<+> VAR -> Doc
forall a. Pretty a => a -> Doc
pretty VAR
v
                          Doc -> Doc -> Doc
<+> String -> Doc
text String
svar_sortS Doc -> Doc -> Doc
<+> CHANNEL_NAME -> Doc
forall a. Pretty a => a -> Doc
pretty CHANNEL_NAME
s
      ChanRecv cn :: CHANNEL_NAME
cn v :: VAR
v s :: CHANNEL_NAME
s _ ->
          CHANNEL_NAME -> Doc
forall a. Pretty a => a -> Doc
pretty CHANNEL_NAME
cn Doc -> Doc -> Doc
<+> String -> Doc
text String
chan_receiveS Doc -> Doc -> Doc
<+> VAR -> Doc
forall a. Pretty a => a -> Doc
pretty VAR
v
                          Doc -> Doc -> Doc
<+> String -> Doc
text String
svar_sortS Doc -> Doc -> Doc
<+> CHANNEL_NAME -> Doc
forall a. Pretty a => a -> Doc
pretty CHANNEL_NAME
s
      FQTermEvent t :: TERM ()
t _ -> TERM () -> Doc
caslPrintTerm TERM ()
t
      FQExternalPrefixChoice t :: TERM ()
t _ -> Doc
external_choice Doc -> Doc -> Doc
<+> TERM () -> Doc
forall a. Pretty a => a -> Doc
pretty TERM ()
t
      FQInternalPrefixChoice t :: TERM ()
t _ -> Doc
internal_choice Doc -> Doc -> Doc
<+> TERM () -> Doc
forall a. Pretty a => a -> Doc
pretty TERM ()
t
      FQChanSend (cn :: CHANNEL_NAME
cn, s :: CHANNEL_NAME
s) t :: TERM ()
t _ -> CHANNEL_NAME -> Doc
forall a. Pretty a => a -> Doc
pretty CHANNEL_NAME
cn Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
colon Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> CHANNEL_NAME -> Doc
forall a. Pretty a => a -> Doc
pretty CHANNEL_NAME
s Doc -> Doc -> Doc
<+>
                                String -> Doc
text String
chan_sendS Doc -> Doc -> Doc
<+> TERM () -> Doc
forall a. Pretty a => a -> Doc
pretty TERM ()
t
      FQChanNonDetSend (cn :: CHANNEL_NAME
cn, s :: CHANNEL_NAME
s) v :: TERM ()
v _ -> CHANNEL_NAME -> Doc
forall a. Pretty a => a -> Doc
pretty CHANNEL_NAME
cn Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
colon Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> CHANNEL_NAME -> Doc
forall a. Pretty a => a -> Doc
pretty CHANNEL_NAME
s Doc -> Doc -> Doc
<+>
                                      String -> Doc
text String
chan_sendS Doc -> Doc -> Doc
<+> TERM () -> Doc
forall a. Pretty a => a -> Doc
pretty TERM ()
v
      FQChanRecv (cn :: CHANNEL_NAME
cn, s :: CHANNEL_NAME
s) v :: TERM ()
v _ -> CHANNEL_NAME -> Doc
forall a. Pretty a => a -> Doc
pretty CHANNEL_NAME
cn Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
colon Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> CHANNEL_NAME -> Doc
forall a. Pretty a => a -> Doc
pretty CHANNEL_NAME
s Doc -> Doc -> Doc
<+>
                                String -> Doc
text String
chan_receiveS Doc -> Doc -> Doc
<+> TERM () -> Doc
forall a. Pretty a => a -> Doc
pretty TERM ()
v

instance Pretty EVENT_SET where
    pretty :: EVENT_SET -> Doc
pretty = EVENT_SET -> Doc
printEventSet

printEventSet :: EVENT_SET -> Doc
printEventSet :: EVENT_SET -> Doc
printEventSet (EventSet es :: [CommType]
es _) = [CommType] -> Doc
forall a. Pretty a => [a] -> Doc
ppWithCommas [CommType]
es