Logic_ExtModal.hs revision a669e4685b32ff5ca1bca785eacc5e30a545b010
66267bcb678a9c341272c323b299337bcfdb7cc5Christian Maeder{-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances #-}
81d182b21020b815887e9057959228546cf61b6bChristian MaederModule : $Header$
66267bcb678a9c341272c323b299337bcfdb7cc5Christian MaederDescription : Instance of class Logic for ExtModal
66267bcb678a9c341272c323b299337bcfdb7cc5Christian MaederCopyright : DFKI GmbH 2009
3f69b6948966979163bdfe8331c38833d5d90ecdChristian MaederLicense : GPLv2 or higher, see LICENSE.txt
66267bcb678a9c341272c323b299337bcfdb7cc5Christian MaederMaintainer : codruta.liliana@gmail.com
ffd01020a4f35f434b912844ad6e0d6918fadffdChristian MaederStability : experimental
66267bcb678a9c341272c323b299337bcfdb7cc5Christian MaederPortability : non-portable (imports Logic)
fb69cd512eab767747f109e40322df7cae2f7bdfChristian MaederInstance of class Logic for ExtModal
f42bcc750a9a02cb4f753b70679f9aacf1b338d7Christian Maederimport qualified Data.Map as Map
f42bcc750a9a02cb4f753b70679f9aacf1b338d7Christian Maederdata ExtModal = ExtModal deriving Show
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maederinstance Language ExtModal where
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder description _ = unlines
946f62de1b188898dde0c472f2a8a6fb86f4d2f5Christian Maeder [ "ExtModal is the 'extended modal logic' extension of CASL. "
6f031207ab25d41ae4740a4151d5946faff4768bChristian Maeder , "Syntax for ordinary modalities, multi-modal logic, dynamic "
6f031207ab25d41ae4740a4151d5946faff4768bChristian Maeder , "logic, graded modal logic, hybrid logic, CTL* and mu-calculus "
e7ce154edb906685b3fa7f6c0a764e18a4658068Christian Maeder , "is provided. Specific modal logics can be optained via "
e7ce154edb906685b3fa7f6c0a764e18a4658068Christian Maeder , "restrictions to sublanguages."
6cb518d88084543c13aa7e56db767c14ee97ab77Christian Maedertype ExtModalSign = Sign EM_FORMULA EModalSign
6cb518d88084543c13aa7e56db767c14ee97ab77Christian Maedertype ExtModalMorph = Morphism EM_FORMULA EModalSign MorphExtension
024621f43239cfe9629e35d35a8669fad7acbba2Christian Maedertype ExtModalFORMULA = FORMULA EM_FORMULA
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maederinstance SignExtension EModalSign where
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder isSubSignExtension = isSubEModalSign
27912d626bf179b82fcb337077e5cd9653bb71cfChristian Maederinstance Syntax ExtModal EM_BASIC_SPEC SYMB_ITEMS SYMB_MAP_ITEMS where
e13ee09381f136f5eadaabdb9699773c0052cf3dChristian Maeder parse_basic_spec ExtModal = Just $ basicSpec ext_modal_reserved_words
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder parse_symb_items ExtModal = Just $ symbItems ext_modal_reserved_words
5c933f3c61d2cfa7e76e4eb610a4b0bac988be47Christian Maeder parse_symb_map_items ExtModal =
5c933f3c61d2cfa7e76e4eb610a4b0bac988be47Christian Maeder Just $ symbMapItems ext_modal_reserved_words
6cb518d88084543c13aa7e56db767c14ee97ab77Christian Maeder-- Modal formula mapping via signature morphism
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maedermap_EM_FORMULA :: MapSen EM_FORMULA EModalSign MorphExtension
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maedermap_EM_FORMULA morph (BoxOrDiamond choice t_m leq_geq number f pos) =
f6fc70956d64365527d77a521a96f54a1cc18f91Christian Maeder let new_tm tm = case tm of
f6fc70956d64365527d77a521a96f54a1cc18f91Christian Maeder Simple_modality sm ->
946f62de1b188898dde0c472f2a8a6fb86f4d2f5Christian Maeder let mds = mod_map (extended_map morph) in
f6fc70956d64365527d77a521a96f54a1cc18f91Christian Maeder if Map.member sm mds then Simple_modality (mds Map.! sm) else tm
f6fc70956d64365527d77a521a96f54a1cc18f91Christian Maeder Composition tm1 tm2 -> Composition (new_tm tm1) (new_tm tm2)
f6fc70956d64365527d77a521a96f54a1cc18f91Christian Maeder Union tm1 tm2 -> Union (new_tm tm1) (new_tm tm2)
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder TransitiveClosure tm1 -> TransitiveClosure (new_tm tm1)
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder Guard frm -> Guard (mapSen map_EM_FORMULA morph frm)
946f62de1b188898dde0c472f2a8a6fb86f4d2f5Christian Maeder new_f = mapSen map_EM_FORMULA morph f
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder in BoxOrDiamond choice (new_tm t_m) leq_geq number new_f pos
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maedermap_EM_FORMULA morph (Hybrid choice nm f pos) =
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder let new_nom = case nm of
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder Nominal nom -> let nms = nom_map (extended_map morph) in
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder if Map.member nom nms then Nominal (nms Map.! nom) else nm
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder new_f = mapSen map_EM_FORMULA morph f
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder in Hybrid choice new_nom new_f pos
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maedermap_EM_FORMULA morph (UntilSince choice f1 f2 pos) =
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder let new_f1 = mapSen map_EM_FORMULA morph f1
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder new_f2 = mapSen map_EM_FORMULA morph f2
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder in UntilSince choice new_f1 new_f2 pos
998747cb2ee575cccdd7d865c95d0ef07516a6a5Christian Maedermap_EM_FORMULA morph (NextY choice f pos) =
07e579405f31fff7f9315685661b5a87cb99c41bChristian Maeder let new_f = mapSen map_EM_FORMULA morph f
07e579405f31fff7f9315685661b5a87cb99c41bChristian Maeder in NextY choice new_f pos
07e579405f31fff7f9315685661b5a87cb99c41bChristian Maedermap_EM_FORMULA morph (PathQuantification choice f pos) =
07e579405f31fff7f9315685661b5a87cb99c41bChristian Maeder let new_f = mapSen map_EM_FORMULA morph f
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder in PathQuantification choice new_f pos
bbcc77a6eb9554dd3092cabafae1e5ca74a054eeChristian Maedermap_EM_FORMULA morph (StateQuantification t_dir choice f pos) =
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder let new_f = mapSen map_EM_FORMULA morph f
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder in StateQuantification t_dir choice new_f pos
6b23467258cdc15e05f1845cd400d60ca6eba966Christian Maedermap_EM_FORMULA morph (FixedPoint choice p_var f pos) =
6b23467258cdc15e05f1845cd400d60ca6eba966Christian Maeder let new_f = mapSen map_EM_FORMULA morph f
6b23467258cdc15e05f1845cd400d60ca6eba966Christian Maeder in FixedPoint choice p_var new_f pos
6b23467258cdc15e05f1845cd400d60ca6eba966Christian Maeder-- Simplification of formulas - simplifySen for ExtFORMULA
6b23467258cdc15e05f1845cd400d60ca6eba966Christian MaedersimEMSen :: Sign EM_FORMULA EModalSign -> EM_FORMULA -> EM_FORMULA
6b23467258cdc15e05f1845cd400d60ca6eba966Christian MaedersimEMSen sign (BoxOrDiamond choice tm leq_geq number f pos) =
6b23467258cdc15e05f1845cd400d60ca6eba966Christian Maeder BoxOrDiamond choice tm leq_geq number
6b23467258cdc15e05f1845cd400d60ca6eba966Christian Maeder (simplifySen frmTypeAna simEMSen sign f) pos
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaedersimEMSen sign (Hybrid choice nom f pos) =
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder Hybrid choice nom (simplifySen frmTypeAna simEMSen sign f) pos
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaedersimEMSen sign (UntilSince choice f1 f2 pos) =
e13ee09381f136f5eadaabdb9699773c0052cf3dChristian Maeder UntilSince choice (simplifySen frmTypeAna simEMSen sign f1)
e13ee09381f136f5eadaabdb9699773c0052cf3dChristian Maeder (simplifySen frmTypeAna simEMSen sign f2) pos
e13ee09381f136f5eadaabdb9699773c0052cf3dChristian MaedersimEMSen sign (NextY choice f pos) =
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder NextY choice (simplifySen frmTypeAna simEMSen sign f) pos
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaedersimEMSen sign (PathQuantification choice f pos) =
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder PathQuantification choice (simplifySen frmTypeAna simEMSen sign f) pos
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaedersimEMSen sign (StateQuantification t_dir choice f pos) =
6cb518d88084543c13aa7e56db767c14ee97ab77Christian Maeder StateQuantification t_dir choice
6cb518d88084543c13aa7e56db767c14ee97ab77Christian Maeder (simplifySen frmTypeAna simEMSen sign f) pos
6cb518d88084543c13aa7e56db767c14ee97ab77Christian MaedersimEMSen sign (FixedPoint choice p_var f pos) =
6cb518d88084543c13aa7e56db767c14ee97ab77Christian Maeder FixedPoint choice p_var (simplifySen frmTypeAna simEMSen sign f) pos
31a189d4cff554f78407cdc422480e84e99a6ec6Christian Maederinstance Sentences ExtModal ExtModalFORMULA ExtModalSign ExtModalMorph Symbol
6cb518d88084543c13aa7e56db767c14ee97ab77Christian Maeder map_sen ExtModal morph = return . mapSen map_EM_FORMULA morph
31a189d4cff554f78407cdc422480e84e99a6ec6Christian Maeder simplify_sen ExtModal = simplifySen frmTypeAna simEMSen
6cb518d88084543c13aa7e56db767c14ee97ab77Christian Maeder print_sign ExtModal sig = printSign
5553cf7e344c2b385a72e1244b419e9986042b8eChristian Maeder (printEModalSign $ simplifySen frmTypeAna simEMSen sig) sig
f42bcc750a9a02cb4f753b70679f9aacf1b338d7Christian Maeder sym_of ExtModal = symOf
946f62de1b188898dde0c472f2a8a6fb86f4d2f5Christian Maeder symmap_of ExtModal = morphismToSymbMap
946f62de1b188898dde0c472f2a8a6fb86f4d2f5Christian Maeder sym_name ExtModal = symName
946f62de1b188898dde0c472f2a8a6fb86f4d2f5Christian Maederinstance StaticAnalysis ExtModal EM_BASIC_SPEC ExtModalFORMULA SYMB_ITEMS
946f62de1b188898dde0c472f2a8a6fb86f4d2f5Christian Maeder SYMB_MAP_ITEMS ExtModalSign ExtModalMorph Symbol RawSymbol where
2ca4cb7c4970015237ff434081c2c5bc74284cadChristian Maeder basic_analysis ExtModal = Just basicEModalAnalysis
2ca4cb7c4970015237ff434081c2c5bc74284cadChristian Maeder stat_symb_map_items ExtModal _ _ = statSymbMapItems
946f62de1b188898dde0c472f2a8a6fb86f4d2f5Christian Maeder stat_symb_items ExtModal _ = statSymbItems
5553cf7e344c2b385a72e1244b419e9986042b8eChristian Maeder symbol_to_raw ExtModal = symbolToRaw
31a189d4cff554f78407cdc422480e84e99a6ec6Christian Maeder id_to_raw ExtModal = idToRaw
31a189d4cff554f78407cdc422480e84e99a6ec6Christian Maeder matches ExtModal = CASL.Morphism.matches
946f62de1b188898dde0c472f2a8a6fb86f4d2f5Christian Maeder empty_signature ExtModal = emptySign emptyEModalSign
946f62de1b188898dde0c472f2a8a6fb86f4d2f5Christian Maeder signature_union ExtModal sgn = return . addSig addEModalSign sgn
946f62de1b188898dde0c472f2a8a6fb86f4d2f5Christian Maeder intersection ExtModal sgn = return . interSig interEModalSign sgn
946f62de1b188898dde0c472f2a8a6fb86f4d2f5Christian Maeder final_union ExtModal = finalUnion addEModalSign
6cb518d88084543c13aa7e56db767c14ee97ab77Christian Maeder morphism_union ExtModal = plainMorphismUnion addEModalSign
946f62de1b188898dde0c472f2a8a6fb86f4d2f5Christian Maeder is_subsig ExtModal = isSubSig isSubEModalSign
5553cf7e344c2b385a72e1244b419e9986042b8eChristian Maeder subsig_inclusion ExtModal = sigInclusion emptyMorphExtension
5553cf7e344c2b385a72e1244b419e9986042b8eChristian Maeder generated_sign ExtModal = generatedSign emptyMorphExtension
946f62de1b188898dde0c472f2a8a6fb86f4d2f5Christian Maeder cogenerated_sign ExtModal = cogeneratedSign emptyMorphExtension
946f62de1b188898dde0c472f2a8a6fb86f4d2f5Christian Maeder induced_from_morphism ExtModal = inducedFromMorphism emptyMorphExtension
946f62de1b188898dde0c472f2a8a6fb86f4d2f5Christian Maeder induced_from_to_morphism ExtModal =
946f62de1b188898dde0c472f2a8a6fb86f4d2f5Christian Maeder inducedFromToMorphism emptyMorphExtension isSubEModalSign
946f62de1b188898dde0c472f2a8a6fb86f4d2f5Christian Maeder diffEModalSign
946f62de1b188898dde0c472f2a8a6fb86f4d2f5Christian Maeder theory_to_taxonomy ExtModal = convTaxo
946f62de1b188898dde0c472f2a8a6fb86f4d2f5Christian Maederinstance Logic ExtModal () EM_BASIC_SPEC ExtModalFORMULA SYMB_ITEMS
946f62de1b188898dde0c472f2a8a6fb86f4d2f5Christian Maeder SYMB_MAP_ITEMS ExtModalSign ExtModalMorph Symbol RawSymbol () where
e13ee09381f136f5eadaabdb9699773c0052cf3dChristian Maeder stability _ = Experimental
e13ee09381f136f5eadaabdb9699773c0052cf3dChristian Maeder empty_proof_tree _ = ()