CspCASL2Modal.hs revision 41486a487c9b065d4d9d1a8adf63c00925cd455b
a0c2edf89c8b51141bc8919b920c85548e388d00Till MossakowskiModule : $Header$
a0c2edf89c8b51141bc8919b920c85548e388d00Till MossakowskiCopyright : (c) Till Mossakowski and Uni Bremen 2004
97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian MaederLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.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
61051521e4d82769a47f23aecb5fb477de47d534Andy Gimblettimport CspCASL.AS_CspCASL (CspBasicSpec (..))
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
61051521e4d82769a47f23aecb5fb477de47d534Andy Gimblett CspBasicSpec () SYMB_ITEMS SYMB_MAP_ITEMS
a0c2edf89c8b51141bc8919b920c85548e388d00Till Mossakowski M_BASIC_SPEC ModalFORMULA SYMB_ITEMS SYMB_MAP_ITEMS
a0c2edf89c8b51141bc8919b920c85548e388d00Till Mossakowski Symbol RawSymbol () where
a0c2edf89c8b51141bc8919b920c85548e388d00Till Mossakowski 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
88ece6e49930670e8fd3ee79c89a2e918d2fbd0cChristian Maeder map_symbol CspCASL2Modal = Set.singleton . mapSym
41486a487c9b065d4d9d1a8adf63c00925cd455bAndy GimblettmapSig :: CspSign -> 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
41486a487c9b065d4d9d1a8adf63c00925cd455bAndy GimblettmapMor :: CspMorphism -> ModalMor
a0c2edf89c8b51141bc8919b920c85548e388d00Till MossakowskimapMor m = Morphism {msource = mapSig $ msource m
e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian Maeder , 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
e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian Maeder , extended_map = ()}
a0c2edf89c8b51141bc8919b920c85548e388d00Till Mossakowski -- ??? add modalities
a0c2edf89c8b51141bc8919b920c85548e388d00Till MossakowskimapSym :: () -> Symbol
a0c2edf89c8b51141bc8919b920c85548e388d00Till MossakowskimapSym = error "CspCASL2Modal.mapSym not yet implemented"
a0c2edf89c8b51141bc8919b920c85548e388d00Till Mossakowski -- needs to be changed once modal symbols are added
a0c2edf89c8b51141bc8919b920c85548e388d00Till MossakowskimapSen :: () -> 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