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