Parse_CspCASL.hs revision a181b88611e09ffc9701a5f1022002cc0bc0c584
7abd0c58a5ce51db13f93de82407b2188d55d298Christian MaederDescription : Parser for CspCASL specifications
75a6279dbae159d018ef812185416cf6df386c10Till MossakowskiCopyright : (c) Uni Bremen 2007
c00adad2e9459b422dee09e3a2bddba66b433bb7Christian MaederLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
7abd0c58a5ce51db13f93de82407b2188d55d298Christian MaederMaintainer : a.m.gimblett@swan.ac.uk
7abd0c58a5ce51db13f93de82407b2188d55d298Christian MaederStability : experimental
7abd0c58a5ce51db13f93de82407b2188d55d298Christian MaederPortability : portable
c00adad2e9459b422dee09e3a2bddba66b433bb7Christian MaederParser for CSP-CASL specifications.
8197d0be8b81692f311ad5ca34e125e2cf9eecb8Christian Maederimport Text.ParserCombinators.Parsec (choice, many1, try, (<|>),
f71a8dcf94fd9eb3c9800e16dcdc5e5ff74e5c22Christian Maeder option, sepBy)
8197d0be8b81692f311ad5ca34e125e2cf9eecb8Christian Maederimport Common.AnnoState (AParser, asKey, colonT, equalT, anSemi)
c18e9c3c6d5039618f1f2c05526ece84c7794ea3Christian Maederimport Common.Lexer (commaSep1, commaT, cParenT, oParenT)
c1124c6303c288db3fcb40518d38169cd7baaa4cChristian MaedercspBasicSpec :: AParser st CspBasicSpec
c18e9c3c6d5039618f1f2c05526ece84c7794ea3Christian MaedercspBasicSpec = do
c1124c6303c288db3fcb40518d38169cd7baaa4cChristian Maeder chans <- option [] $ do
c1124c6303c288db3fcb40518d38169cd7baaa4cChristian Maeder choice [asKey channelS, asKey channelsS]
64f7c2188d578b920d8e5513a423449af633e9bcChristian Maeder cds <- chanDecl `sepBy` anSemi
64f7c2188d578b920d8e5513a423449af633e9bcChristian Maeder -- XXX how to have an _optional_ final semicolon here?
64f7c2188d578b920d8e5513a423449af633e9bcChristian Maeder items <- processItems
c1124c6303c288db3fcb40518d38169cd7baaa4cChristian Maeder return (CspBasicSpec chans items)
0f67ca7b0c738a28f6688ba6e96d44d7c14af611Christian MaederchanDecl :: AParser st CHANNEL_DECL
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian MaederchanDecl = do vs <- commaSep1 channel_name
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder es <- csp_casl_sort
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder return (ChannelDecl vs es)
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian MaederprocessItems :: AParser st [PROC_ITEM]
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian MaederprocessItems = do asKey processS
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder procItems <|> fmap singleProcess csp_casl_process
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder-- Turn an unnamed singleton process into a declaration/equation.
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian MaedersingleProcess :: PROCESS -> [PROC_ITEM]
c1124c6303c288db3fcb40518d38169cd7baaa4cChristian MaedersingleProcess p =
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder [Proc_Decl singletonProcessName [] singletonProcessAlpha,
bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maeder Proc_Eq (ParmProcname singletonProcessName []) p]
e289294500ad68fa0706b09521af340bbb356a69Christian Maeder where singletonProcessName = mkSimpleId "P"
e289294500ad68fa0706b09521af340bbb356a69Christian Maeder singletonProcessAlpha =
c1124c6303c288db3fcb40518d38169cd7baaa4cChristian Maeder (ProcAlphabet [mkSimpleId "singletonProcessSort"]
c1124c6303c288db3fcb40518d38169cd7baaa4cChristian MaederprocItems :: AParser st [PROC_ITEM]
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian MaederprocItems = many1 procItem
c1124c6303c288db3fcb40518d38169cd7baaa4cChristian MaederprocItem :: AParser st PROC_ITEM
c1124c6303c288db3fcb40518d38169cd7baaa4cChristian MaederprocItem = try (do pdcl <- procDecl
c1124c6303c288db3fcb40518d38169cd7baaa4cChristian Maeder <|> (do peq <- procEq
c1124c6303c288db3fcb40518d38169cd7baaa4cChristian MaederprocDecl :: AParser st PROC_ITEM
c1124c6303c288db3fcb40518d38169cd7baaa4cChristian Maeder pn <- process_name
c1124c6303c288db3fcb40518d38169cd7baaa4cChristian Maeder parms <- option [] $ do
c1124c6303c288db3fcb40518d38169cd7baaa4cChristian Maeder parms <- commaSep1 csp_casl_sort
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder cts <- (comm_type `sepBy` commaT)
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder return (Proc_Decl pn parms (ProcAlphabet cts (getRange cts)))
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian MaederprocEq :: AParser st PROC_ITEM
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder pn <- parmProcname
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder p <- csp_casl_process
c1124c6303c288db3fcb40518d38169cd7baaa4cChristian Maeder return (Proc_Eq pn p)
c1124c6303c288db3fcb40518d38169cd7baaa4cChristian MaederparmProcname :: AParser st PARM_PROCNAME
c1124c6303c288db3fcb40518d38169cd7baaa4cChristian MaederparmProcname = do
c1124c6303c288db3fcb40518d38169cd7baaa4cChristian Maeder pn <- process_name
c1124c6303c288db3fcb40518d38169cd7baaa4cChristian Maeder pv <- option [] $ do
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder vs <- commaSep1 var
c1124c6303c288db3fcb40518d38169cd7baaa4cChristian Maeder return (ParmProcname pn pv)