hets/CspCASL/Comorphisms.hs

	Comorphisms.hs revision 400321fd7a25a1c34eb95855ee86daf722734bd4
57221209d11b05aa0373cc3892d5df89ba96ebf9Christian Maeder{- |
57221209d11b05aa0373cc3892d5df89ba96ebf9Christian MaederModule      :  $Header$
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederDescription :  generic CspCASL instance for comorphisms
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederCopyright   :  (c) Liam O'Reilly, Swansea University 2009
e6d40133bc9f858308654afb1262b8b483ec5922Till MossakowskiLicense     :  similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
1549f3abf73c1122acff724f718b615c82fa3648Till Mossakowski
98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuMaintainer  :  csliam@swansea.ac.uk
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederStability   :  experimental
3f69b6948966979163bdfe8331c38833d5d90ecdChristian MaederPortability :  non-portable(import Logic.Logic)
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder
351145cfe8c03b4d47133c96b209f2bd6cfbf504Christian Maeder-}
f3a94a197960e548ecd6520bb768cb0d547457bbChristian Maeder
e6d40133bc9f858308654afb1262b8b483ec5922Till Mossakowskimodule CspCASL.Comorphisms where
1549f3abf73c1122acff724f718b615c82fa3648Till Mossakowski
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maederimport Logic.Logic
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maederimport Logic.Comorphism
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder-- CASL
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maederimport CASL.Sign
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maederimport CASL.AS_Basic_CASL
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maederimport CASL.Morphism
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder-- CspCASL
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maederimport CspCASL.Logic_CspCASL
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maederimport CspCASL.SignCSP
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maederimport CspCASL.AS_CspCASL (CspBasicSpec (..))
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maederimport qualified Data.Set as Set
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder-- | The identity of the comorphism
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maederdata CspCASL2CspCASL a b = CspCASL2CspCASL a b deriving Show
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder
351391e0e3226210e7ffb183b334da9f96de36eaChristian MaedercspCASLTrace :: CspCASL2CspCASL () Trace
351391e0e3226210e7ffb183b334da9f96de36eaChristian MaedercspCASLTrace = CspCASL2CspCASL () Trace
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder
351391e0e3226210e7ffb183b334da9f96de36eaChristian MaedercspCASLFailure :: CspCASL2CspCASL () Failure
351391e0e3226210e7ffb183b334da9f96de36eaChristian MaedercspCASLFailure = CspCASL2CspCASL () Failure
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maederinstance (Show a, Show b) => Language (CspCASL2CspCASL a b) where
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder  language_name (CspCASL2CspCASL a b) =
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder      language_name (GenCspCASL a)
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder      ++ "2" ++ language_name (GenCspCASL b)
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maederinstance (CspCASLSemantics a, CspCASLSemantics b)
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder   => Comorphism (CspCASL2CspCASL a b)
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder               (GenCspCASL a) ()
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder               CspBasicSpec CspCASLSen SYMB_ITEMS SYMB_MAP_ITEMS
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder               CspCASLSign
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder               CspMorphism
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder               Symbol RawSymbol ()
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder               (GenCspCASL b) ()
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder               CspBasicSpec CspCASLSen SYMB_ITEMS SYMB_MAP_ITEMS
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder               CspCASLSign
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder               CspMorphism
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder               Symbol RawSymbol () where
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder    sourceLogic (CspCASL2CspCASL a _) = GenCspCASL a
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder    sourceSublogic _ = ()
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder    targetLogic (CspCASL2CspCASL _ b) = GenCspCASL b
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder    mapSublogic _ _ = Just ()
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder    map_theory _ = return
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder    map_morphism _ = return
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder    map_sentence _ = \_ -> return
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder    map_symbol _ _ = Set.singleton
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder    is_model_transportable _ = True
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder    has_model_expansion _ = True
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder    is_weakly_amalgamable _ = True
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder    isInclusionComorphism _ = True
f8b715ab2993083761c0aedb78f1819bcf67b6ccChristian Maeder