Logic_ExtModal.hs revision 55cf6e01272ec475edea32aa9b7923de2d36cb42
7fb4c0766e858653c9776474005a6ae6d94828afgryzor{-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances, FlexibleInstances #-}
7fb4c0766e858653c9776474005a6ae6d94828afgryzorModule : $Header$
7fb4c0766e858653c9776474005a6ae6d94828afgryzorDescription : Instance of class Logic for ExtModal
7fb4c0766e858653c9776474005a6ae6d94828afgryzorCopyright : DFKI GmbH 2009
7fb4c0766e858653c9776474005a6ae6d94828afgryzorLicense : GPLv2 or higher, see LICENSE.txt
7fb4c0766e858653c9776474005a6ae6d94828afgryzorMaintainer : codruta.liliana@gmail.com
7fb4c0766e858653c9776474005a6ae6d94828afgryzorStability : experimental
7fb4c0766e858653c9776474005a6ae6d94828afgryzorPortability : non-portable (imports Logic)
d29d9ab4614ff992b0e8de6e2b88d52b6f1f153erbowenInstance of class Logic for ExtModal
7fb4c0766e858653c9776474005a6ae6d94828afgryzorimport qualified Data.Map as Map
e7eb98e34575dcf6536530bcf08e00d7ab3d3124gryzordata ExtModal = ExtModal deriving Show
7fb4c0766e858653c9776474005a6ae6d94828afgryzorinstance Language ExtModal where
b03f9485e6dfcf9326e6122f91eaa1ced8939818jim description _ = unlines
30471a4650391f57975f60bbb6e4a90be7b284bfhumbedooh [ "ExtModal is the 'extended modal logic' extension of CASL. "
7fb4c0766e858653c9776474005a6ae6d94828afgryzor , "Syntax for ordinary modalities, multi-modal logic, dynamic "
7fb4c0766e858653c9776474005a6ae6d94828afgryzor , "logic, graded modal logic, hybrid logic, CTL* and mu-calculus "
70f5253b24dd333c67fb6502d557a8b48ad3ba87igalic , "is provided. Specific modal logics can be optained via "
70f5253b24dd333c67fb6502d557a8b48ad3ba87igalic , "restrictions to sublanguages."
70f5253b24dd333c67fb6502d557a8b48ad3ba87igalictype ExtModalSign = Sign EM_FORMULA EModalSign
70f5253b24dd333c67fb6502d557a8b48ad3ba87igalictype ExtModalMorph = Morphism EM_FORMULA EModalSign MorphExtension
888cb40bdeec5abf452bd85d6bf63b26d5913d4chumbedoohtype ExtModalFORMULA = FORMULA EM_FORMULA
888cb40bdeec5abf452bd85d6bf63b26d5913d4chumbedoohinstance SignExtension EModalSign where
888cb40bdeec5abf452bd85d6bf63b26d5913d4chumbedooh isSubSignExtension = isSubEModalSign
888cb40bdeec5abf452bd85d6bf63b26d5913d4chumbedoohinstance Syntax ExtModal EM_BASIC_SPEC SYMB_ITEMS SYMB_MAP_ITEMS where
888cb40bdeec5abf452bd85d6bf63b26d5913d4chumbedooh parse_basic_spec ExtModal = Just $ basicSpec ext_modal_reserved_words
888cb40bdeec5abf452bd85d6bf63b26d5913d4chumbedooh parse_symb_items ExtModal = Just $ symbItems ext_modal_reserved_words
888cb40bdeec5abf452bd85d6bf63b26d5913d4chumbedooh parse_symb_map_items ExtModal =
888cb40bdeec5abf452bd85d6bf63b26d5913d4chumbedooh Just $ symbMapItems ext_modal_reserved_words
70f5253b24dd333c67fb6502d557a8b48ad3ba87igalic-- Modal formula mapping via signature morphism
70f5253b24dd333c67fb6502d557a8b48ad3ba87igalicmap_EM_FORMULA :: MapSen EM_FORMULA EModalSign MorphExtension
7fb4c0766e858653c9776474005a6ae6d94828afgryzormap_EM_FORMULA morph (BoxOrDiamond choice t_m leq_geq number f pos) =
7fb4c0766e858653c9776474005a6ae6d94828afgryzor let new_tm tm = case tm of
7fb4c0766e858653c9776474005a6ae6d94828afgryzor Simple_modality sm ->
7fb4c0766e858653c9776474005a6ae6d94828afgryzor let mds = mod_map (extended_map morph) in
7fb4c0766e858653c9776474005a6ae6d94828afgryzor if Map.member sm mds then Simple_modality (mds Map.! sm) else tm
7fb4c0766e858653c9776474005a6ae6d94828afgryzor Composition tm1 tm2 -> Composition (new_tm tm1) (new_tm tm2)
7fb4c0766e858653c9776474005a6ae6d94828afgryzor Union tm1 tm2 -> Union (new_tm tm1) (new_tm tm2)
7fb4c0766e858653c9776474005a6ae6d94828afgryzor TransitiveClosure tm1 -> TransitiveClosure (new_tm tm1)
7fb4c0766e858653c9776474005a6ae6d94828afgryzor Guard frm -> Guard (mapSen map_EM_FORMULA morph frm)
7fb4c0766e858653c9776474005a6ae6d94828afgryzor new_f = mapSen map_EM_FORMULA morph f
7fb4c0766e858653c9776474005a6ae6d94828afgryzor in BoxOrDiamond choice (new_tm t_m) leq_geq number new_f pos
7fb4c0766e858653c9776474005a6ae6d94828afgryzormap_EM_FORMULA morph (Hybrid choice nm f pos) =
7fb4c0766e858653c9776474005a6ae6d94828afgryzor let new_nom = case nm of
7fb4c0766e858653c9776474005a6ae6d94828afgryzor Nominal nom -> let nms = nom_map (extended_map morph) in
7fb4c0766e858653c9776474005a6ae6d94828afgryzor if Map.member nom nms then Nominal (nms Map.! nom) else nm
888cb40bdeec5abf452bd85d6bf63b26d5913d4chumbedooh new_f = mapSen map_EM_FORMULA morph f
888cb40bdeec5abf452bd85d6bf63b26d5913d4chumbedooh in Hybrid choice new_nom new_f pos
7fb4c0766e858653c9776474005a6ae6d94828afgryzormap_EM_FORMULA morph (UntilSince choice f1 f2 pos) =
7fb4c0766e858653c9776474005a6ae6d94828afgryzor let new_f1 = mapSen map_EM_FORMULA morph f1
e7eb98e34575dcf6536530bcf08e00d7ab3d3124gryzor new_f2 = mapSen map_EM_FORMULA morph f2
9534272616b71aaea50aeec4162e749a96aebd7fsf in UntilSince choice new_f1 new_f2 pos
9534272616b71aaea50aeec4162e749a96aebd7fsfmap_EM_FORMULA morph (NextY choice f pos) =
9534272616b71aaea50aeec4162e749a96aebd7fsf let new_f = mapSen map_EM_FORMULA morph f
e7eb98e34575dcf6536530bcf08e00d7ab3d3124gryzor in NextY choice new_f pos
888cb40bdeec5abf452bd85d6bf63b26d5913d4chumbedoohmap_EM_FORMULA morph (PathQuantification choice f pos) =
888cb40bdeec5abf452bd85d6bf63b26d5913d4chumbedooh let new_f = mapSen map_EM_FORMULA morph f
888cb40bdeec5abf452bd85d6bf63b26d5913d4chumbedooh in PathQuantification choice new_f pos
e7eb98e34575dcf6536530bcf08e00d7ab3d3124gryzormap_EM_FORMULA morph (StateQuantification t_dir choice f pos) =
e7eb98e34575dcf6536530bcf08e00d7ab3d3124gryzor let new_f = mapSen map_EM_FORMULA morph f
e7eb98e34575dcf6536530bcf08e00d7ab3d3124gryzor in StateQuantification t_dir choice new_f pos
e7eb98e34575dcf6536530bcf08e00d7ab3d3124gryzormap_EM_FORMULA morph (FixedPoint choice p_var f pos) =
7fb4c0766e858653c9776474005a6ae6d94828afgryzor let new_f = mapSen map_EM_FORMULA morph f
7fb4c0766e858653c9776474005a6ae6d94828afgryzor in FixedPoint choice p_var new_f pos
7fb4c0766e858653c9776474005a6ae6d94828afgryzor-- Simplification of formulas - simplifySen for ExtFORMULA
7fb4c0766e858653c9776474005a6ae6d94828afgryzorsimEMSen :: Sign EM_FORMULA EModalSign -> EM_FORMULA -> EM_FORMULA
7fb4c0766e858653c9776474005a6ae6d94828afgryzorsimEMSen sign (BoxOrDiamond choice tm leq_geq number f pos) =
7fb4c0766e858653c9776474005a6ae6d94828afgryzor BoxOrDiamond choice tm leq_geq number
7fb4c0766e858653c9776474005a6ae6d94828afgryzor (simplifySen frmTypeAna simEMSen sign f) pos
7fb4c0766e858653c9776474005a6ae6d94828afgryzorsimEMSen sign (Hybrid choice nom f pos) =
888cb40bdeec5abf452bd85d6bf63b26d5913d4chumbedooh Hybrid choice nom (simplifySen frmTypeAna simEMSen sign f) pos
888cb40bdeec5abf452bd85d6bf63b26d5913d4chumbedoohsimEMSen sign (UntilSince choice f1 f2 pos) =
888cb40bdeec5abf452bd85d6bf63b26d5913d4chumbedooh UntilSince choice (simplifySen frmTypeAna simEMSen sign f1)
888cb40bdeec5abf452bd85d6bf63b26d5913d4chumbedooh (simplifySen frmTypeAna simEMSen sign f2) pos
888cb40bdeec5abf452bd85d6bf63b26d5913d4chumbedoohsimEMSen sign (NextY choice f pos) =
888cb40bdeec5abf452bd85d6bf63b26d5913d4chumbedooh NextY choice (simplifySen frmTypeAna simEMSen sign f) pos
888cb40bdeec5abf452bd85d6bf63b26d5913d4chumbedoohsimEMSen sign (PathQuantification choice f pos) =
888cb40bdeec5abf452bd85d6bf63b26d5913d4chumbedooh PathQuantification choice (simplifySen frmTypeAna simEMSen sign f) pos
888cb40bdeec5abf452bd85d6bf63b26d5913d4chumbedoohsimEMSen sign (StateQuantification t_dir choice f pos) =
888cb40bdeec5abf452bd85d6bf63b26d5913d4chumbedooh StateQuantification t_dir choice
888cb40bdeec5abf452bd85d6bf63b26d5913d4chumbedooh (simplifySen frmTypeAna simEMSen sign f) pos
7fb4c0766e858653c9776474005a6ae6d94828afgryzorsimEMSen sign (FixedPoint choice p_var f pos) =
7fb4c0766e858653c9776474005a6ae6d94828afgryzor FixedPoint choice p_var (simplifySen frmTypeAna simEMSen sign f) pos
7fb4c0766e858653c9776474005a6ae6d94828afgryzorinstance Sentences ExtModal ExtModalFORMULA ExtModalSign ExtModalMorph Symbol
7fb4c0766e858653c9776474005a6ae6d94828afgryzor map_sen ExtModal morph = return . mapSen map_EM_FORMULA morph
7fb4c0766e858653c9776474005a6ae6d94828afgryzor simplify_sen ExtModal = simplifySen frmTypeAna simEMSen
7fb4c0766e858653c9776474005a6ae6d94828afgryzor print_sign ExtModal sig = printSign
7fb4c0766e858653c9776474005a6ae6d94828afgryzor (printEModalSign $ simplifySen frmTypeAna simEMSen sig) sig
7fb4c0766e858653c9776474005a6ae6d94828afgryzor sym_of ExtModal = symOf
7fb4c0766e858653c9776474005a6ae6d94828afgryzor symmap_of ExtModal = morphismToSymbMap
7fb4c0766e858653c9776474005a6ae6d94828afgryzor sym_name ExtModal = symName
7fb4c0766e858653c9776474005a6ae6d94828afgryzorinstance StaticAnalysis ExtModal EM_BASIC_SPEC ExtModalFORMULA SYMB_ITEMS
7fb4c0766e858653c9776474005a6ae6d94828afgryzor SYMB_MAP_ITEMS ExtModalSign ExtModalMorph Symbol RawSymbol where
7fb4c0766e858653c9776474005a6ae6d94828afgryzor basic_analysis ExtModal = Just basicEModalAnalysis
7fb4c0766e858653c9776474005a6ae6d94828afgryzor stat_symb_map_items ExtModal = statSymbMapItems
7fb4c0766e858653c9776474005a6ae6d94828afgryzor stat_symb_items ExtModal = statSymbItems
7fb4c0766e858653c9776474005a6ae6d94828afgryzor symbol_to_raw ExtModal = symbolToRaw
7fb4c0766e858653c9776474005a6ae6d94828afgryzor id_to_raw ExtModal = idToRaw
7fb4c0766e858653c9776474005a6ae6d94828afgryzor matches ExtModal = CASL.Morphism.matches
7fb4c0766e858653c9776474005a6ae6d94828afgryzor empty_signature ExtModal = emptySign emptyEModalSign
7fb4c0766e858653c9776474005a6ae6d94828afgryzor signature_union ExtModal sgn = return . addSig addEModalSign sgn
7fb4c0766e858653c9776474005a6ae6d94828afgryzor intersection ExtModal sgn = return . interSig interEModalSign sgn
7fb4c0766e858653c9776474005a6ae6d94828afgryzor final_union ExtModal = finalUnion addEModalSign
7fb4c0766e858653c9776474005a6ae6d94828afgryzor morphism_union ExtModal = plainMorphismUnion addEModalSign
7fb4c0766e858653c9776474005a6ae6d94828afgryzor is_subsig ExtModal = isSubSig isSubEModalSign
7fb4c0766e858653c9776474005a6ae6d94828afgryzor subsig_inclusion ExtModal = sigInclusion emptyMorphExtension
7fb4c0766e858653c9776474005a6ae6d94828afgryzor generated_sign ExtModal = generatedSign emptyMorphExtension
7fb4c0766e858653c9776474005a6ae6d94828afgryzor cogenerated_sign ExtModal = cogeneratedSign emptyMorphExtension
888cb40bdeec5abf452bd85d6bf63b26d5913d4chumbedooh induced_from_morphism ExtModal = inducedFromMorphism emptyMorphExtension
888cb40bdeec5abf452bd85d6bf63b26d5913d4chumbedooh induced_from_to_morphism ExtModal =
888cb40bdeec5abf452bd85d6bf63b26d5913d4chumbedooh inducedFromToMorphism emptyMorphExtension isSubEModalSign
888cb40bdeec5abf452bd85d6bf63b26d5913d4chumbedooh diffEModalSign
888cb40bdeec5abf452bd85d6bf63b26d5913d4chumbedooh theory_to_taxonomy ExtModal = convTaxo
888cb40bdeec5abf452bd85d6bf63b26d5913d4chumbedoohinstance Logic ExtModal () EM_BASIC_SPEC ExtModalFORMULA SYMB_ITEMS
888cb40bdeec5abf452bd85d6bf63b26d5913d4chumbedooh SYMB_MAP_ITEMS ExtModalSign ExtModalMorph Symbol RawSymbol () where
7fb4c0766e858653c9776474005a6ae6d94828afgryzor stability _ = Experimental
7fb4c0766e858653c9776474005a6ae6d94828afgryzor empty_proof_tree _ = ()