8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakova{- |

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina SojakovaModule : $Header$

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

097b7fb3f8f90e87120d30bf37a1d89fe0ddfaf0Kristina SojakovaLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakova

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina SojakovaMaintainer : luecke@informatik.uni-bremen.de

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovaStability : provisional

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovaPortability : portable

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovaParser for modal logic extension of CASL

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova-}

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakovamodule Modal.Parse_AS where

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakovaimport Common.AnnoState

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakovaimport Common.AS_Annotation

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakovaimport Common.Id

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakovaimport Common.Keywords

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakovaimport Common.Lexer

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakovaimport Common.Token

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakovaimport Modal.AS_Modal

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakovaimport Text.ParserCombinators.Parsec

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakovaimport CASL.Formula

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakovaimport CASL.OpItem

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakova

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakovamodal_reserved_words :: [String]

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakovamodal_reserved_words = diamondS:termS:rigidS:flexibleS:modalityS:[modalitiesS]

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovamodalFormula :: AParser st M_FORMULA

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina SojakovamodalFormula =

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakova do o <- oBracketT

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakova m <- modality []

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakova c <- cBracketT

cb5d588c4c3b286cc1e7210335d6ef7f584d79bcKristina Sojakova f <- primFormula modal_reserved_words

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

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakova <|>

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakova do o <- asKey lessS

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

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakova c <- asKey greaterS

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakova f <- primFormula modal_reserved_words

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

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakova <|>

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakova do d <- asKey diamondS

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakova f <- primFormula modal_reserved_words

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakova let p = tokPos d

cb5d588c4c3b286cc1e7210335d6ef7f584d79bcKristina Sojakova return (BoxOrDiamond False (Simple_mod $ Token emptyS p) f p)

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakova

81d28e8372831ae5e6054d8d2212f0114b09b79aKristina Sojakovamodality :: [String] -> AParser st MODALITY

81d28e8372831ae5e6054d8d2212f0114b09b79aKristina Sojakovamodality ks =

cb5d588c4c3b286cc1e7210335d6ef7f584d79bcKristina Sojakova do t <- term (ks ++ modal_reserved_words)

cb5d588c4c3b286cc1e7210335d6ef7f584d79bcKristina Sojakova return $ Term_mod t

cb5d588c4c3b286cc1e7210335d6ef7f584d79bcKristina Sojakova <|> return (Simple_mod $ mkSimpleId emptyS)

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakova

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakovainstance AParsable M_FORMULA where

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakova aparser = modalFormula

cb5d588c4c3b286cc1e7210335d6ef7f584d79bcKristina Sojakova

cb5d588c4c3b286cc1e7210335d6ef7f584d79bcKristina Sojakovarigor :: AParser st RIGOR

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakovarigor = (asKey rigidS >> return Rigid)

cb5d588c4c3b286cc1e7210335d6ef7f584d79bcKristina Sojakova <|> (asKey flexibleS >> return Flexible)

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakova

cb5d588c4c3b286cc1e7210335d6ef7f584d79bcKristina SojakovarigidSigItems :: AParser st M_SIG_ITEM

81d28e8372831ae5e6054d8d2212f0114b09b79aKristina SojakovarigidSigItems =

81d28e8372831ae5e6054d8d2212f0114b09b79aKristina Sojakova do r <- rigor

cb5d588c4c3b286cc1e7210335d6ef7f584d79bcKristina Sojakova do itemList modal_reserved_words opS opItem (Rigid_op_items r)

81d28e8372831ae5e6054d8d2212f0114b09b79aKristina Sojakova <|> itemList modal_reserved_words predS predItem (Rigid_pred_items r)

81d28e8372831ae5e6054d8d2212f0114b09b79aKristina Sojakova

81d28e8372831ae5e6054d8d2212f0114b09b79aKristina Sojakovainstance AParsable M_SIG_ITEM where

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakova aparser = rigidSigItems

81d28e8372831ae5e6054d8d2212f0114b09b79aKristina Sojakova

cb5d588c4c3b286cc1e7210335d6ef7f584d79bcKristina SojakovamKey :: AParser st Token

81d28e8372831ae5e6054d8d2212f0114b09b79aKristina SojakovamKey = asKey modalityS <|> asKey modalitiesS

81d28e8372831ae5e6054d8d2212f0114b09b79aKristina Sojakova

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovamBasic :: AParser st M_BASIC_ITEM

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina SojakovamBasic =

f2f62e61c66f678b0042d1a772ff89849d8b2113Kristina Sojakova do (as, fs, ps) <- mItem simpleId

f2f62e61c66f678b0042d1a772ff89849d8b2113Kristina Sojakova return (Simple_mod_decl as fs ps)

f2f62e61c66f678b0042d1a772ff89849d8b2113Kristina Sojakova <|>

f2f62e61c66f678b0042d1a772ff89849d8b2113Kristina Sojakova do t <- asKey termS

f2f62e61c66f678b0042d1a772ff89849d8b2113Kristina Sojakova (as, fs, ps) <- mItem (sortId modal_reserved_words)

f2f62e61c66f678b0042d1a772ff89849d8b2113Kristina Sojakova return (Term_mod_decl as fs (tokPos t `appRange` ps))

f2f62e61c66f678b0042d1a772ff89849d8b2113Kristina Sojakova

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovamItem :: AParser st a -> AParser st ([Annoted a], [AnModFORM], Range)

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovamItem pr = do

887a1999374d1fb3a534e602a8d322de6ef4c8e8Kristina Sojakova c <- mKey

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova (as, cs) <- separatedBy (annoParser pr) anComma

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova let ps = catRange $ c : cs

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova do o <- oBraceT

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova (fs, qs) <- annoParser (formula modal_reserved_words)

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova `separatedBy` anSemi

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova p <- cBraceT

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova return (as, fs, ps `appRange` toRange o qs p)

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova <|> return (as, [], ps)

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakovainstance AParsable M_BASIC_ITEM where

887a1999374d1fb3a534e602a8d322de6ef4c8e8Kristina Sojakova aparser = mBasic

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova