53d399c20374a99bd95db1f9b5b93980cbf6a984Christian MaederCopyright : (c) Till Mossakowski, Wiebke Herding, C. Maeder, Uni Bremen 2004
98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuLicense : GPLv2 or higher, see LICENSE.txt
34bff097c14521b5e57ce37279a34256e1f78aa5Klaus LuettichMaintainer : luecke@informatik.uni-bremen.de
2b4130336e941b7d01c78a6da55449a4c6eca609Till MossakowskiStability : provisional
2b4130336e941b7d01c78a6da55449a4c6eca609Till MossakowskiPortability : portable
f3a94a197960e548ecd6520bb768cb0d547457bbChristian MaederParser for modal logic extension of CASL
76647324ed70f33b95a881b536d883daccf9568dChristian Maedermodal_reserved_words :: [String]
180a3a4783d6d3cdeb9b9e61ec4f5111f95cfe23Christian Maedermodal_reserved_words =
180a3a4783d6d3cdeb9b9e61ec4f5111f95cfe23Christian Maeder diamondS : termS : rigidS : flexibleS : modalityS : [modalitiesS]
414ffa281d82f05a2d742c702f8e06b0cb05b229Christian MaedermodalFormula :: AParser st M_FORMULA
76647324ed70f33b95a881b536d883daccf9568dChristian MaedermodalFormula =
856bdbffc895793cc5739dbb862323944cb76fdbChristian Maeder do o <- oBracketT
856bdbffc895793cc5739dbb862323944cb76fdbChristian Maeder m <- modality []
856bdbffc895793cc5739dbb862323944cb76fdbChristian Maeder c <- cBracketT
626f5c8caee66bf5a5e2acbfa878dc17c0e25f96Christian Maeder f <- primFormula modal_reserved_words
61e38a4f194d3adc66646326c938eb9263a2f39bChristian Maeder return (BoxOrDiamond True m f $ toRange o [] c)
856bdbffc895793cc5739dbb862323944cb76fdbChristian Maeder do o <- asKey lessS
856bdbffc895793cc5739dbb862323944cb76fdbChristian Maeder m <- modality [greaterS] -- do not consume matching ">"!
856bdbffc895793cc5739dbb862323944cb76fdbChristian Maeder c <- asKey greaterS
626f5c8caee66bf5a5e2acbfa878dc17c0e25f96Christian Maeder f <- primFormula modal_reserved_words
61e38a4f194d3adc66646326c938eb9263a2f39bChristian Maeder return (BoxOrDiamond False m f $ toRange o [] c)
856bdbffc895793cc5739dbb862323944cb76fdbChristian Maeder do d <- asKey diamondS
626f5c8caee66bf5a5e2acbfa878dc17c0e25f96Christian Maeder f <- primFormula modal_reserved_words
856bdbffc895793cc5739dbb862323944cb76fdbChristian Maeder let p = tokPos d
b645cf3dc1e449038ed291bbd11fcc6e02b2fc7fChristian Maeder return (BoxOrDiamond False (Simple_mod $ Token emptyS p) f p)
414ffa281d82f05a2d742c702f8e06b0cb05b229Christian Maedermodality :: [String] -> AParser st MODALITY
d297778800daa7ceba73ad9b19884c883487dee7Christian Maeder do t <- term (ks ++ modal_reserved_words)
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder return $ Term_mod t
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder <|> return (Simple_mod $ mkSimpleId emptyS)
4ac9fad8454f66963e8985a41e061653147d4d60Christian Maederinstance TermParser M_FORMULA where
4ac9fad8454f66963e8985a41e061653147d4d60Christian Maeder termParser = aToTermParser modalFormula
414ffa281d82f05a2d742c702f8e06b0cb05b229Christian Maederrigor :: AParser st RIGOR
76647324ed70f33b95a881b536d883daccf9568dChristian Maederrigor = (asKey rigidS >> return Rigid)
e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian Maeder <|> (asKey flexibleS >> return Flexible)
414ffa281d82f05a2d742c702f8e06b0cb05b229Christian MaederrigidSigItems :: AParser st M_SIG_ITEM
76647324ed70f33b95a881b536d883daccf9568dChristian MaederrigidSigItems =
53d399c20374a99bd95db1f9b5b93980cbf6a984Christian Maeder do r <- rigor
4ac9fad8454f66963e8985a41e061653147d4d60Christian Maeder itemList modal_reserved_words opS opItem (Rigid_op_items r)
e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian Maeder <|> itemList modal_reserved_words predS predItem (Rigid_pred_items r)
53d399c20374a99bd95db1f9b5b93980cbf6a984Christian Maederinstance AParsable M_SIG_ITEM where
53d399c20374a99bd95db1f9b5b93980cbf6a984Christian Maeder aparser = rigidSigItems
414ffa281d82f05a2d742c702f8e06b0cb05b229Christian MaedermKey :: AParser st Token
5bc645bae86e7cc7714ab73934b77bb98ecbd078Christian MaedermKey = asKey modalityS <|> asKey modalitiesS
414ffa281d82f05a2d742c702f8e06b0cb05b229Christian MaedermBasic :: AParser st M_BASIC_ITEM
310532f8a7a1a1f1b6c25c67b7c340abc0889335Christian Maeder do (as, fs, ps) <- mItem simpleId
310532f8a7a1a1f1b6c25c67b7c340abc0889335Christian Maeder return (Simple_mod_decl as fs ps)
53d399c20374a99bd95db1f9b5b93980cbf6a984Christian Maeder do t <- asKey termS
310532f8a7a1a1f1b6c25c67b7c340abc0889335Christian Maeder (as, fs, ps) <- mItem (sortId modal_reserved_words)
42c01284bba8d7c8d995c8dfb96ace57d28ed1bcTill Mossakowski return (Term_mod_decl as fs (tokPos t `appRange` ps))
42c01284bba8d7c8d995c8dfb96ace57d28ed1bcTill MossakowskimItem :: AParser st a -> AParser st ([Annoted a], [AnModFORM], Range)
99cf1c277851e5ac7725b8b18980284d9e9aeb99Christian Maeder (as, cs) <- separatedBy (annoParser pr) anSemiOrComma
61e38a4f194d3adc66646326c938eb9263a2f39bChristian Maeder let ps = catRange $ c : cs
310532f8a7a1a1f1b6c25c67b7c340abc0889335Christian Maeder do o <- oBraceT
495330bf77fe4c742a31816b03251c9d29ae1efdChristian Maeder (fs, q) <- auxItemList (delete diamondS modal_reserved_words) []
180a3a4783d6d3cdeb9b9e61ec4f5111f95cfe23Christian Maeder (formula modal_reserved_words) (,)
180a3a4783d6d3cdeb9b9e61ec4f5111f95cfe23Christian Maeder return (as, fs, ps `appRange` q `appRange` toRange o [] p)
4ac9fad8454f66963e8985a41e061653147d4d60Christian Maeder <|> return (as, [], ps)
53d399c20374a99bd95db1f9b5b93980cbf6a984Christian Maederinstance AParsable M_BASIC_ITEM where
53d399c20374a99bd95db1f9b5b93980cbf6a984Christian Maeder aparser = mBasic