faf8ae9e57aecf780f77f114de886af4c1a0f0ccChristian Maeder{- |

faf8ae9e57aecf780f77f114de886af4c1a0f0ccChristian MaederModule : $Id$

faf8ae9e57aecf780f77f114de886af4c1a0f0ccChristian MaederDescription : Parser for CspCASL specifications

faf8ae9e57aecf780f77f114de886af4c1a0f0ccChristian MaederCopyright : (c) Uni Bremen 2007

faf8ae9e57aecf780f77f114de886af4c1a0f0ccChristian MaederLicense : GPLv2 or higher, see LICENSE.txt

aa1c971871ba8f793a9e2e62189369cbfbbe0054Christian Maeder

9db48b4604636bfdf03e60890fc094b7bec775dcChristian MaederMaintainer : a.m.gimblett@swan.ac.uk

9db48b4604636bfdf03e60890fc094b7bec775dcChristian MaederStability : experimental

9db48b4604636bfdf03e60890fc094b7bec775dcChristian MaederPortability : portable

faf8ae9e57aecf780f77f114de886af4c1a0f0ccChristian Maeder

Parser for CSP-CASL specifications.

-}

module CspCASL.Parse_CspCASL (

cspBasicSpec

) where

import Text.ParserCombinators.Parsec (choice, many1, try, (<|>),

option, sepBy)

import Common.AS_Annotation(Annoted (..), emptyAnno)

import Common.AnnoState (AParser, asKey, colonT, equalT, anSemi, allAnnoParser)

import Common.Id

import Common.Lexer (commaSep1, cParenT, oParenT)

import CspCASL.AS_CspCASL

import CspCASL.AS_CspCASL_Process

import CspCASL.CspCASL_Keywords

import CspCASL.Parse_CspCASL_Process

cspBasicSpec :: AParser st CspBasicSpec

cspBasicSpec = do chans <- option [] $ chanDecls

items <- processItems

return (CspBasicSpec chans items)

chanDecls :: AParser st [CHANNEL_DECL]

chanDecls = do choice [asKey channelS, asKey channelsS]

cds <- chanDecl `sepBy` anSemi

-- XXX optional final semicolon how?

return cds

chanDecl :: AParser st CHANNEL_DECL

chanDecl = do vs <- commaSep1 channel_name

colonT

es <- csp_casl_sort

return (ChannelDecl vs es)

processItems :: AParser st [Annoted PROC_ITEM]

processItems = do asKey processS

procItems <|> fmap singleProcess csp_casl_process

-- Turn an unnamed singleton process into a declaration/equation. THIS WHOLE

-- functions seems odd. Why would we want a fixed process "P" which communicates

-- over sort "singletonProcessSort". BUG?

singleProcess :: PROCESS -> [Annoted PROC_ITEM]

singleProcess p =

map emptyAnno [Proc_Decl singletonProcessName [] singletonProcessAlpha,

Proc_Eq (ParmProcname (PROCESS_NAME singletonProcessName) []) p]

where singletonProcessName = mkSimpleId "P"

singletonProcessAlpha =

(ProcAlphabet [mkSimpleId "singletonProcessSort"]

nullRange)

procItems :: AParser st [Annoted PROC_ITEM]

procItems = many1 procItem

procItem :: AParser st (Annoted PROC_ITEM)

procItem = try procDecl

<|> procEq

procDecl :: AParser st (Annoted PROC_ITEM)

procDecl = do (pn, parms, comms) <- procNameWithParamsAndComms

anSemi

-- We don't currently allow annotations on declarations

return (emptyAnno $ Proc_Decl pn parms comms)

procEq :: AParser st (Annoted PROC_ITEM)

procEq = allAnnoParser $

do pn <- parmProcname

equalT

p <- csp_casl_process

return (Proc_Eq pn p)

parmProcname :: AParser st PARM_PROCNAME

parmProcname = do pn <- process_name

pv <- option [] $ do try oParenT

vs <- commaSep1 var

cParenT

return vs

return (ParmProcname pn pv)