Logic_ExtModal.hs revision a65c6747c9acbbebc93baba7bae94d2e3d8cdafb
2b873214c9ab511bbca437c036371ab664aedaceChristian Maeder{-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances, FlexibleInstances #-}
c63ebf815c8a874525cf18670ad74847f7fc7b26Christian MaederModule : $Header$
c092fcac4b8f5c524c22ca579189c4487c13edf7Christian MaederDescription : Instance of class Logic for ExtModal
54ed6a6b1a6c7d27fadb39ec5b59d0806c81f7c8Christian MaederCopyright : DFKI GmbH 2009
75a6279dbae159d018ef812185416cf6df386c10Till MossakowskiLicense : GPLv2 or higher, see LICENSE.txt
3f69b6948966979163bdfe8331c38833d5d90ecdChristian MaederMaintainer : Christian.Maeder@dfki.de
75a6279dbae159d018ef812185416cf6df386c10Till MossakowskiStability : experimental
75a6279dbae159d018ef812185416cf6df386c10Till MossakowskiPortability : non-portable (imports Logic)
c092fcac4b8f5c524c22ca579189c4487c13edf7Christian MaederInstance of class Logic for ExtModal
6352f3c31da3043783a13be6594aacb2147378baRazvan Pascanuimport qualified Common.Lib.MapSet as MapSet
8ef91a173e69219fc2ebd45c76a35891c7785abdMarkus Grossimport qualified Data.Set as Set
a2b04db3e156312a8596d8084f7f0f51acf8a96bChristian Maederdata ExtModal = ExtModal deriving Show
fc1a590cd3ee36797c0a032ff41e07f8e2469341Christian Maederinstance Language ExtModal where
66a774f13272fde036481edd2298081ab3d04678Razvan Pascanu description _ = unlines
834c2e71b8e390e5b05c8d02bb6eb22621125133Markus Gross [ "ExtModal is the 'extended modal logic' extension of CASL. "
d27b1887e61f1dc53d77c37f59dbf5019242a686Christian Maeder , "Syntax for ordinary modalities, multi-modal logic, dynamic "
d27b1887e61f1dc53d77c37f59dbf5019242a686Christian Maeder , "logic, graded modal logic, hybrid logic, CTL* and mu-calculus "
d27b1887e61f1dc53d77c37f59dbf5019242a686Christian Maeder , "is provided. Specific modal logics can be obtained via "
6e52f1dfc0da4bc4a7701cf856641c9dce08fc7dChristian Maeder , "restrictions to sublanguages."
63da71bfb4226f504944b293fb77177ebcaea7d4Ewaryst Schulztype ExtModalSign = Sign EM_FORMULA EModalSign
e1ea9a046e9640148ca876dfe47e391559a9fdf3Christian Maedertype ExtModalMorph = Morphism EM_FORMULA EModalSign MorphExtension
14c89b2d830777bf4db2850f038c9f60acaca486Christian Maedertype ExtModalFORMULA = FORMULA EM_FORMULA
57026bc09337d158b89775048a9bcc9c17d825caChristian Maederinstance SignExtension EModalSign where
57026bc09337d158b89775048a9bcc9c17d825caChristian Maeder isSubSignExtension = isSubEModalSign
e1ea9a046e9640148ca876dfe47e391559a9fdf3Christian Maederinstance Syntax ExtModal EM_BASIC_SPEC Symbol SYMB_ITEMS SYMB_MAP_ITEMS where
923e25bb8c7cf9f2978c7844ad173704482cc3b0Martin Kühl parse_basic_spec ExtModal = Just $ basicSpec ext_modal_reserved_words
f66fcd981f556c238df7dd6dfa42123745e3b1d2Christian Maeder parse_symb_items ExtModal = Just $ symbItems ext_modal_reserved_words
2b873214c9ab511bbca437c036371ab664aedaceChristian Maeder parse_symb_map_items ExtModal =
52d922076b89f12234f721974e82531bc69a6f69Christian Maeder Just $ symbMapItems ext_modal_reserved_words
d27b1887e61f1dc53d77c37f59dbf5019242a686Christian Maeder-- Simplification of formulas - simplifySen for ExtFORMULA
d27b1887e61f1dc53d77c37f59dbf5019242a686Christian MaedersimEMSen :: Sign EM_FORMULA EModalSign -> EM_FORMULA -> EM_FORMULA
d27b1887e61f1dc53d77c37f59dbf5019242a686Christian MaedersimEMSen sign = mapExtForm (simplifySen frmTypeAna simEMSen sign)
8ef91a173e69219fc2ebd45c76a35891c7785abdMarkus GrosscorrectTarget :: Morphism f EModalSign m -> Morphism f EModalSign m
8ef91a173e69219fc2ebd45c76a35891c7785abdMarkus GrosscorrectTarget m = m
9175e29c044318498a40f323f189f9dfd50378efChristian Maeder { mtarget = correctSign $ mtarget m
31bc219bae758272d0f064281b8ce7740a4553e9Till Mossakowski , msource = correctSign $ msource m }
31bc219bae758272d0f064281b8ce7740a4553e9Till Mossakowskiinstance Sentences ExtModal ExtModalFORMULA ExtModalSign ExtModalMorph Symbol
a31430de8b0632d29f42634d6395e982bf31b14dChristian Maeder map_sen ExtModal morph = return . mapSen mapEMform morph
a31430de8b0632d29f42634d6395e982bf31b14dChristian Maeder simplify_sen ExtModal = simplifySen frmTypeAna simEMSen . setRevSortRel
a31430de8b0632d29f42634d6395e982bf31b14dChristian Maeder print_named ExtModal = printTheoryFormula
a31430de8b0632d29f42634d6395e982bf31b14dChristian Maeder print_sign ExtModal sig = let e = extendedInfo sig in pretty sig
a31430de8b0632d29f42634d6395e982bf31b14dChristian Maeder { opMap = diffOpMapSet (opMap sig) $ flexOps e
a31430de8b0632d29f42634d6395e982bf31b14dChristian Maeder , predMap = Set.fold (`MapSet.delete` nomPType)
a31430de8b0632d29f42634d6395e982bf31b14dChristian Maeder (diffMapSet (predMap sig) $ flexPreds e) $ nominals e
a31430de8b0632d29f42634d6395e982bf31b14dChristian Maeder sym_of ExtModal = symOf
a31430de8b0632d29f42634d6395e982bf31b14dChristian Maeder symmap_of ExtModal = morphismToSymbMap
a31430de8b0632d29f42634d6395e982bf31b14dChristian Maeder sym_name ExtModal = symName
9175e29c044318498a40f323f189f9dfd50378efChristian Maederinstance StaticAnalysis ExtModal EM_BASIC_SPEC ExtModalFORMULA SYMB_ITEMS
9175e29c044318498a40f323f189f9dfd50378efChristian Maeder SYMB_MAP_ITEMS ExtModalSign ExtModalMorph Symbol RawSymbol where
9175e29c044318498a40f323f189f9dfd50378efChristian Maeder basic_analysis ExtModal = Just basicEModalAnalysis
9175e29c044318498a40f323f189f9dfd50378efChristian Maeder stat_symb_map_items ExtModal = statSymbMapItems
9175e29c044318498a40f323f189f9dfd50378efChristian Maeder stat_symb_items ExtModal = statSymbItems
ee1c7c5796832536932d7b06cbfb1ca13f9a0d7bMartin Kühl symbol_to_raw ExtModal = symbolToRaw
f63e7684d8db7503c22e5d8d499c94a9405f8f9eChristian Maeder id_to_raw ExtModal = idToRaw
91eeff7b19b22d7e5c5d83fa6e357496e291c718Christian Maeder matches ExtModal = CASL.Morphism.matches
f63e7684d8db7503c22e5d8d499c94a9405f8f9eChristian Maeder empty_signature ExtModal = emptySign emptyEModalSign
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder signature_union ExtModal sgn = return . addSig addEModalSign sgn
c0c2380bced8159ff0297ece14eba948bd236471Christian Maeder intersection ExtModal sgn = return . interSig interEModalSign sgn
bdc103981a28a51938de98a956d8a3767f6cf43dAivaras Jakubauskas signatureDiff ExtModal sgn = return . diffSig diffEModalSign sgn
c0c2380bced8159ff0297ece14eba948bd236471Christian Maeder final_union ExtModal = finalUnion addEModalSign
e1ea9a046e9640148ca876dfe47e391559a9fdf3Christian Maeder morphism_union ExtModal = plainMorphismUnion addEModalSign
e1ea9a046e9640148ca876dfe47e391559a9fdf3Christian Maeder is_subsig ExtModal = isSubSig isSubEModalSign
57026bc09337d158b89775048a9bcc9c17d825caChristian Maeder subsig_inclusion ExtModal = sigInclusion emptyMorphExtension
57026bc09337d158b89775048a9bcc9c17d825caChristian Maeder generated_sign ExtModal s = fmap correctTarget
22b772f8753f0cdb4508ba460356c238de2ee375Jonathan von Schroeder . generatedSign emptyMorphExtension s
7bbfb15142ab4286dfc6fcde2fc94a5512297e41Jonathan von Schroeder cogenerated_sign ExtModal s = fmap correctTarget
fa388aea9cef5f9734fec346159899a74432ce26Christian Maeder . cogeneratedSign emptyMorphExtension s
63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder induced_from_morphism ExtModal =
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder inducedFromMorphismExt inducedEMsign
0c885f1348fd58f7cb706472a3ff20b52dbef0a7Jonathan von Schroeder (constMorphExt emptyMorphExtension)
52d922076b89f12234f721974e82531bc69a6f69Christian Maeder induced_from_to_morphism ExtModal =
52d922076b89f12234f721974e82531bc69a6f69Christian Maeder inducedFromToMorphismExt inducedEMsign
923e25bb8c7cf9f2978c7844ad173704482cc3b0Martin Kühl (constMorphExt emptyMorphExtension)
9f85afecbd79b3df5a0bb17bd28cd0b288dc3213Kristina Sojakova (\ _ _ -> return emptyMorphExtension) isSubEModalSign diffEModalSign
72079df98b3cb7cc1fd82a0a24984893dcd05ecaEwaryst Schulz theory_to_taxonomy ExtModal = convTaxo
fbc4f8708092d571a45cb483f37cc6b674da45a7Christian Maederinstance Logic ExtModal ExtModalSL EM_BASIC_SPEC ExtModalFORMULA SYMB_ITEMS
8a77240a809197c92c0736c431b4b88947a7bac1Christian Maeder SYMB_MAP_ITEMS ExtModalSign ExtModalMorph Symbol RawSymbol () where
8a77240a809197c92c0736c431b4b88947a7bac1Christian Maeder stability ExtModal = Experimental
1c4dfa148603d4fcf4cdd2ed66c8b6e1de0dd696Till Mossakowski all_sublogics ExtModal = sublogics_all $ foleml : concat sublogicsDim
bb63f684c4f5f33ffcd1dcc02c58d6a703900fafJonathan von Schroeder sublogicDimensions ExtModal = sDims sublogicsDim
b0234f0a84fcd3587073fbc11d38759108997c3cChristian Maeder parseSublogic ExtModal = parseSL $ Just . parseSublog
b0234f0a84fcd3587073fbc11d38759108997c3cChristian Maeder empty_proof_tree ExtModal = ()
8ef91a173e69219fc2ebd45c76a35891c7785abdMarkus Grossinstance MinSL Sublogic EM_FORMULA where
d56ece59c372cb887355825901222b9f3377f7e6Thiemo Wiedemeyer minSL = minSublogicOfEM
9175e29c044318498a40f323f189f9dfd50378efChristian Maederinstance ProjForm Sublogic EM_FORMULA where
9175e29c044318498a40f323f189f9dfd50378efChristian Maeder projForm _ = Just . ExtFORMULA
f1dec6898638ba1131a9fadbc4d1544c93dfabb0Klaus Luettichinstance ProjSigItem Sublogic EM_SIG_ITEM EM_FORMULA where
9175e29c044318498a40f323f189f9dfd50378efChristian Maeder projSigItems _ s = (Just $ Ext_SIG_ITEMS s, [])