CspCASL2Modal.hs revision e54c5af823b9775dd2c058185ea5bdf7593950fa
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederModule : $Header$
e6d40133bc9f858308654afb1262b8b483ec5922Till MossakowskiCopyright : (c) Till Mossakowski and Uni Bremen 2004
1549f3abf73c1122acff724f718b615c82fa3648Till MossakowskiLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederMaintainer : till@informatik.uni-bremen.de
3f69b6948966979163bdfe8331c38833d5d90ecdChristian MaederStability : provisional
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederPortability : non-portable (imports Logic.Logic)
f3a94a197960e548ecd6520bb768cb0d547457bbChristian MaederThe embedding comorphism from CspCASL to ModalCASL.
e6d40133bc9f858308654afb1262b8b483ec5922Till Mossakowski It keeps the CASL part and interprets the CspCASL LTS semantics as
1549f3abf73c1122acff724f718b615c82fa3648Till Mossakowski Kripke structure
ad270004874ce1d0697fb30d7309f180553bb315Christian Maederimport qualified Data.Set as Set
575a55eadc8dcab8ee350324b417cbd9e52e69c0Christian Maederimport CspCASL.AS_CspCASL (CspBasicSpec (..))
90c174bac60a72ffd81bc3bf5ae2dd9a61943b8bChristian Maeder-- | The identity of the comorphism
2561b4bfc45d280ee2be8a7870314670e4e682e4Christian Maederdata CspCASL2Modal = CspCASL2Modal deriving (Show)
aea143fff7a50aceb809845fbc42698b0b3f545aChristian Maederinstance Language CspCASL2Modal -- default definition is okay
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maederinstance Comorphism CspCASL2Modal
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski CspBasicSpec () SYMB_ITEMS SYMB_MAP_ITEMS
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder M_BASIC_SPEC ModalFORMULA SYMB_ITEMS SYMB_MAP_ITEMS
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder Symbol RawSymbol () where
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder sourceLogic CspCASL2Modal = CspCASL
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder sourceSublogic CspCASL2Modal = ()
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder targetLogic CspCASL2Modal = Modal
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder mapSublogic CspCASL2Modal _ = Just ()
16e124196c6b204769042028c74f533509c9b5d3Christian Maeder map_theory CspCASL2Modal = return . simpleTheoryMapping mapSig mapSen
4c7f058cdd19ce67b2b5d4b7f69703d0f8a21e38Christian Maeder map_morphism CspCASL2Modal = return . mapMor
16e124196c6b204769042028c74f533509c9b5d3Christian Maeder map_sentence CspCASL2Modal _ = return . mapSen
9eb39c7a0e7a1ddad1eec1d23c6d4e3a99c54023Christian Maeder map_symbol CspCASL2Modal = Set.singleton . mapSym
9eb39c7a0e7a1ddad1eec1d23c6d4e3a99c54023Christian MaedermapSig :: CspCASLSign -> MSign
9eb39c7a0e7a1ddad1eec1d23c6d4e3a99c54023Christian Maeder (emptySign emptyModalSign) {sortSet = sortSet sign
9eb39c7a0e7a1ddad1eec1d23c6d4e3a99c54023Christian Maeder , sortRel = sortRel sign
9eb39c7a0e7a1ddad1eec1d23c6d4e3a99c54023Christian Maeder , opMap = opMap sign
351145cfe8c03b4d47133c96b209f2bd6cfbf504Christian Maeder , assocOps = assocOps sign
351145cfe8c03b4d47133c96b209f2bd6cfbf504Christian Maeder , predMap = predMap sign }
3c8d067accf18572352351ec42ff905c7297a8a5Christian Maeder -- ??? add modalities
81101b83a042f5a1bdeeef93b1b49aff05817e44Christian MaedermapMor :: CspMorphism -> ModalMor
81101b83a042f5a1bdeeef93b1b49aff05817e44Christian MaedermapMor m = Morphism {msource = mapSig $ msource m
351145cfe8c03b4d47133c96b209f2bd6cfbf504Christian Maeder , mtarget = mapSig $ mtarget m
351145cfe8c03b4d47133c96b209f2bd6cfbf504Christian Maeder , sort_map = sort_map m
3c8d067accf18572352351ec42ff905c7297a8a5Christian Maeder , fun_map = fun_map m
81101b83a042f5a1bdeeef93b1b49aff05817e44Christian Maeder , pred_map = pred_map m
81101b83a042f5a1bdeeef93b1b49aff05817e44Christian Maeder , extended_map = ()}
81101b83a042f5a1bdeeef93b1b49aff05817e44Christian Maeder -- ??? add modalities
3c8d067accf18572352351ec42ff905c7297a8a5Christian MaedermapSym :: () -> Symbol
81101b83a042f5a1bdeeef93b1b49aff05817e44Christian MaedermapSym = error "CspCASL2Modal.mapSym not yet implemented"
81101b83a042f5a1bdeeef93b1b49aff05817e44Christian Maeder -- needs to be changed once modal symbols are added
9eb39c7a0e7a1ddad1eec1d23c6d4e3a99c54023Christian MaedermapSen :: () -> ModalFORMULA
d0c66a832d7b556e20ea4af4852cdc27a5463d51Christian MaedermapSen _f = True_atom nullRange
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder Quantification q vs frm ps ->
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder Quantification q vs (mapSen frm) ps
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder Conjunction fs ps ->
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder Conjunction (map mapSen fs) ps
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder Disjunction fs ps ->
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder Disjunction (map mapSen fs) ps
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder Implication f1 f2 b ps ->
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder Implication (mapSen f1) (mapSen f2) b ps
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder Equivalence f1 f2 ps ->
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder Equivalence (mapSen f1) (mapSen f2) ps
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder Negation frm ps -> Negation (mapSen frm) ps
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski True_atom ps -> True_atom ps
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder False_atom ps -> False_atom ps
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder Existl_equation t1 t2 ps ->
fa167e362877db231378e17ba49c66fbb84862fcChristian Maeder Existl_equation (mapTERM t1) (mapTERM t2) ps
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder Strong_equation t1 t2 ps ->
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder Strong_equation (mapTERM t1) (mapTERM t2) ps
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder Predication pn as qs ->
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder Predication pn (map mapTERM as) qs
6a22b2854c3bc9cb4877cb7d29049d6559238639Christian Maeder Definedness t ps -> Definedness (mapTERM t) ps
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder Membership t ty ps -> Membership (mapTERM t) ty ps
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder Sort_gen_ax constrs isFree -> Sort_gen_ax constrs isFree
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskimapTERM :: TERM () -> TERM M_FORMULA
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskimapTERM t = case t of
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski Qual_var v ty ps -> Qual_var v ty ps
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder Application opsym as qs -> Application opsym (map mapTERM as) qs
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder Sorted_term trm ty ps -> Sorted_term (mapTERM trm) ty ps
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder Cast trm ty ps -> Cast (mapTERM trm) ty ps
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder Conditional t1 f t2 ps ->
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder Conditional (mapTERM t1) (mapSen f) (mapTERM t2) ps