Print_CspCASL.hs

{- |
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