Core_CspCASL.hs revision 5858e6262048894b0e933b547852f04aed009b58
e39a1626bee36d6ad13a2c0014a80ef179a65bcbChristian MaederDescription : Conversion to core CspCASL
e39a1626bee36d6ad13a2c0014a80ef179a65bcbChristian MaederCopyright : (c) Andy Gimblett and Uni Bremen 2006
e39a1626bee36d6ad13a2c0014a80ef179a65bcbChristian MaederLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
e39a1626bee36d6ad13a2c0014a80ef179a65bcbChristian MaederMaintainer : a.m.gimblett@swansea.ac.uk
e39a1626bee36d6ad13a2c0014a80ef179a65bcbChristian MaederStability : provisional
e39a1626bee36d6ad13a2c0014a80ef179a65bcbChristian MaederPortability : portable
e39a1626bee36d6ad13a2c0014a80ef179a65bcbChristian MaederConverting sugared CspCASL to core CspCASL.
e39a1626bee36d6ad13a2c0014a80ef179a65bcbChristian MaederThe following process types are core:
e39a1626bee36d6ad13a2c0014a80ef179a65bcbChristian Maeder PrefixProcess ev p
0243238805d31e597195ef974e8e7eccb587a390Christian Maeder ExternalPrefixProcess v es p
14a6ec72de5c35d65c2adcd54b6fecbd8bc271b6Christian Maeder InternalPrefixProcess v es p
e39a1626bee36d6ad13a2c0014a80ef179a65bcbChristian Maeder Sequential p q
0243238805d31e597195ef974e8e7eccb587a390Christian Maeder ExternalChoice p q
e39a1626bee36d6ad13a2c0014a80ef179a65bcbChristian Maeder InternalChoice p q
e39a1626bee36d6ad13a2c0014a80ef179a65bcbChristian Maeder GeneralisedParallel p es q
e39a1626bee36d6ad13a2c0014a80ef179a65bcbChristian Maeder RelationalRenaming p RENAMING
14a6ec72de5c35d65c2adcd54b6fecbd8bc271b6Christian Maeder NamedProcess pn evs
14a6ec72de5c35d65c2adcd54b6fecbd8bc271b6Christian Maeder ConditionalProcess CSP_FORMULA p q
e39a1626bee36d6ad13a2c0014a80ef179a65bcbChristian Maeder (Also the interrupt operator should be added, and core?)
e39a1626bee36d6ad13a2c0014a80ef179a65bcbChristian Maedermodule CspCASL.Core_CspCASL (basicToCore) where
e39a1626bee36d6ad13a2c0014a80ef179a65bcbChristian MaederbasicToCore :: CspBasicSpec -> CspBasicSpec
14a6ec72de5c35d65c2adcd54b6fecbd8bc271b6Christian MaederbasicToCore c = CspBasicSpec (channels c) (core_procs)
14a6ec72de5c35d65c2adcd54b6fecbd8bc271b6Christian Maeder where core_procs = map procEqToCore (proc_items c)
e39a1626bee36d6ad13a2c0014a80ef179a65bcbChristian Maeder procEqToCore (Proc_Eq pn p) = (Proc_Eq pn (procToCore p))
e39a1626bee36d6ad13a2c0014a80ef179a65bcbChristian Maeder procEqToCore x = x
e39a1626bee36d6ad13a2c0014a80ef179a65bcbChristian MaederprocToCore :: PROCESS -> PROCESS
e39a1626bee36d6ad13a2c0014a80ef179a65bcbChristian MaederprocToCore proc = let p' = procToCore in case proc of
e39a1626bee36d6ad13a2c0014a80ef179a65bcbChristian Maeder -- First the core operators: we just need to recurse.
e39a1626bee36d6ad13a2c0014a80ef179a65bcbChristian Maeder (Skip r) -> (Skip r)
e39a1626bee36d6ad13a2c0014a80ef179a65bcbChristian Maeder (Stop r) -> (Stop r)
e39a1626bee36d6ad13a2c0014a80ef179a65bcbChristian Maeder (PrefixProcess ev p r) -> (PrefixProcess ev (p' p) r)
918c36f05614a959f186fe02bd4f943e0a1d91e3Christian Maeder (ExternalPrefixProcess v es p r) -> (ExternalPrefixProcess v es (p' p) r)
918c36f05614a959f186fe02bd4f943e0a1d91e3Christian Maeder (InternalPrefixProcess v es p r) -> (InternalPrefixProcess v es (p' p) r)
e39a1626bee36d6ad13a2c0014a80ef179a65bcbChristian Maeder (Sequential p q r) -> (Sequential (p' p) (p' q) r)
e39a1626bee36d6ad13a2c0014a80ef179a65bcbChristian Maeder (ExternalChoice p q r) -> (ExternalChoice (p' p) (p' q) r)
e39a1626bee36d6ad13a2c0014a80ef179a65bcbChristian Maeder (InternalChoice p q r) -> (InternalChoice (p' p) (p' q) r)
e39a1626bee36d6ad13a2c0014a80ef179a65bcbChristian Maeder (GeneralisedParallel p es q r) -> (GeneralisedParallel (p' p) es (p' q) r)
e39a1626bee36d6ad13a2c0014a80ef179a65bcbChristian Maeder (Hiding p es r) -> (Hiding (p' p) es r)
e39a1626bee36d6ad13a2c0014a80ef179a65bcbChristian Maeder (RelationalRenaming p rn r) -> (RelationalRenaming (p' p) rn r)
14a6ec72de5c35d65c2adcd54b6fecbd8bc271b6Christian Maeder (NamedProcess pn evs r) -> (NamedProcess pn evs r)
14a6ec72de5c35d65c2adcd54b6fecbd8bc271b6Christian Maeder (ConditionalProcess f p q r) -> (ConditionalProcess f (p' p) (p' q) r)
14a6ec72de5c35d65c2adcd54b6fecbd8bc271b6Christian Maeder -- Non-core, done.
14a6ec72de5c35d65c2adcd54b6fecbd8bc271b6Christian Maeder (Interleaving p q r) -> (GeneralisedParallel (p' p)
14a6ec72de5c35d65c2adcd54b6fecbd8bc271b6Christian Maeder (EventSet [] nullRange) (p' q) r)
14a6ec72de5c35d65c2adcd54b6fecbd8bc271b6Christian Maeder -- Non-core, not done yet.
e39a1626bee36d6ad13a2c0014a80ef179a65bcbChristian Maeder (Div r) -> (Div r)
14a6ec72de5c35d65c2adcd54b6fecbd8bc271b6Christian Maeder (Run es r) -> (Run es r)
14a6ec72de5c35d65c2adcd54b6fecbd8bc271b6Christian Maeder (Chaos es r) -> (Chaos es r)
14a6ec72de5c35d65c2adcd54b6fecbd8bc271b6Christian Maeder (SynchronousParallel p q r) -> (SynchronousParallel (p' p) (p' q) r)
14a6ec72de5c35d65c2adcd54b6fecbd8bc271b6Christian Maeder (AlphabetisedParallel p esp esq q r) ->
14a6ec72de5c35d65c2adcd54b6fecbd8bc271b6Christian Maeder (AlphabetisedParallel (p' p) esp esq (p' q) r)