{-# LANGUAGE DeriveDataTypeable #-}
{- |
Module      :  $Header$
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)
