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