55cf6e01272ec475edea32aa9b7923de2d36cb42Christian Maeder{-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances, FlexibleInstances #-}
4c7f058cdd19ce67b2b5d4b7f69703d0f8a21e38Christian MaederDescription : Instance of class Logic for Modal CASL
2a693c01b154f1e25931ff6c754d2d02096e2662Till MossakowskiCopyright : (c) Till Mossakowski, Uni Bremen 2002-2004
98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuLicense : GPLv2 or higher, see LICENSE.txt
34bff097c14521b5e57ce37279a34256e1f78aa5Klaus LuettichMaintainer : luecke@informatik.uni-bremen.de
2a693c01b154f1e25931ff6c754d2d02096e2662Till MossakowskiStability : provisional
2a693c01b154f1e25931ff6c754d2d02096e2662Till MossakowskiPortability : portable
f3a94a197960e548ecd6520bb768cb0d547457bbChristian MaederInstance of class Logic for modal logic.
2a693c01b154f1e25931ff6c754d2d02096e2662Till Mossakowskidata Modal = Modal deriving Show
99cf1c277851e5ac7725b8b18980284d9e9aeb99Christian Maederinstance Language Modal where
7c757dd5b0b027dfc0cd0b9535758c8992cdde2fChristian Maeder description _ = unlines
602041e384342ea908c976a298e8b47774d3500cTill Mossakowski [ "ModalCASL extends CASL by modal operators."
602041e384342ea908c976a298e8b47774d3500cTill Mossakowski , "Syntax for ordinary"
7c757dd5b0b027dfc0cd0b9535758c8992cdde2fChristian Maeder , "modalities, multi-modal logics as well as term-modal"
7c757dd5b0b027dfc0cd0b9535758c8992cdde2fChristian Maeder , "logic (also covering dynamic logic) is provided."
7c757dd5b0b027dfc0cd0b9535758c8992cdde2fChristian Maeder , "Specific modal logics can be obtained via restrictions to"
7c757dd5b0b027dfc0cd0b9535758c8992cdde2fChristian Maeder , "sublanguages." ]
3a761fd74f4f3c5587a199553c0ee7383e5d8ff3Christian Maedertype MSign = Sign M_FORMULA ModalSign
9eb39c7a0e7a1ddad1eec1d23c6d4e3a99c54023Christian Maedertype ModalMor = Morphism M_FORMULA ModalSign (DefMorExt ModalSign)
3a761fd74f4f3c5587a199553c0ee7383e5d8ff3Christian Maedertype ModalFORMULA = FORMULA M_FORMULA
86b1d0c80abdd4ca36491cf7025b718a5fea5080Christian Maederinstance SignExtension ModalSign where
86b1d0c80abdd4ca36491cf7025b718a5fea5080Christian Maeder isSubSignExtension = isSubModalSign
a65c6747c9acbbebc93baba7bae94d2e3d8cdafbTill Mossakowskiinstance Syntax Modal M_BASIC_SPEC Symbol SYMB_ITEMS SYMB_MAP_ITEMS where
4c7f058cdd19ce67b2b5d4b7f69703d0f8a21e38Christian Maeder parse_basic_spec Modal = Just $ basicSpec modal_reserved_words
4c7f058cdd19ce67b2b5d4b7f69703d0f8a21e38Christian Maeder parse_symb_items Modal = Just $ symbItems modal_reserved_words
4c7f058cdd19ce67b2b5d4b7f69703d0f8a21e38Christian Maeder parse_symb_map_items Modal = Just $ symbMapItems modal_reserved_words
2a693c01b154f1e25931ff6c754d2d02096e2662Till Mossakowski-- Modal logic
9eb39c7a0e7a1ddad1eec1d23c6d4e3a99c54023Christian Maedermap_M_FORMULA :: MapSen M_FORMULA ModalSign (DefMorExt ModalSign)
f7d2e793728bbb7fd185e027eb9dfd7b9dd11c21Christian Maedermap_M_FORMULA mor (BoxOrDiamond b m f ps) =
e85b224577b78d08ba5c39fe9dcc2e53995454a2Christian Maeder let newM = case m of
f7d2e793728bbb7fd185e027eb9dfd7b9dd11c21Christian Maeder Simple_mod _ -> m
f7d2e793728bbb7fd185e027eb9dfd7b9dd11c21Christian Maeder Term_mod t -> let newT = mapTerm map_M_FORMULA mor t
f7d2e793728bbb7fd185e027eb9dfd7b9dd11c21Christian Maeder in Term_mod newT
f7d2e793728bbb7fd185e027eb9dfd7b9dd11c21Christian Maeder newF = mapSen map_M_FORMULA mor f
e85b224577b78d08ba5c39fe9dcc2e53995454a2Christian Maeder in BoxOrDiamond b newM newF ps
cd6e5706893519bfcf24539afa252fcbed5097ddKlaus Luettichinstance Sentences Modal ModalFORMULA MSign ModalMor Symbol where
f7d2e793728bbb7fd185e027eb9dfd7b9dd11c21Christian Maeder map_sen Modal m = return . mapSen map_M_FORMULA m
2a693c01b154f1e25931ff6c754d2d02096e2662Till Mossakowski sym_of Modal = symOf
2a693c01b154f1e25931ff6c754d2d02096e2662Till Mossakowski symmap_of Modal = morphismToSymbMap
2a693c01b154f1e25931ff6c754d2d02096e2662Till Mossakowski sym_name Modal = symName
bec7e681b0ba4d085638ec7af0cf7ae5068840caChristian Maeder simplify_sen Modal = simplifySen minExpForm simModal
5824312cc0cfccce61f195fbe92307a21a467049Christian Maeder print_sign Modal sig = printSign
a10ff6125d62484ec5961c8a5d9d1c5a3e14fa66Christian Maeder (printModalSign $ simplifySen minExpForm simModal sig) sig
99cf1c277851e5ac7725b8b18980284d9e9aeb99Christian Maeder print_named Modal = printTheoryFormula
e85b224577b78d08ba5c39fe9dcc2e53995454a2Christian Maeder-- simplifySen for ExtFORMULA
0d9160e906743b226d4768707f84151ab6c66253Heng JiangsimModal :: Sign M_FORMULA ModalSign -> M_FORMULA -> M_FORMULA
f7d2e793728bbb7fd185e027eb9dfd7b9dd11c21Christian MaedersimModal sign (BoxOrDiamond b md form pos) =
f7d2e793728bbb7fd185e027eb9dfd7b9dd11c21Christian Maeder let mod' = case md of
e85b224577b78d08ba5c39fe9dcc2e53995454a2Christian Maeder Term_mod term -> Term_mod $ rmTypesT minExpForm
bec7e681b0ba4d085638ec7af0cf7ae5068840caChristian Maeder simModal sign term
e85b224577b78d08ba5c39fe9dcc2e53995454a2Christian Maeder in BoxOrDiamond b mod'
bec7e681b0ba4d085638ec7af0cf7ae5068840caChristian Maeder (simplifySen minExpForm simModal sign form) pos
f7d2e793728bbb7fd185e027eb9dfd7b9dd11c21Christian MaederrmTypesExt :: a -> b -> b
f6c04b8534762854072795add026d4551156a410Heng JiangrmTypesExt _ f = f
cd6e5706893519bfcf24539afa252fcbed5097ddKlaus Luettichinstance StaticAnalysis Modal M_BASIC_SPEC ModalFORMULA
2a693c01b154f1e25931ff6c754d2d02096e2662Till Mossakowski SYMB_ITEMS SYMB_MAP_ITEMS
2a693c01b154f1e25931ff6c754d2d02096e2662Till Mossakowski Symbol RawSymbol where
5824312cc0cfccce61f195fbe92307a21a467049Christian Maeder basic_analysis Modal = Just basicModalAnalysis
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder stat_symb_map_items Modal = statSymbMapItems
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder stat_symb_items Modal = statSymbItems
2a693c01b154f1e25931ff6c754d2d02096e2662Till Mossakowski symbol_to_raw Modal = symbolToRaw
2a693c01b154f1e25931ff6c754d2d02096e2662Till Mossakowski id_to_raw Modal = idToRaw
3a761fd74f4f3c5587a199553c0ee7383e5d8ff3Christian Maeder empty_signature Modal = emptySign emptyModalSign
eca4db63ed0bdbd93b62678feea6e3eb80aa47bbChristian Maeder signature_union Modal s = return . addSig addModalSign s
4aa35aadcb28f8a962096efc70d3bdb58ab7d9faChristian Maeder intersection Modal s = return . interSig interModalSign s
7857a35e3af533dfbd0f0e18638ebd211e6358a0Christian Maeder morphism_union Modal = plainMorphismUnion addModalSign
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder final_union Modal = finalUnion addModalSign
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder is_subsig Modal = isSubSig isSubModalSign
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder subsig_inclusion Modal = sigInclusion emptyMorExt
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder cogenerated_sign Modal = cogeneratedSign emptyMorExt
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder generated_sign Modal = generatedSign emptyMorExt
fbf1cdad9a9775bd7332e85f01b6a307d7dbb1cfChristian Maeder induced_from_morphism Modal = inducedFromMorphism emptyMorExt
e85b224577b78d08ba5c39fe9dcc2e53995454a2Christian Maeder induced_from_to_morphism Modal =
9eb39c7a0e7a1ddad1eec1d23c6d4e3a99c54023Christian Maeder inducedFromToMorphism emptyMorExt isSubModalSign diffModalSign
7b27b67b1c8516d7ccf1610a17fec93662d6a93fChristian Maeder theory_to_taxonomy Modal = convTaxo
3a761fd74f4f3c5587a199553c0ee7383e5d8ff3Christian Maederinstance Logic Modal ()
3a761fd74f4f3c5587a199553c0ee7383e5d8ff3Christian Maeder M_BASIC_SPEC ModalFORMULA SYMB_ITEMS SYMB_MAP_ITEMS
2a693c01b154f1e25931ff6c754d2d02096e2662Till Mossakowski Symbol RawSymbol () where
cdcf5d3f1e79d8798d77efa29e6193af94ea0604Till Mossakowski stability _ = Testing
cd6e5706893519bfcf24539afa252fcbed5097ddKlaus Luettich empty_proof_tree _ = ()