Parse_AS.hs revision c8780740df5c36654f22036278feefbf435538c4
60be96a6bed14ee4d7625e3d73040a74ca26321eCodruta GirleaModule : $Header$
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian MaederCopyright : (c) Till Mossakowski, Wiebke Herding, C. Maeder, Uni Bremen 2004
60be96a6bed14ee4d7625e3d73040a74ca26321eCodruta GirleaLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuMaintainer : luecke@informatik.uni-bremen.de
cb1bcdcebd18280e73151a05cf9846b940674518Codruta GirleaStability : provisional
60be96a6bed14ee4d7625e3d73040a74ca26321eCodruta GirleaPortability : portable
60be96a6bed14ee4d7625e3d73040a74ca26321eCodruta GirleaParser for modal logic extension of CASL
60be96a6bed14ee4d7625e3d73040a74ca26321eCodruta Girleamodal_reserved_words :: [String]
60be96a6bed14ee4d7625e3d73040a74ca26321eCodruta Girleamodal_reserved_words = diamondS:termS:rigidS:flexibleS:modalityS:[modalitiesS]
cb5be4f31df88b8137ef3cabf4e8b0ddec52f351Christian MaedermodalFormula :: AParser st M_FORMULA
60be96a6bed14ee4d7625e3d73040a74ca26321eCodruta GirleamodalFormula =
fd1c864a3dec70aa22ecb2bc85816ec8251c6decCodruta Girlea do o <- oBracketT
fd1c864a3dec70aa22ecb2bc85816ec8251c6decCodruta Girlea m <- modality []
60be96a6bed14ee4d7625e3d73040a74ca26321eCodruta Girlea c <- cBracketT
cb5be4f31df88b8137ef3cabf4e8b0ddec52f351Christian Maeder f <- primFormula modal_reserved_words
60be96a6bed14ee4d7625e3d73040a74ca26321eCodruta Girlea return (BoxOrDiamond True m f $ toPos o [] c)
b5fc3c116b803863fe86b55bb75b164d4029c696Christian Maeder do o <- asKey lessS
b5fc3c116b803863fe86b55bb75b164d4029c696Christian Maeder m <- modality [greaterS] -- do not consume matching ">"!
cb1bcdcebd18280e73151a05cf9846b940674518Codruta Girlea c <- asKey greaterS
cb1bcdcebd18280e73151a05cf9846b940674518Codruta Girlea f <- primFormula modal_reserved_words
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian Maeder return (BoxOrDiamond False m f $ toPos o [] c)
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian Maeder do d <- asKey diamondS
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian Maeder f <- primFormula modal_reserved_words
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian Maeder let p = tokPos d
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian Maeder return (BoxOrDiamond False (Simple_mod $ Token emptyS p) f p)
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian Maedermodality :: [String] -> AParser st MODALITY
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian Maeder do t <- term (ks ++ modal_reserved_words)
cb1bcdcebd18280e73151a05cf9846b940674518Codruta Girlea return $ Term_mod t
cb1bcdcebd18280e73151a05cf9846b940674518Codruta Girlea <|> return (Simple_mod $ mkSimpleId emptyS)
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian Maederinstance AParsable M_FORMULA where
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian Maeder aparser = modalFormula
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian Maederrigor :: AParser st RIGOR
cb5be4f31df88b8137ef3cabf4e8b0ddec52f351Christian Maederrigor = (asKey rigidS >> return Rigid)
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian Maeder <|> (asKey flexibleS >> return Flexible)
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian MaederrigidSigItems :: AParser st M_SIG_ITEM
cb1bcdcebd18280e73151a05cf9846b940674518Codruta GirlearigidSigItems =
2025793bdf95b956b34761af691fe9bde01f6d83Christian Maeder do r <- rigor
2025793bdf95b956b34761af691fe9bde01f6d83Christian Maeder do itemList modal_reserved_words opS opItem (Rigid_op_items r)
2025793bdf95b956b34761af691fe9bde01f6d83Christian Maeder <|> itemList modal_reserved_words predS predItem (Rigid_pred_items r)
2025793bdf95b956b34761af691fe9bde01f6d83Christian Maederinstance AParsable M_SIG_ITEM where
2025793bdf95b956b34761af691fe9bde01f6d83Christian Maeder aparser = rigidSigItems
cb1bcdcebd18280e73151a05cf9846b940674518Codruta GirleamKey :: AParser st Token
cb1bcdcebd18280e73151a05cf9846b940674518Codruta GirleamKey = asKey modalityS <|> asKey modalitiesS
2025793bdf95b956b34761af691fe9bde01f6d83Christian MaedermBasic :: AParser st M_BASIC_ITEM
2025793bdf95b956b34761af691fe9bde01f6d83Christian Maeder do (as, fs, ps) <- mItem simpleId
2025793bdf95b956b34761af691fe9bde01f6d83Christian Maeder return (Simple_mod_decl as fs ps)
2025793bdf95b956b34761af691fe9bde01f6d83Christian Maeder do t <- asKey termS
2025793bdf95b956b34761af691fe9bde01f6d83Christian Maeder (as, fs, ps) <- mItem (sortId modal_reserved_words)
2025793bdf95b956b34761af691fe9bde01f6d83Christian Maeder return (Term_mod_decl as fs (tokPos t `appRange` ps))
2025793bdf95b956b34761af691fe9bde01f6d83Christian MaedermItem :: AParser st a -> AParser st ([Annoted a], [AnModFORM], Range)
b5fc3c116b803863fe86b55bb75b164d4029c696Christian Maeder (as, cs) <- separatedBy (annoParser pr) anComma
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian Maeder let ps = catPos $ c : cs
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian Maeder do o <- oBraceT
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian Maeder (fs, qs) <- annoParser (formula modal_reserved_words)
2025793bdf95b956b34761af691fe9bde01f6d83Christian Maeder `separatedBy` anSemi
b5fc3c116b803863fe86b55bb75b164d4029c696Christian Maeder return (as, fs, ps `appRange` toPos o qs p)
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian Maeder <|> return (as, [], ps)
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian Maederinstance AParsable M_BASIC_ITEM where
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian Maeder aparser = mBasic