content: {- |
  Module      :  ./CspCASL/Core_CspCASL.hs
  Description :  Conversion to core 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
  
  Converting sugared CspCASL to core CspCASL.
  
  The following process types are core:
  
    Skip
    Stop
    PrefixProcess ev p
    ExternalPrefixProcess v es p
    InternalPrefixProcess v es p
    Sequential p q
    ExternalChoice p q
    InternalChoice p q
    GeneralisedParallel p es q
    Hiding p es
    RelationalRenaming p RENAMING
    NamedProcess pn evs
    ConditionalProcess CSP_FORMULA p q
  
    (Also the interrupt operator should be added, and core?)
  
  -}
  
  module CspCASL.Core_CspCASL (basicToCore) where
  
  import Common.Id
  
  import CspCASL.AS_CspCASL
  import CspCASL.AS_CspCASL_Process
  
  basicToCore :: CspBasicSpec -> CspBasicSpec
  basicToCore c = CspBasicSpec (channels c) core_procs
      where core_procs = map procEqToCore (proc_items c)
            procEqToCore (Proc_Eq pn p) = Proc_Eq pn (procToCore p)
            procEqToCore x = x
  
  procToCore :: PROCESS -> PROCESS
  procToCore proc = let p' = procToCore in case proc of
      -- First the core operators: we just need to recurse.
      (Skip r) -> Skip r
      (Stop r) -> Stop r
      (PrefixProcess ev p r) -> PrefixProcess ev (p' p) r
      (ExternalPrefixProcess v es p r) -> ExternalPrefixProcess v es (p' p) r
      (InternalPrefixProcess v es p r) -> InternalPrefixProcess v es (p' p) r
      (Sequential p q r) -> Sequential (p' p) (p' q) r
      (ExternalChoice p q r) -> ExternalChoice (p' p) (p' q) r
      (InternalChoice p q r) -> InternalChoice (p' p) (p' q) r
      (GeneralisedParallel p es q r) -> GeneralisedParallel (p' p) es (p' q) r
      (Hiding p es r) -> Hiding (p' p) es r
      (RelationalRenaming p rn r) -> RelationalRenaming (p' p) rn r
      (NamedProcess pn evs r) -> NamedProcess pn evs r
      (ConditionalProcess f p q r) -> ConditionalProcess f (p' p) (p' q) r
      -- Non-core, done.
      (Interleaving p q r) -> GeneralisedParallel (p' p
                               (EventSet [] nullRange) (p' q) r)
      -- Non-core, not done yet.
      (Div r) -> Div r
      (Run es r) -> Run es r
      (Chaos es r) -> Chaos es r
      (SynchronousParallel p q r) -> SynchronousParallel (p' p) (p' q) r
      (AlphabetisedParallel p esp esq q r) ->
          AlphabetisedParallel (p' p) esp esq (p' q) r
  