{- |
Module      :  ./CspCASL/Parse_CspCASL_Process.hs
Description :  Parser for CspCASL processes
Copyright   :  (c)
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  a.m.gimblett@swan.ac.uk
Stability   :  experimental
Portability :  portable

Parser for CSP-CASL processes.

-}

module CspCASL.Parse_CspCASL_Process
  ( channel_name
  , parens
  , parenList
  , cspStartKeys
  , cspSortId
  , parseCspId
  , csp_casl_process
  , event_set
  , process_name
  , var
  , commType
  , bracedList
  , procDeclOrDefn
  ) where

import Text.ParserCombinators.Parsec

import CASL.AS_Basic_CASL
import qualified CASL.Formula as CASL

import Common.AnnoState
import Common.Id
import Common.Keywords
import Common.Lexer hiding (parens)
import Common.Parsec
import Common.Token (parseId, sortId, varId)
import qualified Control.Monad.Fail as Fail

import CspCASL.AS_CspCASL_Process
import CspCASL.CspCASL_Keywords

import qualified Data.Set as Set

csp_casl_process :: AParser st PROCESS
csp_casl_process :: AParser st PROCESS
csp_casl_process = AParser st PROCESS
forall st. AParser st PROCESS
par_proc

cond_proc :: AParser st PROCESS
cond_proc :: AParser st PROCESS
cond_proc = do
    Token
ift <- String -> AParser st Token
forall st. String -> AParser st Token
asKey String
ifS
    FORMULA ()
f <- AParser st (FORMULA ())
forall st. AParser st (FORMULA ())
formula
    String -> AParser st Token
forall st. String -> AParser st Token
asKey String
thenS
    PROCESS
p <- AParser st PROCESS
forall st. AParser st PROCESS
csp_casl_process
    String -> AParser st Token
forall st. String -> AParser st Token
asKey String
elseS
    PROCESS
q <- AParser st PROCESS
forall st. AParser st PROCESS
csp_casl_process
    PROCESS -> AParser st PROCESS
forall (m :: * -> *) a. Monad m => a -> m a
return (PROCESS -> AParser st PROCESS) -> PROCESS -> AParser st PROCESS
forall a b. (a -> b) -> a -> b
$ FORMULA () -> PROCESS -> PROCESS -> Range -> PROCESS
ConditionalProcess FORMULA ()
f PROCESS
p PROCESS
q (Range -> PROCESS) -> Range -> PROCESS
forall a b. (a -> b) -> a -> b
$ Token -> PROCESS -> Range
forall a b. (GetRange a, GetRange b) => a -> b -> Range
compRange Token
ift PROCESS
q

par_proc :: AParser st PROCESS
par_proc :: AParser st PROCESS
par_proc = AParser st PROCESS
forall st. AParser st PROCESS
choice_proc AParser st PROCESS
-> (PROCESS -> AParser st PROCESS) -> AParser st PROCESS
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= PROCESS -> AParser st PROCESS
forall st. PROCESS -> AParser st PROCESS
par_proc'

asKeySign :: String -> AParser st Token
asKeySign :: String -> AParser st Token
asKeySign s :: String
s =
  AParser st Token -> AParser st Token
forall st a. AParser st a -> AParser st a
wrapAnnos (AParser st Token -> AParser st Token)
-> (CharParser (AnnoState st) String -> AParser st Token)
-> CharParser (AnnoState st) String
-> AParser st Token
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CharParser (AnnoState st) String -> AParser st Token
forall st. CharParser st String -> CharParser st Token
pToken (CharParser (AnnoState st) String -> AParser st Token)
-> CharParser (AnnoState st) String -> AParser st Token
forall a b. (a -> b) -> a -> b
$ String -> CharParser (AnnoState st) String
forall st. String -> CharParser st String
tryString String
s
    CharParser (AnnoState st) String
-> ParsecT String (AnnoState st) Identity ()
-> CharParser (AnnoState st) String
forall (m :: * -> *) a b. Monad m => m a -> m b -> m a
<< ParsecT String (AnnoState st) Identity Char
-> ParsecT String (AnnoState st) Identity ()
forall s (m :: * -> *) t a u.
(Stream s m t, Show a) =>
ParsecT s u m a -> ParsecT s u m ()
notFollowedBy ((Char -> Bool) -> ParsecT String (AnnoState st) Identity Char
forall s (m :: * -> *) u.
Stream s m Char =>
(Char -> Bool) -> ParsecT s u m Char
satisfy ((Char -> Bool) -> ParsecT String (AnnoState st) Identity Char)
-> (Char -> Bool) -> ParsecT String (AnnoState st) Identity Char
forall a b. (a -> b) -> a -> b
$ \ c :: Char
c -> Char -> String -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem Char
c "[]" Bool -> Bool -> Bool
|| Char -> Bool
isSignChar Char
c)

par_proc' :: PROCESS -> AParser st PROCESS
par_proc' :: PROCESS -> AParser st PROCESS
par_proc' lp :: PROCESS
lp = do
    String -> AParser st Token
forall st. String -> AParser st Token
asKeySign String
interleavingS
    PROCESS
rp <- AParser st PROCESS
forall st. AParser st PROCESS
choice_proc
    PROCESS -> AParser st PROCESS
forall st. PROCESS -> AParser st PROCESS
par_proc' (PROCESS -> PROCESS -> Range -> PROCESS
Interleaving PROCESS
lp PROCESS
rp (PROCESS -> PROCESS -> Range
forall a b. (GetRange a, GetRange b) => a -> b -> Range
compRange PROCESS
lp PROCESS
rp))
  AParser st PROCESS -> AParser st PROCESS -> AParser st PROCESS
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> do
    String -> AParser st Token
forall st. String -> AParser st Token
asKeySign String
synchronousS
    PROCESS
rp <- AParser st PROCESS
forall st. AParser st PROCESS
choice_proc
    PROCESS -> AParser st PROCESS
forall st. PROCESS -> AParser st PROCESS
par_proc' (PROCESS -> PROCESS -> Range -> PROCESS
SynchronousParallel PROCESS
lp PROCESS
rp (PROCESS -> PROCESS -> Range
forall a b. (GetRange a, GetRange b) => a -> b -> Range
compRange PROCESS
lp PROCESS
rp))
  AParser st PROCESS -> AParser st PROCESS -> AParser st PROCESS
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> do
    Token
k <- String -> AParser st Token
forall st. String -> AParser st Token
asKeySign String
genpar_openS AParser st Token -> AParser st Token -> AParser st Token
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> String -> AParser st Token
forall st. String -> AParser st Token
asKeySign "|[" AParser st Token -> AParser st Token -> AParser st Token
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> String -> AParser st Token
forall st. String -> AParser st Token
asKeySign String
alpar_openS
    EVENT_SET
es <- AParser st EVENT_SET
forall st. AParser st EVENT_SET
event_set
    Maybe EVENT_SET
mes <- (if Token -> String
tokStr Token
k String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
alpar_openS then (EVENT_SET -> Maybe EVENT_SET)
-> AParser st EVENT_SET
-> ParsecT String (AnnoState st) Identity (Maybe EVENT_SET)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap EVENT_SET -> Maybe EVENT_SET
forall a. a -> Maybe a
Just else AParser st EVENT_SET
-> ParsecT String (AnnoState st) Identity (Maybe EVENT_SET)
forall s (m :: * -> *) t u a.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m (Maybe a)
optionMaybe)
      (AParser st EVENT_SET
 -> ParsecT String (AnnoState st) Identity (Maybe EVENT_SET))
-> AParser st EVENT_SET
-> ParsecT String (AnnoState st) Identity (Maybe EVENT_SET)
forall a b. (a -> b) -> a -> b
$ (String -> AParser st Token
forall st. String -> AParser st Token
asKeySign String
alpar_sepS AParser st Token -> AParser st Token -> AParser st Token
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> String -> AParser st Token
forall st. String -> AParser st Token
asKeySign String
barS)
      AParser st Token -> AParser st EVENT_SET -> AParser st EVENT_SET
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> AParser st EVENT_SET
forall st. AParser st EVENT_SET
event_set
    String -> AParser st Token
forall st. String -> AParser st Token
asKeySign String
genpar_closeS AParser st Token -> AParser st Token -> AParser st Token
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> String -> AParser st Token
forall st. String -> AParser st Token
asKeySign "]|" AParser st Token -> AParser st Token -> AParser st Token
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> String -> AParser st Token
forall st. String -> AParser st Token
asKeySign String
alpar_closeS
    PROCESS
rp <- AParser st PROCESS
forall st. AParser st PROCESS
choice_proc
    PROCESS -> AParser st PROCESS
forall st. PROCESS -> AParser st PROCESS
par_proc' (PROCESS -> AParser st PROCESS) -> PROCESS -> AParser st PROCESS
forall a b. (a -> b) -> a -> b
$ (case Maybe EVENT_SET
mes of
        Nothing -> PROCESS -> EVENT_SET -> PROCESS -> Range -> PROCESS
GeneralisedParallel PROCESS
lp EVENT_SET
es
        Just res :: EVENT_SET
res -> PROCESS -> EVENT_SET -> EVENT_SET -> PROCESS -> Range -> PROCESS
AlphabetisedParallel PROCESS
lp EVENT_SET
es EVENT_SET
res) PROCESS
rp (Range -> PROCESS) -> Range -> PROCESS
forall a b. (a -> b) -> a -> b
$ PROCESS -> PROCESS -> Range
forall a b. (GetRange a, GetRange b) => a -> b -> Range
compRange PROCESS
lp PROCESS
rp
  AParser st PROCESS -> AParser st PROCESS -> AParser st PROCESS
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> PROCESS -> AParser st PROCESS
forall (m :: * -> *) a. Monad m => a -> m a
return PROCESS
lp

choice_proc :: AParser st PROCESS
choice_proc :: AParser st PROCESS
choice_proc = AParser st PROCESS
forall st. AParser st PROCESS
seq_proc AParser st PROCESS
-> (PROCESS -> AParser st PROCESS) -> AParser st PROCESS
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= PROCESS -> AParser st PROCESS
forall st. PROCESS -> AParser st PROCESS
choice_proc'

choice_proc' :: PROCESS -> AParser st PROCESS
choice_proc' :: PROCESS -> AParser st PROCESS
choice_proc' lp :: PROCESS
lp = do
    String -> AParser st Token
forall st. String -> AParser st Token
asKeySign String
external_choiceS
    PROCESS
rp <- AParser st PROCESS
forall st. AParser st PROCESS
seq_proc
    PROCESS -> AParser st PROCESS
forall st. PROCESS -> AParser st PROCESS
choice_proc' (PROCESS -> PROCESS -> Range -> PROCESS
ExternalChoice PROCESS
lp PROCESS
rp (PROCESS -> PROCESS -> Range
forall a b. (GetRange a, GetRange b) => a -> b -> Range
compRange PROCESS
lp PROCESS
rp))
  AParser st PROCESS -> AParser st PROCESS -> AParser st PROCESS
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> do
    String -> AParser st Token
forall st. String -> AParser st Token
asKeySign String
internal_choiceS
    PROCESS
rp <- AParser st PROCESS
forall st. AParser st PROCESS
seq_proc
    PROCESS -> AParser st PROCESS
forall st. PROCESS -> AParser st PROCESS
choice_proc' (PROCESS -> PROCESS -> Range -> PROCESS
InternalChoice PROCESS
lp PROCESS
rp (PROCESS -> PROCESS -> Range
forall a b. (GetRange a, GetRange b) => a -> b -> Range
compRange PROCESS
lp PROCESS
rp))
  AParser st PROCESS -> AParser st PROCESS -> AParser st PROCESS
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> PROCESS -> AParser st PROCESS
forall (m :: * -> *) a. Monad m => a -> m a
return PROCESS
lp

seq_proc :: AParser st PROCESS
seq_proc :: AParser st PROCESS
seq_proc = AParser st PROCESS
forall st. AParser st PROCESS
pref_proc AParser st PROCESS
-> (PROCESS -> AParser st PROCESS) -> AParser st PROCESS
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= PROCESS -> AParser st PROCESS
forall st. PROCESS -> AParser st PROCESS
seq_proc'

cspStartKeys :: [String]
cspStartKeys :: [String]
cspStartKeys = [String]
startCspKeywords [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String]
startKeyword

seqSym :: AParser st Token
seqSym :: AParser st Token
seqSym = String -> AParser st Token
forall st. String -> AParser st Token
asKeySign String
sequentialS AParser st Token
-> GenParser Char (AnnoState st) () -> AParser st Token
forall tok st a b.
GenParser tok st a -> GenParser tok st b -> GenParser tok st a
`notFollowedWith`
  (ParsecT
  String
  (AnnoState st)
  Identity
  (Either
     (FQ_PROCESS_NAME, [Token])
     (PROCESS_NAME, Either [PROCESS_NAME] [VAR_DECL], PROC_ALPHABET))
-> GenParser Char (AnnoState st) ()
forall (m :: * -> *) a. Monad m => m a -> m ()
forget ParsecT
  String
  (AnnoState st)
  Identity
  (Either
     (FQ_PROCESS_NAME, [Token])
     (PROCESS_NAME, Either [PROCESS_NAME] [VAR_DECL], PROC_ALPHABET))
forall st.
AParser
  st
  (Either
     (FQ_PROCESS_NAME, [Token])
     (PROCESS_NAME, Either [PROCESS_NAME] [VAR_DECL], PROC_ALPHABET))
procDeclOrDefn GenParser Char (AnnoState st) ()
-> GenParser Char (AnnoState st) ()
-> GenParser Char (AnnoState st) ()
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> [GenParser Char (AnnoState st) ()]
-> GenParser Char (AnnoState st) ()
forall s (m :: * -> *) t u a.
Stream s m t =>
[ParsecT s u m a] -> ParsecT s u m a
choice ((String -> GenParser Char (AnnoState st) ())
-> [String] -> [GenParser Char (AnnoState st) ()]
forall a b. (a -> b) -> [a] -> [b]
map (AParser st Token -> GenParser Char (AnnoState st) ()
forall (m :: * -> *) a. Monad m => m a -> m ()
forget (AParser st Token -> GenParser Char (AnnoState st) ())
-> (String -> AParser st Token)
-> String
-> GenParser Char (AnnoState st) ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> AParser st Token
forall st. String -> AParser st Token
asKey) [String]
cspStartKeys))

seq_proc' :: PROCESS -> AParser st PROCESS
seq_proc' :: PROCESS -> AParser st PROCESS
seq_proc' lp :: PROCESS
lp = do
    String -> AParser st Token
forall st. String -> AParser st Token
asKeySign String
doubleSemis AParser st Token -> AParser st Token -> AParser st Token
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> AParser st Token
forall st. AParser st Token
seqSym
    PROCESS
rp <- AParser st PROCESS
forall st. AParser st PROCESS
pref_proc
    PROCESS -> AParser st PROCESS
forall st. PROCESS -> AParser st PROCESS
seq_proc' (PROCESS -> PROCESS -> Range -> PROCESS
Sequential PROCESS
lp PROCESS
rp (PROCESS -> PROCESS -> Range
forall a b. (GetRange a, GetRange b) => a -> b -> Range
compRange PROCESS
lp PROCESS
rp))
  AParser st PROCESS -> AParser st PROCESS -> AParser st PROCESS
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> PROCESS -> AParser st PROCESS
forall (m :: * -> *) a. Monad m => a -> m a
return PROCESS
lp

pref_proc :: AParser st PROCESS
pref_proc :: AParser st PROCESS
pref_proc = AParser st PROCESS
forall st. AParser st PROCESS
cond_proc AParser st PROCESS -> AParser st PROCESS -> AParser st PROCESS
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> AParser st PROCESS
forall st. AParser st PROCESS
hid_ren_proc
  AParser st PROCESS -> AParser st PROCESS -> AParser st PROCESS
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> (AParser st FQ_PROCESS_NAME
forall st. AParser st FQ_PROCESS_NAME
qualProc AParser st FQ_PROCESS_NAME
-> (FQ_PROCESS_NAME -> AParser st PROCESS) -> AParser st PROCESS
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= FQ_PROCESS_NAME -> AParser st PROCESS
forall st. FQ_PROCESS_NAME -> AParser st PROCESS
namedProc AParser st PROCESS
-> (PROCESS -> AParser st PROCESS) -> AParser st PROCESS
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= PROCESS -> AParser st PROCESS
forall st. PROCESS -> AParser st PROCESS
hid_ren_proc')
  AParser st PROCESS -> AParser st PROCESS -> AParser st PROCESS
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> (AParser st EVENT
forall st. AParser st EVENT
event AParser st EVENT
-> (EVENT -> AParser st PROCESS) -> AParser st PROCESS
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= EVENT -> AParser st PROCESS
forall st. EVENT -> AParser st PROCESS
mkPrefProc)
  AParser st PROCESS -> AParser st PROCESS -> AParser st PROCESS
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> AParser st PROCESS -> AParser st PROCESS
forall tok st a. GenParser tok st a -> GenParser tok st a
try
    (((((PROCESS_NAME -> FQ_PROCESS_NAME)
-> ParsecT String (AnnoState st) Identity PROCESS_NAME
-> AParser st FQ_PROCESS_NAME
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap PROCESS_NAME -> FQ_PROCESS_NAME
PROCESS_NAME ParsecT String (AnnoState st) Identity PROCESS_NAME
forall st. AParser st PROCESS_NAME
processId AParser st FQ_PROCESS_NAME
-> (FQ_PROCESS_NAME -> AParser st PROCESS) -> AParser st PROCESS
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= FQ_PROCESS_NAME -> AParser st PROCESS
forall st. FQ_PROCESS_NAME -> AParser st PROCESS
namedProc)
        AParser st PROCESS -> AParser st PROCESS -> AParser st PROCESS
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> AParser st PROCESS -> AParser st PROCESS
forall st a. AParser st a -> AParser st a
parens AParser st PROCESS
forall st. AParser st PROCESS
csp_casl_process) AParser st PROCESS
-> (PROCESS -> AParser st PROCESS) -> AParser st PROCESS
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= PROCESS -> AParser st PROCESS
forall st. PROCESS -> AParser st PROCESS
hid_ren_proc')
    AParser st PROCESS
-> GenParser Char (AnnoState st) Token -> AParser st PROCESS
forall tok st a b.
GenParser tok st a -> GenParser tok st b -> GenParser tok st a
`notFollowedWith` (GenParser Char (AnnoState st) Token
forall st. AParser st Token
prefSym GenParser Char (AnnoState st) Token
-> GenParser Char (AnnoState st) Token
-> GenParser Char (AnnoState st) Token
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> GenParser Char (AnnoState st) Token
forall st. AParser st Token
colonT))
  AParser st PROCESS -> AParser st PROCESS -> AParser st PROCESS
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> (AParser st EVENT -> AParser st EVENT
forall tok st a. GenParser tok st a -> GenParser tok st a
try (AParser st EVENT
forall st. AParser st EVENT
term_event AParser st EVENT
-> GenParser Char (AnnoState st) Token -> AParser st EVENT
forall (m :: * -> *) a b. Monad m => m a -> m b -> m a
<< GenParser Char (AnnoState st) Token
forall st. AParser st Token
prefSym)
      AParser st EVENT
-> (EVENT -> AParser st PROCESS) -> AParser st PROCESS
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= EVENT -> AParser st PROCESS
forall st. EVENT -> AParser st PROCESS
mkPrefProc)

prefSym :: AParser st Token
prefSym :: AParser st Token
prefSym = String -> AParser st Token
forall st. String -> AParser st Token
asKeySign String
prefix_procS

mkPrefProc :: EVENT -> AParser st PROCESS
mkPrefProc :: EVENT -> AParser st PROCESS
mkPrefProc e :: EVENT
e = do
    PROCESS
p <- AParser st PROCESS
forall st. AParser st PROCESS
pref_proc
    PROCESS -> AParser st PROCESS
forall (m :: * -> *) a. Monad m => a -> m a
return (EVENT -> PROCESS -> Range -> PROCESS
PrefixProcess EVENT
e PROCESS
p (EVENT -> PROCESS -> Range
forall a b. (GetRange a, GetRange b) => a -> b -> Range
compRange EVENT
e PROCESS
p))

hid_ren_proc :: AParser st PROCESS
hid_ren_proc :: AParser st PROCESS
hid_ren_proc = AParser st PROCESS
forall st. AParser st PROCESS
prim_proc AParser st PROCESS
-> (PROCESS -> AParser st PROCESS) -> AParser st PROCESS
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= PROCESS -> AParser st PROCESS
forall st. PROCESS -> AParser st PROCESS
hid_ren_proc'

hid_ren_proc' :: PROCESS -> AParser st PROCESS
hid_ren_proc' :: PROCESS -> AParser st PROCESS
hid_ren_proc' lp :: PROCESS
lp = do
    String -> AParser st Token
forall st. String -> AParser st Token
asKeySign String
hiding_procS
    EVENT_SET
es <- AParser st EVENT_SET
forall st. AParser st EVENT_SET
event_set
    PROCESS -> AParser st PROCESS
forall st. PROCESS -> AParser st PROCESS
hid_ren_proc' (PROCESS -> EVENT_SET -> Range -> PROCESS
Hiding PROCESS
lp EVENT_SET
es (PROCESS -> EVENT_SET -> Range
forall a b. (GetRange a, GetRange b) => a -> b -> Range
compRange PROCESS
lp EVENT_SET
es))
  AParser st PROCESS -> AParser st PROCESS -> AParser st PROCESS
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> do
    String -> AParser st Token
forall st. String -> AParser st Token
asKeySign String
ren_proc_openS
    RENAMING
rn <- AParser st RENAMING
forall st. AParser st RENAMING
renaming
    Token
ck <- String -> AParser st Token
forall st. String -> AParser st Token
asKeySign String
ren_proc_closeS
    PROCESS -> AParser st PROCESS
forall st. PROCESS -> AParser st PROCESS
hid_ren_proc' (PROCESS -> RENAMING -> Range -> PROCESS
RenamingProcess PROCESS
lp RENAMING
rn (PROCESS -> Token -> Range
forall a b. (GetRange a, GetRange b) => a -> b -> Range
compRange PROCESS
lp Token
ck))
  AParser st PROCESS -> AParser st PROCESS -> AParser st PROCESS
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> PROCESS -> AParser st PROCESS
forall (m :: * -> *) a. Monad m => a -> m a
return PROCESS
lp

-- | parser for parens
parens :: AParser st a -> AParser st a
parens :: AParser st a -> AParser st a
parens p :: AParser st a
p = CharParser (AnnoState st) Token
forall st. CharParser st Token
oParenT CharParser (AnnoState st) Token -> AParser st a -> AParser st a
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> AParser st a
p AParser st a -> CharParser (AnnoState st) Token -> AParser st a
forall (m :: * -> *) a b. Monad m => m a -> m b -> m a
<< CharParser (AnnoState st) Token
forall st. CharParser st Token
cParenT

-- | parser for comma-separated items in parens
parenList :: AParser st a -> AParser st [a]
parenList :: AParser st a -> AParser st [a]
parenList = AParser st [a] -> AParser st [a]
forall st a. AParser st a -> AParser st a
parens (AParser st [a] -> AParser st [a])
-> (AParser st a -> AParser st [a])
-> AParser st a
-> AParser st [a]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AParser st a -> AParser st [a]
forall st a. CharParser st a -> CharParser st [a]
commaSep1

namedProc :: FQ_PROCESS_NAME -> AParser st PROCESS
namedProc :: FQ_PROCESS_NAME -> AParser st PROCESS
namedProc pn :: FQ_PROCESS_NAME
pn = do
    [TERM ()]
args <- AParser st [TERM ()]
forall st. AParser st [TERM ()]
procArgs
    PROCESS -> AParser st PROCESS
forall (m :: * -> *) a. Monad m => a -> m a
return (PROCESS -> AParser st PROCESS) -> PROCESS -> AParser st PROCESS
forall a b. (a -> b) -> a -> b
$ FQ_PROCESS_NAME -> [TERM ()] -> Range -> PROCESS
NamedProcess FQ_PROCESS_NAME
pn [TERM ()]
args (Range -> PROCESS) -> Range -> PROCESS
forall a b. (a -> b) -> a -> b
$ FQ_PROCESS_NAME -> [TERM ()] -> Range
forall a b. (GetRange a, GetRange b) => a -> b -> Range
compRange FQ_PROCESS_NAME
pn [TERM ()]
args

prim_proc :: AParser st PROCESS
prim_proc :: AParser st PROCESS
prim_proc = do
    Token
rk <- String -> AParser st Token
forall st. String -> AParser st Token
asKey String
runS
    EVENT_SET
es <- AParser st EVENT_SET -> AParser st EVENT_SET
forall st a. AParser st a -> AParser st a
parens AParser st EVENT_SET
forall st. AParser st EVENT_SET
event_set
    PROCESS -> AParser st PROCESS
forall (m :: * -> *) a. Monad m => a -> m a
return (PROCESS -> AParser st PROCESS) -> PROCESS -> AParser st PROCESS
forall a b. (a -> b) -> a -> b
$ EVENT_SET -> Range -> PROCESS
Run EVENT_SET
es (Range -> PROCESS) -> Range -> PROCESS
forall a b. (a -> b) -> a -> b
$ Token -> Range
forall a. GetRange a => a -> Range
getRange Token
rk
  AParser st PROCESS -> AParser st PROCESS -> AParser st PROCESS
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> do
    Token
ck <- String -> AParser st Token
forall st. String -> AParser st Token
asKey String
chaosS
    EVENT_SET
es <- AParser st EVENT_SET -> AParser st EVENT_SET
forall st a. AParser st a -> AParser st a
parens AParser st EVENT_SET
forall st. AParser st EVENT_SET
event_set
    PROCESS -> AParser st PROCESS
forall (m :: * -> *) a. Monad m => a -> m a
return (PROCESS -> AParser st PROCESS) -> PROCESS -> AParser st PROCESS
forall a b. (a -> b) -> a -> b
$ EVENT_SET -> Range -> PROCESS
Chaos EVENT_SET
es (Range -> PROCESS) -> Range -> PROCESS
forall a b. (a -> b) -> a -> b
$ Token -> Range
forall a. GetRange a => a -> Range
getRange Token
ck
  AParser st PROCESS -> AParser st PROCESS -> AParser st PROCESS
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> (Token -> PROCESS) -> AParser st Token -> AParser st PROCESS
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Range -> PROCESS
Div (Range -> PROCESS) -> (Token -> Range) -> Token -> PROCESS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Token -> Range
forall a. GetRange a => a -> Range
getRange) (String -> AParser st Token
forall st. String -> AParser st Token
asKey String
divS)
  AParser st PROCESS -> AParser st PROCESS -> AParser st PROCESS
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> (Token -> PROCESS) -> AParser st Token -> AParser st PROCESS
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Range -> PROCESS
Stop (Range -> PROCESS) -> (Token -> Range) -> Token -> PROCESS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Token -> Range
forall a. GetRange a => a -> Range
getRange) (String -> AParser st Token
forall st. String -> AParser st Token
asKey String
stopS)
  AParser st PROCESS -> AParser st PROCESS -> AParser st PROCESS
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> (Token -> PROCESS) -> AParser st Token -> AParser st PROCESS
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Range -> PROCESS
Skip (Range -> PROCESS) -> (Token -> Range) -> Token -> PROCESS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Token -> Range
forall a. GetRange a => a -> Range
getRange) (String -> AParser st Token
forall st. String -> AParser st Token
asKey String
skipS)

-- | Parse a process name which can be a simple one or a fully qualified one.
process_name :: AParser st FQ_PROCESS_NAME
process_name :: AParser st FQ_PROCESS_NAME
process_name = AParser st FQ_PROCESS_NAME
forall st. AParser st FQ_PROCESS_NAME
qualProc AParser st FQ_PROCESS_NAME
-> AParser st FQ_PROCESS_NAME -> AParser st FQ_PROCESS_NAME
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> (PROCESS_NAME -> FQ_PROCESS_NAME)
-> ParsecT String (AnnoState st) Identity PROCESS_NAME
-> AParser st FQ_PROCESS_NAME
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap PROCESS_NAME -> FQ_PROCESS_NAME
PROCESS_NAME ParsecT String (AnnoState st) Identity PROCESS_NAME
forall st. AParser st PROCESS_NAME
processId

-- | Parse a process identifier
processId :: AParser st PROCESS_NAME
processId :: AParser st PROCESS_NAME
processId = do
  Token
s <- AParser st Token
forall st. AParser st Token
var
  (c :: [PROCESS_NAME]
c, p :: Range
p) <- ([PROCESS_NAME], Range)
-> ParsecT String (AnnoState st) Identity ([PROCESS_NAME], Range)
-> ParsecT String (AnnoState st) Identity ([PROCESS_NAME], Range)
forall s (m :: * -> *) t a u.
Stream s m t =>
a -> ParsecT s u m a -> ParsecT s u m a
option ([], Range
nullRange) ParsecT String (AnnoState st) Identity ([PROCESS_NAME], Range)
forall st. AParser st ([PROCESS_NAME], Range)
cspComps
  PROCESS_NAME -> AParser st PROCESS_NAME
forall (m :: * -> *) a. Monad m => a -> m a
return ([Token] -> [PROCESS_NAME] -> Range -> PROCESS_NAME
Id [Token
s] [PROCESS_NAME]
c Range
p)

cspComps :: AParser st ([Id], Range)
cspComps :: AParser st ([PROCESS_NAME], Range)
cspComps = AParser st ([PROCESS_NAME], Range)
-> AParser st ([PROCESS_NAME], Range)
forall tok st a. GenParser tok st a -> GenParser tok st a
try (AParser st ([PROCESS_NAME], Range)
 -> AParser st ([PROCESS_NAME], Range))
-> AParser st ([PROCESS_NAME], Range)
-> AParser st ([PROCESS_NAME], Range)
forall a b. (a -> b) -> a -> b
$ do
  Token
o <- CharParser (AnnoState st) String -> CharParser (AnnoState st) Token
forall st. CharParser st String -> CharParser st Token
pToken (CharParser (AnnoState st) String
 -> CharParser (AnnoState st) Token)
-> CharParser (AnnoState st) String
-> CharParser (AnnoState st) Token
forall a b. (a -> b) -> a -> b
$ String -> CharParser (AnnoState st) String
forall s (m :: * -> *) u.
Stream s m Char =>
String -> ParsecT s u m String
string "[" CharParser (AnnoState st) String
-> ParsecT String (AnnoState st) Identity ()
-> CharParser (AnnoState st) String
forall (m :: * -> *) a b. Monad m => m a -> m b -> m a
<< ParsecT String (AnnoState st) Identity Char
-> ParsecT String (AnnoState st) Identity ()
forall s (m :: * -> *) t a u.
(Stream s m t, Show a) =>
ParsecT s u m a -> ParsecT s u m ()
notFollowedBy (String -> ParsecT String (AnnoState st) Identity Char
forall s (m :: * -> *) u.
Stream s m Char =>
String -> ParsecT s u m Char
oneOf "[]|")
  (ts :: [PROCESS_NAME]
ts, ps :: [Token]
ps) <- [String] -> GenParser Char (AnnoState st) PROCESS_NAME
forall st. [String] -> GenParser Char st PROCESS_NAME
parseId [String]
cspKeywords GenParser Char (AnnoState st) PROCESS_NAME
-> CharParser (AnnoState st) Token
-> GenParser Char (AnnoState st) ([PROCESS_NAME], [Token])
forall tok st a b.
GenParser tok st a
-> GenParser tok st b -> GenParser tok st ([a], [b])
`separatedBy` CharParser (AnnoState st) Token
forall st. CharParser st Token
commaT
  Token
c <- CharParser (AnnoState st) Token
forall st. CharParser st Token
cBracketT
  ([PROCESS_NAME], Range) -> AParser st ([PROCESS_NAME], Range)
forall (m :: * -> *) a. Monad m => a -> m a
return ([PROCESS_NAME]
ts, Token -> [Token] -> Token -> Range
toRange Token
o [Token]
ps Token
c)

channel_name :: AParser st CHANNEL_NAME
channel_name :: AParser st PROCESS_NAME
channel_name = AParser st PROCESS_NAME
forall st. AParser st PROCESS_NAME
cspSortId

-- List of arguments to a named process
procArgs :: AParser st [TERM ()]
procArgs :: AParser st [TERM ()]
procArgs = AParser st [TERM ()] -> AParser st [TERM ()]
forall tok st a. GenParser tok st [a] -> GenParser tok st [a]
optionL (AParser st [TERM ()] -> AParser st [TERM ()])
-> AParser st [TERM ()] -> AParser st [TERM ()]
forall a b. (a -> b) -> a -> b
$ AParser st (TERM ()) -> AParser st [TERM ()]
forall st a. AParser st a -> AParser st [a]
parenList (AParser st (TERM ()) -> AParser st [TERM ()])
-> AParser st (TERM ()) -> AParser st [TERM ()]
forall a b. (a -> b) -> a -> b
$ [String] -> AParser st (TERM ())
forall f st. TermParser f => [String] -> AParser st (TERM f)
CASL.term [String]
cspKeywords

event_set :: AParser st EVENT_SET
event_set :: AParser st EVENT_SET
event_set = do
    [CommType]
cts <- AParser st [CommType]
forall st. AParser st [CommType]
alphabet AParser st [CommType] -> String -> AParser st [CommType]
forall s u (m :: * -> *) a.
ParsecT s u m a -> String -> ParsecT s u m a
<?> "communication type"
    EVENT_SET -> AParser st EVENT_SET
forall (m :: * -> *) a. Monad m => a -> m a
return ([CommType] -> Range -> EVENT_SET
EventSet [CommType]
cts ([CommType] -> Range
forall a. GetRange a => a -> Range
getRange [CommType]
cts))

{- Events may be simple CASL terms or channel send/receives or
internal / external prefix choice. -}
event :: AParser st EVENT
event :: AParser st EVENT
event = (AParser st EVENT
forall st. AParser st EVENT
prefixChoice AParser st EVENT -> AParser st EVENT -> AParser st EVENT
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> AParser st EVENT
forall st. AParser st EVENT
chanComm) AParser st EVENT
-> ParsecT String (AnnoState st) Identity Token -> AParser st EVENT
forall (m :: * -> *) a b. Monad m => m a -> m b -> m a
<< ParsecT String (AnnoState st) Identity Token
forall st. AParser st Token
prefSym

svarKey :: AParser st Token
svarKey :: AParser st Token
svarKey = String -> AParser st Token
forall st. String -> AParser st Token
asKeySign String
svar_sortS AParser st Token -> AParser st Token -> AParser st Token
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> String -> AParser st Token
forall st. String -> AParser st Token
asKeySign String
colonS

chanComm :: AParser st EVENT
chanComm :: AParser st EVENT
chanComm = do
    (cn :: PROCESS_NAME
cn, sr :: Token
sr) <- GenParser Char (AnnoState st) (PROCESS_NAME, Token)
-> GenParser Char (AnnoState st) (PROCESS_NAME, Token)
forall tok st a. GenParser tok st a -> GenParser tok st a
try (GenParser Char (AnnoState st) (PROCESS_NAME, Token)
 -> GenParser Char (AnnoState st) (PROCESS_NAME, Token))
-> GenParser Char (AnnoState st) (PROCESS_NAME, Token)
-> GenParser Char (AnnoState st) (PROCESS_NAME, Token)
forall a b. (a -> b) -> a -> b
$ ParsecT String (AnnoState st) Identity PROCESS_NAME
-> ParsecT String (AnnoState st) Identity Token
-> GenParser Char (AnnoState st) (PROCESS_NAME, Token)
forall (m :: * -> *) a b. Monad m => m a -> m b -> m (a, b)
pair ParsecT String (AnnoState st) Identity PROCESS_NAME
forall st. AParser st PROCESS_NAME
channel_name
       (ParsecT String (AnnoState st) Identity Token
 -> GenParser Char (AnnoState st) (PROCESS_NAME, Token))
-> ParsecT String (AnnoState st) Identity Token
-> GenParser Char (AnnoState st) (PROCESS_NAME, Token)
forall a b. (a -> b) -> a -> b
$ String -> ParsecT String (AnnoState st) Identity Token
forall st. String -> AParser st Token
asKeySign String
chan_sendS ParsecT String (AnnoState st) Identity Token
-> ParsecT String (AnnoState st) Identity Token
-> ParsecT String (AnnoState st) Identity Token
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> String -> ParsecT String (AnnoState st) Identity Token
forall st. String -> AParser st Token
asKeySign String
chan_receiveS
    if Token -> String
tokStr Token
sr String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
chan_sendS then do
         -- a double colon makes the difference to a CASL term
         Token
v <- ParsecT String (AnnoState st) Identity Token
-> ParsecT String (AnnoState st) Identity Token
forall tok st a. GenParser tok st a -> GenParser tok st a
try (ParsecT String (AnnoState st) Identity Token
 -> ParsecT String (AnnoState st) Identity Token)
-> ParsecT String (AnnoState st) Identity Token
-> ParsecT String (AnnoState st) Identity Token
forall a b. (a -> b) -> a -> b
$ ParsecT String (AnnoState st) Identity Token
forall st. AParser st Token
var ParsecT String (AnnoState st) Identity Token
-> ParsecT String (AnnoState st) Identity Token
-> ParsecT String (AnnoState st) Identity Token
forall (m :: * -> *) a b. Monad m => m a -> m b -> m a
<< String -> ParsecT String (AnnoState st) Identity Token
forall st. String -> AParser st Token
asKeySign String
svar_sortS
         PROCESS_NAME
s <- ParsecT String (AnnoState st) Identity PROCESS_NAME
forall st. AParser st PROCESS_NAME
cspSortId
         EVENT -> AParser st EVENT
forall (m :: * -> *) a. Monad m => a -> m a
return (PROCESS_NAME -> Token -> PROCESS_NAME -> Range -> EVENT
ChanNonDetSend PROCESS_NAME
cn Token
v PROCESS_NAME
s (PROCESS_NAME -> PROCESS_NAME -> Range
forall a b. (GetRange a, GetRange b) => a -> b -> Range
compRange PROCESS_NAME
cn PROCESS_NAME
s))
       AParser st EVENT -> AParser st EVENT -> AParser st EVENT
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> do
         TERM ()
t <- [String] -> AParser st (TERM ())
forall f st. TermParser f => [String] -> AParser st (TERM f)
CASL.term [String]
cspKeywords
         EVENT -> AParser st EVENT
forall (m :: * -> *) a. Monad m => a -> m a
return (PROCESS_NAME -> TERM () -> Range -> EVENT
ChanSend PROCESS_NAME
cn TERM ()
t (PROCESS_NAME -> Range
forall a. GetRange a => a -> Range
getRange PROCESS_NAME
cn))
       else do
         Token
v <- ParsecT String (AnnoState st) Identity Token
forall st. AParser st Token
var ParsecT String (AnnoState st) Identity Token
-> ParsecT String (AnnoState st) Identity Token
-> ParsecT String (AnnoState st) Identity Token
forall (m :: * -> *) a b. Monad m => m a -> m b -> m a
<< ParsecT String (AnnoState st) Identity Token
forall st. AParser st Token
svarKey
         PROCESS_NAME
s <- ParsecT String (AnnoState st) Identity PROCESS_NAME
forall st. AParser st PROCESS_NAME
cspSortId
         EVENT -> AParser st EVENT
forall (m :: * -> *) a. Monad m => a -> m a
return (PROCESS_NAME -> Token -> PROCESS_NAME -> Range -> EVENT
ChanRecv PROCESS_NAME
cn Token
v PROCESS_NAME
s (PROCESS_NAME -> PROCESS_NAME -> Range
forall a b. (GetRange a, GetRange b) => a -> b -> Range
compRange PROCESS_NAME
cn PROCESS_NAME
s))

prefixChoice :: AParser st EVENT
prefixChoice :: AParser st EVENT
prefixChoice = do
    Token -> PROCESS_NAME -> Range -> EVENT
constr <- (Token -> Token -> PROCESS_NAME -> Range -> EVENT)
-> ParsecT String (AnnoState st) Identity Token
-> ParsecT
     String
     (AnnoState st)
     Identity
     (Token -> PROCESS_NAME -> Range -> EVENT)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Token -> PROCESS_NAME -> Range -> EVENT)
-> Token -> Token -> PROCESS_NAME -> Range -> EVENT
forall a b. a -> b -> a
const Token -> PROCESS_NAME -> Range -> EVENT
InternalPrefixChoice) (String -> ParsecT String (AnnoState st) Identity Token
forall st. String -> AParser st Token
asKeySign String
internal_choiceS)
      ParsecT
  String
  (AnnoState st)
  Identity
  (Token -> PROCESS_NAME -> Range -> EVENT)
-> ParsecT
     String
     (AnnoState st)
     Identity
     (Token -> PROCESS_NAME -> Range -> EVENT)
-> ParsecT
     String
     (AnnoState st)
     Identity
     (Token -> PROCESS_NAME -> Range -> EVENT)
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> (Token -> Token -> PROCESS_NAME -> Range -> EVENT)
-> ParsecT String (AnnoState st) Identity Token
-> ParsecT
     String
     (AnnoState st)
     Identity
     (Token -> PROCESS_NAME -> Range -> EVENT)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Token -> PROCESS_NAME -> Range -> EVENT)
-> Token -> Token -> PROCESS_NAME -> Range -> EVENT
forall a b. a -> b -> a
const Token -> PROCESS_NAME -> Range -> EVENT
ExternalPrefixChoice) (String -> ParsecT String (AnnoState st) Identity Token
forall st. String -> AParser st Token
asKeySign String
external_choiceS)
    Token
v <- ParsecT String (AnnoState st) Identity Token
forall st. AParser st Token
var
    ParsecT String (AnnoState st) Identity Token
forall st. AParser st Token
svarKey
    PROCESS_NAME
s <- AParser st PROCESS_NAME
forall st. AParser st PROCESS_NAME
cspSortId
    EVENT -> AParser st EVENT
forall (m :: * -> *) a. Monad m => a -> m a
return (EVENT -> AParser st EVENT) -> EVENT -> AParser st EVENT
forall a b. (a -> b) -> a -> b
$ Token -> PROCESS_NAME -> Range -> EVENT
constr Token
v PROCESS_NAME
s (Range -> EVENT) -> Range -> EVENT
forall a b. (a -> b) -> a -> b
$ PROCESS_NAME -> Range
forall a. GetRange a => a -> Range
getRange PROCESS_NAME
s

term_event :: AParser st EVENT
term_event :: AParser st EVENT
term_event = do
    TERM ()
t <- [String] -> AParser st (TERM ())
forall f st. TermParser f => [String] -> AParser st (TERM f)
CASL.term [String]
cspKeywords
    EVENT -> AParser st EVENT
forall (m :: * -> *) a. Monad m => a -> m a
return (TERM () -> Range -> EVENT
TermEvent TERM ()
t (TERM () -> Range
forall a. GetRange a => a -> Range
getRange TERM ()
t))

{- Formulas are CASL formulas.  We make our own wrapper around them
however. -}

formula :: AParser st (FORMULA ())
formula :: AParser st (FORMULA ())
formula = [String] -> AParser st (FORMULA ())
forall f st. TermParser f => [String] -> AParser st (FORMULA f)
CASL.formula [String]
cspKeywords

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

renameKind :: Maybe RenameKind -> AParser st (RenameKind, Maybe (SORT, SORT))
renameKind :: Maybe RenameKind
-> AParser st (RenameKind, Maybe (PROCESS_NAME, PROCESS_NAME))
renameKind ok :: Maybe RenameKind
ok = do
  let funs :: [(String, RenameKind)]
funs = [(String
pFun, RenameKind
PartOp), (String
funS, RenameKind
TotOp)]
      preds :: [(String, RenameKind)]
preds = [(String
prodS, RenameKind
BinPred), (String
timesS, RenameKind
BinPred)]
      expectedSymbs :: [(String, RenameKind)]
expectedSymbs = case Maybe RenameKind
ok of
        Just BinPred -> [(String, RenameKind)]
preds
        Just PartOp -> [(String, RenameKind)]
funs
        _ -> [(String, RenameKind)]
funs [(String, RenameKind)]
-> [(String, RenameKind)] -> [(String, RenameKind)]
forall a. [a] -> [a] -> [a]
++ [(String, RenameKind)]
preds
  PROCESS_NAME
s1 <- AParser st PROCESS_NAME
forall st. AParser st PROCESS_NAME
cspSortId
  RenameKind
c <- [ParsecT String (AnnoState st) Identity RenameKind]
-> ParsecT String (AnnoState st) Identity RenameKind
forall s (m :: * -> *) t u a.
Stream s m t =>
[ParsecT s u m a] -> ParsecT s u m a
choice ([ParsecT String (AnnoState st) Identity RenameKind]
 -> ParsecT String (AnnoState st) Identity RenameKind)
-> [ParsecT String (AnnoState st) Identity RenameKind]
-> ParsecT String (AnnoState st) Identity RenameKind
forall a b. (a -> b) -> a -> b
$ ((String, RenameKind)
 -> ParsecT String (AnnoState st) Identity RenameKind)
-> [(String, RenameKind)]
-> [ParsecT String (AnnoState st) Identity RenameKind]
forall a b. (a -> b) -> [a] -> [b]
map (\ (s :: String
s, k :: RenameKind
k) -> (String -> AParser st Token
forall st. String -> AParser st Token
asKey String
s AParser st Token
-> ParsecT String (AnnoState st) Identity RenameKind
-> ParsecT String (AnnoState st) Identity RenameKind
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> RenameKind -> ParsecT String (AnnoState st) Identity RenameKind
forall (m :: * -> *) a. Monad m => a -> m a
return RenameKind
k))
        [(String, RenameKind)]
expectedSymbs
  PROCESS_NAME
s2 <- AParser st PROCESS_NAME
forall st. AParser st PROCESS_NAME
cspSortId
  (RenameKind, Maybe (PROCESS_NAME, PROCESS_NAME))
-> AParser st (RenameKind, Maybe (PROCESS_NAME, PROCESS_NAME))
forall (m :: * -> *) a. Monad m => a -> m a
return (RenameKind
c, (PROCESS_NAME, PROCESS_NAME) -> Maybe (PROCESS_NAME, PROCESS_NAME)
forall a. a -> Maybe a
Just (PROCESS_NAME
s1, PROCESS_NAME
s2))

renameOpOrPred :: RenameKind -> AParser st Rename
renameOpOrPred :: RenameKind -> AParser st Rename
renameOpOrPred k :: RenameKind
k = do
   PROCESS_NAME
i <- AParser st PROCESS_NAME
forall st. AParser st PROCESS_NAME
parseCspId
   (RenameKind, Maybe (PROCESS_NAME, PROCESS_NAME))
c <- (RenameKind, Maybe (PROCESS_NAME, PROCESS_NAME))
-> ParsecT
     String
     (AnnoState st)
     Identity
     (RenameKind, Maybe (PROCESS_NAME, PROCESS_NAME))
-> ParsecT
     String
     (AnnoState st)
     Identity
     (RenameKind, Maybe (PROCESS_NAME, PROCESS_NAME))
forall s (m :: * -> *) t a u.
Stream s m t =>
a -> ParsecT s u m a -> ParsecT s u m a
option (RenameKind
k, Maybe (PROCESS_NAME, PROCESS_NAME)
forall a. Maybe a
Nothing) (ParsecT
   String
   (AnnoState st)
   Identity
   (RenameKind, Maybe (PROCESS_NAME, PROCESS_NAME))
 -> ParsecT
      String
      (AnnoState st)
      Identity
      (RenameKind, Maybe (PROCESS_NAME, PROCESS_NAME)))
-> ParsecT
     String
     (AnnoState st)
     Identity
     (RenameKind, Maybe (PROCESS_NAME, PROCESS_NAME))
-> ParsecT
     String
     (AnnoState st)
     Identity
     (RenameKind, Maybe (PROCESS_NAME, PROCESS_NAME))
forall a b. (a -> b) -> a -> b
$ Maybe RenameKind
-> ParsecT
     String
     (AnnoState st)
     Identity
     (RenameKind, Maybe (PROCESS_NAME, PROCESS_NAME))
forall st.
Maybe RenameKind
-> AParser st (RenameKind, Maybe (PROCESS_NAME, PROCESS_NAME))
renameKind (Maybe RenameKind
 -> ParsecT
      String
      (AnnoState st)
      Identity
      (RenameKind, Maybe (PROCESS_NAME, PROCESS_NAME)))
-> Maybe RenameKind
-> ParsecT
     String
     (AnnoState st)
     Identity
     (RenameKind, Maybe (PROCESS_NAME, PROCESS_NAME))
forall a b. (a -> b) -> a -> b
$ RenameKind -> Maybe RenameKind
forall a. a -> Maybe a
Just RenameKind
k
   Rename -> AParser st Rename
forall (m :: * -> *) a. Monad m => a -> m a
return (Rename -> AParser st Rename) -> Rename -> AParser st Rename
forall a b. (a -> b) -> a -> b
$ PROCESS_NAME
-> Maybe (RenameKind, Maybe (PROCESS_NAME, PROCESS_NAME)) -> Rename
Rename PROCESS_NAME
i (Maybe (RenameKind, Maybe (PROCESS_NAME, PROCESS_NAME)) -> Rename)
-> Maybe (RenameKind, Maybe (PROCESS_NAME, PROCESS_NAME)) -> Rename
forall a b. (a -> b) -> a -> b
$ (RenameKind, Maybe (PROCESS_NAME, PROCESS_NAME))
-> Maybe (RenameKind, Maybe (PROCESS_NAME, PROCESS_NAME))
forall a. a -> Maybe a
Just (RenameKind, Maybe (PROCESS_NAME, PROCESS_NAME))
c

rename :: AParser st Rename
rename :: AParser st Rename
rename = do
    PROCESS_NAME
i <- AParser st PROCESS_NAME
forall st. AParser st PROCESS_NAME
parseCspId
    Maybe (RenameKind, Maybe (PROCESS_NAME, PROCESS_NAME))
mc <- ParsecT
  String
  (AnnoState st)
  Identity
  (RenameKind, Maybe (PROCESS_NAME, PROCESS_NAME))
-> ParsecT
     String
     (AnnoState st)
     Identity
     (Maybe (RenameKind, Maybe (PROCESS_NAME, PROCESS_NAME)))
forall s (m :: * -> *) t u a.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m (Maybe a)
optionMaybe (ParsecT
   String
   (AnnoState st)
   Identity
   (RenameKind, Maybe (PROCESS_NAME, PROCESS_NAME))
 -> ParsecT
      String
      (AnnoState st)
      Identity
      (Maybe (RenameKind, Maybe (PROCESS_NAME, PROCESS_NAME))))
-> ParsecT
     String
     (AnnoState st)
     Identity
     (RenameKind, Maybe (PROCESS_NAME, PROCESS_NAME))
-> ParsecT
     String
     (AnnoState st)
     Identity
     (Maybe (RenameKind, Maybe (PROCESS_NAME, PROCESS_NAME)))
forall a b. (a -> b) -> a -> b
$ Maybe RenameKind
-> ParsecT
     String
     (AnnoState st)
     Identity
     (RenameKind, Maybe (PROCESS_NAME, PROCESS_NAME))
forall st.
Maybe RenameKind
-> AParser st (RenameKind, Maybe (PROCESS_NAME, PROCESS_NAME))
renameKind Maybe RenameKind
forall a. Maybe a
Nothing
    Rename -> AParser st Rename
forall (m :: * -> *) a. Monad m => a -> m a
return (Rename -> AParser st Rename) -> Rename -> AParser st Rename
forall a b. (a -> b) -> a -> b
$ PROCESS_NAME
-> Maybe (RenameKind, Maybe (PROCESS_NAME, PROCESS_NAME)) -> Rename
Rename PROCESS_NAME
i Maybe (RenameKind, Maybe (PROCESS_NAME, PROCESS_NAME))
mc
  AParser st Rename -> AParser st Rename -> AParser st Rename
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> do
    String -> AParser st Token
forall st. String -> AParser st Token
asKey String
opS
    RenameKind -> AParser st Rename
forall st. RenameKind -> AParser st Rename
renameOpOrPred RenameKind
PartOp
  AParser st Rename -> AParser st Rename -> AParser st Rename
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> do
    String -> AParser st Token
forall st. String -> AParser st Token
asKey String
predS
    RenameKind -> AParser st Rename
forall st. RenameKind -> AParser st Rename
renameOpOrPred RenameKind
BinPred

renaming :: AParser st RENAMING
renaming :: AParser st RENAMING
renaming = ([Rename] -> RENAMING)
-> ParsecT String (AnnoState st) Identity [Rename]
-> AParser st RENAMING
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [Rename] -> RENAMING
Renaming (ParsecT String (AnnoState st) Identity [Rename]
 -> AParser st RENAMING)
-> ParsecT String (AnnoState st) Identity [Rename]
-> AParser st RENAMING
forall a b. (a -> b) -> a -> b
$ AParser st Rename
forall st. AParser st Rename
rename AParser st Rename
-> ParsecT String (AnnoState st) Identity Token
-> ParsecT String (AnnoState st) Identity [Rename]
forall s (m :: * -> *) t u a sep.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m sep -> ParsecT s u m [a]
`sepBy1` ParsecT String (AnnoState st) Identity Token
forall st. CharParser st Token
commaT

-- names come from CASL/Hets.

var :: AParser st VAR
var :: AParser st Token
var = [String] -> AParser st Token
forall st. [String] -> GenParser Char st Token
varId [String]
cspKeywords

parseCspId :: AParser st Id
parseCspId :: AParser st PROCESS_NAME
parseCspId = [String] -> AParser st PROCESS_NAME
forall st. [String] -> GenParser Char st PROCESS_NAME
parseId [String]
cspKeywords

cspSortId :: AParser st SORT
cspSortId :: AParser st PROCESS_NAME
cspSortId = [String] -> AParser st PROCESS_NAME
forall st. [String] -> GenParser Char st PROCESS_NAME
sortId [String]
cspKeywords

-- Composition of ranges

compRange :: (GetRange a, GetRange b) => a -> b -> Range
compRange :: a -> b -> Range
compRange x :: a
x y :: b
y = a -> Range
forall a. GetRange a => a -> Range
getRange a
x Range -> Range -> Range
`appRange` b -> Range
forall a. GetRange a => a -> Range
getRange b
y

-- * parse the beginning of a process declaration or equation

-- | parse many vars with the same sort
sortedVars :: AParser st (Either [SORT] VAR_DECL)
sortedVars :: AParser st (Either [PROCESS_NAME] VAR_DECL)
sortedVars = do
    [PROCESS_NAME]
is <- CharParser (AnnoState st) PROCESS_NAME
-> CharParser (AnnoState st) [PROCESS_NAME]
forall st a. CharParser st a -> CharParser st [a]
commaSep1 CharParser (AnnoState st) PROCESS_NAME
forall st. AParser st PROCESS_NAME
cspSortId
    Maybe (Token, PROCESS_NAME)
ms <- ParsecT String (AnnoState st) Identity (Token, PROCESS_NAME)
-> ParsecT
     String (AnnoState st) Identity (Maybe (Token, PROCESS_NAME))
forall s (m :: * -> *) t u a.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m (Maybe a)
optionMaybe (ParsecT String (AnnoState st) Identity (Token, PROCESS_NAME)
 -> ParsecT
      String (AnnoState st) Identity (Maybe (Token, PROCESS_NAME)))
-> ParsecT String (AnnoState st) Identity (Token, PROCESS_NAME)
-> ParsecT
     String (AnnoState st) Identity (Maybe (Token, PROCESS_NAME))
forall a b. (a -> b) -> a -> b
$ ParsecT String (AnnoState st) Identity Token
-> CharParser (AnnoState st) PROCESS_NAME
-> ParsecT String (AnnoState st) Identity (Token, PROCESS_NAME)
forall (m :: * -> *) a b. Monad m => m a -> m b -> m (a, b)
pair ParsecT String (AnnoState st) Identity Token
forall st. AParser st Token
colonT CharParser (AnnoState st) PROCESS_NAME
forall st. AParser st PROCESS_NAME
cspSortId
    case Maybe (Token, PROCESS_NAME)
ms of
      Nothing -> Either [PROCESS_NAME] VAR_DECL
-> AParser st (Either [PROCESS_NAME] VAR_DECL)
forall (m :: * -> *) a. Monad m => a -> m a
return (Either [PROCESS_NAME] VAR_DECL
 -> AParser st (Either [PROCESS_NAME] VAR_DECL))
-> Either [PROCESS_NAME] VAR_DECL
-> AParser st (Either [PROCESS_NAME] VAR_DECL)
forall a b. (a -> b) -> a -> b
$ [PROCESS_NAME] -> Either [PROCESS_NAME] VAR_DECL
forall a b. a -> Either a b
Left [PROCESS_NAME]
is
      Just (r :: Token
r, s :: PROCESS_NAME
s) -> if (PROCESS_NAME -> Bool) -> [PROCESS_NAME] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all PROCESS_NAME -> Bool
isSimpleId [PROCESS_NAME]
is
        then Either [PROCESS_NAME] VAR_DECL
-> AParser st (Either [PROCESS_NAME] VAR_DECL)
forall (m :: * -> *) a. Monad m => a -> m a
return (Either [PROCESS_NAME] VAR_DECL
 -> AParser st (Either [PROCESS_NAME] VAR_DECL))
-> Either [PROCESS_NAME] VAR_DECL
-> AParser st (Either [PROCESS_NAME] VAR_DECL)
forall a b. (a -> b) -> a -> b
$ VAR_DECL -> Either [PROCESS_NAME] VAR_DECL
forall a b. b -> Either a b
Right (VAR_DECL -> Either [PROCESS_NAME] VAR_DECL)
-> VAR_DECL -> Either [PROCESS_NAME] VAR_DECL
forall a b. (a -> b) -> a -> b
$ [Token] -> PROCESS_NAME -> Range -> VAR_DECL
Var_decl ((PROCESS_NAME -> Token) -> [PROCESS_NAME] -> [Token]
forall a b. (a -> b) -> [a] -> [b]
map PROCESS_NAME -> Token
idToSimpleId [PROCESS_NAME]
is) PROCESS_NAME
s (Range -> VAR_DECL) -> Range -> VAR_DECL
forall a b. (a -> b) -> a -> b
$ Token -> Range
tokPos Token
r else
        String -> AParser st (Either [PROCESS_NAME] VAR_DECL)
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail "expected only simple vars before colon"

-- | parse variables with possibly different sorts
manySortedVars :: AParser st (Either [SORT] [VAR_DECL])
manySortedVars :: AParser st (Either [PROCESS_NAME] [VAR_DECL])
manySortedVars = do
  Either [PROCESS_NAME] VAR_DECL
e <- AParser st (Either [PROCESS_NAME] VAR_DECL)
forall st. AParser st (Either [PROCESS_NAME] VAR_DECL)
sortedVars
  case Either [PROCESS_NAME] VAR_DECL
e of
    Left s :: [PROCESS_NAME]
s -> Either [PROCESS_NAME] [VAR_DECL]
-> AParser st (Either [PROCESS_NAME] [VAR_DECL])
forall (m :: * -> *) a. Monad m => a -> m a
return (Either [PROCESS_NAME] [VAR_DECL]
 -> AParser st (Either [PROCESS_NAME] [VAR_DECL]))
-> Either [PROCESS_NAME] [VAR_DECL]
-> AParser st (Either [PROCESS_NAME] [VAR_DECL])
forall a b. (a -> b) -> a -> b
$ [PROCESS_NAME] -> Either [PROCESS_NAME] [VAR_DECL]
forall a b. a -> Either a b
Left [PROCESS_NAME]
s
    Right vd :: VAR_DECL
vd -> do
       [VAR_DECL]
vs <- GenParser Char (AnnoState st) [VAR_DECL]
-> GenParser Char (AnnoState st) [VAR_DECL]
forall tok st a. GenParser tok st [a] -> GenParser tok st [a]
optionL (GenParser Char (AnnoState st) [VAR_DECL]
 -> GenParser Char (AnnoState st) [VAR_DECL])
-> GenParser Char (AnnoState st) [VAR_DECL]
-> GenParser Char (AnnoState st) [VAR_DECL]
forall a b. (a -> b) -> a -> b
$ AParser st Token
forall st. AParser st Token
anSemiOrComma
          AParser st Token
-> GenParser Char (AnnoState st) [VAR_DECL]
-> GenParser Char (AnnoState st) [VAR_DECL]
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (([VAR_DECL], [Token]) -> [VAR_DECL])
-> ParsecT String (AnnoState st) Identity ([VAR_DECL], [Token])
-> GenParser Char (AnnoState st) [VAR_DECL]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ([VAR_DECL], [Token]) -> [VAR_DECL]
forall a b. (a, b) -> a
fst ([String]
-> ParsecT String (AnnoState st) Identity ([VAR_DECL], [Token])
forall st. [String] -> AParser st ([VAR_DECL], [Token])
CASL.varDecls [String]
cspKeywords)
       Either [PROCESS_NAME] [VAR_DECL]
-> AParser st (Either [PROCESS_NAME] [VAR_DECL])
forall (m :: * -> *) a. Monad m => a -> m a
return (Either [PROCESS_NAME] [VAR_DECL]
 -> AParser st (Either [PROCESS_NAME] [VAR_DECL]))
-> Either [PROCESS_NAME] [VAR_DECL]
-> AParser st (Either [PROCESS_NAME] [VAR_DECL])
forall a b. (a -> b) -> a -> b
$ [VAR_DECL] -> Either [PROCESS_NAME] [VAR_DECL]
forall a b. b -> Either a b
Right ([VAR_DECL] -> Either [PROCESS_NAME] [VAR_DECL])
-> [VAR_DECL] -> Either [PROCESS_NAME] [VAR_DECL]
forall a b. (a -> b) -> a -> b
$ VAR_DECL
vd VAR_DECL -> [VAR_DECL] -> [VAR_DECL]
forall a. a -> [a] -> [a]
: [VAR_DECL]
vs

-- | parse a sort or a sorted channel
commType :: AParser st CommType
commType :: AParser st CommType
commType = do
  PROCESS_NAME
s <- AParser st PROCESS_NAME
forall st. AParser st PROCESS_NAME
cspSortId
  do
    AParser st Token
forall st. AParser st Token
colonT
    PROCESS_NAME
r <- AParser st PROCESS_NAME
forall st. AParser st PROCESS_NAME
cspSortId
    CommType -> AParser st CommType
forall (m :: * -> *) a. Monad m => a -> m a
return (CommType -> AParser st CommType)
-> CommType -> AParser st CommType
forall a b. (a -> b) -> a -> b
$ TypedChanName -> CommType
CommTypeChan (TypedChanName -> CommType) -> TypedChanName -> CommType
forall a b. (a -> b) -> a -> b
$ PROCESS_NAME -> PROCESS_NAME -> TypedChanName
TypedChanName PROCESS_NAME
s PROCESS_NAME
r
   AParser st CommType -> AParser st CommType -> AParser st CommType
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> CommType -> AParser st CommType
forall (m :: * -> *) a. Monad m => a -> m a
return (PROCESS_NAME -> CommType
CommTypeSort PROCESS_NAME
s)

-- | parse a possibly empty list of comm types within braces
bracedList :: AParser st [CommType]
bracedList :: AParser st [CommType]
bracedList = AParser st [CommType] -> AParser st [CommType]
forall st a. CharParser st a -> CharParser st a
braces (AParser st [CommType] -> AParser st [CommType])
-> AParser st [CommType] -> AParser st [CommType]
forall a b. (a -> b) -> a -> b
$ ParsecT String (AnnoState st) Identity CommType
-> ParsecT String (AnnoState st) Identity Token
-> AParser st [CommType]
forall s (m :: * -> *) t u a sep.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m sep -> ParsecT s u m [a]
sepBy ParsecT String (AnnoState st) Identity CommType
forall st. AParser st CommType
commType ParsecT String (AnnoState st) Identity Token
forall st. CharParser st Token
commaT

-- | parse a set of comm types possibly within braces or the empty set
alphabet :: AParser st [CommType]
alphabet :: AParser st [CommType]
alphabet = AParser st [CommType]
forall st. AParser st [CommType]
bracedList AParser st [CommType]
-> AParser st [CommType] -> AParser st [CommType]
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> ParsecT String (AnnoState st) Identity CommType
-> ParsecT String (AnnoState st) Identity Token
-> AParser st [CommType]
forall s (m :: * -> *) t u a sep.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m sep -> ParsecT s u m [a]
sepBy1 ParsecT String (AnnoState st) Identity CommType
forall st. AParser st CommType
commType ParsecT String (AnnoState st) Identity Token
forall st. CharParser st Token
commaT

procTail :: AParser st PROC_ALPHABET
procTail :: AParser st PROC_ALPHABET
procTail = ([CommType] -> PROC_ALPHABET)
-> ParsecT String (AnnoState st) Identity [CommType]
-> AParser st PROC_ALPHABET
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [CommType] -> PROC_ALPHABET
ProcAlphabet (ParsecT String (AnnoState st) Identity [CommType]
 -> AParser st PROC_ALPHABET)
-> ParsecT String (AnnoState st) Identity [CommType]
-> AParser st PROC_ALPHABET
forall a b. (a -> b) -> a -> b
$ AParser st Token
forall st. AParser st Token
colonT AParser st Token
-> ParsecT String (AnnoState st) Identity [CommType]
-> ParsecT String (AnnoState st) Identity [CommType]
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> ParsecT String (AnnoState st) Identity [CommType]
forall st. AParser st [CommType]
alphabet

procDecl :: AParser st FQ_PROCESS_NAME
procDecl :: AParser st FQ_PROCESS_NAME
procDecl = do
  PROCESS_NAME
pn <- AParser st PROCESS_NAME
forall st. AParser st PROCESS_NAME
processId
  [PROCESS_NAME]
argSorts <- GenParser Char (AnnoState st) [PROCESS_NAME]
-> GenParser Char (AnnoState st) [PROCESS_NAME]
forall tok st a. GenParser tok st [a] -> GenParser tok st [a]
optionL (GenParser Char (AnnoState st) [PROCESS_NAME]
 -> GenParser Char (AnnoState st) [PROCESS_NAME])
-> GenParser Char (AnnoState st) [PROCESS_NAME]
-> GenParser Char (AnnoState st) [PROCESS_NAME]
forall a b. (a -> b) -> a -> b
$ AParser st PROCESS_NAME
-> GenParser Char (AnnoState st) [PROCESS_NAME]
forall st a. AParser st a -> AParser st [a]
parenList AParser st PROCESS_NAME
forall st. AParser st PROCESS_NAME
cspSortId
  PROC_ALPHABET
al <- AParser st PROC_ALPHABET
forall st. AParser st PROC_ALPHABET
procTail
  {- BUG for the parse tree we should preserve the order of the decalred
  ccommunication alphabet. -}
  let alSet :: Set CommType
alSet = case PROC_ALPHABET
al of
        ProcAlphabet al' :: [CommType]
al' -> [CommType] -> Set CommType
forall a. Ord a => [a] -> Set a
Set.fromList [CommType]
al'
  FQ_PROCESS_NAME -> AParser st FQ_PROCESS_NAME
forall (m :: * -> *) a. Monad m => a -> m a
return (FQ_PROCESS_NAME -> AParser st FQ_PROCESS_NAME)
-> FQ_PROCESS_NAME -> AParser st FQ_PROCESS_NAME
forall a b. (a -> b) -> a -> b
$ PROCESS_NAME -> ProcProfile -> FQ_PROCESS_NAME
FQ_PROCESS_NAME PROCESS_NAME
pn ([PROCESS_NAME] -> Set CommType -> ProcProfile
ProcProfile [PROCESS_NAME]
argSorts Set CommType
alSet)

qualProc :: AParser st FQ_PROCESS_NAME
qualProc :: AParser st FQ_PROCESS_NAME
qualProc = do
    GenParser Char (AnnoState st) Token
-> GenParser Char (AnnoState st) Token
forall tok st a. GenParser tok st a -> GenParser tok st a
try (GenParser Char (AnnoState st) Token
forall st. CharParser st Token
oParenT GenParser Char (AnnoState st) Token
-> GenParser Char (AnnoState st) Token
-> GenParser Char (AnnoState st) Token
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> String -> GenParser Char (AnnoState st) Token
forall st. String -> AParser st Token
asKey String
processS)
    FQ_PROCESS_NAME
pd <- AParser st FQ_PROCESS_NAME
forall st. AParser st FQ_PROCESS_NAME
procDecl
    GenParser Char (AnnoState st) Token
forall st. CharParser st Token
cParenT
    FQ_PROCESS_NAME -> AParser st FQ_PROCESS_NAME
forall (m :: * -> *) a. Monad m => a -> m a
return FQ_PROCESS_NAME
pd

procDeclOrDefn :: AParser st (Either (FQ_PROCESS_NAME, [VAR])
    (PROCESS_NAME, Either [SORT] [VAR_DECL], PROC_ALPHABET))
procDeclOrDefn :: AParser
  st
  (Either
     (FQ_PROCESS_NAME, [Token])
     (PROCESS_NAME, Either [PROCESS_NAME] [VAR_DECL], PROC_ALPHABET))
procDeclOrDefn = do
    FQ_PROCESS_NAME
fqn <- AParser st FQ_PROCESS_NAME
forall st. AParser st FQ_PROCESS_NAME
qualProc
    [Token]
as <- GenParser Char (AnnoState st) [Token]
-> GenParser Char (AnnoState st) [Token]
forall tok st a. GenParser tok st [a] -> GenParser tok st [a]
optionL (GenParser Char (AnnoState st) [Token]
 -> GenParser Char (AnnoState st) [Token])
-> GenParser Char (AnnoState st) [Token]
-> GenParser Char (AnnoState st) [Token]
forall a b. (a -> b) -> a -> b
$ AParser st Token -> GenParser Char (AnnoState st) [Token]
forall st a. AParser st a -> AParser st [a]
parenList AParser st Token
forall st. AParser st Token
var
    AParser st Token
forall st. AParser st Token
equalT
    Either
  (FQ_PROCESS_NAME, [Token])
  (PROCESS_NAME, Either [PROCESS_NAME] [VAR_DECL], PROC_ALPHABET)
-> AParser
     st
     (Either
        (FQ_PROCESS_NAME, [Token])
        (PROCESS_NAME, Either [PROCESS_NAME] [VAR_DECL], PROC_ALPHABET))
forall (m :: * -> *) a. Monad m => a -> m a
return (Either
   (FQ_PROCESS_NAME, [Token])
   (PROCESS_NAME, Either [PROCESS_NAME] [VAR_DECL], PROC_ALPHABET)
 -> AParser
      st
      (Either
         (FQ_PROCESS_NAME, [Token])
         (PROCESS_NAME, Either [PROCESS_NAME] [VAR_DECL], PROC_ALPHABET)))
-> Either
     (FQ_PROCESS_NAME, [Token])
     (PROCESS_NAME, Either [PROCESS_NAME] [VAR_DECL], PROC_ALPHABET)
-> AParser
     st
     (Either
        (FQ_PROCESS_NAME, [Token])
        (PROCESS_NAME, Either [PROCESS_NAME] [VAR_DECL], PROC_ALPHABET))
forall a b. (a -> b) -> a -> b
$ (FQ_PROCESS_NAME, [Token])
-> Either
     (FQ_PROCESS_NAME, [Token])
     (PROCESS_NAME, Either [PROCESS_NAME] [VAR_DECL], PROC_ALPHABET)
forall a b. a -> Either a b
Left (FQ_PROCESS_NAME
fqn, [Token]
as)
  AParser
  st
  (Either
     (FQ_PROCESS_NAME, [Token])
     (PROCESS_NAME, Either [PROCESS_NAME] [VAR_DECL], PROC_ALPHABET))
-> AParser
     st
     (Either
        (FQ_PROCESS_NAME, [Token])
        (PROCESS_NAME, Either [PROCESS_NAME] [VAR_DECL], PROC_ALPHABET))
-> AParser
     st
     (Either
        (FQ_PROCESS_NAME, [Token])
        (PROCESS_NAME, Either [PROCESS_NAME] [VAR_DECL], PROC_ALPHABET))
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> do
    PROCESS_NAME
pn <- AParser st PROCESS_NAME
forall st. AParser st PROCESS_NAME
processId
    Maybe (Either [PROCESS_NAME] [VAR_DECL])
ma <- ParsecT
  String (AnnoState st) Identity (Either [PROCESS_NAME] [VAR_DECL])
-> ParsecT
     String
     (AnnoState st)
     Identity
     (Maybe (Either [PROCESS_NAME] [VAR_DECL]))
forall s (m :: * -> *) t u a.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m (Maybe a)
optionMaybe (ParsecT
   String (AnnoState st) Identity (Either [PROCESS_NAME] [VAR_DECL])
 -> ParsecT
      String
      (AnnoState st)
      Identity
      (Maybe (Either [PROCESS_NAME] [VAR_DECL])))
-> ParsecT
     String (AnnoState st) Identity (Either [PROCESS_NAME] [VAR_DECL])
-> ParsecT
     String
     (AnnoState st)
     Identity
     (Maybe (Either [PROCESS_NAME] [VAR_DECL]))
forall a b. (a -> b) -> a -> b
$ ParsecT
  String (AnnoState st) Identity (Either [PROCESS_NAME] [VAR_DECL])
-> ParsecT
     String (AnnoState st) Identity (Either [PROCESS_NAME] [VAR_DECL])
forall st a. AParser st a -> AParser st a
parens ParsecT
  String (AnnoState st) Identity (Either [PROCESS_NAME] [VAR_DECL])
forall st. AParser st (Either [PROCESS_NAME] [VAR_DECL])
manySortedVars
    Maybe PROC_ALPHABET
mal <- ParsecT String (AnnoState st) Identity PROC_ALPHABET
-> ParsecT String (AnnoState st) Identity (Maybe PROC_ALPHABET)
forall s (m :: * -> *) t u a.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m (Maybe a)
optionMaybe ParsecT String (AnnoState st) Identity PROC_ALPHABET
forall st. AParser st PROC_ALPHABET
procTail
    case Maybe PROC_ALPHABET
mal of
      Nothing -> do
        AParser st Token
forall st. AParser st Token
equalT
        case Maybe (Either [PROCESS_NAME] [VAR_DECL])
ma of
          Just (Left ss :: [PROCESS_NAME]
ss) | (PROCESS_NAME -> Bool) -> [PROCESS_NAME] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all PROCESS_NAME -> Bool
isSimpleId [PROCESS_NAME]
ss ->
             Either
  (FQ_PROCESS_NAME, [Token])
  (PROCESS_NAME, Either [PROCESS_NAME] [VAR_DECL], PROC_ALPHABET)
-> AParser
     st
     (Either
        (FQ_PROCESS_NAME, [Token])
        (PROCESS_NAME, Either [PROCESS_NAME] [VAR_DECL], PROC_ALPHABET))
forall (m :: * -> *) a. Monad m => a -> m a
return (Either
   (FQ_PROCESS_NAME, [Token])
   (PROCESS_NAME, Either [PROCESS_NAME] [VAR_DECL], PROC_ALPHABET)
 -> AParser
      st
      (Either
         (FQ_PROCESS_NAME, [Token])
         (PROCESS_NAME, Either [PROCESS_NAME] [VAR_DECL], PROC_ALPHABET)))
-> Either
     (FQ_PROCESS_NAME, [Token])
     (PROCESS_NAME, Either [PROCESS_NAME] [VAR_DECL], PROC_ALPHABET)
-> AParser
     st
     (Either
        (FQ_PROCESS_NAME, [Token])
        (PROCESS_NAME, Either [PROCESS_NAME] [VAR_DECL], PROC_ALPHABET))
forall a b. (a -> b) -> a -> b
$ (FQ_PROCESS_NAME, [Token])
-> Either
     (FQ_PROCESS_NAME, [Token])
     (PROCESS_NAME, Either [PROCESS_NAME] [VAR_DECL], PROC_ALPHABET)
forall a b. a -> Either a b
Left (PROCESS_NAME -> FQ_PROCESS_NAME
PROCESS_NAME PROCESS_NAME
pn, (PROCESS_NAME -> Token) -> [PROCESS_NAME] -> [Token]
forall a b. (a -> b) -> [a] -> [b]
map PROCESS_NAME -> Token
idToSimpleId [PROCESS_NAME]
ss)
          Nothing -> Either
  (FQ_PROCESS_NAME, [Token])
  (PROCESS_NAME, Either [PROCESS_NAME] [VAR_DECL], PROC_ALPHABET)
-> AParser
     st
     (Either
        (FQ_PROCESS_NAME, [Token])
        (PROCESS_NAME, Either [PROCESS_NAME] [VAR_DECL], PROC_ALPHABET))
forall (m :: * -> *) a. Monad m => a -> m a
return (Either
   (FQ_PROCESS_NAME, [Token])
   (PROCESS_NAME, Either [PROCESS_NAME] [VAR_DECL], PROC_ALPHABET)
 -> AParser
      st
      (Either
         (FQ_PROCESS_NAME, [Token])
         (PROCESS_NAME, Either [PROCESS_NAME] [VAR_DECL], PROC_ALPHABET)))
-> Either
     (FQ_PROCESS_NAME, [Token])
     (PROCESS_NAME, Either [PROCESS_NAME] [VAR_DECL], PROC_ALPHABET)
-> AParser
     st
     (Either
        (FQ_PROCESS_NAME, [Token])
        (PROCESS_NAME, Either [PROCESS_NAME] [VAR_DECL], PROC_ALPHABET))
forall a b. (a -> b) -> a -> b
$ (FQ_PROCESS_NAME, [Token])
-> Either
     (FQ_PROCESS_NAME, [Token])
     (PROCESS_NAME, Either [PROCESS_NAME] [VAR_DECL], PROC_ALPHABET)
forall a b. a -> Either a b
Left (PROCESS_NAME -> FQ_PROCESS_NAME
PROCESS_NAME PROCESS_NAME
pn, [])
          _ -> String
-> AParser
     st
     (Either
        (FQ_PROCESS_NAME, [Token])
        (PROCESS_NAME, Either [PROCESS_NAME] [VAR_DECL], PROC_ALPHABET))
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail "unexpected argument list"
      Just al :: PROC_ALPHABET
al -> case Maybe (Either [PROCESS_NAME] [VAR_DECL])
ma of
        Nothing -> do
          Maybe Token
me <- AParser st Token
-> ParsecT String (AnnoState st) Identity (Maybe Token)
forall s (m :: * -> *) t u a.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m (Maybe a)
optionMaybe AParser st Token
forall st. AParser st Token
equalT
          case Maybe Token
me of
            Nothing -> Either
  (FQ_PROCESS_NAME, [Token])
  (PROCESS_NAME, Either [PROCESS_NAME] [VAR_DECL], PROC_ALPHABET)
-> AParser
     st
     (Either
        (FQ_PROCESS_NAME, [Token])
        (PROCESS_NAME, Either [PROCESS_NAME] [VAR_DECL], PROC_ALPHABET))
forall (m :: * -> *) a. Monad m => a -> m a
return (Either
   (FQ_PROCESS_NAME, [Token])
   (PROCESS_NAME, Either [PROCESS_NAME] [VAR_DECL], PROC_ALPHABET)
 -> AParser
      st
      (Either
         (FQ_PROCESS_NAME, [Token])
         (PROCESS_NAME, Either [PROCESS_NAME] [VAR_DECL], PROC_ALPHABET)))
-> Either
     (FQ_PROCESS_NAME, [Token])
     (PROCESS_NAME, Either [PROCESS_NAME] [VAR_DECL], PROC_ALPHABET)
-> AParser
     st
     (Either
        (FQ_PROCESS_NAME, [Token])
        (PROCESS_NAME, Either [PROCESS_NAME] [VAR_DECL], PROC_ALPHABET))
forall a b. (a -> b) -> a -> b
$ (PROCESS_NAME, Either [PROCESS_NAME] [VAR_DECL], PROC_ALPHABET)
-> Either
     (FQ_PROCESS_NAME, [Token])
     (PROCESS_NAME, Either [PROCESS_NAME] [VAR_DECL], PROC_ALPHABET)
forall a b. b -> Either a b
Right (PROCESS_NAME
pn, [PROCESS_NAME] -> Either [PROCESS_NAME] [VAR_DECL]
forall a b. a -> Either a b
Left [], PROC_ALPHABET
al)
            Just _ -> Either
  (FQ_PROCESS_NAME, [Token])
  (PROCESS_NAME, Either [PROCESS_NAME] [VAR_DECL], PROC_ALPHABET)
-> AParser
     st
     (Either
        (FQ_PROCESS_NAME, [Token])
        (PROCESS_NAME, Either [PROCESS_NAME] [VAR_DECL], PROC_ALPHABET))
forall (m :: * -> *) a. Monad m => a -> m a
return (Either
   (FQ_PROCESS_NAME, [Token])
   (PROCESS_NAME, Either [PROCESS_NAME] [VAR_DECL], PROC_ALPHABET)
 -> AParser
      st
      (Either
         (FQ_PROCESS_NAME, [Token])
         (PROCESS_NAME, Either [PROCESS_NAME] [VAR_DECL], PROC_ALPHABET)))
-> Either
     (FQ_PROCESS_NAME, [Token])
     (PROCESS_NAME, Either [PROCESS_NAME] [VAR_DECL], PROC_ALPHABET)
-> AParser
     st
     (Either
        (FQ_PROCESS_NAME, [Token])
        (PROCESS_NAME, Either [PROCESS_NAME] [VAR_DECL], PROC_ALPHABET))
forall a b. (a -> b) -> a -> b
$ (PROCESS_NAME, Either [PROCESS_NAME] [VAR_DECL], PROC_ALPHABET)
-> Either
     (FQ_PROCESS_NAME, [Token])
     (PROCESS_NAME, Either [PROCESS_NAME] [VAR_DECL], PROC_ALPHABET)
forall a b. b -> Either a b
Right (PROCESS_NAME
pn, [VAR_DECL] -> Either [PROCESS_NAME] [VAR_DECL]
forall a b. b -> Either a b
Right [], PROC_ALPHABET
al)
        Just as :: Either [PROCESS_NAME] [VAR_DECL]
as -> case Either [PROCESS_NAME] [VAR_DECL]
as of
          Left ss :: [PROCESS_NAME]
ss -> Either
  (FQ_PROCESS_NAME, [Token])
  (PROCESS_NAME, Either [PROCESS_NAME] [VAR_DECL], PROC_ALPHABET)
-> AParser
     st
     (Either
        (FQ_PROCESS_NAME, [Token])
        (PROCESS_NAME, Either [PROCESS_NAME] [VAR_DECL], PROC_ALPHABET))
forall (m :: * -> *) a. Monad m => a -> m a
return (Either
   (FQ_PROCESS_NAME, [Token])
   (PROCESS_NAME, Either [PROCESS_NAME] [VAR_DECL], PROC_ALPHABET)
 -> AParser
      st
      (Either
         (FQ_PROCESS_NAME, [Token])
         (PROCESS_NAME, Either [PROCESS_NAME] [VAR_DECL], PROC_ALPHABET)))
-> Either
     (FQ_PROCESS_NAME, [Token])
     (PROCESS_NAME, Either [PROCESS_NAME] [VAR_DECL], PROC_ALPHABET)
-> AParser
     st
     (Either
        (FQ_PROCESS_NAME, [Token])
        (PROCESS_NAME, Either [PROCESS_NAME] [VAR_DECL], PROC_ALPHABET))
forall a b. (a -> b) -> a -> b
$ (PROCESS_NAME, Either [PROCESS_NAME] [VAR_DECL], PROC_ALPHABET)
-> Either
     (FQ_PROCESS_NAME, [Token])
     (PROCESS_NAME, Either [PROCESS_NAME] [VAR_DECL], PROC_ALPHABET)
forall a b. b -> Either a b
Right (PROCESS_NAME
pn, [PROCESS_NAME] -> Either [PROCESS_NAME] [VAR_DECL]
forall a b. a -> Either a b
Left [PROCESS_NAME]
ss, PROC_ALPHABET
al)
          Right vds :: [VAR_DECL]
vds -> do
            AParser st Token
forall st. AParser st Token
equalT
            Either
  (FQ_PROCESS_NAME, [Token])
  (PROCESS_NAME, Either [PROCESS_NAME] [VAR_DECL], PROC_ALPHABET)
-> AParser
     st
     (Either
        (FQ_PROCESS_NAME, [Token])
        (PROCESS_NAME, Either [PROCESS_NAME] [VAR_DECL], PROC_ALPHABET))
forall (m :: * -> *) a. Monad m => a -> m a
return (Either
   (FQ_PROCESS_NAME, [Token])
   (PROCESS_NAME, Either [PROCESS_NAME] [VAR_DECL], PROC_ALPHABET)
 -> AParser
      st
      (Either
         (FQ_PROCESS_NAME, [Token])
         (PROCESS_NAME, Either [PROCESS_NAME] [VAR_DECL], PROC_ALPHABET)))
-> Either
     (FQ_PROCESS_NAME, [Token])
     (PROCESS_NAME, Either [PROCESS_NAME] [VAR_DECL], PROC_ALPHABET)
-> AParser
     st
     (Either
        (FQ_PROCESS_NAME, [Token])
        (PROCESS_NAME, Either [PROCESS_NAME] [VAR_DECL], PROC_ALPHABET))
forall a b. (a -> b) -> a -> b
$ (PROCESS_NAME, Either [PROCESS_NAME] [VAR_DECL], PROC_ALPHABET)
-> Either
     (FQ_PROCESS_NAME, [Token])
     (PROCESS_NAME, Either [PROCESS_NAME] [VAR_DECL], PROC_ALPHABET)
forall a b. b -> Either a b
Right (PROCESS_NAME
pn, [VAR_DECL] -> Either [PROCESS_NAME] [VAR_DECL]
forall a b. b -> Either a b
Right [VAR_DECL]
vds, PROC_ALPHABET
al)