content: {-# LANGUAGE DeriveDataTypeable #-}
  {- |
  Module      :  ./CspCASL/AS_CspCASL_Process.der.hs
  Description :  Abstract syntax of CSP-CASL processes
  Copyright   :  (c) Markus Roggenbach and Till Mossakowski and Uni Bremen 2004
  License     :  GPLv2 or higher, see LICENSE.txt
  
  Maintainer  :  a.m.gimblett@swan.ac.uk
  Stability   :  provisional
  Portability :  portable
  
  Abstract syntax of CSP-CASL processes.
  
  -}
  
  module CspCASL.AS_CspCASL_Process
    ( CHANNEL_NAME
    , CommAlpha
    , CommType (..)
    , EVENT (..)
    , EVENT_SET (..)
    , FQ_PROCESS_NAME (..)
    , PROCESS (..)
    , PROCESS_NAME
    , PROC_ARGS
    , PROC_ALPHABET (..)
    , procNameToSimpProcName
    , ProcProfile (..)
    , RenameKind (..)
    , Rename (..)
    , RENAMING (..)
    , splitCASLVar
    , TypedChanName (..)
    ) where
  
  import CASL.AS_Basic_CASL (FORMULA, SORT, TERM (..), VAR)
  
  import Common.Id
  
  import Data.Data
  import qualified Data.Set as Set
  
  -- DrIFT command
  {-! global: GetRange !-}
  
  data EVENT
      -- | @t -> p@ - Term prefix
      = TermEvent (TERM ()) Range
      -- | @[] var :: s -> p@ - External nondeterministic prefix choice
      | ExternalPrefixChoice VAR SORT Range
      -- | @|~| var :: s -> p@ - Internal nondeterministic prefix choice
      | InternalPrefixChoice VAR SORT Range
      -- | @c ! t -> p@ - Channel send
      | ChanSend CHANNEL_NAME (TERM ()) Range
      -- | @c ! var :: s -> p@ - Channel nondeterministic send
      | ChanNonDetSend CHANNEL_NAME VAR SORT Range
      -- | @c ? var :: s -> p@ - Channel recieve
      | ChanRecv CHANNEL_NAME VAR SORT Range
      -- | @t -> p@ - Fully Qualified Term prefix
      | FQTermEvent (TERM ()) Range
      {- | @[] var :: s -> p@ - Fully Qualified External nondeterministic prefix
      choice. The term here holds the fully qualified variable (name and sort). -}
      | FQExternalPrefixChoice (TERM ()) Range
      {- | @|~| var :: s -> p@ - Fully Qualified Internal nondeterministic prefix
      choice. The term here holds the fully qualified variable (name and sort). -}
      | FQInternalPrefixChoice (TERM ()) Range
      {- | @c ! t -> p@ - Fully Qualified Channel send. The term holds the fully
      term to send. -}
      | FQChanSend (CHANNEL_NAME, SORT) (TERM ()) Range
      {- | @c ! var :: s -> p@ - Fully Qualified Channel nondeterministic
      send. The term here holds the fully qualified variable (name and sort). -}
      | FQChanNonDetSend (CHANNEL_NAME, SORT) (TERM ()) Range
      {- | @c ? var :: s -> p@ - Fully Qualified Channel recieve. The term here
      holds the fully qualified variable (name and sort). -}
      | FQChanRecv (CHANNEL_NAME, SORT) (TERM ()) Range
      deriving (Show, Eq, Ord, Typeable, Data)
  
  -- | Event sets are sets of communication types.
  data EVENT_SET = EventSet [CommType] Range
                   deriving (Show, Eq, Ord, Typeable, Data)
  
  data RenameKind = TotOp | PartOp | BinPred deriving (Show, Eq, Ord, Typeable, Data)
  
  data Rename = Rename Id (Maybe (RenameKind, Maybe (SORT, SORT)))
      deriving (Show, Eq, Ord, Typeable, Data)
  
  -- | CSP renamings are predicate names or op names.
  data RENAMING = Renaming [Rename]
                  deriving (Show, Eq, Ord, Typeable, Data)
  
  type CHANNEL_NAME = Id
  
  type PROCESS_NAME = Id
  
  type PROC_ARGS = [SORT]
  
  data PROC_ALPHABET = ProcAlphabet [CommType]
                       deriving (Show, Eq, Ord, Typeable, Data)
  
  splitCASLVar :: TERM () -> (VAR, SORT)
  splitCASLVar (Qual_var v s _ ) = (v, s)
  splitCASLVar _ =
    error "CspCASL.AS_CspCASL_Process: Can not split non Qual_var CASL Term"
  
  {- | Fully qualified process names have parameter sorts, and a communication
  alphabet (a Set of sorts). The CommAlpha here should always contain the minimal
  super sorts only. The communication over subsorts is implied -}
  data ProcProfile = ProcProfile PROC_ARGS CommAlpha
                     deriving (Show, Eq, Ord, Typeable, Data)
  
  {- | A process name is either a fully qualified process name or a plain process
  name. -}
  data FQ_PROCESS_NAME
    -- | A non-fully qualified process name
    = PROCESS_NAME PROCESS_NAME
    {- | A name with parameter sorts and communication ids from the parser.
    This is where the user has tried to specify a fully qualified process name -}
    | FQ_PROCESS_NAME PROCESS_NAME ProcProfile
                    deriving (Show, Eq, Ord, Typeable, Data)
  
  procNameToSimpProcName :: FQ_PROCESS_NAME -> PROCESS_NAME
  procNameToSimpProcName (PROCESS_NAME pn) = pn
  procNameToSimpProcName (FQ_PROCESS_NAME pn _) = pn
  
  {- | A process communication alphabet consists of a set of sort names
  and typed channel names. -}
  data TypedChanName = TypedChanName CHANNEL_NAME SORT
                       deriving (Show, Eq, Ord, Typeable, Data)
  
  data CommType = CommTypeSort SORT
                | CommTypeChan TypedChanName
                  deriving (Eq, Ord, Typeable, Data)
  
  {- | Type of communication types, either a sort communication or a typed channel
  communications. -}
  instance Show CommType where
      show (CommTypeSort s) = show s
      show (CommTypeChan (TypedChanName c s)) = show (c, s)
  
  -- | Type of communication alphabet
  type CommAlpha = Set.Set CommType
  
  -- | CSP-CASL process expressions.
  data PROCESS
      -- | @Skip@ - Terminate immediately
      = Skip Range
      -- | @Stop@ - Do nothing
      | Stop Range
      -- | @div@ - Divergence
      | Div Range
      -- | @Run es@ - Accept any event in es, forever
      | Run EVENT_SET Range
      -- | @Chaos es@ - Accept\/refuse any event in es, forever
      | Chaos EVENT_SET Range
      -- | @event -> p@ - Prefix process
      | PrefixProcess EVENT PROCESS Range
      -- | @p ; q@ - Sequential process
      | Sequential PROCESS PROCESS Range
      -- | @p [] q@ - External choice
      | ExternalChoice PROCESS PROCESS Range
      -- | @p |~| q@ - Internal choice
      | InternalChoice PROCESS PROCESS Range
      -- | @p ||| q@ - Interleaving
      | Interleaving PROCESS PROCESS Range
      -- | @p || q @ - Synchronous parallel
      | SynchronousParallel PROCESS PROCESS Range
      -- | @p [| a |] q@ - Generalised parallel
      | GeneralisedParallel PROCESS EVENT_SET PROCESS Range
      -- | @p [ a || b ] q@ - Alphabetised parallel
      | AlphabetisedParallel PROCESS EVENT_SET EVENT_SET PROCESS Range
      -- | @p \\ es@ - Hiding
      | Hiding PROCESS EVENT_SET Range
      -- | @p [[r]]@ - Renaming
      | RenamingProcess PROCESS RENAMING Range
      -- | @if f then p else q@ - Conditional
      | ConditionalProcess (FORMULA ()) PROCESS PROCESS Range
      -- | Named process
      | NamedProcess FQ_PROCESS_NAME [TERM ()] Range
      {- | Fully qualified process. The range here shall be the same as
      in the process. -}
      | FQProcess PROCESS CommAlpha Range
      deriving (Show, Eq, Ord, Typeable, Data)
  