Parse_CspCASL_Process.hs revision 7996f5f893cc14b5e22fdb7ec90a3474ba3c51ab
4b0a4c7dea0f67a233dcc42ce9bb18d36de109aeChristian Maeder{- |
4b0a4c7dea0f67a233dcc42ce9bb18d36de109aeChristian MaederModule : $Id$
c58a94c44b76b072ace930f2126c889c0b64cb2aChristian MaederDescription : Parser for CspCASL processes
97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian MaederCopyright : (c)
ea03c5d09694b4a966fbd19d46cfa5772648d95fChristian MaederLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
e7ce154edb906685b3fa7f6c0a764e18a4658068Christian Maeder
4b0a4c7dea0f67a233dcc42ce9bb18d36de109aeChristian MaederMaintainer : a.m.gimblett@swan.ac.uk
4b0a4c7dea0f67a233dcc42ce9bb18d36de109aeChristian MaederStability : experimental
4b0a4c7dea0f67a233dcc42ce9bb18d36de109aeChristian MaederPortability :
f3a94a197960e548ecd6520bb768cb0d547457bbChristian Maeder
ea03c5d09694b4a966fbd19d46cfa5772648d95fChristian MaederParser for CSP-CASL processes.
ea03c5d09694b4a966fbd19d46cfa5772648d95fChristian Maeder
e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maeder-}
502ed7ed7fecd10b6d0c83cdd48a244ec45e840aChristian Maeder
e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maedermodule CspCASL.Parse_CspCASL_Process (
0a85c4dc6f4bba88e1994e8f1cd3657b6503b220Christian Maeder channel_name,
0a85c4dc6f4bba88e1994e8f1cd3657b6503b220Christian Maeder comm_type,
ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maeder csp_casl_sort,
dc6b48bb46df8e56da3491c98476e6da0d1d5d1dChristian Maeder csp_casl_process,
ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maeder event_set,
c00adad2e9459b422dee09e3a2bddba66b433bb7Christian Maeder process_name,
9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder var,
fd5d3885a092ac0727fa2436cdfc3b248318ebd8Christian Maeder) where
9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maederimport Text.ParserCombinators.Parsec (sepBy, try, (<|>))
9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder
e7ce154edb906685b3fa7f6c0a764e18a4658068Christian Maederimport CASL.AS_Basic_CASL (SORT, TERM, VAR)
502ed7ed7fecd10b6d0c83cdd48a244ec45e840aChristian Maederimport qualified CASL.Formula
0a85c4dc6f4bba88e1994e8f1cd3657b6503b220Christian Maederimport Common.AnnoState (AParser, asKey)
c00adad2e9459b422dee09e3a2bddba66b433bb7Christian Maederimport Common.Id
9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maederimport Common.Keywords
502ed7ed7fecd10b6d0c83cdd48a244ec45e840aChristian Maederimport Common.Lexer ((<<), commaSep1, commaT, cParenT, oParenT)
9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maederimport Common.Token (parseId, sortId, varId)
e7ce154edb906685b3fa7f6c0a764e18a4658068Christian Maeder
fd5d3885a092ac0727fa2436cdfc3b248318ebd8Christian Maederimport CspCASL.AS_CspCASL_Process
9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maederimport CspCASL.CspCASL_Keywords
5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maeder
5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maedercsp_casl_process :: AParser st PROCESS
e7ce154edb906685b3fa7f6c0a764e18a4658068Christian Maedercsp_casl_process = conditional_process <|> parallel_process
23f8d286586ff38a9e73052b2c7c04c62c5c638fChristian Maeder
9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maederconditional_process :: AParser st PROCESS
5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maederconditional_process = do ift <- asKey ifS
e7ce154edb906685b3fa7f6c0a764e18a4658068Christian Maeder f <- formula
23f8d286586ff38a9e73052b2c7c04c62c5c638fChristian Maeder asKey thenS
9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder p <- csp_casl_process
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder asKey elseS
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder q <- csp_casl_process
9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder return (ConditionalProcess f p q
e1839fb37a3a2ccd457464cb0dcc5efd466dbe22Christian Maeder ((getRange ift) `appRange` (getRange q)))
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder
e1839fb37a3a2ccd457464cb0dcc5efd466dbe22Christian Maederparallel_process :: AParser st PROCESS
9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maederparallel_process = do cp <- choice_process
cf3232cec840a6945667bdb06f5b47b22243bc8fChristian Maeder p <- parallel_process' cp
836e72a3c413366ba9801726f3b249c7791cb9caChristian Maeder return p
0f894093b1d435fd222074706d7fdadb9725cfdfChristian Maeder
e1839fb37a3a2ccd457464cb0dcc5efd466dbe22Christian Maederparallel_process' :: PROCESS -> AParser st PROCESS
e7ce154edb906685b3fa7f6c0a764e18a4658068Christian Maederparallel_process' lp =
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder do asKey interleavingS
cf3232cec840a6945667bdb06f5b47b22243bc8fChristian Maeder rp <- choice_process
9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder p <- parallel_process' (Interleaving lp rp
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder ((getRange lp) `appRange` (getRange rp)))
e7ce154edb906685b3fa7f6c0a764e18a4658068Christian Maeder return p
e7ce154edb906685b3fa7f6c0a764e18a4658068Christian Maeder <|> do asKey synchronousS
e7ce154edb906685b3fa7f6c0a764e18a4658068Christian Maeder rp <- choice_process
e7ce154edb906685b3fa7f6c0a764e18a4658068Christian Maeder p <- parallel_process' (SynchronousParallel lp rp
e8a2ca3a7b3e9a19ef03b6b1c0b5d03dbad6463cChristian Maeder ((getRange lp) `appRange` (getRange rp)))
9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder return p
9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder <|> do asKey genpar_openS
9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder es <- event_set
1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian Maeder asKey genpar_closeS
003a6b38b11909af0e6d0575cca4c1fcfc9ffd24Christian Maeder rp <- choice_process
1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian Maeder p <- parallel_process' (GeneralisedParallel lp es rp
9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder ((getRange lp) `appRange` (getRange rp)))
9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder return p
9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder <|> do asKey alpar_openS
9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder les <- event_set
9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder asKey alpar_sepS
9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder res <- event_set
9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder asKey alpar_closeS
9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder rp <- choice_process
9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder p <- parallel_process' (AlphabetisedParallel lp les res rp
9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder ((getRange lp) `appRange` (getRange rp)))
9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder return p
9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder <|> return lp
9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder
9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maederchoice_process :: AParser st PROCESS
9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maederchoice_process = do sp <- sequence_process
9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder p <- choice_process' sp
9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder return p
9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder
9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maederchoice_process' :: PROCESS -> AParser st PROCESS
9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maederchoice_process' lp =
9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder do asKey external_choiceS
9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder rp <- sequence_process
9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder p <- choice_process' (ExternalChoice lp rp
9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder ((getRange lp) `appRange` (getRange rp)))
9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder return p
9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder <|> do asKey internal_choiceS
9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder rp <- sequence_process
9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder p <- choice_process' (InternalChoice lp rp
9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder ((getRange lp) `appRange` (getRange rp)))
9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder return p
e7ce154edb906685b3fa7f6c0a764e18a4658068Christian Maeder <|> return lp
e1839fb37a3a2ccd457464cb0dcc5efd466dbe22Christian Maeder
e7ce154edb906685b3fa7f6c0a764e18a4658068Christian Maedersequence_process :: AParser st PROCESS
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maedersequence_process = do pp <- prefix_process
cf3232cec840a6945667bdb06f5b47b22243bc8fChristian Maeder p <- sequence_process' pp
9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder return p
502ed7ed7fecd10b6d0c83cdd48a244ec45e840aChristian Maeder
9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maedersequence_process' :: PROCESS -> AParser st PROCESS
9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maedersequence_process' lp =
7c57322afb6342e5cc8b1fdc96050b707407fc61Christian Maeder do asKey sequentialS
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder rp <- prefix_process
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder p <- sequence_process' (Sequential lp rp
9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder ((getRange lp) `appRange` (getRange rp)))
9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder return p
fd5d3885a092ac0727fa2436cdfc3b248318ebd8Christian Maeder <|> return lp
9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder
628310b42327ad76ce471caf0dde6563d6fa6307Christian Maederprefix_process :: AParser st PROCESS
9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maederprefix_process =
31242f7541fd6ef179e4eb5be7522ddf54ae397bChristian Maeder do ipk <- asKey internal_choiceS
e7ce154edb906685b3fa7f6c0a764e18a4658068Christian Maeder v <- var
e7ce154edb906685b3fa7f6c0a764e18a4658068Christian Maeder asKey svar_sortS
31242f7541fd6ef179e4eb5be7522ddf54ae397bChristian Maeder s <- csp_casl_sort
9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder asKey prefix_procS
76fa667489c5e0868ac68de9f0253ac10f73d0b5Christian Maeder p <- prefix_process
e7ce154edb906685b3fa7f6c0a764e18a4658068Christian Maeder return (InternalPrefixProcess v s p
e7ce154edb906685b3fa7f6c0a764e18a4658068Christian Maeder ((getRange ipk) `appRange` (getRange p)))
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder <|> do epk <- asKey external_choiceS
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder v <- var
628310b42327ad76ce471caf0dde6563d6fa6307Christian Maeder asKey svar_sortS
9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder s <- csp_casl_sort
9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder asKey prefix_procS
9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder p <- prefix_process
9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder return (ExternalPrefixProcess v s p
9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder ((getRange epk) `appRange` (getRange p)))
628310b42327ad76ce471caf0dde6563d6fa6307Christian Maeder <|> do e <- try (event << asKey prefix_procS)
9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder p <- prefix_process
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder return (PrefixProcess e p
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder ((getRange e) `appRange` (getRange p)))
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder <|> hiding_renaming_process
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maederhiding_renaming_process :: AParser st PROCESS
9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maederhiding_renaming_process = do pl <- parenthesised_or_primitive_process
cbbb99ab370e6ad265b14a37e7d35b7f08a50d43Christian Maeder p <- (hiding_renaming' pl)
ffd01020a4f35f434b912844ad6e0d6918fadffdChristian Maeder return p
0a85c4dc6f4bba88e1994e8f1cd3657b6503b220Christian Maeder
fd5d3885a092ac0727fa2436cdfc3b248318ebd8Christian Maederhiding_renaming' :: PROCESS -> AParser st PROCESS
9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maederhiding_renaming' lp =
502ed7ed7fecd10b6d0c83cdd48a244ec45e840aChristian Maeder do asKey hiding_procS
9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder es <- event_set
c9892acbf03a509d874ac6d79b9a2cb09042e0dcChristian Maeder p <- (hiding_renaming' (Hiding lp es
c9892acbf03a509d874ac6d79b9a2cb09042e0dcChristian Maeder ((getRange lp) `appRange` (getRange es))))
9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder return p
7c57322afb6342e5cc8b1fdc96050b707407fc61Christian Maeder <|> do asKey ren_proc_openS
ac07a6558423dae7adc488ed9092cd8e9450a29dChristian Maeder rn <- renaming
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder ck <- asKey ren_proc_closeS
e7ce154edb906685b3fa7f6c0a764e18a4658068Christian Maeder p <- (hiding_renaming' (RelationalRenaming lp rn
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder ((getRange lp) `appRange` (getRange ck))))
e7ce154edb906685b3fa7f6c0a764e18a4658068Christian Maeder return p
e7ce154edb906685b3fa7f6c0a764e18a4658068Christian Maeder <|> return lp
e7ce154edb906685b3fa7f6c0a764e18a4658068Christian Maeder
154d4152b38c55c3c4ab8f35578669a65fc04df9Christian Maederparenthesised_or_primitive_process :: AParser st PROCESS
e7ce154edb906685b3fa7f6c0a764e18a4658068Christian Maederparenthesised_or_primitive_process =
b49276c9f50038e0bd499ad49f7bd6444566a834Christian Maeder do try oParenT
9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder p <- csp_casl_process
c00adad2e9459b422dee09e3a2bddba66b433bb7Christian Maeder cParenT
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder return p
e7ce154edb906685b3fa7f6c0a764e18a4658068Christian Maeder <|> do rk <- asKey runS
c00adad2e9459b422dee09e3a2bddba66b433bb7Christian Maeder oParenT
9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder es <- event_set
ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maeder cp <- cParenT
9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder return (Run es ((getRange rk) `appRange` (getRange cp)))
ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maeder <|> do ck <- asKey chaosS
e7ce154edb906685b3fa7f6c0a764e18a4658068Christian Maeder oParenT
e7ce154edb906685b3fa7f6c0a764e18a4658068Christian Maeder es <- event_set
e7ce154edb906685b3fa7f6c0a764e18a4658068Christian Maeder cp <- cParenT
ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maeder return (Chaos es ((getRange ck) `appRange` (getRange cp)))
9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder <|> do dk <- asKey divS
ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maeder return (Div (getRange dk))
e7ce154edb906685b3fa7f6c0a764e18a4658068Christian Maeder <|> do sk <- asKey stopS
ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maeder return (Stop (getRange sk))
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder <|> do sk <- asKey skipS
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder return (Skip (getRange sk))
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder <|> do n <- (try process_name)
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder args <- procArgs
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder return (NamedProcess n args
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder ((getRange n) `appRange` (getRange args)))
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder
ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maederprocess_name :: AParser st PROCESS_NAME
ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maederprocess_name = varId csp_casl_keywords
ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maeder
ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maederchannel_name :: AParser st CHANNEL_NAME
ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maederchannel_name = varId csp_casl_keywords
ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maeder
ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maedercomm_type :: AParser st COMM_TYPE
ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maedercomm_type = varId csp_casl_keywords
ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maeder
ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maeder
ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maeder-- List of arguments to a named process
ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian MaederprocArgs :: AParser st [(TERM ())]
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian MaederprocArgs = do try oParenT
ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maeder es <- commaSep1 (CASL.Formula.term csp_casl_keywords)
e7ce154edb906685b3fa7f6c0a764e18a4658068Christian Maeder cParenT
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder return es
e7ce154edb906685b3fa7f6c0a764e18a4658068Christian Maeder <|> return []
ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maeder
ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maeder-- Sort IDs, excluding CspCasl keywords
ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maedercsp_casl_sort :: AParser st SORT
ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maedercsp_casl_sort = sortId csp_casl_keywords
ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maeder
ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maederevent_set :: AParser st EVENT_SET
ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maederevent_set = do cts <- comm_type `sepBy` commaT
ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maeder return (EventSet cts (getRange cts))
ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maeder
ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maeder-- Events may be simple CASL terms or channel send/receives.
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder
ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maederevent :: AParser st EVENT
ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maederevent = try chan_recv <|> try chan_nondet_send <|> try chan_send <|> term_event
ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maeder
ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maederchan_send :: AParser st EVENT
ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maederchan_send = do
ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maeder cn <- channel_name
ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maeder asKey chan_sendS
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder t <- CASL.Formula.term csp_casl_keywords
ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maeder return (ChanSend cn t (getRange cn))
ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maeder
ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maederchan_nondet_send :: AParser st EVENT
ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maederchan_nondet_send = do
e7ce154edb906685b3fa7f6c0a764e18a4658068Christian Maeder cn <- channel_name
e7ce154edb906685b3fa7f6c0a764e18a4658068Christian Maeder asKey chan_sendS
e7ce154edb906685b3fa7f6c0a764e18a4658068Christian Maeder v <- var
e7ce154edb906685b3fa7f6c0a764e18a4658068Christian Maeder asKey svar_sortS
s <- csp_casl_sort
return (ChanNonDetSend cn v s ((getRange cn) `appRange` (getRange s)))
chan_recv :: AParser st EVENT
chan_recv = do
cn <- channel_name
asKey chan_receiveS
v <- var
asKey svar_sortS
s <- csp_casl_sort
return (ChanRecv cn v s ((getRange cn) `appRange` (getRange s)))
term_event :: AParser st EVENT
term_event = do
t <- CASL.Formula.term csp_casl_keywords
return (TermEvent t (getRange t))
-- Formulas are CASL formulas. We make our own wrapper around them
-- however.
formula :: AParser st CSP_FORMULA
formula = do f <- CASL.Formula.formula csp_casl_keywords
return (Formula f (getRange f))
-- Primitive renaming is done using an operator name or a predicate
-- name. They're both Ids. Separation between operator or predicate
-- (or some other non-applicable Id) must be a static analysis
-- problem.
renaming :: AParser st RENAMING
renaming = (parseId csp_casl_keywords) `sepBy` commaT
-- Variables come from CASL/Hets.
var :: AParser st VAR
var = varId csp_casl_keywords