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
6ea54752d184beb92c92fbae17ae9f7dd065d988Christian MaederModule : $Header$
306763c67bb99228487345b32ab8c5c6cd41f23cChristian MaederDescription : morphisms implementation
3a6c7a7ff823616f56cd3d205fc44664a683effdChristian MaederCopyright : (c) Christian Maeder and Uni Bremen 2002-2006
6ea54752d184beb92c92fbae17ae9f7dd065d988Christian MaederLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
2eeec5240b424984e3ee26296da1eeab6c6d739eChristian MaederMaintainer : Christian.Maeder@dfki.de
306763c67bb99228487345b32ab8c5c6cd41f23cChristian MaederStability : provisional
306763c67bb99228487345b32ab8c5c6cd41f23cChristian MaederPortability : portable
9f87aabedf02d74917d94fe1ac0300e07d3d4bc2Christian Maedermapping entities of morphisms
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maederimport qualified Data.Set as Set
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maederimport qualified Data.Map as Map
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maederinstance Eq Morphism where
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder m1 == m2 = (msource m1, mtarget m1, typeIdMap m1, classIdMap m1, funMap m1)
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder == (msource m2, mtarget m2, typeIdMap m2, classIdMap m2, funMap m2)
556f473448dfcceee22afaa89ed7a364489cdbbbChristian MaederdisjointKeys :: (Ord a, Pretty a, Monad m) => Map.Map a b -> Map.Map a c
556f473448dfcceee22afaa89ed7a364489cdbbbChristian MaederdisjointKeys m1 m2 = let d = Map.keysSet $ Map.intersection m1 m2 in
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder if Set.null d then return () else
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski (sep [ text "overlapping identifiers for types and classes:"
63324a97283728a30932828a612c7b0b0f687624Christian Maeder-- | map a kind along an identifier map
f9e0b18852b238ddb649d341194e05d7200d1bbeChristian MaedermapKindI :: IdMap -> Kind -> Kind
a89e661aad28f1b39f4fc9f9f9a4d46074234123Christian MaedermapKindI jm = mapKind $ (\ a -> Map.findWithDefault a a jm)
19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder-- | map a kind along a signature morphism (variance is preserved)
9f87aabedf02d74917d94fe1ac0300e07d3d4bc2Christian MaedermapKinds :: Morphism -> Kind -> Kind
9f87aabedf02d74917d94fe1ac0300e07d3d4bc2Christian MaedermapKinds mor = mapKindI $ classIdMap mor
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder-- | only rename the kinds in a type
e9249d3ecd51a2b6a966a58669953e58d703adc6Till MossakowskimapKindsOfType :: IdMap -> TypeMap -> IdMap -> Type -> Type
59fa9b1349ae1e001d996da732c4ac805c2938e2Christian MaedermapKindsOfType jm tm im = foldType mapTypeRec
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski { foldTypeAbs = \ _ a t p -> TypeAbs (mapTypeArg jm tm im a) t p
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski , foldKindedType = \ _ t ks p -> KindedType t
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski (Set.map (mapKindI jm) ks) p }
53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder-- | map type, expand it, and also adjust the kinds
e9249d3ecd51a2b6a966a58669953e58d703adc6Till MossakowskimapTypeE :: IdMap -> TypeMap -> IdMap -> Type -> Type
e9249d3ecd51a2b6a966a58669953e58d703adc6Till MossakowskimapTypeE jm tm im =
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski mapKindsOfType jm tm im . expandAliases tm . mapType im
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski-- | map a kind along a signature morphism (variance is preserved)
e9249d3ecd51a2b6a966a58669953e58d703adc6Till MossakowskimapVarKind :: IdMap -> TypeMap -> IdMap -> VarKind -> VarKind
3a87487c048b275c56e502c4a933273788e8d0bbChristian MaedermapVarKind jm tm im vk = case vk of
2b565fe5cfb9f99857fd25b52304758d8544e266Mihai Codescu VarKind k -> VarKind $ mapKindI jm k
2b565fe5cfb9f99857fd25b52304758d8544e266Mihai Codescu Downset ty -> Downset $ mapTypeE jm tm im ty
2ecf6cfb90e84d40f224cda5d92c191182c976d2Till MossakowskimapTypeArg :: IdMap -> TypeMap -> IdMap -> TypeArg -> TypeArg
2ecf6cfb90e84d40f224cda5d92c191182c976d2Till MossakowskimapTypeArg jm tm im (TypeArg i v vk rk c s r) =
4184cb191a9081cb2a9cf3ef5f060f56f0ca5922Till Mossakowski TypeArg i v (mapVarKind jm tm im vk) rk c s r
4184cb191a9081cb2a9cf3ef5f060f56f0ca5922Till MossakowskimapTypeScheme :: IdMap -> TypeMap -> IdMap -> TypeScheme -> TypeScheme
2ecf6cfb90e84d40f224cda5d92c191182c976d2Till MossakowskimapTypeScheme jm tm im (TypeScheme args ty ps) =
bba825b39570777866d560bfde3807731131097eKlaus Luettich TypeScheme (map (mapTypeArg jm tm im) args) (mapTypeE jm tm im ty) ps
53310804002cd9e3c9c5844db3b984abcf001788Christian MaedermapSen :: IdMap -> TypeMap -> IdMap -> FunMap -> Term -> Term
e9249d3ecd51a2b6a966a58669953e58d703adc6Till MossakowskimapSen jm tm im fm = mapTerm (mapFunSym jm tm im fm, mapTypeE jm tm im)
e9249d3ecd51a2b6a966a58669953e58d703adc6Till MossakowskisetToMap :: Ord a => Set.Set a -> Map.Map a a
5d6e7ea3bd14fc987436cff0f542393ea9ba34bbTill MossakowskisetToMap = Map.fromAscList . map ( \ a -> (a, a)) . Set.toList
a89e661aad28f1b39f4fc9f9f9a4d46074234123Christian MaedergetDatatypeIds :: DataEntry -> Set.Set Id
a89e661aad28f1b39f4fc9f9f9a4d46074234123Christian MaedergetDatatypeIds (DataEntry _ i _ _ _ alts) =
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski let getAltIds (Construct _ tys _ sels) = Set.union
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski (Set.unions $ map getTypeIds tys)
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski $ Set.unions $ concatMap (map getSelIds) sels
b60a22e76e983e8129c5dae4d713fe2794ed7054Christian Maeder getSelIds (Select _ ty _) = getTypeIds ty
0647a6c86b231e391826c7715338ba29cb4934c0Christian Maeder getTypeIds = idsOf (== 0)
b60a22e76e983e8129c5dae4d713fe2794ed7054Christian Maeder in Set.insert i $ Set.unions $ map getAltIds $ Set.toList alts
a975722baf6fee1ca3e67df170c732c4abd0a945Christian MaedermapDataEntry :: IdMap -> TypeMap -> IdMap -> FunMap -> DataEntry -> DataEntry
a975722baf6fee1ca3e67df170c732c4abd0a945Christian MaedermapDataEntry jm tm im fm de@(DataEntry dm i k args rk alts) =
a975722baf6fee1ca3e67df170c732c4abd0a945Christian Maeder let tim = Map.intersection (compIdMap dm im) $ setToMap $ getDatatypeIds de
63324a97283728a30932828a612c7b0b0f687624Christian Maeder newargs = map (mapTypeArg jm tm im) args
a98fd29a06e80e447af26d898044c23497adbc73Mihai Codescu in DataEntry tim i k newargs rk $ Set.map
a98fd29a06e80e447af26d898044c23497adbc73Mihai Codescu (mapAlt jm tm tim fm newargs
a98fd29a06e80e447af26d898044c23497adbc73Mihai Codescu $ patToType (Map.findWithDefault i i tim) args rk) alts
830e14495f9cac8e154dd4813dae010166f33d09Mihai CodescumapAlt :: IdMap -> TypeMap -> IdMap -> FunMap -> [TypeArg] -> Type -> AltDefn
a98fd29a06e80e447af26d898044c23497adbc73Mihai CodescumapAlt jm tm im fm args dt c@(Construct mi ts p sels) =
f2c050360525df494e6115073b0edc4c443a847cMihai Codescu let sc = TypeScheme args
b60a22e76e983e8129c5dae4d713fe2794ed7054Christian Maeder (getFunType dt p $ map (mapTypeE jm tm im) ts) nullRange
f2c050360525df494e6115073b0edc4c443a847cMihai Codescu (j, TypeScheme _ ty _) = mapFunSym jm tm im fm (i, sc)
0e51a998b1b213654c7a9eca451562041971f100Till Mossakowski in Construct (Just j) ts (getPartiality ts ty) $
0e51a998b1b213654c7a9eca451562041971f100Till Mossakowski map (map (mapSel jm tm im fm args dt)) sels
e9249d3ecd51a2b6a966a58669953e58d703adc6Till MossakowskimapSel :: IdMap -> TypeMap -> IdMap -> FunMap -> [TypeArg] -> Type -> Selector
5c358300e78157f4bfaf5415c70e1096a9205b61Christian MaedermapSel jm tm im fm args dt s@(Select mid t p) = case mid of
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder Just i -> let
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder sc = TypeScheme args (getSelType dt p $ mapTypeE jm tm im t) nullRange
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder (j, TypeScheme _ ty _) = mapFunSym jm tm im fm (i, sc)
da955132262baab309a50fdffe228c9efe68251dCui Jian in Select (Just j) t $ getPartiality [dt] ty
bba825b39570777866d560bfde3807731131097eKlaus Luettich-- | get the partiality from a constructor type
da955132262baab309a50fdffe228c9efe68251dCui Jian-- with a given number of curried arguments
bba825b39570777866d560bfde3807731131097eKlaus LuettichgetPartiality :: [a] -> Type -> Partiality
5c358300e78157f4bfaf5415c70e1096a9205b61Christian MaedergetPartiality args t = case getTypeAppl t of
9f87aabedf02d74917d94fe1ac0300e07d3d4bc2Christian Maeder (TypeName i _ _, [_, res]) | isArrow i -> case args of
19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder [_] -> if isPartialArrow i then Partial else Total
19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder _ : rs -> getPartiality rs res
19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder (TypeName i _ _, [_]) | i == lazyTypeId ->
19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder if null args then Partial else error "getPartiality"
19298cbfd6ee2abd904f3181af7760b965b822c3Christian MaedermapSentence :: Morphism -> Sentence -> Result Sentence
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian MaedermapSentence m s = let
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder tm = filterAliases $ typeMap $ mtarget m
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder im = typeIdMap m
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder jm = classIdMap m
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder fm = funMap m
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder f = mapFunSym jm tm im fm
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder in return $ case s of
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder Formula t -> Formula $ mapSen jm tm im fm t
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder DatatypeSen td -> DatatypeSen $ map (mapDataEntry jm tm im fm) td
64e1905404e5135e98a26d2ab4150b6764956576Christian Maeder ProgEqSen i sc pe ->
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder let (ni, nsc) = f (i, sc)
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder in ProgEqSen ni nsc $ mapEq (f, mapTypeE jm tm im) pe
5c358300e78157f4bfaf5415c70e1096a9205b61Christian MaedermapFunSym :: IdMap -> TypeMap -> IdMap -> FunMap -> (Id, TypeScheme)
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder -> (Id, TypeScheme)
5c358300e78157f4bfaf5415c70e1096a9205b61Christian MaedermapFunSym jm tm im fm (i, sc) =
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder let msc = mapTypeScheme jm tm im sc
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder in Map.findWithDefault (i, msc) (i, msc) fm
4c7f058cdd19ce67b2b5d4b7f69703d0f8a21e38Christian MaederideMor :: Env -> Morphism
5c358300e78157f4bfaf5415c70e1096a9205b61Christian MaederideMor e = mkMorphism e e
5c358300e78157f4bfaf5415c70e1096a9205b61Christian MaedercompIdMap :: IdMap -> IdMap -> IdMap
5c358300e78157f4bfaf5415c70e1096a9205b61Christian MaedercompIdMap im1 im2 = Map.foldWithKey ( \ i j ->
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder let k = Map.findWithDefault j j im2 in
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder if i == k then id else Map.insert i k) im2 im1
5c358300e78157f4bfaf5415c70e1096a9205b61Christian MaedercompMor :: Morphism -> Morphism -> Result Morphism
5c358300e78157f4bfaf5415c70e1096a9205b61Christian MaedercompMor m1 m2 = if mtarget m1 == msource m2 then
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder let tm1 = typeIdMap m1
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder tm2 = typeIdMap m2
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder im = compIdMap tm1 tm2
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder cm1 = classIdMap m1
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder cm2 = classIdMap m2
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder cm = compIdMap cm1 cm2
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder fm2 = funMap m2
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder fm1 = funMap m1
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder tar = mtarget m2
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder src = msource m1
9f87aabedf02d74917d94fe1ac0300e07d3d4bc2Christian Maeder tm = filterAliases $ typeMap tar
b1f59a4ea7c96f4c03a4d7cfcb9c5e66871cfbbbChristian Maeder ctm = Map.intersection im $ typeMap src
6ea54752d184beb92c92fbae17ae9f7dd065d988Christian Maeder ccm = Map.intersection cm $ classMap src
6ea54752d184beb92c92fbae17ae9f7dd065d988Christian Maeder emb = mkMorphism src tar
6ea54752d184beb92c92fbae17ae9f7dd065d988Christian Maeder in if Map.null tm1 && Map.null tm2 && Map.null cm1 && Map.null cm2
6ea54752d184beb92c92fbae17ae9f7dd065d988Christian Maeder && Map.null fm1 && Map.null fm2 then return emb else do
6ea54752d184beb92c92fbae17ae9f7dd065d988Christian Maeder disjointKeys ctm ccm
6ea54752d184beb92c92fbae17ae9f7dd065d988Christian Maeder { typeIdMap = ctm
b1f59a4ea7c96f4c03a4d7cfcb9c5e66871cfbbbChristian Maeder , classIdMap = ccm
9f87aabedf02d74917d94fe1ac0300e07d3d4bc2Christian Maeder , funMap = Map.intersection (Map.foldWithKey ( \ p1 p2 ->
9f87aabedf02d74917d94fe1ac0300e07d3d4bc2Christian Maeder let p3 = mapFunSym cm tm tm2 fm2 p2 in
9f87aabedf02d74917d94fe1ac0300e07d3d4bc2Christian Maeder if p1 == p3 then id else Map.insert p1 p3)
9f87aabedf02d74917d94fe1ac0300e07d3d4bc2Christian Maeder concatMap ( \ (k, os) ->
6ea54752d184beb92c92fbae17ae9f7dd065d988Christian Maeder map ( \ o -> ((k, mapTypeScheme cm tm im
6ea54752d184beb92c92fbae17ae9f7dd065d988Christian Maeder $ opType o), ())) $ Set.toList os)
6ea54752d184beb92c92fbae17ae9f7dd065d988Christian Maeder $ Map.toList $ assumps src }
4ef5e33657aae95850b7e6941f67ac1fb73cd13fChristian Maeder else fail "intermediate signatures of morphisms do not match"
4ef5e33657aae95850b7e6941f67ac1fb73cd13fChristian MaederinclusionMor :: Env -> Env -> Result Morphism
6ea54752d184beb92c92fbae17ae9f7dd065d988Christian MaederinclusionMor e1 e2 =
4ef5e33657aae95850b7e6941f67ac1fb73cd13fChristian Maeder if isSubEnv e1 e2
9f87aabedf02d74917d94fe1ac0300e07d3d4bc2Christian Maeder then return (mkMorphism e1 e2)
9f87aabedf02d74917d94fe1ac0300e07d3d4bc2Christian Maeder else Result [Diag Error
6ea54752d184beb92c92fbae17ae9f7dd065d988Christian Maeder ("Attempt to construct inclusion between non-subsignatures:\n"
53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder ++ showEnvDiff e1 e2) nullRange] Nothing
19298cbfd6ee2abd904f3181af7760b965b822c3Christian MaedershowEnvDiff :: Env -> Env -> String
53310804002cd9e3c9c5844db3b984abcf001788Christian MaedershowEnvDiff e1 e2 =
19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder "Signature 1:\n" ++ showDoc e1 "\nSignature 2:\n"
19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder ++ showDoc e2 "\nDifference\n" ++ showDoc
19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder (diffEnv e1 e2) ""
53310804002cd9e3c9c5844db3b984abcf001788Christian MaederlegalEnv :: Env -> Bool
19298cbfd6ee2abd904f3181af7760b965b822c3Christian MaederlegalEnv _ = True -- maybe a closure test?
19298cbfd6ee2abd904f3181af7760b965b822c3Christian MaederlegalMor :: Morphism -> Bool
19298cbfd6ee2abd904f3181af7760b965b822c3Christian MaederlegalMor m = let
a129422b14eea673dc481d2553cec108e35e72efChristian Maeder s = msource m
19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder t = mtarget m
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder ts = typeIdMap m
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder cs = classIdMap m
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder fs = funMap m in
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder all (`elem` Map.keys (typeMap s)) (Map.keys ts)
eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettich && all (`elem` Map.keys (typeMap t)) (Map.elems ts)
eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettich && all (`elem` Map.keys (classMap s)) (Map.keys cs)
eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettich && all (`elem` Map.keys (classMap t)) (Map.elems cs)
eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettich && all ((`elem` Map.keys (assumps s)) . fst) (Map.keys fs)
eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettich && all ((`elem` Map.keys (assumps t)) . fst) (Map.elems fs)
556f473448dfcceee22afaa89ed7a364489cdbbbChristian MaedermorphismUnion :: Morphism -> Morphism -> Result Morphism
556f473448dfcceee22afaa89ed7a364489cdbbbChristian MaedermorphismUnion m1 m2 = do
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder let s1 = msource m1
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder s2 = msource m2
eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettich s <- merge s1 s2
eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettich t <- merge (mtarget m1) $ mtarget m2
eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettich let tm1 = typeMap s1
eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettich tm2 = typeMap s2
eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettich im1 = typeIdMap m1
eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettich im2 = typeIdMap m2
da955132262baab309a50fdffe228c9efe68251dCui Jian -- unchanged types
da955132262baab309a50fdffe228c9efe68251dCui Jian ima1 = Map.union im1 $ setToMap ut1
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder ima2 = Map.union im2 $ setToMap ut2
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder sAs = filterAliases $ typeMap s
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder tAs = filterAliases $ typeMap t
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder cm1 = classMap s1
da955132262baab309a50fdffe228c9efe68251dCui Jian cm2 = classMap s2
eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettich jm1 = classIdMap m1
eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettich jm2 = classIdMap m2
797595aad6dfd626bc1c9df52616f1ac4235c669Till Mossakowski -- unchanged classes
797595aad6dfd626bc1c9df52616f1ac4235c669Till Mossakowski cut1 = Map.keysSet cm1 Set.\\ Map.keysSet jm1
797595aad6dfd626bc1c9df52616f1ac4235c669Till Mossakowski cut2 = Map.keysSet cm2 Set.\\ Map.keysSet jm2
eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettich cima1 = Map.union jm1 $ setToMap cut1
53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder cima2 = Map.union jm2 $ setToMap cut2
797595aad6dfd626bc1c9df52616f1ac4235c669Till Mossakowski expP = Map.fromList . map ( \ ((i, o), (j, p)) ->
933baca0720dae81434de384b32a93b47e754d09Christian Maeder ((i, expand tAs o), (j, expand tAs p)))
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski fm1 = expP $ funMap m1
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski fm2 = expP $ funMap m2
eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettich af jm im = Set.unions . map ( \ (i, os) ->
eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettich Set.map ( \ o -> (i, mapTypeScheme jm tAs im
4ef5e33657aae95850b7e6941f67ac1fb73cd13fChristian Maeder $ expand sAs $ opType o)) os)
da955132262baab309a50fdffe228c9efe68251dCui Jian -- unchanged functions
4ef5e33657aae95850b7e6941f67ac1fb73cd13fChristian Maeder uf1 = af jm1 im1 (assumps s1) Set.\\ Map.keysSet fm1
4ef5e33657aae95850b7e6941f67ac1fb73cd13fChristian Maeder uf2 = af jm2 im2 (assumps s2) Set.\\ Map.keysSet fm2
4ef5e33657aae95850b7e6941f67ac1fb73cd13fChristian Maeder fma1 = Map.union fm1 $ setToMap uf1
4ef5e33657aae95850b7e6941f67ac1fb73cd13fChristian Maeder fma2 = Map.union fm2 $ setToMap uf2
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski showFun (i, ty) = showId i . (" : " ++) . showDoc ty
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski tma <- mergeMap ( \ t1 t2 -> if t1 == t2 then return t1 else
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski fail $ "incompatible type mapping to `"
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski ++ showId t1 "' and '" ++ showId t2 "'") ima1 ima2
6ca6ffc92f5c0058ae4b92d46e4e8cbc7beb11fcMihai Codescu cma <- mergeMap ( \ t1 t2 -> if t1 == t2 then return t1 else
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski fail $ "incompatible class mapping to `"
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski ++ showId t1 "' and '" ++ showId t2 "'") cima1 cima2
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski fma <- mergeMap ( \ o1 o2 -> if o1 == o2 then return o1 else
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski fail $ "incompatible mapping to '"
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski ++ showFun o1 "' and '" ++ showFun o2 "'") fma1 fma2
53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder disjointKeys tma cma
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski return (mkMorphism s t)
eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettich { typeIdMap = tma
eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettich , classIdMap = cma
eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettich , funMap = fma }
3fb8a83c3c06671ee94fd12a1782b14563d09df1Christian MaedermorphismToSymbMap :: Morphism -> SymbolMap
3fb8a83c3c06671ee94fd12a1782b14563d09df1Christian MaedermorphismToSymbMap mor = let
eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettich src = msource mor
19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder tar = mtarget mor
a89e661aad28f1b39f4fc9f9f9a4d46074234123Christian Maeder im = typeIdMap mor
a89e661aad28f1b39f4fc9f9f9a4d46074234123Christian Maeder jm = classIdMap mor
88ece6e49930670e8fd3ee79c89a2e918d2fbd0cChristian Maeder tm = filterAliases $ typeMap tar
da955132262baab309a50fdffe228c9efe68251dCui Jian classSymMap = Map.foldWithKey ( \ i ti ->
da955132262baab309a50fdffe228c9efe68251dCui Jian k = rawKind ti
eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettich in Map.insert (idToClassSymbol src i k)
da955132262baab309a50fdffe228c9efe68251dCui Jian $ idToClassSymbol tar j k) Map.empty $ classMap src
a98fd29a06e80e447af26d898044c23497adbc73Mihai Codescu typeSymMap = Map.foldWithKey ( \ i ti ->
f2c050360525df494e6115073b0edc4c443a847cMihai Codescu k = typeKind ti
b60a22e76e983e8129c5dae4d713fe2794ed7054Christian Maeder in Map.insert (idToTypeSymbol src i k)
da955132262baab309a50fdffe228c9efe68251dCui Jian $ idToTypeSymbol tar j k) classSymMap $ typeMap src
d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder let ty = opType oi
53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder (j, t2) = mapFunSym jm tm im (funMap mor) (i, ty)
4ef5e33657aae95850b7e6941f67ac1fb73cd13fChristian Maeder in Map.insert (idToOpSymbol src i ty)
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski (idToOpSymbol tar j t2)) m s)
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski typeSymMap $ assumps src