CASL2CspCASL.hs revision f2c050360525df494e6115073b0edc4c443a847c
66267bcb678a9c341272c323b299337bcfdb7cc5Christian Maeder{- |
81d182b21020b815887e9057959228546cf61b6bChristian MaederModule : $Header$
81d182b21020b815887e9057959228546cf61b6bChristian MaederCopyright : (c) Till Mossakowski and Uni Bremen 2003
a39175891082dc8a598e5630e5558cb08b84ac0aChristian MaederLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
66267bcb678a9c341272c323b299337bcfdb7cc5Christian Maeder
3f69b6948966979163bdfe8331c38833d5d90ecdChristian MaederMaintainer : M.Roggenbach@swansea.ac.uk
66267bcb678a9c341272c323b299337bcfdb7cc5Christian MaederStability : provisional
ffd01020a4f35f434b912844ad6e0d6918fadffdChristian MaederPortability : non-portable (imports Logic.Logic)
66267bcb678a9c341272c323b299337bcfdb7cc5Christian Maeder
66267bcb678a9c341272c323b299337bcfdb7cc5Christian MaederThe embedding comorphism from CASL to CspCASL.
fb69cd512eab767747f109e40322df7cae2f7bdfChristian Maeder-}
fb69cd512eab767747f109e40322df7cae2f7bdfChristian Maeder
5553cf7e344c2b385a72e1244b419e9986042b8eChristian Maedermodule Comorphisms.CASL2CspCASL where
5553cf7e344c2b385a72e1244b419e9986042b8eChristian Maeder
5553cf7e344c2b385a72e1244b419e9986042b8eChristian Maederimport Logic.Logic
f42bcc750a9a02cb4f753b70679f9aacf1b338d7Christian Maederimport Logic.Comorphism
f42bcc750a9a02cb4f753b70679f9aacf1b338d7Christian Maederimport qualified Data.Map as Map
f42bcc750a9a02cb4f753b70679f9aacf1b338d7Christian Maeder
5553cf7e344c2b385a72e1244b419e9986042b8eChristian Maeder-- CASL
5553cf7e344c2b385a72e1244b419e9986042b8eChristian Maederimport CASL.Logic_CASL
5553cf7e344c2b385a72e1244b419e9986042b8eChristian Maederimport CASL.Sublogic as SL
fb69cd512eab767747f109e40322df7cae2f7bdfChristian Maederimport CASL.Sign
e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maederimport CASL.AS_Basic_CASL
678e45c045799ce271c4719123ecd9cf4f456d4bChristian Maederimport CASL.Morphism
e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maeder
e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maeder-- CspCASL
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maederimport CspCASL.Logic_CspCASL
59c301c268f79cfde0a4c30a2c572a368db98da5Christian Maederimport CspCASL.AS_CspCASL (BASIC_CSP_CASL_SPEC (..))
05e2a3161e4589a717c6fe5c7306820273a473c5Christian Maederimport CspCASL.SignCSP
31a189d4cff554f78407cdc422480e84e99a6ec6Christian Maeder
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder-- | The identity of the comorphism
5d7e4bf173534e7eb3fc84dce7bb0151079d3f8aChristian Maederdata CASL2CspCASL = CASL2CspCASL deriving (Show)
f42bcc750a9a02cb4f753b70679f9aacf1b338d7Christian Maeder
ad270004874ce1d0697fb30d7309f180553bb315Christian Maederinstance Language CASL2CspCASL -- default definition is okay
ad270004874ce1d0697fb30d7309f180553bb315Christian Maeder
e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maederinstance Comorphism CASL2CspCASL
f42bcc750a9a02cb4f753b70679f9aacf1b338d7Christian Maeder CASL CASL_Sublogics
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS
f42bcc750a9a02cb4f753b70679f9aacf1b338d7Christian Maeder CASLSign
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder CASLMor
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder Symbol RawSymbol ()
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder CspCASL ()
946f62de1b188898dde0c472f2a8a6fb86f4d2f5Christian Maeder BASIC_CSP_CASL_SPEC () SYMB_ITEMS SYMB_MAP_ITEMS
6f031207ab25d41ae4740a4151d5946faff4768bChristian Maeder CSPSign
6f031207ab25d41ae4740a4151d5946faff4768bChristian Maeder CSPMorphism
e7ce154edb906685b3fa7f6c0a764e18a4658068Christian Maeder () () () where
e7ce154edb906685b3fa7f6c0a764e18a4658068Christian Maeder sourceLogic CASL2CspCASL = CASL
e7ce154edb906685b3fa7f6c0a764e18a4658068Christian Maeder sourceSublogic CASL2CspCASL = SL.top
6cb518d88084543c13aa7e56db767c14ee97ab77Christian Maeder targetLogic CASL2CspCASL = CspCASL
6cb518d88084543c13aa7e56db767c14ee97ab77Christian Maeder mapSublogic CASL2CspCASL _ = ()
6cb518d88084543c13aa7e56db767c14ee97ab77Christian Maeder map_theory CASL2CspCASL = return . simpleTheoryMapping mapSig (const ())
024621f43239cfe9629e35d35a8669fad7acbba2Christian Maeder map_morphism CASL2CspCASL = return . mapMor
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder map_sentence CASL2CspCASL _sig = return . (const ()) -- toSentence sig
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder map_symbol = errMapSymbol -- Set.singleton . mapSym
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder has_model_expansion CASL2CspCASL = True
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder is_weakly_amalgamable CASL2CspCASL = True
27912d626bf179b82fcb337077e5cd9653bb71cfChristian Maeder
e13ee09381f136f5eadaabdb9699773c0052cf3dChristian MaedermapSig :: CASLSign -> CSPSign
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaedermapSig sign =
5c933f3c61d2cfa7e76e4eb610a4b0bac988be47Christian Maeder (emptySign emptyCSPAddSign) {sortSet = sortSet sign
5c933f3c61d2cfa7e76e4eb610a4b0bac988be47Christian Maeder , sortRel = sortRel sign
6cb518d88084543c13aa7e56db767c14ee97ab77Christian Maeder , opMap = opMap sign
6cb518d88084543c13aa7e56db767c14ee97ab77Christian Maeder , assocOps = assocOps sign
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder , predMap = predMap sign }
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder
f6fc70956d64365527d77a521a96f54a1cc18f91Christian MaedermapMor :: CASLMor -> CSPMorphism
51c65d5fb2d720dc77bc5cca15640cfa09711986Christian MaedermapMor m = Morphism {msource = mapSig $ msource m
946f62de1b188898dde0c472f2a8a6fb86f4d2f5Christian Maeder , mtarget = mapSig $ mtarget m
51c65d5fb2d720dc77bc5cca15640cfa09711986Christian Maeder , sort_map = sort_map m
51c65d5fb2d720dc77bc5cca15640cfa09711986Christian Maeder , fun_map = fun_map m
51c65d5fb2d720dc77bc5cca15640cfa09711986Christian Maeder , pred_map = pred_map m
f6fc70956d64365527d77a521a96f54a1cc18f91Christian Maeder , extended_map =
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder CSPAddMorphism { channelMap = Map.empty,
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder processMap = Map.empty
946f62de1b188898dde0c472f2a8a6fb86f4d2f5Christian Maeder }}
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder