CASL2CspCASL.hs revision 05bf9cbe382548c2665dd01a6a402640c9ec3813
4b0a4c7dea0f67a233dcc42ce9bb18d36de109aeChristian Maeder{-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances #-}
4b0a4c7dea0f67a233dcc42ce9bb18d36de109aeChristian Maeder{- |
5ba323da9f037264b4a356085e844889aedeac23Christian MaederModule : $Header$
10397bcc134edbcfbe3ae2c7ea4c6080036aae22Christian MaederCopyright : (c) Till Mossakowski and Uni Bremen 2003
97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian MaederLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
23f2c59644866aa82e90de353e77f9f1d1b51b9aChristian Maeder
3f69b6948966979163bdfe8331c38833d5d90ecdChristian MaederMaintainer : M.Roggenbach@swansea.ac.uk
4b0a4c7dea0f67a233dcc42ce9bb18d36de109aeChristian MaederStability : provisional
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian MaederPortability : non-portable (imports Logic.Logic)
4b0a4c7dea0f67a233dcc42ce9bb18d36de109aeChristian Maeder
f3a94a197960e548ecd6520bb768cb0d547457bbChristian MaederThe embedding comorphism from CASL to CspCASL.
23f2c59644866aa82e90de353e77f9f1d1b51b9aChristian Maeder-}
23f2c59644866aa82e90de353e77f9f1d1b51b9aChristian Maeder
e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maedermodule Comorphisms.CASL2CspCASL where
23f2c59644866aa82e90de353e77f9f1d1b51b9aChristian Maeder
e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maederimport Logic.Logic
4b0a4c7dea0f67a233dcc42ce9bb18d36de109aeChristian Maederimport Logic.Comorphism
afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maederimport Common.ProofTree
fc8c6570c7b4ee13f375eb607bed2290438573bfChristian Maeder
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder-- CASL
23f8d286586ff38a9e73052b2c7c04c62c5c638fChristian Maederimport CASL.Logic_CASL
ad270004874ce1d0697fb30d7309f180553bb315Christian Maederimport CASL.Sublogic as SL
ad270004874ce1d0697fb30d7309f180553bb315Christian Maederimport CASL.Sign
fc8c6570c7b4ee13f375eb607bed2290438573bfChristian Maederimport CASL.AS_Basic_CASL
f8f78a2c8796a387a4348cc672ae08e8d9f69315Christian Maederimport CASL.Morphism
950e053ba55ac9c7d9c26a1ab48bd00202b29511Christian Maeder
f8f78a2c8796a387a4348cc672ae08e8d9f69315Christian Maeder-- CspCASL
10397bcc134edbcfbe3ae2c7ea4c6080036aae22Christian Maederimport CspCASL.Logic_CspCASL
afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maederimport CspCASL.AS_CspCASL (CspBasicSpec (..))
f8f78a2c8796a387a4348cc672ae08e8d9f69315Christian Maederimport CspCASL.SignCSP
af621d0066770895fd79562728e93099c8c52060Christian Maederimport CspCASL.Morphism (CspMorphism, emptyCspAddMorphism)
7c554e9d4a39b8eb3b0881f20807c95dd8e793aeChristian Maeder
e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maeder-- | The identity of the comorphism
79d11c2e3ad242ebb241f5d4a5e98a674c0b986fChristian Maederdata CASL2CspCASL = CASL2CspCASL deriving (Show)
59c301c268f79cfde0a4c30a2c572a368db98da5Christian Maeder
59c301c268f79cfde0a4c30a2c572a368db98da5Christian Maederinstance Language CASL2CspCASL -- default definition is okay
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder
e13ee09381f136f5eadaabdb9699773c0052cf3dChristian Maederinstance Comorphism CASL2CspCASL
f8f78a2c8796a387a4348cc672ae08e8d9f69315Christian Maeder CASL CASL_Sublogics
024621f43239cfe9629e35d35a8669fad7acbba2Christian Maeder CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS
afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder CASLSign
afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder CASLMor
afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder Symbol RawSymbol ProofTree
afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder CspCASL ()
afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder CspBasicSpec CspCASLSen SYMB_ITEMS SYMB_MAP_ITEMS
afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder CspCASLSign
afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder CspMorphism
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder Symbol RawSymbol () where
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder sourceLogic CASL2CspCASL = CASL
afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder sourceSublogic CASL2CspCASL = SL.top
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder targetLogic CASL2CspCASL = cspCASL
7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder mapSublogic CASL2CspCASL _ = Just ()
7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder map_theory CASL2CspCASL = return . simpleTheoryMapping mapSig mapSen
7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder map_morphism CASL2CspCASL = return . mapMor
7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder map_sentence CASL2CspCASL _sig = return . mapSen -- toSentence sig
7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder -- this function has now the error implementation as default
7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder -- map_symbol = errMapSymbol -- Set.singleton . mapSym
afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder has_model_expansion CASL2CspCASL = True
afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder is_weakly_amalgamable CASL2CspCASL = True
afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder isInclusionComorphism CASL2CspCASL = True
afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder
afa6848d579d235c9677e1ab477916df8e5ae11aChristian MaedermapSig :: CASLSign -> CspCASLSign
7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian MaedermapSig sign =
7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder (emptySign emptyCspSign) {sortSet = sortSet sign
7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder , sortRel = sortRel sign
7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder , opMap = opMap sign
afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder , assocOps = assocOps sign
9e0472be46104307b974fe5079bf5cc9e94a1a96Christian Maeder , predMap = predMap sign }
9e0472be46104307b974fe5079bf5cc9e94a1a96Christian Maeder
9e0472be46104307b974fe5079bf5cc9e94a1a96Christian MaedermapMor :: CASLMor -> CspMorphism
9e0472be46104307b974fe5079bf5cc9e94a1a96Christian MaedermapMor m =
7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder (embedMorphism emptyCspAddMorphism (mapSig $ msource m) $ mapSig $ mtarget m)
9e0472be46104307b974fe5079bf5cc9e94a1a96Christian Maeder { sort_map = sort_map m
7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder , op_map = op_map m
7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder , pred_map = pred_map m }
9e0472be46104307b974fe5079bf5cc9e94a1a96Christian Maeder
9e0472be46104307b974fe5079bf5cc9e94a1a96Christian MaedermapSen :: CASLFORMULA -> CspCASLSen
7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian MaedermapSen f = CASLSen f
afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder