Cross Reference: /hets/CommonLogic/Morphism.hs
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
{- |
Module : $Header$
Description : Morphism of Common Logic
Copyright : (c) Uni Bremen DFKI 2010
License : GPLv2 or higher, see LICENSE.txt
Maintainer : eugenk@informatik.uni-bremen.de
Stability : experimental
Portability : non-portable (via Logic.Logic)
Morphism of Common Logic
-}
module CommonLogic.Morphism
( Morphism (..)
, pretty -- pretty printing
, idMor -- identity morphism
, isLegalMorphism -- check if morhpism is ok
, composeMor -- composition
, inclusionMap -- inclusion map
, mkMorphism -- create Morphism
, mapSentence -- map of sentences
, applyMap -- application function for maps
, applyMorphism -- application function for morphism
, morphismUnion
) where
import qualified Data.Map as Map
import qualified Data.Set as Set
import qualified Common.Result as Result
import Common.Id as Id
import Common.Result
import Common.Doc
import Common.DocUtils
import CommonLogic.AS_CommonLogic as AS
import CommonLogic.Sign as Sign
-- maps of sets
data Morphism = Morphism
{ source :: Sign
, target :: Sign
, propMap :: Map.Map Id Id
} deriving (Eq, Ord, Show)
instance Pretty Morphism where
pretty = printMorphism
-- | Constructs an id-morphism
idMor :: Sign -> Morphism
idMor a = inclusionMap a a
-- | Determines whether a morphism is valid
isLegalMorphism :: Morphism -> Result ()
isLegalMorphism pmor =
let psource = allItems $ source pmor
ptarget = allItems $ target pmor
pdom = Map.keysSet $ propMap pmor
pcodom = Set.map (applyMorphism pmor) psource
in if Set.isSubsetOf pcodom ptarget && Set.isSubsetOf pdom psource
then return () else fail "illegal CommonLogic morphism"
-- | Application funtion for morphisms
applyMorphism :: Morphism -> Id -> Id
applyMorphism mor idt = Map.findWithDefault idt idt $ propMap mor
-- | Application function for propMaps
applyMap :: Map.Map Id Id -> Id -> Id
applyMap pmap idt = Map.findWithDefault idt idt pmap
-- | Composition of morphisms in propositional Logic
composeMor :: Morphism -> Morphism -> Result Morphism
composeMor f g =
let fSource = source f
gTarget = target g
fMap = propMap f
gMap = propMap g
in return Morphism
{ source = fSource
, target = gTarget
, propMap = if Map.null gMap then fMap else
Set.fold ( \ i -> let j = applyMap gMap (applyMap fMap i) in
if i == j then id else Map.insert i j)
Map.empty $ allItems fSource }
-- | Pretty printing for Morphisms
printMorphism :: Morphism -> Doc
printMorphism m = pretty (source m) <> text "-->" <> pretty (target m)
<> vcat (map ( \ (x, y) -> lparen <> pretty x <> text ","
<> pretty y <> rparen) $ Map.assocs $ propMap m)
-- | Inclusion map of a subsig into a supersig
inclusionMap :: Sign.Sign -> Sign.Sign -> Morphism
inclusionMap s1 s2 = Morphism
{ source = s1
, target = s2
, propMap = Map.empty }
-- | creates a Morphism
mkMorphism :: Sign.Sign -> Sign.Sign -> Map.Map Id Id -> Morphism
mkMorphism s t p =
Morphism { source = s
, target = t
, propMap = p }
-- | sentence (text) translation along signature morphism
-- here just the renaming of formulae
mapSentence :: Morphism -> AS.TEXT_META -> Result.Result AS.TEXT_META
mapSentence mor tm =
return $ tm { getText = mapSen_txt mor $ getText tm }
-- propagates the translation to sentences
mapSen_txt :: Morphism -> AS.TEXT -> AS.TEXT
mapSen_txt mor txt = case txt of
AS.Text phrs r -> AS.Text (map (mapSen_phr mor) phrs) r
AS.Named_text n t r -> AS.Named_text n (mapSen_txt mor t) r
-- propagates the translation to sentences
mapSen_phr :: Morphism -> AS.PHRASE -> AS.PHRASE
mapSen_phr mor phr = case phr of
AS.Module m -> AS.Module $ mapSen_mod mor m
AS.Sentence s -> AS.Sentence $ mapSen_sen mor s
AS.Comment_text c t r -> AS.Comment_text c (mapSen_txt mor t) r
x -> x
-- propagates the translation to sentences
mapSen_mod :: Morphism -> AS.MODULE -> AS.MODULE
mapSen_mod mor m = case m of
AS.Mod n t rn -> AS.Mod n (mapSen_txt mor t) rn
AS.Mod_ex n exs t rn -> AS.Mod_ex n exs (mapSen_txt mor t) rn
mapSen_sen :: Morphism -> AS.SENTENCE -> AS.SENTENCE
mapSen_sen mor frm = case frm of
AS.Quant_sent q vs is rn ->
AS.Quant_sent q (map (mapSen_nos mor) vs) (mapSen_sen mor is) rn
AS.Bool_sent bs rn -> AS.Bool_sent (case bs of
AS.Junction j sens -> AS.Junction j (map (mapSen_sen mor) sens)
AS.Negation sen -> AS.Negation (mapSen_sen mor sen)
AS.BinOp op s1 s2 ->
AS.BinOp op (mapSen_sen mor s1) (mapSen_sen mor s2)
) rn
AS.Atom_sent atom rn -> AS.Atom_sent (case atom of
AS.Equation t1 t2 -> AS.Equation (mapSen_trm mor t1) (mapSen_trm mor t2)
AS.Atom t tss -> AS.Atom (mapSen_trm mor t) (map (mapSen_trmSeq mor) tss)
) rn
AS.Comment_sent cm sen rn -> AS.Comment_sent cm (mapSen_sen mor sen) rn
AS.Irregular_sent sen rn -> AS.Irregular_sent (mapSen_sen mor sen) rn
mapSen_trm :: Morphism -> AS.TERM -> AS.TERM
mapSen_trm mor trm = case trm of
AS.Name_term n -> AS.Name_term (mapSen_tok mor n)
AS.Funct_term t ts rn ->
AS.Funct_term (mapSen_trm mor t) (map (mapSen_trmSeq mor) ts) rn
AS.Comment_term t c rn -> AS.Comment_term (mapSen_trm mor t) c rn
AS.That_term s rn -> AS.That_term (mapSen_sen mor s) rn
mapSen_nos :: Morphism -> AS.NAME_OR_SEQMARK -> AS.NAME_OR_SEQMARK
mapSen_nos mor nos = case nos of
AS.Name n -> AS.Name (mapSen_tok mor n)
AS.SeqMark s -> AS.SeqMark (mapSen_tok mor s)
mapSen_trmSeq :: Morphism -> AS.TERM_SEQ -> AS.TERM_SEQ
mapSen_trmSeq mor ts = case ts of
AS.Term_seq t -> AS.Term_seq (mapSen_trm mor t)
AS.Seq_marks s -> AS.Seq_marks (mapSen_tok mor s)
mapSen_tok :: Morphism -> Id.Token -> Id.Token
mapSen_tok mor tok = Id.idToSimpleId $ applyMorphism mor $ Id.simpleIdToId tok
-- | Union of two morphisms.
morphismUnion :: Morphism -> Morphism -> Result.Result Morphism
morphismUnion mor1 mor2 =
let pmap1 = propMap mor1
pmap2 = propMap mor2
p1 = source mor1
p2 = source mor2
up1 = Set.difference (allItems p1) $ Map.keysSet pmap1
up2 = Set.difference (allItems p2) $ Map.keysSet pmap2
(pds, pmap) = foldr ( \ (i, j) (ds, m) -> case Map.lookup i m of
Nothing -> (ds, Map.insert i j m)
Just k -> if j == k then (ds, m) else
(Diag Error
("incompatible mapping of prop " ++ showId i " to "
++ showId j " and " ++ showId k "")
nullRange : ds, m))
([], pmap1)
(Map.toList pmap2 ++ map (\ a -> (a, a))
(Set.toList $ Set.union up1 up2))
in if null pds then return Morphism
{ source = unite p1 p2
, target = unite (target mor1) $ target mor2
, propMap = pmap } else Result pds Nothing