Cross Reference: /hets/Logic/Comorphism.hs
Comorphism.hs revision 1a38107941725211e7c3f051f7a8f5e12199f03a
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
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
967e5f3c25249c779575864692935627004d3f9eChristian Maeder{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies, DeriveDataTypeable
967e5f3c25249c779575864692935627004d3f9eChristian Maeder , FlexibleInstances, UndecidableInstances, ExistentialQuantification #-}
81d182b21020b815887e9057959228546cf61b6bChristian Maeder{- |
f11f713bebd8e1e623a0a4361065df256033de47Christian MaederModule : $Header$
97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian MaederDescription : interface and class for logic translations
967e5f3c25249c779575864692935627004d3f9eChristian MaederCopyright : (c) Till Mossakowski, Uni Bremen 2002-2006
3f69b6948966979163bdfe8331c38833d5d90ecdChristian MaederLicense : GPLv2 or higher, see LICENSE.txt
967e5f3c25249c779575864692935627004d3f9eChristian MaederMaintainer : till@informatik.uni-bremen.de
89054b2b95a3f92e78324dc852f3d34704e2ca49Christian MaederStability : provisional
f3a94a197960e548ecd6520bb768cb0d547457bbChristian MaederPortability : non-portable (via Logic)
717686b54b9650402e2ebfbaadf433eab8ba5171Christian Maeder
717686b54b9650402e2ebfbaadf433eab8ba5171Christian MaederCentral interface (type class) for logic translations (comorphisms) in Hets
967e5f3c25249c779575864692935627004d3f9eChristian Maeder These are just collections of
967e5f3c25249c779575864692935627004d3f9eChristian Maeder functions between (some of) the types of logics.
967e5f3c25249c779575864692935627004d3f9eChristian Maeder
967e5f3c25249c779575864692935627004d3f9eChristian Maeder References: see Logic.hs
fd896e2068ad7e50aed66ac18c3720ea7ff2619fChristian Maeder-}
7221c71b38c871ce66eee4537cb681d468308dfbChristian Maeder
ee93fb771fcf3000d73c8e2f2000adb4b9a5158cChristian Maedermodule Logic.Comorphism
ee93fb771fcf3000d73c8e2f2000adb4b9a5158cChristian Maeder ( CompComorphism (..)
ee93fb771fcf3000d73c8e2f2000adb4b9a5158cChristian Maeder , InclComorphism
ac19f8695aa1b2d2d1cd1319da2530edd8f46a96Christian Maeder , inclusion_logic
8b9fda012e5ee53b7b2320c0638896a0ff6e99f3Christian Maeder , inclusion_source_sublogic
ee93fb771fcf3000d73c8e2f2000adb4b9a5158cChristian Maeder , inclusion_target_sublogic
ee93fb771fcf3000d73c8e2f2000adb4b9a5158cChristian Maeder , mkInclComorphism
e1839fb37a3a2ccd457464cb0dcc5efd466dbe22Christian Maeder , mkIdComorphism
4ef2a978e66e2246ff0b7f00c77deb7aabb28b8eChristian Maeder , Comorphism (..)
551af0e4ba6d96bb24f3555f3b30ed648e22e34aChristian Maeder , targetSublogic
fd896e2068ad7e50aed66ac18c3720ea7ff2619fChristian Maeder , map_sign
967e5f3c25249c779575864692935627004d3f9eChristian Maeder , wrapMapTheory
8e9c3881fb6e710b1e08bf5ac8ff9d393df2e74eChristian Maeder , mkTheoryMapping
78eeae099616e255ccf2e5f9122387bb10c68338Christian Maeder , AnyComorphism (..)
ad187062b0009820118c1b773a232e29b879a2faChristian Maeder , idComorphism
ad270004874ce1d0697fb30d7309f180553bb315Christian Maeder , isIdComorphism
fd896e2068ad7e50aed66ac18c3720ea7ff2619fChristian Maeder , isModelTransportable
551af0e4ba6d96bb24f3555f3b30ed648e22e34aChristian Maeder , hasModelExpansion
551af0e4ba6d96bb24f3555f3b30ed648e22e34aChristian Maeder , isWeaklyAmalgamable
551af0e4ba6d96bb24f3555f3b30ed648e22e34aChristian Maeder , compComorphism
551af0e4ba6d96bb24f3555f3b30ed648e22e34aChristian Maeder ) where
551af0e4ba6d96bb24f3555f3b30ed648e22e34aChristian Maeder
551af0e4ba6d96bb24f3555f3b30ed648e22e34aChristian Maederimport Logic.Logic
551af0e4ba6d96bb24f3555f3b30ed648e22e34aChristian Maederimport Logic.Coerce
551af0e4ba6d96bb24f3555f3b30ed648e22e34aChristian Maeder
1a75698c909ad515d59c76e65bd783f015c21c4dChristian Maederimport Common.AS_Annotation
1a75698c909ad515d59c76e65bd783f015c21c4dChristian Maederimport Common.Doc
51fb5d7edd9369c367dda2f8b15ddd6f8a146606Christian Maederimport Common.DocUtils
1a75698c909ad515d59c76e65bd783f015c21c4dChristian Maederimport Common.Id
1a75698c909ad515d59c76e65bd783f015c21c4dChristian Maederimport Common.LibName
1a75698c909ad515d59c76e65bd783f015c21c4dChristian Maederimport Common.ProofUtils
51fb5d7edd9369c367dda2f8b15ddd6f8a146606Christian Maederimport Common.Result
1a75698c909ad515d59c76e65bd783f015c21c4dChristian Maeder
67d92da5e9610aabad39055a16031154b4dc3748Christian Maederimport Data.Data
67d92da5e9610aabad39055a16031154b4dc3748Christian Maederimport Data.Maybe
67d92da5e9610aabad39055a16031154b4dc3748Christian Maederimport qualified Data.Set as Set
67d92da5e9610aabad39055a16031154b4dc3748Christian Maeder
67d92da5e9610aabad39055a16031154b4dc3748Christian Maederclass (Language cid,
67d92da5e9610aabad39055a16031154b4dc3748Christian Maeder Logic lid1 sublogics1
67d92da5e9610aabad39055a16031154b4dc3748Christian Maeder basic_spec1 sentence1 symb_items1 symb_map_items1
67d92da5e9610aabad39055a16031154b4dc3748Christian Maeder sign1 morphism1 symbol1 raw_symbol1 proof_tree1,
67d92da5e9610aabad39055a16031154b4dc3748Christian Maeder Logic lid2 sublogics2
67d92da5e9610aabad39055a16031154b4dc3748Christian Maeder basic_spec2 sentence2 symb_items2 symb_map_items2
67d92da5e9610aabad39055a16031154b4dc3748Christian Maeder sign2 morphism2 symbol2 raw_symbol2 proof_tree2) =>
7a879b08ae0ca30006f9be887a73212b07f10204Christian Maeder Comorphism cid
1a75698c909ad515d59c76e65bd783f015c21c4dChristian Maeder lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
1a75698c909ad515d59c76e65bd783f015c21c4dChristian Maeder sign1 morphism1 symbol1 raw_symbol1 proof_tree1
1a75698c909ad515d59c76e65bd783f015c21c4dChristian Maeder lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
1a75698c909ad515d59c76e65bd783f015c21c4dChristian Maeder sign2 morphism2 symbol2 raw_symbol2 proof_tree2
67d92da5e9610aabad39055a16031154b4dc3748Christian Maeder | cid -> lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
1a75698c909ad515d59c76e65bd783f015c21c4dChristian Maeder sign1 morphism1 symbol1 raw_symbol1 proof_tree1
1a75698c909ad515d59c76e65bd783f015c21c4dChristian Maeder lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
1a75698c909ad515d59c76e65bd783f015c21c4dChristian Maeder sign2 morphism2 symbol2 raw_symbol2 proof_tree2
1a75698c909ad515d59c76e65bd783f015c21c4dChristian Maeder where
1a75698c909ad515d59c76e65bd783f015c21c4dChristian Maeder {- source and target logic and sublogic
1a75698c909ad515d59c76e65bd783f015c21c4dChristian Maeder the source sublogic is the maximal one for which the comorphism works -}
1a75698c909ad515d59c76e65bd783f015c21c4dChristian Maeder sourceLogic :: cid -> lid1
1a75698c909ad515d59c76e65bd783f015c21c4dChristian Maeder sourceSublogic :: cid -> sublogics1
67d92da5e9610aabad39055a16031154b4dc3748Christian Maeder sourceSublogic cid = top_sublogic $ sourceLogic cid
7a879b08ae0ca30006f9be887a73212b07f10204Christian Maeder minSourceTheory :: cid -> Maybe (LibName, String)
1a75698c909ad515d59c76e65bd783f015c21c4dChristian Maeder minSourceTheory _ = Nothing
67d92da5e9610aabad39055a16031154b4dc3748Christian Maeder targetLogic :: cid -> lid2
b66eb6038bfbcd2fe520d87c151bb4f1f510e985Christian Maeder {- finer information of target sublogics corresponding to source sublogics
a89389521ddf76109168a0b339031575aafbd512Christian Maeder this function must be partial because mapTheory is partial -}
a89389521ddf76109168a0b339031575aafbd512Christian Maeder mapSublogic :: cid -> sublogics1 -> Maybe sublogics2
a89389521ddf76109168a0b339031575aafbd512Christian Maeder mapSublogic cid _ = Just $ top_sublogic $ targetLogic cid
a89389521ddf76109168a0b339031575aafbd512Christian Maeder {- the translation functions are partial
a89389521ddf76109168a0b339031575aafbd512Christian Maeder because the target may be a sublanguage
a89389521ddf76109168a0b339031575aafbd512Christian Maeder map_basic_spec :: cid -> basic_spec1 -> Result basic_spec2
a89389521ddf76109168a0b339031575aafbd512Christian Maeder cover theoroidal comorphisms as well -}
a89389521ddf76109168a0b339031575aafbd512Christian Maeder map_theory :: cid -> (sign1, [Named sentence1])
a89389521ddf76109168a0b339031575aafbd512Christian Maeder -> Result (sign2, [Named sentence2])
3c8d067accf18572352351ec42ff905c7297a8a5Christian Maeder -- map_theory but also consider sentence marks
3c8d067accf18572352351ec42ff905c7297a8a5Christian Maeder mapMarkedTheory :: cid -> (sign1, [Named sentence1])
1a75698c909ad515d59c76e65bd783f015c21c4dChristian Maeder -> Result (sign2, [Named sentence2])
9b30898b139ee02f97ac933b6d935ef0a4206921Christian Maeder mapMarkedTheory cid (sig, sens) = do
1a75698c909ad515d59c76e65bd783f015c21c4dChristian Maeder (sig2, sens2) <- map_theory cid (sig, map unmark sens)
1a75698c909ad515d59c76e65bd783f015c21c4dChristian Maeder return (sig2, map (markSen $ language_name cid) sens2)
67d92da5e9610aabad39055a16031154b4dc3748Christian Maeder map_morphism :: cid -> morphism1 -> Result morphism2
51fb5d7edd9369c367dda2f8b15ddd6f8a146606Christian Maeder map_morphism = mapDefaultMorphism
e1839fb37a3a2ccd457464cb0dcc5efd466dbe22Christian Maeder map_sentence :: cid -> sign1 -> sentence1 -> Result sentence2
67d92da5e9610aabad39055a16031154b4dc3748Christian Maeder {- also covers semi-comorphisms
b66eb6038bfbcd2fe520d87c151bb4f1f510e985Christian Maeder with no sentence translation
51fb5d7edd9369c367dda2f8b15ddd6f8a146606Christian Maeder - but these are spans! -}
ee93fb771fcf3000d73c8e2f2000adb4b9a5158cChristian Maeder map_sentence = failMapSentence
ee93fb771fcf3000d73c8e2f2000adb4b9a5158cChristian Maeder map_symbol :: cid -> sign1 -> symbol1 -> Set.Set symbol2
ee93fb771fcf3000d73c8e2f2000adb4b9a5158cChristian Maeder map_symbol = errMapSymbol
ee93fb771fcf3000d73c8e2f2000adb4b9a5158cChristian Maeder extractModel :: cid -> sign1 -> proof_tree2
ee93fb771fcf3000d73c8e2f2000adb4b9a5158cChristian Maeder -> Result (sign1, [Named sentence1])
ee93fb771fcf3000d73c8e2f2000adb4b9a5158cChristian Maeder extractModel cid _ _ = fail
51fb5d7edd9369c367dda2f8b15ddd6f8a146606Christian Maeder $ "extractModel not implemented for comorphism "
e7ce154edb906685b3fa7f6c0a764e18a4658068Christian Maeder ++ language_name cid
67d92da5e9610aabad39055a16031154b4dc3748Christian Maeder -- properties of comorphisms
67086e0fe40a985c5e8a3cf50e611f43234580c2Christian Maeder is_model_transportable :: cid -> Bool
ee93fb771fcf3000d73c8e2f2000adb4b9a5158cChristian Maeder {- a comorphism (\phi, \alpha, \beta) is model-transportable
ee93fb771fcf3000d73c8e2f2000adb4b9a5158cChristian Maeder if for any signature \Sigma,
ee93fb771fcf3000d73c8e2f2000adb4b9a5158cChristian Maeder any \Sigma-model M and any \phi(\Sigma)-model N
67086e0fe40a985c5e8a3cf50e611f43234580c2Christian Maeder for any isomorphism h : \beta_\Sigma(N) -> M
ee93fb771fcf3000d73c8e2f2000adb4b9a5158cChristian Maeder there exists an isomorphism h': N -> M' such that \beta_\Sigma(h') = h -}
67d92da5e9610aabad39055a16031154b4dc3748Christian Maeder is_model_transportable _ = False
ee93fb771fcf3000d73c8e2f2000adb4b9a5158cChristian Maeder has_model_expansion :: cid -> Bool
67086e0fe40a985c5e8a3cf50e611f43234580c2Christian Maeder has_model_expansion _ = False
588c0c022a0f4e129a89c3bc569daf6a835e182dChristian Maeder is_weakly_amalgamable :: cid -> Bool
717686b54b9650402e2ebfbaadf433eab8ba5171Christian Maeder is_weakly_amalgamable _ = False
717686b54b9650402e2ebfbaadf433eab8ba5171Christian Maeder constituents :: cid -> [String]
d48085f765fca838c1d972d2123601997174583dChristian Maeder constituents cid = [language_name cid]
d48085f765fca838c1d972d2123601997174583dChristian Maeder isInclusionComorphism :: cid -> Bool
717686b54b9650402e2ebfbaadf433eab8ba5171Christian Maeder isInclusionComorphism _ = False
d48085f765fca838c1d972d2123601997174583dChristian Maeder
d48085f765fca838c1d972d2123601997174583dChristian MaedertargetSublogic :: Comorphism cid
588c0c022a0f4e129a89c3bc569daf6a835e182dChristian Maeder lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
d48085f765fca838c1d972d2123601997174583dChristian Maeder sign1 morphism1 symbol1 raw_symbol1 proof_tree1
717686b54b9650402e2ebfbaadf433eab8ba5171Christian Maeder lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
717686b54b9650402e2ebfbaadf433eab8ba5171Christian Maeder sign2 morphism2 symbol2 raw_symbol2 proof_tree2
e7ce154edb906685b3fa7f6c0a764e18a4658068Christian Maeder => cid -> sublogics2
b66eb6038bfbcd2fe520d87c151bb4f1f510e985Christian MaedertargetSublogic cid = fromMaybe (top_sublogic $ targetLogic cid)
9b30898b139ee02f97ac933b6d935ef0a4206921Christian Maeder $ mapSublogic cid $ sourceSublogic cid
b66eb6038bfbcd2fe520d87c151bb4f1f510e985Christian Maeder
1a75698c909ad515d59c76e65bd783f015c21c4dChristian Maeder-- | this function is based on 'map_theory' using no sentences as input
b66eb6038bfbcd2fe520d87c151bb4f1f510e985Christian Maedermap_sign :: Comorphism cid
1a75698c909ad515d59c76e65bd783f015c21c4dChristian Maeder lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
b66eb6038bfbcd2fe520d87c151bb4f1f510e985Christian Maeder sign1 morphism1 symbol1 raw_symbol1 proof_tree1
1a75698c909ad515d59c76e65bd783f015c21c4dChristian Maeder lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
1a75698c909ad515d59c76e65bd783f015c21c4dChristian Maeder sign2 morphism2 symbol2 raw_symbol2 proof_tree2
b66eb6038bfbcd2fe520d87c151bb4f1f510e985Christian Maeder => cid -> sign1 -> Result (sign2, [Named sentence2])
b66eb6038bfbcd2fe520d87c151bb4f1f510e985Christian Maedermap_sign cid sign = wrapMapTheory cid (sign, [])
67d92da5e9610aabad39055a16031154b4dc3748Christian Maeder
b66eb6038bfbcd2fe520d87c151bb4f1f510e985Christian MaedermapDefaultMorphism :: Comorphism cid
1a75698c909ad515d59c76e65bd783f015c21c4dChristian Maeder lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
1a75698c909ad515d59c76e65bd783f015c21c4dChristian Maeder sign1 morphism1 symbol1 raw_symbol1 proof_tree1
1a75698c909ad515d59c76e65bd783f015c21c4dChristian Maeder lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
1a75698c909ad515d59c76e65bd783f015c21c4dChristian Maeder sign2 morphism2 symbol2 raw_symbol2 proof_tree2
f11f713bebd8e1e623a0a4361065df256033de47Christian Maeder => cid -> morphism1 -> Result morphism2
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian MaedermapDefaultMorphism cid mor = do
967e5f3c25249c779575864692935627004d3f9eChristian Maeder (sig1, _) <- map_sign cid $ dom mor
18b513ff41708f24e1a7407f36b719add813ffeaChristian Maeder (sig2, _) <- map_sign cid $ cod mor
dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian Maeder inclusion (targetLogic cid) sig1 sig2
a89e661aad28f1b39f4fc9f9f9a4d46074234123Christian Maeder
a23e572c8f957cc051a1b0831abd6fe9380d45c7Christian MaederfailMapSentence :: Comorphism cid
58b5ac21d1c88344246aaedab0c0bdc7b759d7c6Christian Maeder lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
58b5ac21d1c88344246aaedab0c0bdc7b759d7c6Christian Maeder sign1 morphism1 symbol1 raw_symbol1 proof_tree1
3c8d067accf18572352351ec42ff905c7297a8a5Christian Maeder lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
58b5ac21d1c88344246aaedab0c0bdc7b759d7c6Christian Maeder sign2 morphism2 symbol2 raw_symbol2 proof_tree2
f2ee9fc53048ea92bad79e3f5d292d83efd7f8beMihai Codescu => cid -> sign1 -> sentence1 -> Result sentence2
3c8d067accf18572352351ec42ff905c7297a8a5Christian MaederfailMapSentence cid _ _ =
81d182b21020b815887e9057959228546cf61b6bChristian Maeder fail $ "Unsupported sentence translation " ++ show cid
58b5ac21d1c88344246aaedab0c0bdc7b759d7c6Christian Maeder
242397ba0f1cc490e892130bf0df239deeecf5daChristian MaedererrMapSymbol :: Comorphism cid
2e9985cd67e4f2414becb670ef33b8f16513e41dChristian Maeder lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
242397ba0f1cc490e892130bf0df239deeecf5daChristian Maeder sign1 morphism1 symbol1 raw_symbol1 proof_tree1
58b5ac21d1c88344246aaedab0c0bdc7b759d7c6Christian Maeder lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
d769b9ca726a9b50d661847c0e58c41d6ef334b4Christian Maeder sign2 morphism2 symbol2 raw_symbol2 proof_tree2
551af0e4ba6d96bb24f3555f3b30ed648e22e34aChristian Maeder => cid -> sign1 -> symbol1 -> Set.Set symbol2
58b5ac21d1c88344246aaedab0c0bdc7b759d7c6Christian MaedererrMapSymbol cid _ _ = error $ "no symbol mapping for " ++ show cid
551af0e4ba6d96bb24f3555f3b30ed648e22e34aChristian Maeder
551af0e4ba6d96bb24f3555f3b30ed648e22e34aChristian Maeder-- | use this function instead of 'mapMarkedTheory'
d769b9ca726a9b50d661847c0e58c41d6ef334b4Christian MaederwrapMapTheory :: Comorphism cid
d769b9ca726a9b50d661847c0e58c41d6ef334b4Christian Maeder lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
3c8d067accf18572352351ec42ff905c7297a8a5Christian Maeder sign1 morphism1 symbol1 raw_symbol1 proof_tree1
d769b9ca726a9b50d661847c0e58c41d6ef334b4Christian Maeder lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
58b5ac21d1c88344246aaedab0c0bdc7b759d7c6Christian Maeder sign2 morphism2 symbol2 raw_symbol2 proof_tree2
ad187062b0009820118c1b773a232e29b879a2faChristian Maeder => cid -> (sign1, [Named sentence1])
3c8d067accf18572352351ec42ff905c7297a8a5Christian Maeder -> Result (sign2, [Named sentence2])
ad187062b0009820118c1b773a232e29b879a2faChristian MaederwrapMapTheory cid (sign, sens) =
551af0e4ba6d96bb24f3555f3b30ed648e22e34aChristian Maeder let res = mapMarkedTheory cid (sign, sens)
dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian Maeder lid1 = sourceLogic cid
842eedc62639561781b6c33533d1949693ef6cc5Christian Maeder thDoc = show (vcat $ pretty sign : map (print_named lid1) sens)
588c0c022a0f4e129a89c3bc569daf6a835e182dChristian Maeder in
588c0c022a0f4e129a89c3bc569daf6a835e182dChristian Maeder if isIdComorphism $ Comorphism cid then res else case sourceSublogic cid of
588c0c022a0f4e129a89c3bc569daf6a835e182dChristian Maeder sub -> case minSublogic sign of
842eedc62639561781b6c33533d1949693ef6cc5Christian Maeder sigLog -> case foldl lub sigLog
bfa9e03532243ceb487f0384d0f6a447f1ce7670Till Mossakowski $ map (minSublogic . sentence) sens of
967e5f3c25249c779575864692935627004d3f9eChristian Maeder senLog ->
967e5f3c25249c779575864692935627004d3f9eChristian Maeder if isSubElem senLog sub
f2ee9fc53048ea92bad79e3f5d292d83efd7f8beMihai Codescu then res
967e5f3c25249c779575864692935627004d3f9eChristian Maeder else Result
a95f5379cabb30d3beb0545002cf50e9e4fc2c86Christian Maeder [ Diag Hint thDoc nullRange
a95f5379cabb30d3beb0545002cf50e9e4fc2c86Christian Maeder , Diag Error
a95f5379cabb30d3beb0545002cf50e9e4fc2c86Christian Maeder ("for '" ++ language_name cid ++
a95f5379cabb30d3beb0545002cf50e9e4fc2c86Christian Maeder "' expected sublogic '" ++
a95f5379cabb30d3beb0545002cf50e9e4fc2c86Christian Maeder sublogicName sub ++
a95f5379cabb30d3beb0545002cf50e9e4fc2c86Christian Maeder "'\n but found sublogic '" ++
a95f5379cabb30d3beb0545002cf50e9e4fc2c86Christian Maeder sublogicName senLog ++
a95f5379cabb30d3beb0545002cf50e9e4fc2c86Christian Maeder "' with signature sublogic '" ++
a95f5379cabb30d3beb0545002cf50e9e4fc2c86Christian Maeder sublogicName sigLog ++ "'") nullRange] Nothing
a95f5379cabb30d3beb0545002cf50e9e4fc2c86Christian Maeder
a95f5379cabb30d3beb0545002cf50e9e4fc2c86Christian MaedermkTheoryMapping :: Monad m => (sign1 -> m (sign2, [Named sentence2]))
a95f5379cabb30d3beb0545002cf50e9e4fc2c86Christian Maeder -> (sign1 -> sentence1 -> m sentence2)
967e5f3c25249c779575864692935627004d3f9eChristian Maeder -> (sign1, [Named sentence1])
967e5f3c25249c779575864692935627004d3f9eChristian Maeder -> m (sign2, [Named sentence2])
ad187062b0009820118c1b773a232e29b879a2faChristian MaedermkTheoryMapping mapSig mapSen (sign, sens) = do
a95f5379cabb30d3beb0545002cf50e9e4fc2c86Christian Maeder (sign', sens') <- mapSig sign
a95f5379cabb30d3beb0545002cf50e9e4fc2c86Christian Maeder sens'' <- mapM (mapNamedM (mapSen sign) . unmark) sens
a95f5379cabb30d3beb0545002cf50e9e4fc2c86Christian Maeder return (sign', nameAndDisambiguate
a95f5379cabb30d3beb0545002cf50e9e4fc2c86Christian Maeder $ map (markSen "SignatureProperty") sens' ++ sens'')
a95f5379cabb30d3beb0545002cf50e9e4fc2c86Christian Maeder
a95f5379cabb30d3beb0545002cf50e9e4fc2c86Christian Maederdata InclComorphism lid sublogics = InclComorphism
a95f5379cabb30d3beb0545002cf50e9e4fc2c86Christian Maeder { inclusion_logic :: lid
a95f5379cabb30d3beb0545002cf50e9e4fc2c86Christian Maeder , inclusion_source_sublogic :: sublogics
a95f5379cabb30d3beb0545002cf50e9e4fc2c86Christian Maeder , inclusion_target_sublogic :: sublogics }
a95f5379cabb30d3beb0545002cf50e9e4fc2c86Christian Maeder deriving (Show, Typeable, Data)
a95f5379cabb30d3beb0545002cf50e9e4fc2c86Christian Maeder
a95f5379cabb30d3beb0545002cf50e9e4fc2c86Christian Maeder-- | construction of an identity comorphism
a95f5379cabb30d3beb0545002cf50e9e4fc2c86Christian MaedermkIdComorphism :: (Logic lid sublogics
a95f5379cabb30d3beb0545002cf50e9e4fc2c86Christian Maeder basic_spec sentence symb_items symb_map_items
a95f5379cabb30d3beb0545002cf50e9e4fc2c86Christian Maeder sign morphism symbol raw_symbol proof_tree) =>
1a75698c909ad515d59c76e65bd783f015c21c4dChristian Maeder lid -> sublogics -> InclComorphism lid sublogics
1a75698c909ad515d59c76e65bd783f015c21c4dChristian MaedermkIdComorphism lid sub = InclComorphism
1a75698c909ad515d59c76e65bd783f015c21c4dChristian Maeder { inclusion_logic = lid
1a75698c909ad515d59c76e65bd783f015c21c4dChristian Maeder , inclusion_source_sublogic = sub
1a75698c909ad515d59c76e65bd783f015c21c4dChristian Maeder , inclusion_target_sublogic = sub }
1a75698c909ad515d59c76e65bd783f015c21c4dChristian Maeder
1a75698c909ad515d59c76e65bd783f015c21c4dChristian Maeder-- | construction of an inclusion comorphism
1a75698c909ad515d59c76e65bd783f015c21c4dChristian MaedermkInclComorphism :: (Logic lid sublogics
1a75698c909ad515d59c76e65bd783f015c21c4dChristian Maeder basic_spec sentence symb_items symb_map_items
a95f5379cabb30d3beb0545002cf50e9e4fc2c86Christian Maeder sign morphism symbol raw_symbol proof_tree,
ad187062b0009820118c1b773a232e29b879a2faChristian Maeder Monad m) =>
ad187062b0009820118c1b773a232e29b879a2faChristian Maeder lid -> sublogics -> sublogics
a95f5379cabb30d3beb0545002cf50e9e4fc2c86Christian Maeder -> m (InclComorphism lid sublogics)
a95f5379cabb30d3beb0545002cf50e9e4fc2c86Christian MaedermkInclComorphism lid srcSub trgSub =
1a75698c909ad515d59c76e65bd783f015c21c4dChristian Maeder if isSubElem srcSub trgSub
1a75698c909ad515d59c76e65bd783f015c21c4dChristian Maeder then return InclComorphism
ad187062b0009820118c1b773a232e29b879a2faChristian Maeder { inclusion_logic = lid
ad187062b0009820118c1b773a232e29b879a2faChristian Maeder , inclusion_source_sublogic = srcSub
ad187062b0009820118c1b773a232e29b879a2faChristian Maeder , inclusion_target_sublogic = trgSub }
1a75698c909ad515d59c76e65bd783f015c21c4dChristian Maeder else fail ("mkInclComorphism: first sublogic must be a " ++
1a75698c909ad515d59c76e65bd783f015c21c4dChristian Maeder "subElem of the second sublogic")
a95f5379cabb30d3beb0545002cf50e9e4fc2c86Christian Maeder
a95f5379cabb30d3beb0545002cf50e9e4fc2c86Christian Maederinstance (Language lid, Eq sublogics, Show sublogics, SublogicName sublogics)
a95f5379cabb30d3beb0545002cf50e9e4fc2c86Christian Maeder => Language (InclComorphism lid sublogics) where
a95f5379cabb30d3beb0545002cf50e9e4fc2c86Christian Maeder language_name (InclComorphism lid sub_src sub_trg) =
9659c509ce5e78adc51d7b02a76274eddcba9338Christian Maeder let sblName = sublogicName sub_src
9659c509ce5e78adc51d7b02a76274eddcba9338Christian Maeder lname = language_name lid
1a75698c909ad515d59c76e65bd783f015c21c4dChristian Maeder in if sub_src == sub_trg
1a75698c909ad515d59c76e65bd783f015c21c4dChristian Maeder then "id_" ++ lname ++
1a75698c909ad515d59c76e65bd783f015c21c4dChristian Maeder if null sblName then "" else '.' : sblName
a95f5379cabb30d3beb0545002cf50e9e4fc2c86Christian Maeder else "incl_" ++ lname ++ ':'
9659c509ce5e78adc51d7b02a76274eddcba9338Christian Maeder : sblName ++ "->" ++ sublogicName sub_trg
9659c509ce5e78adc51d7b02a76274eddcba9338Christian Maeder
551af0e4ba6d96bb24f3555f3b30ed648e22e34aChristian Maederinstance Logic lid sublogics
a95f5379cabb30d3beb0545002cf50e9e4fc2c86Christian Maeder basic_spec sentence symb_items symb_map_items
a95f5379cabb30d3beb0545002cf50e9e4fc2c86Christian Maeder sign morphism symbol raw_symbol proof_tree =>
1a75698c909ad515d59c76e65bd783f015c21c4dChristian Maeder Comorphism (InclComorphism lid sublogics)
a95f5379cabb30d3beb0545002cf50e9e4fc2c86Christian Maeder lid sublogics
83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maeder basic_spec sentence symb_items symb_map_items
83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maeder sign morphism symbol raw_symbol proof_tree
a95f5379cabb30d3beb0545002cf50e9e4fc2c86Christian Maeder lid sublogics
97ee7048e63953c5617342ce38c30cbcb35cc0beChristian Maeder basic_spec sentence symb_items symb_map_items
97ee7048e63953c5617342ce38c30cbcb35cc0beChristian Maeder sign morphism symbol raw_symbol proof_tree
b66eb6038bfbcd2fe520d87c151bb4f1f510e985Christian Maeder where
1a75698c909ad515d59c76e65bd783f015c21c4dChristian Maeder sourceLogic = inclusion_logic
b66eb6038bfbcd2fe520d87c151bb4f1f510e985Christian Maeder targetLogic = inclusion_logic
1a75698c909ad515d59c76e65bd783f015c21c4dChristian Maeder sourceSublogic = inclusion_source_sublogic
1a75698c909ad515d59c76e65bd783f015c21c4dChristian Maeder mapSublogic cid subl =
1a75698c909ad515d59c76e65bd783f015c21c4dChristian Maeder if isSubElem subl $ inclusion_source_sublogic cid
1a75698c909ad515d59c76e65bd783f015c21c4dChristian Maeder then Just subl
1a75698c909ad515d59c76e65bd783f015c21c4dChristian Maeder else Nothing
588c0c022a0f4e129a89c3bc569daf6a835e182dChristian Maeder map_theory _ = return
b66eb6038bfbcd2fe520d87c151bb4f1f510e985Christian Maeder map_morphism _ = return
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder map_sentence _ _ = return
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder map_symbol _ _ = Set.singleton
1a75698c909ad515d59c76e65bd783f015c21c4dChristian Maeder constituents cid =
dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian Maeder if inclusion_source_sublogic cid
ad187062b0009820118c1b773a232e29b879a2faChristian Maeder == inclusion_target_sublogic cid
ad187062b0009820118c1b773a232e29b879a2faChristian Maeder then []
588c0c022a0f4e129a89c3bc569daf6a835e182dChristian Maeder else [language_name cid]
1a75698c909ad515d59c76e65bd783f015c21c4dChristian Maeder is_model_transportable _ = True
588c0c022a0f4e129a89c3bc569daf6a835e182dChristian Maeder has_model_expansion _ = True
ad187062b0009820118c1b773a232e29b879a2faChristian Maeder is_weakly_amalgamable _ = True
07b72edb610ee53b4832d132e96b0a3d8423f8ebChristian Maeder isInclusionComorphism _ = True
data CompComorphism cid1 cid2 = CompComorphism cid1 cid2
deriving (Show, Typeable, Data)
instance (Language cid1, Language cid2)
=> Language (CompComorphism cid1 cid2) where
language_name (CompComorphism cid1 cid2) =
language_name cid1 ++ ";" ++ language_name cid2
instance (Comorphism cid1
lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
sign1 morphism1 symbol1 raw_symbol1 proof_tree1
lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
sign2 morphism2 symbol2 raw_symbol2 proof_tree2,
Comorphism cid2
lid4 sublogics4 basic_spec4 sentence4 symb_items4 symb_map_items4
sign4 morphism4 symbol4 raw_symbol4 proof_tree4
lid3 sublogics3 basic_spec3 sentence3 symb_items3 symb_map_items3
sign3 morphism3 symbol3 raw_symbol3 proof_tree3)
=> Comorphism (CompComorphism cid1 cid2)
lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
sign1 morphism1 symbol1 raw_symbol1 proof_tree1
lid3 sublogics3 basic_spec3 sentence3 symb_items3 symb_map_items3
sign3 morphism3 symbol3 raw_symbol3 proof_tree3 where
sourceLogic (CompComorphism cid1 _) =
sourceLogic cid1
targetLogic (CompComorphism _ cid2) =
targetLogic cid2
sourceSublogic (CompComorphism cid1 _) =
sourceSublogic cid1
mapSublogic (CompComorphism cid1 cid2) sl =
mapSublogic cid1 sl >>=
mapSublogic cid2 .
forceCoerceSublogic (targetLogic cid1) (sourceLogic cid2)
map_sentence (CompComorphism cid1 cid2) si1 se1 =
do (si2, _) <- map_sign cid1 si1
se2 <- map_sentence cid1 si1 se1
(si2', se2') <- coerceBasicTheory
(targetLogic cid1) (sourceLogic cid2)
"Mapping sentence along comorphism" (si2, [makeNamed "" se2])
case se2' of
[x] -> map_sentence cid2 si2' $ sentence x
_ -> error "CompComorphism.map_sentence"
map_theory (CompComorphism cid1 cid2) ti1 =
do ti2 <- map_theory cid1 ti1
ti2' <- coerceBasicTheory (targetLogic cid1) (sourceLogic cid2)
"Mapping theory along comorphism" ti2
wrapMapTheory cid2 ti2'
map_morphism (CompComorphism cid1 cid2) m1 =
do m2 <- map_morphism cid1 m1
m3 <- coerceMorphism (targetLogic cid1) (sourceLogic cid2)
"Mapping signature morphism along comorphism" m2
map_morphism cid2 m3
map_symbol (CompComorphism cid1 cid2) sig1 = let
th = map_sign cid1 sig1 in
case maybeResult th of
Nothing -> error "failed translating signature"
Just (sig2', _) -> let
th2 = coerceBasicTheory
(targetLogic cid1) (sourceLogic cid2)
"Mapping symbol along comorphism" (sig2', [])
in case maybeResult th2 of
Nothing -> error "failed coercing"
Just (sig2, _) ->
\ s1 ->
let mycast = coerceSymbol (targetLogic cid1) (sourceLogic cid2)
in Set.unions
(map (map_symbol cid2 sig2 . mycast)
(Set.toList (map_symbol cid1 sig1 s1)))
extractModel (CompComorphism cid1 cid2) sign pt3 =
let lid1 = sourceLogic cid1
lid3 = sourceLogic cid2
in if language_name lid1 == language_name lid3 then do
bTh1 <- map_sign cid1 sign
(sign1, _) <-
coerceBasicTheory (targetLogic cid1) lid3 "extractModel1" bTh1
bTh2 <- extractModel cid2 sign1 pt3
coerceBasicTheory lid3 lid1 "extractModel2" bTh2
else fail $ "extractModel not implemented for comorphism composition with "
++ language_name cid1
constituents (CompComorphism cid1 cid2) =
constituents cid1 ++ constituents cid2
is_model_transportable (CompComorphism cid1 cid2) =
is_model_transportable cid1 && is_model_transportable cid2
has_model_expansion (CompComorphism cid1 cid2) =
has_model_expansion cid1 && has_model_expansion cid2
is_weakly_amalgamable (CompComorphism cid1 cid2) =
is_weakly_amalgamable cid1 && is_weakly_amalgamable cid2
isInclusionComorphism (CompComorphism cid1 cid2) =
isInclusionComorphism cid1 && isInclusionComorphism cid2
-- * Comorphisms and existential types for the logic graph
-- | Existential type for comorphisms
data AnyComorphism = forall cid lid1 sublogics1
basic_spec1 sentence1 symb_items1 symb_map_items1
sign1 morphism1 symbol1 raw_symbol1 proof_tree1
lid2 sublogics2
basic_spec2 sentence2 symb_items2 symb_map_items2
sign2 morphism2 symbol2 raw_symbol2 proof_tree2 .
Comorphism cid
lid1 sublogics1 basic_spec1 sentence1
symb_items1 symb_map_items1
sign1 morphism1 symbol1 raw_symbol1 proof_tree1
lid2 sublogics2 basic_spec2 sentence2
symb_items2 symb_map_items2
sign2 morphism2 symbol2 raw_symbol2 proof_tree2 =>
Comorphism cid deriving Typeable -- used for GTheory
instance Eq AnyComorphism where
a == b = compare a b == EQ
instance Ord AnyComorphism where
compare (Comorphism cid1) (Comorphism cid2) = compare
(language_name cid1, constituents cid1)
(language_name cid2, constituents cid2)
-- maybe needs to be refined, using comorphism translations?
instance Show AnyComorphism where
show (Comorphism cid) = language_name cid
++ " : " ++ language_name (sourceLogic cid)
++ " -> " ++ language_name (targetLogic cid)
instance Pretty AnyComorphism where
pretty = text . show
-- | compute the identity comorphism for a logic
idComorphism :: AnyLogic -> AnyComorphism
idComorphism (Logic lid) = Comorphism (mkIdComorphism lid (top_sublogic lid))
-- | Test whether a comporphism is the identity
isIdComorphism :: AnyComorphism -> Bool
isIdComorphism (Comorphism cid) = null $ constituents cid
-- * Properties of comorphisms
-- | Test whether a comorphism is model-transportable
isModelTransportable :: AnyComorphism -> Bool
isModelTransportable (Comorphism cid) = is_model_transportable cid
-- | Test whether a comorphism has model expansion
hasModelExpansion :: AnyComorphism -> Bool
hasModelExpansion (Comorphism cid) = has_model_expansion cid
-- | Test whether a comorphism is weakly amalgamable
isWeaklyAmalgamable :: AnyComorphism -> Bool
isWeaklyAmalgamable (Comorphism cid) = is_weakly_amalgamable cid
-- | Compose comorphisms
compComorphism :: Monad m => AnyComorphism -> AnyComorphism -> m AnyComorphism
compComorphism (Comorphism cid1) (Comorphism cid2) =
let l1 = targetLogic cid1
l2 = sourceLogic cid2
msg = "ogic mismatch in composition of " ++ language_name cid1
++ " and " ++ language_name cid2
in
if language_name l1 == language_name l2 then
if isSubElem (forceCoerceSublogic l1 l2 $ targetSublogic cid1)
$ sourceSublogic cid2
then return $ Comorphism (CompComorphism cid1 cid2)
else fail $ "Subl" ++ msg ++ " (Expected sublogic "
++ sublogicName (sourceSublogic cid2)
++ " but found sublogic "
++ sublogicName (targetSublogic cid1) ++ ")"
else fail $ 'L' : msg ++ " (Expected logic "
++ language_name l2
++ " but found logic "
++ language_name l1 ++ ")"