6be66de4257f4f564e35f7b8ee57a282e3cf3e96vboxsync{- |

9eb499828dd875d229531b50d05f016b8a1f1dd9vboxsyncModule : $Header$

365b40dec2ed01d9983d29e276e7431c5a4a9c18vboxsyncCopyright : (c) Till Mossakowski and Uni Bremen 2004

9eb499828dd875d229531b50d05f016b8a1f1dd9vboxsyncLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt

9eb499828dd875d229531b50d05f016b8a1f1dd9vboxsync

9eb499828dd875d229531b50d05f016b8a1f1dd9vboxsyncMaintainer : till@informatik.uni-bremen.de

9eb499828dd875d229531b50d05f016b8a1f1dd9vboxsyncStability : provisional

9eb499828dd875d229531b50d05f016b8a1f1dd9vboxsyncPortability : non-portable (imports Logic.Logic)

9eb499828dd875d229531b50d05f016b8a1f1dd9vboxsync

9eb499828dd875d229531b50d05f016b8a1f1dd9vboxsyncThe embedding comorphism from CspCASL to ModalCASL.

9eb499828dd875d229531b50d05f016b8a1f1dd9vboxsync It keeps the CASL part and interprets the CspCASL LTS semantics as

9eb499828dd875d229531b50d05f016b8a1f1dd9vboxsync Kripke structure

9eb499828dd875d229531b50d05f016b8a1f1dd9vboxsync-}

6be66de4257f4f564e35f7b8ee57a282e3cf3e96vboxsync

6be66de4257f4f564e35f7b8ee57a282e3cf3e96vboxsyncmodule Comorphisms.CspCASL2Modal where

6be66de4257f4f564e35f7b8ee57a282e3cf3e96vboxsync

6be66de4257f4f564e35f7b8ee57a282e3cf3e96vboxsyncimport Logic.Logic

6be66de4257f4f564e35f7b8ee57a282e3cf3e96vboxsyncimport Logic.Comorphism

7529922bd11d7d1c38fbdc7bad6aec83eb2ec0advboxsyncimport qualified Data.Set as Set

6be66de4257f4f564e35f7b8ee57a282e3cf3e96vboxsyncimport Common.Id

6be66de4257f4f564e35f7b8ee57a282e3cf3e96vboxsync

6be66de4257f4f564e35f7b8ee57a282e3cf3e96vboxsync-- CASL

6be66de4257f4f564e35f7b8ee57a282e3cf3e96vboxsyncimport CASL.Sign

6be66de4257f4f564e35f7b8ee57a282e3cf3e96vboxsyncimport CASL.AS_Basic_CASL

6be66de4257f4f564e35f7b8ee57a282e3cf3e96vboxsyncimport CASL.Morphism

6be66de4257f4f564e35f7b8ee57a282e3cf3e96vboxsync

8eb4989e815c8f374b965265ccf184d6ce17d9e8vboxsync-- CspCASL

bffb24521128f5183aafbef6542e7dacf20b5132vboxsyncimport CspCASL.Logic_CspCASL

6be66de4257f4f564e35f7b8ee57a282e3cf3e96vboxsyncimport CspCASL.SignCSP

6be66de4257f4f564e35f7b8ee57a282e3cf3e96vboxsyncimport CspCASL.AS_CspCASL (CspBasicSpec (..), CspCASLSentence)

6be66de4257f4f564e35f7b8ee57a282e3cf3e96vboxsync

da6747c2419b9cea8b5e2c576a30a5de999a8ab3vboxsync-- ModalCASL

da6747c2419b9cea8b5e2c576a30a5de999a8ab3vboxsyncimport Modal.Logic_Modal

6be66de4257f4f564e35f7b8ee57a282e3cf3e96vboxsyncimport Modal.AS_Modal

6be66de4257f4f564e35f7b8ee57a282e3cf3e96vboxsyncimport Modal.ModalSign

6be66de4257f4f564e35f7b8ee57a282e3cf3e96vboxsync

6be66de4257f4f564e35f7b8ee57a282e3cf3e96vboxsync-- | The identity of the comorphism

da6747c2419b9cea8b5e2c576a30a5de999a8ab3vboxsyncdata CspCASL2Modal = CspCASL2Modal deriving (Show)

6be66de4257f4f564e35f7b8ee57a282e3cf3e96vboxsync

6be66de4257f4f564e35f7b8ee57a282e3cf3e96vboxsyncinstance Language CspCASL2Modal -- default definition is okay

46e6cceda24bf6c589e4cb151afefe4fffecca7bvboxsync

8eb4989e815c8f374b965265ccf184d6ce17d9e8vboxsyncinstance Comorphism CspCASL2Modal

bffb24521128f5183aafbef6542e7dacf20b5132vboxsync CspCASL ()

6be66de4257f4f564e35f7b8ee57a282e3cf3e96vboxsync CspBasicSpec CspCASLSentence SYMB_ITEMS SYMB_MAP_ITEMS

6be66de4257f4f564e35f7b8ee57a282e3cf3e96vboxsync CspCASLSign

6be66de4257f4f564e35f7b8ee57a282e3cf3e96vboxsync CspMorphism

6be66de4257f4f564e35f7b8ee57a282e3cf3e96vboxsync () () ()

20b950300ed7ebcdf78f414c3d98b20d010ff74fvboxsync Modal ()

6be66de4257f4f564e35f7b8ee57a282e3cf3e96vboxsync M_BASIC_SPEC ModalFORMULA SYMB_ITEMS SYMB_MAP_ITEMS

6be66de4257f4f564e35f7b8ee57a282e3cf3e96vboxsync MSign

6be66de4257f4f564e35f7b8ee57a282e3cf3e96vboxsync ModalMor

7529922bd11d7d1c38fbdc7bad6aec83eb2ec0advboxsync Symbol RawSymbol () where

7529922bd11d7d1c38fbdc7bad6aec83eb2ec0advboxsync sourceLogic CspCASL2Modal = CspCASL

7529922bd11d7d1c38fbdc7bad6aec83eb2ec0advboxsync sourceSublogic CspCASL2Modal = ()

6be66de4257f4f564e35f7b8ee57a282e3cf3e96vboxsync targetLogic CspCASL2Modal = Modal

6be66de4257f4f564e35f7b8ee57a282e3cf3e96vboxsync mapSublogic CspCASL2Modal _ = Just ()

6be66de4257f4f564e35f7b8ee57a282e3cf3e96vboxsync map_theory CspCASL2Modal = return . simpleTheoryMapping mapSig mapSen

6be66de4257f4f564e35f7b8ee57a282e3cf3e96vboxsync map_morphism CspCASL2Modal = return . mapMor

7529922bd11d7d1c38fbdc7bad6aec83eb2ec0advboxsync map_sentence CspCASL2Modal _ = return . mapSen

6be66de4257f4f564e35f7b8ee57a282e3cf3e96vboxsync map_symbol CspCASL2Modal = Set.singleton . mapSym

6be66de4257f4f564e35f7b8ee57a282e3cf3e96vboxsync

7529922bd11d7d1c38fbdc7bad6aec83eb2ec0advboxsyncmapSig :: CspCASLSign -> MSign

6be66de4257f4f564e35f7b8ee57a282e3cf3e96vboxsyncmapSig sign =

7529922bd11d7d1c38fbdc7bad6aec83eb2ec0advboxsync (emptySign emptyModalSign) {sortSet = sortSet sign

6be66de4257f4f564e35f7b8ee57a282e3cf3e96vboxsync , sortRel = sortRel sign

6be66de4257f4f564e35f7b8ee57a282e3cf3e96vboxsync , opMap = opMap sign

6be66de4257f4f564e35f7b8ee57a282e3cf3e96vboxsync , assocOps = assocOps sign

da6747c2419b9cea8b5e2c576a30a5de999a8ab3vboxsync , predMap = predMap sign }

0a724db1030736c131a45392c0ebb6bb25362917vboxsync -- ??? add modalities

6be66de4257f4f564e35f7b8ee57a282e3cf3e96vboxsync

13c94cb9d95cf4865646e86b944c09e1af2fe48cvboxsyncmapMor :: CspMorphism -> ModalMor

6be66de4257f4f564e35f7b8ee57a282e3cf3e96vboxsyncmapMor m = (embedMorphism emptyMorExt (mapSig $ msource m) $ mapSig $ mtarget m)

6be66de4257f4f564e35f7b8ee57a282e3cf3e96vboxsync { sort_map = sort_map m

6be66de4257f4f564e35f7b8ee57a282e3cf3e96vboxsync , op_map = op_map m

c33cfcef143f5dc2148c35d7b1dd1a32183f1926vboxsync , pred_map = pred_map m }

bffb24521128f5183aafbef6542e7dacf20b5132vboxsync -- ??? add modalities

6be66de4257f4f564e35f7b8ee57a282e3cf3e96vboxsync

6be66de4257f4f564e35f7b8ee57a282e3cf3e96vboxsync

13c94cb9d95cf4865646e86b944c09e1af2fe48cvboxsyncmapSym :: () -> Symbol

6be66de4257f4f564e35f7b8ee57a282e3cf3e96vboxsyncmapSym = error "CspCASL2Modal.mapSym not yet implemented"

ad34209dccf31d54e2277d732a90ce6ea4374362vboxsync -- needs to be changed once modal symbols are added

6be66de4257f4f564e35f7b8ee57a282e3cf3e96vboxsync

6be66de4257f4f564e35f7b8ee57a282e3cf3e96vboxsync

6be66de4257f4f564e35f7b8ee57a282e3cf3e96vboxsyncmapSen :: CspCASLSentence -> ModalFORMULA

6be66de4257f4f564e35f7b8ee57a282e3cf3e96vboxsyncmapSen _f = True_atom nullRange

6be66de4257f4f564e35f7b8ee57a282e3cf3e96vboxsync

6be66de4257f4f564e35f7b8ee57a282e3cf3e96vboxsync{- case f of

6be66de4257f4f564e35f7b8ee57a282e3cf3e96vboxsync Quantification q vs frm ps ->

7529922bd11d7d1c38fbdc7bad6aec83eb2ec0advboxsync Quantification q vs (mapSen frm) ps

6be66de4257f4f564e35f7b8ee57a282e3cf3e96vboxsync Conjunction fs ps ->

7529922bd11d7d1c38fbdc7bad6aec83eb2ec0advboxsync Conjunction (map mapSen fs) ps

27efd9329f6a90f7cacf840031e5305f98975960vboxsync Disjunction fs ps ->

6be66de4257f4f564e35f7b8ee57a282e3cf3e96vboxsync Disjunction (map mapSen fs) ps

ad34209dccf31d54e2277d732a90ce6ea4374362vboxsync Implication f1 f2 b ps ->

6be66de4257f4f564e35f7b8ee57a282e3cf3e96vboxsync Implication (mapSen f1) (mapSen f2) b ps

bbfc28b1a00ce00001b2ead074d47254bec3e5cfvboxsync Equivalence f1 f2 ps ->

da6747c2419b9cea8b5e2c576a30a5de999a8ab3vboxsync Equivalence (mapSen f1) (mapSen f2) ps

6be66de4257f4f564e35f7b8ee57a282e3cf3e96vboxsync Negation frm ps -> Negation (mapSen frm) ps

6be66de4257f4f564e35f7b8ee57a282e3cf3e96vboxsync True_atom ps -> True_atom ps

6be66de4257f4f564e35f7b8ee57a282e3cf3e96vboxsync False_atom ps -> False_atom ps

6be66de4257f4f564e35f7b8ee57a282e3cf3e96vboxsync Existl_equation t1 t2 ps ->

6be66de4257f4f564e35f7b8ee57a282e3cf3e96vboxsync Existl_equation (mapTERM t1) (mapTERM t2) ps

6be66de4257f4f564e35f7b8ee57a282e3cf3e96vboxsync Strong_equation t1 t2 ps ->

6be66de4257f4f564e35f7b8ee57a282e3cf3e96vboxsync Strong_equation (mapTERM t1) (mapTERM t2) ps

6be66de4257f4f564e35f7b8ee57a282e3cf3e96vboxsync Predication pn as qs ->

27efd9329f6a90f7cacf840031e5305f98975960vboxsync Predication pn (map mapTERM as) qs

6be66de4257f4f564e35f7b8ee57a282e3cf3e96vboxsync Definedness t ps -> Definedness (mapTERM t) ps

ad34209dccf31d54e2277d732a90ce6ea4374362vboxsync Membership t ty ps -> Membership (mapTERM t) ty ps

6be66de4257f4f564e35f7b8ee57a282e3cf3e96vboxsync Sort_gen_ax constrs isFree -> Sort_gen_ax constrs isFree

bbfc28b1a00ce00001b2ead074d47254bec3e5cfvboxsync _ -> error "CspCASL2Modal.mapSen"

27efd9329f6a90f7cacf840031e5305f98975960vboxsync

da6747c2419b9cea8b5e2c576a30a5de999a8ab3vboxsyncmapTERM :: TERM () -> TERM M_FORMULA

6be66de4257f4f564e35f7b8ee57a282e3cf3e96vboxsyncmapTERM t = case t of

6be66de4257f4f564e35f7b8ee57a282e3cf3e96vboxsync Qual_var v ty ps -> Qual_var v ty ps

6be66de4257f4f564e35f7b8ee57a282e3cf3e96vboxsync Application opsym as qs -> Application opsym (map mapTERM as) qs

6be66de4257f4f564e35f7b8ee57a282e3cf3e96vboxsync Sorted_term trm ty ps -> Sorted_term (mapTERM trm) ty ps

6be66de4257f4f564e35f7b8ee57a282e3cf3e96vboxsync Cast trm ty ps -> Cast (mapTERM trm) ty ps

20b950300ed7ebcdf78f414c3d98b20d010ff74fvboxsync Conditional t1 f t2 ps ->

6be66de4257f4f564e35f7b8ee57a282e3cf3e96vboxsync Conditional (mapTERM t1) (mapSen f) (mapTERM t2) ps

6be66de4257f4f564e35f7b8ee57a282e3cf3e96vboxsync _ -> error "CspCASL2Modal.mapTERM"

7529922bd11d7d1c38fbdc7bad6aec83eb2ec0advboxsync

6be66de4257f4f564e35f7b8ee57a282e3cf3e96vboxsync-}

27efd9329f6a90f7cacf840031e5305f98975960vboxsync