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
2e0e43889f746e31eacf8eeccdeaa4032a65b07eMihai Codescu{- |
2e0e43889f746e31eacf8eeccdeaa4032a65b07eMihai CodescuModule      :  $Header$
2e0e43889f746e31eacf8eeccdeaa4032a65b07eMihai CodescuDescription :  Morphism of Common Logic
2e0e43889f746e31eacf8eeccdeaa4032a65b07eMihai CodescuCopyright   :  (c) Uni Bremen DFKI 2010
2e0e43889f746e31eacf8eeccdeaa4032a65b07eMihai CodescuLicense     :  GPLv2 or higher, see LICENSE.txt
2e0e43889f746e31eacf8eeccdeaa4032a65b07eMihai Codescu
2e0e43889f746e31eacf8eeccdeaa4032a65b07eMihai CodescuMaintainer  :  eugenk@informatik.uni-bremen.de
2e0e43889f746e31eacf8eeccdeaa4032a65b07eMihai CodescuStability   :  experimental
2e0e43889f746e31eacf8eeccdeaa4032a65b07eMihai CodescuPortability :  non-portable (via Logic.Logic)
2e0e43889f746e31eacf8eeccdeaa4032a65b07eMihai Codescu
2e0e43889f746e31eacf8eeccdeaa4032a65b07eMihai CodescuMorphism of Common Logic
2e0e43889f746e31eacf8eeccdeaa4032a65b07eMihai Codescu
2e0e43889f746e31eacf8eeccdeaa4032a65b07eMihai Codescu-}
2e0e43889f746e31eacf8eeccdeaa4032a65b07eMihai Codescu
2e0e43889f746e31eacf8eeccdeaa4032a65b07eMihai Codescumodule CommonLogic.Morphism
2e0e43889f746e31eacf8eeccdeaa4032a65b07eMihai Codescu  ( Morphism (..)
c208973c890b8f993297720fd0247bc7481d4304Christian Maeder  , pretty                      -- pretty printing
2e0e43889f746e31eacf8eeccdeaa4032a65b07eMihai Codescu  , idMor                       -- identity morphism
2e0e43889f746e31eacf8eeccdeaa4032a65b07eMihai Codescu  , isLegalMorphism             -- check if morhpism is ok
2e0e43889f746e31eacf8eeccdeaa4032a65b07eMihai Codescu  , composeMor                  -- composition
2e0e43889f746e31eacf8eeccdeaa4032a65b07eMihai Codescu  , inclusionMap                -- inclusion map
2e0e43889f746e31eacf8eeccdeaa4032a65b07eMihai Codescu  , mkMorphism                  -- create Morphism
2e0e43889f746e31eacf8eeccdeaa4032a65b07eMihai Codescu  , mapSentence                 -- map of sentences
2e0e43889f746e31eacf8eeccdeaa4032a65b07eMihai Codescu  , applyMap                    -- application function for maps
2e0e43889f746e31eacf8eeccdeaa4032a65b07eMihai Codescu  , applyMorphism               -- application function for morphism
2e0e43889f746e31eacf8eeccdeaa4032a65b07eMihai Codescu  , morphismUnion
2e0e43889f746e31eacf8eeccdeaa4032a65b07eMihai Codescu  ) where
2e0e43889f746e31eacf8eeccdeaa4032a65b07eMihai Codescu
2e0e43889f746e31eacf8eeccdeaa4032a65b07eMihai Codescuimport qualified Data.Map as Map
a77aecc59cee605ea48e33b65a627e0aa0a245e0Mihai Codescuimport qualified Data.Set as Set
a77aecc59cee605ea48e33b65a627e0aa0a245e0Mihai Codescuimport qualified Common.Result as Result
2e0e43889f746e31eacf8eeccdeaa4032a65b07eMihai Codescuimport Common.Id as Id
2e0e43889f746e31eacf8eeccdeaa4032a65b07eMihai Codescuimport Common.Result
2e0e43889f746e31eacf8eeccdeaa4032a65b07eMihai Codescuimport Common.Doc
2e0e43889f746e31eacf8eeccdeaa4032a65b07eMihai Codescuimport Common.DocUtils
2e0e43889f746e31eacf8eeccdeaa4032a65b07eMihai Codescu
2e0e43889f746e31eacf8eeccdeaa4032a65b07eMihai Codescuimport CommonLogic.AS_CommonLogic as AS
a9cc955b0a33e631b9ce3404e4e25b62cd067a77Christian Maederimport CommonLogic.Sign as Sign
2e0e43889f746e31eacf8eeccdeaa4032a65b07eMihai Codescu
2e0e43889f746e31eacf8eeccdeaa4032a65b07eMihai Codescu-- maps of sets
2e0e43889f746e31eacf8eeccdeaa4032a65b07eMihai Codescudata Morphism = Morphism
2e0e43889f746e31eacf8eeccdeaa4032a65b07eMihai Codescu  { source :: Sign
a9cc955b0a33e631b9ce3404e4e25b62cd067a77Christian Maeder  , target :: Sign
2e0e43889f746e31eacf8eeccdeaa4032a65b07eMihai Codescu  , propMap :: Map.Map Id Id
2e0e43889f746e31eacf8eeccdeaa4032a65b07eMihai Codescu  } deriving (Eq, Ord, Show)
2e0e43889f746e31eacf8eeccdeaa4032a65b07eMihai Codescu
2e0e43889f746e31eacf8eeccdeaa4032a65b07eMihai Codescuinstance Pretty Morphism where
a9cc955b0a33e631b9ce3404e4e25b62cd067a77Christian Maeder    pretty = printMorphism
2e0e43889f746e31eacf8eeccdeaa4032a65b07eMihai Codescu
a9cc955b0a33e631b9ce3404e4e25b62cd067a77Christian Maeder-- | Constructs an id-morphism
a9cc955b0a33e631b9ce3404e4e25b62cd067a77Christian MaederidMor :: Sign -> Morphism
2e0e43889f746e31eacf8eeccdeaa4032a65b07eMihai CodescuidMor a = inclusionMap a a
2e0e43889f746e31eacf8eeccdeaa4032a65b07eMihai Codescu
a9cc955b0a33e631b9ce3404e4e25b62cd067a77Christian Maeder-- | Determines whether a morphism is valid
2e0e43889f746e31eacf8eeccdeaa4032a65b07eMihai CodescuisLegalMorphism :: Morphism -> Result ()
2e0e43889f746e31eacf8eeccdeaa4032a65b07eMihai CodescuisLegalMorphism pmor =
a9cc955b0a33e631b9ce3404e4e25b62cd067a77Christian Maeder    let psource = allItems $ source pmor
a9cc955b0a33e631b9ce3404e4e25b62cd067a77Christian Maeder        ptarget = allItems $ target pmor
2e0e43889f746e31eacf8eeccdeaa4032a65b07eMihai Codescu        pdom = Map.keysSet $ propMap pmor
2e0e43889f746e31eacf8eeccdeaa4032a65b07eMihai Codescu        pcodom = Set.map (applyMorphism pmor) psource
a9cc955b0a33e631b9ce3404e4e25b62cd067a77Christian Maeder    in if Set.isSubsetOf pcodom ptarget && Set.isSubsetOf pdom psource
a9cc955b0a33e631b9ce3404e4e25b62cd067a77Christian Maeder    then return () else fail "illegal CommonLogic morphism"
a9cc955b0a33e631b9ce3404e4e25b62cd067a77Christian Maeder
2e0e43889f746e31eacf8eeccdeaa4032a65b07eMihai Codescu-- | Application funtion for morphisms
2e0e43889f746e31eacf8eeccdeaa4032a65b07eMihai CodescuapplyMorphism :: Morphism -> Id -> Id
a9cc955b0a33e631b9ce3404e4e25b62cd067a77Christian MaederapplyMorphism mor idt = Map.findWithDefault idt idt $ propMap mor
2e0e43889f746e31eacf8eeccdeaa4032a65b07eMihai Codescu
2e0e43889f746e31eacf8eeccdeaa4032a65b07eMihai Codescu-- | Application function for propMaps
a9cc955b0a33e631b9ce3404e4e25b62cd067a77Christian MaederapplyMap :: Map.Map Id Id -> Id -> Id
a77aecc59cee605ea48e33b65a627e0aa0a245e0Mihai CodescuapplyMap pmap idt = Map.findWithDefault idt idt pmap
2e0e43889f746e31eacf8eeccdeaa4032a65b07eMihai Codescu
a9cc955b0a33e631b9ce3404e4e25b62cd067a77Christian Maeder-- | Composition of morphisms in propositional Logic
a9cc955b0a33e631b9ce3404e4e25b62cd067a77Christian MaedercomposeMor :: Morphism -> Morphism -> Result Morphism
a9cc955b0a33e631b9ce3404e4e25b62cd067a77Christian MaedercomposeMor f g =
a9cc955b0a33e631b9ce3404e4e25b62cd067a77Christian Maeder  let fSource = source f
a77aecc59cee605ea48e33b65a627e0aa0a245e0Mihai Codescu      gTarget = target g
2e0e43889f746e31eacf8eeccdeaa4032a65b07eMihai Codescu      fMap    = propMap f
2e0e43889f746e31eacf8eeccdeaa4032a65b07eMihai Codescu      gMap    = propMap g
2e0e43889f746e31eacf8eeccdeaa4032a65b07eMihai Codescu  in return Morphism
a77aecc59cee605ea48e33b65a627e0aa0a245e0Mihai Codescu  { source = fSource
a9cc955b0a33e631b9ce3404e4e25b62cd067a77Christian Maeder  , target = gTarget
2e0e43889f746e31eacf8eeccdeaa4032a65b07eMihai Codescu  , propMap = if Map.null gMap then fMap else
2e0e43889f746e31eacf8eeccdeaa4032a65b07eMihai Codescu      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