Morphism.hs revision d2d5606ab65ddf48599bd044416de07a205095f2
4b0a4c7dea0f67a233dcc42ce9bb18d36de109aeChristian MaederModule : $Header$
5ba323da9f037264b4a356085e844889aedeac23Christian MaederDescription : Morphism of Common Logic
10397bcc134edbcfbe3ae2c7ea4c6080036aae22Christian MaederCopyright : (c) Uni Bremen DFKI 2010
97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian MaederLicense : GPLv2 or higher, see LICENSE.txt
3f69b6948966979163bdfe8331c38833d5d90ecdChristian MaederMaintainer : eugenk@informatik.uni-bremen.de
4b0a4c7dea0f67a233dcc42ce9bb18d36de109aeChristian MaederStability : experimental
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian MaederPortability : non-portable (via Logic.Logic)
f3a94a197960e548ecd6520bb768cb0d547457bbChristian MaederMorphism of Common Logic
e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maeder ( Morphism (..)
4b0a4c7dea0f67a233dcc42ce9bb18d36de109aeChristian Maeder , pretty -- pretty printing
afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder , idMor -- identity morphism
fc8c6570c7b4ee13f375eb607bed2290438573bfChristian Maeder , isLegalMorphism -- check if morhpism is ok
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder , composeMor -- composition
23f8d286586ff38a9e73052b2c7c04c62c5c638fChristian Maeder , inclusionMap -- inclusion map
ad270004874ce1d0697fb30d7309f180553bb315Christian Maeder , mkMorphism -- create Morphism
ad270004874ce1d0697fb30d7309f180553bb315Christian Maeder , mapSentence -- map of sentences
fc8c6570c7b4ee13f375eb607bed2290438573bfChristian Maeder , applyMap -- application function for maps
f8f78a2c8796a387a4348cc672ae08e8d9f69315Christian Maeder , applyMorphism -- application function for morphism
950e053ba55ac9c7d9c26a1ab48bd00202b29511Christian Maeder , morphismUnion
afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maederimport qualified Data.Map as Map
f8f78a2c8796a387a4348cc672ae08e8d9f69315Christian Maederimport qualified Data.Set as Set
af621d0066770895fd79562728e93099c8c52060Christian Maederimport qualified Common.Result as Result
024621f43239cfe9629e35d35a8669fad7acbba2Christian Maeder-- maps of sets
afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maederdata Morphism = Morphism
afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder { source :: Sign
afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder , target :: Sign
afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder , propMap :: Map.Map Id Id
afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder } deriving (Eq, Ord, Show)
afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maederinstance Pretty Morphism where
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder pretty = printMorphism
afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder-- | Constructs an id-morphism
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian MaederidMor :: Sign -> Morphism
7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian MaederidMor a = inclusionMap a a
7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder-- | Determines whether a morphism is valid
7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian MaederisLegalMorphism :: Morphism -> Result ()
7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian MaederisLegalMorphism pmor =
7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder let psource = allItems $ source pmor
afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder ptarget = allItems $ target pmor
afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder pdom = Map.keysSet $ propMap pmor
afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder pcodom = Set.map (applyMorphism pmor) psource
afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder in if Set.isSubsetOf pcodom ptarget && Set.isSubsetOf pdom psource
afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder then return () else fail "illegal CommonLogic morphism"
7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder-- | Application funtion for morphisms
7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian MaederapplyMorphism :: Morphism -> Id -> Id
7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian MaederapplyMorphism mor idt = Map.findWithDefault idt idt $ propMap mor
9e0472be46104307b974fe5079bf5cc9e94a1a96Christian Maeder-- | Application function for propMaps
9e0472be46104307b974fe5079bf5cc9e94a1a96Christian MaederapplyMap :: Map.Map Id Id -> Id -> Id
9e0472be46104307b974fe5079bf5cc9e94a1a96Christian MaederapplyMap pmap idt = Map.findWithDefault idt idt pmap
7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder-- | Composition of morphisms in propositional Logic
9e0472be46104307b974fe5079bf5cc9e94a1a96Christian MaedercomposeMor :: Morphism -> Morphism -> Result Morphism
7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian MaedercomposeMor f g =
7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder let fSource = source f
9e0472be46104307b974fe5079bf5cc9e94a1a96Christian Maeder gTarget = target g
9e0472be46104307b974fe5079bf5cc9e94a1a96Christian Maeder fMap = propMap f
7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder gMap = propMap g
afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder in return Morphism
afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder { source = fSource
afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder , target = gTarget
e8a2ca3a7b3e9a19ef03b6b1c0b5d03dbad6463cChristian Maeder , propMap = if Map.null gMap then fMap else
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder Set.fold ( \ i -> let j = applyMap gMap (applyMap fMap i) in
eca4db63ed0bdbd93b62678feea6e3eb80aa47bbChristian Maeder if i == j then id else Map.insert i j)
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder Map.empty $ allItems fSource }
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder-- | Pretty printing for Morphisms
eca4db63ed0bdbd93b62678feea6e3eb80aa47bbChristian MaederprintMorphism :: Morphism -> Doc
986e0e9cf8c2358f455460b3fc75ce7c5dcf0973Christian MaederprintMorphism m = pretty (source m) <> text "-->" <> pretty (target m)
6a7e00a968cb0f3f9ccae19ab47ef3636c7e79bfChristian Maeder <> vcat (map ( \ (x, y) -> lparen <> pretty x <> text ","
6a7e00a968cb0f3f9ccae19ab47ef3636c7e79bfChristian Maeder <> pretty y <> rparen) $ Map.assocs $ propMap m)
88ece6e49930670e8fd3ee79c89a2e918d2fbd0cChristian Maeder-- | Inclusion map of a subsig into a supersig
88ece6e49930670e8fd3ee79c89a2e918d2fbd0cChristian MaederinclusionMap :: Sign.Sign -> Sign.Sign -> Morphism
6a7e00a968cb0f3f9ccae19ab47ef3636c7e79bfChristian MaederinclusionMap s1 s2 = Morphism
6a7e00a968cb0f3f9ccae19ab47ef3636c7e79bfChristian Maeder { source = s1
6a7e00a968cb0f3f9ccae19ab47ef3636c7e79bfChristian Maeder , target = s2
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder-- | creates a Morphism
e8a2ca3a7b3e9a19ef03b6b1c0b5d03dbad6463cChristian MaedermkMorphism :: Sign.Sign -> Sign.Sign -> Map.Map Id Id -> Morphism
59c301c268f79cfde0a4c30a2c572a368db98da5Christian MaedermkMorphism s t p =
59c301c268f79cfde0a4c30a2c572a368db98da5Christian Maeder Morphism { source = s
0a320bc4cdbf38f480b75ac15a54db1c4885b497Christian Maeder , propMap = p }
59c301c268f79cfde0a4c30a2c572a368db98da5Christian Maeder-- | sentence (text) translation along signature morphism
0a320bc4cdbf38f480b75ac15a54db1c4885b497Christian Maeder-- here just the renaming of formulae
5334aa8fe0b0d1eb8a1cad40b741aa07172773c9Christian MaedermapSentence :: Morphism -> AS.TEXT_META -> Result.Result AS.TEXT_META
59c301c268f79cfde0a4c30a2c572a368db98da5Christian MaedermapSentence mor tm =
e8a2ca3a7b3e9a19ef03b6b1c0b5d03dbad6463cChristian Maeder return $ tm { getText = mapSen_txt mor $ getText tm }
e8a2ca3a7b3e9a19ef03b6b1c0b5d03dbad6463cChristian Maeder-- propagates the translation to sentences
e8a2ca3a7b3e9a19ef03b6b1c0b5d03dbad6463cChristian MaedermapSen_txt :: Morphism -> AS.TEXT -> AS.TEXT
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian MaedermapSen_txt mor txt = case txt of
e8a2ca3a7b3e9a19ef03b6b1c0b5d03dbad6463cChristian Maeder AS.Text phrs r -> AS.Text (map (mapSen_phr mor) phrs) r
e8a2ca3a7b3e9a19ef03b6b1c0b5d03dbad6463cChristian Maeder AS.Named_text n t r -> AS.Named_text n (mapSen_txt mor t) r
ad187062b0009820118c1b773a232e29b879a2faChristian Maeder-- propagates the translation to sentences
5334aa8fe0b0d1eb8a1cad40b741aa07172773c9Christian MaedermapSen_phr :: Morphism -> AS.PHRASE -> AS.PHRASE
5334aa8fe0b0d1eb8a1cad40b741aa07172773c9Christian MaedermapSen_phr mor phr = case phr of
ad187062b0009820118c1b773a232e29b879a2faChristian Maeder AS.Module m -> AS.Module $ mapSen_mod mor m
ad187062b0009820118c1b773a232e29b879a2faChristian Maeder AS.Sentence s -> AS.Sentence $ mapSen_sen mor s
5334aa8fe0b0d1eb8a1cad40b741aa07172773c9Christian Maeder AS.Comment_text c t r -> AS.Comment_text c (mapSen_txt mor t) r
ad187062b0009820118c1b773a232e29b879a2faChristian Maeder-- propagates the translation to sentences
5334aa8fe0b0d1eb8a1cad40b741aa07172773c9Christian MaedermapSen_mod :: Morphism -> AS.MODULE -> AS.MODULE
ad187062b0009820118c1b773a232e29b879a2faChristian MaedermapSen_mod mor m = case m of
ad187062b0009820118c1b773a232e29b879a2faChristian Maeder AS.Mod n t rn -> AS.Mod n (mapSen_txt mor t) rn
ad187062b0009820118c1b773a232e29b879a2faChristian Maeder AS.Mod_ex n exs t rn -> AS.Mod_ex n exs (mapSen_txt mor t) rn
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian MaedermapSen_sen :: Morphism -> AS.SENTENCE -> AS.SENTENCE
e8a2ca3a7b3e9a19ef03b6b1c0b5d03dbad6463cChristian MaedermapSen_sen mor frm = case frm of
e8a2ca3a7b3e9a19ef03b6b1c0b5d03dbad6463cChristian Maeder AS.Quant_sent qs rn -> AS.Quant_sent (case qs of
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder QUANT_SENT q xs sen ->
e76e6a43f51438215737d6fc176c89da05bb86daChristian Maeder QUANT_SENT q (map (mapSen_nos mor) xs) (mapSen_sen mor sen)
da5ddac3b07f5910940727d765a4431b8c17cdbbChristian Maeder AS.Bool_sent bs rn -> AS.Bool_sent (case bs of
997c56f3bc74a703043010978e5013fdb074d659Christian Maeder AS.Junction j sens -> AS.Junction j (map (mapSen_sen mor) sens)
e8a2ca3a7b3e9a19ef03b6b1c0b5d03dbad6463cChristian Maeder AS.Negation sen -> AS.Negation (mapSen_sen mor sen)
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder AS.BinOp op (mapSen_sen mor s1) (mapSen_sen mor s2)
8485da94b57d8b5135ee685b55c982b037ed4140Christian Maeder AS.Atom_sent atom rn -> AS.Atom_sent (case atom of
ad187062b0009820118c1b773a232e29b879a2faChristian Maeder AS.Equation t1 t2 -> AS.Equation (mapSen_trm mor t1) (mapSen_trm mor t2)
e76e6a43f51438215737d6fc176c89da05bb86daChristian Maeder AS.Atom t tss -> AS.Atom (mapSen_trm mor t) (map (mapSen_trmSeq mor) tss)
e76e6a43f51438215737d6fc176c89da05bb86daChristian Maeder AS.Comment_sent cm sen rn -> AS.Comment_sent cm (mapSen_sen mor sen) rn
ad187062b0009820118c1b773a232e29b879a2faChristian Maeder AS.Irregular_sent sen rn -> AS.Irregular_sent (mapSen_sen mor sen) rn
e76e6a43f51438215737d6fc176c89da05bb86daChristian MaedermapSen_trm :: Morphism -> AS.TERM -> AS.TERM
e76e6a43f51438215737d6fc176c89da05bb86daChristian MaedermapSen_trm mor trm = case trm of
e76e6a43f51438215737d6fc176c89da05bb86daChristian Maeder AS.Name_term n -> AS.Name_term (mapSen_tok mor n)
59c301c268f79cfde0a4c30a2c572a368db98da5Christian Maeder AS.Funct_term (mapSen_trm mor t) (map (mapSen_trmSeq mor) ts) rn
dc6b48bb46df8e56da3491c98476e6da0d1d5d1dChristian Maeder AS.Comment_term t c rn -> AS.Comment_term (mapSen_trm mor t) c rn
4b0a4c7dea0f67a233dcc42ce9bb18d36de109aeChristian MaedermapSen_nos :: Morphism -> AS.NAME_OR_SEQMARK -> AS.NAME_OR_SEQMARK
e8a2ca3a7b3e9a19ef03b6b1c0b5d03dbad6463cChristian MaedermapSen_nos mor nos = case nos of
7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder AS.SeqMark s -> AS.SeqMark (mapSen_tok mor s)
7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian MaedermapSen_trmSeq :: Morphism -> AS.TERM_SEQ -> AS.TERM_SEQ
7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian MaedermapSen_trmSeq mor ts = case ts of
ff9a53595208f532c25ac5168f772f48fd80fdb5Christian Maeder AS.Term_seq t -> AS.Term_seq (mapSen_trm mor t)
7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder AS.Seq_marks s -> AS.Seq_marks (mapSen_tok mor s)
ff9a53595208f532c25ac5168f772f48fd80fdb5Christian MaedermapSen_tok :: Morphism -> Id.Token -> Id.Token
7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian MaedermapSen_tok mor tok = Id.idToSimpleId $ applyMorphism mor $ Id.simpleIdToId tok
ff9a53595208f532c25ac5168f772f48fd80fdb5Christian Maeder-- | Union of two morphisms.
7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian MaedermorphismUnion :: Morphism -> Morphism -> Result.Result Morphism
7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian MaedermorphismUnion mor1 mor2 =
62ecb1e7f8fd9573eea8369657de12c7bf9f4f25Christian Maeder let pmap1 = propMap mor1
f6f2955769bfe80dbb4cca3b3ee33c5a8a0f5355Christian Maeder pmap2 = propMap mor2
c1031ac42b3f3d7d0fe7d9d6b54423a092d473a0Christian Maeder p1 = source mor1
fce77b2785912d1abbcc3680088b235f534bdeffChristian Maeder p2 = source mor2
7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder up1 = Set.difference (allItems p1) $ Map.keysSet pmap1
7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder up2 = Set.difference (allItems p2) $ Map.keysSet pmap2
ff9a53595208f532c25ac5168f772f48fd80fdb5Christian Maeder (pds, pmap) = foldr ( \ (i, j) (ds, m) -> case Map.lookup i m of
7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder Nothing -> (ds, Map.insert i j m)
ac19566dc64536c38b5d1d3ae510fb8a07784c2fChristian Maeder Just k -> if j == k then (ds, m) else
fe5dbb45b6a8abf34375b4bc5f2a81cda664c0e4Christian Maeder ("incompatible mapping of prop " ++ showId i " to "
3cafc73a998493f9ed3d5e934c0ab80bcfb465c2Christian Maeder ++ showId j " and " ++ showId k "")
e13ee09381f136f5eadaabdb9699773c0052cf3dChristian Maeder nullRange : ds, m))
ac19566dc64536c38b5d1d3ae510fb8a07784c2fChristian Maeder (Map.toList pmap2 ++ map (\ a -> (a, a))
7bf6d421b0ea31ae63f1fe04919942b931abda47Christian Maeder in if null pds then return Morphism
021d7137df04ec1834911d99d90243a092841cedChristian Maeder { source = unite p1 p2
021d7137df04ec1834911d99d90243a092841cedChristian Maeder , target = unite (target mor1) $ target mor2
7c554e9d4a39b8eb3b0881f20807c95dd8e793aeChristian Maeder , propMap = pmap } else Result pds Nothing