Morphism.hs revision 18b513ff41708f24e1a7407f36b719add813ffea
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
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
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski -- 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
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder morMapSublogicSen :: cid -> sublogics2 -> sublogics1
adea2e45fa61f1097aadc490a0aeaf4831b729ccChristian Maeder -- the translation functions are partial
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski -- because the target may be a sublanguage
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski -- map_basic_spec :: cid -> basic_spec1 -> Maybe basic_spec2
adea2e45fa61f1097aadc490a0aeaf4831b729ccChristian Maeder -- we do not cover theoroidal morphisms,
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski -- since there are no relevant examples and they do not compose nicely
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder -- 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
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski -- - but these are spans!
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder 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
adea2e45fa61f1097aadc490a0aeaf4831b729ccChristian Maederdata IdMorphism lid sublogics =
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder IdMorphism lid sublogics deriving (Typeable, Show)
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowskiinstance Logic lid sublogics
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski basic_spec sentence symb_items symb_map_items
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder sign morphism sign_symbol symbol proof_tree =>
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski Language (IdMorphism lid sublogics) where
4ef5e33657aae95850b7e6941f67ac1fb73cd13fChristian Maeder language_name (IdMorphism lid sub) =
4ef5e33657aae95850b7e6941f67ac1fb73cd13fChristian Maeder case sublogic_names sub of
4ef5e33657aae95850b7e6941f67ac1fb73cd13fChristian Maeder [] -> error "language_name IdMorphism"
4ef5e33657aae95850b7e6941f67ac1fb73cd13fChristian Maeder h : _ -> "id_" ++ language_name lid ++ "." ++ h
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowskiinstance Logic lid sublogics
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski basic_spec sentence symb_items symb_map_items
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder sign morphism sign_symbol symbol proof_tree =>
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski 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
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder sign morphism sign_symbol symbol proof_tree
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski morSourceLogic (IdMorphism lid _sub) = lid
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski morTargetLogic (IdMorphism lid _sub) = lid
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski morSourceSublogic (IdMorphism _lid sub) = sub
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski morTargetSublogic (IdMorphism _lid sub) = sub
a98fd29a06e80e447af26d898044c23497adbc73Mihai Codescu --changed to identities!
a98fd29a06e80e447af26d898044c23497adbc73Mihai Codescu morMapSublogicSign _ x = x
a98fd29a06e80e447af26d898044c23497adbc73Mihai Codescu morMapSublogicSen _ x = x
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski morMap_sign _ = Just
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski morMap_morphism _ = Just
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski morMap_sentence _ = \_ -> Just
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder morMap_sign_symbol _ = Set.singleton
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski-- composition not needed, use lax triangles instead
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder-- | comorphisms inducing morphisms
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowskiclass Comorphism cid
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder sign1 morphism1 sign_symbol1 symbol1 proof_tree1
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder sign2 morphism2 sign_symbol2 symbol2 proof_tree2 =>
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski InducingComorphism cid
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder sign1 morphism1 sign_symbol1 symbol1 proof_tree1
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder sign2 morphism2 sign_symbol2 symbol2 proof_tree2
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski indMorMap_sign :: cid -> sign2 -> Maybe sign1
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski indMorMap_morphism :: cid -> morphism2 -> Maybe morphism1
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski 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
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder-- ModI beta -> psi^op;ModJ id <- psi^op;ModJ
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder-- 1. introduce a new logic for the domain of the span
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder-- this logic will have
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder-- * the name (SpanDomain cid) where cid is the name of the morphism
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder-- * sublogics - pairs (s1, s2) with s1 being a sublogic of I and s2
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder-- being a sublogic of J; the lattice is the product lattice of the two
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder-- existing lattices
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder-- * basic_spec will be () - the unit type, because we mix signatures
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder-- with sentences in specifications
a98fd29a06e80e447af26d898044c23497adbc73Mihai Codescu-- * 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
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder-- * proof_tree - proof_tree of J
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maederdata SpanDomain cid = SpanDomain cid deriving (Eq, Show)
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maederdata SublogicsPair a b = SublogicsPair a b deriving (Eq, Ord, Show)
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maederinstance Language cid => Language (SpanDomain cid) where
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder language_name (SpanDomain cid) = "SpanDomain" ++ language_name cid
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder{- the category of signatures is exactly the category of signatures of
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maederthe sublogic on which the morphism is defined, but with another name -}
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
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder sign2 morphism2 sign_symbol2 symbol2 proof_tree2
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder => Syntax (SpanDomain cid) () () ()
4d7d53fec6b551333c79da6ae3b8ca2af0a741abChristian Maeder-- default is ok
e8eb2b9d68adc3024eb1aa9899b902ed5a3fb460Christian Maedernewtype S2 s = S2 { sentence2 :: s } deriving (Eq, Ord, Show, Typeable)
a98fd29a06e80e447af26d898044c23497adbc73Mihai Codescuinstance Pretty s => Pretty (S2 s) where
a98fd29a06e80e447af26d898044c23497adbc73Mihai Codescu pretty (S2 x) = pretty x
c18a07fe36512679e66faa59274bb273e735738aMihai Codescuinstance ShATermConvertible s => ShATermConvertible (S2 s) where
da955132262baab309a50fdffe228c9efe68251dCui Jian toShATermAux att (S2 s) = do
c18a07fe36512679e66faa59274bb273e735738aMihai Codescu (att1, i) <- toShATerm' att s
c18a07fe36512679e66faa59274bb273e735738aMihai Codescu return $ addATerm (ShAAppl "S2" [i] []) att1
da955132262baab309a50fdffe228c9efe68251dCui Jian fromShATermAux ix att =
c18a07fe36512679e66faa59274bb273e735738aMihai Codescu case getShATerm ix att of
da955132262baab309a50fdffe228c9efe68251dCui Jian ShAAppl "S2" [i] _ -> case fromShATerm' i att of
c18a07fe36512679e66faa59274bb273e735738aMihai Codescu (att1, i1) -> (att1, S2 i1)
c18a07fe36512679e66faa59274bb273e735738aMihai Codescu u -> fromShATermError "S2" u
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
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder sign2 morphism2 sign_symbol2 symbol2 proof_tree2
cd6e5706893519bfcf24539afa252fcbed5097ddKlaus Luettich => 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
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)
e8eb2b9d68adc3024eb1aa9899b902ed5a3fb460Christian 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
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder sign2 morphism2 sign_symbol2 symbol2 proof_tree2)
cd6e5706893519bfcf24539afa252fcbed5097ddKlaus Luettich => 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"
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder symbol_to_raw (SpanDomain cid) = symbol_to_raw (morSourceLogic cid)
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder id_to_raw (SpanDomain cid) = id_to_raw (morSourceLogic cid)
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder 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 final_union (SpanDomain cid) = final_union (morSourceLogic cid)
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder morphism_union (SpanDomain cid) = morphism_union (morSourceLogic cid)
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder inclusion (SpanDomain cid)= inclusion (morSourceLogic cid)
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder generated_sign (SpanDomain cid) = generated_sign (morSourceLogic cid)
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder cogenerated_sign (SpanDomain cid) = cogenerated_sign (morSourceLogic cid)
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder 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)
556f473448dfcceee22afaa89ed7a364489cdbbbChristian 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? -}
a98fd29a06e80e447af26d898044c23497adbc73Mihai Codescuinstance (MinSublogic sublogics1 alpha, SemiLatticeWithTop sublogics2)
a98fd29a06e80e447af26d898044c23497adbc73Mihai Codescu => MinSublogic (SublogicsPair sublogics1 sublogics2) alpha where
a98fd29a06e80e447af26d898044c23497adbc73Mihai Codescu minSublogic x = SublogicsPair (minSublogic x) top
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder{- also should have instances of MinSublogic class for Sublogics-pair
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maederand morphism1, sign_symbol1, sign1 this is why the wrapping is needed -}
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder-- instance SemiLatticeWithTop sublogics => MinSublogic sublogics () where
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder-- minSublogic _ = top
a98fd29a06e80e447af26d898044c23497adbc73Mihai Codescuinstance (MinSublogic sublogics1 alpha, SemiLatticeWithTop sublogics2)
a98fd29a06e80e447af26d898044c23497adbc73Mihai Codescu => ProjectSublogic (SublogicsPair sublogics1 sublogics2) alpha where
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder projectSublogic _ x = x
a98fd29a06e80e447af26d898044c23497adbc73Mihai Codescu-- it should be used for (), morphism1, sign_symbol1, sign1
09b431a868c79a92ae7c9bd141565f43f9034144Christian 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
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder (att1,i1) <- toShATerm' att0 sub1
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder (att2,i2) <- toShATerm' att1 sub2
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder return $ addATerm (ShAAppl "SublogicsPair" [i1,i2] []) att2
da955132262baab309a50fdffe228c9efe68251dCui Jian fromShATermAux ix att =
c18a07fe36512679e66faa59274bb273e735738aMihai Codescu case getShATerm ix att of
da955132262baab309a50fdffe228c9efe68251dCui Jian ShAAppl "SublogicsPair" [i1, i2] _ ->
da955132262baab309a50fdffe228c9efe68251dCui Jian case fromShATerm' i2 att of
da955132262baab309a50fdffe228c9efe68251dCui Jian (att2, i2') -> case fromShATerm' i1 att2 of
c18a07fe36512679e66faa59274bb273e735738aMihai Codescu (att1, i1') -> (att1, SublogicsPair i1' i2')
c18a07fe36512679e66faa59274bb273e735738aMihai Codescu u -> fromShATermError "SublogicsPair" u
4ef5e33657aae95850b7e6941f67ac1fb73cd13fChristian Maederinstance (Sublogics sublogics1, Sublogics sublogics2)
4ef5e33657aae95850b7e6941f67ac1fb73cd13fChristian Maeder => Sublogics (SublogicsPair sublogics1 sublogics2) where
4ef5e33657aae95850b7e6941f67ac1fb73cd13fChristian Maeder sublogic_names (SublogicsPair sub1 sub2) =
4ef5e33657aae95850b7e6941f67ac1fb73cd13fChristian Maeder [ x1 ++ " " ++ x2
4ef5e33657aae95850b7e6941f67ac1fb73cd13fChristian Maeder | x1 <- sublogic_names sub1
4ef5e33657aae95850b7e6941f67ac1fb73cd13fChristian Maeder , x2 <- sublogic_names sub2 ]
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maederinstance ( MinSublogic sublogics1 ()
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder , 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 ) => Logic (SpanDomain cid) (SublogicsPair sublogics1 sublogics2) ()
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder (S2 sentence2) () () sign1 morphism1 sign_symbol1 symbol1 proof_tree2
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder stability (SpanDomain _) = Experimental
e8eb2b9d68adc3024eb1aa9899b902ed5a3fb460Christian Maeder data_logic (SpanDomain _) = Nothing
e8eb2b9d68adc3024eb1aa9899b902ed5a3fb460Christian Maeder top_sublogic (SpanDomain cid) = SublogicsPair
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder (top_sublogic $ morSourceLogic cid) $ top_sublogic $ morTargetLogic cid
e8eb2b9d68adc3024eb1aa9899b902ed5a3fb460Christian Maeder all_sublogics (SpanDomain cid) =
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder [ SublogicsPair x y
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder | x <- all_sublogics (morSourceLogic cid)
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder , y <- all_sublogics (morTargetLogic cid) ]
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder -- project_sublogic_epsilon - default implementation for now
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder provers _ = []
cd6e5706893519bfcf24539afa252fcbed5097ddKlaus Luettich cons_checkers _ = []
cd6e5706893519bfcf24539afa252fcbed5097ddKlaus Luettich conservativityCheck l _ _ _ = statErr l "conservativityCheck"
c40a1fdc8ec6978bd27240d6780d0e0a7b6b0056Dominik Luecke empty_proof_tree (SpanDomain cid) = empty_proof_tree (morTargetLogic cid)
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder-- * Morphisms
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder-- | Existential type for morphisms
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maederdata AnyMorphism = forall cid lid1 sublogics1
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder basic_spec1 sentence1 symb_items1 symb_map_items1
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder sign1 morphism1 symbol1 raw_symbol1 proof_tree1
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder lid2 sublogics2
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder basic_spec2 sentence2 symb_items2 symb_map_items2
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder sign2 morphism2 symbol2 raw_symbol2 proof_tree2 .
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder lid1 sublogics1 basic_spec1 sentence1
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder symb_items1 symb_map_items1
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder sign1 morphism1 symbol1 raw_symbol1 proof_tree1
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder lid2 sublogics2 basic_spec2 sentence2
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder symb_items2 symb_map_items2
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder sign2 morphism2 symbol2 raw_symbol2 proof_tree2 =>
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maederinstance Eq AnyMorphism where
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder Morphism cid1 == Morphism cid2 =
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder constituents cid1 == constituents cid2
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder -- need to be refined, using morphism translations !!!
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maederinstance Show AnyMorphism where
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder show (Morphism cid) = language_name cid
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder ++ " : " ++ language_name (morSourceLogic cid)
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder ++ " -> " ++ language_name (morTargetLogic cid)