Morphism.hs revision b3138d7e20d2d6dd26a325b844a8b21b0ecbb602
7abd0c58a5ce51db13f93de82407b2188d55d298Christian MaederModule : $Header$
14a1af9d9909dc47dc7fee6b0170b7ac0aef85daChristian MaederDescription : Morphism of Common Logic
97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian MaederCopyright : (c) Uni Bremen DFKI 2010
c00adad2e9459b422dee09e3a2bddba66b433bb7Christian MaederLicense : GPLv2 or higher, see LICENSE.txt
7abd0c58a5ce51db13f93de82407b2188d55d298Christian MaederMaintainer : kluc@informatik.uni-bremen.de
2ac1742771a267119f1d839054b5e45d0a468085Christian MaederStability : experimental
7abd0c58a5ce51db13f93de82407b2188d55d298Christian MaederPortability : non-portable (via Logic.Logic)
c00adad2e9459b422dee09e3a2bddba66b433bb7Christian MaederMorphism of Common Logic
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder ( Morphism (..)
e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maeder , pretty -- pretty printing
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder , idMor -- identity morphism
14a1af9d9909dc47dc7fee6b0170b7ac0aef85daChristian Maeder , isLegalMorphism -- check if morhpism is ok
ad270004874ce1d0697fb30d7309f180553bb315Christian Maeder , composeMor -- composition
ad270004874ce1d0697fb30d7309f180553bb315Christian Maeder , inclusionMap -- inclusion map
4ef2a978e66e2246ff0b7f00c77deb7aabb28b8eChristian Maeder , mkMorphism -- create Morphism
8197d0be8b81692f311ad5ca34e125e2cf9eecb8Christian Maeder , mapSentence -- map of sentences
e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maeder , mapSentenceH -- map of sentences, without Result type
ccf3de3d66b521a260e5c22d335c64a48e3f0195Christian Maeder , applyMap -- application function for maps
d42a01c4eb6892fe23ca9eff107bb29f4a229480Christian Maeder , applyMorphism -- application function for morphism
b1bd8688a1ce545444792a307412711c2c61df5fChristian Maeder , morphismUnion
c18e9c3c6d5039618f1f2c05526ece84c7794ea3Christian Maederimport qualified Data.Map as Map
2ac1742771a267119f1d839054b5e45d0a468085Christian Maederimport qualified Data.Set as Set
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maederimport qualified Common.Result as Result
2ac1742771a267119f1d839054b5e45d0a468085Christian Maederimport CommonLogic.AS_CommonLogic as AS_BASIC
b1bd8688a1ce545444792a307412711c2c61df5fChristian Maeder-- maps of sets
81946e2b3f6dde6167f48769bd02c7a634736856Christian Maederdata Morphism = Morphism
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder { source :: Sign
35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder , target :: Sign
14a1af9d9909dc47dc7fee6b0170b7ac0aef85daChristian Maeder , propMap :: Map.Map Id Id
2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder } deriving (Eq, Ord, Show)
2ac1742771a267119f1d839054b5e45d0a468085Christian Maederinstance Pretty Morphism where
81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder pretty = printMorphism
81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder-- | Constructs an id-morphism
81946e2b3f6dde6167f48769bd02c7a634736856Christian MaederidMor :: Sign -> Morphism
81946e2b3f6dde6167f48769bd02c7a634736856Christian MaederidMor a = inclusionMap a a
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder-- | Determines whether a morphism is valid
2ac1742771a267119f1d839054b5e45d0a468085Christian MaederisLegalMorphism :: Morphism -> Result ()
ce7653c9c71e23bf04a5ec0ca5cb600c3738a909Christian MaederisLegalMorphism pmor =
2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder let psource = items $ source pmor
ce7653c9c71e23bf04a5ec0ca5cb600c3738a909Christian Maeder ptarget = items $ target pmor
ce7653c9c71e23bf04a5ec0ca5cb600c3738a909Christian Maeder pdom = Map.keysSet $ propMap pmor
2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder pcodom = Set.map (applyMorphism pmor) psource
ce7653c9c71e23bf04a5ec0ca5cb600c3738a909Christian Maeder in if Set.isSubsetOf pcodom ptarget && Set.isSubsetOf pdom psource
d48085f765fca838c1d972d2123601997174583dChristian Maeder then return () else fail "illegal CommonLogic morphism"
b1bd8688a1ce545444792a307412711c2c61df5fChristian Maeder-- | Application funtion for morphisms
b1bd8688a1ce545444792a307412711c2c61df5fChristian MaederapplyMorphism :: Morphism -> Id -> Id
b1bd8688a1ce545444792a307412711c2c61df5fChristian MaederapplyMorphism mor idt = Map.findWithDefault idt idt $ propMap mor
b1bd8688a1ce545444792a307412711c2c61df5fChristian Maeder-- | Application function for propMaps
b1bd8688a1ce545444792a307412711c2c61df5fChristian MaederapplyMap :: Map.Map Id Id -> Id -> Id
b1bd8688a1ce545444792a307412711c2c61df5fChristian MaederapplyMap pmap idt = Map.findWithDefault idt idt pmap
b1bd8688a1ce545444792a307412711c2c61df5fChristian Maeder-- | Composition of morphisms in propositional Logic
b1bd8688a1ce545444792a307412711c2c61df5fChristian MaedercomposeMor :: Morphism -> Morphism -> Result Morphism
b1bd8688a1ce545444792a307412711c2c61df5fChristian MaedercomposeMor f g =
b1bd8688a1ce545444792a307412711c2c61df5fChristian Maeder let fSource = source f
b1bd8688a1ce545444792a307412711c2c61df5fChristian Maeder gTarget = target g
b1bd8688a1ce545444792a307412711c2c61df5fChristian Maeder fMap = propMap f
b1bd8688a1ce545444792a307412711c2c61df5fChristian Maeder gMap = propMap g
b1bd8688a1ce545444792a307412711c2c61df5fChristian Maeder in return Morphism
b1bd8688a1ce545444792a307412711c2c61df5fChristian Maeder { source = fSource
b1bd8688a1ce545444792a307412711c2c61df5fChristian Maeder , target = gTarget
b1bd8688a1ce545444792a307412711c2c61df5fChristian Maeder , propMap = if Map.null gMap then fMap else
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder Set.fold ( \ i -> let j = applyMap gMap (applyMap fMap i) in
14a1af9d9909dc47dc7fee6b0170b7ac0aef85daChristian Maeder if i == j then id else Map.insert i j)
5ba383b1607c20c57e14324e72cee2c789436d5fChristian Maeder Map.empty $ items fSource }
2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder-- | Pretty printing for Morphisms
14a1af9d9909dc47dc7fee6b0170b7ac0aef85daChristian MaederprintMorphism :: Morphism -> Doc
2ac1742771a267119f1d839054b5e45d0a468085Christian MaederprintMorphism m = pretty (source m) <> text "-->" <> pretty (target m)
2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder <> vcat (map ( \ (x, y) -> lparen <> pretty x <> text ","
0f0aa53f11a0d1ab08c76428b9de73db5b17c977Christian Maeder <> pretty y <> rparen) $ Map.assocs $ propMap m)
7c35990c03276d1e675ea6f4ba38f47081620d77Christian Maeder-- | Inclusion map of a subsig into a supersig
0f0aa53f11a0d1ab08c76428b9de73db5b17c977Christian MaederinclusionMap :: Sign.Sign -> Sign.Sign -> Morphism
14a1af9d9909dc47dc7fee6b0170b7ac0aef85daChristian MaederinclusionMap s1 s2 = Morphism
14a1af9d9909dc47dc7fee6b0170b7ac0aef85daChristian Maeder { source = s1
2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder , target = s2
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder-- | creates a Morphism
14a1af9d9909dc47dc7fee6b0170b7ac0aef85daChristian MaedermkMorphism :: Sign.Sign -> Sign.Sign -> Map.Map Id Id -> Morphism
840b2a6f37ec58f3281da16fafbc4121462c856aChristian MaedermkMorphism s t p =
5ba383b1607c20c57e14324e72cee2c789436d5fChristian Maeder Morphism { source = s
0f0aa53f11a0d1ab08c76428b9de73db5b17c977Christian Maeder , propMap = p }
5ba383b1607c20c57e14324e72cee2c789436d5fChristian Maeder-- | sentence (text) translation along signature morphism
2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder-- here just the renaming of formulae
36c6cc568751e4235502cfee00ba7b597dae78dcChristian MaedermapSentence :: Morphism -> AS_BASIC.TEXT_MRS -> Result.Result AS_BASIC.TEXT_MRS
14a1af9d9909dc47dc7fee6b0170b7ac0aef85daChristian MaedermapSentence mor (t,mrs) = return (mapSentence_txt mor t, mrs)
14a1af9d9909dc47dc7fee6b0170b7ac0aef85daChristian MaedermapSentence_txt :: Morphism -> AS_BASIC.TEXT -> AS_BASIC.TEXT
2ac1742771a267119f1d839054b5e45d0a468085Christian MaedermapSentence_txt mor = mapSentenceH mor
2118d66b6aa3c90458925019c9b2fb986e2b2aabChristian Maeder-- propagates the translation to sentences
2118d66b6aa3c90458925019c9b2fb986e2b2aabChristian MaedermapSentenceH :: Morphism -> AS_BASIC.TEXT -> AS_BASIC.TEXT
2118d66b6aa3c90458925019c9b2fb986e2b2aabChristian MaedermapSentenceH mor txt = case txt of
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder AS_BASIC.Text phrs r -> AS_BASIC.Text (map (mapSentenceH_phr mor) phrs) r
35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder AS_BASIC.Named_text n t r -> AS_BASIC.Named_text n (mapSentenceH mor t) r
d48085f765fca838c1d972d2123601997174583dChristian Maeder-- propagates the translation to sentences
0f0aa53f11a0d1ab08c76428b9de73db5b17c977Christian MaedermapSentenceH_phr :: Morphism -> AS_BASIC.PHRASE -> AS_BASIC.PHRASE
0f0aa53f11a0d1ab08c76428b9de73db5b17c977Christian MaedermapSentenceH_phr mor phr = case phr of
d48085f765fca838c1d972d2123601997174583dChristian Maeder AS_BASIC.Module m -> AS_BASIC.Module $ mapSentenceH_mod mor m
d48085f765fca838c1d972d2123601997174583dChristian Maeder AS_BASIC.Sentence s -> AS_BASIC.Sentence $ mapSentenceH_sen mor s
0f0aa53f11a0d1ab08c76428b9de73db5b17c977Christian Maeder AS_BASIC.Comment_text c t r -> AS_BASIC.Comment_text c (mapSentenceH mor t) r
35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder-- propagates the translation to sentences
35597678f1c9da703de8d0b6b66ea63247ebe884Christian MaedermapSentenceH_mod :: Morphism -> AS_BASIC.MODULE -> AS_BASIC.MODULE
2ac1742771a267119f1d839054b5e45d0a468085Christian MaedermapSentenceH_mod mor m = case m of
35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder AS_BASIC.Mod n t rn -> AS_BASIC.Mod n (mapSentenceH mor t) rn
35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder AS_BASIC.Mod_ex n exs t rn -> AS_BASIC.Mod_ex n exs (mapSentenceH mor t) rn
2ac1742771a267119f1d839054b5e45d0a468085Christian MaedermapSentenceH_sen :: Morphism -> AS_BASIC.SENTENCE -> AS_BASIC.SENTENCE
35597678f1c9da703de8d0b6b66ea63247ebe884Christian MaedermapSentenceH_sen mor frm = case frm of
5ba383b1607c20c57e14324e72cee2c789436d5fChristian Maeder AS_BASIC.Quant_sent qs rn -> case qs of
5ba383b1607c20c57e14324e72cee2c789436d5fChristian Maeder AS_BASIC.Universal xs sen -> AS_BASIC.Quant_sent
0f0aa53f11a0d1ab08c76428b9de73db5b17c977Christian Maeder (AS_BASIC.Universal xs (mapSentenceH_sen mor sen)) rn -- fix
35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder AS_BASIC.Existential xs sen -> AS_BASIC.Quant_sent
2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder (AS_BASIC.Existential xs (mapSentenceH_sen mor sen)) rn -- fix
2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder AS_BASIC.Bool_sent bs rn -> case bs of
793945d4ac7c0f22760589c87af8e71427c76118Christian Maeder AS_BASIC.Conjunction sens -> AS_BASIC.Bool_sent
2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder (AS_BASIC.Conjunction (map (mapSentenceH_sen mor) sens)) rn
2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder AS_BASIC.Disjunction sens -> AS_BASIC.Bool_sent
d93bbbec133697cc79d59f9d7cc8e97458976c15Christian Maeder (AS_BASIC.Disjunction (map (mapSentenceH_sen mor) sens)) rn
35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder AS_BASIC.Negation sen -> AS_BASIC.Bool_sent
35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder (AS_BASIC.Negation (mapSentenceH_sen mor sen)) rn
2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder AS_BASIC.Implication s1 s2 -> AS_BASIC.Bool_sent
2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder (AS_BASIC.Implication (mapSentenceH_sen mor s1)
35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder (mapSentenceH_sen mor s2)) rn
81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder AS_BASIC.Biconditional s1 s2 -> AS_BASIC.Bool_sent
81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder (AS_BASIC.Biconditional (mapSentenceH_sen mor s1)
35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder (mapSentenceH_sen mor s2)) rn
d93bbbec133697cc79d59f9d7cc8e97458976c15Christian Maeder AS_BASIC.Atom_sent atom rn -> AS_BASIC.Atom_sent atom rn -- fix
35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder AS_BASIC.Comment_sent cm sen rn -> AS_BASIC.Comment_sent cm sen rn -- unused
2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder AS_BASIC.Irregular_sent sen rn -> AS_BASIC.Irregular_sent sen rn -- unused
2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder AS_BASIC.Predication predH -> AS_BASIC.Predication
975642b989852fc24119c59cf40bc1af653608ffChristian Maeder $ id2SimpleId $ applyMorphism mor $ Id.simpleIdToId predH
35597678f1c9da703de8d0b6b66ea63247ebe884Christian MaedermorphismUnion :: Morphism -> Morphism -> Result.Result Morphism
35597678f1c9da703de8d0b6b66ea63247ebe884Christian MaedermorphismUnion mor1 mor2 =
0f0aa53f11a0d1ab08c76428b9de73db5b17c977Christian Maeder let pmap1 = propMap mor1
0f0aa53f11a0d1ab08c76428b9de73db5b17c977Christian Maeder pmap2 = propMap mor2
d48085f765fca838c1d972d2123601997174583dChristian Maeder p1 = source mor1
d48085f765fca838c1d972d2123601997174583dChristian Maeder p2 = source mor2
0f0aa53f11a0d1ab08c76428b9de73db5b17c977Christian Maeder up1 = Set.difference (items p1) $ Map.keysSet pmap1
0f0aa53f11a0d1ab08c76428b9de73db5b17c977Christian Maeder up2 = Set.difference (items p2) $ Map.keysSet pmap2
0f0aa53f11a0d1ab08c76428b9de73db5b17c977Christian Maeder (pds, pmap) = foldr ( \ (i, j) (ds, m) -> case Map.lookup i m of
d93bbbec133697cc79d59f9d7cc8e97458976c15Christian Maeder Nothing -> (ds, Map.insert i j m)
c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian Maeder Just k -> if j == k then (ds, m) else
2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder ("incompatible mapping of prop " ++ showId i " to "
c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian Maeder ++ showId j " and " ++ showId k "")
2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder nullRange : ds, m)) ([], pmap1)
2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder (Map.toList pmap2 ++ map (\ a -> (a, a))
c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian Maeder in if null pds then return Morphism
c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian Maeder { source = unite p1 p2
c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian Maeder , target = unite (target mor1) $ target mor2
793945d4ac7c0f22760589c87af8e71427c76118Christian Maeder , propMap = pmap } else Result pds Nothing