AS_Modal.der.hs revision f7d2e793728bbb7fd185e027eb9dfd7b9dd11c21
2a693c01b154f1e25931ff6c754d2d02096e2662Till MossakowskiModule : $Header$
e9458b1a7a19a63aa4c179f9ab20f4d50681c168Jens ElknerCopyright : (c) Till Mossakowski, Wiebke Herding, C. Maeder, Uni Bremen 2004
4c7f058cdd19ce67b2b5d4b7f69703d0f8a21e38Christian MaederLicence : similar to LGPL, see HetCATS/LICENCE.txt or LIZENZ.txt
98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuMaintainer : hets@tzi.de
2a693c01b154f1e25931ff6c754d2d02096e2662Till MossakowskiStability : provisional
34bff097c14521b5e57ce37279a34256e1f78aa5Klaus LuettichPortability : portable
2a693c01b154f1e25931ff6c754d2d02096e2662Till Mossakowski Abstract syntax for modal logic extension of CASL
2a693c01b154f1e25931ff6c754d2d02096e2662Till Mossakowski Only the added syntax is specified
3a761fd74f4f3c5587a199553c0ee7383e5d8ff3Christian Maeder-- DrIFT command
a10ff6125d62484ec5961c8a5d9d1c5a3e14fa66Christian Maeder{-! global: UpPos !-}
a10ff6125d62484ec5961c8a5d9d1c5a3e14fa66Christian Maedertype M_BASIC_SPEC = BASIC_SPEC M_BASIC_ITEM M_SIG_ITEM M_FORMULA
a10ff6125d62484ec5961c8a5d9d1c5a3e14fa66Christian Maedertype AnModFORM = Annoted (FORMULA M_FORMULA)
2a693c01b154f1e25931ff6c754d2d02096e2662Till Mossakowskidata M_BASIC_ITEM = Simple_mod_decl [Annoted SIMPLE_ID] [AnModFORM] [Pos]
2a693c01b154f1e25931ff6c754d2d02096e2662Till Mossakowski | Term_mod_decl [Annoted SORT] [AnModFORM] [Pos]
3a761fd74f4f3c5587a199553c0ee7383e5d8ff3Christian Maeder deriving (Eq, Show)
3a761fd74f4f3c5587a199553c0ee7383e5d8ff3Christian Maederdata RIGOR = Rigid | Flexible deriving (Eq, Show)
50dce6b011347f92377adb8bbabaeeb80975e86dChristian Maederdata M_SIG_ITEM =
c74040e2ca9d0534d0c4244f69a3e76a01341f05Klaus Luettich Rigid_op_items RIGOR [Annoted (OP_ITEM M_FORMULA)] [Pos]
99cf1c277851e5ac7725b8b18980284d9e9aeb99Christian Maeder -- pos: op, semi colons
81101b83a042f5a1bdeeef93b1b49aff05817e44Christian Maeder | Rigid_pred_items RIGOR [Annoted (PRED_ITEM M_FORMULA)] [Pos]
a10ff6125d62484ec5961c8a5d9d1c5a3e14fa66Christian Maeder -- pos: pred, semi colons
2a693c01b154f1e25931ff6c754d2d02096e2662Till Mossakowski deriving (Eq, Show)
99cf1c277851e5ac7725b8b18980284d9e9aeb99Christian Maederdata MODALITY = Simple_mod SIMPLE_ID | Term_mod (TERM M_FORMULA)
7c757dd5b0b027dfc0cd0b9535758c8992cdde2fChristian Maeder deriving (Eq, Ord, Show)
7c757dd5b0b027dfc0cd0b9535758c8992cdde2fChristian Maederdata M_FORMULA = BoxOrDiamond Bool MODALITY (FORMULA M_FORMULA) [Pos]
7c757dd5b0b027dfc0cd0b9535758c8992cdde2fChristian Maeder -- The identifier and the term specify the kind of the modality
7c757dd5b0b027dfc0cd0b9535758c8992cdde2fChristian Maeder -- pos: "[]" or "<>", True if Box, False if Diamond
7c757dd5b0b027dfc0cd0b9535758c8992cdde2fChristian Maeder deriving (Eq, Ord, Show)
3a761fd74f4f3c5587a199553c0ee7383e5d8ff3Christian MaedermodalityS, modalitiesS, flexibleS, rigidS, termS, emptyS, diamondS, greaterS
3a761fd74f4f3c5587a199553c0ee7383e5d8ff3Christian MaedermodalityS = "modality"
2a693c01b154f1e25931ff6c754d2d02096e2662Till MossakowskimodalitiesS = init modalityS ++ "ies"
86b1d0c80abdd4ca36491cf7025b718a5fea5080Christian MaederflexibleS = "flexible"
86b1d0c80abdd4ca36491cf7025b718a5fea5080Christian MaederrigidS = "rigid"
86b1d0c80abdd4ca36491cf7025b718a5fea5080Christian MaedertermS = "term"
a65c6747c9acbbebc93baba7bae94d2e3d8cdafbTill MossakowskiemptyS = "empty"
4c7f058cdd19ce67b2b5d4b7f69703d0f8a21e38Christian MaederdiamondS = "<>"
4c7f058cdd19ce67b2b5d4b7f69703d0f8a21e38Christian MaedergreaterS = ">"
c2db39a683438b0f3d484519f4c93db26eec9d2eWiebke Herdingmodal_reserved_words :: [String]
2a693c01b154f1e25931ff6c754d2d02096e2662Till Mossakowskimodal_reserved_words = diamondS:termS:rigidS:flexibleS:modalityS:[modalitiesS]