55cf6e01272ec475edea32aa9b7923de2d36cb42Christian Maeder{-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances, FlexibleInstances #-}
60be96a6bed14ee4d7625e3d73040a74ca26321eCodruta GirleaDescription : Instance of class Logic for ExtModal
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian MaederCopyright : DFKI GmbH 2009
98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuLicense : GPLv2 or higher, see LICENSE.txt
1dfd1687e9ee6a45e2cb5268a701ead79c1c1f79Christian MaederMaintainer : Christian.Maeder@dfki.de
60be96a6bed14ee4d7625e3d73040a74ca26321eCodruta GirleaStability : experimental
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian MaederPortability : non-portable (imports Logic)
60be96a6bed14ee4d7625e3d73040a74ca26321eCodruta GirleaInstance of class Logic for ExtModal
1445ecc2d9c5c298117a0e7ea2c5accde351d07eChristian Maederimport qualified Common.Lib.MapSet as MapSet
1445ecc2d9c5c298117a0e7ea2c5accde351d07eChristian Maederimport qualified Data.Set as Set
cb1bcdcebd18280e73151a05cf9846b940674518Codruta Girleadata ExtModal = ExtModal deriving Show
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian Maederinstance Language ExtModal where
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian Maeder description _ = unlines
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian Maeder [ "ExtModal is the 'extended modal logic' extension of CASL. "
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian Maeder , "Syntax for ordinary modalities, multi-modal logic, dynamic "
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian Maeder , "logic, graded modal logic, hybrid logic, CTL* and mu-calculus "
a641f28dd33a3b94a9f28f9515ec50ea1b879fe4Christian Maeder , "is provided. Specific modal logics can be obtained via "
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian Maeder , "restrictions to sublanguages."
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian Maedertype ExtModalSign = Sign EM_FORMULA EModalSign
cb1bcdcebd18280e73151a05cf9846b940674518Codruta Girleatype ExtModalMorph = Morphism EM_FORMULA EModalSign MorphExtension
cb1bcdcebd18280e73151a05cf9846b940674518Codruta Girleatype ExtModalFORMULA = FORMULA EM_FORMULA
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian Maederinstance SignExtension EModalSign where
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian Maeder isSubSignExtension = isSubEModalSign
a65c6747c9acbbebc93baba7bae94d2e3d8cdafbTill Mossakowskiinstance Syntax ExtModal EM_BASIC_SPEC Symbol SYMB_ITEMS SYMB_MAP_ITEMS where
cb5be4f31df88b8137ef3cabf4e8b0ddec52f351Christian Maeder parse_basic_spec ExtModal = Just $ basicSpec ext_modal_reserved_words
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian Maeder parse_symb_items ExtModal = Just $ symbItems ext_modal_reserved_words
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian Maeder parse_symb_map_items ExtModal =
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian Maeder Just $ symbMapItems ext_modal_reserved_words
cb1bcdcebd18280e73151a05cf9846b940674518Codruta Girlea-- Simplification of formulas - simplifySen for ExtFORMULA
cb1bcdcebd18280e73151a05cf9846b940674518Codruta GirleasimEMSen :: Sign EM_FORMULA EModalSign -> EM_FORMULA -> EM_FORMULA
246cef3345515dc289e03fda4b04b1500db3ff6aChristian MaedersimEMSen sign = mapExtForm (simplifySen frmTypeAna simEMSen sign)
d9c00098d4d65865ad7130e7e0c22e24cfe5fbb6Christian MaedercorrectTarget :: Morphism f EModalSign m -> Morphism f EModalSign m
d9c00098d4d65865ad7130e7e0c22e24cfe5fbb6Christian MaedercorrectTarget m = m
d9c00098d4d65865ad7130e7e0c22e24cfe5fbb6Christian Maeder { mtarget = correctSign $ mtarget m
d9c00098d4d65865ad7130e7e0c22e24cfe5fbb6Christian Maeder , msource = correctSign $ msource m }
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian Maederinstance Sentences ExtModal ExtModalFORMULA ExtModalSign ExtModalMorph Symbol
2025793bdf95b956b34761af691fe9bde01f6d83Christian Maeder map_sen ExtModal morph = return . mapSen mapEMform morph
3e0ed56e973aeef92177e50f7272cafa7eb96fbeChristian Maeder simplify_sen ExtModal = simplifySen frmTypeAna simEMSen . setRevSortRel
c578c3805234bc223ab96f7d1892d3c73518ee94Christian Maeder print_named ExtModal = printTheoryFormula
29d8536ce8b1f05e6efd0b7d40e5c15cec3943c7Christian Maeder print_sign ExtModal sig = let e = extendedInfo sig in pretty sig
29d8536ce8b1f05e6efd0b7d40e5c15cec3943c7Christian Maeder { opMap = diffOpMapSet (opMap sig) $ flexOps e
d20b265a2765e843986ceed6bf0055582981bf0fChristian Maeder , predMap = Set.fold (`MapSet.delete` nomPType)
1445ecc2d9c5c298117a0e7ea2c5accde351d07eChristian Maeder (diffMapSet (predMap sig) $ flexPreds e) $ nominals e
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian Maeder sym_of ExtModal = symOf
d8bc05ccb67185d1253da7b8e92293767e0a4623mscodescu symKind ExtModal = show . pretty . symbolKind . symbType
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian Maeder symmap_of ExtModal = morphismToSymbMap
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian Maeder sym_name ExtModal = symName
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian Maederinstance StaticAnalysis ExtModal EM_BASIC_SPEC ExtModalFORMULA SYMB_ITEMS
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian Maeder SYMB_MAP_ITEMS ExtModalSign ExtModalMorph Symbol RawSymbol where
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian Maeder basic_analysis ExtModal = Just basicEModalAnalysis
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder stat_symb_map_items ExtModal = statSymbMapItems
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder stat_symb_items ExtModal = statSymbItems
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian Maeder symbol_to_raw ExtModal = symbolToRaw
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian Maeder id_to_raw ExtModal = idToRaw
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian Maeder matches ExtModal = CASL.Morphism.matches
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian Maeder empty_signature ExtModal = emptySign emptyEModalSign
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian Maeder signature_union ExtModal sgn = return . addSig addEModalSign sgn
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian Maeder intersection ExtModal sgn = return . interSig interEModalSign sgn
98ca12832943f9b8e6edd28bc59716a2f7798899Christian Maeder signatureDiff ExtModal sgn = return . diffSig diffEModalSign sgn
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian Maeder final_union ExtModal = finalUnion addEModalSign
7857a35e3af533dfbd0f0e18638ebd211e6358a0Christian Maeder morphism_union ExtModal = plainMorphismUnion addEModalSign
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian Maeder is_subsig ExtModal = isSubSig isSubEModalSign
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian Maeder subsig_inclusion ExtModal = sigInclusion emptyMorphExtension
d9c00098d4d65865ad7130e7e0c22e24cfe5fbb6Christian Maeder generated_sign ExtModal s = fmap correctTarget
d9c00098d4d65865ad7130e7e0c22e24cfe5fbb6Christian Maeder . generatedSign emptyMorphExtension s
d9c00098d4d65865ad7130e7e0c22e24cfe5fbb6Christian Maeder cogenerated_sign ExtModal s = fmap correctTarget
d9c00098d4d65865ad7130e7e0c22e24cfe5fbb6Christian Maeder . cogeneratedSign emptyMorphExtension s
e157cd543bda5d5a5d1bd23204ddfe61a9192419Christian Maeder induced_from_morphism ExtModal =
e157cd543bda5d5a5d1bd23204ddfe61a9192419Christian Maeder inducedFromMorphismExt inducedEMsign
e157cd543bda5d5a5d1bd23204ddfe61a9192419Christian Maeder (constMorphExt emptyMorphExtension)
e157cd543bda5d5a5d1bd23204ddfe61a9192419Christian Maeder induced_from_to_morphism ExtModal =
e157cd543bda5d5a5d1bd23204ddfe61a9192419Christian Maeder inducedFromToMorphismExt inducedEMsign
417437c97b9f3ef102275ebd1e3d015b52ef6201Christian Maeder (constMorphExt emptyMorphExtension)
d9c00098d4d65865ad7130e7e0c22e24cfe5fbb6Christian Maeder (\ _ _ -> return emptyMorphExtension) isSubEModalSign diffEModalSign
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian Maeder theory_to_taxonomy ExtModal = convTaxo
1dfd1687e9ee6a45e2cb5268a701ead79c1c1f79Christian Maederinstance Logic ExtModal ExtModalSL EM_BASIC_SPEC ExtModalFORMULA SYMB_ITEMS
f588d2cfbdd1e6d4855df164fce25cf7db1a8e2dChristian Maeder SYMB_MAP_ITEMS ExtModalSign ExtModalMorph Symbol RawSymbol () where
cdcf5d3f1e79d8798d77efa29e6193af94ea0604Till Mossakowski stability ExtModal = Testing
1dfd1687e9ee6a45e2cb5268a701ead79c1c1f79Christian Maeder all_sublogics ExtModal = sublogics_all $ foleml : concat sublogicsDim
1dfd1687e9ee6a45e2cb5268a701ead79c1c1f79Christian Maeder sublogicDimensions ExtModal = sDims sublogicsDim
1dfd1687e9ee6a45e2cb5268a701ead79c1c1f79Christian Maeder parseSublogic ExtModal = parseSL $ Just . parseSublog
1dfd1687e9ee6a45e2cb5268a701ead79c1c1f79Christian Maeder empty_proof_tree ExtModal = ()
1dfd1687e9ee6a45e2cb5268a701ead79c1c1f79Christian Maederinstance MinSL Sublogic EM_FORMULA where
1dfd1687e9ee6a45e2cb5268a701ead79c1c1f79Christian Maeder minSL = minSublogicOfEM
1dfd1687e9ee6a45e2cb5268a701ead79c1c1f79Christian Maederinstance ProjForm Sublogic EM_FORMULA where
1dfd1687e9ee6a45e2cb5268a701ead79c1c1f79Christian Maeder projForm _ = Just . ExtFORMULA
1dfd1687e9ee6a45e2cb5268a701ead79c1c1f79Christian Maederinstance ProjSigItem Sublogic EM_SIG_ITEM EM_FORMULA where
1dfd1687e9ee6a45e2cb5268a701ead79c1c1f79Christian Maeder projSigItems _ s = (Just $ Ext_SIG_ITEMS s, [])
1dfd1687e9ee6a45e2cb5268a701ead79c1c1f79Christian Maederinstance ProjBasic Sublogic EM_BASIC_ITEM EM_SIG_ITEM EM_FORMULA where
1dfd1687e9ee6a45e2cb5268a701ead79c1c1f79Christian Maeder projBasicItems _ b = (Just $ Ext_BASIC_ITEMS b, [])
1dfd1687e9ee6a45e2cb5268a701ead79c1c1f79Christian Maederinstance MinSL Sublogic EM_SIG_ITEM where
1dfd1687e9ee6a45e2cb5268a701ead79c1c1f79Christian Maeder minSL = comp_list . minSLExtSigItem
1dfd1687e9ee6a45e2cb5268a701ead79c1c1f79Christian Maederinstance MinSL Sublogic EM_BASIC_ITEM where
1dfd1687e9ee6a45e2cb5268a701ead79c1c1f79Christian Maeder minSL = minSublogicEMBasic
1dfd1687e9ee6a45e2cb5268a701ead79c1c1f79Christian Maederinstance MinSL Sublogic EModalSign where
1dfd1687e9ee6a45e2cb5268a701ead79c1c1f79Christian Maeder minSL = minSublogicEMSign
1dfd1687e9ee6a45e2cb5268a701ead79c1c1f79Christian Maederinstance NameSL Sublogic where
1dfd1687e9ee6a45e2cb5268a701ead79c1c1f79Christian Maeder nameSL = sublogName