Cross Reference: /hets/Logic/Comorphism.hs
Comorphism.hs revision ca8550c6d47234042130bdc10a152806ecbc9832
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
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
306763c67bb99228487345b32ab8c5c6cd41f23cChristian Maeder{-|
306763c67bb99228487345b32ab8c5c6cd41f23cChristian Maeder
306763c67bb99228487345b32ab8c5c6cd41f23cChristian MaederModule : $Header$
306763c67bb99228487345b32ab8c5c6cd41f23cChristian MaederCopyright : (c) Till Mossakowski, Uni Bremen 2002-2004
97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian MaederLicence : similar to LGPL, see HetCATS/LICENCE.txt or LIZENZ.txt
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski
b4fbc96e05117839ca409f5f20f97b3ac872d1edTill MossakowskiMaintainer : hets@tzi.de
306763c67bb99228487345b32ab8c5c6cd41f23cChristian MaederStability : provisional
306763c67bb99228487345b32ab8c5c6cd41f23cChristian MaederPortability : non-portable (via Logic)
f3a94a197960e548ecd6520bb768cb0d547457bbChristian Maeder
f3a94a197960e548ecd6520bb768cb0d547457bbChristian Maeder Provides data structures for institution comorphisms.
44fb55f639914f4f531641f32dd4904f15c510a4Till Mossakowski These are just collections of
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski functions between (some of) the types of logics.
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski
306763c67bb99228487345b32ab8c5c6cd41f23cChristian Maeder-}
306763c67bb99228487345b32ab8c5c6cd41f23cChristian Maeder
306763c67bb99228487345b32ab8c5c6cd41f23cChristian Maeder{- References: see Logic.hs
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski Todo:
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski Weak amalgamability, also for comorphisms
2ecf6cfb90e84d40f224cda5d92c191182c976d2Till Mossakowski comorphism modifications
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski comorphisms out of sublogic relationships
2ecf6cfb90e84d40f224cda5d92c191182c976d2Till Mossakowski restrictions of comorphisms to sublogics
ae7058143db9e9993b5eff70bd6b7aede7cec658Till Mossakowski morphisms and other translations via spans
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski-}
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowskimodule Logic.Comorphism where
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowskiimport Logic.Logic
0647a6c86b231e391826c7715338ba29cb4934c0Christian Maederimport Common.Lib.Set
a89e661aad28f1b39f4fc9f9f9a4d46074234123Christian Maederimport Common.Result
19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maederimport Data.Maybe
e1a3923b210f24dc1b0ff16b60c6fb0855ff4266Christian Maederimport Data.Dynamic
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowskiimport Common.DynamicUtils
59fa9b1349ae1e001d996da732c4ac805c2938e2Christian Maederimport Common.AS_Annotation
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowskiclass (Language cid,
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski Logic lid1 sublogics1
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski basic_spec1 sentence1 symb_items1 symb_map_items1
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski sign1 morphism1 symbol1 raw_symbol1 proof_tree1,
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski Logic lid2 sublogics2
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski basic_spec2 sentence2 symb_items2 symb_map_items2
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski sign2 morphism2 symbol2 raw_symbol2 proof_tree2) =>
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski Comorphism cid
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski sign1 morphism1 symbol1 raw_symbol1 proof_tree1
d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder sign2 morphism2 symbol2 raw_symbol2 proof_tree2
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski | cid -> lid1, cid -> lid2
2ecf6cfb90e84d40f224cda5d92c191182c976d2Till Mossakowski
2ecf6cfb90e84d40f224cda5d92c191182c976d2Till Mossakowski where
2ecf6cfb90e84d40f224cda5d92c191182c976d2Till Mossakowski -- source and target logic and sublogic
4184cb191a9081cb2a9cf3ef5f060f56f0ca5922Till Mossakowski -- the source sublogic is the maximal one for which the comorphism works
8731f7b93b26083dc34a2c0937cd6493b42f2c2cTill Mossakowski -- the target sublogic is the resulting one
4184cb191a9081cb2a9cf3ef5f060f56f0ca5922Till Mossakowski sourceLogic :: cid -> lid1
8731f7b93b26083dc34a2c0937cd6493b42f2c2cTill Mossakowski sourceSublogic :: cid -> sublogics1
2ecf6cfb90e84d40f224cda5d92c191182c976d2Till Mossakowski targetLogic :: cid -> lid2
2ecf6cfb90e84d40f224cda5d92c191182c976d2Till Mossakowski targetSublogic :: cid -> sublogics2
2ecf6cfb90e84d40f224cda5d92c191182c976d2Till Mossakowski -- finer information of target sublogics corresponding to source sublogics
2ecf6cfb90e84d40f224cda5d92c191182c976d2Till Mossakowski mapSublogic :: cid -> sublogics1 -> sublogics2
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski -- default implementation
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski mapSublogic cid _ = targetSublogic cid
a89e661aad28f1b39f4fc9f9f9a4d46074234123Christian Maeder -- the translation functions are partial
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski -- because the target may be a sublanguage
5d6e7ea3bd14fc987436cff0f542393ea9ba34bbTill Mossakowski -- map_basic_spec :: cid -> basic_spec1 -> Result basic_spec2
a89e661aad28f1b39f4fc9f9f9a4d46074234123Christian Maeder -- cover theoroidal comorphisms as well
a89e661aad28f1b39f4fc9f9f9a4d46074234123Christian Maeder map_theory :: cid -> (sign1,[Named sentence1])
a89e661aad28f1b39f4fc9f9f9a4d46074234123Christian Maeder -> Result (sign2,[Named sentence2])
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski map_morphism :: cid -> morphism1 -> Result morphism2
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski map_sentence :: cid -> sign1 -> sentence1 -> Result sentence2
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski -- also covers semi-comorphisms
0647a6c86b231e391826c7715338ba29cb4934c0Christian Maeder -- with no sentence translation
0e51a998b1b213654c7a9eca451562041971f100Till Mossakowski -- - but these are spans!
0e51a998b1b213654c7a9eca451562041971f100Till Mossakowski map_symbol :: cid -> symbol1 -> Set symbol2
0e51a998b1b213654c7a9eca451562041971f100Till Mossakowski constituents :: cid -> [String]
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski -- default implementation
19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder constituents cid = [language_name cid]
19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder
19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maedermap_sign :: Comorphism cid
19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder sign1 morphism1 symbol1 raw_symbol1 proof_tree1
19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder sign2 morphism2 symbol2 raw_symbol2 proof_tree2
19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder => cid -> sign1 -> Result (sign2,[Named sentence2])
19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maedermap_sign cid sign = map_theory cid (sign,[])
19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder
19298cbfd6ee2abd904f3181af7760b965b822c3Christian MaedersimpleTheoryMapping :: (sign1 -> sign2) -> (sentence1 -> sentence2)
19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder -> (sign1, [Named sentence1])
19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder -> (sign2, [Named sentence2])
19298cbfd6ee2abd904f3181af7760b965b822c3Christian MaedersimpleTheoryMapping mapSig mapSen (sign,sens) =
19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder (mapSig sign, map (mapNamed mapSen) sens)
19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder
19298cbfd6ee2abd904f3181af7760b965b822c3Christian MaedermkTheoryMapping :: (Monad m) => (sign1 -> m (sign2, [Named sentence2]))
19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder -> (sign1 -> sentence1 -> m sentence2)
19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder -> (sign1, [Named sentence1])
19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder -> m (sign2, [Named sentence2])
19298cbfd6ee2abd904f3181af7760b965b822c3Christian MaedermkTheoryMapping mapSig mapSen (sign,sens) = do
19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder (sign',sens') <- mapSig sign
19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder sens'' <- mapM (mapNamedM $ mapSen sign) sens
586af0e9490a14dd3075095692b584c652584875Till Mossakowski return (sign',sens'++sens'')
797595aad6dfd626bc1c9df52616f1ac4235c669Till Mossakowski
797595aad6dfd626bc1c9df52616f1ac4235c669Till Mossakowskidata IdComorphism lid sublogics =
797595aad6dfd626bc1c9df52616f1ac4235c669Till Mossakowski IdComorphism lid sublogics
797595aad6dfd626bc1c9df52616f1ac4235c669Till Mossakowski
797595aad6dfd626bc1c9df52616f1ac4235c669Till Mossakowskiinstance Logic lid sublogics
797595aad6dfd626bc1c9df52616f1ac4235c669Till Mossakowski basic_spec sentence symb_items symb_map_items
797595aad6dfd626bc1c9df52616f1ac4235c669Till Mossakowski sign morphism symbol raw_symbol proof_tree =>
797595aad6dfd626bc1c9df52616f1ac4235c669Till Mossakowski Show (IdComorphism lid sublogics)
933baca0720dae81434de384b32a93b47e754d09Christian Maeder where
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski show = language_name
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski
e9249d3ecd51a2b6a966a58669953e58d703adc6Till MossakowskiidComorphismTc :: TyCon
586af0e9490a14dd3075095692b584c652584875Till MossakowskiidComorphismTc = mkTyCon "Logic.Comorphism.IdComorphism"
586af0e9490a14dd3075095692b584c652584875Till Mossakowski
933baca0720dae81434de384b32a93b47e754d09Christian Maederinstance Typeable (IdComorphism lid sub) where
933baca0720dae81434de384b32a93b47e754d09Christian Maeder typeOf _ = mkTyConApp idComorphismTc []
933baca0720dae81434de384b32a93b47e754d09Christian Maeder
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowskiinstance Logic lid sublogics
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski basic_spec sentence symb_items symb_map_items
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski sign morphism symbol raw_symbol proof_tree =>
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski Language (IdComorphism lid sublogics) where
586af0e9490a14dd3075095692b584c652584875Till Mossakowski language_name (IdComorphism lid sub) =
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski case sublogic_names lid sub of
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski [] -> error "language_name IdComorphism"
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski h : _ -> "id_" ++ language_name lid ++ "." ++ h
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowskiinstance Logic lid sublogics
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski basic_spec sentence symb_items symb_map_items
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski sign morphism symbol raw_symbol proof_tree =>
933baca0720dae81434de384b32a93b47e754d09Christian Maeder Comorphism (IdComorphism lid sublogics)
933baca0720dae81434de384b32a93b47e754d09Christian Maeder lid sublogics
933baca0720dae81434de384b32a93b47e754d09Christian Maeder basic_spec sentence symb_items symb_map_items
933baca0720dae81434de384b32a93b47e754d09Christian Maeder sign morphism symbol raw_symbol proof_tree
f2a87c712ea3cd13f86a95cae738f861f6c4a908Till Mossakowski lid sublogics
19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder basic_spec sentence symb_items symb_map_items
a89e661aad28f1b39f4fc9f9f9a4d46074234123Christian Maeder sign morphism symbol raw_symbol proof_tree
a89e661aad28f1b39f4fc9f9f9a4d46074234123Christian Maeder where
88ece6e49930670e8fd3ee79c89a2e918d2fbd0cChristian Maeder sourceLogic (IdComorphism lid _sub) = lid
0e51a998b1b213654c7a9eca451562041971f100Till Mossakowski targetLogic (IdComorphism lid _sub) = lid
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski sourceSublogic (IdComorphism _lid sub) = sub
d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder targetSublogic (IdComorphism _lid sub) = sub
d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder mapSublogic _ = id
ca8550c6d47234042130bdc10a152806ecbc9832Christian Maeder map_theory _ = return
d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder map_morphism _ = return
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski map_sentence _ = \_ -> return
ca8550c6d47234042130bdc10a152806ecbc9832Christian Maeder map_symbol _ = single
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski constituents _ = []
d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowskidata CompComorphism cid1 cid2 = CompComorphism cid1 cid2 deriving Show
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski
e9249d3ecd51a2b6a966a58669953e58d703adc6Till MossakowskityconCompComorphism :: TyCon
e9249d3ecd51a2b6a966a58669953e58d703adc6Till MossakowskityconCompComorphism = mkTyCon "Logic.Comorphism.CompComorphism"
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowskiinstance Typeable (CompComorphism cid1 cid2) where
d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder typeOf _ = mkTyConApp tyconCompComorphism []
d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowskiinstance (Language cid1, Language cid2)
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski => Language (CompComorphism cid1 cid2) where
d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder language_name (CompComorphism cid1 cid2) =
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski language_name cid1++ ";" ++language_name cid2
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski
d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maederinstance (Comorphism cid1
f7819aa9d183836144a98c70d4fa7d65e31cb513Till Mossakowski lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
f7819aa9d183836144a98c70d4fa7d65e31cb513Till Mossakowski sign1 morphism1 symbol1 raw_symbol1 proof_tree1
f7819aa9d183836144a98c70d4fa7d65e31cb513Till Mossakowski lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
f7819aa9d183836144a98c70d4fa7d65e31cb513Till Mossakowski sign2 morphism2 symbol2 raw_symbol2 proof_tree2,
8731f7b93b26083dc34a2c0937cd6493b42f2c2cTill Mossakowski Comorphism cid2
8731f7b93b26083dc34a2c0937cd6493b42f2c2cTill Mossakowski lid4 sublogics4 basic_spec4 sentence4 symb_items4 symb_map_items4
f2a87c712ea3cd13f86a95cae738f861f6c4a908Till Mossakowski sign4 morphism4 symbol4 raw_symbol4 proof_tree4
f2a87c712ea3cd13f86a95cae738f861f6c4a908Till Mossakowski lid3 sublogics3 basic_spec3 sentence3 symb_items3 symb_map_items3
f2a87c712ea3cd13f86a95cae738f861f6c4a908Till Mossakowski sign3 morphism3 symbol3 raw_symbol3 proof_tree3)
f2a87c712ea3cd13f86a95cae738f861f6c4a908Till Mossakowski => Comorphism (CompComorphism cid1 cid2)
f2a87c712ea3cd13f86a95cae738f861f6c4a908Till Mossakowski lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
f2a87c712ea3cd13f86a95cae738f861f6c4a908Till Mossakowski sign1 morphism1 symbol1 raw_symbol1 proof_tree1
f2a87c712ea3cd13f86a95cae738f861f6c4a908Till Mossakowski lid3 sublogics3 basic_spec3 sentence3 symb_items3 symb_map_items3
f2a87c712ea3cd13f86a95cae738f861f6c4a908Till Mossakowski sign3 morphism3 symbol3 raw_symbol3 proof_tree3 where
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski sourceLogic (CompComorphism cid1 _) =
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski sourceLogic cid1
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski targetLogic (CompComorphism _ cid2) =
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski targetLogic cid2
19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder sourceSublogic (CompComorphism cid1 _) =
19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder sourceSublogic cid1
d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder targetSublogic (CompComorphism cid1 cid2) =
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski mapSublogic cid2
5bb3727ef464d9f08ab0decb2d4a59c1352a389eChristian Maeder (idcoerce (targetLogic cid1) (sourceLogic cid2)
5bb3727ef464d9f08ab0decb2d4a59c1352a389eChristian Maeder (targetSublogic cid1))
5bb3727ef464d9f08ab0decb2d4a59c1352a389eChristian Maeder mapSublogic (CompComorphism cid1 cid2) =
9d34a8049237647d0188ee2ec88db2dc45f1f848Till Mossakowski mapSublogic cid2
9d34a8049237647d0188ee2ec88db2dc45f1f848Till Mossakowski . idcoerce (targetLogic cid1) (sourceLogic cid2)
5bb3727ef464d9f08ab0decb2d4a59c1352a389eChristian Maeder . mapSublogic cid1
5bb3727ef464d9f08ab0decb2d4a59c1352a389eChristian Maeder map_sentence (CompComorphism cid1 cid2) =
d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder \si1 se1 ->
d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder do (si2,_) <- map_sign cid1 si1
19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder se2 <- map_sentence cid1 si1 se1
9d34a8049237647d0188ee2ec88db2dc45f1f848Till Mossakowski (si2', se2') <- mcoerce (targetLogic cid1) (sourceLogic cid2)
d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder "Mapping sentence along comorphism" (si2, se2)
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski map_sentence cid2 si2' se2'
d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder
9d34a8049237647d0188ee2ec88db2dc45f1f848Till Mossakowski map_theory (CompComorphism cid1 cid2) =
9d34a8049237647d0188ee2ec88db2dc45f1f848Till Mossakowski \ti1 ->
0647a6c86b231e391826c7715338ba29cb4934c0Christian Maeder do ti2 <- map_theory cid1 ti1
19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder ti2' <- mcoerce (targetLogic cid1) (sourceLogic cid2)
0647a6c86b231e391826c7715338ba29cb4934c0Christian Maeder "Mapping theory along comorphism" ti2
0e51a998b1b213654c7a9eca451562041971f100Till Mossakowski map_theory cid2 ti2'
933baca0720dae81434de384b32a93b47e754d09Christian Maeder
map_morphism (CompComorphism cid1 cid2) = \ m1 ->
do m2 <- map_morphism cid1 m1
m3 <- mcoerce (targetLogic cid1) (sourceLogic cid2)
"Mapping signature morphism along comorphism"m2
map_morphism cid2 m3
map_symbol (CompComorphism cid1 cid2) = \ s1 ->
let mycast = fromJust . mcoerce (targetLogic cid1) (sourceLogic cid2)
"Mapping symbol along comorphism"
in unions
(map (map_symbol cid2 . mycast)
(toList (map_symbol cid1 s1)))
constituents (CompComorphism cid1 cid2) =
constituents cid1 ++ constituents cid2