hets/Modal/Logic_Modal.hs

	Logic_Modal.hs revision a10ff6125d62484ec5961c8a5d9d1c5a3e14fa66
5693N/A{- |
5693N/AModule      :  $Header$
5693N/ADescription :  Instance of class Logic for Modal CASL
5693N/ACopyright   :  (c) Till Mossakowski, Uni Bremen 2002-2004
5693N/ALicense     :  similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
5693N/A
5693N/AMaintainer  :  luecke@informatik.uni-bremen.de
5693N/AStability   :  provisional
5693N/APortability :  portable
5693N/A
5693N/AInstance of class Logic for modal logic.
5693N/A-}
5693N/A
5693N/Amodule Modal.Logic_Modal where
5693N/A
5693N/Aimport Logic.Logic
5693N/A
5693N/Aimport Modal.AS_Modal
5693N/Aimport Modal.ModalSign
5693N/Aimport Modal.ATC_Modal ()
5693N/Aimport Modal.Parse_AS
5693N/Aimport Modal.Print_AS
5693N/Aimport Modal.StatAna
5693N/A
5693N/Aimport CASL.Sign
5693N/Aimport CASL.Morphism
5693N/Aimport CASL.SymbolMapAnalysis
5693N/Aimport CASL.AS_Basic_CASL
5693N/Aimport CASL.Parse_AS_Basic
5693N/Aimport CASL.MapSentence
5693N/Aimport CASL.SimplifySen
5693N/Aimport CASL.SymbolParser
5693N/Aimport CASL.Taxonomy
5693N/Aimport CASL.Logic_CASL (SignExtension(..))
5693N/A
5693N/Aimport Common.DocUtils
5693N/A
5693N/Adata Modal = Modal deriving Show
5693N/A
5693N/Ainstance Language Modal  where
5693N/A description _ = unlines
5693N/A  [ "ModalCASL extends CASL by modal operators. Syntax for ordinary"
5693N/A  , "modalities, multi-modal logics as well as  term-modal"
5693N/A  , "logic (also covering dynamic logic) is provided."
5693N/A  , "Specific modal logics can be obtained via restrictions to"
5693N/A  , "sublanguages." ]
5693N/A
5693N/Atype MSign = Sign M_FORMULA ModalSign
5693N/Atype ModalMor = Morphism M_FORMULA ModalSign ()
5693N/Atype ModalFORMULA = FORMULA M_FORMULA
5693N/A
5693N/Ainstance SignExtension ModalSign where
5693N/A  isSubSignExtension = isSubModalSign
5693N/A
5693N/Ainstance Syntax Modal M_BASIC_SPEC SYMB_ITEMS SYMB_MAP_ITEMS where
5693N/A    parse_basic_spec Modal = Just $ basicSpec modal_reserved_words
5693N/A    parse_symb_items Modal = Just $ symbItems modal_reserved_words
5693N/A    parse_symb_map_items Modal = Just $ symbMapItems modal_reserved_words
5693N/A
5693N/A-- Modal logic
5693N/A
5693N/Amap_M_FORMULA :: MapSen M_FORMULA ModalSign ()
5693N/Amap_M_FORMULA mor (BoxOrDiamond b m f ps) =
5693N/A    let newM = case m of
5693N/A                   Simple_mod _ -> m
5693N/A                   Term_mod t -> let newT = mapTerm map_M_FORMULA mor t
5693N/A                                 in Term_mod newT
5693N/A        newF = mapSen map_M_FORMULA mor f
5693N/A    in BoxOrDiamond b newM newF ps
5693N/A
5693N/Ainstance Sentences Modal ModalFORMULA MSign ModalMor Symbol where
5693N/A      map_sen Modal m = return . mapSen map_M_FORMULA m
5693N/A      parse_sentence Modal = Nothing
5693N/A      sym_of Modal = symOf
5693N/A      symmap_of Modal = morphismToSymbMap
5693N/A      sym_name Modal = symName
5693N/A      simplify_sen Modal = simplifySen minExpForm simModal
5693N/A      print_sign Modal sig = printSign pretty
5693N/A          (printModalSign $ simplifySen minExpForm simModal sig) sig
5693N/A
5693N/A-- simplifySen for ExtFORMULA
5693N/AsimModal :: Sign M_FORMULA ModalSign -> M_FORMULA -> M_FORMULA
5693N/AsimModal sign (BoxOrDiamond b md form pos) =
5693N/A    let mod' = case md of
5693N/A                        Term_mod term -> Term_mod $ rmTypesT minExpForm
5693N/A                                         simModal sign term
5693N/A                        t -> t
5693N/A    in BoxOrDiamond b mod'
5693N/A                 (simplifySen minExpForm simModal sign form) pos
5693N/A
5693N/ArmTypesExt :: a -> b -> b
5693N/ArmTypesExt _ f = f
5693N/A
5693N/Ainstance StaticAnalysis Modal M_BASIC_SPEC ModalFORMULA
5693N/A               SYMB_ITEMS SYMB_MAP_ITEMS
5693N/A               MSign
5693N/A               ModalMor
5693N/A               Symbol RawSymbol where
5693N/A         basic_analysis Modal = Just $ basicModalAnalysis
5693N/A         stat_symb_map_items Modal = statSymbMapItems
5693N/A         stat_symb_items Modal = statSymbItems
5693N/A
5693N/A         symbol_to_raw Modal = symbolToRaw
5693N/A         id_to_raw Modal = idToRaw
5693N/A         matches Modal = CASL.Morphism.matches
5693N/A
5693N/A         empty_signature Modal = emptySign emptyModalSign
5693N/A         signature_union Modal s = return . addSig addModalSign s
5693N/A         intersection Modal s = return . interSig interModalSign s
5693N/A         morphism_union Modal = morphismUnion (const id) addModalSign
5693N/A         final_union Modal = finalUnion addModalSign
5693N/A         inclusion Modal = sigInclusion () isSubModalSign diffModalSign
5693N/A         cogenerated_sign Modal = cogeneratedSign () isSubModalSign
5693N/A         generated_sign Modal = generatedSign () isSubModalSign
5693N/A         induced_from_morphism Modal = inducedFromMorphism () isSubModalSign
5693N/A         induced_from_to_morphism Modal =
5693N/A             inducedFromToMorphism () isSubModalSign diffModalSign
5693N/A         theory_to_taxonomy Modal = convTaxo
5693N/A
5693N/Ainstance Logic Modal ()
5693N/A               M_BASIC_SPEC ModalFORMULA SYMB_ITEMS SYMB_MAP_ITEMS
5693N/A               MSign
5693N/A               ModalMor
5693N/A               Symbol RawSymbol () where
5693N/A         stability _ = Unstable
5693N/A         empty_proof_tree _ = ()
5693N/A