Cross Reference: /hets/CspCASL/Comorphisms.hs
Comorphisms.hs revision 286f4deb69d3912337bb09dd7f81284d12912ce8
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
2e0e43889f746e31eacf8eeccdeaa4032a65b07eMihai Codescu{- |
2e0e43889f746e31eacf8eeccdeaa4032a65b07eMihai CodescuModule : $Header$
2e0e43889f746e31eacf8eeccdeaa4032a65b07eMihai CodescuDescription : generic CspCASL instance for comorphisms
2e0e43889f746e31eacf8eeccdeaa4032a65b07eMihai CodescuCopyright : (c) Liam O'Reilly, Swansea University 2009
2e0e43889f746e31eacf8eeccdeaa4032a65b07eMihai CodescuLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
2e0e43889f746e31eacf8eeccdeaa4032a65b07eMihai Codescu
2e0e43889f746e31eacf8eeccdeaa4032a65b07eMihai CodescuMaintainer : csliam@swansea.ac.uk
2e0e43889f746e31eacf8eeccdeaa4032a65b07eMihai CodescuStability : experimental
2e0e43889f746e31eacf8eeccdeaa4032a65b07eMihai CodescuPortability : non-portable(import Logic.Logic)
2e0e43889f746e31eacf8eeccdeaa4032a65b07eMihai Codescu
2e0e43889f746e31eacf8eeccdeaa4032a65b07eMihai Codescu-}
2e0e43889f746e31eacf8eeccdeaa4032a65b07eMihai Codescu
2e0e43889f746e31eacf8eeccdeaa4032a65b07eMihai Codescumodule CspCASL.Comorphisms where
2e0e43889f746e31eacf8eeccdeaa4032a65b07eMihai Codescu
2e0e43889f746e31eacf8eeccdeaa4032a65b07eMihai Codescuimport Logic.Logic
2e0e43889f746e31eacf8eeccdeaa4032a65b07eMihai Codescuimport Logic.Comorphism
c208973c890b8f993297720fd0247bc7481d4304Christian Maeder
2e0e43889f746e31eacf8eeccdeaa4032a65b07eMihai Codescu-- CASL
2e0e43889f746e31eacf8eeccdeaa4032a65b07eMihai Codescuimport CASL.Sign
2e0e43889f746e31eacf8eeccdeaa4032a65b07eMihai Codescuimport CASL.AS_Basic_CASL
2e0e43889f746e31eacf8eeccdeaa4032a65b07eMihai Codescuimport CASL.Morphism
2e0e43889f746e31eacf8eeccdeaa4032a65b07eMihai Codescu
2e0e43889f746e31eacf8eeccdeaa4032a65b07eMihai Codescu-- CspCASL
2e0e43889f746e31eacf8eeccdeaa4032a65b07eMihai Codescuimport CspCASL.Logic_CspCASL
2e0e43889f746e31eacf8eeccdeaa4032a65b07eMihai Codescuimport CspCASL.SignCSP
2e0e43889f746e31eacf8eeccdeaa4032a65b07eMihai Codescuimport CspCASL.AS_CspCASL (CspBasicSpec (..))
2e0e43889f746e31eacf8eeccdeaa4032a65b07eMihai Codescu
2e0e43889f746e31eacf8eeccdeaa4032a65b07eMihai Codescuimport qualified Data.Set as Set
2e0e43889f746e31eacf8eeccdeaa4032a65b07eMihai Codescu
a77aecc59cee605ea48e33b65a627e0aa0a245e0Mihai Codescu-- | The identity of the comorphism
a77aecc59cee605ea48e33b65a627e0aa0a245e0Mihai Codescudata CspCASL2CspCASL a b = CspCASL2CspCASL a b deriving Show
2e0e43889f746e31eacf8eeccdeaa4032a65b07eMihai Codescu
2e0e43889f746e31eacf8eeccdeaa4032a65b07eMihai CodescucspCASLTrace :: CspCASL2CspCASL () Trace
2e0e43889f746e31eacf8eeccdeaa4032a65b07eMihai CodescucspCASLTrace = CspCASL2CspCASL () Trace
2e0e43889f746e31eacf8eeccdeaa4032a65b07eMihai Codescu
2e0e43889f746e31eacf8eeccdeaa4032a65b07eMihai CodescucspCASLFailure :: CspCASL2CspCASL () Failure
2e0e43889f746e31eacf8eeccdeaa4032a65b07eMihai CodescucspCASLFailure = CspCASL2CspCASL () Failure
a9cc955b0a33e631b9ce3404e4e25b62cd067a77Christian Maeder
2e0e43889f746e31eacf8eeccdeaa4032a65b07eMihai Codescuinstance (Show a, Show b) => Language (CspCASL2CspCASL a b) where
2e0e43889f746e31eacf8eeccdeaa4032a65b07eMihai Codescu language_name (CspCASL2CspCASL a b) =
2e0e43889f746e31eacf8eeccdeaa4032a65b07eMihai Codescu language_name (GenCspCASL a)
2e0e43889f746e31eacf8eeccdeaa4032a65b07eMihai Codescu ++ "2" ++ language_name (GenCspCASL b)
a9cc955b0a33e631b9ce3404e4e25b62cd067a77Christian Maeder
2e0e43889f746e31eacf8eeccdeaa4032a65b07eMihai Codescuinstance (CspCASLSemantics a, CspCASLSemantics b)
2e0e43889f746e31eacf8eeccdeaa4032a65b07eMihai Codescu => Comorphism (CspCASL2CspCASL a b)
2e0e43889f746e31eacf8eeccdeaa4032a65b07eMihai Codescu (GenCspCASL a) ()
2e0e43889f746e31eacf8eeccdeaa4032a65b07eMihai Codescu CspBasicSpec CspCASLSen SYMB_ITEMS SYMB_MAP_ITEMS
a9cc955b0a33e631b9ce3404e4e25b62cd067a77Christian Maeder CspCASLSign
2e0e43889f746e31eacf8eeccdeaa4032a65b07eMihai Codescu CspMorphism
a9cc955b0a33e631b9ce3404e4e25b62cd067a77Christian Maeder Symbol RawSymbol ()
a9cc955b0a33e631b9ce3404e4e25b62cd067a77Christian Maeder (GenCspCASL b) ()
2e0e43889f746e31eacf8eeccdeaa4032a65b07eMihai Codescu CspBasicSpec CspCASLSen SYMB_ITEMS SYMB_MAP_ITEMS
2e0e43889f746e31eacf8eeccdeaa4032a65b07eMihai Codescu CspCASLSign
a9cc955b0a33e631b9ce3404e4e25b62cd067a77Christian Maeder CspMorphism
2e0e43889f746e31eacf8eeccdeaa4032a65b07eMihai Codescu Symbol RawSymbol () where
2e0e43889f746e31eacf8eeccdeaa4032a65b07eMihai Codescu sourceLogic (CspCASL2CspCASL a _) = GenCspCASL a
a9cc955b0a33e631b9ce3404e4e25b62cd067a77Christian Maeder sourceSublogic _ = ()
a9cc955b0a33e631b9ce3404e4e25b62cd067a77Christian Maeder targetLogic (CspCASL2CspCASL _ b) = GenCspCASL b
2e0e43889f746e31eacf8eeccdeaa4032a65b07eMihai Codescu mapSublogic _ _ = Just ()
2e0e43889f746e31eacf8eeccdeaa4032a65b07eMihai Codescu map_theory _ = return
a9cc955b0a33e631b9ce3404e4e25b62cd067a77Christian Maeder map_morphism _ = return
a9cc955b0a33e631b9ce3404e4e25b62cd067a77Christian Maeder map_sentence _ = \_ -> return
a9cc955b0a33e631b9ce3404e4e25b62cd067a77Christian Maeder map_symbol _ = Set.singleton
2e0e43889f746e31eacf8eeccdeaa4032a65b07eMihai Codescu is_model_transportable _ = True
2e0e43889f746e31eacf8eeccdeaa4032a65b07eMihai Codescu has_model_expansion _ = True
a9cc955b0a33e631b9ce3404e4e25b62cd067a77Christian Maeder is_weakly_amalgamable _ = True
2e0e43889f746e31eacf8eeccdeaa4032a65b07eMihai Codescu isInclusionComorphism _ = True
2e0e43889f746e31eacf8eeccdeaa4032a65b07eMihai Codescu