{- |
Module      :  ./CspCASL/Parse_CspCASL.hs
Description :  Parser for CspCASL specifications
Copyright   :  (c) Uni Bremen 2007
License     :  GPLv2 or higher, see LICENSE.txt

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

Parser for CSP-CASL specifications.
-}

module CspCASL.Parse_CspCASL (cspBasicExt) where

import Text.ParserCombinators.Parsec
import Common.AnnoState
import Common.Lexer

import CspCASL.AS_CspCASL
import CspCASL.CspCASL_Keywords
import CspCASL.Parse_CspCASL_Process

instance AParsable CspBasicExt where
  aparser :: AParser st CspBasicExt
aparser = AParser st CspBasicExt
forall st. AParser st CspBasicExt
cspBasicExt

cspBasicExt :: AParser st CspBasicExt
cspBasicExt :: AParser st CspBasicExt
cspBasicExt =
  [String]
-> String
-> ([String] -> AParser st CHANNEL_DECL)
-> ([Annoted CHANNEL_DECL] -> Range -> CspBasicExt)
-> AParser st CspBasicExt
forall st b a.
[String]
-> String
-> ([String] -> AParser st b)
-> ([Annoted b] -> Range -> a)
-> AParser st a
itemList [String]
cspKeywords String
channelS (AParser st CHANNEL_DECL -> [String] -> AParser st CHANNEL_DECL
forall a b. a -> b -> a
const AParser st CHANNEL_DECL
forall st. AParser st CHANNEL_DECL
chanDecl) [Annoted CHANNEL_DECL] -> Range -> CspBasicExt
Channels
  AParser st CspBasicExt
-> AParser st CspBasicExt -> AParser st CspBasicExt
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> do
    Token
p <- String -> AParser st Token
forall st. String -> AParser st Token
asKey String
processS
    [String]
-> [Token]
-> AParser st PROC_ITEM
-> ([Annoted PROC_ITEM] -> Range -> CspBasicExt)
-> AParser st CspBasicExt
forall st b a.
[String]
-> [Token]
-> AParser st b
-> ([Annoted b] -> Range -> a)
-> AParser st a
auxItemList [String]
cspStartKeys [Token
p] AParser st PROC_ITEM
forall st. AParser st PROC_ITEM
procItem [Annoted PROC_ITEM] -> Range -> CspBasicExt
ProcItems

chanDecl :: AParser st CHANNEL_DECL
chanDecl :: AParser st CHANNEL_DECL
chanDecl = do
  [CHANNEL_NAME]
vs <- CharParser (AnnoState st) CHANNEL_NAME
-> CharParser (AnnoState st) [CHANNEL_NAME]
forall st a. CharParser st a -> CharParser st [a]
commaSep1 CharParser (AnnoState st) CHANNEL_NAME
forall st. AParser st CHANNEL_NAME
channel_name
  AParser st Token
forall st. AParser st Token
colonT
  CHANNEL_NAME
es <- CharParser (AnnoState st) CHANNEL_NAME
forall st. AParser st CHANNEL_NAME
cspSortId
  CHANNEL_DECL -> AParser st CHANNEL_DECL
forall (m :: * -> *) a. Monad m => a -> m a
return ([CHANNEL_NAME] -> CHANNEL_NAME -> CHANNEL_DECL
ChannelDecl [CHANNEL_NAME]
vs CHANNEL_NAME
es)

procItem :: AParser st PROC_ITEM
procItem :: AParser st PROC_ITEM
procItem = do
  Either
  (FQ_PROCESS_NAME, [Token])
  (CHANNEL_NAME, Either [CHANNEL_NAME] [VAR_DECL], PROC_ALPHABET)
ep <- AParser
  st
  (Either
     (FQ_PROCESS_NAME, [Token])
     (CHANNEL_NAME, Either [CHANNEL_NAME] [VAR_DECL], PROC_ALPHABET))
forall st.
AParser
  st
  (Either
     (FQ_PROCESS_NAME, [Token])
     (CHANNEL_NAME, Either [CHANNEL_NAME] [VAR_DECL], PROC_ALPHABET))
procDeclOrDefn
  case Either
  (FQ_PROCESS_NAME, [Token])
  (CHANNEL_NAME, Either [CHANNEL_NAME] [VAR_DECL], PROC_ALPHABET)
ep of
    Left (fpn :: FQ_PROCESS_NAME
fpn, vs :: [Token]
vs) -> do
      PROCESS
p <- AParser st PROCESS
forall st. AParser st PROCESS
csp_casl_process
      PROC_ITEM -> AParser st PROC_ITEM
forall (m :: * -> *) a. Monad m => a -> m a
return (PROC_ITEM -> AParser st PROC_ITEM)
-> PROC_ITEM -> AParser st PROC_ITEM
forall a b. (a -> b) -> a -> b
$ PARM_PROCNAME -> PROCESS -> PROC_ITEM
Proc_Eq (FQ_PROCESS_NAME -> [Token] -> PARM_PROCNAME
ParmProcname FQ_PROCESS_NAME
fpn [Token]
vs) PROCESS
p
    Right (pn :: CHANNEL_NAME
pn, eas :: Either [CHANNEL_NAME] [VAR_DECL]
eas, al :: PROC_ALPHABET
al) -> case Either [CHANNEL_NAME] [VAR_DECL]
eas of
      Left ss :: [CHANNEL_NAME]
ss -> PROC_ITEM -> AParser st PROC_ITEM
forall (m :: * -> *) a. Monad m => a -> m a
return (PROC_ITEM -> AParser st PROC_ITEM)
-> PROC_ITEM -> AParser st PROC_ITEM
forall a b. (a -> b) -> a -> b
$ CHANNEL_NAME -> [CHANNEL_NAME] -> PROC_ALPHABET -> PROC_ITEM
Proc_Decl CHANNEL_NAME
pn [CHANNEL_NAME]
ss PROC_ALPHABET
al
      Right vds :: [VAR_DECL]
vds -> do
        PROCESS
p <- AParser st PROCESS
forall st. AParser st PROCESS
csp_casl_process
        PROC_ITEM -> AParser st PROC_ITEM
forall (m :: * -> *) a. Monad m => a -> m a
return (PROC_ITEM -> AParser st PROC_ITEM)
-> PROC_ITEM -> AParser st PROC_ITEM
forall a b. (a -> b) -> a -> b
$ CHANNEL_NAME -> [VAR_DECL] -> PROC_ALPHABET -> PROCESS -> PROC_ITEM
Proc_Defn CHANNEL_NAME
pn [VAR_DECL]
vds PROC_ALPHABET
al PROCESS
p