1a38107941725211e7c3f051f7a8f5e12199f03acmaeder{-# LANGUAGE DeriveDataTypeable #-}
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian MaederDescription : Morphism of Common Logic
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian MaederCopyright : (c) Uni Bremen DFKI 2010
98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuLicense : GPLv2 or higher, see LICENSE.txt
a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen KuksaMaintainer : eugenk@informatik.uni-bremen.de
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian MaederStability : experimental
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian MaederPortability : non-portable (via Logic.Logic)
75067b1beba1380cde707c30e7fc050d86f6927fKarl LucMorphism of Common Logic
7b1111ca3b126f71cce47e60ce4b56e6f92422e9Karl Luc ( Morphism (..)
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder , pretty -- pretty printing
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder , idMor -- identity morphism
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder , isLegalMorphism -- check if morhpism is ok
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder , composeMor -- composition
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder , inclusionMap -- inclusion map
e036e115761fe7c09c210c337440a1864d794093Martha Rohte , mkMorphism -- create Morphism
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder , mapSentence -- map of sentences
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder , applyMap -- application function for maps
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder , applyMorphism -- application function for morphism
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder , morphismUnion
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maederimport qualified Data.Map as Map
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maederimport qualified Data.Set as Set
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maederimport qualified Common.Result as Result
7b1111ca3b126f71cce47e60ce4b56e6f92422e9Karl Luc-- maps of sets
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maederdata Morphism = Morphism
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder { source :: Sign
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder , target :: Sign
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder , propMap :: Map.Map Id Id
1a38107941725211e7c3f051f7a8f5e12199f03acmaeder } deriving (Eq, Ord, Show, Typeable)
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maederinstance Pretty Morphism where
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder pretty = printMorphism
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder-- | Constructs an id-morphism
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian MaederidMor :: Sign -> Morphism
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian MaederidMor a = inclusionMap a a
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder-- | Determines whether a morphism is valid
656f17ae9b7610ff2de1b6eedeeadea0c3bcdc8dChristian MaederisLegalMorphism :: Morphism -> Result ()
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian MaederisLegalMorphism pmor =
a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen Kuksa let psource = allItems $ source pmor
a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen Kuksa ptarget = allItems $ target pmor
7b1111ca3b126f71cce47e60ce4b56e6f92422e9Karl Luc pdom = Map.keysSet $ propMap pmor
7b1111ca3b126f71cce47e60ce4b56e6f92422e9Karl Luc pcodom = Set.map (applyMorphism pmor) psource
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder in unless (Set.isSubsetOf pcodom ptarget && Set.isSubsetOf pdom psource) $
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder fail "illegal CommonLogic morphism"
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder-- | Application funtion for morphisms
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian MaederapplyMorphism :: Morphism -> Id -> Id
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian MaederapplyMorphism mor idt = Map.findWithDefault idt idt $ propMap mor
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder-- | Application function for propMaps
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian MaederapplyMap :: Map.Map Id Id -> Id -> Id
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian MaederapplyMap pmap idt = Map.findWithDefault idt idt pmap
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder-- | Composition of morphisms in propositional Logic
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian MaedercomposeMor :: Morphism -> Morphism -> Result Morphism
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian MaedercomposeMor f g =
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder let fSource = source f
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder gTarget = target g
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder fMap = propMap f
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder gMap = propMap g
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder in return Morphism
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder { source = fSource
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder , target = gTarget
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder , propMap = if Map.null gMap then fMap else
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder Set.fold ( \ i -> let j = applyMap gMap (applyMap fMap i) in
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder if i == j then id else Map.insert i j)
a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen Kuksa Map.empty $ allItems fSource }
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder-- | Pretty printing for Morphisms
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian MaederprintMorphism :: Morphism -> Doc
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian MaederprintMorphism m = pretty (source m) <> text "-->" <> pretty (target m)
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder <> vcat (map ( \ (x, y) -> lparen <> pretty x <> text ","
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder <> pretty y <> rparen) $ Map.assocs $ propMap m)
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder-- | Inclusion map of a subsig into a supersig
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian MaederinclusionMap :: Sign.Sign -> Sign.Sign -> Morphism
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian MaederinclusionMap s1 s2 = Morphism
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder { source = s1
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder , target = s2
e9e5281899ddaec4778ad14c64800975377630ecChristian Maeder-- | creates a Morphism
e036e115761fe7c09c210c337440a1864d794093Martha RohtemkMorphism :: Sign.Sign -> Sign.Sign -> Map.Map Id Id -> Morphism
e9e5281899ddaec4778ad14c64800975377630ecChristian MaedermkMorphism s t p =
e9e5281899ddaec4778ad14c64800975377630ecChristian Maeder Morphism { source = s
e9e5281899ddaec4778ad14c64800975377630ecChristian Maeder , propMap = p }
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder{- | sentence (text) translation along signature morphism
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederhere just the renaming of formulae -}
a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen KuksamapSentence :: Morphism -> AS.TEXT_META -> Result.Result AS.TEXT_META
a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen KuksamapSentence mor tm =
a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen Kuksa return $ tm { getText = mapSen_txt mor $ getText tm }
2c10bceb28a74fc291959697e023f22a66753655Eugen Kuksa-- propagates the translation to sentences
a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen KuksamapSen_txt mor txt = case txt of
a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen Kuksa AS.Text phrs r -> AS.Text (map (mapSen_phr mor) phrs) r
a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen Kuksa AS.Named_text n t r -> AS.Named_text n (mapSen_txt mor t) r
2c10bceb28a74fc291959697e023f22a66753655Eugen Kuksa-- propagates the translation to sentences
a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen KuksamapSen_phr mor phr = case phr of
a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen Kuksa AS.Comment_text c t r -> AS.Comment_text c (mapSen_txt mor t) r
2c10bceb28a74fc291959697e023f22a66753655Eugen Kuksa-- propagates the translation to sentences
a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen KuksamapSen_mod mor m = case m of
a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen Kuksa AS.Mod_ex n exs t rn -> AS.Mod_ex n exs (mapSen_txt mor t) rn
a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen KuksamapSen_sen :: Morphism -> AS.SENTENCE -> AS.SENTENCE
a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen KuksamapSen_sen mor frm = case frm of
ea570f40967ef8bc16b76c54f9b867a8036cc750Soeren D. Schulze AS.Quant_sent q (map (mapSen_nos mor) vs) (mapSen_sen mor is) rn
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder AS.Junction j sens -> AS.Junction j (map (mapSen_sen mor) sens)
a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen Kuksa AS.Negation sen -> AS.Negation (mapSen_sen mor sen)
d2d5606ab65ddf48599bd044416de07a205095f2Soeren D. Schulze AS.BinOp op (mapSen_sen mor s1) (mapSen_sen mor s2)
a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen Kuksa AS.Atom_sent atom rn -> AS.Atom_sent (case atom of
a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen Kuksa AS.Equation t1 t2 -> AS.Equation (mapSen_trm mor t1) (mapSen_trm mor t2)
a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen Kuksa AS.Atom t tss -> AS.Atom (mapSen_trm mor t) (map (mapSen_trmSeq mor) tss)
a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen Kuksa AS.Comment_sent cm sen rn -> AS.Comment_sent cm (mapSen_sen mor sen) rn
a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen Kuksa AS.Irregular_sent sen rn -> AS.Irregular_sent (mapSen_sen mor sen) rn
a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen KuksamapSen_trm mor trm = case trm of
a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen Kuksa AS.Name_term n -> AS.Name_term (mapSen_tok mor n)
a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen Kuksa AS.Funct_term (mapSen_trm mor t) (map (mapSen_trmSeq mor) ts) rn
a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen Kuksa AS.Comment_term t c rn -> AS.Comment_term (mapSen_trm mor t) c rn
f03aa0b723e5545fddf7019e287368b9e208ca69Soeren D. Schulze AS.That_term s rn -> AS.That_term (mapSen_sen mor s) rn
a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen KuksamapSen_nos :: Morphism -> AS.NAME_OR_SEQMARK -> AS.NAME_OR_SEQMARK
a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen KuksamapSen_nos mor nos = case nos of
a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen KuksamapSen_trmSeq :: Morphism -> AS.TERM_SEQ -> AS.TERM_SEQ
a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen KuksamapSen_trmSeq mor ts = case ts of
a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen Kuksa AS.Seq_marks s -> AS.Seq_marks (mapSen_tok mor s)
a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen KuksamapSen_tok mor tok = Id.idToSimpleId $ applyMorphism mor $ Id.simpleIdToId tok
0fe5514fdf12b7559c1a470cf22d89737d55b0a0Eugen Kuksa-- | Union of two morphisms.
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian MaedermorphismUnion :: Morphism -> Morphism -> Result.Result Morphism
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian MaedermorphismUnion mor1 mor2 =
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder let pmap1 = propMap mor1
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder pmap2 = propMap mor2
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder p1 = source mor1
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder p2 = source mor2
a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen Kuksa up1 = Set.difference (allItems p1) $ Map.keysSet pmap1
a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen Kuksa up2 = Set.difference (allItems p2) $ Map.keysSet pmap2
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder (pds, pmap) = foldr ( \ (i, j) (ds, m) -> case Map.lookup i m of
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder Nothing -> (ds, Map.insert i j m)
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder Just k -> if j == k then (ds, m) else
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder ("incompatible mapping of prop " ++ showId i " to "
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder ++ showId j " and " ++ showId k "")
0fe5514fdf12b7559c1a470cf22d89737d55b0a0Eugen Kuksa nullRange : ds, m))
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder (Map.toList pmap2 ++ map (\ a -> (a, a))
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder in if null pds then return Morphism
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder { source = unite p1 p2
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder , target = unite (target mor1) $ target mor2
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder , propMap = pmap } else Result pds Nothing