hets/CspCASL/Comorphisms.hs

	Comorphisms.hs revision 33bdce26495121cdbce30331ef90a1969126a840
286f4deb69d3912337bb09dd7f81284d12912ce8Christian Maeder{- |
286f4deb69d3912337bb09dd7f81284d12912ce8Christian MaederModule      :  $Header$
286f4deb69d3912337bb09dd7f81284d12912ce8Christian MaederDescription :  generic CspCASL instance for comorphisms
286f4deb69d3912337bb09dd7f81284d12912ce8Christian MaederCopyright   :  (c) Liam O'Reilly, Swansea University 2009
286f4deb69d3912337bb09dd7f81284d12912ce8Christian MaederLicense     :  similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
286f4deb69d3912337bb09dd7f81284d12912ce8Christian Maeder
286f4deb69d3912337bb09dd7f81284d12912ce8Christian MaederMaintainer  :  csliam@swansea.ac.uk
286f4deb69d3912337bb09dd7f81284d12912ce8Christian MaederStability   :  experimental
286f4deb69d3912337bb09dd7f81284d12912ce8Christian MaederPortability :  non-portable(import Logic.Logic)
286f4deb69d3912337bb09dd7f81284d12912ce8Christian Maeder
286f4deb69d3912337bb09dd7f81284d12912ce8Christian Maeder-}
286f4deb69d3912337bb09dd7f81284d12912ce8Christian Maeder
286f4deb69d3912337bb09dd7f81284d12912ce8Christian Maedermodule CspCASL.Comorphisms where
286f4deb69d3912337bb09dd7f81284d12912ce8Christian Maeder
286f4deb69d3912337bb09dd7f81284d12912ce8Christian Maederimport Logic.Logic
286f4deb69d3912337bb09dd7f81284d12912ce8Christian Maederimport Logic.Comorphism
286f4deb69d3912337bb09dd7f81284d12912ce8Christian Maeder
286f4deb69d3912337bb09dd7f81284d12912ce8Christian Maeder-- CASL
286f4deb69d3912337bb09dd7f81284d12912ce8Christian Maederimport CASL.Sign
286f4deb69d3912337bb09dd7f81284d12912ce8Christian Maederimport CASL.AS_Basic_CASL
286f4deb69d3912337bb09dd7f81284d12912ce8Christian Maederimport CASL.Morphism
286f4deb69d3912337bb09dd7f81284d12912ce8Christian Maeder
286f4deb69d3912337bb09dd7f81284d12912ce8Christian Maeder-- CspCASL
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reillyimport CspCASL.AS_CspCASL (CspBasicSpec (..))
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reillyimport CspCASL.Morphism
286f4deb69d3912337bb09dd7f81284d12912ce8Christian Maederimport CspCASL.Logic_CspCASL
286f4deb69d3912337bb09dd7f81284d12912ce8Christian Maederimport CspCASL.SignCSP
286f4deb69d3912337bb09dd7f81284d12912ce8Christian Maeder
286f4deb69d3912337bb09dd7f81284d12912ce8Christian Maederimport qualified Data.Set as Set
286f4deb69d3912337bb09dd7f81284d12912ce8Christian Maeder
286f4deb69d3912337bb09dd7f81284d12912ce8Christian Maeder-- | The identity of the comorphism
286f4deb69d3912337bb09dd7f81284d12912ce8Christian Maederdata CspCASL2CspCASL a b = CspCASL2CspCASL a b deriving Show
286f4deb69d3912337bb09dd7f81284d12912ce8Christian Maeder
286f4deb69d3912337bb09dd7f81284d12912ce8Christian MaedercspCASLTrace :: CspCASL2CspCASL () Trace
286f4deb69d3912337bb09dd7f81284d12912ce8Christian MaedercspCASLTrace = CspCASL2CspCASL () Trace
286f4deb69d3912337bb09dd7f81284d12912ce8Christian Maeder
286f4deb69d3912337bb09dd7f81284d12912ce8Christian MaedercspCASLFailure :: CspCASL2CspCASL () Failure
286f4deb69d3912337bb09dd7f81284d12912ce8Christian MaedercspCASLFailure = CspCASL2CspCASL () Failure
286f4deb69d3912337bb09dd7f81284d12912ce8Christian Maeder
286f4deb69d3912337bb09dd7f81284d12912ce8Christian Maederinstance (Show a, Show b) => Language (CspCASL2CspCASL a b) where
286f4deb69d3912337bb09dd7f81284d12912ce8Christian Maeder  language_name (CspCASL2CspCASL a b) =
286f4deb69d3912337bb09dd7f81284d12912ce8Christian Maeder      language_name (GenCspCASL a)
286f4deb69d3912337bb09dd7f81284d12912ce8Christian Maeder      ++ "2" ++ language_name (GenCspCASL b)
286f4deb69d3912337bb09dd7f81284d12912ce8Christian Maeder
286f4deb69d3912337bb09dd7f81284d12912ce8Christian Maederinstance (CspCASLSemantics a, CspCASLSemantics b)
286f4deb69d3912337bb09dd7f81284d12912ce8Christian Maeder   => Comorphism (CspCASL2CspCASL a b)
286f4deb69d3912337bb09dd7f81284d12912ce8Christian Maeder               (GenCspCASL a) ()
286f4deb69d3912337bb09dd7f81284d12912ce8Christian Maeder               CspBasicSpec CspCASLSen SYMB_ITEMS SYMB_MAP_ITEMS
286f4deb69d3912337bb09dd7f81284d12912ce8Christian Maeder               CspCASLSign
286f4deb69d3912337bb09dd7f81284d12912ce8Christian Maeder               CspMorphism
286f4deb69d3912337bb09dd7f81284d12912ce8Christian Maeder               Symbol RawSymbol ()
286f4deb69d3912337bb09dd7f81284d12912ce8Christian Maeder               (GenCspCASL b) ()
286f4deb69d3912337bb09dd7f81284d12912ce8Christian Maeder               CspBasicSpec CspCASLSen SYMB_ITEMS SYMB_MAP_ITEMS
286f4deb69d3912337bb09dd7f81284d12912ce8Christian Maeder               CspCASLSign
286f4deb69d3912337bb09dd7f81284d12912ce8Christian Maeder               CspMorphism
286f4deb69d3912337bb09dd7f81284d12912ce8Christian Maeder               Symbol RawSymbol () where
286f4deb69d3912337bb09dd7f81284d12912ce8Christian Maeder    sourceLogic (CspCASL2CspCASL a _) = GenCspCASL a
286f4deb69d3912337bb09dd7f81284d12912ce8Christian Maeder    sourceSublogic _ = ()
286f4deb69d3912337bb09dd7f81284d12912ce8Christian Maeder    targetLogic (CspCASL2CspCASL _ b) = GenCspCASL b
286f4deb69d3912337bb09dd7f81284d12912ce8Christian Maeder    mapSublogic _ _ = Just ()
286f4deb69d3912337bb09dd7f81284d12912ce8Christian Maeder    map_theory _ = return
286f4deb69d3912337bb09dd7f81284d12912ce8Christian Maeder    map_morphism _ = return
286f4deb69d3912337bb09dd7f81284d12912ce8Christian Maeder    map_sentence _ = \_ -> return
400321fd7a25a1c34eb95855ee86daf722734bd4Mihai Codescu    map_symbol _ _ = Set.singleton
286f4deb69d3912337bb09dd7f81284d12912ce8Christian Maeder    is_model_transportable _ = True
286f4deb69d3912337bb09dd7f81284d12912ce8Christian Maeder    has_model_expansion _ = True
286f4deb69d3912337bb09dd7f81284d12912ce8Christian Maeder    is_weakly_amalgamable _ = True
286f4deb69d3912337bb09dd7f81284d12912ce8Christian Maeder    isInclusionComorphism _ = True