-----------------------------------------------------------------------------
-- |
-- Module      :  CSPM.CoreLanguage.Process
-- Copyright   :  (c) Fontaine 2010
-- License     :  BSD
-- 
-- Maintainer  :  fontaine@cs.uni-duesseldorf.de
-- Stability   :  experimental
-- Portability :  GHC-only
--
-- This modules defines a FDR-compatible CSP core language.
-- The core language deals with CSP related constructs like processes and events,
-- but abstracts, e.g. from the underlying functional programming language.
--
-- The implementation of the underlying language
-- must provide instances for the type families 'Prefix' and 'ExtProcess' and class 'BL'.
-----------------------------------------------------------------------------
{-# LANGUAGE TypeFamilies #-}

module CSPM.CoreLanguage.Process where

import CSPM.CoreLanguage.Event

-- | A prefix expression.
type family Prefix i

-- | A process that has not yet been switched on.
type family ExtProcess i

class (BE i) => BL i where
  -- | Try to perform an 'Event' return the successor 'Process' or Nothing if the event is
  -- not possible.
  prefixNext :: Prefix i -> Event i -> Maybe (Process i)
  switchOn :: ExtProcess i -> Process i

{-|
  A data type for CSPM processes.
  For efficiency, replicated alphabetized parallel has an explicit constructor.
  Other replicated operations get translated on the fly.
  For constructing processes one should rather uses the wrappers from 
  CSPM.CoreLanguage.ProcessWrappers.
-}
data Process i
  = Prefix (Prefix i)
  | ExternalChoice (Process i) (Process i)
  | InternalChoice (Process i) (Process i)
  | Interleave  (Process i) (Process i)
  | Interrupt (Process i) (Process i)
  | Timeout (Process i) (Process i)
  | Sharing (Process i) (EventSet i) (Process i)
  | AParallel (EventSet i) (EventSet i) (Process i) (Process i) 
  | RepAParallel [(EventSet i,Process i)]
  | Seq (Process i) (Process i)
  | Hide (EventSet i) (Process i)
  | Stop
  | Skip
  | Omega
  | Chaos (EventSet i)
  | AProcess Int -- ^ Just for debugging.
  | SwitchedOff  (ExtProcess i)
  | Renaming (RenamingRelation i) (Process i)
  | LinkParallel (RenamingRelation i) (Process i) (Process i)
  | Exception (EventSet i) (Process i) (Process i)

isOmega :: Process i -> Bool
isOmega Omega = True
isOmega _ = False