Logic_Modal.hs revision 781d04c5e02635caed8b98f0adcf559f9426a39c
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder{- |
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaederModule : $Header$
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaederCopyright : (c) Till Mossakowski, Uni Bremen 2002-2004
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaederLicence : similar to LGPL, see HetCATS/LICENCE.txt or LIZENZ.txt
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder
b4fbc96e05117839ca409f5f20f97b3ac872d1edTill MossakowskiMaintainer : hets@tzi.de
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaederStability : provisional
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaederPortability : portable
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder Instance of class Logic for modal logic.
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder-}
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder{- todo:
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder check preservation of rigidity of morphisms
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder-}
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maedermodule Modal.Logic_Modal where
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maederimport Modal.AS_Modal
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maederimport Modal.ModalSign
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maederimport Modal.ATC_Modal
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maederimport Modal.Parse_AS
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maederimport Modal.StatAna
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maederimport Modal.LaTeX_Modal
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maederimport CASL.Sign
d6025ee06343191f356a59704d467866afa29900Paolo Torriniimport CASL.StaticAna
ae59cddaa1f9e2dd031cae95a3ba867b9e8e095dPaolo Torriniimport CASL.Morphism
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maederimport CASL.SymbolMapAnalysis
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maederimport CASL.Logic_CASL
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maederimport CASL.AS_Basic_CASL
ae59cddaa1f9e2dd031cae95a3ba867b9e8e095dPaolo Torriniimport CASL.Parse_AS_Basic
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maederimport CASL.MapSentence
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maederimport CASL.SymbolParser
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maederimport Logic.Logic
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maederimport Data.Dynamic
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maederdata Modal = Modal deriving Show
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder
ae59cddaa1f9e2dd031cae95a3ba867b9e8e095dPaolo Torriniinstance Language Modal -- default definition is okay
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maedertype MSign = Sign M_FORMULA ModalSign
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maedertype ModalMor = Morphism M_FORMULA ModalSign ()
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maedertype ModalFORMULA = FORMULA M_FORMULA
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maedertc_M_FORMULA, tc_M_SIG_ITEM, tc_M_BASIC_ITEM, modalSignTc :: TyCon
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maedertc_M_FORMULA = mkTyCon "Modal.AS_Modal.M_FORMULA"
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maedertc_M_SIG_ITEM = mkTyCon "Modal.AS_Modal.M_SIG_ITEM"
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maedertc_M_BASIC_ITEM = mkTyCon "Modal.AS_Modal.M_BASIC_ITEM"
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaedermodalSignTc = mkTyCon "Modal.ModalSign.ModalSign"
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maederinstance Typeable M_FORMULA where
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder typeOf _ = mkAppTy tc_M_FORMULA []
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maederinstance Typeable M_SIG_ITEM where
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder typeOf _ = mkAppTy tc_M_SIG_ITEM []
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maederinstance Typeable M_BASIC_ITEM where
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder typeOf _ = mkAppTy tc_M_BASIC_ITEM []
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maederinstance Typeable ModalSign where
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder typeOf _ = mkAppTy modalSignTc []
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maederinstance Category Modal MSign ModalMor
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder where
10a92a06296c3c8d522543de7e3a4534bf528505Paolo Torrini -- ide :: id -> object -> morphism
10a92a06296c3c8d522543de7e3a4534bf528505Paolo Torrini ide Modal = idMor dummy
10a92a06296c3c8d522543de7e3a4534bf528505Paolo Torrini -- comp :: id -> morphism -> morphism -> Maybe morphism
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder comp Modal = compose (const id)
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder -- dom, cod :: id -> morphism -> object
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder dom Modal = msource
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder cod Modal = mtarget
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder -- legal_obj :: id -> object -> Bool
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder legal_obj Modal = legalSign
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder -- legal_mor :: id -> morphism -> Bool
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder legal_mor Modal = legalMor
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder-- abstract syntax, parsing (and printing)
eaa2614d79ad5ef6a6b9b08c7e6dde46c5ad1fb3Till Mossakowski
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maederinstance Syntax Modal M_BASIC_SPEC
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder SYMB_ITEMS SYMB_MAP_ITEMS
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder where
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder parse_basic_spec Modal = Just $ basicSpec modal_reserved_words
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder parse_symb_items Modal = Just $ symbItems modal_reserved_words
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder parse_symb_map_items Modal = Just $ symbMapItems modal_reserved_words
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder-- Modal logic
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maederinstance Sentences Modal ModalFORMULA () MSign ModalMor Symbol where
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder map_sen Modal = mapSen map_M_FORMULA
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder parse_sentence Modal = Nothing
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder sym_of Modal = symOf
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder symmap_of Modal = morphismToSymbMap
ae59cddaa1f9e2dd031cae95a3ba867b9e8e095dPaolo Torrini sym_name Modal = symName
ae59cddaa1f9e2dd031cae95a3ba867b9e8e095dPaolo Torrini provers Modal = []
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder cons_checkers Modal = []
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maederinstance StaticAnalysis Modal M_BASIC_SPEC ModalFORMULA ()
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder SYMB_ITEMS SYMB_MAP_ITEMS
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder MSign
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder ModalMor
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder Symbol RawSymbol where
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder basic_analysis Modal = Just $ basicAnalysis minExpForm
7f39d44f0b8c39a92606ba06fd668dc0cc2752caPaolo Torrini ana_M_BASIC_ITEM ana_M_SIG_ITEM
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder stat_symb_map_items Modal = statSymbMapItems
7f39d44f0b8c39a92606ba06fd668dc0cc2752caPaolo Torrini stat_symb_items Modal = statSymbItems
7f39d44f0b8c39a92606ba06fd668dc0cc2752caPaolo Torrini ensures_amalgamability Modal _ =
7f39d44f0b8c39a92606ba06fd668dc0cc2752caPaolo Torrini fail "Modal: ensures_amalgamability nyi" -- ???
7f39d44f0b8c39a92606ba06fd668dc0cc2752caPaolo Torrini
7f39d44f0b8c39a92606ba06fd668dc0cc2752caPaolo Torrini sign_to_basic_spec Modal _sigma _sens = Basic_spec [] -- ???
7f39d44f0b8c39a92606ba06fd668dc0cc2752caPaolo Torrini
7f39d44f0b8c39a92606ba06fd668dc0cc2752caPaolo Torrini symbol_to_raw Modal = symbolToRaw
7f39d44f0b8c39a92606ba06fd668dc0cc2752caPaolo Torrini id_to_raw Modal = idToRaw
matches Modal = CASL.Morphism.matches
empty_signature Modal = emptySign emptyModalSign
signature_union Modal sigma1 sigma2 =
return $ addSig sigma1 sigma2
morphism_union Modal = morphismUnion (const id)
final_union Modal = finalUnion
is_subsig Modal = isSubSig
inclusion Modal = sigInclusion dummy
cogenerated_sign Modal = cogeneratedSign dummy
generated_sign Modal = generatedSign dummy
induced_from_morphism Modal = inducedFromMorphism dummy
induced_from_to_morphism Modal = inducedFromToMorphism dummy
instance Logic Modal ()
M_BASIC_SPEC ModalFORMULA SYMB_ITEMS SYMB_MAP_ITEMS
MSign
ModalMor
Symbol RawSymbol () where
min_sublogic_basic_spec Modal _basic_spec = ()
min_sublogic_sentence Modal _sentence = ()
min_sublogic_symb_items Modal _symb_items = ()
min_sublogic_symb_map_items Modal _symb_map_items = ()
min_sublogic_sign Modal _sign = ()
min_sublogic_morphism Modal _morphism = ()
min_sublogic_symbol Modal _symbol = ()
-- sublogic_names Modal _ = ["Modal"]
-- all_sublogics Modal = [()]