b332ea78705d9ed8708bb30eb914c0eb9a8e6361Till Mossakowski{- |

e9458b1a7a19a63aa4c179f9ab20f4d50681c168Jens ElknerModule : $Header$

876bd2c70a93981cc80f8376284616bce4a0fefcChristian MaederCopyright : (c) Till Mossakowski and Uni Bremen 2003

b332ea78705d9ed8708bb30eb914c0eb9a8e6361Till MossakowskiLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt

98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu Prodescu

b332ea78705d9ed8708bb30eb914c0eb9a8e6361Till MossakowskiMaintainer : M.Roggenbach@swansea.ac.uk

2eeec5240b424984e3ee26296da1eeab6c6d739eChristian MaederStability : provisional

b332ea78705d9ed8708bb30eb914c0eb9a8e6361Till MossakowskiPortability : non-portable (imports Logic.Logic)

b332ea78705d9ed8708bb30eb914c0eb9a8e6361Till Mossakowski

b332ea78705d9ed8708bb30eb914c0eb9a8e6361Till MossakowskiThe embedding comorphism from CASL to CspCASL.

876bd2c70a93981cc80f8376284616bce4a0fefcChristian Maeder-}

0095c7efbddd0ffeed6aaf8ec015346be161d819Till Mossakowski

b332ea78705d9ed8708bb30eb914c0eb9a8e6361Till Mossakowskimodule Comorphisms.CASL2CspCASL where

b332ea78705d9ed8708bb30eb914c0eb9a8e6361Till Mossakowski

b332ea78705d9ed8708bb30eb914c0eb9a8e6361Till Mossakowskiimport Logic.Logic

b332ea78705d9ed8708bb30eb914c0eb9a8e6361Till Mossakowskiimport Logic.Comorphism

b332ea78705d9ed8708bb30eb914c0eb9a8e6361Till Mossakowskiimport qualified Data.Map as Map

b332ea78705d9ed8708bb30eb914c0eb9a8e6361Till Mossakowski

0ea724a1bbc3c692c3cc4cc572975e51e45f137eTill Mossakowski-- CASL

2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maederimport CASL.Logic_CASL

0ea724a1bbc3c692c3cc4cc572975e51e45f137eTill Mossakowskiimport CASL.Sublogic as SL

0ea724a1bbc3c692c3cc4cc572975e51e45f137eTill Mossakowskiimport CASL.Sign

ea8e98e298f33f9362293f392c8fb192722b8904Eugen Kuksaimport CASL.AS_Basic_CASL

47d6bc7bc9a708427f96be8d805f712697ad3d9eChristian Maederimport CASL.Morphism

f5c16d70215311c0392b5723f427f714e34ba6b9Till Mossakowski

f5c16d70215311c0392b5723f427f714e34ba6b9Till Mossakowski-- CspCASL

b332ea78705d9ed8708bb30eb914c0eb9a8e6361Till Mossakowskiimport CspCASL.Logic_CspCASL

2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maederimport CspCASL.AS_CspCASL (CspBasicSpec (..))

2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maederimport CspCASL.SignCSP

2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder

e1ca87d857ab0461cbcd260484ba0498ec10e1a4Till Mossakowski-- | The identity of the comorphism

ea8e98e298f33f9362293f392c8fb192722b8904Eugen Kuksadata CASL2CspCASL = CASL2CspCASL deriving (Show)

f5c16d70215311c0392b5723f427f714e34ba6b9Till Mossakowski

94e112d16f89130a688db8b03ad3224903f5e97eChristian Maederinstance Language CASL2CspCASL -- default definition is okay

f5c16d70215311c0392b5723f427f714e34ba6b9Till Mossakowski

f5c16d70215311c0392b5723f427f714e34ba6b9Till Mossakowskiinstance Comorphism CASL2CspCASL

47d6bc7bc9a708427f96be8d805f712697ad3d9eChristian Maeder CASL CASL_Sublogics

e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian Maeder CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS

47d6bc7bc9a708427f96be8d805f712697ad3d9eChristian Maeder CASLSign

e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian Maeder CASLMor

f5c16d70215311c0392b5723f427f714e34ba6b9Till Mossakowski Symbol RawSymbol Q_ProofTree

47d6bc7bc9a708427f96be8d805f712697ad3d9eChristian Maeder CspCASL ()

f5c16d70215311c0392b5723f427f714e34ba6b9Till Mossakowski CspBasicSpec () SYMB_ITEMS SYMB_MAP_ITEMS

049d1590fff7cde05c68d63547aa7660c2034a0cTill Mossakowski CspSign

049d1590fff7cde05c68d63547aa7660c2034a0cTill Mossakowski CspMorphism

049d1590fff7cde05c68d63547aa7660c2034a0cTill Mossakowski () () () where

049d1590fff7cde05c68d63547aa7660c2034a0cTill Mossakowski sourceLogic CASL2CspCASL = CASL

47d6bc7bc9a708427f96be8d805f712697ad3d9eChristian Maeder sourceSublogic CASL2CspCASL = SL.top

47d6bc7bc9a708427f96be8d805f712697ad3d9eChristian Maeder targetLogic CASL2CspCASL = CspCASL

94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder mapSublogic CASL2CspCASL _ = Just ()

47d6bc7bc9a708427f96be8d805f712697ad3d9eChristian Maeder map_theory CASL2CspCASL = return . simpleTheoryMapping mapSig (const ())

e1ca87d857ab0461cbcd260484ba0498ec10e1a4Till Mossakowski map_morphism CASL2CspCASL = return . mapMor

94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder map_sentence CASL2CspCASL _sig = return . (const ()) -- toSentence sig

dece9056c18ada64bcc8f2fba285270374139ee8Christian Maeder -- this function has now the error implementation as default

47d6bc7bc9a708427f96be8d805f712697ad3d9eChristian Maeder -- map_symbol = errMapSymbol -- Set.singleton . mapSym

94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder has_model_expansion CASL2CspCASL = True

47d6bc7bc9a708427f96be8d805f712697ad3d9eChristian Maeder is_weakly_amalgamable CASL2CspCASL = True

f5c16d70215311c0392b5723f427f714e34ba6b9Till Mossakowski

94e112d16f89130a688db8b03ad3224903f5e97eChristian MaedermapSig :: CASLSign -> CspSign

f5c16d70215311c0392b5723f427f714e34ba6b9Till MossakowskimapSig sign =

94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder (emptySign emptyCspProcSign) {sortSet = sortSet sign

f5c16d70215311c0392b5723f427f714e34ba6b9Till Mossakowski , sortRel = sortRel sign

f5c16d70215311c0392b5723f427f714e34ba6b9Till Mossakowski , opMap = opMap sign

2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder , assocOps = assocOps sign

94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder , predMap = predMap sign }

94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder

e7ddd5495421698701a2bbc57a5b3390a11d12caChristian MaedermapMor :: CASLMor -> CspMorphism

94e112d16f89130a688db8b03ad3224903f5e97eChristian MaedermapMor m = Morphism {msource = mapSig $ msource m

f5c16d70215311c0392b5723f427f714e34ba6b9Till Mossakowski , mtarget = mapSig $ mtarget m

2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder , sort_map = sort_map m

47d6bc7bc9a708427f96be8d805f712697ad3d9eChristian Maeder , fun_map = fun_map m

933997b6313fc8fd4711dbc9e01dff7c68f58cd7Till Mossakowski , pred_map = pred_map m

933997b6313fc8fd4711dbc9e01dff7c68f58cd7Till Mossakowski , extended_map =

933997b6313fc8fd4711dbc9e01dff7c68f58cd7Till Mossakowski CspAddMorphism { channelMap = Map.empty,

933997b6313fc8fd4711dbc9e01dff7c68f58cd7Till Mossakowski processMap = Map.empty

47d6bc7bc9a708427f96be8d805f712697ad3d9eChristian Maeder }}

933997b6313fc8fd4711dbc9e01dff7c68f58cd7Till Mossakowski

933997b6313fc8fd4711dbc9e01dff7c68f58cd7Till Mossakowski