55cf6e01272ec475edea32aa9b7923de2d36cb42Christian Maeder{-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances, FlexibleInstances #-}
a0c2edf89c8b51141bc8919b920c85548e388d00Till Mossakowski{- |
e9458b1a7a19a63aa4c179f9ab20f4d50681c168Jens ElknerModule : ./Comorphisms/CspCASL2Modal.hs
a0c2edf89c8b51141bc8919b920c85548e388d00Till MossakowskiCopyright : (c) Till Mossakowski and Uni Bremen 2004
98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuLicense : GPLv2 or higher, see LICENSE.txt
a0c2edf89c8b51141bc8919b920c85548e388d00Till Mossakowski
2eeec5240b424984e3ee26296da1eeab6c6d739eChristian MaederMaintainer : till@informatik.uni-bremen.de
a0c2edf89c8b51141bc8919b920c85548e388d00Till MossakowskiStability : provisional
a0c2edf89c8b51141bc8919b920c85548e388d00Till MossakowskiPortability : non-portable (imports Logic.Logic)
a0c2edf89c8b51141bc8919b920c85548e388d00Till Mossakowski
f3a94a197960e548ecd6520bb768cb0d547457bbChristian MaederThe embedding comorphism from CspCASL to ModalCASL.
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder It keeps the CASL part and interprets the CspCASL LTS semantics as
a0c2edf89c8b51141bc8919b920c85548e388d00Till Mossakowski Kripke structure
a0c2edf89c8b51141bc8919b920c85548e388d00Till Mossakowski-}
a0c2edf89c8b51141bc8919b920c85548e388d00Till Mossakowski
a0c2edf89c8b51141bc8919b920c85548e388d00Till Mossakowskimodule Comorphisms.CspCASL2Modal where
a0c2edf89c8b51141bc8919b920c85548e388d00Till Mossakowski
a0c2edf89c8b51141bc8919b920c85548e388d00Till Mossakowskiimport Logic.Logic
a0c2edf89c8b51141bc8919b920c85548e388d00Till Mossakowskiimport Logic.Comorphism
a0c2edf89c8b51141bc8919b920c85548e388d00Till Mossakowski
a0c2edf89c8b51141bc8919b920c85548e388d00Till Mossakowski-- CASL
a0c2edf89c8b51141bc8919b920c85548e388d00Till Mossakowskiimport CASL.Sign
a0c2edf89c8b51141bc8919b920c85548e388d00Till Mossakowskiimport CASL.AS_Basic_CASL
a0c2edf89c8b51141bc8919b920c85548e388d00Till Mossakowskiimport CASL.Morphism
a0c2edf89c8b51141bc8919b920c85548e388d00Till Mossakowski
a0c2edf89c8b51141bc8919b920c85548e388d00Till Mossakowski-- CspCASL
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maederimport CspCASL.Logic_CspCASL
a0c2edf89c8b51141bc8919b920c85548e388d00Till Mossakowskiimport CspCASL.SignCSP
12b2ae689353ecbaad720a9af9f9be01c1a3fe2dChristian Maederimport CspCASL.StatAnaCSP (CspBasicSpec)
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reillyimport CspCASL.Morphism (CspCASLMorphism)
3b48e17c1da54ee669e70b626d9fbc32ce495b2cChristian Maederimport CspCASL.SymbItems
3b48e17c1da54ee669e70b626d9fbc32ce495b2cChristian Maederimport CspCASL.Symbol
a0c2edf89c8b51141bc8919b920c85548e388d00Till Mossakowski
a0c2edf89c8b51141bc8919b920c85548e388d00Till Mossakowski-- ModalCASL
a0c2edf89c8b51141bc8919b920c85548e388d00Till Mossakowskiimport Modal.Logic_Modal
a0c2edf89c8b51141bc8919b920c85548e388d00Till Mossakowskiimport Modal.AS_Modal
a0c2edf89c8b51141bc8919b920c85548e388d00Till Mossakowskiimport Modal.ModalSign
a0c2edf89c8b51141bc8919b920c85548e388d00Till Mossakowski
a0c2edf89c8b51141bc8919b920c85548e388d00Till Mossakowski-- | The identity of the comorphism
a0c2edf89c8b51141bc8919b920c85548e388d00Till Mossakowskidata CspCASL2Modal = CspCASL2Modal deriving (Show)
a0c2edf89c8b51141bc8919b920c85548e388d00Till Mossakowski
a0c2edf89c8b51141bc8919b920c85548e388d00Till Mossakowskiinstance Language CspCASL2Modal -- default definition is okay
a0c2edf89c8b51141bc8919b920c85548e388d00Till Mossakowski
a0c2edf89c8b51141bc8919b920c85548e388d00Till Mossakowskiinstance Comorphism CspCASL2Modal
23a0d43ca980983c7d7aebaa9f03bfe120be7de8Christian Maeder CspCASL () CspBasicSpec CspCASLSen CspSymbItems CspSymbMapItems
3b48e17c1da54ee669e70b626d9fbc32ce495b2cChristian Maeder CspCASLSign CspCASLMorphism CspSymbol CspRawSymbol ()
3b48e17c1da54ee669e70b626d9fbc32ce495b2cChristian Maeder Modal () M_BASIC_SPEC ModalFORMULA SYMB_ITEMS SYMB_MAP_ITEMS
3b48e17c1da54ee669e70b626d9fbc32ce495b2cChristian Maeder MSign ModalMor Symbol RawSymbol () where
286f4deb69d3912337bb09dd7f81284d12912ce8Christian Maeder sourceLogic CspCASL2Modal = cspCASL
a0c2edf89c8b51141bc8919b920c85548e388d00Till Mossakowski sourceSublogic CspCASL2Modal = ()
a0c2edf89c8b51141bc8919b920c85548e388d00Till Mossakowski targetLogic CspCASL2Modal = Modal
bba825b39570777866d560bfde3807731131097eKlaus Luettich mapSublogic CspCASL2Modal _ = Just ()
b5056cf24da461ee868c4be7b803a76b677fa21dChristian Maeder map_theory CspCASL2Modal = return . embedTheory mapSen emptyModalSign
b5056cf24da461ee868c4be7b803a76b677fa21dChristian Maeder map_morphism CspCASL2Modal = return . mapCASLMor emptyModalSign emptyMorExt
578b677874296e4ba48e57b5e4b4b0270d995603Christian Maeder map_sentence CspCASL2Modal _ = return . mapSen
a0c2edf89c8b51141bc8919b920c85548e388d00Till Mossakowski
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'ReillymapSen :: CspCASLSen -> ModalFORMULA
94e112d16f89130a688db8b03ad3224903f5e97eChristian MaedermapSen _ = trueForm