Morphism.hs revision ea570f40967ef8bc16b76c54f9b867a8036cc750
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
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian MaederModule : $Header$
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian MaederDescription : Morphism of Common Logic
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian MaederCopyright : (c) Uni Bremen DFKI 2010
98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuLicense : GPLv2 or higher, see LICENSE.txt
a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen KuksaMaintainer : eugenk@informatik.uni-bremen.de
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian MaederStability : experimental
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian MaederPortability : non-portable (via Logic.Logic)
75067b1beba1380cde707c30e7fc050d86f6927fKarl LucMorphism of Common Logic
7b1111ca3b126f71cce47e60ce4b56e6f92422e9Karl Luc ( Morphism (..)
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder , pretty -- pretty printing
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder , idMor -- identity morphism
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder , isLegalMorphism -- check if morhpism is ok
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder , composeMor -- composition
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder , inclusionMap -- inclusion map
e036e115761fe7c09c210c337440a1864d794093Martha Rohte , mkMorphism -- create Morphism
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder , mapSentence -- map of sentences
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder , applyMap -- application function for maps
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder , applyMorphism -- application function for morphism
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder , morphismUnion
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maederimport qualified Data.Map as Map
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maederimport qualified Data.Set as Set
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maederimport qualified Common.Result as Result
7b1111ca3b126f71cce47e60ce4b56e6f92422e9Karl Luc-- maps of sets
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maederdata Morphism = Morphism
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder { source :: Sign
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder , target :: Sign
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder , propMap :: Map.Map Id Id
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder } deriving (Eq, Ord, Show)
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maederinstance Pretty Morphism where
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder pretty = printMorphism
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder-- | Constructs an id-morphism
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian MaederidMor :: Sign -> Morphism
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian MaederidMor a = inclusionMap a a
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder-- | Determines whether a morphism is valid
656f17ae9b7610ff2de1b6eedeeadea0c3bcdc8dChristian MaederisLegalMorphism :: Morphism -> Result ()
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian MaederisLegalMorphism pmor =
a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen Kuksa let psource = allItems $ source pmor
a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen Kuksa ptarget = allItems $ target pmor
7b1111ca3b126f71cce47e60ce4b56e6f92422e9Karl Luc pdom = Map.keysSet $ propMap pmor
7b1111ca3b126f71cce47e60ce4b56e6f92422e9Karl Luc pcodom = Set.map (applyMorphism pmor) psource
656f17ae9b7610ff2de1b6eedeeadea0c3bcdc8dChristian Maeder in if Set.isSubsetOf pcodom ptarget && Set.isSubsetOf pdom psource
656f17ae9b7610ff2de1b6eedeeadea0c3bcdc8dChristian Maeder then return () else fail "illegal CommonLogic morphism"
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder-- | Application funtion for morphisms
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian MaederapplyMorphism :: Morphism -> Id -> Id
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian MaederapplyMorphism mor idt = Map.findWithDefault idt idt $ propMap mor
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder-- | Application function for propMaps
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian MaederapplyMap :: Map.Map Id Id -> Id -> Id
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian MaederapplyMap pmap idt = Map.findWithDefault idt idt pmap
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder-- | Composition of morphisms in propositional Logic
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian MaedercomposeMor :: Morphism -> Morphism -> Result Morphism
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian MaedercomposeMor f g =
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder let fSource = source f
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder gTarget = target g
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder fMap = propMap f
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder gMap = propMap g
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder in return Morphism
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder { source = fSource
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder , target = gTarget
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder , propMap = if Map.null gMap then fMap else
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder Set.fold ( \ i -> let j = applyMap gMap (applyMap fMap i) in
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder if i == j then id else Map.insert i j)
a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen Kuksa Map.empty $ allItems fSource }
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder-- | Pretty printing for Morphisms
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian MaederprintMorphism :: Morphism -> Doc
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian MaederprintMorphism m = pretty (source m) <> text "-->" <> pretty (target m)
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder <> vcat (map ( \ (x, y) -> lparen <> pretty x <> text ","
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder <> pretty y <> rparen) $ Map.assocs $ propMap m)
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder-- | Inclusion map of a subsig into a supersig
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian MaederinclusionMap :: Sign.Sign -> Sign.Sign -> Morphism
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian MaederinclusionMap s1 s2 = Morphism
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder { source = s1
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder , target = s2
e9e5281899ddaec4778ad14c64800975377630ecChristian Maeder-- | creates a Morphism
e036e115761fe7c09c210c337440a1864d794093Martha RohtemkMorphism :: Sign.Sign -> Sign.Sign -> Map.Map Id Id -> Morphism
e9e5281899ddaec4778ad14c64800975377630ecChristian MaedermkMorphism s t p =
e9e5281899ddaec4778ad14c64800975377630ecChristian Maeder Morphism { source = s
e9e5281899ddaec4778ad14c64800975377630ecChristian Maeder , propMap = p }
2c10bceb28a74fc291959697e023f22a66753655Eugen Kuksa-- | sentence (text) translation along signature morphism
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder-- here just the renaming of formulae
a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen KuksamapSentence :: Morphism -> AS.TEXT_META -> Result.Result AS.TEXT_META
a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen KuksamapSentence mor tm =
a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen Kuksa return $ tm { getText = mapSen_txt mor $ getText tm }
2c10bceb28a74fc291959697e023f22a66753655Eugen Kuksa-- propagates the translation to sentences
a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen KuksamapSen_txt mor txt = case txt of
a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen Kuksa AS.Text phrs r -> AS.Text (map (mapSen_phr mor) phrs) r
a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen Kuksa AS.Named_text n t r -> AS.Named_text n (mapSen_txt mor t) r
2c10bceb28a74fc291959697e023f22a66753655Eugen Kuksa-- propagates the translation to sentences
a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen KuksamapSen_phr mor phr = case phr of
a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen Kuksa AS.Comment_text c t r -> AS.Comment_text c (mapSen_txt mor t) r
2c10bceb28a74fc291959697e023f22a66753655Eugen Kuksa-- propagates the translation to sentences
a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen KuksamapSen_mod mor m = case m of
a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen Kuksa AS.Mod_ex n exs t rn -> AS.Mod_ex n exs (mapSen_txt mor t) rn
a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen KuksamapSen_sen :: Morphism -> AS.SENTENCE -> AS.SENTENCE
a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen KuksamapSen_sen mor frm = case frm of
ea570f40967ef8bc16b76c54f9b867a8036cc750Soeren D. Schulze AS.Quant_sent q (map (mapSen_nos mor) vs) (mapSen_sen mor is) rn
d2d5606ab65ddf48599bd044416de07a205095f2Soeren D. Schulze AS.Junction j sens -> AS.Junction j (map (mapSen_sen mor) sens)
a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen Kuksa AS.Negation sen -> AS.Negation (mapSen_sen mor sen)
d2d5606ab65ddf48599bd044416de07a205095f2Soeren D. Schulze AS.BinOp op (mapSen_sen mor s1) (mapSen_sen mor s2)
a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen Kuksa AS.Atom_sent atom rn -> AS.Atom_sent (case atom of
a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen Kuksa AS.Equation t1 t2 -> AS.Equation (mapSen_trm mor t1) (mapSen_trm mor t2)
a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen Kuksa AS.Atom t tss -> AS.Atom (mapSen_trm mor t) (map (mapSen_trmSeq mor) tss)
a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen Kuksa AS.Comment_sent cm sen rn -> AS.Comment_sent cm (mapSen_sen mor sen) rn
a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen Kuksa AS.Irregular_sent sen rn -> AS.Irregular_sent (mapSen_sen mor sen) rn
a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen KuksamapSen_trm mor trm = case trm of
a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen Kuksa AS.Name_term n -> AS.Name_term (mapSen_tok mor n)
a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen Kuksa AS.Funct_term (mapSen_trm mor t) (map (mapSen_trmSeq mor) ts) rn
a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen Kuksa AS.Comment_term t c rn -> AS.Comment_term (mapSen_trm mor t) c rn
f03aa0b723e5545fddf7019e287368b9e208ca69Soeren D. Schulze AS.That_term s rn -> AS.That_term (mapSen_sen mor s) rn
a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen KuksamapSen_nos :: Morphism -> AS.NAME_OR_SEQMARK -> AS.NAME_OR_SEQMARK
a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen KuksamapSen_nos mor nos = case nos of
a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen KuksamapSen_trmSeq :: Morphism -> AS.TERM_SEQ -> AS.TERM_SEQ
a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen KuksamapSen_trmSeq mor ts = case ts of
a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen Kuksa AS.Seq_marks s -> AS.Seq_marks (mapSen_tok mor s)
a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen KuksamapSen_tok mor tok = Id.idToSimpleId $ applyMorphism mor $ Id.simpleIdToId tok
0fe5514fdf12b7559c1a470cf22d89737d55b0a0Eugen Kuksa-- | Union of two morphisms.
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian MaedermorphismUnion :: Morphism -> Morphism -> Result.Result Morphism
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian MaedermorphismUnion mor1 mor2 =
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder let pmap1 = propMap mor1
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder pmap2 = propMap mor2
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder p1 = source mor1
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder p2 = source mor2
a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen Kuksa up1 = Set.difference (allItems p1) $ Map.keysSet pmap1
a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen Kuksa up2 = Set.difference (allItems p2) $ Map.keysSet pmap2
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder (pds, pmap) = foldr ( \ (i, j) (ds, m) -> case Map.lookup i m of
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder Nothing -> (ds, Map.insert i j m)
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder Just k -> if j == k then (ds, m) else
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder ("incompatible mapping of prop " ++ showId i " to "
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder ++ showId j " and " ++ showId k "")
0fe5514fdf12b7559c1a470cf22d89737d55b0a0Eugen Kuksa nullRange : ds, m))
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder (Map.toList pmap2 ++ map (\ a -> (a, a))
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder in if null pds then return Morphism
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder { source = unite p1 p2
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder , target = unite (target mor1) $ target mor2
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder , propMap = pmap } else Result pds Nothing