{- |

Module : $Header$

Copyright : (c) Till Mossakowski, Wiebke Herding, C. Maeder, Uni Bremen 2004

License : GPLv2 or higher, see LICENSE.txt

Maintainer : luecke@informatik.uni-bremen.de

Stability : provisional

Portability : portable

Parser for modal logic extension of CASL

-}

module Hybrid.Parse_AS where

import CASL.Formula

import CASL.OpItem

import Common.AS_Annotation

import Common.AnnoState

import Common.Id

import Common.Keywords

import Common.Lexer

import Common.Token

import Hybrid.AS_Hybrid

import Hybrid.Keywords

import Text.ParserCombinators.Parsec

hybrid_reserved_words :: [String]

hybrid_reserved_words = [

diamondS,

termS,

rigidS,

flexibleS,

modalityS,

modalitiesS,

nominalS,

nominalsS]

hybridFormula :: AParser st H_FORMULA

hybridFormula =

do

a <- asKey hereP

n <- nominal

return (Here n $ toRange a [] a)

<|>

do

a <- asKey asP

n <- nominal

f <- primFormula hybrid_reserved_words

return (At n f $ toRange a [] a)

<|>

do

a <- asKey exMark

n <- nominal

f <- primFormula hybrid_reserved_words

return (Univ n f $ toRange a [] a)

<|>

do

a <- asKey "?"

n <- nominal

f <- primFormula hybrid_reserved_words

return (Exist n f $ toRange a [] a)

<|>

do

o <- oBracketT

m <- modality []

c <- cBracketT

f <- primFormula hybrid_reserved_words

return (BoxOrDiamond True m f $ toRange o [] c)

<|>

do

o <- asKey lessS

m <- modality [greaterS] -- do not consume matching ">"!

c <- asKey greaterS

f <- primFormula hybrid_reserved_words

return (BoxOrDiamond False m f $ toRange o [] c)

nominal :: AParser st NOMINAL

nominal =

do

n <- simpleId

return (Simple_nom n)

modality :: [String] -> AParser st MODALITY

modality ks =

do t <- term (ks ++ hybrid_reserved_words)

return $ Term_mod t

instance TermParser H_FORMULA where

termParser = aToTermParser hybridFormula

rigor :: AParser st RIGOR

rigor = (asKey rigidS >> return Rigid)

<|> (asKey flexibleS >> return Flexible)

rigidSigItems :: AParser st H_SIG_ITEM

rigidSigItems =

do r <- rigor

itemList hybrid_reserved_words opS opItem (Rigid_op_items r)

<|> itemList hybrid_reserved_words predS predItem (Rigid_pred_items r)

instance AParsable H_SIG_ITEM where

aparser = rigidSigItems

hKey :: AParser st Token

hKey = asKey modalityS <|> asKey modalitiesS

hKey' :: AParser st Token

hKey' = asKey nominalS <|> asKey nominalsS

hBasic :: AParser st H_BASIC_ITEM

hBasic =

do (as, fs, ps) <- hItem'' hKey simpleId

return (Simple_mod_decl as fs ps)

<|>

do (as, fs, ps) <- hItem'' hKey' simpleId

return (Simple_nom_decl as fs ps)

hItem'' :: AParser st Token -> AParser st a ->

AParser st ([Annoted a], [AnHybFORM], Range)

hItem'' k pr = do

c <- k

(as, cs) <- separatedBy (annoParser pr) anSemiOrComma

let ps = catRange $ c : cs

return (as, [], ps)

instance AParsable H_BASIC_ITEM where

aparser = hBasic