Parse_CspCASL.hs revision 9f93b2a8b552789cd939d599504d39732672dc84
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian MaederDescription : Parser for CspCASL specifications
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian MaederCopyright : (c) Uni Bremen 2007
97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian MaederLicense : GPLv2 or higher, see LICENSE.txt
3f69b6948966979163bdfe8331c38833d5d90ecdChristian MaederMaintainer : a.m.gimblett@swan.ac.uk
ca010363454de207082dfaa4b753531ce2a34551Christian MaederStability : experimental
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian MaederPortability : portable
79d11c2e3ad242ebb241f5d4a5e98a674c0b986fChristian MaederParser for CSP-CASL specifications.
ac142c1b088711f911018d8108a64be80b2f2a58Christian Maederimport Common.AS_Annotation (Annoted (..), emptyAnno)
ac142c1b088711f911018d8108a64be80b2f2a58Christian Maederimport Common.AnnoState (AParser, asKey, colonT, equalT, anSemi, allAnnoParser)
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian MaedercspBasicSpec :: AParser st CspBasicSpec
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian MaedercspBasicSpec = do
c438c79d00fc438f99627e612498744bdc0d0c89Christian Maeder chans <- option [] chanDecls
23f8d286586ff38a9e73052b2c7c04c62c5c638fChristian Maeder items <- processItems
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder return (CspBasicSpec chans items)
e68f45f355ed9d4026ee9baff5aa75aa7c911cc2Christian MaederchanDecls :: AParser st [CHANNEL_DECL]
ad270004874ce1d0697fb30d7309f180553bb315Christian MaederchanDecls = do
fc8c6570c7b4ee13f375eb607bed2290438573bfChristian Maeder pluralKeyword channelS
83cc27e4ca7cf1a4bb5f4a8df17d3e6d44e6f1eaChristian Maeder chanDecl `sepBy` anSemi
028f19cdb09d52bb2fd207399b6fa874540d1670Christian MaederchanDecl :: AParser st CHANNEL_DECL
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder vs <- commaSep1 channel_name
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder es <- csp_casl_sort
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder return (ChannelDecl vs es)
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian MaederprocessItems :: AParser st [Annoted PROC_ITEM]
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian MaederprocessItems = do
fc8c6570c7b4ee13f375eb607bed2290438573bfChristian Maeder asKey processS
83cc27e4ca7cf1a4bb5f4a8df17d3e6d44e6f1eaChristian Maeder procItems <|> fmap singleProcess csp_casl_process
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder{- Turn an unnamed singleton process into a declaration/equation. THIS WHOLE
53301de22afd7190981b363b57c48df86fcb50f7Christian Maederfunctions seems odd. Why would we want a fixed process "P" which communicates
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maederover sort "singletonProcessSort". BUG? -}
53301de22afd7190981b363b57c48df86fcb50f7Christian MaedersingleProcess :: PROCESS -> [Annoted PROC_ITEM]
53301de22afd7190981b363b57c48df86fcb50f7Christian MaedersingleProcess p =
da2b959c50c95309d8eb8b24174249c2847e74b5Christian Maeder map emptyAnno [Proc_Decl singletonProcessName [] singletonProcessAlpha,
da2b959c50c95309d8eb8b24174249c2847e74b5Christian Maeder Proc_Eq (ParmProcname (PROCESS_NAME singletonProcessName) []) p]
962036a37b92afb04ac0725cde9f20e599c04c5fChristian Maeder where singletonProcessName = mkSimpleId "P"
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder singletonProcessAlpha =
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder ProcAlphabet [mkSimpleId "singletonProcessSort"]
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian MaederprocItems :: AParser st [Annoted PROC_ITEM]
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian MaederprocItems = many1 procItem
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian MaederprocItem :: AParser st (Annoted PROC_ITEM)
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian MaederprocItem = try procDecl <|> procEq
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian MaederprocDecl :: AParser st (Annoted PROC_ITEM)
962036a37b92afb04ac0725cde9f20e599c04c5fChristian Maeder (pn, parms, comms) <- procNameWithParamsAndComms
962036a37b92afb04ac0725cde9f20e599c04c5fChristian Maeder -- We don't currently allow annotations on declarations
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder return (emptyAnno $ Proc_Decl pn parms comms)
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian MaederprocEq :: AParser st (Annoted PROC_ITEM)
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian MaederprocEq = allAnnoParser $ do
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder pn <- parmProcname
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder p <- csp_casl_process
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder return (Proc_Eq pn p)
1eb10c0c30323eed3cc21082fd242cd09a612dc5Christian MaederparmProcname :: AParser st PARM_PROCNAME
1eb10c0c30323eed3cc21082fd242cd09a612dc5Christian MaederparmProcname = do
1eb10c0c30323eed3cc21082fd242cd09a612dc5Christian Maeder pn <- process_name
1eb10c0c30323eed3cc21082fd242cd09a612dc5Christian Maeder pv <- option [] $ do
1eb10c0c30323eed3cc21082fd242cd09a612dc5Christian Maeder vs <- commaSep1 var
1eb10c0c30323eed3cc21082fd242cd09a612dc5Christian Maeder return (ParmProcname pn pv)