CspCASL2Modal.hs revision f3a94a197960e548ecd6520bb768cb0d547457bb
a0c2edf89c8b51141bc8919b920c85548e388d00Till Mossakowski{- |
a0c2edf89c8b51141bc8919b920c85548e388d00Till MossakowskiModule : $Header$
a0c2edf89c8b51141bc8919b920c85548e388d00Till MossakowskiCopyright : (c) Till Mossakowski and Uni Bremen 2004
97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian MaederLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
a0c2edf89c8b51141bc8919b920c85548e388d00Till Mossakowski
b4fbc96e05117839ca409f5f20f97b3ac872d1edTill MossakowskiMaintainer : till@tzi.de
a0c2edf89c8b51141bc8919b920c85548e388d00Till MossakowskiStability : provisional
a0c2edf89c8b51141bc8919b920c85548e388d00Till MossakowskiPortability : non-portable (imports Logic.Logic)
a0c2edf89c8b51141bc8919b920c85548e388d00Till Mossakowski
f3a94a197960e548ecd6520bb768cb0d547457bbChristian MaederThe embedding comorphism from CspCASL to ModalCASL.
a0c2edf89c8b51141bc8919b920c85548e388d00Till Mossakowski 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 Mossakowskiimport qualified Common.Lib.Set as Set
a0c2edf89c8b51141bc8919b920c85548e388d00Till Mossakowski
a0c2edf89c8b51141bc8919b920c85548e388d00Till Mossakowski-- CASL
a0c2edf89c8b51141bc8919b920c85548e388d00Till Mossakowskiimport CASL.Sign
a0c2edf89c8b51141bc8919b920c85548e388d00Till Mossakowskiimport CASL.AS_Basic_CASL
a0c2edf89c8b51141bc8919b920c85548e388d00Till Mossakowskiimport CASL.Morphism
a0c2edf89c8b51141bc8919b920c85548e388d00Till Mossakowski
a0c2edf89c8b51141bc8919b920c85548e388d00Till Mossakowski-- CspCASL
a0c2edf89c8b51141bc8919b920c85548e388d00Till Mossakowskiimport CspCASL.Logic_CspCASL
a0c2edf89c8b51141bc8919b920c85548e388d00Till Mossakowskiimport CspCASL.SignCSP
a0c2edf89c8b51141bc8919b920c85548e388d00Till Mossakowskiimport CspCASL.AS_CSP_CASL
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
a0c2edf89c8b51141bc8919b920c85548e388d00Till Mossakowski CspCASL ()
a0c2edf89c8b51141bc8919b920c85548e388d00Till Mossakowski Basic_CSP_CASL_C_SPEC () SYMB_ITEMS SYMB_MAP_ITEMS
a0c2edf89c8b51141bc8919b920c85548e388d00Till Mossakowski CSPSign
a0c2edf89c8b51141bc8919b920c85548e388d00Till Mossakowski CSPMorphism
a0c2edf89c8b51141bc8919b920c85548e388d00Till Mossakowski () () ()
a0c2edf89c8b51141bc8919b920c85548e388d00Till Mossakowski Modal ()
a0c2edf89c8b51141bc8919b920c85548e388d00Till Mossakowski M_BASIC_SPEC ModalFORMULA SYMB_ITEMS SYMB_MAP_ITEMS
a0c2edf89c8b51141bc8919b920c85548e388d00Till Mossakowski MSign
a0c2edf89c8b51141bc8919b920c85548e388d00Till Mossakowski ModalMor
a0c2edf89c8b51141bc8919b920c85548e388d00Till Mossakowski Symbol RawSymbol () where
a0c2edf89c8b51141bc8919b920c85548e388d00Till Mossakowski sourceLogic CspCASL2Modal = CspCASL
a0c2edf89c8b51141bc8919b920c85548e388d00Till Mossakowski sourceSublogic CspCASL2Modal = ()
a0c2edf89c8b51141bc8919b920c85548e388d00Till Mossakowski targetLogic CspCASL2Modal = Modal
a0c2edf89c8b51141bc8919b920c85548e388d00Till Mossakowski targetSublogic CspCASL2Modal = ()
7592d4dc0461feff73113f4679e0b1823fd117faChristian Maeder map_theory CspCASL2Modal = return . simpleTheoryMapping mapSig mapSen
578b677874296e4ba48e57b5e4b4b0270d995603Christian Maeder map_morphism CspCASL2Modal = return . mapMor
578b677874296e4ba48e57b5e4b4b0270d995603Christian Maeder map_sentence CspCASL2Modal _ = return . mapSen
88ece6e49930670e8fd3ee79c89a2e918d2fbd0cChristian Maeder map_symbol CspCASL2Modal = Set.singleton . mapSym
a0c2edf89c8b51141bc8919b920c85548e388d00Till Mossakowski
a0c2edf89c8b51141bc8919b920c85548e388d00Till MossakowskimapSig :: CSPSign -> MSign
a0c2edf89c8b51141bc8919b920c85548e388d00Till MossakowskimapSig sign =
a0c2edf89c8b51141bc8919b920c85548e388d00Till Mossakowski (emptySign emptyModalSign) {sortSet = sortSet sign
a0c2edf89c8b51141bc8919b920c85548e388d00Till Mossakowski , sortRel = sortRel sign
a0c2edf89c8b51141bc8919b920c85548e388d00Till Mossakowski , opMap = opMap sign
a0c2edf89c8b51141bc8919b920c85548e388d00Till Mossakowski , assocOps = assocOps sign
a0c2edf89c8b51141bc8919b920c85548e388d00Till Mossakowski , predMap = predMap sign }
a0c2edf89c8b51141bc8919b920c85548e388d00Till Mossakowski -- ??? add modalities
a0c2edf89c8b51141bc8919b920c85548e388d00Till Mossakowski
a0c2edf89c8b51141bc8919b920c85548e388d00Till MossakowskimapMor :: CSPMorphism -> ModalMor
a0c2edf89c8b51141bc8919b920c85548e388d00Till MossakowskimapMor m = Morphism {msource = mapSig $ msource m
a0c2edf89c8b51141bc8919b920c85548e388d00Till Mossakowski , mtarget = mapSig $ mtarget m
a0c2edf89c8b51141bc8919b920c85548e388d00Till Mossakowski , sort_map = sort_map m
a0c2edf89c8b51141bc8919b920c85548e388d00Till Mossakowski , fun_map = fun_map m
a0c2edf89c8b51141bc8919b920c85548e388d00Till Mossakowski , pred_map = pred_map m
a0c2edf89c8b51141bc8919b920c85548e388d00Till Mossakowski , extended_map = ()}
a0c2edf89c8b51141bc8919b920c85548e388d00Till Mossakowski -- ??? add modalities
a0c2edf89c8b51141bc8919b920c85548e388d00Till Mossakowski
a0c2edf89c8b51141bc8919b920c85548e388d00Till Mossakowski
a0c2edf89c8b51141bc8919b920c85548e388d00Till MossakowskimapSym :: () -> Symbol
a0c2edf89c8b51141bc8919b920c85548e388d00Till MossakowskimapSym = error "CspCASL2Modal.mapSym not yet implemented"
a0c2edf89c8b51141bc8919b920c85548e388d00Till Mossakowski -- needs to be changed once modal symbols are added
a0c2edf89c8b51141bc8919b920c85548e388d00Till Mossakowski
a0c2edf89c8b51141bc8919b920c85548e388d00Till Mossakowski
a0c2edf89c8b51141bc8919b920c85548e388d00Till MossakowskimapSen :: () -> ModalFORMULA
578b677874296e4ba48e57b5e4b4b0270d995603Christian MaedermapSen _f = True_atom []
a0c2edf89c8b51141bc8919b920c85548e388d00Till Mossakowski
a0c2edf89c8b51141bc8919b920c85548e388d00Till Mossakowski{- case f of
a0c2edf89c8b51141bc8919b920c85548e388d00Till Mossakowski Quantification q vs frm ps ->
a0c2edf89c8b51141bc8919b920c85548e388d00Till Mossakowski Quantification q vs (mapSen frm) ps
a0c2edf89c8b51141bc8919b920c85548e388d00Till Mossakowski Conjunction fs ps ->
a0c2edf89c8b51141bc8919b920c85548e388d00Till Mossakowski Conjunction (map mapSen fs) ps
a0c2edf89c8b51141bc8919b920c85548e388d00Till Mossakowski Disjunction fs ps ->
a0c2edf89c8b51141bc8919b920c85548e388d00Till Mossakowski Disjunction (map mapSen fs) ps
a0c2edf89c8b51141bc8919b920c85548e388d00Till Mossakowski Implication f1 f2 b ps ->
a0c2edf89c8b51141bc8919b920c85548e388d00Till Mossakowski Implication (mapSen f1) (mapSen f2) b ps
a0c2edf89c8b51141bc8919b920c85548e388d00Till Mossakowski Equivalence f1 f2 ps ->
a0c2edf89c8b51141bc8919b920c85548e388d00Till Mossakowski 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
a0c2edf89c8b51141bc8919b920c85548e388d00Till Mossakowski Existl_equation t1 t2 ps ->
a0c2edf89c8b51141bc8919b920c85548e388d00Till Mossakowski Existl_equation (mapTERM t1) (mapTERM t2) ps
a0c2edf89c8b51141bc8919b920c85548e388d00Till Mossakowski Strong_equation t1 t2 ps ->
a0c2edf89c8b51141bc8919b920c85548e388d00Till Mossakowski 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 Mossakowski _ -> error "CspCASL2Modal.mapSen"
a0c2edf89c8b51141bc8919b920c85548e388d00Till Mossakowski
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
a0c2edf89c8b51141bc8919b920c85548e388d00Till Mossakowski Sorted_term trm ty ps -> Sorted_term (mapTERM trm) ty ps
a0c2edf89c8b51141bc8919b920c85548e388d00Till Mossakowski Cast trm ty ps -> Cast (mapTERM trm) ty ps
a0c2edf89c8b51141bc8919b920c85548e388d00Till Mossakowski Conditional t1 f t2 ps ->
a0c2edf89c8b51141bc8919b920c85548e388d00Till Mossakowski Conditional (mapTERM t1) (mapSen f) (mapTERM t2) ps
a0c2edf89c8b51141bc8919b920c85548e388d00Till Mossakowski _ -> error "CspCASL2Modal.mapTERM"
a0c2edf89c8b51141bc8919b920c85548e388d00Till Mossakowski
8f1a4a6c8c0f098e5253c03eafe50aead6e8873cChristian Maeder-}