Morphism.hs revision 568da6120906d5283c4322114eee10f24ea8dd6d
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
8a77240a809197c92c0736c431b4b88947a7bac1Christian MaederModule : $Header$
6ea54752d184beb92c92fbae17ae9f7dd065d988Christian MaederDescription : morphisms implementation
306763c67bb99228487345b32ab8c5c6cd41f23cChristian MaederCopyright : (c) Christian Maeder and Uni Bremen 2002-2006
3a6c7a7ff823616f56cd3d205fc44664a683effdChristian MaederLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuMaintainer : Christian.Maeder@dfki.de
2eeec5240b424984e3ee26296da1eeab6c6d739eChristian MaederStability : provisional
306763c67bb99228487345b32ab8c5c6cd41f23cChristian MaederPortability : portable
f3a94a197960e548ecd6520bb768cb0d547457bbChristian Maedermapping entities of morphisms
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maederimport Common.Utils (composeMap)
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maederimport Common.Lib.Rel (setToMap)
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maederimport qualified Data.Set as Set
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maederimport qualified Data.Map as Map
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
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder if Set.null d then return () else
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski (sep [ text "overlapping identifiers for types and classes:"
19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder-- | map a kind along an identifier map
9f87aabedf02d74917d94fe1ac0300e07d3d4bc2Christian MaedermapKindI :: IdMap -> Kind -> Kind
9f87aabedf02d74917d94fe1ac0300e07d3d4bc2Christian MaedermapKindI jm = mapKind (\ a -> Map.findWithDefault a a jm)
24a0fbb77b860bc28d25be37ba555fd5746cb6d6Christian Maeder-- | map a kind along a signature morphism (variance is preserved)
27166b063721ef1a2efd8f00ab3d9bc820b315fbChristian MaedermapKinds :: Morphism -> Kind -> Kind
27166b063721ef1a2efd8f00ab3d9bc820b315fbChristian MaedermapKinds = mapKindI . classIdMap
1a38107941725211e7c3f051f7a8f5e12199f03acmaeder-- | only rename the kinds in a type
27166b063721ef1a2efd8f00ab3d9bc820b315fbChristian MaedermapKindsOfType :: IdMap -> TypeMap -> IdMap -> Type -> Type
63324a97283728a30932828a612c7b0b0f687624Christian MaedermapKindsOfType jm tm im = foldType mapTypeRec
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski { foldTypeAbs = \ _ a t p -> TypeAbs (mapTypeArg jm tm im a) t p
59fa9b1349ae1e001d996da732c4ac805c2938e2Christian Maeder , foldKindedType = \ _ t ks p -> KindedType t
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski (Set.map (mapKindI jm) ks) p }
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski-- | map type, expand it, and also adjust the kinds
e9249d3ecd51a2b6a966a58669953e58d703adc6Till MossakowskimapTypeE :: IdMap -> TypeMap -> IdMap -> Type -> Type
53310804002cd9e3c9c5844db3b984abcf001788Christian MaedermapTypeE 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
e9249d3ecd51a2b6a966a58669953e58d703adc6Till MossakowskimapVarKind jm tm im vk = case vk of
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski VarKind k -> VarKind $ mapKindI jm k
3a87487c048b275c56e502c4a933273788e8d0bbChristian Maeder Downset ty -> Downset $ mapTypeE jm tm im ty
2b565fe5cfb9f99857fd25b52304758d8544e266Mihai CodescumapTypeArg :: IdMap -> TypeMap -> IdMap -> TypeArg -> TypeArg
e9249d3ecd51a2b6a966a58669953e58d703adc6Till MossakowskimapTypeArg jm tm im (TypeArg i v vk rk c s r) =
b5056cf24da461ee868c4be7b803a76b677fa21dChristian Maeder TypeArg i v (mapVarKind jm tm im vk) rk c s r
4184cb191a9081cb2a9cf3ef5f060f56f0ca5922Till MossakowskimapTypeScheme :: IdMap -> TypeMap -> IdMap -> TypeScheme -> TypeScheme
8731f7b93b26083dc34a2c0937cd6493b42f2c2cTill MossakowskimapTypeScheme jm tm im (TypeScheme args ty ps) =
d97cb7d1c9beadc4d9102738da0a88c4efcf8fddChristian Maeder TypeScheme (map (mapTypeArg jm tm im) args) (mapTypeE jm tm im ty) ps
24a0fbb77b860bc28d25be37ba555fd5746cb6d6Christian MaedermapSen :: IdMap -> TypeMap -> IdMap -> FunMap -> Term -> Term
4184cb191a9081cb2a9cf3ef5f060f56f0ca5922Till MossakowskimapSen jm tm im fm = mapTerm (mapFunSym jm tm im fm, mapTypeE jm tm im)
b5056cf24da461ee868c4be7b803a76b677fa21dChristian MaedergetDatatypeIds :: DataEntry -> Set.Set Id
bba825b39570777866d560bfde3807731131097eKlaus LuettichgetDatatypeIds (DataEntry _ i _ _ _ alts) =
d97cb7d1c9beadc4d9102738da0a88c4efcf8fddChristian Maeder let getAltIds (Construct _ tys _ sels) = Set.union
b5056cf24da461ee868c4be7b803a76b677fa21dChristian Maeder (Set.unions $ map getTypeIds tys)
b5056cf24da461ee868c4be7b803a76b677fa21dChristian Maeder $ Set.unions $ concatMap (map getSelIds) sels
b5056cf24da461ee868c4be7b803a76b677fa21dChristian Maeder getSelIds (Select _ ty _) = getTypeIds ty
b5056cf24da461ee868c4be7b803a76b677fa21dChristian Maeder getTypeIds = idsOf (== 0)
fd496ec12c6be2731410ea84111f1ff88d8b6384Christian Maeder in Set.insert i $ Set.unions $ map getAltIds $ Set.toList alts
f23641ce10de2d58493d41a4b39c64d904e5b534Christian MaedermapDataEntry :: IdMap -> TypeMap -> IdMap -> FunMap -> DataEntry
f23641ce10de2d58493d41a4b39c64d904e5b534Christian MaedermapDataEntry jm tm im fm de@(DataEntry dm i k args rk alts) =
f23641ce10de2d58493d41a4b39c64d904e5b534Christian Maeder let tim = composeMap (setToMap $ getDatatypeIds de) dm im
f23641ce10de2d58493d41a4b39c64d904e5b534Christian Maeder newargs = map (mapTypeArg jm tm im) args
f23641ce10de2d58493d41a4b39c64d904e5b534Christian Maeder in DataEntry tim i k newargs rk $ Set.map
a89e661aad28f1b39f4fc9f9f9a4d46074234123Christian Maeder (mapAlt jm tm tim fm newargs
3d86f079b07a6a058cdd6c112d287e01a69d9c0cChristian Maeder $ patToType (Map.findWithDefault i i tim) newargs rk) alts
b5056cf24da461ee868c4be7b803a76b677fa21dChristian MaedermapAlt :: IdMap -> TypeMap -> IdMap -> FunMap -> [TypeArg] -> Type -> AltDefn
b5056cf24da461ee868c4be7b803a76b677fa21dChristian MaedermapAlt jm tm im fm args dt (Construct mi ts p sels) =
b60a22e76e983e8129c5dae4d713fe2794ed7054Christian Maeder let newTs = map (mapTypeE jm tm im) ts in case mi of
83b3260413a3b1b7dee1f9c4d3249dec994a875cMihai Codescu Just i -> let
b60a22e76e983e8129c5dae4d713fe2794ed7054Christian Maeder sc = TypeScheme args (getFunType dt p newTs) nullRange
a975722baf6fee1ca3e67df170c732c4abd0a945Christian Maeder (j, TypeScheme _ ty _) = mapFunSym jm tm im fm (i, sc)
a975722baf6fee1ca3e67df170c732c4abd0a945Christian Maeder in Construct (Just j) newTs (getPartiality newTs ty)
a975722baf6fee1ca3e67df170c732c4abd0a945Christian Maeder $ map (map (mapSel jm tm im fm args dt)) sels
a975722baf6fee1ca3e67df170c732c4abd0a945Christian Maeder Nothing -> Construct mi newTs p sels
fd496ec12c6be2731410ea84111f1ff88d8b6384Christian MaedermapSel :: IdMap -> TypeMap -> IdMap -> FunMap -> [TypeArg] -> Type -> Selector
b5056cf24da461ee868c4be7b803a76b677fa21dChristian MaedermapSel jm tm im fm args dt (Select mid t p) =
b5056cf24da461ee868c4be7b803a76b677fa21dChristian Maeder let newT = mapTypeE jm tm im t in case mid of
b5056cf24da461ee868c4be7b803a76b677fa21dChristian Maeder Nothing -> Select mid newT p
b5056cf24da461ee868c4be7b803a76b677fa21dChristian Maeder Just i -> let
b5056cf24da461ee868c4be7b803a76b677fa21dChristian Maeder sc = TypeScheme args (getSelType dt p newT) nullRange
f2c050360525df494e6115073b0edc4c443a847cMihai Codescu (j, TypeScheme _ ty _) = mapFunSym jm tm im fm (i, sc)
b60a22e76e983e8129c5dae4d713fe2794ed7054Christian Maeder in Select (Just j) newT $ getPartiality [dt] ty
b60a22e76e983e8129c5dae4d713fe2794ed7054Christian Maeder-- | get the partiality from a constructor type
f2c050360525df494e6115073b0edc4c443a847cMihai Codescu-- with a given number of curried arguments
0e51a998b1b213654c7a9eca451562041971f100Till MossakowskigetPartiality :: [a] -> Type -> Partiality
0e51a998b1b213654c7a9eca451562041971f100Till MossakowskigetPartiality args t = case getTypeAppl t of
b60a22e76e983e8129c5dae4d713fe2794ed7054Christian Maeder (TypeName i _ _, [_, res]) | isArrow i -> case args of
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski [_] -> if isPartialArrow i then Partial else Total
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder _ : rs -> getPartiality rs res
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder (TypeName i _ _, [_]) | i == lazyTypeId ->
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder if null args then Partial else error "getPartiality"
5c358300e78157f4bfaf5415c70e1096a9205b61Christian MaedermapSentence :: Morphism -> Sentence -> Result Sentence
27166b063721ef1a2efd8f00ab3d9bc820b315fbChristian MaedermapSentence m s = let
27166b063721ef1a2efd8f00ab3d9bc820b315fbChristian Maeder tm = filterAliases . typeMap $ mtarget m
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder im = typeIdMap m
f23641ce10de2d58493d41a4b39c64d904e5b534Christian Maeder jm = classIdMap m
19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder fm = funMap m
19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder f = mapFunSym jm tm im fm
19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder in return $ case s of
19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder Formula t -> Formula $ mapSen jm tm im fm t
19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder DatatypeSen td -> DatatypeSen $ map (mapDataEntry jm tm im fm) td
fd496ec12c6be2731410ea84111f1ff88d8b6384Christian Maeder ProgEqSen i sc pe ->
fd496ec12c6be2731410ea84111f1ff88d8b6384Christian Maeder let (ni, nsc) = f (i, sc)
19298cbfd6ee2abd904f3181af7760b965b822c3Christian 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
4c7f058cdd19ce67b2b5d4b7f69703d0f8a21e38Christian MaederideMor e = mkMorphism e e
5c358300e78157f4bfaf5415c70e1096a9205b61Christian MaedercompMor :: Morphism -> Morphism -> Result Morphism
5c358300e78157f4bfaf5415c70e1096a9205b61Christian MaedercompMor m1 m2 =
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder let tm1 = typeIdMap m1
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder tm2 = typeIdMap m2
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder ctm = composeMap (typeMap src) tm1 tm2
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder cm1 = classIdMap m1
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder cm2 = classIdMap m2
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder ccm = composeMap (classMap src) cm1 cm2
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder fm2 = funMap m2
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder fm1 = funMap m1
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder tar = mtarget m2
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder src = msource m1
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder tm = filterAliases $ typeMap tar
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder emb = mkMorphism src tar
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder in if isInclMor m1 && isInclMor m2 then return emb else do
83b3260413a3b1b7dee1f9c4d3249dec994a875cMihai Codescu disjointKeys ctm ccm
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder { typeIdMap = ctm
f23641ce10de2d58493d41a4b39c64d904e5b534Christian Maeder , classIdMap = ccm
b1f59a4ea7c96f4c03a4d7cfcb9c5e66871cfbbbChristian Maeder , funMap = Map.intersection (if Map.null fm2 then fm1 else
6ea54752d184beb92c92fbae17ae9f7dd065d988Christian Maeder let p3 = mapFunSym ccm tm tm2 fm2 p2 in
6ea54752d184beb92c92fbae17ae9f7dd065d988Christian Maeder if p1 == p3 then Map.delete p1 else Map.insert p1 p3)
6ea54752d184beb92c92fbae17ae9f7dd065d988Christian Maeder concatMap ( \ (k, os) ->
6ea54752d184beb92c92fbae17ae9f7dd065d988Christian Maeder map ( \ o -> ((k, mapTypeScheme ccm tm ctm
fd496ec12c6be2731410ea84111f1ff88d8b6384Christian Maeder $ opType o), ())) $ Set.toList os)
f23641ce10de2d58493d41a4b39c64d904e5b534Christian Maeder $ Map.toList $ assumps src }
fd496ec12c6be2731410ea84111f1ff88d8b6384Christian MaedershowEnvDiff :: Env -> Env -> String
fd496ec12c6be2731410ea84111f1ff88d8b6384Christian MaedershowEnvDiff e1 e2 =
255f43c567972176c2078e3de2fb7a2798bcfde0Christian Maeder "Signature 1:\n" ++ showDoc e1 "\nSignature 2:\n"
9f87aabedf02d74917d94fe1ac0300e07d3d4bc2Christian Maeder ++ showDoc e2 "\nDifference\n" ++ showDoc
8c7aa750542dcadb94b971be712564a9a8f1d189Christian Maeder (diffEnv e1 e2) ""
9f87aabedf02d74917d94fe1ac0300e07d3d4bc2Christian MaederlegalEnv :: Env -> Bool
9f87aabedf02d74917d94fe1ac0300e07d3d4bc2Christian MaederlegalEnv _ = True -- maybe a closure test?
27166b063721ef1a2efd8f00ab3d9bc820b315fbChristian MaederlegalMor :: Morphism -> Bool
fd496ec12c6be2731410ea84111f1ff88d8b6384Christian MaederlegalMor m = let
27166b063721ef1a2efd8f00ab3d9bc820b315fbChristian Maeder s = msource m
27166b063721ef1a2efd8f00ab3d9bc820b315fbChristian Maeder t = mtarget m
6ea54752d184beb92c92fbae17ae9f7dd065d988Christian Maeder ts = typeIdMap m
4ef5e33657aae95850b7e6941f67ac1fb73cd13fChristian Maeder cs = classIdMap m
6ea54752d184beb92c92fbae17ae9f7dd065d988Christian Maeder fs = funMap m in
4ef5e33657aae95850b7e6941f67ac1fb73cd13fChristian Maeder all (`elem` Map.keys (typeMap s)) (Map.keys ts)
6ea54752d184beb92c92fbae17ae9f7dd065d988Christian Maeder && all (`elem` Map.keys (typeMap t)) (Map.elems ts)
27166b063721ef1a2efd8f00ab3d9bc820b315fbChristian Maeder && all (`elem` Map.keys (classMap s)) (Map.keys cs)
6ea54752d184beb92c92fbae17ae9f7dd065d988Christian Maeder && all (`elem` Map.keys (classMap t)) (Map.elems cs)
b5056cf24da461ee868c4be7b803a76b677fa21dChristian Maeder && all ((`elem` Map.keys (assumps s)) . fst) (Map.keys fs)
53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder && all ((`elem` Map.keys (assumps t)) . fst) (Map.elems fs)
19298cbfd6ee2abd904f3181af7760b965b822c3Christian MaedermorphismUnion :: Morphism -> Morphism -> Result Morphism
fd496ec12c6be2731410ea84111f1ff88d8b6384Christian MaedermorphismUnion m1 m2 = do
fd496ec12c6be2731410ea84111f1ff88d8b6384Christian Maeder let s1 = msource m1
f23641ce10de2d58493d41a4b39c64d904e5b534Christian Maeder s2 = msource m2
f23641ce10de2d58493d41a4b39c64d904e5b534Christian Maeder s <- merge s1 s2
f23641ce10de2d58493d41a4b39c64d904e5b534Christian Maeder t <- merge (mtarget m1) $ mtarget m2
19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder let tm1 = typeMap s1
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder tm2 = typeMap s2
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder im1 = typeIdMap m1
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder im2 = typeIdMap m2
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder -- unchanged types
eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettich ima1 = Map.union im1 $ setToMap ut1
eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettich ima2 = Map.union im2 $ setToMap ut2
eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettich sAs = filterAliases $ typeMap s
eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettich tAs = filterAliases $ typeMap t
6ca6ffc92f5c0058ae4b92d46e4e8cbc7beb11fcMihai Codescu cm1 = classMap s1
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder cm2 = classMap s2
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder jm1 = classIdMap m1
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder jm2 = classIdMap m2
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder -- unchanged classes
eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettich cut1 = Map.keysSet cm1 Set.\\ Map.keysSet jm1
eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettich cut2 = Map.keysSet cm2 Set.\\ Map.keysSet jm2
eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettich cima1 = Map.union jm1 $ setToMap cut1
eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettich cima2 = Map.union jm2 $ setToMap cut2
eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettich expP = Map.fromList . map ( \ ((i, o), (j, p)) ->
eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettich ((i, expand tAs o), (j, expand tAs p)))
eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettich fm1 = expP $ funMap m1
eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettich fm2 = expP $ funMap m2
da955132262baab309a50fdffe228c9efe68251dCui Jian af jm im = Set.unions . map ( \ (i, os) ->
27166b063721ef1a2efd8f00ab3d9bc820b315fbChristian Maeder Set.map ( \ o -> (i, mapTypeScheme jm tAs im
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder $ expand sAs $ opType o)) os)
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder -- unchanged functions
fd496ec12c6be2731410ea84111f1ff88d8b6384Christian Maeder uf1 = af jm1 im1 (assumps s1) Set.\\ Map.keysSet fm1
eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettich uf2 = af jm2 im2 (assumps s2) Set.\\ Map.keysSet fm2
eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettich fma1 = Map.union fm1 $ setToMap uf1
3946c010d94321f14139e12061dd4261a3cc7295Christian Maeder fma2 = Map.union fm2 $ setToMap uf2
3946c010d94321f14139e12061dd4261a3cc7295Christian Maeder showFun (i, ty) = showId i . (" : " ++) . showDoc ty
3946c010d94321f14139e12061dd4261a3cc7295Christian Maeder tma <- mergeMap ( \ t1 t2 -> if t1 == t2 then return t1 else
3946c010d94321f14139e12061dd4261a3cc7295Christian Maeder fail $ "incompatible type mapping to `"
3946c010d94321f14139e12061dd4261a3cc7295Christian Maeder ++ showId t1 "' and '" ++ showId t2 "'") ima1 ima2
3946c010d94321f14139e12061dd4261a3cc7295Christian Maeder cma <- mergeMap ( \ t1 t2 -> if t1 == t2 then return t1 else
3946c010d94321f14139e12061dd4261a3cc7295Christian Maeder fail $ "incompatible class mapping to `"
27166b063721ef1a2efd8f00ab3d9bc820b315fbChristian Maeder ++ showId t1 "' and '" ++ showId t2 "'") cima1 cima2
27166b063721ef1a2efd8f00ab3d9bc820b315fbChristian Maeder fma <- mergeMap ( \ o1 o2 -> if o1 == o2 then return o1 else
27166b063721ef1a2efd8f00ab3d9bc820b315fbChristian Maeder fail $ "incompatible mapping to '"
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski ++ showFun o1 "' and '" ++ showFun o2 "'") fma1 fma2
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski disjointKeys tma cma
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski return (mkMorphism s t)
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski { typeIdMap = tma
6ca6ffc92f5c0058ae4b92d46e4e8cbc7beb11fcMihai Codescu , classIdMap = cma
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski , funMap = fma }
e9249d3ecd51a2b6a966a58669953e58d703adc6Till MossakowskimorphismToSymbMap :: Morphism -> SymbolMap
e9249d3ecd51a2b6a966a58669953e58d703adc6Till MossakowskimorphismToSymbMap mor = let
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski src = msource mor
53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder tar = mtarget mor
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski im = typeIdMap mor
eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettich jm = classIdMap mor
eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettich tm = filterAliases $ typeMap tar
eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettich classSymMap = Map.foldWithKey ( \ i ti ->
3fb8a83c3c06671ee94fd12a1782b14563d09df1Christian Maeder k = rawKind ti
3fb8a83c3c06671ee94fd12a1782b14563d09df1Christian Maeder in Map.insert (idToClassSymbol src i k)
eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettich $ idToClassSymbol tar j k) Map.empty $ classMap src
19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder typeSymMap = Map.foldWithKey ( \ i ti ->
27166b063721ef1a2efd8f00ab3d9bc820b315fbChristian Maeder k = typeKind ti
83b3260413a3b1b7dee1f9c4d3249dec994a875cMihai Codescu in Map.insert (idToTypeSymbol src i k)
da955132262baab309a50fdffe228c9efe68251dCui Jian $ idToTypeSymbol tar j k) classSymMap $ typeMap src
da955132262baab309a50fdffe228c9efe68251dCui Jian ( \ i s m ->
da955132262baab309a50fdffe228c9efe68251dCui Jian let ty = opType oi
a98fd29a06e80e447af26d898044c23497adbc73Mihai Codescu (j, t2) = mapFunSym jm tm im (funMap mor) (i, ty)
f2c050360525df494e6115073b0edc4c443a847cMihai Codescu in Map.insert (idToOpSymbol src i ty)
f2c050360525df494e6115073b0edc4c443a847cMihai Codescu (idToOpSymbol tar j t2)) m s)
b60a22e76e983e8129c5dae4d713fe2794ed7054Christian Maeder typeSymMap $ assumps src