Morphism.hs revision ea570f40967ef8bc16b76c54f9b867a8036cc750
ce5ff829db5f0bb4f16ad4de150eed4401d6acd5Christian MaederModule : $Header$
81d182b21020b815887e9057959228546cf61b6bChristian MaederDescription : Morphism of Common Logic
c438c79d00fc438f99627e612498744bdc0d0c89Christian MaederCopyright : (c) Uni Bremen DFKI 2010
97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian MaederLicense : GPLv2 or higher, see LICENSE.txt
3f69b6948966979163bdfe8331c38833d5d90ecdChristian MaederMaintainer : eugenk@informatik.uni-bremen.de
ce5ff829db5f0bb4f16ad4de150eed4401d6acd5Christian MaederStability : experimental
c438c79d00fc438f99627e612498744bdc0d0c89Christian MaederPortability : non-portable (via Logic.Logic)
f3a94a197960e548ecd6520bb768cb0d547457bbChristian MaederMorphism of Common Logic
3f63b98c111e5e2bb2cf13795cf6e084a78b0a8dChristian Maeder ( Morphism (..)
950e053ba55ac9c7d9c26a1ab48bd00202b29511Christian Maeder , pretty -- pretty printing
c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian Maeder , idMor -- identity morphism
4ef2a978e66e2246ff0b7f00c77deb7aabb28b8eChristian Maeder , isLegalMorphism -- check if morhpism is ok
5334aa8fe0b0d1eb8a1cad40b741aa07172773c9Christian Maeder , composeMor -- composition
c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian Maeder , inclusionMap -- inclusion map
3f63b98c111e5e2bb2cf13795cf6e084a78b0a8dChristian Maeder , mkMorphism -- create Morphism
15c12a3ac049a4528da05b1017b78145f308aeb0Christian Maeder , mapSentence -- map of sentences
ad270004874ce1d0697fb30d7309f180553bb315Christian Maeder , applyMap -- application function for maps
ad270004874ce1d0697fb30d7309f180553bb315Christian Maeder , applyMorphism -- application function for morphism
4ef2a978e66e2246ff0b7f00c77deb7aabb28b8eChristian Maeder , morphismUnion
3f63b98c111e5e2bb2cf13795cf6e084a78b0a8dChristian Maederimport qualified Data.Map as Map
15c12a3ac049a4528da05b1017b78145f308aeb0Christian Maederimport qualified Data.Set as Set
fc7df539e6d41b050161ed8f9ae6e444b1b5ab14Christian Maederimport qualified Common.Result as Result
c438c79d00fc438f99627e612498744bdc0d0c89Christian Maeder-- maps of sets
04dada28736b4a237745e92063d8bdd49a362debChristian Maederdata Morphism = Morphism
5334aa8fe0b0d1eb8a1cad40b741aa07172773c9Christian Maeder { source :: Sign
6d96cc81e7926a65188fea5626e0e4e199f9d782Christian Maeder , target :: Sign
6d96cc81e7926a65188fea5626e0e4e199f9d782Christian Maeder , propMap :: Map.Map Id Id
6b1153c560b677f9f5da2a60ee8a10de75ff90c5Christian Maeder } deriving (Eq, Ord, Show)
6d96cc81e7926a65188fea5626e0e4e199f9d782Christian Maederinstance Pretty Morphism where
5334aa8fe0b0d1eb8a1cad40b741aa07172773c9Christian Maeder pretty = printMorphism
c438c79d00fc438f99627e612498744bdc0d0c89Christian Maeder-- | Constructs an id-morphism
6d96cc81e7926a65188fea5626e0e4e199f9d782Christian MaederidMor :: Sign -> Morphism
6d96cc81e7926a65188fea5626e0e4e199f9d782Christian MaederidMor a = inclusionMap a a
6d96cc81e7926a65188fea5626e0e4e199f9d782Christian Maeder-- | Determines whether a morphism is valid
6d96cc81e7926a65188fea5626e0e4e199f9d782Christian MaederisLegalMorphism :: Morphism -> Result ()
cf5149eb4d0faef6272231879c04aa740f5abc2bChristian MaederisLegalMorphism pmor =
f4741f6b7da52b5417899c8fcbe4349b920b006eChristian Maeder let psource = allItems $ source pmor
6d96cc81e7926a65188fea5626e0e4e199f9d782Christian Maeder ptarget = allItems $ target pmor
6d96cc81e7926a65188fea5626e0e4e199f9d782Christian Maeder pdom = Map.keysSet $ propMap pmor
6d96cc81e7926a65188fea5626e0e4e199f9d782Christian Maeder pcodom = Set.map (applyMorphism pmor) psource
6d96cc81e7926a65188fea5626e0e4e199f9d782Christian Maeder in if Set.isSubsetOf pcodom ptarget && Set.isSubsetOf pdom psource
f4741f6b7da52b5417899c8fcbe4349b920b006eChristian Maeder then return () else fail "illegal CommonLogic morphism"
f4741f6b7da52b5417899c8fcbe4349b920b006eChristian Maeder-- | Application funtion for morphisms
04dada28736b4a237745e92063d8bdd49a362debChristian MaederapplyMorphism :: Morphism -> Id -> Id
9ae2df7accdbf35839d56f90e1e8662be7112cdbChristian MaederapplyMorphism mor idt = Map.findWithDefault idt idt $ propMap mor
ad623ebb0fa505940a039fe967ecff8749719ac9Christian Maeder-- | Application function for propMaps
9ae2df7accdbf35839d56f90e1e8662be7112cdbChristian MaederapplyMap :: Map.Map Id Id -> Id -> Id
9ae2df7accdbf35839d56f90e1e8662be7112cdbChristian MaederapplyMap pmap idt = Map.findWithDefault idt idt pmap
9ae2df7accdbf35839d56f90e1e8662be7112cdbChristian Maeder-- | Composition of morphisms in propositional Logic
9ae2df7accdbf35839d56f90e1e8662be7112cdbChristian MaedercomposeMor :: Morphism -> Morphism -> Result Morphism
9ae2df7accdbf35839d56f90e1e8662be7112cdbChristian MaedercomposeMor f g =
9ae2df7accdbf35839d56f90e1e8662be7112cdbChristian Maeder let fSource = source f
9ae2df7accdbf35839d56f90e1e8662be7112cdbChristian Maeder gTarget = target g
6d96cc81e7926a65188fea5626e0e4e199f9d782Christian Maeder fMap = propMap f
6d96cc81e7926a65188fea5626e0e4e199f9d782Christian Maeder gMap = propMap g
6d96cc81e7926a65188fea5626e0e4e199f9d782Christian Maeder in return Morphism
6d96cc81e7926a65188fea5626e0e4e199f9d782Christian Maeder { source = fSource
6d96cc81e7926a65188fea5626e0e4e199f9d782Christian Maeder , target = gTarget
6d96cc81e7926a65188fea5626e0e4e199f9d782Christian Maeder , propMap = if Map.null gMap then fMap else
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder Set.fold ( \ i -> let j = applyMap gMap (applyMap fMap i) in
c438c79d00fc438f99627e612498744bdc0d0c89Christian Maeder if i == j then id else Map.insert i j)
c438c79d00fc438f99627e612498744bdc0d0c89Christian Maeder Map.empty $ allItems fSource }
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder-- | Pretty printing for Morphisms
36c6cc568751e4235502cfee00ba7b597dae78dcChristian MaederprintMorphism :: Morphism -> Doc
36c6cc568751e4235502cfee00ba7b597dae78dcChristian MaederprintMorphism m = pretty (source m) <> text "-->" <> pretty (target m)
ab0f35d8b9012e459417e086773049ce33dda2a0Christian Maeder <> vcat (map ( \ (x, y) -> lparen <> pretty x <> text ","
ab0f35d8b9012e459417e086773049ce33dda2a0Christian Maeder <> pretty y <> rparen) $ Map.assocs $ propMap m)
ab0f35d8b9012e459417e086773049ce33dda2a0Christian Maeder-- | Inclusion map of a subsig into a supersig
72b9099aeec0762bae4546db3bc4b48721027bf4Christian MaederinclusionMap :: Sign.Sign -> Sign.Sign -> Morphism
ab0f35d8b9012e459417e086773049ce33dda2a0Christian MaederinclusionMap s1 s2 = Morphism
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder { source = s1
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder , target = s2
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder-- | creates a Morphism
36c6cc568751e4235502cfee00ba7b597dae78dcChristian MaedermkMorphism :: Sign.Sign -> Sign.Sign -> Map.Map Id Id -> Morphism
36c6cc568751e4235502cfee00ba7b597dae78dcChristian MaedermkMorphism s t p =
7dec34aee2b609b9535c48d060e0f7baf3536457Christian Maeder Morphism { source = s
e76e6a43f51438215737d6fc176c89da05bb86daChristian Maeder , propMap = p }
0df692ce8b9293499b2e1768458613a63e7b5cd0Christian Maeder-- | sentence (text) translation along signature morphism
0df692ce8b9293499b2e1768458613a63e7b5cd0Christian Maeder-- here just the renaming of formulae
0df692ce8b9293499b2e1768458613a63e7b5cd0Christian MaedermapSentence :: Morphism -> AS.TEXT_META -> Result.Result AS.TEXT_META
0b14ccc700093e203914052bf6aceda3164af730Christian MaedermapSentence mor tm =
6b1153c560b677f9f5da2a60ee8a10de75ff90c5Christian Maeder return $ tm { getText = mapSen_txt mor $ getText tm }
9c03fbe72966fb21c99238c449efdb0126dae9deChristian Maeder-- propagates the translation to sentences
9c03fbe72966fb21c99238c449efdb0126dae9deChristian MaedermapSen_txt :: Morphism -> AS.TEXT -> AS.TEXT
9c03fbe72966fb21c99238c449efdb0126dae9deChristian MaedermapSen_txt mor txt = case txt of
9c03fbe72966fb21c99238c449efdb0126dae9deChristian Maeder AS.Text phrs r -> AS.Text (map (mapSen_phr mor) phrs) r
9c03fbe72966fb21c99238c449efdb0126dae9deChristian Maeder AS.Named_text n t r -> AS.Named_text n (mapSen_txt mor t) r
6d96cc81e7926a65188fea5626e0e4e199f9d782Christian Maeder-- propagates the translation to sentences
793945d4ac7c0f22760589c87af8e71427c76118Christian MaedermapSen_phr :: Morphism -> AS.PHRASE -> AS.PHRASE
0f0aa53f11a0d1ab08c76428b9de73db5b17c977Christian MaedermapSen_phr mor phr = case phr of
9c03fbe72966fb21c99238c449efdb0126dae9deChristian Maeder AS.Module m -> AS.Module $ mapSen_mod mor m
9c03fbe72966fb21c99238c449efdb0126dae9deChristian Maeder AS.Sentence s -> AS.Sentence $ mapSen_sen mor s
c438c79d00fc438f99627e612498744bdc0d0c89Christian Maeder AS.Comment_text c t r -> AS.Comment_text c (mapSen_txt mor t) r
d48085f765fca838c1d972d2123601997174583dChristian Maeder-- propagates the translation to sentences
c438c79d00fc438f99627e612498744bdc0d0c89Christian MaedermapSen_mod :: Morphism -> AS.MODULE -> AS.MODULE
c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian MaedermapSen_mod mor m = case m of
c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian Maeder AS.Mod n t rn -> AS.Mod n (mapSen_txt mor t) rn
c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian Maeder AS.Mod_ex n exs t rn -> AS.Mod_ex n exs (mapSen_txt mor t) rn
c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian MaedermapSen_sen :: Morphism -> AS.SENTENCE -> AS.SENTENCE
c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian MaedermapSen_sen mor frm = case frm of
c438c79d00fc438f99627e612498744bdc0d0c89Christian Maeder AS.Quant_sent q (map (mapSen_nos mor) vs) (mapSen_sen mor is) rn
c438c79d00fc438f99627e612498744bdc0d0c89Christian Maeder AS.Bool_sent bs rn -> AS.Bool_sent (case bs of
c438c79d00fc438f99627e612498744bdc0d0c89Christian Maeder AS.Junction j sens -> AS.Junction j (map (mapSen_sen mor) sens)
72b9099aeec0762bae4546db3bc4b48721027bf4Christian Maeder AS.Negation sen -> AS.Negation (mapSen_sen mor sen)
72b9099aeec0762bae4546db3bc4b48721027bf4Christian Maeder AS.BinOp op (mapSen_sen mor s1) (mapSen_sen mor s2)
a716971174535184da7713ed308423e355a4aa66Christian Maeder AS.Atom_sent atom rn -> AS.Atom_sent (case atom of
a716971174535184da7713ed308423e355a4aa66Christian Maeder AS.Equation t1 t2 -> AS.Equation (mapSen_trm mor t1) (mapSen_trm mor t2)
a716971174535184da7713ed308423e355a4aa66Christian Maeder AS.Atom t tss -> AS.Atom (mapSen_trm mor t) (map (mapSen_trmSeq mor) tss)
c438c79d00fc438f99627e612498744bdc0d0c89Christian Maeder AS.Comment_sent cm sen rn -> AS.Comment_sent cm (mapSen_sen mor sen) rn
c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian Maeder AS.Irregular_sent sen rn -> AS.Irregular_sent (mapSen_sen mor sen) rn
c438c79d00fc438f99627e612498744bdc0d0c89Christian MaedermapSen_trm :: Morphism -> AS.TERM -> AS.TERM
c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian MaedermapSen_trm mor trm = case trm of
c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian Maeder AS.Name_term n -> AS.Name_term (mapSen_tok mor n)
7551e65ddba3503270d1bf54712217cbd6b8d5fcChristian Maeder AS.Funct_term (mapSen_trm mor t) (map (mapSen_trmSeq mor) ts) rn
7551e65ddba3503270d1bf54712217cbd6b8d5fcChristian Maeder AS.Comment_term t c rn -> AS.Comment_term (mapSen_trm mor t) c rn
7551e65ddba3503270d1bf54712217cbd6b8d5fcChristian Maeder AS.That_term s rn -> AS.That_term (mapSen_sen mor s) rn
0f0aa53f11a0d1ab08c76428b9de73db5b17c977Christian MaedermapSen_nos :: Morphism -> AS.NAME_OR_SEQMARK -> AS.NAME_OR_SEQMARK
0f0aa53f11a0d1ab08c76428b9de73db5b17c977Christian MaedermapSen_nos mor nos = case nos of
0f0aa53f11a0d1ab08c76428b9de73db5b17c977Christian Maeder AS.SeqMark s -> AS.SeqMark (mapSen_tok mor s)
0f0aa53f11a0d1ab08c76428b9de73db5b17c977Christian MaedermapSen_trmSeq :: Morphism -> AS.TERM_SEQ -> AS.TERM_SEQ
0b14ccc700093e203914052bf6aceda3164af730Christian MaedermapSen_trmSeq mor ts = case ts of
cc8b603388a7deb7fb8045db0341f550f8be5844Christian Maeder AS.Term_seq t -> AS.Term_seq (mapSen_trm mor t)
c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian Maeder AS.Seq_marks s -> AS.Seq_marks (mapSen_tok mor s)
f4741f6b7da52b5417899c8fcbe4349b920b006eChristian MaedermapSen_tok :: Morphism -> Id.Token -> Id.Token
c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian MaedermapSen_tok mor tok = Id.idToSimpleId $ applyMorphism mor $ Id.simpleIdToId tok
1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian Maeder-- | Union of two morphisms.
cc8b603388a7deb7fb8045db0341f550f8be5844Christian MaedermorphismUnion :: Morphism -> Morphism -> Result.Result Morphism
ad623ebb0fa505940a039fe967ecff8749719ac9Christian MaedermorphismUnion mor1 mor2 =
ad623ebb0fa505940a039fe967ecff8749719ac9Christian Maeder let pmap1 = propMap mor1
6d96cc81e7926a65188fea5626e0e4e199f9d782Christian Maeder pmap2 = propMap mor2
6d96cc81e7926a65188fea5626e0e4e199f9d782Christian Maeder p1 = source mor1
6d96cc81e7926a65188fea5626e0e4e199f9d782Christian Maeder p2 = source mor2
6d96cc81e7926a65188fea5626e0e4e199f9d782Christian Maeder up1 = Set.difference (allItems p1) $ Map.keysSet pmap1
6d96cc81e7926a65188fea5626e0e4e199f9d782Christian Maeder up2 = Set.difference (allItems p2) $ Map.keysSet pmap2
6d96cc81e7926a65188fea5626e0e4e199f9d782Christian Maeder (pds, pmap) = foldr ( \ (i, j) (ds, m) -> case Map.lookup i m of
c438c79d00fc438f99627e612498744bdc0d0c89Christian Maeder Nothing -> (ds, Map.insert i j m)
e9490701e16d1e8abd995ef876d6f937da93b412Christian Maeder Just k -> if j == k then (ds, m) else
e9490701e16d1e8abd995ef876d6f937da93b412Christian Maeder ("incompatible mapping of prop " ++ showId i " to "
e9490701e16d1e8abd995ef876d6f937da93b412Christian Maeder ++ showId j " and " ++ showId k "")
e9490701e16d1e8abd995ef876d6f937da93b412Christian Maeder nullRange : ds, m))
e9490701e16d1e8abd995ef876d6f937da93b412Christian Maeder (Map.toList pmap2 ++ map (\ a -> (a, a))
e9490701e16d1e8abd995ef876d6f937da93b412Christian Maeder in if null pds then return Morphism
e9490701e16d1e8abd995ef876d6f937da93b412Christian Maeder { source = unite p1 p2
e9490701e16d1e8abd995ef876d6f937da93b412Christian Maeder , target = unite (target mor1) $ target mor2
e9490701e16d1e8abd995ef876d6f937da93b412Christian Maeder , propMap = pmap } else Result pds Nothing