Logic_Modal.hs revision a7be28e157e9ceeec73a8fd0e642c36ea29d4218
2a693c01b154f1e25931ff6c754d2d02096e2662Till MossakowskiModule : $Header$
2a693c01b154f1e25931ff6c754d2d02096e2662Till MossakowskiDescription : Instance of class Logic for Modal CASL
2a693c01b154f1e25931ff6c754d2d02096e2662Till MossakowskiCopyright : (c) Till Mossakowski, Uni Bremen 2002-2004
2a693c01b154f1e25931ff6c754d2d02096e2662Till MossakowskiLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
2a693c01b154f1e25931ff6c754d2d02096e2662Till MossakowskiMaintainer : luecke@informatik.uni-bremen.de
2a693c01b154f1e25931ff6c754d2d02096e2662Till MossakowskiStability : provisional
2a693c01b154f1e25931ff6c754d2d02096e2662Till MossakowskiPortability : portable
684ada8af5c3e6da5c1a69edb6f233c9f2db4ebdWiebke HerdingInstance of class Logic for modal logic.
2a693c01b154f1e25931ff6c754d2d02096e2662Till Mossakowskidata Modal = Modal deriving Show
2a693c01b154f1e25931ff6c754d2d02096e2662Till Mossakowskiinstance Language Modal where
3a761fd74f4f3c5587a199553c0ee7383e5d8ff3Christian Maeder description _ = unlines
2a693c01b154f1e25931ff6c754d2d02096e2662Till Mossakowski [ "ModalCASL extends CASL by modal operators. Syntax for ordinary"
3a761fd74f4f3c5587a199553c0ee7383e5d8ff3Christian Maeder , "modalities, multi-modal logics as well as term-modal"
3a761fd74f4f3c5587a199553c0ee7383e5d8ff3Christian Maeder , "logic (also covering dynamic logic) is provided."
3a761fd74f4f3c5587a199553c0ee7383e5d8ff3Christian Maeder , "Specific modal logics can be obtained via restrictions to"
3a761fd74f4f3c5587a199553c0ee7383e5d8ff3Christian Maeder , "sublanguages." ]
684ada8af5c3e6da5c1a69edb6f233c9f2db4ebdWiebke Herdingtype MSign = Sign M_FORMULA ModalSign
3a761fd74f4f3c5587a199553c0ee7383e5d8ff3Christian Maedertype ModalMor = Morphism M_FORMULA ModalSign (DefMorExt ModalSign)
3a761fd74f4f3c5587a199553c0ee7383e5d8ff3Christian Maedertype ModalFORMULA = FORMULA M_FORMULA
3a761fd74f4f3c5587a199553c0ee7383e5d8ff3Christian Maederinstance SignExtension ModalSign where
3a761fd74f4f3c5587a199553c0ee7383e5d8ff3Christian Maeder isSubSignExtension = isSubModalSign
2a693c01b154f1e25931ff6c754d2d02096e2662Till Mossakowskiinstance Syntax Modal M_BASIC_SPEC SYMB_ITEMS SYMB_MAP_ITEMS where
3a761fd74f4f3c5587a199553c0ee7383e5d8ff3Christian Maeder parse_basic_spec Modal = Just $ basicSpec modal_reserved_words
684ada8af5c3e6da5c1a69edb6f233c9f2db4ebdWiebke Herding parse_symb_items Modal = Just $ symbItems modal_reserved_words
3a761fd74f4f3c5587a199553c0ee7383e5d8ff3Christian Maeder parse_symb_map_items Modal = Just $ symbMapItems modal_reserved_words
2a693c01b154f1e25931ff6c754d2d02096e2662Till Mossakowski-- Modal logic
2a693c01b154f1e25931ff6c754d2d02096e2662Till Mossakowskimap_M_FORMULA :: MapSen M_FORMULA ModalSign (DefMorExt ModalSign)
2a693c01b154f1e25931ff6c754d2d02096e2662Till Mossakowskimap_M_FORMULA mor (BoxOrDiamond b m f ps) =
2a693c01b154f1e25931ff6c754d2d02096e2662Till Mossakowski let newM = case m of
2a693c01b154f1e25931ff6c754d2d02096e2662Till Mossakowski Simple_mod _ -> m
2a693c01b154f1e25931ff6c754d2d02096e2662Till Mossakowski Term_mod t -> let newT = mapTerm map_M_FORMULA mor t
2a693c01b154f1e25931ff6c754d2d02096e2662Till Mossakowski in Term_mod newT
2a693c01b154f1e25931ff6c754d2d02096e2662Till Mossakowski newF = mapSen map_M_FORMULA mor f
2a693c01b154f1e25931ff6c754d2d02096e2662Till Mossakowski in BoxOrDiamond b newM newF ps
684ada8af5c3e6da5c1a69edb6f233c9f2db4ebdWiebke Herdinginstance Sentences Modal ModalFORMULA MSign ModalMor Symbol where
684ada8af5c3e6da5c1a69edb6f233c9f2db4ebdWiebke Herding map_sen Modal m = return . mapSen map_M_FORMULA m
684ada8af5c3e6da5c1a69edb6f233c9f2db4ebdWiebke Herding parse_sentence Modal = Nothing
3a761fd74f4f3c5587a199553c0ee7383e5d8ff3Christian Maeder sym_of Modal = symOf
2a693c01b154f1e25931ff6c754d2d02096e2662Till Mossakowski symmap_of Modal = morphismToSymbMap
2a693c01b154f1e25931ff6c754d2d02096e2662Till Mossakowski sym_name Modal = symName
50dce6b011347f92377adb8bbabaeeb80975e86dChristian Maeder simplify_sen Modal = simplifySen minExpForm simModal
50dce6b011347f92377adb8bbabaeeb80975e86dChristian Maeder print_sign Modal sig = printSign
50dce6b011347f92377adb8bbabaeeb80975e86dChristian Maeder (printModalSign $ simplifySen minExpForm simModal sig) sig
2a693c01b154f1e25931ff6c754d2d02096e2662Till Mossakowski-- simplifySen for ExtFORMULA
c2db39a683438b0f3d484519f4c93db26eec9d2eWiebke HerdingsimModal :: Sign M_FORMULA ModalSign -> M_FORMULA -> M_FORMULA
3a761fd74f4f3c5587a199553c0ee7383e5d8ff3Christian MaedersimModal sign (BoxOrDiamond b md form pos) =
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder let mod' = case md of
2a693c01b154f1e25931ff6c754d2d02096e2662Till Mossakowski Term_mod term -> Term_mod $ rmTypesT minExpForm
2a693c01b154f1e25931ff6c754d2d02096e2662Till Mossakowski simModal sign term
2a693c01b154f1e25931ff6c754d2d02096e2662Till Mossakowski in BoxOrDiamond b mod'
2a693c01b154f1e25931ff6c754d2d02096e2662Till Mossakowski (simplifySen minExpForm simModal sign form) pos
c2db39a683438b0f3d484519f4c93db26eec9d2eWiebke HerdingrmTypesExt :: a -> b -> b
3a761fd74f4f3c5587a199553c0ee7383e5d8ff3Christian MaederrmTypesExt _ f = f
3a761fd74f4f3c5587a199553c0ee7383e5d8ff3Christian Maederinstance StaticAnalysis Modal M_BASIC_SPEC ModalFORMULA
2a693c01b154f1e25931ff6c754d2d02096e2662Till Mossakowski SYMB_ITEMS SYMB_MAP_ITEMS
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder Symbol RawSymbol where
2a693c01b154f1e25931ff6c754d2d02096e2662Till Mossakowski basic_analysis Modal = Just basicModalAnalysis
2a693c01b154f1e25931ff6c754d2d02096e2662Till Mossakowski stat_symb_map_items Modal = statSymbMapItems
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder stat_symb_items Modal = statSymbItems
c2db39a683438b0f3d484519f4c93db26eec9d2eWiebke Herding symbol_to_raw Modal = symbolToRaw
3a761fd74f4f3c5587a199553c0ee7383e5d8ff3Christian Maeder id_to_raw Modal = idToRaw
2a693c01b154f1e25931ff6c754d2d02096e2662Till Mossakowski empty_signature Modal = emptySign emptyModalSign
3a761fd74f4f3c5587a199553c0ee7383e5d8ff3Christian Maeder signature_union Modal s = return . addSig addModalSign s
2a693c01b154f1e25931ff6c754d2d02096e2662Till Mossakowski intersection Modal s = return . interSig interModalSign s
3a761fd74f4f3c5587a199553c0ee7383e5d8ff3Christian Maeder morphism_union Modal = morphismUnion (const id) addModalSign
2a693c01b154f1e25931ff6c754d2d02096e2662Till Mossakowski final_union Modal = finalUnion addModalSign
2a693c01b154f1e25931ff6c754d2d02096e2662Till Mossakowski is_subsig Modal = isSubSig isSubModalSign
2a693c01b154f1e25931ff6c754d2d02096e2662Till Mossakowski subsig_inclusion Modal = sigInclusion emptyMorExt
2a693c01b154f1e25931ff6c754d2d02096e2662Till Mossakowski cogenerated_sign Modal = cogeneratedSign emptyMorExt
2a693c01b154f1e25931ff6c754d2d02096e2662Till Mossakowski generated_sign Modal = generatedSign emptyMorExt
2a693c01b154f1e25931ff6c754d2d02096e2662Till Mossakowski induced_from_morphism Modal = inducedFromMorphism emptyMorExt
2a693c01b154f1e25931ff6c754d2d02096e2662Till Mossakowski induced_from_to_morphism Modal =
2a693c01b154f1e25931ff6c754d2d02096e2662Till Mossakowski inducedFromToMorphism emptyMorExt isSubModalSign diffModalSign
2a693c01b154f1e25931ff6c754d2d02096e2662Till Mossakowski theory_to_taxonomy Modal = convTaxo
c2db39a683438b0f3d484519f4c93db26eec9d2eWiebke Herdinginstance Logic Modal ()
3a761fd74f4f3c5587a199553c0ee7383e5d8ff3Christian Maeder M_BASIC_SPEC ModalFORMULA SYMB_ITEMS SYMB_MAP_ITEMS
2a693c01b154f1e25931ff6c754d2d02096e2662Till Mossakowski Symbol RawSymbol () where
2a693c01b154f1e25931ff6c754d2d02096e2662Till Mossakowski stability _ = Unstable
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian Maeder empty_proof_tree _ = ()