Morphism.hs revision ea570f40967ef8bc16b76c54f9b867a8036cc750
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae BungiuModule : $Header$
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae BungiuDescription : Morphism of Common Logic
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae BungiuCopyright : (c) Uni Bremen DFKI 2010
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae BungiuLicense : GPLv2 or higher, see LICENSE.txt
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae BungiuMaintainer : eugenk@informatik.uni-bremen.de
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae BungiuStability : experimental
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae BungiuPortability : non-portable (via Logic.Logic)
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae BungiuMorphism of Common Logic
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu ( Morphism (..)
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu , pretty -- pretty printing
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu , idMor -- identity morphism
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu , isLegalMorphism -- check if morhpism is ok
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu , composeMor -- composition
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu , inclusionMap -- inclusion map
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu , mkMorphism -- create Morphism
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu , mapSentence -- map of sentences
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu , applyMap -- application function for maps
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu , applyMorphism -- application function for morphism
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu , morphismUnion
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiuimport qualified Data.Map as Map
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiuimport qualified Data.Set as Set
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiuimport qualified Common.Result as Result
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiuimport CommonLogic.AS_CommonLogic as AS
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiudata Morphism = Morphism
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu { source :: Sign
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu , target :: Sign
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu , propMap :: Map.Map Id Id
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu } deriving (Eq, Ord, Show)
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiuinstance Pretty Morphism where
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu pretty = printMorphism
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu-- | Constructs an id-morphism
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae BungiuidMor :: Sign -> Morphism
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae BungiuidMor a = inclusionMap a a
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu-- | Determines whether a morphism is valid
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae BungiuisLegalMorphism :: Morphism -> Result ()
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae BungiuisLegalMorphism pmor =
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu let psource = allItems $ source pmor
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu ptarget = allItems $ target pmor
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu pdom = Map.keysSet $ propMap pmor
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu pcodom = Set.map (applyMorphism pmor) psource
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu in if Set.isSubsetOf pcodom ptarget && Set.isSubsetOf pdom psource
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu then return () else fail "illegal CommonLogic morphism"
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu-- | Application funtion for morphisms
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae BungiuapplyMorphism :: Morphism -> Id -> Id
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae BungiuapplyMorphism mor idt = Map.findWithDefault idt idt $ propMap mor
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu-- | Application function for propMaps
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae BungiuapplyMap :: Map.Map Id Id -> Id -> Id
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae BungiuapplyMap pmap idt = Map.findWithDefault idt idt pmap
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu-- | Composition of morphisms in propositional Logic
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae BungiucomposeMor :: Morphism -> Morphism -> Result Morphism
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae BungiucomposeMor f g =
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu let fSource = source f
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu gTarget = target g
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu fMap = propMap f
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu gMap = propMap g
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu in return Morphism
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu { source = fSource
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu , target = gTarget
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu , propMap = if Map.null gMap then fMap else
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu Set.fold ( \ i -> let j = applyMap gMap (applyMap fMap i) in
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu if i == j then id else Map.insert i j)
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu Map.empty $ allItems fSource }
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu-- | Pretty printing for Morphisms
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae BungiuprintMorphism :: Morphism -> Doc
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae BungiuprintMorphism m = pretty (source m) <> text "-->" <> pretty (target m)
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu <> vcat (map ( \ (x, y) -> lparen <> pretty x <> text ","
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu <> pretty y <> rparen) $ Map.assocs $ propMap m)
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu-- | Inclusion map of a subsig into a supersig
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae BungiuinclusionMap :: Sign.Sign -> Sign.Sign -> Morphism
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae BungiuinclusionMap s1 s2 = Morphism
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu-- | creates a Morphism
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae BungiumkMorphism :: Sign.Sign -> Sign.Sign -> Map.Map Id Id -> Morphism
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae BungiumkMorphism s t p =
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu Morphism { source = s
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu , propMap = p }
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu-- | sentence (text) translation along signature morphism
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu-- here just the renaming of formulae
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae BungiumapSentence :: Morphism -> AS.TEXT_META -> Result.Result AS.TEXT_META
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae BungiumapSentence mor tm =
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu return $ tm { getText = mapSen_txt mor $ getText tm }
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu-- propagates the translation to sentences
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae BungiumapSen_txt :: Morphism -> AS.TEXT -> AS.TEXT
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae BungiumapSen_txt mor txt = case txt of
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu AS.Text phrs r -> AS.Text (map (mapSen_phr mor) phrs) r
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu AS.Named_text n t r -> AS.Named_text n (mapSen_txt mor t) r
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu-- propagates the translation to sentences
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae BungiumapSen_phr :: Morphism -> AS.PHRASE -> AS.PHRASE
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae BungiumapSen_phr mor phr = case phr of
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu AS.Module m -> AS.Module $ mapSen_mod mor m
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu AS.Sentence s -> AS.Sentence $ mapSen_sen mor s
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu AS.Comment_text c t r -> AS.Comment_text c (mapSen_txt mor t) r
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu-- propagates the translation to sentences
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae BungiumapSen_mod :: Morphism -> AS.MODULE -> AS.MODULE
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae BungiumapSen_mod mor m = case m of
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu AS.Mod n t rn -> AS.Mod n (mapSen_txt mor t) rn
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu AS.Mod_ex n exs t rn -> AS.Mod_ex n exs (mapSen_txt mor t) rn
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae BungiumapSen_sen :: Morphism -> AS.SENTENCE -> AS.SENTENCE
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae BungiumapSen_sen mor frm = case frm of
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu AS.Quant_sent q (map (mapSen_nos mor) vs) (mapSen_sen mor is) rn
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu AS.Bool_sent bs rn -> AS.Bool_sent (case bs of
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu AS.Junction j sens -> AS.Junction j (map (mapSen_sen mor) sens)
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu AS.Negation sen -> AS.Negation (mapSen_sen mor sen)
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu AS.BinOp op (mapSen_sen mor s1) (mapSen_sen mor s2)
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu AS.Atom_sent atom rn -> AS.Atom_sent (case atom of
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu AS.Equation t1 t2 -> AS.Equation (mapSen_trm mor t1) (mapSen_trm mor t2)
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu AS.Atom t tss -> AS.Atom (mapSen_trm mor t) (map (mapSen_trmSeq mor) tss)
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu AS.Comment_sent cm sen rn -> AS.Comment_sent cm (mapSen_sen mor sen) rn
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu AS.Irregular_sent sen rn -> AS.Irregular_sent (mapSen_sen mor sen) rn
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae BungiumapSen_trm :: Morphism -> AS.TERM -> AS.TERM
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae BungiumapSen_trm mor trm = case trm of
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu AS.Name_term n -> AS.Name_term (mapSen_tok mor n)
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu AS.Funct_term (mapSen_trm mor t) (map (mapSen_trmSeq mor) ts) rn
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu AS.Comment_term t c rn -> AS.Comment_term (mapSen_trm mor t) c rn
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu AS.That_term s rn -> AS.That_term (mapSen_sen mor s) rn
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae BungiumapSen_nos :: Morphism -> AS.NAME_OR_SEQMARK -> AS.NAME_OR_SEQMARK
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae BungiumapSen_nos mor nos = case nos of
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu AS.Name n -> AS.Name (mapSen_tok mor n)
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu AS.SeqMark s -> AS.SeqMark (mapSen_tok mor s)
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae BungiumapSen_trmSeq :: Morphism -> AS.TERM_SEQ -> AS.TERM_SEQ
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae BungiumapSen_trmSeq mor ts = case ts of
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu AS.Term_seq t -> AS.Term_seq (mapSen_trm mor t)
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu AS.Seq_marks s -> AS.Seq_marks (mapSen_tok mor s)
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae BungiumapSen_tok :: Morphism -> Id.Token -> Id.Token
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae BungiumapSen_tok mor tok = Id.idToSimpleId $ applyMorphism mor $ Id.simpleIdToId tok
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu-- | Union of two morphisms.
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae BungiumorphismUnion :: Morphism -> Morphism -> Result.Result Morphism
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae BungiumorphismUnion mor1 mor2 =
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu let pmap1 = propMap mor1
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu pmap2 = propMap mor2
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu p1 = source mor1
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu p2 = source mor2
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu up1 = Set.difference (allItems p1) $ Map.keysSet pmap1
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu up2 = Set.difference (allItems p2) $ Map.keysSet pmap2
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu (pds, pmap) = foldr ( \ (i, j) (ds, m) -> case Map.lookup i m of
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu Nothing -> (ds, Map.insert i j m)
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu Just k -> if j == k then (ds, m) else
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu ("incompatible mapping of prop " ++ showId i " to "
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu ++ showId j " and " ++ showId k "")
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu nullRange : ds, m))
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu (Map.toList pmap2 ++ map (\ a -> (a, a))
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu in if null pds then return Morphism
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu { source = unite p1 p2
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu , target = unite (target mor1) $ target mor2
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu , propMap = pmap } else Result pds Nothing