CspCASL2Modal.hs revision 3b48e17c1da54ee669e70b626d9fbc32ce495b2c
05bf9cbe382548c2665dd01a6a402640c9ec3813Christian Maeder{-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances #-}
a0c2edf89c8b51141bc8919b920c85548e388d00Till MossakowskiModule : $Header$
a0c2edf89c8b51141bc8919b920c85548e388d00Till MossakowskiCopyright : (c) Till Mossakowski and Uni Bremen 2004
98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuLicense : GPLv2 or higher, see LICENSE.txt
2eeec5240b424984e3ee26296da1eeab6c6d739eChristian MaederMaintainer : till@informatik.uni-bremen.de
a0c2edf89c8b51141bc8919b920c85548e388d00Till MossakowskiStability : provisional
a0c2edf89c8b51141bc8919b920c85548e388d00Till MossakowskiPortability : non-portable (imports Logic.Logic)
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
ad270004874ce1d0697fb30d7309f180553bb315Christian Maederimport qualified Data.Set as Set
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reillyimport CspCASL.AS_CspCASL (CspBasicSpec (..))
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reillyimport CspCASL.Morphism (CspCASLMorphism)
a0c2edf89c8b51141bc8919b920c85548e388d00Till Mossakowski-- | The identity of the comorphism
a0c2edf89c8b51141bc8919b920c85548e388d00Till Mossakowskidata CspCASL2Modal = CspCASL2Modal deriving (Show)
a0c2edf89c8b51141bc8919b920c85548e388d00Till Mossakowskiinstance Language CspCASL2Modal -- default definition is okay
a0c2edf89c8b51141bc8919b920c85548e388d00Till Mossakowskiinstance Comorphism CspCASL2Modal
3b48e17c1da54ee669e70b626d9fbc32ce495b2cChristian Maeder CspCASL () CspBasicSpec CspCASLSen SymbItems SymbMapItems
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 ()
7592d4dc0461feff73113f4679e0b1823fd117faChristian Maeder map_theory CspCASL2Modal = return . simpleTheoryMapping mapSig mapSen
578b677874296e4ba48e57b5e4b4b0270d995603Christian Maeder map_morphism CspCASL2Modal = return . mapMor
578b677874296e4ba48e57b5e4b4b0270d995603Christian Maeder map_sentence CspCASL2Modal _ = return . mapSen
e54c5af823b9775dd2c058185ea5bdf7593950faAndy GimblettmapSig :: CspCASLSign -> MSign
a0c2edf89c8b51141bc8919b920c85548e388d00Till Mossakowski (emptySign emptyModalSign) {sortSet = sortSet sign
e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian Maeder , sortRel = sortRel sign
a0c2edf89c8b51141bc8919b920c85548e388d00Till Mossakowski , opMap = opMap sign
e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian Maeder , assocOps = assocOps sign
e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian Maeder , predMap = predMap sign }
a0c2edf89c8b51141bc8919b920c85548e388d00Till Mossakowski -- ??? add modalities
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'ReillymapMor :: CspCASLMorphism -> ModalMor
9eb39c7a0e7a1ddad1eec1d23c6d4e3a99c54023Christian MaedermapMor m = (embedMorphism emptyMorExt (mapSig $ msource m) $ mapSig $ mtarget m)
2b2f3b72e82e28b34db9c69af2d1ec38f228272eChristian Maeder { sort_map = sort_map m
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder , op_map = op_map m
2b2f3b72e82e28b34db9c69af2d1ec38f228272eChristian Maeder , pred_map = pred_map m }
a0c2edf89c8b51141bc8919b920c85548e388d00Till Mossakowski -- ??? add modalities
765e55b764e0fd32c09d33709d6e2770c4766799Christian MaedermapSym :: Symbol -> Symbol
a0c2edf89c8b51141bc8919b920c85548e388d00Till MossakowskimapSym = error "CspCASL2Modal.mapSym not yet implemented"
a0c2edf89c8b51141bc8919b920c85548e388d00Till Mossakowski -- needs to be changed once modal symbols are added
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'ReillymapSen :: CspCASLSen -> ModalFORMULA
42c01284bba8d7c8d995c8dfb96ace57d28ed1bcTill MossakowskimapSen _f = True_atom nullRange
a0c2edf89c8b51141bc8919b920c85548e388d00Till Mossakowski Quantification q vs frm ps ->
e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian Maeder Quantification q vs (mapSen frm) ps
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder Conjunction fs ps ->
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder Conjunction (map mapSen fs) ps
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder Disjunction fs ps ->
a0c2edf89c8b51141bc8919b920c85548e388d00Till Mossakowski Disjunction (map mapSen fs) ps
a0c2edf89c8b51141bc8919b920c85548e388d00Till Mossakowski Implication f1 f2 b ps ->
e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian Maeder Implication (mapSen f1) (mapSen f2) b ps
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder Equivalence f1 f2 ps ->
e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian Maeder Equivalence (mapSen f1) (mapSen f2) ps
a0c2edf89c8b51141bc8919b920c85548e388d00Till Mossakowski Negation frm ps -> Negation (mapSen frm) ps
a0c2edf89c8b51141bc8919b920c85548e388d00Till Mossakowski True_atom ps -> True_atom ps
a0c2edf89c8b51141bc8919b920c85548e388d00Till Mossakowski False_atom ps -> False_atom ps
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder Existl_equation t1 t2 ps ->
e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian Maeder Existl_equation (mapTERM t1) (mapTERM t2) ps
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder Strong_equation t1 t2 ps ->
e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian Maeder Strong_equation (mapTERM t1) (mapTERM t2) ps
a0c2edf89c8b51141bc8919b920c85548e388d00Till Mossakowski Predication pn as qs ->
a0c2edf89c8b51141bc8919b920c85548e388d00Till Mossakowski Predication pn (map mapTERM as) qs
a0c2edf89c8b51141bc8919b920c85548e388d00Till Mossakowski Definedness t ps -> Definedness (mapTERM t) ps
a0c2edf89c8b51141bc8919b920c85548e388d00Till Mossakowski Membership t ty ps -> Membership (mapTERM t) ty ps
a0c2edf89c8b51141bc8919b920c85548e388d00Till Mossakowski Sort_gen_ax constrs isFree -> Sort_gen_ax constrs isFree
a0c2edf89c8b51141bc8919b920c85548e388d00Till MossakowskimapTERM :: TERM () -> TERM M_FORMULA
a0c2edf89c8b51141bc8919b920c85548e388d00Till MossakowskimapTERM t = case t of
a0c2edf89c8b51141bc8919b920c85548e388d00Till Mossakowski Qual_var v ty ps -> Qual_var v ty ps
a0c2edf89c8b51141bc8919b920c85548e388d00Till Mossakowski Application opsym as qs -> Application opsym (map mapTERM as) qs
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder Sorted_term trm ty ps -> Sorted_term (mapTERM trm) ty ps
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder Cast trm ty ps -> Cast (mapTERM trm) ty ps
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder Conditional t1 f t2 ps ->
a0c2edf89c8b51141bc8919b920c85548e388d00Till Mossakowski Conditional (mapTERM t1) (mapSen f) (mapTERM t2) ps