hets/CspCASL/Parse_CspCASL.hs

	Parse_CspCASL.hs revision 53f89daf88665d3ea96d871110a5c0d9d8326bd2
{- |
Module      :  $Id$
Description :  Parser for CspCASL specifications
Copyright   :  (c) Uni Bremen 2007
License     :  similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt

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

Parser for CSP-CASL specifications.
-}

module CspCASL.Parse_CspCASL (
    cspBasicSpec
) where

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

import Common.AnnoState (AParser, asKey, colonT, equalT, anSemi)
import Common.Id (genName)
import Common.Lexer (commaSep1, cParenT, oParenT)

import CspCASL.AS_CspCASL
import CspCASL.AS_CspCASL_Process
import CspCASL.Core_CspCASL
import CspCASL.CspCASL_Keywords
import CspCASL.Parse_CspCASL_Process

cspBasicSpec :: AParser st CspBasicSpec
cspBasicSpec = do
    chans <- option [] $ do
                 choice [asKey channelS, asKey channelsS]
                 cds <- chanDecl `sepBy` anSemi
                 -- XXX how to have an _optional_ final semicolon here?
                 return cds
    items <- processItems
    return (basicToCore (CspBasicSpec chans items))

chanDecl :: AParser st CHANNEL_DECL
chanDecl = do vs <- commaSep1 channel_name
              colonT
              es <- csp_casl_sort
              return (ChannelDecl vs es)

processItems :: AParser st [PROC_ITEM]
processItems = do asKey processS
                  procItems <|> fmap singleProcess csp_casl_process

-- Turn an unnamed singleton process into a declaration/equation.
singleProcess :: PROCESS -> [PROC_ITEM]
singleProcess p =
    [ProcDecl singletonProcessName [] singletonProcessSort,
     ProcEq (ParmProcname singletonProcessName []) p]
        where singletonProcessName = genName "P"
              singletonProcessSort = genName "singletonProcessSort"

procItems :: AParser st [PROC_ITEM]
procItems = many1 procItem

procItem :: AParser st PROC_ITEM
procItem = try (do pdcl <- procDecl
                   return pdcl)
           <|> (do peq <- procEq
                   return peq)

procDecl :: AParser st PROC_ITEM
procDecl = do
    pn <- process_name
    parms <- option [] $ do
               try oParenT
               parms <- commaSep1 csp_casl_sort
               cParenT
               return parms
    colonT
    s <- csp_casl_sort
    return (ProcDecl pn parms s)

procEq :: AParser st PROC_ITEM
procEq = do
    pn <- parmProcname
    equalT
    p <- csp_casl_process
    return (ProcEq 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)