Parse_AS.hs revision 5bc645bae86e7cc7714ab73934b77bb98ecbd078
e9458b1a7a19a63aa4c179f9ab20f4d50681c168Jens ElknerModule : $Header$
e6d40133bc9f858308654afb1262b8b483ec5922Till MossakowskiCopyright : (c) Till Mossakowski, Wiebke Herding, C. Maeder, Uni Bremen 2004
333780eae2be9f20fe46dedbf5eb46ffa0cbfd02Christian MaederLicence : All rights reserved.
120eec9ff1748e1ae786e2ab073234198bc0f701Christian MaederMaintainer : hets@tzi.de
cfbd735270fe52115cef0508d265785efcb99cd7Christian MaederStability : provisional
120eec9ff1748e1ae786e2ab073234198bc0f701Christian MaederPortability : portable
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder Parser for modal logic extension of CASL
54a0a1e10bd93721cf52dbd9b816c8f108997ec0Christian MaedermodalFormula :: AParser M_FORMULA
d6a6c1a2fb6526fdcacd8386c9aa3340169a1049Cui JianmodalFormula =
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder do o <- oBracketT
c208973c890b8f993297720fd0247bc7481d4304Christian Maeder m <- modality []
55c5e901b5c3466300009135585bc70bd576dcb6Christian Maeder c <- cBracketT
7308170a663b06590b9ca5c9470baafbbf411f35Christian Maeder f <- formula modal_reserved_words
697e63e30aa3c309a1ef1f9357745111f8dfc5a9Christian Maeder return (Box m f $ toPos o [] c)
54a0a1e10bd93721cf52dbd9b816c8f108997ec0Christian Maeder do o <- asKey lessS
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder m <- modality [greaterS] -- do not consume matching ">"!
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder c <- asKey greaterS
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder f <- formula modal_reserved_words
0a5165c161ce13d434b5c0488b533a8de98aafaaChristian Maeder return (Diamond m f $ toPos o [] c)
c4df2219ea6f47a5e510503e475c38362e8464ebChristian Maeder do d <- asKey diamondS
04d04d19fdd5320953c78ad5b6d2d11f85bc4bcfChristian Maeder f <- formula modal_reserved_words
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder let p = tokPos d
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder return (Diamond (Simple_mod $ Token emptyS p) f [p])
120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maedermodality :: [String] -> AParser MODALITY
afddef51d985ac2ea76a6bd846f04cbbc4311305Razvan Pascanu do t <- term (ks ++ modal_reserved_words)
99e6fb75f064189db8f26fe74eb8f01af353e58eCui Jian return $ Term_mod t
99e6fb75f064189db8f26fe74eb8f01af353e58eCui Jian <|> return (Simple_mod $ mkSimpleId emptyS)
99e6fb75f064189db8f26fe74eb8f01af353e58eCui Jianinstance AParsable M_FORMULA where
99e6fb75f064189db8f26fe74eb8f01af353e58eCui Jian aparser = modalFormula
99e6fb75f064189db8f26fe74eb8f01af353e58eCui Jianrigor :: AParser RIGOR
17d4f8c5576d93f36cafe68161cdb960ec49ce7cChristian Maederrigor = (asKey rigidS >> return Rigid)
99e6fb75f064189db8f26fe74eb8f01af353e58eCui Jian <|> (asKey flexibleS >> return Flexible)
6948b7295a0521212803f15cf919395d2073e2c9Christian MaederrigidSigItems :: AParser M_SIG_ITEM
6948b7295a0521212803f15cf919395d2073e2c9Christian MaederrigidSigItems =
6948b7295a0521212803f15cf919395d2073e2c9Christian Maeder do r <- rigor
4b136ad539bd9f4e115dff4eee4d552a42d4437eChristian Maeder do itemList modal_reserved_words opS opItem (Rigid_op_items r)
7308170a663b06590b9ca5c9470baafbbf411f35Christian Maeder <|> itemList modal_reserved_words predS predItem (Rigid_pred_items r)
4b136ad539bd9f4e115dff4eee4d552a42d4437eChristian Maederinstance AParsable M_SIG_ITEM where
d6a6c1a2fb6526fdcacd8386c9aa3340169a1049Cui Jian aparser = rigidSigItems
99e6fb75f064189db8f26fe74eb8f01af353e58eCui JianmKey :: AParser Token
99e6fb75f064189db8f26fe74eb8f01af353e58eCui JianmKey = asKey modalityS <|> asKey modalitiesS
99e6fb75f064189db8f26fe74eb8f01af353e58eCui JianmBasic :: AParser M_BASIC_ITEM
afe76697dd6888856a066934a1112a38809b27faChristian Maeder do (as, fs, ps) <- mItem simpleId
99e6fb75f064189db8f26fe74eb8f01af353e58eCui Jian return (Simple_mod_decl as fs ps)
afe76697dd6888856a066934a1112a38809b27faChristian Maeder do t <- asKey termS
afe76697dd6888856a066934a1112a38809b27faChristian Maeder (as, fs, ps) <- mItem (sortId modal_reserved_words)
4b136ad539bd9f4e115dff4eee4d552a42d4437eChristian Maeder return (Term_mod_decl as fs (tokPos t : ps))
290674793b16476e77c99fcf6cadecdb7b2947c9Christian MaedermItem :: AParser a -> AParser ([Annoted a], [AnModFORM], [Pos])
290674793b16476e77c99fcf6cadecdb7b2947c9Christian Maeder (as, ps) <- auxItemList (modal_reserved_words ++ startKeyword)
17d4f8c5576d93f36cafe68161cdb960ec49ce7cChristian Maeder do o <- oBraceT
17d4f8c5576d93f36cafe68161cdb960ec49ce7cChristian Maeder (fs, qs) <- annoParser (formula modal_reserved_words)
99e6fb75f064189db8f26fe74eb8f01af353e58eCui Jian `separatedBy` anSemi
7308170a663b06590b9ca5c9470baafbbf411f35Christian Maeder return (as, fs, ps ++ toPos o qs p)
4b136ad539bd9f4e115dff4eee4d552a42d4437eChristian Maeder <|> return (as, [], ps)
d6a6c1a2fb6526fdcacd8386c9aa3340169a1049Cui Jianinstance AParsable M_BASIC_ITEM where
99e6fb75f064189db8f26fe74eb8f01af353e58eCui Jian aparser = mBasic