Morphism.hs revision 58b5ac21d1c88344246aaedab0c0bdc7b759d7c6
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
a9de0a2f34860a24f457c777e740b7e87e6e3827Christian Maeder{-# OPTIONS -fglasgow-exts -fallow-undecidable-instances #-}
a9de0a2f34860a24f457c777e740b7e87e6e3827Christian Maeder{-# OPTIONS -fallow-incoherent-instances #-}
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till MossakowskiModule : $Header$
09b431a868c79a92ae7c9bd141565f43f9034144Christian MaederDescription : interface (type class) for logic projections (morphisms) in Hets
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till MossakowskiCopyright : (c) Till Mossakowski, Uni Bremen 2002-2004
97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian MaederLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
2eeec5240b424984e3ee26296da1eeab6c6d739eChristian MaederMaintainer : till@informatik.uni-bremen.de
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till MossakowskiStability : provisional
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till MossakowskiPortability : non-portable (via Logic)
09b431a868c79a92ae7c9bd141565f43f9034144Christian MaederInterface (type class) for logic projections (morphisms) in Hets
adea2e45fa61f1097aadc490a0aeaf4831b729ccChristian MaederProvides data structures for institution morphisms.
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski These are just collections of
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski functions between (some of) the types of logics.
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder{- References: see Logic.hs
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder morphism modifications / representation maps
ad270004874ce1d0697fb30d7309f180553bb315Christian Maederimport qualified Data.Set as Set
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maederimport Common.ATerm.Lib -- (ShATermConvertible)
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowskiclass (Language cid,
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski Logic lid1 sublogics1
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski basic_spec1 sentence1 symb_items1 symb_map_items1
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder sign1 morphism1 sign_symbol1 symbol1 proof_tree1,
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski Logic lid2 sublogics2
adea2e45fa61f1097aadc490a0aeaf4831b729ccChristian Maeder basic_spec2 sentence2 symb_items2 symb_map_items2
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder sign2 morphism2 sign_symbol2 symbol2 proof_tree2) =>
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder sign1 morphism1 sign_symbol1 symbol1 proof_tree1
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder sign2 morphism2 sign_symbol2 symbol2 proof_tree2
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder | cid -> lid1, cid -> lid2
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder , lid1 -> sublogics1 basic_spec1 sentence1 symb_items1
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder symb_map_items1 sign1 morphism1 sign_symbol1 symbol1 proof_tree1
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder , lid2 -> sublogics2 basic_spec2 sentence2 symb_items2
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder symb_map_items2 sign2 morphism2 sign_symbol2 symbol2 proof_tree2
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski -- source and target logic and sublogic
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski -- the source sublogic is the maximal one for which the comorphism works
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski -- the target sublogic is the resulting one
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski morSourceLogic :: cid -> lid1
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski morSourceSublogic :: cid -> sublogics1
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski morTargetLogic :: cid -> lid2
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski morTargetSublogic :: cid -> sublogics2
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder -- finer information of target sublogics corresponding to source sublogics
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder morMapSublogicSign :: cid -> sublogics1 -> sublogics2
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder -- information about the source sublogics corresponding to target sublogics
adea2e45fa61f1097aadc490a0aeaf4831b729ccChristian Maeder morMapSublogicSen :: cid -> sublogics2 -> sublogics1
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski -- the translation functions are partial
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski -- because the target may be a sublanguage
adea2e45fa61f1097aadc490a0aeaf4831b729ccChristian Maeder -- map_basic_spec :: cid -> basic_spec1 -> Maybe basic_spec2
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski -- we do not cover theoroidal morphisms,
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder -- since there are no relevant examples and they do not compose nicely
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski -- no mapping of theories, since signatures and sentences are mapped
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski -- contravariantly
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski morMap_sign :: cid -> sign1 -> Maybe sign2
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski morMap_morphism :: cid -> morphism1 -> Maybe morphism2
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski morMap_sentence :: cid -> sign1 -> sentence2 -> Maybe sentence1
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski -- also covers semi-morphisms ??
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski -- with no sentence translation
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder -- - but these are spans!
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski morMap_sign_symbol :: cid -> sign_symbol1 -> Set.Set sign_symbol2
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski -- morConstituents not needed, because composition only via lax triangles
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder-- identity morphisms
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowskidata IdMorphism lid sublogics =
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski IdMorphism lid sublogics deriving (Typeable, Show)
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowskiinstance Logic lid sublogics
4ef5e33657aae95850b7e6941f67ac1fb73cd13fChristian Maeder basic_spec sentence symb_items symb_map_items
4ef5e33657aae95850b7e6941f67ac1fb73cd13fChristian Maeder sign morphism sign_symbol symbol proof_tree =>
4ef5e33657aae95850b7e6941f67ac1fb73cd13fChristian Maeder Language (IdMorphism lid sublogics) where
4ef5e33657aae95850b7e6941f67ac1fb73cd13fChristian Maeder language_name (IdMorphism lid sub) =
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski case sublogic_names sub of
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski [] -> error "language_name IdMorphism"
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski h : _ -> "id_" ++ language_name lid ++ "." ++ h
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowskiinstance Logic lid sublogics
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski basic_spec sentence symb_items symb_map_items
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski sign morphism sign_symbol symbol proof_tree =>
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder Morphism (IdMorphism lid sublogics)
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski lid sublogics
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski basic_spec sentence symb_items symb_map_items
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder sign morphism sign_symbol symbol proof_tree
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski lid sublogics
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski basic_spec sentence symb_items symb_map_items
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski sign morphism sign_symbol symbol proof_tree
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski morSourceLogic (IdMorphism lid _sub) = lid
a98fd29a06e80e447af26d898044c23497adbc73Mihai Codescu morTargetLogic (IdMorphism lid _sub) = lid
a98fd29a06e80e447af26d898044c23497adbc73Mihai Codescu morSourceSublogic (IdMorphism _lid sub) = sub
a98fd29a06e80e447af26d898044c23497adbc73Mihai Codescu morTargetSublogic (IdMorphism _lid sub) = sub
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski --changed to identities!
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski morMapSublogicSign _ x = x
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski morMapSublogicSen _ x = x
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder morMap_sign _ = Just
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski morMap_morphism _ = Just
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski morMap_sentence _ = \_ -> Just
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski morMap_sign_symbol _ = Set.singleton
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski-- composition not needed, use lax triangles instead
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder-- comorphisms inducing morphisms
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maederclass Comorphism cid
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski sign1 morphism1 sign_symbol1 symbol1 proof_tree1
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski sign2 morphism2 sign_symbol2 symbol2 proof_tree2 =>
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder InducingComorphism cid
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski sign1 morphism1 sign_symbol1 symbol1 proof_tree1
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski sign2 morphism2 sign_symbol2 symbol2 proof_tree2
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder indMorMap_sign :: cid -> sign2 -> Maybe sign1
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder indMorMap_morphism :: cid -> morphism2 -> Maybe morphism1
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder epsilon :: cid -> sign2 -> Maybe morphism2
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder--------------------------------------------------------------------------
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder-- Morphisms as spans of comorphisms
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder-- if the morphism is (psi, alpha, beta) : I -> J
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder-- it is replaced with the following span
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder-- SignI id -> SignI psi -> SignJ
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder-- SenI alpha <- psi;SenJ id -> psi;SenJ
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder-- ModI beta -> psi^op;ModJ id <- psi^op;ModJ
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder-- 1. introduce a new logic for the domain of the span
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder-- this logic will have
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder-- * the name (SpanDomain cid) where cid is the name of the morphism
a98fd29a06e80e447af26d898044c23497adbc73Mihai Codescu-- * sublogics - pairs (s1, s2) with s1 being a sublogic of I and s2 being a sublogic of J; the lattice is the product lattice of the two existing lattices
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder-- * basic_spec will be () - the unit type, because we mix signatures with sentences in specifications
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder-- * sentence - sentences of J, wrapped
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder-- * symb_items - ()
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder-- * symb_map_items - ()
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder-- * sign - signatures of I
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder-- * morphism - morphisms of I
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder-- * sign_symbol - sign_symbols of I
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder-- * symbol - symbols of I
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder-- * proof_tree - proof_tree of J
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maederdata SpanDomain cid = SpanDomain cid
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder deriving (Eq, Show)
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maederdata SublogicsPair a b = SublogicsPair a b
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder deriving (Eq, Ord, Show)
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maederinstance Language cid =>
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder Language (SpanDomain cid) where
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder language_name (SpanDomain cid) = "SpanDomain" ++ language_name cid
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maederinstance Morphism cid
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder sign1 morphism1 sign_symbol1 symbol1 proof_tree1
4d7d53fec6b551333c79da6ae3b8ca2af0a741abChristian Maeder lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder sign2 morphism2 sign_symbol2 symbol2 proof_tree2=>
e8eb2b9d68adc3024eb1aa9899b902ed5a3fb460Christian Maeder Category (SpanDomain cid) sign1 morphism1
a98fd29a06e80e447af26d898044c23497adbc73Mihai Codescu ide (SpanDomain cid) = ide (morSourceLogic cid)
a98fd29a06e80e447af26d898044c23497adbc73Mihai Codescu -- ok in Haskell, because cid is a variable of type cid
a98fd29a06e80e447af26d898044c23497adbc73Mihai Codescu comp (SpanDomain cid) = comp (morSourceLogic cid)
c18a07fe36512679e66faa59274bb273e735738aMihai Codescu cod (SpanDomain cid) = cod (morSourceLogic cid)
da955132262baab309a50fdffe228c9efe68251dCui Jian dom (SpanDomain cid) = dom (morSourceLogic cid)
c18a07fe36512679e66faa59274bb273e735738aMihai Codescu legal_obj (SpanDomain cid) = legal_obj (morSourceLogic cid)
c18a07fe36512679e66faa59274bb273e735738aMihai Codescu legal_mor (SpanDomain cid) = legal_mor (morSourceLogic cid)
c18a07fe36512679e66faa59274bb273e735738aMihai Codescu{- the category of signatures is exactly the category of signatures of
da955132262baab309a50fdffe228c9efe68251dCui Jianthe sublogic on which the morphism is defined, but with another name -}
c18a07fe36512679e66faa59274bb273e735738aMihai Codescuinstance Morphism cid
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder sign1 morphism1 sign_symbol1 symbol1 proof_tree1
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder sign2 morphism2 sign_symbol2 symbol2 proof_tree2
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder Syntax (SpanDomain cid) () () () where
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder parse_basic_spec _ = Nothing
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder parse_symb_items _ = Nothing
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder parse_symb_map_items _ = Nothing
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maedernewtype S2 s = S2 { sentence2 :: s } deriving (Eq, Ord, Show, Typeable)
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maederinstance Pretty s => Pretty (S2 s) where
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder pretty (S2 x) = pretty x
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maederinstance ShATermConvertible s => ShATermConvertible (S2 s) where
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder toShATermAux att (S2 s) = do
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder (att1, i) <- toShATerm' att s
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder return $ addATerm (ShAAppl "S2" [i] []) att1
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder fromShATermAux ix att =
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder case getShATerm ix att of
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder ShAAppl "S2" [i] _ -> case fromShATerm' i att of
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder (att1, i1) -> (att1, S2 i1)
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder u -> fromShATermError "S2" u
e8eb2b9d68adc3024eb1aa9899b902ed5a3fb460Christian Maederinstance Morphism cid
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder sign1 morphism1 sign_symbol1 symbol1 proof_tree1
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder sign2 morphism2 sign_symbol2 symbol2 proof_tree2
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder => Sentences (SpanDomain cid) (S2 sentence2) sign1 morphism1
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder sign_symbol1 where
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder--one has to take care about signature and morphisms
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder--and translate them to targetLogic
cd6e5706893519bfcf24539afa252fcbed5097ddKlaus Luettich--we get a Maybe sign/morphism
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder map_sen (SpanDomain cid) mor1 (S2 sen) =
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder case morMap_morphism cid mor1 of
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder Just mor2 -> fmap S2 $
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder map_sen (morTargetLogic cid) mor2 sen
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder Nothing -> statErr (SpanDomain cid) "map_sen"
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder simplify_sen (SpanDomain cid) sigma (S2 sen) =
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder case morMap_sign cid sigma of
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder Just sigma2 -> S2 $
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder simplify_sen (morTargetLogic cid) sigma2 sen
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder Nothing -> error "simplify_sen"
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder parse_sentence (SpanDomain cid) = fmap (fmap S2) $
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder parse_sentence (morTargetLogic cid)
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder print_named (SpanDomain cid) = print_named (morTargetLogic cid)
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder . mapNamed sentence2
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder sym_of (SpanDomain cid) = sym_of (morSourceLogic cid)
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder symmap_of (SpanDomain cid) = symmap_of (morSourceLogic cid)
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder sym_name (SpanDomain cid) = sym_name (morSourceLogic cid)
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maederinstance (Morphism cid
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder sign1 morphism1 sign_symbol1 symbol1 proof_tree1
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder sign2 morphism2 sign_symbol2 symbol2 proof_tree2)
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder => StaticAnalysis (SpanDomain cid) () (S2 sentence2) () ()
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder sign1 morphism1 sign_symbol1 symbol1 where
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder sign_to_basic_spec _ _ _ = ()
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder ensures_amalgamability l _ = statErr l "ensures_amalgamability"
a98fd29a06e80e447af26d898044c23497adbc73Mihai Codescu symbol_to_raw (SpanDomain cid) = symbol_to_raw (morSourceLogic cid)
a98fd29a06e80e447af26d898044c23497adbc73Mihai Codescu id_to_raw (SpanDomain cid) = id_to_raw (morSourceLogic cid)
a98fd29a06e80e447af26d898044c23497adbc73Mihai Codescu matches (SpanDomain cid) = matches (morSourceLogic cid)
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder empty_signature (SpanDomain cid) = empty_signature (morSourceLogic cid)
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder signature_union (SpanDomain cid) = signature_union (morSourceLogic cid)
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder is_subsig (SpanDomain cid) = is_subsig (morSourceLogic cid)
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder final_union (SpanDomain cid) = final_union (morSourceLogic cid)
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder morphism_union (SpanDomain cid) = morphism_union (morSourceLogic cid)
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder inclusion (SpanDomain cid)= inclusion (morSourceLogic cid)
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder generated_sign (SpanDomain cid) = generated_sign (morSourceLogic cid)
a98fd29a06e80e447af26d898044c23497adbc73Mihai Codescu cogenerated_sign (SpanDomain cid) = cogenerated_sign (morSourceLogic cid)
a98fd29a06e80e447af26d898044c23497adbc73Mihai Codescu is_transportable (SpanDomain cid) = is_transportable (morSourceLogic cid)
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder is_injective (SpanDomain cid) = is_injective (morSourceLogic cid)
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maederinstance (SemiLatticeWithTop sublogics1, SemiLatticeWithTop sublogics2)
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder => SemiLatticeWithTop (SublogicsPair sublogics1 sublogics2) where
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder top = SublogicsPair top top
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder join (SublogicsPair x1 y1) (SublogicsPair x2 y2) =
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder SublogicsPair (join x1 x2) (join y1 y2)
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maederinstance (SemiLatticeWithTop sublogics1, MinSublogic sublogics2 sentence2)
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder => MinSublogic (SublogicsPair sublogics1 sublogics2) (S2 sentence2) where
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder minSublogic (S2 sen2) = SublogicsPair top (minSublogic sen2)
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder{- just a dummy implementation, it should be the sublogic of sen2 in J
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maederpaired with its image through morMapSublogicSen? -}
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maederinstance (MinSublogic sublogics1 alpha, SemiLatticeWithTop sublogics2)
da955132262baab309a50fdffe228c9efe68251dCui Jian => MinSublogic (SublogicsPair sublogics1 sublogics2) alpha where
c18a07fe36512679e66faa59274bb273e735738aMihai Codescu minSublogic x = SublogicsPair (minSublogic x) top
da955132262baab309a50fdffe228c9efe68251dCui Jian{- also should have instances of MinSublogic class for Sublogics-pair
da955132262baab309a50fdffe228c9efe68251dCui Jianand morphism1, sign_symbol1, sign1 this is why the wrapping is needed -}
c18a07fe36512679e66faa59274bb273e735738aMihai Codescu-- instance SemiLatticeWithTop sublogics => MinSublogic sublogics () where
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder-- minSublogic _ = top
4ef5e33657aae95850b7e6941f67ac1fb73cd13fChristian Maederinstance (MinSublogic sublogics1 alpha, SemiLatticeWithTop sublogics2)
4ef5e33657aae95850b7e6941f67ac1fb73cd13fChristian Maeder => ProjectSublogic (SublogicsPair sublogics1 sublogics2) alpha where
4ef5e33657aae95850b7e6941f67ac1fb73cd13fChristian Maeder projectSublogic _ x = x
4ef5e33657aae95850b7e6941f67ac1fb73cd13fChristian Maeder-- it should be used for (), morphism1, sign_symbol1, sign1
4ef5e33657aae95850b7e6941f67ac1fb73cd13fChristian Maederinstance (MinSublogic sublogics1 sign1, SemiLatticeWithTop sublogics2)
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder => ProjectSublogicM (SublogicsPair sublogics1 sublogics2) sign1 where
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder projectSublogicM _ x = Just x
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maederinstance (Typeable sublogics1, Typeable sublogics2)
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder => Typeable (SublogicsPair sublogics1 sublogics2) where
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder typeOf _ = mkTyConApp (mkTyCon "Logic.Morphism.SpanDomain") []
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maederinstance (ShATermConvertible sublogics1, ShATermConvertible sublogics2)
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder => ShATermConvertible (SublogicsPair sublogics1 sublogics2) where
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder toShATermAux att0 (SublogicsPair sub1 sub2) = do
e8eb2b9d68adc3024eb1aa9899b902ed5a3fb460Christian Maeder (att1,i1) <- toShATerm' att0 sub1
e8eb2b9d68adc3024eb1aa9899b902ed5a3fb460Christian Maeder (att2,i2) <- toShATerm' att1 sub2
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder return $ addATerm (ShAAppl "SublogicsPair" [i1,i2] []) att2
e8eb2b9d68adc3024eb1aa9899b902ed5a3fb460Christian Maeder fromShATermAux ix att =
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder case getShATerm ix att of
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder ShAAppl "SublogicsPair" [i1, i2] _ ->
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder case fromShATerm' i2 att of
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder (att2, i2') -> case fromShATerm' i1 att2 of
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder (att1, i1') -> (att1, SublogicsPair i1' i2')
cd6e5706893519bfcf24539afa252fcbed5097ddKlaus Luettich u -> fromShATermError "SublogicsPair" u
c40a1fdc8ec6978bd27240d6780d0e0a7b6b0056Dominik Lueckeinstance (Sublogics sublogics1, Sublogics sublogics2)
cd6e5706893519bfcf24539afa252fcbed5097ddKlaus Luettich => Sublogics (SublogicsPair sublogics1 sublogics2) where
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder sublogic_names (SublogicsPair sub1 sub2) =
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder [ x1 ++ " " ++ x2
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder | x1 <- sublogic_names sub1
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder , x2 <- sublogic_names sub2 ]
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maederinstance ( MinSublogic sublogics1 ()
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder , Morphism cid
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder sign1 morphism1 sign_symbol1 symbol1 proof_tree1
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder sign2 morphism2 sign_symbol2 symbol2 proof_tree2
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder ) => Logic (SpanDomain cid) (SublogicsPair sublogics1 sublogics2) ()
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder (S2 sentence2) () () sign1 morphism1 sign_symbol1 symbol1 proof_tree2
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder stability (SpanDomain _) = Experimental
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder data_logic (SpanDomain _) = Nothing
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder top_sublogic (SpanDomain cid) = SublogicsPair
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder (top_sublogic $ morSourceLogic cid) $ top_sublogic $ morTargetLogic cid
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder all_sublogics (SpanDomain cid) =
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder [ SublogicsPair x y
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder | x <- all_sublogics (morSourceLogic cid)
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder , y <- all_sublogics (morTargetLogic cid) ]
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder -- project_sublogic_epsilon - default implementation for now
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder provers _ = []
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder cons_checkers _ = []
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder conservativityCheck l _ _ _ = statErr l "conservativityCheck"
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder empty_proof_tree (SpanDomain cid) = empty_proof_tree (morTargetLogic cid)